Implement abduction-related methods in what4's SMTWriter class

This bumps the `what4` submodule to bring in the changes from GaloisInc/what4#213. This requires implementing some new methods that were added to the `SMTWriter` class, which proves straightforward.
GaloisInc · Oct 13, 2022 · 80d3080 · 80d3080
1 parent 3a67165
commit 80d3080
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.16
     , parameterized-utils      >=2.0   && <2.2
-    , what4                    >=1.2
+    , what4                    >=1.3
     , what4-transition-system  >=0.0.3
 
 library

diff --git a/src/Language/Sally/Writer.hs b/src/Language/Sally/Writer.hs
@@ -230,6 +230,8 @@ instance SMTLib2Tweaks a => SMTWriter (SallyWriter a) where
 
   pushCommand _ = pure $ SMT2.push 1
   popCommand _ = pure $ SMT2.pop 1
+  push2Command _ = pure $ SMT2.push 2
+  pop2Command _ = pure $ SMT2.pop 2
   resetCommand _ = pure SMT2.resetAssertions
 
   checkCommands _ = [pure SMT2.checkSat]
@@ -238,6 +240,9 @@ instance SMTLib2Tweaks a => SMTWriter (SallyWriter a) where
 
   getUnsatAssumptionsCommand _ = pure SMT2.getUnsatAssumptions
   getUnsatCoreCommand _ = pure SMT2.getUnsatCore
+  getAbductCommand _ nm e = SMT2.getAbduct nm <$> e
+  getAbductNextCommand _ = pure SMT2.getAbductNext
+
   setOptCommand _ = (pure <$>) <$> SMT2.setOption
 
   declareCommand _proxy v argTypes retType =
+2 −4		.github/workflows/gen_matrix.pl
+5 −5		README.md
+2 −0		what4/CHANGES.md
+1 −1		what4/README.md
+32 −4		what4/src/What4/Interface.hs
+6 −0		what4/src/What4/ProblemFeatures.hs
+47 −0		what4/src/What4/Protocol/Online.hs
+6 −0		what4/src/What4/Protocol/SExp.hs
+54 −0		what4/src/What4/Protocol/SMTLib2.hs
+1 −1		what4/src/What4/Protocol/SMTLib2/Parse.hs
+12 −2		what4/src/What4/Protocol/SMTLib2/Syntax.hs
+20 −2		what4/src/What4/Protocol/SMTWriter.hs
+6 −0		what4/src/What4/Solver/CVC5.hs
+11 −0		what4/src/What4/Solver/Yices.hs
+155 −0		what4/test/Abduct.hs
+58 −0		what4/test/ExprsTest.hs
+13 −0		what4/what4.cabal