This PR adds a theory reference page for the transcendental extension.
color: #ba2121;
}
+/* Removes margin of code blocks within tabs */
+.sphinx-tabs-panel div[class^="highlight"] {
+ margin: 1px 0 0 0;
+}
+
#c-api-class-hierarchy code {
font-size: 100%;
font-weight: normal;
+@article{DBLP:journals/tocl/CimattiGIRS18,
+ author = {Alessandro Cimatti and
+ Alberto Griggio and
+ Ahmed Irfan and
+ Marco Roveri and
+ Roberto Sebastiani},
+ title = {Incremental Linearization for Satisfiability and Verification Modulo
+ Nonlinear Arithmetic and Transcendental Functions},
+ journal = {{ACM} Trans. Comput. Log.},
+ volume = {19},
+ number = {3},
+ pages = {19:1--19:52},
+ year = {2018},
+ doi = {10.1145/3230639},
+ timestamp = {Fri, 09 Apr 2021 18:33:35 +0200},
+ biburl = {https://dblp.org/rec/journals/tocl/CimattiGIRS18.bib},
+ bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+
@article{IEEE754,
author={IEEE},
journal={IEEE Std 754-2019 (Revision of IEEE 754-2008)},
--- /dev/null
+Theory Reference: Transcendentals
+=================================
+
+cvc5 supports transcendental functions that naturally extend the nonlinear real arithmetic theories ``NRA`` and ``NIRA``.
+The theory consists of the constant :math:`\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:
+
+.. code:: smtlib
+
+ (set-logic QF_NRAT)
+
+Alternatively, use the ``ALL`` logic:
+
+.. code:: smtlib
+
+ (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 :cite:`DBLP:journals/tocl/CimattiGIRS18`.
+
+Examples
+--------
+
+.. api-examples::
+ ../../examples/api/cpp/transcendentals.cpp
+ ../../examples/api/python/transcendentals.py
+ ../../examples/api/smtlib/transcendentals.smt2
\ No newline at end of file
theories/datatypes
theories/separation-logic
theories/sets-and-relations
+ theories/transcendentals
extract
helloworld
linear_arith
- sets
+ quickstart
sequences
+ sets
strings
- quickstart
+ transcendentals
)
foreach(example ${CVC5_EXAMPLES_API})
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Aina Niemetz, Tim King, Mudathir Mohamed
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * A simple demonstration of the transcendental extension.
+ */
+
+#include <iostream>
+
+#include <cvc5/cvc5.h>
+
+using namespace std;
+using namespace cvc5::api;
+
+int main()
+{
+ Solver slv;
+ slv.setLogic("QF_NRAT");
+
+ Sort real = slv.getRealSort();
+
+ // Variables
+ Term x = slv.mkConst(real, "x");
+ Term y = slv.mkConst(real, "y");
+
+ // Helper terms
+ Term two = slv.mkReal(2);
+ Term pi = slv.mkPi();
+ Term twopi = slv.mkTerm(MULT, two, pi);
+ Term ysq = slv.mkTerm(MULT, y, y);
+ Term sinx = slv.mkTerm(SINE, x);
+
+ // Formulas
+ Term x_gt_pi = slv.mkTerm(GT, x, pi);
+ Term x_lt_tpi = slv.mkTerm(LT, x, twopi);
+ Term ysq_lt_sinx = slv.mkTerm(LT, ysq, sinx);
+
+ slv.assertFormula(x_gt_pi);
+ slv.assertFormula(x_lt_tpi);
+ slv.assertFormula(ysq_lt_sinx);
+
+ cout << "cvc5 should report UNSAT." << endl;
+ cout << "Result from cvc5 is: " << slv.checkSat() << endl;
+
+ return 0;
+}
extract
floating_point
helloworld
+ id
linear_arith
sequences
sets
sygus-fun
sygus-grammar
sygus-inv
- id
+ transcendentals
)
find_package(PythonInterp ${CVC5_BINDINGS_PYTHON_VERSION} REQUIRED)
--- /dev/null
+#!/usr/bin/env python
+###############################################################################
+# Top contributors (to current version):
+# Makai Mann, Mudathir Mohamed, Aina Niemetz
+#
+# 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.
+# #############################################################################
+#
+# A simple demonstration of the transcendental extension.
+##
+
+import pycvc5
+from pycvc5 import kinds
+
+if __name__ == "__main__":
+ slv = pycvc5.Solver()
+ slv.setLogic("QF_NRAT")
+
+ real = slv.getRealSort()
+
+ # Variables
+ x = slv.mkConst(real, "x")
+ y = slv.mkConst(real, "y")
+
+ # Helper terms
+ two = slv.mkReal(2)
+ pi = slv.mkPi()
+ twopi = slv.mkTerm(kinds.Mult, two, pi)
+ ysq = slv.mkTerm(kinds.Mult, y, y)
+ sinx = slv.mkTerm(kinds.Sine, x)
+
+ # Formulas
+ x_gt_pi = slv.mkTerm(kinds.Gt, x, pi)
+ x_lt_tpi = slv.mkTerm(kinds.Lt, x, twopi)
+ ysq_lt_sinx = slv.mkTerm(kinds.Lt, ysq, sinx)
+
+ slv.assertFormula(x_gt_pi)
+ slv.assertFormula(x_lt_tpi)
+ slv.assertFormula(ysq_lt_sinx)
+
+ print("cvc5 should report UNSAT")
+ print("Result from cvc5 is:", slv.checkSat())
--- /dev/null
+(set-logic QF_NRAT)
+(declare-fun x () Real)
+(declare-fun y () Real)
+
+(assert (> x real.pi))
+(assert (< x (* 2 real.pi)))
+(assert (< (* y y) (sin x)))
+(check-sat)
projects / cvc5.git / commitdiff