Make sep pto a trigger kind, track in equality engines and term database.

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" );
   }
 }