From 472c5a592c78e4757b3201f9e20908a4c645921b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 4 Oct 2019 02:12:02 -0500 Subject: [PATCH] Avoid duplicate lemmas in datatypes (#3310) We previously were sending e.g. dt.size >= 0 lemmas when size terms are pre-registered, which can happen multiple times in a user context. This ensures we cache whether a lemma is sent in a user-context dependent way in the datatypes solver. This ensures we don't send the same lemma twice for dt.size >= 0 lemmas. --- src/theory/datatypes/theory_datatypes.cpp | 142 +++++++++++----------- src/theory/datatypes/theory_datatypes.h | 10 +- 2 files changed, 82 insertions(+), 70 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 609cdaf6e..8bac280b6 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -57,6 +57,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, d_addedLemma(false), d_addedFact(false), d_collectTermsCache(c), + d_collectTermsCacheU(u), d_functionTerms(c), d_singleton_eq(u), d_lemmas_produced_c(u) @@ -459,8 +460,9 @@ bool TheoryDatatypes::doSendLemma( Node lem ) { } bool TheoryDatatypes::doSendLemmas( std::vector< Node >& lemmas ){ bool ret = false; - for( unsigned i=0; ilemma( NodeManager::currentNM()->mkNode( LEQ, d_zero, n ) ); - } // Function applications/predicates d_equalityEngine.addTerm(n); if( d_sygus_sym_break ){ @@ -1664,74 +1663,79 @@ Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) { } void TheoryDatatypes::collectTerms( Node n ) { - if( d_collectTermsCache.find( n )==d_collectTermsCache.end() ){ - d_collectTermsCache[n] = true; - //for( int i=0; i<(int)n.getNumChildren(); i++ ) { - // collectTerms( n[i] ); - //} - if( n.getKind() == APPLY_CONSTRUCTOR ){ - Debug("datatypes") << " Found constructor " << n << endl; - if( n.getNumChildren()>0 ){ - d_functionTerms.push_back( n ); - } - }else{ + if (d_collectTermsCache.find(n) != d_collectTermsCache.end()) + { + // already processed + return; + } + d_collectTermsCache[n] = true; + Kind nk = n.getKind(); + if (nk == APPLY_CONSTRUCTOR) + { + Debug("datatypes") << " Found constructor " << n << endl; + if (n.getNumChildren() > 0) + { + d_functionTerms.push_back(n); + } + return; + } + if (nk == APPLY_SELECTOR_TOTAL || nk == DT_SIZE || nk == DT_HEIGHT_BOUND) + { + d_functionTerms.push_back(n); + // we must also record which selectors exist + Trace("dt-collapse-sel") << " Found selector " << n << endl; + Node rep = getRepresentative(n[0]); + // record it in the selectors + EqcInfo* eqc = getOrMakeEqcInfo(rep, true); + // add it to the eqc info + addSelector(n, eqc, rep); + } + + // now, do user-context-dependent lemmas + if (nk != DT_SIZE && nk != DT_HEIGHT_BOUND) + { + // if not one of these kinds, there are no lemmas + return; + } + if (d_collectTermsCacheU.find(n) != d_collectTermsCacheU.end()) + { + return; + } + d_collectTermsCacheU[n] = true; - if( n.getKind() == APPLY_SELECTOR_TOTAL || n.getKind() == DT_SIZE || n.getKind() == DT_HEIGHT_BOUND ){ - d_functionTerms.push_back( n ); - //we must also record which selectors exist - Trace("dt-collapse-sel") << " Found selector " << n << endl; - Node rep = getRepresentative( n[0] ); - //record it in the selectors - EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); - //add it to the eqc info - addSelector( n, eqc, rep ); - - if( n.getKind() == DT_SIZE ){ - /* - //add size = 0 lemma - Node nn = n.eqNode( NodeManager::currentNM()->mkConst( Rational(0) ) ); - std::vector< Node > children; - children.push_back( nn.negate() ); - const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype(); - for( unsigned i=0; imkNode( OR, children ); - Trace("datatypes-infer") << "DtInfer : zero size : " << conc << std::endl; - d_pending.push_back( conc ); - d_pending_exp[ conc ] = d_true; - d_infer.push_back( conc ); - */ - } + NodeManager* nm = NodeManager::currentNM(); - if( n.getKind() == DT_HEIGHT_BOUND ){ - if( n[1].getConst().isZero() ){ - std::vector< Node > children; - const Datatype& dt = ((DatatypeType)(n[0].getType()).toType()).getDatatype(); - for( unsigned i=0; imkNode( EQUAL, n, children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ) ); - } - Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl; - //d_pending.push_back( lem ); - //d_pending_exp[ lem ] = d_true; - //d_infer.push_back( lem ); - d_pending_lem.push_back( lem ); - } - } + if (nk == DT_SIZE) + { + Node lem = nm->mkNode(LEQ, d_zero, n); + Trace("datatypes-infer") + << "DtInfer : size geq zero : " << lem << std::endl; + d_pending_lem.push_back(lem); + } + else if (nk == DT_HEIGHT_BOUND && n[1].getConst().isZero()) + { + std::vector children; + const Datatype& dt = n[0].getType().getDatatype(); + for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) + { + if (DatatypesRewriter::isNullaryConstructor(dt[i])) + { + Node test = DatatypesRewriter::mkTester(n[0], i, dt); + children.push_back(test); } } + Node lem; + if (children.empty()) + { + lem = n.negate(); + } + else + { + lem = n.eqNode(children.size() == 1 ? children[0] + : nm->mkNode(OR, children)); + } + Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl; + d_pending_lem.push_back(lem); } } diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index b4803e69a..e14a78df2 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -205,8 +205,16 @@ private: bool d_addedFact; /** The conflict node */ Node d_conflictNode; - /** cache for which terms we have called collectTerms(...) on */ + /** + * SAT-context dependent cache for which terms we have called + * collectTerms(...) on. + */ BoolMap d_collectTermsCache; + /** + * User-context dependent cache for which terms we have called + * collectTerms(...) on. + */ + BoolMap d_collectTermsCacheU; /** pending assertions/merges */ std::vector< Node > d_pending_lem; std::vector< Node > d_pending; -- 2.30.2