Merge pull request #58 from bruderj15/develop

Develop

CHANGELOG.md

@@ -6,6 +6,24 @@ file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [PVP versioning](https://pvp.haskell.org/).
 
+## v2.0.0 _(2024-07-23)_
+
+### Added
+- Arithmetic functions: `isIntSort`, `toIntSort` & `toRealSort`
+- Asserting maybe-formulas: `assertMaybe :: MonadSMT s m => Maybe (Expr BoolSort) -> m ()`
+- Logical equivalence `(<==>)` & reverse logical implication `(<==)`
+- Solvers: OpenSMT, OptiMathSAT
+- Iterative refinement optimizations utilizing incremental stack
+- Custom solver options via `Custom String String :: SMTOption`
+- Optimization Modulo Theories (OMT) / MaxSMT support with: `minimize`, `maximize` & `assertSoft`
+
+### Changed
+- *(breaking change)* The functions `solver` and `debug` which create `Solver`s from `ProcessSolver`s are polymorph in the state `s` now.
+This requires you to annotate the mentioned functions with the targetted state.
+These are `SMT` and `OMT`.
+For example, `solverWith (solver cvc5) $ do ...` becomes `solverWith (solver @SMT cvc5) $ do ...`.
+- Prefix `xor` now has an `infix 4`
+
 ## v1.3.1 _(2024-07-12)_
 
 ### Added

README.md

@@ -41,7 +41,7 @@ instance Variable a => Variable (V3 a)
 
 main :: IO ()
 main = do
-  res <- solveWith (solver cvc5) $ do
+  res <- solveWith (solver @SMT cvc5) $ do
     setLogic "QF_NRA"
 
     u :: V3 (Expr RealSort) <- variable
@@ -57,7 +57,6 @@ May print: `(Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))`
 
 ## Features
 
-### Supported
 - [x] SMTLib2-Sorts in the Haskell-Type
   ```haskell
     data SMTSort = BoolSort | IntSort | RealSort | BvSort Nat | ArraySort SMTSort SMTSort
@@ -72,7 +71,7 @@ May print: `(Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))`
   ```
 - [x] Pure API with Expression-instances for Num, Floating, Bounded, ...
   ```haskell
-    solveWith (solver yices) $ do
+    solveWith (solver @SMT yices) $ do
       setLogic "QF_BV"
       x <- var @(BvSort 16)
       y <- var
@@ -81,12 +80,12 @@ May print: `(Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))`
   ```
 - [x] Add your own solvers via the [Solver type](https://github.com/bruderj15/Hasmtlib/blob/master/src/Language/Hasmtlib/Type/Solution.hs)
   ```haskell
-    -- | Function that turns a state (SMT) into a result and a solution
+    -- | Function that turns a state (usually SMT or OMT) into a result and a solution
     type Solver s m = s -> m (Result, Solution)
   ```
-- [x] Solvers via external processes: CVC5, Z3, Yices2-SMT & MathSAT
+- [x] Solvers via external processes: CVC5, Z3, Yices2-SMT, MathSAT, OptiMathSAT & OpenSMT
   ```haskell
-    (result, solution) <- solveWith (solver mathsat) $ do
+    (result, solution) <- solveWith (solver @SMT mathsat) $ do
       setLogic "QF_LIA"
       assert $ ...
   ```
@@ -109,7 +108,7 @@ May print: `(Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))`
   ```
 - [x] Pure quantifiers `for_all` and `exists`
   ```haskell
-    solveWith (solver z3) $ do
+    solveWith (solver @SMT z3) $ do
       setLogic "LIA"
       z <- var @IntSort
       assert $ z === 0
@@ -119,11 +118,18 @@ May print: `(Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))`
               x + y === z
       return z
   ```
+- [x] Optimization Modulo Theories (OMT) / MaxSMT
+  ```haskell
+    res <- solveWith (solver @OMT z3) $ do
+      setLogic "QF_LIA"
+      x <- var @IntSort
 
-### Coming
-- [ ] Observable sharing & access to the expression-tree (useful for rewriting, ...)
-- [ ] (Maybe) signed BitVec with corresponding encoding on the type-level (unsigned, ones-complement, twos-complement)
-- [ ] ...
+      assert $ x >? -2
+      assertSoftWeighted (x >? -1) 5.0
+      minimize x
+
+      return x
+  ```
 
 ## Examples
 There are some examples in [here](https://github.com/bruderj15/Hasmtlib/tree/master/src/Language/Hasmtlib/Example).

hasmtlib.cabal

@@ -1,7 +1,7 @@
 cabal-version:         3.0
 
 name:                  hasmtlib
-version:               1.3.1
+version:               2.0.0
 synopsis:              A monad for interfacing with external SMT solvers
 description:           Hasmtlib is a library for generating SMTLib2-problems using a monad.
   It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.
@@ -40,12 +40,15 @@ library
                      , Language.Hasmtlib.Solver.Common
                      , Language.Hasmtlib.Solver.CVC5
                      , Language.Hasmtlib.Solver.MathSAT
+                     , Language.Hasmtlib.Solver.OpenSMT
                      , Language.Hasmtlib.Solver.Yices
                      , Language.Hasmtlib.Solver.Z3
                      , Language.Hasmtlib.Type.Expr
                      , Language.Hasmtlib.Type.MonadSMT
                      , Language.Hasmtlib.Type.SMT
+                     , Language.Hasmtlib.Type.OMT
                      , Language.Hasmtlib.Type.Pipe
+                     , Language.Hasmtlib.Type.SMTSort
                      , Language.Hasmtlib.Type.Solution
                      , Language.Hasmtlib.Type.Solver
                      , Language.Hasmtlib.Type.Option

src/Language/Hasmtlib.hs

@@ -2,10 +2,12 @@ module Language.Hasmtlib
   (
     module Language.Hasmtlib.Type.MonadSMT
   , module Language.Hasmtlib.Type.SMT
+  , module Language.Hasmtlib.Type.OMT
   , module Language.Hasmtlib.Type.Pipe
   , module Language.Hasmtlib.Type.Expr
   , module Language.Hasmtlib.Type.Solver
   , module Language.Hasmtlib.Type.Option
+  , module Language.Hasmtlib.Type.SMTSort
   , module Language.Hasmtlib.Type.Solution
   , module Language.Hasmtlib.Type.ArrayMap
   , module Language.Hasmtlib.Integraled
@@ -20,16 +22,19 @@ module Language.Hasmtlib
   , module Language.Hasmtlib.Solver.CVC5
   , module Language.Hasmtlib.Solver.Z3
   , module Language.Hasmtlib.Solver.Yices
+  , module Language.Hasmtlib.Solver.OpenSMT
   , module Language.Hasmtlib.Solver.MathSAT
   )
   where
 
 import Language.Hasmtlib.Type.MonadSMT
 import Language.Hasmtlib.Type.SMT
+import Language.Hasmtlib.Type.OMT
 import Language.Hasmtlib.Type.Pipe
 import Language.Hasmtlib.Type.Expr
 import Language.Hasmtlib.Type.Solver
 import Language.Hasmtlib.Type.Option
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
 import Language.Hasmtlib.Integraled
@@ -44,4 +49,5 @@ import Language.Hasmtlib.Solver.Common
 import Language.Hasmtlib.Solver.CVC5
 import Language.Hasmtlib.Solver.Z3
 import Language.Hasmtlib.Solver.Yices
+import Language.Hasmtlib.Solver.OpenSMT
 import Language.Hasmtlib.Solver.MathSAT

src/Language/Hasmtlib/Boolean.hs

@@ -35,12 +35,25 @@ class Boolean b where
   (==>) :: b -> b -> b
   x ==> y = not x || y
 
+  -- | Logical implication with arrow reversed.
+  --
+  -- @
+  -- forall x y. (x ==> y) === (y <== x)
+  -- @
+  (<==) :: b -> b -> b
+  y <== x = not x || y
+
+  -- | Logical equivalence.
+  (<==>) :: b -> b -> b
+  x <==> y = (x ==> y) && (y ==> x)
+
   -- | Logical negation
   not :: b -> b
 
   -- | Exclusive-or
   xor :: b -> b -> b
 
+  infix 4 `xor`
   infixr 3 &&
   infixr 2 ||
   infixr 0 ==>

src/Language/Hasmtlib/Codec.hs

@@ -10,6 +10,7 @@ import Language.Hasmtlib.Internal.Bitvec
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Boolean
 import Data.Kind
 import Data.Coerce

src/Language/Hasmtlib/Counting.hs

@@ -3,6 +3,7 @@ module Language.Hasmtlib.Counting where
 import Prelude hiding (not, (&&), (||), or)
 import Language.Hasmtlib.Internal.Expr.Num ()
 import Language.Hasmtlib.Internal.Expr
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Equatable
 import Language.Hasmtlib.Orderable
 import Language.Hasmtlib.Iteable

src/Language/Hasmtlib/Equatable.hs

@@ -6,6 +6,7 @@ module Language.Hasmtlib.Equatable where
 
 import Prelude hiding (not, (&&))
 import Language.Hasmtlib.Internal.Expr
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Boolean
 import Data.Int
 import Data.Word

src/Language/Hasmtlib/Example/Arith.hs

@@ -5,7 +5,7 @@ import Language.Hasmtlib
 
 main :: IO ()
 main = do
-  res <- solveWith (solver cvc5) $ do
+  res <- solveWith (solver @SMT cvc5) $ do
     setLogic "QF_LIA"
 
     x <- var @IntSort
@@ -14,7 +14,7 @@ main = do
     assert $ y >? 0 && x /== y
     assert $ x `mod` 42 === y
     assert $ y + x + 1 >=? x + y
-    
+
     return (x,y)
 
   print res

src/Language/Hasmtlib/Example/ArithFun.hs

@@ -0,0 +1,20 @@
+module Language.Hasmtlib.Example.ArithFun where
+
+import Prelude hiding (mod, (&&))
+import Language.Hasmtlib
+import Control.Monad
+
+main :: IO ()
+main = do
+  res <- solveWith (solver @SMT cvc5) $ do
+    setLogic "QF_LIRA"
+
+    xs <- replicateM 10 $ var @RealSort
+
+    forM_ xs $ \x -> assert $ x >=? 0 && x <? fromIntegral (length xs)
+    forM_ xs $ assert . isIntSort
+    assert $ distinct xs
+
+    return xs
+
+  print res

src/Language/Hasmtlib/Example/Array.hs

@@ -4,7 +4,7 @@ import Language.Hasmtlib
 
 main :: IO ()
 main = do
-  res <- solveWith (solver cvc5) $ do
+  res <- solveWith (solver @SMT cvc5) $ do
     setLogic "QF_AUFLIA"
 
     x <- var @(ArraySort IntSort BoolSort)

src/Language/Hasmtlib/Example/Bitvector.hs

@@ -4,7 +4,7 @@ import Language.Hasmtlib
 
 main :: IO ()
 main = do
-  res <- solveWith (debug yices) $ do
+  res <- solveWith (debug @SMT yices) $ do
     setLogic "QF_BV"
 
     xbv8 <- variable

src/Language/Hasmtlib/Example/Codec.hs

@@ -9,17 +9,17 @@ instance Applicative Foo where
   pure x = Foo x x
   (Foo f g) <*> (Foo x y) = Foo (f x) (g y)
 
-instance Equatable a => Equatable (Foo a) 
+instance Equatable a => Equatable (Foo a)
 -- Leverage Functor, Foldable, Traversable and Applicative and get default instances
 instance Codec a => Codec (Foo a)
 instance Variable a => Variable (Foo a)
 
 main :: IO ()
 main = do
-  res <- solveWith (solver z3) $ do
+  res <- solveWith (solver @SMT z3) $ do
     setLogic "ALL"
 
--- These do all the same:    
+-- These do all the same:
     let (c1,c2) :: (Expr IntSort, Expr RealSort) = (5, 10)
 --  let (c1,c2) :: (Expr IntSort, Expr RealSort) = encode (5, 10)
 --  let (c1,c2) :: (Expr IntSort, Expr RealSort) = (constant 5, constant 10)

src/Language/Hasmtlib/Example/Counting.hs

@@ -5,7 +5,7 @@ import Control.Monad
 
 main :: IO ()
 main = do
-  res <- solveWith (solver cvc5) $ do
+  res <- solveWith (solver @SMT cvc5) $ do
     setLogic "QF_LIA"
 
     xs <- replicateM 10 $ var @BoolSort
@@ -14,7 +14,7 @@ main = do
     assert $ atMost  (2 :: Expr IntSort) xs
     assert $ atLeast @IntSort 1 xs
 
-    assert $ count @IntSort xs === 1 -- eqivalent to: exactly 1
+    assert $ count @IntSort xs === 1 -- equivalent to: exactly 1
 
     return xs
 

src/Language/Hasmtlib/Example/IncrementalOptimization.hs

@@ -0,0 +1,23 @@
+module Language.Hasmtlib.Example.IncrementalOptimization where
+
+import Language.Hasmtlib
+import Control.Monad.IO.Class
+
+main :: IO ()
+main = do
+  iSolver <- interactiveSolver z3
+  interactiveWith iSolver $ do
+    setOption $ ProduceModels True
+    setLogic "QF_LIA"
+
+    x <- var @IntSort
+
+    assert $ x >? -2
+    assertSoftWeighted (x >? -1) 5.0
+
+    minimize x
+
+    (_, sol) <- solve
+    liftIO $ print $ decode sol x
+
+    return ()

src/Language/Hasmtlib/Example/McCarthyArrayAxioms.hs

@@ -6,15 +6,15 @@ import Language.Hasmtlib
 
 main :: IO ()
 main = do
-  res <- solveWith (solver cvc5) $ do
+  res <- solveWith (solver @SMT cvc5) $ do
     setLogic "AUFLIRA"
 
     assert $
       for_all @(ArraySort RealSort RealSort) \arr ->
          for_all \i ->
             for_all \x ->
-               select (store arr i x) i === x 
-    
+               select (store arr i x) i === x
+
     assert $
       for_all @(ArraySort IntSort BoolSort) \arr ->
          for_all \i ->

src/Language/Hasmtlib/Example/Monad.hs

@@ -5,13 +5,13 @@ import Control.Monad
 
 main :: IO ()
 main = do
-  res <- solveWith (solver cvc5) $ do
+  res <- solveWith (solver @SMT cvc5) $ do
     setLogic "QF_LIA"
 
     xs <- replicateM 100 $ var @IntSort
 
     forM_ (zip xs [1 :: Integer .. ]) $ \(x, i) -> assert $ x === fromInteger i
-  
+
     return xs
 
   case res of

src/Language/Hasmtlib/Example/OMTOptimization.hs

@@ -0,0 +1,19 @@
+module Language.Hasmtlib.Example.IncrementalOptimization where
+
+import Language.Hasmtlib
+
+main :: IO ()
+main = do
+  res <- solveWith (solver @OMT z3) $ do
+    setLogic "QF_LIA"
+
+    x <- var @IntSort
+
+    assert $ x >? -2
+    assertSoftWeighted (x >? -1) 5.0
+
+    minimize x
+
+    return x
+
+  print res