From 6942ed1f963ff30c8acfe465f939fe078f7bc4fe Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 13 Aug 2013 16:10:41 -0500
Subject: [PATCH] Minor fixes for --fmf-fmc for quantifiers containing
 datatypes

---
 src/theory/quantifiers/first_order_model.cpp |  2 +-
 src/theory/quantifiers/full_model_check.cpp  |  9 ++++++---
 src/theory/quantifiers/term_database.cpp     | 14 ++++++++------
 3 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index be6844a1e..63cac9c15 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -630,7 +630,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
   Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);
   Node curr;
   for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {
-    Node v = getUsedRepresentative( d_models[op]->d_value[i] );
+    Node v = getRepresentative( d_models[op]->d_value[i] );
     if( curr.isNull() ){
       curr = v;
     }else{
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 6e7986390..ce03a1877 100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -553,7 +553,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
 
 void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){
   if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){
-    Trace("fmc") << "Initialize type " << tn << std::endl;
+    Trace("fmc") << "Initialize type " << tn << " hasType = " << fm->d_rep_set.hasType(tn) << std::endl;
     Node mbn;
     if (!fm->d_rep_set.hasType(tn)) {
       mbn = fm->getSomeDomainElement(tn);
@@ -684,13 +684,16 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f,
             }
             d_triedLemmas++;
             if( d_qe->addInstantiation( f, m ) ){
+              Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
               d_addedLemmas++;
             }else{
+              Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl;
               //this can happen if evaluation is unknown
               //might try it next effort level
               d_star_insts[f].push_back(i);
             }
           }else{
+            Trace("fmc-debug-inst") << "** Instantiation was already true." << std::endl;
             //might try it next effort level
             d_star_insts[f].push_back(i);
           }
@@ -1146,7 +1149,7 @@ void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, De
 }
 
 int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
-  Trace("fmc-debug2") << "isCompat " << c << std::endl;
+  Trace("fmc-debug3") << "isCompat " << c << std::endl;
   Assert(cond.size()==c.getNumChildren()+1);
   for (unsigned i=1; i<cond.size(); i++) {
     if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){
@@ -1164,7 +1167,7 @@ int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & c
 }
 
 bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
-  Trace("fmc-debug2") << "doMeet " << c << std::endl;
+  Trace("fmc-debug3") << "doMeet " << c << std::endl;
   Assert(cond.size()==c.getNumChildren()+1);
   for (unsigned i=1; i<cond.size(); i++) {
     if( cond[i]!=c[i-1] ) {
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 5569f6843..e18a4e0dc 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -194,18 +194,20 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
 Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
   if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
     Node mbt;
-    if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){
-      if( tn.isInteger() || tn.isReal() ){
-        mbt = NodeManager::currentNM()->mkConst( Rational( 0 ) );
-      }else{
+    if( tn.isInteger() || tn.isReal() ){
+      mbt = NodeManager::currentNM()->mkConst( Rational( 0 ) );
+    }else if( !tn.isSort() ){
+      mbt = tn.mkGroundTerm();
+    }else{
+      if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){
         std::stringstream ss;
         ss << Expr::setlanguage(options::outputLanguage());
         ss << "e_" << tn;
         mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" );
         Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl;
+      }else{
+        mbt = d_type_map[ tn ][ 0 ];
       }
-    }else{
-      mbt = d_type_map[ tn ][ 0 ];
     }
     ModelBasisAttribute mba;
     mbt.setAttribute(mba,true);
-- 
2.30.2