From 3619c784bd5dd4b91ab0a2ad429ea145636d3424 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 24 Aug 2012 23:20:22 +0000
Subject: [PATCH] disallow assertions to inactive theories.

this fixes at least one known bug where quantifiers could be asserted in quantifier-free logics, with incorrect results.
---
 src/theory/theory_engine.cpp | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d4e1c89c5..7a67012a2 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -676,6 +676,16 @@ void TheoryEngine::shutdown() {
 theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) {
   TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
   Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
+
+  if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(atom)) &&
+     Theory::theoryOf(atom) != THEORY_SAT_SOLVER) {
+    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";
+    throw Exception(ss.str());
+  }
+
   Theory::PPAssertStatus solveStatus = theoryOf(atom)->ppAssert(literal, substitutionOut);
   Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl;
   return solveStatus;
@@ -755,6 +765,15 @@ Node TheoryEngine::preprocess(TNode assertion) {
       continue;
     }
 
+    if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(current)) &&
+       Theory::theoryOf(current) != THEORY_SAT_SOLVER) {
+      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";
+      throw Exception(ss.str());
+    }
+
     // If this is an atom, we preprocess its terms with the theory ppRewriter
     if (Theory::theoryOf(current) != THEORY_BOOL) {
       d_ppCache[current] = ppTheoryRewrite(current);
@@ -836,6 +855,14 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId,
   Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << std::endl;
 
   Assert(toTheoryId != fromTheoryId);
+  if(! d_logicInfo.isTheoryEnabled(toTheoryId) &&
+     toTheoryId != THEORY_SAT_SOLVER) {
+    stringstream ss;
+    ss << "The logic was specified as " << d_logicInfo.getLogicString()
+       << ", which doesn't include " << toTheoryId
+       << ", but got an asserted fact to that theory";
+    throw Exception(ss.str());
+  }
 
   if (d_inConflict) {
     return;
-- 
2.30.2