diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-27 19:27:45 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-27 19:27:45 +0000 |
| commit | 9a994c449d65e64d574a423ad9caad519f8c2148 (patch) | |
| tree | 3c4571098d1771f8d277406c9f6e9c5b09dcd1da /src/theory/theory_engine.cpp | |
| parent | 4bfa927dac67bbcadf219f70e61f1d123e33944b (diff) | |
merging fmf-devel branch, includes refactored datatype theory, updates to model.h/cpp to prepare for release, and major refactoring of quantifiers/finite model finding. Note that new datatype theory does not insist upon any interpretation for selectors applied to incorrect constructors and consequently some answers may differ with previous version
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 872924385..1fb7305d4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -86,7 +86,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_quantEngine = new QuantifiersEngine(context, this); //build model information if applicable - d_curr_model = new theory::DefaultModel( context, "DefaultModel" ); + d_curr_model = new theory::DefaultModel( context, "DefaultModel", false ); d_curr_model_builder = new theory::TheoryEngineModelBuilder( this ); Rewriter::init(); @@ -409,8 +409,8 @@ void TheoryEngine::combineTheories() { Assert(d_sharedTerms.isShared(carePair.a) || carePair.a.isConst()); Assert(d_sharedTerms.isShared(carePair.b) || carePair.b.isConst()); - Assert(!d_sharedTerms.areEqual(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); - Assert(!d_sharedTerms.areDisequal(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); + //AJR-temp Assert(!d_sharedTerms.areEqual(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); + //AJR-temp Assert(!d_sharedTerms.areDisequal(carePair.a, carePair.b), "Please don't care about stuff you were notified about"); // The equality in question Node equality = carePair.a < carePair.b ? |