Merge branch 'origin' of https://github.com/CVC4/CVC4.git

Conflicts:
	src/options/quantifiers_options

1 files changed, 104 insertions, 0 deletions

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index b9aab0236..f4284a8ab 100755
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -419,3 +419,107 @@ void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol,
   }
 }
 
+void QuantEPR::registerNode( Node n, std::map< int, std::map< Node, bool > >& visited, bool beneathQuant, bool hasPol, bool pol ) {
+  int vindex = hasPol ? ( pol ? 1 : -1 ) : 0;
+  if( visited[vindex].find( n )==visited[vindex].end() ){
+    visited[vindex][n] = true;
+    Trace("quant-epr-debug") << "QuantEPR::registerNode " << n << std::endl;
+    if( n.getKind()==FORALL ){
+      if( beneathQuant || !hasPol || !pol ){
+        for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+          TypeNode tn = n[0][i].getType();
+          if( d_non_epr.find( tn )==d_non_epr.end() ){
+            Trace("quant-epr") << "Sort " << tn << " is non-EPR because of nested or possible existential quantification." << std::endl;
+            d_non_epr[tn] = true;
+          }
+        }
+      }else{
+        beneathQuant = true;
+      }
+    }
+    TypeNode tn = n.getType();
+    
+    if( n.getNumChildren()>0 ){
+      if( tn.isSort() ){
+        if( d_non_epr.find( tn )==d_non_epr.end() ){
+          Trace("quant-epr") << "Sort " << tn << " is non-EPR because of " << n << std::endl;
+          d_non_epr[tn] = true;
+        }
+      }
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        bool newHasPol;
+        bool newPol;
+        QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
+        registerNode( n[i], visited, beneathQuant, newHasPol, newPol );
+      }
+    }else if( tn.isSort() ){
+      if( n.getKind()==BOUND_VARIABLE ){
+        if( d_consts.find( tn )==d_consts.end() ){
+          //mark that at least one constant must occur
+          d_consts[tn].clear();
+        }
+      }else if( std::find( d_consts[tn].begin(), d_consts[tn].end(), n )==d_consts[tn].end() ){
+        d_consts[tn].push_back( n );
+        Trace("quant-epr") << "...constant of type " << tn << " : " << n << std::endl;
+      }
+    }
+  }
+}
+
+void QuantEPR::registerAssertion( Node assertion ) {
+  std::map< int, std::map< Node, bool > > visited;
+  registerNode( assertion, visited, false, true, true );
+}
+
+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;
+      it->second.clear();
+    }else{
+      Trace("quant-epr-debug") << "...epr, #consts = " << it->second.size() << std::endl;
+      if( it->second.empty() ){
+        it->second.push_back( NodeManager::currentNM()->mkSkolem( "e", it->first, "EPR base constant" ) );
+      }
+      if( Trace.isOn("quant-epr") ){
+        Trace("quant-epr") << "Type " << it->first << " is EPR, with constants : " << std::endl;
+        for( unsigned i=0; i<it->second.size(); i++ ){
+          Trace("quant-epr") << "  " << it->second[i] << std::endl;
+        }
+      }
+    }
+  }
+}
+
+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;
+  }
+}
+