From: Morgan Deters Date: Fri, 24 Aug 2012 23:20:22 +0000 (+0000) Subject: disallow assertions to inactive theories. X-Git-Tag: cvc5-1.0.0~7847 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3619c784bd5dd4b91ab0a2ad429ea145636d3424;p=cvc5.git disallow assertions to inactive theories. this fixes at least one known bug where quantifiers could be asserted in quantifier-free logics, with incorrect results. --- 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;