diff options
Diffstat (limited to 'src/theory/quantifiers')
20 files changed, 106 insertions, 69 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 163a49b8c..425ab0484 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -36,8 +36,8 @@ namespace quantifiers { ArithInstantiator::ArithInstantiator(Env& env, TypeNode tn, VtsTermCache* vtc) : Instantiator(env, tn), d_vtc(vtc) { - d_zero = NodeManager::currentNM()->mkConst(Rational(0)); - d_one = NodeManager::currentNM()->mkConst(Rational(1)); + d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); + d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1)); } void ArithInstantiator::reset(CegInstantiator* ci, @@ -185,7 +185,8 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, uval = nm->mkNode( PLUS, val, - nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1))); + nm->mkConst(CONST_RATIONAL, + Rational(isUpperBoundCTT(uires) ? 1 : -1))); uval = rewrite(uval); } else @@ -252,8 +253,11 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, if (d_type.isInteger()) { uires = is_upper ? CEG_TT_LOWER : CEG_TT_UPPER; - uval = nm->mkNode( - PLUS, val, nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1))); + uval = + nm->mkNode(PLUS, + val, + nm->mkConst(CONST_RATIONAL, + Rational(isUpperBoundCTT(uires) ? 1 : -1))); uval = rewrite(uval); } else @@ -274,8 +278,8 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, { if (options().quantifiers.cegqiModel) { - Node delta_coeff = - nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1)); + Node delta_coeff = nm->mkConst( + CONST_RATIONAL, Rational(isUpperBoundCTT(uires) ? 1 : -1)); if (vts_coeff_delta.isNull()) { vts_coeff_delta = delta_coeff; @@ -451,8 +455,9 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, Assert(d_mbp_coeff[rr][j].isConst()); value[t] = nm->mkNode( MULT, - nm->mkConst(Rational(1) - / d_mbp_coeff[rr][j].getConst<Rational>()), + nm->mkConst( + CONST_RATIONAL, + Rational(1) / d_mbp_coeff[rr][j].getConst<Rational>()), value[t]); value[t] = rewrite(value[t]); } @@ -606,9 +611,10 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, } else { - val = nm->mkNode(MULT, - nm->mkNode(PLUS, vals[0], vals[1]), - nm->mkConst(Rational(1) / Rational(2))); + val = + nm->mkNode(MULT, + nm->mkNode(PLUS, vals[0], vals[1]), + nm->mkConst(CONST_RATIONAL, Rational(1) / Rational(2))); val = rewrite(val); } } @@ -803,7 +809,7 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci, vts_coeff[t] = itminf->second; if (vts_coeff[t].isNull()) { - vts_coeff[t] = nm->mkConst(Rational(1)); + vts_coeff[t] = nm->mkConst(CONST_RATIONAL, Rational(1)); } // negate if coefficient on variable is positive std::map<Node, Node>::iterator itv = msum.find(pv); @@ -820,7 +826,8 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci, { vts_coeff[t] = nm->mkNode( MULT, - nm->mkConst(Rational(-1) / itv->second.getConst<Rational>()), + nm->mkConst(CONST_RATIONAL, + Rational(-1) / itv->second.getConst<Rational>()), vts_coeff[t]); vts_coeff[t] = rewrite(vts_coeff[t]); } @@ -880,7 +887,7 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci, } } // multiply everything by this coefficient - Node rcoeff = nm->mkConst(Rational(coeff)); + Node rcoeff = nm->mkConst(CONST_RATIONAL, Rational(coeff)); std::vector<Node> real_part; 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 9dc11955b..494ac8e53 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -138,7 +138,8 @@ void TermProperties::composeProperty(TermProperties& p) else { NodeManager* nm = NodeManager::currentNM(); - d_coeff = nm->mkConst(Rational(d_coeff.getConst<Rational>() + d_coeff = nm->mkConst(CONST_RATIONAL, + Rational(d_coeff.getConst<Rational>() * p.d_coeff.getConst<Rational>())); } } @@ -165,7 +166,8 @@ void SolvedForm::push_back(Node pv, Node n, TermProperties& pv_prop) Assert(new_theta.getKind() == CONST_RATIONAL); Assert(pv_prop.d_coeff.getKind() == CONST_RATIONAL); NodeManager* nm = NodeManager::currentNM(); - new_theta = nm->mkConst(Rational(new_theta.getConst<Rational>() + new_theta = nm->mkConst(CONST_RATIONAL, + Rational(new_theta.getConst<Rational>() * pv_prop.d_coeff.getConst<Rational>())); } d_theta.push_back(new_theta); @@ -1151,7 +1153,12 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node if( !prop[i].d_coeff.isNull() ){ Assert(vars[i].getType().isInteger()); Assert(prop[i].d_coeff.isConst()); - Node nn = NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/prop[i].d_coeff.getConst<Rational>() ) ); + Node nn = NodeManager::currentNM()->mkNode( + MULT, + subs[i], + NodeManager::currentNM()->mkConst( + CONST_RATIONAL, + Rational(1) / prop[i].d_coeff.getConst<Rational>())); nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn ); nn = rewrite(nn); nsubs.push_back( nn ); @@ -1199,8 +1206,9 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node Node c_coeff; if( !msum_coeff[it->first].isNull() ){ c_coeff = rewrite(NodeManager::currentNM()->mkConst( + CONST_RATIONAL, pv_prop.d_coeff.getConst<Rational>() - / msum_coeff[it->first].getConst<Rational>())); + / msum_coeff[it->first].getConst<Rational>())); }else{ c_coeff = pv_prop.d_coeff; } @@ -1264,7 +1272,7 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >& }else{ atom_lhs = nm->mkNode(MINUS, atom[0], atom[1]); atom_lhs = rewrite(atom_lhs); - atom_rhs = nm->mkConst(Rational(0)); + atom_rhs = nm->mkConst(CONST_RATIONAL, Rational(0)); } //must be an eligible term if( isEligible( atom_lhs ) ){ diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 6340e2a2a..65ad79e29 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -58,8 +58,8 @@ InstStrategyCegqi::InstStrategyCegqi(Env& env, d_added_cbqi_lemma(userContext()), d_vtsCache(new VtsTermCache(qim)), d_bv_invert(nullptr), - d_small_const_multiplier( - NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000))), + d_small_const_multiplier(NodeManager::currentNM()->mkConst( + CONST_RATIONAL, Rational(1) / Rational(1000000))), d_small_const(d_small_const_multiplier) { d_check_vts_lemma_lc = false; @@ -453,7 +453,12 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { d_vtsCache->getVtsTerms(inf, true, false, false); for( unsigned i=0; i<inf.size(); i++ ){ Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl; - Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) ); + Node inf_lem_lb = NodeManager::currentNM()->mkNode( + GT, + inf[i], + NodeManager::currentNM()->mkConst( + CONST_RATIONAL, + Rational(1) / d_small_const.getConst<Rational>())); d_qim.lemma(inf_lem_lb, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF); } } diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp index fe47f1dd1..37ded9b7f 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp +++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp @@ -30,7 +30,7 @@ namespace quantifiers { VtsTermCache::VtsTermCache(QuantifiersInferenceManager& qim) : d_qim(qim) { - d_zero = NodeManager::currentNM()->mkConst(Rational(0)); + d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); } void VtsTermCache::getVtsTerms(std::vector<Node>& t, diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 075299583..8c2d8e6c4 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -364,7 +364,8 @@ int InstMatchGenerator::getMatch(Node f, Node t, InstMatch& m) { if (pat.getKind() == GT) { - t_match = nm->mkNode(MINUS, t, nm->mkConst(Rational(1))); + t_match = + nm->mkNode(MINUS, t, nm->mkConst(CONST_RATIONAL, Rational(1))); }else{ t_match = t; } @@ -380,12 +381,13 @@ int InstMatchGenerator::getMatch(Node f, Node t, InstMatch& m) else { Assert(t.getType().isReal()); - t_match = nm->mkNode(PLUS, t, nm->mkConst(Rational(1))); + t_match = + nm->mkNode(PLUS, t, nm->mkConst(CONST_RATIONAL, Rational(1))); } } else if (pat.getKind() == GEQ) { - t_match = nm->mkNode(PLUS, t, nm->mkConst(Rational(1))); + t_match = nm->mkNode(PLUS, t, nm->mkConst(CONST_RATIONAL, Rational(1))); } else if (pat.getKind() == GT) { diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp index 332346f3f..0ab6e1098 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp +++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp @@ -678,7 +678,8 @@ Node PatternTermSelector::getInversion(Node n, Node x) Assert(nc.isConst()); if (x.getType().isInteger()) { - Node coeff = nm->mkConst(nc.getConst<Rational>().abs()); + Node coeff = + nm->mkConst(CONST_RATIONAL, nc.getConst<Rational>().abs()); if (!nc.getConst<Rational>().abs().isOne()) { x = nm->mkNode(INTS_DIVISION_TOTAL, x, coeff); @@ -690,7 +691,8 @@ Node PatternTermSelector::getInversion(Node n, Node x) } else { - Node coeff = nm->mkConst(Rational(1) / nc.getConst<Rational>()); + Node coeff = nm->mkConst(CONST_RATIONAL, + Rational(1) / nc.getConst<Rational>()); x = nm->mkNode(MULT, x, coeff); } } diff --git a/src/theory/quantifiers/ematching/relational_match_generator.cpp b/src/theory/quantifiers/ematching/relational_match_generator.cpp index 8981a7a2d..dc8f64f6d 100644 --- a/src/theory/quantifiers/ematching/relational_match_generator.cpp +++ b/src/theory/quantifiers/ematching/relational_match_generator.cpp @@ -94,7 +94,10 @@ int RelationalMatchGenerator::getNextMatch(Node q, InstMatch& m) s = rhs; if (!checkPol) { - s = nm->mkNode(PLUS, s, nm->mkConst(Rational(d_rel == GEQ ? -1 : 1))); + s = nm->mkNode( + PLUS, + s, + nm->mkConst(CONST_RATIONAL, Rational(d_rel == GEQ ? -1 : 1))); } d_counter++; Trace("relational-match-gen") diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp index 75a353dbe..24efc60c3 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.cpp +++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp @@ -54,7 +54,7 @@ bool TriggerTermInfo::isAtomicTriggerKind(Kind k) // where these two things require those kinds respectively. return k == APPLY_UF || k == SELECT || k == STORE || k == APPLY_CONSTRUCTOR || k == APPLY_SELECTOR || k == APPLY_SELECTOR_TOTAL - || k == APPLY_TESTER || k == SET_UNION || k == SET_INTERSECTION + || k == APPLY_TESTER || k == SET_UNION || k == SET_INTER || k == SET_SUBSET || k == SET_MINUS || k == SET_MEMBER || k == SET_SINGLETON || k == SEP_PTO || k == BITVECTOR_TO_NAT || k == INT_TO_BITVECTOR || k == HO_APPLY || k == STRING_LENGTH diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 3d20f66b3..5aab618c0 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -49,7 +49,7 @@ ExtendedRewriter::ExtendedRewriter(Rewriter& rew, bool aggr) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); - d_zero = NodeManager::currentNM()->mkConst(Rational(0)); + d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); } void ExtendedRewriter::setCache(Node n, Node ret) const diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 26b526315..b5b9e7d88 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -59,7 +59,7 @@ BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic( Node BoundedIntegers::IntRangeDecisionHeuristic::mkLiteral(unsigned n) { NodeManager* nm = NodeManager::currentNM(); - Node cn = nm->mkConst(Rational(n == 0 ? 0 : n - 1)); + Node cn = nm->mkConst(CONST_RATIONAL, Rational(n == 0 ? 0 : n - 1)); return nm->mkNode(n == 0 ? LT : LEQ, d_proxy_range, cn); } @@ -81,12 +81,13 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma() d_ranges_proxied[curr] = true; NodeManager* nm = NodeManager::currentNM(); Node currLit = getLiteral(curr); - Node lem = - nm->mkNode(EQUAL, - currLit, - nm->mkNode(curr == 0 ? LT : LEQ, - d_range, - nm->mkConst(Rational(curr == 0 ? 0 : curr - 1)))); + Node lem = nm->mkNode( + EQUAL, + currLit, + nm->mkNode( + curr == 0 ? LT : LEQ, + d_range, + nm->mkConst(CONST_RATIONAL, Rational(curr == 0 ? 0 : curr - 1)))); return lem; } @@ -692,7 +693,8 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) { } choices.pop_back(); Node bvl = nm->mkNode(BOUND_VAR_LIST, choice_i); - Node cMinCard = nm->mkNode(LEQ, srCardN, nm->mkConst(Rational(i))); + Node cMinCard = + nm->mkNode(LEQ, srCardN, nm->mkConst(CONST_RATIONAL, Rational(i))); choice_i = nm->mkNode(WITNESS, bvl, nm->mkNode(OR, cMinCard, cBody)); d_setm_choice[sro].push_back(choice_i); } @@ -816,7 +818,8 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node Node range = rewrite(nm->mkNode(MINUS, u, l)); // 9999 is an arbitrary range past which we do not do exhaustive // bounded instantation, based on the check below. - Node ra = rewrite(nm->mkNode(LEQ, range, nm->mkConst(Rational(9999)))); + Node ra = rewrite(nm->mkNode( + LEQ, range, nm->mkConst(CONST_RATIONAL, Rational(9999)))); Node tl = l; Node tu = u; getBounds( q, v, rsi, tl, tu ); @@ -827,7 +830,8 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; for (long k = 0; k < rr; k++) { - Node t = nm->mkNode(PLUS, tl, nm->mkConst(Rational(k))); + Node t = + nm->mkNode(PLUS, tl, nm->mkConst(CONST_RATIONAL, Rational(k))); t = rewrite(t); elements.push_back( t ); } diff --git a/src/theory/quantifiers/quant_bound_inference.cpp b/src/theory/quantifiers/quant_bound_inference.cpp index 83e48bf9c..af72e2a7c 100644 --- a/src/theory/quantifiers/quant_bound_inference.cpp +++ b/src/theory/quantifiers/quant_bound_inference.cpp @@ -61,9 +61,10 @@ bool QuantifiersBoundInference::mayComplete(TypeNode tn, unsigned maxCard) if (!c.isLargeFinite()) { NodeManager* nm = NodeManager::currentNM(); - Node card = nm->mkConst(Rational(c.getFiniteCardinality())); + Node card = + nm->mkConst(CONST_RATIONAL, Rational(c.getFiniteCardinality())); // check if less than fixed upper bound - Node oth = nm->mkConst(Rational(maxCard)); + Node oth = nm->mkConst(CONST_RATIONAL, Rational(maxCard)); Node eq = nm->mkNode(LEQ, card, oth); eq = Rewriter::rewrite(eq); mc = eq.isConst() && eq.getConst<bool>(); diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index f04514480..9f7b270de 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2281,7 +2281,7 @@ TNode QuantConflictFind::getZero( Kind k ) { if( it==d_zero.end() ){ Node nn; if( k==PLUS ){ - nn = NodeManager::currentNM()->mkConst( Rational(0) ); + nn = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)); } d_zero[k] = nn; return nn; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 88c6cd96f..adb91fddd 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -920,7 +920,7 @@ bool QuantifiersRewriter::getVarElimLit(Node body, for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++) { TypeNode tn = tspec[j]; - Node rn = nm->mkConst(Rational(j)); + Node rn = nm->mkConst(CONST_RATIONAL, Rational(j)); Node cacheVal = BoundVarManager::getCacheValue(body, lit, rn); Node v = bvm->mkBoundVar<QRewDtExpandAttribute>(cacheVal, tn); newChildren.push_back(v); diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 6dcb318f3..4dea0dc22 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -285,10 +285,12 @@ Node Skolemize::mkSkolemizedBody(Node f, } else if (options::intWfInduction() && tn.isInteger()) { - Node icond = nm->mkNode(GEQ, k, nm->mkConst(Rational(0))); - Node iret = ret.substitute(ind_vars[0], - nm->mkNode(MINUS, k, nm->mkConst(Rational(1)))) - .negate(); + Node icond = nm->mkNode(GEQ, k, nm->mkConst(CONST_RATIONAL, Rational(0))); + Node iret = + ret.substitute( + ind_vars[0], + nm->mkNode(MINUS, k, nm->mkConst(CONST_RATIONAL, Rational(1)))) + .negate(); n_str_ind = nm->mkNode(OR, icond.negate(), iret); n_str_ind = nm->mkNode(AND, icond, n_str_ind); } diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index b60bc2736..be80992ea 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -480,7 +480,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) std::set<TypeNode> unresolvedTypes; unresolvedTypes.insert(u); std::vector<TypeNode> cargsEmpty; - Node cr = nm->mkConst(Rational(1)); + Node cr = nm->mkConst(CONST_RATIONAL, Rational(1)); sdt.addConstructor(cr, "1", cargsEmpty); std::vector<TypeNode> cargsPlus; cargsPlus.push_back(u); @@ -503,8 +503,8 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) if (pow_two > 0) { Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum); - Node fair_lemma = - nm->mkNode(GEQ, size_ve, nm->mkConst(Rational(pow_two - 1))); + Node fair_lemma = nm->mkNode( + GEQ, size_ve, nm->mkConst(CONST_RATIONAL, Rational(pow_two - 1))); fair_lemma = nm->mkNode(OR, newLit, fair_lemma); Trace("cegis-unif-enum-lemma") << "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n"; diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 959532d98..674183b20 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -257,7 +257,7 @@ void SygusEnumerator::TermCache::initialize(SygusStatistics* s, // more aggressive merging of constructor classes. On the negative side, // this adds another level of indirection to remember which argument // positions the argument types occur in, for each constructor. - Node n = nm->mkConst(Rational(i)); + Node n = nm->mkConst(CONST_RATIONAL, Rational(i)); nToC[n] = i; tnit.add(n, argTypes[i]); } diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 034f5f23c..cca1d76e2 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -84,7 +84,7 @@ void CegGrammarConstructor::collectTerms( TypeNode tn = cur.getType(); Node c = cur; if( tn.isReal() ){ - c = nm->mkConst( c.getConst<Rational>().abs() ); + c = nm->mkConst(CONST_RATIONAL, c.getConst<Rational>().abs()); } consts[tn].insert(c); if (tn.isInteger()) @@ -409,8 +409,8 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, NodeManager* nm = NodeManager::currentNM(); if (type.isReal()) { - ops.push_back(nm->mkConst(Rational(0))); - ops.push_back(nm->mkConst(Rational(1))); + ops.push_back(nm->mkConst(CONST_RATIONAL, Rational(0))); + ops.push_back(nm->mkConst(CONST_RATIONAL, Rational(1))); } else if (type.isBitVector()) { @@ -555,7 +555,7 @@ Node CegGrammarConstructor::createLambdaWithZeroArg( Assert(bArgType.isReal() || bArgType.isBitVector()); if (bArgType.isReal()) { - zarg = nm->mkConst(Rational(0)); + zarg = nm->mkConst(CONST_RATIONAL, Rational(0)); } else { @@ -798,7 +798,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( /* Add operator 1 */ Trace("sygus-grammar-def") << "\t...add for 1 to Pos_Int\n"; std::vector<TypeNode> cargsEmpty; - sdts.back().addConstructor(nm->mkConst(Rational(1)), "1", cargsEmpty); + sdts.back().addConstructor( + nm->mkConst(CONST_RATIONAL, Rational(1)), "1", cargsEmpty); /* Add operator PLUS */ Kind kind = PLUS; Trace("sygus-grammar-def") << "\t...add for PLUS to Pos_Int\n"; @@ -990,7 +991,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( sdts[i].addConstructor(lambda, "singleton", cargsSingleton); // add for union, difference, intersection - std::vector<Kind> bin_kinds = {SET_UNION, SET_INTERSECTION, SET_MINUS}; + std::vector<Kind> bin_kinds = {SET_UNION, SET_INTER, SET_MINUS}; std::vector<TypeNode> cargsBinary; cargsBinary.push_back(unres_t); cargsBinary.push_back(unres_t); diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 2fc7f0c29..89cee0145 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -32,6 +32,8 @@ #include "util/sampler.h" #include "util/string.h" +using namespace cvc5::kind; + namespace cvc5 { namespace theory { namespace quantifiers { @@ -587,14 +589,14 @@ Node SygusSampler::getRandomValue(TypeNode tn) std::vector<Node> sum; for (unsigned j = 0, size = vec.size(); j < size; j++) { - Node digit = nm->mkConst(Rational(vec[j]) * curr); + Node digit = nm->mkConst(CONST_RATIONAL, Rational(vec[j]) * curr); sum.push_back(digit); curr = curr * baser; } Node ret; if (sum.empty()) { - ret = nm->mkConst(Rational(0)); + ret = nm->mkConst(CONST_RATIONAL, Rational(0)); } else if (sum.size() == 1) { @@ -629,7 +631,7 @@ Node SygusSampler::getRandomValue(TypeNode tn) } else { - return nm->mkConst(sr / rr); + return nm->mkConst(CONST_RATIONAL, sr / rr); } } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 5c9e91d32..0408d27da 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -186,7 +186,7 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn) Node TermDb::getMatchOperator( Node n ) { Kind k = n.getKind(); //datatype operators may be parametric, always assume they are - if (k == SELECT || k == STORE || k == SET_UNION || k == SET_INTERSECTION + if (k == SELECT || k == STORE || k == SET_UNION || k == SET_INTER || k == SET_SUBSET || k == SET_MINUS || k == SET_MEMBER || k == SET_SINGLETON || k == APPLY_SELECTOR_TOTAL || k == APPLY_SELECTOR || k == APPLY_TESTER || k == SEP_PTO || k == HO_APPLY || k == SEQ_NTH diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index de4c56552..cb8bad174 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -283,7 +283,7 @@ bool TermUtil::isAssoc(Kind k, bool reqNAry) { if (reqNAry) { - if (k == SET_UNION || k == SET_INTERSECTION) + if (k == SET_UNION || k == SET_INTER) { return false; } @@ -292,7 +292,7 @@ bool TermUtil::isAssoc(Kind k, bool reqNAry) || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR || k == BITVECTOR_XNOR || k == BITVECTOR_CONCAT || k == STRING_CONCAT - || k == SET_UNION || k == SET_INTERSECTION || k == RELATION_JOIN + || k == SET_UNION || k == SET_INTER || k == RELATION_JOIN || k == RELATION_PRODUCT || k == SEP_STAR; } @@ -300,7 +300,7 @@ bool TermUtil::isComm(Kind k, bool reqNAry) { if (reqNAry) { - if (k == SET_UNION || k == SET_INTERSECTION) + if (k == SET_UNION || k == SET_INTER) { return false; } @@ -308,7 +308,7 @@ bool TermUtil::isComm(Kind k, bool reqNAry) return k == EQUAL || k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR - || k == BITVECTOR_XNOR || k == SET_UNION || k == SET_INTERSECTION + || k == BITVECTOR_XNOR || k == SET_UNION || k == SET_INTER || k == SEP_STAR; } @@ -332,7 +332,7 @@ Node TermUtil::mkTypeValue(TypeNode tn, int32_t val) if (tn.isInteger() || tn.isReal()) { Rational c(val); - n = NodeManager::currentNM()->mkConst(c); + n = NodeManager::currentNM()->mkConst(CONST_RATIONAL, c); } else if (tn.isBitVector()) { |