Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arrays/theory_arrays_rewriter.cpp	Lines:	351	356	98.6 %
Date:	2021-09-10	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	573	void setMostFrequentValue(TNode store, TNode value) {
48	573	return store.setAttribute(ArrayConstantMostFrequentValueAttr(), value);
49		}
50	573	void setMostFrequentValueCount(TNode store, uint64_t count) {
51	573	return store.setAttribute(ArrayConstantMostFrequentValueCountAttr(), count);
52		}
53
54	9913	TheoryArraysRewriter::TheoryArraysRewriter(ProofNodeManager* pnm)
55	9913	: d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr)
56		{
57	9913	}
58
59	7953	Node TheoryArraysRewriter::normalizeConstant(TNode node)
60		{
61	7953	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	7953	Node TheoryArraysRewriter::normalizeConstant(TNode node, Cardinality indexCard)
66		{
67	15906	TNode store = node[0];
68	15906	TNode index = node[1];
69	15906	TNode value = node[2];
70
71	15906	std::vector<TNode> indices;
72	15906	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	15906	TNode replacedValue;
80	7953	uint32_t depth = 1;
81	7953	uint32_t valCount = 1;
82	9343	while (store.getKind() == kind::STORE)
83		{
84	2713	if (index == store[1])
85		{
86	146	replacedValue = store[2];
87	146	store = store[0];
88	146	break;
89		}
90	2567	else if (index >= store[1])
91		{
92	1872	break;
93		}
94	695	if (value == store[2])
95		{
96	145	valCount += 1;
97		}
98	695	depth += 1;
99	695	indices.push_back(store[1]);
100	695	elements.push_back(store[2]);
101	695	store = store[0];
102		}
103	15906	Node n = store;
104
105		// Get the default value at the bottom of the nested stores
106	17945	while (store.getKind() == kind::STORE)
107		{
108	4996	if (value == store[2])
109		{
110	634	valCount += 1;
111		}
112	4996	depth += 1;
113	4996	store = store[0];
114		}
115	7953	Assert(store.getKind() == kind::STORE_ALL);
116	15906	ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
117	15906	Node defaultValue = storeAll.getValue();
118	7953	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	7953	if (value == defaultValue)
123		{
124	337	if (replacedValue.isNull())
125		{
126		// Quick exit - if writing to default value and nothing was
127		// replaced, we can just return node[0]
128	325	return node[0];
129		}
130		// else rebuild the store without the replaced write and then exit
131		}
132		else
133		{
134	7616	n = nm->mkNode(kind::STORE, n, index, value);
135		}
136
137		// Build the rest of the store after inserting/deleting
138	8836	while (!indices.empty())
139		{
140	604	n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
141	604	indices.pop_back();
142	604	elements.pop_back();
143		}
144
145		// Ready to exit if write was to the default value (see previous comment)
146	7628	if (value == defaultValue)
147		{
148	12	return n;
149		}
150
151	7616	if (indexCard.isInfinite())
152		{
153	6115	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	3002	TNode mostFrequentValue;
161	1501	uint32_t mostFrequentValueCount = 0;
162	1501	store = node[0];
163	1501	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	1501	if (valCount > mostFrequentValueCount
171	1501	\|\| (valCount == mostFrequentValueCount && value < mostFrequentValue))
172		{
173	991	mostFrequentValue = value;
174	991	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	1501	indexCard.compare(mostFrequentValueCount + depth);
181	1501	Assert(compare != Cardinality::UNKNOWN);
182	1501	if (compare == Cardinality::GREATER
183	1501	\|\| (compare == Cardinality::EQUAL && (defaultValue < mostFrequentValue)))
184		{
185	1416	return n;
186		}
187
188		// Bad case: have to recompute value counts and/or possibly switch out
189		// default value
190	85	store = n;
191	170	std::unordered_set<TNode> indexSet;
192	170	std::unordered_map<TNode, uint32_t> elementsMap;
193	85	std::unordered_map<TNode, uint32_t>::iterator it;
194		uint32_t count;
195	85	uint32_t max = 0;
196	170	TNode maxValue;
197	367	while (store.getKind() == kind::STORE)
198		{
199	141	indices.push_back(store[1]);
200	141	indexSet.insert(store[1]);
201	141	elements.push_back(store[2]);
202	141	it = elementsMap.find(store[2]);
203	141	if (it != elementsMap.end())
204		{
205	39	(it).second = (it).second + 1;
206	39	count = (*it).second;
207		}
208		else
209		{
210	102	elementsMap[store[2]] = 1;
211	102	count = 1;
212		}
213	141	if (count > max \|\| (count == max && store[2] < maxValue))
214		{
215	133	max = count;
216	133	maxValue = store[2];
217		}
218	141	store = store[0];
219		}
220
221	85	Assert(depth == indices.size());
222	85	compare = indexCard.compare(max + depth);
223	85	Assert(compare != Cardinality::UNKNOWN);
224	85	if (compare == Cardinality::GREATER
225	85	\|\| (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	170	std::vector<Node> newIndices;
235	170	TypeEnumerator te(index.getType());
236	85	bool needToSort = false;
237	85	uint32_t numTe = 0;
238	541	while (!te.isFinished()
239	1167	&& (!indexCard.isFinite()
240	541	\|\| numTe < indexCard.getFiniteCardinality().toUnsignedInt()))
241		{
242	228	if (indexSet.find(*te) == indexSet.end())
243		{
244	87	if (!newIndices.empty() && (!(newIndices.back() < (*te))))
245		{
246	6	needToSort = true;
247		}
248	87	newIndices.push_back(*te);
249		}
250	228	++numTe;
251	228	++te;
252		}
253	85	Assert(indexCard.compare(newIndices.size() + depth) == Cardinality::EQUAL);
254	85	if (needToSort)
255		{
256	4	std::sort(newIndices.begin(), newIndices.end());
257		}
258
259	85	n = nm->mkConst(ArrayStoreAll(node.getType(), maxValue));
260	85	std::vector<Node>::iterator itNew = newIndices.begin(),
261	85	it_end = newIndices.end();
262	541	while (itNew != it_end \|\| !indices.empty())
263		{
264	228	if (itNew != it_end && (indices.empty() \|\| (*itNew) < indices.back()))
265		{
266	87	n = nm->mkNode(kind::STORE, n, (*itNew), defaultValue);
267	87	++itNew;
268		}
269	141	else if (itNew == it_end \|\| indices.back() < (*itNew))
270		{
271	141	if (elements.back() != maxValue)
272		{
273	17	n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
274		}
275	141	indices.pop_back();
276	141	elements.pop_back();
277		}
278		}
279	85	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	57513	RewriteResponse TheoryArraysRewriter::postRewrite(TNode node)
325		{
326	115026	Trace("arrays-postrewrite")
327	57513	<< "Arrays::postRewrite start " << node << std::endl;
328	57513	switch (node.getKind())
329		{
330	21646	case kind::SELECT:
331		{
332	21646	TNode store = node[0];
333	21646	TNode index = node[1];
334	21646	Node n;
335		bool val;
336	22894	while (store.getKind() == kind::STORE)
337		{
338	8143	if (index == store[1])
339		{
340	39	val = true;
341		}
342	8104	else if (index.isConst() && store[1].isConst())
343		{
344	294	val = false;
345		}
346		else
347		{
348	7810	n = Rewriter::rewrite(mkEqNode(store[1], index));
349	7810	if (n.getKind() != kind::CONST_BOOLEAN)
350		{
351	7480	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	21607	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	21312	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	21248	break;
383		}
384	15581	case kind::STORE:
385		{
386	15581	TNode store = node[0];
387	15581	TNode value = node[2];
388		// store(a,i,select(a,i)) = a
389	32142	if (value.getKind() == kind::SELECT && value[0] == store
390	31408	&& 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	15541	TNode index = node[1];
397	15541	if (store.isConst() && index.isConst() && value.isConst())
398		{
399		// normalize constant
400	15906	Node n = normalizeConstant(node);
401	7953	Assert(n.isConst());
402	15906	Trace("arrays-postrewrite")
403	7953	<< "Arrays::postRewrite returning " << n << std::endl;
404	7953	return RewriteResponse(REWRITE_DONE, n);
405		}
406	7588	if (store.getKind() == kind::STORE)
407		{
408		// store(store(a,i,v),j,w)
409		bool val;
410	4500	if (index == store[1])
411		{
412	19	val = true;
413		}
414	4481	else if (index.isConst() && store[1].isConst())
415		{
416	438	val = false;
417		}
418		else
419		{
420	6245	Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
421	4043	if (eqRewritten.getKind() != kind::CONST_BOOLEAN)
422		{
423	3682	Trace("arrays-postrewrite")
424	1841	<< "Arrays::postRewrite returning " << node << std::endl;
425	1841	return RewriteResponse(REWRITE_DONE, node);
426		}
427	2202	val = eqRewritten.getConst<bool>();
428		}
429	2659	NodeManager* nm = NodeManager::currentNM();
430	2659	if (val)
431		{
432		// store(store(a,i,v),i,w) = store(a,i,w)
433	38	Node result = nm->mkNode(kind::STORE, store[0], index, value);
434	38	Trace("arrays-postrewrite")
435	19	<< "Arrays::postRewrite returning " << result << std::endl;
436	19	return RewriteResponse(REWRITE_AGAIN, result);
437		}
438	2640	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	410	std::vector<TNode> indices;
443	410	std::vector<TNode> elements;
444	205	indices.push_back(store[1]);
445	205	elements.push_back(store[2]);
446	205	store = store[0];
447	410	Node n;
448	1671	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	435	if (value.getKind() == kind::SELECT && value[0] == store
481	424	&& value[1] == index)
482		{
483	6	n = store;
484		}
485		else
486		{
487	199	n = nm->mkNode(kind::STORE, store, index, value);
488		}
489	2081	while (!indices.empty())
490		{
491	938	n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
492	938	indices.pop_back();
493	938	elements.pop_back();
494		}
495	205	Assert(n != node);
496	410	Trace("arrays-postrewrite")
497	205	<< "Arrays::postRewrite returning " << n << std::endl;
498	205	return RewriteResponse(REWRITE_AGAIN, n);
499		}
500		}
501	5523	break;
502		}
503	18927	case kind::EQUAL:
504		{
505	18927	if (node[0] == node[1])
506		{
507	1452	Trace("arrays-postrewrite")
508	726	<< "Arrays::postRewrite returning true" << std::endl;
509		return RewriteResponse(REWRITE_DONE,
510	726	NodeManager::currentNM()->mkConst(true));
511		}
512	18201	else if (node[0].isConst() && node[1].isConst())
513		{
514	522	Trace("arrays-postrewrite")
515	261	<< "Arrays::postRewrite returning false" << std::endl;
516		return RewriteResponse(REWRITE_DONE,
517	261	NodeManager::currentNM()->mkConst(false));
518		}
519	17940	if (node[0] > node[1])
520		{
521		Node newNode =
522	6612	NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
523	6612	Trace("arrays-postrewrite")
524	3306	<< "Arrays::postRewrite returning " << newNode << std::endl;
525	3306	return RewriteResponse(REWRITE_DONE, newNode);
526		}
527	14634	break;
528		}
529	1359	default: break;
530		}
531	85528	Trace("arrays-postrewrite")
532	42764	<< "Arrays::postRewrite returning " << node << std::endl;
533	42764	return RewriteResponse(REWRITE_DONE, node);
534		}
535
536	32463	RewriteResponse TheoryArraysRewriter::preRewrite(TNode node)
537		{
538	64926	Trace("arrays-prerewrite")
539	32463	<< "Arrays::preRewrite start " << node << std::endl;
540	32463	switch (node.getKind())
541		{
542	12874	case kind::SELECT:
543		{
544	12874	TNode store = node[0];
545	12874	TNode index = node[1];
546	12874	Node n;
547		bool val;
548	17590	while (store.getKind() == kind::STORE)
549		{
550	7091	if (index == store[1])
551		{
552	924	val = true;
553		}
554	6167	else if (index.isConst() && store[1].isConst())
555		{
556	1583	val = false;
557		}
558		else
559		{
560	4584	n = Rewriter::rewrite(mkEqNode(store[1], index));
561	4584	if (n.getKind() != kind::CONST_BOOLEAN)
562		{
563	3756	break;
564		}
565	828	val = n.getConst<bool>();
566		}
567	3335	if (val)
568		{
569		// select(store(a,i,v),j) = v if i = j
570	1954	Trace("arrays-prerewrite")
571	977	<< "Arrays::preRewrite returning " << store[2] << std::endl;
572	977	return RewriteResponse(REWRITE_AGAIN, store[2]);
573		}
574		// select(store(a,i,v),j) = select(a,j) if i /= j
575	2358	store = store[0];
576		}
577	11897	if (store.getKind() == kind::STORE_ALL)
578		{
579		// select(store_all(v),i) = v
580	892	ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
581	446	n = storeAll.getValue();
582	892	Trace("arrays-prerewrite")
583	446	<< "Arrays::preRewrite returning " << n << std::endl;
584	446	Assert(n.isConst());
585	446	return RewriteResponse(REWRITE_DONE, n);
586		}
587	11451	else if (store != node[0])
588		{
589	298	n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
590	596	Trace("arrays-prerewrite")
591	298	<< "Arrays::preRewrite returning " << n << std::endl;
592	298	return RewriteResponse(REWRITE_DONE, n);
593		}
594	11153	break;
595		}
596	7934	case kind::STORE:
597		{
598	7934	TNode store = node[0];
599	7934	TNode value = node[2];
600		// store(a,i,select(a,i)) = a
601	16348	if (value.getKind() == kind::SELECT && value[0] == store
602	15994	&& 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	7919	if (store.getKind() == kind::STORE)
609		{
610		// store(store(a,i,v),j,w)
611	5347	TNode index = node[1];
612		bool val;
613	3186	if (index == store[1])
614		{
615	226	val = true;
616		}
617	2960	else if (index.isConst() && store[1].isConst())
618		{
619	1324	val = false;
620		}
621		else
622		{
623	2487	Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
624	1636	if (eqRewritten.getKind() != kind::CONST_BOOLEAN)
625		{
626	785	break;
627		}
628	851	val = eqRewritten.getConst<bool>();
629		}
630	2401	NodeManager* nm = NodeManager::currentNM();
631	2401	if (val)
632		{
633		// store(store(a,i,v),i,w) = store(a,i,w)
634	480	Node newNode = nm->mkNode(kind::STORE, store[0], index, value);
635	480	Trace("arrays-prerewrite")
636	240	<< "Arrays::preRewrite returning " << newNode << std::endl;
637	240	return RewriteResponse(REWRITE_DONE, newNode);
638		}
639		}
640	6894	break;
641		}
642	11062	case kind::EQUAL:
643		{
644	11062	if (node[0] == node[1])
645		{
646	1960	Trace("arrays-prerewrite")
647	980	<< "Arrays::preRewrite returning true" << std::endl;
648		return RewriteResponse(REWRITE_DONE,
649	980	NodeManager::currentNM()->mkConst(true));
650		}
651	10082	break;
652		}
653	593	default: break;
654		}
655
656	59014	Trace("arrays-prerewrite")
657	29507	<< "Arrays::preRewrite returning " << node << std::endl;
658	29507	return RewriteResponse(REWRITE_DONE, node);
659		}
660
661	22444	TrustNode TheoryArraysRewriter::expandDefinition(Node node)
662		{
663	22444	Kind kind = node.getKind();
664
665	22444	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	22424	return TrustNode::null();
680		}
681
682		} // namespace arrays
683		} // namespace theory
684	29502	} // namespace cvc5