Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/datatypes/sygus_simple_sym.cpp	Lines:	261	281	92.9 %
Date:	2021-11-07	Branches:	560	1104	50.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Haniel Barbosa, Mathias Preiner
 *
 * 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 simple symmetry breaking for sygus.
 */

#include "theory/datatypes/sygus_simple_sym.h"

#include "expr/dtype_cons.h"
#include "theory/quantifiers/term_util.h"
#include "util/rational.h"

using namespace std;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace datatypes {

SygusSimpleSymBreak::SygusSimpleSymBreak(quantifiers::TermDbSygus* tds)
    : d_tds(tds)
{
}

/** Requirement trie
 *
 * This class is used to make queries about sygus grammars, including what
 * constructors they contain, and their types.
 *
 * As a simple example, consider the trie:
 * root:
 *   d_req_kind = PLUS
 *   d_children[0]:
 *     d_req_type = A
 *   d_children[1]:
 *     d_req_type = A
 * This trie is satisfied by sygus types that have a constructor whose builtin
 * kind is PLUS and whose argument types are both A.
 */
class ReqTrie
{
 public:
  ReqTrie() : d_req_kind(UNDEFINED_KIND) {}
  /** the children of this node */
  std::map<unsigned, ReqTrie> d_children;
  /** the (builtin) kind required by this node */
  Kind d_req_kind;
  /** the type that this node is required to be */
  TypeNode d_req_type;
  /** the constant required by this node */
  Node d_req_const;
  /** print this trie */
  void print(const char* c, int indent = 0)
  {
    if (d_req_kind != UNDEFINED_KIND)
    {
      Trace(c) << d_req_kind << " ";
    }
    else if (!d_req_type.isNull())
    {
      Trace(c) << d_req_type;
    }
    else if (!d_req_const.isNull())
    {
      Trace(c) << d_req_const;
    }
    else
    {
      Trace(c) << "_";
    }
    Trace(c) << std::endl;
    for (std::map<unsigned, ReqTrie>::iterator it = d_children.begin();
         it != d_children.end();
         ++it)
    {
      for (int i = 0; i <= indent; i++)
      {
        Trace(c) << "  ";
      }
      Trace(c) << it->first << " : ";
      it->second.print(c, indent + 1);
    }
  }
  /**
   * Are the requirements of this trie satisfied by sygus type tn?
   * tdb is a reference to the sygus term database.
   */
  bool satisfiedBy(quantifiers::TermDbSygus* tdb, TypeNode tn)
  {
    if (!d_req_const.isNull())
    {
      quantifiers::SygusTypeInfo& sti = tdb->getTypeInfo(tn);
      if (!sti.hasConst(d_req_const))
      {
        return false;
      }
    }
    if (!d_req_type.isNull())
    {
      Trace("sygus-sb-debug")
          << "- check if " << tn << " is type " << d_req_type << std::endl;
      if (tn != d_req_type)
      {
        return false;
      }
    }
    if (d_req_kind != UNDEFINED_KIND)
    {
      Trace("sygus-sb-debug")
          << "- check if " << tn << " has " << d_req_kind << std::endl;
      std::vector<TypeNode> argts;
      if (tdb->canConstructKind(tn, d_req_kind, argts))
      {
        for (std::map<unsigned, ReqTrie>::iterator it = d_children.begin();
             it != d_children.end();
             ++it)
        {
          if (it->first < argts.size())
          {
            TypeNode tnc = argts[it->first];
            if (!it->second.satisfiedBy(tdb, tnc))
            {
              return false;
            }
          }
          else
          {
            return false;
          }
        }
      }
      else
      {
        return false;
      }
    }
    return true;
  }
  /** is this the empty (trivially satisfied) trie? */
  bool empty()
  {
    return d_req_kind == UNDEFINED_KIND && d_req_const.isNull()
           && d_req_type.isNull() && d_children.empty();
  }
};

bool SygusSimpleSymBreak::considerArgKind(
    TypeNode tn, TypeNode tnp, Kind k, Kind pk, int arg)
{
  const DType& pdt = tnp.getDType();
  const DType& dt = tn.getDType();
  quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
  quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
  Assert(ti.hasKind(k));
  Assert(pti.hasKind(pk));
  Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
                          << ", arg = " << arg << " in " << tnp << "?"
                          << std::endl;
  int c = ti.getKindConsNum(k);
  int pc = pti.getKindConsNum(pk);
  // check for associativity
  if (k == pk && quantifiers::TermUtil::isAssoc(k))
  {
    // if the operator is associative, then a repeated occurrence should only
    // occur in the leftmost argument position
    int firstArg = getFirstArgOccurrence(pdt[pc], tn);
    Assert(firstArg != -1);
    if (arg == firstArg)
    {
      return true;
    }
    // the argument types of the child must be the parent's type
    for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
    {
      TypeNode type = dt[c].getArgType(i);
      if (type != tnp)
      {
        return true;
      }
    }
    Trace("sygus-sb-simple")
        << "  sb-simple : do not consider " << k << " at child arg " << arg
        << " of " << k
        << " since it is associative, with first arg = " << firstArg
        << std::endl;
    return false;
  }
  // describes the shape of an alternate term to construct
  //  we check whether this term is in the sygus grammar below
  ReqTrie rt;
  Assert(rt.empty());

  // construct rt by cases
  if (pk == NOT || pk == BITVECTOR_NOT || pk == UMINUS || pk == BITVECTOR_NEG)
  {
    // negation normal form
    if (pk == k)
    {
      rt.d_req_type = dt[c].getArgType(0);
    }
    else
    {
      Kind reqk = UNDEFINED_KIND;      // required kind for all children
      std::map<unsigned, Kind> reqkc;  // required kind for some children
      if (pk == NOT)
      {
        if (k == AND)
        {
          rt.d_req_kind = OR;
          reqk = NOT;
        }
        else if (k == OR)
        {
          rt.d_req_kind = AND;
          reqk = NOT;
        }
        else if (k == EQUAL)
        {
          rt.d_req_kind = XOR;
        }
        else if (k == XOR)
        {
          rt.d_req_kind = EQUAL;
        }
        else if (k == ITE)
        {
          rt.d_req_kind = ITE;
          reqkc[1] = NOT;
          reqkc[2] = NOT;
          rt.d_children[0].d_req_type = dt[c].getArgType(0);
        }
        else if (k == LEQ || k == GT)
        {
          //  (not (~ x y)) ----->  (~ (+ y 1) x)
          rt.d_req_kind = k;
          rt.d_children[0].d_req_kind = PLUS;
          rt.d_children[0].d_children[0].d_req_type = dt[c].getArgType(1);
          rt.d_children[0].d_children[1].d_req_const =
              NodeManager::currentNM()->mkConst(Rational(1));
          rt.d_children[1].d_req_type = dt[c].getArgType(0);
        }
        else if (k == LT || k == GEQ)
        {
          //  (not (~ x y)) ----->  (~ y (+ x 1))
          rt.d_req_kind = k;
          rt.d_children[0].d_req_type = dt[c].getArgType(1);
          rt.d_children[1].d_req_kind = PLUS;
          rt.d_children[1].d_children[0].d_req_type = dt[c].getArgType(0);
          rt.d_children[1].d_children[1].d_req_const =
              NodeManager::currentNM()->mkConst(Rational(1));
        }
      }
      else if (pk == BITVECTOR_NOT)
      {
        if (k == BITVECTOR_AND)
        {
          rt.d_req_kind = BITVECTOR_OR;
          reqk = BITVECTOR_NOT;
        }
        else if (k == BITVECTOR_OR)
        {
          rt.d_req_kind = BITVECTOR_AND;
          reqk = BITVECTOR_NOT;
        }
        else if (k == BITVECTOR_XNOR)
        {
          rt.d_req_kind = BITVECTOR_XOR;
        }
        else if (k == BITVECTOR_XOR)
        {
          rt.d_req_kind = BITVECTOR_XNOR;
        }
      }
      else if (pk == UMINUS)
      {
        if (k == PLUS)
        {
          rt.d_req_kind = PLUS;
          reqk = UMINUS;
        }
      }
      else if (pk == BITVECTOR_NEG)
      {
        if (k == PLUS)
        {
          rt.d_req_kind = PLUS;
          reqk = BITVECTOR_NEG;
        }
      }
      if (!rt.empty() && (reqk != UNDEFINED_KIND || !reqkc.empty()))
      {
        int pcr = pti.getKindConsNum(rt.d_req_kind);
        if (pcr != -1)
        {
          Assert(pcr < static_cast<int>(pdt.getNumConstructors()));
          // must have same number of arguments
          if (pdt[pcr].getNumArgs() == dt[c].getNumArgs())
          {
            for (unsigned i = 0, nargs = pdt[pcr].getNumArgs(); i < nargs; i++)
            {
              Kind rk = reqk;
              if (reqk == UNDEFINED_KIND)
              {
                std::map<unsigned, Kind>::iterator itr = reqkc.find(i);
                if (itr != reqkc.end())
                {
                  rk = itr->second;
                }
              }
              if (rk != UNDEFINED_KIND)
              {
                rt.d_children[i].d_req_kind = rk;
                rt.d_children[i].d_children[0].d_req_type = dt[c].getArgType(i);
              }
            }
          }
        }
      }
    }
  }
  else if (k == MINUS || k == BITVECTOR_SUB)
  {
    if (pk == EQUAL || pk == MINUS || pk == BITVECTOR_SUB || pk == LEQ
        || pk == LT || pk == GEQ || pk == GT)
    {
      int oarg = arg == 0 ? 1 : 0;
      //  (~ x (- y z))  ---->  (~ (+ x z) y)
      //  (~ (- y z) x)  ---->  (~ y (+ x z))
      rt.d_req_kind = pk;
      rt.d_children[arg].d_req_type = dt[c].getArgType(0);
      rt.d_children[oarg].d_req_kind = k == MINUS ? PLUS : BITVECTOR_ADD;
      rt.d_children[oarg].d_children[0].d_req_type = pdt[pc].getArgType(oarg);
      rt.d_children[oarg].d_children[1].d_req_type = dt[c].getArgType(1);
    }
    else if (pk == PLUS || pk == BITVECTOR_ADD)
    {
      //  (+ x (- y z))  -----> (- (+ x y) z)
      //  (+ (- y z) x)  -----> (- (+ x y) z)
      rt.d_req_kind = pk == PLUS ? MINUS : BITVECTOR_SUB;
      int oarg = arg == 0 ? 1 : 0;
      rt.d_children[0].d_req_kind = pk;
      rt.d_children[0].d_children[0].d_req_type = pdt[pc].getArgType(oarg);
      rt.d_children[0].d_children[1].d_req_type = dt[c].getArgType(0);
      rt.d_children[1].d_req_type = dt[c].getArgType(1);
    }
  }
  else if (k == ITE)
  {
    if (pk != ITE)
    {
      //  (o X (ite y z w) X')  -----> (ite y (o X z X') (o X w X'))
      rt.d_req_kind = ITE;
      rt.d_children[0].d_req_type = dt[c].getArgType(0);
      unsigned n_args = pdt[pc].getNumArgs();
      for (unsigned r = 1; r <= 2; r++)
      {
        rt.d_children[r].d_req_kind = pk;
        for (unsigned q = 0; q < n_args; q++)
        {
          if ((int)q == arg)
          {
            rt.d_children[r].d_children[q].d_req_type = dt[c].getArgType(r);
          }
          else
          {
            rt.d_children[r].d_children[q].d_req_type = pdt[pc].getArgType(q);
          }
        }
      }
      // this increases term size but is probably a good idea
    }
  }
  else if (k == NOT)
  {
    if (pk == ITE)
    {
      //  (ite (not y) z w)  -----> (ite y w z)
      rt.d_req_kind = ITE;
      rt.d_children[0].d_req_type = dt[c].getArgType(0);
      rt.d_children[1].d_req_type = pdt[pc].getArgType(2);
      rt.d_children[2].d_req_type = pdt[pc].getArgType(1);
    }
  }
  Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
                          << ", arg = " << arg << "?" << std::endl;
  if (!rt.empty())
  {
    rt.print("sygus-sb-debug");
    // check if it meets the requirements
    if (rt.satisfiedBy(d_tds, tnp))
    {
      Trace("sygus-sb-debug") << "...success!" << std::endl;
      Trace("sygus-sb-simple")
          << "  sb-simple : do not consider " << k << " as arg " << arg
          << " of " << pk << std::endl;
      // do not need to consider the kind in the search since there are ways to
      // construct equivalent terms
      return false;
    }
    else
    {
      Trace("sygus-sb-debug") << "...failed." << std::endl;
    }
    Trace("sygus-sb-debug") << std::endl;
  }
  // must consider this kind in the search
  return true;
}

bool SygusSimpleSymBreak::considerConst(
    TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg)
{
  const DType& pdt = tnp.getDType();
  // child grammar-independent
  if (!considerConst(pdt, tnp, c, pk, arg))
  {
    return false;
  }
  // this can probably be made child grammar independent
  quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
  quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
  int pc = pti.getKindConsNum(pk);
  if (pdt[pc].getNumArgs() == 2)
  {
    Kind ok;
    int offset;
    if (quantifiers::TermUtil::hasOffsetArg(pk, arg, offset, ok))
    {
      Trace("sygus-sb-simple-debug")
          << pk << " has offset arg " << ok << " " << offset << std::endl;
      int ok_arg = pti.getKindConsNum(ok);
      if (ok_arg != -1)
      {
        Trace("sygus-sb-simple-debug")
            << "...at argument " << ok_arg << std::endl;
        // other operator be the same type
        if (d_tds->isTypeMatch(pdt[ok_arg], pdt[arg]))
        {
          int status;
          Node co = quantifiers::TermUtil::mkTypeValueOffset(
              c.getType(), c, offset, status);
          Trace("sygus-sb-simple-debug")
              << c << " with offset " << offset << " is " << co
              << ", status=" << status << std::endl;
          if (status == 0 && !co.isNull())
          {
            if (ti.hasConst(co))
            {
              Trace("sygus-sb-simple")
                  << "  sb-simple : by offset reasoning, do not consider const "
                  << c;
              Trace("sygus-sb-simple")
                  << " as arg " << arg << " of " << pk << " since we can use "
                  << co << " under " << ok << " " << std::endl;
              return false;
            }
          }
        }
      }
    }
  }
  return true;
}

bool SygusSimpleSymBreak::considerConst(
    const DType& pdt, TypeNode tnp, Node c, Kind pk, int arg)
{
  quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
  Assert(pti.hasKind(pk));
  int pc = pti.getKindConsNum(pk);
  bool ret = true;
  Trace("sygus-sb-debug") << "Consider sygus const " << c << ", parent = " << pk
                          << ", arg = " << arg << "?" << std::endl;
  if (quantifiers::TermUtil::isIdempotentArg(c, pk, arg))
  {
    if (pdt[pc].getNumArgs() == 2)
    {
      int oarg = arg == 0 ? 1 : 0;
      TypeNode otn = pdt[pc].getArgType(oarg);
      if (otn == tnp)
      {
        Trace("sygus-sb-simple")
            << "  sb-simple : " << c << " is idempotent arg " << arg << " of "
            << pk << "..." << std::endl;
        ret = false;
      }
    }
  }
  else
  {
    Node sc = quantifiers::TermUtil::isSingularArg(c, pk, arg);
    if (!sc.isNull())
    {
      if (pti.hasConst(sc))
      {
        Trace("sygus-sb-simple")
            << "  sb-simple : " << c << " is singular arg " << arg << " of "
            << pk << ", evaluating to " << sc << "..." << std::endl;
        ret = false;
      }
    }
  }
  if (ret)
  {
    ReqTrie rt;
    Assert(rt.empty());
    Node max_c = quantifiers::TermUtil::mkTypeMaxValue(c.getType());
    Node zero_c = quantifiers::TermUtil::mkTypeValue(c.getType(), 0);
    Node one_c = quantifiers::TermUtil::mkTypeValue(c.getType(), 1);
    if (pk == XOR || pk == BITVECTOR_XOR)
    {
      if (c == max_c)
      {
        rt.d_req_kind = pk == XOR ? NOT : BITVECTOR_NOT;
      }
    }
    else if (pk == ITE)
    {
      if (arg == 0)
      {
        if (c == max_c)
        {
          rt.d_children[1].d_req_type = tnp;
        }
        else if (c == zero_c)
        {
          rt.d_children[2].d_req_type = tnp;
        }
      }
    }
    else if (pk == STRING_SUBSTR)
    {
      if (c == one_c && arg == 2)
      {
        rt.d_req_kind = STRING_CHARAT;
        rt.d_children[0].d_req_type = pdt[pc].getArgType(0);
        rt.d_children[1].d_req_type = pdt[pc].getArgType(1);
      }
    }
    if (!rt.empty())
    {
      // check if satisfied
      if (rt.satisfiedBy(d_tds, tnp))
      {
        Trace("sygus-sb-simple") << "  sb-simple : do not consider const " << c
                                 << " as arg " << arg << " of " << pk;
        Trace("sygus-sb-simple") << " in " << pdt.getName() << std::endl;
        // do not need to consider the constant in the search since there are
        // ways to construct equivalent terms
        ret = false;
      }
    }
  }
  return ret;
}

int SygusSimpleSymBreak::solveForArgument(TypeNode tn,
                                          unsigned cindex,
                                          unsigned arg)
{
  // we currently do not solve for arguments
  return -1;
}

int SygusSimpleSymBreak::getFirstArgOccurrence(const DTypeConstructor& c,
                                               TypeNode tn)
{
  for (unsigned i = 0, nargs = c.getNumArgs(); i < nargs; i++)
  {
    if (c.getArgType(i) == tn)
    {
      return i;
    }
  }
  return -1;
}

}  // 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, Haniel Barbosa, Mathias Preiner
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 simple symmetry breaking for sygus.
14		*/
15
16		#include "theory/datatypes/sygus_simple_sym.h"
17
18		#include "expr/dtype_cons.h"
19		#include "theory/quantifiers/term_util.h"
20		#include "util/rational.h"
21
22		using namespace std;
23		using namespace cvc5::kind;
24
25		namespace cvc5 {
26		namespace theory {
27		namespace datatypes {
28
29	1900	SygusSimpleSymBreak::SygusSimpleSymBreak(quantifiers::TermDbSygus* tds)
30	1900	: d_tds(tds)
31		{
32	1900	}
33
34		/** Requirement trie
35		*
36		* This class is used to make queries about sygus grammars, including what
37		* constructors they contain, and their types.
38		*
39		* As a simple example, consider the trie:
40		* root:
41		* d_req_kind = PLUS
42		* d_children[0]:
43		* d_req_type = A
44		* d_children[1]:
45		* d_req_type = A
46		* This trie is satisfied by sygus types that have a constructor whose builtin
47		* kind is PLUS and whose argument types are both A.
48		*/
49	12138	class ReqTrie
50		{
51		public:
52	12138	ReqTrie() : d_req_kind(UNDEFINED_KIND) {}
53		/** the children of this node */
54		std::map<unsigned, ReqTrie> d_children;
55		/** the (builtin) kind required by this node */
56		Kind d_req_kind;
57		/** the type that this node is required to be */
58		TypeNode d_req_type;
59		/** the constant required by this node */
60		Node d_req_const;
61		/** print this trie */
62	7138	void print(const char* c, int indent = 0)
63		{
64	7138	if (d_req_kind != UNDEFINED_KIND)
65		{
66	2779	Trace(c) << d_req_kind << " ";
67		}
68	4359	else if (!d_req_type.isNull())
69		{
70	4341	Trace(c) << d_req_type;
71		}
72	18	else if (!d_req_const.isNull())
73		{
74	18	Trace(c) << d_req_const;
75		}
76		else
77		{
78		Trace(c) << "_";
79		}
80	7138	Trace(c) << std::endl;
81	13096	for (std::map<unsigned, ReqTrie>::iterator it = d_children.begin();
82	13096	it != d_children.end();
83		++it)
84		{
85	15080	for (int i = 0; i <= indent; i++)
86		{
87	9122	Trace(c) << " ";
88		}
89	5958	Trace(c) << it->first << " : ";
90	5958	it->second.print(c, indent + 1);
91		}
92	7138	}
93		/**
94		* Are the requirements of this trie satisfied by sygus type tn?
95		* tdb is a reference to the sygus term database.
96		*/
97	6858	bool satisfiedBy(quantifiers::TermDbSygus* tdb, TypeNode tn)
98		{
99	6858	if (!d_req_const.isNull())
100		{
101	18	quantifiers::SygusTypeInfo& sti = tdb->getTypeInfo(tn);
102	18	if (!sti.hasConst(d_req_const))
103		{
104	4	return false;
105		}
106		}
107	6854	if (!d_req_type.isNull())
108		{
109	8142	Trace("sygus-sb-debug")
110	4071	<< "- check if " << tn << " is type " << d_req_type << std::endl;
111	4071	if (tn != d_req_type)
112		{
113	40	return false;
114		}
115		}
116	6814	if (d_req_kind != UNDEFINED_KIND)
117		{
118	5362	Trace("sygus-sb-debug")
119	2681	<< "- check if " << tn << " has " << d_req_kind << std::endl;
120	5209	std::vector<TypeNode> argts;
121	2681	if (tdb->canConstructKind(tn, d_req_kind, argts))
122		{
123	8118	for (std::map<unsigned, ReqTrie>::iterator it = d_children.begin();
124	8118	it != d_children.end();
125		++it)
126		{
127	5590	if (it->first < argts.size())
128		{
129	11104	TypeNode tnc = argts[it->first];
130	5590	if (!it->second.satisfiedBy(tdb, tnc))
131		{
132	76	return false;
133		}
134		}
135		else
136		{
137		return false;
138		}
139		}
140		}
141		else
142		{
143	77	return false;
144		}
145		}
146	6661	return true;
147		}
148		/** is this the empty (trivially satisfied) trie? */
149	12369	bool empty()
150		{
151	23480	return d_req_kind == UNDEFINED_KIND && d_req_const.isNull()
152	23480	&& d_req_type.isNull() && d_children.empty();
153		}
154		};
155
156	4458	bool SygusSimpleSymBreak::considerArgKind(
157		TypeNode tn, TypeNode tnp, Kind k, Kind pk, int arg)
158		{
159	4458	const DType& pdt = tnp.getDType();
160	4458	const DType& dt = tn.getDType();
161	4458	quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
162	4458	quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
163	4458	Assert(ti.hasKind(k));
164	4458	Assert(pti.hasKind(pk));
165	8916	Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
166	4458	<< ", arg = " << arg << " in " << tnp << "?"
167	4458	<< std::endl;
168	4458	int c = ti.getKindConsNum(k);
169	4458	int pc = pti.getKindConsNum(pk);
170		// check for associativity
171	4458	if (k == pk && quantifiers::TermUtil::isAssoc(k))
172		{
173		// if the operator is associative, then a repeated occurrence should only
174		// occur in the leftmost argument position
175	418	int firstArg = getFirstArgOccurrence(pdt[pc], tn);
176	418	Assert(firstArg != -1);
177	418	if (arg == firstArg)
178		{
179	211	return true;
180		}
181		// the argument types of the child must be the parent's type
182	601	for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
183		{
184	798	TypeNode type = dt[c].getArgType(i);
185	404	if (type != tnp)
186		{
187	10	return true;
188		}
189		}
190	394	Trace("sygus-sb-simple")
191	197	<< " sb-simple : do not consider " << k << " at child arg " << arg
192	197	<< " of " << k
193	197	<< " since it is associative, with first arg = " << firstArg
194	197	<< std::endl;
195	197	return false;
196		}
197		// describes the shape of an alternate term to construct
198		// we check whether this term is in the sygus grammar below
199	8080	ReqTrie rt;
200	4040	Assert(rt.empty());
201
202		// construct rt by cases
203	4040	if (pk == NOT \|\| pk == BITVECTOR_NOT \|\| pk == UMINUS \|\| pk == BITVECTOR_NEG)
204		{
205		// negation normal form
206	220	if (pk == k)
207		{
208	35	rt.d_req_type = dt[c].getArgType(0);
209		}
210		else
211		{
212	185	Kind reqk = UNDEFINED_KIND; // required kind for all children
213	370	std::map<unsigned, Kind> reqkc; // required kind for some children
214	185	if (pk == NOT)
215		{
216	111	if (k == AND)
217		{
218	27	rt.d_req_kind = OR;
219	27	reqk = NOT;
220		}
221	84	else if (k == OR)
222		{
223	25	rt.d_req_kind = AND;
224	25	reqk = NOT;
225		}
226	59	else if (k == EQUAL)
227		{
228	25	rt.d_req_kind = XOR;
229		}
230	34	else if (k == XOR)
231		{
232	4	rt.d_req_kind = EQUAL;
233		}
234	30	else if (k == ITE)
235		{
236	2	rt.d_req_kind = ITE;
237	2	reqkc[1] = NOT;
238	2	reqkc[2] = NOT;
239	2	rt.d_children[0].d_req_type = dt[c].getArgType(0);
240		}
241	28	else if (k == LEQ \|\| k == GT)
242		{
243		// (not (~ x y)) -----> (~ (+ y 1) x)
244	18	rt.d_req_kind = k;
245	18	rt.d_children[0].d_req_kind = PLUS;
246	18	rt.d_children[0].d_children[0].d_req_type = dt[c].getArgType(1);
247	36	rt.d_children[0].d_children[1].d_req_const =
248	54	NodeManager::currentNM()->mkConst(Rational(1));
249	18	rt.d_children[1].d_req_type = dt[c].getArgType(0);
250		}
251	10	else if (k == LT \|\| k == GEQ)
252		{
253		// (not (~ x y)) -----> (~ y (+ x 1))
254		rt.d_req_kind = k;
255		rt.d_children[0].d_req_type = dt[c].getArgType(1);
256		rt.d_children[1].d_req_kind = PLUS;
257		rt.d_children[1].d_children[0].d_req_type = dt[c].getArgType(0);
258		rt.d_children[1].d_children[1].d_req_const =
259		NodeManager::currentNM()->mkConst(Rational(1));
260		}
261		}
262	74	else if (pk == BITVECTOR_NOT)
263		{
264	44	if (k == BITVECTOR_AND)
265		{
266	4	rt.d_req_kind = BITVECTOR_OR;
267	4	reqk = BITVECTOR_NOT;
268		}
269	40	else if (k == BITVECTOR_OR)
270		{
271	4	rt.d_req_kind = BITVECTOR_AND;
272	4	reqk = BITVECTOR_NOT;
273		}
274	36	else if (k == BITVECTOR_XNOR)
275		{
276		rt.d_req_kind = BITVECTOR_XOR;
277		}
278	36	else if (k == BITVECTOR_XOR)
279		{
280	4	rt.d_req_kind = BITVECTOR_XNOR;
281		}
282		}
283	30	else if (pk == UMINUS)
284		{
285		if (k == PLUS)
286		{
287		rt.d_req_kind = PLUS;
288		reqk = UMINUS;
289		}
290		}
291	30	else if (pk == BITVECTOR_NEG)
292		{
293	30	if (k == PLUS)
294		{
295		rt.d_req_kind = PLUS;
296		reqk = BITVECTOR_NEG;
297		}
298		}
299	185	if (!rt.empty() && (reqk != UNDEFINED_KIND \|\| !reqkc.empty()))
300		{
301	62	int pcr = pti.getKindConsNum(rt.d_req_kind);
302	62	if (pcr != -1)
303		{
304	56	Assert(pcr < static_cast<int>(pdt.getNumConstructors()));
305		// must have same number of arguments
306	56	if (pdt[pcr].getNumArgs() == dt[c].getNumArgs())
307		{
308	170	for (unsigned i = 0, nargs = pdt[pcr].getNumArgs(); i < nargs; i++)
309		{
310	114	Kind rk = reqk;
311	114	if (reqk == UNDEFINED_KIND)
312		{
313	6	std::map<unsigned, Kind>::iterator itr = reqkc.find(i);
314	6	if (itr != reqkc.end())
315		{
316	4	rk = itr->second;
317		}
318		}
319	114	if (rk != UNDEFINED_KIND)
320		{
321	112	rt.d_children[i].d_req_kind = rk;
322	112	rt.d_children[i].d_children[0].d_req_type = dt[c].getArgType(i);
323		}
324		}
325		}
326		}
327		}
328	220	}
329		}
330	3820	else if (k == MINUS \|\| k == BITVECTOR_SUB)
331		{
332	568	if (pk == EQUAL \|\| pk == MINUS \|\| pk == BITVECTOR_SUB \|\| pk == LEQ
333	230	\|\| pk == LT \|\| pk == GEQ \|\| pk == GT)
334		{
335	338	int oarg = arg == 0 ? 1 : 0;
336		// (~ x (- y z)) ----> (~ (+ x z) y)
337		// (~ (- y z) x) ----> (~ y (+ x z))
338	338	rt.d_req_kind = pk;
339	338	rt.d_children[arg].d_req_type = dt[c].getArgType(0);
340	338	rt.d_children[oarg].d_req_kind = k == MINUS ? PLUS : BITVECTOR_ADD;
341	338	rt.d_children[oarg].d_children[0].d_req_type = pdt[pc].getArgType(oarg);
342	338	rt.d_children[oarg].d_children[1].d_req_type = dt[c].getArgType(1);
343		}
344	230	else if (pk == PLUS \|\| pk == BITVECTOR_ADD)
345		{
346		// (+ x (- y z)) -----> (- (+ x y) z)
347		// (+ (- y z) x) -----> (- (+ x y) z)
348	114	rt.d_req_kind = pk == PLUS ? MINUS : BITVECTOR_SUB;
349	114	int oarg = arg == 0 ? 1 : 0;
350	114	rt.d_children[0].d_req_kind = pk;
351	114	rt.d_children[0].d_children[0].d_req_type = pdt[pc].getArgType(oarg);
352	114	rt.d_children[0].d_children[1].d_req_type = dt[c].getArgType(0);
353	114	rt.d_children[1].d_req_type = dt[c].getArgType(1);
354	568	}
355		}
356	3252	else if (k == ITE)
357		{
358	652	if (pk != ITE)
359		{
360		// (o X (ite y z w) X') -----> (ite y (o X z X') (o X w X'))
361	526	rt.d_req_kind = ITE;
362	526	rt.d_children[0].d_req_type = dt[c].getArgType(0);
363	526	unsigned n_args = pdt[pc].getNumArgs();
364	1578	for (unsigned r = 1; r <= 2; r++)
365		{
366	1052	rt.d_children[r].d_req_kind = pk;
367	3164	for (unsigned q = 0; q < n_args; q++)
368		{
369	2112	if ((int)q == arg)
370		{
371	1052	rt.d_children[r].d_children[q].d_req_type = dt[c].getArgType(r);
372		}
373		else
374		{
375	1060	rt.d_children[r].d_children[q].d_req_type = pdt[pc].getArgType(q);
376		}
377		}
378		}
379		// this increases term size but is probably a good idea
380		}
381		}
382	2600	else if (k == NOT)
383		{
384	250	if (pk == ITE)
385		{
386		// (ite (not y) z w) -----> (ite y w z)
387	54	rt.d_req_kind = ITE;
388	54	rt.d_children[0].d_req_type = dt[c].getArgType(0);
389	54	rt.d_children[1].d_req_type = pdt[pc].getArgType(2);
390	54	rt.d_children[2].d_req_type = pdt[pc].getArgType(1);
391		}
392		}
393	8080	Trace("sygus-sb-debug") << "Consider sygus arg kind " << k << ", pk = " << pk
394	4040	<< ", arg = " << arg << "?" << std::endl;
395	4040	if (!rt.empty())
396		{
397	1180	rt.print("sygus-sb-debug");
398		// check if it meets the requirements
399	1180	if (rt.satisfiedBy(d_tds, tnp))
400		{
401	1059	Trace("sygus-sb-debug") << "...success!" << std::endl;
402	2118	Trace("sygus-sb-simple")
403	1059	<< " sb-simple : do not consider " << k << " as arg " << arg
404	1059	<< " of " << pk << std::endl;
405		// do not need to consider the kind in the search since there are ways to
406		// construct equivalent terms
407	1059	return false;
408		}
409		else
410		{
411	121	Trace("sygus-sb-debug") << "...failed." << std::endl;
412		}
413	121	Trace("sygus-sb-debug") << std::endl;
414		}
415		// must consider this kind in the search
416	2981	return true;
417		}
418
419	2544	bool SygusSimpleSymBreak::considerConst(
420		TypeNode tn, TypeNode tnp, Node c, Kind pk, int arg)
421		{
422	2544	const DType& pdt = tnp.getDType();
423		// child grammar-independent
424	2544	if (!considerConst(pdt, tnp, c, pk, arg))
425		{
426	580	return false;
427		}
428		// this can probably be made child grammar independent
429	1964	quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
430	1964	quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
431	1964	int pc = pti.getKindConsNum(pk);
432	1964	if (pdt[pc].getNumArgs() == 2)
433		{
434		Kind ok;
435		int offset;
436	1592	if (quantifiers::TermUtil::hasOffsetArg(pk, arg, offset, ok))
437		{
438	88	Trace("sygus-sb-simple-debug")
439	44	<< pk << " has offset arg " << ok << " " << offset << std::endl;
440	44	int ok_arg = pti.getKindConsNum(ok);
441	44	if (ok_arg != -1)
442		{
443	16	Trace("sygus-sb-simple-debug")
444	8	<< "...at argument " << ok_arg << std::endl;
445		// other operator be the same type
446	8	if (d_tds->isTypeMatch(pdt[ok_arg], pdt[arg]))
447		{
448		int status;
449		Node co = quantifiers::TermUtil::mkTypeValueOffset(
450	12	c.getType(), c, offset, status);
451	16	Trace("sygus-sb-simple-debug")
452	8	<< c << " with offset " << offset << " is " << co
453	8	<< ", status=" << status << std::endl;
454	8	if (status == 0 && !co.isNull())
455		{
456	8	if (ti.hasConst(co))
457		{
458	8	Trace("sygus-sb-simple")
459	4	<< " sb-simple : by offset reasoning, do not consider const "
460	4	<< c;
461	8	Trace("sygus-sb-simple")
462	4	<< " as arg " << arg << " of " << pk << " since we can use "
463	4	<< co << " under " << ok << " " << std::endl;
464	4	return false;
465		}
466		}
467		}
468		}
469		}
470		}
471	1960	return true;
472		}
473
474	2544	bool SygusSimpleSymBreak::considerConst(
475		const DType& pdt, TypeNode tnp, Node c, Kind pk, int arg)
476		{
477	2544	quantifiers::SygusTypeInfo& pti = d_tds->getTypeInfo(tnp);
478	2544	Assert(pti.hasKind(pk));
479	2544	int pc = pti.getKindConsNum(pk);
480	2544	bool ret = true;
481	5088	Trace("sygus-sb-debug") << "Consider sygus const " << c << ", parent = " << pk
482	2544	<< ", arg = " << arg << "?" << std::endl;
483	2544	if (quantifiers::TermUtil::isIdempotentArg(c, pk, arg))
484		{
485	326	if (pdt[pc].getNumArgs() == 2)
486		{
487	326	int oarg = arg == 0 ? 1 : 0;
488	652	TypeNode otn = pdt[pc].getArgType(oarg);
489	326	if (otn == tnp)
490		{
491	564	Trace("sygus-sb-simple")
492	282	<< " sb-simple : " << c << " is idempotent arg " << arg << " of "
493	282	<< pk << "..." << std::endl;
494	282	ret = false;
495		}
496		}
497		}
498		else
499		{
500	4436	Node sc = quantifiers::TermUtil::isSingularArg(c, pk, arg);
501	2218	if (!sc.isNull())
502		{
503	238	if (pti.hasConst(sc))
504		{
505	420	Trace("sygus-sb-simple")
506	210	<< " sb-simple : " << c << " is singular arg " << arg << " of "
507	210	<< pk << ", evaluating to " << sc << "..." << std::endl;
508	210	ret = false;
509		}
510		}
511		}
512	2544	if (ret)
513		{
514	4104	ReqTrie rt;
515	2052	Assert(rt.empty());
516	4104	Node max_c = quantifiers::TermUtil::mkTypeMaxValue(c.getType());
517	4104	Node zero_c = quantifiers::TermUtil::mkTypeValue(c.getType(), 0);
518	4104	Node one_c = quantifiers::TermUtil::mkTypeValue(c.getType(), 1);
519	2052	if (pk == XOR \|\| pk == BITVECTOR_XOR)
520		{
521	8	if (c == max_c)
522		{
523		rt.d_req_kind = pk == XOR ? NOT : BITVECTOR_NOT;
524		}
525		}
526	2048	else if (pk == ITE)
527		{
528	348	if (arg == 0)
529		{
530	88	if (c == max_c)
531		{
532	44	rt.d_children[1].d_req_type = tnp;
533		}
534	44	else if (c == zero_c)
535		{
536	44	rt.d_children[2].d_req_type = tnp;
537		}
538		}
539		}
540	1700	else if (pk == STRING_SUBSTR)
541		{
542		if (c == one_c && arg == 2)
543		{
544		rt.d_req_kind = STRING_CHARAT;
545		rt.d_children[0].d_req_type = pdt[pc].getArgType(0);
546		rt.d_children[1].d_req_type = pdt[pc].getArgType(1);
547		}
548		}
549	2052	if (!rt.empty())
550		{
551		// check if satisfied
552	88	if (rt.satisfiedBy(d_tds, tnp))
553		{
554	176	Trace("sygus-sb-simple") << " sb-simple : do not consider const " << c
555	88	<< " as arg " << arg << " of " << pk;
556	88	Trace("sygus-sb-simple") << " in " << pdt.getName() << std::endl;
557		// do not need to consider the constant in the search since there are
558		// ways to construct equivalent terms
559	88	ret = false;
560		}
561		}
562		}
563	2544	return ret;
564		}
565
566	4641	int SygusSimpleSymBreak::solveForArgument(TypeNode tn,
567		unsigned cindex,
568		unsigned arg)
569		{
570		// we currently do not solve for arguments
571	4641	return -1;
572		}
573
574	418	int SygusSimpleSymBreak::getFirstArgOccurrence(const DTypeConstructor& c,
575		TypeNode tn)
576		{
577	418	for (unsigned i = 0, nargs = c.getNumArgs(); i < nargs; i++)
578		{
579	418	if (c.getArgType(i) == tn)
580		{
581	418	return i;
582		}
583		}
584		return -1;
585		}
586
587		} // namespace datatypes
588		} // namespace theory
589	31137	} // namespace cvc5