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

3 files changed, 25 insertions, 3 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