Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/enum_stream_substitution.cpp	Lines:	228	342	66.7 %
Date:	2021-09-10	Branches:	325	1110	29.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Haniel Barbosa, Andrew Reynolds, Gereon Kremer
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * Class for streaming concrete values (through substitutions) from
 * enumerated abstract ones.
 */

#include "theory/quantifiers/sygus/enum_stream_substitution.h"

#include <numeric>  // for std::iota
#include <sstream>

#include "expr/dtype_cons.h"
#include "options/base_options.h"
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/rewriter.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

EnumStreamPermutation::EnumStreamPermutation(TermDbSygus* tds)
    : d_tds(tds), d_first(true), d_curr_ind(0)
{
}

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 = tn.getDType().getSygusVarList();
  NodeManager* nm = NodeManager::currentNM();
  // get subtypes in value's type
  SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
  std::vector<TypeNode> sf_types;
  ti.getSubfieldTypes(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 DType& dt = stn.getDType();
      for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
      {
        if (dt[i].getNumArgs() == 0 && 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> visited;
  collectVars(value, vars, visited);
  // partition permutation variables
  d_curr_ind = 0;
  Trace("synth-stream-concrete") << " ..permutting vars :";
  std::unordered_set<Node> 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[ti.getSubclassForVar(var)].push_back(var);
    }
  }
  for (const std::pair<const 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;
        TermDbSygus::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;
    TermDbSygus::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(Rewriter::callExtendedRewrite(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;
    if (options::sygusSymBreakDynamic())
    {
      bultin_perm_value = Rewriter::callExtendedRewrite(bultin_perm_value);
      Trace("synth-stream-concrete-debug")
          << " and rewrites to " << bultin_perm_value;
    }
    Trace("synth-stream-concrete-debug") << "\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;
    TermDbSygus::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>& 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;
      TermDbSygus::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), d_curr_ind(0)
{
}

void EnumStreamSubstitution::initialize(TypeNode tn)
{
  d_tn = tn;
  // get variables in value's type
  Node var_list = tn.getDType().getSygusVarList();
  // get subtypes in value's type
  NodeManager* nm = NodeManager::currentNM();
  SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
  std::vector<TypeNode> sf_types;
  ti.getSubfieldTypes(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 DType& dt = stn.getDType();
      for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
      {
        if (dt[i].getNumArgs() == 0 && 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(ti.getSubclassForVar(v) > 0);
    d_var_classes[ti.getSubclassForVar(v)].push_back(v);
  }
}

void EnumStreamSubstitution::resetValue(Node value)
{
  if (Trace.isOn("synth-stream-concrete"))
  {
    std::stringstream ss;
    TermDbSygus::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<const 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;
        TermDbSygus::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;
    TermDbSygus::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;
    TermDbSygus::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->sygusToBuiltin(comb_value, comb_value.getType());
  if (options::sygusSymBreakDynamic())
  {
    builtin_comb_value = Rewriter::callExtendedRewrite(builtin_comb_value);
  }
  if (Trace.isOn("synth-stream-concrete"))
  {
    std::stringstream ss;
    TermDbSygus::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)
  {
    if (Trace.isOn("synth-stream-concrete"))
    {
      std::stringstream ss, ss1;
      TermDbSygus::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;
    TermDbSygus::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;
      TermDbSygus::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;
}

void EnumStreamConcrete::initialize(Node e) { d_ess.initialize(e.getType()); }
void EnumStreamConcrete::addValue(Node v)
{
  d_ess.resetValue(v);
  d_currTerm = d_ess.getNext();
}
bool EnumStreamConcrete::increment()
{
  d_currTerm = d_ess.getNext();
  return !d_currTerm.isNull();
}
Node EnumStreamConcrete::getCurrent() { return d_currTerm; }
}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Haniel Barbosa, Andrew Reynolds, Gereon Kremer
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Class for streaming concrete values (through substitutions) from
14		* enumerated abstract ones.
15		*/
16
17		#include "theory/quantifiers/sygus/enum_stream_substitution.h"
18
19		#include <numeric> // for std::iota
20		#include <sstream>
21
22		#include "expr/dtype_cons.h"
23		#include "options/base_options.h"
24		#include "options/datatypes_options.h"
25		#include "options/quantifiers_options.h"
26		#include "printer/printer.h"
27		#include "theory/quantifiers/sygus/term_database_sygus.h"
28		#include "theory/rewriter.h"
29
30		using namespace cvc5::kind;
31
32		namespace cvc5 {
33		namespace theory {
34		namespace quantifiers {
35
36	1	EnumStreamPermutation::EnumStreamPermutation(TermDbSygus* tds)
37	1	: d_tds(tds), d_first(true), d_curr_ind(0)
38		{
39	1	}
40
41	1	void EnumStreamPermutation::reset(Node value)
42		{
43		// clean state
44	1	d_var_classes.clear();
45	1	d_var_tn_cons.clear();
46	1	d_first = true;
47	1	d_perm_state_class.clear();
48	1	d_perm_values.clear();
49	1	d_value = value;
50		// get variables in value's type
51	2	TypeNode tn = value.getType();
52	2	Node var_list = tn.getDType().getSygusVarList();
53	1	NodeManager* nm = NodeManager::currentNM();
54		// get subtypes in value's type
55	1	SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
56	2	std::vector<TypeNode> sf_types;
57	1	ti.getSubfieldTypes(sf_types);
58		// associate variables with constructors in all subfield types
59	2	std::map<Node, Node> cons_var;
60	3	for (const Node& v : var_list)
61		{
62		// collect constructors for variable in all subtypes
63	4	for (const TypeNode& stn : sf_types)
64		{
65	2	const DType& dt = stn.getDType();
66	8	for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
67		{
68	6	if (dt[i].getNumArgs() == 0 && dt[i].getSygusOp() == v)
69		{
70	4	Node cons = nm->mkNode(APPLY_CONSTRUCTOR, dt[i].getConstructor());
71	2	d_var_tn_cons[v][stn] = cons;
72	2	cons_var[cons] = v;
73		}
74		}
75		}
76		}
77		// collect variables occurring in value
78	2	std::vector<Node> vars;
79	2	std::unordered_set<Node> visited;
80	1	collectVars(value, vars, visited);
81		// partition permutation variables
82	1	d_curr_ind = 0;
83	1	Trace("synth-stream-concrete") << " ..permutting vars :";
84	2	std::unordered_set<Node> seen_vars;
85	2	for (const Node& v_cons : vars)
86		{
87	1	Assert(cons_var.find(v_cons) != cons_var.end());
88	2	Node var = cons_var[v_cons];
89	1	if (seen_vars.insert(var).second)
90		{
91		// do not add repeated vars
92	1	d_var_classes[ti.getSubclassForVar(var)].push_back(var);
93		}
94		}
95	2	for (const std::pair<const unsigned, std::vector<Node>>& p : d_var_classes)
96		{
97	1	d_perm_state_class.push_back(PermutationState(p.second));
98	1	if (Trace.isOn("synth-stream-concrete"))
99		{
100		Trace("synth-stream-concrete") << " " << p.first << " -> [";
101		for (const Node& var : p.second)
102		{
103		std::stringstream ss;
104		TermDbSygus::toStreamSygus(ss, var);
105		Trace("synth-stream-concrete") << " " << ss.str();
106		}
107		Trace("synth-stream-concrete") << " ]";
108		}
109		}
110	1	Trace("synth-stream-concrete") << "\n";
111	1	}
112
113	2	Node EnumStreamPermutation::getNext()
114		{
115	2	if (Trace.isOn("synth-stream-concrete"))
116		{
117		std::stringstream ss;
118		TermDbSygus::toStreamSygus(ss, d_value);
119		Trace("synth-stream-concrete")
120		<< " ....streaming next permutation for value : " << ss.str()
121		<< " with " << d_perm_state_class.size() << " permutation classes\n";
122		}
123		// initial value
124	2	if (d_first)
125		{
126	1	d_first = false;
127	2	Node bultin_value = d_tds->sygusToBuiltin(d_value, d_value.getType());
128	1	d_perm_values.insert(Rewriter::callExtendedRewrite(bultin_value));
129	1	return d_value;
130		}
131	1	unsigned n_classes = d_perm_state_class.size();
132	2	Node perm_value, bultin_perm_value;
133		do
134		{
135	1	bool new_perm = false;
136	3	while (!new_perm && d_curr_ind < n_classes)
137		{
138	1	if (d_perm_state_class[d_curr_ind].getNextPermutation())
139		{
140		new_perm = true;
141		Trace("synth-stream-concrete-debug2")
142		<< " ....class " << d_curr_ind << " has new perm\n";
143		d_curr_ind = 0;
144		}
145		else
146		{
147	2	Trace("synth-stream-concrete-debug2")
148	1	<< " ....class " << d_curr_ind << " reset\n";
149	1	d_perm_state_class[d_curr_ind].reset();
150	1	d_curr_ind++;
151		}
152		}
153		// no new permutation
154	1	if (!new_perm)
155		{
156	1	Trace("synth-stream-concrete") << " ....no new perm, return null\n";
157	1	return Node::null();
158		}
159		// building substitution
160		std::vector<Node> domain_sub, range_sub;
161		for (unsigned i = 0, size = d_perm_state_class.size(); i < size; ++i)
162		{
163		Trace("synth-stream-concrete") << " ..perm for class " << i << " is";
164		std::vector<Node> raw_sub;
165		d_perm_state_class[i].getLastPerm(raw_sub);
166		// retrieve variables for substitution domain
167		const std::vector<Node>& domain_sub_class =
168		d_perm_state_class[i].getVars();
169		Assert(domain_sub_class.size() == raw_sub.size());
170		// build proper substitution based on variables types and constructors
171		for (unsigned j = 0, size_j = raw_sub.size(); j < size_j; ++j)
172		{
173		for (std::pair<const TypeNode, Node>& p :
174		d_var_tn_cons[domain_sub_class[j]])
175		{
176		// get constructor of type p.first from variable being permuted
177		domain_sub.push_back(p.second);
178		// get constructor of type p.first from variable to be permuted for
179		range_sub.push_back(d_var_tn_cons[raw_sub[j]][p.first]);
180		Trace("synth-stream-concrete-debug2")
181		<< "\n ....{ adding " << domain_sub.back() << " ["
182		<< domain_sub.back().getType() << "] -> " << range_sub.back()
183		<< " [" << range_sub.back().getType() << "] }";
184		}
185		}
186		Trace("synth-stream-concrete") << "\n";
187		}
188		perm_value = d_value.substitute(domain_sub.begin(),
189		domain_sub.end(),
190		range_sub.begin(),
191		range_sub.end());
192		bultin_perm_value = d_tds->sygusToBuiltin(perm_value, perm_value.getType());
193		Trace("synth-stream-concrete-debug")
194		<< " ......perm builtin is " << bultin_perm_value;
195		if (options::sygusSymBreakDynamic())
196		{
197		bultin_perm_value = Rewriter::callExtendedRewrite(bultin_perm_value);
198		Trace("synth-stream-concrete-debug")
199		<< " and rewrites to " << bultin_perm_value;
200		}
201		Trace("synth-stream-concrete-debug") << "\n";
202		// if permuted value is equivalent modulo rewriting to a previous one, look
203		// for another
204		} while (!d_perm_values.insert(bultin_perm_value).second);
205		if (Trace.isOn("synth-stream-concrete"))
206		{
207		std::stringstream ss;
208		TermDbSygus::toStreamSygus(ss, perm_value);
209		Trace("synth-stream-concrete")
210		<< " ....return new perm " << ss.str() << "\n";
211		}
212		return perm_value;
213		}
214
215	2	const std::vector<Node>& EnumStreamPermutation::getVarsClass(unsigned id) const
216		{
217		std::map<unsigned, std::vector<Node>>::const_iterator it =
218	2	d_var_classes.find(id);
219	2	Assert(it != d_var_classes.end());
220	2	return it->second;
221		}
222
223	1	unsigned EnumStreamPermutation::getVarClassSize(unsigned id) const
224		{
225		std::map<unsigned, std::vector<Node>>::const_iterator it =
226	1	d_var_classes.find(id);
227	1	if (it == d_var_classes.end())
228		{
229		return 0;
230		}
231	1	return it->second.size();
232		}
233
234	1	void EnumStreamPermutation::collectVars(Node n,
235		std::vector<Node>& vars,
236		std::unordered_set<Node>& visited)
237		{
238	1	if (visited.find(n) != visited.end())
239		{
240		return;
241		}
242	1	visited.insert(n);
243	1	if (n.getNumChildren() > 0)
244		{
245		for (const Node& ni : n)
246		{
247		collectVars(ni, vars, visited);
248		}
249		return;
250		}
251	1	if (d_tds->sygusToBuiltin(n, n.getType()).getKind() == kind::BOUND_VARIABLE)
252		{
253	1	if (std::find(vars.begin(), vars.end(), n) == vars.end())
254		{
255	1	vars.push_back(n);
256		}
257	1	return;
258		}
259		}
260
261	1	EnumStreamPermutation::PermutationState::PermutationState(
262	1	const std::vector<Node>& vars)
263		{
264	1	d_vars = vars;
265	1	d_curr_ind = 0;
266	1	d_seq.resize(vars.size());
267	1	std::fill(d_seq.begin(), d_seq.end(), 0);
268		// initialize variable indices
269	1	d_last_perm.resize(vars.size());
270	1	std::iota(d_last_perm.begin(), d_last_perm.end(), 0);
271	1	}
272
273	1	void EnumStreamPermutation::PermutationState::reset()
274		{
275	1	d_curr_ind = 0;
276	1	std::fill(d_seq.begin(), d_seq.end(), 0);
277	1	std::iota(d_last_perm.begin(), d_last_perm.end(), 0);
278	1	}
279
280		const std::vector<Node>& EnumStreamPermutation::PermutationState::getVars()
281		const
282		{
283		return d_vars;
284		}
285
286		void EnumStreamPermutation::PermutationState::getLastPerm(
287		std::vector<Node>& vars)
288		{
289		for (unsigned i = 0, size = d_last_perm.size(); i < size; ++i)
290		{
291		if (Trace.isOn("synth-stream-concrete"))
292		{
293		std::stringstream ss;
294		TermDbSygus::toStreamSygus(ss, d_vars[d_last_perm[i]]);
295		Trace("synth-stream-concrete") << " " << ss.str();
296		}
297		vars.push_back(d_vars[d_last_perm[i]]);
298		}
299		}
300
301	2	bool EnumStreamPermutation::PermutationState::getNextPermutation()
302		{
303		// exhausted permutations
304	2	if (d_curr_ind == d_vars.size())
305		{
306	1	Trace("synth-stream-concrete-debug2") << "exhausted perms, ";
307	1	return false;
308		}
309	1	if (d_seq[d_curr_ind] >= d_curr_ind)
310		{
311	1	d_seq[d_curr_ind] = 0;
312	1	d_curr_ind++;
313	1	return getNextPermutation();
314		}
315		if (d_curr_ind % 2 == 0)
316		{
317		// swap with first element
318		std::swap(d_last_perm[0], d_last_perm[d_curr_ind]);
319		}
320		else
321		{
322		// swap with element in index in sequence of current index
323		std::swap(d_last_perm[d_seq[d_curr_ind]], d_last_perm[d_curr_ind]);
324		}
325		d_seq[d_curr_ind] += 1;
326		d_curr_ind = 0;
327		return true;
328		}
329
330	1	EnumStreamSubstitution::EnumStreamSubstitution(quantifiers::TermDbSygus* tds)
331	1	: d_tds(tds), d_stream_permutations(tds), d_curr_ind(0)
332		{
333	1	}
334
335	1	void EnumStreamSubstitution::initialize(TypeNode tn)
336		{
337	1	d_tn = tn;
338		// get variables in value's type
339	2	Node var_list = tn.getDType().getSygusVarList();
340		// get subtypes in value's type
341	1	NodeManager* nm = NodeManager::currentNM();
342	1	SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
343	2	std::vector<TypeNode> sf_types;
344	1	ti.getSubfieldTypes(sf_types);
345		// associate variables with constructors in all subfield types
346	3	for (const Node& v : var_list)
347		{
348		// collect constructors for variable in all subtypes
349	4	for (const TypeNode& stn : sf_types)
350		{
351	2	const DType& dt = stn.getDType();
352	8	for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
353		{
354	6	if (dt[i].getNumArgs() == 0 && dt[i].getSygusOp() == v)
355		{
356	2	d_var_tn_cons[v][stn] =
357	4	nm->mkNode(APPLY_CONSTRUCTOR, dt[i].getConstructor());
358		}
359		}
360		}
361		}
362		// split initial variables into classes
363	3	for (const Node& v : var_list)
364		{
365	2	Assert(ti.getSubclassForVar(v) > 0);
366	2	d_var_classes[ti.getSubclassForVar(v)].push_back(v);
367		}
368	1	}
369
370	1	void EnumStreamSubstitution::resetValue(Node value)
371		{
372	1	if (Trace.isOn("synth-stream-concrete"))
373		{
374		std::stringstream ss;
375		TermDbSygus::toStreamSygus(ss, value);
376		Trace("synth-stream-concrete")
377		<< " * Streaming concrete: registering value " << ss.str() << "\n";
378		}
379	1	d_last = Node::null();
380	1	d_value = value;
381		// reset permutation util
382	1	d_stream_permutations.reset(value);
383		// reset combination utils
384	1	d_curr_ind = 0;
385	1	d_comb_state_class.clear();
386	1	Trace("synth-stream-concrete") << " ..combining vars :";
387	2	for (const std::pair<const unsigned, std::vector<Node>>& p : d_var_classes)
388		{
389		// ignore classes without variables being permuted
390	1	unsigned perm_var_class_sz = d_stream_permutations.getVarClassSize(p.first);
391	1	if (perm_var_class_sz == 0)
392		{
393		continue;
394		}
395	3	d_comb_state_class.push_back(CombinationState(
396	2	p.second.size(), perm_var_class_sz, p.first, p.second));
397	1	if (Trace.isOn("synth-stream-concrete"))
398		{
399		Trace("synth-stream-concrete")
400		<< " " << p.first << " -> " << perm_var_class_sz << " from [ ";
401		for (const Node& var : p.second)
402		{
403		std::stringstream ss;
404		TermDbSygus::toStreamSygus(ss, var);
405		Trace("synth-stream-concrete") << " " << ss.str();
406		}
407		Trace("synth-stream-concrete") << " ]";
408		}
409		}
410	1	Trace("synth-stream-concrete") << "\n";
411	1	}
412
413	3	Node EnumStreamSubstitution::getNext()
414		{
415	3	if (Trace.isOn("synth-stream-concrete"))
416		{
417		std::stringstream ss;
418		TermDbSygus::toStreamSygus(ss, d_value);
419		Trace("synth-stream-concrete")
420		<< " ..streaming next combination of " << ss.str() << "\n";
421		}
422	3	unsigned n_classes = d_comb_state_class.size();
423		// intial case
424	3	if (d_last.isNull())
425		{
426	1	d_last = d_stream_permutations.getNext();
427		}
428		else
429		{
430	2	bool new_comb = false;
431	6	while (!new_comb && d_curr_ind < n_classes)
432		{
433	2	if (d_comb_state_class[d_curr_ind].getNextCombination())
434		{
435	1	new_comb = true;
436	2	Trace("synth-stream-concrete-debug2")
437	1	<< " ....class " << d_curr_ind << " has new comb\n";
438	1	d_curr_ind = 0;
439		}
440		else
441		{
442	2	Trace("synth-stream-concrete-debug2")
443	1	<< " ....class " << d_curr_ind << " reset\n";
444	1	d_comb_state_class[d_curr_ind].reset();
445	1	d_curr_ind++;
446		}
447		}
448		// no new combination
449	2	if (!new_comb)
450		{
451	2	Trace("synth-stream-concrete")
452		<< " ..no new comb, get next permutation\n ....total combs until "
453	1	"here : "
454	1	<< d_comb_values.size() << "\n";
455	1	d_last = d_stream_permutations.getNext();
456		// exhausted permutations
457	1	if (d_last.isNull())
458		{
459	1	Trace("synth-stream-concrete") << " ..no new comb, return null\n";
460	1	return Node::null();
461		}
462		// reset combination classes for next permutation
463		d_curr_ind = 0;
464		for (unsigned i = 0, size = d_comb_state_class.size(); i < size; ++i)
465		{
466		d_comb_state_class[i].reset();
467		}
468		}
469		}
470	2	if (Trace.isOn("synth-stream-concrete-debug"))
471		{
472		std::stringstream ss;
473		TermDbSygus::toStreamSygus(ss, d_last);
474		Trace("synth-stream-concrete-debug")
475		<< " ..using base perm " << ss.str() << "\n";
476		}
477		// building substitution
478	4	std::vector<Node> domain_sub, range_sub;
479	4	for (unsigned i = 0, size = d_comb_state_class.size(); i < size; ++i)
480		{
481	4	Trace("synth-stream-concrete")
482	4	<< " ..comb for class " << d_comb_state_class[i].getSubclassId()
483	2	<< " is";
484	4	std::vector<Node> raw_sub;
485	2	d_comb_state_class[i].getLastComb(raw_sub);
486		// retrieve variables for substitution domain
487		const std::vector<Node>& domain_sub_class =
488		d_stream_permutations.getVarsClass(
489	2	d_comb_state_class[i].getSubclassId());
490	2	Assert(domain_sub_class.size() == raw_sub.size());
491		// build proper substitution based on variables types and constructors
492	4	for (unsigned j = 0, size_j = raw_sub.size(); j < size_j; ++j)
493		{
494	2	for (std::pair<const TypeNode, Node>& p :
495	2	d_var_tn_cons[domain_sub_class[j]])
496		{
497		// get constructor of type p.first from variable being permuted
498	2	domain_sub.push_back(p.second);
499		// get constructor of type p.first from variable to be permuted for
500	2	range_sub.push_back(d_var_tn_cons[raw_sub[j]][p.first]);
501	4	Trace("synth-stream-concrete-debug2")
502	2	<< "\n ....{ adding " << domain_sub.back() << " ["
503	4	<< domain_sub.back().getType() << "] -> " << range_sub.back()
504	2	<< " [" << range_sub.back().getType() << "] }";
505		}
506		}
507	2	Trace("synth-stream-concrete") << "\n";
508		}
509		Node comb_value = d_last.substitute(
510	4	domain_sub.begin(), domain_sub.end(), range_sub.begin(), range_sub.end());
511		// the new combination value should be fresh, modulo rewriting, by
512		// construction (unless it's equiv to a constant, e.g. true / false)
513		Node builtin_comb_value =
514	4	d_tds->sygusToBuiltin(comb_value, comb_value.getType());
515	2	if (options::sygusSymBreakDynamic())
516		{
517	2	builtin_comb_value = Rewriter::callExtendedRewrite(builtin_comb_value);
518		}
519	2	if (Trace.isOn("synth-stream-concrete"))
520		{
521		std::stringstream ss;
522		TermDbSygus::toStreamSygus(ss, comb_value);
523		Trace("synth-stream-concrete")
524		<< " ....register new comb value " << ss.str()
525		<< " with rewritten form " << builtin_comb_value
526		<< (builtin_comb_value.isConst() ? " (isConst)" : "") << "\n";
527		}
528	4	if (!builtin_comb_value.isConst()
529	2	&& !d_comb_values.insert(builtin_comb_value).second)
530		{
531		if (Trace.isOn("synth-stream-concrete"))
532		{
533		std::stringstream ss, ss1;
534		TermDbSygus::toStreamSygus(ss, comb_value);
535		Trace("synth-stream-concrete")
536		<< " ..term " << ss.str() << " is REDUNDANT with " << builtin_comb_value
537		<< "\n ..excluding all other concretizations (had "
538		<< d_comb_values.size() << " already)\n\n";
539		}
540		return Node::null();
541		}
542	2	if (Trace.isOn("synth-stream-concrete"))
543		{
544		std::stringstream ss;
545		TermDbSygus::toStreamSygus(ss, comb_value);
546		Trace("synth-stream-concrete")
547		<< " ..return new comb " << ss.str() << "\n\n";
548		}
549	2	return comb_value;
550		}
551
552	1	EnumStreamSubstitution::CombinationState::CombinationState(
553	1	unsigned n, unsigned k, unsigned subclass_id, const std::vector<Node>& vars)
554	1	: d_n(n), d_k(k)
555		{
556	1	Assert(!vars.empty());
557	1	Assert(k <= n);
558	1	d_last_comb.resize(k);
559	1	std::iota(d_last_comb.begin(), d_last_comb.end(), 0);
560	1	d_vars = vars;
561	1	d_subclass_id = subclass_id;
562	1	}
563
564	4	const unsigned EnumStreamSubstitution::CombinationState::getSubclassId() const
565		{
566	4	return d_subclass_id;
567		}
568
569	1	void EnumStreamSubstitution::CombinationState::reset()
570		{
571	1	std::iota(d_last_comb.begin(), d_last_comb.end(), 0);
572	1	}
573
574	2	void EnumStreamSubstitution::CombinationState::getLastComb(
575		std::vector<Node>& vars)
576		{
577	4	for (unsigned i = 0, size = d_last_comb.size(); i < size; ++i)
578		{
579	2	if (Trace.isOn("synth-stream-concrete"))
580		{
581		std::stringstream ss;
582		TermDbSygus::toStreamSygus(ss, d_vars[d_last_comb[i]]);
583		Trace("synth-stream-concrete") << " " << ss.str();
584		}
585	2	vars.push_back(d_vars[d_last_comb[i]]);
586		}
587	2	}
588
589	2	bool EnumStreamSubstitution::CombinationState::getNextCombination()
590		{
591		// find what to increment
592	2	bool new_comb = false;
593	3	for (int i = d_k - 1; i >= 0; --i)
594		{
595	2	if (d_last_comb[i] < d_n - d_k + i)
596		{
597	1	unsigned j = d_last_comb[i] + 1;
598	3	while (static_cast<unsigned>(i) <= d_k - 1)
599		{
600	1	d_last_comb[i++] = j++;
601		}
602	1	new_comb = true;
603	1	break;
604		}
605		}
606	2	return new_comb;
607		}
608
609	1	void EnumStreamConcrete::initialize(Node e) { d_ess.initialize(e.getType()); }
610	1	void EnumStreamConcrete::addValue(Node v)
611		{
612	1	d_ess.resetValue(v);
613	1	d_currTerm = d_ess.getNext();
614	1	}
615	2	bool EnumStreamConcrete::increment()
616		{
617	2	d_currTerm = d_ess.getNext();
618	2	return !d_currTerm.isNull();
619		}
620	2	Node EnumStreamConcrete::getCurrent() { return d_currTerm; }
621		} // namespace quantifiers
622		} // namespace theory
623	29502	} // namespace cvc5