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

1 files changed, 26 insertions, 0 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;
+  }
+}
+