From 47b910a85de71b6617e4d1d210dcb57de597961b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 13 Aug 2019 10:39:45 -0500 Subject: Implement check abduct feature (#3152) --- src/smt/smt_engine.h | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'src/smt/smt_engine.h') 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 d_sssfVarlist; std::vector 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 -- cgit v1.2.3