--- /dev/null
+/********************* */
+/*! \file enum_stream_substitution.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Haniel Barbosa, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief class for streaming concrete values (through substitutions) from
+ ** enumerated abstract ones
+ **/
+
+#include "theory/quantifiers/sygus/enum_stream_substitution.h"
+
+#include "options/base_options.h"
+#include "options/quantifiers_options.h"
+#include "printer/printer.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+
+#include <numeric> // for std::iota
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+EnumStreamPermutation::EnumStreamPermutation(quantifiers::TermDbSygus* tds)
+ : d_tds(tds)
+{
+}
+
+void EnumStreamPermutation::reset(Node value)
+{
+ // clean state
+ d_var_classes.clear();
+ d_var_tn_cons.clear();
+ d_first = true;
+ d_perm_state_class.clear();
+ d_perm_values.clear();
+ d_value = value;
+ // get variables in value's type
+ TypeNode tn = value.getType();
+ Node var_list = Node::fromExpr(tn.getDatatype().getSygusVarList());
+ NodeManager* nm = NodeManager::currentNM();
+ // get subtypes in value's type
+ std::vector<TypeNode> sf_types;
+ d_tds->getSubfieldTypes(tn, sf_types);
+ // associate variables with constructors in all subfield types
+ std::map<Node, Node> cons_var;
+ for (const Node& v : var_list)
+ {
+ // collect constructors for variable in all subtypes
+ for (const TypeNode& stn : sf_types)
+ {
+ const Datatype& dt = stn.getDatatype();
+ for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
+ {
+ if (dt[i].getNumArgs() == 0 && Node::fromExpr(dt[i].getSygusOp()) == v)
+ {
+ Node cons = nm->mkNode(APPLY_CONSTRUCTOR, dt[i].getConstructor());
+ d_var_tn_cons[v][stn] = cons;
+ cons_var[cons] = v;
+ }
+ }
+ }
+ }
+ // collect variables occurring in value
+ std::vector<Node> vars;
+ std::unordered_set<Node, NodeHashFunction> visited;
+ collectVars(value, vars, visited);
+ // partition permutation variables
+ d_curr_ind = 0;
+ Trace("synth-stream-concrete") << " ..permutting vars :";
+ std::unordered_set<Node, NodeHashFunction> seen_vars;
+ for (const Node& v_cons : vars)
+ {
+ Assert(cons_var.find(v_cons) != cons_var.end());
+ Node var = cons_var[v_cons];
+ if (seen_vars.insert(var).second)
+ {
+ // do not add repeated vars
+ d_var_classes[d_tds->getSubclassForVar(tn, var)].push_back(var);
+ }
+ }
+ for (const std::pair<unsigned, std::vector<Node>>& p : d_var_classes)
+ {
+ d_perm_state_class.push_back(PermutationState(p.second));
+ if (Trace.isOn("synth-stream-concrete"))
+ {
+ Trace("synth-stream-concrete") << " " << p.first << " -> [";
+ for (const Node& var : p.second)
+ {
+ std::stringstream ss;
+ Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, var);
+ Trace("synth-stream-concrete") << " " << ss.str();
+ }
+ Trace("synth-stream-concrete") << " ]";
+ }
+ }
+ Trace("synth-stream-concrete") << "\n";
+}
+
+Node EnumStreamPermutation::getNext()
+{
+ if (Trace.isOn("synth-stream-concrete"))
+ {
+ std::stringstream ss;
+ Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_value);
+ Trace("synth-stream-concrete")
+ << " ....streaming next permutation for value : " << ss.str()
+ << " with " << d_perm_state_class.size() << " permutation classes\n";
+ }
+ // initial value
+ if (d_first)
+ {
+ d_first = false;
+ Node bultin_value = d_tds->sygusToBuiltin(d_value, d_value.getType());
+ d_perm_values.insert(
+ d_tds->getExtRewriter()->extendedRewrite(bultin_value));
+ return d_value;
+ }
+ unsigned n_classes = d_perm_state_class.size();
+ Node perm_value, bultin_perm_value;
+ do
+ {
+ bool new_perm = false;
+ while (!new_perm && d_curr_ind < n_classes)
+ {
+ if (d_perm_state_class[d_curr_ind].getNextPermutation())
+ {
+ new_perm = true;
+ Trace("synth-stream-concrete-debug2")
+ << " ....class " << d_curr_ind << " has new perm\n";
+ d_curr_ind = 0;
+ }
+ else
+ {
+ Trace("synth-stream-concrete-debug2")
+ << " ....class " << d_curr_ind << " reset\n";
+ d_perm_state_class[d_curr_ind].reset();
+ d_curr_ind++;
+ }
+ }
+ // no new permutation
+ if (!new_perm)
+ {
+ Trace("synth-stream-concrete") << " ....no new perm, return null\n";
+ return Node::null();
+ }
+ // building substitution
+ std::vector<Node> domain_sub, range_sub;
+ for (unsigned i = 0, size = d_perm_state_class.size(); i < size; ++i)
+ {
+ Trace("synth-stream-concrete") << " ..perm for class " << i << " is";
+ std::vector<Node> raw_sub;
+ d_perm_state_class[i].getLastPerm(raw_sub);
+ // retrieve variables for substitution domain
+ const std::vector<Node>& domain_sub_class =
+ d_perm_state_class[i].getVars();
+ Assert(domain_sub_class.size() == raw_sub.size());
+ // build proper substitution based on variables types and constructors
+ for (unsigned j = 0, size_j = raw_sub.size(); j < size_j; ++j)
+ {
+ for (std::pair<const TypeNode, Node>& p :
+ d_var_tn_cons[domain_sub_class[j]])
+ {
+ // get constructor of type p.first from variable being permuted
+ domain_sub.push_back(p.second);
+ // get constructor of type p.first from variable to be permuted for
+ range_sub.push_back(d_var_tn_cons[raw_sub[j]][p.first]);
+ Trace("synth-stream-concrete-debug2")
+ << "\n ....{ adding " << domain_sub.back() << " ["
+ << domain_sub.back().getType() << "] -> " << range_sub.back()
+ << " [" << range_sub.back().getType() << "] }";
+ }
+ }
+ Trace("synth-stream-concrete") << "\n";
+ }
+ perm_value = d_value.substitute(domain_sub.begin(),
+ domain_sub.end(),
+ range_sub.begin(),
+ range_sub.end());
+ bultin_perm_value = d_tds->sygusToBuiltin(perm_value, perm_value.getType());
+ Trace("synth-stream-concrete-debug")
+ << " ......perm builtin is " << bultin_perm_value;
+ bultin_perm_value =
+ d_tds->getExtRewriter()->extendedRewrite(bultin_perm_value);
+ Trace("synth-stream-concrete-debug")
+ << " and rewrites to " << bultin_perm_value << "\n";
+ // if permuted value is equivalent modulo rewriting to a previous one, look
+ // for another
+ } while (!d_perm_values.insert(bultin_perm_value).second);
+ if (Trace.isOn("synth-stream-concrete"))
+ {
+ std::stringstream ss;
+ Printer::getPrinter(options::outputLanguage())
+ ->toStreamSygus(ss, perm_value);
+ Trace("synth-stream-concrete")
+ << " ....return new perm " << ss.str() << "\n";
+ }
+ return perm_value;
+}
+
+const std::vector<Node>& EnumStreamPermutation::getVarsClass(unsigned id) const
+{
+ std::map<unsigned, std::vector<Node>>::const_iterator it =
+ d_var_classes.find(id);
+ Assert(it != d_var_classes.end());
+ return it->second;
+}
+
+unsigned EnumStreamPermutation::getVarClassSize(unsigned id) const
+{
+ std::map<unsigned, std::vector<Node>>::const_iterator it =
+ d_var_classes.find(id);
+ if (it == d_var_classes.end())
+ {
+ return 0;
+ }
+ return it->second.size();
+}
+
+void EnumStreamPermutation::collectVars(
+ Node n,
+ std::vector<Node>& vars,
+ std::unordered_set<Node, NodeHashFunction>& visited)
+{
+ if (visited.find(n) != visited.end())
+ {
+ return;
+ }
+ visited.insert(n);
+ if (n.getNumChildren() > 0)
+ {
+ for (const Node& ni : n)
+ {
+ collectVars(ni, vars, visited);
+ }
+ return;
+ }
+ if (d_tds->sygusToBuiltin(n, n.getType()).getKind() == kind::BOUND_VARIABLE)
+ {
+ if (std::find(vars.begin(), vars.end(), n) == vars.end())
+ {
+ vars.push_back(n);
+ }
+ return;
+ }
+}
+
+EnumStreamPermutation::PermutationState::PermutationState(
+ const std::vector<Node>& vars)
+{
+ d_vars = vars;
+ d_curr_ind = 0;
+ d_seq.resize(vars.size());
+ std::fill(d_seq.begin(), d_seq.end(), 0);
+ // initialize variable indices
+ d_last_perm.resize(vars.size());
+ std::iota(d_last_perm.begin(), d_last_perm.end(), 0);
+}
+
+void EnumStreamPermutation::PermutationState::reset()
+{
+ d_curr_ind = 0;
+ std::fill(d_seq.begin(), d_seq.end(), 0);
+ std::iota(d_last_perm.begin(), d_last_perm.end(), 0);
+}
+
+const std::vector<Node>& EnumStreamPermutation::PermutationState::getVars()
+ const
+{
+ return d_vars;
+}
+
+void EnumStreamPermutation::PermutationState::getLastPerm(
+ std::vector<Node>& vars)
+{
+ for (unsigned i = 0, size = d_last_perm.size(); i < size; ++i)
+ {
+ if (Trace.isOn("synth-stream-concrete"))
+ {
+ std::stringstream ss;
+ Printer::getPrinter(options::outputLanguage())
+ ->toStreamSygus(ss, d_vars[d_last_perm[i]]);
+ Trace("synth-stream-concrete") << " " << ss.str();
+ }
+ vars.push_back(d_vars[d_last_perm[i]]);
+ }
+}
+
+bool EnumStreamPermutation::PermutationState::getNextPermutation()
+{
+ // exhausted permutations
+ if (d_curr_ind == d_vars.size())
+ {
+ Trace("synth-stream-concrete-debug2") << "exhausted perms, ";
+ return false;
+ }
+ if (d_seq[d_curr_ind] >= d_curr_ind)
+ {
+ d_seq[d_curr_ind] = 0;
+ d_curr_ind++;
+ return getNextPermutation();
+ }
+ if (d_curr_ind % 2 == 0)
+ {
+ // swap with first element
+ std::swap(d_last_perm[0], d_last_perm[d_curr_ind]);
+ }
+ else
+ {
+ // swap with element in index in sequence of current index
+ std::swap(d_last_perm[d_seq[d_curr_ind]], d_last_perm[d_curr_ind]);
+ }
+ d_seq[d_curr_ind] += 1;
+ d_curr_ind = 0;
+ return true;
+}
+
+EnumStreamSubstitution::EnumStreamSubstitution(quantifiers::TermDbSygus* tds)
+ : d_tds(tds), d_stream_permutations(tds)
+{
+}
+
+void EnumStreamSubstitution::initialize(TypeNode tn)
+{
+ d_tn = tn;
+ // get variables in value's type
+ Node var_list = Node::fromExpr(tn.getDatatype().getSygusVarList());
+ // get subtypes in value's type
+ NodeManager* nm = NodeManager::currentNM();
+ std::vector<TypeNode> sf_types;
+ d_tds->getSubfieldTypes(tn, sf_types);
+ // associate variables with constructors in all subfield types
+ for (const Node& v : var_list)
+ {
+ // collect constructors for variable in all subtypes
+ for (const TypeNode& stn : sf_types)
+ {
+ const Datatype& dt = stn.getDatatype();
+ for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
+ {
+ if (dt[i].getNumArgs() == 0 && Node::fromExpr(dt[i].getSygusOp()) == v)
+ {
+ d_var_tn_cons[v][stn] =
+ nm->mkNode(APPLY_CONSTRUCTOR, dt[i].getConstructor());
+ }
+ }
+ }
+ }
+ // split initial variables into classes
+ for (const Node& v : var_list)
+ {
+ Assert(d_tds->getSubclassForVar(tn, v) > 0);
+ d_var_classes[d_tds->getSubclassForVar(tn, v)].push_back(v);
+ }
+}
+
+void EnumStreamSubstitution::resetValue(Node value)
+{
+ if (Trace.isOn("synth-stream-concrete"))
+ {
+ std::stringstream ss;
+ Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, value);
+ Trace("synth-stream-concrete")
+ << " * Streaming concrete: registering value " << ss.str() << "\n";
+ }
+ d_last = Node::null();
+ d_value = value;
+ // reset permutation util
+ d_stream_permutations.reset(value);
+ // reset combination utils
+ d_curr_ind = 0;
+ d_comb_state_class.clear();
+ Trace("synth-stream-concrete") << " ..combining vars :";
+ for (const std::pair<unsigned, std::vector<Node>>& p : d_var_classes)
+ {
+ // ignore classes without variables being permuted
+ unsigned perm_var_class_sz = d_stream_permutations.getVarClassSize(p.first);
+ if (perm_var_class_sz == 0)
+ {
+ continue;
+ }
+ d_comb_state_class.push_back(CombinationState(
+ p.second.size(), perm_var_class_sz, p.first, p.second));
+ if (Trace.isOn("synth-stream-concrete"))
+ {
+ Trace("synth-stream-concrete")
+ << " " << p.first << " -> " << perm_var_class_sz << " from [ ";
+ for (const Node& var : p.second)
+ {
+ std::stringstream ss;
+ Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, var);
+ Trace("synth-stream-concrete") << " " << ss.str();
+ }
+ Trace("synth-stream-concrete") << " ]";
+ }
+ }
+ Trace("synth-stream-concrete") << "\n";
+}
+
+Node EnumStreamSubstitution::getNext()
+{
+ if (Trace.isOn("synth-stream-concrete"))
+ {
+ std::stringstream ss;
+ Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_value);
+ Trace("synth-stream-concrete")
+ << " ..streaming next combination of " << ss.str() << "\n";
+ }
+ unsigned n_classes = d_comb_state_class.size();
+ // intial case
+ if (d_last.isNull())
+ {
+ d_last = d_stream_permutations.getNext();
+ }
+ else
+ {
+ bool new_comb = false;
+ while (!new_comb && d_curr_ind < n_classes)
+ {
+ if (d_comb_state_class[d_curr_ind].getNextCombination())
+ {
+ new_comb = true;
+ Trace("synth-stream-concrete-debug2")
+ << " ....class " << d_curr_ind << " has new comb\n";
+ d_curr_ind = 0;
+ }
+ else
+ {
+ Trace("synth-stream-concrete-debug2")
+ << " ....class " << d_curr_ind << " reset\n";
+ d_comb_state_class[d_curr_ind].reset();
+ d_curr_ind++;
+ }
+ }
+ // no new combination
+ if (!new_comb)
+ {
+ Trace("synth-stream-concrete")
+ << " ..no new comb, get next permutation\n ....total combs until "
+ "here : "
+ << d_comb_values.size() << "\n";
+ d_last = d_stream_permutations.getNext();
+ // exhausted permutations
+ if (d_last.isNull())
+ {
+ Trace("synth-stream-concrete") << " ..no new comb, return null\n";
+ return Node::null();
+ }
+ // reset combination classes for next permutation
+ d_curr_ind = 0;
+ for (unsigned i = 0, size = d_comb_state_class.size(); i < size; ++i)
+ {
+ d_comb_state_class[i].reset();
+ }
+ }
+ }
+ if (Trace.isOn("synth-stream-concrete-debug"))
+ {
+ std::stringstream ss;
+ Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, d_last);
+ Trace("synth-stream-concrete-debug")
+ << " ..using base perm " << ss.str() << "\n";
+ }
+ // building substitution
+ std::vector<Node> domain_sub, range_sub;
+ for (unsigned i = 0, size = d_comb_state_class.size(); i < size; ++i)
+ {
+ Trace("synth-stream-concrete")
+ << " ..comb for class " << d_comb_state_class[i].getSubclassId()
+ << " is";
+ std::vector<Node> raw_sub;
+ d_comb_state_class[i].getLastComb(raw_sub);
+ // retrieve variables for substitution domain
+ const std::vector<Node>& domain_sub_class =
+ d_stream_permutations.getVarsClass(
+ d_comb_state_class[i].getSubclassId());
+ Assert(domain_sub_class.size() == raw_sub.size());
+ // build proper substitution based on variables types and constructors
+ for (unsigned j = 0, size_j = raw_sub.size(); j < size_j; ++j)
+ {
+ for (std::pair<const TypeNode, Node>& p :
+ d_var_tn_cons[domain_sub_class[j]])
+ {
+ // get constructor of type p.first from variable being permuted
+ domain_sub.push_back(p.second);
+ // get constructor of type p.first from variable to be permuted for
+ range_sub.push_back(d_var_tn_cons[raw_sub[j]][p.first]);
+ Trace("synth-stream-concrete-debug2")
+ << "\n ....{ adding " << domain_sub.back() << " ["
+ << domain_sub.back().getType() << "] -> " << range_sub.back()
+ << " [" << range_sub.back().getType() << "] }";
+ }
+ }
+ Trace("synth-stream-concrete") << "\n";
+ }
+ Node comb_value = d_last.substitute(
+ domain_sub.begin(), domain_sub.end(), range_sub.begin(), range_sub.end());
+ // the new combination value should be fresh, modulo rewriting, by
+ // construction (unless it's equiv to a constant, e.g. true / false)
+ Node builtin_comb_value = d_tds->getExtRewriter()->extendedRewrite(
+ d_tds->sygusToBuiltin(comb_value, comb_value.getType()));
+ if (Trace.isOn("synth-stream-concrete"))
+ {
+ std::stringstream ss;
+ Printer::getPrinter(options::outputLanguage())
+ ->toStreamSygus(ss, comb_value);
+ Trace("synth-stream-concrete")
+ << " ....register new comb value " << ss.str()
+ << " with rewritten form " << builtin_comb_value
+ << (builtin_comb_value.isConst() ? " (isConst)" : "") << "\n";
+ }
+ if (!builtin_comb_value.isConst()
+ && !d_comb_values.insert(builtin_comb_value).second)
+ {
+ std::stringstream ss, ss1;
+ Printer::getPrinter(options::outputLanguage())
+ ->toStreamSygus(ss, comb_value);
+ Trace("synth-stream-concrete")
+ << " ..term " << ss.str() << " is REDUNDANT with " << builtin_comb_value
+ << "\n ..excluding all other concretizations (had "
+ << d_comb_values.size() << " already)\n\n";
+ return Node::null();
+ }
+ if (Trace.isOn("synth-stream-concrete"))
+ {
+ std::stringstream ss;
+ Printer::getPrinter(options::outputLanguage())
+ ->toStreamSygus(ss, comb_value);
+ Trace("synth-stream-concrete")
+ << " ..return new comb " << ss.str() << "\n\n";
+ }
+ return comb_value;
+}
+
+EnumStreamSubstitution::CombinationState::CombinationState(
+ unsigned n, unsigned k, unsigned subclass_id, const std::vector<Node>& vars)
+ : d_n(n), d_k(k)
+{
+ Assert(!vars.empty());
+ Assert(k <= n);
+ d_last_comb.resize(k);
+ std::iota(d_last_comb.begin(), d_last_comb.end(), 0);
+ d_vars = vars;
+ d_subclass_id = subclass_id;
+}
+
+const unsigned EnumStreamSubstitution::CombinationState::getSubclassId() const
+{
+ return d_subclass_id;
+}
+
+void EnumStreamSubstitution::CombinationState::reset()
+{
+ std::iota(d_last_comb.begin(), d_last_comb.end(), 0);
+}
+
+void EnumStreamSubstitution::CombinationState::getLastComb(
+ std::vector<Node>& vars)
+{
+ for (unsigned i = 0, size = d_last_comb.size(); i < size; ++i)
+ {
+ if (Trace.isOn("synth-stream-concrete"))
+ {
+ std::stringstream ss;
+ Printer::getPrinter(options::outputLanguage())
+ ->toStreamSygus(ss, d_vars[d_last_comb[i]]);
+ Trace("synth-stream-concrete") << " " << ss.str();
+ }
+ vars.push_back(d_vars[d_last_comb[i]]);
+ }
+}
+
+bool EnumStreamSubstitution::CombinationState::getNextCombination()
+{
+ // find what to increment
+ bool new_comb = false;
+ for (int i = d_k - 1; i >= 0; --i)
+ {
+ if (d_last_comb[i] < d_n - d_k + i)
+ {
+ unsigned j = d_last_comb[i] + 1;
+ while (static_cast<unsigned>(i) <= d_k - 1)
+ {
+ d_last_comb[i++] = j++;
+ }
+ new_comb = true;
+ break;
+ }
+ }
+ return new_comb;
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file enum_stream_substitution.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Haniel Barbosa, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief class for streaming concrete values (through substitutions) from
+ ** enumerated abstract ones
+ **/
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
+#define __CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
+
+#include "expr/node.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** Streamer of different values according to variable permutations
+ *
+ * Generates a new value (modulo rewriting) when queried in which its variables
+ * are permuted (see EnumStreamSubstitution for more details).
+ */
+class EnumStreamPermutation
+{
+ public:
+ EnumStreamPermutation(quantifiers::TermDbSygus* tds);
+ ~EnumStreamPermutation() {}
+ /** resets utility
+ *
+ * for each subset of the variables in value (according to their
+ * subclasses_classes), a permutation utility is initialized
+ */
+ void reset(Node value);
+ /** computes next permutation, if any, of value
+ *
+ * a "next" permutation is determined by having at least one new permutation
+ * in one of the variable subclasses in the value.
+ *
+ * For example, if the variables of value (OP x1 x2 x3 x4) are partioned into
+ * {{x1, x4}, {x2, x3}} then the sequence of getNext() is
+ *
+ * (OP x4 x2 x3 x1)
+ * (OP x1 x3 x2 x4)
+ * (OP x4 x3 x2 x1)
+ *
+ * Moreover, new values are only considered if they are unique modulo
+ * rewriting. If for example OP were "+", then no next value would exist,
+ * while if OP were "-" the only next value would be: (- x4 x2 x3 x1)
+ *
+ * Since the same variable can occur in different subfield types (and
+ * therefore their datatype equivalents would have different types) a map from
+ * variables to sets of constructors (see var_cons) is used to build
+ * substitutions in a proper way when generating different combinations.
+ */
+ Node getNext();
+ /** retrieve variables in class with given id */
+ const std::vector<Node>& getVarsClass(unsigned id) const;
+ /** retrieve number of variables being permuted from subclass with given id */
+ unsigned getVarClassSize(unsigned id) const;
+
+ private:
+ /** sygus term database of current quantifiers engine */
+ quantifiers::TermDbSygus* d_tds;
+ /** maps subclass ids to subset of d_vars with that subclass id */
+ std::map<unsigned, std::vector<Node>> d_var_classes;
+ /** maps variables to subfield types with constructors for
+ * the that variable, which are themselves associated with the respective
+ * constructors */
+ std::map<Node, std::map<TypeNode, Node>> d_var_tn_cons;
+ /** whether first query */
+ bool d_first;
+ /** value to which we are generating permutations */
+ Node d_value;
+ /** generated permutations (modulo rewriting) */
+ std::unordered_set<Node, NodeHashFunction> d_perm_values;
+ /** retrieves variables occurring in value */
+ void collectVars(Node n,
+ std::vector<Node>& vars,
+ std::unordered_set<Node, NodeHashFunction>& visited);
+ /** Utility for stepwise application of Heap's algorithm for permutation
+ *
+ * see https://en.wikipedia.org/wiki/Heap%27s_algorithm
+ */
+ class PermutationState
+ {
+ public:
+ PermutationState(const std::vector<Node>& vars);
+ /** computes next permutation, i.e. execute one step of Heap's algorithm
+ *
+ * returns true if one exists, false otherwise
+ *
+ * when a new permutation is generated the the new variable arrangement is
+ * stored in d_last_perm (in terms of d_vars' indices)
+ */
+ bool getNextPermutation();
+ /** resets permutation state to initial variable ordering */
+ void reset();
+ /** retrieves last variable permutation
+ *
+ * vars is populated with the new variable arrangement
+ */
+ void getLastPerm(std::vector<Node>& vars);
+ /** retrieve variables being permuted */
+ const std::vector<Node>& getVars() const;
+
+ private:
+ /** variables being permuted */
+ std::vector<Node> d_vars;
+ /** last computed permutation of variables */
+ std::vector<unsigned> d_last_perm;
+ /** auxiliary position list for generating permutations */
+ std::vector<unsigned> d_seq;
+ /** current index being permuted */
+ unsigned d_curr_ind;
+ };
+ /** permutation state of each variable subclass */
+ std::vector<PermutationState> d_perm_state_class;
+ /** current variable subclass being permuted */
+ unsigned d_curr_ind;
+};
+
+/** Streamer of concrete values for enumerator
+ *
+ * When a given enumerator is "variable agnostic", only values in which
+ * variables are ordered are chosen for it (see
+ * TermDbSygus::registerEnumerator). If such values are seen as "abstract", in
+ * the sense that each represent a set of values, this class can be used to
+ * stream all the concrete values that correspond to them.
+ *
+ * For example a variable agnostic enumerator that contains three variables, x1,
+ * x2, x3, in which x1 < x2 < x3, for which an "abstract" value (OP x1 x2) is
+ * derived, will lead to the stream of "concrete" values
+ *
+ * (OP x1 x2)
+ * (OP x1 x3)
+ * (OP x2 x3)
+ *
+ * (OP x2 x1)
+ * (OP x3 x1)
+ * (OP x3 x2)
+ *
+ * in which for each permutation of the variables in the abstract value ([x1,
+ * x2] and [x2, x1] in the above) we generate all the substitutions through
+ * ordered combinations of the variables of the enumerator ([x1, x2], [x1, x3],
+ * and [x2, x3] in the above).
+ *
+ * Moreover the permutations are generated modulo rewriting, s.t. if two
+ * permutations are equivalent, only one is used.
+ *
+ * It should be noted that the variables of a variable agnostic enumerator are
+ * kept in independent "subclasses" (see TermDbSygus::getSubclassForVar).
+ * Therefore when streaming concrete values, permutations and combinations are
+ * generated by the product of the permutations and combinations of each class.
+ */
+class EnumStreamSubstitution
+{
+ public:
+ EnumStreamSubstitution(quantifiers::TermDbSygus* tds);
+ ~EnumStreamSubstitution() {}
+ /** initializes utility
+ *
+ * the combinations are generated from a initial set of variables (for now all
+ * variables in given type).
+ */
+ void initialize(TypeNode tn);
+ /** resets value for which substitutions will be generated through
+ * combinations
+ *
+ * For each variable subclass in this utility, a subset is chosen with as
+ * many variables as in the same variable subclass of value's variables.
+ *
+ * The combinations are performed modulo subclasses. For each subclass of the
+ * given variables, a combination utility is initialized.
+ *
+ * For example, if the initial variable set is partioned into
+ *
+ * {1 -> {x1, x4}, 2 -> {x2, x3, x6}, 3 -> {x5}}
+ *
+ * and value's variables into
+ *
+ * {1 -> {x1, x4}, 2 -> {x2}, 3 -> {}}
+ *
+ * then the combination utilities are initialized such that for class 1 all
+ * ordered subsets with two variables are chosen; for class 2 all ordered
+ * subsets with one variable; and for class 3 no combination can be chosen.
+ */
+ void resetValue(Node value);
+ /** computes next combination, if any, of value
+ *
+ * a "next" combination is determined by having at least one new combination
+ * in one of the variable subclasses in the initial set of variables. If no
+ * new combination exists, the cycle restarts with a new base value generated
+ * by EnumStreamPermutation::getNext() (see above).
+ *
+ * This layered approach (of deriving all combinations for each permutation)
+ * allows to consider only ordered combinations to generate all possible
+ * variations of the base value. See the example in EnumStreamSubstitution for
+ * further details.
+ */
+ Node getNext();
+
+ private:
+ /** sygus term database of current quantifiers engine */
+ quantifiers::TermDbSygus* d_tds;
+ /** type this utility has been initialized for */
+ TypeNode d_tn;
+ /** current value */
+ Node d_value;
+ /** maps subclass ids to d_tn's variables with that subclass id */
+ std::map<unsigned, std::vector<Node>> d_var_classes;
+ /** maps variables to subfield types with constructors for
+ * the that variable, which are themselves associated with the respective
+ * constructors */
+ std::map<Node, std::map<TypeNode, Node>> d_var_tn_cons;
+ /** last value generated after a combination
+ *
+ * If getNext() has been called, this is the return value of the most recent
+ * call to getNext(). Otherwise, this value is null.
+ */
+ Node d_last;
+ /** generated combinations */
+ std::unordered_set<Node, NodeHashFunction> d_comb_values;
+ /** permutation utility */
+ EnumStreamPermutation d_stream_permutations;
+ /** Utility for stepwise generation of ordered subsets of size k from n
+ * variables */
+ class CombinationState
+ {
+ public:
+ CombinationState(unsigned n,
+ unsigned k,
+ unsigned subclass_id,
+ const std::vector<Node>& vars);
+ /** computes next combination
+ *
+ * returns true if one exists, false otherwise
+ */
+ bool getNextCombination();
+ /** resets combination state to first k variables in vars */
+ void reset();
+ /** retrieves last variable combination
+ *
+ * variables in new combination are stored in argument vars
+ */
+ void getLastComb(std::vector<Node>& vars);
+ /** retrieve subclass id */
+ const unsigned getSubclassId() const;
+
+ private:
+ /** subclass id of variables being combined */
+ unsigned d_subclass_id;
+ /** number of variables */
+ unsigned d_n;
+ /** size of subset */
+ unsigned d_k;
+ /** last combination state */
+ std::vector<unsigned> d_last_comb;
+ /** variables from which combination is extracted */
+ std::vector<Node> d_vars;
+ };
+ /** combination state for each variable subclass */
+ std::vector<CombinationState> d_comb_state_class;
+ /** current class being combined */
+ unsigned d_curr_ind;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
+
+#endif
projects / cvc5.git / commitdiff