From e7d418f9aafd33d5893ac83c925ff958965a48b9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 17 Sep 2018 16:26:00 -0500 Subject: [PATCH] Decision strategy: incorporate datatypes sygus solver. (#2479) --- src/theory/datatypes/datatypes_sygus.cpp | 125 +++++++++------------- src/theory/datatypes/datatypes_sygus.h | 74 +++++-------- src/theory/datatypes/kinds | 2 +- src/theory/datatypes/theory_datatypes.cpp | 11 -- src/theory/datatypes/theory_datatypes.h | 2 - 5 files changed, 81 insertions(+), 133 deletions(-) diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 18ccd483c..82aa570c2 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -50,9 +50,7 @@ SygusSymBreakNew::SygusSymBreakNew(TheoryDatatypes* td, } SygusSymBreakNew::~SygusSymBreakNew() { - for( std::map< Node, SearchSizeInfo * >::iterator it = d_szinfo.begin(); it != d_szinfo.end(); ++it ){ - delete it->second; - } + } /** add tester */ @@ -108,7 +106,8 @@ void SygusSymBreakNew::assertFact( Node n, bool polarity, std::vector< Node >& l 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 ); + std::map>::iterator its = + d_szinfo.find(m); Assert( its!=d_szinfo.end() ); Node mt = its->second->getOrMkMeasureValue(lemmas); //it relates the measure term to arithmetic @@ -238,7 +237,8 @@ void SygusSymBreakNew::assertTesterInternal( int tindex, TNode n, Node exp, std: Node a = d_term_to_anchor[n]; Assert( d_anchor_to_measure_term.find( a )!=d_anchor_to_measure_term.end() ); Node m = d_anchor_to_measure_term[a]; - std::map< Node, SearchSizeInfo * >::iterator itsz = d_szinfo.find( m ); + std::map>::iterator itsz = + d_szinfo.find(m); Assert( itsz!=d_szinfo.end() ); unsigned ssz = itsz->second->d_curr_search_size; @@ -1073,6 +1073,19 @@ void SygusSymBreakNew::registerSizeTerm( Node e, std::vector< Node >& lemmas ) { Node ag = d_tds->getActiveGuardForEnumerator(e); if( !ag.isNull() ){ d_anchor_to_active_guard[e] = ag; + std::map>::iterator itaas = + d_anchor_to_ag_strategy.find(e); + if (itaas == d_anchor_to_ag_strategy.end()) + { + d_anchor_to_ag_strategy[e].reset( + new DecisionStrategySingleton("sygus_enum_active", + ag, + d_td->getSatContext(), + d_td->getValuation())); + } + d_td->getDecisionManager()->registerStrategy( + DecisionManager::STRAT_DT_SYGUS_ENUM_ACTIVE, + d_anchor_to_ag_strategy[e].get()); } Node m; if( !ag.isNull() ){ @@ -1119,15 +1132,21 @@ void SygusSymBreakNew::registerSizeTerm( Node e, std::vector< Node >& lemmas ) { } void SygusSymBreakNew::registerMeasureTerm( Node m ) { - std::map< Node, SearchSizeInfo * >::iterator it = d_szinfo.find( m ); + std::map>::iterator it = + d_szinfo.find(m); if( it==d_szinfo.end() ){ Trace("sygus-sb") << "Sygus : register measure term : " << m << std::endl; - d_szinfo[m] = new SearchSizeInfo( m, d_td->getSatContext() ); + d_szinfo[m].reset(new SygusSizeDecisionStrategy( + m, d_td->getSatContext(), d_td->getValuation())); + // register this as a decision strategy + d_td->getDecisionManager()->registerStrategy( + DecisionManager::STRAT_DT_SYGUS_ENUM_SIZE, d_szinfo[m].get()); } } void SygusSymBreakNew::notifySearchSize( Node m, unsigned s, Node exp, std::vector< Node >& lemmas ) { - std::map< Node, SearchSizeInfo * >::iterator its = d_szinfo.find( m ); + std::map>::iterator its = + d_szinfo.find(m); Assert( its!=d_szinfo.end() ); if( its->second->d_search_size.find( s )==its->second->d_search_size.end() ){ its->second->d_search_size[s] = true; @@ -1174,13 +1193,15 @@ unsigned SygusSymBreakNew::getSearchSizeForAnchor( Node a ) { unsigned SygusSymBreakNew::getSearchSizeForMeasureTerm(Node m) { Trace("sygus-sb-debug2") << "get search size for measure : " << m << std::endl; - std::map< Node, SearchSizeInfo * >::iterator its = d_szinfo.find( m ); + std::map>::iterator its = + d_szinfo.find(m); Assert( its!=d_szinfo.end() ); return its->second->d_curr_search_size; } void SygusSymBreakNew::incrementCurrentSearchSize( Node m, std::vector< Node >& lemmas ) { - std::map< Node, SearchSizeInfo * >::iterator itsz = d_szinfo.find( m ); + std::map>::iterator itsz = + d_szinfo.find(m); 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; @@ -1322,8 +1343,10 @@ void SygusSymBreakNew::check( std::vector< Node >& lemmas ) { if (lemmas.empty() && !d_szinfo.empty()) { Trace("cegqi-engine") << "*** Sygus : passed datatypes check. term size(s) : "; - for( std::map< Node, SearchSizeInfo * >::iterator it = d_szinfo.begin(); it != d_szinfo.end(); ++it ){ - SearchSizeInfo * s = it->second; + for (std::pair>& + p : d_szinfo) + { + SygusSizeDecisionStrategy* s = p.second.get(); Trace("cegqi-engine") << s->d_curr_search_size << " "; } Trace("cegqi-engine") << std::endl; @@ -1403,7 +1426,7 @@ Node SygusSymBreakNew::getCurrentTemplate( Node n, std::map< TypeNode, int >& va } } -Node SygusSymBreakNew::SearchSizeInfo::getOrMkMeasureValue( +Node SygusSymBreakNew::SygusSizeDecisionStrategy::getOrMkMeasureValue( std::vector& lemmas) { if (d_measure_value.isNull()) @@ -1418,7 +1441,7 @@ Node SygusSymBreakNew::SearchSizeInfo::getOrMkMeasureValue( return d_measure_value; } -Node SygusSymBreakNew::SearchSizeInfo::getOrMkActiveMeasureValue( +Node SygusSymBreakNew::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue( std::vector& lemmas, bool mkNew) { if (mkNew) @@ -1436,69 +1459,23 @@ Node SygusSymBreakNew::SearchSizeInfo::getOrMkActiveMeasureValue( return d_measure_value_active; } -Node SygusSymBreakNew::SearchSizeInfo::getFairnessLiteral( unsigned s, TheoryDatatypes * d, std::vector< Node >& lemmas ) { - if( options::sygusFair()!=SYGUS_FAIR_NONE ){ - std::map< unsigned, Node >::iterator it = d_lits.find( s ); - if( it==d_lits.end() ){ - if (options::sygusAbortSize() != -1 - && static_cast(s) > options::sygusAbortSize()) - { - std::stringstream ss; - ss << "Maximum term size (" << options::sygusAbortSize() - << ") for enumerative SyGuS exceeded."; - throw LogicException(ss.str()); - } - Assert( !d_this.isNull() ); - Node c = NodeManager::currentNM()->mkConst( Rational( s ) ); - Node lit = NodeManager::currentNM()->mkNode( DT_SYGUS_BOUND, d_this, c ); - lit = d->getValuation().ensureLiteral( lit ); - - Trace("sygus-fair") << "******* Sygus : allocate size literal " << s << " for " << d_this << " : " << lit << std::endl; - Trace("cegqi-engine") << "******* Sygus : allocate size literal " << s << " for " << d_this << std::endl; - Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() ); - Trace("sygus-dec") << "Sygus : Fairness split : " << lem << std::endl; - lemmas.push_back( lem ); - d->getOutputChannel().requirePhase( lit, true ); - - d_lits[s] = lit; - return lit; - }else{ - return it->second; - } - }else{ +Node SygusSymBreakNew::SygusSizeDecisionStrategy::mkLiteral(unsigned s) +{ + if (options::sygusFair() == SYGUS_FAIR_NONE) + { return Node::null(); } -} - -Node SygusSymBreakNew::getNextDecisionRequest( unsigned& priority, std::vector< Node >& lemmas ) { - Trace("sygus-dec-debug") << "SygusSymBreakNew: Get next decision " << std::endl; - for( std::map< Node, Node >::iterator it = d_anchor_to_active_guard.begin(); it != d_anchor_to_active_guard.end(); ++it ){ - if( getGuardStatus( it->second )==0 ){ - Trace("sygus-dec") << "Sygus : Decide next on active guard : " << it->second << "..." << std::endl; - priority = 1; - return it->second; - } - } - for( std::map< Node, SearchSizeInfo * >::iterator it = d_szinfo.begin(); it != d_szinfo.end(); ++it ){ - SearchSizeInfo * s = it->second; - std::vector< Node > new_lit; - Node c_lit = s->getCurrentFairnessLiteral( d_td, lemmas ); - Assert( !c_lit.isNull() ); - int gstatus = getGuardStatus( c_lit ); - if( gstatus==-1 ){ - s->incrementCurrentLiteral(); - c_lit = s->getCurrentFairnessLiteral( d_td, lemmas ); - Assert( !c_lit.isNull() ); - Trace("sygus-dec") << "Sygus : Decide on next lit : " << c_lit << "..." << std::endl; - priority = 1; - return c_lit; - }else if( gstatus==0 ){ - Trace("sygus-dec") << "Sygus : Decide on current lit : " << c_lit << "..." << std::endl; - priority = 1; - return c_lit; - } + if (options::sygusAbortSize() != -1 + && static_cast(s) > options::sygusAbortSize()) + { + std::stringstream ss; + ss << "Maximum term size (" << options::sygusAbortSize() + << ") for enumerative SyGuS exceeded."; + throw LogicException(ss.str()); } - return Node::null(); + Assert(!d_this.isNull()); + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(DT_SYGUS_BOUND, d_this, nm->mkConst(Rational(s))); } int SygusSymBreakNew::getGuardStatus( Node g ) { diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index c5f3fe560..e2ed4192a 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -51,6 +51,18 @@ class TheoryDatatypes; * 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. + * + * This class enforces two decisions stragies via calls to registerStrategy + * of the owning theory's DecisionManager: + * (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). Both kinds of decision are + * critical for solution completeness, which is enforced by DecisionManager. */ class SygusSymBreakNew { @@ -95,24 +107,6 @@ class SygusSymBreakNew * 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: /** Pointer to the datatype theory that owns this class. */ TheoryDatatypes* d_td; @@ -453,14 +447,17 @@ private: * 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 + * SygusSizeDecisionStrategy 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 + /** A decision strategy for each measure term allocated by this class */ + class SygusSizeDecisionStrategy : public DecisionStrategyFmf { public: - SearchSizeInfo( Node t, context::Context* c ) : d_this( t ), d_curr_search_size(0), d_curr_lit( c, 0 ) {} + SygusSizeDecisionStrategy(Node t, context::Context* c, Valuation valuation) + : DecisionStrategyFmf(c, valuation), d_this(t), d_curr_search_size(0) + { + } /** the measure term */ Node d_this; /** @@ -512,28 +509,13 @@ private: */ 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 ); + /** Returns the s^th fairness literal for this measure term. */ + Node mkLiteral(unsigned s) override; + /** identify */ + std::string identify() const override + { + return std::string("sygus_enum_size"); } - /** increment current term size */ - void incrementCurrentLiteral() { d_curr_lit.set( d_curr_lit.get() + 1 ); } private: /** the measure value */ @@ -542,11 +524,13 @@ private: Node d_measure_value_active; }; /** the above information for each registered measure term */ - std::map< Node, SearchSizeInfo * > d_szinfo; + std::map> 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; + /** map from enumerators (anchors) to a decision stratregy for that guard */ + std::map> d_anchor_to_ag_strategy; /** generic measure term * * This is a global term that is used as the measure term for all sygus @@ -571,7 +555,7 @@ private: * 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. */ + /** Allocates a SygusSizeDecisionStrategy object in d_szinfo. */ void registerMeasureTerm( Node m ); /** * Return the current search size for arbitrary term n. This is the current diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 9c7365ac1..b83e9616a 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -7,7 +7,7 @@ theory THEORY_DATATYPES ::CVC4::theory::datatypes::TheoryDatatypes "theory/datatypes/theory_datatypes.h" typechecker "theory/datatypes/theory_datatypes_type_rules.h" -properties check presolve parametric propagate getNextDecisionRequest +properties check presolve parametric propagate rewriter ::CVC4::theory::datatypes::DatatypesRewriter "theory/datatypes/datatypes_rewriter.h" diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 283c70ada..10328c653 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -2238,17 +2238,6 @@ std::pair TheoryDatatypes::entailmentCheck(TNode lit, const Entailme return make_pair(false, Node::null()); } -Node TheoryDatatypes::getNextDecisionRequest( unsigned& priority ) { - if( d_sygus_sym_break ){ - std::vector< Node > lemmas; - Node ret = d_sygus_sym_break->getNextDecisionRequest( priority, lemmas ); - doSendLemmas( lemmas ); - return ret; - }else{ - return Node::null(); - } -} - } /* namepsace CVC4::theory::datatypes */ } /* namepsace CVC4::theory */ } /* namepsace CVC4 */ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 233ebd052..de2863718 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -346,8 +346,6 @@ private: /** sygus symmetry breaking utility */ SygusSymBreakNew* d_sygus_sym_break; -public: - Node getNextDecisionRequest(unsigned& priority) override; };/* class TheoryDatatypes */ }/* CVC4::theory::datatypes namespace */ -- 2.30.2