diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-07-18 21:21:28 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-07-18 21:21:28 +0000 |
| commit | d6d1763f41c3b9351b969bfdd2c44dae779f9ee3 (patch) | |
| tree | 0ef5e8386d8bfefb84aaab6d96e8f7f8b15b4433 /src/theory/model.cpp | |
| parent | 4228332c346147daa83c0c4123c8781909a23a03 (diff) | |
small change to model-generation function, after discussion w/ Andy
Diffstat (limited to 'src/theory/model.cpp')
| -rw-r--r-- | src/theory/model.cpp | 6 |
1 files changed, 3 insertions, 3 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{
|