updates to model generation : do not modify equality engine during getValue, other minor changes, still problems with constants not being specified for some eq classes

3 files changed, 12 insertions, 9 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 6e3e27828..e0723f432 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -28,7 +28,7 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : DefaultModel( c, name, true ),
+FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : TheoryModel( c, name, true ),
 d_axiom_asserted( c, false ), d_forall_asserts( c ){
 
 }
@@ -41,11 +41,11 @@ void FirstOrderModel::assertQuantifier( Node n ){
 }
 
 void FirstOrderModel::reset(){
-  DefaultModel::reset();
+  TheoryModel::reset();
 }
 
 void FirstOrderModel::addTerm( Node n ){
-  DefaultModel::addTerm( n );
+  TheoryModel::addTerm( n );
 }
 
 void FirstOrderModel::initialize( bool considerAxioms ){
@@ -94,16 +94,16 @@ void FirstOrderModel::initializeModelForTerm( Node n ){
 }
 
 Node FirstOrderModel::getInterpretedValue( TNode n ){
-  Trace("fo-model") << "get interpreted value " << n << std::endl;
-  TypeNode type = n.getType();
+  //Trace("fo-model") << "get interpreted value " << n << std::endl;
+  /*TypeNode type = n.getType();
   if( type.isFunction() || type.isPredicate() ){
     if( d_uf_model_tree.find( n )!=d_uf_model_tree.end() ){
       if( d_uf_models.find( n )==d_uf_models.end() ){
         d_uf_models[n] = d_uf_model_tree[n].getFunctionValue( "$x" );
       }
     }
-  }
-  return DefaultModel::getInterpretedValue( n );
+  }*/
+  return TheoryModel::getInterpretedValue( n );
 }
 
 void FirstOrderModel::toStream(std::ostream& out){
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 1fc4fd76e..64e5fc904 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -39,7 +39,7 @@ namespace quantifiers{
 
 class TermDb;
 
-class FirstOrderModel : public DefaultModel
+class FirstOrderModel : public TheoryModel
 {
 private:
   //add term function
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index c09346f35..8eac4da95 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -76,8 +76,11 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
     //update models
     for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
       it->second.update( fm );
+      Trace("model-func") << "ModelEngineBuilder: Make function value from tree " << it->first << std::endl;
+      //construct function values
+      fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" );
     }
-
+    TheoryEngineModelBuilder::processBuildModel( m, fullModel );
   }else{
     d_curr_model = fm;
     //build model for relevant symbols contained in quantified formulas