Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/operator_elim.cpp	Lines:	182	195	93.3 %
Date:	2021-09-07	Branches:	487	984	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/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(ProofNodeManager* pnm, const LogicInfo& info)
    : EagerProofGenerator(pnm), d_info(info)
{
}

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