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

@@ -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,17 +391,16 @@ 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 _ _'"
         Just (_ :*: p1 :*: p2) ->
           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

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

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

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."

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

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

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 ()