From 20c1eb502d1b9f2b19419ec925e306744d9e53bf Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 17 Jul 2018 16:17:43 +0200 Subject: [PATCH] sygusComp2018: Improvements to datatypes sygus solver (#2177) --- src/theory/datatypes/datatypes_sygus.cpp | 157 ++++++++++-------- src/theory/datatypes/datatypes_sygus.h | 17 +- .../quantifiers/sygus/sygus_explain.cpp | 13 +- src/theory/quantifiers/sygus/sygus_explain.h | 7 + 4 files changed, 113 insertions(+), 81 deletions(-) diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 5e0bb420e..c9b3a17f4 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -44,6 +44,7 @@ SygusSymBreakNew::SygusSymBreakNew(TheoryDatatypes* td, d_active_terms(c), d_currTermSize(c) { d_zero = NodeManager::currentNM()->mkConst(Rational(0)); + d_true = NodeManager::currentNM()->mkConst(true); } SygusSymBreakNew::~SygusSymBreakNew() { @@ -160,7 +161,7 @@ Node SygusSymBreakNew::getTermOrderPredicate( Node n1, Node n2 ) { return nm->mkNode(kind::OR, comm_disj); } - + void SygusSymBreakNew::registerTerm( Node n, std::vector< Node >& lemmas ) { if( d_is_top_level.find( n )==d_is_top_level.end() ){ d_is_top_level[n] = false; @@ -293,6 +294,7 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std: Trace("sygus-sb-debug") << "Get simple symmetry breaking predicates...\n"; unsigned max_depth = ssz>=d ? ssz-d : 0; unsigned min_depth = d_simple_proc[exp]; + NodeManager* nm = NodeManager::currentNM(); if( min_depth<=max_depth ){ TNode x = getFreeVar( ntn ); std::vector sb_lemmas; @@ -324,15 +326,16 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std: } // add the above symmetry breaking predicates to lemmas + std::unordered_map cache; Node rlv = getRelevancyCondition(n); - for (unsigned i = 0; i < sb_lemmas.size(); i++) + for (const Node& slem : sb_lemmas) { - Node pred = sb_lemmas[i].substitute(x, n); + Node sslem = slem.substitute(x, n, cache); if (!rlv.isNull()) { - pred = NodeManager::currentNM()->mkNode(kind::OR, rlv.negate(), pred); + sslem = nm->mkNode(OR, rlv, sslem); } - lemmas.push_back(pred); + lemmas.push_back(sslem); } } d_simple_proc[exp] = max_depth + 1; @@ -371,7 +374,7 @@ Node SygusSymBreakNew::getRelevancyCondition( Node n ) { int sindexi = dt[i].getSelectorIndexInternal(selExpr); if (sindexi != -1) { - disj.push_back(DatatypesRewriter::mkTester(n[0], i, dt)); + disj.push_back(DatatypesRewriter::mkTester(n[0], i, dt).negate()); } else { @@ -380,18 +383,20 @@ Node SygusSymBreakNew::getRelevancyCondition( Node n ) { } Assert( !disj.empty() ); if( excl ){ - cond = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ); + cond = disj.size() == 1 + ? disj[0] + : NodeManager::currentNM()->mkNode(kind::AND, disj); } }else{ int sindex = Datatype::cindexOf( selExpr ); Assert( sindex!=-1 ); - cond = DatatypesRewriter::mkTester( n[0], sindex, dt ); + cond = DatatypesRewriter::mkTester(n[0], sindex, dt).negate(); } Node c1 = getRelevancyCondition( n[0] ); if( cond.isNull() ){ cond = c1; }else if( !c1.isNull() ){ - cond = NodeManager::currentNM()->mkNode( kind::AND, cond, c1 ); + cond = NodeManager::currentNM()->mkNode(kind::OR, cond, c1); } } Trace("sygus-sb-debug2") << "Relevancy condition for " << n << " is " << cond << std::endl; @@ -567,24 +572,9 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn, if (tnc == children[c2].getType() && !tnc.getCardinality().isOne()) { Node sym_lem_deq = children[c1].eqNode(children[c2]).negate(); - // must guard if there are symbolic constructors - // the issue is that ite( C, _any_constant, _any_constant ) is - // a useful solution, since the two instances of _any_constant - // can be repaired to different values. Hence, below, we say - // e.g. d.i is a symbolic constructor, or it must be different - // from d.j. - int anyc_cons_num_c = d_tds->getAnyConstantConsNum(tnc); - if (anyc_cons_num_c != -1) - { - const Datatype& cdt = - static_cast(tnc.toType()).getDatatype(); - Node fv = d_tds->getFreeVar(tnc, 0); - Node guard_val = datatypes::DatatypesRewriter::getInstCons( - fv, cdt, anyc_cons_num_c); - Node exp = d_tds->getExplain()->getExplanationForEquality( - children[c1], guard_val); - sym_lem_deq = nm->mkNode(OR, exp, sym_lem_deq); - } + // notice that this symmetry breaking still allows for + // ite( C, any_constant(x), any_constant(y) ) + // since any_constant takes a builtin argument. sbp_conj.push_back(sym_lem_deq); } } @@ -800,15 +790,21 @@ Node SygusSymBreakNew::registerSearchValue( } } Trace("sygus-sb-debug2") << "Registering search value " << n << " -> " << nv << std::endl; + std::map var_count; + Node cnv = d_tds->canonizeBuiltin(nv, var_count); + Trace("sygus-sb-debug") << " ...canonized value is " << cnv << std::endl; // must do this for all nodes, regardless of top-level - if( d_cache[a].d_search_val_proc.find( nv )==d_cache[a].d_search_val_proc.end() ){ - d_cache[a].d_search_val_proc.insert(nv); + if (d_cache[a].d_search_val_proc.find(cnv) + == d_cache[a].d_search_val_proc.end()) + { + d_cache[a].d_search_val_proc.insert(cnv); // get the root (for PBE symmetry breaking) Assert(d_anchor_to_conj.find(a) != d_anchor_to_conj.end()); quantifiers::CegConjecture* aconj = d_anchor_to_conj[a]; Assert(aconj != NULL); - Trace("sygus-sb-debug") << " ...register search value " << nv << ", type=" << tn << std::endl; - Node bv = d_tds->sygusToBuiltin( nv, tn ); + Trace("sygus-sb-debug") + << " ...register search value " << cnv << ", type=" << tn << std::endl; + Node bv = d_tds->sygusToBuiltin(cnv, tn); Trace("sygus-sb-debug") << " ......builtin is " << bv << std::endl; Node bvr = d_tds->getExtRewriter()->extendedRewrite(bv); Trace("sygus-sb-debug") << " ......rewrites to " << bvr << std::endl; @@ -816,8 +812,10 @@ Node SygusSymBreakNew::registerSearchValue( unsigned sz = d_tds->getSygusTermSize( nv ); if( d_tds->involvesDivByZero( bvr ) ){ quantifiers::DivByZeroSygusInvarianceTest dbzet; - Trace("sygus-sb-mexp-debug") << "Minimize explanation for div-by-zero in " << d_tds->sygusToBuiltin( nv ) << std::endl; - registerSymBreakLemmaForValue(a, nv, dbzet, Node::null(), lemmas); + Trace("sygus-sb-mexp-debug") + << "Minimize explanation for div-by-zero in " << bv << std::endl; + registerSymBreakLemmaForValue( + a, nv, dbzet, Node::null(), var_count, lemmas); return Node::null(); }else{ std::unordered_map::iterator itsv = @@ -945,14 +943,16 @@ Node SygusSymBreakNew::registerSearchValue( } Assert( d_tds->getSygusTermSize( bad_val )==sz ); - Node x = getFreeVar( tn ); - - // do analysis of the evaluation FIXME: does not work (evaluation is non-constant) + // generalize the explanation for why the analog of bad_val + // is equivalent to bvr quantifiers::EquivSygusInvarianceTest eset; eset.init(d_tds, tn, aconj, a, bvr); Trace("sygus-sb-mexp-debug") << "Minimize explanation for eval[" << d_tds->sygusToBuiltin( bad_val ) << "] = " << bvr << std::endl; - registerSymBreakLemmaForValue(a, bad_val, eset, bad_val_o, lemmas); + registerSymBreakLemmaForValue( + a, bad_val, eset, bad_val_o, var_count, lemmas); + + // other generalization criteria go here return Node::null(); } } @@ -965,13 +965,14 @@ void SygusSymBreakNew::registerSymBreakLemmaForValue( Node val, quantifiers::SygusInvarianceTest& et, Node valr, + std::map& var_count, std::vector& lemmas) { TypeNode tn = val.getType(); Node x = getFreeVar(tn); unsigned sz = d_tds->getSygusTermSize(val); std::vector exp; - d_tds->getExplain()->getExplanationFor(x, val, exp, et, valr, sz); + d_tds->getExplain()->getExplanationFor(x, val, exp, et, valr, var_count, sz); Node lem = exp.size() == 1 ? exp[0] : NodeManager::currentNM()->mkNode(AND, exp); lem = lem.negate(); @@ -992,13 +993,22 @@ void SygusSymBreakNew::registerSymBreakLemma( TypeNode tn, Node lem, unsigned sz TNode x = getFreeVar( tn ); unsigned csz = getSearchSizeForAnchor( a ); int max_depth = ((int)csz)-((int)sz); + NodeManager* nm = NodeManager::currentNM(); for( int d=0; d<=max_depth; d++ ){ std::map< unsigned, std::vector< Node > >::iterator itt = d_cache[a].d_search_terms[tn].find( d ); if( itt!=d_cache[a].d_search_terms[tn].end() ){ - for( unsigned k=0; ksecond.size(); k++ ){ - TNode t = itt->second[k]; - if( !options::sygusSymBreakLazy() || d_active_terms.find( t )!=d_active_terms.end() ){ - addSymBreakLemma(lem, x, t, lemmas); + for (const TNode& t : itt->second) + { + if (!options::sygusSymBreakLazy() + || d_active_terms.find(t) != d_active_terms.end()) + { + Node slem = lem.substitute(x, t); + Node rlv = getRelevancyCondition(t); + if (!rlv.isNull()) + { + slem = nm->mkNode(OR, rlv, slem); + } + lemmas.push_back(slem); } } } @@ -1016,6 +1026,8 @@ void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, No Trace("sygus-sb-debug2") << "add sym break lemmas for " << t << " " << d << " " << a << std::endl; std::map< TypeNode, std::map< unsigned, std::vector< Node > > >::iterator its = d_cache[a].d_sb_lemmas.find( tn ); + Node rlv = getRelevancyCondition(t); + NodeManager* nm = NodeManager::currentNM(); if( its != d_cache[a].d_sb_lemmas.end() ){ TNode x = getFreeVar( tn ); //get symmetry breaking lemmas for this term @@ -1024,11 +1036,18 @@ void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, No Trace("sygus-sb-debug2") << "add lemmas up to size " << max_sz << ", which is (search_size) " << csz << " - (depth) " << d << std::endl; + std::unordered_map cache; for( std::map< unsigned, std::vector< Node > >::iterator it = its->second.begin(); it != its->second.end(); ++it ){ if( (int)it->first<=max_sz ){ - for( unsigned k=0; ksecond.size(); k++ ){ - Node lem = it->second[k]; - addSymBreakLemma(lem, x, t, lemmas); + for (const Node& lem : it->second) + { + Node slem = lem.substitute(x, t, cache); + // add the relevancy condition for t + if (!rlv.isNull()) + { + slem = nm->mkNode(OR, rlv, slem); + } + lemmas.push_back(slem); } } } @@ -1036,22 +1055,7 @@ void SygusSymBreakNew::addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, No Trace("sygus-sb-debug2") << "...finished." << std::endl; } -void SygusSymBreakNew::addSymBreakLemma(Node lem, - TNode x, - TNode n, - std::vector& lemmas) -{ - Assert( !options::sygusSymBreakLazy() || d_active_terms.find( n )!=d_active_terms.end() ); - // apply lemma - Node slem = lem.substitute( x, n ); - Trace("sygus-sb-exc-debug") << "SymBreak lemma : " << slem << std::endl; - Node rlv = getRelevancyCondition( n ); - if( !rlv.isNull() ){ - slem = NodeManager::currentNM()->mkNode( kind::OR, rlv.negate(), slem ); - } - lemmas.push_back( slem ); -} - + void SygusSymBreakNew::preRegisterTerm( TNode n, std::vector< Node >& lemmas ) { if( n.isVar() ){ Trace("sygus-sb-debug") << "Pre-register variable : " << n << std::endl; @@ -1181,6 +1185,7 @@ void SygusSymBreakNew::incrementCurrentSearchSize( Node m, std::vector< Node >& Assert( itsz!=d_szinfo.end() ); itsz->second->d_curr_search_size++; Trace("sygus-fair") << " register search size " << itsz->second->d_curr_search_size << " for " << m << std::endl; + NodeManager* nm = NodeManager::currentNM(); for( std::map< Node, SearchCache >::iterator itc = d_cache.begin(); itc != d_cache.end(); ++itc ){ Node a = itc->first; Trace("sygus-fair-debug") << " look at anchor " << a << "..." << std::endl; @@ -1196,12 +1201,19 @@ void SygusSymBreakNew::incrementCurrentSearchSize( Node m, std::vector< Node >& int new_depth = ((int)itsz->second->d_curr_search_size) - ((int)sz); std::map< unsigned, std::vector< Node > >::iterator itt = itc->second.d_search_terms[tn].find( new_depth ); if( itt!=itc->second.d_search_terms[tn].end() ){ - for( unsigned k=0; ksecond.size(); k++ ){ - TNode t = itt->second[k]; - if( !options::sygusSymBreakLazy() || d_active_terms.find( t )!=d_active_terms.end() ){ - for( unsigned j=0; jsecond.size(); j++ ){ - Node lem = it->second[j]; - addSymBreakLemma(lem, x, t, lemmas); + for (const TNode& t : itt->second) + { + if (!options::sygusSymBreakLazy() + || d_active_terms.find(t) != d_active_terms.end() + && !it->second.empty()) + { + Node rlv = getRelevancyCondition(t); + std::unordered_map cache; + for (const Node& lem : it->second) + { + Node slem = lem.substitute(x, t, cache); + slem = nm->mkNode(OR, rlv, slem); + lemmas.push_back(slem); } } } @@ -1343,9 +1355,14 @@ bool SygusSymBreakNew::checkTesters(Node n, const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); int cindex = DatatypesRewriter::indexOf(vn.getOperator()); Node tst = DatatypesRewriter::mkTester( n, cindex, dt ); - bool hastst = d_td->getValuation().getModel()->hasTerm( tst ); - Node tstrep = d_td->getValuation().getModel()->getRepresentative( tst ); - if( !hastst || tstrep!=NodeManager::currentNM()->mkConst( true ) ){ + bool hastst = d_td->getEqualityEngine()->hasTerm(tst); + Node tstrep; + if (hastst) + { + tstrep = d_td->getEqualityEngine()->getRepresentative(tst); + } + if (!hastst || tstrep != d_true) + { Trace("sygus-sb-warn") << "- has tester : " << tst << " : " << ( hastst ? "true" : "false" ); Trace("sygus-sb-warn") << ", value=" << tstrep << std::endl; if( !hastst ){ diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index 752c94426..5f6ca935d 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -145,6 +145,8 @@ class SygusSymBreakNew IntMap d_currTermSize; /** zero */ Node d_zero; + /** true */ + Node d_true; /** * Map from terms (selector chains) to their anchors. The anchor of a * selector chain S1( ... Sn( x ) ... ) is x. @@ -337,6 +339,7 @@ private: Node val, quantifiers::SygusInvarianceTest& et, Node valr, + std::map& var_count, std::vector& lemmas); /** Add symmetry breaking lemmas for term * @@ -358,20 +361,14 @@ private: TypeNode tn, Node t, unsigned d, Node a, std::vector& lemmas); /** calls the above function where a is the anchor t */ void addSymBreakLemmasFor( TypeNode tn, Node t, unsigned d, std::vector< Node >& lemmas ); - /** add symmetry breaking lemma - * - * This adds the lemma R => lem{ x -> n } to lemmas, where R is a "relevancy - * condition" that states which contexts n is relevant in (see - * getRelevancyCondition). - */ - void addSymBreakLemma(Node lem, TNode x, TNode n, std::vector& lemmas); //------------------------end dynamic symmetry breaking /** Get relevancy condition * - * This returns a predicate that holds in the contexts in which the selector - * chain n is specified. For example, the relevancy condition for - * sel_{C2,1}( sel_{C1,1}( d ) ) is is-C1( d ) ^ is-C2( sel_{C1,1}( d ) ). + * This returns (the negation of) a predicate that holds in the contexts in + * which the selector chain n is specified. For example, the negation of the + * relevancy condition for sel_{C2,1}( sel_{C1,1}( d ) ) is + * ~( is-C1( d ) ^ is-C2( sel_{C1,1}( d ) ) ) * If shared selectors are enabled, this is a conjunction of disjunctions, * since shared selectors may apply to multiple constructors. */ diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index 665390271..ddf52001e 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -283,12 +283,23 @@ void SygusExplain::getExplanationFor(Node n, SygusInvarianceTest& et, Node vnr, unsigned& sz) +{ + std::map var_count; + return getExplanationFor(n, vn, exp, et, vnr, var_count, sz); +} + +void SygusExplain::getExplanationFor(Node n, + Node vn, + std::vector& exp, + SygusInvarianceTest& et, + Node vnr, + std::map& var_count, + unsigned& sz) { // naive : // return getExplanationForEquality( n, vn, exp ); // set up the recursion object; - std::map var_count; TermRecBuild trb; trb.init(vn); Node vnr_exp; diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h index 7455c3287..4efc171d3 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.h +++ b/src/theory/quantifiers/sygus/sygus_explain.h @@ -198,6 +198,13 @@ class SygusExplain SygusInvarianceTest& et, Node vnr, unsigned& sz); + void getExplanationFor(Node n, + Node vn, + std::vector& exp, + SygusInvarianceTest& et, + Node vnr, + std::map& var_count, + unsigned& sz); void getExplanationFor(Node n, Node vn, std::vector& exp, -- 2.30.2