From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 17 Jan 2020 20:24:03 +0000 (-0600)
Subject: Use axioms when checking goal entailment for abduction algorithm (#3611)
X-Git-Tag: cvc5-1.0.0~3733
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=77eb7c81060ae590a5ae1bbab88c7e21d57b39b9;p=cvc5.git

Use axioms when checking goal entailment for abduction algorithm (#3611)
---

diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index a924873d0..d1bd5db63 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -603,9 +603,10 @@ void CegisCoreConnective::getModel(SmtEngine& smt,
   }
 }
 
-bool CegisCoreConnective::getUnsatCore(SmtEngine& smt,
-                                       Node query,
-                                       std::vector<Node>& uasserts) const
+bool CegisCoreConnective::getUnsatCore(
+    SmtEngine& smt,
+    const std::unordered_set<Node, NodeHashFunction>& queryAsserts,
+    std::vector<Node>& uasserts) const
 {
   UnsatCore uc = smt.getUnsatCore();
   bool hasQuery = false;
@@ -613,7 +614,7 @@ bool CegisCoreConnective::getUnsatCore(SmtEngine& smt,
   {
     Node uassert = Node::fromExpr(*i);
     Trace("sygus-ccore-debug") << "  uc " << uassert << std::endl;
-    if (uassert == query)
+    if (queryAsserts.find(uassert) != queryAsserts.end())
     {
       hasQuery = true;
       continue;
@@ -766,6 +767,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
     checkSol.setLogic(smt::currentSmtEngine()->getLogicInfo());
     Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
     std::vector<Node> rasserts = asserts;
+    rasserts.push_back(d_sc);
     rasserts.push_back(ccheck.getFormula());
     std::shuffle(rasserts.begin(), rasserts.end(), Random::getRandom());
     Node query = rasserts.size() == 1 ? rasserts[0] : nm->mkNode(AND, rasserts);
@@ -775,15 +777,18 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
     }
     Result r = checkSol.checkSat();
     Trace("sygus-ccore") << "----- check-sat returned " << r << std::endl;
-    // In terms of Variant #2, this is the check "if D => B"
+    // In terms of Variant #2, this is the check "if (S ^ D) => B"
     if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
     {
       // it entails the postcondition, now get the unsat core
       // In terms of Variant #2, this is the line
-      //   "Let U be a subset of D such that U ^ ~B is unsat."
+      //   "Let U be a subset of D such that S ^ U ^ ~B is unsat."
       // and uasserts is set to U.
       std::vector<Node> uasserts;
-      bool hasQuery = getUnsatCore(checkSol, ccheck.getFormula(), uasserts);
+      std::unordered_set<Node, NodeHashFunction> queryAsserts;
+      queryAsserts.insert(ccheck.getFormula());
+      queryAsserts.insert(d_sc);
+      bool hasQuery = getUnsatCore(checkSol, queryAsserts, uasserts);
       // now, check the side condition
       bool falseCore = false;
       if (!d_sc.isNull())
@@ -818,7 +823,9 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
             //   "Let W be a subset of D such that S ^ W is unsat."
             // and uasserts is set to W.
             uasserts.clear();
-            getUnsatCore(checkSc, d_sc, uasserts);
+            std::unordered_set<Node, NodeHashFunction> queryAsserts;
+            queryAsserts.insert(d_sc);
+            getUnsatCore(checkSc, queryAsserts, uasserts);
             falseCore = true;
           }
         }
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h
index 3589d97e5..a55cee564 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.h
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.h
@@ -139,8 +139,8 @@ class VariadicTrie
  *   {
  *     D += { d' }
  *     if D is false for all v in pts(B)
- *       if D => B
- *         Let U be a subset of D such that U ^ ~B is unsat.
+ *       if (S ^ D) => B
+ *         Let U be a subset of D such that S ^ U ^ ~B is unsat.
  *         if S ^ U is unsat
  *           Let W be a subset of D such that S ^ W is unsat.
  *             cores(B) += W
@@ -337,13 +337,15 @@ class CegisCoreConnective : public Cegis
    * Assuming smt has just been called to check-sat and returned "UNSAT", this
    * method get the unsat core and adds it to uasserts.
    *
-   * If query is non-null, then it is excluded from uasserts. If query was
-   * in the unsat core, then this method returns true. Otherwise, this method
-   * returns false. It also returns false if query was null.
+   * The assertions in the argument queryAsserts (which we are not interested
+   * in tracking in the unsat core) are excluded from uasserts.
+   * If one of the formulas in queryAsserts was in the unsat core, then this
+   * method returns true. Otherwise, this method returns false.
    */
-  bool getUnsatCore(SmtEngine& smt,
-                    Node query,
-                    std::vector<Node>& uasserts) const;
+  bool getUnsatCore(
+      SmtEngine& smt,
+      const std::unordered_set<Node, NodeHashFunction>& queryAsserts,
+      std::vector<Node>& uasserts) const;
   /**
    * Return the result of checking satisfiability of formula n.
    * If n was satisfiable, then we store the model for d_vars in mvs.