From 80c89d9d221218b35d2eaf7ba69144ecfe9e8abd Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Sat, 29 Sep 2018 08:41:21 -0500 Subject: Stream concrete values for variable agnostic enumerators (#2526) --- src/CMakeLists.txt | 2 + src/Makefile.am | 2 + .../quantifiers/sygus/enum_stream_substitution.cpp | 602 +++++++++++++++++++++ .../quantifiers/sygus/enum_stream_substitution.h | 281 ++++++++++ 4 files changed, 887 insertions(+) create mode 100644 src/theory/quantifiers/sygus/enum_stream_substitution.cpp create mode 100644 src/theory/quantifiers/sygus/enum_stream_substitution.h (limited to 'src') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9948b0ec9..afc8c0f1b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -524,6 +524,8 @@ libcvc4_add_sources( theory/quantifiers/sygus/cegis.h theory/quantifiers/sygus/cegis_unif.cpp theory/quantifiers/sygus/cegis_unif.h + theory/quantifiers/sygus/enum_stream_substitution.cpp + theory/quantifiers/sygus/enum_stream_substitution.h theory/quantifiers/sygus/sygus_eval_unfold.cpp theory/quantifiers/sygus/sygus_eval_unfold.h theory/quantifiers/sygus/sygus_explain.cpp diff --git a/src/Makefile.am b/src/Makefile.am index 77cfccda5..0a32cb645 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -534,6 +534,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/sygus/cegis_unif.h \ theory/quantifiers/sygus/ce_guided_single_inv.cpp \ theory/quantifiers/sygus/ce_guided_single_inv.h \ + theory/quantifiers/sygus/enum_stream_substitution.cpp \ + theory/quantifiers/sygus/enum_stream_substitution.h \ theory/quantifiers/sygus/sygus_pbe.cpp \ theory/quantifiers/sygus/sygus_pbe.h \ theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp \ diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp new file mode 100644 index 000000000..3a879640f --- /dev/null +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -0,0 +1,602 @@ +/********************* */ +/*! \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 // 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 sf_types; + d_tds->getSubfieldTypes(tn, sf_types); + // associate variables with constructors in all subfield types + std::map 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 vars; + std::unordered_set visited; + collectVars(value, vars, visited); + // partition permutation variables + d_curr_ind = 0; + Trace("synth-stream-concrete") << " ..permutting vars :"; + std::unordered_set 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>& 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 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 raw_sub; + d_perm_state_class[i].getLastPerm(raw_sub); + // retrieve variables for substitution domain + const std::vector& 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& 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& EnumStreamPermutation::getVarsClass(unsigned id) const +{ + std::map>::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>::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& vars, + std::unordered_set& 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& 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& EnumStreamPermutation::PermutationState::getVars() + const +{ + return d_vars; +} + +void EnumStreamPermutation::PermutationState::getLastPerm( + std::vector& 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 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>& 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 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 raw_sub; + d_comb_state_class[i].getLastComb(raw_sub); + // retrieve variables for substitution domain + const std::vector& 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& 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& 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& 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(i) <= d_k - 1) + { + d_last_comb[i++] = j++; + } + new_comb = true; + break; + } + } + return new_comb; +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h new file mode 100644 index 000000000..5d3daa538 --- /dev/null +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h @@ -0,0 +1,281 @@ +/********************* */ +/*! \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& 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> d_var_classes; + /** maps variables to subfield types with constructors for + * the that variable, which are themselves associated with the respective + * constructors */ + std::map> 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 d_perm_values; + /** retrieves variables occurring in value */ + void collectVars(Node n, + std::vector& vars, + std::unordered_set& 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& 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& vars); + /** retrieve variables being permuted */ + const std::vector& getVars() const; + + private: + /** variables being permuted */ + std::vector d_vars; + /** last computed permutation of variables */ + std::vector d_last_perm; + /** auxiliary position list for generating permutations */ + std::vector d_seq; + /** current index being permuted */ + unsigned d_curr_ind; + }; + /** permutation state of each variable subclass */ + std::vector 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> d_var_classes; + /** maps variables to subfield types with constructors for + * the that variable, which are themselves associated with the respective + * constructors */ + std::map> 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 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& 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& 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 d_last_comb; + /** variables from which combination is extracted */ + std::vector d_vars; + }; + /** combination state for each variable subclass */ + std::vector d_comb_state_class; + /** current class being combined */ + unsigned d_curr_ind; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif -- cgit v1.2.3