small change to model-generation function, after discussion w/ Andy

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 19169efa36de2a68343a7b836e744971b49d81c2..609275a98a4d9bb3e8aa44e355f0cf77c75a623d 100644 (file)
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -201,7 +201,7 @@ Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){
 }\r
 \r
 //FIXME: use the theory enumerator to generate constants here\r
-Node TheoryModel::getNewDomainValue( TypeNode tn, bool mkConst ){\r
+Node TheoryModel::getNewDomainValue( TypeNode tn ){\r
   if( tn==NodeManager::currentNM()->booleanType() ){\r
     if( d_ra.d_type_reps[tn].empty() ){\r
       return d_false;\r
@@ -352,7 +352,7 @@ Node DefaultModel::getInterpretedValue( TNode n ){
       return n2;\r
     }else{\r
       //otherwise, choose new value\r
-      n2 = getNewDomainValue( type, true );\r
+      n2 = getNewDomainValue( type );\r
       if( !n2.isNull() ){\r
         return n2;\r
       }else{\r
@@ -422,7 +422,7 @@ void TheoryEngineModelBuilder::processBuildModel( TheoryModel* tm ){
     if( tm->d_reps.find( n )!=tm->d_reps.end() ){\r
       TypeNode tn = n.getType();\r
       //add new constant to equivalence class\r
-      Node rep = tm->getNewDomainValue( tn, true );\r
+      Node rep = tm->getNewDomainValue( tn );\r
       if( !rep.isNull() ){\r
         tm->assertEquality( n, rep, true );\r
       }else{\r

diff --git a/src/theory/model.h b/src/theory/model.h
index 4d6035ae57b8221f83588e37156faa166946dbc3..278f85dfe86852dc5674e1fb8ce3ff22fe2fd49f 100644 (file)
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -98,7 +98,7 @@ public:
   /** get existing domain value, with possible exclusions */\r
   Node getDomainValue( TypeNode tn, std::vector< Node >& exclude );\r
   /** get new domain value */\r
-  Node getNewDomainValue( TypeNode tn, bool mkConst = false );\r
+  Node getNewDomainValue( TypeNode tn );\r
 public:\r
   /** assert equality */\r
   void assertEquality( Node a, Node b, bool polarity );\r
@@ -162,4 +162,4 @@ public:
 }\r
 }\r
 \r
-#endif
\ No newline at end of file
+#endif\r