From: Andrew Reynolds Date: Fri, 6 May 2011 20:17:57 +0000 (+0000) Subject: significant revisions/improvements to code for theory datatypes solver X-Git-Tag: cvc5-1.0.0~8554 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b0b3a1fca9a40915fe2a8a73ca0567accc4832a4;p=cvc5.git significant revisions/improvements to code for theory datatypes solver --- diff --git a/src/theory/datatypes/explanation_manager.cpp b/src/theory/datatypes/explanation_manager.cpp index 3594037a6..06f7bb29e 100644 --- a/src/theory/datatypes/explanation_manager.cpp +++ b/src/theory/datatypes/explanation_manager.cpp @@ -33,17 +33,20 @@ void ExplanationManager::process( Node n, NodeBuilder<>& nb, ProofManager* pm ) 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, explainer says that n is an input - if( exp==n ){ - r.d_isInput = true; + if( !r.d_isInput ){ + if( r.d_e ){ + + Debug("emanager") << "Em::process: Consult externally for " << n << std::endl; + exp = r.d_e->explain( n, pm ); + //trivial case, explainer says that n is an input + if( exp==n ){ + r.d_isInput = true; + } + }else{ + 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; } - }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; } } diff --git a/src/theory/datatypes/explanation_manager.h b/src/theory/datatypes/explanation_manager.h index aaf0e06e9..2232d0048 100644 --- a/src/theory/datatypes/explanation_manager.h +++ b/src/theory/datatypes/explanation_manager.h @@ -47,9 +47,11 @@ public: cc_coarse, + //coarse rules for idt + idt_cycle_coarse, + idt_inst_coarse, //unification rules idt_unify, - idt_cycle, idt_clash, //tester rules idt_taxiom, @@ -133,12 +135,12 @@ public: ~CongruenceClosureExplainer(){} /** assert that n is true */ void assert( Node n ){ - Assert( n.getKind() == kind::EQUAL ); + Assert( n.getKind() == kind::EQUAL || n.getKind() == kind::IFF ); d_cc->addEquality( n ); } /** get the explanation for n */ Node explain( Node n, ProofManager* pm ){ - Assert( n.getKind() == kind::EQUAL ); + Assert( n.getKind() == kind::EQUAL || n.getKind() == kind::IFF ); if( pm->getEffort()==ProofManager::FULL_EFFORT ){ //unsupported Assert( false ); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 104992bd4..6808ef749 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -69,16 +69,9 @@ TheoryDatatypes::TheoryDatatypes(Context* c, OutputChannel& out, Valuation valua d_cc(c, &d_ccChannel), d_unionFind(c), d_disequalities(c), - d_noMerge(false), - d_inCheck(false), d_em(c), d_cce(&d_cc){ - ////bug test for transitive closure - //TransitiveClosure tc( c ); - //Debug("datatypes-tc") << "33 -> 32 : " << tc.addEdge( 33, 32 ) << std::endl; - //Debug("datatypes-tc") << "32 -> 33 : " << tc.addEdge( 32, 33 ) << std::endl; - //tc.debugPrintMatrix(); } @@ -133,7 +126,7 @@ void TheoryDatatypes::check(Effort e) { } //clear from the derived map - d_inCheck = true; + d_checkMap.clear(); collectTerms( assertion ); if( !hasConflict() ){ if( d_em.hasNode( assertion ) ){ @@ -200,8 +193,22 @@ void TheoryDatatypes::check(Effort e) { } } } - Debug("datatypes-debug-pf") << "Done check " << assertion << " " << hasConflict() << std::endl; - d_inCheck = false; + //rules to check for collapse, instantiate + while( !hasConflict() && !d_checkMap.empty() ){ + std::map< Node, bool > temp; + temp = d_checkMap; + d_checkMap.clear(); + std::map< Node, bool >::iterator i; + for( i = temp.begin(); i != temp.end(); i++ ){ + Node n = find( i->first ); + if( temp.find( n )==temp.end() || temp[n] ){ + if( !hasConflict() ) checkInstantiateEqClass( n ); + if( !hasConflict() ) updateSelectors( n ); + temp[n] = false; + } + } + } + //if there is now a conflict if( hasConflict() ) { Debug("datatypes-conflict") << "Constructing conflict..." << endl; Debug("datatypes-conflict") << d_cc << std::endl; @@ -214,7 +221,6 @@ void TheoryDatatypes::check(Effort e) { // conflict = NodeManager::currentNM()->mkNode(kind::AND, conflict, conflict); //} d_out->conflict( conflict, false ); - //Assert( false ); return; } } @@ -224,14 +230,13 @@ void TheoryDatatypes::check(Effort e) { //do splitting 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 ) { + if( 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 << ", 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(); + if( lbl->empty() || (*lbl)[ lbl->size()-1 ].getKind() == NOT ) { //there are more than 1 possible constructors for sf + const Datatype& dt = ((DatatypeType)(sf.getType()).toType()).getDatatype(); vector< bool > possibleCons; possibleCons.resize( dt.getNumConstructors(), true ); for( EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) { @@ -247,7 +252,6 @@ void TheoryDatatypes::check(Effort e) { for( unsigned int k=0; kmkNode( 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; } @@ -255,7 +259,7 @@ void TheoryDatatypes::check(Effort e) { } } if( !foundSel ){ - for( unsigned int j=0; j<(int)possibleCons.size(); j++ ) { + for( unsigned int j=0; jempty() || lbl->begin()==lbl->end() ); + EqList* lbl = (*d_labels.find( tassertion[0] )).second; //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 { + if( assertion.getKind() != NOT ) { conflict = NodeManager::currentNM()->mkNode( AND, leqn, assertion ); r = Reason::contradiction; Debug("datatypes") << "Contradictory labels " << conflict << endl; - return false; } - break; + return false; } }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 false; } } - return !redundant; + return true; } void TheoryDatatypes::addTester( Node assertion ){ - Debug("datatypes") << "Add tester " << assertion << endl; + Debug("datatypes") << "addTester " << assertion << endl; //preprocess the tester Node tassertion = ( assertion.getKind() == NOT ) ? assertion[0] : assertion; @@ -352,15 +348,24 @@ void TheoryDatatypes::addTester( Node assertion ){ tRep = find( tRep ); //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 - 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 ); + //explanation is trivial (do not add to labels) + if( tRep.getKind()==APPLY_CONSTRUCTOR && assertion.getKind()== kind::APPLY_TESTER && + Datatype::indexOf(assertion.getOperator().toExpr())==Datatype::indexOf(tRep.getOperator().toExpr()) ){ + tassertionRep = NodeManager::currentNM()->mkNode( APPLY_TESTER, tassertion.getOperator(), tRep ); + assertionRep = tassertionRep; + d_em.addNodeAxiom( assertionRep, Reason::idt_taxiom ); + return; + }else{ + tassertionRep = NodeManager::currentNM()->mkNode( APPLY_TESTER, tassertion.getOperator(), tRep ); + assertionRep = ( assertion.getKind() == NOT ) ? tassertionRep.notNode() : tassertionRep; + //add explanation + 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; @@ -369,10 +374,11 @@ void TheoryDatatypes::addTester( Node assertion ){ Node conflict; unsigned r; if( checkTester( assertionRep, conflict, r ) ){ + //it is not redundant/contradictory, add it to labels 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; + Debug("datatypes") << "Add to labels " << assertionRep << endl; if( assertionRep.getKind()==NOT ){ const Datatype& dt = Datatype::datatypeOf( tassertion.getOperator().toExpr() ); //we can conclude the final one @@ -384,15 +390,14 @@ void TheoryDatatypes::addTester( Node assertion ){ 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 ); + Assert( testerIndex!=-1 ); + assertionRep = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[unsigned(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 @@ -400,89 +405,203 @@ void TheoryDatatypes::addTester( Node assertion ){ } } 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; - } - //update all selectors whose arguments are in the equivalence class of tRep - updateSelectors( tRep ); + d_checkMap[ tRep ] = true; } }else if( !conflict.isNull() ){ d_em.addNodeConflict( conflict, r ); } } -void TheoryDatatypes::checkInstantiate( Node t ) { - Debug("datatypes") << "TheoryDatatypes::checkInstantiate() " << t << endl; +//if only one constructor remaining for t, this function will return it +Node TheoryDatatypes::getInstantiateCons( Node t ){ + if( t.getKind() != APPLY_CONSTRUCTOR ){ + Assert( t == find( t ) ); + addTermToLabels( t ); + EqLists::iterator lbl_i = d_labels.find( t ); + if( lbl_i!=d_labels.end() ) { + EqList* lbl = (*lbl_i).second; + if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind() != NOT ) { + const Datatype& dt = ((DatatypeType)(t.getType()).toType()).getDatatype(); + size_t testerIndex = Datatype::indexOf( (*lbl)[ lbl->size()-1 ].getOperator().toExpr() ); + return Node::fromExpr( dt[ testerIndex ].getConstructor() ); + } + } + } + return Node::null(); +} + +void TheoryDatatypes::checkInstantiateEqClass( Node t ) { + Debug("datatypes") << "TheoryDatatypes::checkInstantiateEqClass() " << t << endl; Assert( t == find( t ) ); //if labels were created for t, and t has not been instantiated - if( t.getKind() != APPLY_CONSTRUCTOR ) { + Node cons = getInstantiateCons( t ); + if( !cons.isNull() ){ //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() ) { - EqLists::iterator lbl_i = d_labels.find( t ); - if( lbl_i!=d_labels.end() ) { - EqList* lbl = (*lbl_i).second; - //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 ); - } - 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 ) ) { - 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; - } - } else { - Debug("datatypes") << "infinite constructor, no selectors " << cons << endl; + if( checkInstantiate( te, cons ) ){ + return; + } + } + } +} + +//pre condition: find( te ) has been proven to be the constructor cons +//that is, is_[cons]( find( te ) ) is stored in d_labels +bool TheoryDatatypes::checkInstantiate( Node te, Node cons ) +{ + Debug("datatypes") << "TheoryDatatypes::checkInstantiate() " << te << endl; + //if term has not yet been instantiated + if( d_inst_map.find( te ) == d_inst_map.end() ) { + //find if selectors have been applied to t + vector< Node > selectorVals; + selectorVals.push_back( cons ); + bool foundSel = false; + const Datatype::Constructor& cn = getConstructor( cons ); + 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 ); + } + 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 ) ) { + //build explaination + NodeBuilder<> nb(kind::AND); + //explanation for tester + Node t = find( te ); + addTermToLabels( t ); + Assert( d_labels.find( t )!=d_labels.end() ); + EqList* lbl = (*d_labels.find( t )).second; + nb << (*lbl)[ lbl->size()-1 ]; //this should be changed to be tester for te, not t for fine-grained + //explanation for arguments + 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 idt_inst to be fined grained + //Node eq = NodeManager::currentNM()->mkNode( EQUAL, s, s ); + //d_em.addNodeAxiom( s, Reason::refl ); + } + } + Node jeq = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; + Node newEq = NodeManager::currentNM()->mkNode( EQUAL, val, te ); + Debug("datatypes") << "Instantiate: " << newEq << "." << endl; + d_em.addNode( newEq, jeq, Reason::idt_inst_coarse ); + //collect terms of instantiation term + collectTerms( val, false ); + //add equality for the instantiation + addEquality( newEq ); + return true; + } + } else { + Debug("datatypes") << "Do not Instantiate: infinite constructor, no selectors " << cons << endl; + } + }else{ + Debug("datatypes") << "Do not Instantiate: " << te << " already instantiated" << endl; + } + return false; +} + +bool TheoryDatatypes::collapseSelector( Node t ) { + if( !hasConflict() && t.getKind() == APPLY_SELECTOR ) { + //collapse constructor + TypeNode typ = t[0].getType(); + Node sel = t.getOperator(); + TypeNode selType = sel.getType(); + Node cons = getConstructorForSelector( sel ); + const Datatype::Constructor& cn = getConstructor( cons ); + Node tmp = find( t[0] ); + Node retNode = t; + if( tmp.getKind() == APPLY_CONSTRUCTOR ) { + if( tmp.getOperator() == cons ) { + Debug("datatypes") << "Applied selector " << t << " to correct constructor." << endl; + retNode = tmp[ Datatype::indexOf( sel.toExpr() ) ]; + } else { + Debug("datatypes") << "Applied selector " << t << " to wrong constructor." << endl; + retNode = selType[1].mkGroundTerm(); + } + 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") << "Add collapse equality " << neq << endl; + addEquality( neq ); + return true; + } else { + //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 is c ^ tester, where conflict => false, but we 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]; } } + conflict = ( jt.getNumChildren()==1 ) ? jt.getChild( 0 ) : jt; + }else{ + Assert( conflict==tester ); + conflict = Node::null(); + } + if( conflict!=tester.notNode() ){ + d_em.addNode( tester.notNode(), conflict, r ); //note that application of r is non-standard (TODO: fix) + } + + 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 true; + } + } + } + return false; +} + +//this function will test if each selector whose argument is in the equivalence class of "a" can be collapsed +void TheoryDatatypes::updateSelectors( Node a ) { + Debug("datatypes") << "updateSelectors: " << a << endl; + EqListsN::iterator sel_a_i = d_selector_eq.find( a ); + if( sel_a_i != d_selector_eq.end() ) { + EqListN* sel_a = (*sel_a_i).second; + for( EqListN::const_iterator i = sel_a->begin(); i != sel_a->end(); i++ ) { + Node s = (*i); + //if a is still a representative, and s has not yet been collapsed + if( find( a )==a && !d_selectors[s] ){ + Assert( s.getKind()==APPLY_SELECTOR && find( s[0] ) == a ); + if( a != s[0] ) { + s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, s.getOperator(), a ); + collectTerms( s, false ); } + d_selectors[s] = collapseSelector( s ); } } } @@ -490,23 +609,19 @@ void TheoryDatatypes::checkInstantiate( Node t ) { Node TheoryDatatypes::getValue(TNode n) { NodeManager* nodeManager = NodeManager::currentNM(); - switch(n.getKind()) { - case kind::VARIABLE: Unhandled(kind::VARIABLE); - case kind::EQUAL: // 2 args return nodeManager-> mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) ); - default: Unhandled(n.getKind()); } } void TheoryDatatypes::merge(TNode a, TNode b) { - if( d_noMerge ) { + if( !d_merge_pending.empty() ) { //Debug("datatypes") << "Append to merge pending list " << d_merge_pending.size() << endl; d_merge_pending[d_merge_pending.size()-1].push_back( pair< Node, Node >( a, b ) ); return; @@ -563,23 +678,65 @@ void TheoryDatatypes::merge(TNode a, TNode b) { } Debug("datatypes-debug") << "Done clash" << endl; - Debug("datatypes-debug-pf") << "Set canon: "<< a << " " << b << endl; + Debug("datatypes-ae") << "Set canon: "<< a << " " << b << endl; // b becomes the canon of a d_unionFind.setCanon(a, b); d_reps[a] = false; d_reps[b] = true; + //add this to the transitive closure module bool result = d_cycle_check.addEdgeNode( a, b ); d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); - + Debug("datatypes-cycles") << "Equal " << a << " -> " << b << " " << d_hasSeenCycle.get() << endl; + if( d_hasSeenCycle.get() ){ + checkCycles(); + if( hasConflict() ){ + return; + } + } + //else{ + // checkCycles(); + // if( hasConflict() ){ + // for( int i=0; i<(int)d_currEqualities.size(); i++ ) { + // Debug("datatypes-cycles") << "currEqualities[" << i << "] = " << d_currEqualities[i] << endl; + // } + // d_cycle_check.debugPrint(); + // Assert( false ); + // } + //} + Debug("datatypes-debug") << "Done cycles" << endl; //merge equivalence classes - initializeEqClass( a ); initializeEqClass( b ); - EqListN* eqc_a = (*d_equivalence_class.find( a )).second; EqListN* eqc_b = (*d_equivalence_class.find( b )).second; - for( EqListN::const_iterator i = eqc_a->begin(); i != eqc_a->end(); i++ ) { - eqc_b->push_back( *i ); + EqListsN::iterator eqc_a_i = d_equivalence_class.find( a ); + if( eqc_a_i!=d_equivalence_class.end() ){ + EqListN* eqc_a = (*eqc_a_i).second; + for( EqListN::const_iterator i = eqc_a->begin(); i != eqc_a->end(); i++ ) { + eqc_b->push_back( *i ); + } + }else{ + eqc_b->push_back( a ); + } + //merge selector lists + EqListsN::iterator sel_a_i = d_selector_eq.find( a ); + if( sel_a_i != d_selector_eq.end() ) { + EqListsN::iterator sel_b_i = d_selector_eq.find( b ); + EqListN* sel_b; + if( sel_b_i == d_selector_eq.end() ) { + sel_b = new(getContext()->getCMM()) EqListN(true, getContext(), false, + ContextMemoryAllocator(getContext()->getCMM())); + d_selector_eq.insertDataFromContextMemory(b, sel_b); + } else { + sel_b = (*sel_b_i).second; + } + EqListN* sel_a = (*sel_a_i).second; + for( EqListN::const_iterator i = sel_a->begin(); i != sel_a->end(); i++ ) { + sel_b->push_back( *i ); + } + if( !sel_a->empty() ){ + d_checkMap[ b ] = true; + } } deq_ia = d_disequalities.find(a); @@ -647,42 +804,14 @@ void TheoryDatatypes::merge(TNode a, TNode b) { } } - Debug("datatypes-cycles") << "Equal " << a << " -> " << b << " " << d_hasSeenCycle.get() << endl; - if( d_hasSeenCycle.get() ){ - checkCycles(); - if( hasConflict() ){ - return; - } - } - //else{ - // checkCycles(); - // if( hasConflict() ){ - // for( int i=0; i<(int)d_currEqualities.size(); i++ ) { - // Debug("datatypes-cycles") << "currEqualities[" << i << "] = " << d_currEqualities[i] << endl; - // } - // d_cycle_check.debugPrint(); - // Assert( false ); - // } - //} - Debug("datatypes-debug") << "Done cycles" << endl; - - //merge selector lists - updateSelectors( a ); - if( hasConflict() ){ - return; - } - Debug("datatypes-debug") << "Done collapse" << endl; - //merge labels EqLists::iterator lbl_i = d_labels.find( a ); if(lbl_i != d_labels.end()) { EqList* lbl = (*lbl_i).second; - if( !lbl->empty() ) { - for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { - addTester( *i ); - if( hasConflict() ) { - return; - } + for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { + addTester( *i ); + if( hasConflict() ) { + return; } } } @@ -699,128 +828,14 @@ void TheoryDatatypes::merge(TNode a, TNode b) { d_em.addNode( ccEq, &d_cce ); d_em.addNode( newEq, ccEq, Reason::idt_unify ); addEquality( newEq ); - } - } - } - - Debug("datatypes-debug") << "merge(): Done" << endl; -} - -Node TheoryDatatypes::collapseSelector( Node t ) { - if( !hasConflict() && t.getKind() == APPLY_SELECTOR ) { - //collapse constructor - TypeNode typ = t[0].getType(); - Node sel = t.getOperator(); - TypeNode selType = sel.getType(); - Node cons = getConstructorForSelector( sel ); - const Datatype::Constructor& cn = getConstructor( cons ); - Node tmp = find( t[0] ); - Node retNode = t; - if( tmp.getKind() == APPLY_CONSTRUCTOR ) { - if( tmp.getOperator() == cons ) { - size_t selIndex = Datatype::indexOf( sel.toExpr() ); - Debug("datatypes") << "Applied selector " << t << " to correct constructor, index = " << selIndex << endl; - Debug("datatypes") << "Return " << tmp[selIndex] << endl; - retNode = tmp[selIndex]; - } else { - Debug("datatypes") << "Applied selector " << t << " to wrong constructor " << endl; - Debug("datatypes") << "Return distinguished term "; - Debug("datatypes") << selType[1].mkGroundTerm() << " of type " << selType[1] << endl; - retNode = selType[1].mkGroundTerm(); - } - 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 { - //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]; - } - } - 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; - } - return t; -} - -void TheoryDatatypes::updateSelectors( Node a ) { - EqListsN::iterator sel_a_i = d_selector_eq.find( a ); - if( sel_a_i != d_selector_eq.end() ) { - EqListN* sel_a = (*sel_a_i).second; - Debug("datatypes") << a << " has " << sel_a->size() << " selectors" << endl; - if( !sel_a->empty() ) { - EqListN* sel_b = NULL; - for( EqListN::const_iterator i = sel_a->begin(); i != sel_a->end(); i++ ) { - Node s = (*i); - Node b = find( a ); - if( b != a ) { - EqListsN::iterator sel_b_i = d_selector_eq.find( b ); - if( sel_b_i == d_selector_eq.end() ) { - sel_b = new(getContext()->getCMM()) EqListN(true, getContext(), false, - ContextMemoryAllocator(getContext()->getCMM())); - d_selector_eq.insertDataFromContextMemory(b, sel_b); - } else { - sel_b = (*sel_b_i).second; - } - a = 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 ); - d_cc.addTerm( t ); - collectTerms( t ); - } - s = collapseSelector( s ); if( hasConflict() ) { return; } - if( sel_b && s.getKind() == APPLY_SELECTOR ) { - sel_b->push_back( s ); - } } } - } else { - Debug("datatypes") << a << " has no selectors" << endl; } + + Debug("datatypes-debug") << "merge(): Done" << endl; } void TheoryDatatypes::addTermToLabels( Node t ) { @@ -855,9 +870,11 @@ void TheoryDatatypes::initializeEqClass( Node t ) { } } -void TheoryDatatypes::collectTerms( Node n ) { - for( int i=0; i<(int)n.getNumChildren(); i++ ) { - collectTerms( n[i] ); +void TheoryDatatypes::collectTerms( Node n, bool recurse ) { + if( recurse ){ + for( int i=0; i<(int)n.getNumChildren(); i++ ) { + collectTerms( n[i] ); + } } if( n.getKind() == APPLY_CONSTRUCTOR ){ for( int i=0; i<(int)n.getNumChildren(); i++ ) { @@ -866,41 +883,30 @@ void TheoryDatatypes::collectTerms( Node n ) { Assert( !result ); //this should not create any new cycles (relevant terms should have been recorded before) } }else{ - if( n.getKind() == APPLY_SELECTOR ) { - if( d_selectors.find( n ) == d_selectors.end() ) { - Debug("datatypes") << " Found selector " << n << endl; - d_selectors[ n ] = true; - d_cc.addTerm( n ); - Node tmp = find( n[0] ); - checkInstantiate( tmp ); - - Node s = n; - if( tmp != n[0] ) { - s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, n.getOperator(), tmp ); - } - s = collapseSelector( s ); - if( s.getKind() == APPLY_SELECTOR ) { - //add selector to selector eq list - Debug("datatypes") << " Add selector to list " << tmp << " " << n << endl; - EqListsN::iterator sel_i = d_selector_eq.find( tmp ); - EqListN* sel; - if( sel_i == d_selector_eq.end() ) { - sel = new(getContext()->getCMM()) EqListN(true, getContext(), false, - ContextMemoryAllocator(getContext()->getCMM())); - d_selector_eq.insertDataFromContextMemory(tmp, sel); - } else { - sel = (*sel_i).second; - } - sel->push_back( s ); - } else { - Debug("datatypes") << " collapsed selector to " << s << endl; - } + if( n.getKind() == APPLY_SELECTOR && d_selectors.find( n ) == d_selectors.end() ) { + Debug("datatypes") << " Found selector " << n << endl; + d_selectors[ n ] = false; + d_cc.addTerm( n ); + Node tmp = find( n[0] ); + d_checkMap[ tmp ] = true; + + //add selector to selector eq list + Debug("datatypes") << " Add selector to list " << tmp << " " << n << endl; + EqListsN::iterator sel_i = d_selector_eq.find( tmp ); + EqListN* sel; + if( sel_i == d_selector_eq.end() ) { + sel = new(getContext()->getCMM()) EqListN(true, getContext(), false, + ContextMemoryAllocator(getContext()->getCMM())); + d_selector_eq.insertDataFromContextMemory(tmp, sel); + } else { + sel = (*sel_i).second; } + sel->push_back( n ); } addTermToLabels( n ); } } - + void TheoryDatatypes::appendToDiseqList(TNode of, TNode eq) { Debug("datatypes") << "appending " << eq << endl << " to diseq list of " << of << endl; @@ -922,51 +928,62 @@ void TheoryDatatypes::appendToDiseqList(TNode of, TNode eq) { //} } -#define DELAY_MERGE - void TheoryDatatypes::addEquality(TNode eq) { Assert(eq.getKind() == kind::EQUAL || eq.getKind() == kind::IFF); - if( find( eq[0] ) != find( eq[1] ) ) { + if( !hasConflict() && find( eq[0] ) != find( eq[1] ) ) { Debug("datatypes") << "Add equality " << eq << "." << endl; Debug("datatypes-debug-pf") << "Add equality " << eq << "." << endl; - +#if 1 //for delayed merging //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_cce.assert(eq); d_cc.addTerm(eq[0]); d_cc.addTerm(eq[1]); - 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; mp.insert( mp.begin(), 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( !hasConflict() ) { merge( eq[0], eq[1] ); + }else{ + Debug("datatypes-debug-pf") << "Forget merge " << eq << std::endl; } -#ifdef DELAY_MERGE //merge nodes waiting to be merged for( int i=0; i<(int)mp.size(); i++ ) { if( !hasConflict() ) { merge( mp[i].first, mp[i].second ); + }else{ + Debug("datatypes-debug-pf") << "Forget merge " << mp[i].first << " " << mp[i].second << std::endl; } } +#elif 0 + Debug("datatypes-ae") << "Add equality " << eq << "." << endl; + Debug("datatypes-ae") << " Find is " << find( eq[0] ) << " = " << find( eq[1] ) << std::endl; + //merge original nodes + merge( eq[0], eq[1] ); + d_cce.assert(eq); + d_cc.addTerm(eq[0]); + d_cc.addTerm(eq[1]); +#else + Debug("datatypes-ae") << "Add equality " << eq << "." << endl; + Debug("datatypes-ae") << " Find is " << find( eq[0] ) << " = " << find( eq[1] ) << std::endl; + merge( eq[0], eq[1] ); + if( !hasConflict() ){ + d_cce.assert(eq); + d_cc.addTerm(eq[0]); + d_cc.addTerm(eq[1]); + } #endif + if( Debug.isOn("datatypes") || Debug.isOn("datatypes-cycles") ){ + d_currEqualities.push_back(eq); + } } } @@ -988,7 +1005,7 @@ void TheoryDatatypes::checkCycles() { NodeBuilder<> explanation(kind::AND); if( searchForCycle( (*i).first, (*i).first, visited, explanation ) ) { Node cCycle = explanation.getNumChildren() == 1 ? explanation.getChild( 0 ) : explanation; - d_em.addNodeConflict( cCycle, Reason::idt_cycle ); + d_em.addNodeConflict( cCycle, Reason::idt_cycle_coarse ); Debug("datatypes") << "Detected cycle for " << (*i).first << endl; Debug("datatypes") << "Conflict is " << cCycle << endl; return; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 23345ef8d..1b9e357ed 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -49,15 +49,16 @@ private: context::CDList d_currAsserts; context::CDList d_currEqualities; - /** list of all selectors */ + /** keeps track of all selectors we care about, value is whether they have been collapsed */ BoolMap d_selectors; - /** list of all representatives */ + /** keeps track of which nodes are representatives */ BoolMap d_reps; - /** map from nodes to a list of selectors whose arguments are in the equivalence class of that node */ + /** map from (representative) nodes to a list of selectors whose arguments are + in the equivalence class of that node */ EqListsN d_selector_eq; - /** map from node representatives to list of nodes in their eq class */ + /** map from (representative) nodes to list of nodes in their eq class */ EqListsN d_equivalence_class; - /** map from terms to whether they have been instantiated */ + /** map from nodes to whether they have been instantiated */ BoolMap d_inst_map; /** transitive closure to record equivalence/subterm relation. */ TransitiveClosureNode d_cycle_check; @@ -69,7 +70,7 @@ private: Node getConstructorForSelector( Node sel ); /** - * map from terms to testers asserted for that term + * map from (representative) nodes to testers that hold for that node * 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 * and n is less than the number of possible constructors for t minus one, @@ -121,14 +122,21 @@ private: /** * information for delayed merging (is this necessary?) */ - bool d_noMerge; std::vector< std::vector< std::pair< Node, Node > > > d_merge_pending; - bool d_inCheck; + + /** + * Terms that currently need to be checked for collapse/instantiation rules + */ + std::map< Node, bool > d_checkMap; /** * explanation manager */ ExplanationManager d_em; + + /** + * explanation manager for the congruence closure module + */ CongruenceClosureExplainer d_cce; public: @@ -148,12 +156,14 @@ private: /* Helper methods */ bool checkTester( Node assertion, Node& conflict, unsigned& r ); void addTester( Node assertion ); - void checkInstantiate( Node t ); - Node collapseSelector( Node t ); + Node getInstantiateCons( Node t ); + void checkInstantiateEqClass( Node t ); + bool checkInstantiate( Node te, Node cons ); + bool collapseSelector( Node t ); void updateSelectors( Node a ); void addTermToLabels( Node t ); void initializeEqClass( Node t ); - void collectTerms( Node n ); + void collectTerms( Node n, bool recurse = true ); bool hasConflict(); /* from uf_morgan */