First chunk of boolean-terms support.

Passes simple tests and doesn't break existing functionality.
Still need some work merged in for models.

This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV).  Tonight's nightly regression run should tell us if/how that hurts performance.

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 9 insertions, 3 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 60d79e90e..42fe10cb9 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -694,7 +694,9 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMa
     stringstream ss;
     ss << "The logic was specified as " << d_logicInfo.getLogicString()
        << ", which doesn't include " << Theory::theoryOf(atom)
-       << ", but got an asserted fact to that theory";
+       << ", but got a preprocessing-time fact for that theory." << endl
+       << "The fact:" << endl
+       << literal;
     throw LogicException(ss.str());
   }
 
@@ -792,7 +794,9 @@ Node TheoryEngine::preprocess(TNode assertion) {
       stringstream ss;
       ss << "The logic was specified as " << d_logicInfo.getLogicString()
          << ", which doesn't include " << Theory::theoryOf(current)
-         << ", but got an asserted fact to that theory";
+         << ", but got a preprocesing-time fact for that theory." << endl
+         << "The fact:" << endl
+         << current;
       throw LogicException(ss.str());
     }
 
@@ -882,7 +886,9 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId,
     stringstream ss;
     ss << "The logic was specified as " << d_logicInfo.getLogicString()
        << ", which doesn't include " << toTheoryId
-       << ", but got an asserted fact to that theory";
+       << ", but got an asserted fact to that theory." << endl
+       << "The fact:" << endl
+       << assertion;
     throw LogicException(ss.str());
   }