Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/datatypes/sygus_datatype_utils.cpp	Lines:	246	287	85.7 %
Date:	2021-11-07	Branches:	495	1274	38.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, Aina Niemetz
 *
 * 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.
 * ****************************************************************************
 *
 * Implementation of rewriter for the theory of (co)inductive datatypes.
 */

#include "theory/datatypes/sygus_datatype_utils.h"

#include <sstream>

#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "expr/node_algorithm.h"
#include "expr/sygus_datatype.h"
#include "smt/env.h"
#include "theory/evaluator.h"
#include "theory/rewriter.h"

using namespace cvc5;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace datatypes {
namespace utils {

Node applySygusArgs(const DType& dt,
                    Node op,
                    Node n,
                    const std::vector<Node>& args)
{
  // optimization: if n is just a sygus bound variable, return immediately
  // by replacing with the proper argument, or returning unchanged if it is
  // a bound variable not corresponding to a formal argument.
  if (n.getKind() == BOUND_VARIABLE)
  {
    if (n.hasAttribute(SygusVarNumAttribute()))
    {
      int vn = n.getAttribute(SygusVarNumAttribute());
      Assert(dt.getSygusVarList()[vn] == n);
      return args[vn];
    }
    // it is a different bound variable, it is unchanged
    return n;
  }
  // n is an application of operator op.
  // We must compute the free variables in op to determine if there are
  // any substitutions we need to make to n.
  TNode val;
  if (!op.hasAttribute(SygusVarFreeAttribute()))
  {
    std::unordered_set<Node> fvs;
    if (expr::getFreeVariables(op, fvs))
    {
      if (fvs.size() == 1)
      {
        for (const Node& v : fvs)
        {
          val = v;
        }
      }
      else
      {
        val = op;
      }
    }
    Trace("dt-sygus-fv") << "Free var in " << op << " : " << val << std::endl;
    op.setAttribute(SygusVarFreeAttribute(), val);
  }
  else
  {
    val = op.getAttribute(SygusVarFreeAttribute());
  }
  if (val.isNull())
  {
    return n;
  }
  if (val.getKind() == BOUND_VARIABLE)
  {
    // single substitution case
    int vn = val.getAttribute(SygusVarNumAttribute());
    TNode sub = args[vn];
    return n.substitute(val, sub);
  }
  // do the full substitution
  std::vector<Node> vars;
  Node bvl = dt.getSygusVarList();
  for (unsigned i = 0, nvars = bvl.getNumChildren(); i < nvars; i++)
  {
    vars.push_back(bvl[i]);
  }
  return n.substitute(vars.begin(), vars.end(), args.begin(), args.end());
}

Kind getOperatorKindForSygusBuiltin(Node op)
{
  Assert(op.getKind() != BUILTIN);
  if (op.getKind() == LAMBDA)
  {
    return APPLY_UF;
  }
  return NodeManager::getKindForFunction(op);
}

Kind getEliminateKind(Kind ok)
{
  Kind nk = ok;
  // We also must ensure that builtin operators which are eliminated
  // during expand definitions are replaced by the proper operator.
  if (ok == DIVISION)
  {
    nk = DIVISION_TOTAL;
  }
  else if (ok == INTS_DIVISION)
  {
    nk = INTS_DIVISION_TOTAL;
  }
  else if (ok == INTS_MODULUS)
  {
    nk = INTS_MODULUS_TOTAL;
  }
  return nk;
}

Node mkSygusTerm(const DType& dt,
                 unsigned i,
                 const std::vector<Node>& children,
                 bool doBetaReduction,
                 bool isExternal)
{
  Trace("dt-sygus-util") << "Make sygus term " << dt.getName() << "[" << i
                         << "] with children: " << children << std::endl;
  Assert(i < dt.getNumConstructors());
  Assert(dt.isSygus());
  Assert(!dt[i].getSygusOp().isNull());
  Node op = dt[i].getSygusOp();
  Node opn = op;
  if (!isExternal)
  {
    // Get the normalized version of the sygus operator. We do this by
    // expanding definitions, rewriting it, and eliminating partial operators.
    if (op.isConst())
    {
      // If it is a builtin operator, convert to total version if necessary.
      // First, get the kind for the operator.
      Kind ok = NodeManager::operatorToKind(op);
      Trace("sygus-grammar-normalize-debug")
          << "...builtin kind is " << ok << std::endl;
      Kind nk = getEliminateKind(ok);
      if (nk != ok)
      {
        Trace("sygus-grammar-normalize-debug")
            << "...replace by builtin operator " << nk << std::endl;
        opn = NodeManager::currentNM()->operatorOf(nk);
      }
    }
    else
    {
      // Get the expanded definition form, if it has been marked. This ensures
      // that user-defined functions have been eliminated from op.
      opn = getExpandedDefinitionForm(op);
    }
  }
  return mkSygusTerm(opn, children, doBetaReduction);
}

Node mkSygusTerm(Node op,
                 const std::vector<Node>& children,
                 bool doBetaReduction)
{
  Trace("dt-sygus-util") << "Operator is " << op << std::endl;
  if (children.empty())
  {
    // no children, return immediately
    Trace("dt-sygus-util") << "...return direct op" << std::endl;
    return op;
  }
  // if it is the any constant, we simply return the child
  if (op.getAttribute(SygusAnyConstAttribute()))
  {
    Assert(children.size() == 1);
    return children[0];
  }
  std::vector<Node> schildren;
  // get the kind of the operator
  Kind ok = op.getKind();
  if (ok != BUILTIN)
  {
    if (ok == LAMBDA && doBetaReduction)
    {
      // Do immediate beta reduction. It suffices to use a normal substitution
      // since neither op nor children have quantifiers, since they are
      // generated by sygus grammars.
      std::vector<Node> vars{op[0].begin(), op[0].end()};
      Assert(vars.size() == children.size());
      Node ret = op[1].substitute(
          vars.begin(), vars.end(), children.begin(), children.end());
      Trace("dt-sygus-util") << "...return (beta-reduce) " << ret << std::endl;
      return ret;
    }
    else
    {
      schildren.push_back(op);
    }
  }
  schildren.insert(schildren.end(), children.begin(), children.end());
  Node ret;
  if (ok == BUILTIN)
  {
    ret = NodeManager::currentNM()->mkNode(op, schildren);
    Trace("dt-sygus-util") << "...return (builtin) " << ret << std::endl;
    return ret;
  }
  // get the kind used for applying op
  Kind otk = NodeManager::operatorToKind(op);
  Trace("dt-sygus-util") << "operator kind is " << otk << std::endl;
  if (otk != UNDEFINED_KIND)
  {
    // If it is an APPLY_UF operator, we should have at least an operator and
    // a child.
    Assert(otk != APPLY_UF || schildren.size() != 1);
    ret = NodeManager::currentNM()->mkNode(otk, schildren);
    Trace("dt-sygus-util") << "...return (op) " << ret << std::endl;
    return ret;
  }
  Kind tok = getOperatorKindForSygusBuiltin(op);
  if (schildren.size() == 1 && tok == UNDEFINED_KIND)
  {
    ret = schildren[0];
  }
  else
  {
    ret = NodeManager::currentNM()->mkNode(tok, schildren);
  }
  Trace("dt-sygus-util") << "...return " << ret << std::endl;
  return ret;
}

struct SygusToBuiltinTermAttributeId
{
};
typedef expr::Attribute<SygusToBuiltinTermAttributeId, Node>
    SygusToBuiltinTermAttribute;

// A variant of the above attribute for cases where we introduce a fresh
// variable. This is to support sygusToBuiltin on non-constant sygus terms,
// where sygus variables should be mapped to canonical builtin variables.
// It is important to cache this so that sygusToBuiltin is deterministic.
struct SygusToBuiltinVarAttributeId
{
};
typedef expr::Attribute<SygusToBuiltinVarAttributeId, Node>
    SygusToBuiltinVarAttribute;

// A variant of the above attribute for cases where we introduce a fresh
// variable. This is to support sygusToBuiltin on non-constant sygus terms,
// where sygus variables should be mapped to canonical builtin variables.
// It is important to cache this so that sygusToBuiltin is deterministic.
struct BuiltinVarToSygusAttributeId
{
};
typedef expr::Attribute<BuiltinVarToSygusAttributeId, Node>
    BuiltinVarToSygusAttribute;

Node sygusToBuiltin(Node n, bool isExternal)
{
  std::unordered_map<TNode, Node> visited;
  std::unordered_map<TNode, Node>::iterator it;
  std::vector<TNode> visit;
  TNode cur;
  unsigned index;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = visited.find(cur);
    if (it == visited.end())
    {
      // Notice this condition succeeds in roughly 99% of the executions of this
      // method (based on our coverage tests), hence the else if / else cases
      // below do not significantly impact performance.
      if (cur.getKind() == APPLY_CONSTRUCTOR)
      {
        if (!isExternal && cur.hasAttribute(SygusToBuiltinTermAttribute()))
        {
          visited[cur] = cur.getAttribute(SygusToBuiltinTermAttribute());
        }
        else
        {
          visited[cur] = Node::null();
          visit.push_back(cur);
          for (const Node& cn : cur)
          {
            visit.push_back(cn);
          }
        }
      }
      else if (cur.getType().isSygusDatatype())
      {
        Assert (cur.isVar());
        if (cur.hasAttribute(SygusToBuiltinVarAttribute()))
        {
          // use the previously constructed variable for it
          visited[cur] = cur.getAttribute(SygusToBuiltinVarAttribute());
        }
        else
        {
          std::stringstream ss;
          ss << cur;
          const DType& dt = cur.getType().getDType();
          // make a fresh variable
          NodeManager * nm = NodeManager::currentNM();
          Node var = nm->mkBoundVar(ss.str(), dt.getSygusType());
          SygusToBuiltinVarAttribute stbv;
          cur.setAttribute(stbv, var);
          visited[cur] = var;
          // create backwards mapping
          BuiltinVarToSygusAttribute bvtsa;
          var.setAttribute(bvtsa, cur);
        }
      }
      else
      {
        // non-datatypes are themselves
        visited[cur] = cur;
      }
    }
    else if (it->second.isNull())
    {
      Node ret = cur;
      Assert(cur.getKind() == APPLY_CONSTRUCTOR);
      const DType& dt = cur.getType().getDType();
      // Non sygus-datatype terms are also themselves. Notice we treat the
      // case of non-sygus datatypes this way since it avoids computing
      // the type / datatype of the node in the pre-traversal above. The
      // case of non-sygus datatypes is very rare, so the extra addition to
      // visited is justified performance-wise.
      if (dt.isSygus())
      {
        std::vector<Node> children;
        for (const Node& cn : cur)
        {
          it = visited.find(cn);
          Assert(it != visited.end());
          Assert(!it->second.isNull());
          children.push_back(it->second);
        }
        index = indexOf(cur.getOperator());
        ret = mkSygusTerm(dt, index, children, true, isExternal);
      }
      visited[cur] = ret;
      // cache
      if (!isExternal)
      {
        SygusToBuiltinTermAttribute stbt;
        cur.setAttribute(stbt, ret);
      }
    }
  } while (!visit.empty());
  Assert(visited.find(n) != visited.end());
  Assert(!visited.find(n)->second.isNull());
  return visited[n];
}

Node builtinVarToSygus(Node v)
{
  BuiltinVarToSygusAttribute bvtsa;
  if (v.hasAttribute(bvtsa))
  {
    return v.getAttribute(bvtsa);
  }
  return Node::null();
}

void getFreeSymbolsSygusType(TypeNode sdt, std::unordered_set<Node>& syms)
{
  // datatype types we need to process
  std::vector<TypeNode> typeToProcess;
  // datatype types we have processed
  std::map<TypeNode, TypeNode> typesProcessed;
  typeToProcess.push_back(sdt);
  while (!typeToProcess.empty())
  {
    std::vector<TypeNode> typeNextToProcess;
    for (const TypeNode& curr : typeToProcess)
    {
      Assert(curr.isDatatype() && curr.getDType().isSygus());
      const DType& dtc = curr.getDType();
      for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++)
      {
        // collect the symbols from the operator
        Node op = dtc[j].getSygusOp();
        expr::getSymbols(op, syms);
        // traverse the argument types
        for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++)
        {
          TypeNode argt = dtc[j].getArgType(k);
          if (!argt.isDatatype() || !argt.getDType().isSygus())
          {
            // not a sygus datatype
            continue;
          }
          if (typesProcessed.find(argt) == typesProcessed.end())
          {
            typeNextToProcess.push_back(argt);
          }
        }
      }
    }
    typeToProcess.clear();
    typeToProcess.insert(typeToProcess.end(),
                         typeNextToProcess.begin(),
                         typeNextToProcess.end());
  }
}

TypeNode substituteAndGeneralizeSygusType(TypeNode sdt,
                                          const std::vector<Node>& syms,
                                          const std::vector<Node>& vars)
{
  NodeManager* nm = NodeManager::currentNM();
  const DType& sdtd = sdt.getDType();
  // compute the new formal argument list
  std::vector<Node> formalVars;
  Node prevVarList = sdtd.getSygusVarList();
  if (!prevVarList.isNull())
  {
    for (const Node& v : prevVarList)
    {
      // if it is not being replaced
      if (std::find(syms.begin(), syms.end(), v) != syms.end())
      {
        formalVars.push_back(v);
      }
    }
  }
  for (const Node& v : vars)
  {
    if (v.getKind() == BOUND_VARIABLE)
    {
      formalVars.push_back(v);
    }
  }
  // make the sygus variable list for the formal argument list
  Node abvl = nm->mkNode(BOUND_VAR_LIST, formalVars);
  Trace("sygus-abduct-debug") << "...finish" << std::endl;

  // must convert all constructors to version with variables in "vars"
  std::vector<SygusDatatype> sdts;
  std::set<TypeNode> unres;

  Trace("dtsygus-gen-debug") << "Process sygus type:" << std::endl;
  Trace("dtsygus-gen-debug") << sdtd.getName() << std::endl;

  // datatype types we need to process
  std::vector<TypeNode> dtToProcess;
  // datatype types we have processed
  std::map<TypeNode, TypeNode> dtProcessed;
  dtToProcess.push_back(sdt);
  std::stringstream ssutn0;
  ssutn0 << sdtd.getName() << "_s";
  TypeNode abdTNew =
      nm->mkSort(ssutn0.str(), NodeManager::SORT_FLAG_PLACEHOLDER);
  unres.insert(abdTNew);
  dtProcessed[sdt] = abdTNew;

  // We must convert all symbols in the sygus datatype type sdt to
  // apply the substitution { syms -> vars }, where syms is the free
  // variables of the input problem, and vars is the formal argument list
  // of the function-to-synthesize.

  // We are traversing over the subfield types of the datatype to convert
  // them into the form described above.
  while (!dtToProcess.empty())
  {
    std::vector<TypeNode> dtNextToProcess;
    for (const TypeNode& curr : dtToProcess)
    {
      Assert(curr.isDatatype() && curr.getDType().isSygus());
      const DType& dtc = curr.getDType();
      std::stringstream ssdtn;
      ssdtn << dtc.getName() << "_s";
      sdts.push_back(SygusDatatype(ssdtn.str()));
      Trace("dtsygus-gen-debug")
          << "Process datatype " << sdts.back().getName() << "..." << std::endl;
      for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++)
      {
        Node op = dtc[j].getSygusOp();
        // apply the substitution to the argument
        Node ops =
            op.substitute(syms.begin(), syms.end(), vars.begin(), vars.end());
        Trace("dtsygus-gen-debug") << "  Process constructor " << op << " / "
                                   << ops << "..." << std::endl;
        std::vector<TypeNode> cargs;
        for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++)
        {
          TypeNode argt = dtc[j].getArgType(k);
          std::map<TypeNode, TypeNode>::iterator itdp = dtProcessed.find(argt);
          TypeNode argtNew;
          if (itdp == dtProcessed.end())
          {
            std::stringstream ssutn;
            ssutn << argt.getDType().getName() << "_s";
            argtNew =
                nm->mkSort(ssutn.str(), NodeManager::SORT_FLAG_PLACEHOLDER);
            Trace("dtsygus-gen-debug") << "    ...unresolved type " << argtNew
                                       << " for " << argt << std::endl;
            unres.insert(argtNew);
            dtProcessed[argt] = argtNew;
            dtNextToProcess.push_back(argt);
          }
          else
          {
            argtNew = itdp->second;
          }
          Trace("dtsygus-gen-debug")
              << "    Arg #" << k << ": " << argtNew << std::endl;
          cargs.push_back(argtNew);
        }
        std::stringstream ss;
        ss << ops.getKind();
        Trace("dtsygus-gen-debug") << "Add constructor : " << ops << std::endl;
        sdts.back().addConstructor(ops, ss.str(), cargs);
      }
      Trace("dtsygus-gen-debug")
          << "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl;
      TypeNode stn = dtc.getSygusType();
      sdts.back().initializeDatatype(
          stn, abvl, dtc.getSygusAllowConst(), dtc.getSygusAllowAll());
    }
    dtToProcess.clear();
    dtToProcess.insert(
        dtToProcess.end(), dtNextToProcess.begin(), dtNextToProcess.end());
  }
  Trace("dtsygus-gen-debug")
      << "Make " << sdts.size() << " datatype types..." << std::endl;
  // extract the datatypes
  std::vector<DType> datatypes;
  for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++)
  {
    datatypes.push_back(sdts[i].getDatatype());
  }
  // make the datatype types
  std::vector<TypeNode> datatypeTypes = nm->mkMutualDatatypeTypes(
      datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
  TypeNode sdtS = datatypeTypes[0];
  if (Trace.isOn("dtsygus-gen-debug"))
  {
    Trace("dtsygus-gen-debug") << "Made datatype types:" << std::endl;
    for (unsigned j = 0, ndts = datatypeTypes.size(); j < ndts; j++)
    {
      const DType& dtj = datatypeTypes[j].getDType();
      Trace("dtsygus-gen-debug") << "#" << j << ": " << dtj << std::endl;
      for (unsigned k = 0, ncons = dtj.getNumConstructors(); k < ncons; k++)
      {
        for (unsigned l = 0, nargs = dtj[k].getNumArgs(); l < nargs; l++)
        {
          if (!dtj[k].getArgType(l).isDatatype())
          {
            Trace("dtsygus-gen-debug")
                << "Argument " << l << " of " << dtj[k]
                << " is not datatype : " << dtj[k].getArgType(l) << std::endl;
            AlwaysAssert(false);
          }
        }
      }
    }
  }
  return sdtS;
}

unsigned getSygusTermSize(Node n)
{
  if (n.getKind() != APPLY_CONSTRUCTOR)
  {
    return 0;
  }
  unsigned sum = 0;
  for (const Node& nc : n)
  {
    sum += getSygusTermSize(nc);
  }
  const DType& dt = datatypeOf(n.getOperator());
  int cindex = indexOf(n.getOperator());
  Assert(cindex >= 0 && static_cast<size_t>(cindex) < dt.getNumConstructors());
  unsigned weight = dt[cindex].getWeight();
  return weight + sum;
}

/**
 * Map terms to the result of expand definitions calling smt::expandDefinitions
 * on it.
 */
struct SygusExpDefFormAttributeId
{
};
typedef expr::Attribute<SygusExpDefFormAttributeId, Node>
    SygusExpDefFormAttribute;

void setExpandedDefinitionForm(Node op, Node eop)
{
  op.setAttribute(SygusExpDefFormAttribute(), eop);
}

Node getExpandedDefinitionForm(Node op)
{
  Node eop = op.getAttribute(SygusExpDefFormAttribute());
  // if not set, assume original
  return eop.isNull() ? op : eop;
}

}  // namespace utils
}  // namespace datatypes
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Mathias Preiner, Aina Niemetz
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		* Implementation of rewriter for the theory of (co)inductive datatypes.
14		*/
15
16		#include "theory/datatypes/sygus_datatype_utils.h"
17
18		#include <sstream>
19
20		#include "expr/dtype.h"
21		#include "expr/dtype_cons.h"
22		#include "expr/node_algorithm.h"
23		#include "expr/sygus_datatype.h"
24		#include "smt/env.h"
25		#include "theory/evaluator.h"
26		#include "theory/rewriter.h"
27
28		using namespace cvc5;
29		using namespace cvc5::kind;
30
31		namespace cvc5 {
32		namespace theory {
33		namespace datatypes {
34		namespace utils {
35
36	90161	Node applySygusArgs(const DType& dt,
37		Node op,
38		Node n,
39		const std::vector<Node>& args)
40		{
41		// optimization: if n is just a sygus bound variable, return immediately
42		// by replacing with the proper argument, or returning unchanged if it is
43		// a bound variable not corresponding to a formal argument.
44	90161	if (n.getKind() == BOUND_VARIABLE)
45		{
46	1630	if (n.hasAttribute(SygusVarNumAttribute()))
47		{
48	1518	int vn = n.getAttribute(SygusVarNumAttribute());
49	1518	Assert(dt.getSygusVarList()[vn] == n);
50	1518	return args[vn];
51		}
52		// it is a different bound variable, it is unchanged
53	112	return n;
54		}
55		// n is an application of operator op.
56		// We must compute the free variables in op to determine if there are
57		// any substitutions we need to make to n.
58	177062	TNode val;
59	88531	if (!op.hasAttribute(SygusVarFreeAttribute()))
60		{
61	1750	std::unordered_set<Node> fvs;
62	875	if (expr::getFreeVariables(op, fvs))
63		{
64	22	if (fvs.size() == 1)
65		{
66	24	for (const Node& v : fvs)
67		{
68	12	val = v;
69		}
70		}
71		else
72		{
73	10	val = op;
74		}
75		}
76	875	Trace("dt-sygus-fv") << "Free var in " << op << " : " << val << std::endl;
77	875	op.setAttribute(SygusVarFreeAttribute(), val);
78		}
79		else
80		{
81	87656	val = op.getAttribute(SygusVarFreeAttribute());
82		}
83	88531	if (val.isNull())
84		{
85	87915	return n;
86		}
87	616	if (val.getKind() == BOUND_VARIABLE)
88		{
89		// single substitution case
90	324	int vn = val.getAttribute(SygusVarNumAttribute());
91	648	TNode sub = args[vn];
92	324	return n.substitute(val, sub);
93		}
94		// do the full substitution
95	584	std::vector<Node> vars;
96	584	Node bvl = dt.getSygusVarList();
97	984	for (unsigned i = 0, nvars = bvl.getNumChildren(); i < nvars; i++)
98		{
99	692	vars.push_back(bvl[i]);
100		}
101	292	return n.substitute(vars.begin(), vars.end(), args.begin(), args.end());
102		}
103
104	217	Kind getOperatorKindForSygusBuiltin(Node op)
105		{
106	217	Assert(op.getKind() != BUILTIN);
107	217	if (op.getKind() == LAMBDA)
108		{
109		return APPLY_UF;
110		}
111	217	return NodeManager::getKindForFunction(op);
112		}
113
114	221613	Kind getEliminateKind(Kind ok)
115		{
116	221613	Kind nk = ok;
117		// We also must ensure that builtin operators which are eliminated
118		// during expand definitions are replaced by the proper operator.
119	221613	if (ok == DIVISION)
120		{
121	105	nk = DIVISION_TOTAL;
122		}
123	221508	else if (ok == INTS_DIVISION)
124		{
125		nk = INTS_DIVISION_TOTAL;
126		}
127	221508	else if (ok == INTS_MODULUS)
128		{
129		nk = INTS_MODULUS_TOTAL;
130		}
131	221613	return nk;
132		}
133
134	763444	Node mkSygusTerm(const DType& dt,
135		unsigned i,
136		const std::vector<Node>& children,
137		bool doBetaReduction,
138		bool isExternal)
139		{
140	1526888	Trace("dt-sygus-util") << "Make sygus term " << dt.getName() << "[" << i
141	763444	<< "] with children: " << children << std::endl;
142	763444	Assert(i < dt.getNumConstructors());
143	763444	Assert(dt.isSygus());
144	763444	Assert(!dt[i].getSygusOp().isNull());
145	1526888	Node op = dt[i].getSygusOp();
146	1526888	Node opn = op;
147	763444	if (!isExternal)
148		{
149		// Get the normalized version of the sygus operator. We do this by
150		// expanding definitions, rewriting it, and eliminating partial operators.
151	755676	if (op.isConst())
152		{
153		// If it is a builtin operator, convert to total version if necessary.
154		// First, get the kind for the operator.
155	221613	Kind ok = NodeManager::operatorToKind(op);
156	443226	Trace("sygus-grammar-normalize-debug")
157	221613	<< "...builtin kind is " << ok << std::endl;
158	221613	Kind nk = getEliminateKind(ok);
159	221613	if (nk != ok)
160		{
161	210	Trace("sygus-grammar-normalize-debug")
162	105	<< "...replace by builtin operator " << nk << std::endl;
163	105	opn = NodeManager::currentNM()->operatorOf(nk);
164		}
165		}
166		else
167		{
168		// Get the expanded definition form, if it has been marked. This ensures
169		// that user-defined functions have been eliminated from op.
170	534063	opn = getExpandedDefinitionForm(op);
171		}
172		}
173	1526888	return mkSygusTerm(opn, children, doBetaReduction);
174		}
175
176	763448	Node mkSygusTerm(Node op,
177		const std::vector<Node>& children,
178		bool doBetaReduction)
179		{
180	763448	Trace("dt-sygus-util") << "Operator is " << op << std::endl;
181	763448	if (children.empty())
182		{
183		// no children, return immediately
184	168802	Trace("dt-sygus-util") << "...return direct op" << std::endl;
185	168802	return op;
186		}
187		// if it is the any constant, we simply return the child
188	594646	if (op.getAttribute(SygusAnyConstAttribute()))
189		{
190	640	Assert(children.size() == 1);
191	640	return children[0];
192		}
193	1188012	std::vector<Node> schildren;
194		// get the kind of the operator
195	594006	Kind ok = op.getKind();
196	594006	if (ok != BUILTIN)
197		{
198	531215	if (ok == LAMBDA && doBetaReduction)
199		{
200		// Do immediate beta reduction. It suffices to use a normal substitution
201		// since neither op nor children have quantifiers, since they are
202		// generated by sygus grammars.
203	1058622	std::vector<Node> vars{op[0].begin(), op[0].end()};
204	529311	Assert(vars.size() == children.size());
205		Node ret = op[1].substitute(
206	1058622	vars.begin(), vars.end(), children.begin(), children.end());
207	529311	Trace("dt-sygus-util") << "...return (beta-reduce) " << ret << std::endl;
208	529311	return ret;
209		}
210		else
211		{
212	1904	schildren.push_back(op);
213		}
214		}
215	64695	schildren.insert(schildren.end(), children.begin(), children.end());
216	129390	Node ret;
217	64695	if (ok == BUILTIN)
218		{
219	62791	ret = NodeManager::currentNM()->mkNode(op, schildren);
220	62791	Trace("dt-sygus-util") << "...return (builtin) " << ret << std::endl;
221	62791	return ret;
222		}
223		// get the kind used for applying op
224	1904	Kind otk = NodeManager::operatorToKind(op);
225	1904	Trace("dt-sygus-util") << "operator kind is " << otk << std::endl;
226	1904	if (otk != UNDEFINED_KIND)
227		{
228		// If it is an APPLY_UF operator, we should have at least an operator and
229		// a child.
230	1687	Assert(otk != APPLY_UF \|\| schildren.size() != 1);
231	1687	ret = NodeManager::currentNM()->mkNode(otk, schildren);
232	1687	Trace("dt-sygus-util") << "...return (op) " << ret << std::endl;
233	1687	return ret;
234		}
235	217	Kind tok = getOperatorKindForSygusBuiltin(op);
236	217	if (schildren.size() == 1 && tok == UNDEFINED_KIND)
237		{
238		ret = schildren[0];
239		}
240		else
241		{
242	217	ret = NodeManager::currentNM()->mkNode(tok, schildren);
243		}
244	217	Trace("dt-sygus-util") << "...return " << ret << std::endl;
245	217	return ret;
246		}
247
248		struct SygusToBuiltinTermAttributeId
249		{
250		};
251		typedef expr::Attribute<SygusToBuiltinTermAttributeId, Node>
252		SygusToBuiltinTermAttribute;
253
254		// A variant of the above attribute for cases where we introduce a fresh
255		// variable. This is to support sygusToBuiltin on non-constant sygus terms,
256		// where sygus variables should be mapped to canonical builtin variables.
257		// It is important to cache this so that sygusToBuiltin is deterministic.
258		struct SygusToBuiltinVarAttributeId
259		{
260		};
261		typedef expr::Attribute<SygusToBuiltinVarAttributeId, Node>
262		SygusToBuiltinVarAttribute;
263
264		// A variant of the above attribute for cases where we introduce a fresh
265		// variable. This is to support sygusToBuiltin on non-constant sygus terms,
266		// where sygus variables should be mapped to canonical builtin variables.
267		// It is important to cache this so that sygusToBuiltin is deterministic.
268		struct BuiltinVarToSygusAttributeId
269		{
270		};
271		typedef expr::Attribute<BuiltinVarToSygusAttributeId, Node>
272		BuiltinVarToSygusAttribute;
273
274	461658	Node sygusToBuiltin(Node n, bool isExternal)
275		{
276	923316	std::unordered_map<TNode, Node> visited;
277	461658	std::unordered_map<TNode, Node>::iterator it;
278	923316	std::vector<TNode> visit;
279	923316	TNode cur;
280		unsigned index;
281	461658	visit.push_back(n);
282	270720	do
283		{
284	732378	cur = visit.back();
285	732378	visit.pop_back();
286	732378	it = visited.find(cur);
287	732378	if (it == visited.end())
288		{
289		// Notice this condition succeeds in roughly 99% of the executions of this
290		// method (based on our coverage tests), hence the else if / else cases
291		// below do not significantly impact performance.
292	631412	if (cur.getKind() == APPLY_CONSTRUCTOR)
293		{
294	622428	if (!isExternal && cur.hasAttribute(SygusToBuiltinTermAttribute()))
295		{
296	526926	visited[cur] = cur.getAttribute(SygusToBuiltinTermAttribute());
297		}
298		else
299		{
300	95502	visited[cur] = Node::null();
301	95502	visit.push_back(cur);
302	270720	for (const Node& cn : cur)
303		{
304	175218	visit.push_back(cn);
305		}
306		}
307		}
308	8984	else if (cur.getType().isSygusDatatype())
309		{
310	8388	Assert (cur.isVar());
311	8388	if (cur.hasAttribute(SygusToBuiltinVarAttribute()))
312		{
313		// use the previously constructed variable for it
314	8263	visited[cur] = cur.getAttribute(SygusToBuiltinVarAttribute());
315		}
316		else
317		{
318	250	std::stringstream ss;
319	125	ss << cur;
320	125	const DType& dt = cur.getType().getDType();
321		// make a fresh variable
322	125	NodeManager * nm = NodeManager::currentNM();
323	250	Node var = nm->mkBoundVar(ss.str(), dt.getSygusType());
324		SygusToBuiltinVarAttribute stbv;
325	125	cur.setAttribute(stbv, var);
326	125	visited[cur] = var;
327		// create backwards mapping
328		BuiltinVarToSygusAttribute bvtsa;
329	125	var.setAttribute(bvtsa, cur);
330		}
331		}
332		else
333		{
334		// non-datatypes are themselves
335	596	visited[cur] = cur;
336		}
337		}
338	100966	else if (it->second.isNull())
339		{
340	191004	Node ret = cur;
341	95502	Assert(cur.getKind() == APPLY_CONSTRUCTOR);
342	95502	const DType& dt = cur.getType().getDType();
343		// Non sygus-datatype terms are also themselves. Notice we treat the
344		// case of non-sygus datatypes this way since it avoids computing
345		// the type / datatype of the node in the pre-traversal above. The
346		// case of non-sygus datatypes is very rare, so the extra addition to
347		// visited is justified performance-wise.
348	95502	if (dt.isSygus())
349		{
350	191004	std::vector<Node> children;
351	270720	for (const Node& cn : cur)
352		{
353	175218	it = visited.find(cn);
354	175218	Assert(it != visited.end());
355	175218	Assert(!it->second.isNull());
356	175218	children.push_back(it->second);
357		}
358	95502	index = indexOf(cur.getOperator());
359	95502	ret = mkSygusTerm(dt, index, children, true, isExternal);
360		}
361	95502	visited[cur] = ret;
362		// cache
363	95502	if (!isExternal)
364		{
365		SygusToBuiltinTermAttribute stbt;
366	87734	cur.setAttribute(stbt, ret);
367		}
368		}
369	732378	} while (!visit.empty());
370	461658	Assert(visited.find(n) != visited.end());
371	461658	Assert(!visited.find(n)->second.isNull());
372	923316	return visited[n];
373		}
374
375	237	Node builtinVarToSygus(Node v)
376		{
377		BuiltinVarToSygusAttribute bvtsa;
378	237	if (v.hasAttribute(bvtsa))
379		{
380	237	return v.getAttribute(bvtsa);
381		}
382		return Node::null();
383		}
384
385		void getFreeSymbolsSygusType(TypeNode sdt, std::unordered_set<Node>& syms)
386		{
387		// datatype types we need to process
388		std::vector<TypeNode> typeToProcess;
389		// datatype types we have processed
390		std::map<TypeNode, TypeNode> typesProcessed;
391		typeToProcess.push_back(sdt);
392		while (!typeToProcess.empty())
393		{
394		std::vector<TypeNode> typeNextToProcess;
395		for (const TypeNode& curr : typeToProcess)
396		{
397		Assert(curr.isDatatype() && curr.getDType().isSygus());
398		const DType& dtc = curr.getDType();
399		for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++)
400		{
401		// collect the symbols from the operator
402		Node op = dtc[j].getSygusOp();
403		expr::getSymbols(op, syms);
404		// traverse the argument types
405		for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++)
406		{
407		TypeNode argt = dtc[j].getArgType(k);
408		if (!argt.isDatatype() \|\| !argt.getDType().isSygus())
409		{
410		// not a sygus datatype
411		continue;
412		}
413		if (typesProcessed.find(argt) == typesProcessed.end())
414		{
415		typeNextToProcess.push_back(argt);
416		}
417		}
418		}
419		}
420		typeToProcess.clear();
421		typeToProcess.insert(typeToProcess.end(),
422		typeNextToProcess.begin(),
423		typeNextToProcess.end());
424		}
425		}
426
427	11	TypeNode substituteAndGeneralizeSygusType(TypeNode sdt,
428		const std::vector<Node>& syms,
429		const std::vector<Node>& vars)
430		{
431	11	NodeManager* nm = NodeManager::currentNM();
432	11	const DType& sdtd = sdt.getDType();
433		// compute the new formal argument list
434	22	std::vector<Node> formalVars;
435	22	Node prevVarList = sdtd.getSygusVarList();
436	11	if (!prevVarList.isNull())
437		{
438		for (const Node& v : prevVarList)
439		{
440		// if it is not being replaced
441		if (std::find(syms.begin(), syms.end(), v) != syms.end())
442		{
443		formalVars.push_back(v);
444		}
445		}
446		}
447	49	for (const Node& v : vars)
448		{
449	38	if (v.getKind() == BOUND_VARIABLE)
450		{
451	38	formalVars.push_back(v);
452		}
453		}
454		// make the sygus variable list for the formal argument list
455	22	Node abvl = nm->mkNode(BOUND_VAR_LIST, formalVars);
456	11	Trace("sygus-abduct-debug") << "...finish" << std::endl;
457
458		// must convert all constructors to version with variables in "vars"
459	22	std::vector<SygusDatatype> sdts;
460	22	std::set<TypeNode> unres;
461
462	11	Trace("dtsygus-gen-debug") << "Process sygus type:" << std::endl;
463	11	Trace("dtsygus-gen-debug") << sdtd.getName() << std::endl;
464
465		// datatype types we need to process
466	22	std::vector<TypeNode> dtToProcess;
467		// datatype types we have processed
468	22	std::map<TypeNode, TypeNode> dtProcessed;
469	11	dtToProcess.push_back(sdt);
470	22	std::stringstream ssutn0;
471	11	ssutn0 << sdtd.getName() << "_s";
472		TypeNode abdTNew =
473	22	nm->mkSort(ssutn0.str(), NodeManager::SORT_FLAG_PLACEHOLDER);
474	11	unres.insert(abdTNew);
475	11	dtProcessed[sdt] = abdTNew;
476
477		// We must convert all symbols in the sygus datatype type sdt to
478		// apply the substitution { syms -> vars }, where syms is the free
479		// variables of the input problem, and vars is the formal argument list
480		// of the function-to-synthesize.
481
482		// We are traversing over the subfield types of the datatype to convert
483		// them into the form described above.
484	51	while (!dtToProcess.empty())
485		{
486	40	std::vector<TypeNode> dtNextToProcess;
487	42	for (const TypeNode& curr : dtToProcess)
488		{
489	22	Assert(curr.isDatatype() && curr.getDType().isSygus());
490	22	const DType& dtc = curr.getDType();
491	44	std::stringstream ssdtn;
492	22	ssdtn << dtc.getName() << "_s";
493	22	sdts.push_back(SygusDatatype(ssdtn.str()));
494	44	Trace("dtsygus-gen-debug")
495	22	<< "Process datatype " << sdts.back().getName() << "..." << std::endl;
496	76	for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++)
497		{
498	108	Node op = dtc[j].getSygusOp();
499		// apply the substitution to the argument
500		Node ops =
501	108	op.substitute(syms.begin(), syms.end(), vars.begin(), vars.end());
502	108	Trace("dtsygus-gen-debug") << " Process constructor " << op << " / "
503	54	<< ops << "..." << std::endl;
504	108	std::vector<TypeNode> cargs;
505	92	for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++)
506		{
507	76	TypeNode argt = dtc[j].getArgType(k);
508	38	std::map<TypeNode, TypeNode>::iterator itdp = dtProcessed.find(argt);
509	76	TypeNode argtNew;
510	38	if (itdp == dtProcessed.end())
511		{
512	22	std::stringstream ssutn;
513	11	ssutn << argt.getDType().getName() << "_s";
514	11	argtNew =
515	22	nm->mkSort(ssutn.str(), NodeManager::SORT_FLAG_PLACEHOLDER);
516	22	Trace("dtsygus-gen-debug") << " ...unresolved type " << argtNew
517	11	<< " for " << argt << std::endl;
518	11	unres.insert(argtNew);
519	11	dtProcessed[argt] = argtNew;
520	11	dtNextToProcess.push_back(argt);
521		}
522		else
523		{
524	27	argtNew = itdp->second;
525		}
526	76	Trace("dtsygus-gen-debug")
527	38	<< " Arg #" << k << ": " << argtNew << std::endl;
528	38	cargs.push_back(argtNew);
529		}
530	108	std::stringstream ss;
531	54	ss << ops.getKind();
532	54	Trace("dtsygus-gen-debug") << "Add constructor : " << ops << std::endl;
533	54	sdts.back().addConstructor(ops, ss.str(), cargs);
534		}
535	44	Trace("dtsygus-gen-debug")
536	22	<< "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl;
537	44	TypeNode stn = dtc.getSygusType();
538	66	sdts.back().initializeDatatype(
539	44	stn, abvl, dtc.getSygusAllowConst(), dtc.getSygusAllowAll());
540		}
541	20	dtToProcess.clear();
542	20	dtToProcess.insert(
543	40	dtToProcess.end(), dtNextToProcess.begin(), dtNextToProcess.end());
544		}
545	22	Trace("dtsygus-gen-debug")
546	11	<< "Make " << sdts.size() << " datatype types..." << std::endl;
547		// extract the datatypes
548	22	std::vector<DType> datatypes;
549	33	for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++)
550		{
551	22	datatypes.push_back(sdts[i].getDatatype());
552		}
553		// make the datatype types
554		std::vector<TypeNode> datatypeTypes = nm->mkMutualDatatypeTypes(
555	22	datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
556	11	TypeNode sdtS = datatypeTypes[0];
557	11	if (Trace.isOn("dtsygus-gen-debug"))
558		{
559		Trace("dtsygus-gen-debug") << "Made datatype types:" << std::endl;
560		for (unsigned j = 0, ndts = datatypeTypes.size(); j < ndts; j++)
561		{
562		const DType& dtj = datatypeTypes[j].getDType();
563		Trace("dtsygus-gen-debug") << "#" << j << ": " << dtj << std::endl;
564		for (unsigned k = 0, ncons = dtj.getNumConstructors(); k < ncons; k++)
565		{
566		for (unsigned l = 0, nargs = dtj[k].getNumArgs(); l < nargs; l++)
567		{
568		if (!dtj[k].getArgType(l).isDatatype())
569		{
570		Trace("dtsygus-gen-debug")
571		<< "Argument " << l << " of " << dtj[k]
572		<< " is not datatype : " << dtj[k].getArgType(l) << std::endl;
573		AlwaysAssert(false);
574		}
575		}
576		}
577		}
578		}
579	22	return sdtS;
580		}
581
582	459013	unsigned getSygusTermSize(Node n)
583		{
584	459013	if (n.getKind() != APPLY_CONSTRUCTOR)
585		{
586	21915	return 0;
587		}
588	437098	unsigned sum = 0;
589	726193	for (const Node& nc : n)
590		{
591	289095	sum += getSygusTermSize(nc);
592		}
593	437098	const DType& dt = datatypeOf(n.getOperator());
594	437098	int cindex = indexOf(n.getOperator());
595	437098	Assert(cindex >= 0 && static_cast<size_t>(cindex) < dt.getNumConstructors());
596	437098	unsigned weight = dt[cindex].getWeight();
597	437098	return weight + sum;
598		}
599
600		/**
601		* Map terms to the result of expand definitions calling smt::expandDefinitions
602		* on it.
603		*/
604		struct SygusExpDefFormAttributeId
605		{
606		};
607		typedef expr::Attribute<SygusExpDefFormAttributeId, Node>
608		SygusExpDefFormAttribute;
609
610	4331	void setExpandedDefinitionForm(Node op, Node eop)
611		{
612	4331	op.setAttribute(SygusExpDefFormAttribute(), eop);
613	4331	}
614
615	534063	Node getExpandedDefinitionForm(Node op)
616		{
617	1068126	Node eop = op.getAttribute(SygusExpDefFormAttribute());
618		// if not set, assume original
619	1068126	return eop.isNull() ? op : eop;
620		}
621
622		} // namespace utils
623		} // namespace datatypes
624		} // namespace theory
625	31137	} // namespace cvc5