diff options
Diffstat (limited to 'src/theory/quantifiers/cegqi')
4 files changed, 44 insertions, 24 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, |