Work on array pf signature, add working example. Add quantifiers proof signature. Ignore terms not in current master EE for QCF. Minor refactoring. Make --rewrite-rules true by default.

8 files changed, 42 insertions, 14 deletions

diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 1b34bc118..9b5e506ea 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -63,7 +63,7 @@ CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) :
   Assert( !d_op.isNull() );
 }
 void CandidateGeneratorQE::resetInstantiationRound(){
-  d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size();
+  d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms( d_op );
 }
 
 void CandidateGeneratorQE::reset( Node eqc ){
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 50a0084fc..a12fc7ca2 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -1039,7 +1039,7 @@ int QModelBuilderInstGen::getSelectionFormulaScore( Node fn ){
     if( fn.getKind()==APPLY_UF ){
       Node op = fn.getOperator();
       //return total number of terms
-      return d_qe->getTermDatabase()->d_op_count[op];
+      return d_qe->getTermDatabase()->d_op_nonred_count[op];
     }else{
       int score = 0;
       for( size_t i=0; i<fn.getNumChildren(); i++ ){
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 7ee416c4e..0865f2c0b 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -125,7 +125,7 @@ option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default
 option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h"
  when to invoke conflict find mechanism for quantifiers
 
-option quantRewriteRules --rewrite-rules bool :default false
+option quantRewriteRules --rewrite-rules bool :default true
  use rewrite rules module
 option rrOneInstPerRound --rr-one-inst-per-round bool :default false
  add one instance of rewrite rule per round
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 51d69ace4..c0b318f23 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2194,11 +2194,10 @@ void QuantConflictFind::computeArgReps( TNode n ) {
 void QuantConflictFind::computeUfTerms( TNode f ) {

   if( d_uf_terms.find( f )==d_uf_terms.end() ){

     d_uf_terms[f].clear();

-    unsigned nt = d_quantEngine->getTermDatabase()->d_op_map[f].size();

+    unsigned nt = d_quantEngine->getTermDatabase()->getNumGroundTerms( f );

     for( unsigned i=0; i<nt; i++ ){

       Node n = d_quantEngine->getTermDatabase()->d_op_map[f][i];

-      if( !n.getAttribute(NoMatchAttribute()) ){

-        Assert( getEqualityEngine()->hasTerm( n ) );

+      if( getEqualityEngine()->hasTerm( n ) && !n.getAttribute(NoMatchAttribute()) ){

         Node r = getRepresentative( n );

         computeArgReps( n );

         d_eqc_uf_terms[f].d_children[r].addTerm( n, d_arg_reps[n] );

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 20ab4e55f..914141995 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -111,7 +111,8 @@ void RelevantDomain::compute(){
     TermDb * db = d_qe->getTermDatabase();
     for( std::map< Node, std::vector< Node > >::iterator it = db->d_op_map.begin(); it != db->d_op_map.end(); ++it ){
       Node op = it->first;
-      for( unsigned i=0; i<it->second.size(); i++ ){
+      unsigned sz = db->getNumGroundTerms( op );
+      for( unsigned i=0; i<sz; i++ ){
         Node n = it->second[i];
         //if it is a non-redundant term
         if( !n.getAttribute(NoMatchAttribute()) ){
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 08a9f5d9f..ea1231e7a 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -46,6 +46,20 @@ bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){
   }
 }
 
+TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ) {
+
+}
+
+/** ground terms */
+unsigned TermDb::getNumGroundTerms( Node f ) {
+  std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f );
+  if( it!=d_op_map.end() ){
+    return it->second.size();
+  }else{
+    return 0;
+  }
+  //return d_op_ccount[f];
+}
 
 Node TermDb::getOperator( Node n ) {
   //return n.getOperator();
@@ -89,6 +103,15 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
         Trace("term-db") << "register term in db " << n << std::endl;
         //std::cout << "register trigger term " << n << std::endl;
         Node op = getOperator( n );
+        /*
+        int occ = d_op_ccount[op];
+        if( occ<(int)d_op_map[op].size() ){
+          d_op_map[op][occ] = n;
+        }else{
+          d_op_map[op].push_back( n );
+        }
+        d_op_ccount[op].set( occ + 1 );
+        */
         d_op_map[op].push_back( n );
         added.insert( n );
 
@@ -120,7 +143,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
    int alreadyCongruentCount = 0;
    //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
    for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
-     d_op_count[ it->first ] = 0;
+     d_op_nonred_count[ it->first ] = 0;
      if( !it->second.empty() ){
        if( it->second[0].getType().isBoolean() ){
          d_pred_map_trie[ 0 ][ it->first ].d_data.clear();
@@ -138,7 +161,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
                congruentCount++;
              }else{
                nonCongruentCount++;
-               d_op_count[ it->first ]++;
+               d_op_nonred_count[ it->first ]++;
              }
            }else{
              congruentCount++;
@@ -166,7 +189,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
                congruentCount++;
              }else{
                nonCongruentCount++;
-               d_op_count[ op ]++;
+               d_op_nonred_count[ op ]++;
              }
            }else{
              alreadyCongruentCount++;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index b3db6d266..41108bc2a 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -88,6 +88,7 @@ class TermDb {
   friend class ::CVC4::theory::inst::Trigger;
   friend class ::CVC4::theory::rrinst::Trigger;
   friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker;
+  typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
 private:
   /** reference to the quantifiers engine */
   QuantifiersEngine* d_quantEngine;
@@ -96,13 +97,17 @@ private:
 private:
   /** select op map */
   std::map< Node, std::map< TypeNode, std::map< TypeNode, Node > > > d_par_op_map;
+  /** count number of ground terms per operator (user-context dependent) */
+  NodeIntMap d_op_ccount;
 public:
-  TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
+  TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe );
   ~TermDb(){}
+  /** ground terms */
+  unsigned getNumGroundTerms( Node f );
+  /** count number of non-redundant ground terms per operator */
+  std::map< Node, int > d_op_nonred_count;
   /** map from APPLY_UF operators to ground terms for that operator */
   std::map< Node, std::vector< Node > > d_op_map;
-  /** count number of APPLY_UF terms per operator */
-  std::map< Node, int > d_op_count;
   /** map from APPLY_UF functions to trie */
   std::map< Node, TermArgTrie > d_func_map_trie;
   /** map from APPLY_UF predicates to trie */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 02423e54d..7fa61477f 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -45,7 +45,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext*
 d_te( te ),
 d_lemmas_produced_c(u){
   d_eq_query = new EqualityQueryQuantifiersEngine( this );
-  d_term_db = new quantifiers::TermDb( this );
+  d_term_db = new quantifiers::TermDb( c, u, this );
   d_tr_trie = new inst::TriggerTrie;
   //d_rr_tr_trie = new rrinst::TriggerTrie;
   //d_eem = new EfficientEMatcher( this );