From 0b2f9943d55152e0958369083649dd71340864c9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 11 May 2014 14:36:50 -0500 Subject: 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. --- src/theory/theory_model.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/theory/theory_model.cpp') 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& noRepSet = TypeSet::getSet(it); set::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); } } } -- cgit v1.2.3