Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arrays/theory_arrays_rewriter.cpp	Lines:	341	346	98.6 %
Date:	2021-05-22	Branches:	832	1565	53.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters
 *
 * 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.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include "expr/attribute.h"
#include "theory/arrays/theory_arrays_rewriter.h"

namespace cvc5 {
namespace theory {
namespace arrays {

namespace attr {
  struct ArrayConstantMostFrequentValueTag { };
  struct ArrayConstantMostFrequentValueCountTag { };
  }  // namespace attr

typedef expr::Attribute<attr::ArrayConstantMostFrequentValueCountTag, uint64_t> ArrayConstantMostFrequentValueCountAttr;
typedef expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node> ArrayConstantMostFrequentValueAttr;

Node getMostFrequentValue(TNode store) {
  return store.getAttribute(ArrayConstantMostFrequentValueAttr());
}
uint64_t getMostFrequentValueCount(TNode store) {
  return store.getAttribute(ArrayConstantMostFrequentValueCountAttr());
}

void setMostFrequentValue(TNode store, TNode value) {
  return store.setAttribute(ArrayConstantMostFrequentValueAttr(), value);
}
void setMostFrequentValueCount(TNode store, uint64_t count) {
  return store.setAttribute(ArrayConstantMostFrequentValueCountAttr(), count);
}

Node TheoryArraysRewriter::normalizeConstant(TNode node)
{
  return normalizeConstant(node, node[1].getType().getCardinality());
}

// this function is called by printers when using the option "--model-u-dt-enum"
Node TheoryArraysRewriter::normalizeConstant(TNode node, Cardinality indexCard)
{
  TNode store = node[0];
  TNode index = node[1];
  TNode value = node[2];

  std::vector<TNode> indices;
  std::vector<TNode> elements;

  // Normal form for nested stores is just ordering by index - but also need
  // to check if we are writing to default value

  // Go through nested stores looking for where to insert index
  // Also check whether we are replacing an existing store
  TNode replacedValue;
  uint32_t depth = 1;
  uint32_t valCount = 1;
  while (store.getKind() == kind::STORE)
  {
    if (index == store[1])
    {
      replacedValue = store[2];
      store = store[0];
      break;
    }
    else if (index >= store[1])
    {
      break;
    }
    if (value == store[2])
    {
      valCount += 1;
    }
    depth += 1;
    indices.push_back(store[1]);
    elements.push_back(store[2]);
    store = store[0];
  }
  Node n = store;

  // Get the default value at the bottom of the nested stores
  while (store.getKind() == kind::STORE)
  {
    if (value == store[2])
    {
      valCount += 1;
    }
    depth += 1;
    store = store[0];
  }
  Assert(store.getKind() == kind::STORE_ALL);
  ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
  Node defaultValue = storeAll.getValue();
  NodeManager* nm = NodeManager::currentNM();

  // Check if we are writing to default value - if so the store
  // to index can be ignored
  if (value == defaultValue)
  {
    if (replacedValue.isNull())
    {
      // Quick exit - if writing to default value and nothing was
      // replaced, we can just return node[0]
      return node[0];
    }
    // else rebuild the store without the replaced write and then exit
  }
  else
  {
    n = nm->mkNode(kind::STORE, n, index, value);
  }

  // Build the rest of the store after inserting/deleting
  while (!indices.empty())
  {
    n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
    indices.pop_back();
    elements.pop_back();
  }

  // Ready to exit if write was to the default value (see previous comment)
  if (value == defaultValue)
  {
    return n;
  }

  if (indexCard.isInfinite())
  {
    return n;
  }

  // When index sort is finite, we have to check whether there is any value
  // that is written to more than the default value.  If so, it must become
  // the new default value

  TNode mostFrequentValue;
  uint32_t mostFrequentValueCount = 0;
  store = node[0];
  if (store.getKind() == kind::STORE)
  {
    mostFrequentValue = getMostFrequentValue(store);
    mostFrequentValueCount = getMostFrequentValueCount(store);
  }

  // Compute the most frequently written value for n
  if (valCount > mostFrequentValueCount
      || (valCount == mostFrequentValueCount && value < mostFrequentValue))
  {
    mostFrequentValue = value;
    mostFrequentValueCount = valCount;
  }

  // Need to make sure the default value count is larger, or the same and the
  // default value is expression-order-less-than nextValue
  Cardinality::CardinalityComparison compare =
      indexCard.compare(mostFrequentValueCount + depth);
  Assert(compare != Cardinality::UNKNOWN);
  if (compare == Cardinality::GREATER
      || (compare == Cardinality::EQUAL && (defaultValue < mostFrequentValue)))
  {
    return n;
  }

  // Bad case: have to recompute value counts and/or possibly switch out
  // default value
  store = n;
  std::unordered_set<TNode> indexSet;
  std::unordered_map<TNode, uint32_t> elementsMap;
  std::unordered_map<TNode, uint32_t>::iterator it;
  uint32_t count;
  uint32_t max = 0;
  TNode maxValue;
  while (store.getKind() == kind::STORE)
  {
    indices.push_back(store[1]);
    indexSet.insert(store[1]);
    elements.push_back(store[2]);
    it = elementsMap.find(store[2]);
    if (it != elementsMap.end())
    {
      (*it).second = (*it).second + 1;
      count = (*it).second;
    }
    else
    {
      elementsMap[store[2]] = 1;
      count = 1;
    }
    if (count > max || (count == max && store[2] < maxValue))
    {
      max = count;
      maxValue = store[2];
    }
    store = store[0];
  }

  Assert(depth == indices.size());
  compare = indexCard.compare(max + depth);
  Assert(compare != Cardinality::UNKNOWN);
  if (compare == Cardinality::GREATER
      || (compare == Cardinality::EQUAL && (defaultValue < maxValue)))
  {
    Assert(!replacedValue.isNull() && mostFrequentValue == replacedValue);
    return n;
  }

  // Out of luck: have to swap out default value

  // Enumerate values from index type into newIndices and sort
  std::vector<Node> newIndices;
  TypeEnumerator te(index.getType());
  bool needToSort = false;
  uint32_t numTe = 0;
  while (!te.isFinished()
         && (!indexCard.isFinite()
             || numTe < indexCard.getFiniteCardinality().toUnsignedInt()))
  {
    if (indexSet.find(*te) == indexSet.end())
    {
      if (!newIndices.empty() && (!(newIndices.back() < (*te))))
      {
        needToSort = true;
      }
      newIndices.push_back(*te);
    }
    ++numTe;
    ++te;
  }
  Assert(indexCard.compare(newIndices.size() + depth) == Cardinality::EQUAL);
  if (needToSort)
  {
    std::sort(newIndices.begin(), newIndices.end());
  }

  n = nm->mkConst(ArrayStoreAll(node.getType(), maxValue));
  std::vector<Node>::iterator itNew = newIndices.begin(),
                              it_end = newIndices.end();
  while (itNew != it_end || !indices.empty())
  {
    if (itNew != it_end && (indices.empty() || (*itNew) < indices.back()))
    {
      n = nm->mkNode(kind::STORE, n, (*itNew), defaultValue);
      ++itNew;
    }
    else if (itNew == it_end || indices.back() < (*itNew))
    {
      if (elements.back() != maxValue)
      {
        n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
      }
      indices.pop_back();
      elements.pop_back();
    }
  }
  return n;
}

RewriteResponse TheoryArraysRewriter::postRewrite(TNode node)
{
  Trace("arrays-postrewrite")
      << "Arrays::postRewrite start " << node << std::endl;
  switch (node.getKind())
  {
    case kind::SELECT:
    {
      TNode store = node[0];
      TNode index = node[1];
      Node n;
      bool val;
      while (store.getKind() == kind::STORE)
      {
        if (index == store[1])
        {
          val = true;
        }
        else if (index.isConst() && store[1].isConst())
        {
          val = false;
        }
        else
        {
          n = Rewriter::rewrite(mkEqNode(store[1], index));
          if (n.getKind() != kind::CONST_BOOLEAN)
          {
            break;
          }
          val = n.getConst<bool>();
        }
        if (val)
        {
          // select(store(a,i,v),j) = v if i = j
          Trace("arrays-postrewrite")
              << "Arrays::postRewrite returning " << store[2] << std::endl;
          return RewriteResponse(REWRITE_DONE, store[2]);
        }
        // select(store(a,i,v),j) = select(a,j) if i /= j
        store = store[0];
      }
      if (store.getKind() == kind::STORE_ALL)
      {
        // select(store_all(v),i) = v
        ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
        n = storeAll.getValue();
        Trace("arrays-postrewrite")
            << "Arrays::postRewrite returning " << n << std::endl;
        Assert(n.isConst());
        return RewriteResponse(REWRITE_DONE, n);
      }
      else if (store != node[0])
      {
        n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
        Trace("arrays-postrewrite")
            << "Arrays::postRewrite returning " << n << std::endl;
        return RewriteResponse(REWRITE_DONE, n);
      }
      break;
    }
    case kind::STORE:
    {
      TNode store = node[0];
      TNode value = node[2];
      // store(a,i,select(a,i)) = a
      if (value.getKind() == kind::SELECT && value[0] == store
          && value[1] == node[1])
      {
        Trace("arrays-postrewrite")
            << "Arrays::postRewrite returning " << store << std::endl;
        return RewriteResponse(REWRITE_DONE, store);
      }
      TNode index = node[1];
      if (store.isConst() && index.isConst() && value.isConst())
      {
        // normalize constant
        Node n = normalizeConstant(node);
        Assert(n.isConst());
        Trace("arrays-postrewrite")
            << "Arrays::postRewrite returning " << n << std::endl;
        return RewriteResponse(REWRITE_DONE, n);
      }
      if (store.getKind() == kind::STORE)
      {
        // store(store(a,i,v),j,w)
        bool val;
        if (index == store[1])
        {
          val = true;
        }
        else if (index.isConst() && store[1].isConst())
        {
          val = false;
        }
        else
        {
          Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
          if (eqRewritten.getKind() != kind::CONST_BOOLEAN)
          {
            Trace("arrays-postrewrite")
                << "Arrays::postRewrite returning " << node << std::endl;
            return RewriteResponse(REWRITE_DONE, node);
          }
          val = eqRewritten.getConst<bool>();
        }
        NodeManager* nm = NodeManager::currentNM();
        if (val)
        {
          // store(store(a,i,v),i,w) = store(a,i,w)
          Node result = nm->mkNode(kind::STORE, store[0], index, value);
          Trace("arrays-postrewrite")
              << "Arrays::postRewrite returning " << result << std::endl;
          return RewriteResponse(REWRITE_AGAIN, result);
        }
        else if (index < store[1])
        {
          // store(store(a,i,v),j,w) = store(store(a,j,w),i,v)
          //    IF i != j and j comes before i in the ordering
          std::vector<TNode> indices;
          std::vector<TNode> elements;
          indices.push_back(store[1]);
          elements.push_back(store[2]);
          store = store[0];
          Node n;
          while (store.getKind() == kind::STORE)
          {
            if (index == store[1])
            {
              val = true;
            }
            else if (index.isConst() && store[1].isConst())
            {
              val = false;
            }
            else
            {
              n = Rewriter::rewrite(mkEqNode(store[1], index));
              if (n.getKind() != kind::CONST_BOOLEAN)
              {
                break;
              }
              val = n.getConst<bool>();
            }
            if (val)
            {
              store = store[0];
              break;
            }
            else if (!(index < store[1]))
            {
              break;
            }
            indices.push_back(store[1]);
            elements.push_back(store[2]);
            store = store[0];
          }
          if (value.getKind() == kind::SELECT && value[0] == store
              && value[1] == index)
          {
            n = store;
          }
          else
          {
            n = nm->mkNode(kind::STORE, store, index, value);
          }
          while (!indices.empty())
          {
            n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
            indices.pop_back();
            elements.pop_back();
          }
          Assert(n != node);
          Trace("arrays-postrewrite")
              << "Arrays::postRewrite returning " << n << std::endl;
          return RewriteResponse(REWRITE_AGAIN, n);
        }
      }
      break;
    }
    case kind::EQUAL:
    {
      if (node[0] == node[1])
      {
        Trace("arrays-postrewrite")
            << "Arrays::postRewrite returning true" << std::endl;
        return RewriteResponse(REWRITE_DONE,
                               NodeManager::currentNM()->mkConst(true));
      }
      else if (node[0].isConst() && node[1].isConst())
      {
        Trace("arrays-postrewrite")
            << "Arrays::postRewrite returning false" << std::endl;
        return RewriteResponse(REWRITE_DONE,
                               NodeManager::currentNM()->mkConst(false));
      }
      if (node[0] > node[1])
      {
        Node newNode =
            NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
        Trace("arrays-postrewrite")
            << "Arrays::postRewrite returning " << newNode << std::endl;
        return RewriteResponse(REWRITE_DONE, newNode);
      }
      break;
    }
    default: break;
  }
  Trace("arrays-postrewrite")
      << "Arrays::postRewrite returning " << node << std::endl;
  return RewriteResponse(REWRITE_DONE, node);
}

RewriteResponse TheoryArraysRewriter::preRewrite(TNode node)
{
  Trace("arrays-prerewrite")
      << "Arrays::preRewrite start " << node << std::endl;
  switch (node.getKind())
  {
    case kind::SELECT:
    {
      TNode store = node[0];
      TNode index = node[1];
      Node n;
      bool val;
      while (store.getKind() == kind::STORE)
      {
        if (index == store[1])
        {
          val = true;
        }
        else if (index.isConst() && store[1].isConst())
        {
          val = false;
        }
        else
        {
          n = Rewriter::rewrite(mkEqNode(store[1], index));
          if (n.getKind() != kind::CONST_BOOLEAN)
          {
            break;
          }
          val = n.getConst<bool>();
        }
        if (val)
        {
          // select(store(a,i,v),j) = v if i = j
          Trace("arrays-prerewrite")
              << "Arrays::preRewrite returning " << store[2] << std::endl;
          return RewriteResponse(REWRITE_AGAIN, store[2]);
        }
        // select(store(a,i,v),j) = select(a,j) if i /= j
        store = store[0];
      }
      if (store.getKind() == kind::STORE_ALL)
      {
        // select(store_all(v),i) = v
        ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
        n = storeAll.getValue();
        Trace("arrays-prerewrite")
            << "Arrays::preRewrite returning " << n << std::endl;
        Assert(n.isConst());
        return RewriteResponse(REWRITE_DONE, n);
      }
      else if (store != node[0])
      {
        n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
        Trace("arrays-prerewrite")
            << "Arrays::preRewrite returning " << n << std::endl;
        return RewriteResponse(REWRITE_DONE, n);
      }
      break;
    }
    case kind::STORE:
    {
      TNode store = node[0];
      TNode value = node[2];
      // store(a,i,select(a,i)) = a
      if (value.getKind() == kind::SELECT && value[0] == store
          && value[1] == node[1])
      {
        Trace("arrays-prerewrite")
            << "Arrays::preRewrite returning " << store << std::endl;
        return RewriteResponse(REWRITE_AGAIN, store);
      }
      if (store.getKind() == kind::STORE)
      {
        // store(store(a,i,v),j,w)
        TNode index = node[1];
        bool val;
        if (index == store[1])
        {
          val = true;
        }
        else if (index.isConst() && store[1].isConst())
        {
          val = false;
        }
        else
        {
          Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
          if (eqRewritten.getKind() != kind::CONST_BOOLEAN)
          {
            break;
          }
          val = eqRewritten.getConst<bool>();
        }
        NodeManager* nm = NodeManager::currentNM();
        if (val)
        {
          // store(store(a,i,v),i,w) = store(a,i,w)
          Node newNode = nm->mkNode(kind::STORE, store[0], index, value);
          Trace("arrays-prerewrite")
              << "Arrays::preRewrite returning " << newNode << std::endl;
          return RewriteResponse(REWRITE_DONE, newNode);
        }
      }
      break;
    }
    case kind::EQUAL:
    {
      if (node[0] == node[1])
      {
        Trace("arrays-prerewrite")
            << "Arrays::preRewrite returning true" << std::endl;
        return RewriteResponse(REWRITE_DONE,
                               NodeManager::currentNM()->mkConst(true));
      }
      break;
    }
    default: break;
  }

  Trace("arrays-prerewrite")
      << "Arrays::preRewrite returning " << node << std::endl;
  return RewriteResponse(REWRITE_DONE, node);
}

TrustNode TheoryArraysRewriter::expandDefinition(Node node)
{
  NodeManager* nm = NodeManager::currentNM();
  Kind kind = node.getKind();

  /* Expand
   *
   *   (eqrange a b i j)
   *
   * to
   *
   *  forall k . i <= k <= j => a[k] = b[k]
   *
   */
  if (kind == kind::EQ_RANGE)
  {
    TNode a = node[0];
    TNode b = node[1];
    TNode i = node[2];
    TNode j = node[3];
    Node k = nm->mkBoundVar(i.getType());
    Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, k);
    TypeNode type = k.getType();

    Kind kle;
    Node range;
    if (type.isBitVector())
    {
      kle = kind::BITVECTOR_ULE;
    }
    else if (type.isFloatingPoint())
    {
      kle = kind::FLOATINGPOINT_LEQ;
    }
    else if (type.isInteger() || type.isReal())
    {
      kle = kind::LEQ;
    }
    else
    {
      Unimplemented() << "Type " << type << " is not supported for predicate "
                      << kind;
    }

    range = nm->mkNode(kind::AND, nm->mkNode(kle, i, k), nm->mkNode(kle, k, j));

    Node eq = nm->mkNode(kind::EQUAL,
                         nm->mkNode(kind::SELECT, a, k),
                         nm->mkNode(kind::SELECT, b, k));
    Node implies = nm->mkNode(kind::IMPLIES, range, eq);
    Node ret = nm->mkNode(kind::FORALL, bvl, implies);
    return TrustNode::mkTrustRewrite(node, ret, nullptr);
  }
  return TrustNode::null();
}

}  // namespace arrays
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters
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		* [[ Add one-line brief description here ]]
14		*
15		* [[ Add lengthier description here ]]
16		* \todo document this file
17		*/
18
19		#include "expr/attribute.h"
20		#include "theory/arrays/theory_arrays_rewriter.h"
21
22		namespace cvc5 {
23		namespace theory {
24		namespace arrays {
25
26		namespace attr {
27		struct ArrayConstantMostFrequentValueTag { };
28		struct ArrayConstantMostFrequentValueCountTag { };
29		} // namespace attr
30
31		typedef expr::Attribute<attr::ArrayConstantMostFrequentValueCountTag, uint64_t> ArrayConstantMostFrequentValueCountAttr;
32		typedef expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node> ArrayConstantMostFrequentValueAttr;
33
34	1032	Node getMostFrequentValue(TNode store) {
35	1032	return store.getAttribute(ArrayConstantMostFrequentValueAttr());
36		}
37	1032	uint64_t getMostFrequentValueCount(TNode store) {
38	1032	return store.getAttribute(ArrayConstantMostFrequentValueCountAttr());
39		}
40
41	500	void setMostFrequentValue(TNode store, TNode value) {
42	500	return store.setAttribute(ArrayConstantMostFrequentValueAttr(), value);
43		}
44	500	void setMostFrequentValueCount(TNode store, uint64_t count) {
45	500	return store.setAttribute(ArrayConstantMostFrequentValueCountAttr(), count);
46		}
47
48	7872	Node TheoryArraysRewriter::normalizeConstant(TNode node)
49		{
50	7872	return normalizeConstant(node, node[1].getType().getCardinality());
51		}
52
53		// this function is called by printers when using the option "--model-u-dt-enum"
54	7872	Node TheoryArraysRewriter::normalizeConstant(TNode node, Cardinality indexCard)
55		{
56	15744	TNode store = node[0];
57	15744	TNode index = node[1];
58	15744	TNode value = node[2];
59
60	15744	std::vector<TNode> indices;
61	15744	std::vector<TNode> elements;
62
63		// Normal form for nested stores is just ordering by index - but also need
64		// to check if we are writing to default value
65
66		// Go through nested stores looking for where to insert index
67		// Also check whether we are replacing an existing store
68	15744	TNode replacedValue;
69	7872	uint32_t depth = 1;
70	7872	uint32_t valCount = 1;
71	9314	while (store.getKind() == kind::STORE)
72		{
73	2711	if (index == store[1])
74		{
75	159	replacedValue = store[2];
76	159	store = store[0];
77	159	break;
78		}
79	2552	else if (index >= store[1])
80		{
81	1831	break;
82		}
83	721	if (value == store[2])
84		{
85	134	valCount += 1;
86		}
87	721	depth += 1;
88	721	indices.push_back(store[1]);
89	721	elements.push_back(store[2]);
90	721	store = store[0];
91		}
92	15744	Node n = store;
93
94		// Get the default value at the bottom of the nested stores
95	18266	while (store.getKind() == kind::STORE)
96		{
97	5197	if (value == store[2])
98		{
99	629	valCount += 1;
100		}
101	5197	depth += 1;
102	5197	store = store[0];
103		}
104	7872	Assert(store.getKind() == kind::STORE_ALL);
105	15744	ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
106	15744	Node defaultValue = storeAll.getValue();
107	7872	NodeManager* nm = NodeManager::currentNM();
108
109		// Check if we are writing to default value - if so the store
110		// to index can be ignored
111	7872	if (value == defaultValue)
112		{
113	344	if (replacedValue.isNull())
114		{
115		// Quick exit - if writing to default value and nothing was
116		// replaced, we can just return node[0]
117	332	return node[0];
118		}
119		// else rebuild the store without the replaced write and then exit
120		}
121		else
122		{
123	7528	n = nm->mkNode(kind::STORE, n, index, value);
124		}
125
126		// Build the rest of the store after inserting/deleting
127	8798	while (!indices.empty())
128		{
129	629	n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
130	629	indices.pop_back();
131	629	elements.pop_back();
132		}
133
134		// Ready to exit if write was to the default value (see previous comment)
135	7540	if (value == defaultValue)
136		{
137	12	return n;
138		}
139
140	7528	if (indexCard.isInfinite())
141		{
142	6146	return n;
143		}
144
145		// When index sort is finite, we have to check whether there is any value
146		// that is written to more than the default value. If so, it must become
147		// the new default value
148
149	2764	TNode mostFrequentValue;
150	1382	uint32_t mostFrequentValueCount = 0;
151	1382	store = node[0];
152	1382	if (store.getKind() == kind::STORE)
153		{
154	786	mostFrequentValue = getMostFrequentValue(store);
155	786	mostFrequentValueCount = getMostFrequentValueCount(store);
156		}
157
158		// Compute the most frequently written value for n
159	1382	if (valCount > mostFrequentValueCount
160	1382	\|\| (valCount == mostFrequentValueCount && value < mostFrequentValue))
161		{
162	878	mostFrequentValue = value;
163	878	mostFrequentValueCount = valCount;
164		}
165
166		// Need to make sure the default value count is larger, or the same and the
167		// default value is expression-order-less-than nextValue
168		Cardinality::CardinalityComparison compare =
169	1382	indexCard.compare(mostFrequentValueCount + depth);
170	1382	Assert(compare != Cardinality::UNKNOWN);
171	1382	if (compare == Cardinality::GREATER
172	1382	\|\| (compare == Cardinality::EQUAL && (defaultValue < mostFrequentValue)))
173		{
174	1312	return n;
175		}
176
177		// Bad case: have to recompute value counts and/or possibly switch out
178		// default value
179	70	store = n;
180	140	std::unordered_set<TNode> indexSet;
181	140	std::unordered_map<TNode, uint32_t> elementsMap;
182	70	std::unordered_map<TNode, uint32_t>::iterator it;
183		uint32_t count;
184	70	uint32_t max = 0;
185	140	TNode maxValue;
186	296	while (store.getKind() == kind::STORE)
187		{
188	113	indices.push_back(store[1]);
189	113	indexSet.insert(store[1]);
190	113	elements.push_back(store[2]);
191	113	it = elementsMap.find(store[2]);
192	113	if (it != elementsMap.end())
193		{
194	31	(it).second = (it).second + 1;
195	31	count = (*it).second;
196		}
197		else
198		{
199	82	elementsMap[store[2]] = 1;
200	82	count = 1;
201		}
202	113	if (count > max \|\| (count == max && store[2] < maxValue))
203		{
204	108	max = count;
205	108	maxValue = store[2];
206		}
207	113	store = store[0];
208		}
209
210	70	Assert(depth == indices.size());
211	70	compare = indexCard.compare(max + depth);
212	70	Assert(compare != Cardinality::UNKNOWN);
213	70	if (compare == Cardinality::GREATER
214	70	\|\| (compare == Cardinality::EQUAL && (defaultValue < maxValue)))
215		{
216		Assert(!replacedValue.isNull() && mostFrequentValue == replacedValue);
217		return n;
218		}
219
220		// Out of luck: have to swap out default value
221
222		// Enumerate values from index type into newIndices and sort
223	140	std::vector<Node> newIndices;
224	140	TypeEnumerator te(index.getType());
225	70	bool needToSort = false;
226	70	uint32_t numTe = 0;
227	450	while (!te.isFinished()
228	970	&& (!indexCard.isFinite()
229	450	\|\| numTe < indexCard.getFiniteCardinality().toUnsignedInt()))
230		{
231	190	if (indexSet.find(*te) == indexSet.end())
232		{
233	77	if (!newIndices.empty() && (!(newIndices.back() < (*te))))
234		{
235	6	needToSort = true;
236		}
237	77	newIndices.push_back(*te);
238		}
239	190	++numTe;
240	190	++te;
241		}
242	70	Assert(indexCard.compare(newIndices.size() + depth) == Cardinality::EQUAL);
243	70	if (needToSort)
244		{
245	4	std::sort(newIndices.begin(), newIndices.end());
246		}
247
248	70	n = nm->mkConst(ArrayStoreAll(node.getType(), maxValue));
249	70	std::vector<Node>::iterator itNew = newIndices.begin(),
250	70	it_end = newIndices.end();
251	450	while (itNew != it_end \|\| !indices.empty())
252		{
253	190	if (itNew != it_end && (indices.empty() \|\| (*itNew) < indices.back()))
254		{
255	77	n = nm->mkNode(kind::STORE, n, (*itNew), defaultValue);
256	77	++itNew;
257		}
258	113	else if (itNew == it_end \|\| indices.back() < (*itNew))
259		{
260	113	if (elements.back() != maxValue)
261		{
262	12	n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
263		}
264	113	indices.pop_back();
265	113	elements.pop_back();
266		}
267		}
268	70	return n;
269		}
270
271	58438	RewriteResponse TheoryArraysRewriter::postRewrite(TNode node)
272		{
273	116876	Trace("arrays-postrewrite")
274	58438	<< "Arrays::postRewrite start " << node << std::endl;
275	58438	switch (node.getKind())
276		{
277	21812	case kind::SELECT:
278		{
279	21812	TNode store = node[0];
280	21812	TNode index = node[1];
281	21812	Node n;
282		bool val;
283	23060	while (store.getKind() == kind::STORE)
284		{
285	8759	if (index == store[1])
286		{
287	39	val = true;
288		}
289	8720	else if (index.isConst() && store[1].isConst())
290		{
291	294	val = false;
292		}
293		else
294		{
295	8426	n = Rewriter::rewrite(mkEqNode(store[1], index));
296	8426	if (n.getKind() != kind::CONST_BOOLEAN)
297		{
298	8096	break;
299		}
300	330	val = n.getConst<bool>();
301		}
302	663	if (val)
303		{
304		// select(store(a,i,v),j) = v if i = j
305	78	Trace("arrays-postrewrite")
306	39	<< "Arrays::postRewrite returning " << store[2] << std::endl;
307	39	return RewriteResponse(REWRITE_DONE, store[2]);
308		}
309		// select(store(a,i,v),j) = select(a,j) if i /= j
310	624	store = store[0];
311		}
312	21773	if (store.getKind() == kind::STORE_ALL)
313		{
314		// select(store_all(v),i) = v
315	522	ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
316	261	n = storeAll.getValue();
317	522	Trace("arrays-postrewrite")
318	261	<< "Arrays::postRewrite returning " << n << std::endl;
319	261	Assert(n.isConst());
320	261	return RewriteResponse(REWRITE_DONE, n);
321		}
322	21512	else if (store != node[0])
323		{
324	64	n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
325	128	Trace("arrays-postrewrite")
326	64	<< "Arrays::postRewrite returning " << n << std::endl;
327	64	return RewriteResponse(REWRITE_DONE, n);
328		}
329	21448	break;
330		}
331	17042	case kind::STORE:
332		{
333	17042	TNode store = node[0];
334	17042	TNode value = node[2];
335		// store(a,i,select(a,i)) = a
336	35026	if (value.getKind() == kind::SELECT && value[0] == store
337	34314	&& value[1] == node[1])
338		{
339	80	Trace("arrays-postrewrite")
340	40	<< "Arrays::postRewrite returning " << store << std::endl;
341	40	return RewriteResponse(REWRITE_DONE, store);
342		}
343	17002	TNode index = node[1];
344	17002	if (store.isConst() && index.isConst() && value.isConst())
345		{
346		// normalize constant
347	15744	Node n = normalizeConstant(node);
348	7872	Assert(n.isConst());
349	15744	Trace("arrays-postrewrite")
350	7872	<< "Arrays::postRewrite returning " << n << std::endl;
351	7872	return RewriteResponse(REWRITE_DONE, n);
352		}
353	9130	if (store.getKind() == kind::STORE)
354		{
355		// store(store(a,i,v),j,w)
356		bool val;
357	6314	if (index == store[1])
358		{
359	22	val = true;
360		}
361	6292	else if (index.isConst() && store[1].isConst())
362		{
363	436	val = false;
364		}
365		else
366		{
367	9498	Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
368	5856	if (eqRewritten.getKind() != kind::CONST_BOOLEAN)
369		{
370	4428	Trace("arrays-postrewrite")
371	2214	<< "Arrays::postRewrite returning " << node << std::endl;
372	2214	return RewriteResponse(REWRITE_DONE, node);
373		}
374	3642	val = eqRewritten.getConst<bool>();
375		}
376	4100	NodeManager* nm = NodeManager::currentNM();
377	4100	if (val)
378		{
379		// store(store(a,i,v),i,w) = store(a,i,w)
380	44	Node result = nm->mkNode(kind::STORE, store[0], index, value);
381	44	Trace("arrays-postrewrite")
382	22	<< "Arrays::postRewrite returning " << result << std::endl;
383	22	return RewriteResponse(REWRITE_AGAIN, result);
384		}
385	4078	else if (index < store[1])
386		{
387		// store(store(a,i,v),j,w) = store(store(a,j,w),i,v)
388		// IF i != j and j comes before i in the ordering
389	406	std::vector<TNode> indices;
390	406	std::vector<TNode> elements;
391	203	indices.push_back(store[1]);
392	203	elements.push_back(store[2]);
393	203	store = store[0];
394	406	Node n;
395	1669	while (store.getKind() == kind::STORE)
396		{
397	839	if (index == store[1])
398		{
399	8	val = true;
400		}
401	831	else if (index.isConst() && store[1].isConst())
402		{
403	20	val = false;
404		}
405		else
406		{
407	811	n = Rewriter::rewrite(mkEqNode(store[1], index));
408	811	if (n.getKind() != kind::CONST_BOOLEAN)
409		{
410	28	break;
411		}
412	783	val = n.getConst<bool>();
413		}
414	811	if (val)
415		{
416	8	store = store[0];
417	8	break;
418		}
419	803	else if (!(index < store[1]))
420		{
421	70	break;
422		}
423	733	indices.push_back(store[1]);
424	733	elements.push_back(store[2]);
425	733	store = store[0];
426		}
427	431	if (value.getKind() == kind::SELECT && value[0] == store
428	420	&& value[1] == index)
429		{
430	6	n = store;
431		}
432		else
433		{
434	197	n = nm->mkNode(kind::STORE, store, index, value);
435		}
436	2075	while (!indices.empty())
437		{
438	936	n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
439	936	indices.pop_back();
440	936	elements.pop_back();
441		}
442	203	Assert(n != node);
443	406	Trace("arrays-postrewrite")
444	203	<< "Arrays::postRewrite returning " << n << std::endl;
445	203	return RewriteResponse(REWRITE_AGAIN, n);
446		}
447		}
448	6691	break;
449		}
450	18402	case kind::EQUAL:
451		{
452	18402	if (node[0] == node[1])
453		{
454	1424	Trace("arrays-postrewrite")
455	712	<< "Arrays::postRewrite returning true" << std::endl;
456		return RewriteResponse(REWRITE_DONE,
457	712	NodeManager::currentNM()->mkConst(true));
458		}
459	17690	else if (node[0].isConst() && node[1].isConst())
460		{
461	320	Trace("arrays-postrewrite")
462	160	<< "Arrays::postRewrite returning false" << std::endl;
463		return RewriteResponse(REWRITE_DONE,
464	160	NodeManager::currentNM()->mkConst(false));
465		}
466	17530	if (node[0] > node[1])
467		{
468		Node newNode =
469	6498	NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
470	6498	Trace("arrays-postrewrite")
471	3249	<< "Arrays::postRewrite returning " << newNode << std::endl;
472	3249	return RewriteResponse(REWRITE_DONE, newNode);
473		}
474	14281	break;
475		}
476	1182	default: break;
477		}
478	87204	Trace("arrays-postrewrite")
479	43602	<< "Arrays::postRewrite returning " << node << std::endl;
480	43602	return RewriteResponse(REWRITE_DONE, node);
481		}
482
483	32709	RewriteResponse TheoryArraysRewriter::preRewrite(TNode node)
484		{
485	65418	Trace("arrays-prerewrite")
486	32709	<< "Arrays::preRewrite start " << node << std::endl;
487	32709	switch (node.getKind())
488		{
489	12789	case kind::SELECT:
490		{
491	12789	TNode store = node[0];
492	12789	TNode index = node[1];
493	12789	Node n;
494		bool val;
495	17573	while (store.getKind() == kind::STORE)
496		{
497	7274	if (index == store[1])
498		{
499	824	val = true;
500		}
501	6450	else if (index.isConst() && store[1].isConst())
502		{
503	1662	val = false;
504		}
505		else
506		{
507	4788	n = Rewriter::rewrite(mkEqNode(store[1], index));
508	4788	if (n.getKind() != kind::CONST_BOOLEAN)
509		{
510	4005	break;
511		}
512	783	val = n.getConst<bool>();
513		}
514	3269	if (val)
515		{
516		// select(store(a,i,v),j) = v if i = j
517	1754	Trace("arrays-prerewrite")
518	877	<< "Arrays::preRewrite returning " << store[2] << std::endl;
519	877	return RewriteResponse(REWRITE_AGAIN, store[2]);
520		}
521		// select(store(a,i,v),j) = select(a,j) if i /= j
522	2392	store = store[0];
523		}
524	11912	if (store.getKind() == kind::STORE_ALL)
525		{
526		// select(store_all(v),i) = v
527	878	ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
528	439	n = storeAll.getValue();
529	878	Trace("arrays-prerewrite")
530	439	<< "Arrays::preRewrite returning " << n << std::endl;
531	439	Assert(n.isConst());
532	439	return RewriteResponse(REWRITE_DONE, n);
533		}
534	11473	else if (store != node[0])
535		{
536	277	n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
537	554	Trace("arrays-prerewrite")
538	277	<< "Arrays::preRewrite returning " << n << std::endl;
539	277	return RewriteResponse(REWRITE_DONE, n);
540		}
541	11196	break;
542		}
543	8627	case kind::STORE:
544		{
545	8627	TNode store = node[0];
546	8627	TNode value = node[2];
547		// store(a,i,select(a,i)) = a
548	17713	if (value.getKind() == kind::SELECT && value[0] == store
549	17372	&& value[1] == node[1])
550		{
551	30	Trace("arrays-prerewrite")
552	15	<< "Arrays::preRewrite returning " << store << std::endl;
553	15	return RewriteResponse(REWRITE_AGAIN, store);
554		}
555	8612	if (store.getKind() == kind::STORE)
556		{
557		// store(store(a,i,v),j,w)
558	6916	TNode index = node[1];
559		bool val;
560	4050	if (index == store[1])
561		{
562	202	val = true;
563		}
564	3848	else if (index.isConst() && store[1].isConst())
565		{
566	1309	val = false;
567		}
568		else
569		{
570	4110	Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
571	2539	if (eqRewritten.getKind() != kind::CONST_BOOLEAN)
572		{
573	968	break;
574		}
575	1571	val = eqRewritten.getConst<bool>();
576		}
577	3082	NodeManager* nm = NodeManager::currentNM();
578	3082	if (val)
579		{
580		// store(store(a,i,v),i,w) = store(a,i,w)
581	432	Node newNode = nm->mkNode(kind::STORE, store[0], index, value);
582	432	Trace("arrays-prerewrite")
583	216	<< "Arrays::preRewrite returning " << newNode << std::endl;
584	216	return RewriteResponse(REWRITE_DONE, newNode);
585		}
586		}
587	7428	break;
588		}
589	10781	case kind::EQUAL:
590		{
591	10781	if (node[0] == node[1])
592		{
593	1976	Trace("arrays-prerewrite")
594	988	<< "Arrays::preRewrite returning true" << std::endl;
595		return RewriteResponse(REWRITE_DONE,
596	988	NodeManager::currentNM()->mkConst(true));
597		}
598	9793	break;
599		}
600	512	default: break;
601		}
602
603	59794	Trace("arrays-prerewrite")
604	29897	<< "Arrays::preRewrite returning " << node << std::endl;
605	29897	return RewriteResponse(REWRITE_DONE, node);
606		}
607
608	23187	TrustNode TheoryArraysRewriter::expandDefinition(Node node)
609		{
610	23187	NodeManager* nm = NodeManager::currentNM();
611	23187	Kind kind = node.getKind();
612
613		/* Expand
614		*
615		* (eqrange a b i j)
616		*
617		* to
618		*
619		* forall k . i <= k <= j => a[k] = b[k]
620		*
621		*/
622	23187	if (kind == kind::EQ_RANGE)
623		{
624	40	TNode a = node[0];
625	40	TNode b = node[1];
626	40	TNode i = node[2];
627	40	TNode j = node[3];
628	40	Node k = nm->mkBoundVar(i.getType());
629	40	Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, k);
630	40	TypeNode type = k.getType();
631
632		Kind kle;
633	40	Node range;
634	20	if (type.isBitVector())
635		{
636	16	kle = kind::BITVECTOR_ULE;
637		}
638	4	else if (type.isFloatingPoint())
639		{
640		kle = kind::FLOATINGPOINT_LEQ;
641		}
642	4	else if (type.isInteger() \|\| type.isReal())
643		{
644	4	kle = kind::LEQ;
645		}
646		else
647		{
648		Unimplemented() << "Type " << type << " is not supported for predicate "
649		<< kind;
650		}
651
652	20	range = nm->mkNode(kind::AND, nm->mkNode(kle, i, k), nm->mkNode(kle, k, j));
653
654		Node eq = nm->mkNode(kind::EQUAL,
655	40	nm->mkNode(kind::SELECT, a, k),
656	80	nm->mkNode(kind::SELECT, b, k));
657	40	Node implies = nm->mkNode(kind::IMPLIES, range, eq);
658	40	Node ret = nm->mkNode(kind::FORALL, bvl, implies);
659	20	return TrustNode::mkTrustRewrite(node, ret, nullptr);
660		}
661	23167	return TrustNode::null();
662		}
663
664		} // namespace arrays
665		} // namespace theory
666	28191	} // namespace cvc5