Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/term_util.cpp	Lines:	259	309	83.8 %
Date:	2021-11-07	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	5850	size_t TermUtil::getVariableNum(Node q, Node v)
35		{
36	5850	Node::iterator it = std::find(q[0].begin(), q[0].end(), v);
37	5850	Assert(it != q[0].end());
38	5850	return it - q[0].begin();
39		}
40
41	26912	Node TermUtil::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ) {
42	26912	std::map< Node, Node >::iterator it = visited.find( n );
43	26912	if( it!=visited.end() ){
44	12213	return it->second;
45		}else{
46	29398	Node ret = n;
47	14699	if( n.getKind()==FORALL ){
48	604	ret = getRemoveQuantifiers2( n[1], visited );
49	14095	}else if( n.getNumChildren()>0 ){
50	21488	std::vector< Node > children;
51	10744	bool childrenChanged = false;
52	36436	for( unsigned i=0; i<n.getNumChildren(); i++ ){
53	51384	Node ni = getRemoveQuantifiers2( n[i], visited );
54	25692	childrenChanged = childrenChanged \|\| ni!=n[i];
55	25692	children.push_back( ni );
56		}
57	10744	if( childrenChanged ){
58	6	if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
59		children.insert( children.begin(), n.getOperator() );
60		}
61	6	ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
62		}
63		}
64	14699	visited[n] = ret;
65	14699	return ret;
66		}
67		}
68
69	12453210	Node TermUtil::getInstConstAttr( Node n ) {
70	12453210	if (!n.hasAttribute(InstConstantAttribute()) ){
71	1024484	Node q;
72	512242	if (n.hasOperator())
73		{
74	378461	q = getInstConstAttr(n.getOperator());
75		}
76	512242	if (q.isNull())
77		{
78	1087081	for (const Node& nc : n)
79		{
80	682695	q = getInstConstAttr(nc);
81	682695	if (!q.isNull())
82		{
83	107775	break;
84		}
85		}
86		}
87		InstConstantAttribute ica;
88	512242	n.setAttribute(ica, q);
89		}
90	12453210	return n.getAttribute(InstConstantAttribute());
91		}
92
93	7948500	bool TermUtil::hasInstConstAttr( Node n ) {
94	7948500	return !getInstConstAttr(n).isNull();
95		}
96
97	175501	Node TermUtil::getBoundVarAttr( Node n ) {
98	175501	if (!n.hasAttribute(BoundVarAttribute()) ){
99	179208	Node bv;
100	89604	if( n.getKind()==BOUND_VARIABLE ){
101	8565	bv = n;
102		}else{
103	106845	for( unsigned i=0; i<n.getNumChildren(); i++ ){
104	90608	bv = getBoundVarAttr(n[i]);
105	90608	if( !bv.isNull() ){
106	64802	break;
107		}
108		}
109		}
110		BoundVarAttribute bva;
111	89604	n.setAttribute(bva, bv);
112		}
113	175501	return n.getAttribute(BoundVarAttribute());
114		}
115
116	84893	bool TermUtil::hasBoundVarAttr( Node n ) {
117	84893	return !getBoundVarAttr(n).isNull();
118		}
119
120		//remove quantifiers
121	616	Node TermUtil::getRemoveQuantifiers( Node n ) {
122	1232	std::map< Node, Node > visited;
123	1232	return getRemoveQuantifiers2( n, visited );
124		}
125
126		//quantified simplify
127	1596	Node TermUtil::getQuantSimplify( Node n ) {
128	3192	std::unordered_set<Node> fvs;
129	1596	expr::getFreeVariables(n, fvs);
130	1596	if (fvs.empty())
131		{
132	980	return Rewriter::rewrite( n );
133		}
134	1232	std::vector<Node> bvs;
135	616	bvs.insert(bvs.end(), fvs.begin(), fvs.end());
136	616	NodeManager* nm = NodeManager::currentNM();
137	1232	Node q = nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, bvs), n);
138	616	q = Rewriter::rewrite(q);
139	616	return getRemoveQuantifiers(q);
140		}
141
142	165115	void TermUtil::computeInstConstContains(Node n, std::vector<Node>& ics)
143		{
144	165115	computeVarContainsInternal(n, INST_CONSTANT, ics);
145	165115	}
146
147		void TermUtil::computeVarContains(Node n, std::vector<Node>& vars)
148		{
149		computeVarContainsInternal(n, BOUND_VARIABLE, vars);
150		}
151
152	1932	void TermUtil::computeQuantContains(Node n, std::vector<Node>& quants)
153		{
154	1932	computeVarContainsInternal(n, FORALL, quants);
155	1932	}
156
157	167047	void TermUtil::computeVarContainsInternal(Node n,
158		Kind k,
159		std::vector<Node>& vars)
160		{
161	334094	std::unordered_set<TNode> visited;
162	167047	std::unordered_set<TNode>::iterator it;
163	334094	std::vector<TNode> visit;
164	334094	TNode cur;
165	167047	visit.push_back(n);
166	1312049	do
167		{
168	1479096	cur = visit.back();
169	1479096	visit.pop_back();
170	1479096	it = visited.find(cur);
171
172	1479096	if (it == visited.end())
173		{
174	1316938	visited.insert(cur);
175	1316938	if (cur.getKind() == k)
176		{
177	387713	if (std::find(vars.begin(), vars.end(), cur) == vars.end())
178		{
179	387713	vars.push_back(cur);
180		}
181		}
182		else
183		{
184	929225	if (cur.hasOperator())
185		{
186	439355	visit.push_back(cur.getOperator());
187		}
188	1801919	for (const Node& cn : cur)
189		{
190	872694	visit.push_back(cn);
191		}
192		}
193		}
194	1479096	} while (!visit.empty());
195	167047	}
196
197	114946	void TermUtil::computeInstConstContainsForQuant(Node q,
198		Node n,
199		std::vector<Node>& vars)
200		{
201	229892	std::vector<Node> ics;
202	114946	computeInstConstContains(n, ics);
203	387581	for (const Node& v : ics)
204		{
205	272635	if (v.getAttribute(InstConstantAttribute()) == q)
206		{
207	272635	if (std::find(vars.begin(), vars.end(), v) == vars.end())
208		{
209	272633	vars.push_back(v);
210		}
211		}
212		}
213	114946	}
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	564359	bool TermUtil::containsUninterpretedConstant( Node n ) {
231	564359	if (!n.hasAttribute(ContainsUConstAttribute()) ){
232	23128	bool ret = false;
233	23128	if( n.getKind()==UNINTERPRETED_CONSTANT ){
234	822	ret = true;
235		}else{
236	42660	for( unsigned i=0; i<n.getNumChildren(); i++ ){
237	20354	if( containsUninterpretedConstant( n[i] ) ){
238		ret = true;
239		break;
240		}
241		}
242		}
243		ContainsUConstAttribute cuca;
244	23128	n.setAttribute(cuca, ret ? 1 : 0);
245		}
246	564359	return n.getAttribute(ContainsUConstAttribute())!=0;
247		}
248
249	8962	Node TermUtil::simpleNegate(Node n)
250		{
251	8962	Assert(n.getType().isBoolean());
252	8962	NodeManager* nm = NodeManager::currentNM();
253	8962	if( n.getKind()==OR \|\| n.getKind()==AND ){
254	5318	std::vector< Node > children;
255	10201	for (const Node& cn : n)
256		{
257	7542	children.push_back(simpleNegate(cn));
258		}
259	2659	return nm->mkNode(n.getKind() == OR ? AND : OR, children);
260		}
261	6303	else if (n.isConst())
262		{
263	128	return nm->mkConst(!n.getConst<bool>());
264		}
265	6175	return n.negate();
266		}
267
268	10332	Node TermUtil::mkNegate(Kind notk, Node n)
269		{
270	10332	if (n.getKind() == notk)
271		{
272	706	return n[0];
273		}
274	9626	return NodeManager::currentNM()->mkNode(notk, n);
275		}
276
277	22415	bool TermUtil::isNegate(Kind k)
278		{
279	22415	return k == NOT \|\| k == BITVECTOR_NOT \|\| k == BITVECTOR_NEG \|\| k == UMINUS;
280		}
281
282	315633	bool TermUtil::isAssoc(Kind k, bool reqNAry)
283		{
284	315633	if (reqNAry)
285		{
286	314729	if (k == UNION \|\| k == INTERSECTION)
287		{
288	298	return false;
289		}
290		}
291	286311	return k == PLUS \|\| k == MULT \|\| k == NONLINEAR_MULT \|\| k == AND \|\| k == OR
292	195207	\|\| k == XOR \|\| k == BITVECTOR_ADD \|\| k == BITVECTOR_MULT
293	185346	\|\| k == BITVECTOR_AND \|\| k == BITVECTOR_OR \|\| k == BITVECTOR_XOR
294	172992	\|\| k == BITVECTOR_XNOR \|\| k == BITVECTOR_CONCAT \|\| k == STRING_CONCAT
295	166739	\|\| k == UNION \|\| k == INTERSECTION \|\| k == JOIN \|\| k == PRODUCT
296	482066	\|\| k == SEP_STAR;
297		}
298
299	616014	bool TermUtil::isComm(Kind k, bool reqNAry)
300		{
301	616014	if (reqNAry)
302		{
303		if (k == UNION \|\| k == INTERSECTION)
304		{
305		return false;
306		}
307		}
308	525961	return k == EQUAL \|\| k == PLUS \|\| k == MULT \|\| k == NONLINEAR_MULT \|\| k == AND
309	411480	\|\| k == OR \|\| k == XOR \|\| k == BITVECTOR_ADD \|\| k == BITVECTOR_MULT
310	343411	\|\| k == BITVECTOR_AND \|\| k == BITVECTOR_OR \|\| k == BITVECTOR_XOR
311	330520	\|\| k == BITVECTOR_XNOR \|\| k == UNION \|\| k == INTERSECTION
312	946167	\|\| k == SEP_STAR;
313		}
314
315	315006	bool TermUtil::isNonAdditive( Kind k ) {
316	315006	return k==AND \|\| k==OR \|\| k==BITVECTOR_AND \|\| k==BITVECTOR_OR;
317		}
318
319	351059	bool TermUtil::isBoolConnective( Kind k ) {
320	351059	return k==OR \|\| k==AND \|\| k==EQUAL \|\| k==ITE \|\| k==FORALL \|\| k==NOT \|\| k==SEP_STAR;
321		}
322
323	289638	bool TermUtil::isBoolConnectiveTerm( TNode n ) {
324	495203	return isBoolConnective( n.getKind() ) &&
325	1207258	( n.getKind()!=EQUAL \|\| n[0].getType().isBoolean() ) &&
326	703428	( n.getKind()!=ITE \|\| n.getType().isBoolean() );
327		}
328
329	92231	Node TermUtil::mkTypeValue(TypeNode tn, int32_t val)
330		{
331	92231	Node n;
332	92231	if (tn.isInteger() \|\| tn.isReal())
333		{
334	15492	Rational c(val);
335	7746	n = NodeManager::currentNM()->mkConst(c);
336		}
337	84485	else if (tn.isBitVector())
338		{
339		// cast to unsigned
340	2186	uint32_t uv = static_cast<uint32_t>(val);
341	4372	BitVector bval(tn.getConst<BitVectorSize>(), uv);
342	2186	n = NodeManager::currentNM()->mkConst<BitVector>(bval);
343		}
344	82299	else if (tn.isBoolean())
345		{
346	81751	if (val == 0)
347		{
348	81099	n = NodeManager::currentNM()->mkConst(false);
349		}
350		}
351	548	else if (tn.isStringLike())
352		{
353	356	if (val == 0)
354		{
355	194	n = strings::Word::mkEmptyWord(tn);
356		}
357		}
358	92231	return n;
359		}
360
361	84053	Node TermUtil::mkTypeMaxValue(TypeNode tn)
362		{
363	84053	Node n;
364	84053	if (tn.isBitVector())
365		{
366	676	n = bv::utils::mkOnes(tn.getConst<BitVectorSize>());
367		}
368	83377	else if (tn.isBoolean())
369		{
370	80747	n = NodeManager::currentNM()->mkConst(true);
371		}
372	84053	return n;
373		}
374
375	8	Node TermUtil::mkTypeValueOffset(TypeNode tn,
376		Node val,
377		int32_t offset,
378		int32_t& status)
379		{
380	8	Node val_o;
381	16	Node offset_val = mkTypeValue(tn, offset);
382	8	status = -1;
383	8	if (!offset_val.isNull())
384		{
385	8	if (tn.isInteger() \|\| tn.isReal())
386		{
387	8	val_o = Rewriter::rewrite(
388	16	NodeManager::currentNM()->mkNode(PLUS, val, offset_val));
389	8	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	16	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	2544	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	5088	TypeNode tn = n.getType();
446	2544	if (n == mkTypeValue(tn, 0))
447		{
448	943	if (ik == PLUS \|\| ik == OR \|\| ik == XOR \|\| ik == BITVECTOR_ADD
449	729	\|\| ik == BITVECTOR_OR \|\| ik == BITVECTOR_XOR \|\| ik == STRING_CONCAT)
450		{
451	244	return true;
452		}
453	699	else if (ik == MINUS \|\| ik == BITVECTOR_SHL \|\| ik == BITVECTOR_LSHR
454	615	\|\| ik == BITVECTOR_ASHR \|\| ik == BITVECTOR_SUB
455	615	\|\| ik == BITVECTOR_UREM)
456		{
457	98	return arg == 1;
458		}
459		}
460	1601	else if (n == mkTypeValue(tn, 1))
461		{
462	656	if (ik == MULT \|\| ik == BITVECTOR_MULT)
463		{
464	10	return true;
465		}
466	646	else if (ik == DIVISION \|\| ik == DIVISION_TOTAL \|\| ik == INTS_DIVISION
467	638	\|\| ik == INTS_DIVISION_TOTAL
468	638	\|\| ik == INTS_MODULUS
469	638	\|\| ik == INTS_MODULUS_TOTAL
470	638	\|\| ik == BITVECTOR_UDIV
471	624	\|\| ik == BITVECTOR_SDIV)
472		{
473	40	return arg == 1;
474		}
475		}
476	945	else if (n == mkTypeMaxValue(tn))
477		{
478	295	if (ik == EQUAL \|\| ik == BITVECTOR_AND \|\| ik == BITVECTOR_XNOR)
479		{
480		return true;
481		}
482		}
483	2152	return false;
484		}
485
486	2218	Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
487		{
488	4436	TypeNode tn = n.getType();
489	2218	if (n == mkTypeValue(tn, 0))
490		{
491	649	if (ik == AND \|\| ik == MULT \|\| ik == BITVECTOR_AND \|\| ik == BITVECTOR_MULT)
492		{
493	80	return n;
494		}
495	569	else if (ik == BITVECTOR_SHL \|\| ik == BITVECTOR_LSHR \|\| ik == BITVECTOR_ASHR
496	569	\|\| ik == BITVECTOR_UREM)
497		{
498	6	if (arg == 0)
499		{
500	6	return n;
501		}
502		}
503	563	else if (ik == BITVECTOR_UDIV \|\| ik == BITVECTOR_UDIV
504	549	\|\| ik == BITVECTOR_SDIV)
505		{
506	28	if (arg == 0)
507		{
508	12	return n;
509		}
510	16	else if (arg == 1)
511		{
512	16	return mkTypeMaxValue(tn);
513		}
514		}
515	535	else if (ik == DIVISION \|\| ik == DIVISION_TOTAL \|\| ik == INTS_DIVISION
516	531	\|\| ik == INTS_DIVISION_TOTAL
517	531	\|\| ik == INTS_MODULUS
518	525	\|\| ik == INTS_MODULUS_TOTAL)
519		{
520	14	if (arg == 0)
521		{
522	6	return n;
523		}
524		}
525	525	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	525	else if (ik == STRING_INDEXOF)
537		{
538		if (arg == 0 \|\| arg == 1)
539		{
540		return mkTypeValue(NodeManager::currentNM()->integerType(), -1);
541		}
542		}
543		}
544	1569	else if (n == mkTypeValue(tn, 1))
545		{
546	624	if (ik == BITVECTOR_UREM)
547		{
548	14	return mkTypeValue(tn, 0);
549		}
550		}
551	945	else if (n == mkTypeMaxValue(tn))
552		{
553	295	if (ik == OR \|\| ik == BITVECTOR_OR)
554		{
555	104	return n;
556		}
557		}
558		else
559		{
560	650	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	1980	return Node::null();
575		}
576
577	1592	bool TermUtil::hasOffsetArg(Kind ik, int arg, int& offset, Kind& ok)
578		{
579	1592	if (ik == LT)
580		{
581	8	Assert(arg == 0 \|\| arg == 1);
582	8	offset = arg == 0 ? 1 : -1;
583	8	ok = LEQ;
584	8	return true;
585		}
586	1584	else if (ik == BITVECTOR_ULT)
587		{
588	18	Assert(arg == 0 \|\| arg == 1);
589	18	offset = arg == 0 ? 1 : -1;
590	18	ok = BITVECTOR_ULE;
591	18	return true;
592		}
593	1566	else if (ik == BITVECTOR_SLT)
594		{
595	18	Assert(arg == 0 \|\| arg == 1);
596	18	offset = arg == 0 ? 1 : -1;
597	18	ok = BITVECTOR_SLE;
598	18	return true;
599		}
600	1548	return false;
601		}
602
603		} // namespace quantifiers
604		} // namespace theory
605	31137	} // namespace cvc5