Implement check abduct feature (#3152)

2 files changed, 85 insertions, 0 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b66d230b7..e9c3f06ae 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4919,6 +4919,70 @@ void SmtEngine::checkSynthSolution()
   }
 }
 
+void SmtEngine::checkAbduct(Expr a)
+{
+  Assert(a.getType().isBoolean());
+  Trace("check-abduct") << "SmtEngine::checkAbduct: get expanded assertions"
+                        << std::endl;
+
+  std::vector<Expr> asserts = getExpandedAssertions();
+  asserts.push_back(a);
+
+  // two checks: first, consistent with assertions, second, implies negated goal
+  // is unsatisfiable.
+  for (unsigned j = 0; j < 2; j++)
+  {
+    Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
+                          << ": make new SMT engine" << std::endl;
+    // Start new SMT engine to check solution
+    SmtEngine abdChecker(d_exprManager);
+    abdChecker.setLogic(getLogicInfo());
+    Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
+                          << ": asserting formulas" << std::endl;
+    for (const Expr& e : asserts)
+    {
+      abdChecker.assertFormula(e);
+    }
+    Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
+                          << ": check the assertions" << std::endl;
+    Result r = abdChecker.checkSat();
+    Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
+                          << ": result is " << r << endl;
+    std::stringstream serr;
+    bool isError = false;
+    if (j == 0)
+    {
+      if (r.asSatisfiabilityResult().isSat() != Result::SAT)
+      {
+        isError = true;
+        serr << "SmtEngine::checkAbduct(): produced solution cannot be shown "
+                "to be consisconsistenttent with assertions, result was "
+             << r;
+      }
+      Trace("check-abduct")
+          << "SmtEngine::checkAbduct: goal is " << d_abdConj << std::endl;
+      // add the goal to the set of assertions
+      Assert(!d_abdConj.isNull());
+      asserts.push_back(d_abdConj);
+    }
+    else
+    {
+      if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+      {
+        isError = true;
+        serr << "SmtEngine::checkAbduct(): negated goal cannot be shown "
+                "unsatisfiable with produced solution, result was "
+             << r;
+      }
+    }
+    // did we get an unexpected result?
+    if (isError)
+    {
+      InternalError(serr.str().c_str());
+    }
+  }
+}
+
 // TODO(#1108): Simplify the error reporting of this method.
 UnsatCore SmtEngine::getUnsatCore() {
   Trace("smt") << "SMT getUnsatCore()" << endl;
@@ -5081,6 +5145,7 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd)
   std::vector<Node> asserts(axioms.begin(), axioms.end());
   // negate the conjecture
   Node conjn = Node::fromExpr(conj).negate();
+  d_abdConj = conjn.toExpr();
   asserts.push_back(conjn);
   d_sssfVarlist.clear();
   d_sssfSyms.clear();
@@ -5153,6 +5218,12 @@ bool SmtEngine::getAbductInternal(Expr& abd)
 
       // convert to expression
       abd = abdn.toExpr();
+
+      // if check abducts option is set, we check the correctness
+      if (options::checkAbducts())
+      {
+        checkAbduct(abd);
+      }
       return true;
     }
     Trace("sygus-abduct") << "SmtEngine::getAbduct: could not find solution!"
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