Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/operator_elim.cpp	Lines:	183	195	93.8 %
Date:	2021-11-07	Branches:	488	986	49.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Tim King, 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.
 * ****************************************************************************
 *
 * Implementation of operator elimination for arithmetic.
 */

#include "theory/arith/operator_elim.h"

#include <sstream>

#include "expr/attribute.h"
#include "expr/bound_var_manager.h"
#include "options/arith_options.h"
#include "proof/conv_proof_generator.h"
#include "smt/env.h"
#include "smt/logic_exception.h"
#include "theory/arith/arith_utilities.h"
#include "theory/rewriter.h"
#include "theory/theory.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace arith {

/**
 * Attribute used for constructing unique bound variables that are binders
 * for witness terms below. In other words, this attribute maps nodes to
 * the bound variable of a witness term for eliminating that node.
 *
 * Notice we use the same attribute for most bound variables below, since using
 * a node itself is a sufficient cache key for constructing a bound variable.
 * The exception is to_int / is_int, which share a skolem based on their
 * argument.
 */
struct ArithWitnessVarAttributeId
{
};
using ArithWitnessVarAttribute = expr::Attribute<ArithWitnessVarAttributeId, Node>;
/**
 * Similar to above, shared for to_int and is_int. This is used for introducing
 * an integer bound variable used to construct the witness term for t in the
 * contexts (to_int t) and (is_int t).
 */
struct ToIntWitnessVarAttributeId
{
};
using ToIntWitnessVarAttribute
 = expr::Attribute<ToIntWitnessVarAttributeId, Node>;

OperatorElim::OperatorElim(Env& env)
    : EnvObj(env), EagerProofGenerator(d_env.getProofNodeManager())
{
}

void OperatorElim::checkNonLinearLogic(Node term)
{
  if (d_env.getLogicInfo().isLinear())
  {
    Trace("arith-logic") << "ERROR: Non-linear term in linear logic: " << term
                         << std::endl;
    std::stringstream serr;
    serr << "A non-linear fact was asserted to arithmetic in a linear logic."
         << std::endl;
    serr << "The fact in question: " << term << std::endl;
    throw LogicException(serr.str());
  }
}

TrustNode OperatorElim::eliminate(Node n,
                                  std::vector<SkolemLemma>& lems,
                                  bool partialOnly)
{
  TConvProofGenerator* tg = nullptr;
  Node nn = eliminateOperators(n, lems, tg, partialOnly);
  if (nn != n)
  {
    return TrustNode::mkTrustRewrite(n, nn, nullptr);
  }
  return TrustNode::null();
}

Node OperatorElim::eliminateOperators(Node node,
                                      std::vector<SkolemLemma>& lems,
                                      TConvProofGenerator* tg,
                                      bool partialOnly)
{
  NodeManager* nm = NodeManager::currentNM();
  BoundVarManager* bvm = nm->getBoundVarManager();
  Kind k = node.getKind();
  switch (k)
  {
    case TANGENT:
    case COSECANT:
    case SECANT:
    case COTANGENT:
    {
      // these are eliminated by rewriting
      return rewrite(node);
      break;
    }
    case TO_INTEGER:
    case IS_INTEGER:
    {
      if (partialOnly)
      {
        // not eliminating total operators
        return node;
      }
      // node[0] - 1 < toIntSkolem <= node[0]
      // -1 < toIntSkolem - node[0] <= 0
      // 0 <= node[0] - toIntSkolem < 1
      Node v =
          bvm->mkBoundVar<ToIntWitnessVarAttribute>(node[0], nm->integerType());
      Node one = mkRationalNode(1);
      Node zero = mkRationalNode(0);
      Node diff = nm->mkNode(MINUS, node[0], v);
      Node lem = mkInRange(diff, zero, one);
      Node toIntSkolem =
          mkWitnessTerm(v,
                        lem,
                        "toInt",
                        "a conversion of a Real term to its Integer part",
                        lems);
      if (k == IS_INTEGER)
      {
        return nm->mkNode(EQUAL, node[0], toIntSkolem);
      }
      Assert(k == TO_INTEGER);
      return toIntSkolem;
    }

    case INTS_DIVISION_TOTAL:
    case INTS_MODULUS_TOTAL:
    {
      if (partialOnly)
      {
        // not eliminating total operators
        return node;
      }
      Node den = rewrite(node[1]);
      Node num = rewrite(node[0]);
      Node rw = nm->mkNode(k, num, den);
      Node v = bvm->mkBoundVar<ArithWitnessVarAttribute>(rw, nm->integerType());
      Node lem;
      Node leqNum = nm->mkNode(LEQ, nm->mkNode(MULT, den, v), num);
      if (den.isConst())
      {
        const Rational& rat = den.getConst<Rational>();
        if (num.isConst() || rat == 0)
        {
          // just rewrite
          return rewrite(node);
        }
        if (rat > 0)
        {
          lem = nm->mkNode(
              AND,
              leqNum,
              nm->mkNode(
                  LT,
                  num,
                  nm->mkNode(MULT,
                             den,
                             nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))));
        }
        else
        {
          lem = nm->mkNode(
              AND,
              leqNum,
              nm->mkNode(
                  LT,
                  num,
                  nm->mkNode(MULT,
                             den,
                             nm->mkNode(PLUS, v, nm->mkConst(Rational(-1))))));
        }
      }
      else
      {
        checkNonLinearLogic(node);
        lem = nm->mkNode(
            AND,
            nm->mkNode(
                IMPLIES,
                nm->mkNode(GT, den, nm->mkConst(Rational(0))),
                nm->mkNode(
                    AND,
                    leqNum,
                    nm->mkNode(
                        LT,
                        num,
                        nm->mkNode(
                            MULT,
                            den,
                            nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))))),
            nm->mkNode(
                IMPLIES,
                nm->mkNode(LT, den, nm->mkConst(Rational(0))),
                nm->mkNode(
                    AND,
                    leqNum,
                    nm->mkNode(
                        LT,
                        num,
                        nm->mkNode(
                            MULT,
                            den,
                            nm->mkNode(PLUS, v, nm->mkConst(Rational(-1))))))));
      }
      Node intVar = mkWitnessTerm(
          v, lem, "linearIntDiv", "the result of an intdiv-by-k term", lems);
      if (k == INTS_MODULUS_TOTAL)
      {
        Node nn = nm->mkNode(MINUS, num, nm->mkNode(MULT, den, intVar));
        return nn;
      }
      else
      {
        return intVar;
      }
      break;
    }
    case DIVISION_TOTAL:
    {
      if (partialOnly)
      {
        // not eliminating total operators
        return node;
      }
      Node num = rewrite(node[0]);
      Node den = rewrite(node[1]);
      if (den.isConst())
      {
        // No need to eliminate here, can eliminate via rewriting later.
        // Moreover, rewriting may change the type of this node from real to
        // int, which impacts certain issues with subtyping.
        return node;
      }
      checkNonLinearLogic(node);
      Node rw = nm->mkNode(k, num, den);
      Node v = bvm->mkBoundVar<ArithWitnessVarAttribute>(rw, nm->realType());
      Node lem = nm->mkNode(IMPLIES,
                            den.eqNode(nm->mkConst(Rational(0))).negate(),
                            nm->mkNode(MULT, den, v).eqNode(num));
      return mkWitnessTerm(
          v, lem, "nonlinearDiv", "the result of a non-linear div term", lems);
      break;
    }
    case DIVISION:
    {
      Node num = rewrite(node[0]);
      Node den = rewrite(node[1]);
      Node ret = nm->mkNode(DIVISION_TOTAL, num, den);
      if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
      {
        checkNonLinearLogic(node);
        Node divByZeroNum = getArithSkolemApp(num, SkolemFunId::DIV_BY_ZERO);
        Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
        ret = nm->mkNode(ITE, denEq0, divByZeroNum, ret);
      }
      return ret;
      break;
    }

    case INTS_DIVISION:
    {
      // partial function: integer div
      Node num = rewrite(node[0]);
      Node den = rewrite(node[1]);
      Node ret = nm->mkNode(INTS_DIVISION_TOTAL, num, den);
      if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
      {
        checkNonLinearLogic(node);
        Node intDivByZeroNum =
            getArithSkolemApp(num, SkolemFunId::INT_DIV_BY_ZERO);
        Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
        ret = nm->mkNode(ITE, denEq0, intDivByZeroNum, ret);
      }
      return ret;
      break;
    }

    case INTS_MODULUS:
    {
      // partial function: mod
      Node num = rewrite(node[0]);
      Node den = rewrite(node[1]);
      Node ret = nm->mkNode(INTS_MODULUS_TOTAL, num, den);
      if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
      {
        checkNonLinearLogic(node);
        Node modZeroNum = getArithSkolemApp(num, SkolemFunId::MOD_BY_ZERO);
        Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
        ret = nm->mkNode(ITE, denEq0, modZeroNum, ret);
      }
      return ret;
      break;
    }

    case ABS:
    {
      return nm->mkNode(ITE,
                        nm->mkNode(LT, node[0], nm->mkConst(Rational(0))),
                        nm->mkNode(UMINUS, node[0]),
                        node[0]);
      break;
    }
    case SQRT:
    case ARCSINE:
    case ARCCOSINE:
    case ARCTANGENT:
    case ARCCOSECANT:
    case ARCSECANT:
    case ARCCOTANGENT:
    {
      if (partialOnly)
      {
        // not eliminating total operators
        return node;
      }
      checkNonLinearLogic(node);
      // eliminate inverse functions here
      Node var =
          bvm->mkBoundVar<ArithWitnessVarAttribute>(node, nm->realType());
      Node lem;
      if (k == SQRT)
      {
        Node skolemApp = getArithSkolemApp(node[0], SkolemFunId::SQRT);
        Node uf = skolemApp.eqNode(var);
        Node nonNeg =
            nm->mkNode(AND, nm->mkNode(MULT, var, var).eqNode(node[0]), uf);

        // sqrt(x) reduces to:
        // witness y. ite(x >= 0.0, y * y = x ^ y = Uf(x), y = Uf(x))
        //
        // Uf(x) makes sure that the reduction still behaves like a function,
        // otherwise the reduction of (x = 1) ^ (sqrt(x) != sqrt(1)) would be
        // satisfiable. On the original formula, this would require that we
        // simultaneously interpret sqrt(1) as 1 and -1, which is not a valid
        // model.
        lem = nm->mkNode(ITE,
                         nm->mkNode(GEQ, node[0], nm->mkConst(Rational(0))),
                         nonNeg,
                         uf);
      }
      else
      {
        Node pi = mkPi();

        // range of the skolem
        Node rlem;
        if (k == ARCSINE || k == ARCTANGENT || k == ARCCOSECANT)
        {
          Node half = nm->mkConst(Rational(1) / Rational(2));
          Node pi2 = nm->mkNode(MULT, half, pi);
          Node npi2 = nm->mkNode(MULT, nm->mkConst(Rational(-1)), pi2);
          // -pi/2 < var <= pi/2
          rlem = nm->mkNode(
              AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2));
        }
        else
        {
          // 0 <= var < pi
          rlem = nm->mkNode(AND,
                            nm->mkNode(LEQ, nm->mkConst(Rational(0)), var),
                            nm->mkNode(LT, var, pi));
        }

        Kind rk =
            k == ARCSINE
                ? SINE
                : (k == ARCCOSINE
                       ? COSINE
                       : (k == ARCTANGENT
                              ? TANGENT
                              : (k == ARCCOSECANT
                                     ? COSECANT
                                     : (k == ARCSECANT ? SECANT : COTANGENT))));
        Node invTerm = nm->mkNode(rk, var);
        lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0]));
      }
      Assert(!lem.isNull());
      return mkWitnessTerm(
          var,
          lem,
          "tfk",
          "Skolem to eliminate a non-standard transcendental function",
          lems);
      break;
    }

    default: break;
  }
  return node;
}

Node OperatorElim::getAxiomFor(Node n) { return Node::null(); }

Node OperatorElim::getArithSkolem(SkolemFunId id)
{
  std::map<SkolemFunId, Node>::iterator it = d_arithSkolem.find(id);
  if (it == d_arithSkolem.end())
  {
    NodeManager* nm = NodeManager::currentNM();
    TypeNode tn;
    if (id == SkolemFunId::DIV_BY_ZERO || id == SkolemFunId::SQRT)
    {
      tn = nm->realType();
    }
    else
    {
      tn = nm->integerType();
    }
    Node skolem;
    SkolemManager* sm = nm->getSkolemManager();
    if (options().arith.arithNoPartialFun)
    {
      // partial function: division, where we treat the skolem function as
      // a constant
      skolem = sm->mkSkolemFunction(id, tn);
    }
    else
    {
      // partial function: division
      skolem = sm->mkSkolemFunction(id, nm->mkFunctionType(tn, tn));
    }
    // cache it
    d_arithSkolem[id] = skolem;
    return skolem;
  }
  return it->second;
}

Node OperatorElim::getArithSkolemApp(Node n, SkolemFunId id)
{
  Node skolem = getArithSkolem(id);
  if (!options().arith.arithNoPartialFun)
  {
    skolem = NodeManager::currentNM()->mkNode(APPLY_UF, skolem, n);
  }
  return skolem;
}

Node OperatorElim::mkWitnessTerm(Node v,
                                 Node pred,
                                 const std::string& prefix,
                                 const std::string& comment,
                                 std::vector<SkolemLemma>& lems)
{
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  // we mark that we should send a lemma
  Node k = sm->mkSkolem(
      v, pred, prefix, comment, SkolemManager::SKOLEM_DEFAULT, this);
  if (d_pnm != nullptr)
  {
    Node lem = SkolemLemma::getSkolemLemmaFor(k);
    TrustNode tlem =
        mkTrustNode(lem, PfRule::THEORY_PREPROCESS_LEMMA, {}, {lem});
    lems.push_back(SkolemLemma(tlem, k));
  }
  else
  {
    lems.push_back(SkolemLemma(k, nullptr));
  }
  return k;
}

}  // namespace arith
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Tim King, 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		* Implementation of operator elimination for arithmetic.
14		*/
15
16		#include "theory/arith/operator_elim.h"
17
18		#include <sstream>
19
20		#include "expr/attribute.h"
21		#include "expr/bound_var_manager.h"
22		#include "options/arith_options.h"
23		#include "proof/conv_proof_generator.h"
24		#include "smt/env.h"
25		#include "smt/logic_exception.h"
26		#include "theory/arith/arith_utilities.h"
27		#include "theory/rewriter.h"
28		#include "theory/theory.h"
29
30		using namespace cvc5::kind;
31
32		namespace cvc5 {
33		namespace theory {
34		namespace arith {
35
36		/**
37		* Attribute used for constructing unique bound variables that are binders
38		* for witness terms below. In other words, this attribute maps nodes to
39		* the bound variable of a witness term for eliminating that node.
40		*
41		* Notice we use the same attribute for most bound variables below, since using
42		* a node itself is a sufficient cache key for constructing a bound variable.
43		* The exception is to_int / is_int, which share a skolem based on their
44		* argument.
45		*/
46		struct ArithWitnessVarAttributeId
47		{
48		};
49		using ArithWitnessVarAttribute = expr::Attribute<ArithWitnessVarAttributeId, Node>;
50		/**
51		* Similar to above, shared for to_int and is_int. This is used for introducing
52		* an integer bound variable used to construct the witness term for t in the
53		* contexts (to_int t) and (is_int t).
54		*/
55		struct ToIntWitnessVarAttributeId
56		{
57		};
58		using ToIntWitnessVarAttribute
59		= expr::Attribute<ToIntWitnessVarAttributeId, Node>;
60
61	15273	OperatorElim::OperatorElim(Env& env)
62	15273	: EnvObj(env), EagerProofGenerator(d_env.getProofNodeManager())
63		{
64	15273	}
65
66	1053	void OperatorElim::checkNonLinearLogic(Node term)
67		{
68	1053	if (d_env.getLogicInfo().isLinear())
69		{
70	12	Trace("arith-logic") << "ERROR: Non-linear term in linear logic: " << term
71	6	<< std::endl;
72	12	std::stringstream serr;
73	6	serr << "A non-linear fact was asserted to arithmetic in a linear logic."
74	6	<< std::endl;
75	6	serr << "The fact in question: " << term << std::endl;
76	6	throw LogicException(serr.str());
77		}
78	1047	}
79
80	434736	TrustNode OperatorElim::eliminate(Node n,
81		std::vector<SkolemLemma>& lems,
82		bool partialOnly)
83		{
84	434736	TConvProofGenerator* tg = nullptr;
85	869466	Node nn = eliminateOperators(n, lems, tg, partialOnly);
86	434730	if (nn != n)
87		{
88	2402	return TrustNode::mkTrustRewrite(n, nn, nullptr);
89		}
90	432328	return TrustNode::null();
91		}
92
93	434736	Node OperatorElim::eliminateOperators(Node node,
94		std::vector<SkolemLemma>& lems,
95		TConvProofGenerator* tg,
96		bool partialOnly)
97		{
98	434736	NodeManager* nm = NodeManager::currentNM();
99	434736	BoundVarManager* bvm = nm->getBoundVarManager();
100	434736	Kind k = node.getKind();
101	434736	switch (k)
102		{
103		case TANGENT:
104		case COSECANT:
105		case SECANT:
106		case COTANGENT:
107		{
108		// these are eliminated by rewriting
109		return rewrite(node);
110		break;
111		}
112	102	case TO_INTEGER:
113		case IS_INTEGER:
114		{
115	102	if (partialOnly)
116		{
117		// not eliminating total operators
118		return node;
119		}
120		// node[0] - 1 < toIntSkolem <= node[0]
121		// -1 < toIntSkolem - node[0] <= 0
122		// 0 <= node[0] - toIntSkolem < 1
123		Node v =
124	204	bvm->mkBoundVar<ToIntWitnessVarAttribute>(node[0], nm->integerType());
125	204	Node one = mkRationalNode(1);
126	204	Node zero = mkRationalNode(0);
127	204	Node diff = nm->mkNode(MINUS, node[0], v);
128	204	Node lem = mkInRange(diff, zero, one);
129		Node toIntSkolem =
130		mkWitnessTerm(v,
131		lem,
132		"toInt",
133		"a conversion of a Real term to its Integer part",
134	204	lems);
135	102	if (k == IS_INTEGER)
136		{
137	16	return nm->mkNode(EQUAL, node[0], toIntSkolem);
138		}
139	86	Assert(k == TO_INTEGER);
140	86	return toIntSkolem;
141		}
142
143	1569	case INTS_DIVISION_TOTAL:
144		case INTS_MODULUS_TOTAL:
145		{
146	1569	if (partialOnly)
147		{
148		// not eliminating total operators
149	1599	return node;
150		}
151	1539	Node den = rewrite(node[1]);
152	1539	Node num = rewrite(node[0]);
153	1539	Node rw = nm->mkNode(k, num, den);
154	1539	Node v = bvm->mkBoundVar<ArithWitnessVarAttribute>(rw, nm->integerType());
155	1539	Node lem;
156	1539	Node leqNum = nm->mkNode(LEQ, nm->mkNode(MULT, den, v), num);
157	1539	if (den.isConst())
158		{
159	1235	const Rational& rat = den.getConst<Rational>();
160	1235	if (num.isConst() \|\| rat == 0)
161		{
162		// just rewrite
163		return rewrite(node);
164		}
165	1235	if (rat > 0)
166		{
167	1235	lem = nm->mkNode(
168		AND,
169		leqNum,
170	2470	nm->mkNode(
171		LT,
172		num,
173	2470	nm->mkNode(MULT,
174		den,
175	2470	nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))));
176		}
177		else
178		{
179		lem = nm->mkNode(
180		AND,
181		leqNum,
182		nm->mkNode(
183		LT,
184		num,
185		nm->mkNode(MULT,
186		den,
187		nm->mkNode(PLUS, v, nm->mkConst(Rational(-1))))));
188		}
189		}
190		else
191		{
192	304	checkNonLinearLogic(node);
193	912	lem = nm->mkNode(
194		AND,
195	1216	nm->mkNode(
196		IMPLIES,
197	608	nm->mkNode(GT, den, nm->mkConst(Rational(0))),
198	608	nm->mkNode(
199		AND,
200		leqNum,
201	608	nm->mkNode(
202		LT,
203		num,
204	608	nm->mkNode(
205		MULT,
206		den,
207	608	nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))))),
208	1216	nm->mkNode(
209		IMPLIES,
210	608	nm->mkNode(LT, den, nm->mkConst(Rational(0))),
211	608	nm->mkNode(
212		AND,
213		leqNum,
214	608	nm->mkNode(
215		LT,
216		num,
217	608	nm->mkNode(
218		MULT,
219		den,
220	608	nm->mkNode(PLUS, v, nm->mkConst(Rational(-1))))))));
221		}
222		Node intVar = mkWitnessTerm(
223	1539	v, lem, "linearIntDiv", "the result of an intdiv-by-k term", lems);
224	1539	if (k == INTS_MODULUS_TOTAL)
225		{
226	1670	Node nn = nm->mkNode(MINUS, num, nm->mkNode(MULT, den, intVar));
227	835	return nn;
228		}
229		else
230		{
231	704	return intVar;
232		}
233		break;
234		}
235	161	case DIVISION_TOTAL:
236		{
237	161	if (partialOnly)
238		{
239		// not eliminating total operators
240	2	return node;
241		}
242	318	Node num = rewrite(node[0]);
243	318	Node den = rewrite(node[1]);
244	159	if (den.isConst())
245		{
246		// No need to eliminate here, can eliminate via rewriting later.
247		// Moreover, rewriting may change the type of this node from real to
248		// int, which impacts certain issues with subtyping.
249		return node;
250		}
251	159	checkNonLinearLogic(node);
252	318	Node rw = nm->mkNode(k, num, den);
253	318	Node v = bvm->mkBoundVar<ArithWitnessVarAttribute>(rw, nm->realType());
254		Node lem = nm->mkNode(IMPLIES,
255	318	den.eqNode(nm->mkConst(Rational(0))).negate(),
256	636	nm->mkNode(MULT, den, v).eqNode(num));
257		return mkWitnessTerm(
258	159	v, lem, "nonlinearDiv", "the result of a non-linear div term", lems);
259		break;
260		}
261	206	case DIVISION:
262		{
263	412	Node num = rewrite(node[0]);
264	412	Node den = rewrite(node[1]);
265	412	Node ret = nm->mkNode(DIVISION_TOTAL, num, den);
266	206	if (!den.isConst() \|\| den.getConst<Rational>().sgn() == 0)
267		{
268	209	checkNonLinearLogic(node);
269	394	Node divByZeroNum = getArithSkolemApp(num, SkolemFunId::DIV_BY_ZERO);
270	394	Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
271	197	ret = nm->mkNode(ITE, denEq0, divByZeroNum, ret);
272		}
273	200	return ret;
274		break;
275		}
276
277	225	case INTS_DIVISION:
278		{
279		// partial function: integer div
280	450	Node num = rewrite(node[0]);
281	450	Node den = rewrite(node[1]);
282	450	Node ret = nm->mkNode(INTS_DIVISION_TOTAL, num, den);
283	225	if (!den.isConst() \|\| den.getConst<Rational>().sgn() == 0)
284		{
285	225	checkNonLinearLogic(node);
286		Node intDivByZeroNum =
287	450	getArithSkolemApp(num, SkolemFunId::INT_DIV_BY_ZERO);
288	450	Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
289	225	ret = nm->mkNode(ITE, denEq0, intDivByZeroNum, ret);
290		}
291	225	return ret;
292		break;
293		}
294
295	106	case INTS_MODULUS:
296		{
297		// partial function: mod
298	212	Node num = rewrite(node[0]);
299	212	Node den = rewrite(node[1]);
300	212	Node ret = nm->mkNode(INTS_MODULUS_TOTAL, num, den);
301	106	if (!den.isConst() \|\| den.getConst<Rational>().sgn() == 0)
302		{
303	106	checkNonLinearLogic(node);
304	212	Node modZeroNum = getArithSkolemApp(num, SkolemFunId::MOD_BY_ZERO);
305	212	Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
306	106	ret = nm->mkNode(ITE, denEq0, modZeroNum, ret);
307		}
308	106	return ret;
309		break;
310		}
311
312	15	case ABS:
313		{
314		return nm->mkNode(ITE,
315	30	nm->mkNode(LT, node[0], nm->mkConst(Rational(0))),
316	30	nm->mkNode(UMINUS, node[0]),
317	75	node[0]);
318		break;
319		}
320	58	case SQRT:
321		case ARCSINE:
322		case ARCCOSINE:
323		case ARCTANGENT:
324		case ARCCOSECANT:
325		case ARCSECANT:
326		case ARCCOTANGENT:
327		{
328	58	if (partialOnly)
329		{
330		// not eliminating total operators
331	2	return node;
332		}
333	56	checkNonLinearLogic(node);
334		// eliminate inverse functions here
335		Node var =
336	112	bvm->mkBoundVar<ArithWitnessVarAttribute>(node, nm->realType());
337	112	Node lem;
338	56	if (k == SQRT)
339		{
340	80	Node skolemApp = getArithSkolemApp(node[0], SkolemFunId::SQRT);
341	80	Node uf = skolemApp.eqNode(var);
342		Node nonNeg =
343	80	nm->mkNode(AND, nm->mkNode(MULT, var, var).eqNode(node[0]), uf);
344
345		// sqrt(x) reduces to:
346		// witness y. ite(x >= 0.0, y * y = x ^ y = Uf(x), y = Uf(x))
347		//
348		// Uf(x) makes sure that the reduction still behaves like a function,
349		// otherwise the reduction of (x = 1) ^ (sqrt(x) != sqrt(1)) would be
350		// satisfiable. On the original formula, this would require that we
351		// simultaneously interpret sqrt(1) as 1 and -1, which is not a valid
352		// model.
353	120	lem = nm->mkNode(ITE,
354	80	nm->mkNode(GEQ, node[0], nm->mkConst(Rational(0))),
355		nonNeg,
356		uf);
357		}
358		else
359		{
360	32	Node pi = mkPi();
361
362		// range of the skolem
363	32	Node rlem;
364	16	if (k == ARCSINE \|\| k == ARCTANGENT \|\| k == ARCCOSECANT)
365		{
366	24	Node half = nm->mkConst(Rational(1) / Rational(2));
367	24	Node pi2 = nm->mkNode(MULT, half, pi);
368	24	Node npi2 = nm->mkNode(MULT, nm->mkConst(Rational(-1)), pi2);
369		// -pi/2 < var <= pi/2
370	36	rlem = nm->mkNode(
371	60	AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2));
372		}
373		else
374		{
375		// 0 <= var < pi
376	12	rlem = nm->mkNode(AND,
377	8	nm->mkNode(LEQ, nm->mkConst(Rational(0)), var),
378	8	nm->mkNode(LT, var, pi));
379		}
380
381	16	Kind rk =
382		k == ARCSINE
383	28	? SINE
384		: (k == ARCCOSINE
385	20	? COSINE
386		: (k == ARCTANGENT
387	8	? TANGENT
388		: (k == ARCCOSECANT
389		? COSECANT
390		: (k == ARCSECANT ? SECANT : COTANGENT))));
391	32	Node invTerm = nm->mkNode(rk, var);
392	16	lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0]));
393		}
394	56	Assert(!lem.isNull());
395		return mkWitnessTerm(
396		var,
397		lem,
398		"tfk",
399		"Skolem to eliminate a non-standard transcendental function",
400	56	lems);
401		break;
402		}
403
404	432294	default: break;
405		}
406	432294	return node;
407		}
408
409		Node OperatorElim::getAxiomFor(Node n) { return Node::null(); }
410
411	568	Node OperatorElim::getArithSkolem(SkolemFunId id)
412		{
413	568	std::map<SkolemFunId, Node>::iterator it = d_arithSkolem.find(id);
414	568	if (it == d_arithSkolem.end())
415		{
416	266	NodeManager* nm = NodeManager::currentNM();
417	532	TypeNode tn;
418	266	if (id == SkolemFunId::DIV_BY_ZERO \|\| id == SkolemFunId::SQRT)
419		{
420	135	tn = nm->realType();
421		}
422		else
423		{
424	131	tn = nm->integerType();
425		}
426	532	Node skolem;
427	266	SkolemManager* sm = nm->getSkolemManager();
428	266	if (options().arith.arithNoPartialFun)
429		{
430		// partial function: division, where we treat the skolem function as
431		// a constant
432	4	skolem = sm->mkSkolemFunction(id, tn);
433		}
434		else
435		{
436		// partial function: division
437	262	skolem = sm->mkSkolemFunction(id, nm->mkFunctionType(tn, tn));
438		}
439		// cache it
440	266	d_arithSkolem[id] = skolem;
441	266	return skolem;
442		}
443	302	return it->second;
444		}
445
446	568	Node OperatorElim::getArithSkolemApp(Node n, SkolemFunId id)
447		{
448	568	Node skolem = getArithSkolem(id);
449	568	if (!options().arith.arithNoPartialFun)
450		{
451	560	skolem = NodeManager::currentNM()->mkNode(APPLY_UF, skolem, n);
452		}
453	568	return skolem;
454		}
455
456	1856	Node OperatorElim::mkWitnessTerm(Node v,
457		Node pred,
458		const std::string& prefix,
459		const std::string& comment,
460		std::vector<SkolemLemma>& lems)
461		{
462	1856	NodeManager* nm = NodeManager::currentNM();
463	1856	SkolemManager* sm = nm->getSkolemManager();
464		// we mark that we should send a lemma
465		Node k = sm->mkSkolem(
466	1856	v, pred, prefix, comment, SkolemManager::SKOLEM_DEFAULT, this);
467	1856	if (d_pnm != nullptr)
468		{
469	1680	Node lem = SkolemLemma::getSkolemLemmaFor(k);
470		TrustNode tlem =
471	1680	mkTrustNode(lem, PfRule::THEORY_PREPROCESS_LEMMA, {}, {lem});
472	840	lems.push_back(SkolemLemma(tlem, k));
473		}
474		else
475		{
476	1016	lems.push_back(SkolemLemma(k, nullptr));
477		}
478	1856	return k;
479		}
480
481		} // namespace arith
482		} // namespace theory
483	31137	} // namespace cvc5