}
SygusSymBreakNew::~SygusSymBreakNew() {
- for( std::map< Node, SearchSizeInfo * >::iterator it = d_szinfo.begin(); it != d_szinfo.end(); ++it ){
- delete it->second;
- }
+
}
/** add tester */
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<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator its =
+ d_szinfo.find(m);
Assert( its!=d_szinfo.end() );
Node mt = its->second->getOrMkMeasureValue(lemmas);
//it relates the measure term to arithmetic
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<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator itsz =
+ d_szinfo.find(m);
Assert( itsz!=d_szinfo.end() );
unsigned ssz = itsz->second->d_curr_search_size;
Node ag = d_tds->getActiveGuardForEnumerator(e);
if( !ag.isNull() ){
d_anchor_to_active_guard[e] = ag;
+ std::map<Node, std::unique_ptr<DecisionStrategy>>::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() ){
}
void SygusSymBreakNew::registerMeasureTerm( Node m ) {
- std::map< Node, SearchSizeInfo * >::iterator it = d_szinfo.find( m );
+ std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::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<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::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;
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<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::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<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::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;
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<const Node, std::unique_ptr<SygusSizeDecisionStrategy>>&
+ p : d_szinfo)
+ {
+ SygusSizeDecisionStrategy* s = p.second.get();
Trace("cegqi-engine") << s->d_curr_search_size << " ";
}
Trace("cegqi-engine") << std::endl;
}
}
-Node SygusSymBreakNew::SearchSizeInfo::getOrMkMeasureValue(
+Node SygusSymBreakNew::SygusSizeDecisionStrategy::getOrMkMeasureValue(
std::vector<Node>& lemmas)
{
if (d_measure_value.isNull())
return d_measure_value;
}
-Node SygusSymBreakNew::SearchSizeInfo::getOrMkActiveMeasureValue(
+Node SygusSymBreakNew::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue(
std::vector<Node>& lemmas, bool mkNew)
{
if (mkNew)
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<int>(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<int>(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 ) {
* 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
{
* all preregistered enumerators.
*/
void check(std::vector<Node>& 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<Node>& lemmas);
-
private:
/** Pointer to the datatype theory that owns this class. */
TheoryDatatypes* d_td;
* 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<Node>& 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;
/**
*/
Node getOrMkActiveMeasureValue(std::vector<Node>& 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 */
Node d_measure_value_active;
};
/** the above information for each registered measure term */
- std::map< Node, SearchSizeInfo * > d_szinfo;
+ std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>> 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<Node, std::unique_ptr<DecisionStrategy>> d_anchor_to_ag_strategy;
/** generic measure term
*
* This is a global term that is used as the measure term for all sygus
* 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
projects / cvc5.git / commitdiff