Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/bv_inverter.cpp	Lines:	187	201	93.0 %
Date:	2021-05-22	Branches:	476	1060	44.9 %


/******************************************************************************
 * 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"

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