From: ajreynol <reynolds@laraserver2.epfl.ch>
Date: Mon, 16 Jun 2014 16:05:36 +0000 (+0200)
Subject: More proof support for CASC : include skolemization
X-Git-Tag: cvc5-1.0.0~6758^2~39
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c6d93155e795e5cce35f75d27766ae6c3d6c205c;p=cvc5.git

More proof support for CASC : include skolemization
---

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index e82fcd00d..383278f82 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -199,11 +199,11 @@ public:
   static void getBoundVars( Node n, std::vector< Node >& bvs);
 //for skolem
 private:
-  /** map from universal quantifiers to the list of skolem constants */
-  std::map< Node, std::vector< Node > > d_skolem_constants;
   /** map from universal quantifiers to their skolemized body */
   std::map< Node, Node > d_skolem_body;
 public:
+  /** map from universal quantifiers to the list of skolem constants */
+  std::map< Node, std::vector< Node > > d_skolem_constants;
   /** make the skolemized body f[e/x] */
   static Node mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs,
                                 std::vector< Node >& sk );
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 8335a084a..5d016fd06 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -150,23 +150,14 @@ Node TheoryQuantifiers::getNextDecisionRequest(){
 void TheoryQuantifiers::assertUniversal( Node n ){
   Assert( n.getKind()==FORALL );
   if( options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){
-    getQuantifiersEngine()->registerQuantifier( n );
-    getQuantifiersEngine()->assertNode( n );
+    getQuantifiersEngine()->assertQuantifier( n, true );
   }
 }
 
 void TheoryQuantifiers::assertExistential( Node n ){
   Assert( n.getKind()== NOT && n[0].getKind()==FORALL );
   if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n[0]) ){
-    if( d_skolemized.find( n )==d_skolemized.end() ){
-      Node body = getQuantifiersEngine()->getTermDatabase()->getSkolemizedBody( n[0] );
-      NodeBuilder<> nb(kind::OR);
-      nb << n[0] << body.notNode();
-      Node lem = nb;
-      Trace("quantifiers-sk") << "Skolemize lemma : " << lem << std::endl;
-      d_out->lemma( lem, false, true );
-      d_skolemized[n] = true;
-    }
+    getQuantifiersEngine()->assertQuantifier( n[0], false );
   }
 }
 
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 84b65cacd..5ce2e1a11 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -41,8 +41,6 @@ class InstantiationEngine;
 class TheoryQuantifiers : public Theory {
 private:
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
-  /** quantifiers that have been skolemized */
-  std::map< Node, bool > d_skolemized;
   /** number of instantiations */
   int d_numInstantiations;
   int d_baseDecLevel;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 66d8f9326..083137148 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -265,10 +265,31 @@ void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
   }
 }
 
-void QuantifiersEngine::assertNode( Node f ){
-  d_model->assertQuantifier( f );
-  for( int i=0; i<(int)d_modules.size(); i++ ){
-    d_modules[i]->assertNode( f );
+void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
+  if( !pol ){
+    //do skolemization
+    if( d_skolemized.find( f )==d_skolemized.end() ){
+      Node body = d_term_db->getSkolemizedBody( f );
+      NodeBuilder<> nb(kind::OR);
+      nb << f << body.notNode();
+      Node lem = nb;
+      if( Trace.isOn("quantifiers-sk") ){
+        Node slem = Rewriter::rewrite( lem );
+        Trace("quantifiers-sk") << "Skolemize lemma : " << slem << std::endl;
+      }
+      getOutputChannel().lemma( lem, false, true );
+      d_skolemized[f] = true;
+    }
+  }
+  //assert to modules TODO : handle !pol
+  if( pol ){
+    //register the quantifier
+    registerQuantifier( f );
+    //assert it to each module
+    d_model->assertQuantifier( f );
+    for( int i=0; i<(int)d_modules.size(); i++ ){
+      d_modules[i]->assertNode( f );
+    }
   }
 }
 
@@ -629,6 +650,16 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
 }
 
 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
+  for( std::map< Node, bool >::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){
+    out << "Skolem constants of " << it->first << " : " << std::endl;
+    out << "  ( ";
+    for( unsigned i=0; i<d_term_db->d_skolem_constants[it->first].size(); i++ ){
+      if( i>0 ){ out << ", "; }
+      out << d_term_db->d_skolem_constants[it->first][i];
+    }
+    out << " )" << std::endl;
+    out << std::endl;
+  }
   if( options::incrementalSolving() ){
     for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
       out << "Instantiations of " << it->first << " : " << std::endl;
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 999a716ba..19f8c55fb 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -125,6 +125,8 @@ private:
   /** list of all instantiations produced for each quantifier */
   std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
   std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie;
+  /** quantifiers that have been skolemized */
+  std::map< Node, bool > d_skolemized;
   /** term database */
   quantifiers::TermDb* d_term_db;
   /** all triggers will be stored in this trie */
@@ -179,7 +181,7 @@ public:
   /** register quantifier */
   void registerPattern( std::vector<Node> & pattern);
   /** assert universal quantifier */
-  void assertNode( Node f );
+  void assertQuantifier( Node q, bool pol );
   /** propagate */
   void propagate( Theory::Effort level );
   /** get next decision request */