{
Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl;
// Init UNIF util
- d_sygus_unif.initialize(d_qe, candidates, d_cond_enums, lemmas);
+ std::map<Node, std::vector<Node>> strategy_lemmas;
+ d_sygus_unif.initialize(d_qe, candidates, d_cond_enums, strategy_lemmas);
Trace("cegis-unif") << "Initializing enums for pure Cegis case\n";
std::vector<Node> unif_candidates;
// Initialize enumerators for non-unif functions-to-synhesize
d_enum_to_active_guard[e] = g;
}
// initialize the enumeration manager
- d_u_enum_manager.initialize(unif_candidates);
+ d_u_enum_manager.initialize(unif_candidates, strategy_lemmas);
return true;
}
std::vector<Node>& lems)
{
// Notify lemma to unification utility and get its purified form
- std::map<Node, std::vector<Node> > eval_pts;
+ std::map<Node, std::vector<Node>> eval_pts;
Node plem = d_sygus_unif.addRefLemma(lem, eval_pts);
d_refinement_lemmas.push_back(plem);
Trace("cegis-unif") << "* Refinement lemma:\n" << plem << "\n";
// Notify the enumeration manager if there are new evaluation points
- for (const std::pair<const Node, std::vector<Node> >& ep : eval_pts)
+ for (const std::pair<const Node, std::vector<Node>>& ep : eval_pts)
{
+ Trace("cegis-unif") << "** Registering new point:\n" << plem << "\n";
d_u_enum_manager.registerEvalPts(ep.second, ep.first);
}
// Make the refinement lemma and add it to lems. This lemma is guarded by the
d_tds = d_qe->getTermDatabaseSygus();
}
-void CegisUnifEnumManager::initialize(const std::vector<Node>& cs)
+void CegisUnifEnumManager::initialize(
+ const std::vector<Node>& cs,
+ const std::map<Node, std::vector<Node>>& strategy_lemmas)
{
Assert(!d_initialized);
d_initialized = true;
{
return;
}
+ // process strategy lemmas
+ std::map<TypeNode, std::pair<Node, std::vector<Node>>> tn_strategy_lemmas;
+ for (const std::pair<const Node, std::vector<Node>>& p : strategy_lemmas)
+ {
+ if (Trace.isOn("cegis-unif-enum-debug"))
+ {
+ Trace("cegis-unif-enum-debug") << "...lemmas of strategy pt " << p.first
+ << ":\n";
+ for (const Node& lem : p.second)
+ {
+ Trace("cegis-unif-enum-debug") << "\t" << lem << "\n";
+ }
+ }
+ TypeNode tn = p.first.getType();
+ Assert(tn_strategy_lemmas.find(tn) == tn_strategy_lemmas.end());
+ tn_strategy_lemmas[tn].first = p.first;
+ tn_strategy_lemmas[tn].second = p.second;
+ }
+ // initialize type information for candidates
+ NodeManager* nm = NodeManager::currentNM();
for (const Node& c : cs)
{
+ Trace("cegis-unif-enum-debug") << "...adding candidate " << c << "\n";
// currently, we allocate the same enumerators for candidates of the same
// type
TypeNode tn = c.getType();
d_ce_info[tn].d_candidates.push_back(c);
+ // retrieve symmetry breaking lemma template for type if not already init
+ if (!d_ce_info[tn].d_sbt_lemma.isNull())
+ {
+ continue;
+ }
+ std::map<const TypeNode, std::pair<Node, std::vector<Node>>>::iterator it =
+ tn_strategy_lemmas.find(tn);
+ if (it == tn_strategy_lemmas.end())
+ {
+ continue;
+ }
+ // collect lemmas for removing redundant ops for this candidate's type
+ d_ce_info[tn].d_sbt_lemma = nm->mkNode(AND, it->second.second);
+ Trace("cegis-unif-enum-debug")
+ << "...adding lemma template to remove redundant operators for " << c
+ << " and its type " << tn << " --> " << d_ce_info[tn].d_sbt_lemma
+ << "\n";
+ d_ce_info[tn].d_sbt_arg = it->second.first;
}
// initialize the current literal
incrementNumEnumerators();
{
TypeNode ct = ci.first;
Node eu = nm->mkSkolem("eu", ct);
+ // instantiate template for removing redundant operators
+ if (!ci.second.d_sbt_lemma.isNull())
+ {
+ Node templ = ci.second.d_sbt_lemma;
+ TNode templ_var = ci.second.d_sbt_arg;
+ Node sym_break_red_ops = templ.substitute(templ_var, eu);
+ Trace("cegis-unif-enum-lemma")
+ << "CegisUnifEnum::lemma, remove redundant ops of " << eu << " : "
+ << sym_break_red_ops << "\n";
+ d_qe->getOutputChannel().lemma(sym_break_red_ops);
+ }
if (!ci.second.d_enums.empty())
{
Node eu_prev = ci.second.d_enums.back();
disj.push_back(ei.eqNode(itc->second.d_enums[i]));
}
Node lem = NodeManager::currentNM()->mkNode(OR, disj);
- Trace("cegis-unif-enum-lemma")
- << "CegisUnifEnum::lemma, domain:" << lem << "\n";
+ Trace("cegis-unif-enum-lemma") << "CegisUnifEnum::lemma, domain:" << lem
+ << "\n";
d_qe->getOutputChannel().lemma(lem);
}
* Each candidate c in cs should be such that we are using a
* synthesis-by-unification approach for c.
*/
- void initialize(const std::vector<Node>& cs);
+ void initialize(const std::vector<Node>& cs,
+ const std::map<Node, std::vector<Node>>& strategy_lemmas);
/** register evaluation point for candidate
*
* This notifies this class that eis is a set of heads of evaluation points
std::vector<Node> d_enums;
/** the set of evaluation points of this type */
std::vector<Node> d_eval_points;
+ /** symmetry breaking lemma template for this type */
+ Node d_sbt_lemma;
+ /** argument (to be instantiated) of symmetry breaking lemma template */
+ Node d_sbt_arg;
};
/** map types to the above info */
std::map<TypeNode, TypeInfo> d_ce_info;
std::vector<Node>& lemmas)
{
Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
-
- for( unsigned i=0; i<candidates.size(); i++ ){
+
+ for (unsigned i = 0; i < candidates.size(); i++)
+ {
Node v = candidates[i];
d_examples[v].clear();
d_examples_out[v].clear();
d_examples_term[v].clear();
}
-
- std::map< Node, bool > visited;
- collectExamples( n, visited, true, true );
-
- for( unsigned i=0; i<candidates.size(); i++ ){
+
+ std::map<Node, bool> visited;
+ collectExamples(n, visited, true, true);
+
+ for (unsigned i = 0; i < candidates.size(); i++)
+ {
Node v = candidates[i];
Trace("sygus-pbe") << " examples for " << v << " : ";
- if( d_examples_invalid.find( v )!=d_examples_invalid.end() ){
+ if (d_examples_invalid.find(v) != d_examples_invalid.end())
+ {
Trace("sygus-pbe") << "INVALID" << std::endl;
- }else{
+ }
+ else
+ {
Trace("sygus-pbe") << std::endl;
- for( unsigned j=0; j<d_examples[v].size(); j++ ){
+ for (unsigned j = 0; j < d_examples[v].size(); j++)
+ {
Trace("sygus-pbe") << " ";
- for( unsigned k=0; k<d_examples[v][j].size(); k++ ){
+ for (unsigned k = 0; k < d_examples[v][j].size(); k++)
+ {
Trace("sygus-pbe") << d_examples[v][j][k] << " ";
}
- if( !d_examples_out[v][j].isNull() ){
+ if (!d_examples_out[v][j].isNull())
+ {
Trace("sygus-pbe") << " -> " << d_examples_out[v][j];
}
Trace("sygus-pbe") << std::endl;
<< std::endl;
std::vector<Node> singleton_c;
singleton_c.push_back(c);
+ std::map<Node, std::vector<Node>> strategy_lemmas;
d_sygus_unif[c].initialize(
- d_qe, singleton_c, d_candidate_to_enum[c], lemmas);
+ d_qe, singleton_c, d_candidate_to_enum[c], strategy_lemmas);
+ // collect lemmas from all strategies
+ for (const std::pair<const Node, std::vector<Node>>& p : strategy_lemmas)
+ {
+ lemmas.insert(lemmas.end(), p.second.begin(), p.second.end());
+ }
Assert(!d_candidate_to_enum[c].empty());
Trace("sygus-pbe") << "Initialize " << d_candidate_to_enum[c].size()
<< " enumerators for " << c << "..." << std::endl;
private:
/** sygus term database of d_qe */
- quantifiers::TermDbSygus * d_tds;
+ quantifiers::TermDbSygus* d_tds;
/** true and false nodes */
Node d_true;
Node d_false;
* In other words, all occurrences of f are guarded by equalities that
* constraint its arguments to constants.
*/
- std::map< Node, bool > d_examples_invalid;
+ std::map<Node, bool> d_examples_invalid;
/** for each candidate variable (function-to-synthesize), whether the
* conjecture is purely PBE for that variable.
* An example of a conjecture for which d_examples_invalid is false but
* However, the domain of f in both cases is finite, which can be used for
* search space pruning.
*/
- std::map< Node, bool > d_examples_out_invalid;
+ std::map<Node, bool> d_examples_out_invalid;
/**
* Map from candidates to sygus unif utility. This class implements
* the core algorithm (e.g. decision tree learning) that this module relies
std::map<Node, Node> d_enum_to_active_guard;
/** for each candidate variable (function-to-synthesize), input of I/O
* examples */
- std::map< Node, std::vector< std::vector< Node > > > d_examples;
+ std::map<Node, std::vector<std::vector<Node> > > d_examples;
/** for each candidate variable (function-to-synthesize), output of I/O
* examples */
- std::map< Node, std::vector< Node > > d_examples_out;
+ std::map<Node, std::vector<Node> > d_examples_out;
/** the list of example terms
* For the example [EX#1] above, this is f( 0 ), f( 5 ), f( 6 )
*/
- std::map< Node, std::vector< Node > > d_examples_term;
+ std::map<Node, std::vector<Node> > d_examples_term;
/** collect the PBE examples in n
* This is called on the input conjecture, and will populate the above vectors.
* hasPol/pol denote the polarity of n in the conjecture.
*/
- void collectExamples( Node n, std::map< Node, bool >& visited, bool hasPol, bool pol );
+ void collectExamples(Node n,
+ std::map<Node, bool>& visited,
+ bool hasPol,
+ bool pol);
//--------------------------------- PBE search values
/**
* term x+y is indexed by 1,4
* term 0 is indexed by 0,0.
*/
- class PbeTrie {
+ class PbeTrie
+ {
public:
PbeTrie() {}
~PbeTrie() {}
* index : the index of the example we are processing,
* ntotal : the total of the examples for enumerator e.
*/
- Node addPbeExample(TypeNode etn, Node e, Node b, CegConjecturePbe* cpbe,
- unsigned index, unsigned ntotal);
+ Node addPbeExample(TypeNode etn,
+ Node e,
+ Node b,
+ CegConjecturePbe* cpbe,
+ unsigned index,
+ unsigned ntotal);
private:
/** Helper function for above, called when we get the current example ex. */
- Node addPbeExampleEval(TypeNode etn, Node e, Node b, std::vector<Node>& ex,
- CegConjecturePbe* cpbe, unsigned index,
+ Node addPbeExampleEval(TypeNode etn,
+ Node e,
+ Node b,
+ std::vector<Node>& ex,
+ CegConjecturePbe* cpbe,
+ unsigned index,
unsigned ntotal);
};
/** trie of candidate solutions tried
*/
std::map<Node, std::map<TypeNode, PbeTrie> > d_pbe_trie;
//--------------------------------- end PBE search values
-
};
-}/* namespace CVC4::theory::quantifiers */
-}/* namespace CVC4::theory */
-}/* namespace CVC4 */
+} /* namespace CVC4::theory::quantifiers */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
#endif
namespace quantifiers {
SygusUnif::SygusUnif() : d_qe(nullptr), d_tds(nullptr) {}
-
SygusUnif::~SygusUnif() {}
void SygusUnif::initialize(QuantifiersEngine* qe,
const std::vector<Node>& funs,
std::vector<Node>& enums,
- std::vector<Node>& lemmas)
+ std::map<Node, std::vector<Node>>& strategy_lemmas)
{
Assert(d_candidates.empty());
d_qe = qe;
Node SygusUnif::constructBestStringToConcat(
const std::vector<Node>& strs,
const std::map<Node, unsigned>& total_inc,
- const std::map<Node, std::vector<unsigned> >& incr)
+ const std::map<Node, std::vector<unsigned>>& incr)
{
Assert(!strs.empty());
std::vector<Node> strs_tmp = strs;
* the grammar of f and adds them to enums. These enumerators are those that
* should be later given to calls to notifyEnumeration below.
*
- * This also may result in lemmas being added to lemmas,
+ * This also may result in lemmas being added to strategy_lemmas,
* which correspond to static symmetry breaking predicates (for example,
* those that exclude ITE from enumerators whose role is enum_io when the
- * strategy is ITE_strat).
+ * strategy is ITE_strat). The lemmas are associated with a strategy point of
+ * the respective function-to-synthesize.
*/
virtual void initialize(QuantifiersEngine* qe,
const std::vector<Node>& funs,
std::vector<Node>& enums,
- std::vector<Node>& lemmas);
+ std::map<Node, std::vector<Node>>& strategy_lemmas);
/**
* Notify that the value v has been enumerated for enumerator e. This call
void SygusUnifIo::initialize(QuantifiersEngine* qe,
const std::vector<Node>& funs,
std::vector<Node>& enums,
- std::vector<Node>& lemmas)
+ std::map<Node, std::vector<Node>>& strategy_lemmas)
{
Assert(funs.size() == 1);
d_examples.clear();
d_examples_out.clear();
d_ecache.clear();
d_candidate = funs[0];
- SygusUnif::initialize(qe, funs, enums, lemmas);
+ SygusUnif::initialize(qe, funs, enums, strategy_lemmas);
// learn redundant operators based on the strategy
- d_strategy[d_candidate].staticLearnRedundantOps(lemmas);
+ d_strategy[d_candidate].staticLearnRedundantOps(strategy_lemmas);
}
void SygusUnifIo::addExample(const std::vector<Node>& input, Node output)
public:
UnifContextIo();
/** get current role */
- virtual NodeRole getCurrentRole() override;
+ NodeRole getCurrentRole() override;
/**
* This intiializes this context based on information in sui regarding the
* This is the current set of enumerator/node role pairs we are currently
* visiting. This set is cleared when the context is updated.
*/
- std::map<Node, std::map<NodeRole, bool> > d_visit_role;
+ std::map<Node, std::map<NodeRole, bool>> d_visit_role;
/** unif context enumerator information */
class UEnumInfo
* resulting in 2 and 4, are equal to the output value for the respective
* pairs.
*/
- std::map<Node, std::map<unsigned, Node> > d_look_ahead_sols;
+ std::map<Node, std::map<unsigned, Node>> d_look_ahead_sols;
};
/** map from enumerators to the above info class */
std::map<Node, UEnumInfo> d_uinfo;
*/
void getLeaves(const std::vector<Node>& vals,
bool pol,
- std::map<int, std::vector<Node> >& v);
+ std::map<int, std::vector<Node>>& v);
/** is this trie empty? */
bool isEmpty() { return d_term.isNull() && d_children.empty(); }
/** clear this trie */
/** helper function for above functions */
void getLeavesInternal(const std::vector<Node>& vals,
bool pol,
- std::map<int, std::vector<Node> >& v,
+ std::map<int, std::vector<Node>>& v,
unsigned index,
int status);
};
* The vector funs should be of length one, since I/O specifications across
* multiple functions can be separated.
*/
- virtual void initialize(QuantifiersEngine* qe,
- const std::vector<Node>& funs,
- std::vector<Node>& enums,
- std::vector<Node>& lemmas) override;
+ void initialize(QuantifiersEngine* qe,
+ const std::vector<Node>& funs,
+ std::vector<Node>& enums,
+ std::map<Node, std::vector<Node>>& strategy_lemmas) override;
/** Notify enumeration */
- virtual void notifyEnumeration(Node e,
- Node v,
- std::vector<Node>& lemmas) override;
+ void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) override;
/** Construct solution */
- virtual bool constructSolution(std::vector<Node>& sols) override;
+ bool constructSolution(std::vector<Node>& sols) override;
/** add example
*
Node d_true;
Node d_false;
/** input of I/O examples */
- std::vector<std::vector<Node> > d_examples;
+ std::vector<std::vector<Node>> d_examples;
/** output of I/O examples */
std::vector<Node> d_examples_out;
* This either stores the values of f( I ) for inputs
* or the value of f( I ) = O if d_role==enum_io
*/
- std::vector<std::vector<Node> > d_enum_vals_res;
+ std::vector<std::vector<Node>> d_enum_vals_res;
/**
* The set of values in d_enum_vals that have been "subsumed" by others
* (see SubsumeTrie for explanation of subsumed).
void SygusUnifRl::initialize(QuantifiersEngine* qe,
const std::vector<Node>& funs,
std::vector<Node>& enums,
- std::vector<Node>& lemmas)
+ std::map<Node, std::vector<Node>>& strategy_lemmas)
{
// initialize
std::vector<Node> all_enums;
- SygusUnif::initialize(qe, funs, all_enums, lemmas);
+ SygusUnif::initialize(qe, funs, all_enums, strategy_lemmas);
// based on the strategy inferred for each function, determine if we are
// using a unification strategy that is compatible our approach.
for (const Node& f : funs)
{
- registerStrategy(f);
+ d_strategy[f].staticLearnRedundantOps(strategy_lemmas);
+ registerStrategy(f, strategy_lemmas);
}
enums.insert(enums.end(), d_cond_enums.begin(), d_cond_enums.end());
// Copy candidates and check whether CegisUnif for any of them
return it->second;
}
-void SygusUnifRl::registerStrategy(Node f)
+void SygusUnifRl::registerStrategy(
+ Node f, std::map<Node, std::vector<Node>>& strategy_lemmas)
{
if (Trace.isOn("sygus-unif-rl-strat"))
{
Trace("sygus-unif-rl-strat") << "Register..." << std::endl;
Node e = d_strategy[f].getRootEnumerator();
std::map<Node, std::map<NodeRole, bool>> visited;
- registerStrategyNode(f, e, role_equal, visited);
+ registerStrategyNode(f, e, role_equal, visited, strategy_lemmas);
}
void SygusUnifRl::registerStrategyNode(
Node f,
Node e,
NodeRole nrole,
- std::map<Node, std::map<NodeRole, bool>>& visited)
+ std::map<Node, std::map<NodeRole, bool>>& visited,
+ std::map<Node, std::vector<Node>>& strategy_lemmas)
{
Trace("sygus-unif-rl-strat") << " register node " << e << std::endl;
if (visited[e].find(nrole) != visited[e].end())
<< " ...detected recursive ITE strategy, condition enumerator : "
<< cond << std::endl;
// indicate that we will be enumerating values for cond
- registerConditionalEnumerator(f, e, cond, j);
+ registerConditionalEnumerator(f, e, cond, j, strategy_lemmas);
}
}
// TODO: recurse? for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
}
}
-void SygusUnifRl::registerConditionalEnumerator(Node f,
- Node e,
- Node cond,
- unsigned strategy_index)
+void SygusUnifRl::registerConditionalEnumerator(
+ Node f,
+ Node e,
+ Node cond,
+ unsigned strategy_index,
+ std::map<Node, std::vector<Node>>& strategy_lemmas)
{
// we will do unification for this candidate
d_unif_candidates.insert(f);
// register the conditional enumerator
d_tds->registerEnumerator(cond, f, d_parent, true);
d_cenum_to_stratpt[cond].clear();
+ // register lemmas to remove redundant operators from condition enumeration
+ std::map<const Node, std::vector<Node>>::iterator it =
+ strategy_lemmas.find(cond);
+ if (it != strategy_lemmas.end())
+ {
+ for (const Node& lemma : it->second)
+ {
+ Trace("cegis-unif-enum-debug")
+ << "* Registering lemma to remove redundand operators for " << cond
+ << " --> " << lemma << "\n";
+ d_qe->getOutputChannel().lemma(lemma);
+ }
+ strategy_lemmas.erase(cond);
+ }
}
// register that this strategy node has a decision tree construction
d_stratpt_to_dt[e].initialize(cond, this, &d_strategy[f], strategy_index);
void initialize(QuantifiersEngine* qe,
const std::vector<Node>& funs,
std::vector<Node>& enums,
- std::vector<Node>& lemmas) override;
+ std::map<Node, std::vector<Node>>& strategy_lemmas) override;
/** Notify enumeration */
void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) override;
/** Construct solution */
*
* Initialize the above data for the relevant enumerators in the strategy tree
* of candidate variable f.
+ *
+ * Lemmas to remove redundant operators from enumerators of specific strategy
+ * points, if any, are retrived from strategy_lemmas.
*/
- void registerStrategy(Node f);
+ void registerStrategy(Node f,
+ std::map<Node, std::vector<Node>>& strategy_lemmas);
/** register strategy node
*
* Called while traversing the strategy tree of f. The arguments e and nrole
* indicate the current node in the tree we are traversing, and visited
* indicates the nodes we have already visited.
+ *
+ * Lemmas to remove redundant operators from enumerators of specific strategy
+ * points, if any, are retrived from strategy_lemmas.
*/
void registerStrategyNode(Node f,
Node e,
NodeRole nrole,
- std::map<Node, std::map<NodeRole, bool>>& visited);
+ std::map<Node, std::map<NodeRole, bool>>& visited,
+ std::map<Node, std::vector<Node>>& strategy_lemmas);
/** register conditional enumerator
*
* Registers that cond is a conditional enumerator for building a (recursive)
* decision tree at strategy node e within the strategy tree of f.
+ *
+ * Lemmas to remove redundant operators from enumerators of specific strategy
+ * points, if any, are retrived from strategy_lemmas.
*/
- void registerConditionalEnumerator(Node f,
- Node e,
- Node cond,
- unsigned strategy_index);
+ void registerConditionalEnumerator(
+ Node f,
+ Node e,
+ Node cond,
+ unsigned strategy_index,
+ std::map<Node, std::vector<Node>>& strategy_lemmas);
};
} /* CVC4::theory::quantifiers namespace */
return true;
}
-void SygusUnifStrategy::staticLearnRedundantOps(std::vector<Node>& lemmas)
+void SygusUnifStrategy::staticLearnRedundantOps(
+ std::map<Node, std::vector<Node>>& strategy_lemmas)
{
for (unsigned i = 0; i < d_esym_list.size(); i++)
{
Node em = nce.first;
const Datatype& dt =
static_cast<DatatypeType>(em.getType().toType()).getDatatype();
+ std::vector<Node> lemmas;
for (std::pair<const unsigned, bool>& nc : nce.second)
{
Assert(nc.first < dt.getNumConstructors());
{
Node tst =
datatypes::DatatypesRewriter::mkTester(em, nc.first, dt).negate();
+
if (std::find(lemmas.begin(), lemmas.end(), tst) == lemmas.end())
{
Trace("sygus-unif") << "...can exclude based on : " << tst
}
}
}
+ if (!lemmas.empty())
+ {
+ strategy_lemmas[em] = lemmas;
+ }
}
}
*
* This learns static lemmas for pruning enumerative space based on the
* strategy for the function-to-synthesize of this class, and stores these
- * into lemmas.
+ * into strategy_lemmas.
*
* These may correspond to static symmetry breaking predicates (for example,
* those that exclude ITE from enumerators whose role is enum_io when the
* strategy is ITE_strat).
*/
- void staticLearnRedundantOps(std::vector<Node>& lemmas);
+ void staticLearnRedundantOps(
+ std::map<Node, std::vector<Node>>& strategy_lemmas);
+
/** debug print this strategy on Trace c */
void debugPrint(const char* c);
projects / cvc5.git / commitdiff