Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arrays/theory_arrays_rewriter.cpp	Lines:	351	356	98.6 %
Date:	2021-08-16	Branches:	852	1613	52.8 %


/******************************************************************************
 * 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 "theory/arrays/theory_arrays_rewriter.h"

#include "expr/array_store_all.h"
#include "expr/attribute.h"
#include "proof/conv_proof_generator.h"
#include "proof/eager_proof_generator.h"
#include "theory/arrays/skolem_cache.h"
#include "util/cardinality.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);
}

TheoryArraysRewriter::TheoryArraysRewriter(ProofNodeManager* pnm)
    : d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr)
{
}

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;
}

Node TheoryArraysRewriter::expandEqRange(TNode node)
{
  Assert(node.getKind() == kind::EQ_RANGE);

  NodeManager* nm = NodeManager::currentNM();
  TNode a = node[0];
  TNode b = node[1];
  TNode i = node[2];
  TNode j = node[3];
  Node k = SkolemCache::getEqRangeVar(node);
  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 "
                    << node.getKind();
  }

  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);
  return nm->mkNode(kind::FORALL, bvl, implies);
}

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)
{
  Kind kind = node.getKind();

  if (kind == kind::EQ_RANGE)
  {
    Node expandedEqRange = expandEqRange(node);
    if (d_epg)
    {
      TrustNode tn = d_epg->mkTrustNode(node.eqNode(expandedEqRange),
                                        PfRule::ARRAYS_EQ_RANGE_EXPAND,
                                        {},
                                        {node});
      return TrustNode::mkTrustRewrite(node, expandedEqRange, d_epg.get());
    }
    return TrustNode::mkTrustRewrite(node, expandedEqRange, 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 "theory/arrays/theory_arrays_rewriter.h"
20
21		#include "expr/array_store_all.h"
22		#include "expr/attribute.h"
23		#include "proof/conv_proof_generator.h"
24		#include "proof/eager_proof_generator.h"
25		#include "theory/arrays/skolem_cache.h"
26		#include "util/cardinality.h"
27
28		namespace cvc5 {
29		namespace theory {
30		namespace arrays {
31
32		namespace attr {
33		struct ArrayConstantMostFrequentValueTag { };
34		struct ArrayConstantMostFrequentValueCountTag { };
35		} // namespace attr
36
37		typedef expr::Attribute<attr::ArrayConstantMostFrequentValueCountTag, uint64_t> ArrayConstantMostFrequentValueCountAttr;
38		typedef expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node> ArrayConstantMostFrequentValueAttr;
39
40	1146	Node getMostFrequentValue(TNode store) {
41	1146	return store.getAttribute(ArrayConstantMostFrequentValueAttr());
42		}
43	1146	uint64_t getMostFrequentValueCount(TNode store) {
44	1146	return store.getAttribute(ArrayConstantMostFrequentValueCountAttr());
45		}
46
47	575	void setMostFrequentValue(TNode store, TNode value) {
48	575	return store.setAttribute(ArrayConstantMostFrequentValueAttr(), value);
49		}
50	575	void setMostFrequentValueCount(TNode store, uint64_t count) {
51	575	return store.setAttribute(ArrayConstantMostFrequentValueCountAttr(), count);
52		}
53
54	9853	TheoryArraysRewriter::TheoryArraysRewriter(ProofNodeManager* pnm)
55	9853	: d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr)
56		{
57	9853	}
58
59	8024	Node TheoryArraysRewriter::normalizeConstant(TNode node)
60		{
61	8024	return normalizeConstant(node, node[1].getType().getCardinality());
62		}
63
64		// this function is called by printers when using the option "--model-u-dt-enum"
65	8024	Node TheoryArraysRewriter::normalizeConstant(TNode node, Cardinality indexCard)
66		{
67	16048	TNode store = node[0];
68	16048	TNode index = node[1];
69	16048	TNode value = node[2];
70
71	16048	std::vector<TNode> indices;
72	16048	std::vector<TNode> elements;
73
74		// Normal form for nested stores is just ordering by index - but also need
75		// to check if we are writing to default value
76
77		// Go through nested stores looking for where to insert index
78		// Also check whether we are replacing an existing store
79	16048	TNode replacedValue;
80	8024	uint32_t depth = 1;
81	8024	uint32_t valCount = 1;
82	9436	while (store.getKind() == kind::STORE)
83		{
84	2745	if (index == store[1])
85		{
86	146	replacedValue = store[2];
87	146	store = store[0];
88	146	break;
89		}
90	2599	else if (index >= store[1])
91		{
92	1893	break;
93		}
94	706	if (value == store[2])
95		{
96	144	valCount += 1;
97		}
98	706	depth += 1;
99	706	indices.push_back(store[1]);
100	706	elements.push_back(store[2]);
101	706	store = store[0];
102		}
103	16048	Node n = store;
104
105		// Get the default value at the bottom of the nested stores
106	18072	while (store.getKind() == kind::STORE)
107		{
108	5024	if (value == store[2])
109		{
110	635	valCount += 1;
111		}
112	5024	depth += 1;
113	5024	store = store[0];
114		}
115	8024	Assert(store.getKind() == kind::STORE_ALL);
116	16048	ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
117	16048	Node defaultValue = storeAll.getValue();
118	8024	NodeManager* nm = NodeManager::currentNM();
119
120		// Check if we are writing to default value - if so the store
121		// to index can be ignored
122	8024	if (value == defaultValue)
123		{
124	345	if (replacedValue.isNull())
125		{
126		// Quick exit - if writing to default value and nothing was
127		// replaced, we can just return node[0]
128	333	return node[0];
129		}
130		// else rebuild the store without the replaced write and then exit
131		}
132		else
133		{
134	7679	n = nm->mkNode(kind::STORE, n, index, value);
135		}
136
137		// Build the rest of the store after inserting/deleting
138	8913	while (!indices.empty())
139		{
140	611	n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
141	611	indices.pop_back();
142	611	elements.pop_back();
143		}
144
145		// Ready to exit if write was to the default value (see previous comment)
146	7691	if (value == defaultValue)
147		{
148	12	return n;
149		}
150
151	7679	if (indexCard.isInfinite())
152		{
153	6174	return n;
154		}
155
156		// When index sort is finite, we have to check whether there is any value
157		// that is written to more than the default value. If so, it must become
158		// the new default value
159
160	3010	TNode mostFrequentValue;
161	1505	uint32_t mostFrequentValueCount = 0;
162	1505	store = node[0];
163	1505	if (store.getKind() == kind::STORE)
164		{
165	851	mostFrequentValue = getMostFrequentValue(store);
166	851	mostFrequentValueCount = getMostFrequentValueCount(store);
167		}
168
169		// Compute the most frequently written value for n
170	1505	if (valCount > mostFrequentValueCount
171	1505	\|\| (valCount == mostFrequentValueCount && value < mostFrequentValue))
172		{
173	995	mostFrequentValue = value;
174	995	mostFrequentValueCount = valCount;
175		}
176
177		// Need to make sure the default value count is larger, or the same and the
178		// default value is expression-order-less-than nextValue
179		Cardinality::CardinalityComparison compare =
180	1505	indexCard.compare(mostFrequentValueCount + depth);
181	1505	Assert(compare != Cardinality::UNKNOWN);
182	1505	if (compare == Cardinality::GREATER
183	1505	\|\| (compare == Cardinality::EQUAL && (defaultValue < mostFrequentValue)))
184		{
185	1419	return n;
186		}
187
188		// Bad case: have to recompute value counts and/or possibly switch out
189		// default value
190	86	store = n;
191	172	std::unordered_set<TNode> indexSet;
192	172	std::unordered_map<TNode, uint32_t> elementsMap;
193	86	std::unordered_map<TNode, uint32_t>::iterator it;
194		uint32_t count;
195	86	uint32_t max = 0;
196	172	TNode maxValue;
197	370	while (store.getKind() == kind::STORE)
198		{
199	142	indices.push_back(store[1]);
200	142	indexSet.insert(store[1]);
201	142	elements.push_back(store[2]);
202	142	it = elementsMap.find(store[2]);
203	142	if (it != elementsMap.end())
204		{
205	39	(it).second = (it).second + 1;
206	39	count = (*it).second;
207		}
208		else
209		{
210	103	elementsMap[store[2]] = 1;
211	103	count = 1;
212		}
213	142	if (count > max \|\| (count == max && store[2] < maxValue))
214		{
215	134	max = count;
216	134	maxValue = store[2];
217		}
218	142	store = store[0];
219		}
220
221	86	Assert(depth == indices.size());
222	86	compare = indexCard.compare(max + depth);
223	86	Assert(compare != Cardinality::UNKNOWN);
224	86	if (compare == Cardinality::GREATER
225	86	\|\| (compare == Cardinality::EQUAL && (defaultValue < maxValue)))
226		{
227		Assert(!replacedValue.isNull() && mostFrequentValue == replacedValue);
228		return n;
229		}
230
231		// Out of luck: have to swap out default value
232
233		// Enumerate values from index type into newIndices and sort
234	172	std::vector<Node> newIndices;
235	172	TypeEnumerator te(index.getType());
236	86	bool needToSort = false;
237	86	uint32_t numTe = 0;
238	546	while (!te.isFinished()
239	1178	&& (!indexCard.isFinite()
240	546	\|\| numTe < indexCard.getFiniteCardinality().toUnsignedInt()))
241		{
242	230	if (indexSet.find(*te) == indexSet.end())
243		{
244	88	if (!newIndices.empty() && (!(newIndices.back() < (*te))))
245		{
246	6	needToSort = true;
247		}
248	88	newIndices.push_back(*te);
249		}
250	230	++numTe;
251	230	++te;
252		}
253	86	Assert(indexCard.compare(newIndices.size() + depth) == Cardinality::EQUAL);
254	86	if (needToSort)
255		{
256	4	std::sort(newIndices.begin(), newIndices.end());
257		}
258
259	86	n = nm->mkConst(ArrayStoreAll(node.getType(), maxValue));
260	86	std::vector<Node>::iterator itNew = newIndices.begin(),
261	86	it_end = newIndices.end();
262	546	while (itNew != it_end \|\| !indices.empty())
263		{
264	230	if (itNew != it_end && (indices.empty() \|\| (*itNew) < indices.back()))
265		{
266	88	n = nm->mkNode(kind::STORE, n, (*itNew), defaultValue);
267	88	++itNew;
268		}
269	142	else if (itNew == it_end \|\| indices.back() < (*itNew))
270		{
271	142	if (elements.back() != maxValue)
272		{
273	17	n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
274		}
275	142	indices.pop_back();
276	142	elements.pop_back();
277		}
278		}
279	86	return n;
280		}
281
282	23	Node TheoryArraysRewriter::expandEqRange(TNode node)
283		{
284	23	Assert(node.getKind() == kind::EQ_RANGE);
285
286	23	NodeManager* nm = NodeManager::currentNM();
287	46	TNode a = node[0];
288	46	TNode b = node[1];
289	46	TNode i = node[2];
290	46	TNode j = node[3];
291	46	Node k = SkolemCache::getEqRangeVar(node);
292	46	Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, k);
293	46	TypeNode type = k.getType();
294
295		Kind kle;
296	46	Node range;
297	23	if (type.isBitVector())
298		{
299	19	kle = kind::BITVECTOR_ULE;
300		}
301	4	else if (type.isFloatingPoint())
302		{
303		kle = kind::FLOATINGPOINT_LEQ;
304		}
305	4	else if (type.isInteger() \|\| type.isReal())
306		{
307	4	kle = kind::LEQ;
308		}
309		else
310		{
311		Unimplemented() << "Type " << type << " is not supported for predicate "
312		<< node.getKind();
313		}
314
315	23	range = nm->mkNode(kind::AND, nm->mkNode(kle, i, k), nm->mkNode(kle, k, j));
316
317		Node eq = nm->mkNode(kind::EQUAL,
318	46	nm->mkNode(kind::SELECT, a, k),
319	92	nm->mkNode(kind::SELECT, b, k));
320	46	Node implies = nm->mkNode(kind::IMPLIES, range, eq);
321	46	return nm->mkNode(kind::FORALL, bvl, implies);
322		}
323
324	57131	RewriteResponse TheoryArraysRewriter::postRewrite(TNode node)
325		{
326	114262	Trace("arrays-postrewrite")
327	57131	<< "Arrays::postRewrite start " << node << std::endl;
328	57131	switch (node.getKind())
329		{
330	21500	case kind::SELECT:
331		{
332	21500	TNode store = node[0];
333	21500	TNode index = node[1];
334	21500	Node n;
335		bool val;
336	22748	while (store.getKind() == kind::STORE)
337		{
338	8137	if (index == store[1])
339		{
340	39	val = true;
341		}
342	8098	else if (index.isConst() && store[1].isConst())
343		{
344	294	val = false;
345		}
346		else
347		{
348	7804	n = Rewriter::rewrite(mkEqNode(store[1], index));
349	7804	if (n.getKind() != kind::CONST_BOOLEAN)
350		{
351	7474	break;
352		}
353	330	val = n.getConst<bool>();
354		}
355	663	if (val)
356		{
357		// select(store(a,i,v),j) = v if i = j
358	78	Trace("arrays-postrewrite")
359	39	<< "Arrays::postRewrite returning " << store[2] << std::endl;
360	39	return RewriteResponse(REWRITE_DONE, store[2]);
361		}
362		// select(store(a,i,v),j) = select(a,j) if i /= j
363	624	store = store[0];
364		}
365	21461	if (store.getKind() == kind::STORE_ALL)
366		{
367		// select(store_all(v),i) = v
368	590	ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
369	295	n = storeAll.getValue();
370	590	Trace("arrays-postrewrite")
371	295	<< "Arrays::postRewrite returning " << n << std::endl;
372	295	Assert(n.isConst());
373	295	return RewriteResponse(REWRITE_DONE, n);
374		}
375	21166	else if (store != node[0])
376		{
377	64	n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
378	128	Trace("arrays-postrewrite")
379	64	<< "Arrays::postRewrite returning " << n << std::endl;
380	64	return RewriteResponse(REWRITE_DONE, n);
381		}
382	21102	break;
383		}
384	15482	case kind::STORE:
385		{
386	15482	TNode store = node[0];
387	15482	TNode value = node[2];
388		// store(a,i,select(a,i)) = a
389	31948	if (value.getKind() == kind::SELECT && value[0] == store
390	31210	&& value[1] == node[1])
391		{
392	80	Trace("arrays-postrewrite")
393	40	<< "Arrays::postRewrite returning " << store << std::endl;
394	40	return RewriteResponse(REWRITE_DONE, store);
395		}
396	15442	TNode index = node[1];
397	15442	if (store.isConst() && index.isConst() && value.isConst())
398		{
399		// normalize constant
400	16048	Node n = normalizeConstant(node);
401	8024	Assert(n.isConst());
402	16048	Trace("arrays-postrewrite")
403	8024	<< "Arrays::postRewrite returning " << n << std::endl;
404	8024	return RewriteResponse(REWRITE_DONE, n);
405		}
406	7418	if (store.getKind() == kind::STORE)
407		{
408		// store(store(a,i,v),j,w)
409		bool val;
410	4507	if (index == store[1])
411		{
412	22	val = true;
413		}
414	4485	else if (index.isConst() && store[1].isConst())
415		{
416	436	val = false;
417		}
418		else
419		{
420	6251	Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
421	4049	if (eqRewritten.getKind() != kind::CONST_BOOLEAN)
422		{
423	3694	Trace("arrays-postrewrite")
424	1847	<< "Arrays::postRewrite returning " << node << std::endl;
425	1847	return RewriteResponse(REWRITE_DONE, node);
426		}
427	2202	val = eqRewritten.getConst<bool>();
428		}
429	2660	NodeManager* nm = NodeManager::currentNM();
430	2660	if (val)
431		{
432		// store(store(a,i,v),i,w) = store(a,i,w)
433	44	Node result = nm->mkNode(kind::STORE, store[0], index, value);
434	44	Trace("arrays-postrewrite")
435	22	<< "Arrays::postRewrite returning " << result << std::endl;
436	22	return RewriteResponse(REWRITE_AGAIN, result);
437		}
438	2638	else if (index < store[1])
439		{
440		// store(store(a,i,v),j,w) = store(store(a,j,w),i,v)
441		// IF i != j and j comes before i in the ordering
442	406	std::vector<TNode> indices;
443	406	std::vector<TNode> elements;
444	203	indices.push_back(store[1]);
445	203	elements.push_back(store[2]);
446	203	store = store[0];
447	406	Node n;
448	1669	while (store.getKind() == kind::STORE)
449		{
450	839	if (index == store[1])
451		{
452	8	val = true;
453		}
454	831	else if (index.isConst() && store[1].isConst())
455		{
456	20	val = false;
457		}
458		else
459		{
460	811	n = Rewriter::rewrite(mkEqNode(store[1], index));
461	811	if (n.getKind() != kind::CONST_BOOLEAN)
462		{
463	28	break;
464		}
465	783	val = n.getConst<bool>();
466		}
467	811	if (val)
468		{
469	8	store = store[0];
470	8	break;
471		}
472	803	else if (!(index < store[1]))
473		{
474	70	break;
475		}
476	733	indices.push_back(store[1]);
477	733	elements.push_back(store[2]);
478	733	store = store[0];
479		}
480	431	if (value.getKind() == kind::SELECT && value[0] == store
481	420	&& value[1] == index)
482		{
483	6	n = store;
484		}
485		else
486		{
487	197	n = nm->mkNode(kind::STORE, store, index, value);
488		}
489	2075	while (!indices.empty())
490		{
491	936	n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
492	936	indices.pop_back();
493	936	elements.pop_back();
494		}
495	203	Assert(n != node);
496	406	Trace("arrays-postrewrite")
497	203	<< "Arrays::postRewrite returning " << n << std::endl;
498	203	return RewriteResponse(REWRITE_AGAIN, n);
499		}
500		}
501	5346	break;
502		}
503	18769	case kind::EQUAL:
504		{
505	18769	if (node[0] == node[1])
506		{
507	1424	Trace("arrays-postrewrite")
508	712	<< "Arrays::postRewrite returning true" << std::endl;
509		return RewriteResponse(REWRITE_DONE,
510	712	NodeManager::currentNM()->mkConst(true));
511		}
512	18057	else if (node[0].isConst() && node[1].isConst())
513		{
514	502	Trace("arrays-postrewrite")
515	251	<< "Arrays::postRewrite returning false" << std::endl;
516		return RewriteResponse(REWRITE_DONE,
517	251	NodeManager::currentNM()->mkConst(false));
518		}
519	17806	if (node[0] > node[1])
520		{
521		Node newNode =
522	6588	NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
523	6588	Trace("arrays-postrewrite")
524	3294	<< "Arrays::postRewrite returning " << newNode << std::endl;
525	3294	return RewriteResponse(REWRITE_DONE, newNode);
526		}
527	14512	break;
528		}
529	1380	default: break;
530		}
531	84680	Trace("arrays-postrewrite")
532	42340	<< "Arrays::postRewrite returning " << node << std::endl;
533	42340	return RewriteResponse(REWRITE_DONE, node);
534		}
535
536	32335	RewriteResponse TheoryArraysRewriter::preRewrite(TNode node)
537		{
538	64670	Trace("arrays-prerewrite")
539	32335	<< "Arrays::preRewrite start " << node << std::endl;
540	32335	switch (node.getKind())
541		{
542	12791	case kind::SELECT:
543		{
544	12791	TNode store = node[0];
545	12791	TNode index = node[1];
546	12791	Node n;
547		bool val;
548	17503	while (store.getKind() == kind::STORE)
549		{
550	7075	if (index == store[1])
551		{
552	917	val = true;
553		}
554	6158	else if (index.isConst() && store[1].isConst())
555		{
556	1581	val = false;
557		}
558		else
559		{
560	4577	n = Rewriter::rewrite(mkEqNode(store[1], index));
561	4577	if (n.getKind() != kind::CONST_BOOLEAN)
562		{
563	3749	break;
564		}
565	828	val = n.getConst<bool>();
566		}
567	3326	if (val)
568		{
569		// select(store(a,i,v),j) = v if i = j
570	1940	Trace("arrays-prerewrite")
571	970	<< "Arrays::preRewrite returning " << store[2] << std::endl;
572	970	return RewriteResponse(REWRITE_AGAIN, store[2]);
573		}
574		// select(store(a,i,v),j) = select(a,j) if i /= j
575	2356	store = store[0];
576		}
577	11821	if (store.getKind() == kind::STORE_ALL)
578		{
579		// select(store_all(v),i) = v
580	890	ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
581	445	n = storeAll.getValue();
582	890	Trace("arrays-prerewrite")
583	445	<< "Arrays::preRewrite returning " << n << std::endl;
584	445	Assert(n.isConst());
585	445	return RewriteResponse(REWRITE_DONE, n);
586		}
587	11376	else if (store != node[0])
588		{
589	296	n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
590	592	Trace("arrays-prerewrite")
591	296	<< "Arrays::preRewrite returning " << n << std::endl;
592	296	return RewriteResponse(REWRITE_DONE, n);
593		}
594	11080	break;
595		}
596	7872	case kind::STORE:
597		{
598	7872	TNode store = node[0];
599	7872	TNode value = node[2];
600		// store(a,i,select(a,i)) = a
601	16226	if (value.getKind() == kind::SELECT && value[0] == store
602	15870	&& value[1] == node[1])
603		{
604	30	Trace("arrays-prerewrite")
605	15	<< "Arrays::preRewrite returning " << store << std::endl;
606	15	return RewriteResponse(REWRITE_AGAIN, store);
607		}
608	7857	if (store.getKind() == kind::STORE)
609		{
610		// store(store(a,i,v),j,w)
611	5373	TNode index = node[1];
612		bool val;
613	3195	if (index == store[1])
614		{
615	221	val = true;
616		}
617	2974	else if (index.isConst() && store[1].isConst())
618		{
619	1341	val = false;
620		}
621		else
622		{
623	2484	Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
624	1633	if (eqRewritten.getKind() != kind::CONST_BOOLEAN)
625		{
626	782	break;
627		}
628	851	val = eqRewritten.getConst<bool>();
629		}
630	2413	NodeManager* nm = NodeManager::currentNM();
631	2413	if (val)
632		{
633		// store(store(a,i,v),i,w) = store(a,i,w)
634	470	Node newNode = nm->mkNode(kind::STORE, store[0], index, value);
635	470	Trace("arrays-prerewrite")
636	235	<< "Arrays::preRewrite returning " << newNode << std::endl;
637	235	return RewriteResponse(REWRITE_DONE, newNode);
638		}
639		}
640	6840	break;
641		}
642	11070	case kind::EQUAL:
643		{
644	11070	if (node[0] == node[1])
645		{
646	2022	Trace("arrays-prerewrite")
647	1011	<< "Arrays::preRewrite returning true" << std::endl;
648		return RewriteResponse(REWRITE_DONE,
649	1011	NodeManager::currentNM()->mkConst(true));
650		}
651	10059	break;
652		}
653	602	default: break;
654		}
655
656	58726	Trace("arrays-prerewrite")
657	29363	<< "Arrays::preRewrite returning " << node << std::endl;
658	29363	return RewriteResponse(REWRITE_DONE, node);
659		}
660
661	22455	TrustNode TheoryArraysRewriter::expandDefinition(Node node)
662		{
663	22455	Kind kind = node.getKind();
664
665	22455	if (kind == kind::EQ_RANGE)
666		{
667	40	Node expandedEqRange = expandEqRange(node);
668	20	if (d_epg)
669		{
670	6	TrustNode tn = d_epg->mkTrustNode(node.eqNode(expandedEqRange),
671		PfRule::ARRAYS_EQ_RANGE_EXPAND,
672		{},
673	12	{node});
674	3	return TrustNode::mkTrustRewrite(node, expandedEqRange, d_epg.get());
675		}
676	17	return TrustNode::mkTrustRewrite(node, expandedEqRange, nullptr);
677		}
678
679	22435	return TrustNode::null();
680		}
681
682		} // namespace arrays
683		} // namespace theory
684	29340	} // namespace cvc5