diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-29 13:58:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-07-29 13:58:09 -0500 |
commit | 90eddb069c3c9abf96719ac20aff45b44af86207 (patch) | |
tree | 5e9b48565fdcc33ecbc094ae5e14101e6e4ccb3c /src/smt/smt_engine.h | |
parent | 3aba99657b39ccc0ab400c7ed9778673a3acddd7 (diff) |
Support get-abduct smt2 command (#3122)
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 5913716e6..566777a89 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -147,6 +147,34 @@ class CVC4_PUBLIC SmtEngine { ProofManager* d_proofManager; /** An index of our defined functions */ DefinedFunctionMap* d_definedFunctions; + /** The SMT engine subsolver + * + * This is a separate copy of the SMT engine which is used for making + * calls that cannot be answered by this copy of the SMT engine. An example + * of invoking this subsolver is the get-abduct command, where we wish to + * solve a sygus conjecture based on the current assertions. In particular, + * consider the input: + * (assert A) + * (get-abduct B) + * In the copy of the SMT engine where these commands are issued, we maintain + * A in the assertion stack. To solve the abduction problem, instead of + * modifying the assertion stack to remove A and add the sygus conjecture + * (exists I. ...), we invoke a fresh copy of the SMT engine and leave the + * assertion stack unchaged. This copy of the SMT engine can be further + * queried for information regarding further solutions. + */ + std::unique_ptr<SmtEngine> d_subsolver; + /** + * If applicable, the function-to-synthesize that the subsolver is solving + * for. This is used for the get-abduct command. + */ + Expr d_sssf; + /** + * The substitution to apply to the solutions from the subsolver, used for + * the get-abduct command. + */ + std::vector<Node> d_sssfVarlist; + std::vector<Node> d_sssfSyms; /** recursive function definition abstractions for --fmf-fun */ std::map< Node, TypeNode > d_fmfRecFunctionsAbs; std::map< Node, std::vector< Node > > d_fmfRecFunctionsConcrete; @@ -849,6 +877,21 @@ class CVC4_PUBLIC SmtEngine { Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict = true) /* throw(Exception) */; + /** + * This method asks this SMT engine to find an abduct with respect to the + * current assertion stack (call it A) and the conjecture (call it B). + * If this method returns true, then abd is set to a formula C such that + * A ^ C is satisfiable, and A ^ B ^ C is unsatisfiable. + * + * The argument grammarType is a sygus datatype type that encodes the syntax + * restrictions on the shape of possible solutions. + * + * This method invokes a separate copy of the SMT engine for solving the + * corresponding sygus problem for generating such a solution. + */ + bool getAbduct(const Expr& conj, const Type& grammarType, Expr& abd); + /** Same as above, but without user-provided grammar restrictions */ + bool getAbduct(const Expr& conj, Expr& abd); /** * Get list of quantified formulas that were instantiated |