Head

GCC Code Coverage Report

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