From 89b0369e887b4cf876e95dc862ae3057383370f3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 29 Apr 2011 22:03:59 +0000 Subject: [PATCH] refactoring to datatypes theory, added working prototype for proof/explanation manager --- src/theory/datatypes/Makefile.am | 4 +- src/theory/datatypes/explanation_manager.cpp | 81 +++ src/theory/datatypes/explanation_manager.h | 220 ++++++ src/theory/datatypes/theory_datatypes.cpp | 680 +++++++++---------- src/theory/datatypes/theory_datatypes.h | 40 +- 5 files changed, 646 insertions(+), 379 deletions(-) create mode 100644 src/theory/datatypes/explanation_manager.cpp create mode 100644 src/theory/datatypes/explanation_manager.h diff --git a/src/theory/datatypes/Makefile.am b/src/theory/datatypes/Makefile.am index 69d83faf4..f8bfa3dc5 100644 --- a/src/theory/datatypes/Makefile.am +++ b/src/theory/datatypes/Makefile.am @@ -11,6 +11,8 @@ libdatatypes_la_SOURCES = \ datatypes_rewriter.h \ theory_datatypes.cpp \ union_find.h \ - union_find.cpp + union_find.cpp \ + explanation_manager.h \ + explanation_manager.cpp EXTRA_DIST = kinds diff --git a/src/theory/datatypes/explanation_manager.cpp b/src/theory/datatypes/explanation_manager.cpp new file mode 100644 index 000000000..424ca8fac --- /dev/null +++ b/src/theory/datatypes/explanation_manager.cpp @@ -0,0 +1,81 @@ +#include "theory/datatypes/explanation_manager.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::datatypes; + +void ProofManager::setExplanation( Node n, Node jn, unsigned r ) +{ + d_exp[n] = std::pair< Node, unsigned >( jn, r ); +} + +//std::ostream& operator<<(std::ostream& os, Reason::Rule r) +//{ +// switch( r ){ +// +// } +//} + +void ExplanationManager::process( Node n, NodeBuilder<>& nb, ProofManager* pm ) +{ + if( n.getKind()==kind::AND ){ + for( int i=0; i<(int)n.getNumChildren(); i++ ) { + process( n[i], nb, pm ); + } + }else{ + if( !pm->hasExplained( n ) ){ + context::CDMap< Node, Reason, NodeHashFunction >::iterator it = d_drv_map.find( n ); + Reason r; + Node exp; + if( it!=d_drv_map.end() ){ + r = (*it).second; + if( r.d_e ){ + Debug("emanager") << "Em::process: Consult externally for " << n << std::endl; + exp = r.d_e->explain( n, pm ); + //trivial case, r says that n is an input + if( exp==n ){ + r.d_isInput = true; + } + }else if( !r.d_isInput ){ + exp = r.d_node; + pm->setExplanation( n, exp, r.d_reason ); + if( exp.isNull() ) Debug("emanager") << "Em::process: " << n << " is an axiom, reason = " << r.d_reason << endl; + } + } + + if( r.d_isInput ){ + Debug("emanager") << "Em::process: " << n << " is an input " << endl; + nb << n; + pm->setExplanation( n, Node::null(), Reason::input ); + }else if( !exp.isNull() ){ + Debug("emanager") << "Em::process: " << exp << " is the explanation for " << n << " " + << ", reason = " << pm->getReason( n ) << endl; + if( exp.getKind()==kind::AND ){ + for( int i=0; i<(int)exp.getNumChildren(); i++ ) { + process( exp[i], nb, pm ); + } + }else{ + process( exp, nb, pm ); + } + } + }else{ + Debug("emanager") << "Em::process: proof manager has already explained " << n << endl; + } + } +} + +Node ExplanationManager::explain( Node n, ProofManager* pm ) +{ + NodeBuilder<> nb(kind::AND); + if( pm ){ + pm->clear(); + process( n, nb, pm ); + }else{ + ProofManager pm; + process( n, nb, &pm ); + } + return ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; +} diff --git a/src/theory/datatypes/explanation_manager.h b/src/theory/datatypes/explanation_manager.h new file mode 100644 index 000000000..d16f48b01 --- /dev/null +++ b/src/theory/datatypes/explanation_manager.h @@ -0,0 +1,220 @@ +/********************* */ +/*! \file explanation_manager.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Theory of datatypes. + ** + ** Theory of datatypes. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__DATATYPES__EXPLANATION_MANAGER_H +#define __CVC4__THEORY__DATATYPES__EXPLANATION_MANAGER_H + +#include "theory/theory.h" +#include "util/congruence_closure.h" +#include "util/datatype.h" +#include "util/hash.h" +#include "util/trans_closure.h" + +#include +#include +#include + +namespace CVC4 { +namespace theory { +namespace datatypes { + + +class Explainer; + +/** reason class */ +class Reason { +public: + enum Rule { + unspecified = 0, + contradiction = 1, + + cc_coarse, + + //unification rules + idt_unify, + idt_cycle, + idt_clash, + //tester rules + idt_taxiom, + idt_tcong, + idt_tclash, + idt_texhaust, + //other rules + idt_inst, + idt_collapse, + idt_collapse2, + + input, + }; +public: + Reason() : d_e( NULL ), d_isInput( true ){} + Reason( Node n, unsigned r ) : d_node( n ), d_reason( r ), d_e( NULL ), d_isInput( false ) {} + Reason( Explainer* e ) : d_reason( 0 ), d_e( e ), d_isInput( false ){} + virtual ~Reason(){} + Node d_node; + unsigned d_reason; + Explainer* d_e; + bool d_isInput; +}; + +/** proof manager for theory lemmas */ +class ProofManager { +protected: + enum Effort { + MIN_EFFORT = 0, + STANDARD = 50, + FULL_EFFORT = 100 + };/* enum Effort */ + /** map from nodes to a description of how they are explained */ + std::map< Node, std::pair< Node, unsigned > > d_exp; + /** whether to produce proofs */ + Effort d_effort; +public: + ProofManager( Effort effort = STANDARD ) : d_effort( effort ){} + ~ProofManager(){} + void setExplanation( Node n, Node jn, unsigned r = 0 ); + bool hasExplained( Node n ) { return d_exp.find( n )!=d_exp.end(); } + Effort getEffort() { return d_effort; } + void clear() { d_exp.clear(); } + /** for debugging */ + Node getJustification( Node n ) { return d_exp[n].first; } + unsigned getReason( Node n ) { return d_exp[n].second; } +}; + +class Explainer +{ +public: + /** assert that n is true */ + virtual void assert( Node n ) = 0; + /** get the explanation for n. + This should call pm->setExplanation( n1, jn1, r1 ) ... pm->setExplanation( nk, jnk, rk ) + for some set of Nodes n1...nk. + Satisfies post conditions: + - If pm->getEffort() = MAX_EFFORT, then each ( ni, jni, ri ) should be a precise + application or rule ri, i.e. applying proof rule ri to jni derives ni. + - If pm->getEffort() = STANDARD, then for each ( ni, jni, ri ), + jni is the (at least informal) justification for ni. + - Return value should be a conjunction of nodes n'1...n'k, where each n'i occurs + (as a conjunct) in jn1...jnk, but not in n1...nk. + For each of these literals n'i, assert( n'i ) was called previously, + - either pm->setExplanation( n, ... ) is called, or n is the return value + */ + virtual Node explain( Node n, ProofManager* pm ) = 0; +}; + +template +class CongruenceClosureExplainer : public Explainer +{ +protected: + //pointer to the congruence closure module + CongruenceClosure* d_cc; +public: + CongruenceClosureExplainer(CongruenceClosure* cc) : + Explainer(), + d_cc( cc ){ + } + ~CongruenceClosureExplainer(){} + /** assert that n is true */ + void assert( Node n ){ + Assert( n.getKind() == kind::EQUAL ); + d_cc->addEquality( n ); + } + /** get the explanation for n */ + Node explain( Node n, ProofManager* pm ){ + Assert( n.getKind() == kind::EQUAL ); + if( pm->getEffort()==ProofManager::FULL_EFFORT ){ + //unsupported + Assert( false ); + return Node::null(); + }else{ + Node exp = d_cc->explain( n[0], n[1] ); + if( exp!=n ){ + pm->setExplanation( n, exp, Reason::cc_coarse ); + } + return exp; + } + } +}; + + +class ExplanationManager : public Explainer +{ +private: + /** map from nodes and the reason for them */ + context::CDMap< Node, Reason, NodeHashFunction > d_drv_map; + /** has conflict */ + context::CDO< bool > d_hasConflict; + /** process the reason for node n */ + void process( Node n, NodeBuilder<>& nb, ProofManager* pm ); +public: + ExplanationManager(context::Context* c) : Explainer(), d_drv_map(c), d_hasConflict( c, false ){} + ~ExplanationManager(){} + + /** assert that n is true (n is an input) */ + void assert( Node n ) { + //TODO: this can be optimized: + // if the previous explanation for n was empty (n is a tautology), + // then we should not claim it to be an input. + Reason r = d_drv_map[n]; + r.d_isInput = true; + } + /** n is explained */ + bool hasNode( Node n ) { return d_drv_map.find( n )!=d_drv_map.end(); } + /** n is explained */ + bool hasConflict() { return d_hasConflict.get() || hasNode( NodeManager::currentNM()->mkConst(false) ); } + /** jn is why n is true, by reason r */ + void addNode( Node n, Node jn, unsigned r = 0 ) { + if( !hasNode( n ) ){ + Assert( n!=jn ); + Debug("emanager") << "em::addNode: (" << jn << ", " << r << ") -> " << n << std::endl; + d_drv_map[n] = Reason( jn, r ); + } + } + /** Explainer e can tell you why n is true in the current state. */ + void addNode( Node n, Explainer* e ) { + if( !hasNode( n ) ){ + Debug("emanager") << "em::addNodeEx: (" << e << ") -> " << n << std::endl; + d_drv_map[n] = Reason( e ); + } + } + /** n is true by reason (axiom) r */ + void addNodeAxiom( Node n, unsigned r = 0 ) { addNode( n, Node::null(), r ); } + /** conclude a contradiction by jn and reason r */ + void addNodeConflict( Node jn, unsigned r = 0 ){ + addNode( NodeManager::currentNM()->mkConst(false), jn, r ); + d_hasConflict.set( true ); + } + /** get explanation for n + Requires pre conditions: TBD + Satisfies post conditions: TBD + */ + Node explain( Node n, ProofManager* pm = NULL ); + /** get conflict */ + Node getConflict( ProofManager* pm = NULL ){ + return explain( NodeManager::currentNM()->mkConst(false), pm ); + } +}; + + +} +} +} + +#endif \ No newline at end of file diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 88667de8d..1c901f38e 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -59,8 +59,6 @@ TheoryDatatypes::TheoryDatatypes(Context* c, OutputChannel& out, Valuation valua Theory(THEORY_DATATYPES, c, out, valuation), d_currAsserts(c), d_currEqualities(c), - d_drv_map(c), - d_axioms(c), d_selectors(c), d_reps(c), d_selector_eq(c), @@ -73,10 +71,10 @@ TheoryDatatypes::TheoryDatatypes(Context* c, OutputChannel& out, Valuation valua d_cc(c, &d_ccChannel), d_unionFind(c), d_disequalities(c), - d_equalities(c), - d_conflict(), d_noMerge(false), - d_inCheck(false){ + d_inCheck(false), + d_em(c), + d_cce(&d_cc){ ////bug test for transitive closure //TransitiveClosure tc( c ); @@ -98,20 +96,13 @@ void TheoryDatatypes::addSharedTerm(TNode t) { void TheoryDatatypes::notifyEq(TNode lhs, TNode rhs) { Debug("datatypes") << "TheoryDatatypes::notifyEq(): " << lhs << " = " << rhs << endl; - //if(!d_conflict.isNull()) { - // return; - //} - //merge(lhs,rhs); - //FIXME - //Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, lhs, rhs); - //addEquality(eq); - //d_drv_map[eq] = d_cc.explain( lhs, rhs ); + } void TheoryDatatypes::notifyCongruent(TNode lhs, TNode rhs) { Debug("datatypes") << "TheoryDatatypes::notifyCongruent(): " << lhs << " = " << rhs << endl; - if(d_conflict.isNull()) { + if(!hasConflict()) { merge(lhs,rhs); } Debug("datatypes-debug") << "TheoryDatatypes::notifyCongruent(): done." << endl; @@ -137,7 +128,8 @@ void TheoryDatatypes::check(Effort e) { while(!done()) { Node assertion = get(); - if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || Debug.isOn("datatypes-cycles") ) { + if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || Debug.isOn("datatypes-cycles") + || Debug.isOn("datatypes-debug-pf") ) { cout << "*** TheoryDatatypes::check(): " << assertion << endl; d_currAsserts.push_back( assertion ); } @@ -145,10 +137,10 @@ void TheoryDatatypes::check(Effort e) { //clear from the derived map d_inCheck = true; collectTerms( assertion ); - if( d_conflict.isNull() ){ - if( !d_drv_map[assertion].get().isNull() ) { + if( !hasConflict() ){ + if( d_em.hasNode( assertion ) ){ Debug("datatypes") << "Assertion has already been derived" << endl; - d_drv_map[assertion] = Node::null(); + d_em.assert( assertion ); } else { switch(assertion.getKind()) { case kind::EQUAL: @@ -156,7 +148,7 @@ void TheoryDatatypes::check(Effort e) { addEquality(assertion); break; case kind::APPLY_TESTER: - checkTester( assertion ); + addTester( assertion ); break; case kind::NOT: { @@ -176,16 +168,17 @@ void TheoryDatatypes::check(Effort e) { << " find(b) == > " << debugFind(b) << endl; } // There are two ways to get a conflict here. - if(d_conflict.isNull()) { + if(!hasConflict()) { if(find(a) == find(b)) { // We get a conflict this way if we WERE previously watching // a, b and were notified previously (via notifyCongruent()) // that they were congruent. - NodeBuilder<> nb(kind::AND); - nb << d_cc.explain( assertion[0][0], assertion[0][1] ); - nb << assertion; - d_conflict = nb; - Debug("datatypes") << "Disequality conflict " << d_conflict << endl; + Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, assertion[0][0], assertion[0][1] ); + NodeBuilder<> nbc(kind::AND); + nbc << ccEq << assertion; + Node contra = nbc; + d_em.addNode( ccEq, &d_cce ); + d_em.addNodeConflict( contra, Reason::contradiction ); } else { // If we get this far, there should be nothing conflicting due // to this disequality. @@ -195,7 +188,7 @@ void TheoryDatatypes::check(Effort e) { } break; case kind::APPLY_TESTER: - checkTester( assertion ); + addTester( assertion ); break; default: Unhandled(assertion[0].getKind()); @@ -209,9 +202,19 @@ void TheoryDatatypes::check(Effort e) { } } } + Debug("datatypes-debug-pf") << "Done check " << assertion << " " << hasConflict() << std::endl; d_inCheck = false; - if(!d_conflict.isNull()) { - throwConflict(); + if( hasConflict() ) { + Debug("datatypes-conflict") << "Constructing conflict..." << endl; + Node conflict = d_em.getConflict(); + if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || + Debug.isOn("datatypes-cycles") || Debug.isOn("datatypes-conflict") ){ + cout << "Conflict constructed : " << conflict << endl; + } + //if( conflict.getKind()!=kind::AND ){ + // conflict = NodeManager::currentNM()->mkNode(kind::AND, conflict, conflict); + //} + d_out->conflict( conflict, false ); return; } } @@ -222,20 +225,56 @@ void TheoryDatatypes::check(Effort e) { for( EqLists::iterator i = d_labels.begin(); i != d_labels.end(); i++ ) { Node sf = find( (*i).first ); if( sf == (*i).first || sf.getKind() != APPLY_CONSTRUCTOR ) { + addTermToLabels( sf ); EqList* lbl = (sf == (*i).first) ? (*i).second : (*d_labels.find( sf )).second; - Debug("datatypes-split") << "Check for splitting " << (*i).first << ", "; - Debug("datatypes-split") << "label size = " << lbl->size() << endl; - Node cons = getPossibleCons( (*i).first, false ); - if( !cons.isNull() ) { - const Datatype::Constructor& cn = getConstructor( cons ); - Debug("datatypes-split") << "*************Split for possible constructor " << cons << endl; - Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), (*i).first ); - NodeBuilder<> nb(kind::OR); - nb << test << test.notNode(); - Node lemma = nb; - Debug("datatypes-split") << "Lemma is " << lemma << endl; - d_out->lemma( lemma ); - return; + Debug("datatypes-split") << "Check for splitting " << (*i).first + << ", label size = " << lbl->size() << endl; + if( lbl->empty() || (*lbl)[ lbl->size()-1 ].getKind() == NOT ) { + TypeNode typ = sf.getType(); + const Datatype& dt = ((DatatypeType)typ.toType()).getDatatype(); + vector< bool > possibleCons; + possibleCons.resize( dt.getNumConstructors(), true ); + for( EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) { + TNode leqn = (*j); + possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false; + } + Node cons; + bool foundSel = false; + for( unsigned int j=0; jmkNode( APPLY_SELECTOR, Node::fromExpr( dt[j][k].getSelector() ), sf ); + if( d_selectors.find( s ) != d_selectors.end() ) { + Debug("datatypes") << " getPosCons: found selector " << s << endl; + foundSel = true; + break; + } + } + } + } + if( !foundSel ){ + for( unsigned int j=0; j<(int)possibleCons.size(); j++ ) { + if( possibleCons[j] && !dt[ j ].isFinite() ) { + Debug("datatypes") << "Did not find selector for " << sf + << " and " << dt[ j ].getConstructor() << " is not finite." << endl; + cons = Node::null(); + break; + } + } + } + if( !cons.isNull() ) { + const Datatype::Constructor& cn = getConstructor( cons ); + Debug("datatypes-split") << "*************Split for possible constructor " << cons << endl; + Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), (*i).first ); + NodeBuilder<> nb(kind::OR); + nb << test << test.notNode(); + Node lemma = nb; + Debug("datatypes-split") << "Lemma is " << lemma << endl; + d_out->lemma( lemma ); + return; + } } } else { Debug("datatypes-split") << (*i).first << " is " << sf << endl; @@ -247,127 +286,132 @@ void TheoryDatatypes::check(Effort e) { } } -void TheoryDatatypes::checkTester( Node assertion, bool doAdd ) { +bool TheoryDatatypes::checkTester( Node assertion, Node& conflict, unsigned& r ){ Debug("datatypes") << "Check tester " << assertion << endl; + //preprocess the tester Node tassertion = ( assertion.getKind() == NOT ) ? assertion[0] : assertion; - const Datatype& dt = Datatype::datatypeOf( tassertion.getOperator().toExpr() ); + Assert( find( tassertion[0] ) == tassertion[0] ); + + //if argument is a constructor, it is trivial + if( tassertion[0].getKind() == APPLY_CONSTRUCTOR ) { + size_t tIndex = Datatype::indexOf(tassertion.getOperator().toExpr()); + size_t cIndex = Datatype::indexOf(tassertion[0].getOperator().toExpr()); + if( (tIndex==cIndex) == (assertion.getKind() == NOT) ) { + conflict = assertion; + r = Reason::idt_tclash; + } + return false; + } + addTermToLabels( tassertion[0] ); + EqLists::iterator lbl_i = d_labels.find( tassertion[0] ); + EqList* lbl = (*lbl_i).second; + Assert( !lbl->empty() || lbl->begin()==lbl->end() ); + //check if empty label (no possible constructors for term) + bool redundant = false; + for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { + Node leqn = (*i); + if( leqn.getKind() == kind::NOT ) { + if( leqn[0].getOperator() == tassertion.getOperator() ) { + if( assertion.getKind() == NOT ) { + redundant = true; + } else { + conflict = NodeManager::currentNM()->mkNode( AND, leqn, assertion ); + r = Reason::contradiction; + Debug("datatypes") << "Contradictory labels " << conflict << endl; + return false; + } + break; + } + }else{ + if( (leqn.getOperator() == tassertion.getOperator()) == (assertion.getKind() == NOT) ) { + conflict = NodeManager::currentNM()->mkNode( AND, leqn, assertion ); + r = Reason::idt_tclash; + Debug("datatypes") << "Contradictory labels(2) " << conflict << endl; + return false; + } + redundant = true; + break; + } + } + return !redundant; +} + +void TheoryDatatypes::addTester( Node assertion ){ + Debug("datatypes") << "Add tester " << assertion << endl; + + //preprocess the tester + Node tassertion = ( assertion.getKind() == NOT ) ? assertion[0] : assertion; //add the term into congruence closure consideration d_cc.addTerm( tassertion[0] ); - Node assertionRep = assertion; - Node tassertionRep = tassertion; + Node assertionRep; + Node tassertionRep; Node tRep = tassertion[0]; - //tRep = collapseSelector( tRep, Node::null(), true ); tRep = find( tRep ); - Debug("datatypes") << "tRep is " << tRep << " " << tassertion[0] << endl; //add label instead for the representative (if it is different) if( tRep != tassertion[0] ) { tassertionRep = NodeManager::currentNM()->mkNode( APPLY_TESTER, tassertion.getOperator(), tRep ); assertionRep = ( assertion.getKind() == NOT ) ? tassertionRep.notNode() : tassertionRep; //add explanation - if( doAdd ) { - Node explanation = d_cc.explain( tRep, tassertion[0] ); - NodeBuilder<> nb(kind::AND); - nb << explanation << assertion; - explanation = nb; - Debug("datatypes-drv") << "Check derived tester " << assertionRep << endl; - Debug("datatypes-drv") << " Justification is " << explanation << endl; - d_drv_map[assertionRep] = explanation; - } - } - - //if tRep is a constructor, it is trivial - if( tRep.getKind() == APPLY_CONSTRUCTOR ) { - if( checkTrivialTester( tassertionRep ) == (assertionRep.getKind() == NOT) ) { - d_conflict = doAdd ? assertionRep : NodeManager::currentNM()->mkConst(true); - Debug("datatypes") << "Trivial conflict " << assertionRep << endl; - } - return; + Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, tRep, tassertion[0] ); + d_em.addNode( ccEq, &d_cce ); + NodeBuilder<> nb2(kind::AND); + nb2 << assertion << ccEq; + Node expl = nb2; + d_em.addNode( assertionRep, expl, Reason::idt_tcong ); + }else{ + tassertionRep = tassertion; + assertionRep = assertion; } - addTermToLabels( tRep ); - EqLists::iterator lbl_i = d_labels.find(tRep); - //Debug("datatypes") << "Found " << (lbl_i == d_labels.end()) << endl; - Assert( lbl_i != d_labels.end() ); - - EqList* lbl = (*lbl_i).second; - //Debug("datatypes") << "Check lbl = " << lbl << ", size = " << lbl->size() << endl; - - //check if empty label (no possible constructors for term) - bool add = true; - unsigned int notCount = 0; - if( !lbl->empty() ) { - for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { - Node leqn = (*i); - if( leqn.getKind() == kind::NOT ) { - if( leqn[0].getOperator() == tassertionRep.getOperator() ) { - if( assertionRep.getKind() == NOT ) { - add = false; - } else { - NodeBuilder<> nb(kind::AND); - nb << leqn; - if( doAdd ) nb << assertionRep; - d_conflict = nb.getNumChildren() == 1 ? nb.getChild( 0 ) : nb; - Debug("datatypes") << "Contradictory labels " << d_conflict << endl; - return; - } - break; - } - notCount++; - } else { - if( (leqn.getOperator() == tassertionRep.getOperator()) == (assertionRep.getKind() == NOT) ) { - NodeBuilder<> nb(kind::AND); - nb << leqn; - if( doAdd ) nb << assertionRep; - d_conflict = nb.getNumChildren() == 1 ? nb.getChild( 0 ) : nb; - Debug("datatypes") << "Contradictory labels(2) " << d_conflict << endl; - return; - } - add = false; - break; - } - } - } - if( add ) { - if( assertionRep.getKind() == NOT && notCount == dt.getNumConstructors()-1 ) { - NodeBuilder<> nb(kind::AND); - if( !lbl->empty() ) { + Node conflict; + unsigned r; + if( checkTester( assertionRep, conflict, r ) ){ + EqLists::iterator lbl_i = d_labels.find( tRep ); + EqList* lbl = (*lbl_i).second; + lbl->push_back( assertionRep ); + Debug("datatypes") << "Add to labels " << lbl->size() << endl; + if( assertionRep.getKind()==NOT ){ + const Datatype& dt = Datatype::datatypeOf( tassertion.getOperator().toExpr() ); + //we can conclude the final one + if( lbl->size()==dt.getNumConstructors()-1 ){ + vector< bool > possibleCons; + possibleCons.resize( dt.getNumConstructors(), true ); + NodeBuilder<> nb(kind::AND); for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { + possibleCons[ Datatype::indexOf( (*i)[0].getOperator().toExpr() ) ] = false; nb << (*i); } + unsigned int testerIndex = -1; + for( unsigned int i=0; imkNode( APPLY_TESTER, Node::fromExpr( dt[testerIndex].getTester() ), tRep ); + Node exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; + d_em.addNode( assertionRep, exp, Reason::idt_texhaust ); + addTester( assertionRep ); //add stronger statement + return; } - if( doAdd ) nb << assertionRep; - d_conflict = nb.getNumChildren() == 1 ? nb.getChild( 0 ) : nb; - Debug("datatypes") << "Exhausted possibilities for labels " << d_conflict << endl; - return; } - if( doAdd ) { - lbl->push_back( assertionRep ); - Debug("datatypes") << "Add to labels " << lbl->size() << endl; - } - } - if( doAdd ) { - checkInstantiate( tRep ); - if( !d_conflict.isNull() ) { - return; + if( assertionRep.getKind()==APPLY_TESTER ){ + //we have concluded that tRep must be a particular tester + //test all nodes in the equivalence class of tRep for instantiation + checkInstantiate( tRep ); + if( hasConflict() ) { + return; + } + //test all selectors whose arguments are in the equivalence class of tRep + updateSelectors( tRep ); } - //inspect selectors - updateSelectors( tRep ); + }else if( !conflict.isNull() ){ + d_em.addNodeConflict( conflict, r ); } - return; -} - -bool TheoryDatatypes::checkTrivialTester(Node assertion) { - AssertArgument(assertion.getKind() == APPLY_TESTER && - assertion[0].getKind() == APPLY_CONSTRUCTOR, - assertion, "argument must be a tester-over-constructor"); - TNode tester = assertion.getOperator(); - TNode ctor = assertion[0].getOperator(); - // if they have the same index (and the node has passed - // typechecking) then this is a trivial tester - return Datatype::indexOf(tester.toExpr()) == Datatype::indexOf(ctor.toExpr()); } void TheoryDatatypes::checkInstantiate( Node t ) { @@ -378,61 +422,65 @@ void TheoryDatatypes::checkInstantiate( Node t ) { if( t.getKind() != APPLY_CONSTRUCTOR ) { //for each term in equivalance class initializeEqClass( t ); + TypeNode typ = t.getType(); EqListN* eqc = (*d_equivalence_class.find( t )).second; for( EqListN::const_iterator iter = eqc->begin(); iter != eqc->end(); iter++ ) { Node te = *iter; Assert( find( te ) == t ); + //if term has not yet been instantiated if( d_inst_map.find( te ) == d_inst_map.end() ) { - Node cons = getPossibleCons( te, true ); EqLists::iterator lbl_i = d_labels.find( t ); - //there is one remaining constructor - if( !cons.isNull() && lbl_i != d_labels.end() ) { + if( lbl_i!=d_labels.end() ) { EqList* lbl = (*lbl_i).second; - const Datatype::Constructor& cn = Datatype::datatypeOf( cons.toExpr() )[ Datatype::indexOf( cons.toExpr() ) ]; - - //only one constructor possible for term (label is singleton), apply instantiation rule - //find if selectors have been applied to t - vector< Node > selectorVals; - selectorVals.push_back( cons ); - NodeBuilder<> justifyEq(kind::AND); - bool foundSel = false; - for( unsigned int i=0; imkNode( APPLY_SELECTOR, Node::fromExpr( cn[i].getSelector() ), te ); - Debug("datatypes") << "Selector[" << i << "] = " << s << endl; - if( d_selectors.find( s ) != d_selectors.end() ) { - Node sf = find( s ); - if( sf != s && sf.getKind() != SKOLEM ) { - justifyEq << d_cc.explain( sf, s ); + //check there is one remaining constructor + const Datatype& dt = ((DatatypeType)typ.toType()).getDatatype(); + Node cons; + if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind() != NOT ) { + size_t testerIndex = Datatype::indexOf( (*lbl)[ lbl->size()-1 ].getOperator().toExpr() ); + Node cons = Node::fromExpr( dt[ testerIndex ].getConstructor() ); + const Datatype::Constructor& cn = Datatype::datatypeOf( cons.toExpr() )[ Datatype::indexOf( cons.toExpr() ) ]; + + //only one constructor possible for term (label is singleton), apply instantiation rule + //find if selectors have been applied to t + vector< Node > selectorVals; + selectorVals.push_back( cons ); + bool foundSel = false; + for( unsigned int i=0; imkNode( APPLY_SELECTOR, Node::fromExpr( cn[i].getSelector() ), te ); + if( d_selectors.find( s ) != d_selectors.end() ) { + foundSel = true; + s = find( s ); } - foundSel = true; - s = sf; + selectorVals.push_back( s ); } - selectorVals.push_back( s ); - } - if( cn.isFinite() || foundSel ) { - d_inst_map[ te ] = true; - //instantiate, add equality - Node val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals ); - if( find( val ) != find( te ) ) { - Node newEq = NodeManager::currentNM()->mkNode( EQUAL, val, te ); - Debug("datatypes") << "Instantiate Equal: " << newEq << "." << endl; - if( lbl->size() == 1 || (*lbl)[ lbl->size()-1 ].getKind() != NOT ) { - justifyEq << (*lbl)[ lbl->size()-1 ]; - } else { - if( !lbl->empty() ) { - for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { - justifyEq << (*i); + if( cn.isFinite() || foundSel ) { + d_inst_map[ te ] = true; + //instantiate, add equality + Node val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals ); + if( find( val ) != find( te ) ) { + collectTerms( val ); + NodeBuilder<> nb(kind::AND); + nb << (*lbl)[ lbl->size()-1 ]; + for( unsigned int i=0; imkNode( APPLY_SELECTOR, Node::fromExpr( cn[i].getSelector() ), te ); + if( selectorVals[i+1]!=s ){ + Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, selectorVals[i+1], s ); + d_em.addNode( ccEq, &d_cce ); + nb << ccEq; + }else{ + //reflexive for s, if we want fined grained } } + Node jeq = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; + Node newEq = NodeManager::currentNM()->mkNode( EQUAL, val, te ); + Debug("datatypes") << "Instantiate Equal: " << newEq << "." << endl; + d_em.addNode( newEq, jeq, Reason::idt_inst ); + addEquality( newEq ); + return; } - Node jeq = ( justifyEq.getNumChildren() == 1 ) ? justifyEq.getChild( 0 ) : justifyEq; - Debug("datatypes-split") << "Instantiate " << newEq << endl; - preRegisterTerm( val ); - addDerivedEquality( newEq, jeq ); - return; + } else { + Debug("datatypes") << "infinite constructor, no selectors " << cons << endl; } - } else { - Debug("datatypes") << "infinite constructor, no selectors " << cons << endl; } } } @@ -440,65 +488,6 @@ void TheoryDatatypes::checkInstantiate( Node t ) { } } -//checkInst = true is for checkInstantiate, checkInst = false is for splitting -Node TheoryDatatypes::getPossibleCons( Node t, bool checkInst ) { - Node tf = find( t ); - EqLists::iterator lbl_i = d_labels.find( tf ); - if( lbl_i != d_labels.end() ) { - EqList* lbl = (*lbl_i).second; - TypeNode typ = t.getType(); - - const Datatype& dt = ((DatatypeType)typ.toType()).getDatatype(); - - //if ended by one positive tester - if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind() != NOT ) { - if( checkInst ) { - size_t testerIndex = Datatype::indexOf( (*lbl)[ lbl->size()-1 ].getOperator().toExpr() ); - return Node::fromExpr( dt[ testerIndex ].getConstructor() ); - } - //if (n-1) negative testers - } else if( !checkInst || lbl->size() == dt.getNumConstructors()-1 ) { - vector< bool > possibleCons; - possibleCons.resize( dt.getNumConstructors(), true ); - if( !lbl->empty() ) { - for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { - TNode leqn = (*i); - possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false; - } - } - Node cons = Node::null(); - for( unsigned int i=0; imkNode( APPLY_SELECTOR, Node::fromExpr( dt[i][j].getSelector() ), tf ); - if( d_selectors.find( s ) != d_selectors.end() ) { - Debug("datatypes") << " getPosCons: found selector " << s << endl; - return cons; - } - } - } - } - } - if( !checkInst ) { - for( int i=0; i<(int)possibleCons.size(); i++ ) { - if( possibleCons[i] && !dt[ i ].isFinite() ) { - Debug("datatypes") << "Did not find selector for " << tf; - Debug("datatypes") << " and " << dt[ i ].getConstructor() << " is not finite." << endl; - return Node::null(); - } - } - } else { - Assert( !cons.isNull() ); - } - return cons; - } - } - return Node::null(); -} - Node TheoryDatatypes::getValue(TNode n) { NodeManager* nodeManager = NodeManager::currentNM(); @@ -522,7 +511,7 @@ void TheoryDatatypes::merge(TNode a, TNode b) { d_merge_pending[d_merge_pending.size()-1].push_back( pair< Node, Node >( a, b ) ); return; } - Assert(d_conflict.isNull()); + Assert(!hasConflict()); a = find(a); b = find(b); if( a == b) { @@ -566,15 +555,15 @@ void TheoryDatatypes::merge(TNode a, TNode b) { NodeBuilder<> explanation(kind::AND); if( a.getKind() == kind::APPLY_CONSTRUCTOR && b.getKind() == kind::APPLY_CONSTRUCTOR && a.getOperator()!=b.getOperator() ){ - explanation << d_cc.explain( a, b ); - d_conflict = explanation.getNumChildren() == 1 ? explanation.getChild( 0 ) : explanation; + Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, a, b ); + d_em.addNode( ccEq, &d_cce ); + d_em.addNodeConflict( ccEq, Reason::idt_clash ); Debug("datatypes") << "Clash " << a << " " << b << endl; - Debug("datatypes") << "Conflict is " << d_conflict << endl; return; } Debug("datatypes-debug") << "Done clash" << endl; - Debug("datatypes") << "Set canon: "<< a << " " << b << endl; + Debug("datatypes-debug-pf") << "Set canon: "<< a << " " << b << endl; // b becomes the canon of a d_unionFind.setCanon(a, b); d_reps[a] = false; @@ -601,7 +590,6 @@ void TheoryDatatypes::merge(TNode a, TNode b) { * since the representative of b does not change and we check all the things * in a's class when we look at the diseq list of find(a) */ - EqLists::iterator deq_ib = d_disequalities.find(b); if(deq_ib != d_disequalities.end()) { EqList* deq = (*deq_ib).second; @@ -626,7 +614,6 @@ void TheoryDatatypes::merge(TNode a, TNode b) { * the side effect that it adds them to the list of b (which * became the canonical representative) */ - EqList* deqa = (*deq_ia).second; for(EqList::const_iterator i = deqa->begin(); i != deqa->end(); i++) { TNode deqn = (*i); @@ -638,15 +625,13 @@ void TheoryDatatypes::merge(TNode a, TNode b) { TNode tp = find(t); if(sp == tp) { Debug("datatypes") << "Construct standard conflict " << deqn << " " << sp << endl; - Node explanation = d_cc.explain(deqn[0], deqn[1]); - d_conflict = NodeManager::currentNM()->mkNode( kind::AND, explanation, deqn.notNode() ); - Debug("datatypes") << "Conflict is " << d_conflict << endl; + d_em.addNode( deqn, &d_cce ); + d_em.addNodeConflict( NodeManager::currentNM()->mkNode( kind::AND, deqn, deqn.notNode() ), Reason::contradiction ); return; } Assert( sp == b || tp == b, "test2"); // make sure not to add duplicates - if(sp == b) { if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) { appendToDiseqList(b, deqn); @@ -667,13 +652,12 @@ void TheoryDatatypes::merge(TNode a, TNode b) { Debug("datatypes-cycles") << "Equal " << a << " -> " << b << " " << d_hasSeenCycle.get() << endl; if( d_hasSeenCycle.get() ){ checkCycles(); - if( !d_conflict.isNull() ){ + if( hasConflict() ){ return; } }else{ checkCycles(); - if( !d_conflict.isNull() ){ - Debug("datatypes-cycles") << "Cycle is " << d_conflict << std::endl; + if( hasConflict() ){ for( int i=0; i<(int)d_currEqualities.size(); i++ ) { Debug("datatypes-cycles") << "currEqualities[" << i << "] = " << d_currEqualities[i] << endl; } @@ -683,7 +667,7 @@ void TheoryDatatypes::merge(TNode a, TNode b) { } #else checkCycles(); - if( !d_conflict.isNull() ){ + if( hasConflict() ){ return; } #endif @@ -691,7 +675,7 @@ void TheoryDatatypes::merge(TNode a, TNode b) { //merge selector lists updateSelectors( a ); - if( !d_conflict.isNull() ){ + if( hasConflict() ){ return; } Debug("datatypes-debug") << "Done collapse" << endl; @@ -702,8 +686,8 @@ void TheoryDatatypes::merge(TNode a, TNode b) { EqList* lbl = (*lbl_i).second; if( !lbl->empty() ) { for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { - checkTester( *i ); - if( !d_conflict.isNull() ) { + addTester( *i ); + if( hasConflict() ) { return; } } @@ -712,15 +696,16 @@ void TheoryDatatypes::merge(TNode a, TNode b) { Debug("datatypes-debug") << "Done merge labels" << endl; //do unification - Assert( d_conflict.isNull() ); if( a.getKind() == APPLY_CONSTRUCTOR && b.getKind() == APPLY_CONSTRUCTOR && a.getOperator() == b.getOperator() ) { Debug("datatypes") << "Unification: " << a << " and " << b << "." << endl; for( int i=0; i<(int)a.getNumChildren(); i++ ) { if( find( a[i] ) != find( b[i] ) ) { + Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, a, b ); Node newEq = NodeManager::currentNM()->mkNode( EQUAL, a[i], b[i] ); - Node jEq = d_cc.explain(a, b); - addDerivedEquality( newEq, jEq ); + d_em.addNode( ccEq, &d_cce ); + d_em.addNode( newEq, ccEq, Reason::idt_unify ); + addEquality( newEq ); } } } @@ -728,8 +713,8 @@ void TheoryDatatypes::merge(TNode a, TNode b) { Debug("datatypes-debug") << "merge(): Done" << endl; } -Node TheoryDatatypes::collapseSelector( TNode t, bool useContext ) { - if( t.getKind() == APPLY_SELECTOR ) { +Node TheoryDatatypes::collapseSelector( Node t ) { + if( !hasConflict() && t.getKind() == APPLY_SELECTOR ) { //collapse constructor TypeNode typ = t[0].getType(); Node sel = t.getOperator(); @@ -750,37 +735,51 @@ Node TheoryDatatypes::collapseSelector( TNode t, bool useContext ) { Debug("datatypes") << selType[1].mkGroundTerm() << " of type " << selType[1] << endl; retNode = selType[1].mkGroundTerm(); } - if( useContext ) { - Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t ); - d_axioms[neq] = true; - Debug("datatypes-split") << "Collapse selector " << neq << endl; - addEquality( neq ); + if( tmp!=t[0] ){ + t = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, t.getOperator(), tmp ); } + Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t ); + d_em.addNodeAxiom( neq, Reason::idt_collapse ); + Debug("datatypes") << "Collapse selector " << neq << endl; + addEquality( neq ); } else { - if( useContext ) { - //check labels - Node tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), tmp ); - checkTester( tester, false ); - if( !d_conflict.isNull() ) { - Debug("datatypes") << "Applied selector " << t << " to provably wrong constructor." << endl; - retNode = selType[1].mkGroundTerm(); - - Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t ); - NodeBuilder<> nb(kind::AND); - Node trueNode = NodeManager::currentNM()->mkConst(true); - if( d_conflict != trueNode ) { - nb << d_conflict; - } - d_conflict = Node::null(); - tmp = find( tmp ); - if( tmp != t[0] ) { - nb << d_cc.explain( tmp, t[0] ); + //see whether we can prove that the selector is applied to the wrong tester + Node tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), tmp ); + Node conflict; + unsigned r; + checkTester( tester, conflict, r ); + if( !conflict.isNull() ) { + Debug("datatypes") << "Applied selector " << t << " to provably wrong constructor." << endl; + // conflict = c ^ tester, conflict => false + // want to say c => ~tester + //must remove tester from conflict + if( conflict.getKind()==kind::AND ){ + NodeBuilder<> jt(kind::AND); + for( int i=0; i<(int)conflict.getNumChildren(); i++ ){ + if( conflict[i]!=tester ){ + jt << conflict[i]; + } } - Assert( nb.getNumChildren()>0 ); - Node jEq = nb.getNumChildren() == 1 ? nb.getChild( 0 ) : nb; - Debug("datatypes-drv") << "Collapse selector " << neq << endl; - addDerivedEquality( neq, jEq ); + conflict = ( jt.getNumChildren()==1 ) ? jt.getChild( 0 ) : jt; + }else if( conflict==tester ){ + conflict = Node::null(); + } + if( conflict!=tester.notNode() ){ + d_em.addNode( tester.notNode(), conflict, r ); } + + if( tmp != t[0] ) { + Node teq = NodeManager::currentNM()->mkNode( EQUAL, tmp, t[0] ); + d_em.addNode( teq, &d_cce ); + Node exp = NodeManager::currentNM()->mkNode( AND, tester.notNode(), teq ); + tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), t[0] ); + d_em.addNode( tester.notNode(), exp, Reason::idt_tcong ); + } + retNode = selType[1].mkGroundTerm(); + Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t ); + + d_em.addNode( neq, tester.notNode(), Reason::idt_collapse2 ); + addEquality( neq ); } } return retNode; @@ -809,21 +808,15 @@ void TheoryDatatypes::updateSelectors( Node a ) { } a = b; } - Debug("datatypes") << "Merge selector " << s << " into " << b << endl; - Debug("datatypes") << "Find is " << find( s[0] ) << endl; - Assert( s.getKind() == APPLY_SELECTOR && - find( s[0] ) == b ); + //Debug("datatypes") << "Merge selector " << s << " into " << b + //Debug("datatypes") << ", find is " << find( s[0] ) << endl; + Assert( s.getKind() == APPLY_SELECTOR && find( s[0] ) == b ); if( b != s[0] ) { Node t = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, s.getOperator(), b ); - //add to labels - addTermToLabels( t ); - merge( s, t ); - s = t; - d_selectors[s] = true; - d_cc.addTerm( s ); + d_cc.addTerm( t ); } - s = collapseSelector( s, true ); - if( !d_conflict.isNull() ) { + s = collapseSelector( s ); + if( hasConflict() ) { return; } if( sel_b && s.getKind() == APPLY_SELECTOR ) { @@ -845,6 +838,13 @@ void TheoryDatatypes::addTermToLabels( Node t ) { if(lbl_i == d_labels.end()) { EqList* lbl = new(getContext()->getCMM()) EqList(true, getContext(), false, ContextMemoryAllocator(getContext()->getCMM())); + //if there is only one constructor, then it must be + const Datatype& dt = ((DatatypeType)(t.getType()).toType()).getDatatype(); + if( dt.getNumConstructors()==1 ){ + Node tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), t ); + addTester( tester ); + d_em.addNodeAxiom( tester, Reason::idt_texhaust ); + } d_labels.insertDataFromContextMemory(tmp, lbl); } } @@ -882,7 +882,7 @@ void TheoryDatatypes::collectTerms( Node n ) { } if( n.getKind() == APPLY_SELECTOR ) { if( d_selectors.find( n ) == d_selectors.end() ) { - Debug("datatypes-split") << " Found selector " << n << endl; + Debug("datatypes") << " Found selector " << n << endl; d_selectors[ n ] = true; d_cc.addTerm( n ); Node tmp = find( n[0] ); @@ -892,9 +892,7 @@ void TheoryDatatypes::collectTerms( Node n ) { if( tmp != n[0] ) { s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, n.getOperator(), tmp ); } - Debug("datatypes-split") << " Before collapse: " << s << endl; - s = collapseSelector( s, true ); - Debug("datatypes-split") << " After collapse: " << s << endl; + s = collapseSelector( s ); if( s.getKind() == APPLY_SELECTOR ) { //add selector to selector eq list Debug("datatypes") << " Add selector to list " << tmp << " " << n << endl; @@ -937,30 +935,30 @@ void TheoryDatatypes::appendToDiseqList(TNode of, TNode eq) { //} } -void TheoryDatatypes::addDerivedEquality(TNode eq, TNode jeq) { - Debug("datatypes-drv") << "Justification for " << eq << "is: " << jeq << "." << endl; - d_drv_map[eq] = jeq; - addEquality( eq ); -} +#define DELAY_MERGE void TheoryDatatypes::addEquality(TNode eq) { Assert(eq.getKind() == kind::EQUAL || eq.getKind() == kind::IFF); - if( eq[0] != eq[1] ) { + if( find( eq[0] ) != find( eq[1] ) ) { Debug("datatypes") << "Add equality " << eq << "." << endl; + Debug("datatypes-debug-pf") << "Add equality " << eq << "." << endl; //setup merge pending list +#ifdef DELAY_MERGE d_merge_pending.push_back( vector< pair< Node, Node > >() ); bool prevNoMerge = d_noMerge; d_noMerge = true; +#endif d_cc.addTerm(eq[0]); d_cc.addTerm(eq[1]); - d_cc.addEquality(eq); + d_cce.assert(eq); if( Debug.isOn("datatypes") || Debug.isOn("datatypes-cycles") ){ d_currEqualities.push_back(eq); } +#ifdef DELAY_MERGE //record which nodes are waiting to be merged d_noMerge = prevNoMerge; vector< pair< Node, Node > > mp; @@ -968,17 +966,20 @@ void TheoryDatatypes::addEquality(TNode eq) { d_merge_pending[d_merge_pending.size()-1].begin(), d_merge_pending[d_merge_pending.size()-1].end() ); d_merge_pending.pop_back(); +#endif //merge original nodes - if( d_conflict.isNull() ) { - merge(eq[0], eq[1]); + if( !hasConflict() ) { + merge( eq[0], eq[1] ); } +#ifdef DELAY_MERGE //merge nodes waiting to be merged for( int i=0; i<(int)mp.size(); i++ ) { - if( d_conflict.isNull() ) { + if( !hasConflict() ) { merge( mp[i].first, mp[i].second ); } } +#endif } } @@ -993,44 +994,16 @@ void TheoryDatatypes::addDisequality(TNode eq) { appendToDiseqList(find(b), eq); } -void TheoryDatatypes::throwConflict() { - Debug("datatypes") << "Convert conflict : " << d_conflict << endl; - NodeBuilder<> nb(kind::AND); - convertDerived( d_conflict, nb ); - d_conflict = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; - if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || Debug.isOn("datatypes-cycles") ) { - cout << "Conflict constructed : " << d_conflict << endl; - } - //if( d_conflict.getKind()!=kind::AND ){ - // d_conflict = NodeManager::currentNM()->mkNode(kind::AND, d_conflict, d_conflict); - //} - d_out->conflict( d_conflict, false ); - d_conflict = Node::null(); -} - -void TheoryDatatypes::convertDerived(Node n, NodeBuilder<>& nb) { - if( n.getKind() == kind::AND ) { - for( int i=0; i<(int)n.getNumChildren(); i++ ) { - convertDerived( n[i], nb ); - } - } else if( !d_drv_map[ n ].get().isNull() ) { - //Debug("datatypes") << "Justification for " << n << " is " << d_drv_map[ n ].get() << endl; - convertDerived( d_drv_map[ n ].get(), nb ); - } else if( d_axioms.find( n ) == d_axioms.end() ) { - nb << n; - } -} - void TheoryDatatypes::checkCycles() { for( BoolMap::iterator i = d_reps.begin(); i != d_reps.end(); i++ ) { if( (*i).second ) { map< Node, bool > visited; NodeBuilder<> explanation(kind::AND); if( searchForCycle( (*i).first, (*i).first, visited, explanation ) ) { - Assert( explanation.getNumChildren()>0 ); - d_conflict = explanation.getNumChildren() == 1 ? explanation.getChild( 0 ) : explanation; + Node cCycle = explanation.getNumChildren() == 1 ? explanation.getChild( 0 ) : explanation; + d_em.addNodeConflict( cCycle, Reason::idt_cycle ); Debug("datatypes") << "Detected cycle for " << (*i).first << endl; - Debug("datatypes") << "Conflict is " << d_conflict << endl; + Debug("datatypes") << "Conflict is " << cCycle << endl; return; } } @@ -1052,19 +1025,12 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on, Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << n[i] << "!!!!" << std::endl; } if( nn != n[i] ) { - Node e = d_cc.explain( nn, n[i] ); if( !d_cycle_check.isConnectedNode( n[i], nn ) ){ Debug("datatypes-cycles") << "Cycle equality: " << n[i] << " is not -> " << nn << "!!!!" << std::endl; - Debug("datatypes-cycles") << "Explanation: " << e << std::endl; - if( e.getKind()==kind::AND ){ - for( int a=0; amkNode( EQUAL, nn, n[i] ); + d_em.addNode( ccEq, &d_cce ); + explanation << ccEq; } return true; } diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 1a944a6e0..1e715b4e4 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -27,6 +27,7 @@ #include "theory/datatypes/union_find.h" #include "util/hash.h" #include "util/trans_closure.h" +#include "theory/datatypes/explanation_manager.h" #include #include @@ -48,10 +49,6 @@ private: context::CDList d_currAsserts; context::CDList d_currEqualities; - /** map from equalties and the equalities they are derived from */ - context::CDMap< Node, Node, NodeHashFunction > d_drv_map; - /** equalities that are axioms */ - BoolMap d_axioms; /** list of all selectors */ BoolMap d_selectors; /** list of all representatives */ @@ -74,7 +71,8 @@ private: /** * map from terms to testers asserted for that term * for each t, this is either a list of equations of the form - * NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ), each of which are unique testers, + * NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ), each of which are unique testers + * and n is less than the number of possible constructors for t, * or a list of equations of the form * NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ) followed by * is_[constructor_(n+1)]( t ), each of which is a unique tester. @@ -120,20 +118,19 @@ private: * */ EqLists d_disequalities; - /** List of all (potential) equalities to be propagated. */ - EqLists d_equalities; - - /** - * stores the conflicting disequality (still need to call construct - * conflict to get the actual explanation) - */ - Node d_conflict; /** * information for delayed merging (is this necessary?) */ bool d_noMerge; std::vector< std::vector< std::pair< Node, Node > > > d_merge_pending; bool d_inCheck; + + /** + * explanation manager + */ + ExplanationManager d_em; + CongruenceClosureExplainer d_cce; + public: TheoryDatatypes(context::Context* c, OutputChannel& out, Valuation valuation); ~TheoryDatatypes(); @@ -149,33 +146,34 @@ public: private: /* Helper methods */ - void checkTester( Node assertion, bool doAdd = true ); - bool checkTrivialTester(Node assertion); + bool checkTester( Node assertion, Node& conflict, unsigned& r ); + void addTester( Node assertion ); void checkInstantiate( Node t ); - Node getPossibleCons( Node t, bool checkInst = false ); - Node collapseSelector( TNode t, bool useContext = false ); + Node collapseSelector( Node t ); void updateSelectors( Node a ); void addTermToLabels( Node t ); void initializeEqClass( Node t ); void collectTerms( Node n ); + bool hasConflict(); /* from uf_morgan */ void merge(TNode a, TNode b); - inline TNode find(TNode a); + inline TNode find(TNode a); inline TNode debugFind(TNode a) const; void appendToDiseqList(TNode of, TNode eq); void addDisequality(TNode eq); - void addDerivedEquality(TNode eq, TNode jeq); void addEquality(TNode eq); - void convertDerived(Node n, NodeBuilder<>& nb); - void throwConflict(); void checkCycles(); bool searchForCycle( Node n, Node on, std::map< Node, bool >& visited, NodeBuilder<>& explanation ); };/* class TheoryDatatypes */ +inline bool TheoryDatatypes::hasConflict() { + return d_em.hasConflict(); +} + inline TNode TheoryDatatypes::find(TNode a) { return d_unionFind.find(a); } -- 2.30.2