Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/term_util.cpp	Lines:	262	309	84.8 %
Date:	2021-08-16	Branches:	561	1020	55.0 %


/******************************************************************************
 * 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	5253	size_t TermUtil::getVariableNum(Node q, Node v)
35		{
36	5253	Node::iterator it = std::find(q[0].begin(), q[0].end(), v);
37	5253	Assert(it != q[0].end());
38	5253	return it - q[0].begin();
39		}
40
41	16166	Node TermUtil::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ) {
42	16166	std::map< Node, Node >::iterator it = visited.find( n );
43	16166	if( it!=visited.end() ){
44	7221	return it->second;
45		}else{
46	17890	Node ret = n;
47	8945	if( n.getKind()==FORALL ){
48	373	ret = getRemoveQuantifiers2( n[1], visited );
49	8572	}else if( n.getNumChildren()>0 ){
50	12954	std::vector< Node > children;
51	6477	bool childrenChanged = false;
52	21887	for( unsigned i=0; i<n.getNumChildren(); i++ ){
53	30820	Node ni = getRemoveQuantifiers2( n[i], visited );
54	15410	childrenChanged = childrenChanged \|\| ni!=n[i];
55	15410	children.push_back( ni );
56		}
57	6477	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	8945	visited[n] = ret;
65	8945	return ret;
66		}
67		}
68
69	11676339	Node TermUtil::getInstConstAttr( Node n ) {
70	11676339	if (!n.hasAttribute(InstConstantAttribute()) ){
71	924206	Node q;
72	462103	if (n.hasOperator())
73		{
74	337685	q = getInstConstAttr(n.getOperator());
75		}
76	462103	if (q.isNull())
77		{
78	959757	for (const Node& nc : n)
79		{
80	599674	q = getInstConstAttr(nc);
81	599674	if (!q.isNull())
82		{
83	101953	break;
84		}
85		}
86		}
87		InstConstantAttribute ica;
88	462103	n.setAttribute(ica, q);
89		}
90	11676339	return n.getAttribute(InstConstantAttribute());
91		}
92
93	7521656	bool TermUtil::hasInstConstAttr( Node n ) {
94	7521656	return !getInstConstAttr(n).isNull();
95		}
96
97	158734	Node TermUtil::getBoundVarAttr( Node n ) {
98	158734	if (!n.hasAttribute(BoundVarAttribute()) ){
99	165466	Node bv;
100	82733	if( n.getKind()==BOUND_VARIABLE ){
101	7732	bv = n;
102		}else{
103	100362	for( unsigned i=0; i<n.getNumChildren(); i++ ){
104	84183	bv = getBoundVarAttr(n[i]);
105	84183	if( !bv.isNull() ){
106	58822	break;
107		}
108		}
109		}
110		BoundVarAttribute bva;
111	82733	n.setAttribute(bva, bv);
112		}
113	158734	return n.getAttribute(BoundVarAttribute());
114		}
115
116	74551	bool TermUtil::hasBoundVarAttr( Node n ) {
117	74551	return !getBoundVarAttr(n).isNull();
118		}
119
120		//remove quantifiers
121	383	Node TermUtil::getRemoveQuantifiers( Node n ) {
122	766	std::map< Node, Node > visited;
123	766	return getRemoveQuantifiers2( n, visited );
124		}
125
126		//quantified simplify
127	954	Node TermUtil::getQuantSimplify( Node n ) {
128	1908	std::unordered_set<Node> fvs;
129	954	expr::getFreeVariables(n, fvs);
130	954	if (fvs.empty())
131		{
132	571	return Rewriter::rewrite( n );
133		}
134	766	std::vector<Node> bvs;
135	383	bvs.insert(bvs.end(), fvs.begin(), fvs.end());
136	383	NodeManager* nm = NodeManager::currentNM();
137	766	Node q = nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, bvs), n);
138	383	q = Rewriter::rewrite(q);
139	383	return getRemoveQuantifiers(q);
140		}
141
142	155661	void TermUtil::computeInstConstContains(Node n, std::vector<Node>& ics)
143		{
144	155661	computeVarContainsInternal(n, INST_CONSTANT, ics);
145	155661	}
146
147	256	void TermUtil::computeVarContains(Node n, std::vector<Node>& vars)
148		{
149	256	computeVarContainsInternal(n, BOUND_VARIABLE, vars);
150	256	}
151
152	1611	void TermUtil::computeQuantContains(Node n, std::vector<Node>& quants)
153		{
154	1611	computeVarContainsInternal(n, FORALL, quants);
155	1611	}
156
157	157528	void TermUtil::computeVarContainsInternal(Node n,
158		Kind k,
159		std::vector<Node>& vars)
160		{
161	315056	std::unordered_set<TNode> visited;
162	157528	std::unordered_set<TNode>::iterator it;
163	315056	std::vector<TNode> visit;
164	315056	TNode cur;
165	157528	visit.push_back(n);
166	1245407	do
167		{
168	1402935	cur = visit.back();
169	1402935	visit.pop_back();
170	1402935	it = visited.find(cur);
171
172	1402935	if (it == visited.end())
173		{
174	1252346	visited.insert(cur);
175	1252346	if (cur.getKind() == k)
176		{
177	368397	if (std::find(vars.begin(), vars.end(), cur) == vars.end())
178		{
179	368397	vars.push_back(cur);
180		}
181		}
182		else
183		{
184	883949	if (cur.hasOperator())
185		{
186	417417	visit.push_back(cur.getOperator());
187		}
188	1711939	for (const Node& cn : cur)
189		{
190	827990	visit.push_back(cn);
191		}
192		}
193		}
194	1402935	} while (!visit.empty());
195	157528	}
196
197	108267	void TermUtil::computeInstConstContainsForQuant(Node q,
198		Node n,
199		std::vector<Node>& vars)
200		{
201	216534	std::vector<Node> ics;
202	108267	computeInstConstContains(n, ics);
203	366421	for (const Node& v : ics)
204		{
205	258154	if (v.getAttribute(InstConstantAttribute()) == q)
206		{
207	258154	if (std::find(vars.begin(), vars.end(), v) == vars.end())
208		{
209	258152	vars.push_back(v);
210		}
211		}
212		}
213	108267	}
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	494269	bool TermUtil::containsUninterpretedConstant( Node n ) {
231	494269	if (!n.hasAttribute(ContainsUConstAttribute()) ){
232	23406	bool ret = false;
233	23406	if( n.getKind()==UNINTERPRETED_CONSTANT ){
234	818	ret = true;
235		}else{
236	42988	for( unsigned i=0; i<n.getNumChildren(); i++ ){
237	20400	if( containsUninterpretedConstant( n[i] ) ){
238		ret = true;
239		break;
240		}
241		}
242		}
243		ContainsUConstAttribute cuca;
244	23406	n.setAttribute(cuca, ret ? 1 : 0);
245		}
246	494269	return n.getAttribute(ContainsUConstAttribute())!=0;
247		}
248
249	4646	Node TermUtil::simpleNegate(Node n)
250		{
251	4646	Assert(n.getType().isBoolean());
252	4646	NodeManager* nm = NodeManager::currentNM();
253	4646	if( n.getKind()==OR \|\| n.getKind()==AND ){
254	2670	std::vector< Node > children;
255	5263	for (const Node& cn : n)
256		{
257	3928	children.push_back(simpleNegate(cn));
258		}
259	1335	return nm->mkNode(n.getKind() == OR ? AND : OR, children);
260		}
261	3311	else if (n.isConst())
262		{
263	79	return nm->mkConst(!n.getConst<bool>());
264		}
265	3232	return n.negate();
266		}
267
268	945	Node TermUtil::mkNegate(Kind notk, Node n)
269		{
270	945	if (n.getKind() == notk)
271		{
272	34	return n[0];
273		}
274	911	return NodeManager::currentNM()->mkNode(notk, n);
275		}
276
277	2725	bool TermUtil::isNegate(Kind k)
278		{
279	2725	return k == NOT \|\| k == BITVECTOR_NOT \|\| k == BITVECTOR_NEG \|\| k == UMINUS;
280		}
281
282	105947	bool TermUtil::isAssoc(Kind k, bool reqNAry)
283		{
284	105947	if (reqNAry)
285		{
286	105444	if (k == UNION \|\| k == INTERSECTION)
287		{
288	27	return false;
289		}
290		}
291	91533	return k == PLUS \|\| k == MULT \|\| k == NONLINEAR_MULT \|\| k == AND \|\| k == OR
292	74030	\|\| k == XOR \|\| k == BITVECTOR_ADD \|\| k == BITVECTOR_MULT
293	69142	\|\| k == BITVECTOR_AND \|\| k == BITVECTOR_OR \|\| k == BITVECTOR_XOR
294	62953	\|\| k == BITVECTOR_XNOR \|\| k == BITVECTOR_CONCAT \|\| k == STRING_CONCAT
295	61565	\|\| k == UNION \|\| k == INTERSECTION \|\| k == JOIN \|\| k == PRODUCT
296	167481	\|\| k == SEP_STAR;
297		}
298
299	391707	bool TermUtil::isComm(Kind k, bool reqNAry)
300		{
301	391707	if (reqNAry)
302		{
303		if (k == UNION \|\| k == INTERSECTION)
304		{
305		return false;
306		}
307		}
308	331381	return k == EQUAL \|\| k == PLUS \|\| k == MULT \|\| k == NONLINEAR_MULT \|\| k == AND
309	274634	\|\| k == OR \|\| k == XOR \|\| k == BITVECTOR_ADD \|\| k == BITVECTOR_MULT
310	245312	\|\| k == BITVECTOR_AND \|\| k == BITVECTOR_OR \|\| k == BITVECTOR_XOR
311	238679	\|\| k == BITVECTOR_XNOR \|\| k == UNION \|\| k == INTERSECTION
312	630300	\|\| k == SEP_STAR;
313		}
314
315	105597	bool TermUtil::isNonAdditive( Kind k ) {
316	105597	return k==AND \|\| k==OR \|\| k==BITVECTOR_AND \|\| k==BITVECTOR_OR;
317		}
318
319	334318	bool TermUtil::isBoolConnective( Kind k ) {
320	334318	return k==OR \|\| k==AND \|\| k==EQUAL \|\| k==ITE \|\| k==FORALL \|\| k==NOT \|\| k==SEP_STAR;
321		}
322
323	281100	bool TermUtil::isBoolConnectiveTerm( TNode n ) {
324	481498	return isBoolConnective( n.getKind() ) &&
325	1172395	( n.getKind()!=EQUAL \|\| n[0].getType().isBoolean() ) &&
326	682492	( n.getKind()!=ITE \|\| n.getType().isBoolean() );
327		}
328
329	19002	Node TermUtil::mkTypeValue(TypeNode tn, int32_t val)
330		{
331	19002	Node n;
332	19002	if (tn.isInteger() \|\| tn.isReal())
333		{
334	6184	Rational c(val);
335	3092	n = NodeManager::currentNM()->mkConst(c);
336		}
337	15910	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	14737	else if (tn.isBoolean())
345		{
346	14497	if (val == 0)
347		{
348	14098	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	19002	return n;
359		}
360
361	14920	Node TermUtil::mkTypeMaxValue(TypeNode tn)
362		{
363	14920	Node n;
364	14920	if (tn.isBitVector())
365		{
366	373	n = bv::utils::mkOnes(tn.getConst<BitVectorSize>());
367		}
368	14547	else if (tn.isBoolean())
369		{
370	13878	n = NodeManager::currentNM()->mkConst(true);
371		}
372	14920	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	1195	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	2390	TypeNode tn = n.getType();
446	1195	if (n == mkTypeValue(tn, 0))
447		{
448	555	if (ik == PLUS \|\| ik == OR \|\| ik == XOR \|\| ik == BITVECTOR_ADD
449	428	\|\| ik == BITVECTOR_OR \|\| ik == BITVECTOR_XOR \|\| ik == STRING_CONCAT)
450		{
451	144	return true;
452		}
453	411	else if (ik == MINUS \|\| ik == BITVECTOR_SHL \|\| ik == BITVECTOR_LSHR
454	361	\|\| ik == BITVECTOR_ASHR \|\| ik == BITVECTOR_SUB
455	361	\|\| ik == BITVECTOR_UREM)
456		{
457	57	return arg == 1;
458		}
459		}
460	640	else if (n == mkTypeValue(tn, 1))
461		{
462	379	if (ik == MULT \|\| ik == BITVECTOR_MULT)
463		{
464	5	return true;
465		}
466	374	else if (ik == DIVISION \|\| ik == DIVISION_TOTAL \|\| ik == INTS_DIVISION
467	370	\|\| ik == INTS_DIVISION_TOTAL
468	370	\|\| ik == INTS_MODULUS
469	370	\|\| ik == INTS_MODULUS_TOTAL
470	370	\|\| ik == BITVECTOR_UDIV
471	363	\|\| ik == BITVECTOR_SDIV)
472		{
473	20	return arg == 1;
474		}
475		}
476	261	else if (n == mkTypeMaxValue(tn))
477		{
478	170	if (ik == EQUAL \|\| ik == BITVECTOR_AND \|\| ik == BITVECTOR_XNOR)
479		{
480		return true;
481		}
482		}
483	969	return false;
484		}
485
486	1006	Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
487		{
488	2012	TypeNode tn = n.getType();
489	1006	if (n == mkTypeValue(tn, 0))
490		{
491	382	if (ik == AND \|\| ik == MULT \|\| ik == BITVECTOR_AND \|\| ik == BITVECTOR_MULT)
492		{
493	47	return n;
494		}
495	335	else if (ik == BITVECTOR_SHL \|\| ik == BITVECTOR_LSHR \|\| ik == BITVECTOR_ASHR
496	335	\|\| ik == BITVECTOR_UREM)
497		{
498	3	if (arg == 0)
499		{
500	3	return n;
501		}
502		}
503	332	else if (ik == BITVECTOR_UDIV \|\| ik == BITVECTOR_UDIV
504	325	\|\| 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	318	else if (ik == DIVISION \|\| ik == DIVISION_TOTAL \|\| ik == INTS_DIVISION
516	316	\|\| ik == INTS_DIVISION_TOTAL
517	316	\|\| ik == INTS_MODULUS
518	313	\|\| ik == INTS_MODULUS_TOTAL)
519		{
520	7	if (arg == 0)
521		{
522	3	return n;
523		}
524		}
525	313	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	313	else if (ik == STRING_INDEXOF)
537		{
538		if (arg == 0 \|\| arg == 1)
539		{
540		return mkTypeValue(NodeManager::currentNM()->integerType(), -1);
541		}
542		}
543		}
544	624	else if (n == mkTypeValue(tn, 1))
545		{
546	363	if (ik == BITVECTOR_UREM)
547		{
548	7	return mkTypeValue(tn, 0);
549		}
550		}
551	261	else if (n == mkTypeMaxValue(tn))
552		{
553	170	if (ik == OR \|\| ik == BITVECTOR_OR)
554		{
555	57	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	875	return Node::null();
575		}
576
577	676	bool TermUtil::hasOffsetArg(Kind ik, int arg, int& offset, Kind& ok)
578		{
579	676	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	672	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	660	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	648	return false;
601		}
602
603		} // namespace quantifiers
604		} // namespace theory
605	29340	} // namespace cvc5