Z3 default tactic (#1527)

* Use scVectorReduced in reconstructArgTerm. * Add support for user-provided Z3 tactics. * Bump What4. * Bump What4. * Update src/SAWScript/Prover/What4.hs Co-authored-by: Ryan Scott <[email protected]> * Add test. * Fix documentation. Co-authored-by: Ryan Scott <[email protected]>
GaloisInc · Dec 2, 2021 · 6bb79b6 · 6bb79b6
1 parent a87ed23
commit 6bb79b6
Show file tree

Hide file tree

Showing 8 changed files with 64 additions and 20 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -14,6 +14,10 @@
   during the LLVM and X86 Crucible symbolic execution. This is used for
   path-sat checks, and sat checks when applying overrides.
 
+* New command `w4_unint_z3_using` like `w4_unint_z3`, but use the given Z3
+  tactic.
+
+
 # Version 0.9
 
 ## New Features

diff --git a/deps/what4 b/deps/what4
diff --git a/intTests/test0071_w4_unint_z3_using/test.saw b/intTests/test0071_w4_unint_z3_using/test.saw
@@ -0,0 +1,13 @@
+enable_experimental;
+
+let {{
+bvToInteger : [1024] -> Integer
+bvToInteger = toInteger
+bvFromInteger : Integer  -> [1024]
+bvFromInteger = fromInteger
+}};
+
+prove_print
+  (w4_unint_z3_using "qfnia" ["bvToInteger", "bvFromInteger"])
+  {{ \(x : [1024]) -> bvFromInteger ((if (bvToInteger x) <= (bvToInteger (x * x)) then 1 else (bvToInteger x)) * (bvToInteger x)) == bvFromInteger ((if (bvToInteger x) <= (bvToInteger (x * x)) then (bvToInteger x) else (bvToInteger x) * (bvToInteger x))) }};
+
diff --git a/intTests/test0071_w4_unint_z3_using/test.sh b/intTests/test0071_w4_unint_z3_using/test.sh
@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw
diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
@@ -1431,7 +1431,7 @@ reconstructArgTerm atrm sc ts =
              pure (x, ts1)
         ArgTermVector ty ats ->
           do (xs, ts1) <- parseList ats ts0
-             x <- scVector sc ty xs
+             x <- scVectorReduced sc ty xs
              return (x, ts1)
         ArgTermUnit ->
           do x <- scUnitValue sc

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
@@ -808,6 +808,9 @@ w4_unint_boolector = wrapW4Prover Prover.proveWhat4_boolector
 w4_unint_z3 :: [String] -> ProofScript ()
 w4_unint_z3 = wrapW4Prover Prover.proveWhat4_z3
 
+w4_unint_z3_using :: String -> [String] -> ProofScript ()
+w4_unint_z3_using tactic = wrapW4Prover (Prover.proveWhat4_z3_using tactic)
+
 w4_unint_cvc4 :: [String] -> ProofScript ()
 w4_unint_cvc4 = wrapW4Prover Prover.proveWhat4_cvc4
 

diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
@@ -1356,7 +1356,7 @@ primitives = Map.fromList
     (pureVal goal_eval)
     Current
     [ "Evaluate the proof goal to a first-order combination of primitives."
-    , "Leave the given names, as defined with 'define', as uninterpreted." ]
+    , "Leave the given names as uninterpreted." ]
 
   , prim "beta_reduce_goal"    "ProofScript ()"
     (pureVal beta_reduce_goal)
@@ -1495,21 +1495,21 @@ primitives = Map.fromList
     (pureVal proveUnintZ3)
     Current
     [ "Use the Z3 theorem prover to prove the current goal. Leave the"
-    , "given list of names, as defined with 'define', as uninterpreted."
+    , "given list of names as uninterpreted."
     ]
 
   , prim "unint_cvc4"            "[String] -> ProofScript ()"
     (pureVal proveUnintCVC4)
     Current
     [ "Use the CVC4 theorem prover to prove the current goal. Leave the"
-    , "given list of names, as defined with 'define', as uninterpreted."
+    , "given list of names as uninterpreted."
     ]
 
   , prim "unint_yices"           "[String] -> ProofScript ()"
     (pureVal proveUnintYices)
     Current
     [ "Use the Yices theorem prover to prove the current goal. Leave the"
-    , "given list of names, as defined with 'define', as uninterpreted."
+    , "given list of names as uninterpreted."
     ]
 
   , prim "sbv_boolector"       "ProofScript ()"
@@ -1541,21 +1541,21 @@ primitives = Map.fromList
     (pureVal proveUnintZ3)
     Current
     [ "Use the Z3 theorem prover to prove the current goal. Leave the"
-    , "given list of names, as defined with 'define', as uninterpreted."
+    , "given list of names as uninterpreted."
     ]
 
   , prim "sbv_unint_cvc4"        "[String] -> ProofScript ()"
     (pureVal proveUnintCVC4)
     Current
     [ "Use the CVC4 theorem prover to prove the current goal. Leave the"
-    , "given list of names, as defined with 'define', as uninterpreted."
+    , "given list of names as uninterpreted."
     ]
 
   , prim "sbv_unint_yices"       "[String] -> ProofScript ()"
     (pureVal proveUnintYices)
     Current
     [ "Use the Yices theorem prover to prove the current goal. Leave the"
-    , "given list of names, as defined with 'define', as uninterpreted."
+    , "given list of names as uninterpreted."
     ]
 
   , prim "offline_aig"         "String -> ProofScript ()"
@@ -1646,21 +1646,28 @@ primitives = Map.fromList
     (pureVal w4_unint_z3)
     Current
     [ "Prove the current goal using What4 (Z3 backend). Leave the"
-    , "given list of names, as defined with 'define', as uninterpreted."
+    , "given list of names as uninterpreted."
+    ]
+
+  , prim "w4_unint_z3_using" "String -> [String] -> ProofScript ()"
+    (pureVal w4_unint_z3_using)
+    Current
+    [ "Prove the current goal using What4 (Z3 backend) using the given"
+    , "Z3 tactic. Leave the given list of names as uninterpreted."
     ]
 
   , prim "w4_unint_yices"         "[String] -> ProofScript ()"
     (pureVal w4_unint_yices)
     Current
     [ "Prove the current goal using What4 (Yices backend). Leave the"
-    , "given list of names, as defined with 'define', as uninterpreted."
+    , "given list of names as uninterpreted."
     ]
 
   , prim "w4_unint_cvc4"         "[String] -> ProofScript ()"
     (pureVal w4_unint_cvc4)
     Current
     [ "Prove the current goal using What4 (CVC4 backend). Leave the"
-    , "given list of names, as defined with 'define', as uninterpreted."
+    , "given list of names as uninterpreted."
     ]
 
   , prim "w4_abc_aiger"        "ProofScript ()"
@@ -1691,24 +1698,21 @@ primitives = Map.fromList
     (pureVal offline_w4_unint_z3)
     Current
     [ "Write the current goal to the given file using What4 (Z3 backend) in"
-    ," SMT-Lib2 format. Leave the given list of names, as defined with"
-    , "'define', as uninterpreted."
+    ," SMT-Lib2 format. Leave the given list of names as uninterpreted."
     ]
 
   , prim "offline_w4_unint_yices" "[String] -> String -> ProofScript ()"
     (pureVal offline_w4_unint_yices)
     Current
     [ "Write the current goal to the given file using What4 (Yices backend) in"
-    ," SMT-Lib2 format. Leave the given list of names, as defined with"
-    , "'define', as uninterpreted."
+    ," SMT-Lib2 format. Leave the given list of names as uninterpreted."
     ]
 
   , prim "offline_w4_unint_cvc4"  "[String] -> String -> ProofScript ()"
     (pureVal offline_w4_unint_cvc4)
     Current
     [ "Write the current goal to the given file using What4 (CVC4 backend) in"
-    ," SMT-Lib2 format. Leave the given list of names, as defined with"
-    , "'define', as uninterpreted."
+    ," SMT-Lib2 format. Leave the given list of names as uninterpreted."
     ]
 
   , prim "split_goal"          "ProofScript ()"

diff --git a/src/SAWScript/Prover/What4.hs b/src/SAWScript/Prover/What4.hs
@@ -10,6 +10,7 @@ module SAWScript.Prover.What4 where
 import           Control.Lens ((^.))
 import           Data.Set (Set)
 import qualified Data.Map as Map
+import qualified Data.Text as Text
 import           System.IO
 
 import Verifier.SAW.SharedTerm
@@ -88,7 +89,7 @@ proveWhat4_sym ::
 proveWhat4_sym solver un hashConsing t =
   getSharedContext >>= \sc -> io $
   do sym <- setupWhat4_sym hashConsing
-     proveWhat4_solver solver sym un sc t
+     proveWhat4_solver solver sym un sc t (return ())
 
 proveExportWhat4_sym ::
   SolverAdapter St ->
@@ -125,6 +126,20 @@ proveWhat4_stp       = proveWhat4_sym stpAdapter
 proveWhat4_yices     = proveWhat4_sym yicesAdapter
 proveWhat4_abc       = proveWhat4_sym externalABCAdapter
 
+proveWhat4_z3_using ::
+  String        {- ^ Solver tactic -} ->
+  Set VarIndex  {- ^ Uninterpreted functions -} ->
+  Bool          {- ^ Hash-consing of What4 terms -}->
+  Prop          {- ^ A proposition to be proved -} ->
+  TopLevel (Maybe CEX, SolverStats)
+proveWhat4_z3_using tactic un hashConsing t =
+  getSharedContext >>= \sc -> io $
+  do sym <- setupWhat4_sym hashConsing
+     proveWhat4_solver z3Adapter sym un sc t $
+       do z3TacticSetting <- getOptionSetting z3Tactic $ getConfiguration sym
+          _ <- setOpt z3TacticSetting $ Text.pack tactic
+          return ()
+
 proveExportWhat4_z3, proveExportWhat4_boolector, proveExportWhat4_cvc4,
   proveExportWhat4_dreal, proveExportWhat4_stp, proveExportWhat4_yices ::
   Set VarIndex  {- ^ Uninterpreted functions -} ->
@@ -176,11 +191,13 @@ proveWhat4_solver :: forall st t ff.
   Set VarIndex       {- ^ Uninterpreted functions -} ->
   SharedContext      {- ^ Context for working with terms -} ->
   Prop               {- ^ A proposition to be proved/checked. -} ->
+  IO ()              {- ^ Extra setup actions -} ->
   IO (Maybe CEX, SolverStats)
   -- ^ (example/counter-example, solver statistics)
-proveWhat4_solver solver sym unintSet sc goal =
+proveWhat4_solver solver sym unintSet sc goal extraSetup =
   do
      (argNames, bvs, lit, stats) <- setupWhat4_solver solver sym unintSet sc goal
+     extraSetup
 
      -- log to stdout
      let logger _ str = putStrLn str
+77 −32		.github/workflows/test.yml
+20 −0		what4/src/What4/Expr/Builder.hs
+2 −0		what4/src/What4/Solver.hs
+15 −1		what4/src/What4/Solver/Z3.hs