Fixes and simplifications for fmf mbqi.

8 files changed, 67 insertions, 87 deletions

diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index de55ecdba..bc638080f 100644
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -774,10 +774,9 @@ bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) {
     if( itut!=fm->d_uf_terms.end() ){
       for( size_t i=0; i<itut->second.size(); i++ ){
         Node n = itut->second[i];
-        if( d_qe->getTermDatabase()->isTermActive( n ) ){
-          Trace("ambqi-model-debug") << "  " << n << " -> " << fm->getRepresentativeId( n ) << std::endl;
-          fapps.push_back( n );
-        }
+        // only consider unique up to congruence (in model equality engine)?
+        Trace("ambqi-model-debug") << "  " << n << " -> " << fm->getRepresentativeId( n ) << std::endl;
+        fapps.push_back( n );
       }
     }
     if( fapps.empty() ){
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 16fc4d4b8..084912f5a 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -615,23 +615,6 @@ FirstOrderModelFmc::~FirstOrderModelFmc() throw() {
   }
 }
 
-Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) {
-  //Assert( fm->hasTerm(n) );
-  TypeNode tn = n.getType();
-  if( tn.isBoolean() ){
-    return areEqual(n, d_true) ? d_true : d_false;
-  }else{
-    if( !hasTerm(n) ){
-      if( strict ){
-        return Node::null();
-      }else{
-        Trace("fmc-warn") << "WARNING : no representative for " << n << std::endl;
-      }
-    }
-    return getRepresentative(n);
-  }
-}
-
 /*
 Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
   Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl;
@@ -753,7 +736,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
           }
         }else if ( !isStar(cond[j]) &&  //handle the case where there are 0 or 1 ground eqc of this type
                    d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && d_rep_set.d_type_reps[ tn ].size()>1 ){
-          Node c = getUsedRepresentative( cond[j] );
+          Node c = getRepresentative( cond[j] );
           c = getRepresentative( c );
           children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
         }
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 05771d1a2..e4adfc8bd 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -167,7 +167,6 @@ private:
   std::map<Node, Def * > d_models;
   std::map<TypeNode, Node > d_type_star;
   Node intervalOp;
-  Node getUsedRepresentative(Node n, bool strict = false);
   /** get current model value */
   void processInitializeModelForTerm(Node n);
 public:
@@ -206,13 +205,13 @@ private:
   void processInitializeModelForTerm(Node n);
   void processInitializeQuantifier( Node q );
   void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars );
+  TNode getUsedRepresentative( TNode n );
 public:
   FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name);
   ~FirstOrderModelAbs() throw();
   FirstOrderModelAbs * asFirstOrderModelAbs() { return this; }
   void processInitialize( bool ispre );
   unsigned getRepresentativeId( TNode n );
-  TNode getUsedRepresentative( TNode n );
   bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); }
   Node getFunctionValue(Node op, const char* argPrefix );
   Node getVariable( Node q, unsigned i );
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 259083e6e..c41d09187 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -379,7 +379,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
     if( it->first.isSort() ){
       Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
       for( size_t a=0; a<it->second.size(); a++ ){
-        Node r = fm->getUsedRepresentative( it->second[a] );
+        Node r = fm->getRepresentative( it->second[a] );
         if( Trace.isOn("fmc-model-debug") ){
           std::vector< Node > eqc;
           ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
@@ -412,18 +412,12 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
       Trace("fmc-model-debug") << itut->second.size() << " model values for " << op << " ... " << std::endl;
       for( size_t i=0; i<itut->second.size(); i++ ){
         Node n = itut->second[i];
-        if( d_qe->getTermDatabase()->isTermActive( n ) ){
-          add_conds.push_back( n );
-          add_values.push_back( n );
-          Node r = fm->getUsedRepresentative(n);
-          Trace("fmc-model-debug") << n << " -> " << r << std::endl;
-          //AlwaysAssert( fm->areEqual( itut->second[i], r ) );
-        }else{
-          if( Trace.isOn("fmc-model-debug") ){
-            Node r = fm->getUsedRepresentative(n);
-            Trace("fmc-model-debug") << "[redundant] " << n << " -> " << r << std::endl;
-          }
-        }
+        // only consider unique up to congruence (in model equality engine)?
+        add_conds.push_back( n );
+        add_values.push_back( n );
+        Node r = fm->getRepresentative(n);
+        Trace("fmc-model-debug") << n << " -> " << r << std::endl;
+        //AlwaysAssert( fm->areEqual( itut->second[i], r ) );
       }
     }else{
       Trace("fmc-model-debug") << "No model values for " << op << " ... " << std::endl;
@@ -449,7 +443,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
     std::vector< Node > conds;
     std::vector< Node > values;
     std::vector< Node > entry_conds;
-    //get the entries for the mdoel
+    //get the entries for the model
     for( size_t i=0; i<add_conds.size(); i++ ){
       Node c = add_conds[i];
       Node v = add_values[i];
@@ -459,7 +453,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
       entry_children.push_back(op);
       bool hasNonStar = false;
       for( unsigned i=0; i<c.getNumChildren(); i++) {
-        Node ri = fm->getUsedRepresentative( c[i] );
+        Node ri = fm->getRepresentative( c[i] );
         children.push_back(ri);
         bool isStar = false;
         if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){
@@ -477,7 +471,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
         entry_children.push_back(ri);
       }
       Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
-      Node nv = fm->getUsedRepresentative( v );
+      Node nv = fm->getRepresentative( v );
       if( !nv.isConst() ){
         Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl;
         Assert( false );
@@ -529,7 +523,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
     for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
       std::vector< Node > inst;
       for( unsigned j=0; j<fm->d_uf_terms[op][i].getNumChildren(); j++ ){
-        Node r = fm->getUsedRepresentative( fm->d_uf_terms[op][i][j] );
+        Node r = fm->getRepresentative( fm->d_uf_terms[op][i][j] );
         inst.push_back( r );
       }
       Node ev = fm->d_models[op]->evaluate( fm, inst );
@@ -784,7 +778,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
         Node rr = riter.getCurrentTerm( i );
         Node r = rr;
         //if( r.getType().isSort() ){
-        r = fm->getUsedRepresentative( r );
+        r = fm->getRepresentative( r );
         //}else{
         //  r = fm->getCurrentModelValue( r );
         //}
@@ -862,7 +856,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
       if( !fm->hasTerm(n) ){
         r = getSomeDomainElement(fm, n.getType() );
       }
-      r = fm->getUsedRepresentative( r );
+      r = fm->getRepresentative( r );
     }
     Trace("fmc-debug") << "Add constant entry..." << std::endl;
     d.addEntry(fm, mkCondDefault(fm, f), r);
@@ -948,7 +942,7 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def
         getSomeDomainElement( fm, tn );  //to verify the type is initialized
       }
       for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {
-        Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] );
+        Node r = fm->getRepresentative( fm->d_rep_set.d_type_reps[tn][i] );
         cond[j+1] = r;
         cond[k+1] = r;
         d.addEntry( fm, mkCond(cond), d_true);
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 7f342c633..055c9e31c 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -334,22 +334,19 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){
       for( size_t i=0; i<itut->second.size(); i++ ){
         Node n = fmig->d_uf_terms[op][i];
         //for calculating if op is constant
-        if( d_qe->getTermDatabase()->isTermActive( n ) ){
-          Node v = fmig->getRepresentative( n );
-          if( i==0 ){
-            d_uf_prefs[op].d_const_val = v;
-          }else if( v!=d_uf_prefs[op].d_const_val ){
-            d_uf_prefs[op].d_const_val = Node::null();
-            break;
-          }
+        Node v = fmig->getRepresentative( n );
+        if( i==0 ){
+          d_uf_prefs[op].d_const_val = v;
+        }else if( v!=d_uf_prefs[op].d_const_val ){
+          d_uf_prefs[op].d_const_val = Node::null();
+          break;
         }
         //for calculating terms that we don't need to consider
-        if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
-          if( d_basisNoMatch.find( n )==d_basisNoMatch.end() ){
-            //need to consider if it is not congruent modulo model basis
-            if( !tabt.addTerm( fmig, n ) ){
-              d_basisNoMatch[n] = true;
-            }
+        //if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
+        if( d_basisNoMatch.find( n )==d_basisNoMatch.end() ){
+          //need to consider if it is not congruent modulo model basis
+          if( !tabt.addTerm( fmig, n ) ){
+            d_basisNoMatch[n] = true;
           }
         }
       }
@@ -409,13 +406,6 @@ QModelBuilderIG::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown);
 }
 
-bool QModelBuilderIG::isTermActive( Node n ){
-  return d_qe->getTermDatabase()->isTermActive( n ) || //it is not congruent to another active term
-         ( n.getAttribute(ModelBasisArgAttribute())!=0 && d_basisNoMatch.find( n )==d_basisNoMatch.end() ); //or it has model basis arguments
-                                                                                                      //and is not congruent modulo model basis
-                                                                                                      //to another active term
-}
-
 //do exhaustive instantiation
 int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
   if( optUseModel() ){
@@ -739,30 +729,29 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
     if( itut!=fmig->d_uf_terms.end() ){
       for( size_t i=0; i<itut->second.size(); i++ ){
         Node n = itut->second[i];
-        if( isTermActive( n ) ){
-          Node v = fmig->getRepresentative( n );
-          Trace("fmf-model-cons") << "Set term " << n << " : " << fmig->d_rep_set.getIndexFor( v ) << " " << v << std::endl;
-          //if this assertion did not help the model, just consider it ground
-          //set n = v in the model tree
-          //set it as ground value
-          fmig->d_uf_model_gen[op].setValue( fm, n, v );
-          if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){
-            //also set as default value if necessary
-            if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){
-              Trace("fmf-model-cons") << "  Set as default." << std::endl;
-              fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
-              if( n==defaultTerm ){
-                //incidentally already set, we will not need to find a default value
-                setDefaultVal = false;
-              }
-            }
-          }else{
+        // only consider unique up to congruence (in model equality engine)?
+        Node v = fmig->getRepresentative( n );
+        Trace("fmf-model-cons") << "Set term " << n << " : " << fmig->d_rep_set.getIndexFor( v ) << " " << v << std::endl;
+        //if this assertion did not help the model, just consider it ground
+        //set n = v in the model tree
+        //set it as ground value
+        fmig->d_uf_model_gen[op].setValue( fm, n, v );
+        if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){
+          //also set as default value if necessary
+          if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){
+            Trace("fmf-model-cons") << "  Set as default." << std::endl;
+            fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
             if( n==defaultTerm ){
-              fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
               //incidentally already set, we will not need to find a default value
               setDefaultVal = false;
             }
           }
+        }else{
+          if( n==defaultTerm ){
+            fmig->d_uf_model_gen[op].setValue( fm, n, v, false );
+            //incidentally already set, we will not need to find a default value
+            setDefaultVal = false;
+          }
         }
       }
     }
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index eedd850d6..3f548c9fd 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -131,8 +131,6 @@ public:
     ~Statistics();
   };
   Statistics d_statistics;
-  // is term active
-  bool isTermActive( Node n );
   // is term selected
   virtual bool isTermSelected( Node n ) { return false; }
   /** quantifier has inst-gen definition */
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 0c13961cc..a91499a6c 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -71,7 +71,8 @@ TESTS =	\
 	bug782.smt2 \
 	quant_real_univ.cvc \
 	constr-ground-to.smt2 \
-	bug-041417-set-options.cvc
+	bug-041417-set-options.cvc \
+	alg202+1.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/alg202+1.smt2 b/test/regress/regress0/fmf/alg202+1.smt2
new file mode 100644
index 000000000..ff3460636
--- /dev/null
+++ b/test/regress/regress0/fmf/alg202+1.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort $$unsorted 0)
+(declare-fun sorti1 ($$unsorted) Bool)
+(declare-fun op1 ($$unsorted $$unsorted) $$unsorted)
+(declare-fun sorti2 ($$unsorted) Bool)
+(declare-fun op2 ($$unsorted $$unsorted) $$unsorted)
+(declare-fun h ($$unsorted) $$unsorted)
+(declare-fun j ($$unsorted) $$unsorted)
+(assert (forall ((U $$unsorted) (BOUND_VARIABLE_345 $$unsorted)) (or (not (sorti1 U)) (not (sorti1 BOUND_VARIABLE_345)) (sorti1 (op1 U BOUND_VARIABLE_345))) ))
+(assert (forall ((U $$unsorted) (BOUND_VARIABLE_364 $$unsorted)) (or (not (sorti2 U)) (not (sorti2 BOUND_VARIABLE_364)) (sorti2 (op2 U BOUND_VARIABLE_364))) ))
+(assert (forall ((U $$unsorted)) (or (not (sorti1 U)) (= U (op1 U U))) ))
+(assert (not (forall ((U $$unsorted)) (or (not (sorti2 U)) (= U (op2 U U))) )))
+(assert (not (=> (and (forall ((U $$unsorted)) (or (not (sorti1 U)) (sorti2 (h U))) ) (forall ((V $$unsorted)) (or (not (sorti2 V)) (sorti1 (j V))) )) (not (and (forall ((W $$unsorted) (BOUND_VARIABLE_406 $$unsorted)) (or (not (sorti1 W)) (not (sorti1 BOUND_VARIABLE_406)) (= (op2 (h W) (h BOUND_VARIABLE_406)) (h (op1 W BOUND_VARIABLE_406)))) ) (forall ((Y $$unsorted) (BOUND_VARIABLE_431 $$unsorted)) (or (not (sorti2 Y)) (not (sorti2 BOUND_VARIABLE_431)) (= (op1 (j Y) (j BOUND_VARIABLE_431)) (j (op2 Y BOUND_VARIABLE_431)))) ) (forall ((X1 $$unsorted)) (or (not (sorti2 X1)) (= X1 (h (j X1)))) ) (forall ((X2 $$unsorted)) (or (not (sorti1 X2)) (= X2 (j (h X2)))) ))))))
+(assert (and (forall ((U $$unsorted)) (or (not (sorti1 U)) (sorti2 (h U))) ) (forall ((V $$unsorted)) (or (not (sorti2 V)) (sorti1 (j V))) ) (forall ((W $$unsorted) (BOUND_VARIABLE_406 $$unsorted)) (or (not (sorti1 W)) (not (sorti1 BOUND_VARIABLE_406)) (= (op2 (h W) (h BOUND_VARIABLE_406)) (h (op1 W BOUND_VARIABLE_406)))) ) (forall ((Y $$unsorted) (BOUND_VARIABLE_431 $$unsorted)) (or (not (sorti2 Y)) (not (sorti2 BOUND_VARIABLE_431)) (= (op1 (j Y) (j BOUND_VARIABLE_431)) (j (op2 Y BOUND_VARIABLE_431)))) ) (forall ((X1 $$unsorted)) (or (not (sorti2 X1)) (= X1 (h (j X1)))) ) (forall ((X2 $$unsorted)) (or (not (sorti1 X2)) (= X2 (j (h X2)))) )))
+(check-sat)