diff options
| -rw-r--r-- | docs/_static/custom.css | 5 | ||||
| -rw-r--r-- | docs/references.bib | 20 | ||||
| -rw-r--r-- | docs/theories/transcendentals.rst | 55 | ||||
| -rw-r--r-- | docs/theory.rst | 1 | ||||
| -rw-r--r-- | examples/api/cpp/CMakeLists.txt | 5 | ||||
| -rw-r--r-- | examples/api/cpp/transcendentals.cpp | 54 | ||||
| -rw-r--r-- | examples/api/python/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | examples/api/python/transcendentals.py | 47 | ||||
| -rw-r--r-- | examples/api/smtlib/transcendentals.smt2 | 8 |
9 files changed, 195 insertions, 3 deletions
diff --git a/docs/_static/custom.css b/docs/_static/custom.css index 9d07edeaf..6934d7017 100644 --- a/docs/_static/custom.css +++ b/docs/_static/custom.css @@ -88,6 +88,11 @@ a:hover, a:focus { 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; diff --git a/docs/references.bib b/docs/references.bib index 8e3fd5e69..12eecc8ba 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -1,3 +1,23 @@ +@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)}, diff --git a/docs/theories/transcendentals.rst b/docs/theories/transcendentals.rst new file mode 100644 index 000000000..cf52b0889 --- /dev/null +++ b/docs/theories/transcendentals.rst @@ -0,0 +1,55 @@ +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 diff --git a/docs/theory.rst b/docs/theory.rst index 2d2a949d5..075de8ba4 100644 --- a/docs/theory.rst +++ b/docs/theory.rst @@ -7,3 +7,4 @@ Theory References theories/datatypes theories/separation-logic theories/sets-and-relations + theories/transcendentals diff --git a/examples/api/cpp/CMakeLists.txt b/examples/api/cpp/CMakeLists.txt index 6f66fdc5f..b33dd3e13 100644 --- a/examples/api/cpp/CMakeLists.txt +++ b/examples/api/cpp/CMakeLists.txt @@ -21,10 +21,11 @@ set(CVC5_EXAMPLES_API extract helloworld linear_arith - sets + quickstart sequences + sets strings - quickstart + transcendentals ) foreach(example ${CVC5_EXAMPLES_API}) diff --git a/examples/api/cpp/transcendentals.cpp b/examples/api/cpp/transcendentals.cpp new file mode 100644 index 000000000..a9a3ce681 --- /dev/null +++ b/examples/api/cpp/transcendentals.cpp @@ -0,0 +1,54 @@ +/****************************************************************************** + * 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; +} diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt index ec4154f4f..426eb0d3d 100644 --- a/examples/api/python/CMakeLists.txt +++ b/examples/api/python/CMakeLists.txt @@ -22,6 +22,7 @@ set(EXAMPLES_API_PYTHON extract floating_point helloworld + id linear_arith sequences sets @@ -29,7 +30,7 @@ set(EXAMPLES_API_PYTHON sygus-fun sygus-grammar sygus-inv - id + transcendentals ) find_package(PythonInterp ${CVC5_BINDINGS_PYTHON_VERSION} REQUIRED) diff --git a/examples/api/python/transcendentals.py b/examples/api/python/transcendentals.py new file mode 100644 index 000000000..39bb343c7 --- /dev/null +++ b/examples/api/python/transcendentals.py @@ -0,0 +1,47 @@ +#!/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()) diff --git a/examples/api/smtlib/transcendentals.smt2 b/examples/api/smtlib/transcendentals.smt2 new file mode 100644 index 000000000..b9d6d41d2 --- /dev/null +++ b/examples/api/smtlib/transcendentals.smt2 @@ -0,0 +1,8 @@ +(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) |