From 2da1033d731495b4925087f06a082a81cadf97a9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 21 Oct 2021 13:48:56 -0500 Subject: [PATCH] Split utilites from CEGIS core connective module (#7441) Towards a new module for enumerating unsat queries via SyGuS. --- .../sygus/cegis_core_connective.cpp | 74 +------------------ .../quantifiers/sygus/cegis_core_connective.h | 42 +---------- src/theory/smt_engine_subsolver.cpp | 37 ++++++++++ src/theory/smt_engine_subsolver.h | 25 +++++++ 4 files changed, 67 insertions(+), 111 deletions(-) diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 936310e4e..5a0cf8724 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -33,41 +33,6 @@ namespace cvc5 { namespace theory { namespace quantifiers { -bool VariadicTrie::add(Node n, const std::vector& i) -{ - VariadicTrie* curr = this; - for (const Node& ic : i) - { - curr = &(curr->d_children[ic]); - } - if (curr->d_data.isNull()) - { - curr->d_data = n; - return true; - } - return false; -} - -bool VariadicTrie::hasSubset(const std::vector& is) const -{ - if (!d_data.isNull()) - { - return true; - } - for (const std::pair& p : d_children) - { - Node n = p.first; - if (std::find(is.begin(), is.end(), n) != is.end()) - { - if (p.second.hasSubset(is)) - { - return true; - } - } - } - return false; -} - CegisCoreConnective::CegisCoreConnective(Env& env, QuantifiersState& qs, QuantifiersInferenceManager& qim, @@ -595,38 +560,6 @@ bool CegisCoreConnective::Component::addToAsserts(CegisCoreConnective* p, return true; } -void CegisCoreConnective::getModel(SolverEngine& smt, - std::vector& vals) const -{ - for (const Node& v : d_vars) - { - Node mv = smt.getValue(v); - Trace("sygus-ccore-model") << v << " -> " << mv << " "; - vals.push_back(mv); - } -} - -bool CegisCoreConnective::getUnsatCore( - SolverEngine& smt, - const std::unordered_set& queryAsserts, - std::vector& uasserts) const -{ - UnsatCore uc = smt.getUnsatCore(); - bool hasQuery = false; - for (UnsatCore::const_iterator i = uc.begin(); i != uc.end(); ++i) - { - Node uassert = *i; - Trace("sygus-ccore-debug") << " uc " << uassert << std::endl; - if (queryAsserts.find(uassert) != queryAsserts.end()) - { - hasQuery = true; - continue; - } - uasserts.push_back(uassert); - } - return hasQuery; -} - Result CegisCoreConnective::checkSat(Node n, std::vector& mvs) const { Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl; @@ -758,7 +691,8 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, std::unordered_set queryAsserts; queryAsserts.insert(ccheck.getFormula()); queryAsserts.insert(d_sc); - bool hasQuery = getUnsatCore(*checkSol, queryAsserts, uasserts); + bool hasQuery = + getUnsatCoreFromSubsolver(*checkSol, queryAsserts, uasserts); // now, check the side condition bool falseCore = false; if (!d_sc.isNull()) @@ -794,7 +728,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, uasserts.clear(); std::unordered_set queryAsserts2; queryAsserts2.insert(d_sc); - getUnsatCore(*checkSc, queryAsserts2, uasserts); + getUnsatCoreFromSubsolver(*checkSc, queryAsserts2, uasserts); falseCore = true; } } @@ -838,7 +772,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, // it does not entail the postcondition, add an assertion that blocks // the current point mvs.clear(); - getModel(*checkSol, mvs); + getModelFromSubsolver(*checkSol, d_vars, mvs); // should evaluate to true Node ean = evaluatePt(an, Node::null(), mvs); Assert(ean.isConst() && ean.getConst()); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index 3ee631dea..26784f939 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -22,6 +22,7 @@ #include "expr/node.h" #include "expr/node_trie.h" +#include "expr/variadic_trie.h" #include "smt/env_obj.h" #include "theory/quantifiers/sygus/cegis.h" #include "util/result.h" @@ -33,30 +34,6 @@ class SolverEngine; namespace theory { namespace quantifiers { -/** - * A trie that stores data at undetermined depth. Storing data at - * undetermined depth is in contrast to the NodeTrie (expr/node_trie.h), which - * assumes all data is stored at a fixed depth. - * - * Since data can be stored at any depth, we require both a d_children field - * and a d_data field. - */ -class VariadicTrie -{ - public: - /** the children of this node */ - std::map d_children; - /** the data at this node */ - Node d_data; - /** - * Add data with identifier n indexed by i, return true if data is not already - * stored at the node indexed by i. - */ - bool add(Node n, const std::vector& i); - /** Is there any data in this trie that is indexed by any subset of is? */ - bool hasSubset(const std::vector& is) const; -}; - /** CegisCoreConnective * * A sygus module that is specialized in handling conjectures of the form: @@ -335,23 +312,6 @@ class CegisCoreConnective : public Cegis */ Node d_sc; //-----------------------------------for SMT engine calls - /** - * Assuming smt has just been called to check-sat and returned "SAT", this - * method adds the model for d_vars to mvs. - */ - void getModel(SolverEngine& smt, std::vector& mvs) const; - /** - * Assuming smt has just been called to check-sat and returned "UNSAT", this - * method get the unsat core and adds it to uasserts. - * - * 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(SolverEngine& smt, - const std::unordered_set& queryAsserts, - std::vector& 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. diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index 99e3f7768..d22bde370 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -16,6 +16,7 @@ #include "theory/smt_engine_subsolver.h" +#include "proof/unsat_core.h" #include "smt/env.h" #include "smt/solver_engine.h" #include "smt/solver_engine_scope.h" @@ -137,5 +138,41 @@ Result checkWithSubsolver(Node query, return r; } +void getModelFromSubsolver(SolverEngine& smt, + const std::vector& vars, + std::vector& vals) +{ + for (const Node& v : vars) + { + Node mv = smt.getValue(v); + vals.push_back(mv); + } +} + +bool getUnsatCoreFromSubsolver(SolverEngine& smt, + const std::unordered_set& queryAsserts, + std::vector& uasserts) +{ + UnsatCore uc = smt.getUnsatCore(); + bool hasQuery = false; + for (UnsatCore::const_iterator i = uc.begin(); i != uc.end(); ++i) + { + Node uassert = *i; + if (queryAsserts.find(uassert) != queryAsserts.end()) + { + hasQuery = true; + continue; + } + uasserts.push_back(uassert); + } + return hasQuery; +} + +void getUnsatCoreFromSubsolver(SolverEngine& smt, std::vector& uasserts) +{ + std::unordered_set queryAsserts; + getUnsatCoreFromSubsolver(smt, queryAsserts, uasserts); +} + } // namespace theory } // namespace cvc5 diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h index 0e1af29db..5de65a5d2 100644 --- a/src/theory/smt_engine_subsolver.h +++ b/src/theory/smt_engine_subsolver.h @@ -113,6 +113,31 @@ Result checkWithSubsolver(Node query, bool needsTimeout = false, unsigned long timeout = 0); +//--------------- utilities + +/** + * Assuming smt has just been called to check-sat and returned "SAT", this + * method adds the model for d_vars to mvs. + */ +void getModelFromSubsolver(SolverEngine& smt, + const std::vector& vars, + std::vector& mvs); + +/** + * Assuming smt has just been called to check-sat and returned "UNSAT", this + * method get the unsat core and adds it to uasserts. + * + * 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 getUnsatCoreFromSubsolver(SolverEngine& smt, + const std::unordered_set& queryAsserts, + std::vector& uasserts); +/** Same as above, without query asserts */ +void getUnsatCoreFromSubsolver(SolverEngine& smt, std::vector& uasserts); + } // namespace theory } // namespace cvc5 -- 2.30.2