diff options
20 files changed, 92 insertions, 212 deletions
diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp index 6b0063ce0..04ac14c11 100644 --- a/src/theory/datatypes/sygus_simple_sym.cpp +++ b/src/theory/datatypes/sygus_simple_sym.cpp @@ -14,6 +14,7 @@ #include "theory/datatypes/sygus_simple_sym.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" using namespace std; @@ -24,7 +25,7 @@ namespace theory { namespace datatypes { SygusSimpleSymBreak::SygusSimpleSymBreak(QuantifiersEngine* qe) - : d_tds(qe->getTermDatabaseSygus()), d_tutil(qe->getTermUtil()) + : d_tds(qe->getTermDatabaseSygus()) { } @@ -430,7 +431,7 @@ bool SygusSimpleSymBreak::considerConst( { Kind ok; int offset; - if (d_tutil->hasOffsetArg(pk, arg, offset, ok)) + if (quantifiers::TermUtil::hasOffsetArg(pk, arg, offset, ok)) { Trace("sygus-sb-simple-debug") << pk << " has offset arg " << ok << " " << offset << std::endl; @@ -443,7 +444,8 @@ bool SygusSimpleSymBreak::considerConst( if (d_tds->isTypeMatch(pdt[ok_arg], pdt[arg])) { int status; - Node co = d_tutil->getTypeValueOffset(c.getType(), c, offset, status); + Node co = quantifiers::TermUtil::mkTypeValueOffset( + c.getType(), c, offset, status); Trace("sygus-sb-simple-debug") << c << " with offset " << offset << " is " << co << ", status=" << status << std::endl; @@ -476,7 +478,7 @@ bool SygusSimpleSymBreak::considerConst( bool ret = true; Trace("sygus-sb-debug") << "Consider sygus const " << c << ", parent = " << pk << ", arg = " << arg << "?" << std::endl; - if (d_tutil->isIdempotentArg(c, pk, arg)) + if (quantifiers::TermUtil::isIdempotentArg(c, pk, arg)) { if (pdt[pc].getNumArgs() == 2) { @@ -493,7 +495,7 @@ bool SygusSimpleSymBreak::considerConst( } else { - Node sc = d_tutil->isSingularArg(c, pk, arg); + Node sc = quantifiers::TermUtil::isSingularArg(c, pk, arg); if (!sc.isNull()) { if (pti.hasConst(sc)) @@ -509,9 +511,9 @@ bool SygusSimpleSymBreak::considerConst( { ReqTrie rt; Assert(rt.empty()); - Node max_c = d_tutil->getTypeMaxValue(c.getType()); - Node zero_c = d_tutil->getTypeValue(c.getType(), 0); - Node one_c = d_tutil->getTypeValue(c.getType(), 1); + Node max_c = quantifiers::TermUtil::mkTypeMaxValue(c.getType()); + Node zero_c = quantifiers::TermUtil::mkTypeValue(c.getType(), 0); + Node one_c = quantifiers::TermUtil::mkTypeValue(c.getType(), 1); if (pk == XOR || pk == BITVECTOR_XOR) { if (c == max_c) diff --git a/src/theory/datatypes/sygus_simple_sym.h b/src/theory/datatypes/sygus_simple_sym.h index a16e7a513..c2940512a 100644 --- a/src/theory/datatypes/sygus_simple_sym.h +++ b/src/theory/datatypes/sygus_simple_sym.h @@ -20,7 +20,6 @@ #include <map> #include "expr/dtype.h" #include "theory/quantifiers/sygus/term_database_sygus.h" -#include "theory/quantifiers/term_util.h" namespace CVC4 { namespace theory { @@ -89,8 +88,6 @@ class SygusSimpleSymBreak private: /** Pointer to the sygus term database */ quantifiers::TermDbSygus* d_tds; - /** Pointer to the quantifiers term utility */ - quantifiers::TermUtil* d_tutil; /** return the index of the first argument position of c that has type tn */ int getFirstArgOccurrence(const DTypeConstructor& c, TypeNode tn); /** diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index d620da7b5..f107c56e5 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -870,10 +870,7 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci, { // redo, split integer/non-integer parts bool useCoeff = false; - Integer coeff = ci->getQuantifiersEngine() - ->getTermUtil() - ->d_one.getConst<Rational>() - .getNumerator(); + Integer coeff(1); for (std::map<Node, Node>::iterator it = msum.begin(); it != msum.end(); ++it) { diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index b2fff012e..8b60152a8 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1246,6 +1246,7 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >& bool pol = lit.getKind()!=NOT; //arithmetic inequalities and disequalities if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){ + NodeManager* nm = NodeManager::currentNM(); Assert(atom.getKind() != GEQ || atom[1].isConst()); Node atom_lhs; Node atom_rhs; @@ -1253,20 +1254,27 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >& atom_lhs = atom[0]; atom_rhs = atom[1]; }else{ - atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] ); + atom_lhs = nm->mkNode(MINUS, atom[0], atom[1]); atom_lhs = Rewriter::rewrite( atom_lhs ); - atom_rhs = getQuantifiersEngine()->getTermUtil()->d_zero; + atom_rhs = nm->mkConst(Rational(0)); } //must be an eligible term if( isEligible( atom_lhs ) ){ //apply substitution to LHS of atom TermProperties atom_lhs_prop; - atom_lhs = applySubstitution( NodeManager::currentNM()->realType(), atom_lhs, vars, subs, prop, non_basic, atom_lhs_prop ); + atom_lhs = applySubstitution(nm->realType(), + atom_lhs, + vars, + subs, + prop, + non_basic, + atom_lhs_prop); if( !atom_lhs.isNull() ){ if( !atom_lhs_prop.d_coeff.isNull() ){ - atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_prop.d_coeff, atom_rhs ) ); + atom_rhs = nm->mkNode(MULT, atom_lhs_prop.d_coeff, atom_rhs); + atom_rhs = Rewriter::rewrite(atom_rhs); } - lret = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); + lret = nm->mkNode(atom.getKind(), atom_lhs, atom_rhs); if( !pol ){ lret = lret.negate(); } diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 3ade304e8..e8b9f5dea 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -783,7 +783,8 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node Node tu = u; getBounds( q, v, rsi, tl, tu ); Assert(!tl.isNull() && !tu.isNull()); - if( ra==d_quantEngine->getTermUtil()->d_true ){ + if (ra.isConst() && ra.getConst<bool>()) + { long rr = range.getConst<Rational>().getNumerator().getLong()+1; Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; for( unsigned k=0; k<rr; k++ ){ diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp index 1d2da7e79..ab08df233 100644 --- a/src/theory/quantifiers/quant_module.cpp +++ b/src/theory/quantifiers/quant_module.cpp @@ -67,11 +67,6 @@ quantifiers::TermDb* QuantifiersModule::getTermDatabase() const return d_quantEngine->getTermDatabase(); } -quantifiers::TermUtil* QuantifiersModule::getTermUtil() const -{ - return d_quantEngine->getTermUtil(); -} - quantifiers::QuantifiersState& QuantifiersModule::getState() { return d_qstate; diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h index 4d0481484..af763265d 100644 --- a/src/theory/quantifiers/quant_module.h +++ b/src/theory/quantifiers/quant_module.h @@ -34,7 +34,6 @@ class QuantifiersEngine; namespace quantifiers { class TermDb; -class TermUtil; } // namespace quantifiers /** QuantifiersModule class @@ -160,8 +159,6 @@ class QuantifiersModule QuantifiersEngine* getQuantifiersEngine() const; /** get currently used term database */ quantifiers::TermDb* getTermDatabase() const; - /** get currently used term utility object */ - quantifiers::TermUtil* getTermUtil() const; /** get the quantifiers state */ quantifiers::QuantifiersState& getState(); /** get the quantifiers inference manager */ diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index 1748dea8e..b296a4421 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -544,7 +544,8 @@ void CegSingleInvSol::getEquivalentTerms(Kind k, } if( !eq.isNull() ){ eq = Rewriter::rewrite( eq ); - if( eq!=d_qe->getTermUtil()->d_true ){ + if (!eq.isConst() || !eq.getConst<bool>()) + { success = false; break; } @@ -788,7 +789,7 @@ void CegSingleInvSol::registerType(TypeNode tn) TypeNode btn = dt.getSygusType(); // for constant reconstruction Kind ck = getComparisonKind(btn); - Node z = d_qe->getTermUtil()->getTypeValue(btn, 0); + Node z = TermUtil::mkTypeValue(btn, 0); // iterate over constructors for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 00a72cbcb..538d80e44 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -25,7 +25,6 @@ #include "theory/quantifiers/sygus/synth_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include "theory/strings/word.h" using namespace CVC4::kind; @@ -34,9 +33,9 @@ namespace CVC4 { namespace theory { namespace quantifiers { -CegGrammarConstructor::CegGrammarConstructor(QuantifiersEngine* qe, +CegGrammarConstructor::CegGrammarConstructor(TermDbSygus* tds, SynthConjecture* p) - : d_qe(qe), d_parent(p), d_is_syntax_restricted(false) + : d_tds(tds), d_parent(p), d_is_syntax_restricted(false) { } @@ -138,7 +137,7 @@ Node CegGrammarConstructor::process(Node q, sfvl = preGrammarType.getDType().getSygusVarList(); tn = preGrammarType; // normalize type, if user-provided - SygusGrammarNorm sygus_norm(d_qe); + SygusGrammarNorm sygus_norm(d_tds); tn = sygus_norm.normalizeSygusType(tn, sfvl); }else{ sfvl = SygusUtils::getSygusArgumentListForSynthFun(sf); @@ -205,7 +204,6 @@ Node CegGrammarConstructor::process(Node q, std::vector<Node> qchildren; Node qbody_subs = q[1]; - TermDbSygus* tds = d_qe->getTermDatabaseSygus(); for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++) { Node sf = q[0][i]; @@ -253,7 +251,7 @@ Node CegGrammarConstructor::process(Node q, Trace("cegqi-debug") << " body is now : " << qbody_subs << std::endl; } } - tds->registerSygusType(tn); + d_tds->registerSygusType(tn); Assert(tn.isDatatype()); const DType& dt = tn.getDType(); Assert(dt.isSygus()); @@ -282,7 +280,6 @@ Node CegGrammarConstructor::convertToEmbedding(Node n) std::stack<TNode> visit; TNode cur; visit.push(n); - TermDbSygus* tds = d_qe->getTermDatabaseSygus(); do { cur = visit.top(); visit.pop(); @@ -347,7 +344,7 @@ Node CegGrammarConstructor::convertToEmbedding(Node n) // lambda x1...xn. (DT_SYGUS_EVAL ef x1 ... xn) // where ef is the first order variable for the // function-to-synthesize. - SygusTypeInfo& ti = tds->getTypeInfo(ef.getType()); + SygusTypeInfo& ti = d_tds->getTypeInfo(ef.getType()); const std::vector<Node>& vars = ti.getVarList(); Assert(!vars.empty()); std::vector<Node> vs; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index 6edfbebd5..67d5eb027 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -28,8 +28,6 @@ namespace CVC4 { namespace theory { -class QuantifiersEngine; - /** * Attribute for associating a function-to-synthesize with a first order * variable whose type is a sygus datatype type that encodes its grammar. @@ -53,6 +51,7 @@ typedef expr::Attribute<SygusSynthFunVarListAttributeId, Node> namespace quantifiers { class SynthConjecture; +class TermDbSygus; /** * Utility for constructing datatypes that correspond to syntactic restrictions, @@ -61,7 +60,7 @@ class SynthConjecture; class CegGrammarConstructor { public: - CegGrammarConstructor(QuantifiersEngine* qe, SynthConjecture* p); + CegGrammarConstructor(TermDbSygus* tds, SynthConjecture* p); ~CegGrammarConstructor() {} /** process * @@ -169,8 +168,8 @@ public: Node convertToEmbedding(Node n); private: - /** reference to quantifier engine */ - QuantifiersEngine * d_qe; + /** The sygus term database we are using */ + TermDbSygus* d_tds; /** parent conjecture * This contains global information about the synthesis conjecture. */ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 644d50a95..7d757ca98 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -25,7 +25,6 @@ #include "theory/quantifiers/sygus/sygus_grammar_red.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" #include <numeric> // for std::iota @@ -68,10 +67,7 @@ bool OpPosTrie::getOrMakeType(TypeNode tn, return d_children[op_pos[ind]].getOrMakeType(tn, unres_tn, op_pos, ind + 1); } -SygusGrammarNorm::SygusGrammarNorm(QuantifiersEngine* qe) - : d_qe(qe), d_tds(d_qe->getTermDatabaseSygus()) -{ -} +SygusGrammarNorm::SygusGrammarNorm(TermDbSygus* tds) : d_tds(tds) {} SygusGrammarNorm::TypeObject::TypeObject(TypeNode src_tn, TypeNode unres_tn) : d_tn(src_tn), @@ -287,7 +283,7 @@ std::unique_ptr<SygusGrammarNorm::Transf> SygusGrammarNorm::inferTransf( if (options::sygusMinGrammar() && dt.getNumConstructors() == op_pos.size()) { SygusRedundantCons src; - src.initialize(d_qe, tn); + src.initialize(d_tds, tn); std::vector<unsigned> rindices; src.getRedundant(rindices); if (!rindices.empty()) diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index 48a5dbe06..2827d2837 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -25,7 +25,6 @@ #include "expr/node.h" #include "expr/sygus_datatype.h" #include "expr/type_node.h" -#include "theory/quantifiers/term_util.h" namespace CVC4 { namespace theory { @@ -128,7 +127,7 @@ class OpPosTrie class SygusGrammarNorm { public: - SygusGrammarNorm(QuantifiersEngine* qe); + SygusGrammarNorm(TermDbSygus* tds); ~SygusGrammarNorm() {} /** creates a normalized typenode from a given one. * @@ -363,8 +362,6 @@ class SygusGrammarNorm }; /* class TransfChain */ - /** reference to quantifier engine */ - QuantifiersEngine* d_qe; /** sygus term database associated with this utility */ TermDbSygus* d_tds; /** List of variable inputs of function-to-synthesize. diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp index e6b9b3593..6e36222b6 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp @@ -19,7 +19,6 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers_engine.h" using namespace std; using namespace CVC4::kind; @@ -28,13 +27,12 @@ namespace CVC4 { namespace theory { namespace quantifiers { -void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn) +void SygusRedundantCons::initialize(TermDbSygus* tds, TypeNode tn) { - Assert(qe != nullptr); + Assert(tds != nullptr); Trace("sygus-red") << "Compute redundant cons for " << tn << std::endl; d_type = tn; Assert(tn.isDatatype()); - TermDbSygus* tds = qe->getTermDatabaseSygus(); tds->registerSygusType(tn); const DType& dt = tn.getDType(); Assert(dt.isSygus()); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h index 7fda6acbe..ace855ee1 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h @@ -24,9 +24,6 @@ namespace CVC4 { namespace theory { - -class QuantifiersEngine; - namespace quantifiers { class TermDbSygus; @@ -48,7 +45,7 @@ class SygusRedundantCons * qe : pointer to the quantifiers engine, * tn : the (sygus) type to compute redundant constructors for */ - void initialize(QuantifiersEngine* qe, TypeNode tn); + void initialize(TermDbSygus* tds, TypeNode tn); /** Get the indices of the redundant constructors of the register type */ void getRedundant(std::vector<unsigned>& indices); /** diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 59edd3070..909a9aecc 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -53,7 +53,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, d_ceg_si(new CegSingleInv(qe)), d_templInfer(new SygusTemplateInfer), d_ceg_proc(new SynthConjectureProcess(qe)), - d_ceg_gc(new CegGrammarConstructor(qe, this)), + d_ceg_gc(new CegGrammarConstructor(d_tds, this)), d_sygus_rconst(new SygusRepairConst(qe)), d_exampleInfer(new ExampleInfer(d_tds)), d_ceg_pbe(new SygusPbe(qe, this)), diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 728797d85..e800a52cf 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -939,8 +939,7 @@ bool TermDbSygus::involvesDivByZero( Node n, std::map< Node, bool >& visited ){ if( k==DIVISION || k==DIVISION_TOTAL || k==INTS_DIVISION || k==INTS_DIVISION_TOTAL || k==INTS_MODULUS || k==INTS_MODULUS_TOTAL ){ if( n[1].isConst() ){ - if (n[1] - == d_quantEngine->getTermUtil()->getTypeValue(n[1].getType(), 0)) + if (n[1] == TermUtil::mkTypeValue(n[1].getType(), 0)) { return true; } diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 97a731fb9..9cbf2cf53 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -35,18 +35,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -TermUtil::TermUtil() -{ - d_true = NodeManager::currentNM()->mkConst(true); - d_false = NodeManager::currentNM()->mkConst(false); - d_zero = NodeManager::currentNM()->mkConst(Rational(0)); - d_one = NodeManager::currentNM()->mkConst(Rational(1)); -} - -TermUtil::~TermUtil(){ - -} - size_t TermUtil::getVariableNum(Node q, Node v) { Node::iterator it = std::find(q[0].begin(), q[0].end(), v); @@ -342,19 +330,7 @@ bool TermUtil::isBoolConnectiveTerm( TNode n ) { ( n.getKind()!=ITE || n.getType().isBoolean() ); } -Node TermUtil::getTypeValue(TypeNode tn, int val) -{ - std::unordered_map<int, Node>::iterator it = d_type_value[tn].find(val); - if (it == d_type_value[tn].end()) - { - Node n = mkTypeValue(tn, val); - d_type_value[tn][val] = n; - return n; - } - return it->second; -} - -Node TermUtil::mkTypeValue(TypeNode tn, int val) +Node TermUtil::mkTypeValue(TypeNode tn, int32_t val) { Node n; if (tn.isInteger() || tn.isReal()) @@ -364,7 +340,8 @@ Node TermUtil::mkTypeValue(TypeNode tn, int val) } else if (tn.isBitVector()) { - unsigned int uv = val; + // cast to unsigned + uint32_t uv = static_cast<uint32_t>(val); BitVector bval(tn.getConst<BitVectorSize>(), uv); n = NodeManager::currentNM()->mkConst<BitVector>(bval); } @@ -385,19 +362,6 @@ Node TermUtil::mkTypeValue(TypeNode tn, int val) return n; } -Node TermUtil::getTypeMaxValue(TypeNode tn) -{ - std::unordered_map<TypeNode, Node, TypeNodeHashFunction>::iterator it = - d_type_max_value.find(tn); - if (it == d_type_max_value.end()) - { - Node n = mkTypeMaxValue(tn); - d_type_max_value[tn] = n; - return n; - } - return it->second; -} - Node TermUtil::mkTypeMaxValue(TypeNode tn) { Node n; @@ -412,39 +376,29 @@ Node TermUtil::mkTypeMaxValue(TypeNode tn) return n; } -Node TermUtil::getTypeValueOffset(TypeNode tn, - Node val, - int offset, - int& status) +Node TermUtil::mkTypeValueOffset(TypeNode tn, + Node val, + int32_t offset, + int32_t& status) { - std::unordered_map<int, Node>::iterator it = - d_type_value_offset[tn][val].find(offset); - if (it == d_type_value_offset[tn][val].end()) + Node val_o; + Node offset_val = mkTypeValue(tn, offset); + status = -1; + if (!offset_val.isNull()) { - Node val_o; - Node offset_val = getTypeValue(tn, offset); - status = -1; - if (!offset_val.isNull()) + if (tn.isInteger() || tn.isReal()) { - if (tn.isInteger() || tn.isReal()) - { - val_o = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(PLUS, val, offset_val)); - status = 0; - } - else if (tn.isBitVector()) - { - val_o = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(BITVECTOR_PLUS, val, offset_val)); - // TODO : enable? watch for overflows - } + val_o = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(PLUS, val, offset_val)); + status = 0; + } + else if (tn.isBitVector()) + { + val_o = Rewriter::rewrite( + NodeManager::currentNM()->mkNode(BITVECTOR_PLUS, val, offset_val)); } - d_type_value_offset[tn][val][offset] = val_o; - d_type_value_offset_status[tn][val][offset] = status; - return val_o; } - status = d_type_value_offset_status[tn][val][offset]; - return it->second; + return val_o; } Node TermUtil::mkTypeConst(TypeNode tn, bool pol) @@ -493,7 +447,7 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg) // Assert( ik!=DIVISION && ik!=INTS_DIVISION && ik!=INTS_MODULUS && // ik!=BITVECTOR_UDIV ); TypeNode tn = n.getType(); - if (n == getTypeValue(tn, 0)) + if (n == mkTypeValue(tn, 0)) { if (ik == PLUS || ik == OR || ik == XOR || ik == BITVECTOR_PLUS || ik == BITVECTOR_OR @@ -511,7 +465,7 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg) return arg == 1; } } - else if (n == getTypeValue(tn, 1)) + else if (n == mkTypeValue(tn, 1)) { if (ik == MULT || ik == BITVECTOR_MULT) { @@ -528,7 +482,7 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg) return arg == 1; } } - else if (n == getTypeMaxValue(tn)) + else if (n == mkTypeMaxValue(tn)) { if (ik == EQUAL || ik == BITVECTOR_AND || ik == BITVECTOR_XNOR) { @@ -541,7 +495,7 @@ bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg) Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg) { TypeNode tn = n.getType(); - if (n == getTypeValue(tn, 0)) + if (n == mkTypeValue(tn, 0)) { if (ik == AND || ik == MULT || ik == BITVECTOR_AND || ik == BITVECTOR_MULT) { @@ -565,7 +519,7 @@ Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg) } else if (arg == 1) { - return getTypeMaxValue(tn); + return mkTypeMaxValue(tn); } } else if (ik == DIVISION || ik == DIVISION_TOTAL || ik == INTS_DIVISION @@ -586,25 +540,25 @@ Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg) } else if (arg == 2) { - return getTypeValue(NodeManager::currentNM()->stringType(), 0); + return mkTypeValue(NodeManager::currentNM()->stringType(), 0); } } else if (ik == STRING_STRIDOF) { if (arg == 0 || arg == 1) { - return getTypeValue(NodeManager::currentNM()->integerType(), -1); + return mkTypeValue(NodeManager::currentNM()->integerType(), -1); } } } - else if (n == getTypeValue(tn, 1)) + else if (n == mkTypeValue(tn, 1)) { if (ik == BITVECTOR_UREM_TOTAL) { - return getTypeValue(tn, 0); + return mkTypeValue(tn, 0); } } - else if (n == getTypeMaxValue(tn)) + else if (n == mkTypeMaxValue(tn)) { if (ik == OR || ik == BITVECTOR_OR) { @@ -618,12 +572,12 @@ Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg) // negative arguments if (ik == STRING_SUBSTR || ik == STRING_CHARAT) { - return getTypeValue(NodeManager::currentNM()->stringType(), 0); + return mkTypeValue(NodeManager::currentNM()->stringType(), 0); } else if (ik == STRING_STRIDOF) { Assert(arg == 2); - return getTypeValue(NodeManager::currentNM()->integerType(), -1); + return mkTypeValue(NodeManager::currentNM()->integerType(), -1); } } } diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index e9e3c7e98..591b7f85f 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -21,7 +21,7 @@ #include <unordered_set> #include "expr/attribute.h" -#include "theory/type_enumerator.h" +#include "expr/node.h" namespace CVC4 { namespace theory { @@ -50,13 +50,6 @@ typedef expr::Attribute<QuantInstLevelAttributeId, uint64_t> QuantInstLevelAttri struct QuantIdNumAttributeId {}; typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute; -class QuantifiersEngine; - -namespace inst{ - class Trigger; - class HigherOrderTrigger; -} - namespace quantifiers { class TermDatabase; @@ -65,14 +58,8 @@ class TermDatabase; class TermUtil { public: - TermUtil(); - ~TermUtil(); - /** boolean terms */ - Node d_true; - Node d_false; - /** constants */ - Node d_zero; - Node d_one; + TermUtil() {} + ~TermUtil() {} // for inst constant public: @@ -114,33 +101,6 @@ public: Node n, std::vector<Node>& vars); -public: - -//general utilities - // TODO #1216 : promote these? - private: - /** cache for getTypeValue */ - std::unordered_map<TypeNode, - std::unordered_map<int, Node>, - TypeNodeHashFunction> - d_type_value; - /** cache for getTypeMaxValue */ - std::unordered_map<TypeNode, Node, TypeNodeHashFunction> d_type_max_value; - /** cache for getTypeValueOffset */ - std::unordered_map<TypeNode, - std::unordered_map<Node, - std::unordered_map<int, Node>, - NodeHashFunction>, - TypeNodeHashFunction> - d_type_value_offset; - /** cache for status of getTypeValueOffset*/ - std::unordered_map<TypeNode, - std::unordered_map<Node, - std::unordered_map<int, int>, - NodeHashFunction>, - TypeNodeHashFunction> - d_type_value_offset_status; - public: /** contains uninterpreted constant */ static bool containsUninterpretedConstant( Node n ); @@ -205,41 +165,35 @@ public: * <k>( ... t_{arg-1}, t_{arg+1}...) * always holds. */ - bool isIdempotentArg(Node n, Kind ik, int arg); + static bool isIdempotentArg(Node n, Kind ik, int arg); /** is singular arg * Returns true if * <k>( ... t_{arg-1}, n, t_{arg+1}...) = ret * always holds for some constant ret, which is returned by this function. */ - Node isSingularArg(Node n, Kind ik, unsigned arg); + static Node isSingularArg(Node n, Kind ik, unsigned arg); - /** get type value + /** get type value with simple value * This gets the Node that represents value val for Type tn * This is used to get simple values, e.g. -1,0,1, * in a uniform way per type. */ - Node getTypeValue(TypeNode tn, int val); - - /** get type value offset + static Node mkTypeValue(TypeNode tn, int32_t val); + /** make type value with simple offset * Returns the value of ( val + getTypeValue( tn, offset ) ), * where + is the additive operator for the type. * Stores the status (0: success, -1: failure) in status. */ - Node getTypeValueOffset(TypeNode tn, Node val, int offset, int& status); - - /** get the "max" value for type tn + static Node mkTypeValueOffset(TypeNode tn, + Node val, + int32_t offset, + int32_t& status); + /** make the "max" value for type tn * For example, * the max value for Bool is true, * the max value for BitVector is 1..1. */ - Node getTypeMaxValue(TypeNode tn); - - /** make value, static version of get value */ - static Node mkTypeValue(TypeNode tn, int val); - /** make value offset, static version of get value offset */ - static Node mkTypeValueOffset(TypeNode tn, Node val, int offset, int& status); - /** make max value, static version of get max value */ static Node mkTypeMaxValue(TypeNode tn); /** * Make const, returns pol ? mkTypeValue(tn,0) : mkTypeMaxValue(tn). diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ebec7a110..1c01eae65 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -45,7 +45,6 @@ QuantifiersEngine::QuantifiersEngine( d_tr_trie(new inst::TriggerTrie), d_model(nullptr), d_builder(nullptr), - d_term_util(new quantifiers::TermUtil), d_term_db(new quantifiers::TermDb(qstate, qim, d_qreg, this)), d_eq_query(nullptr), d_sygus_tdb(nullptr), @@ -166,10 +165,6 @@ quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const { return d_sygus_tdb.get(); } -quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const -{ - return d_term_util.get(); -} quantifiers::QuantAttributes* QuantifiersEngine::getQuantAttributes() const { return d_quant_attr.get(); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 2fbf6b70f..f8f92f2e9 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -90,8 +90,6 @@ class QuantifiersEngine { quantifiers::TermDb* getTermDatabase() const; /** get term database sygus */ quantifiers::TermDbSygus* getTermDatabaseSygus() const; - /** get term utilities */ - quantifiers::TermUtil* getTermUtil() const; /** get quantifiers attributes */ quantifiers::QuantAttributes* getQuantAttributes() const; /** get instantiate utility */ @@ -294,8 +292,6 @@ public: std::unique_ptr<quantifiers::FirstOrderModel> d_model; /** model builder */ std::unique_ptr<quantifiers::QModelBuilder> d_builder; - /** term utilities */ - std::unique_ptr<quantifiers::TermUtil> d_term_util; /** term database */ std::unique_ptr<quantifiers::TermDb> d_term_db; /** equality query class */ |