diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-16 16:46:05 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-16 18:46:05 -0500 |
commit | 7fc04bf78c6c20f3711d14425469eef2e0c2cd60 (patch) | |
tree | d9f2e91a52406edf66967faccad550631cd9e4a5 /src/theory/quantifiers/cegqi | |
parent | 4e62cdade61514f268b96e78e2f82ad12dfcad07 (diff) |
Move node algorithms to separate file (#2311)
Diffstat (limited to 'src/theory/quantifiers/cegqi')
5 files changed, 12 insertions, 6 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; |