Lemma cache in theory sep. Minor optimization for sets. Minor improvements to EPR

7 files changed, 76 insertions, 17 deletions

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 9158734e4..c3ddfacff 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -474,6 +474,7 @@ void QuantEPR::registerAssertion( Node assertion ) {
 void QuantEPR::finishInit() {
   Trace("quant-epr-debug") << "QuantEPR::finishInit" << std::endl;
   for( std::map< TypeNode, std::vector< Node > >::iterator it = d_consts.begin(); it != d_consts.end(); ++it ){
+    Assert( d_epr_axiom.find( it->first )==d_epr_axiom.end() );
     Trace("quant-epr-debug") << "process " << it->first << std::endl;
     if( d_non_epr.find( it->first )!=d_non_epr.end() ){
       Trace("quant-epr-debug") << "...non-epr" << std::endl;
@@ -497,3 +498,28 @@ bool QuantEPR::isEPRConstant( TypeNode tn, Node k ) {
   return std::find( d_consts[tn].begin(), d_consts[tn].end(), k )!=d_consts[tn].end();
 }
 
+void QuantEPR::addEPRConstant( TypeNode tn, Node k ) {
+  Assert( isEPR( tn ) );
+  Assert( d_epr_axiom.find( tn )==d_epr_axiom.end() );
+  if( !isEPRConstant( tn, k ) ){
+    d_consts[tn].push_back( k );
+  }
+}
+
+Node QuantEPR::mkEPRAxiom( TypeNode tn ) {
+  Assert( isEPR( tn ) );
+  std::map< TypeNode, Node >::iterator ita = d_epr_axiom.find( tn );
+  if( ita==d_epr_axiom.end() ){
+    std::vector< Node > disj;
+    Node x = NodeManager::currentNM()->mkBoundVar( tn );
+    for( unsigned i=0; i<d_consts[tn].size(); i++ ){
+      disj.push_back( NodeManager::currentNM()->mkNode( tn.isBoolean() ? IFF : EQUAL, x, d_consts[tn][i] ) );
+    }
+    Assert( !disj.empty() );
+    d_epr_axiom[tn] = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ), disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ) );
+    return d_epr_axiom[tn];
+  }else{
+    return ita->second;
+  }
+}
+
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 049644ffb..d8e57b1ca 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -177,6 +177,8 @@ private:
   void registerNode( Node n, std::map< int, std::map< Node, bool > >& visited, bool beneathQuant, bool hasPol, bool pol );
   /** non-epr */
   std::map< TypeNode, bool > d_non_epr;
+  /** axioms for epr */
+  std::map< TypeNode, Node > d_epr_axiom;
 public:
   QuantEPR(){}
   virtual ~QuantEPR(){}
@@ -191,9 +193,15 @@ public:
   /** finish init */
   void finishInit();
   /** is EPR */
-  bool isEPR( TypeNode tn ) { return d_non_epr.find( tn )!=d_non_epr.end() ? false : true; }
+  bool isEPR( TypeNode tn ) const { return d_non_epr.find( tn )==d_non_epr.end(); }
   /** is EPR constant */
   bool isEPRConstant( TypeNode tn, Node k ); 
+  /** add EPR constant */
+  void addEPRConstant( TypeNode tn, Node k ); 
+  /** get EPR axiom */
+  Node mkEPRAxiom( TypeNode tn );
+  /** has EPR axiom */
+  bool hasEPRAxiom( TypeNode tn ) const { return d_epr_axiom.find( tn )!=d_epr_axiom.end(); }
 };
 
 }
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 5b50526c4..e48c6eafe 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1246,6 +1246,18 @@ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool
   return addSplit( fm );
 }
 
+bool QuantifiersEngine::addEPRAxiom( TypeNode tn ) {
+  if( d_qepr ){
+    Assert( !options::incrementalSolving() );
+    if( d_qepr->isEPR( tn ) && !d_qepr->hasEPRAxiom( tn ) ){
+      Node lem = d_qepr->mkEPRAxiom( tn );
+      Trace("quant-epr") << "EPR lemma for " << tn << " : " << lem << std::endl;
+      getOutputChannel().lemma( lem );
+    }
+  }
+  return false;
+}
+  
 void QuantifiersEngine::markRelevant( Node q ) {
   d_model->markRelevant( q );
 }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index bcc33327e..25542e49e 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -333,6 +333,8 @@ public:
   bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
   /** add split equality */
   bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true );
+  /** add EPR axiom */
+  bool addEPRAxiom( TypeNode tn );
   /** mark relevant quantified formula, this will indicate it should be checked before the others */
   void markRelevant( Node q );
   /** has added lemma */
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index e96badfd3..7ee5a1b73 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -36,6 +36,7 @@ namespace sep {
 
 TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
   Theory(THEORY_SEP, c, u, out, valuation, logicInfo),
+  d_lemmas_produced_c(u),
   d_notify(*this),
   d_equalityEngine(d_notify, c, "theory::sep::TheorySep", true),
   d_conflict(c, false),
@@ -1025,14 +1026,14 @@ void TheorySep::initializeBounds() {
         d_type_ref_card_id[e] = r;
         //must include this constant back into EPR handling
         if( qepr && qepr->isEPR( tn ) ){
-          qepr->d_consts[tn].push_back( e );
+          qepr->addEPRConstant( tn, e );
         }
       }
       //EPR must include nil ref    
       if( qepr && qepr->isEPR( tn ) ){
         Node nr = getNilRef( tn );
         if( !qepr->isEPRConstant( tn, nr ) ){
-          qepr->d_consts[tn].push_back( nr );
+          qepr->addEPRConstant( tn, nr );
         }
       }      
     }
@@ -1530,9 +1531,9 @@ void TheorySep::addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity )
       if( pb[0][1]!=p[0][1] ){
         conc.push_back( pb[0][1].eqNode( p[0][1] ).negate() );
       }
-      if( pb[1]!=p[1] ){
-        conc.push_back( pb[1].eqNode( p[1] ).negate() );
-      }
+      //if( pb[1]!=p[1] ){
+      //  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 ) );
       sendLemma( exp, n_conc, "PTO_NEG_PROP" );
     }
@@ -1631,8 +1632,11 @@ void TheorySep::doPendingFacts() {
       }
       int index = d_pending_lem[i];
       Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, d_pending_exp[index], d_pending[index] );
-      d_out->lemma( lem );
-      Trace("sep-pending") << "Sep : Lemma : " << lem << std::endl;
+      if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
+        d_lemmas_produced_c.insert( lem );
+        d_out->lemma( lem );
+        Trace("sep-pending") << "Sep : Lemma : " << lem << std::endl;
+      }
     }
   }
   d_pending_exp.clear();
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 1ca78801b..982fc3c70 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -44,6 +44,8 @@ class TheorySep : public Theory {
   /////////////////////////////////////////////////////////////////////////////
 
   private:
+  /** all lemmas sent */
+  NodeSet d_lemmas_produced_c;
 
   /** True node for predicates = true */
   Node d_true;
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index dbe94ff4b..ec6bb7fcd 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1249,15 +1249,20 @@ Node TheorySetsPrivate::getLemma() {
 
     Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet());
     TypeNode elementType = n[0].getType().getSetElementType();
-    Node x = NodeManager::currentNM()->mkSkolem("sde_",  elementType);
-    Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]);
-
-    if(n[0].getKind() == kind::EMPTYSET) {
-      lemma = OR(n, l2);
-    } else if(n[1].getKind() == kind::EMPTYSET) {
-      lemma = OR(n, l1);
-    } else {
-      lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2));
+    // { x } != { y } => x != y
+    if( n[0].getKind()==kind::SINGLETON && n[1].getKind()==kind::SINGLETON ){
+      lemma = OR(n, NodeManager::currentNM()->mkNode( elementType.isBoolean() ? kind::IFF : kind::EQUAL, n[0][0], n[1][0] ).negate() );
+    }else{
+      Node x = NodeManager::currentNM()->mkSkolem("sde_",  elementType);
+      Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]);
+
+      if(n[0].getKind() == kind::EMPTYSET) {
+        lemma = OR(n, l2);
+      } else if(n[1].getKind() == kind::EMPTYSET) {
+        lemma = OR(n, l1);
+      } else {
+        lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2));
+      }
     }
   }