crucible-cli: Use new goal-proving helpers

GaloisInc · Jun 20, 2024 · 672f0a0 · 672f0a0
1 parent b37a9fa
commit 672f0a0
Showing 1 changed file with 9 additions and 12 deletions.
diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs
@@ -20,7 +20,6 @@ module Lang.Crucible.CLI
   , execCommand
   ) where
 
-import Control.Lens (view)
 import Control.Monad
 
 import Data.Foldable
@@ -50,18 +49,19 @@ import Lang.Crucible.Syntax.SExpr
 
 import Lang.Crucible.Analysis.Postdom
 import Lang.Crucible.Backend
+import Lang.Crucible.Backend.Prove (ProofResult(..), proveProofGoal)
 import Lang.Crucible.Backend.Simple
 import Lang.Crucible.FunctionHandle
 import Lang.Crucible.Simulator
 import Lang.Crucible.Simulator.Profiling
 
 import What4.Config
-import What4.Interface (getConfiguration,notPred)
+import What4.Interface (getConfiguration)
 import What4.Expr (ExprBuilder, newExprBuilder, EmptyExprBuilderState(..))
 import What4.FunctionName
 import What4.ProgramLoc
-import What4.SatResult
-import What4.Solver (defaultLogData, runZ3InOverride, z3Options)
+import What4.Solver (defaultLogData)
+import What4.Solver.Z3 (z3Adapter, z3Options)
 
 -- | Allows users to hook into the various stages of 'simulateProgram'.
 data SimulateProgramHooks ext = SimulateProgramHooks
@@ -184,14 +184,11 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks =
                            do hPutStrLn outh "==== Proof obligations ===="
                               forM_ (goalsToList gs) (\g ->
                                 do hPrint outh =<< ppProofObligation sym g
-                                   neggoal <- notPred sym (view labeledPred (proofGoal g))
-                                   asms <- assumptionsPred sym (proofAssumptions g)
-                                   let bs = [neggoal, asms]
-                                   runZ3InOverride sym defaultLogData bs (\case
-                                     Sat _   -> hPutStrLn outh "COUNTEREXAMPLE"
-                                     Unsat _ -> hPutStrLn outh "PROVED"
-                                     Unknown -> hPutStrLn outh "UNKNOWN"
-                                     )
+                                   proveProofGoal sym defaultLogData z3Adapter g $
+                                     \case
+                                       Proved {} -> hPutStrLn outh "PROVED"
+                                       Disproved {} -> hPutStrLn outh "COUNTEREXAMPLE"
+                                       Unknown {} -> hPutStrLn outh "UNKNOWN"
                                 )
 
                   _ -> hPutStrLn outh "No suitable main function found"