Adapt to changes in GaloisInc/what4#226

GaloisInc/what4#226 adds some additional methods to `SMTWriter` that `language-sally` must implement.
GaloisInc · Mar 13, 2023 · 24d53a9 · 24d53a9
1 parent a217a9f
commit 24d53a9
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 2 deletions.
diff --git a/dependencies/what4 b/dependencies/what4
diff --git a/language-sally.cabal b/language-sally.cabal
@@ -27,7 +27,7 @@ common dependencies
   build-depends:
     , base                     >=4.8   && <4.17
     , parameterized-utils      >=2.0   && <2.2
-    , what4                    >=1.3
+    , what4                    >=1.4
     , what4-transition-system  >=0.0.3
 
 library

diff --git a/src/Language/Sally/Writer.hs b/src/Language/Sally/Writer.hs
@@ -257,6 +257,11 @@ instance SMTLib2Tweaks a => SMTWriter (SallyWriter a) where
     let resolveArg (var, Some tp) = (var, asSMT2Type @a tp)
      in SMT2.defineFun f (resolveArg <$> args) (asSMT2Type @a return_type) <$> e
 
+  synthFunCommand _proxy f args ret_tp =
+    pure $ SMT2.synthFun f (map (\(var, Some tp) -> (var, asSMT2Type @a tp)) args) (asSMT2Type @a ret_tp)
+  declareVarCommand _proxy v tp = pure $ SMT2.declareVar v (asSMT2Type @a tp)
+  constraintCommand _proxy e = SMT2.constraint <$> e
+
   stringTerm bs = pure $ smtlib2StringTerm @a bs
   stringLength x = smtlib2StringLength @a <$> x
   stringAppend xs = smtlib2StringAppend @a <$> sequence xs
+1 −0		.github/workflows/gen_matrix.pl
+9 −4		.github/workflows/test.yml
+1 −1		dependencies/aig
+1 −1		what4-abc/what4-abc.cabal
+1 −1		what4-blt/what4-blt.cabal
+2 −2		what4-transition-system/what4-transition-system.cabal
+27 −5		what4/CHANGES.md
+1 −1		what4/LICENSE
+6 −0		what4/README.md
+2 −0		what4/src/What4/Expr/App.hs
+54 −13		what4/src/What4/Expr/Builder.hs
+2 −3		what4/src/What4/Expr/VarIdentification.hs
+56 −2		what4/src/What4/Interface.hs
+398 −16		what4/src/What4/Protocol/SMTLib2.hs
+5 −1		what4/src/What4/Protocol/SMTLib2/Response.hs
+34 −1		what4/src/What4/Protocol/SMTLib2/Syntax.hs
+90 −0		what4/src/What4/Protocol/SMTWriter.hs
+1 −0		what4/src/What4/Protocol/VerilogWriter.hs
+184 −0		what4/src/What4/Serialize/FastSExpr.hs
+436 −0		what4/src/What4/Serialize/Log.hs
+162 −0		what4/src/What4/Serialize/Normalize.hs
+1,070 −0		what4/src/What4/Serialize/Parser.hs
+779 −0		what4/src/What4/Serialize/Printer.hs
+259 −0		what4/src/What4/Serialize/SETokens.hs
+134 −0		what4/src/What4/Solver/CVC5.hs
+4 −0		what4/src/What4/Solver/Yices.hs
+95 −3		what4/src/What4/Solver/Z3.hs
+1 −0		what4/src/What4/Utils/AbstractDomains.hs
+1 −0		what4/src/What4/Utils/OnlyIntRepr.hs
+127 −0		what4/src/What4/Utils/Serialize.hs
+153 −0		what4/test/InvariantSynthesis.hs
+1 −0		what4/test/OnlineSolverTest.hs
+58 −0		what4/test/SerializeTestUtils.hs
+20 −0		what4/test/SerializeTests.hs
+1 −1		what4/test/SolverParserTest.hs
+242 −0		what4/test/SymFnTests.hs
+58 −5		what4/what4.cabal