diff options
author | Gereon Kremer <nafur42@gmail.com> | 2021-07-06 04:13:47 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-07-05 21:13:47 -0500 |
commit | 898f11d0945bdaaa8bb79a536b66b266c78f1daa (patch) | |
tree | 308af61986c14fb79d3d67ba56b9f929f02d04ec /examples | |
parent | adf5216eff4e75dd9c5d08fce3bfc2161250c86e (diff) |
Add doc page about transcendentals (#6755)
This PR adds a theory reference page for the transcendental extension.
Diffstat (limited to 'examples')
-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 |
5 files changed, 114 insertions, 3 deletions
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) |