diff options
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_core_connective.cpp | 23 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis_core_connective.h | 18 |
2 files changed, 25 insertions, 16 deletions
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. |