Theory Reference: Transcendentals

cvc5 supports transcendental functions that naturally extend the nonlinear real arithmetic theories NRA and NIRA. The theory consists of the constant \(\pi\) and function symbols for most common transcendental functions like, e.g., sin, cos and tan.

Logic

To enable cvc5’s decision procedure for transcendentals, append T to the arithmetic logic that is being used:

(set-logic QF_NRAT)

Alternatively, use the ALL logic:

(set-logic ALL)

Syntax

cvc5 internally defines a constant real.pi of sort Real and the following unary function symbols from Real to Real:

  • the square root function sqrt

  • the exponential function exp

  • the sine function sin

  • the cosine function cos

  • the tangent function tan

  • the cosecant function csc

  • the secant function sec

  • the cotangent function cot

  • the arcsine function arcsin

  • the arccosine function arccos

  • the arctangent function arctan

  • the arccosecant function arccsc

  • the arcsecant function arcsec

  • the arccotangent function arccot

Semantics

Both the constant real.pi and all function symbols are defined on real numbers and are thus not subject to limited precision. That being said, cvc5 internally uses inexact techniques based on incremental linearization. While real.pi is specified using a rational enclosing interval that is automatically refined on demand, the function symbols are approximated using tangent planes and secant lines using the techniques described in [CGI+18].

Examples

examples/api/cpp/transcendentals.cpp

 1/******************************************************************************
 2 * Top contributors (to current version):
 3 *   Gereon Kremer, Aina Niemetz, Mathias Preiner
 4 *
 5 * This file is part of the cvc5 project.
 6 *
 7 * Copyright (c) 2009-2024 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 * A simple demonstration of the transcendental extension.
14 */
15
16#include <iostream>
17
18#include <cvc5/cvc5.h>
19
20using namespace std;
21using namespace cvc5;
22
23int main()
24{
25  TermManager tm;
26  Solver slv(tm);
27  slv.setLogic("QF_NRAT");
28
29  Sort real = tm.getRealSort();
30
31  // Variables
32  Term x = tm.mkConst(real, "x");
33  Term y = tm.mkConst(real, "y");
34
35  // Helper terms
36  Term two = tm.mkReal(2);
37  Term pi = tm.mkPi();
38  Term twopi = tm.mkTerm(Kind::MULT, {two, pi});
39  Term ysq = tm.mkTerm(Kind::MULT, {y, y});
40  Term sinx = tm.mkTerm(Kind::SINE, {x});
41
42  // Formulas
43  Term x_gt_pi = tm.mkTerm(Kind::GT, {x, pi});
44  Term x_lt_pi = tm.mkTerm(Kind::LT, {x, twopi});
45  Term ysq_lt_sinx = tm.mkTerm(Kind::LT, {ysq, sinx});
46
47  slv.assertFormula(x_gt_pi);
48  slv.assertFormula(x_lt_pi);
49  slv.assertFormula(ysq_lt_sinx);
50
51  cout << "cvc5 should report UNSAT." << endl;
52  cout << "Result from cvc5 is: " << slv.checkSat() << endl;
53
54  return 0;
55}