Fix term database for non-equal, congruent terms in master equality engine. Disable ITE terms in quant conflict find.

6 files changed, 76 insertions, 79 deletions

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index ff0da13e1..e44a322b5 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -411,6 +411,11 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
           Node r = fm->getUsedRepresentative(n);
           Trace("fmc-model-debug") << n << " -> " << r << std::endl;
           //AlwaysAssert( fm->areEqual( fm->d_uf_terms[op][i], r ) );
+        }else{
+          if( Trace.isOn("fmc-model-debug") ){
+            Node r = fm->getUsedRepresentative(n);
+            Trace("fmc-model-debug") << "[redundant] " << n << " -> " << r << std::endl;
+          }
         }
       }
       Trace("fmc-model-debug") << std::endl;
@@ -614,7 +619,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
 
         //consider all entries going to non-true
         for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) {
-          if( d_quant_models[f].d_value[i]!=d_true) {
+          if( d_quant_models[f].d_value[i]!=d_true ) {
             Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;
             bool hasStar = false;
             std::vector< Node > inst;
@@ -684,7 +689,11 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
                   }
                 }else{
                   Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl;
-                  //this can happen if evaluation is unknown
+                  //this can happen if evaluation is unknown, or if we are generalizing a star that already has a value
+                  if( !hasStar && d_quant_models[f].d_value[i]==d_false ){
+                    Trace("fmc-warn") << "**** FMC warning: inconsistent duplicate instantiation." << std::endl;
+                  }
+                  Assert( hasStar || d_quant_models[f].d_value[i]!=d_false );
                   //might try it next effort level
                   d_star_insts[f].push_back(i);
                 }
@@ -780,11 +789,11 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
       for( int i=0; i<riter.getNumTerms(); i++ ){
         Node rr = riter.getTerm( i );
         Node r = rr;
-        if( r.getType().isSort() ){
-          r = fm->getUsedRepresentative( r );
-        }else{
-          r = fm->getCurrentModelValue( r );
-        }
+        //if( r.getType().isSort() ){
+        r = fm->getUsedRepresentative( r );
+        //}else{
+        //  r = fm->getCurrentModelValue( r );
+        //}
         debugPrint("fmc-exh-debug", r);
         Trace("fmc-exh-debug") << " (term : " << rr << ")";
         ev_inst.push_back( r );
@@ -846,38 +855,12 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
     d.addEntry(fm, mkCondDefault(fm, f), Node::null());
   }
   else if( n.getType().isArray() ){
-    //make the definition
-    bool success = false;
-    /*
-    Node r = fm->getRepresentative(n);
-    Trace("fmc-debug") << "Representative for array is " << r << std::endl;
-    while( r.getKind() == kind::STORE ){
-      Node i = fm->getUsedRepresentative( r[1] );
-      Node e = fm->getUsedRepresentative( r[2] );
-      d.addEntry(fm, mkArrayCond(i), e );
-      r = fm->getRepresentative( r[0] );
-    }
-    Node defC = mkArrayCond(fm->getStar(n.getType().getArrayIndexType()));
-    bool success = false;
-    Node odefaultValue;
-    if( r.getKind() == kind::STORE_ALL ){
-      ArrayStoreAll storeAll = r.getConst<ArrayStoreAll>();
-      odefaultValue = Node::fromExpr(storeAll.getExpr());
-      Node defaultValue = fm->getUsedRepresentative( odefaultValue, true );
-      if( !defaultValue.isNull() ){
-        d.addEntry(fm, defC, defaultValue);
-        success = true;
-      }
-    }
-    */
-    if( !success ){
-      //Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl;
-      //Trace("fmc-warn") << "          Default value was : " << odefaultValue << std::endl;
-      //Trace("fmc-debug") << "Can't process base array " << r << std::endl;
-      //can't process this array
-      d.reset();
-      d.addEntry(fm, mkCondDefault(fm, f), Node::null());
-    }
+    //Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl;
+    //Trace("fmc-warn") << "          Default value was : " << odefaultValue << std::endl;
+    //Trace("fmc-debug") << "Can't process base array " << r << std::endl;
+    //can't process this array
+    d.reset();
+    d.addEntry(fm, mkCondDefault(fm, f), Node::null());
   }
   else if( n.getNumChildren()==0 ){
     Node r = n;
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 95b674cca..a698b33e1 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -50,8 +50,8 @@ bool QModelBuilder::optUseModel() {
 
 void QModelBuilder::debugModel( FirstOrderModel* fm ){
   //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
-  if( Trace.isOn("quant-model-warn") ){
-    Trace("quant-model-warn") << "Testing quantifier instantiations..." << std::endl;
+  if( Trace.isOn("quant-check-model") ){
+    Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl;
     int tests = 0;
     int bad = 0;
     for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
@@ -71,20 +71,20 @@ void QModelBuilder::debugModel( FirstOrderModel* fm ){
           Node n = d_qe->getInstantiation( f, vars, terms );
           Node val = fm->getValue( n );
           if( val!=fm->d_true ){
-            Trace("quant-model-warn") << "*******  Instantiation " << n << " for " << std::endl;
-            Trace("quant-model-warn") << "         " << f << std::endl;
-            Trace("quant-model-warn") << "         Evaluates to " << val << std::endl;
+            Trace("quant-check-model") << "*******  Instantiation " << n << " for " << std::endl;
+            Trace("quant-check-model") << "         " << f << std::endl;
+            Trace("quant-check-model") << "         Evaluates to " << val << std::endl;
             bad++;
           }
           riter.increment();
         }
-        Trace("quant-model-warn") << "Tested " << tests << " instantiations";
+        Trace("quant-check-model") << "Tested " << tests << " instantiations";
         if( bad>0 ){
-          Trace("quant-model-warn") << ", " << bad << " failed" << std::endl;
+          Trace("quant-check-model") << ", " << bad << " failed" << std::endl;
         }
-        Trace("quant-model-warn") << "." << std::endl;
+        Trace("quant-check-model") << "." << std::endl;
       }else{
-        Trace("quant-model-warn") << "Warning: Could not test quantifier " << f << std::endl;
+        Trace("quant-check-model") << "Warning: Could not test quantifier " << f << std::endl;
       }
     }
   }
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index a890276f7..5cff55d21 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -801,6 +801,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
   if( isVar ){
     Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() );
     if( n.getKind()==ITE ){
+  /*
       d_type = typ_ite_var;
       d_type_not = false;
       d_n = n;
@@ -817,8 +818,9 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
           }
         }
       }else{
+*/
         d_type = typ_invalid;
-      }
+     //}
     }else{
       d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym;
       d_qni_var_num[0] = qi->getVarNum( n );
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 3c155c421..ff55c5c9b 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1739,31 +1739,29 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
     //check if it contains a quantifier as a subterm
     //if so, we will write this node
     if( containsQuantifiers( n ) ){
-      if( n.getType().isBoolean() ){
-        if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){
-          if( options::preSkolemQuantAgg() ){
-            Node nn;
-            //must remove structure
-            if( n.getKind()==kind::ITE ){
-              nn = NodeManager::currentNM()->mkNode( kind::AND,
-                    NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
-                    NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
-            }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
-              nn = NodeManager::currentNM()->mkNode( kind::AND,
-                    NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
-                    NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
-            }else if( n.getKind()==kind::IMPLIES ){
-              nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
-            }
-            return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs );
-          }
-        }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
-          vector< Node > children;
-          for( int i=0; i<(int)n.getNumChildren(); i++ ){
-            children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvTypes, fvs ) );
+      if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || n.getKind()==kind::IFF ){
+        if( options::preSkolemQuantAgg() ){
+          Node nn;
+          //must remove structure
+          if( n.getKind()==kind::ITE ){
+            nn = NodeManager::currentNM()->mkNode( kind::AND,
+                  NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
+                  NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
+          }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
+            nn = NodeManager::currentNM()->mkNode( kind::AND,
+                  NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
+                  NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
+          }else if( n.getKind()==kind::IMPLIES ){
+            nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
           }
-          return NodeManager::currentNM()->mkNode( n.getKind(), children );
+          return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs );
+        }
+      }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
+        vector< Node > children;
+        for( int i=0; i<(int)n.getNumChildren(); i++ ){
+          children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvTypes, fvs ) );
         }
+        return NodeManager::currentNM()->mkNode( n.getKind(), children );
       }
     }
   }
@@ -1771,15 +1769,20 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v
 }
 
 Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
+  Node prev = n;
   if( options::preSkolemQuant() ){
     if( !isInst || !options::preSkolemQuantNested() ){
-      //apply pre-skolemization to existential quantifiers
       Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl;
+      //apply pre-skolemization to existential quantifiers
       std::vector< TypeNode > fvTypes;
       std::vector< TNode > fvs;
-      n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( n, true, fvTypes, fvs );
+      n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs );
     }
   }
+  if( n!=prev ){       
+    Trace("quantifiers-preprocess") << "Preprocess " << prev<< std::endl;
+    Trace("quantifiers-preprocess") << "..returned " << n << std::endl;
+  }
   return n;
 }
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 3e5e30bd7..cb23b8bb7 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -59,16 +59,20 @@ TNode TermArgTrie::existsTerm( std::vector< TNode >& reps, int argIndex ) {
 }
 
 bool TermArgTrie::addTerm( TNode n, std::vector< TNode >& reps, int argIndex ){
+  return addOrGetTerm( n, reps, argIndex )==n;
+}
+
+TNode TermArgTrie::addOrGetTerm( TNode n, std::vector< TNode >& reps, int argIndex ) {
   if( argIndex==(int)reps.size() ){
     if( d_data.empty() ){
       //store n in d_data (this should be interpretted as the "data" and not as a reference to a child)
       d_data[n].clear();
-      return true;
+      return n;
     }else{
-      return false;
+      return d_data.begin()->first;
     }
   }else{
-    return d_data[reps[argIndex]].addTerm( n, reps, argIndex+1 );
+    return d_data[reps[argIndex]].addOrGetTerm( n, reps, argIndex+1 );
   }
 }
 
@@ -502,9 +506,12 @@ void TermDb::reset( Theory::Effort effort ){
               Trace("term-db-debug") << d_arg_reps[n] << " ";
             }
             Trace("term-db-debug") << std::endl;
+            if( ee->hasTerm( n ) ){
+              Trace("term-db-debug") << "  and value : " << ee->getRepresentative( n ) << std::endl;
+            }
           }
-
-          if( !d_func_map_trie[ it->first ].addTerm( n, d_arg_reps[n] ) ){
+          Node at = d_func_map_trie[ it->first ].addOrGetTerm( n, d_arg_reps[n] );
+          if( at!=n && ee->areEqual( at, n ) ){
             NoMatchAttribute nma;
             n.setAttribute(nma,true);
             Trace("term-db-debug") << n << " is redundant." << std::endl;
@@ -514,6 +521,7 @@ void TermDb::reset( Theory::Effort effort ){
             d_op_nonred_count[ it->first ]++;
           }
         }else{
+          Trace("term-db-debug") << n << " is already redundant." << std::endl;
           congruentCount++;
           alreadyCongruentCount++;
         }
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index c770f0e6f..5560098c9 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -121,6 +121,7 @@ public:
   std::map< TNode, TermArgTrie > d_data;
 public:
   TNode existsTerm( std::vector< TNode >& reps, int argIndex = 0 );
+  TNode addOrGetTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 );
   bool addTerm( TNode n, std::vector< TNode >& reps, int argIndex = 0 );
   void debugPrint( const char * c, Node n, unsigned depth = 0 );
   void clear() { d_data.clear(); }