Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/enum_stream_substitution.cpp	Lines:	230	345	66.7 %
Date:	2021-08-17	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 "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 <numeric>  // for std::iota
#include <sstream>

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

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