From 2aeeef283fd322b94754ca3f24d201c8bb9c7310 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 3 Mar 2021 17:34:57 -0800 Subject: [PATCH] More work on making proof and solver conventions more uniform. Use the SATQuery type for the "offline" proof exporters, and a variety of other tweaks. --- src/SAWScript/Builtins.hs | 45 ++++++--- src/SAWScript/Crucible/JVM/Builtins.hs | 2 +- src/SAWScript/Crucible/LLVM/Builtins.hs | 4 +- src/SAWScript/Proof.hs | 108 ++++++++++++-------- src/SAWScript/Prover/Exporter.hs | 127 +++++++++++------------- src/SAWScript/Prover/MRSolver.hs | 2 +- src/SAWScript/X86.hs | 2 +- 7 files changed, 160 insertions(+), 130 deletions(-) diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 21ea694cf6..60e691b975 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -64,6 +64,7 @@ import Verifier.SAW.FiniteValue , FirstOrderValue(..), asFiniteType , toFirstOrderValue, scFirstOrderValue ) +import Verifier.SAW.SATQuery import Verifier.SAW.SCTypeCheck hiding (TypedTerm) import qualified Verifier.SAW.SCTypeCheck as TC (TypedTerm(..)) import Verifier.SAW.SharedTerm @@ -780,47 +781,60 @@ offline_w4_unint_yices :: [String] -> String -> ProofScript SV.SatResult offline_w4_unint_yices unints path = wrapW4ProveExporter Prover.proveExportWhat4_yices unints path ".smt2" -proveWithExporter :: +proveWithSATExporter :: + (SharedContext -> FilePath -> SATQuery -> TopLevel ()) -> + Set VarIndex -> + String -> + String -> + ProofScript SV.SatResult +proveWithSATExporter exporter unintSet path ext = + withFirstGoal $ tacticSolve $ \g -> + do let file = path ++ "." ++ goalType g ++ show (goalNum g) ++ ext + stats <- Prover.proveWithSATExporter exporter unintSet file (goalProp g) + return (SV.Unsat stats, stats, Just (SolverEvidence stats (goalProp g))) + +proveWithPropExporter :: (SharedContext -> FilePath -> Prop -> TopLevel ()) -> String -> String -> ProofScript SV.SatResult -proveWithExporter exporter path ext = +proveWithPropExporter exporter path ext = withFirstGoal $ tacticSolve $ \g -> do let file = path ++ "." ++ goalType g ++ show (goalNum g) ++ ext - stats <- Prover.proveWithExporter exporter file (goalProp g) + stats <- Prover.proveWithPropExporter exporter file (goalProp g) return (SV.Unsat stats, stats, Just (SolverEvidence stats (goalProp g))) + offline_aig :: FilePath -> ProofScript SV.SatResult offline_aig path = do SV.AIGProxy proxy <- lift $ SV.getProxy - proveWithExporter (Prover.adaptExporter (Prover.writeAIG proxy)) path ".aig" + proveWithSATExporter (Prover.writeAIG_SAT proxy) mempty path ".aig" offline_cnf :: FilePath -> ProofScript SV.SatResult offline_cnf path = do SV.AIGProxy proxy <- lift $ SV.getProxy - proveWithExporter (Prover.adaptExporter (Prover.writeCNF proxy)) path ".cnf" + proveWithSATExporter (Prover.writeCNF proxy) mempty path ".cnf" offline_coq :: FilePath -> ProofScript SV.SatResult -offline_coq path = proveWithExporter (const (Prover.writeCoqProp "goal" [] [])) path ".v" +offline_coq path = proveWithPropExporter (const (Prover.writeCoqProp "goal" [] [])) path ".v" offline_extcore :: FilePath -> ProofScript SV.SatResult -offline_extcore path = proveWithExporter (const Prover.writeCoreProp) path ".extcore" +offline_extcore path = proveWithPropExporter (const Prover.writeCoreProp) path ".extcore" offline_smtlib2 :: FilePath -> ProofScript SV.SatResult -offline_smtlib2 path = proveWithExporter Prover.writeSMTLib2 path ".smt2" +offline_smtlib2 path = proveWithSATExporter Prover.writeSMTLib2 mempty path ".smt2" w4_offline_smtlib2 :: FilePath -> ProofScript SV.SatResult -w4_offline_smtlib2 path = proveWithExporter Prover.writeSMTLib2What4 path ".smt2" +w4_offline_smtlib2 path = proveWithSATExporter Prover.writeSMTLib2What4 mempty path ".smt2" offline_unint_smtlib2 :: [String] -> FilePath -> ProofScript SV.SatResult offline_unint_smtlib2 unints path = do unintSet <- lift $ resolveNames unints - proveWithExporter (Prover.writeUnintSMTLib2 unintSet) path ".smt2" + proveWithSATExporter Prover.writeSMTLib2 unintSet path ".smt2" offline_verilog :: FilePath -> ProofScript SV.SatResult offline_verilog path = - proveWithExporter (Prover.adaptExporter Prover.write_verilog) path ".v" + proveWithSATExporter Prover.writeVerilogSAT mempty path ".v" parseAigerCex :: String -> IO [Bool] parseAigerCex text = @@ -892,7 +906,8 @@ provePrim :: ProofScript SV.SatResult provePrim script t = do io $ checkBooleanSchema (ttSchema t) sc <- getSharedContext - goal <- io $ makeProofGoal sc Universal 0 "prove" "prove" (ttTerm t) + prop <- io $ predicateToProp sc Universal (ttTerm t) + let goal = ProofGoal 0 "prove" "prove" prop (r, pstate) <- runStateT script (startProof goal) io (finishProof sc pstate) >>= \case (_stats, Just _) -> return () @@ -904,7 +919,8 @@ provePrintPrim :: ProofScript SV.SatResult -> TypedTerm -> TopLevel Theorem provePrintPrim script t = do sc <- getSharedContext - goal <- io $ makeProofGoal sc Universal 0 "prove" "prove" (ttTerm t) + prop <- io $ predicateToProp sc Universal (ttTerm t) + let goal = ProofGoal 0 "prove" "prove" prop (r, pstate) <- runStateT script (startProof goal) opts <- rwPPOpts <$> getTopLevelRW io (finishProof sc pstate) >>= \case @@ -919,7 +935,8 @@ satPrim :: ProofScript SV.SatResult -> TypedTerm satPrim script t = do io $ checkBooleanSchema (ttSchema t) sc <- getSharedContext - goal <- io $ makeProofGoal sc Existential 0 "sat" "sat" (ttTerm t) + prop <- io $ predicateToProp sc Existential (ttTerm t) + let goal = ProofGoal 0 "sat" "sat" prop evalStateT script (startProof goal) satPrintPrim :: ProofScript SV.SatResult diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index bc2fde7baa..a119fa1457 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -268,7 +268,7 @@ verifyObligations cc mspec tactic assumes asserts = let nm = mspec ^. csMethodName stats <- forM (zip [(0::Int)..] asserts) $ \(n, (msg, assert)) -> do goal <- io $ scImplies sc assume assert - goal' <- io $ predicateToProp sc Universal [] goal + goal' <- io $ predicateToProp sc Universal goal let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"] proofgoal = ProofGoal n "vc" goalname goal' r <- evalStateT tactic (startProof proofgoal) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index fb23a85832..ab9f9b5c61 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -598,7 +598,7 @@ verifyObligations cc mspec tactic assumes asserts = stats <- forM (zip [(0::Int)..] asserts) $ \(n, (msg, assert)) -> do goal <- io $ scImplies sc assume assert - goal' <- io $ predicateToProp sc Universal [] goal + goal' <- io $ predicateToProp sc Universal goal let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"] proofgoal = ProofGoal n "vc" goalname goal' r <- evalStateT tactic (startProof proofgoal) @@ -760,7 +760,7 @@ assumptionsContainContradiction cc tactic assumptions = assume <- scAndList sc (toListOf (folded . Crucible.labeledPred) assumptions) -- implies falsehood goal <- scImplies sc assume =<< toSC sym st (W4.falsePred sym) - goal' <- predicateToProp sc Universal [] goal + goal' <- predicateToProp sc Universal goal return $ ProofGoal 0 "vc" "vacuousness check" goal' evalStateT tactic (startProof pgl) >>= \case Unsat _stats -> return True diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs index 5a811fbb5b..bf7e53f946 100644 --- a/src/SAWScript/Proof.hs +++ b/src/SAWScript/Proof.hs @@ -42,10 +42,8 @@ module SAWScript.Proof , Evidence(..) , checkEvidence - , ProofGoal(..) - , withFirstGoal - , Tactic + , withFirstGoal , tacticIntro , tacticCut , tacticAssume @@ -57,7 +55,6 @@ module SAWScript.Proof , tacticSolve , Quantification(..) - , makeProofGoal , predicateToProp , propToPredicate @@ -65,8 +62,11 @@ module SAWScript.Proof , psTimeout , psGoals , setProofTimeout + , ProofGoal(..) , startProof , finishProof + + , predicateToSATQuery ) where import qualified Control.Monad.Fail as F @@ -411,47 +411,32 @@ data ProofGoal = data Quantification = Existential | Universal deriving Eq --- | Construct a 'ProofGoal' from a term of type @Bool@, or a function --- of any arity with a boolean result type. Any function arguments are --- treated as quantified variables. If the 'Quantification' argument --- is 'Existential', then the predicate is negated and turned into a --- universally-quantified goal. -makeProofGoal :: - SharedContext -> - Quantification -> - Int {- goal number -} -> - String {- goal type -} -> - String {- goal name -} -> - Term {- goal predicate -} -> - IO ProofGoal -makeProofGoal sc quant gnum gtype gname t = - do t' <- predicateToProp sc quant [] t - return (ProofGoal gnum gtype gname t') - -- | Convert a term with a function type of any arity into a pi type. -- Negate the term if the result type is @Bool@ and the quantification -- is 'Existential'. -predicateToProp :: SharedContext -> Quantification -> [Term] -> Term -> IO Prop -predicateToProp sc quant env t = - case asLambda t of - Just (x, ty, body) -> - do Prop body' <- predicateToProp sc quant (ty : env) body - Prop <$> scPi sc x ty body' - Nothing -> - do (argTs, resT) <- asPiList <$> scTypeOf' sc env t - let toPi [] t0 = - case asBoolType resT of - Nothing -> return t0 -- TODO: check quantification - Just () -> - case quant of - Universal -> scEqTrue sc t0 - Existential -> scEqTrue sc =<< scNot sc t0 - toPi ((x, xT) : tys) t0 = - do t1 <- incVars sc 0 1 t0 - t2 <- scApply sc t1 =<< scLocalVar sc 0 - t3 <- toPi tys t2 - scPi sc x xT t3 - Prop <$> toPi argTs t +predicateToProp :: SharedContext -> Quantification -> Term -> IO Prop +predicateToProp sc quant = loop [] + where + loop env t = + case asLambda t of + Just (x, ty, body) -> + do Prop body' <- loop (ty : env) body + Prop <$> scPi sc x ty body' + Nothing -> + do (argTs, resT) <- asPiList <$> scTypeOf' sc env t + let toPi [] t0 = + case asBoolType resT of + Nothing -> return t0 -- TODO: check quantification TODO2: should this just be an error? + Just () -> + case quant of + Universal -> scEqTrue sc t0 + Existential -> scEqTrue sc =<< scNot sc t0 + toPi ((x, xT) : tys) t0 = + do t1 <- incVars sc 0 1 t0 + t2 <- scApply sc t1 =<< scLocalVar sc 0 + t3 <- toPi tys t2 + scPi sc x xT t3 + Prop <$> toPi argTs t -- | Turn a pi type with an @EqTrue@ result into a lambda term with a -- boolean result type. This function exists to interface the new @@ -683,6 +668,42 @@ withFirstGoal f = evidenceCont (e:es2) return (x, ProofState (gs' <> gs) concl (stats <> stats') timeout evidenceCont') +predicateToSATQuery :: SharedContext -> Set VarIndex -> Term -> IO SATQuery +predicateToSATQuery sc unintSet tm0 = + do (initVars, abstractVars) <- filterFirstOrderVars mempty mempty (getAllExts tm0) + (finalVars, tm') <- processTerm initVars tm0 + return SATQuery + { satVariables = finalVars + , satUninterp = Set.union unintSet abstractVars + , satAsserts = [tm'] + } + where + filterFirstOrderVars fovars absvars [] = pure (fovars, absvars) + filterFirstOrderVars fovars absvars (e:es) = + runMaybeT (asFirstOrderTypeMaybe sc (ecType e)) >>= \case + Nothing -> filterFirstOrderVars fovars (Set.insert (ecVarIndex e) absvars) es + Just fot -> filterFirstOrderVars (Map.insert e fot fovars) absvars es + + processTerm vars tm = + case asLambda tm of + Just (lnm,tp,body) -> + do fot <- asFirstOrderType sc tp + ec <- scFreshEC sc (Text.unpack lnm) tp + etm <- scExtCns sc ec + body' <- instantiateVar sc 0 etm body + processTerm (Map.insert ec fot vars) body' + + -- TODO: check that the type is a boolean + Nothing -> + do ty <- scTypeOf sc tm + ok <- scConvertible sc True ty =<< scBoolType sc + unless ok $ fail $ unlines + [ "predicateToSATQuery: expected boolean result but got:" + , showTerm ty + , showTerm tm0 + ] + return (vars, tm) + -- | Given a proposition, compute a SAT query which will prove the proposition -- iff the SAT query is unsatisfiable. propToSATQuery :: SharedContext -> Set VarIndex -> Prop -> IO SATQuery @@ -710,7 +731,7 @@ propToSATQuery sc unintSet prop = , looseVars body == emptyBitSet -> do processTerm vars (x:xs) body - -- TODO? Allow first-order hypotheses... + -- TODO? Allow universal hypotheses... | otherwise -> do fot <- asFirstOrderType sc tp @@ -749,6 +770,7 @@ goalApply sc rule goal = applyFirst (asPiLists (unProp rule)) mkNewGoals mts args mkNewGoals _ _ = return [] newgoalterms <- mkNewGoals inst' (reverse ruleArgs) + -- TODO, change the "ty" field to list the hypotheses? let newgoals = reverse [ goal { goalProp = t } | t <- newgoalterms ] return (Just newgoals) diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs index cc39797571..e5c9920ca2 100644 --- a/src/SAWScript/Prover/Exporter.hs +++ b/src/SAWScript/Prover/Exporter.hs @@ -6,11 +6,12 @@ {-# Language FlexibleContexts #-} {-# Language TypeApplications #-} module SAWScript.Prover.Exporter - ( proveWithExporter - , adaptExporter + ( proveWithSATExporter + , proveWithPropExporter -- * External formats , writeAIG + , writeAIG_SAT , writeSAIG , writeSAIGInferLatches , writeAIGComputedLatches @@ -20,8 +21,6 @@ module SAWScript.Prover.Exporter , writeSMTLib2What4 , write_smtlib2 , write_smtlib2_w4 - , writeUnintSMTLib2 - , writeUnintSMTLib2What4 , writeCoqCryptolPrimitivesForSAWCore , writeCoqCryptolModule , writeCoqSAWCorePrelude @@ -29,6 +28,7 @@ module SAWScript.Prover.Exporter , writeCoqProp , writeCore , writeVerilog + , writeVerilogSAT , write_verilog , writeCoreProp @@ -57,7 +57,8 @@ import Verifier.SAW.ExternalFormat(scWriteExternal) import Verifier.SAW.FiniteValue import Verifier.SAW.Module (emptyModule, moduleDecls) import Verifier.SAW.Prelude (preludeModule) -import Verifier.SAW.Recognizer (asPi, asPiList, asEqTrue) +import Verifier.SAW.Recognizer (asPi) +import Verifier.SAW.SATQuery import Verifier.SAW.SharedTerm as SC import qualified Verifier.SAW.Translation.Coq as Coq import Verifier.SAW.TypedAST (mkModuleName) @@ -65,55 +66,57 @@ import Verifier.SAW.TypedTerm import qualified Verifier.SAW.Simulator.BitBlast as BBSim import qualified Verifier.SAW.Simulator.Value as Sim import qualified Verifier.SAW.Simulator.What4 as W4Sim +import qualified Verifier.SAW.Simulator.SBV as SBV import qualified Verifier.SAW.UntypedAST as Un import SAWScript.Crucible.Common -import SAWScript.Proof (Prop, propSize, propToTerm, predicateToProp, Quantification(..), propToPredicate) +import SAWScript.Proof (Prop, propSize, propToTerm, predicateToSATQuery, propToSATQuery) import SAWScript.Prover.SolverStats import SAWScript.Prover.Util -import SAWScript.Prover.SBV (prepNegatedSBV) import SAWScript.Prover.What4 import SAWScript.Value -import qualified What4.Interface as W4 import qualified What4.Expr.Builder as W4 import What4.Protocol.SMTLib2 (writeDefaultSMT2) import What4.Protocol.VerilogWriter (exprVerilog) import What4.Solver.Adapter import qualified What4.SWord as W4Sim -proveWithExporter :: +proveWithSATExporter :: + (SharedContext -> FilePath -> SATQuery -> TopLevel ()) -> + Set VarIndex -> + String -> + Prop -> + TopLevel SolverStats +proveWithSATExporter exporter unintSet path goal = + do sc <- getSharedContext + satq <- io $ propToSATQuery sc unintSet goal + exporter sc path satq + let stats = solverStats ("offline: "++ path) (propSize goal) + return stats + + +proveWithPropExporter :: (SharedContext -> FilePath -> Prop -> TopLevel ()) -> String -> Prop -> TopLevel SolverStats -proveWithExporter exporter path goal = +proveWithPropExporter exporter path goal = do sc <- getSharedContext exporter sc path goal let stats = solverStats ("offline: "++ path) (propSize goal) return stats --- | Converts an old-style exporter (which expects to take a predicate --- as an argument) into a new-style one (which takes a pi-type proposition). -adaptExporter :: - (SharedContext -> FilePath -> Term -> TopLevel ()) -> - (SharedContext -> FilePath -> Prop -> TopLevel ()) -adaptExporter exporter sc path goal = - -- TODO, move this into Proof.hs - do (args, concl) <- asPiList <$> io (propToTerm sc goal) - p <- - case asEqTrue concl of - Just p -> return p - Nothing -> throwTopLevel "adaptExporter: expected EqTrue" - p' <- io $ scNot sc p -- is this right? - t <- io $ scLambdaList sc args p' - exporter sc path t - -------------------------------------------------------------------------------- --- | Write a @Term@ representing a theorem or an arbitrary --- function to an AIG file. +writeAIG_SAT :: (AIG.IsAIG l g) => AIG.Proxy l g -> SharedContext -> FilePath -> SATQuery -> TopLevel () +writeAIG_SAT proxy sc f satq = io $ + do t <- satQueryAsTerm sc satq + BBSim.withBitBlastedPred proxy sc mempty t $ \g l _vars -> do + AIG.writeAiger f (AIG.Network g [l]) + +-- | Write a @Term@ representing a an arbitrary function to an AIG file. writeAIG :: (AIG.IsAIG l g) => AIG.Proxy l g -> SharedContext -> FilePath -> Term -> TopLevel () writeAIG proxy sc f t = do io $ do @@ -175,31 +178,18 @@ writeAIGComputedLatches :: writeAIGComputedLatches proxy sc file term numLatches = writeSAIG proxy sc file term numLatches -writeCNF :: (AIG.IsAIG l g) => AIG.Proxy l g -> SharedContext -> FilePath -> Term -> TopLevel () -writeCNF proxy sc f t = do - AIG.Network be ls <- io $ bitblastPrim proxy sc t - case ls of - [l] -> do - _ <- io $ AIG.writeCNF be l f - return () - _ -> throwTopLevel "writeCNF: non-boolean term" +writeCNF :: (AIG.IsAIG l g) => AIG.Proxy l g -> SharedContext -> FilePath -> SATQuery -> TopLevel () +writeCNF proxy sc f satq = io $ + do t <- satQueryAsTerm sc satq + _ <- BBSim.withBitBlastedPred proxy sc mempty t $ \g l _vars -> AIG.writeCNF g l f + return () write_cnf :: SharedContext -> FilePath -> TypedTerm -> TopLevel () write_cnf sc f (TypedTerm schema t) = do liftIO $ checkBooleanSchema schema AIGProxy proxy <- getProxy - writeCNF proxy sc f t - --- | Write a proposition to an SMT-Lib version 2 file. Because @Prop@ is --- assumed to have universally quantified variables, it will be negated. -writeSMTLib2 :: SharedContext -> FilePath -> Prop -> TopLevel () -writeSMTLib2 sc f t = writeUnintSMTLib2 mempty sc f t - --- | Write a proposition to an SMT-Lib version 2 file. Because @Prop@ is --- assumed to have universally quantified variables, it will be negated. --- This version uses What4 instead of SBV. -writeSMTLib2What4 :: SharedContext -> FilePath -> Prop -> TopLevel () -writeSMTLib2What4 sc f t = writeUnintSMTLib2What4 mempty sc f t + satq <- io (predicateToSATQuery sc mempty t) + writeCNF proxy sc f satq -- | Write a @Term@ representing a predicate (i.e. a monomorphic -- function returning a boolean) to an SMT-Lib version 2 file. The goal @@ -208,8 +198,8 @@ writeSMTLib2What4 sc f t = writeUnintSMTLib2What4 mempty sc f t write_smtlib2 :: SharedContext -> FilePath -> TypedTerm -> TopLevel () write_smtlib2 sc f (TypedTerm schema t) = do io $ checkBooleanSchema schema - p <- io $ predicateToProp sc Existential [] t - writeSMTLib2 sc f p + satq <- io $ predicateToSATQuery sc mempty t + writeSMTLib2 sc f satq -- | Write a @Term@ representing a predicate (i.e. a monomorphic -- function returning a boolean) to an SMT-Lib version 2 file. The goal @@ -218,38 +208,39 @@ write_smtlib2 sc f (TypedTerm schema t) = do write_smtlib2_w4 :: SharedContext -> FilePath -> TypedTerm -> TopLevel () write_smtlib2_w4 sc f (TypedTerm schema t) = do io $ checkBooleanSchema schema - p <- io $ predicateToProp sc Existential [] t - writeUnintSMTLib2What4 mempty sc f p - --- | Write a proposition to an SMT-Lib version 2 file, treating some --- constants as uninterpreted. Because @Prop@ is assumed to have --- universally quantified variables, it will be negated. -writeUnintSMTLib2 :: Set VarIndex -> SharedContext -> FilePath -> Prop -> TopLevel () -writeUnintSMTLib2 unintSet sc f p = io $ - do (_, _, l) <- prepNegatedSBV sc unintSet p + satq <- io $ predicateToSATQuery sc mempty t + writeSMTLib2What4 sc f satq + +-- | Write a SAT query to an SMT-Lib version 2 file. +writeSMTLib2 :: SharedContext -> FilePath -> SATQuery -> TopLevel () +writeSMTLib2 sc f satq = io $ + do (_, _, l) <- SBV.sbvSATQuery sc mempty satq let isSat = True -- l is encoded as an existential formula txt <- SBV.generateSMTBenchmark isSat l writeFile f txt --- | Write a proposition to an SMT-Lib version 2 file, treating some --- constants as uninterpreted. Because @Prop@ is assumed to have --- universally quantified variables, it will be negated. This version --- uses What4 instead of SBV. -writeUnintSMTLib2What4 :: Set VarIndex -> SharedContext -> FilePath -> Prop -> TopLevel () -writeUnintSMTLib2What4 unints sc f goal = io $ +-- | Write a SAT query an SMT-Lib version 2 file. +-- This version uses What4 instead of SBV. +writeSMTLib2What4 :: SharedContext -> FilePath -> SATQuery -> TopLevel () +writeSMTLib2What4 sc f satq = io $ do sym <- W4.newExprBuilder W4.FloatRealRepr St globalNonceGenerator - term <- propToPredicate sc goal - (_, _, (_,lit0)) <- prepWhat4 sym sc unints term - lit <- W4.notPred sym lit0 -- for symmetry with `prepNegatedSBV` above + term <- satQueryAsTerm sc satq + (_, _, (_,lit)) <- prepWhat4 sym sc (satUninterp satq) term withFile f WriteMode $ \h -> writeDefaultSMT2 () "Offline SMTLib2" defaultWriteSMTLIB2Features sym h [lit] + writeCore :: FilePath -> Term -> TopLevel () writeCore path t = io $ writeFile path (scWriteExternal t) write_verilog :: SharedContext -> FilePath -> Term -> TopLevel () write_verilog sc path t = io $ writeVerilog sc path t +writeVerilogSAT :: SharedContext -> FilePath -> SATQuery -> TopLevel () +writeVerilogSAT sc path satq = io $ + do t <- satQueryAsTerm sc satq + writeVerilog sc path t + writeVerilog :: SharedContext -> FilePath -> Term -> IO () writeVerilog sc path t = do sym <- newSAWCoreBackend sc diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs index d7e12d3b61..db4d3254d2 100644 --- a/src/SAWScript/Prover/MRSolver.hs +++ b/src/SAWScript/Prover/MRSolver.hs @@ -281,7 +281,7 @@ mrProvable bool_prop = path_prop <- mrPathCondition <$> get bool_prop' <- liftSC2 scImplies path_prop bool_prop sc <- mrSC <$> get - prop <- liftIO (predicateToProp sc Universal [] bool_prop') + prop <- liftIO (predicateToProp sc Universal bool_prop') (smt_res, _) <- liftSC1 (SBV.proveUnintSBV smt_conf mempty timeout) prop case smt_res of Just _ -> return False diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs index 432e6263de..2400bf4086 100644 --- a/src/SAWScript/X86.hs +++ b/src/SAWScript/X86.hs @@ -540,7 +540,7 @@ data Goal = Goal -- | The proposition that needs proving (i.e., assumptions imply conclusion) gGoal :: SharedContext -> Goal -> IO Prop -gGoal sc g0 = predicateToProp sc Universal [] =<< go (gAssumes g) +gGoal sc g0 = predicateToProp sc Universal =<< go (gAssumes g) where g = g0 { gAssumes = mapMaybe skip (gAssumes g0) }