Avoid completion for large finite types. Fix bug for --fmf-fun.

6 files changed, 47 insertions, 16 deletions

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index c10f1db53..2c65b62b3 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -313,12 +313,11 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int
 }
 
 void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
-  Assert( n.getKind()!=IMPLIES && n.getKind()!=XOR );
   newHasPol = hasPol;
   newPol = pol;
-  if( n.getKind()==NOT ){
+  if( n.getKind()==NOT || ( n.getKind()==IMPLIES && child==0 ) ){
     newPol = !pol;
-  }else if( n.getKind()==IFF ){
+  }else if( n.getKind()==IFF || n.getKind()==XOR ){
     newHasPol = false;
   }else if( n.getKind()==ITE ){
     if( child==0 ){
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index eba080a0e..2671f616b 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -409,6 +409,25 @@ bool TermDb::isInstClosure( Node r ) {
   return d_iclosure_processed.find( r )!=d_iclosure_processed.end();
 }
 
+//checks whether a type is reasonably small enough such that all of its domain elements can be enumerated
+bool TermDb::mayComplete( TypeNode tn ) {
+  std::map< TypeNode, bool >::iterator it = d_may_complete.find( tn );
+  if( it==d_may_complete.end() ){
+    bool mc = false;
+    if( !tn.isArray() && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() ){
+      Node card = NodeManager::currentNM()->mkConst( Rational(tn.getCardinality().getFiniteCardinality()) );
+      Node oth = NodeManager::currentNM()->mkConst( Rational(1000) );
+      Node eq = NodeManager::currentNM()->mkNode( LEQ, card, oth );
+      eq = Rewriter::rewrite( eq );
+      mc = eq==d_true;
+    }
+    d_may_complete[tn] = mc;
+    return mc;
+  }else{
+    return it->second;
+  }
+}
+
 void TermDb::setHasTerm( Node n ) {
   Trace("term-db-debug2") << "hasTerm : " << n  << std::endl;
   //if( inst::Trigger::isAtomicTrigger( n ) ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 455287feb..b7fa4e999 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -137,6 +137,8 @@ private:
   NodeIntMap d_op_ccount;
   /** set has term */
   void setHasTerm( Node n );
+  /** may complete */
+  std::map< TypeNode, bool > d_may_complete;
 public:
   TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe );
   ~TermDb(){}
@@ -191,6 +193,8 @@ public:
   Node getEligibleTermInEqc( TNode r );
   /** is inst closure */
   bool isInstClosure( Node r );
+  /** may complete */
+  bool mayComplete( TypeNode tn );
 //for model basis
 private:
   //map from types to model basis terms
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 454fe8971..eb05564e5 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -15,6 +15,7 @@
 #include "theory/rep_set.h"
 #include "theory/type_enumerator.h"
 #include "theory/quantifiers/bounded_integers.h"
+#include "theory/quantifiers/term_database.h"
 
 using namespace std;
 using namespace CVC4;
@@ -86,8 +87,15 @@ int RepSet::getIndexFor( Node n ) const {
   }
 }
 
-void RepSet::complete( TypeNode t ){
-  if( d_type_complete.find( t )==d_type_complete.end() ){
+bool RepSet::complete( TypeNode t ){
+  std::map< TypeNode, bool >::iterator it = d_type_complete.find( t );
+  if( it==d_type_complete.end() ){
+    //remove all previous 
+    for( unsigned i=0; i<d_type_reps[t].size(); i++ ){
+      d_tmap.erase( d_type_reps[t][i] );
+    }
+    d_type_reps[t].clear();
+    //now complete the type
     d_type_complete[t] = true;
     TypeEnumerator te(t);
     while( !te.isFinished() ){
@@ -101,6 +109,9 @@ void RepSet::complete( TypeNode t ){
       Trace("reps-complete") << d_type_reps[t][i] << " ";
     }
     Trace("reps-complete") << std::endl;
+    return true;
+  }else{
+    return it->second;
   }
 }
 
@@ -165,6 +176,7 @@ bool RepSetIterator::setFunctionDomain( Node op ){
 }
 
 bool RepSetIterator::initialize(){
+  Trace("rsi") << "Initialize rep set iterator..." << std::endl;
   for( size_t i=0; i<d_types.size(); i++ ){
     d_index.push_back( 0 );
     //store default index order
@@ -173,6 +185,7 @@ bool RepSetIterator::initialize(){
     //store default domain
     d_domain.push_back( RepDomain() );
     TypeNode tn = d_types[i];
+    Trace("rsi") << "Var #" << i << " is type " << tn << "..." << std::endl;
     if( tn.isSort() ){
       if( !d_rep_set->hasType( tn ) ){
         Node var = NodeManager::currentNM()->mkSkolem( "repSet", tn, "is a variable created by the RepSetIterator" );
@@ -184,7 +197,7 @@ bool RepSetIterator::initialize(){
       //check if it is bound
       if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){
         if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][i] ) ){
-          Trace("bound-int-rsi") << "Rep set iterator: variable #" << i << " is bounded integer." << std::endl;
+          Trace("rsi") << "  variable is bounded integer." << std::endl;
           d_enum_type.push_back( ENUM_RANGE );
         }else{
           inc = true;
@@ -195,18 +208,20 @@ bool RepSetIterator::initialize(){
       if( inc ){
         //check if it is otherwise bound
         if( d_bounds[0].find(i)!=d_bounds[0].end() && d_bounds[1].find(i)!=d_bounds[1].end() ){
-          Trace("bound-int-rsi") << "Rep set iterator: variable #" << i << " is bounded." << std::endl;
+          Trace("rsi") << "  variable is bounded." << std::endl;
           d_enum_type.push_back( ENUM_RANGE );
         }else{
+          Trace("rsi") << "  variable cannot be bounded." << std::endl;
           Trace("fmf-incomplete") << "Incomplete because of integer quantification of " << d_owner[0][i] << "." << std::endl;
           d_incomplete = true;
         }
       }
     //enumerate if the sort is reasonably small, not an Array, the upper bound of 1000 is chosen arbitrarily for now
-    }else if( !tn.isArray() && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() &&
-              tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=1000 ){
+    }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){
+      Trace("rsi") << "  do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl;
       d_rep_set->complete( tn );
     }else{
+      Trace("rsi") << "  variable cannot be bounded." << std::endl;
       Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl;
       d_incomplete = true;
     }
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 4aab230e6..f1114edcf 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -48,7 +48,7 @@ public:
   /** returns index in d_type_reps for node n */
   int getIndexFor( Node n ) const;
   /** complete all values */
-  void complete( TypeNode t );
+  bool complete( TypeNode t );
   /** debug print */
   void toStream(std::ostream& out);
 };/* class RepSet */
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 4e5c84f42..be202fb69 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -77,12 +77,6 @@ public:
     *   If it cannot find such a node, it returns null.
     */
   Node getNewDomainValue( TypeNode tn );
-  /** complete all values for type
-    *   Calling this function ensures that all terms of type tn exist in d_rep_set.d_type_reps[tn]
-    */
-  void completeDomainValues( TypeNode tn ){
-    d_rep_set.complete( tn );
-  }
 public:
   /** Adds a substitution from x to t. */
   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);