diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
commit | 0b2f9943d55152e0958369083649dd71340864c9 (patch) | |
tree | cd040f1dd12816c6af37548597bd674cafb45271 /src/theory | |
parent | 8ebd49cb903ba19f9330820d02af08e226c9b791 (diff) |
More preparation for CASC proofs. Minor fix for sort inference (rewrite new assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.
Diffstat (limited to 'src/theory')
-rwxr-xr-x | src/theory/quantifiers/ambqi_builder.cpp | 34 | ||||
-rwxr-xr-x | src/theory/quantifiers/ambqi_builder.h | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 24 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 22 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 2 | ||||
-rw-r--r-- | src/theory/rep_set.cpp | 12 | ||||
-rw-r--r-- | src/theory/rep_set.h | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 6 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 5 | ||||
-rw-r--r-- | src/theory/theory_model.cpp | 6 |
14 files changed, 83 insertions, 59 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index c6a5f4227..e86a96a8f 100755 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -73,20 +73,20 @@ void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps }
}
-void AbsDef::simplify( FirstOrderModelAbs * m, TNode n, unsigned depth ) {
+void AbsDef::simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth ) {
if( d_value==val_none && !d_def.empty() ){
//process the default
std::map< unsigned, AbsDef >::iterator defd = d_def.find( d_default );
Assert( defd!=d_def.end() );
unsigned newDef = d_default;
std::vector< unsigned > to_erase;
- defd->second.simplify( m, n, depth+1 );
+ defd->second.simplify( m, q, n, depth+1 );
int defVal = defd->second.d_value;
bool isConstant = ( defVal!=val_none );
//process each child
for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
if( it->first!=d_default ){
- it->second.simplify( m, n, depth+1 );
+ it->second.simplify( m, q, n, depth+1 );
if( it->second.d_value==defVal && it->second.d_value!=val_none ){
newDef = newDef | it->first;
to_erase.push_back( it->first );
@@ -101,7 +101,7 @@ void AbsDef::simplify( FirstOrderModelAbs * m, TNode n, unsigned depth ) { d_def.erase( d_default );
//set new default
d_default = newDef;
- d_def[d_default].construct_def_entry( m, n, defVal, depth+1 );
+ d_def[d_default].construct_def_entry( m, q, n, defVal, depth+1 );
//erase redundant entries
for( unsigned i=0; i<to_erase.size(); i++ ){
d_def.erase( to_erase[i] );
@@ -120,6 +120,11 @@ void AbsDef::debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const{ for( unsigned i=0; i<dSize; i++ ){
Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");
}
+ //Trace(c) << "(";
+ //for( unsigned i=0; i<32; i++ ){
+ // Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");
+ //}
+ //Trace(c) << ")";
}
void AbsDef::debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth ) const{
@@ -257,11 +262,12 @@ void AbsDef::construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector< }
}
-void AbsDef::construct_def_entry( FirstOrderModelAbs * m, TNode n, int v, unsigned depth ) {
+void AbsDef::construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth ) {
d_value = v;
if( depth<n.getNumChildren() ){
- unsigned dom = m->d_domain[n[depth].getType()];
- d_def[dom].construct_def_entry( m, n, v, depth+1 );
+ TypeNode tn = q.isNull() ? n[depth].getType() : m->getVariable( q, depth ).getType();
+ unsigned dom = m->d_domain[tn] ;
+ d_def[dom].construct_def_entry( m, q, n, v, depth+1 );
d_default = dom;
}
}
@@ -556,7 +562,7 @@ bool AbsDef::construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f, for( std::map< unsigned, int >::iterator it = bchildren.begin(); it !=bchildren.end(); ++it ){
if( ( it->second==0 && n.getKind()==AND ) ||
( it->second==1 && n.getKind()==OR ) ){
- construct_def_entry( m, q[0], it->second );
+ construct_def_entry( m, q, q[0], it->second );
return true;
}
}
@@ -654,11 +660,11 @@ bool AbsDef::isSimple( unsigned n ) { return (n & (n - 1))==0;
}
-unsigned AbsDef::getId( unsigned n, unsigned start ) {
+unsigned AbsDef::getId( unsigned n, unsigned start, unsigned end ) {
Assert( n!=0 );
while( (n & ( 1 << start )) == 0 ){
start++;
- if( start==32 ){
+ if( start==end ){
return start;
}
}
@@ -808,7 +814,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) { Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl;
it->second->debugPrint("ambqi-model-debug", fm, fapps[0] );
Trace("ambqi-model-debug") << "Simplifying " << f << "..." << std::endl;
- it->second->simplify( fm, fapps[0] );
+ it->second->simplify( fm, TNode::null(), fapps[0] );
Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl;
it->second->debugPrint("ambqi-model", fm, fapps[0] );
@@ -831,7 +837,7 @@ void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) { //do exhaustive instantiation
bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {
- Trace("ambqi-check") << "exhaustive instantiation " << q << " " << effort << std::endl;
+ Trace("ambqi-check") << "Exhaustive instantiation " << q << " " << effort << std::endl;
if (effort==0) {
FirstOrderModelAbs * fma = fm->asFirstOrderModelAbs();
bool quantValid = true;
@@ -843,6 +849,7 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in }
}
if( quantValid ){
+ Trace("ambqi-check") << "Compute interpretation..." << std::endl;
AbsDef ad;
doCheck( fma, q, ad, q[1] );
//now process entries
@@ -850,6 +857,7 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in Trace("ambqi-inst") << "Interpretation of " << q << " is : " << std::endl;
ad.debugPrint( "ambqi-inst", fma, q[0] );
Trace("ambqi-inst") << std::endl;
+ Trace("ambqi-check") << "Add instantiations..." << std::endl;
int lem = 0;
quantValid = ad.addInstantiations( fma, d_qe, q, lem );
Trace("ambqi-inst") << "...Added " << lem << " lemmas." << std::endl;
@@ -919,7 +927,7 @@ bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNod }
Trace("ambqi-check-try") << "Interpretation for " << n << " is : " << std::endl;
ad.debugPrint("ambqi-check-try", m, q[0] );
- ad.simplify( m, q[0] );
+ ad.simplify( m, q, q[0] );
Trace("ambqi-check-debug") << "(Simplified) Interpretation for " << n << " is : " << std::endl;
ad.debugPrint("ambqi-check-debug", m, q[0] );
Trace("ambqi-check-debug") << std::endl;
diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h index 784fa5093..349073cb4 100755 --- a/src/theory/quantifiers/ambqi_builder.h +++ b/src/theory/quantifiers/ambqi_builder.h @@ -36,7 +36,7 @@ private: std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,
std::vector< unsigned >& entry, std::vector< bool >& entry_def );
void construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth = 0 );
- void construct_def_entry( FirstOrderModelAbs * m, TNode n, int v, unsigned depth = 0 );
+ void construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth = 0 );
void apply_ucompose( FirstOrderModelAbs * m, TNode q,
std::vector< unsigned >& entry, std::vector< bool >& entry_def, std::vector< int >& terms,
std::map< unsigned, int >& vchildren, AbsDef * a, unsigned depth = 0 );
@@ -59,7 +59,7 @@ public: void construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth = 0 );
void debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const;
void debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth = 0 ) const;
- void simplify( FirstOrderModelAbs * m, TNode q, unsigned depth = 0 );
+ void simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth = 0 );
int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, int& inst ){
std::vector< Node > terms;
terms.resize( q[0].getNumChildren() );
@@ -73,7 +73,7 @@ public: void negate();
Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 );
static bool isSimple( unsigned n );
- static unsigned getId( unsigned n, unsigned start=0 );
+ static unsigned getId( unsigned n, unsigned start=0, unsigned end=32 );
Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args );
Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 );
//for debugging
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index e4b588ac1..3edf97467 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -102,7 +102,8 @@ Node FirstOrderModel::getSomeDomainElement(TypeNode tn){ if (!d_rep_set.hasType(tn)) { Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl; Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn); - d_rep_set.add(mbt); + Trace("fmc-model-debug") << "Add to representative set..." << std::endl; + d_rep_set.add(tn, mbt); }else if( d_rep_set.d_type_reps[tn].size()==0 ){ Message() << "empty reps" << std::endl; exit(0); @@ -986,7 +987,7 @@ void FirstOrderModelAbs::collectEqVars( TNode q, TNode n, std::map< int, bool >& for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( n.getKind()==EQUAL && n[i].getKind()==BOUND_VARIABLE ){ int v = getVariableId( q, n[i] ); - Assert( v>=0 && v<q.getNumChildren() ); + Assert( v>=0 && v<(int)q[0].getNumChildren() ); eq_vars[v] = true; } collectEqVars( q, n[i], eq_vars ); diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 0f3e53827..63df56392 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -61,7 +61,7 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) { return true; } } - if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !c[index].getType().isInteger() ){ + if( c[index].getType().isSort() ){ //for star: check if all children are defined and have generalizations if( c[index]==st ){ ///options::fmfFmcCoverSimplify() //check if all children exist and are complete @@ -537,7 +537,9 @@ void FullModelChecker::initializeType( FirstOrderModelFmc * fm, TypeNode tn ){ }else{ mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn); } + Trace("fmc") << "Get used rep for " << mbn << std::endl; Node mbnr = fm->getUsedRepresentative( mbn ); + Trace("fmc") << "...got " << mbnr << std::endl; fm->d_model_basis_rep[tn] = mbnr; Trace("fmc") << "Add model basis for type " << tn << " : " << mbn << " " << mbnr << std::endl; } diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 096d0cab2..703a44d03 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -198,18 +198,18 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No } } -void InstMatchTrie::print( const char * c, Node q, std::vector< Node >& terms ) const { +void InstMatchTrie::print( std::ostream& out, Node q, std::vector< Node >& terms ) const { if( terms.size()==q[0].getNumChildren() ){ - Trace(c) << " ( "; + out << " ( "; for( unsigned i=0; i<terms.size(); i++ ){ - if( i>0 ) Trace(c) << ", "; - Trace(c) << terms[i]; + if( i>0 ) out << ", "; + //out << terms[i]; } - Trace(c) << " )" << std::endl; + out << " )" << std::endl; }else{ for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ terms.push_back( it->first ); - it->second.print( c, q, terms ); + it->second.print( out, q, terms ); terms.pop_back(); } } @@ -282,19 +282,19 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< } } -void CDInstMatchTrie::print( const char * c, Node q, std::vector< Node >& terms ) const{ +void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< Node >& terms ) const{ if( d_valid.get() ){ if( terms.size()==q[0].getNumChildren() ){ - Trace(c) << " ( "; + out << " ( "; for( unsigned i=0; i<terms.size(); i++ ){ - if( i>0 ) Trace(c) << ", "; - Trace(c) << terms[i]; + if( i>0 ) out << ", "; + //out << terms[i]; } - Trace(c) << " )" << std::endl; + out << " )" << std::endl; }else{ for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ terms.push_back( it->first ); - it->second->print( c, q, terms ); + it->second->print( out, q, terms ); terms.pop_back(); } } diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 2cf63210b..accd3baed 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -101,7 +101,7 @@ public: /** the data */ std::map< Node, InstMatchTrie > d_data; private: - void print( const char * c, Node q, std::vector< Node >& terms ) const; + void print( std::ostream& out, Node q, std::vector< Node >& terms ) const; public: InstMatchTrie(){} ~InstMatchTrie(){} @@ -128,9 +128,9 @@ public: } bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false, bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ); - void print( const char * c, Node q ) const{ + void print( std::ostream& out, Node q ) const{ std::vector< Node > terms; - print( c, q, terms ); + print( out, q, terms ); } };/* class InstMatchTrie */ @@ -142,7 +142,7 @@ public: /** is valid */ context::CDO< bool > d_valid; private: - void print( const char * c, Node q, std::vector< Node >& terms ) const; + void print( std::ostream& out, Node q, std::vector< Node >& terms ) const; public: CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){} ~CDInstMatchTrie(){} @@ -169,9 +169,9 @@ public: } bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0, bool onlyExist = false ); - void print( const char * c, Node q ) const{ + void print( std::ostream& out, Node q ) const{ std::vector< Node > terms; - print( c, q, terms ); + print( out, q, terms ); } };/* class CDInstMatchTrie */ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 06858cf92..123dc02b6 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -210,7 +210,7 @@ void InstantiationEngine::check( Theory::Effort e ){ } ++(d_statistics.d_instantiation_rounds); bool quantActive = false; - Debug("quantifiers") << "quantifiers: check: asserted quantifiers size" + Debug("quantifiers") << "quantifiers: check: asserted quantifiers size=" << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl; for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node n = d_quantEngine->getModel()->getAssertedQuantifier( i ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 8fecc6ee0..a16f46ace 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -623,18 +623,20 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ } } -void QuantifiersEngine::printInstantiations( const char * c ) { - if( options::incrementalSolving() ){ - for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ - Trace(c) << "Instantiations of " << it->first << " : " << std::endl; - it->second->print( c, it->first ); - } - }else{ +void QuantifiersEngine::printInstantiations( std::ostream& out ) { + //Trace("ajr-temp") << "QE print inst." << std::endl; + //if( options::incrementalSolving() ){ + // for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ + // out << "Instantiations of " << it->first << " : " << std::endl; + // it->second->print( out, it->first ); + // } + //}else{ for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ - Trace(c) << "Instantiations of " << it->first << " : " << std::endl; - it->second.print( c, it->first ); + out << "Instantiations of " << it->first << " : " << std::endl; + it->second.print( out, it->first ); + out << std::endl; } - } + //} } QuantifiersEngine::Statistics::Statistics(): diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 7a899db0c..fa3c66f4f 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -236,7 +236,7 @@ public: eq::EqualityEngine* getMasterEqualityEngine() ; public: /** print instantiations */ - void printInstantiations( const char * c ); + void printInstantiations( std::ostream& out ); /** statistics class */ class Statistics { public: diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 2e8eb51b1..7dd8d02f6 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -37,10 +37,10 @@ int RepSet::getNumRepresentatives( TypeNode tn ) const{ } } -void RepSet::add( Node n ){ - TypeNode t = n.getType(); - d_tmap[ n ] = (int)d_type_reps[t].size(); - d_type_reps[t].push_back( n ); +void RepSet::add( TypeNode tn, Node n ){ + d_tmap[ n ] = (int)d_type_reps[tn].size(); + Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl; + d_type_reps[tn].push_back( n ); } int RepSet::getIndexFor( Node n ) const { @@ -59,7 +59,7 @@ void RepSet::complete( TypeNode t ){ while( !te.isFinished() ){ Node n = *te; if( std::find( d_type_reps[t].begin(), d_type_reps[t].end(), n )==d_type_reps[t].end() ){ - add( n ); + add( t, n ); } ++te; } @@ -143,7 +143,7 @@ bool RepSetIterator::initialize(){ if( !d_rep_set->hasType( tn ) ){ Node var = NodeManager::currentNM()->mkSkolem( "repSet", tn, "is a variable created by the RepSetIterator" ); Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; - d_rep_set->add( var ); + d_rep_set->add( tn, var ); } }else if( tn.isInteger() ){ bool inc = false; diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index a619915ee..c72e46e76 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -40,7 +40,7 @@ public: /** get cardinality for type */ int getNumRepresentatives( TypeNode tn ) const; /** add representative for type */ - void add( Node n ); + void add( TypeNode tn, Node n ); /** returns index in d_type_reps for node n */ int getIndexFor( Node n ) const; /** complete all values */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 18968e897..c63df83ee 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1179,6 +1179,12 @@ Node TheoryEngine::getModelValue(TNode var) { return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var); } +void TheoryEngine::printInstantiations( std::ostream& out ) { + if( d_quantEngine ){ + d_quantEngine->printInstantiations( out ); + } +} + static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) { std::set<TNode> all; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0495a866b..615598e44 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -759,6 +759,11 @@ public: Node getModelValue(TNode var); /** + * Print all instantiations made by the quantifiers module. + */ + void printInstantiations( std::ostream& out ); + + /** * Forwards an entailment check according to the given theoryOfMode. * See theory.h for documentation on entailmentCheck(). */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 7187a373f..203f116bb 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -737,7 +737,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) std::map< Node, Node >::iterator itMap; for (itMap = constantReps.begin(); itMap != constantReps.end(); ++itMap) { tm->d_reps[itMap->first] = itMap->second; - tm->d_rep_set.add(itMap->second); + tm->d_rep_set.add(itMap->second.getType(), itMap->second); } if (!fullModel) { @@ -745,14 +745,14 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) // Make sure every EC has a rep for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap ) { tm->d_reps[itMap->first] = itMap->second; - tm->d_rep_set.add(itMap->second); + tm->d_rep_set.add(itMap->second.getType(), itMap->second); } for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) { set<Node>& noRepSet = TypeSet::getSet(it); set<Node>::iterator i; for (i = noRepSet.begin(); i != noRepSet.end(); ++i) { tm->d_reps[*i] = *i; - tm->d_rep_set.add(*i); + tm->d_rep_set.add((*i).getType(), *i); } } } |