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

2 files changed, 35 insertions, 1 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(); }
 };
 
 }