Eager introduction of eqc, lemma cache for ground fmf. Apply preprocessing to quantifier instantiations.

6 files changed, 81 insertions, 29 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 850b37fe0..deb9770c0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3895,14 +3895,11 @@ void SmtEnginePrivate::processAssertions() {
       //apply pre-skolemization to existential quantifiers
       for (unsigned i = 0; i < d_assertions.size(); ++ i) {
         Node prev = d_assertions[i];
-        Trace("quantifiers-rewrite-debug") << "Pre-skolemize " << prev << "..." << std::endl;
-        vector< TypeNode > fvTypes;
-        vector< TNode > fvs;
-        d_assertions.replace(i, quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ));
-        if( prev!=d_assertions[i] ){
-          d_assertions.replace(i, Rewriter::rewrite( d_assertions[i] ));
-          Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl;
-          Trace("quantifiers-rewrite") << "   ...got " << d_assertions[i] << endl;
+        Node next = quantifiers::QuantifiersRewriter::preprocess( prev );
+        if( next!=prev ){
+          d_assertions.replace(i, Rewriter::rewrite( next ));
+          Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl;
+          Trace("quantifiers-preprocess") << "   ...got " << d_assertions[i] << endl;
         }
       }
     }
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index fc5b692b2..462f8377f 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1737,6 +1737,18 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
   return n;
 }
 
+Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
+  if( options::preSkolemQuant() ){
+    if( !isInst || !options::preSkolemQuantNested() ){
+      //apply pre-skolemization to existential quantifiers
+      Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl;
+      std::vector< TypeNode > fvTypes;
+      std::vector< TNode > fvs;
+      n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( n, true, fvTypes, fvs );
+    }
+  }
+  return n;
+}
 
 Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term,
                                           std::map< Node, std::vector< int > >& var_parent, int parentId ){
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 38c1bdd58..47997f9a7 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -91,10 +91,12 @@ public:
 private:
   /** options */
   static bool doOperation( Node f, bool isNested, int computeOption );
+private:
+  static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
 public:
   static Node rewriteRewriteRule( Node r );
   static bool containsQuantifiers(Node n);
-  static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
+  static Node preprocess( Node n, bool isInst = false );
 };/* class QuantifiersRewriter */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 19d66165a..6fedc14f0 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -695,6 +695,8 @@ bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& v
     Trace("quant-vts-debug") << "            ...result: " << body_r << std::endl;
     body = body_r;
   }
+  body = quantifiers::QuantifiersRewriter::preprocess( body, true );
+  Trace("inst-debug") << "...preprocess to " << body << std::endl;
   Trace("inst-assert") << "(assert " << body << ")" << std::endl;
   //make the lemma
   Node lem = NodeManager::currentNM()->mkNode( kind::OR, f.negate(), body );
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 9fceedc96..3ed1c4d40 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -26,6 +26,7 @@
 //#define ONE_SPLIT_REGION
 //#define DISABLE_QUICK_CLIQUE_CHECKS
 //#define COMBINE_REGIONS_SMALL_INTO_LARGE
+//#define LAZY_REL_EQC
 
 using namespace std;
 using namespace CVC4;
@@ -406,7 +407,7 @@ void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool in
 StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ) : d_type( n.getType() ),
           d_thss( thss ), d_regions_index( c, 0 ), d_regions_map( c ), d_split_score( c ), d_disequalities_index( c, 0 ),
           d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( u, 0 ),
-          d_cardinality_assertions( c ), d_hasCard( c, false ), d_maxNegCard( c, 0 ), d_initialized( u, false ){
+          d_cardinality_assertions( c ), d_hasCard( c, false ), d_maxNegCard( c, 0 ), d_initialized( u, false ), d_lemma_cache( u ){
   d_cardinality_term = n;
   //if( d_type.isSort() ){
   //  TypeEnumerator te(tn);
@@ -1070,11 +1071,12 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){
     //add splitting lemma for cardinality constraint
     Assert( !d_cardinality_term.isNull() );
     Node lem = getCardinalityLiteral( d_aloc_cardinality );
-    Trace("uf-ss-lemma") << "*** Cardinality split on : " << lem << std::endl;
     lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() );
     d_cardinality_lemma[ d_aloc_cardinality ] = lem;
     //add as lemma to output channel
-    out->lemma( lem );
+    if( doSendLemma( lem ) ){
+      Trace("uf-ss-lemma") << "*** Cardinality split on : " << lem << std::endl;
+    }
     //require phase
     out->requirePhase( d_cardinality_literal[ d_aloc_cardinality ], true );
     //add the appropriate lemma, propagate as decision
@@ -1121,7 +1123,6 @@ int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
   if (!s.isNull() ){
     //add lemma to output channel
     Assert( s.getKind()==EQUAL );
-    Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
     Node ss = Rewriter::rewrite( s );
     if( ss.getKind()!=EQUAL ){
       Node b_t = NodeManager::currentNM()->mkConst( true );
@@ -1150,10 +1151,13 @@ int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
     //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl;
     //Notice() << "*** Split on " << s << std::endl;
     //split on the equality s
-    out->split( ss );
-    //tell the sat solver to explore the equals branch first
-    out->requirePhase( ss, true );
-    ++( d_thss->d_statistics.d_split_lemmas );
+    Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() );
+    if( doSendLemma( lem ) ){
+      Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
+      //tell the sat solver to explore the equals branch first
+      out->requirePhase( ss, true );
+      ++( d_thss->d_statistics.d_split_lemmas );
+    }
     return 1;
   }else{
     return 0;
@@ -1185,9 +1189,10 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu
     }
     eqs.push_back( d_cardinality_literal[ d_cardinality ].notNode() );
     Node lem = NodeManager::currentNM()->mkNode( OR, eqs );
-    Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
-    ++( d_thss->d_statistics.d_clique_lemmas );
-    out->lemma( lem );
+    if( doSendLemma( lem ) ){
+      Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
+      ++( d_thss->d_statistics.d_clique_lemmas );
+    }
   }else{
     //found a clique
     Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl;
@@ -1303,9 +1308,10 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu
       //Assert( hasValue );
       //Assert( value );
       conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() );
-      Trace("uf-ss-lemma") << "*** Add clique lemma " << conflictNode << std::endl;
-      out->lemma( conflictNode );
-      ++( d_thss->d_statistics.d_clique_lemmas );
+      if( doSendLemma( conflictNode ) ){
+        Trace("uf-ss-lemma") << "*** Add clique lemma " << conflictNode << std::endl;
+        ++( d_thss->d_statistics.d_clique_lemmas );
+      }
     }
 
     //DO_THIS: ensure that the same clique is not reported???  Check standard effort after assertDisequal can produce same clique.
@@ -1364,10 +1370,9 @@ void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality,
 }
 
 void StrongSolverTheoryUF::SortModel::addClique( int c, std::vector< Node >& clique ) {
-
-  if( d_clique_trie[c].add( clique ) ){
-    d_cliques[ c ].push_back( clique );
-  }
+  //if( d_clique_trie[c].add( clique ) ){
+  //  d_cliques[ c ].push_back( clique );
+  //}
 }
 
 
@@ -1395,6 +1400,16 @@ void StrongSolverTheoryUF::SortModel::simpleCheckCardinality() {
   }
 }
 
+bool StrongSolverTheoryUF::SortModel::doSendLemma( Node lem ) {
+  if( d_lemma_cache.find( lem )==d_lemma_cache.end() ){
+    d_lemma_cache[lem] = true;
+    d_thss->getOutputChannel().lemma( lem );
+    return true;
+  }else{
+    return false;
+  }
+}
+
 void StrongSolverTheoryUF::SortModel::debugPrint( const char* c ){
   Debug( c ) << "--  Conflict Find:" << std::endl;
   Debug( c ) << "Number of reps = " << d_reps << std::endl;
@@ -1568,10 +1583,19 @@ bool StrongSolverTheoryUF::hasEqc( Node a ) {
 }
 
 /** new node */
-void StrongSolverTheoryUF::newEqClass( Node n ){
-  SortModel* c = getSortModel( n );
+void StrongSolverTheoryUF::newEqClass( Node a ){
+  SortModel* c = getSortModel( a );
   if( c ){
+#ifdef LAZY_REL_EQC
     //do nothing
+#else
+    Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl;
+    c->newEqClass( a );
+    if( options::ufssSymBreak() ){
+      d_sym_break->newEqClass( a );
+    }
+    Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl;
+#endif
   }
 }
 
@@ -1580,6 +1604,7 @@ void StrongSolverTheoryUF::merge( Node a, Node b ){
   //TODO: ensure they are relevant
   SortModel* c = getSortModel( a );
   if( c ){
+#ifdef LAZY_REL_EQC
     ensureEqc( c, a );
     if( hasEqc( b ) ){
       Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl;
@@ -1589,6 +1614,11 @@ void StrongSolverTheoryUF::merge( Node a, Node b ){
       //c->assignEqClass( b, a );
       d_rel_eqc[b] = true;
     }
+#else
+    Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl;
+    c->merge( a, b );
+    Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Merge." << std::endl;
+#endif
   }else{
     if( options::ufssDiseqPropagation() ){
       d_deq_prop->merge(a, b);
@@ -1600,8 +1630,10 @@ void StrongSolverTheoryUF::merge( Node a, Node b ){
 void StrongSolverTheoryUF::assertDisequal( Node a, Node b, Node reason ){
   SortModel* c = getSortModel( a );
   if( c ){
+#ifdef LAZY_REL_EQC
     ensureEqc( c, a );
     ensureEqc( c, b );
+#endif
     Trace("uf-ss-solver") << "StrongSolverTheoryUF: Assert disequal " << a << " " << b << " : " << a.getType() << std::endl;
     //Assert( d_th->d_equalityEngine.getRepresentative( a )==a );
     //Assert( d_th->d_equalityEngine.getRepresentative( b )==b );
@@ -1617,7 +1649,9 @@ void StrongSolverTheoryUF::assertDisequal( Node a, Node b, Node reason ){
 /** assert a node */
 void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){
   Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl;
+#ifdef LAZY_REL_EQC
   ensureEqcRec( n );
+#endif
   bool polarity = n.getKind() != kind::NOT;
   TNode lit = polarity ? n : n[0];
   if( lit.getKind()==CARDINALITY_CONSTRAINT ){
@@ -2042,6 +2076,7 @@ void StrongSolverTheoryUF::allocateCombinedCardinality() {
   d_com_card_literal[ d_aloc_com_card.get() ] = lem;
   lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() );
   //add as lemma to output channel
+  Trace("uf-ss-lemma") << "*** Combined cardinality split : " << lem << std::endl;
   getOutputChannel().lemma( lem );
   //require phase
   getOutputChannel().requirePhase( d_com_card_literal[ d_aloc_com_card.get() ], true );
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 24d7f840f..db4c50423 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -244,6 +244,8 @@ public:
     std::vector< Node > d_fresh_aloc_reps;
     /** whether we are initialized */
     context::CDO< bool > d_initialized;
+    /** cache for lemmas */
+    NodeBoolMap d_lemma_cache;
   private:
     /** apply totality */
     bool applyTotality( int cardinality );
@@ -251,6 +253,8 @@ public:
     Node getTotalityLemmaTerm( int cardinality, int i );
     /** simple check cardinality */
     void simpleCheckCardinality();
+  private:
+    bool doSendLemma( Node lem );
   public:
     SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss );
     virtual ~SortModel(){}