Fix hasSubterm calls for higher-order (#1760)

diff --git a/src/expr/node.h b/src/expr/node.h
index 14630bae10db0b5df78aea95a49d1193a644550b..de14723e67827586e6bea4997982060f7f285a32 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1539,6 +1539,10 @@ bool NodeTemplate<ref_count>::hasSubterm(NodeTemplate<false> t, bool strict) con
 
   for (unsigned i = 0; i < toProcess.size(); ++ i) {
     TNode current = toProcess[i];
+    if (current.hasOperator() && current.getOperator() == t)
+    {
+      return true;
+    }
     for(unsigned j = 0, j_end = current.getNumChildren(); j < j_end; ++ j) {
       TNode child = current[j];
       if (child == t) {

diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
index b526fb1ee99b3b09acdf8b58b002379174178575..a4599627d7894ba437df3627e7589d751121f970 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
@@ -156,7 +156,7 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No
         Trace("cegqi-arith-debug") << pv << " " << atom.getKind() << " " << val << std::endl;
       }
       // when not pure LIA/LRA, we must check whether the lhs contains pv
-      if (TermUtil::containsTerm(val, pv))
+      if (val.hasSubterm(pv))
       {
         Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl;
         return 0;
@@ -756,7 +756,8 @@ Node DtInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) {
   }
   if( !ret.isNull() ){
     //ensure does not contain
-    if( TermUtil::containsTerm( ret, v ) ){
+    if (ret.hasSubterm(v))
+    {
       ret = Node::null();
     }
   }
@@ -869,7 +870,8 @@ void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node cat
 }
 
 void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score ) {
-  if( inst::Trigger::isAtomicTrigger( catom ) && TermUtil::containsTerm( catom, pv ) ){
+  if (inst::Trigger::isAtomicTrigger(catom) && catom.hasSubterm(pv))
+  {
     Trace("cegqi-epr") << "Find matches for " << catom << "..." << std::endl;
     std::vector< Node > arg_reps;
     for( unsigned j=0; j<catom.getNumChildren(); j++ ){

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
index c07ddcd8fc03a8591d35248d817aa55c07afb9f7..df04a743b4b5ae6579e487213f64aa99f0d508bd 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
@@ -768,7 +768,7 @@ bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
         }
       }
       //only legal if current quantified formula contains n
-      return TermUtil::containsTerm( d_curr_quant, n );
+      return d_curr_quant.hasSubterm(n);
     }
   }else{
     return true;

diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 4039c632fc4d28abdea58f156d1a7bb9b06a80b9..cb5afbfabb12ee7c3cd11737b8e6679abc210b78 100644 (file)
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -300,7 +300,9 @@ bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) {
       }
     }
   }else if( isUsableAtomicTrigger( n1, q ) ){
-    if( options::relationalTriggers() && n2.getKind()==INST_CONSTANT && !quantifiers::TermUtil::containsTerm( n1, n2 ) ){
+    if (options::relationalTriggers() && n2.getKind() == INST_CONSTANT
+        && !n1.hasSubterm(n2))
+    {
       return true;
     }else if( !quantifiers::TermUtil::hasInstConstAttr(n2) ){
       return true;

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index a8089d2296131bec2212cb505fb1f9d332bc6bc6..bb92cbaf743350e42bbdde8604a7916858110252 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -776,7 +776,8 @@ 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( !TermUtil::containsTerm( n[1-i], n[i] ) ){
+        if (!n[1 - i].hasSubterm(n[i]))
+        {
           return true;
         }
       }
@@ -874,11 +875,7 @@ Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){
 }
 
 bool QuantifiersRewriter::isVariableElim( Node v, Node s ) {
-  if( TermUtil::containsTerm( s, v ) || !s.getType().isSubtypeOf( v.getType() ) ){
-    return false;
-  }else{
-    return true;
-  }
+  return !s.hasSubterm(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, 

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 0979e8b4eb3393e02bd07fa726c2574e3cf5ed3c..e10219fdd50351c8baa5cdf535af16c4cf01e63b 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -721,7 +721,8 @@ void TransitionInference::getConstantSubstitution( std::vector< Node >& vars, st
       Node s;
       for( unsigned r=0; r<2; r++ ){
         if( std::find( vars.begin(), vars.end(), slit[r] )!=vars.end() ){
-          if( !TermUtil::containsTerm( slit[1-r], slit[r] ) ){
+          if (!slit[1 - r].hasSubterm(slit[r]))
+          {
             v = slit[r];
             s = slit[1-r];
             break;
@@ -739,7 +740,8 @@ void TransitionInference::getConstantSubstitution( std::vector< Node >& vars, st
               Node val;
               int ires =
                   ArithMSum::isolate(itm->first, msum, veq_c, val, EQUAL);
-              if( ires!=0 && veq_c.isNull() && !TermUtil::containsTerm( val, itm->first ) ){
+              if (ires != 0 && veq_c.isNull() && !val.hasSubterm(itm->first))
+              {
                 v = itm->first;
                 s = val;
               }

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 f900297e5613f5465569626fc25e478826e4a4a0..c37c0a57a2af0cf8520c5231aab041fe16756b7b 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -294,7 +294,8 @@ 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( !d_qe->getTermUtil()->containsTerm( eqro, eq[r] ) ){
+        if (!eqro.hasSubterm(eq[r]))
+        {
           Trace("csi-simp-debug") << "---equality " << eq[r] << " = " << eqro << std::endl;
           new_vars.push_back( eq[r] );
           new_subs.push_back( eqro );

diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 5965906cbd04fef281031dc50ab589b48e0d76e1..9aa4561ce2e1c8bb31d6802d7d0360812b4472fb 100644 (file)
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -553,7 +553,8 @@ 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() && containsTerm( n, inf ) ){
+      if (!inf.isNull() && n.hasSubterm(inf))
+      {
         if( rew_vts_inf.isNull() ){
           rew_vts_inf = inf;
         }else{
@@ -566,14 +567,16 @@ Node TermUtil::rewriteVtsSymbols( Node n ) {
           n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() );
           n = Rewriter::rewrite( n );
           //may have cancelled
-          if( !containsTerm( n, rew_vts_inf ) ){
+          if (!n.hasSubterm(rew_vts_inf))
+          {
             rew_vts_inf = Node::null();
           }
         }
       }
     }
     if( rew_vts_inf.isNull() ){
-      if( !d_vts_delta.isNull() && containsTerm( n, d_vts_delta ) ){
+      if (!d_vts_delta.isNull() && n.hasSubterm(d_vts_delta))
+      {
         rew_delta = true;
       }
     }
@@ -690,43 +693,31 @@ Node TermUtil::ensureType( Node n, TypeNode tn ) {
   }
 }
 
-bool TermUtil::containsTerm2( Node n, Node t, std::map< Node, bool >& visited ) {
-  if( n==t ){
-    return true;
-  }else{
-    if( visited.find( n )==visited.end() ){
-      visited[n] = true;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        if( containsTerm2( n[i], t, visited ) ){
-          return true;
-        }
-      }
-    }
-    return false;
-  }
-}
-
 bool TermUtil::containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited ) {
-  if( visited.find( n )==visited.end() ){
+  if (visited.find(n) == visited.end())
+  {
     if( std::find( t.begin(), t.end(), n )!=t.end() ){
       return true;
-    }else{
-      visited[n] = true;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        if( containsTerms2( n[i], t, visited ) ){
-          return true;
-        }
+    }
+    visited[n] = true;
+    if (n.hasOperator())
+    {
+      if (containsTerms2(n.getOperator(), t, visited))
+      {
+        return true;
+      }
+    }
+    for (const Node& nc : n)
+    {
+      if (containsTerms2(nc, t, visited))
+      {
+        return true;
       }
     }
   }
   return false;
 }
 
-bool TermUtil::containsTerm( Node n, Node t ) {
-  std::map< Node, bool > visited;
-  return containsTerm2( n, t, visited );
-}
-
 bool TermUtil::containsTerms( Node n, std::vector< Node >& t ) {
   if( t.empty() ){
     return false;

diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 97f4edcd5cfa735cff0692a7b4e9c6d0c80c3c0f..6b83ad639fc1ed5fd1795d5fc25729ddbc9fc402 100644 (file)
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -254,7 +254,6 @@ public:
   // TODO #1216 : promote these?
  private:
   //helper for contains term
-  static bool containsTerm2( Node n, Node t, std::map< Node, bool >& visited );
   static bool containsTerms2( Node n, std::vector< Node >& t, std::map< Node, bool >& visited );
   /** cache for getTypeValue */
   std::unordered_map<TypeNode,
@@ -279,8 +278,6 @@ public:
       d_type_value_offset_status;
 
  public:
-  /** simple check for whether n contains t as subterm */
-  static bool containsTerm( Node n, Node t );
   /** simple check for contains term, true if contains at least one term in t */
   static bool containsTerms( Node n, std::vector< Node >& t );
   /** contains uninterpreted constant */

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 8f5b9bf4f7b724fb3f38d8636f51d824711ade96..46d85615643daafb35eccf6df70540f281e92448 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1080,6 +1080,7 @@ REG1_TESTS = \
        regress1/ho/auth0068.smt2 \
        regress1/ho/fta0210.smt2 \
        regress1/ho/fta0409.smt2 \
+       regress1/ho/hoa0008.smt2 \
        regress1/ho/ho-exponential-model.smt2 \
        regress1/ho/ho-matching-enum-2.smt2 \
        regress1/ho/ho-std-fmf.smt2 \

diff --git a/test/regress/regress1/ho/hoa0008.smt2 b/test/regress/regress1/ho/hoa0008.smt2
new file mode 100644 (file)
index 0000000..f4833aa
--- /dev/null
+++ b/test/regress/regress1/ho/hoa0008.smt2
@@ -0,0 +1,68 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort A$ 0)
+(declare-sort Com$ 0)
+(declare-sort Loc$ 0)
+(declare-sort Nat$ 0)
+(declare-sort Pname$ 0)
+(declare-sort State$ 0)
+(declare-sort Vname$ 0)
+(declare-sort Literal$ 0)
+(declare-sort Natural$ 0)
+(declare-sort Typerep$ 0)
+(declare-sort A_triple$ 0)
+(declare-sort Com_option$ 0)
+(declare-fun p$ () (-> A$ (-> State$ Bool)))
+(declare-fun q$ () (-> A$ (-> State$ Bool)))
+(declare-fun pn$ () Pname$)
+(declare-fun wt$ (Com$) Bool)
+(declare-fun ass$ (Vname$ (-> State$ Nat$)) Com$)
+(declare-fun suc$ (Nat$) Nat$)
+(declare-fun the$ (Com_option$) Com$)
+(declare-fun body$ (Pname$) Com$)
+(declare-fun call$ (Vname$ Pname$ (-> State$ Nat$)) Com$)
+(declare-fun cond$ ((-> State$ Bool) Com$ Com$) Com$)
+(declare-fun none$ () Com_option$)
+(declare-fun plus$ (Nat$ Nat$) Nat$)
+(declare-fun semi$ (Com$ Com$) Com$)
+(declare-fun size$ (A_triple$) Nat$)
+(declare-fun skip$ () Com$)
+(declare-fun some$ (Com$) Com_option$)
+(declare-fun suc$a (Natural$) Natural$)
+(declare-fun zero$ () Nat$)
+(declare-fun body$a (Pname$) Com_option$)
+(declare-fun evalc$ (Com$ State$ State$) Bool)
+(declare-fun evaln$ (Com$ State$ Nat$ State$) Bool)
+(declare-fun local$ (Loc$ (-> State$ Nat$) Com$) Com$)
+(declare-fun plus$a (Natural$ Natural$) Natural$)
+(declare-fun size$a (Com$) Nat$)
+(declare-fun size$b (Natural$) Nat$)
+(declare-fun size$c (Bool) Nat$)
+(declare-fun size$d (Com_option$) Nat$)
+(declare-fun size$e (Typerep$) Nat$)
+(declare-fun size$f (Literal$) Nat$)
+(declare-fun while$ ((-> State$ Bool) Com$) Com$)
+(declare-fun zero$a () Natural$)
+(declare-fun triple$ ((-> A$ (-> State$ Bool)) Com$ (-> A$ (-> State$ Bool))) A_triple$)
+(declare-fun rec_bool$ (Nat$ Nat$) (-> Bool Nat$))
+(declare-fun size_com$ (Com$) Nat$)
+(declare-fun size_bool$ (Bool) Nat$)
+(declare-fun wT_bodies$ () Bool)
+(declare-fun size_option$ ((-> Com$ Nat$)) (-> Com_option$ Nat$))
+(declare-fun size_triple$ ((-> A$ Nat$) A_triple$) Nat$)
+(declare-fun size_natural$ (Natural$) Nat$)
+(declare-fun triple_valid$ (Nat$ A_triple$) Bool)
+(assert (! (not (triple_valid$ zero$ (triple$ p$ (body$ pn$) q$))) :named a0))
+
+(assert (! (forall ((?v0 Nat$) (?v1 (-> A$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> A$ (-> State$ Bool)))) (= (triple_valid$ ?v0 (triple$ ?v1 ?v2 ?v3)) (forall ((?v4 A$) (?v5 State$)) (=> (?v1 ?v4 ?v5) (forall ((?v6 State$)) (=> (evaln$ ?v2 ?v5 ?v0 ?v6) (?v3 ?v4 ?v6))))))) :named a6))
+
+(assert (! (= (size_bool$ true) zero$) :named a13))
+(assert (! (= size_bool$ (rec_bool$ zero$ zero$)) :named a14))
+
+(assert (! (forall ((?v0 Nat$)) (not (= zero$ (suc$ ?v0)))) :named a37))
+
+(assert (! (forall ((?v0 Pname$) (?v1 State$) (?v2 Nat$) (?v3 State$)) (=> (and (evaln$ (body$ ?v0) ?v1 ?v2 ?v3) (forall ((?v4 Nat$)) (=> (and (= ?v2 (suc$ ?v4)) (evaln$ (the$ (body$a ?v0)) ?v1 ?v4 ?v3)) false))) false)) :named a204))
+
+(check-sat)
+;(get-proof)