From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 13 Aug 2019 15:39:45 +0000 (-0500)
Subject: Implement check abduct feature (#3152)
X-Git-Tag: cvc5-1.0.0~4026
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=47b910a85de71b6617e4d1d210dcb57de597961b;p=cvc5.git

Implement check abduct feature (#3152)
---

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 733819780..394875fae 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -634,3 +634,12 @@ header = "options/smt_options.h"
   default    = "false"
   read_only  = true
   help       = "support the get-abduct command"
+
+[[option]]
+  name       = "checkAbducts"
+  category   = "regular"
+  long       = "check-abducts"
+  type       = "bool"
+  default    = "false"
+  read_only  = true
+  help       = "checks whether produced solutions to get-abduct are correct"
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
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 8918c75c1..61b89d9c5 100755
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -293,6 +293,10 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, wrapper,
                '--unconstrained-simp' not in all_args and \
                not cvc4_binary.endswith('pcvc4'):
                 extra_command_line_args += ['--check-unsat-cores']
+        if '--no-check-abducts' not in all_args and \
+            '--check-abducts' not in all_args and \
+            not cvc4_binary.endswith('pcvc4'):
+            extra_command_line_args += ['--check-abducts']
         if extra_command_line_args:
             command_line_args_configs.append(all_args +
                                              extra_command_line_args)