From f81c51ca8af1c38126336f0c31a33fba72614dc1 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 3 Mar 2017 16:17:24 -0600 Subject: Fix for collectModelInfo related to finite types + preregistration. Generalize previous fix for sets, minor changes to Datatypes. --- src/theory/datatypes/theory_datatypes.cpp | 115 +++++++++++++--------------- src/theory/datatypes/theory_datatypes.h | 2 + src/theory/sep/theory_sep.cpp | 7 +- src/theory/sets/theory_sets_private.cpp | 18 ++--- src/theory/strings/theory_strings.cpp | 9 +++ src/theory/uf/theory_uf.cpp | 7 +- test/regress/regress0/sets/Makefile.am | 4 +- test/regress/regress0/sets/abt-te-exh2.smt2 | 24 ++++++ 8 files changed, 109 insertions(+), 77 deletions(-) create mode 100644 test/regress/regress0/sets/abt-te-exh2.smt2 diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index b66cb15ff..d285f292a 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -173,7 +173,7 @@ void TheoryDatatypes::check(Effort e) { return; } }while( d_addedFact ); - + //check for splits Trace("datatypes-debug") << "Check for splits " << e << endl; do { @@ -183,6 +183,7 @@ void TheoryDatatypes::check(Effort e) { eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node n = (*eqcs_i); + //TODO : avoid irrelevant (pre-registered but not asserted) terms here? TypeNode tn = n.getType(); if( tn.isDatatype() ){ Trace("datatypes-debug") << "Process equivalence class " << n << std::endl; @@ -1414,9 +1415,15 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ Trace("dt-model") << std::endl; printModelDebug( "dt-model" ); Trace("dt-model") << std::endl; + + set termSet; + + // Compute terms appearing in assertions and shared terms, and in inferred equalities + getRelevantTerms(termSet); //combine the equality engine - m->assertEqualityEngine( &d_equalityEngine ); + m->assertEqualityEngine( &d_equalityEngine, &termSet ); + //get all constructors eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine ); @@ -1426,18 +1433,22 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ while( !eqccs_i.isFinished() ){ Node eqc = (*eqccs_i); //for all equivalence classes that are datatypes - if( eqc.getType().isDatatype() ){ - EqcInfo* ei = getOrMakeEqcInfo( eqc ); - if( ei && !ei->d_constructor.get().isNull() ){ - Node c = ei->d_constructor.get(); - cons.push_back( c ); - eqc_cons[ eqc ] = c; - }else{ - //if eqc contains a symbol known to datatypes (a selector), then we must assign - //should assign constructors to EQC if they have a selector or a tester - bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc ); - if( shouldConsider ){ - nodes.push_back( eqc ); + if( termSet.find( eqc )==termSet.end() ){ + Trace("dt-cmi-debug") << "Irrelevant eqc : " << eqc << std::endl; + }else{ + if( eqc.getType().isDatatype() ){ + EqcInfo* ei = getOrMakeEqcInfo( eqc ); + if( ei && !ei->d_constructor.get().isNull() ){ + Node c = ei->d_constructor.get(); + cons.push_back( c ); + eqc_cons[ eqc ] = c; + }else{ + //if eqc contains a symbol known to datatypes (a selector), then we must assign + //should assign constructors to EQC if they have a selector or a tester + bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc ); + if( shouldConsider ){ + nodes.push_back( eqc ); + } } } } @@ -1456,54 +1467,6 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ const Datatype& dt = ((DatatypeType)tt).getDatatype(); if( !d_equalityEngine.hasTerm( eqc ) ){ Assert( false ); - /* - if( !dt.isCodatatype() ){ - Trace("dt-cmi") << "NOTICE : Datatypes: need to assign constructor for " << eqc << std::endl; - Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; - TypeNode tn = eqc.getType(); - //if it is infinite, make sure it is fresh - // this ensures that the term that this is an argument of is distinct. - if( eqc.getType().getCardinality().isInfinite() ){ - std::map< TypeNode, int >::iterator it = typ_enum_map.find( tn ); - int teIndex; - if( it==typ_enum_map.end() ){ - teIndex = (int)typ_enum.size(); - typ_enum_map[tn] = teIndex; - typ_enum.push_back( TypeEnumerator(tn) ); - }else{ - teIndex = it->second; - } - bool success; - do{ - success = true; - Assert( !typ_enum[teIndex].isFinished() ); - neqc = *typ_enum[teIndex]; - Trace("dt-cmi-debug") << "Try " << neqc << " ... " << std::endl; - ++typ_enum[teIndex]; - for( unsigned i=0; iareEqual( cons[i][j], neqc[j] ) ){ - diff = true; - break; - } - } - if( !diff ){ - Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; - success = false; - break; - } - } - } - }while( !success ); - }else{ - TypeEnumerator te(tn); - neqc = *te; - } - } - */ }else{ Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl; Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; @@ -2186,6 +2149,34 @@ bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >& return false; } +void TheoryDatatypes::getRelevantTerms( std::set& termSet ) { + // Compute terms appearing in assertions and shared terms + computeRelevantTerms(termSet); + + //also include non-singleton equivalence classes + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + TNode r = (*eqcs_i); + bool addedFirst = false; + Node first; + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + TNode n = (*eqc_i); + if( first.isNull() ){ + first = n; + }else{ + if( !addedFirst ){ + addedFirst = true; + termSet.insert( first ); + } + termSet.insert( n ); + } + ++eqc_i; + } + ++eqcs_i; + } +} + std::pair TheoryDatatypes::entailmentCheck(TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* out) { Trace("dt-entail") << "Check entailed : " << lit << std::endl; Node atom = lit.getKind()==NOT ? lit[0] : lit; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 49c45590c..770c3a9d4 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -310,6 +310,8 @@ private: bool mustCommunicateFact( Node n, Node exp ); /** check clash mod eq */ bool checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand ); + /** get relevant terms */ + void getRelevantTerms( std::set& termSet ); private: //equality queries bool hasTerm( TNode a ); diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 81afc0da2..4f31f10b5 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -201,8 +201,13 @@ void TheorySep::computeCareGraph() { void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel ){ + set termSet; + + // Compute terms appearing in assertions and shared terms + computeRelevantTerms(termSet); + // Send the equality engine information to the model - m->assertEqualityEngine( &d_equalityEngine ); + m->assertEqualityEngine( &d_equalityEngine, &termSet ); } void TheorySep::postProcessModel( TheoryModel* m ){ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 7d2bbf3d1..e78575791 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -506,7 +506,6 @@ void TheorySetsPrivate::fullEffortCheck(){ d_sentLemma = false; d_addedFact = false; d_set_eqc.clear(); - d_set_eqc_relevant.clear(); d_set_eqc_list.clear(); d_eqc_emptyset.clear(); d_eqc_singleton.clear(); @@ -532,9 +531,6 @@ void TheorySetsPrivate::fullEffortCheck(){ if( tn.isSet() ){ isSet = true; d_set_eqc.push_back( eqc ); - if( d_equalityEngine.isTriggerTerm(eqc, THEORY_SETS) ){ - d_set_eqc_relevant[eqc] = true; - } } Trace("sets-eqc") << "[" << eqc << "] : "; eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); @@ -551,7 +547,6 @@ void TheorySetsPrivate::fullEffortCheck(){ if( pindex!=-1 ){ if( d_pol_mems[pindex][s].find( x )==d_pol_mems[pindex][s].end() ){ d_pol_mems[pindex][s][x] = n; - d_set_eqc_relevant[s] = true; Trace("sets-debug2") << "Membership[" << x << "][" << s << "] : " << n << ", pindex = " << pindex << std::endl; } if( d_members_index[s].find( x )==d_members_index[s].end() ){ @@ -579,8 +574,6 @@ void TheorySetsPrivate::fullEffortCheck(){ }else{ Node r1 = d_equalityEngine.getRepresentative( n[0] ); Node r2 = d_equalityEngine.getRepresentative( n[1] ); - d_set_eqc_relevant[r1] = true; - d_set_eqc_relevant[r2] = true; if( d_bop_index[n.getKind()][r1].find( r2 )==d_bop_index[n.getKind()][r1].end() ){ d_bop_index[n.getKind()][r1][r2] = n; d_op_list[n.getKind()].push_back( n ); @@ -601,7 +594,6 @@ void TheorySetsPrivate::fullEffortCheck(){ //TODO: extend approach for this case } Node r = d_equalityEngine.getRepresentative( n[0] ); - d_set_eqc_relevant[r] = true; if( d_eqc_to_card_term.find( r )==d_eqc_to_card_term.end() ){ d_eqc_to_card_term[ r ] = n; registerCardinalityTerm( n[0], lemmas ); @@ -1740,14 +1732,18 @@ EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) { void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) { - Trace("sets") << "Set collect model info" << std::endl; + Trace("sets-model") << "Set collect model info" << std::endl; + set termSet; + // Compute terms appearing in assertions and shared terms + d_external.computeRelevantTerms(termSet); + // Assert equalities and disequalities to the model - m->assertEqualityEngine(&d_equalityEngine); + m->assertEqualityEngine(&d_equalityEngine,&termSet); std::map< Node, Node > mvals; for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){ Node eqc = d_set_eqc[i]; - if( d_set_eqc_relevant.find( eqc )==d_set_eqc_relevant.end() ){ + if( termSet.find( eqc )==termSet.end() ){ Trace("sets-model") << "* Do not assign value for " << eqc << " since is not relevant." << std::endl; }else{ std::vector< Node > els; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 09cc3cb3b..45a6a93d1 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -442,7 +442,16 @@ void TheoryStrings::presolve() { void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { Trace("strings-model") << "TheoryStrings : Collect model info, fullModel = " << fullModel << std::endl; Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl; + + //AJR : no use doing this since we cannot preregister terms with finite types that don't belong to strings. + // change this if we generalize to sequences. + //set termSet; + // Compute terms appearing in assertions and shared terms + //computeRelevantTerms(termSet); + //m->assertEqualityEngine( &d_equalityEngine, &termSet ); + m->assertEqualityEngine( &d_equalityEngine ); + // Generate model std::vector< Node > nodes; getEquivalenceClasses( nodes ); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index e4a3ac78c..35aee5305 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -246,7 +246,12 @@ Node TheoryUF::explain(TNode literal, eq::EqProof* pf) { } void TheoryUF::collectModelInfo( TheoryModel* m, bool fullModel ){ - m->assertEqualityEngine( &d_equalityEngine ); + set termSet; + + // Compute terms appearing in assertions and shared terms + computeRelevantTerms(termSet); + + m->assertEqualityEngine( &d_equalityEngine, &termSet ); // if( fullModel ){ // std::map< TypeNode, TypeEnumerator* > type_enums; // //must choose proper representatives diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 62f8665ec..f4f921c43 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -73,8 +73,8 @@ TESTS = \ card-6.smt2 \ card-7.smt2 \ abt-min.smt2 \ - abt-te-exh.smt2 - + abt-te-exh.smt2 \ + abt-te-exh2.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/sets/abt-te-exh2.smt2 b/test/regress/regress0/sets/abt-te-exh2.smt2 new file mode 100644 index 000000000..9ff80e14c --- /dev/null +++ b/test/regress/regress0/sets/abt-te-exh2.smt2 @@ -0,0 +1,24 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic ALL) +(declare-sort Atom 0) + +(declare-fun p ((Set Atom) (Set Atom)) (Set Atom)) +(declare-fun j ((Set Atom) (Set Atom)) (Set Atom)) +(declare-fun k ((Set Atom) (Set Atom)) (Set Atom)) +(declare-fun d ((Set Atom) (Set Atom)) (Set Atom)) + +(declare-fun a () (Set Atom)) +(declare-fun n () Atom) +(declare-fun v () Atom) + +(assert (forall ((b Atom) (c Atom)) +(or +(member v (k (singleton n) (j (singleton b) a))) +(= (as emptyset (Set Atom)) (d (j (singleton b) a) (singleton n))) +) +) +) + +(check-sat) + -- cgit v1.2.3