Add doc page about transcendentals (#6755)

This PR adds a theory reference page for the transcendental extension.

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)