From 94fe6a0d525bff3cdd4450b2abd04eb2cb044308 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 13 Jan 2016 23:08:40 +0100 Subject: [PATCH] Lemma cache datatypes. Do not send true lemma in quantifiers. Minor fix for datatypes model generation for UFinite datatypes when FMF. --- src/theory/datatypes/theory_datatypes.cpp | 58 +++++++++++++++-------- src/theory/datatypes/theory_datatypes.h | 8 ++-- src/theory/quantifiers_engine.cpp | 2 + src/theory/strings/theory_strings.cpp | 1 + 4 files changed, 46 insertions(+), 23 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 9ba20fcc9..35d82b2ae 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -57,7 +57,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_collectTermsCache( c ), d_consTerms( c ), d_selTerms( c ), - d_singleton_eq( u ) + d_singleton_eq( u ), + d_lemmas_produced_c( u ) { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); @@ -131,6 +132,7 @@ void TheoryDatatypes::check(Effort e) { if (done() && !fullEffort(e)) { return; } + Assert( d_pending.empty() && d_pending_merge.empty() ); d_addedLemma = false; TimerStat::CodeTimer checkTimer(d_checkTime); @@ -221,7 +223,7 @@ void TheoryDatatypes::check(Effort e) { assumptions.push_back( eq ); Node lemma = assumptions.size()==1 ? assumptions[0] : NodeManager::currentNM()->mkNode( OR, assumptions ); Trace("dt-singleton") << "*************Singleton equality lemma " << lemma << std::endl; - d_out->lemma( lemma ); + doSendLemma( lemma ); } } }else{ @@ -246,7 +248,7 @@ void TheoryDatatypes::check(Effort e) { if( consIndex==-1 ){ consIndex = j; } - if( !dt[ j ].isFinite() && ( !options::finiteModelFind() || !dt.isUFinite() ) ) { + if( options::finiteModelFind() ? !dt[ j ].isUFinite() : !dt[ j ].isFinite() ) { if( !eqc || !eqc->d_selectors ){ needSplit = false; } @@ -281,7 +283,7 @@ void TheoryDatatypes::check(Effort e) { NodeBuilder<> nb(kind::OR); nb << test << test.notNode(); Node lemma = nb; - d_out->lemma( lemma ); + doSendLemma( lemma ); d_out->requirePhase( test, true ); }else{ Trace("dt-split") << "*************Split for constructors on " << n << endl; @@ -291,7 +293,7 @@ void TheoryDatatypes::check(Effort e) { d_sygus_split->getSygusSplits( n, dt, children, lemmas ); for( unsigned i=0; ilemma( lemmas[i] ); + doSendLemma( lemmas[i] ); } }else{ for( unsigned i=0; imkNode( kind::OR, children ); Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl; - d_out->lemma( lemma ); + doSendLemma( lemma ); } return; } @@ -339,6 +341,7 @@ void TheoryDatatypes::check(Effort e) { } } + Trace("datatypes-check") << "Finished check effort " << e << std::endl; if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) { Notice() << "TheoryDatatypes::check(): done" << endl; } @@ -365,7 +368,7 @@ void TheoryDatatypes::flushPendingFacts(){ lem = Rewriter::rewrite( lem ); } Trace("dt-lemma") << "Datatypes lemma : " << lem << std::endl; - d_out->lemma( lem ); + doSendLemma( lem ); d_addedLemma = true; }else{ assertFact( fact, exp ); @@ -390,6 +393,13 @@ void TheoryDatatypes::doPendingMerges(){ d_pending_merge.clear(); } +void TheoryDatatypes::doSendLemma( Node lem ) { + if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){ + d_lemmas_produced_c[lem] = true; + d_out->lemma( lem ); + } +} + void TheoryDatatypes::assertFact( Node fact, Node exp ){ Assert( d_pending_merge.empty() ); bool polarity = fact.getKind() != kind::NOT; @@ -412,7 +422,7 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){ d_sygus_sym_break->addTester( atom ); for( unsigned i=0; id_lemmas.size(); i++ ){ Trace("dt-lemma-sygus") << "Sygus symmetry breaking lemma : " << d_sygus_sym_break->d_lemmas[i] << std::endl; - d_out->lemma( d_sygus_sym_break->d_lemmas[i] ); + doSendLemma( d_sygus_sym_break->d_lemmas[i] ); } d_sygus_sym_break->d_lemmas.clear(); /* @@ -768,6 +778,7 @@ void TheoryDatatypes::eqNotifyPreMerge(TNode t1, TNode t2){ /** called when two equivalance classes have merged */ void TheoryDatatypes::eqNotifyPostMerge(TNode t1, TNode t2){ if( DatatypesRewriter::isTermDatatype( t1 ) ){ + Debug("datatypes-debug") << "NotifyPostMerge : " << t1 << " " << t2 << std::endl; d_pending_merge.push_back( t1.eqNode( t2 ) ); } } @@ -785,6 +796,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ } EqcInfo* eqc1 = getOrMakeEqcInfo( t1 ); if( eqc1 ){ + Debug("datatypes-debug") << " merge eqc info " << eqc2 << " into " << eqc1 << std::endl; if( !eqc1->d_constructor.get().isNull() ){ trep1 = eqc1->d_constructor.get(); } @@ -793,7 +805,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ TNode cons2 = eqc2->d_constructor.get(); //if both have constructor, then either clash or unification if( !cons1.isNull() && !cons2.isNull() ){ - Debug("datatypes-debug") << "Constructors : " << cons1 << " " << cons2 << std::endl; + Debug("datatypes-debug") << " constructors : " << cons1 << " " << cons2 << std::endl; Node unifEq = cons1.eqNode( cons2 ); /* std::vector< Node > exp; @@ -812,6 +824,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ if( conf ){ exp.push_back( unifEq ); d_conflictNode = explain( exp ); + } */ std::vector< Node > rew; if( DatatypesRewriter::checkClash( cons1, cons2, rew ) ){ @@ -844,12 +857,11 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ */ } } - if( !eqc1->d_inst && eqc2->d_inst ){ - eqc1->d_inst = true; - } + Debug("datatypes-debug") << " instantiated : " << eqc1->d_inst << " " << eqc2->d_inst << std::endl; + eqc1->d_inst = eqc1->d_inst || eqc2->d_inst; if( !cons2.isNull() ){ if( cons1.isNull() ){ - Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl; + Debug("datatypes-debug") << " must check if it is okay to set the constructor." << std::endl; checkInst = true; addConstructor( eqc2->d_constructor.get(), eqc1, t1 ); if( d_conflict ){ @@ -860,7 +872,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ //d_consEqc[t2] = false; } }else{ - Debug("datatypes-debug") << "No eqc info for " << t1 << ", must create" << std::endl; + Debug("datatypes-debug") << " no eqc info for " << t1 << ", must create" << std::endl; //just copy the equivalence class information eqc1 = getOrMakeEqcInfo( t1, true ); eqc1->d_inst.set( eqc2->d_inst ); @@ -872,12 +884,12 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ //merge labels NodeListMap::iterator lbl_i = d_labels.find( t2 ); if( lbl_i != d_labels.end() ){ - Debug("datatypes-debug") << "Merge labels from " << eqc2 << " " << t2 << std::endl; + Debug("datatypes-debug") << " merge labels from " << eqc2 << " " << t2 << std::endl; NodeList* lbl = (*lbl_i).second; for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); ++j ){ addTester( *j, eqc1, t1 ); if( d_conflict ){ - Debug("datatypes-debug") << "Conflict!" << std::endl; + Debug("datatypes-debug") << " conflict!" << std::endl; return; } } @@ -889,19 +901,21 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ } NodeListMap::iterator sel_i = d_selector_apps.find( t2 ); if( sel_i != d_selector_apps.end() ){ - Debug("datatypes-debug") << "Merge selectors from " << eqc2 << " " << t2 << std::endl; + Debug("datatypes-debug") << " merge selectors from " << eqc2 << " " << t2 << std::endl; NodeList* sel = (*sel_i).second; for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){ addSelector( *j, eqc1, t1, eqc2->d_constructor.get().isNull() ); } } if( checkInst ){ + Debug("datatypes-debug") << " checking instantiate" << std::endl; instantiate( eqc1, t1 ); if( d_conflict ){ return; } } } + Debug("datatypes-debug") << "Finished Merge " << t1 << " " << t2 << std::endl; } } @@ -1363,7 +1377,8 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ if( neqc.isNull() ){ for( unsigned i=0; imkSkolem( "k2", tn ); a = v1.eqNode( v2 ).negate(); //send out immediately as lemma - d_out->lemma( a ); + doSendLemma( a ); Trace("dt-singleton") << "******** assert " << a << " to avoid singleton cardinality for type " << tn << std::endl; } d_singleton_lemma[index][tn] = a; @@ -1554,7 +1569,9 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index k = NodeManager::currentNM()->mkSkolem( "k", n.getType(), "for dt instantiation" ); Node eq = k.eqNode( n ); Trace("datatypes-infer") << "DtInfer : instantiation ref : " << eq << std::endl; - d_out->lemma( eq ); + //doSendLemma( eq ); + d_pending.push_back( eq ); + d_pending_exp[ eq ] = d_true; } Node n_ic = DatatypesRewriter::getInstCons( k, dt, index ); //Assert( n_ic==Rewriter::rewrite( n_ic ) ); @@ -1592,6 +1609,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl; d_pending.push_back( eq ); d_pending_exp[ eq ] = exp; + Trace("datatypes-infer-debug") << "inst : " << eqc << " " << n << std::endl; Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp << std::endl; //eqc->d_inst.set( eq ); d_infer.push_back( eq ); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index fc6e435cc..212b9d7cf 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -184,10 +184,11 @@ private: private: /** singleton lemmas (for degenerate co-datatype case) */ std::map< TypeNode, Node > d_singleton_lemma[2]; - /** Cache for singleton equalities processed */ BoolMap d_singleton_eq; - + /** list of all lemmas produced */ + BoolMap d_lemmas_produced_c; +private: /** assert fact */ void assertFact( Node fact, Node exp ); @@ -196,7 +197,8 @@ private: /** do pending merged */ void doPendingMerges(); - + /** do send lemma */ + void doSendLemma( Node lem ); /** get or make eqc info */ EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 3813d7cd2..e7a87927a 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -95,6 +95,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_term_db = new quantifiers::TermDb( c, u, this ); d_tr_trie = new inst::TriggerTrie; d_hasAddedLemma = false; + //don't add true lemma + d_lemmas_produced_c[d_term_db->d_true] = true; Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 4405fe406..07a170a08 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -4023,6 +4023,7 @@ void TheoryStrings::checkExtendedFuncs() { addMembership( it->first ? it->second[i] : it->second[i].negate() ); } } + Trace("strings-process") << "Checking memberships..." << std::endl; checkMemberships(); Trace("strings-process") << "Done check memberships, addedLemma = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; } -- 2.30.2