Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/term_util.cpp	Lines:	259	309	83.8 %
Date:	2021-09-30	Branches:	560	1020	54.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 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/rewriter.h"
#include "theory/strings/word.h"
#include "util/bitvector.h"
#include "util/rational.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_INDEXOF)
    {
      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_INDEXOF)
      {
        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/rewriter.h"
24		#include "theory/strings/word.h"
25		#include "util/bitvector.h"
26		#include "util/rational.h"
27
28		using namespace cvc5::kind;
29
30		namespace cvc5 {
31		namespace theory {
32		namespace quantifiers {
33
34	5388	size_t TermUtil::getVariableNum(Node q, Node v)
35		{
36	5388	Node::iterator it = std::find(q[0].begin(), q[0].end(), v);
37	5388	Assert(it != q[0].end());
38	5388	return it - q[0].begin();
39		}
40
41	16370	Node TermUtil::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ) {
42	16370	std::map< Node, Node >::iterator it = visited.find( n );
43	16370	if( it!=visited.end() ){
44	7468	return it->second;
45		}else{
46	17804	Node ret = n;
47	8902	if( n.getKind()==FORALL ){
48	354	ret = getRemoveQuantifiers2( n[1], visited );
49	8548	}else if( n.getNumChildren()>0 ){
50	13052	std::vector< Node > children;
51	6526	bool childrenChanged = false;
52	22180	for( unsigned i=0; i<n.getNumChildren(); i++ ){
53	31308	Node ni = getRemoveQuantifiers2( n[i], visited );
54	15654	childrenChanged = childrenChanged \|\| ni!=n[i];
55	15654	children.push_back( ni );
56		}
57	6526	if( childrenChanged ){
58	3	if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
59		children.insert( children.begin(), n.getOperator() );
60		}
61	3	ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
62		}
63		}
64	8902	visited[n] = ret;
65	8902	return ret;
66		}
67		}
68
69	4937485	Node TermUtil::getInstConstAttr( Node n ) {
70	4937485	if (!n.hasAttribute(InstConstantAttribute()) ){
71	528112	Node q;
72	264056	if (n.hasOperator())
73		{
74	187880	q = getInstConstAttr(n.getOperator());
75		}
76	264056	if (q.isNull())
77		{
78	582674	for (const Node& nc : n)
79		{
80	359105	q = getInstConstAttr(nc);
81	359105	if (!q.isNull())
82		{
83	40451	break;
84		}
85		}
86		}
87		InstConstantAttribute ica;
88	264056	n.setAttribute(ica, q);
89		}
90	4937485	return n.getAttribute(InstConstantAttribute());
91		}
92
93	3099175	bool TermUtil::hasInstConstAttr( Node n ) {
94	3099175	return !getInstConstAttr(n).isNull();
95		}
96
97	71656	Node TermUtil::getBoundVarAttr( Node n ) {
98	71656	if (!n.hasAttribute(BoundVarAttribute()) ){
99	79742	Node bv;
100	39871	if( n.getKind()==BOUND_VARIABLE ){
101	4035	bv = n;
102		}else{
103	45346	for( unsigned i=0; i<n.getNumChildren(); i++ ){
104	38533	bv = getBoundVarAttr(n[i]);
105	38533	if( !bv.isNull() ){
106	29023	break;
107		}
108		}
109		}
110		BoundVarAttribute bva;
111	39871	n.setAttribute(bva, bv);
112		}
113	71656	return n.getAttribute(BoundVarAttribute());
114		}
115
116	33123	bool TermUtil::hasBoundVarAttr( Node n ) {
117	33123	return !getBoundVarAttr(n).isNull();
118		}
119
120		//remove quantifiers
121	362	Node TermUtil::getRemoveQuantifiers( Node n ) {
122	724	std::map< Node, Node > visited;
123	724	return getRemoveQuantifiers2( n, visited );
124		}
125
126		//quantified simplify
127	946	Node TermUtil::getQuantSimplify( Node n ) {
128	1892	std::unordered_set<Node> fvs;
129	946	expr::getFreeVariables(n, fvs);
130	946	if (fvs.empty())
131		{
132	584	return Rewriter::rewrite( n );
133		}
134	724	std::vector<Node> bvs;
135	362	bvs.insert(bvs.end(), fvs.begin(), fvs.end());
136	362	NodeManager* nm = NodeManager::currentNM();
137	724	Node q = nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, bvs), n);
138	362	q = Rewriter::rewrite(q);
139	362	return getRemoveQuantifiers(q);
140		}
141
142	61851	void TermUtil::computeInstConstContains(Node n, std::vector<Node>& ics)
143		{
144	61851	computeVarContainsInternal(n, INST_CONSTANT, ics);
145	61851	}
146
147		void TermUtil::computeVarContains(Node n, std::vector<Node>& vars)
148		{
149		computeVarContainsInternal(n, BOUND_VARIABLE, vars);
150		}
151
152	1127	void TermUtil::computeQuantContains(Node n, std::vector<Node>& quants)
153		{
154	1127	computeVarContainsInternal(n, FORALL, quants);
155	1127	}
156
157	62978	void TermUtil::computeVarContainsInternal(Node n,
158		Kind k,
159		std::vector<Node>& vars)
160		{
161	125956	std::unordered_set<TNode> visited;
162	62978	std::unordered_set<TNode>::iterator it;
163	125956	std::vector<TNode> visit;
164	125956	TNode cur;
165	62978	visit.push_back(n);
166	502911	do
167		{
168	565889	cur = visit.back();
169	565889	visit.pop_back();
170	565889	it = visited.find(cur);
171
172	565889	if (it == visited.end())
173		{
174	502591	visited.insert(cur);
175	502591	if (cur.getKind() == k)
176		{
177	136855	if (std::find(vars.begin(), vars.end(), cur) == vars.end())
178		{
179	136855	vars.push_back(cur);
180		}
181		}
182		else
183		{
184	365736	if (cur.hasOperator())
185		{
186	169500	visit.push_back(cur.getOperator());
187		}
188	699147	for (const Node& cn : cur)
189		{
190	333411	visit.push_back(cn);
191		}
192		}
193		}
194	565889	} while (!visit.empty());
195	62978	}
196
197	42606	void TermUtil::computeInstConstContainsForQuant(Node q,
198		Node n,
199		std::vector<Node>& vars)
200		{
201	85212	std::vector<Node> ics;
202	42606	computeInstConstContains(n, ics);
203	138766	for (const Node& v : ics)
204		{
205	96160	if (v.getAttribute(InstConstantAttribute()) == q)
206		{
207	96160	if (std::find(vars.begin(), vars.end(), v) == vars.end())
208		{
209	96158	vars.push_back(v);
210		}
211		}
212		}
213	42606	}
214
215		int TermUtil::getTermDepth( Node n ) {
216		if (!n.hasAttribute(TermDepthAttribute()) ){
217		int maxDepth = -1;
218		for( unsigned i=0; i<n.getNumChildren(); i++ ){
219		int depth = getTermDepth( n[i] );
220		if( depth>maxDepth ){
221		maxDepth = depth;
222		}
223		}
224		TermDepthAttribute tda;
225		n.setAttribute(tda,1+maxDepth);
226		}
227		return n.getAttribute(TermDepthAttribute());
228		}
229
230	250646	bool TermUtil::containsUninterpretedConstant( Node n ) {
231	250646	if (!n.hasAttribute(ContainsUConstAttribute()) ){
232	13718	bool ret = false;
233	13718	if( n.getKind()==UNINTERPRETED_CONSTANT ){
234	579	ret = true;
235		}else{
236	26580	for( unsigned i=0; i<n.getNumChildren(); i++ ){
237	13441	if( containsUninterpretedConstant( n[i] ) ){
238		ret = true;
239		break;
240		}
241		}
242		}
243		ContainsUConstAttribute cuca;
244	13718	n.setAttribute(cuca, ret ? 1 : 0);
245		}
246	250646	return n.getAttribute(ContainsUConstAttribute())!=0;
247		}
248
249	4545	Node TermUtil::simpleNegate(Node n)
250		{
251	4545	Assert(n.getType().isBoolean());
252	4545	NodeManager* nm = NodeManager::currentNM();
253	4545	if( n.getKind()==OR \|\| n.getKind()==AND ){
254	2606	std::vector< Node > children;
255	5124	for (const Node& cn : n)
256		{
257	3821	children.push_back(simpleNegate(cn));
258		}
259	1303	return nm->mkNode(n.getKind() == OR ? AND : OR, children);
260		}
261	3242	else if (n.isConst())
262		{
263	71	return nm->mkConst(!n.getConst<bool>());
264		}
265	3171	return n.negate();
266		}
267
268	1822	Node TermUtil::mkNegate(Kind notk, Node n)
269		{
270	1822	if (n.getKind() == notk)
271		{
272	70	return n[0];
273		}
274	1752	return NodeManager::currentNM()->mkNode(notk, n);
275		}
276
277	3887	bool TermUtil::isNegate(Kind k)
278		{
279	3887	return k == NOT \|\| k == BITVECTOR_NOT \|\| k == BITVECTOR_NEG \|\| k == UMINUS;
280		}
281
282	113113	bool TermUtil::isAssoc(Kind k, bool reqNAry)
283		{
284	113113	if (reqNAry)
285		{
286	112608	if (k == UNION \|\| k == INTERSECTION)
287		{
288	31	return false;
289		}
290		}
291	99941	return k == PLUS \|\| k == MULT \|\| k == NONLINEAR_MULT \|\| k == AND \|\| k == OR
292	79243	\|\| k == XOR \|\| k == BITVECTOR_ADD \|\| k == BITVECTOR_MULT
293	74252	\|\| k == BITVECTOR_AND \|\| k == BITVECTOR_OR \|\| k == BITVECTOR_XOR
294	66984	\|\| k == BITVECTOR_XNOR \|\| k == BITVECTOR_CONCAT \|\| k == STRING_CONCAT
295	65325	\|\| k == UNION \|\| k == INTERSECTION \|\| k == JOIN \|\| k == PRODUCT
296	178403	\|\| k == SEP_STAR;
297		}
298
299	235579	bool TermUtil::isComm(Kind k, bool reqNAry)
300		{
301	235579	if (reqNAry)
302		{
303		if (k == UNION \|\| k == INTERSECTION)
304		{
305		return false;
306		}
307		}
308	200065	return k == EQUAL \|\| k == PLUS \|\| k == MULT \|\| k == NONLINEAR_MULT \|\| k == AND
309	161543	\|\| k == OR \|\| k == XOR \|\| k == BITVECTOR_ADD \|\| k == BITVECTOR_MULT
310	140924	\|\| k == BITVECTOR_AND \|\| k == BITVECTOR_OR \|\| k == BITVECTOR_XOR
311	133236	\|\| k == BITVECTOR_XNOR \|\| k == UNION \|\| k == INTERSECTION
312	368747	\|\| k == SEP_STAR;
313		}
314
315	112761	bool TermUtil::isNonAdditive( Kind k ) {
316	112761	return k==AND \|\| k==OR \|\| k==BITVECTOR_AND \|\| k==BITVECTOR_OR;
317		}
318
319	138971	bool TermUtil::isBoolConnective( Kind k ) {
320	138971	return k==OR \|\| k==AND \|\| k==EQUAL \|\| k==ITE \|\| k==FORALL \|\| k==NOT \|\| k==SEP_STAR;
321		}
322
323	114668	bool TermUtil::isBoolConnectiveTerm( TNode n ) {
324	194379	return isBoolConnective( n.getKind() ) &&
325	477233	( n.getKind()!=EQUAL \|\| n[0].getType().isBoolean() ) &&
326	280006	( n.getKind()!=ITE \|\| n.getType().isBoolean() );
327		}
328
329	21641	Node TermUtil::mkTypeValue(TypeNode tn, int32_t val)
330		{
331	21641	Node n;
332	21641	if (tn.isInteger() \|\| tn.isReal())
333		{
334	5756	Rational c(val);
335	2878	n = NodeManager::currentNM()->mkConst(c);
336		}
337	18763	else if (tn.isBitVector())
338		{
339		// cast to unsigned
340	1173	uint32_t uv = static_cast<uint32_t>(val);
341	2346	BitVector bval(tn.getConst<BitVectorSize>(), uv);
342	1173	n = NodeManager::currentNM()->mkConst<BitVector>(bval);
343		}
344	17590	else if (tn.isBoolean())
345		{
346	17350	if (val == 0)
347		{
348	16957	n = NodeManager::currentNM()->mkConst(false);
349		}
350		}
351	240	else if (tn.isStringLike())
352		{
353	150	if (val == 0)
354		{
355	87	n = strings::Word::mkEmptyWord(tn);
356		}
357		}
358	21641	return n;
359		}
360
361	17780	Node TermUtil::mkTypeMaxValue(TypeNode tn)
362		{
363	17780	Node n;
364	17780	if (tn.isBitVector())
365		{
366	373	n = bv::utils::mkOnes(tn.getConst<BitVectorSize>());
367		}
368	17407	else if (tn.isBoolean())
369		{
370	16744	n = NodeManager::currentNM()->mkConst(true);
371		}
372	17780	return n;
373		}
374
375	4	Node TermUtil::mkTypeValueOffset(TypeNode tn,
376		Node val,
377		int32_t offset,
378		int32_t& status)
379		{
380	4	Node val_o;
381	8	Node offset_val = mkTypeValue(tn, offset);
382	4	status = -1;
383	4	if (!offset_val.isNull())
384		{
385	4	if (tn.isInteger() \|\| tn.isReal())
386		{
387	4	val_o = Rewriter::rewrite(
388	8	NodeManager::currentNM()->mkNode(PLUS, val, offset_val));
389	4	status = 0;
390		}
391		else if (tn.isBitVector())
392		{
393		val_o = Rewriter::rewrite(
394		NodeManager::currentNM()->mkNode(BITVECTOR_ADD, val, offset_val));
395		}
396		}
397	8	return val_o;
398		}
399
400	2	Node TermUtil::mkTypeConst(TypeNode tn, bool pol)
401		{
402	2	return pol ? mkTypeMaxValue(tn) : mkTypeValue(tn, 0);
403		}
404
405		bool TermUtil::isAntisymmetric(Kind k, Kind& dk)
406		{
407		if (k == GT)
408		{
409		dk = LT;
410		return true;
411		}
412		else if (k == GEQ)
413		{
414		dk = LEQ;
415		return true;
416		}
417		else if (k == BITVECTOR_UGT)
418		{
419		dk = BITVECTOR_ULT;
420		return true;
421		}
422		else if (k == BITVECTOR_UGE)
423		{
424		dk = BITVECTOR_ULE;
425		return true;
426		}
427		else if (k == BITVECTOR_SGT)
428		{
429		dk = BITVECTOR_SLT;
430		return true;
431		}
432		else if (k == BITVECTOR_SGE)
433		{
434		dk = BITVECTOR_SLE;
435		return true;
436		}
437		return false;
438		}
439
440	1183	bool TermUtil::isIdempotentArg(Node n, Kind ik, int arg)
441		{
442		// these should all be binary operators
443		// Assert( ik!=DIVISION && ik!=INTS_DIVISION && ik!=INTS_MODULUS &&
444		// ik!=BITVECTOR_UDIV );
445	2366	TypeNode tn = n.getType();
446	1183	if (n == mkTypeValue(tn, 0))
447		{
448	549	if (ik == PLUS \|\| ik == OR \|\| ik == XOR \|\| ik == BITVECTOR_ADD
449	424	\|\| ik == BITVECTOR_OR \|\| ik == BITVECTOR_XOR \|\| ik == STRING_CONCAT)
450		{
451	142	return true;
452		}
453	407	else if (ik == MINUS \|\| ik == BITVECTOR_SHL \|\| ik == BITVECTOR_LSHR
454	357	\|\| ik == BITVECTOR_ASHR \|\| ik == BITVECTOR_SUB
455	357	\|\| ik == BITVECTOR_UREM)
456		{
457	57	return arg == 1;
458		}
459		}
460	634	else if (n == mkTypeValue(tn, 1))
461		{
462	374	if (ik == MULT \|\| ik == BITVECTOR_MULT)
463		{
464	4	return true;
465		}
466	370	else if (ik == DIVISION \|\| ik == DIVISION_TOTAL \|\| ik == INTS_DIVISION
467	366	\|\| ik == INTS_DIVISION_TOTAL
468	366	\|\| ik == INTS_MODULUS
469	366	\|\| ik == INTS_MODULUS_TOTAL
470	366	\|\| ik == BITVECTOR_UDIV
471	359	\|\| ik == BITVECTOR_SDIV)
472		{
473	20	return arg == 1;
474		}
475		}
476	260	else if (n == mkTypeMaxValue(tn))
477		{
478	169	if (ik == EQUAL \|\| ik == BITVECTOR_AND \|\| ik == BITVECTOR_XNOR)
479		{
480		return true;
481		}
482		}
483	960	return false;
484		}
485
486	997	Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
487		{
488	1994	TypeNode tn = n.getType();
489	997	if (n == mkTypeValue(tn, 0))
490		{
491	378	if (ik == AND \|\| ik == MULT \|\| ik == BITVECTOR_AND \|\| ik == BITVECTOR_MULT)
492		{
493	44	return n;
494		}
495	334	else if (ik == BITVECTOR_SHL \|\| ik == BITVECTOR_LSHR \|\| ik == BITVECTOR_ASHR
496	334	\|\| ik == BITVECTOR_UREM)
497		{
498	3	if (arg == 0)
499		{
500	3	return n;
501		}
502		}
503	331	else if (ik == BITVECTOR_UDIV \|\| ik == BITVECTOR_UDIV
504	324	\|\| ik == BITVECTOR_SDIV)
505		{
506	14	if (arg == 0)
507		{
508	6	return n;
509		}
510	8	else if (arg == 1)
511		{
512	8	return mkTypeMaxValue(tn);
513		}
514		}
515	317	else if (ik == DIVISION \|\| ik == DIVISION_TOTAL \|\| ik == INTS_DIVISION
516	315	\|\| ik == INTS_DIVISION_TOTAL
517	315	\|\| ik == INTS_MODULUS
518	312	\|\| ik == INTS_MODULUS_TOTAL)
519		{
520	7	if (arg == 0)
521		{
522	3	return n;
523		}
524		}
525	312	else if (ik == STRING_SUBSTR)
526		{
527		if (arg == 0)
528		{
529		return n;
530		}
531		else if (arg == 2)
532		{
533		return mkTypeValue(NodeManager::currentNM()->stringType(), 0);
534		}
535		}
536	312	else if (ik == STRING_INDEXOF)
537		{
538		if (arg == 0 \|\| arg == 1)
539		{
540		return mkTypeValue(NodeManager::currentNM()->integerType(), -1);
541		}
542		}
543		}
544	619	else if (n == mkTypeValue(tn, 1))
545		{
546	359	if (ik == BITVECTOR_UREM)
547		{
548	7	return mkTypeValue(tn, 0);
549		}
550		}
551	260	else if (n == mkTypeMaxValue(tn))
552		{
553	169	if (ik == OR \|\| ik == BITVECTOR_OR)
554		{
555	59	return n;
556		}
557		}
558		else
559		{
560	91	if (n.getType().isReal() && n.getConst<Rational>().sgn() < 0)
561		{
562		// negative arguments
563	2	if (ik == STRING_SUBSTR \|\| ik == STRING_CHARAT)
564		{
565		return mkTypeValue(NodeManager::currentNM()->stringType(), 0);
566		}
567	2	else if (ik == STRING_INDEXOF)
568		{
569		Assert(arg == 2);
570		return mkTypeValue(NodeManager::currentNM()->integerType(), -1);
571		}
572		}
573		}
574	867	return Node::null();
575		}
576
577	668	bool TermUtil::hasOffsetArg(Kind ik, int arg, int& offset, Kind& ok)
578		{
579	668	if (ik == LT)
580		{
581	4	Assert(arg == 0 \|\| arg == 1);
582	4	offset = arg == 0 ? 1 : -1;
583	4	ok = LEQ;
584	4	return true;
585		}
586	664	else if (ik == BITVECTOR_ULT)
587		{
588	12	Assert(arg == 0 \|\| arg == 1);
589	12	offset = arg == 0 ? 1 : -1;
590	12	ok = BITVECTOR_ULE;
591	12	return true;
592		}
593	652	else if (ik == BITVECTOR_SLT)
594		{
595	12	Assert(arg == 0 \|\| arg == 1);
596	12	offset = arg == 0 ? 1 : -1;
597	12	ok = BITVECTOR_SLE;
598	12	return true;
599		}
600	640	return false;
601		}
602
603		} // namespace quantifiers
604		} // namespace theory
605	22755	} // namespace cvc5