Move node algorithms to separate file (#2311)

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;