diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/model.cpp | 6 | ||||
-rw-r--r-- | src/theory/model.h | 4 |
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
|