More examples & transcendentals (#75)

Co-authored-by: Gereon Kremer <nafur42@gmail.com>

Author: alex-ozdemir

cvc5_pythonic_api/cvc5_pythonic.py

@@ -3063,6 +3063,149 @@ def Gt(a, b):
     return a > b
 
 
+#########################################
+#
+# Transcendentals
+#
+#########################################
+
+
+def Pi(ctx=None):
+    """ Create the constant pi
+
+    >>> Pi()
+    Pi
+    """
+    ctx = get_ctx(ctx)
+    return _to_expr_ref(ctx.solver.mkTerm(Kind.PI), ctx)
+
+
+def Exponential(x):
+    """ Create an exponential function
+
+    >>> x = Real('x')
+    >>> solve(Exponential(x) == 1)
+    [x = 0]
+    """
+    return _nary_kind_builder(Kind.EXPONENTIAL, RealSort().cast(x))
+
+
+def Sine(x):
+    """ Create a sine function
+
+    >>> x = Real('x')
+    >>> i = Int('i')
+    >>> prove(Sine(x) < 2)
+    proved
+    >>> prove(Sine(i) < 2)
+    proved
+    """
+    return _nary_kind_builder(Kind.SINE, RealSort().cast(x))
+
+
+def Cosine(x):
+    """ Create a cosine function
+
+    >>> x = Real('x')
+    >>> i = Int('i')
+    >>> prove(Cosine(x) < 2)
+    proved
+    >>> prove(Cosine(i) < 2)
+    proved
+    """
+    return _nary_kind_builder(Kind.COSINE, RealSort().cast(x))
+
+
+def Tangent(x):
+    """ Create a tangent function
+
+    >>> Tangent(Real('x'))
+    Tangent(x)
+    """
+    return _nary_kind_builder(Kind.TANGENT, RealSort().cast(x))
+
+
+def Arcsine(x):
+    """ Create an arcsine function
+
+    >>> Arcsine(Real('x'))
+    Arcsine(x)
+    """
+    return _nary_kind_builder(Kind.ARCSINE, RealSort().cast(x))
+
+
+def Arccosine(x):
+    """ Create an arccosine function
+
+    >>> Arccosine(Real('x'))
+    Arccosine(x)
+    """
+    return _nary_kind_builder(Kind.ARCCOSINE, RealSort().cast(x))
+
+
+def Arctangent(x):
+    """ Create an arctangent function
+
+    >>> Arctangent(Real('x'))
+    Arctangent(x)
+    """
+    return _nary_kind_builder(Kind.ARCTANGENT, RealSort().cast(x))
+
+
+def Secant(x):
+    """ Create a secant function
+
+    >>> Secant(Real('x'))
+    Secant(x)
+    """
+    return _nary_kind_builder(Kind.SECANT, RealSort().cast(x))
+
+
+def Cosecant(x):
+    """ Create a cosecant function
+
+    >>> Cosecant(Real('x'))
+    Cosecant(x)
+    """
+    return _nary_kind_builder(Kind.COSECANT, RealSort().cast(x))
+
+
+def Cotangent(x):
+    """ Create a cotangent function
+
+    >>> Cotangent(Real('x'))
+    Cotangent(x)
+    """
+    return _nary_kind_builder(Kind.COTANGENT, RealSort().cast(x))
+
+
+def Arcsecant(x):
+    """ Create an arcsecant function
+
+    >>> Arcsecant(Real('x'))
+    Arcsecant(x)
+    """
+    return _nary_kind_builder(Kind.ARCSECANT, RealSort().cast(x))
+
+
+def Arccosecant(x):
+    """ Create an arccosecant function
+
+    >>> Arccosecant(Real('x'))
+    Arccosecant(x)
+    """
+    return _nary_kind_builder(Kind.ARCCOSECANT, RealSort().cast(x))
+
+
+def Arccotangent(x):
+    """ Create an arccotangent function
+
+    >>> Arccotangent(Real('x'))
+    Arccotangent(x)
+    """
+    return _nary_kind_builder(Kind.ARCCOTANGENT, RealSort().cast(x))
+
+
 #########################################
 #
 # Bit-Vectors
@@ -6892,19 +7035,19 @@ def fpIsInf(a, ctx=None):
 def fpIsZero(a, ctx=None):
     """Create a SMT floating-point isZero expression.
     """
-    return _mk_fp_unary_pred(Kind.FPIsZ, a, ctx)
+    return _mk_fp_unary_pred(Kind.FLOATINGPOINT_IS_ZERO, a, ctx)
 
 
 def fpIsNormal(a, ctx=None):
     """Create a SMT floating-point isNormal expression.
     """
-    return _mk_fp_unary_pred(Kind.FPIsN, a, ctx)
+    return _mk_fp_unary_pred(Kind.FLOATINGPOINT_IS_NORMAL, a, ctx)
 
 
 def fpIsSubnormal(a, ctx=None):
     """Create a SMT floating-point isSubnormal expression.
     """
-    return _mk_fp_unary_pred(Kind.FPIsSn, a, ctx)
+    return _mk_fp_unary_pred(Kind.FLOATINGPOINT_IS_SUBNORMAL, a, ctx)
 
 
 def fpIsNegative(a, ctx=None):
@@ -7538,7 +7681,7 @@ def accessor(self, i, j):
 
 class DatatypeConstructorRef(FuncDeclRef):
     def __init__(self, datatype, ctx=None, r=False):
-        super().__init__(datatype.getConstructorTerm(), ctx, r)
+        super().__init__(datatype.getTerm(), ctx, r)
         self.dt = datatype
 
     def arity(self):
@@ -7611,7 +7754,7 @@ def __call__(self, *args):
 
 class DatatypeSelectorRef(FuncDeclRef):
     def __init__(self, datatype, ctx=None, r=False):
-        super().__init__(datatype.getSelectorTerm(), ctx, r)
+        super().__init__(datatype.getTerm(), ctx, r)
         self.dt = datatype
 
     def arity(self):

cvc5_pythonic_api/cvc5_pythonic_printer.py

@@ -122,6 +122,21 @@ def _assert(cond, msg):
     Kind.FLOATINGPOINT_IS_SUBNORMAL: "fpIsMinusnormal",
     Kind.FLOATINGPOINT_IS_NEG: "fpIsNegative",
     Kind.FLOATINGPOINT_IS_POS: "fpIsPositive",
+    # Transcendental
+    Kind.SINE: "Sine",
+    Kind.COSINE: "Cosine",
+    Kind.TANGENT: "Tangent",
+    Kind.SECANT: "Secant",
+    Kind.COSECANT: "Cosecant",
+    Kind.COTANGENT: "Cotangent",
+    Kind.ARCSINE: "Arcsine",
+    Kind.ARCCOSINE: "Arccosine",
+    Kind.ARCTANGENT: "Arctangent",
+    Kind.ARCSECANT: "Arcsecant",
+    Kind.ARCCOSECANT: "Arccosecant",
+    Kind.ARCCOTANGENT: "Arccotangent",
+    Kind.PI: "Pi",
+    Kind.EXPONENTIAL: "Exponential",
 }
 
 # List of infix operators
@@ -346,7 +361,7 @@ def _op_name(a):
     k = a.kind()
     n = _cvc5_kinds_to_str.get(k, None)
     if n is None:
-        if k in [Kind.CONSTANT, Kind.CONST_FLOATINGPOINT, Kind.CONST_ROUNDINGMODE, Kind.VARIABLE, Kind.UNINTERPRETED_SORT_VALUE]:
+        if k in [Kind.CONSTANT, Kind.CONST_FLOATINGPOINT, Kind.CONST_ROUNDINGMODE, Kind.VARIABLE, Kind.UNINTERPRETED_SORT_VALUE, Kind.PI]:
             return str(a.ast)
         if k == Kind.INTERNAL_KIND:
             # Hack to handle DT selectors and constructors
@@ -1088,7 +1103,7 @@ def pp_app(self, a, d, xs):
             elif k == Kind.CONST_ARRAY:
                 return self.pp_K(a, d, xs)
             # Slight hack to handle DT fns here (InternalKind case).
-            elif k in [Kind.CONSTANT, Kind.INTERNAL_KIND, Kind.VARIABLE, Kind.UNINTERPRETED_SORT_VALUE]:
+            elif k in [Kind.CONSTANT, Kind.INTERNAL_KIND, Kind.VARIABLE, Kind.UNINTERPRETED_SORT_VALUE, Kind.PI]:
                 return self.pp_name(a)
             # elif cvc.is_pattern(a):
             #     return self.pp_pattern(a, d, xs)

test/pgm_outputs/example_exceptions.py.out

@@ -0,0 +1 @@
+no solution

test/pgm_outputs/example_id.py.out

@@ -0,0 +1,23 @@
+from cvc5_pythonic_api import *
+
+if __name__ == '__main__':
+    s = Solver()
+    s.set("produce-models", True)
+    try:
+        # invalid option
+        s.set("non-existing-option", True)
+    except:
+        pass
+
+    try:
+        # type error
+        Int("x") + BitVec("a", 5)
+    except:
+        pass
+
+    s += BoolVal(False)
+    s.check()
+    try:
+        s.model()
+    except:
+        pass

test/pgm_outputs/example_transcendentals.py.out

@@ -0,0 +1,12 @@
+from cvc5_pythonic_api import *
+
+if __name__ == '__main__':
+    A = Set("A", SetSort(IntSort()))
+    B = Set("B", SetSort(IntSort()))
+    C = Set("C", SetSort(IntSort()))
+
+    assert A.get_id() != B.get_id()
+    assert C.get_id() != B.get_id()
+    assert A.get_id() == A.get_id()
+    assert B.get_id() == B.get_id()
+    assert C.get_id() == C.get_id()

test/pgms/example_exceptions.py

@@ -0,0 +1,7 @@
+from cvc5_pythonic_api import *
+
+if __name__ == '__main__':
+    x, y = Reals("x y")
+    solve(x > Pi(),
+            x < 2 * Pi(),
+            y ** 2 < Sine(x))