diff options
Diffstat (limited to 'src/theory')
50 files changed, 2755 insertions, 733 deletions
diff --git a/src/theory/arith/nl_constraint.cpp b/src/theory/arith/nl/nl_constraint.cpp index 8fb4535ea..c4c4dfbe7 100644 --- a/src/theory/arith/nl_constraint.cpp +++ b/src/theory/arith/nl/nl_constraint.cpp @@ -12,7 +12,7 @@ ** \brief Implementation of utilities for non-linear constraints **/ -#include "theory/arith/nl_constraint.h" +#include "theory/arith/nl/nl_constraint.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" @@ -22,6 +22,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { namespace arith { +namespace nl { ConstraintDb::ConstraintDb(MonomialDb& mdb) : d_mdb(mdb) {} @@ -118,6 +119,7 @@ bool ConstraintDb::isMaximal(Node atom, Node x) const return itcm->second.find(x) != itcm->second.end(); } +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_constraint.h b/src/theory/arith/nl/nl_constraint.h index faa3cc812..e86ac4b66 100644 --- a/src/theory/arith/nl_constraint.h +++ b/src/theory/arith/nl/nl_constraint.h @@ -12,19 +12,20 @@ ** \brief Utilities for non-linear constraints **/ -#ifndef CVC4__THEORY__ARITH__NL_CONSTRAINT_H -#define CVC4__THEORY__ARITH__NL_CONSTRAINT_H +#ifndef CVC4__THEORY__ARITH__NL__NL_CONSTRAINT_H +#define CVC4__THEORY__ARITH__NL__NL_CONSTRAINT_H #include <map> #include <vector> #include "expr/kind.h" #include "expr/node.h" -#include "theory/arith/nl_monomial.h" +#include "theory/arith/nl/nl_monomial.h" namespace CVC4 { namespace theory { namespace arith { +namespace nl { /** constraint information * @@ -79,6 +80,7 @@ class ConstraintDb std::map<Node, std::map<Node, ConstraintInfo> > d_c_info; }; +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp index e43a77b06..ca34d91a9 100644 --- a/src/theory/arith/nl_lemma_utils.cpp +++ b/src/theory/arith/nl/nl_lemma_utils.cpp @@ -12,13 +12,14 @@ ** \brief Implementation of utilities for the non-linear solver **/ -#include "theory/arith/nl_lemma_utils.h" +#include "theory/arith/nl/nl_lemma_utils.h" -#include "theory/arith/nl_model.h" +#include "theory/arith/nl/nl_model.h" namespace CVC4 { namespace theory { namespace arith { +namespace nl { bool SortNlModel::operator()(Node i, Node j) { @@ -58,6 +59,7 @@ Node ArgTrie::add(Node d, const std::vector<Node>& args) return at->d_data; } +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h index bd729dad9..64a4deb17 100644 --- a/src/theory/arith/nl_lemma_utils.h +++ b/src/theory/arith/nl/nl_lemma_utils.h @@ -12,8 +12,8 @@ ** \brief Utilities for processing lemmas from the non-linear solver **/ -#ifndef CVC4__THEORY__ARITH__NL_LEMMA_UTILS_H -#define CVC4__THEORY__ARITH__NL_LEMMA_UTILS_H +#ifndef CVC4__THEORY__ARITH__NL__NL_LEMMA_UTILS_H +#define CVC4__THEORY__ARITH__NL__NL_LEMMA_UTILS_H #include <tuple> #include <vector> @@ -22,6 +22,7 @@ namespace CVC4 { namespace theory { namespace arith { +namespace nl { class NlModel; @@ -98,6 +99,7 @@ class ArgTrie Node add(Node d, const std::vector<Node>& args); }; +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index 0d47c8874..d5df96bd8 100644 --- a/src/theory/arith/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -12,7 +12,7 @@ ** \brief Model object for the non-linear extension class **/ -#include "theory/arith/nl_model.h" +#include "theory/arith/nl/nl_model.h" #include "expr/node_algorithm.h" #include "options/arith_options.h" @@ -25,6 +25,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { namespace arith { +namespace nl { NlModel::NlModel(context::Context* c) : d_used_approx(false) { @@ -320,7 +321,7 @@ bool NlModel::checkModel(const std::vector<Node>& assertions, Node mg = nm->mkSkolem("model", nm->booleanType()); gs.push_back(mg); // assert the constructed model as assertions - for (const std::pair<const Node, std::pair<Node, Node> > cb : + for (const std::pair<const Node, std::pair<Node, Node>> cb : d_check_model_bounds) { Node l = cb.second.first; @@ -350,7 +351,7 @@ bool NlModel::addCheckModelSubstitution(TNode v, TNode s) } // if we previously had an approximate bound, the exact bound should be in its // range - std::map<Node, std::pair<Node, Node> >::iterator itb = + std::map<Node, std::pair<Node, Node>>::iterator itb = d_check_model_bounds.find(v); if (itb != d_check_model_bounds.end()) { @@ -852,7 +853,7 @@ bool NlModel::simpleCheckModelLit(Node lit) for (const Node& v : vs) { // is it a valid variable? - std::map<Node, std::pair<Node, Node> >::iterator bit = + std::map<Node, std::pair<Node, Node>>::iterator bit = d_check_model_bounds.find(v); if (!expr::hasSubterm(invalid_vsum, v) && bit != d_check_model_bounds.end()) { @@ -1041,7 +1042,7 @@ bool NlModel::simpleCheckModelMsum(const std::map<Node, Node>& msum, bool pol) } Trace("nl-ext-cms-debug") << " "; } - std::map<Node, std::pair<Node, Node> >::iterator bit = + std::map<Node, std::pair<Node, Node>>::iterator bit = d_check_model_bounds.find(vc); // if there is a model bound for this term if (bit != d_check_model_bounds.end()) @@ -1284,7 +1285,7 @@ void NlModel::getModelValueRepair( // values for variables that we solved for, using techniques specific to // this class. NodeManager* nm = NodeManager::currentNM(); - for (const std::pair<const Node, std::pair<Node, Node> >& cb : + for (const std::pair<const Node, std::pair<Node, Node>>& cb : d_check_model_bounds) { Node l = cb.second.first; @@ -1342,6 +1343,7 @@ void NlModel::getModelValueRepair( } } +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_model.h b/src/theory/arith/nl/nl_model.h index 5129a7a32..61193fc12 100644 --- a/src/theory/arith/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -12,8 +12,8 @@ ** \brief Model object for the non-linear extension class **/ -#ifndef CVC4__THEORY__ARITH__NL_MODEL_H -#define CVC4__THEORY__ARITH__NL_MODEL_H +#ifndef CVC4__THEORY__ARITH__NL__NL_MODEL_H +#define CVC4__THEORY__ARITH__NL__NL_MODEL_H #include <map> #include <unordered_map> @@ -28,6 +28,7 @@ namespace CVC4 { namespace theory { namespace arith { +namespace nl { class NonlinearExtension; @@ -307,7 +308,7 @@ class NlModel * (2) variables we have solved quadratic equations for, whose value * involves approximations of square roots. */ - std::map<Node, std::pair<Node, Node> > d_check_model_bounds; + std::map<Node, std::pair<Node, Node>> d_check_model_bounds; /** * The map from literals that our model construction solved, to the variable * that was solved for. Examples of such literals are: @@ -326,6 +327,7 @@ class NlModel std::unordered_set<Node, NodeHashFunction> d_tautology; }; /* class NlModel */ +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_monomial.cpp b/src/theory/arith/nl/nl_monomial.cpp index be472217d..e8e7aceba 100644 --- a/src/theory/arith/nl_monomial.cpp +++ b/src/theory/arith/nl/nl_monomial.cpp @@ -12,10 +12,10 @@ ** \brief Implementation of utilities for monomials **/ -#include "theory/arith/nl_monomial.h" +#include "theory/arith/nl/nl_monomial.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/nl_lemma_utils.h" +#include "theory/arith/nl/nl_lemma_utils.h" #include "theory/rewriter.h" using namespace CVC4::kind; @@ -23,6 +23,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { namespace arith { +namespace nl { // Returns a[key] if key is in a or value otherwise. unsigned getCountWithDefault(const NodeMultiset& a, Node key, unsigned value) @@ -329,6 +330,7 @@ Node MonomialDb::mkMonomialRemFactor(Node n, return ret; } +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_monomial.h b/src/theory/arith/nl/nl_monomial.h index 81665c4d9..b226730ac 100644 --- a/src/theory/arith/nl_monomial.h +++ b/src/theory/arith/nl/nl_monomial.h @@ -12,8 +12,8 @@ ** \brief Utilities for monomials **/ -#ifndef CVC4__THEORY__ARITH__NL_MONOMIAL_H -#define CVC4__THEORY__ARITH__NL_MONOMIAL_H +#ifndef CVC4__THEORY__ARITH__NL__NL_MONOMIAL_H +#define CVC4__THEORY__ARITH__NL__NL_MONOMIAL_H #include <map> #include <vector> @@ -23,6 +23,7 @@ namespace CVC4 { namespace theory { namespace arith { +namespace nl { class MonomialDb; class NlModel; @@ -140,6 +141,7 @@ class MonomialDb std::map<Node, std::map<Node, Node> > d_m_contain_umult; }; +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_solver.cpp b/src/theory/arith/nl/nl_solver.cpp index 893d3dbd7..12cb02c70 100644 --- a/src/theory/arith/nl_solver.cpp +++ b/src/theory/arith/nl/nl_solver.cpp @@ -12,7 +12,7 @@ ** \brief Implementation of non-linear solver **/ -#include "theory/arith/nl_solver.h" +#include "theory/arith/nl/nl_solver.h" #include "options/arith_options.h" #include "theory/arith/arith_msum.h" @@ -25,6 +25,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { namespace arith { +namespace nl { void debugPrintBound(const char* c, Node coeff, Node x, Kind type, Node rhs) { @@ -1580,6 +1581,7 @@ std::vector<Node> NlSolver::checkMonomialInferResBounds() return lemmas; } +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_solver.h b/src/theory/arith/nl/nl_solver.h index 73ca97f00..35c51569b 100644 --- a/src/theory/arith/nl_solver.h +++ b/src/theory/arith/nl/nl_solver.h @@ -27,15 +27,16 @@ #include "context/context.h" #include "expr/kind.h" #include "expr/node.h" -#include "theory/arith/nl_constraint.h" -#include "theory/arith/nl_lemma_utils.h" -#include "theory/arith/nl_model.h" -#include "theory/arith/nl_monomial.h" +#include "theory/arith/nl/nl_constraint.h" +#include "theory/arith/nl/nl_lemma_utils.h" +#include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/nl_monomial.h" #include "theory/arith/theory_arith.h" namespace CVC4 { namespace theory { namespace arith { +namespace nl { typedef std::map<Node, unsigned> NodeMultiset; @@ -361,6 +362,7 @@ class NlSolver Node getFactorSkolem(Node n, std::vector<Node>& lemmas); }; /* class NlSolver */ +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index b638d8a59..4b2d2fd37 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -15,7 +15,7 @@ ** \todo document this file **/ -#include "theory/arith/nonlinear_extension.h" +#include "theory/arith/nl/nonlinear_extension.h" #include "options/arith_options.h" #include "theory/arith/arith_utilities.h" @@ -28,6 +28,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { namespace arith { +namespace nl { NonlinearExtension::NonlinearExtension(TheoryArith& containing, eq::EqualityEngine* ee) @@ -49,27 +50,37 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, NonlinearExtension::~NonlinearExtension() {} bool NonlinearExtension::getCurrentSubstitution( - int effort, const std::vector<Node>& vars, std::vector<Node>& subs, - std::map<Node, std::vector<Node> >& exp) { + int effort, + const std::vector<Node>& vars, + std::vector<Node>& subs, + std::map<Node, std::vector<Node>>& exp) +{ // get the constant equivalence classes - std::map<Node, std::vector<int> > rep_to_subs_index; + std::map<Node, std::vector<int>> rep_to_subs_index; bool retVal = false; - for (unsigned i = 0; i < vars.size(); i++) { + for (unsigned i = 0; i < vars.size(); i++) + { Node n = vars[i]; - if (d_ee->hasTerm(n)) { + if (d_ee->hasTerm(n)) + { Node nr = d_ee->getRepresentative(n); - if (nr.isConst()) { + if (nr.isConst()) + { subs.push_back(nr); Trace("nl-subs") << "Basic substitution : " << n << " -> " << nr << std::endl; exp[n].push_back(n.eqNode(nr)); retVal = true; - } else { + } + else + { rep_to_subs_index[nr].push_back(i); subs.push_back(n); } - } else { + } + else + { subs.push_back(n); } } @@ -79,8 +90,10 @@ bool NonlinearExtension::getCurrentSubstitution( } std::pair<bool, Node> NonlinearExtension::isExtfReduced( - int effort, Node n, Node on, const std::vector<Node>& exp) const { - if (n != d_zero) { + int effort, Node n, Node on, const std::vector<Node>& exp) const +{ + if (n != d_zero) + { Kind k = n.getKind(); return std::make_pair(k != NONLINEAR_MULT && !isTranscendentalKind(k), Node::null()); @@ -88,15 +101,15 @@ std::pair<bool, Node> NonlinearExtension::isExtfReduced( Assert(n == d_zero); if (on.getKind() == NONLINEAR_MULT) { - Trace("nl-ext-zero-exp") << "Infer zero : " << on << " == " << n - << std::endl; + Trace("nl-ext-zero-exp") + << "Infer zero : " << on << " == " << n << std::endl; // minimize explanation if a substitution+rewrite results in zero const std::set<Node> vars(on.begin(), on.end()); for (unsigned i = 0, size = exp.size(); i < size; i++) { - Trace("nl-ext-zero-exp") << " exp[" << i << "] = " << exp[i] - << std::endl; + Trace("nl-ext-zero-exp") + << " exp[" << i << "] = " << exp[i] << std::endl; std::vector<Node> eqs; if (exp[i].getKind() == EQUAL) { @@ -119,8 +132,8 @@ std::pair<bool, Node> NonlinearExtension::isExtfReduced( { if (eqs[j][r] == d_zero && vars.find(eqs[j][1 - r]) != vars.end()) { - Trace("nl-ext-zero-exp") << "...single exp : " << eqs[j] - << std::endl; + Trace("nl-ext-zero-exp") + << "...single exp : " << eqs[j] << std::endl; return std::make_pair(true, eqs[j]); } } @@ -337,9 +350,10 @@ std::vector<Node> NonlinearExtension::checkModelEval( const std::vector<Node>& assertions) { std::vector<Node> false_asserts; - for (size_t i = 0; i < assertions.size(); ++i) { + for (size_t i = 0; i < assertions.size(); ++i) + { Node lit = assertions[i]; - Node atom = lit.getKind()==NOT ? lit[0] : lit; + Node atom = lit.getKind() == NOT ? lit[0] : lit; Node litv = d_model.computeConcreteModelValue(lit); Trace("nl-ext-mv-assert") << "M[[ " << lit << " ]] -> " << litv; if (litv != d_true) @@ -403,7 +417,8 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, } //----------------------------------- possibly split on zero - if (options::nlExtSplitZero()) { + if (options::nlExtSplitZero()) + { Trace("nl-ext") << "Get zero split lemmas..." << std::endl; lemmas = d_nlSlv.checkSplitZero(); filterLemmas(lemmas, lems); @@ -415,7 +430,8 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, } } - //-----------------------------------initial lemmas for transcendental functions + //-----------------------------------initial lemmas for transcendental + //functions lemmas = d_trSlv.checkTranscendentalInitialRefine(); filterLemmas(lemmas, lems); if (!lems.empty()) @@ -445,8 +461,10 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, return lems.size(); } - //-----------------------------------lemmas based on magnitude of non-zero monomials - for (unsigned c = 0; c < 3; c++) { + //-----------------------------------lemmas based on magnitude of non-zero + //monomials + for (unsigned c = 0; c < 3; c++) + { // c is effort level lemmas = d_nlSlv.checkMonomialMagnitude(c); unsigned nlem = lemmas.size(); @@ -462,7 +480,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, //-----------------------------------inferred bounds lemmas // e.g. x >= t => y*x >= y*t - std::vector< Node > nt_lemmas; + std::vector<Node> nt_lemmas; lemmas = d_nlSlv.checkMonomialInferBounds(nt_lemmas, assertions, false_asserts); // Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " << @@ -494,7 +512,8 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, //------------------------------------factoring lemmas // x*y + x*z >= t => exists k. k = y + z ^ x*k >= t - if( options::nlExtFactor() ){ + if (options::nlExtFactor()) + { lemmas = d_nlSlv.checkFactoring(assertions, false_asserts); filterLemmas(lemmas, lems); if (!lems.empty()) @@ -507,7 +526,8 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, //------------------------------------resolution bound inferences // e.g. ( y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t - if (options::nlExtResBound()) { + if (options::nlExtResBound()) + { lemmas = d_nlSlv.checkMonomialInferResBounds(); filterLemmas(lemmas, lems); if (!lems.empty()) @@ -517,7 +537,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, return lems.size(); } } - + //------------------------------------tangent planes if (options::nlExtTangentPlanes() && !options::nlExtTangentPlanesInterleave()) { @@ -535,7 +555,8 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, return 0; } -void NonlinearExtension::check(Theory::Effort e) { +void NonlinearExtension::check(Theory::Effort e) +{ Trace("nl-ext") << std::endl; Trace("nl-ext") << "NonlinearExtension::check, effort = " << e << ", built model = " << d_builtModel.get() << std::endl; @@ -543,15 +564,20 @@ void NonlinearExtension::check(Theory::Effort e) { { d_containing.getExtTheory()->clearCache(); d_needsLastCall = true; - if (options::nlExtRewrites()) { + if (options::nlExtRewrites()) + { std::vector<Node> nred; - if (!d_containing.getExtTheory()->doInferences(0, nred)) { + if (!d_containing.getExtTheory()->doInferences(0, nred)) + { Trace("nl-ext") << "...sent no lemmas, # extf to reduce = " << nred.size() << std::endl; - if (nred.empty()) { + if (nred.empty()) + { d_needsLastCall = false; } - } else { + } + else + { Trace("nl-ext") << "...sent lemmas." << std::endl; } } @@ -809,7 +835,7 @@ void NonlinearExtension::presolve() Trace("nl-ext") << "NonlinearExtension::presolve" << std::endl; } - +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 5aa2070a6..855310daa 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -15,8 +15,8 @@ ** multiplication via axiom instantiations. **/ -#ifndef CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H -#define CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H +#ifndef CVC4__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H +#define CVC4__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H #include <stdint.h> #include <map> @@ -25,16 +25,17 @@ #include "context/cdlist.h" #include "expr/kind.h" #include "expr/node.h" -#include "theory/arith/nl_lemma_utils.h" -#include "theory/arith/nl_model.h" -#include "theory/arith/nl_solver.h" +#include "theory/arith/nl/nl_lemma_utils.h" +#include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/nl_solver.h" +#include "theory/arith/nl/transcendental_solver.h" #include "theory/arith/theory_arith.h" -#include "theory/arith/transcendental_solver.h" #include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { namespace arith { +namespace nl { /** Non-linear extension class * @@ -60,7 +61,8 @@ namespace arith { * for valid arithmetic theory lemmas, based on the current set of assertions, * where d_out is the output channel of TheoryArith. */ -class NonlinearExtension { +class NonlinearExtension +{ typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; public: @@ -84,9 +86,10 @@ class NonlinearExtension { * that hold in the current context. We call { vars -> subs } a "derivable * substituion" (see Reynolds et al. FroCoS 2017). */ - bool getCurrentSubstitution(int effort, const std::vector<Node>& vars, + bool getCurrentSubstitution(int effort, + const std::vector<Node>& vars, std::vector<Node>& subs, - std::map<Node, std::vector<Node> >& exp); + std::map<Node, std::vector<Node>>& exp); /** Is the term n in reduced form? * * Used for context-dependent simplification. @@ -103,7 +106,9 @@ class NonlinearExtension { * The second part of the pair is used for constructing * minimal explanations for context-dependent simplifications. */ - std::pair<bool, Node> isExtfReduced(int effort, Node n, Node on, + std::pair<bool, Node> isExtfReduced(int effort, + Node n, + Node on, const std::vector<Node>& exp) const; /** Check at effort level e. * @@ -157,6 +162,7 @@ class NonlinearExtension { * on the output channel of TheoryArith in this function. */ void presolve(); + private: /** Model-based refinement * @@ -179,7 +185,6 @@ class NonlinearExtension { std::vector<Node>& mlemsPp, std::map<Node, NlLemmaSideEffect>& lemSE); - /** check last call * * Check assertions for consistency in the effort LAST_CALL with a subset of @@ -328,6 +333,7 @@ class NonlinearExtension { context::CDO<bool> d_builtModel; }; /* class NonlinearExtension */ +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/transcendental_solver.cpp b/src/theory/arith/nl/transcendental_solver.cpp index 665accc0a..3e10f6397 100644 --- a/src/theory/arith/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental_solver.cpp @@ -12,7 +12,7 @@ ** \brief Implementation of solver for handling transcendental functions. **/ -#include "theory/arith/transcendental_solver.h" +#include "theory/arith/nl/transcendental_solver.h" #include <cmath> #include <set> @@ -29,6 +29,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { namespace arith { +namespace nl { TranscendentalSolver::TranscendentalSolver(NlModel& m) : d_model(m) { @@ -1470,6 +1471,7 @@ Node TranscendentalSolver::mkValidPhase(Node a, Node pi) NodeManager::currentNM()->mkNode(MULT, mkRationalNode(-1), pi), a, pi); } +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/transcendental_solver.h b/src/theory/arith/nl/transcendental_solver.h index 88de49af3..5cd57d8fa 100644 --- a/src/theory/arith/transcendental_solver.h +++ b/src/theory/arith/nl/transcendental_solver.h @@ -12,8 +12,8 @@ ** \brief Solving for handling transcendental functions. **/ -#ifndef CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H -#define CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H +#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL_SOLVER_H +#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL_SOLVER_H #include <map> #include <unordered_map> @@ -21,12 +21,13 @@ #include <vector> #include "expr/node.h" -#include "theory/arith/nl_lemma_utils.h" -#include "theory/arith/nl_model.h" +#include "theory/arith/nl/nl_lemma_utils.h" +#include "theory/arith/nl/nl_model.h" namespace CVC4 { namespace theory { namespace arith { +namespace nl { /** Transcendental solver class * @@ -421,6 +422,7 @@ class TranscendentalSolver Node d_pi_bound[2]; }; /* class TranscendentalSolver */ +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 09b6d742a..3ff3966cc 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -55,7 +55,7 @@ #include "theory/arith/dio_solver.h" #include "theory/arith/linear_equality.h" #include "theory/arith/matrix.h" -#include "theory/arith/nonlinear_extension.h" +#include "theory/arith/nl/nonlinear_extension.h" #include "theory/arith/normal_form.h" #include "theory/arith/partial_model.h" #include "theory/arith/simplex.h" @@ -162,7 +162,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_nlin_inverse_skolem(u) { if( options::nlExt() ){ - d_nonlinearExtension = new NonlinearExtension( + d_nonlinearExtension = new nl::NonlinearExtension( containing, d_congruenceManager.getEqualityEngine()); } } @@ -1112,14 +1112,8 @@ void TheoryArithPrivate::checkNonLinearLogic(Node term) } } -struct ArithElimOpAttributeId -{ -}; -typedef expr::Attribute<ArithElimOpAttributeId, Node> ArithElimOpAttribute; - Node TheoryArithPrivate::eliminateOperatorsRec(Node n) { - ArithElimOpAttribute aeoa; Trace("arith-elim") << "Begin elim: " << n << std::endl; NodeManager* nm = NodeManager::currentNM(); std::unordered_map<Node, Node, TNodeHashFunction> visited; @@ -1138,18 +1132,11 @@ Node TheoryArithPrivate::eliminateOperatorsRec(Node n) } else if (it == visited.end()) { - if (cur.hasAttribute(aeoa)) - { - visited[cur] = cur.getAttribute(aeoa); - } - else + visited[cur] = Node::null(); + visit.push_back(cur); + for (const Node& cn : cur) { - visited[cur] = Node::null(); - visit.push_back(cur); - for (const Node& cn : cur) - { - visit.push_back(cn); - } + visit.push_back(cn); } } else if (it->second.isNull()) @@ -1180,7 +1167,6 @@ Node TheoryArithPrivate::eliminateOperatorsRec(Node n) // are defined in terms of other non-standard operators. ret = eliminateOperatorsRec(retElim); } - cur.setAttribute(aeoa, ret); visited[cur] = ret; } } while (!visit.empty()); diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 8198dbcf1..822b38f69 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -83,7 +83,9 @@ namespace inferbounds { } class InferBoundsResult; +namespace nl { class NonlinearExtension; +} /** * Implementation of QF_LRA. @@ -372,7 +374,7 @@ private: AttemptSolutionSDP d_attemptSolSimplex; /** non-linear algebraic approach */ - NonlinearExtension * d_nonlinearExtension; + nl::NonlinearExtension* d_nonlinearExtension; bool solveRealRelaxation(Theory::Effort effortLevel); diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp new file mode 100644 index 000000000..8fdbe9f6b --- /dev/null +++ b/src/theory/booleans/proof_checker.cpp @@ -0,0 +1,568 @@ +/********************* */ +/*! \file proof_checker.cpp + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of equality proof checker + **/ + +#include "theory/booleans/proof_checker.h" + +namespace CVC4 { +namespace theory { +namespace booleans { + +void BoolProofRuleChecker::registerTo(ProofChecker* pc) +{ + pc->registerChecker(PfRule::SPLIT, this); + pc->registerChecker(PfRule::AND_ELIM, this); + pc->registerChecker(PfRule::AND_INTRO, this); + pc->registerChecker(PfRule::NOT_OR_ELIM, this); + pc->registerChecker(PfRule::IMPLIES_ELIM, this); + pc->registerChecker(PfRule::NOT_IMPLIES_ELIM1, this); + pc->registerChecker(PfRule::NOT_IMPLIES_ELIM2, this); + pc->registerChecker(PfRule::EQUIV_ELIM1, this); + pc->registerChecker(PfRule::EQUIV_ELIM2, this); + pc->registerChecker(PfRule::NOT_EQUIV_ELIM1, this); + pc->registerChecker(PfRule::NOT_EQUIV_ELIM2, this); + pc->registerChecker(PfRule::XOR_ELIM1, this); + pc->registerChecker(PfRule::XOR_ELIM2, this); + pc->registerChecker(PfRule::NOT_XOR_ELIM1, this); + pc->registerChecker(PfRule::NOT_XOR_ELIM2, this); + pc->registerChecker(PfRule::ITE_ELIM1, this); + pc->registerChecker(PfRule::ITE_ELIM2, this); + pc->registerChecker(PfRule::NOT_ITE_ELIM1, this); + pc->registerChecker(PfRule::NOT_ITE_ELIM2, this); + pc->registerChecker(PfRule::NOT_AND, this); + pc->registerChecker(PfRule::CNF_AND_POS, this); + pc->registerChecker(PfRule::CNF_AND_NEG, this); + pc->registerChecker(PfRule::CNF_OR_POS, this); + pc->registerChecker(PfRule::CNF_OR_NEG, this); + pc->registerChecker(PfRule::CNF_IMPLIES_POS, this); + pc->registerChecker(PfRule::CNF_IMPLIES_NEG1, this); + pc->registerChecker(PfRule::CNF_IMPLIES_NEG2, this); + pc->registerChecker(PfRule::CNF_EQUIV_POS1, this); + pc->registerChecker(PfRule::CNF_EQUIV_POS2, this); + pc->registerChecker(PfRule::CNF_EQUIV_NEG1, this); + pc->registerChecker(PfRule::CNF_EQUIV_NEG2, this); + pc->registerChecker(PfRule::CNF_XOR_POS1, this); + pc->registerChecker(PfRule::CNF_XOR_POS2, this); + pc->registerChecker(PfRule::CNF_XOR_NEG1, this); + pc->registerChecker(PfRule::CNF_XOR_NEG2, this); + pc->registerChecker(PfRule::CNF_ITE_POS1, this); + pc->registerChecker(PfRule::CNF_ITE_POS2, this); + pc->registerChecker(PfRule::CNF_ITE_POS3, this); + pc->registerChecker(PfRule::CNF_ITE_NEG1, this); + pc->registerChecker(PfRule::CNF_ITE_NEG2, this); + pc->registerChecker(PfRule::CNF_ITE_NEG3, this); +} + +Node BoolProofRuleChecker::checkInternal(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args) +{ + if (id == PfRule::SPLIT) + { + Assert(children.empty()); + Assert(args.size() == 1); + return NodeManager::currentNM()->mkNode( + kind::OR, args[0], args[0].notNode()); + } + // natural deduction rules + if (id == PfRule::AND_ELIM) + { + Assert(children.size() == 1); + Assert(args.size() == 1); + uint32_t i; + if (children[0].getKind() != kind::AND || !getUInt32(args[0], i)) + { + return Node::null(); + } + if (i >= children[0].getNumChildren()) + { + return Node::null(); + } + return children[0][i]; + } + if (id == PfRule::AND_INTRO) + { + Assert(children.size() >= 1); + return children.size() == 1 + ? children[0] + : NodeManager::currentNM()->mkNode(kind::AND, children); + } + if (id == PfRule::NOT_OR_ELIM) + { + Assert(children.size() == 1); + Assert(args.size() == 1); + uint32_t i; + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::OR || !getUInt32(args[0], i)) + { + return Node::null(); + } + if (i >= children[0][0].getNumChildren()) + { + return Node::null(); + } + return children[0][0][i].notNode(); + } + if (id == PfRule::IMPLIES_ELIM) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::IMPLIES) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0].notNode(), children[0][1]); + } + if (id == PfRule::NOT_IMPLIES_ELIM1) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::IMPLIES) + { + return Node::null(); + } + return children[0][0][0]; + } + if (id == PfRule::NOT_IMPLIES_ELIM2) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::IMPLIES) + { + return Node::null(); + } + return children[0][0][1].notNode(); + } + if (id == PfRule::EQUIV_ELIM1) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0].notNode(), children[0][1]); + } + if (id == PfRule::EQUIV_ELIM2) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0], children[0][1].notNode()); + } + if (id == PfRule::NOT_EQUIV_ELIM1) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::EQUAL) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0][0], children[0][0][1]); + } + if (id == PfRule::NOT_EQUIV_ELIM2) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::EQUAL) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode()); + } + if (id == PfRule::XOR_ELIM1) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::XOR) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0], children[0][1]); + } + if (id == PfRule::XOR_ELIM2) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::XOR) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0].notNode(), children[0][1].notNode()); + } + if (id == PfRule::NOT_XOR_ELIM1) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::XOR) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0][0], children[0][0][1].notNode()); + } + if (id == PfRule::NOT_XOR_ELIM2) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::XOR) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0][0].notNode(), children[0][0][1]); + } + if (id == PfRule::ITE_ELIM1) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::ITE) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0].notNode(), children[0][1]); + } + if (id == PfRule::ITE_ELIM2) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::ITE) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0], children[0][2]); + } + if (id == PfRule::NOT_ITE_ELIM1) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::ITE) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode()); + } + if (id == PfRule::NOT_ITE_ELIM2) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::ITE) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0][0], children[0][0][2].notNode()); + } + // De Morgan + if (id == PfRule::NOT_AND) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::AND) + { + return Node::null(); + } + std::vector<Node> disjuncts; + for (unsigned i = 0, size = children[0][0].getNumChildren(); i < size; ++i) + { + disjuncts.push_back(children[0][0][i].notNode()); + } + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + // valid clauses rules for Tseitin CNF transformation + if (id == PfRule::CNF_AND_POS) + { + Assert(children.empty()); + Assert(args.size() == 2); + uint32_t i; + if (args[0].getKind() != kind::AND || !getUInt32(args[1], i)) + { + return Node::null(); + } + if (i >= args[0].getNumChildren()) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, args[0].notNode(), args[0][i]); + } + if (id == PfRule::CNF_AND_NEG) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::AND) + { + return Node::null(); + } + std::vector<Node> disjuncts{args[0]}; + for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i) + { + disjuncts.push_back(args[0][i].notNode()); + } + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_OR_POS) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::OR) + { + return Node::null(); + } + std::vector<Node> disjuncts{args[0].notNode()}; + for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i) + { + disjuncts.push_back(args[0][i]); + } + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_OR_NEG) + { + Assert(children.empty()); + Assert(args.size() == 2); + uint32_t i; + if (args[0].getKind() != kind::OR || !getUInt32(args[1], i)) + { + return Node::null(); + } + if (i >= args[0].getNumChildren()) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, args[0], args[0][i].notNode()); + } + if (id == PfRule::CNF_IMPLIES_POS) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::IMPLIES) + { + return Node::null(); + } + std::vector<Node> disjuncts{ + args[0].notNode(), args[0][0].notNode(), args[0][1]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_IMPLIES_NEG1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::IMPLIES) + { + return Node::null(); + } + std::vector<Node> disjuncts{args[0], args[0][0]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_IMPLIES_NEG2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::IMPLIES) + { + return Node::null(); + } + std::vector<Node> disjuncts{args[0], args[0][1].notNode()}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_EQUIV_POS1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + std::vector<Node> disjuncts{ + args[0].notNode(), args[0][0].notNode(), args[0][1]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_EQUIV_POS2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + std::vector<Node> disjuncts{ + args[0].notNode(), args[0][0], args[0][1].notNode()}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_EQUIV_NEG1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + std::vector<Node> disjuncts{args[0], args[0][0], args[0][1]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_EQUIV_NEG2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + std::vector<Node> disjuncts{ + args[0], args[0][0].notNode(), args[0][1].notNode()}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_XOR_POS1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::XOR) + { + return Node::null(); + } + std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][1]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_XOR_POS2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::XOR) + { + return Node::null(); + } + std::vector<Node> disjuncts{ + args[0].notNode(), args[0][0].notNode(), args[0][1].notNode()}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_XOR_NEG1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::XOR) + { + return Node::null(); + } + std::vector<Node> disjuncts{args[0], args[0][0].notNode(), args[0][1]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_XOR_NEG2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::XOR) + { + return Node::null(); + } + std::vector<Node> disjuncts{args[0], args[0][0], args[0][1].notNode()}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_ITE_POS1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + std::vector<Node> disjuncts{ + args[0].notNode(), args[0][0].notNode(), args[0][1]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_ITE_POS2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][2]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_ITE_POS3) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + std::vector<Node> disjuncts{args[0].notNode(), args[0][1], args[0][2]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_ITE_NEG1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + std::vector<Node> disjuncts{ + args[0], args[0][0].notNode(), args[0][1].notNode()}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_ITE_NEG2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + std::vector<Node> disjuncts{args[0], args[0][0], args[0][2].notNode()}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_ITE_NEG3) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + std::vector<Node> disjuncts{ + args[0], args[0][1].notNode(), args[0][2].notNode()}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + // no rule + return Node::null(); +} + +} // namespace booleans +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/booleans/proof_checker.h b/src/theory/booleans/proof_checker.h new file mode 100644 index 000000000..56414ff91 --- /dev/null +++ b/src/theory/booleans/proof_checker.h @@ -0,0 +1,49 @@ +/********************* */ +/*! \file proof_checker.h + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Boolean proof checker utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__BOOLEANS__PROOF_CHECKER_H +#define CVC4__THEORY__BOOLEANS__PROOF_CHECKER_H + +#include "expr/node.h" +#include "expr/proof_checker.h" +#include "expr/proof_node.h" + +namespace CVC4 { +namespace theory { +namespace booleans { + +/** A checker for boolean reasoning in proofs */ +class BoolProofRuleChecker : public ProofRuleChecker +{ + public: + BoolProofRuleChecker() {} + ~BoolProofRuleChecker() {} + + /** Register all rules owned by this rule checker into pc. */ + void registerTo(ProofChecker* pc) override; + + protected: + /** Return the conclusion of the given proof step, or null if it is invalid */ + Node checkInternal(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args) override; +}; + +} // namespace booleans +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__BOOLEANS__PROOF_CHECKER_H */ diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp new file mode 100644 index 000000000..8d2a1540c --- /dev/null +++ b/src/theory/builtin/proof_checker.cpp @@ -0,0 +1,359 @@ +/********************* */ +/*! \file proof_checker.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of equality proof checker + **/ + +#include "theory/builtin/proof_checker.h" + +#include "expr/proof_skolem_cache.h" +#include "theory/rewriter.h" +#include "theory/theory.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { + +const char* toString(MethodId id) +{ + switch (id) + { + case MethodId::RW_REWRITE: return "RW_REWRITE"; + case MethodId::RW_IDENTITY: return "RW_IDENTITY"; + case MethodId::SB_DEFAULT: return "SB_DEFAULT"; + case MethodId::SB_LITERAL: return "SB_LITERAL"; + case MethodId::SB_FORMULA: return "SB_FORMULA"; + default: return "MethodId::Unknown"; + }; +} + +std::ostream& operator<<(std::ostream& out, MethodId id) +{ + out << toString(id); + return out; +} + +Node mkMethodId(MethodId id) +{ + return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(id))); +} + +namespace builtin { + +void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) +{ + pc->registerChecker(PfRule::ASSUME, this); + pc->registerChecker(PfRule::SCOPE, this); + pc->registerChecker(PfRule::SUBS, this); + pc->registerChecker(PfRule::REWRITE, this); + pc->registerChecker(PfRule::MACRO_SR_EQ_INTRO, this); + pc->registerChecker(PfRule::MACRO_SR_PRED_INTRO, this); + pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this); + pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this); +} + +Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr) +{ + Node nk = ProofSkolemCache::getSkolemForm(n); + Node nkr = applyRewriteExternal(nk, idr); + return ProofSkolemCache::getWitnessForm(nkr); +} + +Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids) +{ + if (exp.isNull() || exp.getKind() != EQUAL) + { + return Node::null(); + } + Node nk = ProofSkolemCache::getSkolemForm(n); + Node nks = applySubstitutionExternal(nk, exp, ids); + return ProofSkolemCache::getWitnessForm(nks); +} + +Node BuiltinProofRuleChecker::applySubstitution(Node n, + const std::vector<Node>& exp, + MethodId ids) +{ + Node nk = ProofSkolemCache::getSkolemForm(n); + Node nks = applySubstitutionExternal(nk, exp, ids); + return ProofSkolemCache::getWitnessForm(nks); +} + +Node BuiltinProofRuleChecker::applySubstitutionRewrite( + Node n, const std::vector<Node>& exp, MethodId ids, MethodId idr) +{ + Node nk = ProofSkolemCache::getSkolemForm(n); + Node nks = applySubstitutionExternal(nk, exp, ids); + Node nksr = applyRewriteExternal(nks, idr); + return ProofSkolemCache::getWitnessForm(nksr); +} + +Node BuiltinProofRuleChecker::applyRewriteExternal(Node n, MethodId idr) +{ + Trace("builtin-pfcheck-debug") + << "applyRewriteExternal (" << idr << "): " << n << std::endl; + if (idr == MethodId::RW_REWRITE) + { + return Rewriter::rewrite(n); + } + else if (idr == MethodId::RW_IDENTITY) + { + // does nothing + return n; + } + // unknown rewriter + Assert(false) + << "BuiltinProofRuleChecker::applyRewriteExternal: no rewriter for " + << idr << std::endl; + return n; +} + +Node BuiltinProofRuleChecker::applySubstitutionExternal(Node n, + Node exp, + MethodId ids) +{ + Assert(!exp.isNull()); + Node expk = ProofSkolemCache::getSkolemForm(exp); + TNode var, subs; + if (ids == MethodId::SB_DEFAULT) + { + if (expk.getKind() != EQUAL) + { + return Node::null(); + } + var = expk[0]; + subs = expk[1]; + } + else if (ids == MethodId::SB_LITERAL) + { + bool polarity = expk.getKind() != NOT; + var = polarity ? expk : expk[0]; + subs = NodeManager::currentNM()->mkConst(polarity); + } + else if (ids == MethodId::SB_FORMULA) + { + var = expk; + subs = NodeManager::currentNM()->mkConst(true); + } + else + { + Assert(false) << "BuiltinProofRuleChecker::applySubstitutionExternal: no " + "substitution for " + << ids << std::endl; + } + return n.substitute(var, subs); +} + +Node BuiltinProofRuleChecker::applySubstitutionExternal( + Node n, const std::vector<Node>& exp, MethodId ids) +{ + Node curr = n; + // apply substitution one at a time, in reverse order + for (size_t i = 0, nexp = exp.size(); i < nexp; i++) + { + if (exp[nexp - 1 - i].isNull()) + { + return Node::null(); + } + curr = applySubstitutionExternal(curr, exp[nexp - 1 - i], ids); + if (curr.isNull()) + { + break; + } + } + return curr; +} + +bool BuiltinProofRuleChecker::getMethodId(TNode n, MethodId& i) +{ + uint32_t index; + if (!getUInt32(n, index)) + { + return false; + } + i = static_cast<MethodId>(index); + return true; +} + +Node BuiltinProofRuleChecker::checkInternal(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args) +{ + // compute what was proven + if (id == PfRule::ASSUME) + { + Assert(children.empty()); + Assert(args.size() == 1); + Assert(args[0].getType().isBoolean()); + return args[0]; + } + else if (id == PfRule::SCOPE) + { + Assert(children.size() == 1); + if (args.empty()) + { + // no antecedant + return children[0]; + } + Node ant = mkAnd(args); + // if the conclusion is false, its the negated antencedant only + if (children[0].isConst() && !children[0].getConst<bool>()) + { + return ant.notNode(); + } + return NodeManager::currentNM()->mkNode(IMPLIES, ant, children[0]); + } + else if (id == PfRule::SUBS) + { + Assert(children.size() > 0); + Assert(1 <= args.size() && args.size() <= 2); + MethodId ids = MethodId::SB_DEFAULT; + if (args.size() == 2 && !getMethodId(args[1], ids)) + { + return Node::null(); + } + std::vector<Node> exp; + for (size_t i = 0, nchild = children.size(); i < nchild; i++) + { + exp.push_back(children[i]); + } + Node res = applySubstitution(args[0], exp); + return args[0].eqNode(res); + } + else if (id == PfRule::REWRITE) + { + Assert(children.empty()); + Assert(1 <= args.size() && args.size() <= 2); + MethodId ids = MethodId::RW_REWRITE; + if (args.size() == 2 && !getMethodId(args[1], ids)) + { + return Node::null(); + } + Node res = applyRewrite(args[0]); + return args[0].eqNode(res); + } + else if (id == PfRule::MACRO_SR_EQ_INTRO) + { + Assert(1 <= args.size() && args.size() <= 3); + MethodId ids, idr; + if (!getMethodIds(args, ids, idr, 1)) + { + return Node::null(); + } + Node res = applySubstitutionRewrite(args[0], children, idr); + return args[0].eqNode(res); + } + else if (id == PfRule::MACRO_SR_PRED_INTRO) + { + Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " " + << args.size() << std::endl; + Assert(1 <= args.size() && args.size() <= 3); + MethodId ids, idr; + if (!getMethodIds(args, ids, idr, 1)) + { + return Node::null(); + } + Node res = applySubstitutionRewrite(args[0], children, ids, idr); + if (res.isNull()) + { + return Node::null(); + } + // **** NOTE: can rewrite the witness form here. This enables certain lemmas + // to be provable, e.g. (= k t) where k is a purification Skolem for t. + res = Rewriter::rewrite(res); + if (!res.isConst() || !res.getConst<bool>()) + { + Trace("builtin-pfcheck") + << "Failed to rewrite to true, res=" << res << std::endl; + return Node::null(); + } + return args[0]; + } + else if (id == PfRule::MACRO_SR_PRED_ELIM) + { + Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " " + << args.size() << std::endl; + Assert(children.size() >= 1); + Assert(args.size() <= 2); + std::vector<Node> exp; + exp.insert(exp.end(), children.begin() + 1, children.end()); + MethodId ids, idr; + if (!getMethodIds(args, ids, idr, 0)) + { + return Node::null(); + } + Node res1 = applySubstitutionRewrite(children[0], exp, ids, idr); + Trace("builtin-pfcheck") << "Returned " << res1 << std::endl; + return res1; + } + else if (id == PfRule::MACRO_SR_PRED_TRANSFORM) + { + Trace("builtin-pfcheck") << "Check " << id << " " << children.size() << " " + << args.size() << std::endl; + Assert(children.size() >= 1); + Assert(1 <= args.size() && args.size() <= 3); + Assert(args[0].getType().isBoolean()); + MethodId ids, idr; + if (!getMethodIds(args, ids, idr, 1)) + { + return Node::null(); + } + std::vector<Node> exp; + exp.insert(exp.end(), children.begin() + 1, children.end()); + Node res1 = applySubstitutionRewrite(children[0], exp, ids, idr); + Node res2 = applySubstitutionRewrite(args[0], exp, ids, idr); + // can rewrite the witness forms + res1 = Rewriter::rewrite(res1); + res2 = Rewriter::rewrite(res2); + if (res1.isNull() || res1 != res2) + { + Trace("builtin-pfcheck") << "Failed to match results" << std::endl; + Trace("builtin-pfcheck-debug") << res1 << " vs " << res2 << std::endl; + return Node::null(); + } + return args[0]; + } + // no rule + return Node::null(); +} + +bool BuiltinProofRuleChecker::getMethodIds(const std::vector<Node>& args, + MethodId& ids, + MethodId& idr, + size_t index) +{ + ids = MethodId::SB_DEFAULT; + idr = MethodId::RW_REWRITE; + if (args.size() > index) + { + if (!getMethodId(args[index], ids)) + { + Trace("builtin-pfcheck") + << "Failed to get id from " << args[index] << std::endl; + return false; + } + } + if (args.size() > index + 1) + { + if (!getMethodId(args[index + 1], idr)) + { + Trace("builtin-pfcheck") + << "Failed to get id from " << args[index + 1] << std::endl; + return false; + } + } + return true; +} + +} // namespace builtin +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h new file mode 100644 index 000000000..f4424b107 --- /dev/null +++ b/src/theory/builtin/proof_checker.h @@ -0,0 +1,150 @@ +/********************* */ +/*! \file proof_checker.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Equality proof checker utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__BUILTIN__PROOF_CHECKER_H +#define CVC4__THEORY__BUILTIN__PROOF_CHECKER_H + +#include "expr/node.h" +#include "expr/proof_checker.h" +#include "expr/proof_node.h" + +namespace CVC4 { +namespace theory { + +/** + * Identifiers for rewriters and substitutions, which we abstractly + * classify as "methods". Methods have a unique identifier in the internal + * proof calculus implemented by the checker below. + * + * A "rewriter" is abstractly a method from Node to Node, where the output + * is semantically equivalent to the input. The identifiers below list + * various methods that have this contract. This identifier is used + * in a number of the builtin rules. + * + * A substitution is a method for turning a formula into a substitution. + */ +enum class MethodId : uint32_t +{ + //---------------------------- Rewriters + // Rewriter::rewrite(n) + RW_REWRITE, + // identity + RW_IDENTITY, + //---------------------------- Substitutions + // (= x y) is interpreted as x -> y, using Node::substitute + SB_DEFAULT, + // P, (not P) are interpreted as P -> true, P -> false using Node::substitute + SB_LITERAL, + // P is interpreted as P -> true using Node::substitute + SB_FORMULA, +}; +/** Converts a rewriter id to a string. */ +const char* toString(MethodId id); +/** Write a rewriter id to out */ +std::ostream& operator<<(std::ostream& out, MethodId id); +/** Make a method id node */ +Node mkMethodId(MethodId id); + +namespace builtin { + +/** A checker for builtin proofs */ +class BuiltinProofRuleChecker : public ProofRuleChecker +{ + public: + BuiltinProofRuleChecker() {} + ~BuiltinProofRuleChecker() {} + /** + * Apply rewrite on n (in witness form). This encapsulates the exact behavior + * of a REWRITE step in a proof. Rewriting is performed on the Skolem form of + * n. + * + * @param n The node (in witness form) to rewrite, + * @param idr The method identifier of the rewriter, by default RW_REWRITE + * specifying a call to Rewriter::rewrite. + * @return The rewritten form of n. + */ + static Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE); + /** + * Apply substitution on n (in witness form). This encapsulates the exact + * behavior of a SUBS step in a proof. Substitution is on the Skolem form of + * n. + * + * @param n The node (in witness form) to substitute, + * @param exp The (set of) equalities (in witness form) corresponding to the + * substitution + * @param ids The method identifier of the substitution, by default SB_DEFAULT + * specifying that lhs/rhs of equalities are interpreted as a substitution. + * @return The substituted form of n. + */ + static Node applySubstitution(Node n, + Node exp, + MethodId ids = MethodId::SB_DEFAULT); + static Node applySubstitution(Node n, + const std::vector<Node>& exp, + MethodId ids = MethodId::SB_DEFAULT); + /** Apply substitution + rewriting + * + * Combines the above two steps. + * + * @param n The node (in witness form) to substitute and rewrite, + * @param exp The (set of) equalities (in witness form) corresponding to the + * substitution + * @param ids The method identifier of the substitution. + * @param idr The method identifier of the rewriter. + * @return The substituted, rewritten form of n. + */ + static Node applySubstitutionRewrite(Node n, + const std::vector<Node>& exp, + MethodId ids = MethodId::SB_DEFAULT, + MethodId idr = MethodId::RW_REWRITE); + /** get a rewriter Id from a node, return false if we fail */ + static bool getMethodId(TNode n, MethodId& i); + + /** Register all rules owned by this rule checker into pc. */ + void registerTo(ProofChecker* pc) override; + + protected: + /** Return the conclusion of the given proof step, or null if it is invalid */ + Node checkInternal(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args) override; + /** get method identifiers */ + bool getMethodIds(const std::vector<Node>& args, + MethodId& ids, + MethodId& idr, + size_t index); + /** + * Apply rewrite (on Skolem form). id is the identifier of the rewriter. + */ + static Node applyRewriteExternal(Node n, MethodId idr = MethodId::RW_REWRITE); + /** + * Apply substitution for n (on Skolem form), where exp is an equality + * (or set of equalities) in Witness form. Returns the result of + * n * sigma{ids}(exp), where sigma{ids} is a substitution based on method + * identifier ids. + */ + static Node applySubstitutionExternal(Node n, Node exp, MethodId ids); + /** Same as above, for a list of substitutions in exp */ + static Node applySubstitutionExternal(Node n, + const std::vector<Node>& exp, + MethodId ids); +}; + +} // namespace builtin +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__BUILTIN__PROOF_CHECKER_H */ diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp index ee0fd814e..ea67ab79d 100644 --- a/src/theory/datatypes/theory_datatypes_utils.cpp +++ b/src/theory/datatypes/theory_datatypes_utils.cpp @@ -23,6 +23,7 @@ #include "smt/smt_engine_scope.h" #include "theory/evaluator.h" #include "theory/rewriter.h" +#include "printer/sygus_print_callback.h" using namespace CVC4; using namespace CVC4::kind; @@ -711,6 +712,223 @@ Node sygusToBuiltinEval(Node n, const std::vector<Node>& args) return visited[n]; } +void getFreeSymbolsSygusType(TypeNode sdt, + std::unordered_set<Node, NodeHashFunction>& syms) +{ + // datatype types we need to process + std::vector<TypeNode> typeToProcess; + // datatype types we have processed + std::map<TypeNode, TypeNode> typesProcessed; + typeToProcess.push_back(sdt); + while (!typeToProcess.empty()) + { + std::vector<TypeNode> typeNextToProcess; + for (const TypeNode& curr : typeToProcess) + { + Assert(curr.isDatatype() && curr.getDType().isSygus()); + const DType& dtc = curr.getDType(); + for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++) + { + // collect the symbols from the operator + Node op = dtc[j].getSygusOp(); + expr::getSymbols(op, syms); + // traverse the argument types + for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++) + { + TypeNode argt = dtc[j].getArgType(k); + if (!argt.isDatatype() || !argt.getDType().isSygus()) + { + // not a sygus datatype + continue; + } + if (typesProcessed.find(argt) == typesProcessed.end()) + { + typeNextToProcess.push_back(argt); + } + } + } + } + typeToProcess.clear(); + typeToProcess.insert(typeToProcess.end(), + typeNextToProcess.begin(), + typeNextToProcess.end()); + } +} + +TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, + const std::vector<Node>& syms, + const std::vector<Node>& vars) +{ + NodeManager* nm = NodeManager::currentNM(); + const DType& sdtd = sdt.getDType(); + // compute the new formal argument list + std::vector<Node> formalVars; + Node prevVarList = sdtd.getSygusVarList(); + if (!prevVarList.isNull()) + { + for (const Node& v : prevVarList) + { + // if it is not being replaced + if (std::find(syms.begin(), syms.end(), v) != syms.end()) + { + formalVars.push_back(v); + } + } + } + for (const Node& v : vars) + { + if (v.getKind() == BOUND_VARIABLE) + { + formalVars.push_back(v); + } + } + // make the sygus variable list for the formal argument list + Node abvl = nm->mkNode(BOUND_VAR_LIST, formalVars); + Trace("sygus-abduct-debug") << "...finish" << std::endl; + + // must convert all constructors to version with variables in "vars" + std::vector<SygusDatatype> sdts; + std::set<Type> unres; + + Trace("dtsygus-gen-debug") << "Process sygus type:" << std::endl; + Trace("dtsygus-gen-debug") << sdtd.getName() << std::endl; + + // datatype types we need to process + std::vector<TypeNode> dtToProcess; + // datatype types we have processed + std::map<TypeNode, TypeNode> dtProcessed; + dtToProcess.push_back(sdt); + std::stringstream ssutn0; + ssutn0 << sdtd.getName() << "_s"; + TypeNode abdTNew = + nm->mkSort(ssutn0.str(), ExprManager::SORT_FLAG_PLACEHOLDER); + unres.insert(abdTNew.toType()); + dtProcessed[sdt] = abdTNew; + + // We must convert all symbols in the sygus datatype type sdt to + // apply the substitution { syms -> vars }, where syms is the free + // variables of the input problem, and vars is the formal argument list + // of the function-to-synthesize. + + // We are traversing over the subfield types of the datatype to convert + // them into the form described above. + while (!dtToProcess.empty()) + { + std::vector<TypeNode> dtNextToProcess; + for (const TypeNode& curr : dtToProcess) + { + Assert(curr.isDatatype() && curr.getDType().isSygus()); + const DType& dtc = curr.getDType(); + std::stringstream ssdtn; + ssdtn << dtc.getName() << "_s"; + sdts.push_back(SygusDatatype(ssdtn.str())); + Trace("dtsygus-gen-debug") + << "Process datatype " << sdts.back().getName() << "..." << std::endl; + for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++) + { + Node op = dtc[j].getSygusOp(); + // apply the substitution to the argument + Node ops = + op.substitute(syms.begin(), syms.end(), vars.begin(), vars.end()); + Trace("dtsygus-gen-debug") << " Process constructor " << op << " / " + << ops << "..." << std::endl; + std::vector<TypeNode> cargs; + for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++) + { + TypeNode argt = dtc[j].getArgType(k); + std::map<TypeNode, TypeNode>::iterator itdp = dtProcessed.find(argt); + TypeNode argtNew; + if (itdp == dtProcessed.end()) + { + std::stringstream ssutn; + ssutn << argt.getDType().getName() << "_s"; + argtNew = + nm->mkSort(ssutn.str(), ExprManager::SORT_FLAG_PLACEHOLDER); + Trace("dtsygus-gen-debug") << " ...unresolved type " << argtNew + << " for " << argt << std::endl; + unres.insert(argtNew.toType()); + dtProcessed[argt] = argtNew; + dtNextToProcess.push_back(argt); + } + else + { + argtNew = itdp->second; + } + Trace("dtsygus-gen-debug") + << " Arg #" << k << ": " << argtNew << std::endl; + cargs.push_back(argtNew); + } + // callback prints as the expression + std::shared_ptr<SygusPrintCallback> spc; + std::vector<Expr> args; + if (op.getKind() == LAMBDA) + { + Node opBody = op[1]; + for (const Node& v : op[0]) + { + args.push_back(v.toExpr()); + } + spc = std::make_shared<printer::SygusExprPrintCallback>( + opBody.toExpr(), args); + } + else if (cargs.empty()) + { + spc = std::make_shared<printer::SygusExprPrintCallback>(op.toExpr(), + args); + } + std::stringstream ss; + ss << ops.getKind(); + Trace("dtsygus-gen-debug") << "Add constructor : " << ops << std::endl; + sdts.back().addConstructor(ops, ss.str(), cargs, spc); + } + Trace("dtsygus-gen-debug") + << "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl; + TypeNode stn = dtc.getSygusType(); + sdts.back().initializeDatatype( + stn, abvl, dtc.getSygusAllowConst(), dtc.getSygusAllowAll()); + } + dtToProcess.clear(); + dtToProcess.insert( + dtToProcess.end(), dtNextToProcess.begin(), dtNextToProcess.end()); + } + Trace("dtsygus-gen-debug") + << "Make " << sdts.size() << " datatype types..." << std::endl; + // extract the datatypes + std::vector<Datatype> datatypes; + for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++) + { + datatypes.push_back(sdts[i].getDatatype()); + } + // make the datatype types + std::vector<DatatypeType> datatypeTypes = + nm->toExprManager()->mkMutualDatatypeTypes( + datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER); + TypeNode sdtS = TypeNode::fromType(datatypeTypes[0]); + if (Trace.isOn("dtsygus-gen-debug")) + { + Trace("dtsygus-gen-debug") << "Made datatype types:" << std::endl; + for (unsigned j = 0, ndts = datatypeTypes.size(); j < ndts; j++) + { + const DType& dtj = TypeNode::fromType(datatypeTypes[j]).getDType(); + Trace("dtsygus-gen-debug") << "#" << j << ": " << dtj << std::endl; + for (unsigned k = 0, ncons = dtj.getNumConstructors(); k < ncons; k++) + { + for (unsigned l = 0, nargs = dtj[k].getNumArgs(); l < nargs; l++) + { + if (!dtj[k].getArgType(l).isDatatype()) + { + Trace("dtsygus-gen-debug") + << "Argument " << l << " of " << dtj[k] + << " is not datatype : " << dtj[k].getArgType(l) << std::endl; + AlwaysAssert(false); + } + } + } + } + } + return sdtS; +} + } // namespace utils } // namespace datatypes } // namespace theory diff --git a/src/theory/datatypes/theory_datatypes_utils.h b/src/theory/datatypes/theory_datatypes_utils.h index 58f719910..038922f37 100644 --- a/src/theory/datatypes/theory_datatypes_utils.h +++ b/src/theory/datatypes/theory_datatypes_utils.h @@ -245,6 +245,46 @@ Node sygusToBuiltin(Node c, bool isExternal = false); */ Node sygusToBuiltinEval(Node n, const std::vector<Node>& args); +/** Get free symbols in a sygus datatype type + * + * Add the free symbols (expr::getSymbols) in terms that can be generated by + * sygus datatype sdt to the set syms. For example, given sdt encodes the + * grammar: + * G -> a | +( b, G ) | c | e + * We have that { a, b, c, e } are added to syms. Notice that expr::getSymbols + * excludes variables whose kind is BOUND_VARIABLE. + */ +void getFreeSymbolsSygusType(TypeNode sdt, + std::unordered_set<Node, NodeHashFunction>& syms); + +/** Substitute and generalize a sygus datatype type + * + * This transforms a sygus datatype sdt into another one sdt' that generates + * terms t such that t * { vars -> syms } is generated by sdt. + * + * The arguments syms and vars should be vectors of the same size and types. + * It is recommended that the arguments in syms and vars should be variables + * (return true for .isVar()) but this is not required. + * + * The variables in vars of type BOUND_VARIABLE are added to the + * formal argument list of t. Other symbols are not. + * + * For example, given sdt encodes the grammar: + * G -> a | +( b, G ) | c | e + * Let syms = { a, b, c } and vars = { x_a, x_b, d }, where x_a and x_b have + * type BOUND_VARIABLE and d does not. + * The returned type encodes the grammar: + * G' -> x_a | +( x_b, G' ) | d | e + * Additionally, x_a and x_b are treated as formal arguments of a function + * to synthesize whose syntax restrictions are specified by G'. + * + * This method traverses the type definition of the datatype corresponding to + * the argument sdt. + */ +TypeNode substituteAndGeneralizeSygusType(TypeNode sdt, + const std::vector<Node>& syms, + const std::vector<Node>& vars); + // ------------------------ end sygus utils } // namespace utils diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index f94fee66b..472dabf68 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -633,7 +633,7 @@ struct SortBvExtractInterval }; void BvInstantiatorPreprocess::registerCounterexampleLemma( - std::vector<Node>& lems, std::vector<Node>& ce_vars) + Node lem, std::vector<Node>& ceVars, std::vector<Node>& auxLems) { // new variables std::vector<Node> vars; @@ -647,12 +647,8 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma( // map from terms to bitvector extracts applied to that term std::map<Node, std::vector<Node> > extract_map; std::unordered_set<TNode, TNodeHashFunction> visited; - for (unsigned i = 0, size = lems.size(); i < size; i++) - { - Trace("cegqi-bv-pp-debug2") - << "Register ce lemma # " << i << " : " << lems[i] << std::endl; - collectExtracts(lems[i], extract_map, visited); - } + Trace("cegqi-bv-pp-debug2") << "Register ce lemma " << lem << std::endl; + collectExtracts(lem, extract_map, visited); for (std::pair<const Node, std::vector<Node> >& es : extract_map) { // sort based on the extract start position @@ -721,10 +717,10 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma( Trace("cegqi-bv-pp") << "Adding " << new_lems.size() << " lemmas..." << std::endl; - lems.insert(lems.end(), new_lems.begin(), new_lems.end()); + auxLems.insert(auxLems.end(), new_lems.begin(), new_lems.end()); Trace("cegqi-bv-pp") << "Adding " << vars.size() << " variables..." << std::endl; - ce_vars.insert(ce_vars.end(), vars.begin(), vars.end()); + ceVars.insert(ceVars.end(), vars.begin(), vars.end()); } } diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h index 3ad45d5be..6f6c216f6 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h @@ -168,32 +168,32 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess ~BvInstantiatorPreprocess() override {} /** register counterexample lemma * - * This method modifies the contents of lems based on the extract terms - * it contains when the option --cbqi-bv-rm-extract is enabled. It introduces + * This method adds to auxLems based on the extract terms that lem + * contains when the option --cbqi-bv-rm-extract is enabled. It introduces * a dummy equality so that segments of terms t under extracts can be solved * independently. * - * For example: + * For example, if lem is: * P[ ((extract 7 4) t), ((extract 3 0) t)] - * becomes: - * P[((extract 7 4) t), ((extract 3 0) t)] ^ + * then we add: * t = concat( x74, x30 ) - * where x74 and x30 are fresh variables of type BV_4. + * to auxLems, where x74 and x30 are fresh variables of type BV_4, which are + * added to ceVars. * - * Another example: + * Another example, for: * P[ ((extract 7 3) t), ((extract 4 0) t)] - * becomes: - * P[((extract 7 4) t), ((extract 3 0) t)] ^ + * we add: * t = concat( x75, x44, x30 ) - * where x75, x44 and x30 are fresh variables of type BV_3, BV_1, and BV_4 - * respectively. + * to auxLems where x75, x44 and x30 are fresh variables of type BV_3, BV_1, + * and BV_4 respectively, which are added to ceVars. * - * Notice we leave the original conjecture alone. This is done for performance + * Notice we leave the original lem alone. This is done for performance * since the added equalities ensure we are able to construct the proper * solved forms for variables in t and for the intermediate variables above. */ - void registerCounterexampleLemma(std::vector<Node>& lems, - std::vector<Node>& ce_vars) override; + void registerCounterexampleLemma(Node lem, + std::vector<Node>& ceVars, + std::vector<Node>& auxLems) override; private: /** collect extracts diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 186024219..95a4037fc 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -21,7 +21,6 @@ #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" -#include "smt/term_formula_removal.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/first_order_model.h" @@ -1571,18 +1570,21 @@ void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) } } -void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) { +void CegInstantiator::registerCounterexampleLemma(Node lem, + std::vector<Node>& ceVars, + std::vector<Node>& auxLems) +{ Trace("cegqi-reg") << "Register counterexample lemma..." << std::endl; d_input_vars.clear(); - d_input_vars.insert(d_input_vars.end(), ce_vars.begin(), ce_vars.end()); + d_input_vars.insert(d_input_vars.end(), ceVars.begin(), ceVars.end()); //Assert( d_vars.empty() ); d_vars.clear(); registerTheoryId(THEORY_UF); - for (unsigned i = 0; i < ce_vars.size(); i++) + for (const Node& cv : ceVars) { - Trace("cegqi-reg") << " register input variable : " << ce_vars[i] << std::endl; - registerVariable(ce_vars[i]); + Trace("cegqi-reg") << " register input variable : " << cv << std::endl; + registerVariable(cv); } // preprocess with all relevant instantiator preprocessors @@ -1592,7 +1594,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st pvars.insert(pvars.end(), d_vars.begin(), d_vars.end()); for (std::pair<const TheoryId, InstantiatorPreprocess*>& p : d_tipp) { - p.second->registerCounterexampleLemma(lems, pvars); + p.second->registerCounterexampleLemma(lem, pvars, auxLems); } // must register variables generated by preprocessors Trace("cegqi-debug") << "Register variables from theory-specific methods " @@ -1600,28 +1602,43 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st << std::endl; for (unsigned i = d_input_vars.size(), size = pvars.size(); i < size; ++i) { - Trace("cegqi-reg") << " register theory preprocess variable : " << pvars[i] - << std::endl; + Trace("cegqi-reg") << " register inst preprocess variable : " << pvars[i] + << std::endl; registerVariable(pvars[i]); } - //remove ITEs - IteSkolemMap iteSkolemMap; - d_qe->getTheoryEngine()->getTermFormulaRemover()->run(lems, iteSkolemMap); - for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) { - Trace("cegqi-reg") << " register aux variable : " << i->first << std::endl; - registerVariable(i->first); - } - for( unsigned i=0; i<lems.size(); i++ ){ - Trace("cegqi-debug") << "Counterexample lemma (pre-rewrite) " << i << " : " << lems[i] << std::endl; - Node rlem = lems[i]; - rlem = Rewriter::rewrite( rlem ); - // also must preprocess to ensure that the counterexample atoms we - // collect below are identical to the atoms that we add to the CNF stream - rlem = d_qe->getTheoryEngine()->preprocess(rlem); - Trace("cegqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl; - lems[i] = rlem; + // register variables that were introduced during TheoryEngine preprocessing + std::unordered_set<Node, NodeHashFunction> ceSyms; + expr::getSymbols(lem, ceSyms); + std::unordered_set<Node, NodeHashFunction> qSyms; + expr::getSymbols(d_quant, qSyms); + // all variables that are in counterexample lemma but not in quantified + // formula + for (const Node& ces : ceSyms) + { + if (qSyms.find(ces) != qSyms.end()) + { + // a free symbol of the quantified formula. + continue; + } + if (std::find(d_vars.begin(), d_vars.end(), ces) != d_vars.end()) + { + // already processed variable + continue; + } + if (ces.getType().isBoolean()) + { + // Boolean variables, including the counterexample literal, don't matter + // since they are always assigned a model value. + continue; + } + Trace("cegqi-reg") << " register theory preprocess variable : " << ces + << std::endl; + // register the variable, which was introduced by TheoryEngine's preprocess + // method, e.g. an ITE skolem. + registerVariable(ces); } + // determine variable order: must do Reals before Ints Trace("cegqi-debug") << "Determine variable order..." << std::endl; if (!d_vars.empty()) @@ -1673,8 +1690,10 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st // the original body d_is_nested_quant = false; std::map< Node, bool > visited; - for( unsigned i=0; i<lems.size(); i++ ){ - collectCeAtoms( lems[i], visited ); + collectCeAtoms(lem, visited); + for (const Node& alem : auxLems) + { + collectCeAtoms(alem, visited); } } diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index 7351e60f0..08f7a1262 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -224,21 +224,20 @@ class CegInstantiator { void presolve(Node q); /** Register the counterexample lemma * - * lems : contains the conjuncts of the counterexample lemma of the - * quantified formula we are processing. The counterexample - * lemma is the formula { ~phi[e/x] } in Figure 1 of Reynolds - * et al. FMSD 2017. - * ce_vars : contains the variables e. Notice these are variables of - * INST_CONSTANT kind, since we do not permit bound - * variables in assertions. - * - * This method may modify the set of lemmas lems based on: - * - ITE removal, - * - Theory-specific preprocessing of instantiation lemmas. - * It may also introduce new variables to ce_vars if necessary. - */ - void registerCounterexampleLemma(std::vector<Node>& lems, - std::vector<Node>& ce_vars); + * @param lem contains the counterexample lemma of the quantified formula we + * are processing. The counterexample lemma is the formula { ~phi[e/x] } in + * Figure 1 of Reynolds et al. FMSD 2017. + * @param ce_vars contains the variables e. Notice these are variables of + * INST_CONSTANT kind, since we do not permit bound variables in assertions. + * This method may add additional variables to this vector if it decides there + * are additional auxiliary variables to solve for. + * @param auxLems : if this method decides that additional lemmas should be + * sent on the output channel, they are added to this vector, and sent out by + * the caller of this method. + */ + void registerCounterexampleLemma(Node lem, + std::vector<Node>& ce_vars, + std::vector<Node>& auxLems); //------------------------------interface for instantiators /** get quantifiers engine */ QuantifiersEngine* getQuantifiersEngine() { return d_qe; } @@ -829,8 +828,9 @@ class InstantiatorPreprocess * of counterexample lemmas, with the same contract as * CegInstantiation::registerCounterexampleLemma. */ - virtual void registerCounterexampleLemma(std::vector<Node>& lems, - std::vector<Node>& ce_vars) + virtual void registerCounterexampleLemma(Node lem, + std::vector<Node>& ceVars, + std::vector<Node>& auxLems) { } }; diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 208eb0bf8..8693f97f4 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -593,15 +593,18 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) { ce_vars.push_back(tutil->getInstantiationConstant(q, i)); } - std::vector<Node> lems; - lems.push_back(lem); CegInstantiator* cinst = getInstantiator(q); - cinst->registerCounterexampleLemma(lems, ce_vars); - for (unsigned i = 0, size = lems.size(); i < size; i++) + LemmaStatus status = d_quantEngine->getOutputChannel().lemma(lem); + Node ppLem = status.getRewrittenLemma(); + Trace("cegqi-debug") << "Counterexample lemma (post-preprocess): " << ppLem + << std::endl; + std::vector<Node> auxLems; + cinst->registerCounterexampleLemma(ppLem, ce_vars, auxLems); + for (unsigned i = 0, size = auxLems.size(); i < size; i++) { - Trace("cegqi-debug") << "Counterexample lemma " << i << " : " << lems[i] - << std::endl; - d_quantEngine->addLemma(lems[i], false); + Trace("cegqi-debug") << "Auxiliary CE lemma " << i << " : " << auxLems[i] + << std::endl; + d_quantEngine->addLemma(auxLems[i], false); } } diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 1f42c384f..8803a9df8 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -586,6 +586,11 @@ Node ExtendedRewriter::extendedRewriteAndOr(Node n) Node ExtendedRewriter::extendedRewritePullIte(Kind itek, Node n) { Assert(n.getKind() != ITE); + if (n.isClosure()) + { + // don't pull ITE out of quantifiers + return n; + } NodeManager* nm = NodeManager::currentNM(); TypeNode tn = n.getType(); std::vector<Node> children; diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index af3a94d96..91cacdc2e 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -592,139 +592,168 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) { int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl; + // register the quantifier + registerQuantifiedFormula(f); Assert(!d_qe->inConflict()); - if( optUseModel() ){ - FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc(); - if (effort==0) { - //register the quantifier - if (d_quant_cond.find(f)==d_quant_cond.end()) { - std::vector< TypeNode > types; - for(unsigned i=0; i<f[0].getNumChildren(); i++){ - types.push_back(f[0][i].getType()); + // we do not do model-based quantifier instantiation if the option + // disables it, or if the quantified formula has an unhandled type. + if (!optUseModel() || !isHandled(f)) + { + return 0; + } + FirstOrderModelFmc* fmfmc = fm->asFirstOrderModelFmc(); + if (effort == 0) + { + if (options::mbqiMode() == options::MbqiMode::NONE) + { + // just exhaustive instantiate + Node c = mkCondDefault(fmfmc, f); + d_quant_models[f].addEntry(fmfmc, c, d_false); + if (!exhaustiveInstantiate(fmfmc, f, c, -1)) + { + return 0; + } + return 1; + } + // model check the quantifier + doCheck(fmfmc, f, d_quant_models[f], f[1]); + std::vector<Node>& mcond = d_quant_models[f].d_cond; + Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl; + Assert(!mcond.empty()); + d_quant_models[f].debugPrint("fmc", Node::null(), this); + Trace("fmc") << std::endl; + + // consider all entries going to non-true + Instantiate* instq = d_qe->getInstantiate(); + for (unsigned i = 0, msize = mcond.size(); i < msize; i++) + { + if (d_quant_models[f].d_value[i] == d_true) + { + // already satisfied + continue; + } + Trace("fmc-inst") << "Instantiate based on " << mcond[i] << "..." + << std::endl; + bool hasStar = false; + std::vector<Node> inst; + for (unsigned j = 0, nchild = mcond[i].getNumChildren(); j < nchild; j++) + { + if (fmfmc->isStar(mcond[i][j])) + { + hasStar = true; + inst.push_back(fmfmc->getModelBasisTerm(mcond[i][j].getType())); + } + else + { + inst.push_back(mcond[i][j]); } - TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() ); - Node op = NodeManager::currentNM()->mkSkolem( "qfmc", typ, "op created for full-model checking" ); - d_quant_cond[f] = op; } - - if (options::mbqiMode() == options::MbqiMode::NONE) + bool addInst = true; + if (hasStar) { - //just exhaustive instantiate - Node c = mkCondDefault( fmfmc, f ); - d_quant_models[f].addEntry( fmfmc, c, d_false ); - return exhaustiveInstantiate( fmfmc, f, c, -1); + // try obvious (specified by inst) + Node ev = d_quant_models[f].evaluate(fmfmc, inst); + if (ev == d_true) + { + addInst = false; + Trace("fmc-debug") + << "...do not instantiate, evaluation was " << ev << std::endl; + } } else { - //model check the quantifier - doCheck(fmfmc, f, d_quant_models[f], f[1]); - Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl; - Assert(!d_quant_models[f].d_cond.empty()); - d_quant_models[f].debugPrint("fmc", Node::null(), this); - Trace("fmc") << std::endl; - - //consider all entries going to non-true - for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) { - if( d_quant_models[f].d_value[i]!=d_true ) { - Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl; - bool hasStar = false; - std::vector< Node > inst; - for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) { - if (fmfmc->isStar(d_quant_models[f].d_cond[i][j])) { - hasStar = true; - inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType())); - }else{ - inst.push_back(d_quant_models[f].d_cond[i][j]); - } - } - bool addInst = true; - if( hasStar ){ - //try obvious (specified by inst) - Node ev = d_quant_models[f].evaluate(fmfmc, inst); - if (ev==d_true) { - addInst = false; - Trace("fmc-debug") << "...do not instantiate, evaluation was " << ev << std::endl; - } - }else{ - //for debugging - if (Trace.isOn("fmc-test-inst")) { - Node ev = d_quant_models[f].evaluate(fmfmc, inst); - if( ev==d_true ){ - Message() << "WARNING: instantiation was true! " << f << " " - << d_quant_models[f].d_cond[i] << std::endl; - AlwaysAssert(false); - }else{ - Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl; - } - } - } - if( addInst ){ - if( options::fmfBound() ){ - std::vector< Node > cond; - cond.push_back(d_quant_cond[f]); - cond.insert( cond.end(), inst.begin(), inst.end() ); - //need to do exhaustive instantiate algorithm to set things properly (should only add one instance) - Node c = mkCond( cond ); - unsigned prevInst = d_addedLemmas; - exhaustiveInstantiate( fmfmc, f, c, -1 ); - if( d_addedLemmas==prevInst ){ - d_star_insts[f].push_back(i); - } - }else{ - //just add the instance - d_triedLemmas++; - if (d_qe->getInstantiate()->addInstantiation(f, inst, true)) - { - Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; - d_addedLemmas++; - if( d_qe->inConflict() || options::fmfOneInstPerRound() ){ - break; - } - }else{ - Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl; - //this can happen if evaluation is unknown, or if we are generalizing a star that already has a value - //if( !hasStar && d_quant_models[f].d_value[i]==d_false ){ - // Trace("fmc-warn") << "**** FMC warning: inconsistent duplicate instantiation." << std::endl; - //} - //this assertion can happen if two instantiations from this round are identical - // (0,1)->false (1,0)->false for forall xy. f( x, y ) = f( y, x ) - //Assert( hasStar || d_quant_models[f].d_value[i]!=d_false ); - //might try it next effort level - d_star_insts[f].push_back(i); - } - } - }else{ - Trace("fmc-debug-inst") << "** Instantiation was already true." << std::endl; - //might try it next effort level - d_star_insts[f].push_back(i); - } + // for debugging + if (Trace.isOn("fmc-test-inst")) + { + Node ev = d_quant_models[f].evaluate(fmfmc, inst); + if (ev == d_true) + { + Message() << "WARNING: instantiation was true! " << f << " " + << mcond[i] << std::endl; + AlwaysAssert(false); + } + else + { + Trace("fmc-test-inst") + << "...instantiation evaluated to false." << std::endl; } } } - }else{ - if (!d_star_insts[f].empty()) { - Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl; - Trace("fmc-exh") << "Definition was : " << std::endl; - d_quant_models[f].debugPrint("fmc-exh", Node::null(), this); - Trace("fmc-exh") << std::endl; - Def temp; - //simplify the exceptions? - for( int i=(d_star_insts[f].size()-1); i>=0; i--) { - //get witness for d_star_insts[f][i] - int j = d_star_insts[f][i]; - if( temp.addEntry(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){ - if( !exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j ) ){ - //something went wrong, resort to exhaustive instantiation - return 0; - } - } + if (!addInst) + { + Trace("fmc-debug-inst") + << "** Instantiation was already true." << std::endl; + // might try it next effort level + d_star_insts[f].push_back(i); + continue; + } + if (options::fmfBound()) + { + std::vector<Node> cond; + cond.push_back(d_quant_cond[f]); + cond.insert(cond.end(), inst.begin(), inst.end()); + // need to do exhaustive instantiate algorithm to set things properly + // (should only add one instance) + Node c = mkCond(cond); + unsigned prevInst = d_addedLemmas; + exhaustiveInstantiate(fmfmc, f, c, -1); + if (d_addedLemmas == prevInst) + { + d_star_insts[f].push_back(i); } + continue; + } + // just add the instance + d_triedLemmas++; + if (instq->addInstantiation(f, inst, true)) + { + Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; + d_addedLemmas++; + if (d_qe->inConflict() || options::fmfOneInstPerRound()) + { + break; + } + } + else + { + Trace("fmc-debug-inst") + << "** Instantiation was duplicate." << std::endl; + // might try it next effort level + d_star_insts[f].push_back(i); } } return 1; - }else{ - return 0; } + // Get the list of instantiation regions (described by "star entries" in the + // definition) that were not tried at the previous effort level. For each + // of these, we add one instantiation. + std::vector<Node>& mcond = d_quant_models[f].d_cond; + if (!d_star_insts[f].empty()) + { + if (Trace.isOn("fmc-exh")) + { + Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl; + Trace("fmc-exh") << "Definition was : " << std::endl; + d_quant_models[f].debugPrint("fmc-exh", Node::null(), this); + Trace("fmc-exh") << std::endl; + } + Def temp; + // simplify the exceptions? + for (int i = (d_star_insts[f].size() - 1); i >= 0; i--) + { + // get witness for d_star_insts[f][i] + int j = d_star_insts[f][i]; + if (temp.addEntry(fmfmc, mcond[j], d_quant_models[f].d_value[j])) + { + if (!exhaustiveInstantiate(fmfmc, f, mcond[j], j)) + { + // something went wrong, resort to exhaustive instantiation + return 0; + } + } + } + } + return 1; } /** Representative bound fmc entry @@ -1290,3 +1319,33 @@ Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const bool FullModelChecker::useSimpleModels() { return options::fmfFmcSimple(); } + +void FullModelChecker::registerQuantifiedFormula(Node q) +{ + if (d_quant_cond.find(q) != d_quant_cond.end()) + { + return; + } + NodeManager* nm = NodeManager::currentNM(); + std::vector<TypeNode> types; + for (const Node& v : q[0]) + { + TypeNode tn = v.getType(); + if (tn.isFunction()) + { + // we will not use model-based quantifier instantiation for q, since + // the model-based instantiation algorithm does not handle (universally + // quantified) functions + d_unhandledQuant.insert(q); + } + types.push_back(tn); + } + TypeNode typ = nm->mkFunctionType(types, nm->booleanType()); + Node op = nm->mkSkolem("qfmc", typ, "op for full-model checking"); + d_quant_cond[q] = op; +} + +bool FullModelChecker::isHandled(Node q) const +{ + return d_unhandledQuant.find(q) == d_unhandledQuant.end(); +} diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index 7dd1991f5..60de5d1eb 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -86,7 +86,16 @@ protected: Node d_false; std::map<TypeNode, std::map< Node, int > > d_rep_ids; std::map<Node, Def > d_quant_models; + /** + * The predicate for the quantified formula. This is used to express + * conditions under which the quantified formula is false in the model. + * For example, for quantified formula (forall x:Int, y:U. P), this is + * a predicate of type (Int x U) -> Bool. + */ std::map<Node, Node > d_quant_cond; + /** A set of quantified formulas that cannot be handled by model-based + * quantifier instantiation */ + std::unordered_set<Node, NodeHashFunction> d_unhandledQuant; std::map< TypeNode, Node > d_array_cond; std::map< Node, Node > d_array_term_cond; std::map< Node, std::vector< int > > d_star_insts; @@ -155,6 +164,16 @@ public: bool processBuildModel(TheoryModel* m) override; bool useSimpleModels(); + + private: + /** + * Register quantified formula. + * This checks whether q can be handled by model-based instantiation and + * initializes the necessary information if so. + */ + void registerQuantifiedFormula(Node q); + /** Is quantified formula q handled by model-based instantiation? */ + bool isHandled(Node q) const; };/* class FullModelChecker */ }/* CVC4::theory::quantifiers::fmcheck namespace */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index df86922bc..43c6e73bc 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1342,15 +1342,19 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& } Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg ){ - if( body.getKind()==FORALL ){ + NodeManager* nm = NodeManager::currentNM(); + Kind k = body.getKind(); + if (k == FORALL) + { if( ( pol || prenexAgg ) && ( options::prenexQuantUser() || body.getNumChildren()==2 ) ){ std::vector< Node > terms; std::vector< Node > subs; //for doing prenexing of same-signed quantifiers //must rename each variable that already exists - for( unsigned i=0; i<body[0].getNumChildren(); i++ ){ - terms.push_back( body[0][i] ); - subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) ); + for (const Node& v : body[0]) + { + terms.push_back(v); + subs.push_back(nm->mkBoundVar(v.getType())); } if( pol ){ args.insert( args.end(), subs.begin(), subs.end() ); @@ -1362,161 +1366,134 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s return newBody; } //must remove structure - }else if( prenexAgg && body.getKind()==kind::ITE && body.getType().isBoolean() ){ - Node nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ), - NodeManager::currentNM()->mkNode( kind::OR, body[0], body[2] ) ); + } + else if (prenexAgg && k == ITE && body.getType().isBoolean()) + { + Node nn = nm->mkNode(AND, + nm->mkNode(OR, body[0].notNode(), body[1]), + nm->mkNode(OR, body[0], body[2])); return computePrenex( nn, args, nargs, pol, prenexAgg ); - }else if( prenexAgg && body.getKind()==kind::EQUAL && body[0].getType().isBoolean() ){ - Node nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ), - NodeManager::currentNM()->mkNode( kind::OR, body[0], body[1].notNode() ) ); + } + else if (prenexAgg && k == EQUAL && body[0].getType().isBoolean()) + { + Node nn = nm->mkNode(AND, + nm->mkNode(OR, body[0].notNode(), body[1]), + nm->mkNode(OR, body[0], body[1].notNode())); return computePrenex( nn, args, nargs, pol, prenexAgg ); }else if( body.getType().isBoolean() ){ - Assert(body.getKind() != EXISTS); + Assert(k != EXISTS); bool childrenChanged = false; std::vector< Node > newChildren; - for( unsigned i=0; i<body.getNumChildren(); i++ ){ + for (size_t i = 0, nchild = body.getNumChildren(); i < nchild; i++) + { bool newHasPol; bool newPol; QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol ); - if( newHasPol ){ - Node n = computePrenex( body[i], args, nargs, newPol, prenexAgg ); - newChildren.push_back( n ); - if( n!=body[i] ){ - childrenChanged = true; - } - }else{ + if (!newHasPol) + { newChildren.push_back( body[i] ); + continue; } + Node n = computePrenex(body[i], args, nargs, newPol, prenexAgg); + newChildren.push_back(n); + childrenChanged = n != body[i] || childrenChanged; } if( childrenChanged ){ - if( body.getKind()==NOT && newChildren[0].getKind()==NOT ){ + if (k == NOT && newChildren[0].getKind() == NOT) + { return newChildren[0][0]; - }else{ - return NodeManager::currentNM()->mkNode( body.getKind(), newChildren ); } + return nm->mkNode(k, newChildren); } } return body; } -Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel, std::map< unsigned, std::map< Node, Node > >& visited ){ - unsigned tindex = topLevel ? 0 : 1; - std::map< Node, Node >::iterator itv = visited[tindex].find( n ); - if( itv!=visited[tindex].end() ){ +Node QuantifiersRewriter::computePrenexAgg(Node n, + std::map<Node, Node>& visited) +{ + std::map< Node, Node >::iterator itv = visited.find( n ); + if( itv!=visited.end() ){ return itv->second; } - if (expr::hasClosure(n)) + if (!expr::hasClosure(n)) + { + // trivial + return n; + } + NodeManager* nm = NodeManager::currentNM(); + Node ret = n; + if (n.getKind() == NOT) + { + ret = computePrenexAgg(n[0], visited).negate(); + } + else if (n.getKind() == FORALL) { - Node ret = n; - if (topLevel - && options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL - && (n.getKind() == AND || (n.getKind() == NOT && n[0].getKind() == OR))) + std::vector<Node> children; + children.push_back(computePrenexAgg(n[1], visited)); + std::vector<Node> args; + args.insert(args.end(), n[0].begin(), n[0].end()); + // for each child, strip top level quant + for (unsigned i = 0; i < children.size(); i++) { - std::vector< Node > children; - Node nc = n.getKind()==NOT ? n[0] : n; - for( unsigned i=0; i<nc.getNumChildren(); i++ ){ - Node ncc = computePrenexAgg( nc[i], true, visited ); - if( n.getKind()==NOT ){ - ncc = ncc.negate(); - } - children.push_back( ncc ); + if (children[i].getKind() == FORALL) + { + args.insert(args.end(), children[i][0].begin(), children[i][0].end()); + children[i] = children[i][1]; } - ret = NodeManager::currentNM()->mkNode( AND, children ); } - else if (n.getKind() == NOT) + // keep the pattern + std::vector<Node> iplc; + if (n.getNumChildren() == 3) { - ret = computePrenexAgg( n[0], false, visited ).negate(); + iplc.insert(iplc.end(), n[2].begin(), n[2].end()); } - else if (n.getKind() == FORALL) + Node nb = children.size() == 1 ? children[0] : nm->mkNode(OR, children); + ret = mkForall(args, nb, iplc, true); + } + else + { + std::vector<Node> args; + std::vector<Node> nargs; + Node nn = computePrenex(n, args, nargs, true, true); + if (n != nn) { - /* - Node nn = computePrenexAgg( n[1], false ); - if( nn!=n[1] ){ - if( n.getNumChildren()==2 ){ - return NodeManager::currentNM()->mkNode( FORALL, n[0], nn ); - }else{ - return NodeManager::currentNM()->mkNode( FORALL, n[0], nn, n[2] ); - } - } - */ - std::vector< Node > children; - if (n[1].getKind() == OR - && options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL) + Node nnn = computePrenexAgg(nn, visited); + // merge prenex + if (nnn.getKind() == FORALL) { - for( unsigned i=0; i<n[1].getNumChildren(); i++ ){ - children.push_back( computePrenexAgg( n[1][i], false, visited ) ); + args.insert(args.end(), nnn[0].begin(), nnn[0].end()); + nnn = nnn[1]; + // pos polarity variables are inner + if (!args.empty()) + { + nnn = mkForall(args, nnn, true); } + args.clear(); } - else + else if (nnn.getKind() == NOT && nnn[0].getKind() == FORALL) { - children.push_back( computePrenexAgg( n[1], false, visited ) ); + nargs.insert(nargs.end(), nnn[0][0].begin(), nnn[0][0].end()); + nnn = nnn[0][1].negate(); } - std::vector< Node > args; - for( unsigned i=0; i<n[0].getNumChildren(); i++ ){ - args.push_back( n[0][i] ); + if (!nargs.empty()) + { + nnn = mkForall(nargs, nnn.negate(), true).negate(); } - std::vector< Node > nargs; - //for each child, strip top level quant - for( unsigned i=0; i<children.size(); i++ ){ - if( children[i].getKind()==FORALL ){ - for( unsigned j=0; j<children[i][0].getNumChildren(); j++ ){ - args.push_back( children[i][0][j] ); - } - children[i] = children[i][1]; - } + if (!args.empty()) + { + nnn = mkForall(args, nnn, true); } - // keep the pattern - std::vector< Node > iplc; - if( n.getNumChildren()==3 ){ - for( unsigned i=0; i<n[2].getNumChildren(); i++ ){ - iplc.push_back( n[2][i] ); - } - } - Node nb = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ); - ret = mkForall( args, nb, iplc, true ); + ret = nnn; } else { - std::vector< Node > args; - std::vector< Node > nargs; - Node nn = computePrenex( n, args, nargs, true, true ); - if( n!=nn ){ - Node nnn = computePrenexAgg( nn, false, visited ); - //merge prenex - if( nnn.getKind()==FORALL ){ - for( unsigned i=0; i<nnn[0].getNumChildren(); i++ ){ - args.push_back( nnn[0][i] ); - } - nnn = nnn[1]; - //pos polarity variables are inner - if( !args.empty() ){ - nnn = mkForall( args, nnn, true ); - } - args.clear(); - }else if( nnn.getKind()==NOT && nnn[0].getKind()==FORALL ){ - for( unsigned i=0; i<nnn[0][0].getNumChildren(); i++ ){ - nargs.push_back( nnn[0][0][i] ); - } - nnn = nnn[0][1].negate(); - } - if( !nargs.empty() ){ - nnn = mkForall( nargs, nnn.negate(), true ).negate(); - } - if( !args.empty() ){ - nnn = mkForall( args, nnn, true ); - } - ret = nnn; - }else{ - Assert(args.empty()); - Assert(nargs.empty()); - } + Assert(args.empty()); + Assert(nargs.empty()); } - visited[tindex][n] = ret; - return ret; } - return n; + visited[n] = ret; + return ret; } Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) { @@ -1925,8 +1902,7 @@ Node QuantifiersRewriter::computeOperation(Node f, if( computeOption==COMPUTE_ELIM_SYMBOLS ){ n = computeElimSymbols( n ); }else if( computeOption==COMPUTE_MINISCOPING ){ - if (options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL - || options::prenexQuant() == options::PrenexQuantMode::NORMAL) + if (options::prenexQuant() == options::PrenexQuantMode::NORMAL) { if( !qa.d_qid_num.isNull() ){ //already processed this, return self @@ -1957,8 +1933,7 @@ Node QuantifiersRewriter::computeOperation(Node f, } else if (computeOption == COMPUTE_PRENEX) { - if (options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL - || options::prenexQuant() == options::PrenexQuantMode::NORMAL) + if (options::prenexQuant() == options::PrenexQuantMode::NORMAL) { //will rewrite at preprocess time return f; @@ -2091,12 +2066,11 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { } } //pull all quantifiers globally - if (options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL - || options::prenexQuant() == options::PrenexQuantMode::NORMAL) + if (options::prenexQuant() == options::PrenexQuantMode::NORMAL) { Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl; - std::map< unsigned, std::map< Node, Node > > visited; - n = computePrenexAgg( n, true, visited ); + std::map<Node, Node> visited; + n = computePrenexAgg(n, visited); n = Rewriter::rewrite( n ); Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl; //Assert( isPrenexNormalForm( n ) ); diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 2a3180e78..c8995ef4e 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -234,8 +234,27 @@ class QuantifiersRewriter : public TheoryRewriter static Node computeElimSymbols( Node body ); static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body ); + /** + * This function removes top-level quantifiers from subformulas of body + * appearing with overall polarity pol. It adds quantified variables that + * appear in positive polarity positions into args, and those at negative + * polarity positions in nargs. + * + * If prenexAgg is true, we ensure that all top-level quantifiers are + * eliminated from subformulas. This means that we must expand ITE and + * Boolean equalities to ensure that quantifiers are at fixed polarities. + * + * For example, calling this function on: + * (or (forall ((x Int)) (P x z)) (not (forall ((y Int)) (Q y z)))) + * would return: + * (or (P x z) (not (Q y z))) + * and add {x} to args, and {y} to nargs. + */ static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg ); - static Node computePrenexAgg( Node n, bool topLevel, std::map< unsigned, std::map< Node, Node > >& visited ); + /** + * Apply prenexing aggressively. Returns the prenex normal form of n. + */ + static Node computePrenexAgg(Node n, std::map<Node, Node>& visited); static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ); private: static Node computeOperation(Node f, diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index a58c5d841..ef2e7e445 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -19,7 +19,6 @@ #include "expr/dtype.h" #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" -#include "printer/sygus_print_callback.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" @@ -58,6 +57,12 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, for (const Node& s : symset) { TypeNode tn = s.getType(); + if (tn.isConstructor() || tn.isSelector() || tn.isTester()) + { + // datatype symbols should be considered interpreted symbols here, not + // (higher-order) variables. + continue; + } // Notice that we allow for non-first class (e.g. function) variables here. // This is applicable to the case where we are doing get-abduct in a logic // with UF. @@ -73,8 +78,6 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, SygusVarToTermAttribute sta; vlv.setAttribute(sta, s); } - // make the sygus variable list - Node abvl = nm->mkNode(BOUND_VAR_LIST, varlist); Trace("sygus-abduct-debug") << "...finish" << std::endl; Trace("sygus-abduct-debug") << "Make abduction predicate..." << std::endl; @@ -84,163 +87,23 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, Node abd = nm->mkBoundVar(name.c_str(), abdType); Trace("sygus-abduct-debug") << "...finish" << std::endl; - // if provided, we will associate it with the function-to-synthesize + // the sygus variable list + Node abvl; + // if provided, we will associate the provide sygus datatype type with the + // function-to-synthesize. However, we must convert it so that its + // free symbols are universally quantified. if (!abdGType.isNull()) { Assert(abdGType.isDatatype() && abdGType.getDType().isSygus()); - // must convert all constructors to version with bound variables in "vars" - std::vector<SygusDatatype> sdts; - std::set<Type> unres; - Trace("sygus-abduct-debug") << "Process abduction type:" << std::endl; Trace("sygus-abduct-debug") << abdGType.getDType().getName() << std::endl; - // datatype types we need to process - std::vector<TypeNode> dtToProcess; - // datatype types we have processed - std::map<TypeNode, TypeNode> dtProcessed; - dtToProcess.push_back(abdGType); - std::stringstream ssutn0; - ssutn0 << abdGType.getDType().getName() << "_s"; - TypeNode abdTNew = - nm->mkSort(ssutn0.str(), ExprManager::SORT_FLAG_PLACEHOLDER); - unres.insert(abdTNew.toType()); - dtProcessed[abdGType] = abdTNew; - - // We must convert all symbols in the sygus datatype type abdGType to - // apply the substitution { syms -> varlist }, where syms is the free - // variables of the input problem, and varlist is the formal argument list - // of the abduct-to-synthesize. For example, given user-provided sygus - // grammar: - // G -> a | +( b, G ) - // we synthesize a abduct A with two arguments x_a and x_b corresponding to - // a and b, and reconstruct the grammar: - // G' -> x_a | +( x_b, G' ) - // In this way, x_a and x_b are treated as bound variables and handled as - // arguments of the abduct-to-synthesize instead of as free variables with - // no relation to A. We additionally require that x_a, when printed, prints - // "a", which we do with a custom sygus callback below. + // substitute the free symbols of the grammar with variables corresponding + // to the formal argument list of the new sygus datatype type. + TypeNode abdGTypeS = datatypes::utils::substituteAndGeneralizeSygusType( + abdGType, syms, varlist); - // We are traversing over the subfield types of the datatype to convert - // them into the form described above. - while (!dtToProcess.empty()) - { - std::vector<TypeNode> dtNextToProcess; - for (const TypeNode& curr : dtToProcess) - { - Assert(curr.isDatatype() && curr.getDType().isSygus()); - const DType& dtc = curr.getDType(); - std::stringstream ssdtn; - ssdtn << dtc.getName() << "_s"; - sdts.push_back(SygusDatatype(ssdtn.str())); - Trace("sygus-abduct-debug") - << "Process datatype " << sdts.back().getName() << "..." - << std::endl; - for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++) - { - Node op = dtc[j].getSygusOp(); - // apply the substitution to the argument - Node ops = op.substitute( - syms.begin(), syms.end(), varlist.begin(), varlist.end()); - Trace("sygus-abduct-debug") << " Process constructor " << op << " / " - << ops << "..." << std::endl; - std::vector<TypeNode> cargs; - for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++) - { - TypeNode argt = dtc[j].getArgType(k); - std::map<TypeNode, TypeNode>::iterator itdp = - dtProcessed.find(argt); - TypeNode argtNew; - if (itdp == dtProcessed.end()) - { - std::stringstream ssutn; - ssutn << argt.getDType().getName() << "_s"; - argtNew = - nm->mkSort(ssutn.str(), ExprManager::SORT_FLAG_PLACEHOLDER); - Trace("sygus-abduct-debug") - << " ...unresolved type " << argtNew << " for " << argt - << std::endl; - unres.insert(argtNew.toType()); - dtProcessed[argt] = argtNew; - dtNextToProcess.push_back(argt); - } - else - { - argtNew = itdp->second; - } - Trace("sygus-abduct-debug") - << " Arg #" << k << ": " << argtNew << std::endl; - cargs.push_back(argtNew); - } - // callback prints as the expression - std::shared_ptr<SygusPrintCallback> spc; - std::vector<Expr> args; - if (op.getKind() == LAMBDA) - { - Node opBody = op[1]; - for (const Node& v : op[0]) - { - args.push_back(v.toExpr()); - } - spc = std::make_shared<printer::SygusExprPrintCallback>( - opBody.toExpr(), args); - } - else if (cargs.empty()) - { - spc = std::make_shared<printer::SygusExprPrintCallback>(op.toExpr(), - args); - } - std::stringstream ss; - ss << ops.getKind(); - Trace("sygus-abduct-debug") - << "Add constructor : " << ops << std::endl; - sdts.back().addConstructor(ops, ss.str(), cargs, spc); - } - Trace("sygus-abduct-debug") - << "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl; - TypeNode stn = dtc.getSygusType(); - sdts.back().initializeDatatype( - stn, abvl, dtc.getSygusAllowConst(), dtc.getSygusAllowAll()); - } - dtToProcess.clear(); - dtToProcess.insert( - dtToProcess.end(), dtNextToProcess.begin(), dtNextToProcess.end()); - } - Trace("sygus-abduct-debug") - << "Make " << sdts.size() << " datatype types..." << std::endl; - // extract the datatypes - std::vector<Datatype> datatypes; - for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++) - { - datatypes.push_back(sdts[i].getDatatype()); - } - // make the datatype types - std::vector<DatatypeType> datatypeTypes = - nm->toExprManager()->mkMutualDatatypeTypes( - datatypes, unres, ExprManager::DATATYPE_FLAG_PLACEHOLDER); - TypeNode abdGTypeS = TypeNode::fromType(datatypeTypes[0]); - if (Trace.isOn("sygus-abduct-debug")) - { - Trace("sygus-abduct-debug") << "Made datatype types:" << std::endl; - for (unsigned j = 0, ndts = datatypeTypes.size(); j < ndts; j++) - { - const DType& dtj = TypeNode::fromType(datatypeTypes[j]).getDType(); - Trace("sygus-abduct-debug") << "#" << j << ": " << dtj << std::endl; - for (unsigned k = 0, ncons = dtj.getNumConstructors(); k < ncons; k++) - { - for (unsigned l = 0, nargs = dtj[k].getNumArgs(); l < nargs; l++) - { - if (!dtj[k].getArgType(l).isDatatype()) - { - Trace("sygus-abduct-debug") - << "Argument " << l << " of " << dtj[k] - << " is not datatype : " << dtj[k].getArgType(l) << std::endl; - AlwaysAssert(false); - } - } - } - } - } + Assert(abdGTypeS.isDatatype() && abdGTypeS.getDType().isSygus()); Trace("sygus-abduct-debug") << "Make sygus grammar attribute..." << std::endl; @@ -250,6 +113,19 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, theory::SygusSynthGrammarAttribute ssg; abd.setAttribute(ssg, sym); Trace("sygus-abduct-debug") << "Finished setting up grammar." << std::endl; + + // use the bound variable list from the new substituted grammar type + const DType& agtsd = abdGTypeS.getDType(); + abvl = agtsd.getSygusVarList(); + Assert(!abvl.isNull() && abvl.getKind() == BOUND_VAR_LIST); + } + else + { + // the bound variable list of the abduct-to-synthesize is determined by + // the variable list above + abvl = nm->mkNode(BOUND_VAR_LIST, varlist); + // We do not set a grammar type for abd (SygusSynthGrammarAttribute). + // Its grammar will be constructed internally in the default way } Trace("sygus-abduct-debug") << "Make abduction predicate app..." << std::endl; diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 06f05a8af..800847ffe 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -58,6 +58,27 @@ constant CONST_STRING \ "util/string.h" \ "a string of characters" +# the type +operator SEQUENCE_TYPE 1 "seuence type, takes as parameter the type of the elements" +cardinality SEQUENCE_TYPE \ + "::CVC4::theory::strings::SequenceProperties::computeCardinality(%TYPE%)" \ + "theory/strings/theory_strings_type_rules.h" +well-founded SEQUENCE_TYPE \ + "::CVC4::theory::strings::SequenceProperties::isWellFounded(%TYPE%)" \ + "::CVC4::theory::strings::SequenceProperties::mkGroundTerm(%TYPE%)" \ + "theory/strings/theory_strings_type_rules.h" +enumerator SEQUENCE_TYPE \ + "::CVC4::theory::strings::SequenceEnumerator" \ + "theory/strings/type_enumerator.h" + +constant CONST_SEQUENCE \ + ::CVC4::ExprSequence \ + ::CVC4::ExprSequenceHashFunction \ + "expr/expr_sequence.h" \ + "a sequence of characters" + +operator SEQ_UNIT 1 "a sequence of length one" + # equal equal / less than / output operator STRING_TO_REGEXP 1 "convert string to regexp" operator REGEXP_CONCAT 2: "regexp concat" @@ -138,4 +159,9 @@ typerule STRING_FROM_CODE "SimpleTypeRule<RString, AInteger>" typerule STRING_TOUPPER "SimpleTypeRule<RString, AString>" typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>" +### sequence specific operators + +typerule CONST_SEQUENCE ::CVC4::theory::strings::ConstSequenceTypeRule +typerule SEQ_UNIT ::CVC4::theory::strings::SeqUnitTypeRule + endtheory diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp index 2953a2b3c..a4055c4f9 100644 --- a/src/theory/strings/rewrites.cpp +++ b/src/theory/strings/rewrites.cpp @@ -200,6 +200,7 @@ const char* toString(Rewrite r) case Rewrite::LEN_REPL_INV: return "LEN_REPL_INV"; case Rewrite::LEN_CONV_INV: return "LEN_CONV_INV"; case Rewrite::CHARAT_ELIM: return "CHARAT_ELIM"; + case Rewrite::SEQ_UNIT_EVAL: return "SEQ_UNIT_EVAL"; default: return "?"; } } diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h index 7a315ebd3..96a3b65fd 100644 --- a/src/theory/strings/rewrites.h +++ b/src/theory/strings/rewrites.h @@ -202,7 +202,8 @@ enum class Rewrite : uint32_t LEN_CONCAT, LEN_REPL_INV, LEN_CONV_INV, - CHARAT_ELIM + CHARAT_ELIM, + SEQ_UNIT_EVAL }; /** diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 2d2ec0af0..4f74d7c15 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -264,7 +264,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) // Add a constant string to the side with more `cn`s to restore // the difference in number of `cn`s std::vector<Node> vec(diff, cn); - trimmed[j].push_back(Word::mkWord(vec)); + trimmed[j].push_back(Word::mkWordFlatten(vec)); } } @@ -602,7 +602,7 @@ Node SequencesRewriter::rewriteConcat(Node node) std::vector<Node> wvec; wvec.push_back(preNode); wvec.push_back(tmpNode[0]); - preNode = Word::mkWord(wvec); + preNode = Word::mkWordFlatten(wvec); node_vec.push_back(preNode); } else @@ -644,7 +644,7 @@ Node SequencesRewriter::rewriteConcat(Node node) std::vector<Node> vec; vec.push_back(preNode); vec.push_back(tmpNode); - preNode = Word::mkWord(vec); + preNode = Word::mkWordFlatten(vec); } } } @@ -1461,6 +1461,10 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node) { retNode = rewriteRepeatRegExp(node); } + else if (nk == SEQ_UNIT) + { + retNode = rewriteSeqUnit(node); + } Trace("sequences-postrewrite") << "Strings::SequencesRewriter::postRewrite returning " << retNode @@ -3095,6 +3099,19 @@ Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype) return res; } +Node SequencesRewriter::rewriteSeqUnit(Node node) +{ + NodeManager* nm = NodeManager::currentNM(); + if (node[0].isConst()) + { + std::vector<Expr> seq; + seq.push_back(node[0].toExpr()); + TypeNode stype = nm->mkSequenceType(node[0].getType()); + Node ret = nm->mkConst(ExprSequence(stype.toType(), seq)); + return returnRewrite(node, ret, Rewrite::SEQ_UNIT_EVAL); + } + return node; +} Node SequencesRewriter::returnRewrite(Node node, Node ret, Rewrite r) { diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h index 56b74f536..490dd8b3c 100644 --- a/src/theory/strings/sequences_rewriter.h +++ b/src/theory/strings/sequences_rewriter.h @@ -224,6 +224,12 @@ class SequencesRewriter : public TheoryRewriter * Returns the rewritten form of node. */ Node rewriteStringToCode(Node node); + /** rewrite seq.unit + * This is the entry point for post-rewriting terms n of the form + * seq.unit( t ) + * Returns the rewritten form of node. + */ + Node rewriteSeqUnit(Node node); /** length preserving rewrite * diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index ec034b0c9..6330d7c10 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -374,6 +374,13 @@ Node TermRegistry::getRegisterTermAtomicLemma(Node n, LengthStatus s, std::map<Node, bool>& reqPhase) { + if (n.isConst()) + { + // No need to send length for constant terms. This case may be triggered + // for cases where the skolem cache automatically replaces a skolem by + // a constant. + return Node::null(); + } Assert(n.getType().isStringLike()); NodeManager* nm = NodeManager::currentNM(); Node n_len = nm->mkNode(kind::STRING_LENGTH, n); @@ -433,14 +440,6 @@ Node TermRegistry::getRegisterTermAtomicLemma(Node n, Assert(false); } - // additionally add len( x ) >= 0 ? - if (options::stringLenGeqZ()) - { - Node n_len_geq = nm->mkNode(kind::GEQ, n_len, d_zero); - n_len_geq = Rewriter::rewrite(n_len_geq); - lems.push_back(n_len_geq); - } - if (lems.empty()) { return Node::null(); diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 939146a3d..50c6ede62 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -38,48 +38,45 @@ StringsPreprocess::StringsPreprocess(SkolemCache* sc, SequencesStatistics& stats) : d_sc(sc), d_statistics(stats) { - //Constants - d_zero = NodeManager::currentNM()->mkConst(Rational(0)); - d_one = NodeManager::currentNM()->mkConst(Rational(1)); - d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); } StringsPreprocess::~StringsPreprocess(){ } -Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { - unsigned prev_new_nodes = new_nodes.size(); - Trace("strings-preprocess-debug") << "StringsPreprocess::simplify: " << t << std::endl; +Node StringsPreprocess::reduce(Node t, + std::vector<Node>& asserts, + SkolemCache* sc) +{ + Trace("strings-preprocess-debug") + << "StringsPreprocess::reduce: " << t << std::endl; Node retNode = t; - NodeManager *nm = NodeManager::currentNM(); + NodeManager* nm = NodeManager::currentNM(); + Node zero = nm->mkConst(Rational(0)); + Node one = nm->mkConst(Rational(1)); + Node negOne = nm->mkConst(Rational(-1)); if( t.getKind() == kind::STRING_SUBSTR ) { // processing term: substr( s, n, m ) Node s = t[0]; Node n = t[1]; Node m = t[2]; - Node skt = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst"); + Node skt = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst"); Node t12 = nm->mkNode(PLUS, n, m); t12 = Rewriter::rewrite(t12); Node lt0 = nm->mkNode(STRING_LENGTH, s); //start point is greater than or equal zero - Node c1 = nm->mkNode(GEQ, n, d_zero); + Node c1 = nm->mkNode(GEQ, n, zero); //start point is less than end of string Node c2 = nm->mkNode(GT, lt0, n); //length is positive - Node c3 = nm->mkNode(GT, m, d_zero); + Node c3 = nm->mkNode(GT, m, zero); Node cond = nm->mkNode(AND, c1, c2, c3); Node emp = Word::mkEmptyWord(t.getType()); - Node sk1 = n == d_zero ? emp - : d_sc->mkSkolemCached( - s, n, SkolemCache::SK_PREFIX, "sspre"); - Node sk2 = ArithEntail::check(t12, lt0) - ? emp - : d_sc->mkSkolemCached( - s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr"); + Node sk1 = sc->mkSkolemCached(s, n, SkolemCache::SK_PREFIX, "sspre"); + Node sk2 = sc->mkSkolemCached(s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr"); Node b11 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, skt, sk2)); //length of first skolem is second argument Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n); @@ -89,7 +86,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node b13 = nm->mkNode( OR, nm->mkNode(EQUAL, lsk2, nm->mkNode(MINUS, lt0, nm->mkNode(PLUS, n, m))), - nm->mkNode(EQUAL, lsk2, d_zero)); + nm->mkNode(EQUAL, lsk2, zero)); // Length of the result is at most m Node b14 = nm->mkNode(LEQ, nm->mkNode(STRING_LENGTH, skt), m); @@ -112,7 +109,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // satisfied. If n + m is less than the length of s, then len(sk2) = 0 // cannot be satisfied because we have the constraint that len(skt) <= m, // so sk2 must be greater than 0. - new_nodes.push_back( lemma ); + asserts.push_back(lemma); // Thus, substr( s, n, m ) = skt retNode = skt; @@ -123,15 +120,16 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node x = t[0]; Node y = t[1]; Node n = t[2]; - Node skk = nm->mkSkolem("iok", nm->integerType(), "created for indexof"); + Node skk = sc->mkTypedSkolemCached( + nm->integerType(), t, SkolemCache::SK_PURIFY, "iok"); Node negone = nm->mkConst(Rational(-1)); Node krange = nm->mkNode(GEQ, skk, negone); // assert: indexof( x, y, n ) >= -1 - new_nodes.push_back( krange ); + asserts.push_back(krange); krange = nm->mkNode(GEQ, nm->mkNode(STRING_LENGTH, x), skk); // assert: len( x ) >= indexof( x, y, z ) - new_nodes.push_back( krange ); + asserts.push_back(krange); // substr( x, n, len( x ) - n ) Node st = nm->mkNode(STRING_SUBSTR, @@ -139,16 +137,16 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { n, nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, x), n)); Node io2 = - d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_PRE, "iopre"); + sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_PRE, "iopre"); Node io4 = - d_sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_POST, "iopost"); + sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_POST, "iopost"); // ~contains( substr( x, n, len( x ) - n ), y ) Node c11 = nm->mkNode(STRING_STRCTN, st, y).negate(); // n > len( x ) Node c12 = nm->mkNode(GT, n, nm->mkNode(STRING_LENGTH, x)); // 0 > n - Node c13 = nm->mkNode(GT, d_zero, n); + Node c13 = nm->mkNode(GT, zero, n); Node cond1 = nm->mkNode(OR, c11, c12, c13); // skk = -1 Node cc1 = skk.eqNode(negone); @@ -171,8 +169,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { nm->mkNode( STRING_SUBSTR, y, - d_zero, - nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, y), d_one))), + zero, + nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, y), one))), y) .negate(); // skk = n + len( io2 ) @@ -189,7 +187,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // skk = n + len( io2 ) // for fresh io2, io4. Node rr = nm->mkNode(ITE, cond1, cc1, nm->mkNode(ITE, cond2, cc2, cc3)); - new_nodes.push_back( rr ); + asserts.push_back(rr); // Thus, indexof( x, y, n ) = skk. retNode = skk; @@ -198,7 +196,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { { // processing term: int.to.str( n ) Node n = t[0]; - Node itost = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "itost"); + Node itost = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "itost"); Node leni = nm->mkNode(STRING_LENGTH, itost); std::vector<Node> conc; @@ -206,21 +204,20 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { argTypes.push_back(nm->integerType()); Node u = nm->mkSkolem("U", nm->mkFunctionType(argTypes, nm->integerType())); - Node lem = nm->mkNode(GEQ, leni, d_one); + Node lem = nm->mkNode(GEQ, leni, one); conc.push_back(lem); lem = n.eqNode(nm->mkNode(APPLY_UF, u, leni)); conc.push_back(lem); - lem = d_zero.eqNode(nm->mkNode(APPLY_UF, u, d_zero)); + lem = zero.eqNode(nm->mkNode(APPLY_UF, u, zero)); conc.push_back(lem); - Node x = nm->mkBoundVar(nm->integerType()); - Node xPlusOne = nm->mkNode(PLUS, x, d_one); + Node x = SkolemCache::mkIndexVar(t); + Node xPlusOne = nm->mkNode(PLUS, x, one); Node xbv = nm->mkNode(BOUND_VAR_LIST, x); - Node g = - nm->mkNode(AND, nm->mkNode(GEQ, x, d_zero), nm->mkNode(LT, x, leni)); - Node sx = nm->mkNode(STRING_SUBSTR, itost, x, d_one); + Node g = nm->mkNode(AND, nm->mkNode(GEQ, x, zero), nm->mkNode(LT, x, leni)); + Node sx = nm->mkNode(STRING_SUBSTR, itost, x, one); Node ux = nm->mkNode(APPLY_UF, u, x); Node ux1 = nm->mkNode(APPLY_UF, u, xPlusOne); Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0"))); @@ -229,10 +226,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node ten = nm->mkConst(Rational(10)); Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux))); Node leadingZeroPos = - nm->mkNode(AND, x.eqNode(d_zero), nm->mkNode(GT, leni, d_one)); + nm->mkNode(AND, x.eqNode(zero), nm->mkNode(GT, leni, one)); Node cb = nm->mkNode( AND, - nm->mkNode(GEQ, c, nm->mkNode(ITE, leadingZeroPos, d_one, d_zero)), + nm->mkNode(GEQ, c, nm->mkNode(ITE, leadingZeroPos, one, zero)), nm->mkNode(LT, c, ten)); Node ux1lem = nm->mkNode(GEQ, n, ux1); @@ -241,11 +238,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { lem = nm->mkNode(FORALL, xbv, lem); conc.push_back(lem); - Node nonneg = nm->mkNode(GEQ, n, d_zero); + Node nonneg = nm->mkNode(GEQ, n, zero); Node emp = Word::mkEmptyWord(t.getType()); lem = nm->mkNode(ITE, nonneg, nm->mkNode(AND, conc), itost.eqNode(emp)); - new_nodes.push_back(lem); + asserts.push_back(lem); // assert: // IF n>=0 // THEN: @@ -274,26 +271,27 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { retNode = itost; } else if( t.getKind() == kind::STRING_STOI ) { Node s = t[0]; - Node stoit = nm->mkSkolem("stoit", nm->integerType(), "created for stoi"); + Node stoit = sc->mkTypedSkolemCached( + nm->integerType(), t, SkolemCache::SK_PURIFY, "stoit"); Node lens = nm->mkNode(STRING_LENGTH, s); std::vector<Node> conc1; - Node lem = stoit.eqNode(d_neg_one); + Node lem = stoit.eqNode(negOne); conc1.push_back(lem); Node emp = Word::mkEmptyWord(s.getType()); Node sEmpty = s.eqNode(emp); Node k = nm->mkSkolem("k", nm->integerType()); - Node kc1 = nm->mkNode(GEQ, k, d_zero); + Node kc1 = nm->mkNode(GEQ, k, zero); Node kc2 = nm->mkNode(LT, k, lens); Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0"))); Node codeSk = nm->mkNode( MINUS, - nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, d_one)), + nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, one)), c0); Node ten = nm->mkConst(Rational(10)); Node kc3 = nm->mkNode( - OR, nm->mkNode(LT, codeSk, d_zero), nm->mkNode(GEQ, codeSk, ten)); + OR, nm->mkNode(LT, codeSk, zero), nm->mkNode(GEQ, codeSk, ten)); conc1.push_back(nm->mkNode(OR, sEmpty, nm->mkNode(AND, kc1, kc2, kc3))); std::vector<Node> conc2; @@ -304,24 +302,22 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { lem = stoit.eqNode(nm->mkNode(APPLY_UF, u, lens)); conc2.push_back(lem); - lem = d_zero.eqNode(nm->mkNode(APPLY_UF, u, d_zero)); + lem = zero.eqNode(nm->mkNode(APPLY_UF, u, zero)); conc2.push_back(lem); - lem = nm->mkNode(GT, lens, d_zero); + lem = nm->mkNode(GT, lens, zero); conc2.push_back(lem); - Node x = nm->mkBoundVar(nm->integerType()); + Node x = SkolemCache::mkIndexVar(t); Node xbv = nm->mkNode(BOUND_VAR_LIST, x); - Node g = - nm->mkNode(AND, nm->mkNode(GEQ, x, d_zero), nm->mkNode(LT, x, lens)); - Node sx = nm->mkNode(STRING_SUBSTR, s, x, d_one); + Node g = nm->mkNode(AND, nm->mkNode(GEQ, x, zero), nm->mkNode(LT, x, lens)); + Node sx = nm->mkNode(STRING_SUBSTR, s, x, one); Node ux = nm->mkNode(APPLY_UF, u, x); - Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(PLUS, x, d_one)); + Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(PLUS, x, one)); Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0); Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux))); - Node cb = - nm->mkNode(AND, nm->mkNode(GEQ, c, d_zero), nm->mkNode(LT, c, ten)); + Node cb = nm->mkNode(AND, nm->mkNode(GEQ, c, zero), nm->mkNode(LT, c, ten)); Node ux1lem = nm->mkNode(GEQ, stoit, ux1); @@ -329,9 +325,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { lem = nm->mkNode(FORALL, xbv, lem); conc2.push_back(lem); - Node sneg = nm->mkNode(LT, stoit, d_zero); + Node sneg = nm->mkNode(LT, stoit, zero); lem = nm->mkNode(ITE, sneg, nm->mkNode(AND, conc1), nm->mkNode(AND, conc2)); - new_nodes.push_back(lem); + asserts.push_back(lem); // assert: // IF stoit < 0 @@ -362,10 +358,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node z = t[2]; TypeNode tn = t[0].getType(); Node rp1 = - d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_PRE, "rfcpre"); + sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_PRE, "rfcpre"); Node rp2 = - d_sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_POST, "rfcpost"); - Node rpw = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpw"); + sc->mkSkolemCached(x, y, SkolemCache::SK_FIRST_CTN_POST, "rfcpost"); + Node rpw = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpw"); // y = "" Node emp = Word::mkEmptyWord(tn); @@ -387,10 +383,10 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { rp1, nm->mkNode(kind::STRING_SUBSTR, y, - d_zero, + zero, nm->mkNode(kind::MINUS, nm->mkNode(kind::STRING_LENGTH, y), - d_one))), + one))), y) .negate(); @@ -410,7 +406,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { cond2, nm->mkNode(kind::AND, c21, c22, c23), rpw.eqNode(x))); - new_nodes.push_back( rr ); + asserts.push_back(rr); // Thus, replace( x, y, z ) = rpw. retNode = rpw; @@ -421,16 +417,16 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node x = t[0]; Node y = t[1]; Node z = t[2]; - Node rpaw = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpaw"); + Node rpaw = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "rpaw"); - Node numOcc = d_sc->mkTypedSkolemCached( + Node numOcc = sc->mkTypedSkolemCached( nm->integerType(), x, y, SkolemCache::SK_NUM_OCCUR, "numOcc"); std::vector<TypeNode> argTypes; argTypes.push_back(nm->integerType()); Node us = nm->mkSkolem("Us", nm->mkFunctionType(argTypes, nm->stringType())); TypeNode ufType = nm->mkFunctionType(argTypes, nm->integerType()); - Node uf = d_sc->mkTypedSkolemCached( + Node uf = sc->mkTypedSkolemCached( ufType, x, y, SkolemCache::SK_OCCUR_INDEX, "Uf"); Node ufno = nm->mkNode(APPLY_UF, uf, numOcc); @@ -438,27 +434,27 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node rem = nm->mkNode(STRING_SUBSTR, x, ufno, nm->mkNode(STRING_LENGTH, x)); std::vector<Node> lem; - lem.push_back(nm->mkNode(GEQ, numOcc, d_zero)); - lem.push_back(rpaw.eqNode(nm->mkNode(APPLY_UF, us, d_zero))); + lem.push_back(nm->mkNode(GEQ, numOcc, zero)); + lem.push_back(rpaw.eqNode(nm->mkNode(APPLY_UF, us, zero))); lem.push_back(usno.eqNode(rem)); - lem.push_back(nm->mkNode(APPLY_UF, uf, d_zero).eqNode(d_zero)); - lem.push_back(nm->mkNode(STRING_STRIDOF, x, y, ufno).eqNode(d_neg_one)); + lem.push_back(nm->mkNode(APPLY_UF, uf, zero).eqNode(zero)); + lem.push_back(nm->mkNode(STRING_STRIDOF, x, y, ufno).eqNode(negOne)); - Node i = nm->mkBoundVar(nm->integerType()); + Node i = SkolemCache::mkIndexVar(t); Node bvli = nm->mkNode(BOUND_VAR_LIST, i); Node bound = - nm->mkNode(AND, nm->mkNode(GEQ, i, d_zero), nm->mkNode(LT, i, numOcc)); + nm->mkNode(AND, nm->mkNode(GEQ, i, zero), nm->mkNode(LT, i, numOcc)); Node ufi = nm->mkNode(APPLY_UF, uf, i); - Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(PLUS, i, d_one)); + Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(PLUS, i, one)); Node ii = nm->mkNode(STRING_STRIDOF, x, y, ufi); Node cc = nm->mkNode( STRING_CONCAT, nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(MINUS, ii, ufi)), z, - nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, i, d_one))); + nm->mkNode(APPLY_UF, us, nm->mkNode(PLUS, i, one))); std::vector<Node> flem; - flem.push_back(ii.eqNode(d_neg_one).negate()); + flem.push_back(ii.eqNode(negOne).negate()); flem.push_back(nm->mkNode(APPLY_UF, us, i).eqNode(cc)); flem.push_back( ufip1.eqNode(nm->mkNode(PLUS, ii, nm->mkNode(STRING_LENGTH, y)))); @@ -487,7 +483,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node emp = Word::mkEmptyWord(t.getType()); Node assert = nm->mkNode(ITE, y.eqNode(emp), rpaw.eqNode(x), nm->mkNode(AND, lem)); - new_nodes.push_back(assert); + asserts.push_back(assert); // Thus, replaceall( x, y, z ) = rpaw retNode = rpaw; @@ -495,19 +491,17 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { else if (t.getKind() == STRING_TOLOWER || t.getKind() == STRING_TOUPPER) { Node x = t[0]; - Node r = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r"); + Node r = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r"); Node lenx = nm->mkNode(STRING_LENGTH, x); Node lenr = nm->mkNode(STRING_LENGTH, r); Node eqLenA = lenx.eqNode(lenr); - Node i = nm->mkBoundVar(nm->integerType()); + Node i = SkolemCache::mkIndexVar(t); Node bvi = nm->mkNode(BOUND_VAR_LIST, i); - Node ci = - nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, x, i, d_one)); - Node ri = - nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, r, i, d_one)); + Node ci = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, x, i, one)); + Node ri = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, r, i, one)); Node lb = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 97 : 65)); Node ub = nm->mkConst(Rational(t.getKind() == STRING_TOUPPER ? 122 : 90)); @@ -521,7 +515,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { ci); Node bound = - nm->mkNode(AND, nm->mkNode(LEQ, d_zero, i), nm->mkNode(LT, i, lenr)); + nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr)); Node rangeA = nm->mkNode(FORALL, bvi, nm->mkNode(OR, bound.negate(), ri.eqNode(res))); @@ -533,7 +527,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // str.code( str.substr(r,i,1) ) = ite( 97 <= ci <= 122, ci-32, ci) // where ci = str.code( str.substr(x,i,1) ) Node assert = nm->mkNode(AND, eqLenA, rangeA); - new_nodes.push_back(assert); + asserts.push_back(assert); // Thus, toLower( x ) = r retNode = r; @@ -541,22 +535,22 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { else if (t.getKind() == STRING_REV) { Node x = t[0]; - Node r = d_sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r"); + Node r = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "r"); Node lenx = nm->mkNode(STRING_LENGTH, x); Node lenr = nm->mkNode(STRING_LENGTH, r); Node eqLenA = lenx.eqNode(lenr); - Node i = nm->mkBoundVar(nm->integerType()); + Node i = SkolemCache::mkIndexVar(t); Node bvi = nm->mkNode(BOUND_VAR_LIST, i); Node revi = nm->mkNode( - MINUS, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, d_one)); - Node ssr = nm->mkNode(STRING_SUBSTR, r, i, d_one); - Node ssx = nm->mkNode(STRING_SUBSTR, x, revi, d_one); + MINUS, nm->mkNode(STRING_LENGTH, x), nm->mkNode(PLUS, i, one)); + Node ssr = nm->mkNode(STRING_SUBSTR, r, i, one); + Node ssx = nm->mkNode(STRING_SUBSTR, x, revi, one); Node bound = - nm->mkNode(AND, nm->mkNode(LEQ, d_zero, i), nm->mkNode(LT, i, lenr)); + nm->mkNode(AND, nm->mkNode(LEQ, zero, i), nm->mkNode(LT, i, lenr)); Node rangeA = nm->mkNode( FORALL, bvi, nm->mkNode(OR, bound.negate(), ssr.eqNode(ssx))); // assert: @@ -564,7 +558,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // forall i. 0 <= i < len(r) => // substr(r,i,1) = substr(x,len(x)-(i+1),1) Node assert = nm->mkNode(AND, eqLenA, rangeA); - new_nodes.push_back(assert); + asserts.push_back(assert); // Thus, (str.rev x) = r retNode = r; @@ -576,31 +570,38 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { //negative contains reduces to existential Node lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x); Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s); - Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); + Node b1 = SkolemCache::mkIndexVar(t); Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1); - Node body = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::LEQ, d_zero, b1 ), - NodeManager::currentNM()->mkNode( kind::LEQ, b1, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ) ), - NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, b1, lens), s ) - ); + Node body = NodeManager::currentNM()->mkNode( + kind::AND, + NodeManager::currentNM()->mkNode(kind::LEQ, zero, b1), + NodeManager::currentNM()->mkNode( + kind::LEQ, + b1, + NodeManager::currentNM()->mkNode(kind::MINUS, lenx, lens)), + NodeManager::currentNM()->mkNode( + kind::EQUAL, + NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, b1, lens), + s)); retNode = NodeManager::currentNM()->mkNode( kind::EXISTS, b1v, body ); } else if (t.getKind() == kind::STRING_LEQ) { - Node ltp = nm->mkSkolem("ltp", nm->booleanType()); + Node ltp = sc->mkTypedSkolemCached( + nm->booleanType(), t, SkolemCache::SK_PURIFY, "ltp"); Node k = nm->mkSkolem("k", nm->integerType()); std::vector<Node> conj; - conj.push_back(nm->mkNode(GEQ, k, d_zero)); + conj.push_back(nm->mkNode(GEQ, k, zero)); Node substr[2]; Node code[2]; for (unsigned r = 0; r < 2; r++) { Node ta = t[r]; Node tb = t[1 - r]; - substr[r] = nm->mkNode(STRING_SUBSTR, ta, d_zero, k); + substr[r] = nm->mkNode(STRING_SUBSTR, ta, zero, k); code[r] = - nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, ta, k, d_one)); + nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, ta, k, one)); conj.push_back(nm->mkNode(LEQ, k, nm->mkNode(STRING_LENGTH, ta))); } conj.push_back(substr[0].eqNode(substr[1])); @@ -632,18 +633,29 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // ELSE: str.code(substr( x, k, 1 )) > str.code(substr( y, k, 1 )) Node assert = nm->mkNode(ITE, t[0].eqNode(t[1]), ltp, nm->mkNode(AND, conj)); - new_nodes.push_back(assert); + asserts.push_back(assert); // Thus, str.<=( x, y ) = ltp retNode = ltp; } + return retNode; +} +Node StringsPreprocess::simplify(Node t, std::vector<Node>& asserts) +{ + size_t prev_asserts = asserts.size(); + // call the static reduce routine + Node retNode = reduce(t, asserts, d_sc); if( t!=retNode ){ Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << " -> " << retNode << std::endl; - if(!new_nodes.empty()) { - Trace("strings-preprocess") << " ... new nodes (" << (new_nodes.size()-prev_new_nodes) << "):" << std::endl; - for(unsigned int i=prev_new_nodes; i<new_nodes.size(); ++i) { - Trace("strings-preprocess") << " " << new_nodes[i] << std::endl; + if (!asserts.empty()) + { + Trace("strings-preprocess") + << " ... new nodes (" << (asserts.size() - prev_asserts) + << "):" << std::endl; + for (size_t i = prev_asserts; i < asserts.size(); ++i) + { + Trace("strings-preprocess") << " " << asserts[i] << std::endl; } } d_statistics.d_reductions << t.getKind(); @@ -656,14 +668,17 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { return retNode; } -Node StringsPreprocess::simplifyRec( Node t, std::vector< Node > & new_nodes, std::map< Node, Node >& visited ){ +Node StringsPreprocess::simplifyRec(Node t, + std::vector<Node>& asserts, + std::map<Node, Node>& visited) +{ std::map< Node, Node >::iterator it = visited.find(t); if( it!=visited.end() ){ return it->second; }else{ Node retNode = t; if( t.getNumChildren()==0 ){ - retNode = simplify( t, new_nodes ); + retNode = simplify(t, asserts); }else if( t.getKind()!=kind::FORALL ){ bool changed = false; std::vector< Node > cc; @@ -671,7 +686,7 @@ Node StringsPreprocess::simplifyRec( Node t, std::vector< Node > & new_nodes, st cc.push_back( t.getOperator() ); } for(unsigned i=0; i<t.getNumChildren(); i++) { - Node s = simplifyRec( t[i], new_nodes, visited ); + Node s = simplifyRec(t[i], asserts, visited); cc.push_back( s ); if( s!=t[i] ) { changed = true; @@ -681,24 +696,27 @@ Node StringsPreprocess::simplifyRec( Node t, std::vector< Node > & new_nodes, st if( changed ){ tmp = NodeManager::currentNM()->mkNode( t.getKind(), cc ); } - retNode = simplify( tmp, new_nodes ); + retNode = simplify(tmp, asserts); } visited[t] = retNode; return retNode; } } -Node StringsPreprocess::processAssertion( Node n, std::vector< Node > &new_nodes ) { +Node StringsPreprocess::processAssertion(Node n, std::vector<Node>& asserts) +{ std::map< Node, Node > visited; - std::vector< Node > new_nodes_curr; - Node ret = simplifyRec( n, new_nodes_curr, visited ); - while( !new_nodes_curr.empty() ){ - Node curr = new_nodes_curr.back(); - new_nodes_curr.pop_back(); - std::vector< Node > new_nodes_tmp; - curr = simplifyRec( curr, new_nodes_tmp, visited ); - new_nodes_curr.insert( new_nodes_curr.end(), new_nodes_tmp.begin(), new_nodes_tmp.end() ); - new_nodes.push_back( curr ); + std::vector<Node> asserts_curr; + Node ret = simplifyRec(n, asserts_curr, visited); + while (!asserts_curr.empty()) + { + Node curr = asserts_curr.back(); + asserts_curr.pop_back(); + std::vector<Node> asserts_tmp; + curr = simplifyRec(curr, asserts_tmp, visited); + asserts_curr.insert( + asserts_curr.end(), asserts_tmp.begin(), asserts_tmp.end()); + asserts.push_back(curr); } return ret; } @@ -708,18 +726,22 @@ void StringsPreprocess::processAssertions( std::vector< Node > &vec_node ){ for( unsigned i=0; i<vec_node.size(); i++ ){ Trace("strings-preprocess-debug") << "Preprocessing assertion " << vec_node[i] << std::endl; //preprocess until fixed point - std::vector< Node > new_nodes; - std::vector< Node > new_nodes_curr; - new_nodes_curr.push_back( vec_node[i] ); - while( !new_nodes_curr.empty() ){ - Node curr = new_nodes_curr.back(); - new_nodes_curr.pop_back(); - std::vector< Node > new_nodes_tmp; - curr = simplifyRec( curr, new_nodes_tmp, visited ); - new_nodes_curr.insert( new_nodes_curr.end(), new_nodes_tmp.begin(), new_nodes_tmp.end() ); - new_nodes.push_back( curr ); + std::vector<Node> asserts; + std::vector<Node> asserts_curr; + asserts_curr.push_back(vec_node[i]); + while (!asserts_curr.empty()) + { + Node curr = asserts_curr.back(); + asserts_curr.pop_back(); + std::vector<Node> asserts_tmp; + curr = simplifyRec(curr, asserts_tmp, visited); + asserts_curr.insert( + asserts_curr.end(), asserts_tmp.begin(), asserts_tmp.end()); + asserts.push_back(curr); } - Node res = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes ); + Node res = asserts.size() == 1 + ? asserts[0] + : NodeManager::currentNM()->mkNode(kind::AND, asserts); if( res!=vec_node[i] ){ res = Rewriter::rewrite( res ); PROOF( ProofManager::currentPM()->addDependence( res, vec_node[i] ); ); diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index fb6404aa6..1392b4ea1 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -44,21 +44,41 @@ class StringsPreprocess { context::UserContext* u, SequencesStatistics& stats); ~StringsPreprocess(); + /** The reduce routine + * + * This is the main routine for constructing the reduction lemma for + * an extended function t. It returns the simplified form of t, as well + * as assertions for t, interpeted conjunctively. The reduction lemma + * for t is: + * asserts[0] ^ ... ^ asserts[n] ^ t = t' + * where t' is the term returned by this method. + * The argument sc defines the methods for generating new Skolem variables. + * The return value is t itself if it is not reduced by this class. + * + * The reduction lemma for t is a way of specifying the complete semantics + * of t. In other words, any model satisfying the reduction lemma of t + * correctly interprets t. + * + * @param t The node to reduce, + * @param asserts The vector for storing the assertions that correspond to + * the reduction of t, + * @param sc The skolem cache for generating new variables, + * @return The reduced form of t. + */ + static Node reduce(Node t, std::vector<Node>& asserts, SkolemCache* sc); /** - * Returns a node t' such that - * (exists k) new_nodes => t = t' - * is valid, where k are the free skolems introduced when constructing - * new_nodes. + * Calls the above method for the skolem cache owned by this class, and + * records statistics. */ - Node simplify(Node t, std::vector<Node>& new_nodes); + Node simplify(Node t, std::vector<Node>& asserts); /** * Applies simplifyRec on t until a fixed point is reached, and returns * the resulting term t', which is such that - * (exists k) new_nodes => t = t' + * (exists k) asserts => t = t' * is valid, where k are the free skolems introduced when constructing - * new_nodes. + * asserts. */ - Node processAssertion(Node t, std::vector<Node>& new_nodes); + Node processAssertion(Node t, std::vector<Node>& asserts); /** * Replaces all formulas t in vec_node with an equivalent formula t' that * contains no free instances of extended functions (that is, extended @@ -68,21 +88,17 @@ class StringsPreprocess { void processAssertions(std::vector<Node>& vec_node); private: - /** commonly used constants */ - Node d_zero; - Node d_one; - Node d_neg_one; /** pointer to the skolem cache used by this class */ SkolemCache* d_sc; /** Reference to the statistics for the theory of strings/sequences. */ SequencesStatistics& d_statistics; /** * Applies simplify to all top-level extended function subterms of t. New - * assertions created in this reduction are added to new_nodes. The argument + * assertions created in this reduction are added to asserts. The argument * visited stores a cache of previous results. */ Node simplifyRec(Node t, - std::vector<Node>& new_nodes, + std::vector<Node>& asserts, std::map<Node, Node>& visited); }; diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 93a32f26e..3229e6631 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -20,6 +20,9 @@ #ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H #define CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H +#include "expr/expr_sequence.h" +#include "expr/sequence.h" + namespace CVC4 { namespace theory { namespace strings { @@ -318,6 +321,53 @@ public: } }; +class ConstSequenceTypeRule +{ + public: + static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) + { + Assert(n.getKind() == kind::CONST_SEQUENCE); + return n.getConst<ExprSequence>().getSequence().getType(); + } +}; + +class SeqUnitTypeRule +{ + public: + static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) + { + return nodeManager->mkSequenceType(n[0].getType(check)); + } +}; + +/** Properties of the sequence type */ +struct SequenceProperties +{ + static Cardinality computeCardinality(TypeNode type) + { + Assert(type.getKind() == kind::SEQUENCE_TYPE); + return Cardinality::INTEGERS; + } + /** A sequence is well-founded if its element type is */ + static bool isWellFounded(TypeNode type) + { + return type[0].isWellFounded(); + } + /** Make ground term for sequence type (return the empty sequence) */ + static Node mkGroundTerm(TypeNode type) + { + Assert(type.isSequence()); + // empty sequence + std::vector<Expr> seq; + return NodeManager::currentNM()->mkConst( + ExprSequence(SequenceType(type.toType()), seq)); + } +}; /* struct SequenceProperties */ + }/* CVC4::theory::strings namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp index d24206860..c25363e65 100644 --- a/src/theory/strings/type_enumerator.cpp +++ b/src/theory/strings/type_enumerator.cpp @@ -158,6 +158,67 @@ void StringEnumLen::mkCurr() d_curr = makeStandardModelConstant(d_witer->getData(), d_cardinality); } +SeqEnumLen::SeqEnumLen(TypeNode tn, + TypeEnumeratorProperties* tep, + uint32_t startLength) + : SEnumLen(tn, startLength) +{ + d_elementEnumerator.reset( + new TypeEnumerator(d_type.getSequenceElementType(), tep)); + mkCurr(); +} + +SeqEnumLen::SeqEnumLen(TypeNode tn, + TypeEnumeratorProperties* tep, + uint32_t startLength, + uint32_t endLength) + : SEnumLen(tn, startLength, endLength) +{ + d_elementEnumerator.reset( + new TypeEnumerator(d_type.getSequenceElementType(), tep)); + mkCurr(); +} + +SeqEnumLen::SeqEnumLen(const SeqEnumLen& wenum) + : SEnumLen(wenum), + d_elementEnumerator(new TypeEnumerator(*wenum.d_elementEnumerator)), + d_elementDomain(wenum.d_elementDomain) +{ +} + +bool SeqEnumLen::increment() +{ + if (!d_elementEnumerator->isFinished()) + { + // yet to establish domain + Assert(d_elementEnumerator != nullptr); + d_elementDomain.push_back((**d_elementEnumerator).toExpr()); + ++(*d_elementEnumerator); + } + // the current cardinality is the domain size of the element + if (!d_witer->increment(d_elementDomain.size())) + { + Assert(d_elementEnumerator->isFinished()); + d_curr = Node::null(); + return false; + } + mkCurr(); + return true; +} + +void SeqEnumLen::mkCurr() +{ + std::vector<Expr> seq; + const std::vector<unsigned>& data = d_witer->getData(); + for (unsigned i : data) + { + seq.push_back(d_elementDomain[i]); + } + // make sequence from seq + d_curr = + NodeManager::currentNM()->mkConst(ExprSequence(d_type.toType(), seq)); +} + StringEnumerator::StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep) : TypeEnumeratorBase<StringEnumerator>(type), d_wenum(0, utils::getAlphabetCardinality()) @@ -182,6 +243,28 @@ StringEnumerator& StringEnumerator::operator++() bool StringEnumerator::isFinished() { return d_wenum.isFinished(); } +SequenceEnumerator::SequenceEnumerator(TypeNode type, + TypeEnumeratorProperties* tep) + : TypeEnumeratorBase<SequenceEnumerator>(type), d_wenum(type, tep, 0) +{ +} + +SequenceEnumerator::SequenceEnumerator(const SequenceEnumerator& enumerator) + : TypeEnumeratorBase<SequenceEnumerator>(enumerator.getType()), + d_wenum(enumerator.d_wenum) +{ +} + +Node SequenceEnumerator::operator*() { return d_wenum.getCurrent(); } + +SequenceEnumerator& SequenceEnumerator::operator++() +{ + d_wenum.increment(); + return *this; +} + +bool SequenceEnumerator::isFinished() { return d_wenum.isFinished(); } + } // namespace strings } // namespace theory } // namespace CVC4 diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h index b379ce5c3..c82892624 100644 --- a/src/theory/strings/type_enumerator.h +++ b/src/theory/strings/type_enumerator.h @@ -136,6 +136,34 @@ class StringEnumLen : public SEnumLen void mkCurr(); }; +/** + * Enumerates sequence values for a given length. + */ +class SeqEnumLen : public SEnumLen +{ + public: + /** For sequences */ + SeqEnumLen(TypeNode tn, TypeEnumeratorProperties* tep, uint32_t startLength); + SeqEnumLen(TypeNode tn, + TypeEnumeratorProperties* tep, + uint32_t startLength, + uint32_t endLength); + /** copy constructor */ + SeqEnumLen(const SeqEnumLen& wenum); + /** destructor */ + ~SeqEnumLen() {} + /** increment */ + bool increment() override; + + private: + /** an enumerator for the elements' type */ + std::unique_ptr<TypeEnumerator> d_elementEnumerator; + /** The domain */ + std::vector<Expr> d_elementDomain; + /** Make the current term from d_data */ + void mkCurr(); +}; + class StringEnumerator : public TypeEnumeratorBase<StringEnumerator> { public: @@ -154,6 +182,21 @@ class StringEnumerator : public TypeEnumeratorBase<StringEnumerator> StringEnumLen d_wenum; }; /* class StringEnumerator */ +class SequenceEnumerator : public TypeEnumeratorBase<SequenceEnumerator> +{ + public: + SequenceEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr); + SequenceEnumerator(const SequenceEnumerator& enumerator); + ~SequenceEnumerator() {} + Node operator*() override; + SequenceEnumerator& operator++() override; + bool isFinished() override; + + private: + /** underlying sequence enumerator */ + SeqEnumLen d_wenum; +}; /* class SequenceEnumerator */ + }/* CVC4::theory::strings namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp index e9ab2652e..3f6a9de32 100644 --- a/src/theory/strings/word.cpp +++ b/src/theory/strings/word.cpp @@ -14,6 +14,7 @@ #include "theory/strings/word.h" +#include "expr/sequence.h" #include "util/string.h" using namespace CVC4::kind; @@ -28,23 +29,28 @@ Node Word::mkEmptyWord(TypeNode tn) { return mkEmptyWord(CONST_STRING); } + else if (tn.isSequence()) + { + std::vector<Expr> seq; + return NodeManager::currentNM()->mkConst( + ExprSequence(tn.getSequenceElementType().toType(), seq)); + } Unimplemented(); return Node::null(); } Node Word::mkEmptyWord(Kind k) { - NodeManager* nm = NodeManager::currentNM(); if (k == CONST_STRING) { std::vector<unsigned> vec; - return nm->mkConst(String(vec)); + return NodeManager::currentNM()->mkConst(String(vec)); } Unimplemented(); return Node::null(); } -Node Word::mkWord(const std::vector<Node>& xs) +Node Word::mkWordFlatten(const std::vector<Node>& xs) { Assert(!xs.empty()); NodeManager* nm = NodeManager::currentNM(); @@ -61,6 +67,22 @@ Node Word::mkWord(const std::vector<Node>& xs) } return nm->mkConst(String(vec)); } + else if (k == CONST_SEQUENCE) + { + std::vector<Expr> seq; + TypeNode tn = xs[0].getType(); + for (TNode x : xs) + { + Assert(x.getType() == tn); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const std::vector<Node>& vecc = sx.getVec(); + for (const Node& c : vecc) + { + seq.push_back(c.toExpr()); + } + } + return NodeManager::currentNM()->mkConst(ExprSequence(tn.toType(), seq)); + } Unimplemented(); return Node::null(); } @@ -72,6 +94,10 @@ size_t Word::getLength(TNode x) { return x.getConst<String>().size(); } + else if (k == CONST_SEQUENCE) + { + return x.getConst<ExprSequence>().getSequence().size(); + } Unimplemented(); return 0; } @@ -111,6 +137,13 @@ bool Word::strncmp(TNode x, TNode y, std::size_t n) String sy = y.getConst<String>(); return sx.strncmp(sy, n); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.strncmp(sy, n); + } Unimplemented(); return false; } @@ -125,6 +158,13 @@ bool Word::rstrncmp(TNode x, TNode y, std::size_t n) String sy = y.getConst<String>(); return sx.rstrncmp(sy, n); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.rstrncmp(sy, n); + } Unimplemented(); return false; } @@ -139,6 +179,13 @@ std::size_t Word::find(TNode x, TNode y, std::size_t start) String sy = y.getConst<String>(); return sx.find(sy, start); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.find(sy, start); + } Unimplemented(); return 0; } @@ -153,6 +200,13 @@ std::size_t Word::rfind(TNode x, TNode y, std::size_t start) String sy = y.getConst<String>(); return sx.rfind(sy, start); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.rfind(sy, start); + } Unimplemented(); return 0; } @@ -167,6 +221,13 @@ bool Word::hasPrefix(TNode x, TNode y) String sy = y.getConst<String>(); return sx.hasPrefix(sy); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.hasPrefix(sy); + } Unimplemented(); return false; } @@ -181,6 +242,13 @@ bool Word::hasSuffix(TNode x, TNode y) String sy = y.getConst<String>(); return sx.hasSuffix(sy); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.hasSuffix(sy); + } Unimplemented(); return false; } @@ -198,6 +266,16 @@ Node Word::replace(TNode x, TNode y, TNode t) String st = t.getConst<String>(); return nm->mkConst(String(sx.replace(sy, st))); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + Assert(t.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + const Sequence& st = t.getConst<ExprSequence>().getSequence(); + Sequence res = sx.replace(sy, st); + return nm->mkConst(res.toExprSequence()); + } Unimplemented(); return Node::null(); } @@ -210,6 +288,12 @@ Node Word::substr(TNode x, std::size_t i) String sx = x.getConst<String>(); return nm->mkConst(String(sx.substr(i))); } + else if (k == CONST_SEQUENCE) + { + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + Sequence res = sx.substr(i); + return nm->mkConst(res.toExprSequence()); + } Unimplemented(); return Node::null(); } @@ -222,6 +306,12 @@ Node Word::substr(TNode x, std::size_t i, std::size_t j) String sx = x.getConst<String>(); return nm->mkConst(String(sx.substr(i, j))); } + else if (k == CONST_SEQUENCE) + { + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + Sequence res = sx.substr(i, j); + return nm->mkConst(res.toExprSequence()); + } Unimplemented(); return Node::null(); } @@ -237,6 +327,12 @@ Node Word::suffix(TNode x, std::size_t i) String sx = x.getConst<String>(); return nm->mkConst(String(sx.suffix(i))); } + else if (k == CONST_SEQUENCE) + { + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + Sequence res = sx.suffix(i); + return nm->mkConst(res.toExprSequence()); + } Unimplemented(); return Node::null(); } @@ -251,6 +347,13 @@ bool Word::noOverlapWith(TNode x, TNode y) String sy = y.getConst<String>(); return sx.noOverlapWith(sy); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.noOverlapWith(sy); + } Unimplemented(); return false; } @@ -265,6 +368,13 @@ std::size_t Word::overlap(TNode x, TNode y) String sy = y.getConst<String>(); return sx.overlap(sy); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.overlap(sy); + } Unimplemented(); return 0; } @@ -279,10 +389,32 @@ std::size_t Word::roverlap(TNode x, TNode y) String sy = y.getConst<String>(); return sx.roverlap(sy); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + return sx.roverlap(sy); + } Unimplemented(); return 0; } +bool Word::isRepeated(TNode x) +{ + Kind k = x.getKind(); + if (k == CONST_STRING) + { + return x.getConst<String>().isRepeated(); + } + else if (k == CONST_SEQUENCE) + { + return x.getConst<ExprSequence>().getSequence().isRepeated(); + } + Unimplemented(); + return false; +} + Node Word::splitConstant(TNode x, TNode y, size_t& index, bool isRev) { Assert(x.isConst() && y.isConst()); diff --git a/src/theory/strings/word.h b/src/theory/strings/word.h index b84ea6874..ad1d9bc74 100644 --- a/src/theory/strings/word.h +++ b/src/theory/strings/word.h @@ -37,7 +37,7 @@ class Word static Node mkEmptyWord(Kind k); /** make word from constants in (non-empty) vector vec */ - static Node mkWord(const std::vector<Node>& xs); + static Node mkWordFlatten(const std::vector<Node>& xs); /** Return the length of word x */ static size_t getLength(TNode x); @@ -139,6 +139,8 @@ class Word * Notice that x.overlap(y) = y.roverlap(x) */ static std::size_t roverlap(TNode x, TNode y); + /** Return true if word x is a repetition of the same character */ + static bool isRepeated(TNode x); /** Split constant * * This returns the suffix remainder (resp. prefix remainder when isRev is diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 2c27c6054..71c144daa 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1931,7 +1931,14 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, // Lemma analysis isn't online yet; this lemma may only live for this // user level. - return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel()); + Node retLemma = additionalLemmas[0]; + if (additionalLemmas.size() > 1) + { + // the returned lemma is the conjunction of all additional lemmas. + retLemma = + NodeManager::currentNM()->mkNode(kind::AND, additionalLemmas.ref()); + } + return theory::LemmaStatus(retLemma, d_userContext->getLevel()); } void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 9c631ca60..233047321 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -890,8 +890,6 @@ public: theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } - RemoveTermFormulas* getTermFormulaRemover() { return &d_tform_remover; } - SortInference* getSortInference() { return &d_sortInfer; } /** Prints the assertions to the debug stream */ diff --git a/src/theory/uf/proof_checker.cpp b/src/theory/uf/proof_checker.cpp new file mode 100644 index 000000000..28ae34b7b --- /dev/null +++ b/src/theory/uf/proof_checker.cpp @@ -0,0 +1,172 @@ +/********************* */ +/*! \file proof_checker.cpp + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of equality proof checker + **/ + +#include "theory/uf/proof_checker.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace uf { + +void UfProofRuleChecker::registerTo(ProofChecker* pc) +{ + // add checkers + pc->registerChecker(PfRule::REFL, this); + pc->registerChecker(PfRule::SYMM, this); + pc->registerChecker(PfRule::TRANS, this); + pc->registerChecker(PfRule::CONG, this); + pc->registerChecker(PfRule::TRUE_INTRO, this); + pc->registerChecker(PfRule::TRUE_ELIM, this); + pc->registerChecker(PfRule::FALSE_INTRO, this); + pc->registerChecker(PfRule::FALSE_ELIM, this); +} + +Node UfProofRuleChecker::checkInternal(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args) +{ + // compute what was proven + if (id == PfRule::REFL) + { + Assert(children.empty()); + Assert(args.size() == 1); + return args[0].eqNode(args[0]); + } + else if (id == PfRule::SYMM) + { + Assert(children.size() == 1); + Assert(args.empty()); + bool polarity = children[0].getKind() != NOT; + Node eqp = polarity ? children[0] : children[0][0]; + if (eqp.getKind() != EQUAL) + { + // not a (dis)equality + return Node::null(); + } + Node conc = eqp[1].eqNode(eqp[0]); + return polarity ? conc : conc.notNode(); + } + else if (id == PfRule::TRANS) + { + Assert(children.size() > 0); + Assert(args.empty()); + Node first; + Node curr; + for (size_t i = 0, nchild = children.size(); i < nchild; i++) + { + Node eqp = children[i]; + if (eqp.getKind() != EQUAL) + { + return Node::null(); + } + if (first.isNull()) + { + first = eqp[0]; + } + else if (eqp[0] != curr) + { + return Node::null(); + } + curr = eqp[1]; + } + return first.eqNode(curr); + } + else if (id == PfRule::CONG) + { + Assert(children.size() > 0); + Assert(args.size() == 1); + // We do congruence over builtin kinds using operatorToKind + std::vector<Node> lchildren; + std::vector<Node> rchildren; + // get the expected kind for args[0] + Kind k = NodeManager::getKindForFunction(args[0]); + if (k == kind::UNDEFINED_KIND) + { + k = NodeManager::operatorToKind(args[0]); + } + if (k == kind::UNDEFINED_KIND) + { + return Node::null(); + } + Trace("uf-pfcheck") << "congruence for " << args[0] << " uses kind " << k + << ", metakind=" << kind::metaKindOf(k) << std::endl; + if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED) + { + // parameterized kinds require the operator + lchildren.push_back(args[0]); + rchildren.push_back(args[0]); + } + for (size_t i = 0, nchild = children.size(); i < nchild; i++) + { + Node eqp = children[i]; + if (eqp.getKind() != EQUAL) + { + return Node::null(); + } + lchildren.push_back(eqp[0]); + rchildren.push_back(eqp[1]); + } + NodeManager* nm = NodeManager::currentNM(); + Node l = nm->mkNode(k, lchildren); + Node r = nm->mkNode(k, rchildren); + return l.eqNode(r); + } + else if (id == PfRule::TRUE_INTRO) + { + Assert(children.size() == 1); + Assert(args.empty()); + Node trueNode = NodeManager::currentNM()->mkConst(true); + return children[0].eqNode(trueNode); + } + else if (id == PfRule::TRUE_ELIM) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != EQUAL || !children[0][1].isConst() + || !children[0][1].getConst<bool>()) + { + return Node::null(); + } + return children[0][0]; + } + else if (id == PfRule::FALSE_INTRO) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT) + { + return Node::null(); + } + Node falseNode = NodeManager::currentNM()->mkConst(false); + return children[0][0].eqNode(falseNode); + } + else if (id == PfRule::FALSE_ELIM) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != EQUAL || !children[0][1].isConst() + || children[0][1].getConst<bool>()) + { + return Node::null(); + } + return children[0][0].notNode(); + } + // no rule + return Node::null(); +} + +} // namespace uf +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/uf/proof_checker.h b/src/theory/uf/proof_checker.h new file mode 100644 index 000000000..022574eab --- /dev/null +++ b/src/theory/uf/proof_checker.h @@ -0,0 +1,49 @@ +/********************* */ +/*! \file proof_checker.h + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Equality proof checker utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__UF__PROOF_CHECKER_H +#define CVC4__THEORY__UF__PROOF_CHECKER_H + +#include "expr/node.h" +#include "expr/proof_checker.h" +#include "expr/proof_node.h" + +namespace CVC4 { +namespace theory { +namespace uf { + +/** A checker for builtin proofs */ +class UfProofRuleChecker : public ProofRuleChecker +{ + public: + UfProofRuleChecker() {} + ~UfProofRuleChecker() {} + + /** Register all rules owned by this rule checker into pc. */ + void registerTo(ProofChecker* pc) override; + + protected: + /** Return the conclusion of the given proof step, or null if it is invalid */ + Node checkInternal(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args) override; +}; + +} // namespace uf +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__UF__PROOF_CHECKER_H */ |