diff options
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 5 | ||||
| -rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 7 | ||||
| -rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 56 | ||||
| -rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 95 | ||||
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 18 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 26 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp | 16 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_util.cpp | 12 |
12 files changed, 158 insertions, 90 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index f1235d185..4ea006d54 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/cegqi/ceg_arith_instantiator.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/partial_model.h" @@ -851,7 +852,7 @@ int ArithInstantiator::solve_arith(CegInstantiator* ci, << pv << " " << atom.getKind() << " " << val << std::endl; } // when not pure LIA/LRA, we must check whether the lhs contains pv - if (val.hasSubterm(pv)) + if (expr::hasSubterm(val, pv)) { Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl; return 0; diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp index 3a0db0273..e56d5f5db 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp @@ -14,6 +14,8 @@ #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h" +#include "expr/node_algorithm.h" + using namespace std; using namespace CVC4::kind; using namespace CVC4::context; @@ -170,7 +172,7 @@ Node DtInstantiator::solve_dt(Node v, Node a, Node b, Node sa, Node sb) if (!ret.isNull()) { // ensure does not contain v - if (ret.hasSubterm(v)) + if (expr::hasSubterm(ret, v)) { ret = Node::null(); } diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp index 9f12f8b23..3535b57b7 100644 --- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/cegqi/ceg_epr_instantiator.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/term_database.h" @@ -145,7 +146,7 @@ void EprInstantiator::computeMatchScore(CegInstantiator* ci, Node eqc, std::map<Node, int>& match_score) { - if (!inst::Trigger::isAtomicTrigger(catom) || !catom.hasSubterm(pv)) + if (!inst::Trigger::isAtomicTrigger(catom) || !expr::hasSubterm(catom, pv)) { return; } diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 1abd1d4e1..2a17f1e36 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -19,6 +19,7 @@ #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h" #include "theory/quantifiers/cegqi/ceg_epr_instantiator.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "smt/term_formula_removal.h" #include "theory/arith/arith_msum.h" @@ -1214,7 +1215,7 @@ void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq { Node nn = n[i == 0 ? 1 : 0]; std::map<Node, std::vector<Node> >::iterator it = teq.find(n[i]); - if (it != teq.end() && !nn.hasFreeVar() + if (it != teq.end() && !expr::hasFreeVar(nn) && std::find(it->second.begin(), it->second.end(), nn) == it->second.end()) { @@ -1268,7 +1269,7 @@ void CegInstantiator::presolve( Node q ) { Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() ); lem = NodeManager::currentNM()->mkNode( OR, g, lem ); Trace("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl; - Assert(!lem.hasFreeVar()); + Assert(!expr::hasFreeVar(lem)); d_qe->getOutputChannel().lemma( lem, false, true ); } } diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp index 615968704..c281e81ca 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp @@ -13,6 +13,7 @@ **/ #include "theory/quantifiers/cegqi/inst_strategy_cbqi.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "smt/term_formula_removal.h" #include "theory/arith/partial_model.h" @@ -662,7 +663,7 @@ bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { } } //only legal if current quantified formula contains n - return d_curr_quant.hasSubterm(n); + return expr::hasSubterm(d_curr_quant, n); } }else{ return true; diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 1fce68de0..3615ef6f4 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/ematching/trigger.h" +#include "expr/node_algorithm.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/ematching/candidate_generator.h" #include "theory/quantifiers/ematching/ho_trigger.h" @@ -305,10 +306,12 @@ bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) { } }else if( isUsableAtomicTrigger( n1, q ) ){ if (options::relationalTriggers() && n2.getKind() == INST_CONSTANT - && !n1.hasSubterm(n2)) + && !expr::hasSubterm(n1, n2)) { return true; - }else if( !quantifiers::TermUtil::hasInstConstAttr(n2) ){ + } + else if (!quantifiers::TermUtil::hasInstConstAttr(n2)) + { return true; } } diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index fd98aa208..f0789a503 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/fmf/bounded_integers.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/first_order_model.h" @@ -436,17 +437,23 @@ void BoundedIntegers::checkOwnership(Node f) << bound_lit_map[2][v] << std::endl; } }else if( it->second==BOUND_FIXED_SET ){ - setBoundedVar( f, v, BOUND_FIXED_SET ); + setBoundedVar(f, v, BOUND_FIXED_SET); setBoundVar = true; - for( unsigned i=0; i<bound_fixed_set[v].size(); i++ ){ + for (unsigned i = 0; i < bound_fixed_set[v].size(); i++) + { Node t = bound_fixed_set[v][i]; - if( t.hasBoundVar() ){ - d_fixed_set_ngr_range[f][v].push_back( t ); - }else{ - d_fixed_set_gr_range[f][v].push_back( t ); + if (expr::hasBoundVar(t)) + { + d_fixed_set_ngr_range[f][v].push_back(t); } - } - Trace("bound-int") << "Variable " << v << " is bound because of disequality conjunction " << bound_lit_map[3][v] << std::endl; + else + { + d_fixed_set_gr_range[f][v].push_back(t); + } + } + Trace("bound-int") << "Variable " << v + << " is bound because of disequality conjunction " + << bound_lit_map[3][v] << std::endl; } if( setBoundVar ){ success = true; @@ -543,9 +550,11 @@ void BoundedIntegers::checkOwnership(Node f) Node r = itr->second; Assert( !r.isNull() ); bool isProxy = false; - if( r.hasBoundVar() ){ - //introduce a new bound - Node new_range = NodeManager::currentNM()->mkSkolem( "bir", r.getType(), "bound for term" ); + if (expr::hasBoundVar(r)) + { + // introduce a new bound + Node new_range = NodeManager::currentNM()->mkSkolem( + "bir", r.getType(), "bound for term"); d_nground_range[f][v] = r; d_range[f][v] = new_range; r = new_range; @@ -645,13 +654,21 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node return; } -bool BoundedIntegers::isGroundRange( Node q, Node v ) { - if( isBoundVar(q,v) ){ - if( d_bound_type[q][v]==BOUND_INT_RANGE ){ - return !getLowerBound(q,v).hasBoundVar() && !getUpperBound(q,v).hasBoundVar(); - }else if( d_bound_type[q][v]==BOUND_SET_MEMBER ){ - return !d_setm_range[q][v].hasBoundVar(); - }else if( d_bound_type[q][v]==BOUND_FIXED_SET ){ +bool BoundedIntegers::isGroundRange(Node q, Node v) +{ + if (isBoundVar(q, v)) + { + if (d_bound_type[q][v] == BOUND_INT_RANGE) + { + return !expr::hasBoundVar(getLowerBound(q, v)) + && !expr::hasBoundVar(getUpperBound(q, v)); + } + else if (d_bound_type[q][v] == BOUND_SET_MEMBER) + { + return !expr::hasBoundVar(d_setm_range[q][v]); + } + else if (d_bound_type[q][v] == BOUND_FIXED_SET) + { return !d_fixed_set_ngr_range[q][v].empty(); } } @@ -684,7 +701,7 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) { return sr; } Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl; - Assert(!sr.hasFreeVar()); + Assert(!expr::hasFreeVar(sr)); Node sro = sr; sr = d_quantEngine->getModel()->getValue(sr); // if non-constant, then sr does not occur in the model, we fail @@ -915,4 +932,3 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node return true; } } - diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 3b2a650ab..3006a07bf 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -17,14 +17,15 @@ #include <vector> +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "smt/smt_statistics_registry.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/ematching/trigger.h" #include "theory/theory_engine.h" using namespace CVC4::kind; @@ -179,23 +180,34 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) registerNode( n[1], hasPol, pol, true ); }else{ if( !MatchGen::isHandledBoolConnective( n ) ){ - if( n.hasBoundVar() ){ - //literals - if( n.getKind()==EQUAL ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - flatten( n[i], beneathQuant ); + if (expr::hasBoundVar(n)) + { + // literals + if (n.getKind() == EQUAL) + { + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + flatten(n[i], beneathQuant); } - }else if( MatchGen::isHandledUfTerm( n ) ){ - flatten( n, beneathQuant ); - }else if( n.getKind()==ITE ){ - for( unsigned i=1; i<=2; i++ ){ - flatten( n[i], beneathQuant ); + } + else if (MatchGen::isHandledUfTerm(n)) + { + flatten(n, beneathQuant); + } + else if (n.getKind() == ITE) + { + for (unsigned i = 1; i <= 2; i++) + { + flatten(n[i], beneathQuant); } - registerNode( n[0], false, pol, beneathQuant ); - }else if( options::qcfTConstraint() ){ - //a theory-specific predicate - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - flatten( n[i], beneathQuant ); + registerNode(n[0], false, pol, beneathQuant); + } + else if (options::qcfTConstraint()) + { + // a theory-specific predicate + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + flatten(n[i], beneathQuant); } } } @@ -215,7 +227,8 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) void QuantInfo::flatten( Node n, bool beneathQuant ) { Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl; - if( n.hasBoundVar() ){ + if (expr::hasBoundVar(n)) + { if( n.getKind()==BOUND_VARIABLE ){ d_inMatchConstraint[n] = true; } @@ -982,7 +995,8 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) } } }else{ - if( n.hasBoundVar() ){ + if (expr::hasBoundVar(n)) + { d_type_not = false; d_n = n; if( d_n.getKind()==NOT ){ @@ -1012,21 +1026,28 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) Assert( d_n.getType().isBoolean() ); d_type = typ_bool_var; }else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){ - for( unsigned i=0; i<d_n.getNumChildren(); i++ ){ - if( d_n[i].hasBoundVar() ){ - if( !qi->isVar( d_n[i] ) ){ - Trace("qcf-qregister-debug") << "ERROR : not var " << d_n[i] << std::endl; + for (unsigned i = 0; i < d_n.getNumChildren(); i++) + { + if (expr::hasBoundVar(d_n[i])) + { + if (!qi->isVar(d_n[i])) + { + Trace("qcf-qregister-debug") + << "ERROR : not var " << d_n[i] << std::endl; } - Assert( qi->isVar( d_n[i] ) ); - if( d_n.getKind()!=EQUAL && qi->isVar( d_n[i] ) ){ - d_qni_var_num[i+1] = qi->d_var_num[d_n[i]]; + Assert(qi->isVar(d_n[i])); + if (d_n.getKind() != EQUAL && qi->isVar(d_n[i])) + { + d_qni_var_num[i + 1] = qi->d_var_num[d_n[i]]; } - }else{ + } + else + { d_qni_gterm[i] = d_n[i]; - qi->setGroundSubterm( d_n[i] ); + qi->setGroundSubterm(d_n[i]); } } - d_type = d_n.getKind()==EQUAL ? typ_eq : typ_tconstraint; + d_type = d_n.getKind() == EQUAL ? typ_eq : typ_tconstraint; Trace("qcf-tconstraint") << "T-Constraint : " << d_n << std::endl; } } @@ -1180,12 +1201,17 @@ void MatchGen::reset_round( QuantConflictFind * p ) { } } }else if( d_type==typ_eq ){ - for( unsigned i=0; i<d_n.getNumChildren(); i++ ){ - if( !d_n[i].hasBoundVar() ){ - TNode t = p->getTermDatabase()->getEntailedTerm( d_n[i] ); - if( t.isNull() ){ + for (unsigned i = 0; i < d_n.getNumChildren(); i++) + { + if (!expr::hasBoundVar(d_n[i])) + { + TNode t = p->getTermDatabase()->getEntailedTerm(d_n[i]); + if (t.isNull()) + { d_ground_eval[i] = d_n[i]; - }else{ + } + else + { d_ground_eval[i] = t; } } @@ -1772,7 +1798,8 @@ Node MatchGen::getMatchOperator( QuantConflictFind * p, Node n ) { } bool MatchGen::isHandled( TNode n ) { - if( n.getKind()!=BOUND_VARIABLE && n.hasBoundVar() ){ + if (n.getKind() != BOUND_VARIABLE && expr::hasBoundVar(n)) + { if( !isHandledBoolConnective( n ) && !isHandledUfTerm( n ) && n.getKind()!=EQUAL && n.getKind()!=ITE ){ return false; } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 4799de09d..37451b776 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -14,14 +14,15 @@ #include "theory/quantifiers/quantifiers_rewriter.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/bv_inverter.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/ematching/trigger.h" using namespace std; using namespace CVC4::kind; @@ -774,9 +775,11 @@ bool QuantifiersRewriter::isConditionalVariableElim( Node n, int pol ){ } } }else if( n.getKind()==EQUAL ){ - for( unsigned i=0; i<2; i++ ){ - if( n[i].getKind()==BOUND_VARIABLE ){ - if (!n[1 - i].hasSubterm(n[i])) + for (unsigned i = 0; i < 2; i++) + { + if (n[i].getKind() == BOUND_VARIABLE) + { + if (!expr::hasSubterm(n[1 - i], n[i])) { return true; } @@ -874,8 +877,9 @@ Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){ return body; } -bool QuantifiersRewriter::isVariableElim( Node v, Node s ) { - return !s.hasSubterm(v) && s.getType().isSubtypeOf(v.getType()); +bool QuantifiersRewriter::isVariableElim(Node v, Node s) +{ + return !expr::hasSubterm(s, v) && s.getType().isSubtypeOf(v.getType()); } void QuantifiersRewriter::isVariableBoundElig( Node n, std::map< Node, int >& exclude, std::map< Node, std::map< int, bool > >& visited, bool hasPol, bool pol, @@ -1112,7 +1116,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Trace("var-elim-quant") << "Variable eliminate based on bit-vector inversion : " << var << " -> " << slv << std::endl; - Assert(!slv.hasSubterm(var)); + Assert(!expr::hasSubterm(slv, var)); Assert(slv.getType().isSubtypeOf(var.getType())); vars.push_back(var); subs.push_back(slv); diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 6a7eb8197..5f5a84a6b 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -14,6 +14,7 @@ **/ #include "theory/quantifiers/sygus/ce_guided_single_inv.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" @@ -726,12 +727,14 @@ void TransitionInference::getConstantSubstitution( std::vector< Node >& vars, st // check if it is a variable equality TNode v; Node s; - for( unsigned r=0; r<2; r++ ){ - if( std::find( vars.begin(), vars.end(), slit[r] )!=vars.end() ){ - if (!slit[1 - r].hasSubterm(slit[r])) + for (unsigned r = 0; r < 2; r++) + { + if (std::find(vars.begin(), vars.end(), slit[r]) != vars.end()) + { + if (!expr::hasSubterm(slit[1 - r], slit[r])) { v = slit[r]; - s = slit[1-r]; + s = slit[1 - r]; break; } } @@ -741,13 +744,18 @@ void TransitionInference::getConstantSubstitution( std::vector< Node >& vars, st std::map< Node, Node > msum; if (ArithMSum::getMonomialSumLit(slit, msum)) { - for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ - if( std::find( vars.begin(), vars.end(), itm->first )!=vars.end() ){ + for (std::map<Node, Node>::iterator itm = msum.begin(); + itm != msum.end(); + ++itm) + { + if (std::find(vars.begin(), vars.end(), itm->first) != vars.end()) + { Node veq_c; Node val; int ires = ArithMSum::isolate(itm->first, msum, veq_c, val, EQUAL); - if (ires != 0 && veq_c.isNull() && !val.hasSubterm(itm->first)) + if (ires != 0 && veq_c.isNull() + && !expr::hasSubterm(val, itm->first)) { v = itm->first; s = val; @@ -859,7 +867,8 @@ void TransitionInference::process( Node n ) { }else{ res = NodeManager::currentNM()->mkNode( kind::OR, disjuncts ); } - if( !res.hasBoundVar() ){ + if (!expr::hasBoundVar(res)) + { Trace("cegqi-inv") << "*** inferred " << ( comp_num==1 ? "pre" : ( comp_num==-1 ? "post" : "trans" ) ) << "-condition : " << res << std::endl; d_com[comp_num].d_conjuncts.push_back( res ); if( !const_var.empty() ){ @@ -1076,4 +1085,3 @@ Node TransitionInference::constructFormulaTrace( DetTrace& dt ) { } } //namespace CVC4 - 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 44835cc26..2ee120211 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -15,15 +15,16 @@ #include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h" #include "expr/datatype.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/sygus/ce_guided_instantiation.h" -#include "theory/quantifiers/sygus/ce_guided_single_inv.h" +#include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/sygus/ce_guided_instantiation.h" +#include "theory/quantifiers/sygus/ce_guided_single_inv.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" -#include "theory/quantifiers/ematching/trigger.h" #include "theory/theory_engine.h" using namespace CVC4::kind; @@ -294,11 +295,12 @@ bool CegConjectureSingleInvSol::getAssignEquality( Node eq, std::vector< Node >& Assert( std::find( vars.begin(), vars.end(), eq[r] )==vars.end() ); if( std::find( new_vars.begin(), new_vars.end(), eq[r] )==new_vars.end() ){ Node eqro = eq[r==0 ? 1 : 0 ]; - if (!eqro.hasSubterm(eq[r])) + if (!expr::hasSubterm(eqro, eq[r])) { - Trace("csi-simp-debug") << "---equality " << eq[r] << " = " << eqro << std::endl; - new_vars.push_back( eq[r] ); - new_subs.push_back( eqro ); + Trace("csi-simp-debug") + << "---equality " << eq[r] << " = " << eqro << std::endl; + new_vars.push_back(eq[r]); + new_subs.push_back(eqro); return true; } } diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index cf06dfa45..7d91e9812 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/term_util.h" #include "expr/datatype.h" +#include "expr/node_algorithm.h" #include "options/base_options.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" @@ -582,7 +583,7 @@ Node TermUtil::rewriteVtsSymbols( Node n ) { //rewriting infinity always takes precedence over rewriting delta for( unsigned r=0; r<2; r++ ){ Node inf = getVtsInfinityIndex( r, false, false ); - if (!inf.isNull() && n.hasSubterm(inf)) + if (!inf.isNull() && expr::hasSubterm(n, inf)) { if( rew_vts_inf.isNull() ){ rew_vts_inf = inf; @@ -595,16 +596,17 @@ Node TermUtil::rewriteVtsSymbols( Node n ) { subs_lhs.push_back( rew_vts_inf ); n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); n = Rewriter::rewrite( n ); - //may have cancelled - if (!n.hasSubterm(rew_vts_inf)) + // may have cancelled + if (!expr::hasSubterm(n, rew_vts_inf)) { rew_vts_inf = Node::null(); } } } } - if( rew_vts_inf.isNull() ){ - if (!d_vts_delta.isNull() && n.hasSubterm(d_vts_delta)) + if (rew_vts_inf.isNull()) + { + if (!d_vts_delta.isNull() && expr::hasSubterm(n, d_vts_delta)) { rew_delta = true; } |