From f2f1e2312d0dd98e89fef63d6595234e27ba5b3a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 9 Apr 2018 21:18:19 -0500 Subject: [PATCH] Fix hasSubterm calls for higher-order (#1760) --- src/expr/node.h | 4 ++ .../quantifiers/cegqi/ceg_t_instantiator.cpp | 8 ++- .../quantifiers/cegqi/inst_strategy_cbqi.cpp | 2 +- src/theory/quantifiers/ematching/trigger.cpp | 4 +- .../quantifiers/quantifiers_rewriter.cpp | 9 +-- .../sygus/ce_guided_single_inv.cpp | 6 +- .../sygus/ce_guided_single_inv_sol.cpp | 3 +- src/theory/quantifiers/term_util.cpp | 53 ++++++--------- src/theory/quantifiers/term_util.h | 3 - test/regress/Makefile.tests | 1 + test/regress/regress1/ho/hoa0008.smt2 | 68 +++++++++++++++++++ 11 files changed, 113 insertions(+), 48 deletions(-) create mode 100644 test/regress/regress1/ho/hoa0008.smt2 diff --git a/src/expr/node.h b/src/expr/node.h index 14630bae1..de14723e6 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -1539,6 +1539,10 @@ bool NodeTemplate::hasSubterm(NodeTemplate 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 b526fb1ee..a4599627d 100644 --- 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& 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 0979e8b4e..e10219fdd 100644 --- 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 f900297e5..c37c0a57a 100644 --- 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 5965906cb..9aa4561ce 100644 --- 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& 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 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 97f4edcd5..6b83ad639 100644 --- 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& t ); /** contains uninterpreted constant */ diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 8f5b9bf4f..46d856156 100644 --- 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 index 000000000..f4833aadf --- /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) -- 2.30.2