From 83c0e6c14955e04b3dca56037508e4ceb6691f10 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 14 Nov 2014 12:25:07 +0100 Subject: [PATCH] Be lazier to consider EQC in UF+cardinality solver. Minor cleanup. --- src/theory/quantifiers/options_handlers.h | 6 --- src/theory/quantifiers/term_database.cpp | 1 + src/theory/uf/theory_uf_strong_solver.cpp | 59 +++++++++++++++++++---- src/theory/uf/theory_uf_strong_solver.h | 10 ++++ 4 files changed, 60 insertions(+), 16 deletions(-) diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index f01e563df..e00879303 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -88,9 +88,6 @@ default \n\ none \n\ + Disable model-based quantifier instantiation.\n\ \n\ -instgen \n\ -+ Use instantiation algorithm that mimics Inst-Gen calculus. \n\ -\n\ gen-ev \n\ + Use model-based quantifier instantiation algorithm from CADE 24 finite\n\ model finding paper based on generalizing evaluations.\n\ @@ -98,9 +95,6 @@ gen-ev \n\ fmc-interval \n\ + Same as default, but with intervals for models of integer functions.\n\ \n\ -interval \n\ -+ Use algorithm that abstracts domain elements as intervals. \n\ -\n\ abs \n\ + Use abstract MBQI algorithm (uses disjoint sets). \n\ \n\ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 9a4961e2c..4979a3dfd 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -356,6 +356,7 @@ void TermDb::reset( Theory::Effort effort ){ TNode r = (*eqcs_i); bool addedFirst = false; Node first; + //TODO: ignoring singleton eqc isn't enough, need to ensure eqc are relevant eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); while( !eqc_i.isFinished() ){ TNode n = (*eqc_i); diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index cddaace3e..28ea995d9 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -763,6 +763,7 @@ bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel* if( validRegionIndex!=-1 ){ combineRegions( validRegionIndex, i ); if( addSplit( d_regions[validRegionIndex], out )!=0 ){ + Trace("uf-ss-debug") << "Minimize model : combined regions, found split. " << std::endl; return false; } }else{ @@ -770,9 +771,12 @@ bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel* } } } + Assert( validRegionIndex!=-1 ); if( addSplit( d_regions[validRegionIndex], out )!=0 ){ + Trace("uf-ss-debug") << "Minimize model : found split. " << std::endl; return false; } + Trace("uf-ss-debug") << "Minimize success. " << std::endl; } } return true; @@ -1480,7 +1484,7 @@ Node StrongSolverTheoryUF::SortModel::getCardinalityLiteral( int c ) { StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) : d_out( &out ), d_th( th ), d_conflict( c, false ), d_rep_model(), d_aloc_com_card( u, 0 ), d_com_card_assertions( c ), -d_card_assertions_eqv_lemma( u ) +d_card_assertions_eqv_lemma( u ), d_rel_eqc( c ) { if( options::ufssDiseqPropagation() ){ d_deq_prop = new DisequalityPropagator( th->getQuantifiersEngine(), this ); @@ -1508,26 +1512,58 @@ OutputChannel& StrongSolverTheoryUF::getOutputChannel() { return d_th->getOutputChannel(); } +/** ensure eqc */ +void StrongSolverTheoryUF::ensureEqc( SortModel* c, Node a ) { + if( !hasEqc( a ) ){ + d_rel_eqc[a] = true; + Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl; + c->newEqClass( a ); + if( options::ufssSymBreak() ){ + d_sym_break->newEqClass( a ); + } + Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl; + } +} + +void StrongSolverTheoryUF::ensureEqcRec( Node n ) { + if( !hasEqc( n ) ){ + SortModel* c = getSortModel( n ); + if( c ){ + ensureEqc( c, n ); + } + for( unsigned i=0; inewEqClass( n ); - if( options::ufssSymBreak() ){ - d_sym_break->newEqClass( n ); - } - Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl; + //do nothing } } /** merge */ void StrongSolverTheoryUF::merge( Node a, Node b ){ + //TODO: ensure they are relevant SortModel* c = getSortModel( a ); if( c ){ - Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl; - c->merge( a, b ); - Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Merge." << std::endl; + ensureEqc( c, a ); + if( hasEqc( b ) ){ + Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl; + c->merge( a, b ); + Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Merge." << std::endl; + }else{ + //c->assignEqClass( b, a ); + d_rel_eqc[b] = true; + } }else{ if( options::ufssDiseqPropagation() ){ d_deq_prop->merge(a, b); @@ -1539,6 +1575,8 @@ void StrongSolverTheoryUF::merge( Node a, Node b ){ void StrongSolverTheoryUF::assertDisequal( Node a, Node b, Node reason ){ SortModel* c = getSortModel( a ); if( c ){ + ensureEqc( c, a ); + ensureEqc( c, b ); Trace("uf-ss-solver") << "StrongSolverTheoryUF: Assert disequal " << a << " " << b << " : " << a.getType() << std::endl; //Assert( d_th->d_equalityEngine.getRepresentative( a )==a ); //Assert( d_th->d_equalityEngine.getRepresentative( b )==b ); @@ -1554,6 +1592,7 @@ void StrongSolverTheoryUF::assertDisequal( Node a, Node b, Node reason ){ /** assert a node */ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){ Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl; + ensureEqcRec( n ); bool polarity = n.getKind() != kind::NOT; TNode lit = polarity ? n : n[0]; if( lit.getKind()==CARDINALITY_CONSTRAINT ){ diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 333f1717e..af316927d 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -320,6 +320,16 @@ private: void allocateCombinedCardinality(); /** check */ void checkCombinedCardinality(); +private: + /** relevant eqc */ + NodeBoolMap d_rel_eqc; + /** ensure eqc */ + void ensureEqc( SortModel* c, Node a ); + /** ensure eqc for all subterms of n */ + void ensureEqcRec( Node n ); +public: + /** has eqc */ + bool hasEqc( Node a ); private: /** disequality propagator */ DisequalityPropagator* d_deq_prop; -- 2.30.2