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

2 files changed, 5 insertions, 5 deletions

diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 19169efa3..609275a98 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -201,7 +201,7 @@ Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){
 }

 

 //FIXME: use the theory enumerator to generate constants here

-Node TheoryModel::getNewDomainValue( TypeNode tn, bool mkConst ){

+Node TheoryModel::getNewDomainValue( TypeNode tn ){

   if( tn==NodeManager::currentNM()->booleanType() ){

     if( d_ra.d_type_reps[tn].empty() ){

       return d_false;

@@ -352,7 +352,7 @@ Node DefaultModel::getInterpretedValue( TNode n ){
       return n2;

     }else{

       //otherwise, choose new value

-      n2 = getNewDomainValue( type, true );

+      n2 = getNewDomainValue( type );

       if( !n2.isNull() ){

         return n2;

       }else{

@@ -422,7 +422,7 @@ void TheoryEngineModelBuilder::processBuildModel( TheoryModel* tm ){
     if( tm->d_reps.find( n )!=tm->d_reps.end() ){

       TypeNode tn = n.getType();

       //add new constant to equivalence class

-      Node rep = tm->getNewDomainValue( tn, true );

+      Node rep = tm->getNewDomainValue( tn );

       if( !rep.isNull() ){

         tm->assertEquality( n, rep, true );

       }else{

diff --git a/src/theory/model.h b/src/theory/model.h
index 4d6035ae5..278f85dfe 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -98,7 +98,7 @@ public:
   /** get existing domain value, with possible exclusions */

   Node getDomainValue( TypeNode tn, std::vector< Node >& exclude );

   /** get new domain value */

-  Node getNewDomainValue( TypeNode tn, bool mkConst = false );

+  Node getNewDomainValue( TypeNode tn );

 public:

   /** assert equality */

   void assertEquality( Node a, Node b, bool polarity );

@@ -162,4 +162,4 @@ public:
 }

 }

 

-#endif
\ No newline at end of file
+#endif