From 49d1898de725a5fac3f68845809ba152eae11282 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 9 Feb 2016 13:23:18 -0600 Subject: [PATCH] Eager introduction of eqc, lemma cache for ground fmf. Apply preprocessing to quantifier instantiations. --- src/smt/smt_engine.cpp | 13 ++-- .../quantifiers/quantifiers_rewriter.cpp | 12 +++ src/theory/quantifiers/quantifiers_rewriter.h | 4 +- src/theory/quantifiers_engine.cpp | 2 + src/theory/uf/theory_uf_strong_solver.cpp | 75 ++++++++++++++----- src/theory/uf/theory_uf_strong_solver.h | 4 + 6 files changed, 81 insertions(+), 29 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 850b37fe0..deb9770c0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3895,14 +3895,11 @@ void SmtEnginePrivate::processAssertions() { //apply pre-skolemization to existential quantifiers for (unsigned i = 0; i < d_assertions.size(); ++ i) { Node prev = d_assertions[i]; - Trace("quantifiers-rewrite-debug") << "Pre-skolemize " << prev << "..." << std::endl; - vector< TypeNode > fvTypes; - vector< TNode > fvs; - d_assertions.replace(i, quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs )); - if( prev!=d_assertions[i] ){ - d_assertions.replace(i, Rewriter::rewrite( d_assertions[i] )); - Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl; - Trace("quantifiers-rewrite") << " ...got " << d_assertions[i] << endl; + Node next = quantifiers::QuantifiersRewriter::preprocess( prev ); + if( next!=prev ){ + d_assertions.replace(i, Rewriter::rewrite( next )); + Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl; + Trace("quantifiers-preprocess") << " ...got " << d_assertions[i] << endl; } } } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index fc5b692b2..462f8377f 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1737,6 +1737,18 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v return n; } +Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { + if( options::preSkolemQuant() ){ + if( !isInst || !options::preSkolemQuantNested() ){ + //apply pre-skolemization to existential quantifiers + Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl; + std::vector< TypeNode > fvTypes; + std::vector< TNode > fvs; + n = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( n, true, fvTypes, fvs ); + } + } + return n; +} Node QuantifiersRewriter::computePurify2( Node body, std::vector< Node >& args, std::map< Node, Node >& visited, std::map< Node, Node >& var_to_term, std::map< Node, std::vector< int > >& var_parent, int parentId ){ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 38c1bdd58..47997f9a7 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -91,10 +91,12 @@ public: private: /** options */ static bool doOperation( Node f, bool isNested, int computeOption ); +private: + static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector& fvs); public: static Node rewriteRewriteRule( Node r ); static bool containsQuantifiers(Node n); - static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector& fvs); + static Node preprocess( Node n, bool isInst = false ); };/* class QuantifiersRewriter */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 19d66165a..6fedc14f0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -695,6 +695,8 @@ bool QuantifiersEngine::addInstantiationInternal( Node f, std::vector< Node >& v Trace("quant-vts-debug") << " ...result: " << body_r << std::endl; body = body_r; } + body = quantifiers::QuantifiersRewriter::preprocess( body, true ); + Trace("inst-debug") << "...preprocess to " << body << std::endl; Trace("inst-assert") << "(assert " << body << ")" << std::endl; //make the lemma Node lem = NodeManager::currentNM()->mkNode( kind::OR, f.negate(), body ); diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 9fceedc96..3ed1c4d40 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -26,6 +26,7 @@ //#define ONE_SPLIT_REGION //#define DISABLE_QUICK_CLIQUE_CHECKS //#define COMBINE_REGIONS_SMALL_INTO_LARGE +//#define LAZY_REL_EQC using namespace std; using namespace CVC4; @@ -406,7 +407,7 @@ void StrongSolverTheoryUF::SortModel::Region::debugPrint( const char* c, bool in StrongSolverTheoryUF::SortModel::SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ) : d_type( n.getType() ), d_thss( thss ), d_regions_index( c, 0 ), d_regions_map( c ), d_split_score( c ), d_disequalities_index( c, 0 ), d_reps( c, 0 ), d_conflict( c, false ), d_cardinality( c, 1 ), d_aloc_cardinality( u, 0 ), - d_cardinality_assertions( c ), d_hasCard( c, false ), d_maxNegCard( c, 0 ), d_initialized( u, false ){ + d_cardinality_assertions( c ), d_hasCard( c, false ), d_maxNegCard( c, 0 ), d_initialized( u, false ), d_lemma_cache( u ){ d_cardinality_term = n; //if( d_type.isSort() ){ // TypeEnumerator te(tn); @@ -1070,11 +1071,12 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){ //add splitting lemma for cardinality constraint Assert( !d_cardinality_term.isNull() ); Node lem = getCardinalityLiteral( d_aloc_cardinality ); - Trace("uf-ss-lemma") << "*** Cardinality split on : " << lem << std::endl; lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() ); d_cardinality_lemma[ d_aloc_cardinality ] = lem; //add as lemma to output channel - out->lemma( lem ); + if( doSendLemma( lem ) ){ + Trace("uf-ss-lemma") << "*** Cardinality split on : " << lem << std::endl; + } //require phase out->requirePhase( d_cardinality_literal[ d_aloc_cardinality ], true ); //add the appropriate lemma, propagate as decision @@ -1121,7 +1123,6 @@ int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ if (!s.isNull() ){ //add lemma to output channel Assert( s.getKind()==EQUAL ); - Trace("uf-ss-lemma") << "*** Split on " << s << std::endl; Node ss = Rewriter::rewrite( s ); if( ss.getKind()!=EQUAL ){ Node b_t = NodeManager::currentNM()->mkConst( true ); @@ -1150,10 +1151,13 @@ int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl; //Notice() << "*** Split on " << s << std::endl; //split on the equality s - out->split( ss ); - //tell the sat solver to explore the equals branch first - out->requirePhase( ss, true ); - ++( d_thss->d_statistics.d_split_lemmas ); + Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() ); + if( doSendLemma( lem ) ){ + Trace("uf-ss-lemma") << "*** Split on " << s << std::endl; + //tell the sat solver to explore the equals branch first + out->requirePhase( ss, true ); + ++( d_thss->d_statistics.d_split_lemmas ); + } return 1; }else{ return 0; @@ -1185,9 +1189,10 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu } eqs.push_back( d_cardinality_literal[ d_cardinality ].notNode() ); Node lem = NodeManager::currentNM()->mkNode( OR, eqs ); - Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl; - ++( d_thss->d_statistics.d_clique_lemmas ); - out->lemma( lem ); + if( doSendLemma( lem ) ){ + Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl; + ++( d_thss->d_statistics.d_clique_lemmas ); + } }else{ //found a clique Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl; @@ -1303,9 +1308,10 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu //Assert( hasValue ); //Assert( value ); conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() ); - Trace("uf-ss-lemma") << "*** Add clique lemma " << conflictNode << std::endl; - out->lemma( conflictNode ); - ++( d_thss->d_statistics.d_clique_lemmas ); + if( doSendLemma( conflictNode ) ){ + Trace("uf-ss-lemma") << "*** Add clique lemma " << conflictNode << std::endl; + ++( d_thss->d_statistics.d_clique_lemmas ); + } } //DO_THIS: ensure that the same clique is not reported??? Check standard effort after assertDisequal can produce same clique. @@ -1364,10 +1370,9 @@ void StrongSolverTheoryUF::SortModel::addTotalityAxiom( Node n, int cardinality, } void StrongSolverTheoryUF::SortModel::addClique( int c, std::vector< Node >& clique ) { - - if( d_clique_trie[c].add( clique ) ){ - d_cliques[ c ].push_back( clique ); - } + //if( d_clique_trie[c].add( clique ) ){ + // d_cliques[ c ].push_back( clique ); + //} } @@ -1395,6 +1400,16 @@ void StrongSolverTheoryUF::SortModel::simpleCheckCardinality() { } } +bool StrongSolverTheoryUF::SortModel::doSendLemma( Node lem ) { + if( d_lemma_cache.find( lem )==d_lemma_cache.end() ){ + d_lemma_cache[lem] = true; + d_thss->getOutputChannel().lemma( lem ); + return true; + }else{ + return false; + } +} + void StrongSolverTheoryUF::SortModel::debugPrint( const char* c ){ Debug( c ) << "-- Conflict Find:" << std::endl; Debug( c ) << "Number of reps = " << d_reps << std::endl; @@ -1568,10 +1583,19 @@ bool StrongSolverTheoryUF::hasEqc( Node a ) { } /** new node */ -void StrongSolverTheoryUF::newEqClass( Node n ){ - SortModel* c = getSortModel( n ); +void StrongSolverTheoryUF::newEqClass( Node a ){ + SortModel* c = getSortModel( a ); if( c ){ +#ifdef LAZY_REL_EQC //do nothing +#else + 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; +#endif } } @@ -1580,6 +1604,7 @@ void StrongSolverTheoryUF::merge( Node a, Node b ){ //TODO: ensure they are relevant SortModel* c = getSortModel( a ); if( c ){ +#ifdef LAZY_REL_EQC ensureEqc( c, a ); if( hasEqc( b ) ){ Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl; @@ -1589,6 +1614,11 @@ void StrongSolverTheoryUF::merge( Node a, Node b ){ //c->assignEqClass( b, a ); d_rel_eqc[b] = true; } +#else + 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; +#endif }else{ if( options::ufssDiseqPropagation() ){ d_deq_prop->merge(a, b); @@ -1600,8 +1630,10 @@ void StrongSolverTheoryUF::merge( Node a, Node b ){ void StrongSolverTheoryUF::assertDisequal( Node a, Node b, Node reason ){ SortModel* c = getSortModel( a ); if( c ){ +#ifdef LAZY_REL_EQC ensureEqc( c, a ); ensureEqc( c, b ); +#endif 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 ); @@ -1617,7 +1649,9 @@ 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; +#ifdef LAZY_REL_EQC ensureEqcRec( n ); +#endif bool polarity = n.getKind() != kind::NOT; TNode lit = polarity ? n : n[0]; if( lit.getKind()==CARDINALITY_CONSTRAINT ){ @@ -2042,6 +2076,7 @@ void StrongSolverTheoryUF::allocateCombinedCardinality() { d_com_card_literal[ d_aloc_com_card.get() ] = lem; lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() ); //add as lemma to output channel + Trace("uf-ss-lemma") << "*** Combined cardinality split : " << lem << std::endl; getOutputChannel().lemma( lem ); //require phase getOutputChannel().requirePhase( d_com_card_literal[ d_aloc_com_card.get() ], true ); diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 24d7f840f..db4c50423 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -244,6 +244,8 @@ public: std::vector< Node > d_fresh_aloc_reps; /** whether we are initialized */ context::CDO< bool > d_initialized; + /** cache for lemmas */ + NodeBoolMap d_lemma_cache; private: /** apply totality */ bool applyTotality( int cardinality ); @@ -251,6 +253,8 @@ public: Node getTotalityLemmaTerm( int cardinality, int i ); /** simple check cardinality */ void simpleCheckCardinality(); + private: + bool doSendLemma( Node lem ); public: SortModel( Node n, context::Context* c, context::UserContext* u, StrongSolverTheoryUF* thss ); virtual ~SortModel(){} -- 2.30.2