From 60687e672ea8f485b4071e485b7b0cabc034fd00 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 15 Sep 2016 14:04:50 -0500 Subject: [PATCH] Make sep pto a trigger kind, track in equality engines and term database. --- src/theory/quantifiers/term_database.cpp | 2 +- src/theory/quantifiers/trigger.cpp | 3 ++- src/theory/sep/theory_sep.cpp | 17 ++++++++++------- 3 files changed, 13 insertions(+), 9 deletions(-) diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index e7b7268b5..a34ad116a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -129,7 +129,7 @@ Node TermDb::getMatchOperator( Node n ) { Kind k = n.getKind(); //datatype operators may be parametric, always assume they are if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || - k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ){ + k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==SEP_PTO ){ //since it is parametric, use a particular one as op TypeNode tn = n[0].getType(); Node op = n.getOperator(); diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 2faed3af0..d0bcd3a69 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -363,7 +363,8 @@ bool Trigger::isAtomicTrigger( Node n ){ bool Trigger::isAtomicTriggerKind( Kind k ) { return k==APPLY_UF || k==SELECT || k==STORE || k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || - k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON; + k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || + k==SEP_PTO; } bool Trigger::isRelationalTrigger( Node n ) { diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 7b4200db0..42c6d1219 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -442,13 +442,9 @@ void TheorySep::check(Effort e) { Trace("sep-assert") << "Done asserting " << atom << " to EE." << std::endl; }else if( s_atom.getKind()==kind::SEP_PTO ){ Node pto_lbl = NodeManager::currentNM()->mkNode( kind::SINGLETON, s_atom[0] ); - if( polarity && s_lbl!=pto_lbl ){ - //also propagate equality - Node eq = s_lbl.eqNode( pto_lbl ); - Trace("sep-assert") << "Asserting implied equality " << eq << " to EE..." << std::endl; - d_equalityEngine.assertEquality(eq, true, fact); - Trace("sep-assert") << "Done asserting implied equality " << eq << " to EE." << std::endl; - } + Assert( s_lbl==pto_lbl ); + Trace("sep-assert") << "Asserting " << s_atom << std::endl; + d_equalityEngine.assertPredicate(s_atom, polarity, fact); //associate the equivalence class of the lhs with this pto Node r = getRepresentative( s_lbl ); HeapAssertInfo * ei = getOrMakeEqcInfo( r, true ); @@ -1523,7 +1519,11 @@ void TheorySep::addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity ) Assert( areEqual( pb[1], p[1] ) ); std::vector< Node > exp; if( pb[1]!=p[1] ){ + //if( pb[1].getKind()==kind::SINGLETON && p[1].getKind()==kind::SINGLETON ){ + // exp.push_back( pb[1][0].eqNode( p[1][0] ) ); + //}else{ exp.push_back( pb[1].eqNode( p[1] ) ); + //} } exp.push_back( pb ); exp.push_back( p.negate() ); @@ -1535,6 +1535,8 @@ void TheorySep::addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity ) // conc.push_back( pb[1].eqNode( p[1] ).negate() ); //} Node n_conc = conc.empty() ? d_false : ( conc.size()==1 ? conc[0] : NodeManager::currentNM()->mkNode( kind::OR, conc ) ); + Trace("sep-pto") << "Conclusion is " << n_conc << std::endl; + // propagation for (pto x y) ^ ~(pto z w) ^ x = z => y != w sendLemma( exp, n_conc, "PTO_NEG_PROP" ); } }else{ @@ -1559,6 +1561,7 @@ void TheorySep::mergePto( Node p1, Node p2 ) { } exp.push_back( p1 ); exp.push_back( p2 ); + //enforces injectiveness of pto : (pto x y) ^ (pto y w) ^ x = y => y = w sendLemma( exp, p1[0][1].eqNode( p2[0][1] ), "PTO_PROP" ); } } -- 2.30.2