From: Clark Barrett Date: Fri, 26 Oct 2012 02:37:38 +0000 (+0000) Subject: More bug fixes and more checks for models X-Git-Tag: cvc5-1.0.0~7669 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ddd3797ee72443bd35f6cea146c3752ea0dd2286;p=cvc5.git More bug fixes and more checks for models --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3813f964d..55ac15ebc 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -712,11 +712,22 @@ void SmtEngine::setLogicInternal() throw() { if(! options::unconstrainedSimp.wasSetByUser() || options::incrementalSolving()) { // bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified(); // bool uncSimp = false && !qf_sat && !options::incrementalSolving(); - bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() && + bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() && !options::produceModels() && (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV)); Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl; options::unconstrainedSimp.set(uncSimp); } + // Unconstrained simp currently does *not* support model generation + if (options::unconstrainedSimp.wasSetByUser() && options::unconstrainedSimp()) { + if (options::produceModels()) { + Notice() << "SmtEngine: turning off produce-models to support unconstrainedSimp" << std::endl; + setOption("produce-models", SExpr("false")); + } + if (options::checkModels()) { + Notice() << "SmtEngine: turning off check-models to support unconstrainedSimp" << std::endl; + setOption("check-models", SExpr("false")); + } + } // Turn on arith rewrite equalities only for pure arithmetic if(! options::arithRewriteEq.wasSetByUser()) { bool arithRewriteEq = d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified(); @@ -1494,6 +1505,11 @@ bool SmtEnginePrivate::nonClausalSimplify() { SubstitutionMap::iterator pos = constantPropagations.begin(); for (; pos != constantPropagations.end(); ++pos) { Node cProp = (*pos).first.eqNode((*pos).second); + Node cPropNew = d_topLevelSubstitutions.apply(cProp); + if (cProp != cPropNew) { + cProp = Rewriter::rewrite(cPropNew); + Assert(Rewriter::rewrite(cProp) == cProp); + } if (s.find(cProp) != s.end()) { continue; } @@ -2343,6 +2359,10 @@ void SmtEngine::checkModel(bool hardFailure) { Notice() << "SmtEngine::checkModel(): generating model" << endl; TheoryModel* m = d_theoryEngine->getModel(); + + // Check individual theory assertions + d_theoryEngine->checkTheoryAssertionsWithModel(); + if(Notice.isOn()) { // This operator<< routine is non-const (i.e., takes a non-const Model&). // This confuses the Notice() output routines, so extract the ostream diff --git a/src/theory/model.cpp b/src/theory/model.cpp index aa2de656e..452317f5b 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -75,6 +75,7 @@ Cardinality TheoryModel::getCardinality( Type t ) const{ } Node TheoryModel::getModelValue( TNode n ) const{ + Assert(n.getKind() != kind::FORALL && n.getKind() != kind::EXISTS && n.getKind() != kind::LAMBDA); if( n.isConst() ) { return n; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f24b11c41..d5c4998d4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1338,8 +1338,28 @@ void TheoryEngine::setUserAttribute( std::string& attr, Node n ){ } } + void TheoryEngine::handleUserAttribute( const char* attr, Theory* t ){ Trace("te-attr") << "Handle user attribute " << attr << " " << t << std::endl; std::string str( attr ); d_attr_handle[ str ].push_back( t ); } + + +void TheoryEngine::checkTheoryAssertionsWithModel() +{ + for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { + Theory* theory = d_theoryTable[theoryId]; + if (theory && d_logicInfo.isTheoryEnabled(theoryId)) { + if (theoryId == THEORY_QUANTIFIERS || theoryId == THEORY_REWRITERULES) { + continue; + } + context::CDList::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); + for (unsigned i = 0; it != it_end; ++ it, ++i) { + Node assertion = (*it).assertion; + Node val = getModel()->getValue(assertion); + Assert(val == d_true); + } + } + } +} diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index d542d0dd7..8331ef61d 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -710,6 +710,11 @@ public: */ void handleUserAttribute( const char* attr, theory::Theory* t ); + /** Check that the theory assertions are satisfied in the model + * This function is called from the smt engine's checkModel routine + */ + void checkTheoryAssertionsWithModel(); + };/* class TheoryEngine */ }/* CVC4 namespace */