Adding a feature to ask for abducts

.github/workflows/gen_matrix.pl

@@ -77,7 +77,7 @@
 main_version(yices, "2_6_4").
 main_version(stp, "2_3_3").
 main_version(cvc4, "1_8").
-main_version(cvc5, "1_0_0").
+main_version(cvc5, "1_0_2").
 main_version(boolector, "3_2_2").
 main_version(abc, "2021_12_30").
 
@@ -114,9 +114,7 @@
 % n.b. stp 2_2_0 fails, no reason to test it
 
 version(cvc4, "1_8").
-version(cvc4, "1_7").
-
-version(cvc5, "1_0_0").
+version(cvc5, "1_0_2").
 
 version(boolector, "3_2_2").
 version(boolector, "3_2_1").

README.md

@@ -18,8 +18,8 @@ views or policies of the Department of Defense or the U.S. Government.
 
 # Solver Compatibility
 
-| Feature                               | ABC | Boolector   | CVC4      | CVC5 | Dreal | STP         | Yices    | Z3                   |
-|---------------------------------------|-----|-------------|-----------|------|-------|-------------|----------|----------------------|
-| Supported                             | yes | >= 3.2.0, ? | >= 1.8, ? | yes  | yes   | >= 2.3.3, ? | 2.6.x, ? | 4.8.8 -- 4.8.14      |
-| goal timeouts                         | ?   | yes         | yes       | yes  | ?     | yes         | yes      | ! (4.8.11 or 4.8.12) |
-| strings with unicode and escape codes | ?   | ?           | >= 1.8    | yes  | ?     | ?           | ?        | >= 4.8.11            |
+| Feature                               | ABC | Boolector   | CVC4      | CVC5  | Dreal | STP         | Yices    | Z3                   |
+|---------------------------------------|-----|-------------|-----------|-------|-------|-------------|----------|----------------------|
+| Supported                             | yes | >= 3.2.0, ? | >= 1.8, ? | 1.0.2 | yes   | >= 2.3.3, ? | 2.6.x, ? | 4.8.8 -- 4.8.14      |
+| goal timeouts                         | ?   | yes         | yes       | yes   | ?     | yes         | yes      | ! (4.8.11 or 4.8.12) |
+| strings with unicode and escape codes | ?   | ?           | >= 1.8    | yes   | ?     | ?           | ?        | >= 4.8.11            |

what4/CHANGES.md

@@ -7,6 +7,8 @@
 
 * Added support for the cvc5 SMT solver.
 
+* Added a `get-abduct` feature which is compatible with cvc5.
+
 # 1.3 (April 2022)
 
 * Allow building with GHC 9.2.

what4/README.md

@@ -273,7 +273,7 @@ on as wide a collection of solvers as is reasonable.
 - Z3 versions 4.8.7 through 4.8.12
 - Yices 2.6.1 and 2.6.2
 - CVC4 1.7 and 1.8
-- CVC5 1.0.0
+- CVC5 1.0.2
 - Boolector 3.2.1 and 3.2.2
 - STP 2.3.3
     (However, note https://github.com/stp/stp/issues/363, which prevents

what4/src/What4/ProblemFeatures.hs

@@ -45,6 +45,7 @@ module What4.ProblemFeatures
   , useUnsatAssumptions
   , useUninterpFunctions
   , useDefinedFunctions
+  , useProduceAbducts
   , hasProblemFeature
   ) where
 
@@ -130,6 +131,11 @@ useUninterpFunctions = ProblemFeatures 0x2000
 useDefinedFunctions :: ProblemFeatures
 useDefinedFunctions = ProblemFeatures 0x4000
 
+-- | Indicates if the solver is able and configured to 
+--   produce abducts.
+useProduceAbducts :: ProblemFeatures
+useProduceAbducts = ProblemFeatures 0x8000
+
 -- | Tests if one set of problem features subsumes another.
 --   In particular, @hasProblemFeature x y@ is true iff
 --   the set of features in @x@ is a superset of those in @y@.

what4/src/What4/Protocol/Online.hs

@@ -32,12 +32,15 @@ module What4.Protocol.Online
   , reset
   , inNewFrame
   , inNewFrameWithVars
+  , inNewFrame2Open
+  , inNewFrame2Close
   , check
   , checkAndGetModel
   , checkWithAssumptions
   , checkWithAssumptionsAndModel
   , getModel
   , getUnsatCore
+  , getAbducts
   , getUnsatAssumptions
   , getSatResult
   , checkSatisfiable
@@ -236,6 +239,39 @@ checkSatisfiable proc rsn p =
         do assume conn p
            check proc rsn
 
+-- | @get-abuct nm t@ queries the solver for the first abduct, which is returned
+--   as an SMT function definition named @nm@. The remaining abducts are obtained
+--   from the solver by successive invocations of the @get-abduct-next@ command,
+--   which return SMT functions bound to the same @nm@ as the first. The name @nm@
+--   is bound within the current assertion frame.
+--   Note that this is an unstable API; we expect that the return type will change 
+--   to a parsed expression in the future
+getAbducts ::
+  SMTReadWriter solver =>
+  SolverProcess scope solver ->
+  Int ->
+  Text ->
+  BoolExpr scope ->
+  IO [String]
+getAbducts proc n nm t =
+  if (n > 0) then do 
+    let conn = solverConn proc
+    unless (supportedFeatures conn `hasProblemFeature` useProduceAbducts) $
+      fail $ show $ pretty (smtWriterName conn) <+> pretty "is not configured to produce abducts"
+    f <- mkFormula conn t
+    -- get the first abduct using the get-abduct command
+    addCommandNoAck conn (getAbductCommand conn nm f)
+    abd1 <- smtAbductResult conn conn nm f
+    -- get the remaining abducts using get-abduct-next commands
+    if (n > 1) then do
+      let rest = n - 1
+      abdRest <- forM [1..rest] $ \_ -> do
+        addCommandNoAck conn (getAbductNextCommand conn)
+        smtAbductNextResult conn conn
+      return (abd1:abdRest)
+    else return [abd1]
+  else return []
+
 -- | Check if the formula is satisifiable in the current
 --   solver state.  This is done in a
 --   fresh frame, which is exited after the continuation
@@ -327,6 +363,17 @@ tryPop p =
 inNewFrame :: (MonadIO m, MonadMask m, SMTReadWriter solver) => SolverProcess scope solver -> m a -> m a
 inNewFrame p action = inNewFrameWithVars p [] action
 
+-- | Open a second solver assumption frame.
+-- For abduction, we want the final assertion to be a in a new frame, so that it 
+-- can be closed before asking for abducts. The following two commands allow frame 2 
+-- to be pushed and popped independently of other commands
+inNewFrame2Open :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
+inNewFrame2Open sp = let c = solverConn sp in addCommand c (push2Command c)
+
+-- | Close a second solver assumption frame.
+inNewFrame2Close :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
+inNewFrame2Close sp = let c = solverConn sp in addCommand c (pop2Command c)
+
 -- | Perform an action in the scope of a solver assumption frame, where the given
 -- bound variables are considered free within that frame.
 inNewFrameWithVars :: (MonadIO m, MonadMask m, SMTReadWriter solver)

what4/src/What4/Protocol/SExp.hs

@@ -19,6 +19,7 @@ module What4.Protocol.SExp
   , asAtomList
   , asNegAtomList
   , skipSpaceOrNewline
+  , sExpToString
   ) where
 
 #if !MIN_VERSION_base(4,13,0)
@@ -111,3 +112,8 @@ asAtomList (SApp xs) = go xs
   go (SAtom a:ys) = (a:) <$> go ys
   go _ = Nothing
 asAtomList _ = Nothing
+
+sExpToString :: SExp -> String
+sExpToString (SAtom t) = Text.unpack t
+sExpToString (SString t) = ('"' : Text.unpack t) ++ ['"']
+sExpToString (SApp ss) = ('(' : Data.String.unwords (map sExpToString ss)) ++ [')']

what4/src/What4/Protocol/SMTLib2.hs

@@ -38,7 +38,10 @@ module What4.Protocol.SMTLib2
   , writeCheckSat
   , writeExit
   , writeGetValue
+  , writeGetAbduct
+  , writeGetAbductNext
   , runCheckSat
+  , runGetAbducts
   , asSMT2Type
   , setOption
   , getVersion
@@ -676,6 +679,8 @@ instance SMTLib2Tweaks a => SMTWriter (Writer a) where
 
   pushCommand _  = SMT2.push 1
   popCommand _   = SMT2.pop 1
+  push2Command _ = SMT2.push 2
+  pop2Command _ = SMT2.pop 2
   resetCommand _ = SMT2.resetAssertions
   popManyCommands _ n = [SMT2.pop (toInteger n)]
 
@@ -684,6 +689,9 @@ instance SMTLib2Tweaks a => SMTWriter (Writer a) where
 
   getUnsatAssumptionsCommand _ = SMT2.getUnsatAssumptions
   getUnsatCoreCommand _ = SMT2.getUnsatCore
+  getAbductCommand _ nm e = SMT2.getAbduct nm e
+  getAbductNextCommand _ = SMT2.getAbductNext
+
   setOptCommand _ = SMT2.setOption
 
   declareCommand _proxy v argTypes retType =
@@ -755,6 +763,12 @@ setProduceModels w b = addCommand w $ SMT2.setProduceModels b
 writeGetValue :: SMTLib2Tweaks a => WriterConn t (Writer a) -> [Term] -> IO ()
 writeGetValue w l = addCommandNoAck w $ SMT2.getValue l
 
+writeGetAbduct :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Text -> Term -> IO ()
+writeGetAbduct w nm p = addCommandNoAck w $ SMT2.getAbduct nm p
+
+writeGetAbductNext :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
+writeGetAbductNext w = addCommandNoAck w SMT2.getAbductNext
+
 parseBoolSolverValue :: MonadFail m => SExp -> m Bool
 parseBoolSolverValue (SAtom "true")  = return True
 parseBoolSolverValue (SAtom "false") = return False
@@ -891,6 +905,32 @@ runGetValue s e = do
         _ -> Nothing
   getLimitedSolverResponse "get value" valRsp (sessionWriter s) (SMT2.getValue [e])
 
+-- | runGetAbducts s nm p n, returns n formulas (as strings) the disjunction of which entails p (along with all
+--   the assertions in the context)
+runGetAbducts :: SMTLib2Tweaks a
+             => Session t a
+             -> Int
+             -> Text
+             -> Term
+             -> IO [String]
+runGetAbducts s n nm p = 
+  if (n > 0) then do
+    writeGetAbduct (sessionWriter s) nm p
+    let valRsp = \x -> case x of
+          -- SMT solver returns `(define-fun nm () Bool X)` where X is the abduct, we discard everything but the abduct
+          AckSuccessSExp (SApp (_ : _ : _ : _ : abduct)) -> Just $ Data.String.unwords (map sExpToString abduct)
+          _ -> Nothing
+    -- get first abduct using the get-abduct command
+    abd1 <- getLimitedSolverResponse "get abduct" valRsp (sessionWriter s) (SMT2.getAbduct nm p)
+    if (n > 1) then do
+      let rest = n - 1
+      replicateM_ rest $ writeGetAbductNext (sessionWriter s)
+      -- get the rest of the abducts using the get-abduct-next command
+      abdRest <- forM [1..rest] $ \_ -> getLimitedSolverResponse "get abduct next" valRsp (sessionWriter s) (SMT2.getAbduct nm p)
+      return (abd1:abdRest)
+    else return [abd1]
+  else return []
+
 -- | This function runs a check sat command
 runCheckSat :: forall b t a.
                SMTLib2Tweaks b
@@ -938,6 +978,20 @@ instance SMTLib2Tweaks a => SMTReadWriter (Writer a) where
         cmd = getUnsatCoreCommand p
     in getLimitedSolverResponse "unsat core" unsatCoreRsp s cmd
 
+  smtAbductResult p s nm t =
+    let abductRsp = \case
+          AckSuccessSExp (SApp (_ : _ : _ : _ : abduct)) -> Just $ Data.String.unwords (map sExpToString abduct)
+          _ -> Nothing
+        cmd = getAbductCommand p nm t
+    in getLimitedSolverResponse "get abduct" abductRsp s cmd
+
+  smtAbductNextResult p s =
+    let abductRsp = \case
+          AckSuccessSExp (SApp (_ : _ : _ : _ : abduct)) -> Just $ Data.String.unwords (map sExpToString abduct)
+          _ -> Nothing
+        cmd = getAbductNextCommand p
+    in getLimitedSolverResponse "get abduct next" abductRsp s cmd
+
 
 smtAckResult :: AcknowledgementAction t (Writer a)
 smtAckResult = AckAction $ getLimitedSolverResponse "get ack" $ \case

what4/src/What4/Protocol/SMTLib2/Parse.hs

@@ -17,7 +17,7 @@ module What4.Protocol.SMTLib2.Parse
   ( -- * CheckSatResponse
     CheckSatResponse(..)
   , readCheckSatResponse
-    -- * GetModelResonse
+    -- * GetModelResponse
   , GetModelResponse
   , readGetModelResponse
   , ModelResponse(..)

what4/src/What4/Protocol/SMTLib2/Syntax.hs

@@ -49,6 +49,8 @@ module What4.Protocol.SMTLib2.Syntax
   , assertNamed
   , getUnsatAssumptions
   , getUnsatCore
+  , getAbduct
+  , getAbductNext
     -- * Logic
   , Logic(..)
   , qf_bv
@@ -296,7 +298,7 @@ or [] = true
 or [x] = x
 or l = term_app "or" l
 
--- | Disjunction of all terms
+-- | Xor of all terms
 xor :: [Term] -> Term
 xor l@(_:_:_) = term_app "xor" l
 xor _ = error "xor expects two or more arguments."
@@ -305,7 +307,7 @@ xor _ = error "xor expects two or more arguments."
 eq :: [Term] -> Term
 eq = chain_app "="
 
--- | Construct a chainable term with the givne relation
+-- | Construct a chainable term with the given relation
 --
 -- @pairwise_app p [x1, x2, ..., xn]@ is equivalent to
 -- \forall_{i,j} p x_i x_j@.
@@ -826,6 +828,14 @@ getUnsatAssumptions = Cmd "(get-unsat-assumptions)"
 getUnsatCore :: Command
 getUnsatCore = Cmd "(get-unsat-core)"
 
+-- | Get an abduct that entails the formula, and bind it to the name
+getAbduct :: Text -> Term -> Command
+getAbduct nm p = Cmd $ "(get-abduct " <> Builder.fromText nm <> " " <> renderTerm p <> ")"
+
+-- | Get the next command, called after a get-abduct command
+getAbductNext :: Command
+getAbductNext = Cmd "(get-abduct-next)"
+
 -- | Get the values associated with the terms from the last call to @check-sat@.
 getValue :: [Term] -> Command
 getValue values = Cmd $ app "get-value" [builder_list (renderTerm <$> values)]

what4/src/What4/Protocol/SMTWriter.hs

@@ -867,12 +867,18 @@ class (SupportTermOps (Term h)) => SMTWriter h where
   --   later reporting unsatisfiable cores).
   assertNamedCommand :: f h -> Term h -> Text -> Command h
 
-  -- | Push 1 new scope
+  -- | Generates command @(push 1)@ that opens the corresponding assertion frame
   pushCommand   :: f h -> Command h
 
-  -- | Pop 1 existing scope
+  -- | Generates command @(pop 1)@ that closes the corresponding assertion frame
   popCommand    :: f h -> Command h
 
+  -- | Generates command @(push 2)@ that opens the corresponding assertion frame
+  push2Command   :: f h -> Command h
+
+  -- | Generates command @(pop 2)@ that closes the corresponding assertion frame, used for abduction
+  pop2Command    :: f h -> Command h
+
   -- | Pop several scopes.
   popManyCommands :: f h -> Int -> [Command h]
   popManyCommands w n = replicate n (popCommand w)
@@ -898,6 +904,12 @@ class (SupportTermOps (Term h)) => SMTWriter h where
   --   `checkCommand`.
   getUnsatCoreCommand :: f h -> Command h
 
+  -- | Ask the solver to return an abduct
+  getAbductCommand :: f h -> Text -> Term h -> Command h
+
+  -- | Ask the solver for the next abduct, used after a get-abduct command
+  getAbductNextCommand :: f h -> Command h
+
   -- | Set an option/parameter.
   setOptCommand :: f h -> Text -> Text -> Command h
 
@@ -2982,6 +2994,12 @@ class SMTWriter h => SMTReadWriter h where
   --   These correspond to previously-named assertions.
   smtUnsatCoreResult :: f h -> WriterConn t h -> IO [Text]
 
+  -- | Parse an abduct returned by the get-abduct command
+  smtAbductResult :: f h -> WriterConn t h -> Text -> Term h -> IO String
+
+  -- | Parse an abduct returned by the get-abduct-next command
+  smtAbductNextResult :: f h -> WriterConn t h -> IO String
+
   -- | Parse a list of names of assumptions that form an unsatisfiable core.
   --   The boolean indicates the polarity of the atom: true for an ordinary
   --   atom, false for a negated atom.

what4/src/What4/Solver/CVC5.hs

@@ -139,6 +139,7 @@ cvc5Features = useComputableReals
            .|. useDefinedFunctions
            .|. useBitvectors
            .|. useQuantifiers
+           .|. useProduceAbducts
 
 writeMultiAsmpCVC5SMT2File
    :: ExprBuilder t st fs
@@ -190,6 +191,8 @@ instance SMT2.SMTLib2GenericSolver CVC5 where
     SMT2.setLogic writer Syntax.allLogic
     -- Tell cvc5 to produce models
     SMT2.setProduceModels writer True
+    -- Tell cvc5 to produce abducts
+    SMT2.setOption writer "produce-abducts" "true"
 
 runCVC5InOverride
   :: ExprBuilder t st fs
@@ -227,6 +230,9 @@ setInteractiveLogicAndOptions writer = do
     -- Tell cvc5 to compute UNSAT cores, if that feature is enabled
     when (supportedFeatures writer `hasProblemFeature` useUnsatCores) $ do
       SMT2.setOption writer "produce-unsat-cores" "true"
+    -- Tell cvc5 to produce abducts, if that feature is enabled
+    when (supportedFeatures writer `hasProblemFeature` useProduceAbducts) $ do
+      SMT2.setOption writer "produce-abducts" "true"
     -- Tell cvc5 to use all supported logics.
     SMT2.setLogic writer Syntax.allLogic