diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 54 |
1 files changed, 31 insertions, 23 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 2782badcb..0adb592f2 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -998,11 +998,13 @@ void TheoryEngine::postsolve() { #ifdef CVC4_FOR_EACH_THEORY_STATEMENT #undef CVC4_FOR_EACH_THEORY_STATEMENT #endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::hasPostsolve) { \ - theoryOf(THEORY)->postsolve(); \ - Assert(! d_inConflict || wasInConflict, "conflict raised during postsolve()"); \ - } +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::hasPostsolve) \ + { \ + theoryOf(THEORY)->postsolve(); \ + Assert(!d_inConflict || wasInConflict) \ + << "conflict raised during postsolve()"; \ + } // Postsolve for each theory using the statement above CVC4_FOR_EACH_THEORY; @@ -1317,7 +1319,8 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo // If sending to the shared terms database, it's also simple if (toTheoryId == THEORY_BUILTIN) { - Assert(atom.getKind() == kind::EQUAL, "atom should be an EQUALity, not `%s'", atom.toString().c_str()); + Assert(atom.getKind() == kind::EQUAL) + << "atom should be an EQUALity, not `" << atom << "'"; if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) { d_sharedTerms.assertEquality(atom, polarity, assertion); } @@ -1561,7 +1564,7 @@ void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) if( d_quantEngine ){ d_quantEngine->getInstantiatedQuantifiedFormulas( qs ); }else{ - Assert( false ); + Assert(false); } } @@ -1569,7 +1572,7 @@ void TheoryEngine::getInstantiations( Node q, std::vector< Node >& insts ) { if( d_quantEngine ){ d_quantEngine->getInstantiations( q, insts ); }else{ - Assert( false ); + Assert(false); } } @@ -1577,7 +1580,7 @@ void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector if( d_quantEngine ){ d_quantEngine->getInstantiationTermVectors( q, tvecs ); }else{ - Assert( false ); + Assert(false); } } @@ -1585,7 +1588,7 @@ void TheoryEngine::getInstantiations( std::map< Node, std::vector< Node > >& ins if( d_quantEngine ){ d_quantEngine->getInstantiations( insts ); }else{ - Assert( false ); + Assert(false); } } @@ -1593,7 +1596,7 @@ void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std if( d_quantEngine ){ d_quantEngine->getInstantiationTermVectors( insts ); }else{ - Assert( false ); + Assert(false); } } @@ -1601,7 +1604,7 @@ Node TheoryEngine::getInstantiatedConjunction( Node q ) { if( d_quantEngine ){ return d_quantEngine->getInstantiatedConjunction( q ); }else{ - Assert( false ); + Assert(false); return Node::null(); } } @@ -1792,8 +1795,9 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The } continue; }else if( eqNormalized.getKind() != kind::EQUAL){ - Assert( eqNormalized.getKind()==kind::BOOLEAN_TERM_VARIABLE || - ( eqNormalized.getKind()==kind::NOT && eqNormalized[0].getKind()==kind::BOOLEAN_TERM_VARIABLE ) ); + Assert(eqNormalized.getKind() == kind::BOOLEAN_TERM_VARIABLE + || (eqNormalized.getKind() == kind::NOT + && eqNormalized[0].getKind() == kind::BOOLEAN_TERM_VARIABLE)); // this happens for Boolean term equalities V = true that are rewritten to V, we should skip // TODO : revisit this continue; @@ -2125,7 +2129,8 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector } Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << endl; - Assert( explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially"); + Assert(explanation != toExplain.node) + << "wasn't sent to you, so why are you explaining it trivially"; // Mark the explanation NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp); explanationVector.push_back(newExplain); @@ -2217,14 +2222,17 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) { ++it) { Node assertion = (*it).assertion; Node val = getModel()->getValue(assertion); - if(val != d_true) { - stringstream ss; - ss << theoryId << " has an asserted fact that the model doesn't satisfy." << endl - << "The fact: " << assertion << endl - << "Model value: " << val << endl; - if(hardFailure) { - InternalError(ss.str()); - } + if (val != d_true) + { + if (hardFailure) + { + InternalError() + << theoryId + << " has an asserted fact that the model doesn't satisfy." + << endl + << "The fact: " << assertion << endl + << "Model value: " << val << endl; + } } } } |