diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-13 10:39:45 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-13 10:39:45 -0500 |
commit | 47b910a85de71b6617e4d1d210dcb57de597961b (patch) | |
tree | 2319441716ca0c10042e011579c67814334fd5b3 /src/smt/smt_engine.h | |
parent | 2267c5050fafde26b34dc1e84de015617efa7cc7 (diff) |
Implement check abduct feature (#3152)
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index ead337862..f783b0a33 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -175,6 +175,11 @@ class CVC4_PUBLIC SmtEngine { */ std::vector<Node> d_sssfVarlist; std::vector<Node> d_sssfSyms; + /** + * The conjecture of the current abduction problem. This expression is only + * valid while we are in mode SMT_MODE_ABDUCT. + */ + Expr d_abdConj; /** recursive function definition abstractions for --fmf-fun */ std::map< Node, TypeNode > d_fmfRecFunctionsAbs; std::map< Node, std::vector< Node > > d_fmfRecFunctionsConcrete; @@ -360,6 +365,15 @@ class CVC4_PUBLIC SmtEngine { * unsatisfiable. If not, then the found solutions are wrong. */ void checkSynthSolution(); + /** + * Check that a solution to an abduction conjecture is indeed a solution. + * + * The check is made by determining that the assertions conjoined with the + * solution to the abduction problem (a) is SAT, and the assertions conjoined + * with the abduct and the goal is UNSAT. If these criteria are not met, an + * internal error is thrown. + */ + void checkAbduct(Expr a); /** * Postprocess a value for output to the user. Involves doing things |