Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arrays/theory_arrays_rewriter.cpp	Lines:	349	357	97.8 %
Date:	2021-09-29	Branches:	842	1613	52.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include "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	1140	Node getMostFrequentValue(TNode store) {
45	1140	return store.getAttribute(ArrayConstantMostFrequentValueAttr());
46		}
47	1140	uint64_t getMostFrequentValueCount(TNode store) {
48	1140	return store.getAttribute(ArrayConstantMostFrequentValueCountAttr());
49		}
50
51	561	void setMostFrequentValue(TNode store, TNode value) {
52	561	return store.setAttribute(ArrayConstantMostFrequentValueAttr(), value);
53		}
54	561	void setMostFrequentValueCount(TNode store, uint64_t count) {
55	561	return store.setAttribute(ArrayConstantMostFrequentValueCountAttr(), count);
56		}
57
58	6271	TheoryArraysRewriter::TheoryArraysRewriter(Rewriter* rewriter,
59	6271	ProofNodeManager* pnm)
60	6271	: d_rewriter(rewriter), d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr)
61		{
62	6271	}
63
64	7770	Node TheoryArraysRewriter::normalizeConstant(TNode node)
65		{
66	7770	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	7770	Node TheoryArraysRewriter::normalizeConstant(TNode node, Cardinality indexCard)
71		{
72	15540	TNode store = node[0];
73	15540	TNode index = node[1];
74	15540	TNode value = node[2];
75
76	15540	std::vector<TNode> indices;
77	15540	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	15540	TNode replacedValue;
85	7770	uint32_t depth = 1;
86	7770	uint32_t valCount = 1;
87	9118	while (store.getKind() == kind::STORE)
88		{
89	2655	if (index == store[1])
90		{
91	146	replacedValue = store[2];
92	146	store = store[0];
93	146	break;
94		}
95	2509	else if (index >= store[1])
96		{
97	1835	break;
98		}
99	674	if (value == store[2])
100		{
101	144	valCount += 1;
102		}
103	674	depth += 1;
104	674	indices.push_back(store[1]);
105	674	elements.push_back(store[2]);
106	674	store = store[0];
107		}
108	15540	Node n = store;
109
110		// Get the default value at the bottom of the nested stores
111	17664	while (store.getKind() == kind::STORE)
112		{
113	4947	if (value == store[2])
114		{
115	611	valCount += 1;
116		}
117	4947	depth += 1;
118	4947	store = store[0];
119		}
120	7770	Assert(store.getKind() == kind::STORE_ALL);
121	15540	ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
122	15540	Node defaultValue = storeAll.getValue();
123	7770	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	7770	if (value == defaultValue)
128		{
129	314	if (replacedValue.isNull())
130		{
131		// Quick exit - if writing to default value and nothing was
132		// replaced, we can just return node[0]
133	302	return node[0];
134		}
135		// else rebuild the store without the replaced write and then exit
136		}
137		else
138		{
139	7456	n = nm->mkNode(kind::STORE, n, index, value);
140		}
141
142		// Build the rest of the store after inserting/deleting
143	8660	while (!indices.empty())
144		{
145	596	n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
146	596	indices.pop_back();
147	596	elements.pop_back();
148		}
149
150		// Ready to exit if write was to the default value (see previous comment)
151	7468	if (value == defaultValue)
152		{
153	12	return n;
154		}
155
156	7456	if (indexCard.isInfinite())
157		{
158	5979	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	2954	TNode mostFrequentValue;
166	1477	uint32_t mostFrequentValueCount = 0;
167	1477	store = node[0];
168	1477	if (store.getKind() == kind::STORE)
169		{
170	847	mostFrequentValue = getMostFrequentValue(store);
171	847	mostFrequentValueCount = getMostFrequentValueCount(store);
172		}
173
174		// Compute the most frequently written value for n
175	1477	if (valCount > mostFrequentValueCount
176	1477	\|\| (valCount == mostFrequentValueCount && value < mostFrequentValue))
177		{
178	968	mostFrequentValue = value;
179	968	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	1477	indexCard.compare(mostFrequentValueCount + depth);
186	1477	Assert(compare != Cardinality::UNKNOWN);
187	1477	if (compare == Cardinality::GREATER
188	1477	\|\| (compare == Cardinality::EQUAL && (defaultValue < mostFrequentValue)))
189		{
190	1394	return n;
191		}
192
193		// Bad case: have to recompute value counts and/or possibly switch out
194		// default value
195	83	store = n;
196	166	std::unordered_set<TNode> indexSet;
197	166	std::unordered_map<TNode, uint32_t> elementsMap;
198	83	std::unordered_map<TNode, uint32_t>::iterator it;
199		uint32_t count;
200	83	uint32_t max = 0;
201	166	TNode maxValue;
202	361	while (store.getKind() == kind::STORE)
203		{
204	139	indices.push_back(store[1]);
205	139	indexSet.insert(store[1]);
206	139	elements.push_back(store[2]);
207	139	it = elementsMap.find(store[2]);
208	139	if (it != elementsMap.end())
209		{
210	39	(it).second = (it).second + 1;
211	39	count = (*it).second;
212		}
213		else
214		{
215	100	elementsMap[store[2]] = 1;
216	100	count = 1;
217		}
218	139	if (count > max \|\| (count == max && store[2] < maxValue))
219		{
220	131	max = count;
221	131	maxValue = store[2];
222		}
223	139	store = store[0];
224		}
225
226	83	Assert(depth == indices.size());
227	83	compare = indexCard.compare(max + depth);
228	83	Assert(compare != Cardinality::UNKNOWN);
229	83	if (compare == Cardinality::GREATER
230	83	\|\| (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	166	std::vector<Node> newIndices;
240	166	TypeEnumerator te(index.getType());
241	83	bool needToSort = false;
242	83	uint32_t numTe = 0;
243	531	while (!te.isFinished()
244	1145	&& (!indexCard.isFinite()
245	531	\|\| numTe < indexCard.getFiniteCardinality().toUnsignedInt()))
246		{
247	224	if (indexSet.find(*te) == indexSet.end())
248		{
249	85	if (!newIndices.empty() && (!(newIndices.back() < (*te))))
250		{
251	6	needToSort = true;
252		}
253	85	newIndices.push_back(*te);
254		}
255	224	++numTe;
256	224	++te;
257		}
258	83	Assert(indexCard.compare(newIndices.size() + depth) == Cardinality::EQUAL);
259	83	if (needToSort)
260		{
261	4	std::sort(newIndices.begin(), newIndices.end());
262		}
263
264	83	n = nm->mkConst(ArrayStoreAll(node.getType(), maxValue));
265	83	std::vector<Node>::iterator itNew = newIndices.begin(),
266	83	it_end = newIndices.end();
267	531	while (itNew != it_end \|\| !indices.empty())
268		{
269	224	if (itNew != it_end && (indices.empty() \|\| (*itNew) < indices.back()))
270		{
271	85	n = nm->mkNode(kind::STORE, n, (*itNew), defaultValue);
272	85	++itNew;
273		}
274	139	else if (itNew == it_end \|\| indices.back() < (*itNew))
275		{
276	139	if (elements.back() != maxValue)
277		{
278	17	n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
279		}
280	139	indices.pop_back();
281	139	elements.pop_back();
282		}
283		}
284	83	return n;
285		}
286
287	11	Node TheoryArraysRewriter::expandEqRange(TNode node)
288		{
289	11	Assert(node.getKind() == kind::EQ_RANGE);
290
291	11	NodeManager* nm = NodeManager::currentNM();
292	22	TNode a = node[0];
293	22	TNode b = node[1];
294	22	TNode i = node[2];
295	22	TNode j = node[3];
296	22	Node k = SkolemCache::getEqRangeVar(node);
297	22	Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, k);
298	22	TypeNode type = k.getType();
299
300		Kind kle;
301	22	Node range;
302	11	if (type.isBitVector())
303		{
304	7	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	11	range = nm->mkNode(kind::AND, nm->mkNode(kle, i, k), nm->mkNode(kle, k, j));
321
322		Node eq = nm->mkNode(kind::EQUAL,
323	22	nm->mkNode(kind::SELECT, a, k),
324	44	nm->mkNode(kind::SELECT, b, k));
325	22	Node implies = nm->mkNode(kind::IMPLIES, range, eq);
326	22	return nm->mkNode(kind::FORALL, bvl, implies);
327		}
328
329	36767	RewriteResponse TheoryArraysRewriter::postRewrite(TNode node)
330		{
331	73534	Trace("arrays-postrewrite")
332	36767	<< "Arrays::postRewrite start " << node << std::endl;
333	36767	switch (node.getKind())
334		{
335	13899	case kind::SELECT:
336		{
337	13899	TNode store = node[0];
338	13899	TNode index = node[1];
339	13899	Node n;
340		bool val;
341	15147	while (store.getKind() == kind::STORE)
342		{
343	6394	if (index == store[1])
344		{
345	36	val = true;
346		}
347	6358	else if (index.isConst() && store[1].isConst())
348		{
349	294	val = false;
350		}
351		else
352		{
353	6064	n = d_rewriter->rewrite(mkEqNode(store[1], index));
354	6064	if (n.getKind() != kind::CONST_BOOLEAN)
355		{
356	5734	break;
357		}
358	330	val = n.getConst<bool>();
359		}
360	660	if (val)
361		{
362		// select(store(a,i,v),j) = v if i = j
363	72	Trace("arrays-postrewrite")
364	36	<< "Arrays::postRewrite returning " << store[2] << std::endl;
365	36	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	13863	if (store.getKind() == kind::STORE_ALL)
371		{
372		// select(store_all(v),i) = v
373	514	ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
374	257	n = storeAll.getValue();
375	514	Trace("arrays-postrewrite")
376	257	<< "Arrays::postRewrite returning " << n << std::endl;
377	257	Assert(n.isConst());
378	257	return RewriteResponse(REWRITE_DONE, n);
379		}
380	13606	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	13542	break;
388		}
389	12843	case kind::STORE:
390		{
391	12843	TNode store = node[0];
392	12843	TNode value = node[2];
393		// store(a,i,select(a,i)) = a
394	26210	if (value.getKind() == kind::SELECT && value[0] == store
395	25778	&& value[1] == node[1])
396		{
397	44	Trace("arrays-postrewrite")
398	22	<< "Arrays::postRewrite returning " << store << std::endl;
399	22	return RewriteResponse(REWRITE_DONE, store);
400		}
401	12821	TNode index = node[1];
402	12821	if (store.isConst() && index.isConst() && value.isConst())
403		{
404		// normalize constant
405	15540	Node n = normalizeConstant(node);
406	7770	Assert(n.isConst());
407	15540	Trace("arrays-postrewrite")
408	7770	<< "Arrays::postRewrite returning " << n << std::endl;
409	7770	return RewriteResponse(REWRITE_DONE, n);
410		}
411	5051	if (store.getKind() == kind::STORE)
412		{
413		// store(store(a,i,v),j,w)
414		bool val;
415	3170	if (index == store[1])
416		{
417	10	val = true;
418		}
419	3160	else if (index.isConst() && store[1].isConst())
420		{
421	310	val = false;
422		}
423		else
424		{
425	4311	Node eqRewritten = d_rewriter->rewrite(mkEqNode(store[1], index));
426	2850	if (eqRewritten.getKind() != kind::CONST_BOOLEAN)
427		{
428	2778	Trace("arrays-postrewrite")
429	1389	<< "Arrays::postRewrite returning " << node << std::endl;
430	1389	return RewriteResponse(REWRITE_DONE, node);
431		}
432	1461	val = eqRewritten.getConst<bool>();
433		}
434	1781	NodeManager* nm = NodeManager::currentNM();
435	1781	if (val)
436		{
437		// store(store(a,i,v),i,w) = store(a,i,w)
438	20	Node result = nm->mkNode(kind::STORE, store[0], index, value);
439	20	Trace("arrays-postrewrite")
440	10	<< "Arrays::postRewrite returning " << result << std::endl;
441	10	return RewriteResponse(REWRITE_AGAIN, result);
442		}
443	1771	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	180	std::vector<TNode> indices;
448	180	std::vector<TNode> elements;
449	90	indices.push_back(store[1]);
450	90	elements.push_back(store[2]);
451	90	store = store[0];
452	180	Node n;
453	596	while (store.getKind() == kind::STORE)
454		{
455	290	if (index == store[1])
456		{
457	5	val = true;
458		}
459	285	else if (index.isConst() && store[1].isConst())
460		{
461	20	val = false;
462		}
463		else
464		{
465	265	n = d_rewriter->rewrite(mkEqNode(store[1], index));
466	265	if (n.getKind() != kind::CONST_BOOLEAN)
467		{
468	10	break;
469		}
470	255	val = n.getConst<bool>();
471		}
472	280	if (val)
473		{
474	5	store = store[0];
475	5	break;
476		}
477	275	else if (!(index < store[1]))
478		{
479	22	break;
480		}
481	253	indices.push_back(store[1]);
482	253	elements.push_back(store[2]);
483	253	store = store[0];
484		}
485	196	if (value.getKind() == kind::SELECT && value[0] == store
486	185	&& value[1] == index)
487		{
488	3	n = store;
489		}
490		else
491		{
492	87	n = nm->mkNode(kind::STORE, store, index, value);
493		}
494	776	while (!indices.empty())
495		{
496	343	n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
497	343	indices.pop_back();
498	343	elements.pop_back();
499		}
500	90	Assert(n != node);
501	180	Trace("arrays-postrewrite")
502	90	<< "Arrays::postRewrite returning " << n << std::endl;
503	90	return RewriteResponse(REWRITE_AGAIN, n);
504		}
505		}
506	3562	break;
507		}
508	8885	case kind::EQUAL:
509		{
510	8885	if (node[0] == node[1])
511		{
512	418	Trace("arrays-postrewrite")
513	209	<< "Arrays::postRewrite returning true" << std::endl;
514		return RewriteResponse(REWRITE_DONE,
515	209	NodeManager::currentNM()->mkConst(true));
516		}
517	8676	else if (node[0].isConst() && node[1].isConst())
518		{
519	508	Trace("arrays-postrewrite")
520	254	<< "Arrays::postRewrite returning false" << std::endl;
521		return RewriteResponse(REWRITE_DONE,
522	254	NodeManager::currentNM()->mkConst(false));
523		}
524	8422	if (node[0] > node[1])
525		{
526		Node newNode =
527	3002	NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
528	3002	Trace("arrays-postrewrite")
529	1501	<< "Arrays::postRewrite returning " << newNode << std::endl;
530	1501	return RewriteResponse(REWRITE_DONE, newNode);
531		}
532	6921	break;
533		}
534	1140	default: break;
535		}
536	50330	Trace("arrays-postrewrite")
537	25165	<< "Arrays::postRewrite returning " << node << std::endl;
538	25165	return RewriteResponse(REWRITE_DONE, node);
539		}
540
541	20596	RewriteResponse TheoryArraysRewriter::preRewrite(TNode node)
542		{
543	41192	Trace("arrays-prerewrite")
544	20596	<< "Arrays::preRewrite start " << node << std::endl;
545	20596	switch (node.getKind())
546		{
547	8545	case kind::SELECT:
548		{
549	8545	TNode store = node[0];
550	8545	TNode index = node[1];
551	8545	Node n;
552		bool val;
553	12931	while (store.getKind() == kind::STORE)
554		{
555	5718	if (index == store[1])
556		{
557	695	val = true;
558		}
559	5023	else if (index.isConst() && store[1].isConst())
560		{
561	1525	val = false;
562		}
563		else
564		{
565	3498	n = d_rewriter->rewrite(mkEqNode(store[1], index));
566	3498	if (n.getKind() != kind::CONST_BOOLEAN)
567		{
568	2805	break;
569		}
570	693	val = n.getConst<bool>();
571		}
572	2913	if (val)
573		{
574		// select(store(a,i,v),j) = v if i = j
575	1440	Trace("arrays-prerewrite")
576	720	<< "Arrays::preRewrite returning " << store[2] << std::endl;
577	720	return RewriteResponse(REWRITE_AGAIN, store[2]);
578		}
579		// select(store(a,i,v),j) = select(a,j) if i /= j
580	2193	store = store[0];
581		}
582	7825	if (store.getKind() == kind::STORE_ALL)
583		{
584		// select(store_all(v),i) = v
585	868	ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
586	434	n = storeAll.getValue();
587	868	Trace("arrays-prerewrite")
588	434	<< "Arrays::preRewrite returning " << n << std::endl;
589	434	Assert(n.isConst());
590	434	return RewriteResponse(REWRITE_DONE, n);
591		}
592	7391	else if (store != node[0])
593		{
594	259	n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
595	518	Trace("arrays-prerewrite")
596	259	<< "Arrays::preRewrite returning " << n << std::endl;
597	259	return RewriteResponse(REWRITE_DONE, n);
598		}
599	7132	break;
600		}
601	6597	case kind::STORE:
602		{
603	6597	TNode store = node[0];
604	6597	TNode value = node[2];
605		// store(a,i,select(a,i)) = a
606	13461	if (value.getKind() == kind::SELECT && value[0] == store
607	13244	&& value[1] == node[1])
608		{
609	26	Trace("arrays-prerewrite")
610	13	<< "Arrays::preRewrite returning " << store << std::endl;
611	13	return RewriteResponse(REWRITE_AGAIN, store);
612		}
613	6584	if (store.getKind() == kind::STORE)
614		{
615		// store(store(a,i,v),j,w)
616	4372	TNode index = node[1];
617		bool val;
618	2560	if (index == store[1])
619		{
620	179	val = true;
621		}
622	2381	else if (index.isConst() && store[1].isConst())
623		{
624	1240	val = false;
625		}
626		else
627		{
628	1719	Node eqRewritten = d_rewriter->rewrite(mkEqNode(store[1], index));
629	1141	if (eqRewritten.getKind() != kind::CONST_BOOLEAN)
630		{
631	563	break;
632		}
633	578	val = eqRewritten.getConst<bool>();
634		}
635	1997	NodeManager* nm = NodeManager::currentNM();
636	1997	if (val)
637		{
638		// store(store(a,i,v),i,w) = store(a,i,w)
639	370	Node newNode = nm->mkNode(kind::STORE, store[0], index, value);
640	370	Trace("arrays-prerewrite")
641	185	<< "Arrays::preRewrite returning " << newNode << std::endl;
642	185	return RewriteResponse(REWRITE_DONE, newNode);
643		}
644		}
645	5836	break;
646		}
647	4966	case kind::EQUAL:
648		{
649	4966	if (node[0] == node[1])
650		{
651	580	Trace("arrays-prerewrite")
652	290	<< "Arrays::preRewrite returning true" << std::endl;
653		return RewriteResponse(REWRITE_DONE,
654	290	NodeManager::currentNM()->mkConst(true));
655		}
656	4676	break;
657		}
658	488	default: break;
659		}
660
661	37390	Trace("arrays-prerewrite")
662	18695	<< "Arrays::preRewrite returning " << node << std::endl;
663	18695	return RewriteResponse(REWRITE_DONE, node);
664		}
665
666	13372	TrustNode TheoryArraysRewriter::expandDefinition(Node node)
667		{
668	13372	Kind kind = node.getKind();
669
670	13372	if (kind == kind::EQ_RANGE)
671		{
672	22	Node expandedEqRange = expandEqRange(node);
673	11	if (d_epg)
674		{
675		TrustNode tn = d_epg->mkTrustNode(node.eqNode(expandedEqRange),
676		PfRule::ARRAYS_EQ_RANGE_EXPAND,
677		{},
678		{node});
679		return TrustNode::mkTrustRewrite(node, expandedEqRange, d_epg.get());
680		}
681	11	return TrustNode::mkTrustRewrite(node, expandedEqRange, nullptr);
682		}
683
684	13361	return TrustNode::null();
685		}
686
687		} // namespace arrays
688		} // namespace theory
689	22746	} // namespace cvc5