Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/term_util.cpp	Lines:	262	309	84.8 %
Date:	2021-05-22	Branches:	569	1022	55.7 %


/******************************************************************************
 * 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 term utilities class.
 */

#include "theory/quantifiers/term_util.h"

#include "expr/node_algorithm.h"
#include "theory/arith/arith_msum.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_enumeration.h"
#include "theory/strings/word.h"
#include "theory/rewriter.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

size_t TermUtil::getVariableNum(Node q, Node v)
{
  Node::iterator it = std::find(q[0].begin(), q[0].end(), v);
  Assert(it != q[0].end());
  return it - q[0].begin();
}

Node TermUtil::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ) {
  std::map< Node, Node >::iterator it = visited.find( n );
  if( it!=visited.end() ){
    return it->second;
  }else{
    Node ret = n;
    if( n.getKind()==FORALL ){
      ret = getRemoveQuantifiers2( n[1], visited );
    }else if( n.getNumChildren()>0 ){
      std::vector< Node > children;
      bool childrenChanged = false;
      for( unsigned i=0; i<n.getNumChildren(); i++ ){
        Node ni = getRemoveQuantifiers2( n[i], visited );
        childrenChanged = childrenChanged || ni!=n[i];
        children.push_back( ni );
      }
      if( childrenChanged ){
        if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
          children.insert( children.begin(), n.getOperator() );
        }
        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
      }
    }
    visited[n] = ret;
    return ret;
  }
}

Node TermUtil::getInstConstAttr( Node n ) {
  if (!n.hasAttribute(InstConstantAttribute()) ){
    Node q;
    if (n.hasOperator())
    {
      q = getInstConstAttr(n.getOperator());
    }
    if (q.isNull())
    {
      for (const Node& nc : n)
      {
        q = getInstConstAttr(nc);
        if (!q.isNull())
        {
          break;
        }
      }
    }
    InstConstantAttribute ica;
    n.setAttribute(ica, q);
  }
  return n.getAttribute(InstConstantAttribute());
}

bool TermUtil::hasInstConstAttr( Node n ) {
  return !getInstConstAttr(n).isNull();
}

Node TermUtil::getBoundVarAttr( Node n ) {
  if (!n.hasAttribute(BoundVarAttribute()) ){
    Node bv;
    if( n.getKind()==BOUND_VARIABLE ){
      bv = n;
    }else{
      for( unsigned i=0; i<n.getNumChildren(); i++ ){
        bv = getBoundVarAttr(n[i]);
        if( !bv.isNull() ){
          break;
        }
      }
    }
    BoundVarAttribute bva;
    n.setAttribute(bva, bv);
  }
  return n.getAttribute(BoundVarAttribute());
}

bool TermUtil::hasBoundVarAttr( Node n ) {
  return !getBoundVarAttr(n).isNull();
}

//remove quantifiers
Node TermUtil::getRemoveQuantifiers( Node n ) {
  std::map< Node, Node > visited;
  return getRemoveQuantifiers2( n, visited );
}

//quantified simplify
Node TermUtil::getQuantSimplify( Node n ) {
  std::unordered_set<Node> fvs;
  expr::getFreeVariables(n, fvs);
  if (fvs.empty())
  {
    return Rewriter::rewrite( n );
  }
  std::vector<Node> bvs;
  bvs.insert(bvs.end(), fvs.begin(), fvs.end());
  NodeManager* nm = NodeManager::currentNM();
  Node q = nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, bvs), n);
  q = Rewriter::rewrite(q);
  return getRemoveQuantifiers(q);
}

void TermUtil::computeInstConstContains(Node n, std::vector<Node>& ics)
{
  computeVarContainsInternal(n, INST_CONSTANT, ics);
}

void TermUtil::computeVarContains(Node n, std::vector<Node>& vars)
{
  computeVarContainsInternal(n, BOUND_VARIABLE, vars);
}

void TermUtil::computeQuantContains(Node n, std::vector<Node>& quants)
{
  computeVarContainsInternal(n, FORALL, quants);
}

void TermUtil::computeVarContainsInternal(Node n,
                                          Kind k,
                                          std::vector<Node>& vars)
{
  std::unordered_set<TNode> visited;
  std::unordered_set<TNode>::iterator it;
  std::vector<TNode> visit;
  TNode cur;
  visit.push_back(n);
  do
  {
    cur = visit.back();
    visit.pop_back();
    it = visited.find(cur);

    if (it == visited.end())
    {
      visited.insert(cur);
      if (cur.getKind() == k)
      {
        if (std::find(vars.begin(), vars.end(), cur) == vars.end())
        {
          vars.push_back(cur);
        }
      }
      else
      {
        if (cur.hasOperator())
        {
          visit.push_back(cur.getOperator());
        }
        for (const Node& cn : cur)
        {
          visit.push_back(cn);
        }
      }
    }
  } while (!visit.empty());
}

void TermUtil::computeInstConstContainsForQuant(Node q,
                                                Node n,
                                                std::vector<Node>& vars)
{
  std::vector<Node> ics;
  computeInstConstContains(n, ics);
  for (const Node& v : ics)
  {
    if (v.getAttribute(InstConstantAttribute()) == q)
    {
      if (std::find(vars.begin(), vars.end(), v) == vars.end())
      {
        vars.push_back(v);
      }
    }
  }
}

int TermUtil::getTermDepth( Node n ) {
  if (!n.hasAttribute(TermDepthAttribute()) ){
    int maxDepth = -1;
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
      int depth = getTermDepth( n[i] );
      if( depth>maxDepth ){
        maxDepth = depth;
      }
    }
    TermDepthAttribute tda;
    n.setAttribute(tda,1+maxDepth);
  }
  return n.getAttribute(TermDepthAttribute());
}

bool TermUtil::containsUninterpretedConstant( Node n ) {
  if (!n.hasAttribute(ContainsUConstAttribute()) ){
    bool ret = false;
    if( n.getKind()==UNINTERPRETED_CONSTANT ){
      ret = true;
    }else{
      for( unsigned i=0; i<n.getNumChildren(); i++ ){
        if( containsUninterpretedConstant( n[i] ) ){
          ret = true;
          break;
        }
      }
    }
    ContainsUConstAttribute cuca;
    n.setAttribute(cuca, ret ? 1 : 0);
  }
  return n.getAttribute(ContainsUConstAttribute())!=0;
}

Node TermUtil::simpleNegate(Node n)
{
  Assert(n.getType().isBoolean());
  NodeManager* nm = NodeManager::currentNM();
  if( n.getKind()==OR || n.getKind()==AND ){
    std::vector< Node > children;
    for (const Node& cn : n)
    {
      children.push_back(simpleNegate(cn));
    }
    return nm->mkNode(n.getKind() == OR ? AND : OR, children);
  }
  else if (n.isConst())
  {
    return nm->mkConst(!n.getConst<bool>());
  }
  return n.negate();
}

Node TermUtil::mkNegate(Kind notk, Node n)
{
  if (n.getKind() == notk)
  {
    return n[0];
  }
  return NodeManager::currentNM()->mkNode(notk, n);
}

bool TermUtil::isNegate(Kind k)
{
  return k == NOT || k == BITVECTOR_NOT || k == BITVECTOR_NEG || k == UMINUS;
}

bool TermUtil::isAssoc(Kind k, bool reqNAry)
{
  if (reqNAry)
  {
    if (k == UNION || k == INTERSECTION)
    {
      return false;
    }
  }
  return k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR
         || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT
         || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR
         || k == BITVECTOR_XNOR || k == BITVECTOR_CONCAT || k == STRING_CONCAT
         || k == UNION || k == INTERSECTION || k == JOIN || k == PRODUCT
         || k == SEP_STAR;
}

bool TermUtil::isComm(Kind k, bool reqNAry)
{
  if (reqNAry)
  {
    if (k == UNION || k == INTERSECTION)
    {
      return false;
    }
  }
  return k == EQUAL || k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND
         || k == OR || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT
         || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR
         || k == BITVECTOR_XNOR || k == UNION || k == INTERSECTION
         || k == SEP_STAR;
}

bool TermUtil::isNonAdditive( Kind k ) {
  return k==AND || k==OR || k==BITVECTOR_AND || k==BITVECTOR_OR;
}

bool TermUtil::isBoolConnective( Kind k ) {
  return k==OR || k==AND || k==EQUAL || k==ITE || k==FORALL || k==NOT || k==SEP_STAR;
}

bool TermUtil::isBoolConnectiveTerm( TNode n ) {
  return isBoolConnective( n.getKind() ) &&
         ( n.getKind()!=EQUAL || n[0].getType().isBoolean() ) &&
         ( n.getKind()!=ITE || n.getType().isBoolean() );
}

Node TermUtil::mkTypeValue(TypeNode tn, int32_t val)
{
  Node n;
  if (tn.isInteger() || tn.isReal())
  {
    Rational c(val);
    n = NodeManager::currentNM()->mkConst(c);
  }
  else if (tn.isBitVector())
  {
    // cast to unsigned
    uint32_t uv = static_cast<uint32_t>(val);
    BitVector bval(tn.getConst<BitVectorSize>(), uv);
    n = NodeManager::currentNM()->mkConst<BitVector>(bval);
  }
  else if (tn.isBoolean())
  {
    if (val == 0)
    {
      n = NodeManager::currentNM()->mkConst(false);
    }
  }
  else if (tn.isStringLike())
  {
    if (val == 0)
    {
      n = strings::Word::mkEmptyWord(tn);
    }
  }
  return n;
}

Node TermUtil::mkTypeMaxValue(TypeNode tn)
{
  Node n;
  if (tn.isBitVector())
  {
    n = bv::utils::mkOnes(tn.getConst<BitVectorSize>());
  }
  else if (tn.isBoolean())
  {
    n = NodeManager::currentNM()->mkConst(true);
  }
  return n;
}

Node TermUtil::mkTypeValueOffset(TypeNode tn,
                                 Node val,
                                 int32_t offset,
                                 int32_t& status)
{
  Node val_o;
  Node offset_val = mkTypeValue(tn, offset);
  status = -1;
  if (!offset_val.isNull())
  {
    if (tn.isInteger() || tn.isReal())
    {
      val_o = Rewriter::rewrite(
          NodeManager::currentNM()->mkNode(PLUS, val, offset_val));
      status = 0;
    }
    else if (tn.isBitVector())
    {
      val_o = Rewriter::rewrite(
          NodeManager::currentNM()->mkNode(BITVECTOR_ADD, val, offset_val));
    }
  }
  return val_o;
}

Node TermUtil::mkTypeConst(TypeNode tn, bool pol)
{
  return pol ? mkTypeMaxValue(tn) : mkTypeValue(tn, 0);
}

bool TermUtil::isAntisymmetric(Kind k, Kind& dk)
{
  if (k == GT)
  {
    dk = LT;
    return true;
  }
  else if (k == GEQ)
  {
    dk = LEQ;
    return true;
  }
  else if (k == BITVECTOR_UGT)
  {
    dk = BITVECTOR_ULT;
    return true;
  }
  else if (k == BITVECTOR_UGE)
  {
    dk = BITVECTOR_ULE;
    return true;
  }
  else if (k == BITVECTOR_SGT)
  {
    dk = BITVECTOR_SLT;
    return true;
  }
  else if (k == BITVECTOR_SGE)
  {
    dk = BITVECTOR_SLE;
    return true;
  }
  return false;
}

bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg)
{
  // these should all be binary operators
  // Assert( ik!=DIVISION && ik!=INTS_DIVISION && ik!=INTS_MODULUS &&
  // ik!=BITVECTOR_UDIV );
  TypeNode tn = n.getType();
  if (n == mkTypeValue(tn, 0))
  {
    if (ik == PLUS || ik == OR || ik == XOR || ik == BITVECTOR_ADD
        || ik == BITVECTOR_OR || ik == BITVECTOR_XOR || ik == STRING_CONCAT)
    {
      return true;
    }
    else if (ik == MINUS || ik == BITVECTOR_SHL || ik == BITVECTOR_LSHR
             || ik == BITVECTOR_ASHR || ik == BITVECTOR_SUB
             || ik == BITVECTOR_UREM)
    {
      return arg == 1;
    }
  }
  else if (n == mkTypeValue(tn, 1))
  {
    if (ik == MULT || ik == BITVECTOR_MULT)
    {
      return true;
    }
    else if (ik == DIVISION || ik == DIVISION_TOTAL || ik == INTS_DIVISION
             || ik == INTS_DIVISION_TOTAL
             || ik == INTS_MODULUS
             || ik == INTS_MODULUS_TOTAL
             || ik == BITVECTOR_UDIV
             || ik == BITVECTOR_SDIV)
    {
      return arg == 1;
    }
  }
  else if (n == mkTypeMaxValue(tn))
  {
    if (ik == EQUAL || ik == BITVECTOR_AND || ik == BITVECTOR_XNOR)
    {
      return true;
    }
  }
  return false;
}

Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
{
  TypeNode tn = n.getType();
  if (n == mkTypeValue(tn, 0))
  {
    if (ik == AND || ik == MULT || ik == BITVECTOR_AND || ik == BITVECTOR_MULT)
    {
      return n;
    }
    else if (ik == BITVECTOR_SHL || ik == BITVECTOR_LSHR || ik == BITVECTOR_ASHR
             || ik == BITVECTOR_UREM)
    {
      if (arg == 0)
      {
        return n;
      }
    }
    else if (ik == BITVECTOR_UDIV || ik == BITVECTOR_UDIV
             || ik == BITVECTOR_SDIV)
    {
      if (arg == 0)
      {
        return n;
      }
      else if (arg == 1)
      {
        return mkTypeMaxValue(tn);
      }
    }
    else if (ik == DIVISION || ik == DIVISION_TOTAL || ik == INTS_DIVISION
             || ik == INTS_DIVISION_TOTAL
             || ik == INTS_MODULUS
             || ik == INTS_MODULUS_TOTAL)
    {
      if (arg == 0)
      {
        return n;
      }
    }
    else if (ik == STRING_SUBSTR)
    {
      if (arg == 0)
      {
        return n;
      }
      else if (arg == 2)
      {
        return mkTypeValue(NodeManager::currentNM()->stringType(), 0);
      }
    }
    else if (ik == STRING_STRIDOF)
    {
      if (arg == 0 || arg == 1)
      {
        return mkTypeValue(NodeManager::currentNM()->integerType(), -1);
      }
    }
  }
  else if (n == mkTypeValue(tn, 1))
  {
    if (ik == BITVECTOR_UREM)
    {
      return mkTypeValue(tn, 0);
    }
  }
  else if (n == mkTypeMaxValue(tn))
  {
    if (ik == OR || ik == BITVECTOR_OR)
    {
      return n;
    }
  }
  else
  {
    if (n.getType().isReal() && n.getConst<Rational>().sgn() < 0)
    {
      // negative arguments
      if (ik == STRING_SUBSTR || ik == STRING_CHARAT)
      {
        return mkTypeValue(NodeManager::currentNM()->stringType(), 0);
      }
      else if (ik == STRING_STRIDOF)
      {
        Assert(arg == 2);
        return mkTypeValue(NodeManager::currentNM()->integerType(), -1);
      }
    }
  }
  return Node::null();
}

bool TermUtil::hasOffsetArg(Kind ik, int arg, int& offset, Kind& ok)
{
  if (ik == LT)
  {
    Assert(arg == 0 || arg == 1);
    offset = arg == 0 ? 1 : -1;
    ok = LEQ;
    return true;
  }
  else if (ik == BITVECTOR_ULT)
  {
    Assert(arg == 0 || arg == 1);
    offset = arg == 0 ? 1 : -1;
    ok = BITVECTOR_ULE;
    return true;
  }
  else if (ik == BITVECTOR_SLT)
  {
    Assert(arg == 0 || arg == 1);
    offset = arg == 0 ? 1 : -1;
    ok = BITVECTOR_SLE;
    return true;
  }
  return false;
}

}  // namespace quantifiers
}  // 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 term utilities class.
14		*/
15
16		#include "theory/quantifiers/term_util.h"
17
18		#include "expr/node_algorithm.h"
19		#include "theory/arith/arith_msum.h"
20		#include "theory/bv/theory_bv_utils.h"
21		#include "theory/quantifiers/term_database.h"
22		#include "theory/quantifiers/term_enumeration.h"
23		#include "theory/strings/word.h"
24		#include "theory/rewriter.h"
25
26		using namespace cvc5::kind;
27
28		namespace cvc5 {
29		namespace theory {
30		namespace quantifiers {
31
32	4264	size_t TermUtil::getVariableNum(Node q, Node v)
33		{
34	4264	Node::iterator it = std::find(q[0].begin(), q[0].end(), v);
35	4264	Assert(it != q[0].end());
36	4264	return it - q[0].begin();
37		}
38
39	14500	Node TermUtil::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ) {
40	14500	std::map< Node, Node >::iterator it = visited.find( n );
41	14500	if( it!=visited.end() ){
42	6202	return it->second;
43		}else{
44	16596	Node ret = n;
45	8298	if( n.getKind()==FORALL ){
46	358	ret = getRemoveQuantifiers2( n[1], visited );
47	7940	}else if( n.getNumChildren()>0 ){
48	12152	std::vector< Node > children;
49	6076	bool childrenChanged = false;
50	19852	for( unsigned i=0; i<n.getNumChildren(); i++ ){
51	27552	Node ni = getRemoveQuantifiers2( n[i], visited );
52	13776	childrenChanged = childrenChanged \|\| ni!=n[i];
53	13776	children.push_back( ni );
54		}
55	6076	if( childrenChanged ){
56	3	if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
57		children.insert( children.begin(), n.getOperator() );
58		}
59	3	ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
60		}
61		}
62	8298	visited[n] = ret;
63	8298	return ret;
64		}
65		}
66
67	12048684	Node TermUtil::getInstConstAttr( Node n ) {
68	12048684	if (!n.hasAttribute(InstConstantAttribute()) ){
69	862604	Node q;
70	431302	if (n.hasOperator())
71		{
72	314468	q = getInstConstAttr(n.getOperator());
73		}
74	431302	if (q.isNull())
75		{
76	895384	for (const Node& nc : n)
77		{
78	565699	q = getInstConstAttr(nc);
79	565699	if (!q.isNull())
80		{
81	101553	break;
82		}
83		}
84		}
85		InstConstantAttribute ica;
86	431302	n.setAttribute(ica, q);
87		}
88	12048684	return n.getAttribute(InstConstantAttribute());
89		}
90
91	7822884	bool TermUtil::hasInstConstAttr( Node n ) {
92	7822884	return !getInstConstAttr(n).isNull();
93		}
94
95	150650	Node TermUtil::getBoundVarAttr( Node n ) {
96	150650	if (!n.hasAttribute(BoundVarAttribute()) ){
97	156026	Node bv;
98	78013	if( n.getKind()==BOUND_VARIABLE ){
99	7670	bv = n;
100		}else{
101	93140	for( unsigned i=0; i<n.getNumChildren(); i++ ){
102	78635	bv = getBoundVarAttr(n[i]);
103	78635	if( !bv.isNull() ){
104	55838	break;
105		}
106		}
107		}
108		BoundVarAttribute bva;
109	78013	n.setAttribute(bva, bv);
110		}
111	150650	return n.getAttribute(BoundVarAttribute());
112		}
113
114	72015	bool TermUtil::hasBoundVarAttr( Node n ) {
115	72015	return !getBoundVarAttr(n).isNull();
116		}
117
118		//remove quantifiers
119	366	Node TermUtil::getRemoveQuantifiers( Node n ) {
120	732	std::map< Node, Node > visited;
121	732	return getRemoveQuantifiers2( n, visited );
122		}
123
124		//quantified simplify
125	936	Node TermUtil::getQuantSimplify( Node n ) {
126	1872	std::unordered_set<Node> fvs;
127	936	expr::getFreeVariables(n, fvs);
128	936	if (fvs.empty())
129		{
130	570	return Rewriter::rewrite( n );
131		}
132	732	std::vector<Node> bvs;
133	366	bvs.insert(bvs.end(), fvs.begin(), fvs.end());
134	366	NodeManager* nm = NodeManager::currentNM();
135	732	Node q = nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, bvs), n);
136	366	q = Rewriter::rewrite(q);
137	366	return getRemoveQuantifiers(q);
138		}
139
140	161807	void TermUtil::computeInstConstContains(Node n, std::vector<Node>& ics)
141		{
142	161807	computeVarContainsInternal(n, INST_CONSTANT, ics);
143	161807	}
144
145	247	void TermUtil::computeVarContains(Node n, std::vector<Node>& vars)
146		{
147	247	computeVarContainsInternal(n, BOUND_VARIABLE, vars);
148	247	}
149
150	1582	void TermUtil::computeQuantContains(Node n, std::vector<Node>& quants)
151		{
152	1582	computeVarContainsInternal(n, FORALL, quants);
153	1582	}
154
155	163636	void TermUtil::computeVarContainsInternal(Node n,
156		Kind k,
157		std::vector<Node>& vars)
158		{
159	327272	std::unordered_set<TNode> visited;
160	163636	std::unordered_set<TNode>::iterator it;
161	327272	std::vector<TNode> visit;
162	327272	TNode cur;
163	163636	visit.push_back(n);
164	1271322	do
165		{
166	1434958	cur = visit.back();
167	1434958	visit.pop_back();
168	1434958	it = visited.find(cur);
169
170	1434958	if (it == visited.end())
171		{
172	1285964	visited.insert(cur);
173	1285964	if (cur.getKind() == k)
174		{
175	378379	if (std::find(vars.begin(), vars.end(), cur) == vars.end())
176		{
177	378379	vars.push_back(cur);
178		}
179		}
180		else
181		{
182	907585	if (cur.hasOperator())
183		{
184	425100	visit.push_back(cur.getOperator());
185		}
186	1753807	for (const Node& cn : cur)
187		{
188	846222	visit.push_back(cn);
189		}
190		}
191		}
192	1434958	} while (!visit.empty());
193	163636	}
194
195	112456	void TermUtil::computeInstConstContainsForQuant(Node q,
196		Node n,
197		std::vector<Node>& vars)
198		{
199	224912	std::vector<Node> ics;
200	112456	computeInstConstContains(n, ics);
201	377562	for (const Node& v : ics)
202		{
203	265106	if (v.getAttribute(InstConstantAttribute()) == q)
204		{
205	265106	if (std::find(vars.begin(), vars.end(), v) == vars.end())
206		{
207	265104	vars.push_back(v);
208		}
209		}
210		}
211	112456	}
212
213		int TermUtil::getTermDepth( Node n ) {
214		if (!n.hasAttribute(TermDepthAttribute()) ){
215		int maxDepth = -1;
216		for( unsigned i=0; i<n.getNumChildren(); i++ ){
217		int depth = getTermDepth( n[i] );
218		if( depth>maxDepth ){
219		maxDepth = depth;
220		}
221		}
222		TermDepthAttribute tda;
223		n.setAttribute(tda,1+maxDepth);
224		}
225		return n.getAttribute(TermDepthAttribute());
226		}
227
228	480973	bool TermUtil::containsUninterpretedConstant( Node n ) {
229	480973	if (!n.hasAttribute(ContainsUConstAttribute()) ){
230	23057	bool ret = false;
231	23057	if( n.getKind()==UNINTERPRETED_CONSTANT ){
232	833	ret = true;
233		}else{
234	42999	for( unsigned i=0; i<n.getNumChildren(); i++ ){
235	20775	if( containsUninterpretedConstant( n[i] ) ){
236		ret = true;
237		break;
238		}
239		}
240		}
241		ContainsUConstAttribute cuca;
242	23057	n.setAttribute(cuca, ret ? 1 : 0);
243		}
244	480973	return n.getAttribute(ContainsUConstAttribute())!=0;
245		}
246
247	4666	Node TermUtil::simpleNegate(Node n)
248		{
249	4666	Assert(n.getType().isBoolean());
250	4666	NodeManager* nm = NodeManager::currentNM();
251	4666	if( n.getKind()==OR \|\| n.getKind()==AND ){
252	2714	std::vector< Node > children;
253	5279	for (const Node& cn : n)
254		{
255	3922	children.push_back(simpleNegate(cn));
256		}
257	1357	return nm->mkNode(n.getKind() == OR ? AND : OR, children);
258		}
259	3309	else if (n.isConst())
260		{
261	86	return nm->mkConst(!n.getConst<bool>());
262		}
263	3223	return n.negate();
264		}
265
266	1169	Node TermUtil::mkNegate(Kind notk, Node n)
267		{
268	1169	if (n.getKind() == notk)
269		{
270	30	return n[0];
271		}
272	1139	return NodeManager::currentNM()->mkNode(notk, n);
273		}
274
275	2683	bool TermUtil::isNegate(Kind k)
276		{
277	2683	return k == NOT \|\| k == BITVECTOR_NOT \|\| k == BITVECTOR_NEG \|\| k == UMINUS;
278		}
279
280	103388	bool TermUtil::isAssoc(Kind k, bool reqNAry)
281		{
282	103388	if (reqNAry)
283		{
284	102867	if (k == UNION \|\| k == INTERSECTION)
285		{
286	39	return false;
287		}
288		}
289	88980	return k == PLUS \|\| k == MULT \|\| k == NONLINEAR_MULT \|\| k == AND \|\| k == OR
290	71081	\|\| k == XOR \|\| k == BITVECTOR_ADD \|\| k == BITVECTOR_MULT
291	66204	\|\| k == BITVECTOR_AND \|\| k == BITVECTOR_OR \|\| k == BITVECTOR_XOR
292	60041	\|\| k == BITVECTOR_XNOR \|\| k == BITVECTOR_CONCAT \|\| k == STRING_CONCAT
293	58729	\|\| k == UNION \|\| k == INTERSECTION \|\| k == JOIN \|\| k == PRODUCT
294	162074	\|\| k == SEP_STAR;
295		}
296
297	383818	bool TermUtil::isComm(Kind k, bool reqNAry)
298		{
299	383818	if (reqNAry)
300		{
301		if (k == UNION \|\| k == INTERSECTION)
302		{
303		return false;
304		}
305		}
306	323084	return k == EQUAL \|\| k == PLUS \|\| k == MULT \|\| k == NONLINEAR_MULT \|\| k == AND
307	267918	\|\| k == OR \|\| k == XOR \|\| k == BITVECTOR_ADD \|\| k == BITVECTOR_MULT
308	239003	\|\| k == BITVECTOR_AND \|\| k == BITVECTOR_OR \|\| k == BITVECTOR_XOR
309	232404	\|\| k == BITVECTOR_XNOR \|\| k == UNION \|\| k == INTERSECTION
310	616124	\|\| k == SEP_STAR;
311		}
312
313	103029	bool TermUtil::isNonAdditive( Kind k ) {
314	103029	return k==AND \|\| k==OR \|\| k==BITVECTOR_AND \|\| k==BITVECTOR_OR;
315		}
316
317	331531	bool TermUtil::isBoolConnective( Kind k ) {
318	331531	return k==OR \|\| k==AND \|\| k==EQUAL \|\| k==ITE \|\| k==FORALL \|\| k==NOT \|\| k==SEP_STAR;
319		}
320
321	280890	bool TermUtil::isBoolConnectiveTerm( TNode n ) {
322	481668	return isBoolConnective( n.getKind() ) &&
323	1170934	( n.getKind()!=EQUAL \|\| n[0].getType().isBoolean() ) &&
324	680787	( n.getKind()!=ITE \|\| n.getType().isBoolean() );
325		}
326
327	19586	Node TermUtil::mkTypeValue(TypeNode tn, int32_t val)
328		{
329	19586	Node n;
330	19586	if (tn.isInteger() \|\| tn.isReal())
331		{
332	5662	Rational c(val);
333	2831	n = NodeManager::currentNM()->mkConst(c);
334		}
335	16755	else if (tn.isBitVector())
336		{
337		// cast to unsigned
338	1343	uint32_t uv = static_cast<uint32_t>(val);
339	2686	BitVector bval(tn.getConst<BitVectorSize>(), uv);
340	1343	n = NodeManager::currentNM()->mkConst<BitVector>(bval);
341		}
342	15412	else if (tn.isBoolean())
343		{
344	15172	if (val == 0)
345		{
346	14759	n = NodeManager::currentNM()->mkConst(false);
347		}
348		}
349	240	else if (tn.isStringLike())
350		{
351	150	if (val == 0)
352		{
353	87	n = strings::Word::mkEmptyWord(tn);
354		}
355		}
356	19586	return n;
357		}
358
359	15539	Node TermUtil::mkTypeMaxValue(TypeNode tn)
360		{
361	15539	Node n;
362	15539	if (tn.isBitVector())
363		{
364	399	n = bv::utils::mkOnes(tn.getConst<BitVectorSize>());
365		}
366	15140	else if (tn.isBoolean())
367		{
368	14531	n = NodeManager::currentNM()->mkConst(true);
369		}
370	15539	return n;
371		}
372
373	4	Node TermUtil::mkTypeValueOffset(TypeNode tn,
374		Node val,
375		int32_t offset,
376		int32_t& status)
377		{
378	4	Node val_o;
379	8	Node offset_val = mkTypeValue(tn, offset);
380	4	status = -1;
381	4	if (!offset_val.isNull())
382		{
383	4	if (tn.isInteger() \|\| tn.isReal())
384		{
385	4	val_o = Rewriter::rewrite(
386	8	NodeManager::currentNM()->mkNode(PLUS, val, offset_val));
387	4	status = 0;
388		}
389		else if (tn.isBitVector())
390		{
391		val_o = Rewriter::rewrite(
392		NodeManager::currentNM()->mkNode(BITVECTOR_ADD, val, offset_val));
393		}
394		}
395	8	return val_o;
396		}
397
398	2	Node TermUtil::mkTypeConst(TypeNode tn, bool pol)
399		{
400	2	return pol ? mkTypeMaxValue(tn) : mkTypeValue(tn, 0);
401		}
402
403		bool TermUtil::isAntisymmetric(Kind k, Kind& dk)
404		{
405		if (k == GT)
406		{
407		dk = LT;
408		return true;
409		}
410		else if (k == GEQ)
411		{
412		dk = LEQ;
413		return true;
414		}
415		else if (k == BITVECTOR_UGT)
416		{
417		dk = BITVECTOR_ULT;
418		return true;
419		}
420		else if (k == BITVECTOR_UGE)
421		{
422		dk = BITVECTOR_ULE;
423		return true;
424		}
425		else if (k == BITVECTOR_SGT)
426		{
427		dk = BITVECTOR_SLT;
428		return true;
429		}
430		else if (k == BITVECTOR_SGE)
431		{
432		dk = BITVECTOR_SLE;
433		return true;
434		}
435		return false;
436		}
437
438	1207	bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg)
439		{
440		// these should all be binary operators
441		// Assert( ik!=DIVISION && ik!=INTS_DIVISION && ik!=INTS_MODULUS &&
442		// ik!=BITVECTOR_UDIV );
443	2414	TypeNode tn = n.getType();
444	1207	if (n == mkTypeValue(tn, 0))
445		{
446	566	if (ik == PLUS \|\| ik == OR \|\| ik == XOR \|\| ik == BITVECTOR_ADD
447	441	\|\| ik == BITVECTOR_OR \|\| ik == BITVECTOR_XOR \|\| ik == STRING_CONCAT)
448		{
449	144	return true;
450		}
451	422	else if (ik == MINUS \|\| ik == BITVECTOR_SHL \|\| ik == BITVECTOR_LSHR
452	368	\|\| ik == BITVECTOR_ASHR \|\| ik == BITVECTOR_SUB
453	364	\|\| ik == BITVECTOR_UREM)
454		{
455	65	return arg == 1;
456		}
457		}
458	641	else if (n == mkTypeValue(tn, 1))
459		{
460	388	if (ik == MULT \|\| ik == BITVECTOR_MULT)
461		{
462	6	return true;
463		}
464	382	else if (ik == DIVISION \|\| ik == DIVISION_TOTAL \|\| ik == INTS_DIVISION
465	378	\|\| ik == INTS_DIVISION_TOTAL
466	378	\|\| ik == INTS_MODULUS
467	378	\|\| ik == INTS_MODULUS_TOTAL
468	378	\|\| ik == BITVECTOR_UDIV
469	369	\|\| ik == BITVECTOR_SDIV)
470		{
471	22	return arg == 1;
472		}
473		}
474	253	else if (n == mkTypeMaxValue(tn))
475		{
476	174	if (ik == EQUAL \|\| ik == BITVECTOR_AND \|\| ik == BITVECTOR_XNOR)
477		{
478		return true;
479		}
480		}
481	970	return false;
482		}
483
484	1012	Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
485		{
486	2024	TypeNode tn = n.getType();
487	1012	if (n == mkTypeValue(tn, 0))
488		{
489	389	if (ik == AND \|\| ik == MULT \|\| ik == BITVECTOR_AND \|\| ik == BITVECTOR_MULT)
490		{
491	52	return n;
492		}
493	337	else if (ik == BITVECTOR_SHL \|\| ik == BITVECTOR_LSHR \|\| ik == BITVECTOR_ASHR
494	334	\|\| ik == BITVECTOR_UREM)
495		{
496	6	if (arg == 0)
497		{
498	6	return n;
499		}
500		}
501	331	else if (ik == BITVECTOR_UDIV \|\| ik == BITVECTOR_UDIV
502	322	\|\| ik == BITVECTOR_SDIV)
503		{
504	16	if (arg == 0)
505		{
506	7	return n;
507		}
508	9	else if (arg == 1)
509		{
510	9	return mkTypeMaxValue(tn);
511		}
512		}
513	315	else if (ik == DIVISION \|\| ik == DIVISION_TOTAL \|\| ik == INTS_DIVISION
514	313	\|\| ik == INTS_DIVISION_TOTAL
515	313	\|\| ik == INTS_MODULUS
516	310	\|\| ik == INTS_MODULUS_TOTAL)
517		{
518	7	if (arg == 0)
519		{
520	3	return n;
521		}
522		}
523	310	else if (ik == STRING_SUBSTR)
524		{
525		if (arg == 0)
526		{
527		return n;
528		}
529		else if (arg == 2)
530		{
531		return mkTypeValue(NodeManager::currentNM()->stringType(), 0);
532		}
533		}
534	310	else if (ik == STRING_STRIDOF)
535		{
536		if (arg == 0 \|\| arg == 1)
537		{
538		return mkTypeValue(NodeManager::currentNM()->integerType(), -1);
539		}
540		}
541		}
542	623	else if (n == mkTypeValue(tn, 1))
543		{
544	370	if (ik == BITVECTOR_UREM)
545		{
546	7	return mkTypeValue(tn, 0);
547		}
548		}
549	253	else if (n == mkTypeMaxValue(tn))
550		{
551	174	if (ik == OR \|\| ik == BITVECTOR_OR)
552		{
553	57	return n;
554		}
555		}
556		else
557		{
558	79	if (n.getType().isReal() && n.getConst<Rational>().sgn() < 0)
559		{
560		// negative arguments
561	2	if (ik == STRING_SUBSTR \|\| ik == STRING_CHARAT)
562		{
563		return mkTypeValue(NodeManager::currentNM()->stringType(), 0);
564		}
565	2	else if (ik == STRING_STRIDOF)
566		{
567		Assert(arg == 2);
568		return mkTypeValue(NodeManager::currentNM()->integerType(), -1);
569		}
570		}
571		}
572	871	return Node::null();
573		}
574
575	667	bool TermUtil::hasOffsetArg(Kind ik, int arg, int& offset, Kind& ok)
576		{
577	667	if (ik == LT)
578		{
579	4	Assert(arg == 0 \|\| arg == 1);
580	4	offset = arg == 0 ? 1 : -1;
581	4	ok = LEQ;
582	4	return true;
583		}
584	663	else if (ik == BITVECTOR_ULT)
585		{
586	12	Assert(arg == 0 \|\| arg == 1);
587	12	offset = arg == 0 ? 1 : -1;
588	12	ok = BITVECTOR_ULE;
589	12	return true;
590		}
591	651	else if (ik == BITVECTOR_SLT)
592		{
593	12	Assert(arg == 0 \|\| arg == 1);
594	12	offset = arg == 0 ? 1 : -1;
595	12	ok = BITVECTOR_SLE;
596	12	return true;
597		}
598	639	return false;
599		}
600
601		} // namespace quantifiers
602		} // namespace theory
603	28194	} // namespace cvc5