diff options
8 files changed, 91 insertions, 82 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 77b1d42a9..85e91fee3 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -33,8 +33,8 @@ namespace cvc5 { namespace theory { namespace quantifiers { -ArithInstantiator::ArithInstantiator(TypeNode tn, VtsTermCache* vtc) - : Instantiator(tn), d_vtc(vtc) +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)); @@ -86,17 +86,15 @@ bool ArithInstantiator::processEquality(CegInstantiator* ci, { Trace("cegqi-arith-debug") << "...mult lhs by " << rhs_coeff << std::endl; eq_lhs = nm->mkNode(MULT, rhs_coeff, eq_lhs); - eq_lhs = Rewriter::rewrite(eq_lhs); } if (!lhs_coeff.isNull()) { Trace("cegqi-arith-debug") << "...mult rhs by " << lhs_coeff << std::endl; eq_rhs = nm->mkNode(MULT, lhs_coeff, eq_rhs); - eq_rhs = Rewriter::rewrite(eq_rhs); } } Node eq = eq_lhs.eqNode(eq_rhs); - eq = Rewriter::rewrite(eq); + eq = rewrite(eq); Node val; TermProperties pv_prop; Node vts_coeff_inf; @@ -188,7 +186,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, PLUS, val, nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1))); - uval = Rewriter::rewrite(uval); + uval = rewrite(uval); } else { @@ -227,7 +225,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, if (!pv_prop.isBasic()) { lhs_value = pv_prop.getModifiedTerm(pv_value); - lhs_value = Rewriter::rewrite(lhs_value); + lhs_value = rewrite(lhs_value); } Trace("cegqi-arith-debug") << "Disequality : check model values " << lhs_value << " " @@ -241,7 +239,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, // where lhs or rhs contains a transcendental function. We consider // the bound to be an upper bound in this case. Node cmp = nm->mkNode(GEQ, lhs_value, rhs_value); - cmp = Rewriter::rewrite(cmp); + cmp = rewrite(cmp); is_upper = !cmp.isConst() || !cmp.getConst<bool>(); } } @@ -256,7 +254,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, uires = is_upper ? CEG_TT_LOWER : CEG_TT_UPPER; uval = nm->mkNode( PLUS, val, nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1))); - uval = Rewriter::rewrite(uval); + uval = rewrite(uval); } else { @@ -285,7 +283,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, else { vts_coeff_delta = nm->mkNode(PLUS, vts_coeff_delta, delta_coeff); - vts_coeff_delta = Rewriter::rewrite(vts_coeff_delta); + vts_coeff_delta = rewrite(vts_coeff_delta); } } else @@ -293,7 +291,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, Node delta = d_vtc->getVtsDelta(); uval = nm->mkNode( uires == CEG_TT_UPPER_STRICT ? PLUS : MINUS, uval, delta); - uval = Rewriter::rewrite(uval); + uval = rewrite(uval); } } if (options::cegqiModel()) @@ -364,7 +362,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, if (rr == 0) { val = nm->mkNode(UMINUS, val); - val = Rewriter::rewrite(val); + val = rewrite(val); } TermProperties pv_prop_no_bound; if (ci->constructInstantiationInc(pv, val, pv_prop_no_bound, sf)) @@ -456,7 +454,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, nm->mkConst(Rational(1) / d_mbp_coeff[rr][j].getConst<Rational>()), value[t]); - value[t] = Rewriter::rewrite(value[t]); + value[t] = rewrite(value[t]); } // check if new best, if we have not already set it. if (best != -1 && !new_best_set) @@ -466,7 +464,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, { Kind k = rr == 0 ? GEQ : LEQ; Node cmp_bound = nm->mkNode(k, value[t], best_bound_value[t]); - cmp_bound = Rewriter::rewrite(cmp_bound); + cmp_bound = rewrite(cmp_bound); // Should be comparing two constant values which should rewrite // to a constant. If a step failed, we assume that this is not // the new best bound. We might not be comparing constant @@ -611,7 +609,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, val = nm->mkNode(MULT, nm->mkNode(PLUS, vals[0], vals[1]), nm->mkConst(Rational(1) / Rational(2))); - val = Rewriter::rewrite(val); + val = rewrite(val); } } else @@ -619,12 +617,12 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, if (!vals[0].isNull()) { val = nm->mkNode(PLUS, vals[0], d_one); - val = Rewriter::rewrite(val); + val = rewrite(val); } else if (!vals[1].isNull()) { val = nm->mkNode(MINUS, vals[1], d_one); - val = Rewriter::rewrite(val); + val = rewrite(val); } } Trace("cegqi-arith-bound") << "Midpoint value : " << val << std::endl; @@ -718,7 +716,7 @@ bool ArithInstantiator::postProcessInstantiationForVariable( // then we are successful Node eq_rhs = sf.d_subs[index]; Node eq = eq_lhs.eqNode(eq_rhs); - eq = Rewriter::rewrite(eq); + eq = rewrite(eq); Trace("cegqi-arith-debug") << "...equality is " << eq << std::endl; std::map<Node, Node> msum; if (!ArithMSum::getMonomialSumLit(eq, msum)) @@ -823,7 +821,7 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci, MULT, nm->mkConst(Rational(-1) / itv->second.getConst<Rational>()), vts_coeff[t]); - vts_coeff[t] = Rewriter::rewrite(vts_coeff[t]); + vts_coeff[t] = rewrite(vts_coeff[t]); } else if (itv->second.getConst<Rational>().sgn() == 1) { @@ -894,8 +892,7 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci, } else { - msum[it->first] = - Rewriter::rewrite(nm->mkNode(MULT, it->second, rcoeff)); + msum[it->first] = rewrite(nm->mkNode(MULT, it->second, rcoeff)); } } if (!it->first.isNull() && !it->first.getType().isInteger()) @@ -910,7 +907,7 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci, // multiply inf if (!vts_coeff[0].isNull()) { - vts_coeff[0] = Rewriter::rewrite(nm->mkNode(MULT, rcoeff, vts_coeff[0])); + vts_coeff[0] = rewrite(nm->mkNode(MULT, rcoeff, vts_coeff[0])); } Node realPart = real_part.empty() ? d_zero @@ -931,7 +928,7 @@ CegTermType ArithInstantiator::solve_arith(CegInstantiator* ci, int ires_use = (msum[pv].isNull() || msum[pv].getConst<Rational>().sgn() == 1) ? 1 : -1; - val = Rewriter::rewrite( + val = rewrite( nm->mkNode(ires_use == -1 ? PLUS : MINUS, nm->mkNode(ires_use == -1 ? MINUS : PLUS, val, realPart), nm->mkNode(TO_INTEGER, realPart))); @@ -982,7 +979,7 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci, { Assert(c.getType().isInteger()); ceValue = nm->mkNode(MULT, ceValue, c); - ceValue = Rewriter::rewrite(ceValue); + ceValue = rewrite(ceValue); if (new_theta.isNull()) { new_theta = c; @@ -990,7 +987,7 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci, else { new_theta = nm->mkNode(MULT, new_theta, c); - new_theta = Rewriter::rewrite(new_theta); + new_theta = rewrite(new_theta); } Trace("cegqi-arith-bound2") << "...c*e = " << ceValue << std::endl; Trace("cegqi-arith-bound2") << "...theta = " << new_theta << std::endl; @@ -1006,31 +1003,31 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci, { rho = nm->mkNode(MINUS, mt, ceValue); } - rho = Rewriter::rewrite(rho); + rho = rewrite(rho); Trace("cegqi-arith-bound2") << "...rho = " << me << " - " << mt << " = " << rho << std::endl; Trace("cegqi-arith-bound2") << "..." << rho << " mod " << new_theta << " = "; rho = nm->mkNode(INTS_MODULUS_TOTAL, rho, new_theta); - rho = Rewriter::rewrite(rho); + rho = rewrite(rho); Trace("cegqi-arith-bound2") << rho << std::endl; Kind rk = isLower ? PLUS : MINUS; val = nm->mkNode(rk, val, rho); - val = Rewriter::rewrite(val); + val = rewrite(val); Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl; } if (!inf_coeff.isNull()) { Assert(!d_vts_sym[0].isNull()); val = nm->mkNode(PLUS, val, nm->mkNode(MULT, inf_coeff, d_vts_sym[0])); - val = Rewriter::rewrite(val); + val = rewrite(val); } if (!delta_coeff.isNull()) { // create delta here if necessary val = nm->mkNode( PLUS, val, nm->mkNode(MULT, delta_coeff, d_vtc->getVtsDelta())); - val = Rewriter::rewrite(val); + val = rewrite(val); } return val; } diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h index 6d65ae16c..e102b834e 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h @@ -44,7 +44,7 @@ namespace quantifiers { class ArithInstantiator : public Instantiator { public: - ArithInstantiator(TypeNode tn, VtsTermCache* vtc); + ArithInstantiator(Env& env, TypeNode tn, VtsTermCache* vtc); virtual ~ArithInstantiator() {} /** reset */ void reset(CegInstantiator* ci, diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 9ffb31df3..5b5c1cc86 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -54,8 +54,8 @@ class CegInstantiatorBvInverterQuery : public BvInverterQuery CegInstantiator* d_ci; }; -BvInstantiator::BvInstantiator(TypeNode tn, BvInverter* inv) - : Instantiator(tn), d_inverter(inv), d_inst_id_counter(0) +BvInstantiator::BvInstantiator(Env& env, TypeNode tn, BvInverter* inv) + : Instantiator(env, tn), d_inverter(inv), d_inst_id_counter(0) { // The inverter utility d_inverter is global to all BvInstantiator classes. // This must be global since we need to: diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h index cbc73dc2c..0c2cb05df 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h @@ -39,7 +39,7 @@ namespace quantifiers { class BvInstantiator : public Instantiator { public: - BvInstantiator(TypeNode tn, BvInverter* inv); + BvInstantiator(Env& env, TypeNode tn, BvInverter* inv); ~BvInstantiator() override; /** reset */ void reset(CegInstantiator* ci, diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h index 72746a39b..9a99c4743 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h @@ -33,7 +33,7 @@ namespace quantifiers { class DtInstantiator : public Instantiator { public: - DtInstantiator(TypeNode tn) : Instantiator(tn) {} + DtInstantiator(Env& env, TypeNode tn) : Instantiator(env, tn) {} virtual ~DtInstantiator() {} /** reset */ void reset(CegInstantiator* ci, diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 4b06589b3..d61dd2bd2 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -137,8 +137,9 @@ void TermProperties::composeProperty(TermProperties& p) } else { - d_coeff = NodeManager::currentNM()->mkNode(MULT, d_coeff, p.d_coeff); - d_coeff = Rewriter::rewrite(d_coeff); + NodeManager* nm = NodeManager::currentNM(); + d_coeff = nm->mkConst(Rational(d_coeff.getConst<Rational>() + * p.d_coeff.getConst<Rational>())); } } @@ -161,9 +162,11 @@ void SolvedForm::push_back(Node pv, Node n, TermProperties& pv_prop) } else { - new_theta = - NodeManager::currentNM()->mkNode(MULT, new_theta, pv_prop.d_coeff); - new_theta = Rewriter::rewrite(new_theta); + 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>() + * pv_prop.d_coeff.getConst<Rational>())); } d_theta.push_back(new_theta); } @@ -182,11 +185,13 @@ void SolvedForm::pop_back(Node pv, Node n, TermProperties& pv_prop) d_theta.pop_back(); } -CegInstantiator::CegInstantiator(Node q, +CegInstantiator::CegInstantiator(Env& env, + Node q, QuantifiersState& qs, TermRegistry& tr, InstStrategyCegqi* parent) - : d_quant(q), + : EnvObj(env), + d_quant(q), d_qstate(qs), d_treg(tr), d_parent(parent), @@ -476,16 +481,16 @@ void CegInstantiator::activateInstantiationVariable(Node v, unsigned index) TypeNode tn = v.getType(); Instantiator * vinst; if( tn.isReal() ){ - vinst = new ArithInstantiator(tn, d_parent->getVtsTermCache()); + vinst = new ArithInstantiator(d_env, tn, d_parent->getVtsTermCache()); }else if( tn.isDatatype() ){ - vinst = new DtInstantiator(tn); + vinst = new DtInstantiator(d_env, tn); }else if( tn.isBitVector() ){ - vinst = new BvInstantiator(tn, d_parent->getBvInverter()); + vinst = new BvInstantiator(d_env, tn, d_parent->getBvInverter()); }else if( tn.isBoolean() ){ - vinst = new ModelValueInstantiator(tn); + vinst = new ModelValueInstantiator(d_env, tn); }else{ //default - vinst = new Instantiator(tn); + vinst = new Instantiator(d_env, tn); } d_instantiator[v] = vinst; } @@ -1120,7 +1125,7 @@ bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& no Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, std::vector< Node >& non_basic, TermProperties& pv_prop, bool try_coeff ) { - n = Rewriter::rewrite(n); + n = rewrite(n); computeProgVars( n ); bool is_basic = canApplyBasicSubstitution( n, non_basic ); if( Trace.isOn("sygus-si-apply-subs-debug") ){ @@ -1144,7 +1149,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node 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>() ) ); nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn ); - nn = Rewriter::rewrite( nn ); + nn = rewrite(nn); nsubs.push_back( nn ); }else{ nsubs.push_back( subs[i] ); @@ -1183,13 +1188,15 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node } //make sum with normalized coefficient if( !pv_prop.d_coeff.isNull() ){ - pv_prop.d_coeff = Rewriter::rewrite( pv_prop.d_coeff ); + pv_prop.d_coeff = rewrite(pv_prop.d_coeff); Trace("sygus-si-apply-subs-debug") << "Combined coeff : " << pv_prop.d_coeff << std::endl; std::vector< Node > children; for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ Node c_coeff; if( !msum_coeff[it->first].isNull() ){ - c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_prop.d_coeff.getConst<Rational>() / msum_coeff[it->first].getConst<Rational>() ) ); + c_coeff = rewrite(NodeManager::currentNM()->mkConst( + pv_prop.d_coeff.getConst<Rational>() + / msum_coeff[it->first].getConst<Rational>())); }else{ c_coeff = pv_prop.d_coeff; } @@ -1207,7 +1214,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node Trace("sygus-si-apply-subs-debug") << "Add child : " << c << std::endl; } Node nretc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children ); - nretc = Rewriter::rewrite( nretc ); + nretc = rewrite(nretc); //ensure that nret does not contain vars if (!expr::hasSubterm(nretc, vars)) { @@ -1226,7 +1233,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node } } if( n!=nret && !nret.isNull() ){ - nret = Rewriter::rewrite( nret ); + nret = rewrite(nret); } return nret; } @@ -1252,7 +1259,7 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >& atom_rhs = atom[1]; }else{ atom_lhs = nm->mkNode(MINUS, atom[0], atom[1]); - atom_lhs = Rewriter::rewrite( atom_lhs ); + atom_lhs = rewrite(atom_lhs); atom_rhs = nm->mkConst(Rational(0)); } //must be an eligible term @@ -1269,7 +1276,7 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >& if( !atom_lhs.isNull() ){ if( !atom_lhs_prop.d_coeff.isNull() ){ atom_rhs = nm->mkNode(MULT, atom_lhs_prop.d_coeff, atom_rhs); - atom_rhs = Rewriter::rewrite(atom_rhs); + atom_rhs = rewrite(atom_rhs); } lret = nm->mkNode(atom.getKind(), atom_lhs, atom_rhs); if( !pol ){ @@ -1282,7 +1289,7 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >& } } if( lit!=lret && !lret.isNull() ){ - lret = Rewriter::rewrite( lret ); + lret = rewrite(lret); } return lret; } @@ -1621,7 +1628,7 @@ void CegInstantiator::registerCounterexampleLemma(Node lem, } } -Instantiator::Instantiator(TypeNode tn) : d_type(tn) +Instantiator::Instantiator(Env& env, TypeNode tn) : EnvObj(env), d_type(tn) { d_closed_enum_type = tn.isClosedEnumerable(); } diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index 2c228777d..600f50f42 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -21,6 +21,7 @@ #include <vector> #include "expr/node.h" +#include "smt/env_obj.h" #include "theory/inference_id.h" #include "util/statistics_stats.h" @@ -86,11 +87,12 @@ class TermProperties { // get cache node // we consider terms + TermProperties that are unique up to their cache node // (see constructInstantiationInc) - virtual Node getCacheNode() const { return d_coeff; } - // is non-basic - virtual bool isBasic() const { return d_coeff.isNull(); } - // get modified term - virtual Node getModifiedTerm( Node pv ) const { + Node getCacheNode() const { return d_coeff; } + // is non-basic + bool isBasic() const { return d_coeff.isNull(); } + // get modified term + Node getModifiedTerm(Node pv) const + { if( !d_coeff.isNull() ){ return NodeManager::currentNM()->mkNode( kind::MULT, d_coeff, pv ); }else{ @@ -99,7 +101,7 @@ class TermProperties { } // compose property, should be such that: // p.getModifiedTerm( this.getModifiedTerm( x ) ) = this_updated.getModifiedTerm( x ) - virtual void composeProperty(TermProperties& p); + void composeProperty(TermProperties& p); }; /** Solved form @@ -203,13 +205,15 @@ std::ostream& operator<<(std::ostream& os, CegHandledStatus status); * For details on counterexample-guided quantifier instantiation * (for linear arithmetic), see Reynolds/King/Kuncak FMSD 2017. */ -class CegInstantiator { +class CegInstantiator : protected EnvObj +{ public: /** * The instantiator will be constructing instantiations for quantified formula * q, parent is the owner of this object. */ - CegInstantiator(Node q, + CegInstantiator(Env& env, + Node q, QuantifiersState& qs, TermRegistry& tr, InstStrategyCegqi* parent); @@ -575,21 +579,22 @@ class CegInstantiator { * In these calls, the Instantiator in turn makes calls to methods in * CegInstanatior (primarily constructInstantiationInc). */ -class Instantiator { -public: - Instantiator(TypeNode tn); - virtual ~Instantiator() {} - /** reset - * This is called once, prior to any of the below methods are called. - * This function sets up any initial information necessary for constructing - * instantiations for pv based on the current context. - */ - virtual void reset(CegInstantiator* ci, - SolvedForm& sf, - Node pv, - CegInstEffort effort) - { - } +class Instantiator : protected EnvObj +{ + public: + Instantiator(Env& env, TypeNode tn); + virtual ~Instantiator() {} + /** reset + * This is called once, prior to any of the below methods are called. + * This function sets up any initial information necessary for constructing + * instantiations for pv based on the current context. + */ + virtual void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) + { + } /** has process equal term * @@ -782,7 +787,7 @@ public: class ModelValueInstantiator : public Instantiator { public: - ModelValueInstantiator(TypeNode tn) : Instantiator(tn) {} + ModelValueInstantiator(Env& env, TypeNode tn) : Instantiator(env, tn) {} virtual ~ModelValueInstantiator() {} bool useModelValue(CegInstantiator* ci, SolvedForm& sf, diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 04fa1d2fe..e4a75cebb 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -506,7 +506,7 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it = d_cinst.find(q); if( it==d_cinst.end() ){ - d_cinst[q].reset(new CegInstantiator(q, d_qstate, d_treg, this)); + d_cinst[q].reset(new CegInstantiator(d_env, q, d_qstate, d_treg, this)); return d_cinst[q].get(); } return it->second.get(); |