#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
#include "theory/quantifiers/sygus/sygus_unif_rl.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/theory_engine.h"
using namespace CVC4::kind;
NodeManager* nm = NodeManager::currentNM();
Valuation& valuation = d_qe->getValuation();
bool addedUnifEnumSymBreakLemma = false;
- Node cost_lit = d_u_enum_manager.getCurrentLiteral();
+ Node cost_lit = d_u_enum_manager.getAssertedLiteral();
std::map<Node, std::vector<Node>> unif_enums[2];
std::map<Node, std::vector<Node>> unif_values[2];
for (const Node& c : d_unif_candidates)
if (index == 0)
{
// given a pool of unification enumerators eu_1, ..., eu_n,
- // CegisUnifEnumManager insists that size(eu_1) <= ... <= size(eu_n).
+ // CegisUnifEnumDecisionStrategy insists that size(eu_1) <= ... <= size(eu_n).
// We additionally insist that M(eu_i) < M(eu_{i+1}) when
// size(eu_i) = size(eu_{i+1}), where < is pointer comparison.
// We enforce this below by adding symmetry breaking lemmas of the
OR, d_parent->getGuard().negate(), plem));
}
-Node CegisUnif::getNextDecisionRequest(unsigned& priority)
-{
- return d_u_enum_manager.getNextDecisionRequest(priority);
-}
-
-CegisUnifEnumManager::CegisUnifEnumManager(QuantifiersEngine* qe,
+CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe,
CegConjecture* parent)
- : d_qe(qe),
- d_parent(parent),
- d_ret_dec(qe->getSatContext(), false),
- d_curr_guq_val(qe->getSatContext(), 0)
+ : DecisionStrategyFmf(qe->getSatContext(), qe->getValuation()),
+ d_qe(qe),
+ d_parent(parent)
{
d_initialized = false;
d_tds = d_qe->getTermDatabaseSygus();
}
-void CegisUnifEnumManager::initialize(
+Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Node new_lit = nm->mkSkolem("G_cost", nm->booleanType());
+ unsigned new_size = n + 1;
+
+ // allocate an enumerator for each candidate
+ for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
+ {
+ Node c = ci.first;
+ TypeNode ct = c.getType();
+ Node eu = nm->mkSkolem("eu", ct);
+ Node ceu;
+ if (!options::sygusUnifCondIndependent() && !ci.second.d_enums[0].empty())
+ {
+ // make a new conditional enumerator as well, starting the
+ // second type around
+ ceu = nm->mkSkolem("cu", ci.second.d_ce_type);
+ }
+ // register the new enumerators
+ for (unsigned index = 0; index < 2; index++)
+ {
+ Node e = index == 0 ? eu : ceu;
+ if (e.isNull())
+ {
+ continue;
+ }
+ setUpEnumerator(e, ci.second, index);
+ }
+ }
+ // register the evaluation points at the new value
+ for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
+ {
+ Node c = ci.first;
+ for (const Node& ei : ci.second.d_eval_points)
+ {
+ Trace("cegis-unif-enum") << "...increasing enum number for hd " << ei
+ << " to new size " << new_size << "\n";
+ registerEvalPtAtSize(c, ei, new_lit, new_size);
+ }
+ }
+ // enforce fairness between number of enumerators and enumerator size
+ if (new_size > 1)
+ {
+ // construct the "virtual enumerator"
+ if (d_virtual_enum.isNull())
+ {
+ // we construct the default integer grammar with no variables, e.g.:
+ // A -> 0 | 1 | A+A
+ TypeNode intTn = nm->integerType();
+ // use a null variable list
+ Node bvl;
+ std::stringstream ss;
+ ss << "_virtual_enum_grammar";
+ std::string virtualEnumName(ss.str());
+ std::map<TypeNode, std::vector<Node>> extra_cons;
+ std::map<TypeNode, std::vector<Node>> exclude_cons;
+ // do not include "-", which is included by default for integers
+ exclude_cons[intTn].push_back(nm->operatorOf(MINUS));
+ std::unordered_set<Node, NodeHashFunction> term_irrelevant;
+ TypeNode vtn = CegGrammarConstructor::mkSygusDefaultType(intTn,
+ bvl,
+ virtualEnumName,
+ extra_cons,
+ exclude_cons,
+ term_irrelevant);
+ d_virtual_enum = nm->mkSkolem("_ve", vtn);
+ d_tds->registerEnumerator(d_virtual_enum, Node::null(), d_parent);
+ }
+ // if new_size is a power of two, then isPow2 returns log2(new_size)+1
+ // otherwise, this returns 0. In the case it returns 0, we don't care
+ // since the floor( log2( i ) ) = floor( log2( i - 1 ) ) and we do not
+ // increase our size bound.
+ unsigned pow_two = Integer(new_size).isPow2();
+ if (pow_two > 0)
+ {
+ Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum);
+ Node fair_lemma =
+ nm->mkNode(GEQ, size_ve, nm->mkConst(Rational(pow_two - 1)));
+ fair_lemma = nm->mkNode(OR, new_lit, fair_lemma);
+ Trace("cegis-unif-enum-lemma")
+ << "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n";
+ // this lemma relates the number of conditions we enumerate and the
+ // maximum size of a term that is part of our solution. It is of the
+ // form:
+ // G_uq_i => size(ve) >= log_2( i-1 )
+ // In other words, if we use i conditions, then we allow terms in our
+ // solution whose size is at most log_2(i-1).
+ d_qe->getOutputChannel().lemma(fair_lemma);
+ }
+ }
+
+ return new_lit;
+}
+
+void CegisUnifEnumDecisionStrategy::initialize(
const std::vector<Node>& es,
const std::map<Node, Node>& e_to_cond,
const std::map<Node, std::vector<Node>>& strategy_lemmas)
std::pair<Node, Node>(d_sbt_lemma, sp);
}
}
- // initialize the current literal
- incrementNumEnumerators();
+
+ // register this strategy
+ d_qe->getTheoryEngine()->getDecisionManager()->registerStrategy(
+ DecisionManager::STRAT_QUANT_CEGIS_UNIF_NUM_ENUMS, this);
+
// create single condition enumerator for each decision tree strategy
if (options::sygusUnifCondIndependent())
{
}
}
-void CegisUnifEnumManager::getEnumeratorsForStrategyPt(Node e,
+void CegisUnifEnumDecisionStrategy::getEnumeratorsForStrategyPt(Node e,
std::vector<Node>& es,
unsigned index) const
{
// the number of active enumerators is related to the current cost value
- unsigned num_enums = d_curr_guq_val.get();
- Assert(num_enums > 0);
+ unsigned num_enums = 0;
+ bool has_num_enums = getAssertedLiteralIndex(num_enums);
+ AlwaysAssert(has_num_enums);
+ num_enums = num_enums + 1;
if (index == 1)
{
// we always use (cost-1) conditions, or 1 if in the indepedent case
}
}
-Node CegisUnifEnumManager::getActiveGuardForEnumerator(Node e)
+Node CegisUnifEnumDecisionStrategy::getActiveGuardForEnumerator(Node e)
{
Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
return d_enum_to_active_guard[e];
}
-void CegisUnifEnumManager::setUpEnumerator(Node e,
+void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
StrategyPtInfo& si,
unsigned index)
{
e, si.d_pt, d_parent, options::sygusUnifCondIndependent() && index == 1);
}
-void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node e)
+void CegisUnifEnumDecisionStrategy::registerEvalPts(const std::vector<Node>& eis, Node e)
{
// candidates of the same type are managed
std::map<Node, StrategyPtInfo>::iterator it = d_ce_info.find(e);
for (const Node& ei : eis)
{
Assert(ei.getType() == e.getType());
- for (const std::pair<const unsigned, Node>& p : d_guq_lit)
+ for (unsigned j = 0, size = d_literals.size(); j < size; j++)
{
Trace("cegis-unif-enum") << "...for cand " << e << " adding hd " << ei
- << " at size " << p.first << "\n";
- registerEvalPtAtSize(e, ei, p.second, p.first);
+ << " at size " << j << "\n";
+ registerEvalPtAtSize(e, ei, d_literals[j], j + 1);
}
}
}
-Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority)
-{
- // are we not initialized or have we returned our decision in the current SAT
- // context?
- if (!d_initialized || d_ret_dec.get())
- {
- return Node::null();
- }
- if (d_ce_info.empty())
- {
- // if no enumerators, the decision is null
- d_ret_dec = true;
- return Node::null();
- }
- Node lit = getCurrentLiteral();
- bool value;
- if (!d_qe->getValuation().hasSatValue(lit, value))
- {
- priority = 1;
- return lit;
- }
- else if (!value)
- {
- // propagated false, increment
- incrementNumEnumerators();
- return getNextDecisionRequest(priority);
- }
- d_ret_dec = true;
- return Node::null();
-}
-
-void CegisUnifEnumManager::incrementNumEnumerators()
-{
- unsigned new_size = d_curr_guq_val.get() + 1;
- d_curr_guq_val.set(new_size);
- // ensure that the literal has been allocated
- std::map<unsigned, Node>::iterator itc = d_guq_lit.find(new_size);
- if (itc == d_guq_lit.end())
- {
- // allocate the new literal
- NodeManager* nm = NodeManager::currentNM();
- Node new_lit = Rewriter::rewrite(nm->mkSkolem("G_cost", nm->booleanType()));
- new_lit = d_qe->getValuation().ensureLiteral(new_lit);
- AlwaysAssert(!new_lit.isNull());
- d_qe->getOutputChannel().requirePhase(new_lit, true);
- d_guq_lit[new_size] = new_lit;
- // allocate an enumerator for each candidate
- for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
- {
- Node c = ci.first;
- TypeNode ct = c.getType();
- Node eu = nm->mkSkolem("eu", ct);
- Node ceu;
- if (!options::sygusUnifCondIndependent() && !ci.second.d_enums[0].empty())
- {
- // make a new conditional enumerator as well, starting the
- // second type around
- ceu = nm->mkSkolem("cu", ci.second.d_ce_type);
- }
- // register the new enumerators
- for (unsigned index = 0; index < 2; index++)
- {
- Node e = index == 0 ? eu : ceu;
- if (e.isNull())
- {
- continue;
- }
- setUpEnumerator(e, ci.second, index);
- }
- }
- // register the evaluation points at the new value
- for (std::pair<const Node, StrategyPtInfo>& ci : d_ce_info)
- {
- Node c = ci.first;
- for (const Node& ei : ci.second.d_eval_points)
- {
- Trace("cegis-unif-enum") << "...increasing enum number for hd " << ei
- << " to new size " << new_size << "\n";
- registerEvalPtAtSize(c, ei, new_lit, new_size);
- }
- }
- // enforce fairness between number of enumerators and enumerator size
- if (new_size > 1)
- {
- // construct the "virtual enumerator"
- if (d_virtual_enum.isNull())
- {
- // we construct the default integer grammar with no variables, e.g.:
- // A -> 0 | 1 | A+A
- TypeNode intTn = nm->integerType();
- // use a null variable list
- Node bvl;
- std::stringstream ss;
- ss << "_virtual_enum_grammar";
- std::string virtualEnumName(ss.str());
- std::map<TypeNode, std::vector<Node>> extra_cons;
- std::map<TypeNode, std::vector<Node>> exclude_cons;
- // do not include "-", which is included by default for integers
- exclude_cons[intTn].push_back(nm->operatorOf(MINUS));
- std::unordered_set<Node, NodeHashFunction> term_irrelevant;
- TypeNode vtn =
- CegGrammarConstructor::mkSygusDefaultType(intTn,
- bvl,
- virtualEnumName,
- extra_cons,
- exclude_cons,
- term_irrelevant);
- d_virtual_enum = nm->mkSkolem("_ve", vtn);
- d_tds->registerEnumerator(d_virtual_enum, Node::null(), d_parent);
- }
- // if new_size is a power of two, then isPow2 returns log2(new_size)+1
- // otherwise, this returns 0. In the case it returns 0, we don't care
- // since the floor( log2( i ) ) = floor( log2( i - 1 ) ) and we do not
- // increase our size bound.
- unsigned pow_two = Integer(new_size).isPow2();
- if (pow_two > 0)
- {
- Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum);
- Node fair_lemma =
- nm->mkNode(GEQ, size_ve, nm->mkConst(Rational(pow_two - 1)));
- fair_lemma = nm->mkNode(OR, new_lit, fair_lemma);
- Trace("cegis-unif-enum-lemma")
- << "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n";
- // this lemma relates the number of conditions we enumerate and the
- // maximum size of a term that is part of our solution. It is of the
- // form:
- // G_uq_i => size(ve) >= log_2( i-1 )
- // In other words, if we use i conditions, then we allow terms in our
- // solution whose size is at most log_2(i-1).
- d_qe->getOutputChannel().lemma(fair_lemma);
- }
- }
- }
-}
-
-Node CegisUnifEnumManager::getCurrentLiteral() const
-{
- return getLiteral(d_curr_guq_val.get());
-}
-
-Node CegisUnifEnumManager::getLiteral(unsigned n) const
-{
- std::map<unsigned, Node>::const_iterator itc = d_guq_lit.find(n);
- Assert(itc != d_guq_lit.end());
- return itc->second;
-}
-void CegisUnifEnumManager::registerEvalPtAtSize(Node e,
+void CegisUnifEnumDecisionStrategy::registerEvalPtAtSize(Node e,
Node ei,
Node guq_lit,
unsigned n)
namespace theory {
namespace quantifiers {
-/** Cegis Unif Enumeration Manager
+/** Cegis Unif Enumerators Decision Strategy
*
- * This class enforces a decision heuristic that limits the number of
+ * This class enforces a decision strategy that limits the number of
* unique values given to the set of heads of evaluation points and conditions
* enumerators for these points, which are variables of sygus datatype type that
* are introduced by CegisUnif.
* To enforce this, we introduce sygus enumerator(s) of the same type as the
* heads of evaluation points and condition enumerators registered to this class
* and add lemmas that enforce that these terms are equal to at least one
- * enumerator (see registerEvalPtAtValue).
+ * enumerator (see registerEvalPtAtSize).
*/
-class CegisUnifEnumManager
+class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
{
public:
- CegisUnifEnumManager(QuantifiersEngine* qe, CegConjecture* parent);
+ CegisUnifEnumDecisionStrategy(QuantifiersEngine* qe, CegConjecture* parent);
+ /** Make the n^th literal of this strategy (G_uq_n).
+ *
+ * This call may add new lemmas of the form described above
+ * registerEvalPtAtValue on the output channel of d_qe.
+ */
+ Node mkLiteral(unsigned n) override;
+ /** identify */
+ std::string identify() const override
+ {
+ return std::string("cegis_unif_num_enums");
+ }
+
/** initialize candidates
*
* Notify this class that it will be managing enumerators for the vector
* for strategy point e, where e was passed to initialize in the vector es.
*
* This may add new lemmas of the form described above
- * registerEvalPtAtValue on the output channel of d_qe.
+ * registerEvalPtAtSize on the output channel of d_qe.
*/
void registerEvalPts(const std::vector<Node>& eis, Node e);
/** Retrieves active guard for enumerator */
Node getActiveGuardForEnumerator(Node e);
- /** get next decision request
- *
- * This function has the same contract as Theory::getNextDecisionRequest.
- *
- * If no guard G_uq_* is asserted positively, then this method returns the
- * minimal G_uq_i that is not asserted negatively. It allocates this guard
- * if necessary.
- *
- * This call may add new lemmas of the form described above
- * registerEvalPtAtValue on the output channel of d_qe.
- */
- Node getNextDecisionRequest(unsigned& priority);
- /**
- * Get the "current" literal G_uq_n, where n is the minimal n such that G_uq_n
- * is not asserted negatively in the current SAT context.
- */
- Node getCurrentLiteral() const;
-
private:
/** reference to quantifier engine */
QuantifiersEngine* d_qe;
};
/** map strategy points to the above info */
std::map<Node, StrategyPtInfo> d_ce_info;
- /** literals of the form G_uq_n for each n */
- std::map<unsigned, Node> d_guq_lit;
- /** Have we returned a decision in the current SAT context? */
- context::CDO<bool> d_ret_dec;
/** the "virtual" enumerator
*
* This enumerator is used for enforcing fairness. In particular, we relate
* (0,8), ..., (0,15), (1,8), ..., (1,15), ... [size 3]
*/
Node d_virtual_enum;
- /**
- * The minimal n such that G_uq_n is not asserted negatively in the
- * current SAT context.
- */
- context::CDO<unsigned> d_curr_guq_val;
/** Registers an enumerator and adds symmetry breaking lemmas
*
* The symmetry breaking lemmas are generated according to the stored
* order of size.
*/
void setUpEnumerator(Node e, StrategyPtInfo& si, unsigned index);
- /** increment the number of enumerators */
- void incrementNumEnumerators();
- /** get literal G_uq_n */
- Node getLiteral(unsigned n) const;
/** register evaluation point at size
*
* This sends a lemma of the form:
void registerRefinementLemma(const std::vector<Node>& vars,
Node lem,
std::vector<Node>& lems) override;
- /** get next decision request */
- Node getNextDecisionRequest(unsigned& priority) override;
private:
/** do cegis-implementation-specific initialization for this class */
*/
SygusUnifRl d_sygus_unif;
/** enumerator manager utility */
- CegisUnifEnumManager d_u_enum_manager;
+ CegisUnifEnumDecisionStrategy d_u_enum_manager;
/* The null node */
Node d_null;
/** the unification candidates */
projects / cvc5.git / commitdiff