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.

Author: robdockins

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

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)

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

src/SAWScript/Proof.hs

@@ -42,10 +42,8 @@ module SAWScript.Proof
   , Evidence(..)
   , checkEvidence
 
-  , ProofGoal(..)
-  , withFirstGoal
-
   , Tactic
+  , withFirstGoal
   , tacticIntro
   , tacticCut
   , tacticAssume
@@ -57,16 +55,18 @@ module SAWScript.Proof
   , tacticSolve
 
   , Quantification(..)
-  , makeProofGoal
   , predicateToProp
   , propToPredicate
 
   , ProofState
   , 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)