summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/node.h4
-rw-r--r--src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp8
-rw-r--r--src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp2
-rw-r--r--src/theory/quantifiers/ematching/trigger.cpp4
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp9
-rw-r--r--src/theory/quantifiers/sygus/ce_guided_single_inv.cpp6
-rw-r--r--src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp3
-rw-r--r--src/theory/quantifiers/term_util.cpp53
-rw-r--r--src/theory/quantifiers/term_util.h3
-rw-r--r--test/regress/Makefile.tests1
-rw-r--r--test/regress/regress1/ho/hoa0008.smt268
11 files changed, 113 insertions, 48 deletions
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<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 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<catom.getNumChildren(); j++ ){
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
index c07ddcd8f..df04a743b 100644
--- 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 4039c632f..cb5afbfab 100644
--- 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 a8089d229..bb92cbaf7 100644
--- 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 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<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 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<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 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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback