Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/bv_inverter.cpp	Lines:	187	201	93.0 %
Date:	2021-09-07	Branches:	473	1052	45.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Andrew Reynolds, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * Inverse rules for bit-vector operators.
 */

#include "theory/quantifiers/bv_inverter.h"

#include <algorithm>

#include "expr/skolem_manager.h"
#include "options/quantifiers_options.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/quantifiers/bv_inverter_utils.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
#include "util/bitvector.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

/*---------------------------------------------------------------------------*/

Node BvInverter::getSolveVariable(TypeNode tn)
{
  std::map<TypeNode, Node>::iterator its = d_solve_var.find(tn);
  if (its == d_solve_var.end())
  {
    SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
    Node k = sm->mkDummySkolem("slv", tn);
    d_solve_var[tn] = k;
    return k;
  }
  return its->second;
}

/*---------------------------------------------------------------------------*/

Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m)
{
  TNode solve_var = getSolveVariable(tn);

  // condition should be rewritten
  Node new_cond = Rewriter::rewrite(cond);
  if (new_cond != cond)
  {
    Trace("cegqi-bv-skvinv-debug")
        << "Condition " << cond << " was rewritten to " << new_cond
        << std::endl;
  }
  // optimization : if condition is ( x = solve_var ) should just return
  // solve_var and not introduce a Skolem this can happen when we ask for
  // the multiplicative inversion with bv1
  Node c;
  if (new_cond.getKind() == EQUAL)
  {
    for (unsigned i = 0; i < 2; i++)
    {
      if (new_cond[i] == solve_var)
      {
        c = new_cond[1 - i];
        Trace("cegqi-bv-skvinv")
            << "SKVINV : " << c << " is trivially associated with conditon "
            << new_cond << std::endl;
        break;
      }
    }
  }

  if (c.isNull())
  {
    NodeManager* nm = NodeManager::currentNM();
    if (m)
    {
      Node x = m->getBoundVariable(tn);
      Node ccond = new_cond.substitute(solve_var, x);
      c = nm->mkNode(kind::WITNESS, nm->mkNode(BOUND_VAR_LIST, x), ccond);
      Trace("cegqi-bv-skvinv")
          << "SKVINV : Make " << c << " for " << new_cond << std::endl;
    }
    else
    {
      Trace("bv-invert") << "...fail for " << cond << " : no inverter query!"
                         << std::endl;
    }
  }
  // currently shouldn't cache since
  // the return value depends on the
  // state of m (which bound variable is returned).
  return c;
}

/*---------------------------------------------------------------------------*/

static bool isInvertible(Kind k, unsigned index)
{
  return k == NOT || k == EQUAL || k == BITVECTOR_ULT || k == BITVECTOR_SLT
         || k == BITVECTOR_COMP || k == BITVECTOR_NOT || k == BITVECTOR_NEG
         || k == BITVECTOR_CONCAT || k == BITVECTOR_SIGN_EXTEND
         || k == BITVECTOR_ADD || k == BITVECTOR_MULT || k == BITVECTOR_UREM
         || k == BITVECTOR_UDIV || k == BITVECTOR_AND || k == BITVECTOR_OR
         || k == BITVECTOR_XOR || k == BITVECTOR_LSHR || k == BITVECTOR_ASHR
         || k == BITVECTOR_SHL;
}

Node BvInverter::getPathToPv(Node lit,
                             Node pv,
                             Node sv,
                             std::vector<unsigned>& path,
                             std::unordered_set<TNode>& visited)
{
  if (visited.find(lit) == visited.end())
  {
    visited.insert(lit);
    if (lit == pv)
    {
      return sv;
    }
    else
    {
      unsigned rmod = 0;  // TODO : randomize?
      for (size_t i = 0, num = lit.getNumChildren(); i < num; i++)
      {
        size_t ii = (i + rmod) % lit.getNumChildren();
        // only recurse if the kind is invertible
        // this allows us to avoid paths that go through skolem functions
        if (!isInvertible(lit.getKind(), ii))
        {
          continue;
        }
        Node litc = getPathToPv(lit[ii], pv, sv, path, visited);
        if (!litc.isNull())
        {
          // path is outermost term index last
          path.push_back(ii);
          std::vector<Node> children;
          if (lit.getMetaKind() == kind::metakind::PARAMETERIZED)
          {
            children.push_back(lit.getOperator());
          }
          for (size_t j = 0, num2 = lit.getNumChildren(); j < num2; j++)
          {
            children.push_back(j == ii ? litc : lit[j]);
          }
          return NodeManager::currentNM()->mkNode(lit.getKind(), children);
        }
      }
    }
  }
  return Node::null();
}

Node BvInverter::getPathToPv(Node lit,
                             Node pv,
                             Node sv,
                             Node pvs,
                             std::vector<unsigned>& path,
                             bool projectNl)
{
  std::unordered_set<TNode> visited;
  Node slit = getPathToPv(lit, pv, sv, path, visited);
  // if we are able to find a (invertible) path to pv
  if (!slit.isNull() && !pvs.isNull())
  {
    // substitute pvs for the other occurrences of pv
    TNode tpv = pv;
    TNode tpvs = pvs;
    Node prev_lit = slit;
    slit = slit.substitute(tpv, tpvs);
    if (!projectNl && slit != prev_lit)
    {
      // found another occurrence of pv that was not on the solve path,
      // hence lit is non-linear wrt pv and we return null.
      return Node::null();
    }
  }
  return slit;
}

/*---------------------------------------------------------------------------*/

/* Drop child at given index from expression.
 * E.g., dropChild((x + y + z), 1) -> (x + z)  */
static Node dropChild(Node n, unsigned index)
{
  unsigned nchildren = n.getNumChildren();
  Assert(nchildren > 0);
  Assert(index < nchildren);

  if (nchildren < 2) return Node::null();

  Kind k = n.getKind();
  NodeBuilder nb(k);
  for (unsigned i = 0; i < nchildren; ++i)
  {
    if (i == index) continue;
    nb << n[i];
  }
  Assert(nb.getNumChildren() > 0);
  return nb.getNumChildren() == 1 ? nb[0] : nb.constructNode();
}

Node BvInverter::solveBvLit(Node sv,
                            Node lit,
                            std::vector<unsigned>& path,
                            BvInverterQuery* m)
{
  Assert(!path.empty());

  bool pol = true;
  unsigned index;
  NodeManager* nm = NodeManager::currentNM();
  Kind k, litk;

  Assert(!path.empty());
  index = path.back();
  Assert(index < lit.getNumChildren());
  path.pop_back();
  litk = k = lit.getKind();

  /* Note: option --bool-to-bv is currently disabled when CBQI BV
   *       is enabled and the logic is quantified.
   *       We currently do not support Boolean operators
   *       that are interpreted as bit-vector operators of width 1.  */

  /* Boolean layer ----------------------------------------------- */

  if (k == NOT)
  {
    pol = !pol;
    lit = lit[index];
    Assert(!path.empty());
    index = path.back();
    Assert(index < lit.getNumChildren());
    path.pop_back();
    litk = k = lit.getKind();
  }

  Assert(k == EQUAL || k == BITVECTOR_ULT || k == BITVECTOR_SLT);

  Node sv_t = lit[index];
  Node t = lit[1 - index];
  if (litk == BITVECTOR_ULT && index == 1)
  {
    litk = BITVECTOR_UGT;
  }
  else if (litk == BITVECTOR_SLT && index == 1)
  {
    litk = BITVECTOR_SGT;
  }

  /* Bit-vector layer -------------------------------------------- */

  while (!path.empty())
  {
    unsigned nchildren = sv_t.getNumChildren();
    Assert(nchildren > 0);
    index = path.back();
    Assert(index < nchildren);
    path.pop_back();
    k = sv_t.getKind();

    /* Note: All n-ary kinds except for CONCAT (i.e., BITVECTOR_AND,
     *       BITVECTOR_OR, MULT, PLUS) are commutative (no case split
     *       based on index). */
    Node s = dropChild(sv_t, index);
    Assert((nchildren == 1 && s.isNull()) || (nchildren > 1 && !s.isNull()));
    TypeNode solve_tn = sv_t[index].getType();
    Node x = getSolveVariable(solve_tn);
    Node ic;

    if (litk == EQUAL && (k == BITVECTOR_NOT || k == BITVECTOR_NEG))
    {
      t = nm->mkNode(k, t);
    }
    else if (litk == EQUAL && k == BITVECTOR_ADD)
    {
      t = nm->mkNode(BITVECTOR_SUB, t, s);
    }
    else if (litk == EQUAL && k == BITVECTOR_XOR)
    {
      t = nm->mkNode(BITVECTOR_XOR, t, s);
    }
    else if (litk == EQUAL && k == BITVECTOR_MULT && s.isConst()
             && bv::utils::getBit(s, 0))
    {
      unsigned w = bv::utils::getSize(s);
      Integer s_val = s.getConst<BitVector>().toInteger();
      Integer mod_val = Integer(1).multiplyByPow2(w);
      Trace("bv-invert-debug")
          << "Compute inverse : " << s_val << " " << mod_val << std::endl;
      Integer inv_val = s_val.modInverse(mod_val);
      Trace("bv-invert-debug") << "Inverse : " << inv_val << std::endl;
      Node inv = bv::utils::mkConst(w, inv_val);
      t = nm->mkNode(BITVECTOR_MULT, inv, t);
    }
    else if (k == BITVECTOR_MULT)
    {
      ic = utils::getICBvMult(pol, litk, k, index, x, s, t);
    }
    else if (k == BITVECTOR_SHL)
    {
      ic = utils::getICBvShl(pol, litk, k, index, x, s, t);
    }
    else if (k == BITVECTOR_UREM)
    {
      ic = utils::getICBvUrem(pol, litk, k, index, x, s, t);
    }
    else if (k == BITVECTOR_UDIV)
    {
      ic = utils::getICBvUdiv(pol, litk, k, index, x, s, t);
    }
    else if (k == BITVECTOR_AND || k == BITVECTOR_OR)
    {
      ic = utils::getICBvAndOr(pol, litk, k, index, x, s, t);
    }
    else if (k == BITVECTOR_LSHR)
    {
      ic = utils::getICBvLshr(pol, litk, k, index, x, s, t);
    }
    else if (k == BITVECTOR_ASHR)
    {
      ic = utils::getICBvAshr(pol, litk, k, index, x, s, t);
    }
    else if (k == BITVECTOR_CONCAT)
    {
      if (litk == EQUAL && options::cegqiBvConcInv())
      {
        /* Compute inverse for s1 o x, x o s2, s1 o x o s2
         * (while disregarding that invertibility depends on si)
         * rather than an invertibility condition (the proper handling).
         * This improves performance on a considerable number of benchmarks.
         *
         * x = t[upper:lower]
         * where
         * upper = getSize(t) - 1 - sum(getSize(sv_t[i])) for i < index
         * lower = getSize(sv_t[i]) for i > index  */
        unsigned upper, lower;
        upper = bv::utils::getSize(t) - 1;
        lower = 0;
        NodeBuilder nb(BITVECTOR_CONCAT);
        for (unsigned i = 0; i < nchildren; i++)
        {
          if (i < index)
          {
            upper -= bv::utils::getSize(sv_t[i]);
          }
          else if (i > index)
          {
            lower += bv::utils::getSize(sv_t[i]);
          }
        }
        t = bv::utils::mkExtract(t, upper, lower);
      }
      else
      {
        ic = utils::getICBvConcat(pol, litk, index, x, sv_t, t);
      }
    }
    else if (k == BITVECTOR_SIGN_EXTEND)
    {
      ic = utils::getICBvSext(pol, litk, index, x, sv_t, t);
    }
    else if (litk == BITVECTOR_ULT || litk == BITVECTOR_UGT)
    {
      ic = utils::getICBvUltUgt(pol, litk, x, t);
    }
    else if (litk == BITVECTOR_SLT || litk == BITVECTOR_SGT)
    {
      ic = utils::getICBvSltSgt(pol, litk, x, t);
    }
    else if (pol == false)
    {
      Assert(litk == EQUAL);
      ic = nm->mkNode(DISTINCT, x, t);
      Trace("bv-invert") << "Add SC_" << litk << "(" << x << "): " << ic
                         << std::endl;
    }
    else
    {
      Trace("bv-invert") << "bv-invert : Unknown kind " << k
                         << " for bit-vector term " << sv_t << std::endl;
      return Node::null();
    }

    if (!ic.isNull())
    {
      /* We generate a witness term (witness x0. ic => x0 <k> s <litk> t) for
       * x <k> s <litk> t. When traversing down, this witness term determines
       * the value for x <k> s = (witness x0. ic => x0 <k> s <litk> t), i.e.,
       * from here on, the propagated literal is a positive equality. */
      litk = EQUAL;
      pol = true;
      /* t = fresh skolem constant */
      t = getInversionNode(ic, solve_tn, m);
      if (t.isNull())
      {
        return t;
      }
    }

    sv_t = sv_t[index];
  }

  /* Base case  */
  Assert(sv_t == sv);
  TypeNode solve_tn = sv.getType();
  Node x = getSolveVariable(solve_tn);
  Node ic;
  if (litk == BITVECTOR_ULT || litk == BITVECTOR_UGT)
  {
    ic = utils::getICBvUltUgt(pol, litk, x, t);
  }
  else if (litk == BITVECTOR_SLT || litk == BITVECTOR_SGT)
  {
    ic = utils::getICBvSltSgt(pol, litk, x, t);
  }
  else if (pol == false)
  {
    Assert(litk == EQUAL);
    ic = nm->mkNode(DISTINCT, x, t);
    Trace("bv-invert") << "Add SC_" << litk << "(" << x << "): " << ic
                       << std::endl;
  }

  return ic.isNull() ? t : getInversionNode(ic, solve_tn, m);
}

/*---------------------------------------------------------------------------*/

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Aina Niemetz, Andrew Reynolds, Mathias Preiner
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		* Inverse rules for bit-vector operators.
14		*/
15
16		#include "theory/quantifiers/bv_inverter.h"
17
18		#include <algorithm>
19
20		#include "expr/skolem_manager.h"
21		#include "options/quantifiers_options.h"
22		#include "theory/bv/theory_bv_utils.h"
23		#include "theory/quantifiers/bv_inverter_utils.h"
24		#include "theory/quantifiers/term_util.h"
25		#include "theory/rewriter.h"
26		#include "util/bitvector.h"
27
28		using namespace cvc5::kind;
29
30		namespace cvc5 {
31		namespace theory {
32		namespace quantifiers {
33
34		/---------------------------------------------------------------------------/
35
36	13789	Node BvInverter::getSolveVariable(TypeNode tn)
37		{
38	13789	std::map<TypeNode, Node>::iterator its = d_solve_var.find(tn);
39	13789	if (its == d_solve_var.end())
40		{
41	1084	SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
42	2168	Node k = sm->mkDummySkolem("slv", tn);
43	1084	d_solve_var[tn] = k;
44	1084	return k;
45		}
46	12705	return its->second;
47		}
48
49		/---------------------------------------------------------------------------/
50
51	1477	Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m)
52		{
53	2954	TNode solve_var = getSolveVariable(tn);
54
55		// condition should be rewritten
56	2954	Node new_cond = Rewriter::rewrite(cond);
57	1477	if (new_cond != cond)
58		{
59	2642	Trace("cegqi-bv-skvinv-debug")
60	1321	<< "Condition " << cond << " was rewritten to " << new_cond
61	1321	<< std::endl;
62		}
63		// optimization : if condition is ( x = solve_var ) should just return
64		// solve_var and not introduce a Skolem this can happen when we ask for
65		// the multiplicative inversion with bv1
66	1477	Node c;
67	1477	if (new_cond.getKind() == EQUAL)
68		{
69	171	for (unsigned i = 0; i < 2; i++)
70		{
71	114	if (new_cond[i] == solve_var)
72		{
73		c = new_cond[1 - i];
74		Trace("cegqi-bv-skvinv")
75		<< "SKVINV : " << c << " is trivially associated with conditon "
76		<< new_cond << std::endl;
77		break;
78		}
79		}
80		}
81
82	1477	if (c.isNull())
83		{
84	1477	NodeManager* nm = NodeManager::currentNM();
85	1477	if (m)
86		{
87	2266	Node x = m->getBoundVariable(tn);
88	2266	Node ccond = new_cond.substitute(solve_var, x);
89	1133	c = nm->mkNode(kind::WITNESS, nm->mkNode(BOUND_VAR_LIST, x), ccond);
90	2266	Trace("cegqi-bv-skvinv")
91	1133	<< "SKVINV : Make " << c << " for " << new_cond << std::endl;
92		}
93		else
94		{
95	688	Trace("bv-invert") << "...fail for " << cond << " : no inverter query!"
96	344	<< std::endl;
97		}
98		}
99		// currently shouldn't cache since
100		// the return value depends on the
101		// state of m (which bound variable is returned).
102	2954	return c;
103		}
104
105		/---------------------------------------------------------------------------/
106
107	21073	static bool isInvertible(Kind k, unsigned index)
108		{
109	21031	return k == NOT \|\| k == EQUAL \|\| k == BITVECTOR_ULT \|\| k == BITVECTOR_SLT
110	12806	\|\| k == BITVECTOR_COMP \|\| k == BITVECTOR_NOT \|\| k == BITVECTOR_NEG
111	11239	\|\| k == BITVECTOR_CONCAT \|\| k == BITVECTOR_SIGN_EXTEND
112	8679	\|\| k == BITVECTOR_ADD \|\| k == BITVECTOR_MULT \|\| k == BITVECTOR_UREM
113	4320	\|\| k == BITVECTOR_UDIV \|\| k == BITVECTOR_AND \|\| k == BITVECTOR_OR
114	2909	\|\| k == BITVECTOR_XOR \|\| k == BITVECTOR_LSHR \|\| k == BITVECTOR_ASHR
115	23376	\|\| k == BITVECTOR_SHL;
116		}
117
118	24630	Node BvInverter::getPathToPv(Node lit,
119		Node pv,
120		Node sv,
121		std::vector<unsigned>& path,
122		std::unordered_set<TNode>& visited)
123		{
124	24630	if (visited.find(lit) == visited.end())
125		{
126	24159	visited.insert(lit);
127	24159	if (lit == pv)
128		{
129	4995	return sv;
130		}
131		else
132		{
133	19164	unsigned rmod = 0; // TODO : randomize?
134	30552	for (size_t i = 0, num = lit.getNumChildren(); i < num; i++)
135		{
136	21073	size_t ii = (i + rmod) % lit.getNumChildren();
137		// only recurse if the kind is invertible
138		// this allows us to avoid paths that go through skolem functions
139	21073	if (!isInvertible(lit.getKind(), ii))
140		{
141	2037	continue;
142		}
143	28387	Node litc = getPathToPv(lit[ii], pv, sv, path, visited);
144	19036	if (!litc.isNull())
145		{
146		// path is outermost term index last
147	9685	path.push_back(ii);
148	19370	std::vector<Node> children;
149	9685	if (lit.getMetaKind() == kind::metakind::PARAMETERIZED)
150		{
151	42	children.push_back(lit.getOperator());
152		}
153	28987	for (size_t j = 0, num2 = lit.getNumChildren(); j < num2; j++)
154		{
155	19302	children.push_back(j == ii ? litc : lit[j]);
156		}
157	9685	return NodeManager::currentNM()->mkNode(lit.getKind(), children);
158		}
159		}
160		}
161		}
162	9950	return Node::null();
163		}
164
165	5594	Node BvInverter::getPathToPv(Node lit,
166		Node pv,
167		Node sv,
168		Node pvs,
169		std::vector<unsigned>& path,
170		bool projectNl)
171		{
172	11188	std::unordered_set<TNode> visited;
173	11188	Node slit = getPathToPv(lit, pv, sv, path, visited);
174		// if we are able to find a (invertible) path to pv
175	5594	if (!slit.isNull() && !pvs.isNull())
176		{
177		// substitute pvs for the other occurrences of pv
178	8966	TNode tpv = pv;
179	8966	TNode tpvs = pvs;
180	8966	Node prev_lit = slit;
181	4569	slit = slit.substitute(tpv, tpvs);
182	4569	if (!projectNl && slit != prev_lit)
183		{
184		// found another occurrence of pv that was not on the solve path,
185		// hence lit is non-linear wrt pv and we return null.
186	172	return Node::null();
187		}
188		}
189	5422	return slit;
190		}
191
192		/---------------------------------------------------------------------------/
193
194		/* Drop child at given index from expression.
195		* E.g., dropChild((x + y + z), 1) -> (x + z) */
196	4128	static Node dropChild(Node n, unsigned index)
197		{
198	4128	unsigned nchildren = n.getNumChildren();
199	4128	Assert(nchildren > 0);
200	4128	Assert(index < nchildren);
201
202	4128	if (nchildren < 2) return Node::null();
203
204	3996	Kind k = n.getKind();
205	7992	NodeBuilder nb(k);
206	12082	for (unsigned i = 0; i < nchildren; ++i)
207		{
208	8086	if (i == index) continue;
209	4090	nb << n[i];
210		}
211	3996	Assert(nb.getNumChildren() > 0);
212	3996	return nb.getNumChildren() == 1 ? nb[0] : nb.constructNode();
213		}
214
215	4823	Node BvInverter::solveBvLit(Node sv,
216		Node lit,
217		std::vector<unsigned>& path,
218		BvInverterQuery* m)
219		{
220	4823	Assert(!path.empty());
221
222	4823	bool pol = true;
223		unsigned index;
224	4823	NodeManager* nm = NodeManager::currentNM();
225		Kind k, litk;
226
227	4823	Assert(!path.empty());
228	4823	index = path.back();
229	4823	Assert(index < lit.getNumChildren());
230	4823	path.pop_back();
231	4823	litk = k = lit.getKind();
232
233		/* Note: option --bool-to-bv is currently disabled when CBQI BV
234		* is enabled and the logic is quantified.
235		* We currently do not support Boolean operators
236		* that are interpreted as bit-vector operators of width 1. */
237
238		/* Boolean layer ----------------------------------------------- */
239
240	4823	if (k == NOT)
241		{
242	42	pol = !pol;
243	42	lit = lit[index];
244	42	Assert(!path.empty());
245	42	index = path.back();
246	42	Assert(index < lit.getNumChildren());
247	42	path.pop_back();
248	42	litk = k = lit.getKind();
249		}
250
251	4823	Assert(k == EQUAL \|\| k == BITVECTOR_ULT \|\| k == BITVECTOR_SLT);
252
253	9646	Node sv_t = lit[index];
254	9646	Node t = lit[1 - index];
255	4823	if (litk == BITVECTOR_ULT && index == 1)
256		{
257	2	litk = BITVECTOR_UGT;
258		}
259	4821	else if (litk == BITVECTOR_SLT && index == 1)
260		{
261		litk = BITVECTOR_SGT;
262		}
263
264		/* Bit-vector layer -------------------------------------------- */
265
266	10319	while (!path.empty())
267		{
268	4128	unsigned nchildren = sv_t.getNumChildren();
269	4128	Assert(nchildren > 0);
270	4128	index = path.back();
271	4128	Assert(index < nchildren);
272	4128	path.pop_back();
273	4128	k = sv_t.getKind();
274
275		/* Note: All n-ary kinds except for CONCAT (i.e., BITVECTOR_AND,
276		* BITVECTOR_OR, MULT, PLUS) are commutative (no case split
277		* based on index). */
278	6876	Node s = dropChild(sv_t, index);
279	4128	Assert((nchildren == 1 && s.isNull()) \|\| (nchildren > 1 && !s.isNull()));
280	6876	TypeNode solve_tn = sv_t[index].getType();
281	6876	Node x = getSolveVariable(solve_tn);
282	6876	Node ic;
283
284	4128	if (litk == EQUAL && (k == BITVECTOR_NOT \|\| k == BITVECTOR_NEG))
285		{
286	90	t = nm->mkNode(k, t);
287		}
288	4038	else if (litk == EQUAL && k == BITVECTOR_ADD)
289		{
290	1049	t = nm->mkNode(BITVECTOR_SUB, t, s);
291		}
292	2989	else if (litk == EQUAL && k == BITVECTOR_XOR)
293		{
294	8	t = nm->mkNode(BITVECTOR_XOR, t, s);
295		}
296	8943	else if (litk == EQUAL && k == BITVECTOR_MULT && s.isConst()
297	5986	&& bv::utils::getBit(s, 0))
298		{
299	24	unsigned w = bv::utils::getSize(s);
300	48	Integer s_val = s.getConst<BitVector>().toInteger();
301	48	Integer mod_val = Integer(1).multiplyByPow2(w);
302	48	Trace("bv-invert-debug")
303	24	<< "Compute inverse : " << s_val << " " << mod_val << std::endl;
304	48	Integer inv_val = s_val.modInverse(mod_val);
305	24	Trace("bv-invert-debug") << "Inverse : " << inv_val << std::endl;
306	48	Node inv = bv::utils::mkConst(w, inv_val);
307	24	t = nm->mkNode(BITVECTOR_MULT, inv, t);
308		}
309	2957	else if (k == BITVECTOR_MULT)
310		{
311	286	ic = utils::getICBvMult(pol, litk, k, index, x, s, t);
312		}
313	2671	else if (k == BITVECTOR_SHL)
314		{
315	172	ic = utils::getICBvShl(pol, litk, k, index, x, s, t);
316		}
317	2499	else if (k == BITVECTOR_UREM)
318		{
319	126	ic = utils::getICBvUrem(pol, litk, k, index, x, s, t);
320		}
321	2373	else if (k == BITVECTOR_UDIV)
322		{
323	108	ic = utils::getICBvUdiv(pol, litk, k, index, x, s, t);
324		}
325	2265	else if (k == BITVECTOR_AND \|\| k == BITVECTOR_OR)
326		{
327	446	ic = utils::getICBvAndOr(pol, litk, k, index, x, s, t);
328		}
329	1819	else if (k == BITVECTOR_LSHR)
330		{
331	134	ic = utils::getICBvLshr(pol, litk, k, index, x, s, t);
332		}
333	1685	else if (k == BITVECTOR_ASHR)
334		{
335	145	ic = utils::getICBvAshr(pol, litk, k, index, x, s, t);
336		}
337	1540	else if (k == BITVECTOR_CONCAT)
338		{
339	462	if (litk == EQUAL && options::cegqiBvConcInv())
340		{
341		/* Compute inverse for s1 o x, x o s2, s1 o x o s2
342		* (while disregarding that invertibility depends on si)
343		* rather than an invertibility condition (the proper handling).
344		* This improves performance on a considerable number of benchmarks.
345		*
346		* x = t[upper:lower]
347		* where
348		* upper = getSize(t) - 1 - sum(getSize(sv_t[i])) for i < index
349		* lower = getSize(sv_t[i]) for i > index */
350		unsigned upper, lower;
351	462	upper = bv::utils::getSize(t) - 1;
352	462	lower = 0;
353	924	NodeBuilder nb(BITVECTOR_CONCAT);
354	1472	for (unsigned i = 0; i < nchildren; i++)
355		{
356	1010	if (i < index)
357		{
358	170	upper -= bv::utils::getSize(sv_t[i]);
359		}
360	840	else if (i > index)
361		{
362	378	lower += bv::utils::getSize(sv_t[i]);
363		}
364		}
365	462	t = bv::utils::mkExtract(t, upper, lower);
366		}
367		else
368		{
369		ic = utils::getICBvConcat(pol, litk, index, x, sv_t, t);
370		}
371		}
372	1078	else if (k == BITVECTOR_SIGN_EXTEND)
373		{
374	42	ic = utils::getICBvSext(pol, litk, index, x, sv_t, t);
375		}
376	1036	else if (litk == BITVECTOR_ULT \|\| litk == BITVECTOR_UGT)
377		{
378		ic = utils::getICBvUltUgt(pol, litk, x, t);
379		}
380	1036	else if (litk == BITVECTOR_SLT \|\| litk == BITVECTOR_SGT)
381		{
382		ic = utils::getICBvSltSgt(pol, litk, x, t);
383		}
384	1036	else if (pol == false)
385		{
386		Assert(litk == EQUAL);
387		ic = nm->mkNode(DISTINCT, x, t);
388		Trace("bv-invert") << "Add SC_" << litk << "(" << x << "): " << ic
389		<< std::endl;
390		}
391		else
392		{
393	2072	Trace("bv-invert") << "bv-invert : Unknown kind " << k
394	1036	<< " for bit-vector term " << sv_t << std::endl;
395	1036	return Node::null();
396		}
397
398	3092	if (!ic.isNull())
399		{
400		/* We generate a witness term (witness x0. ic => x0 <k> s <litk> t) for
401		* x <k> s <litk> t. When traversing down, this witness term determines
402		* the value for x <k> s = (witness x0. ic => x0 <k> s <litk> t), i.e.,
403		* from here on, the propagated literal is a positive equality. */
404	1459	litk = EQUAL;
405	1459	pol = true;
406		/* t = fresh skolem constant */
407	1459	t = getInversionNode(ic, solve_tn, m);
408	1459	if (t.isNull())
409		{
410	344	return t;
411		}
412		}
413
414	2748	sv_t = sv_t[index];
415		}
416
417		/* Base case */
418	3443	Assert(sv_t == sv);
419	6886	TypeNode solve_tn = sv.getType();
420	6886	Node x = getSolveVariable(solve_tn);
421	6886	Node ic;
422	3443	if (litk == BITVECTOR_ULT \|\| litk == BITVECTOR_UGT)
423		{
424	6	ic = utils::getICBvUltUgt(pol, litk, x, t);
425		}
426	3437	else if (litk == BITVECTOR_SLT \|\| litk == BITVECTOR_SGT)
427		{
428		ic = utils::getICBvSltSgt(pol, litk, x, t);
429		}
430	3437	else if (pol == false)
431		{
432	12	Assert(litk == EQUAL);
433	12	ic = nm->mkNode(DISTINCT, x, t);
434	24	Trace("bv-invert") << "Add SC_" << litk << "(" << x << "): " << ic
435	12	<< std::endl;
436		}
437
438	3443	return ic.isNull() ? t : getInversionNode(ic, solve_tn, m);
439		}
440
441		/---------------------------------------------------------------------------/
442
443		} // namespace quantifiers
444		} // namespace theory
445	29502	} // namespace cvc5