diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 65 |
1 files changed, 59 insertions, 6 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index c7d200a90..ba80b130e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -2230,14 +2230,67 @@ void TheoryEngine::checkTheoryAssertionsWithModel() { std::pair<bool, Node> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* seffects) { TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit; - theory::TheoryId tid = theory::Theory::theoryOf(mode, atom); - theory::Theory* th = theoryOf(tid); + if( atom.getKind()==kind::AND || atom.getKind()==kind::OR || atom.getKind()==kind::IMPLIES ){ + //Boolean connective, recurse + std::vector< Node > children; + bool pol = (lit.getKind()!=kind::NOT); + bool is_conjunction = pol==(lit.getKind()==kind::AND); + for( unsigned i=0; i<atom.getNumChildren(); i++ ){ + Node ch = atom[i]; + if( pol==( lit.getKind()==kind::IMPLIES && i==0 ) ){ + ch = atom[i].negate(); + } + std::pair<bool, Node> chres = entailmentCheck( mode, ch, params, seffects ); + if( chres.first ){ + if( !is_conjunction ){ + return chres; + }else{ + children.push_back( chres.second ); + } + }else if( !chres.first && is_conjunction ){ + return std::pair<bool, Node>(false, Node::null()); + } + } + if( is_conjunction ){ + return std::pair<bool, Node>(true, NodeManager::currentNM()->mkNode(kind::AND, children)); + }else{ + return std::pair<bool, Node>(false, Node::null()); + } + }else if( atom.getKind()==kind::ITE || ( atom.getKind()==kind::EQUAL && atom[0].getType().isBoolean() ) ){ + bool pol = (lit.getKind()!=kind::NOT); + for( unsigned r=0; r<2; r++ ){ + Node ch = atom[0]; + if( r==1 ){ + ch = ch.negate(); + } + std::pair<bool, Node> chres = entailmentCheck( mode, ch, params, seffects ); + if( chres.first ){ + Node ch2 = atom[ atom.getKind()==kind::ITE ? r+1 : 1 ]; + if( pol==( atom.getKind()==kind::ITE ? true : r==1 ) ){ + ch2 = ch2.negate(); + } + std::pair<bool, Node> chres2 = entailmentCheck( mode, ch2, params, seffects ); + if( chres2.first ){ + return std::pair<bool, Node>(true, NodeManager::currentNM()->mkNode(kind::AND, chres.second, chres2.second)); + }else{ + break; + } + } + } + return std::pair<bool, Node>(false, Node::null()); + }else{ + //it is a theory atom + theory::TheoryId tid = theory::Theory::theoryOf(mode, atom); + theory::Theory* th = theoryOf(tid); - Assert(th != NULL); - Assert(params == NULL || tid == params->getTheoryId()); - Assert(seffects == NULL || tid == seffects->getTheoryId()); + Assert(th != NULL); + Assert(params == NULL || tid == params->getTheoryId()); + Assert(seffects == NULL || tid == seffects->getTheoryId()); + Trace("theory-engine-entc") << "Entailment check : " << lit << std::endl; - return th->entailmentCheck(lit, params, seffects); + std::pair<bool, Node> chres = th->entailmentCheck(lit, params, seffects); + return chres; + } } void TheoryEngine::spendResource(unsigned ammount) { |