From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 18 Jul 2012 21:21:28 +0000 (+0000)
Subject: small change to model-generation function, after discussion w/ Andy
X-Git-Tag: cvc5-1.0.0~7914
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d6d1763f41c3b9351b969bfdd2c44dae779f9ee3;p=cvc5.git

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

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