From: Andrew Reynolds Date: Fri, 4 May 2018 00:54:28 +0000 (-0500) Subject: Document datatypes sygus (#1818) X-Git-Tag: cvc5-1.0.0~5092 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=09f164674497e70044cc7759b00c6477db90b7be;p=cvc5.git Document datatypes sygus (#1818) --- diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 4d3584596..6f660642e 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -40,7 +40,6 @@ SygusSymBreakNew::SygusSymBreakNew(TheoryDatatypes* td, : d_td(td), d_tds(tds), d_testers(c), - d_is_const(c), d_testers_exp(c), d_active_terms(c), d_currTermSize(c) { @@ -100,21 +99,15 @@ void SygusSymBreakNew::assertTester( int tindex, TNode n, Node exp, std::vector< } void SygusSymBreakNew::assertFact( Node n, bool polarity, std::vector< Node >& lemmas ) { - if( n.getKind()==kind::DT_SYGUS_TERM_ORDER ){ - if( polarity ){ - Trace("sygus-sb-torder") << "Sygus term order : " << n[0] << " < " << n[1] << std::endl; - Node comm_sb = getTermOrderPredicate( n[0], n[1] ); - Node comm_lem = NodeManager::currentNM()->mkNode( kind::OR, n.negate(), comm_sb ); - lemmas.push_back( comm_lem ); - } - }else if( n.getKind()==kind::DT_SYGUS_BOUND ){ + if (n.getKind() == kind::DT_SYGUS_BOUND) + { Node m = n[0]; Trace("sygus-fair") << "Have sygus bound : " << n << ", polarity=" << polarity << " on measure " << m << std::endl; registerMeasureTerm( m ); if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){ std::map< Node, SearchSizeInfo * >::iterator its = d_szinfo.find( m ); Assert( its!=d_szinfo.end() ); - Node mt = its->second->getOrMkSygusMeasureTerm( lemmas ); + Node mt = its->second->getOrMkMeasureValue(lemmas); //it relates the measure term to arithmetic Node blem = n.eqNode( NodeManager::currentNM()->mkNode( kind::LEQ, mt, n[1] ) ); lemmas.push_back( blem ); @@ -123,57 +116,12 @@ void SygusSymBreakNew::assertFact( Node n, bool polarity, std::vector< Node >& l unsigned s = n[1].getConst().getNumerator().toUnsignedInt(); notifySearchSize( m, s, n, lemmas ); } - }else if( n.getKind() == kind::DT_SYGUS_IS_CONST ){ - assertIsConst( n[0], polarity, lemmas ); }else if( n.getKind() == kind::DT_HEIGHT_BOUND || n.getKind()==DT_SIZE_BOUND ){ //reduce to arithmetic TODO ? } } -void SygusSymBreakNew::assertIsConst( Node n, bool polarity, std::vector< Node >& lemmas ) { - if( d_active_terms.find( n )!=d_active_terms.end() ) { - // what kind of constructor is n? - IntMap::const_iterator itt = d_testers.find( n ); - Assert( itt!=d_testers.end() ); - int tindex = (*itt).second; - TypeNode tn = n.getType(); - const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); - Node lem; - if( dt[tindex].getNumArgs()==0 ){ - // is this a constant? - Node sygus_op = Node::fromExpr( dt[tindex].getSygusOp() ); - if( sygus_op.isConst()!=polarity ){ - lem = NodeManager::currentNM()->mkNode( kind::DT_SYGUS_IS_CONST, n ); - if( polarity ){ - lem.negate(); - } - } - }else{ - // reduce - std::vector< Node > child_conj; - for( unsigned j=0; jmkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( tn.toType(), j ) ), n ); - child_conj.push_back( NodeManager::currentNM()->mkNode( kind::DT_SYGUS_IS_CONST, sel ) ); - } - lem = child_conj.size()==1 ? child_conj[0] : NodeManager::currentNM()->mkNode( kind::AND, child_conj ); - // only an implication (TODO : strengthen?) - lem = NodeManager::currentNM()->mkNode( kind::OR, lem.negate(), NodeManager::currentNM()->mkNode( kind::DT_SYGUS_IS_CONST, n ) ); - } - if( !lem.isNull() ){ - Trace("sygus-isc") << "Sygus is-const lemma : " << lem << std::endl; - Node rlv = getRelevancyCondition( n ); - if( !rlv.isNull() ){ - lem = NodeManager::currentNM()->mkNode( kind::OR, rlv.negate(), lem ); - } - lemmas.push_back( lem ); - } - }else{ - // lazy - d_is_const[n] = polarity ? 1 : -1; - } -} - Node SygusSymBreakNew::getTermOrderPredicate( Node n1, Node n2 ) { NodeManager* nm = NodeManager::currentNM(); std::vector< Node > comm_disj; @@ -269,13 +217,6 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std: d_active_terms.insert( n ); Trace("sygus-sb-debug2") << "Sygus : activate term : " << n << " : " << exp << std::endl; - /* TODO - IntMap::const_iterator itisc = d_is_const.find( n ); - if( itisc != d_is_const.end() ){ - assertIsConst( n, (*itisc).second==1, lemmas ); - } - */ - TypeNode ntn = n.getType(); const Datatype& dt = ((DatatypeType)ntn.toType()).getDatatype(); @@ -502,21 +443,8 @@ Node SygusSymBreakNew::getSimpleSymBreakPred( TypeNode tn, int tindex, unsigned if( quantifiers::TermUtil::isComm( nk ) ){ if( children.size()==2 ){ if( children[0].getType()==children[1].getType() ){ - #if 0 - Node order_pred = NodeManager::currentNM()->mkNode( DT_SYGUS_TERM_ORDER, children[0], children[1] ); - sbp_conj.push_back( order_pred ); - Node child11 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[tindex].getSelectorInternal( tn.toType(), 1 ) ), children[0] ); - Assert( child11.getType()==children[1].getType() ); - //chainable - if( children[0].getType()==tn ){ - Node order_pred_trans = NodeManager::currentNM()->mkNode( OR, DatatypesRewriter::mkTester( children[0], tindex, dt ).negate(), - NodeManager::currentNM()->mkNode( DT_SYGUS_TERM_ORDER, child11, children[1] ) ); - sbp_conj.push_back( order_pred_trans ); - } - #else Node order_pred = getTermOrderPredicate( children[0], children[1] ); sbp_conj.push_back( order_pred ); - #endif } } } @@ -672,23 +600,6 @@ TNode SygusSymBreakNew::getFreeVar( TypeNode tn ) { return d_tds->getFreeVar(tn, 0); } -unsigned SygusSymBreakNew::processSelectorChain( Node n, std::map< TypeNode, Node >& top_level, std::map< Node, unsigned >& tdepth, std::vector< Node >& lemmas ) { - unsigned ret = 0; - if( n.getKind()==APPLY_SELECTOR_TOTAL ){ - ret = processSelectorChain( n[0], top_level, tdepth, lemmas ); - } - TypeNode tn = n.getType(); - if( top_level.find( tn )==top_level.end() ){ - top_level[tn] = n; - //tdepth[n] = ret; - registerSearchTerm( tn, ret, n, true, lemmas ); - }else{ - registerSearchTerm( tn, ret, n, false, lemmas ); - } - tdepth[n] = ret; - return ret+1; -} - void SygusSymBreakNew::registerSearchTerm( TypeNode tn, unsigned d, Node n, bool topLevel, std::vector< Node >& lemmas ) { //register this term std::unordered_map::iterator ita = @@ -1001,21 +912,17 @@ void SygusSymBreakNew::registerSizeTerm( Node e, std::vector< Node >& lemmas ) { if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){ // update constraints on the measure term if( options::sygusFairMax() ){ - if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){ - Node ds = NodeManager::currentNM()->mkNode( kind::DT_SIZE, e ); - Node slem = NodeManager::currentNM()->mkNode( kind::LEQ, ds, d_szinfo[m]->getOrMkSygusMeasureTerm( lemmas ) ); - lemmas.push_back( slem ); - } + Node ds = NodeManager::currentNM()->mkNode(kind::DT_SIZE, e); + Node slem = NodeManager::currentNM()->mkNode( + kind::LEQ, ds, d_szinfo[m]->getOrMkMeasureValue(lemmas)); + lemmas.push_back(slem); }else{ - Node mt = d_szinfo[m]->getOrMkSygusActiveMeasureTerm( lemmas ); - Node new_mt = NodeManager::currentNM()->mkSkolem( "mt", NodeManager::currentNM()->integerType() ); - lemmas.push_back( NodeManager::currentNM()->mkNode( kind::GEQ, new_mt, d_zero ) ); - if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){ - Node ds = NodeManager::currentNM()->mkNode( kind::DT_SIZE, e ); - lemmas.push_back( mt.eqNode( NodeManager::currentNM()->mkNode( kind::PLUS, new_mt, ds ) ) ); - //lemmas.push_back( NodeManager::currentNM()->mkNode( kind::GEQ, ds, d_zero ) ); - } - d_szinfo[m]->d_sygus_measure_term_active = new_mt; + Node mt = d_szinfo[m]->getOrMkActiveMeasureValue(lemmas); + Node new_mt = + d_szinfo[m]->getOrMkActiveMeasureValue(lemmas, true); + Node ds = NodeManager::currentNM()->mkNode(kind::DT_SIZE, e); + lemmas.push_back(mt.eqNode( + NodeManager::currentNM()->mkNode(kind::PLUS, new_mt, ds))); } } }else{ @@ -1166,7 +1073,8 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { Trace("dt-sygus") << ss.str() << std::endl; } // TODO : remove this step (ensure there is no way a sygus term cannot be assigned a tester before this point) - if( !debugTesters( prog, progv, 0, lemmas ) ){ + if (!checkTesters(prog, progv, 0, lemmas)) + { Trace("sygus-sb") << " SygusSymBreakNew::check: ...WARNING: considered missing split for " << prog << "." << std::endl; // this should not happen generally, it is caused by a sygus term not being assigned a tester //Assert( false ); @@ -1221,7 +1129,11 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { } } -bool SygusSymBreakNew::debugTesters( Node n, Node vn, int ind, std::vector< Node >& lemmas ) { +bool SygusSymBreakNew::checkTesters(Node n, + Node vn, + int ind, + std::vector& lemmas) +{ Assert( vn.getKind()==kind::APPLY_CONSTRUCTOR ); if( Trace.isOn("sygus-sb-warn") ){ Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, n ); @@ -1249,7 +1161,8 @@ bool SygusSymBreakNew::debugTesters( Node n, Node vn, int ind, std::vector< Node } for( unsigned i=0; imkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex].getSelectorInternal( tn.toType(), i ) ), n ); - if( !debugTesters( sel, vn[i], ind+1, lemmas ) ){ + if (!checkTesters(sel, vn[i], ind + 1, lemmas)) + { return false; } } @@ -1278,19 +1191,37 @@ Node SygusSymBreakNew::getCurrentTemplate( Node n, std::map< TypeNode, int >& va } } -Node SygusSymBreakNew::SearchSizeInfo::getOrMkSygusMeasureTerm( std::vector< Node >& lemmas ) { - if( d_sygus_measure_term.isNull() ){ - d_sygus_measure_term = NodeManager::currentNM()->mkSkolem( "mt", NodeManager::currentNM()->integerType() ); - lemmas.push_back( NodeManager::currentNM()->mkNode( kind::GEQ, d_sygus_measure_term, NodeManager::currentNM()->mkConst( Rational(0) ) ) ); +Node SygusSymBreakNew::SearchSizeInfo::getOrMkMeasureValue( + std::vector& lemmas) +{ + if (d_measure_value.isNull()) + { + d_measure_value = NodeManager::currentNM()->mkSkolem( + "mt", NodeManager::currentNM()->integerType()); + lemmas.push_back(NodeManager::currentNM()->mkNode( + kind::GEQ, + d_measure_value, + NodeManager::currentNM()->mkConst(Rational(0)))); } - return d_sygus_measure_term; + return d_measure_value; } -Node SygusSymBreakNew::SearchSizeInfo::getOrMkSygusActiveMeasureTerm( std::vector< Node >& lemmas ) { - if( d_sygus_measure_term_active.isNull() ){ - d_sygus_measure_term_active = getOrMkSygusMeasureTerm( lemmas ); +Node SygusSymBreakNew::SearchSizeInfo::getOrMkActiveMeasureValue( + std::vector& lemmas, bool mkNew) +{ + if (mkNew) + { + Node new_mt = NodeManager::currentNM()->mkSkolem( + "mt", NodeManager::currentNM()->integerType()); + lemmas.push_back(NodeManager::currentNM()->mkNode( + kind::GEQ, new_mt, NodeManager::currentNM()->mkConst(Rational(0)))); + d_measure_value_active = new_mt; + } + else if (d_measure_value_active.isNull()) + { + d_measure_value_active = getOrMkMeasureValue(lemmas); } - return d_sygus_measure_term_active; + return d_measure_value_active; } Node SygusSymBreakNew::SearchSizeInfo::getFairnessLiteral( unsigned s, TheoryDatatypes * d, std::vector< Node >& lemmas ) { diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index 2936c1561..e0b29efd2 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -40,6 +40,17 @@ namespace datatypes { class TheoryDatatypes; +/** + * This is the sygus extension of the decision procedure for quantifier-free + * inductive datatypes. At a high level, this class takes as input a + * set of asserted testers is-C1( x ), is-C2( x.1 ), is-C3( x.2 ), and + * generates lemmas that restrict the models of x, if x is a "sygus enumerator" + * (see TermDbSygus::registerEnumerator). + * + * Some of these techniques are described in these papers: + * "Refutation-Based Synthesis in SMT", Reynolds et al 2017. + * "Sygus Techniques in the Core of an SMT Solver", Reynolds et al 2017. + */ class SygusSymBreakNew { typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap; @@ -52,11 +63,53 @@ class SygusSymBreakNew quantifiers::TermDbSygus* tds, context::Context* c); ~SygusSymBreakNew(); - /** add tester */ + /** + * Notify this class that tester for constructor tindex has been asserted for + * n. Exp is the literal corresponding to this tester. This method may add + * lemmas to the vector lemmas, for details see assertTesterInternal below. + * These lemmas are sent out on the output channel of datatypes by the caller. + */ void assertTester(int tindex, TNode n, Node exp, std::vector& lemmas); + /** + * Notify this class that literal n has been asserted with the given + * polarity. This method may add lemmas to the vector lemmas, for instance + * based on inferring consequences of (not) n. One example is if n is + * (DT_SIZE_BOUND x n), we add the lemma: + * (DT_SIZE_BOUND x n) <=> ((DT_SIZE x) <= n ) + */ void assertFact(Node n, bool polarity, std::vector& lemmas); + /** pre-register term n + * + * This is called when n is pre-registered with the theory of datatypes. + * If n is a sygus enumerator, then we may add lemmas to the vector lemmas + * that are used to enforce fairness regarding the size of n. + */ void preRegisterTerm(TNode n, std::vector& lemmas); + /** check + * + * This is called at last call effort, when the current model assignment is + * satisfiable according to the quantifier-free decision procedures and a + * model is built. This method may add lemmas to the vector lemmas based + * on dynamic symmetry breaking techniques, based on the model values of + * all preregistered enumerators. + */ void check(std::vector& lemmas); + /** get next decision request + * + * This function has the same interface as Theory::getNextDecisionRequest. + * + * The decisions returned by this method are of one of two forms: + * (1) Positive decisions on the active guards G of enumerators e registered + * to this class. These assert "there are more values to enumerate for e". + * (2) Positive bounds (DT_SYGUS_BOUND m n) for "measure terms" m (see below), + * where n is a non-negative integer. This asserts "the measure of terms + * we are enumerating for enumerators whose measure term m is at most n", + * where measure is commonly term size, but can also be height. + * + * We prioritize decisions of form (1) before (2). For both decisions, + * we set the priority argument to "1", indicating that the decision is + * critical for solution completeness. + */ Node getNextDecisionRequest(unsigned& priority, std::vector& lemmas); private: @@ -64,11 +117,33 @@ class SygusSymBreakNew TheoryDatatypes* d_td; /** Pointer to the sygus term database */ quantifiers::TermDbSygus* d_tds; + /** + * Map from terms to the index of the tester that is asserted for them in + * the current SAT context. In other words, if d_testers[n] = 2, then the + * tester is-C_2(n) is asserted in this SAT context. + */ IntMap d_testers; - IntMap d_is_const; + /** + * Map from terms to the tester asserted for them. In the example above, + * d_testers[n] = is-C_2(n). + */ NodeMap d_testers_exp; + /** + * The set of (selector chain) terms that are active in the current SAT + * context. A selector chain term S_n( ... S_1( x )... ) is active if either: + * (1) n=0 and x is a sygus enumerator, + * or: + * (2.1) S_{n-1}( ... S_1( x )) is active, + * (2.2) is-C( S_{n-1}( ... S_1( x )) ) is asserted in this SAT context, and + * (2.3) S_n is a selector for constructor C. + */ NodeSet d_active_terms; + /** + * Map from enumerators to a lower bound on their size in the current SAT + * context. + */ IntMap d_currTermSize; + /** zero */ Node d_zero; /** * Map from terms (selector chains) to their anchors. The anchor of a @@ -96,7 +171,6 @@ class SygusSymBreakNew * S4 : T1 -> T3 * Then, x, S1( x ), and S4( S3( S2( S1( x ) ) ) ) are top-level terms, * whereas S2( S1( x ) ) and S3( S2( S1( x ) ) ) are not. - * */ std::unordered_map d_is_top_level; /** @@ -330,59 +404,207 @@ private: /** Get the canonical free variable for type tn */ TNode getFreeVar( TypeNode tn ); + /** get term order predicate + * + * Assuming that n1 and n2 are children of a commutative operator, this + * returns a symmetry breaking predicate that can be instantiated for n1 and + * n2 while preserving satisfiability. By default, this is the predicate + * ( DT_SIZE n1 ) >= ( DT_SIZE n2 ) + */ Node getTermOrderPredicate( Node n1, Node n2 ); -private: - /** - * Map from registered variables to whether they are a sygus enumerator. - * - * This should be user context-dependent if sygus is updated to work in - * incremental mode. - */ - std::map d_register_st; - void registerSizeTerm(Node e, std::vector& lemmas); - class SearchSizeInfo - { - public: + + private: + /** + * Map from registered variables to whether they are a sygus enumerator. + * + * This should be user context-dependent if sygus is updated to work in + * incremental mode. + */ + std::map d_register_st; + //----------------------search size information + /** + * Checks whether e is a sygus enumerator, that is, a term for which this + * class will track size for. + * + * We associate each sygus enumerator e with a "measure term", which is used + * for bounding the size of terms for the models of e. The measure term for a + * sygus enumerator may be e itself (if e has an active guard), or an + * arbitrary sygus variable otherwise. A measure term m is one for which our + * decision strategy decides on literals of the form (DT_SYGUS_BOUND m n). + * + * After determining the measure term m for e, if applicable, we initialize + * SearchSizeInfo for m below. This may result in lemmas + */ + void registerSizeTerm(Node e, std::vector& lemmas); + /** information for each measure term allocated by this class */ + class SearchSizeInfo + { + public: SearchSizeInfo( Node t, context::Context* c ) : d_this( t ), d_curr_search_size(0), d_curr_lit( c, 0 ) {} + /** the measure term */ Node d_this; + /** + * For each size n, an explanation for why this measure term has size at + * most n. This is typically the literal (DT_SYGUS_BOUND m n), which + * we call the (n^th) "fairness literal" for m. + */ std::map< unsigned, Node > d_search_size_exp; + /** + * For each size, whether we have called SygusSymBreakNew::notifySearchSize. + */ std::map< unsigned, bool > d_search_size; + /** + * The current search size. This corresponds to the number of times + * incrementCurrentSearchSize has been called for this measure term. + */ unsigned d_curr_search_size; - Node d_sygus_measure_term; - Node d_sygus_measure_term_active; + /** the list of all enumerators whose measure term is this */ std::vector< Node > d_anchors; - Node getOrMkSygusMeasureTerm( std::vector< Node >& lemmas ); - Node getOrMkSygusActiveMeasureTerm( std::vector< Node >& lemmas ); - public: - /** current cardinality */ + /** get or make the measure value + * + * The measure value is an integer variable v that is a (symbolic) integer + * value that is constrained to be less than or equal to the current search + * size. For example, if we are using the fairness strategy + * SYGUS_FAIR_DT_SIZE (see options/datatype_options.h), then we constrain: + * (DT_SYGUS_BOUND m n) <=> (v <= n) + * for all asserted fairness literals. Then, if we are enforcing fairness + * based on the maximum size, we assert: + * (DT_SIZE e) <= v + * for all enumerators e. + */ + Node getOrMkMeasureValue(std::vector& lemmas); + /** get or make the active measure value + * + * The active measure value av is an integer variable that corresponds to + * the (symbolic) value of the sum of enumerators that are yet to be + * registered. This is to enforce the "sum of measures" strategy. For + * example, if we are using the fairness strategy SYGUS_FAIR_DT_SIZE, + * then initially av is equal to the measure value v, and the constraints + * (DT_SYGUS_BOUND m n) <=> (v <= n) + * are added as before. When an enumerator e is registered, we add the + * lemma: + * av = (DT_SIZE e) + av' + * and update the active measure value to av'. This ensures that the sum + * of sizes of active enumerators is at most n. + * + * If the flag mkNew is set to true, then we return a fresh variable and + * update the active measure value. + */ + Node getOrMkActiveMeasureValue(std::vector& lemmas, + bool mkNew = false); + /** + * The current search size literal for this measure term. This corresponds + * to the minimial n such that (DT_SYGUS_BOUND d_this n) is asserted in + * this SAT context. + */ context::CDO< unsigned > d_curr_lit; + /** + * Map from integers n to the fairness literal, for each n such that this + * literal has been allocated (by getFairnessLiteral below). + */ std::map< unsigned, Node > d_lits; + /** + * Returns the s^th fairness literal for this measure term. This adds a + * split on this literal to lemmas. + */ Node getFairnessLiteral( unsigned s, TheoryDatatypes * d, std::vector< Node >& lemmas ); + /** get the current fairness literal */ Node getCurrentFairnessLiteral( TheoryDatatypes * d, std::vector< Node >& lemmas ) { return getFairnessLiteral( d_curr_lit.get(), d, lemmas ); } /** increment current term size */ void incrementCurrentLiteral() { d_curr_lit.set( d_curr_lit.get() + 1 ); } + + private: + /** the measure value */ + Node d_measure_value; + /** the sygus measure value */ + Node d_measure_value_active; }; + /** the above information for each registered measure term */ std::map< Node, SearchSizeInfo * > d_szinfo; + /** map from enumerators (anchors) to their associated measure term */ std::map< Node, Node > d_anchor_to_measure_term; + /** map from enumerators (anchors) to their active guard*/ std::map< Node, Node > d_anchor_to_active_guard; + /** generic measure term + * + * This is a global term that is used as the measure term for all sygus + * enumerators that do not have active guards. This class enforces that + * all enumerators have size at most n, where n is the minimal integer + * such that (DT_SYGUS_BOUND d_generic_measure_term n) is asserted. + */ Node d_generic_measure_term; + /** + * This increments the current search size for measure term m. This may + * cause lemmas to be added to lemmas based on the fact that symmetry + * breaking lemmas are now relevant for new search terms, see discussion + * of how search size affects which lemmas are relevant above + * addSymBreakLemmasFor. + */ void incrementCurrentSearchSize( Node m, std::vector< Node >& lemmas ); + /** + * Notify this class that we are currently searching for terms of size at + * most s as model values for measure term m. Literal exp corresponds to the + * explanation of why the measure term has size at most n. This calls + * incrementSearchSize above, until the total number of times we have called + * incrementSearchSize so far is at least s. + */ void notifySearchSize( Node m, unsigned s, Node exp, std::vector< Node >& lemmas ); + /** Allocates a SearchSizeInfo object in d_szinfo. */ void registerMeasureTerm( Node m ); + /** + * Return the current search size for arbitrary term n. This is the current + * search size of the anchor of n. + */ unsigned getSearchSizeFor( Node n ); - unsigned getSearchSizeForAnchor( Node n ); + /** return the current search size for enumerator (anchor) e */ + unsigned getSearchSizeForAnchor(Node e); + /** Get the current search size for measure term m in this SAT context. */ unsigned getSearchSizeForMeasureTerm(Node m); - - private: - unsigned processSelectorChain( Node n, std::map< TypeNode, Node >& top_level, - std::map< Node, unsigned >& tdepth, std::vector< Node >& lemmas ); - bool debugTesters( Node n, Node vn, int ind, std::vector< Node >& lemmas ); + /** get current template + * + * For debugging. This returns a term that corresponds to the current + * inferred shape of n. For example, if the testers + * is-C1( n ) and is-C2( n.1 ) + * have been asserted where C1 and C2 are binary constructors, then this + * method may return a term of the form: + * C1( C2( x1, x2 ), x3 ) + * for fresh variables x1, x2, x3. The map var_count maintains the variable + * count for generating these fresh variables. + */ Node getCurrentTemplate( Node n, std::map< TypeNode, int >& var_count ); + //----------------------end search size information + /** check testers + * + * This is called when we have a model assignment vn for n, where n is + * a selector chain applied to an enumerator (a search term). This function + * ensures that testers have been asserted for each subterm of vn. This is + * critical for ensuring that the proper steps have been taken by this class + * regarding whether or not vn is a legal value for n (not greater than the + * current search size and not a value that can be blocked by symmetry + * breaking). + * + * For example, if vn = +( x(), x() ), then we ensure that the testers + * is-+( n ), is-x( n.1 ), is-x( n.2 ) + * have been asserted to this class. If a tester is not asserted for some + * relevant selector chain S( n ) of n, then we add a lemma L for that + * selector chain to lemmas, where L is the "splitting lemma" for S( n ), that + * states that the top symbol of S( n ) must be one of the constructors of + * its type. + * + * Notice that this function is a sanity check. Typically, it should be the + * case that testers are asserted for all subterms of vn, and hence this + * method should not ever add anything to lemmas. However, due to its + * importance, we check this regardless. + */ + bool checkTesters(Node n, Node vn, int ind, std::vector& lemmas); + /** + * Get the current SAT status of the guard g. + * In particular, this returns 1 if g is asserted true, -1 if it is asserted + * false, and 0 if it is not asserted. + */ int getGuardStatus( Node g ); -private: - void assertIsConst( Node n, bool polarity, std::vector< Node >& lemmas ); }; } diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 3ce416b40..65f258de1 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -114,10 +114,4 @@ typerule DT_SIZE_BOUND ::CVC4::theory::datatypes::DtBoundTypeRule operator DT_SYGUS_BOUND 2 "datatypes sygus bound" typerule DT_SYGUS_BOUND ::CVC4::theory::datatypes::DtSygusBoundTypeRule -operator DT_SYGUS_TERM_ORDER 2 "datatypes sygus term order" -typerule DT_SYGUS_TERM_ORDER ::CVC4::theory::datatypes::DtSygusPredTypeRule - -operator DT_SYGUS_IS_CONST 1 "datatypes sygus is constant" -typerule DT_SYGUS_IS_CONST ::CVC4::theory::datatypes::DtSygusPredTypeRule - endtheory diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index d6045404d..6ba64d8dd 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -359,28 +359,6 @@ class DtSygusBoundTypeRule { } }; /* class DtSygusBoundTypeRule */ - -class DtSygusPredTypeRule { - public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) { - if (check) { - TypeNode tn = n[0].getType(); - if (!tn.isDatatype() || !((DatatypeType)tn.toType()).getDatatype().isSygus()) { - throw TypeCheckingExceptionPrivate( - n, "datatype sygus predicate expecting terms of sygus type"); - } - for( unsigned i=0; ibooleanType(); - } -}; /* class DtSygusPredTypeRule */ - } /* CVC4::theory::datatypes namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */