From 519805188a4986d00e9cced0bc919c8c267fdd0f Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Fri, 5 Apr 2019 17:02:43 -0700 Subject: [PATCH] Simplify ProofGoal representation; fix negation convention in backends. As of this commit, we now treat every ProofGoal as having universally- quantified variables. The `sat` command creates a universally-quantified goal by logically negating the given predicate. As a result the solver backends don't need to know whether the current proof goal came from a `prove` or a `sat` command; they should behave the same in either case. Fixes #322. --- src/SAWScript/Builtins.hs | 54 ++++++++++----------------- src/SAWScript/CrucibleBuiltins.hs | 4 +- src/SAWScript/JVM/CrucibleBuiltins.hs | 2 +- src/SAWScript/JavaBuiltins.hs | 2 +- src/SAWScript/LLVMBuiltins.hs | 2 +- src/SAWScript/Proof.hs | 19 +++++----- src/SAWScript/Prover/Exporter.hs | 3 +- 7 files changed, 35 insertions(+), 51 deletions(-) diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 4bb65c3e17..8fad574dfc 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -121,7 +121,6 @@ import qualified SAWScript.Value as SV import SAWScript.Value (ProofScript, printOutLnTop, AIGNetwork) import SAWScript.Prover.Util(checkBooleanSchema,liftCexBB) -import SAWScript.Prover.Mode(ProverMode(..)) import SAWScript.Prover.SolverStats import SAWScript.Prover.Rewrite(rewriteEqs) import qualified SAWScript.Prover.SBV as Prover @@ -392,8 +391,7 @@ split_goal = StateT $ \(ProofState goals concl stats timeout) -> case goals of [] -> fail "ProofScript failed: no subgoal" - (ProofGoal Existential _ _ _ _) : _ -> fail "not a universally-quantified goal" - (ProofGoal Universal num ty name prop) : gs -> + (ProofGoal num ty name prop) : gs -> let (vars, body) = asLambdaList prop in case (isGlobalDef "Prelude.and" <@> return <@> return) body of Nothing -> fail "split_goal: goal not of form 'Prelude.and _ _'" @@ -401,8 +399,8 @@ split_goal = do sc <- getSharedContext t1 <- io $ scLambdaList sc vars p1 t2 <- io $ scLambdaList sc vars p2 - let g1 = ProofGoal Universal num (ty ++ ".left") name t1 - let g2 = ProofGoal Universal num (ty ++ ".right") name t2 + let g1 = ProofGoal num (ty ++ ".left") name t1 + let g2 = ProofGoal num (ty ++ ".right") name t2 return ((), ProofState (g1 : g2 : gs) concl stats timeout) getTopLevelPPOpts :: TopLevel PPOpts @@ -588,16 +586,14 @@ parseDimacsSolution vars ls = map lkup vars assgnMap = Map.fromList (map varToPair vs) lkup v = Map.findWithDefault False v assgnMap -satExternal :: Bool -> String -> [String] - -> ProofScript SV.SatResult -satExternal doCNF execName args = withFirstGoal $ \g0 -> do +satExternal :: Bool -> String -> [String] -> ProofScript SV.SatResult +satExternal doCNF execName args = withFirstGoal $ \g -> do sc <- SV.getSharedContext SV.AIGProxy proxy <- SV.getProxy io $ do - let (vars, concl) = asPiList (goalTerm g0) + let (vars, concl) = asPiList (goalTerm g) t0 <- scLambdaList sc vars =<< asEqTrue concl - let g = g0 { goalTerm = t0 } - t <- rewriteEqs sc (goalTerm g) + t <- rewriteEqs sc t0 tp <- scWhnf sc =<< scTypeOf sc t let cnfName = goalType g ++ show (goalNum g) ++ ".cnf" argNames = map fst (fst (asPiList tp)) @@ -607,9 +603,8 @@ satExternal doCNF execName args = withFirstGoal $ \g0 -> do replaceFileName "%f" = path replaceFileName a = a BBSim.withBitBlastedPred proxy sc bitblastPrimitives t $ \be l0 shapes -> do - let l = case goalQuant g of - Existential -> l0 - Universal -> AIG.not l0 + -- negate formula to turn it into an existentially-quantified SAT query + let l = AIG.not l0 variables <- (if doCNF then AIG.writeCNF else writeAIGWithMapping) be l path (_ec, out, err) <- readProcessWithExitCode execName args' "" removeFile path @@ -618,7 +613,7 @@ satExternal doCNF execName args = withFirstGoal $ \g0 -> do let ls = lines out sls = filter ("s " `isPrefixOf`) ls vls = filter ("v " `isPrefixOf`) ls - ft <- scApplyPrelude_False sc + ft <- scEqTrue sc =<< scApplyPrelude_False sc let stats = solverStats ("external SAT:" ++ execName) (scSharedSize t) case (sls, vls) of (["s SATISFIABLE"], _) -> do @@ -629,14 +624,10 @@ satExternal doCNF execName args = withFirstGoal $ \g0 -> do Right vs | length argNames == length vs -> do let r' = SV.SatMulti stats (zip argNames (map toFirstOrderValue vs)) - case goalQuant g of - Universal -> return (r', stats, Just (g { goalTerm = ft })) - Existential -> return (r', stats, Nothing) + return (r', stats, Just (g { goalTerm = ft })) | otherwise -> fail $ unwords ["external SAT results do not match expected arguments", show argNames, show vs] (["s UNSATISFIABLE"], []) -> - case goalQuant g of - Universal -> return (SV.Unsat stats, stats, Nothing) - Existential -> return (SV.Unsat stats, stats, Just (g { goalTerm = ft })) + return (SV.Unsat stats, stats, Nothing) _ -> fail $ "Unexpected result from SAT solver:\n" ++ out writeAIGWithMapping :: AIG.IsAIG l g => g s -> l s -> FilePath -> IO [Int] @@ -696,20 +687,15 @@ wrapProver :: wrapProver f = do sc <- lift $ SV.getSharedContext withFirstGoal $ \g -> do - let mode = case goalQuant g of - Existential -> CheckSat - Universal -> Prove - (mb,stats) <- io $ f sc (goalTerm g) + (mb, stats) <- io $ f sc (goalTerm g) - let nope r = do ft <- io $ scApplyPrelude_False sc + let nope r = do ft <- io $ scEqTrue sc =<< scApplyPrelude_False sc return (r, stats, Just g { goalTerm = ft }) - case (mode,mb) of - (CheckSat, Just a) -> return (SV.SatMulti stats a, stats, Nothing) - (CheckSat, Nothing) -> nope (SV.Unsat stats) - (Prove, Nothing) -> return (SV.Unsat stats, stats, Nothing) - (Prove, Just a) -> nope (SV.SatMulti stats a) + case mb of + Nothing -> return (SV.Unsat stats, stats, Nothing) + Just a -> nope (SV.SatMulti stats a) -------------------------------------------------- satBoolector :: ProofScript SV.SatResult @@ -780,9 +766,7 @@ satWithExporter exporter path ext = sc <- SV.getSharedContext stats <- io $ Prover.satWithExporter exporter file sc (goalTerm g) - case goalQuant g of - Existential -> return (SV.Unsat stats, stats, Just g) - Universal -> return (SV.Unsat stats, stats, Nothing) + return (SV.Unsat stats, stats, Nothing) satAIG :: FilePath -> ProofScript SV.SatResult satAIG path = do @@ -1228,7 +1212,7 @@ parse_core input = do prove_core :: ProofScript SV.SatResult -> String -> TopLevel Theorem prove_core script input = do t <- parseCore input - (r', pstate) <- runStateT script (startProof (ProofGoal Universal 0 "prove" "prove" t)) + (r', pstate) <- runStateT script (startProof (ProofGoal 0 "prove" "prove" t)) let r = SV.flipSatResult r' opts <- rwPPOpts <$> getTopLevelRW case finishProof pstate of diff --git a/src/SAWScript/CrucibleBuiltins.hs b/src/SAWScript/CrucibleBuiltins.hs index 658bf4f8f1..9dc748dd91 100644 --- a/src/SAWScript/CrucibleBuiltins.hs +++ b/src/SAWScript/CrucibleBuiltins.hs @@ -253,8 +253,8 @@ verifyObligations cc mspec tactic assumes asserts = do goal <- io $ scImplies sc assume assert goal' <- io $ scGeneralizeExts sc (getAllExts goal) =<< scEqTrue sc goal let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"] - proofgoal = ProofGoal Universal n "vc" goalname goal' - r <- evalStateT tactic (startProof proofgoal) + proofgoal = ProofGoal n "vc" goalname goal' + r <- evalStateT tactic (startProof proofgoal) case r of Unsat stats -> return stats SatMulti stats vals -> do diff --git a/src/SAWScript/JVM/CrucibleBuiltins.hs b/src/SAWScript/JVM/CrucibleBuiltins.hs index 26f22b35cf..8f765e6117 100644 --- a/src/SAWScript/JVM/CrucibleBuiltins.hs +++ b/src/SAWScript/JVM/CrucibleBuiltins.hs @@ -266,7 +266,7 @@ verifyObligations cc mspec tactic assumes asserts = goal <- io $ scImplies sc assume assert goal' <- io $ scGeneralizeExts sc (getAllExts goal) =<< scEqTrue sc goal let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"] - proofgoal = ProofGoal Universal n "vc" goalname goal' + proofgoal = ProofGoal n "vc" goalname goal' r <- evalStateT tactic (startProof proofgoal) case r of Unsat stats -> return stats diff --git a/src/SAWScript/JavaBuiltins.hs b/src/SAWScript/JavaBuiltins.hs index 1a87e9f47a..1480662136 100644 --- a/src/SAWScript/JavaBuiltins.hs +++ b/src/SAWScript/JavaBuiltins.hs @@ -250,7 +250,7 @@ verifyJava bic opts cls mname overrides setup = do let exts = getAllExts g gprop <- io $ scGeneralizeExts jsc exts =<< scEqTrue jsc g io $ doExtraChecks opts bsc gprop - let goal = ProofGoal Universal n "vc" (vsVCName vs) gprop + let goal = ProofGoal n "vc" (vsVCName vs) gprop r <- evalStateT script (startProof goal) case r of SS.Unsat _ -> liftIO $ printOutLn opts Debug "Valid." diff --git a/src/SAWScript/LLVMBuiltins.hs b/src/SAWScript/LLVMBuiltins.hs index 4401b5cd7e..82ddfbb412 100644 --- a/src/SAWScript/LLVMBuiltins.hs +++ b/src/SAWScript/LLVMBuiltins.hs @@ -314,7 +314,7 @@ prover vpopts sc ms script vs n g = do let exts = getAllExts g ppopts <- fmap rwPPOpts getTopLevelRW tt <- io $ scGeneralizeExts sc exts =<< scEqTrue sc g - let goal = ProofGoal Universal n "vc" (vsVCName vs) tt + let goal = ProofGoal n "vc" (vsVCName vs) tt r <- evalStateT script (startProof goal) case r of SV.Unsat stats -> do diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs index 44808d14ad..1233a4616e 100644 --- a/src/SAWScript/Proof.hs +++ b/src/SAWScript/Proof.hs @@ -15,26 +15,25 @@ import SAWScript.Prover.SolverStats -- or more lambdas which are interpreted as universal quantifiers. data Theorem = Theorem { thmTerm :: Term } -data Quantification = Existential | Universal - deriving Eq - -- | A ProofGoal is a term of type @sort n@, or a pi type of any arity -- with a @sort n@ result type. The abstracted arguments are treated --- as either universally quantified. If the 'goalQuant' field is set --- to 'Existential', then the entire goal is considered to be --- logically negated, so it is as if the quantifiers are existential. +-- as universally quantified. data ProofGoal = ProofGoal - { goalQuant :: Quantification - , goalNum :: Int + { goalNum :: Int , goalType :: String , goalName :: String , goalTerm :: Term } +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. +-- 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 -> @@ -45,7 +44,7 @@ makeProofGoal :: IO ProofGoal makeProofGoal sc quant gnum gtype gname t = do t' <- predicateToProp sc quant [] t - return (ProofGoal quant gnum gtype gname 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 diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs index b91c0d0833..b1242433a8 100644 --- a/src/SAWScript/Prover/Exporter.hs +++ b/src/SAWScript/Prover/Exporter.hs @@ -163,7 +163,8 @@ write_smtlib2 sc f (TypedTerm schema t) = do writeUnintSMTLib2 :: [String] -> SharedContext -> FilePath -> Term -> IO () writeUnintSMTLib2 unints sc f t = do (_, _, l) <- prepSBV sc unints t - txt <- SBV.generateSMTBenchmark True l + let isSat = False -- term is a proof goal with universally-quantified variables + txt <- SBV.generateSMTBenchmark isSat l writeFile f txt writeCore :: FilePath -> Term -> IO ()