From 705f59a117d1ce89b09a6eb16dc61ea31d98bddd Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Tue, 29 Mar 2022 13:31:24 -0700 Subject: [PATCH 1/4] More examples, added transcendentals --- cvc5_z3py_compat/z3.py | 143 ++++++++++++++++++ cvc5_z3py_compat/z3printer.py | 19 ++- test/pgm_outputs/example_exceptions.py.out | 0 test/pgm_outputs/example_id.py.out | 0 .../example_transcendentals.py.out | 1 + test/pgms/example_exceptions.py | 23 +++ test/pgms/example_id.py | 12 ++ test/pgms/example_transcendentals.py | 7 + 8 files changed, 203 insertions(+), 2 deletions(-) create mode 100644 test/pgm_outputs/example_exceptions.py.out create mode 100644 test/pgm_outputs/example_id.py.out create mode 100644 test/pgm_outputs/example_transcendentals.py.out create mode 100644 test/pgms/example_exceptions.py create mode 100644 test/pgms/example_id.py create mode 100644 test/pgms/example_transcendentals.py diff --git a/cvc5_z3py_compat/z3.py b/cvc5_z3py_compat/z3.py index 7006799..04fff5b 100644 --- a/cvc5_z3py_compat/z3.py +++ b/cvc5_z3py_compat/z3.py @@ -3057,6 +3057,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 a sine function + + >>> Arcsine(Real('x')) + Arcsine(x) + """ + return _nary_kind_builder(Kind.Arcsine, RealSort().cast(x)) + + +def Arccosine(x): + """ Create a cosine function + + >>> Arccosine(Real('x')) + Arccosine(x) + """ + return _nary_kind_builder(Kind.Arccosine, RealSort().cast(x)) + + +def Arctangent(x): + """ Create a tangent 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 a secant function + + >>> Arcsecant(Real('x')) + Arcsecant(x) + """ + return _nary_kind_builder(Kind.Arcsecant, RealSort().cast(x)) + + +def Arccosecant(x): + """ Create a cosecant function + + >>> Arccosecant(Real('x')) + Arccosecant(x) + """ + return _nary_kind_builder(Kind.Arccosecant, RealSort().cast(x)) + + +def Arccotangent(x): + """ Create a cotangent function + + >>> Arccotangent(Real('x')) + Arccotangent(x) + """ + return _nary_kind_builder(Kind.Arccotangent, RealSort().cast(x)) + + ######################################### # # Bit-Vectors diff --git a/cvc5_z3py_compat/z3printer.py b/cvc5_z3py_compat/z3printer.py index c157bdc..c4fb30b 100644 --- a/cvc5_z3py_compat/z3printer.py +++ b/cvc5_z3py_compat/z3printer.py @@ -122,6 +122,21 @@ def _assert(cond, msg): Kind.FPIsSubnormal: "fpIsMinusnormal", Kind.FPIsNeg: "fpIsNegative", Kind.FPIsPos: "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 = _z3_op_to_str.get(k, None) if n is None: - if k in [Kind.Constant, Kind.ConstFP, Kind.ConstRoundingmode, Kind.Variable, Kind.UninterpretedSortValue]: + if k in [Kind.Constant, Kind.ConstFP, Kind.ConstRoundingmode, Kind.Variable, Kind.UninterpretedSortValue, Kind.Pi]: return str(a.ast) if k == Kind.InternalKind: # Hack to handle DT selectors and constructors @@ -1117,7 +1132,7 @@ def pp_app(self, a, d, xs): elif k == Kind.ConstArray: return self.pp_K(a, d, xs) # Slight hack to handle DT fns here (InternalKind case). - elif k in [Kind.Constant, Kind.InternalKind, Kind.Variable, Kind.UninterpretedSortValue]: + elif k in [Kind.Constant, Kind.InternalKind, Kind.Variable, Kind.UninterpretedSortValue, Kind.Pi]: return self.pp_name(a) # elif k == Z3_OP_PB_AT_MOST: # return self.pp_atmost(a, d, f, xs) diff --git a/test/pgm_outputs/example_exceptions.py.out b/test/pgm_outputs/example_exceptions.py.out new file mode 100644 index 0000000..e69de29 diff --git a/test/pgm_outputs/example_id.py.out b/test/pgm_outputs/example_id.py.out new file mode 100644 index 0000000..e69de29 diff --git a/test/pgm_outputs/example_transcendentals.py.out b/test/pgm_outputs/example_transcendentals.py.out new file mode 100644 index 0000000..f5a4390 --- /dev/null +++ b/test/pgm_outputs/example_transcendentals.py.out @@ -0,0 +1 @@ +no solution diff --git a/test/pgms/example_exceptions.py b/test/pgms/example_exceptions.py new file mode 100644 index 0000000..d8c758a --- /dev/null +++ b/test/pgms/example_exceptions.py @@ -0,0 +1,23 @@ +from cvc5_z3py_compat 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 diff --git a/test/pgms/example_id.py b/test/pgms/example_id.py new file mode 100644 index 0000000..26158b2 --- /dev/null +++ b/test/pgms/example_id.py @@ -0,0 +1,12 @@ +from cvc5_z3py_compat 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() diff --git a/test/pgms/example_transcendentals.py b/test/pgms/example_transcendentals.py new file mode 100644 index 0000000..00b495f --- /dev/null +++ b/test/pgms/example_transcendentals.py @@ -0,0 +1,7 @@ +from cvc5_z3py_compat import * + +if __name__ == '__main__': + x, y = Reals("x y") + solve(x > Pi(), + x < 2 * Pi(), + y ** 2 < Sine(x)) From 3fd7b647714c88e6437d907d309acf8a5c9126b2 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Tue, 29 Mar 2022 13:38:33 -0700 Subject: [PATCH 2/4] fix doc --- cvc5_z3py_compat/z3.py | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/cvc5_z3py_compat/z3.py b/cvc5_z3py_compat/z3.py index 04fff5b..acb9699 100644 --- a/cvc5_z3py_compat/z3.py +++ b/cvc5_z3py_compat/z3.py @@ -3120,7 +3120,7 @@ def Tangent(x): def Arcsine(x): - """ Create a sine function + """ Create an arcsine function >>> Arcsine(Real('x')) Arcsine(x) @@ -3129,7 +3129,7 @@ def Arcsine(x): def Arccosine(x): - """ Create a cosine function + """ Create an arccosine function >>> Arccosine(Real('x')) Arccosine(x) @@ -3138,7 +3138,7 @@ def Arccosine(x): def Arctangent(x): - """ Create a tangent function + """ Create an arctangent function >>> Arctangent(Real('x')) Arctangent(x) @@ -3174,7 +3174,7 @@ def Cotangent(x): def Arcsecant(x): - """ Create a secant function + """ Create an arcsecant function >>> Arcsecant(Real('x')) Arcsecant(x) @@ -3183,7 +3183,7 @@ def Arcsecant(x): def Arccosecant(x): - """ Create a cosecant function + """ Create an arccosecant function >>> Arccosecant(Real('x')) Arccosecant(x) @@ -3192,7 +3192,7 @@ def Arccosecant(x): def Arccotangent(x): - """ Create a cotangent function + """ Create an arccotangent function >>> Arccotangent(Real('x')) Arccotangent(x) From 5525e35d71a949e0b9b17baeacfd6f5ab62e7c99 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Mon, 4 Apr 2022 09:54:38 -0700 Subject: [PATCH 3/4] fix tests --- cvc5_pythonic_api/cvc5_pythonic.py | 38 ++++++++++++++-------------- test/pgms/example_exceptions.py | 2 +- test/pgms/example_id.py | 2 +- test/pgms/example_transcendentals.py | 2 +- 4 files changed, 22 insertions(+), 22 deletions(-) diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py index 8bc1ef6..13ca94b 100644 --- a/cvc5_pythonic_api/cvc5_pythonic.py +++ b/cvc5_pythonic_api/cvc5_pythonic.py @@ -3077,7 +3077,7 @@ def Pi(ctx=None): Pi """ ctx = get_ctx(ctx) - return _to_expr_ref(ctx.solver.mkTerm(Kind.Pi, []), ctx) + return _to_expr_ref(ctx.solver.mkTerm(Kind.PI), ctx) def Exponential(x): @@ -3087,7 +3087,7 @@ def Exponential(x): >>> solve(Exponential(x) == 1) [x = 0] """ - return _nary_kind_builder(Kind.Exponential, RealSort().cast(x)) + return _nary_kind_builder(Kind.EXPONENTIAL, RealSort().cast(x)) def Sine(x): @@ -3100,7 +3100,7 @@ def Sine(x): >>> prove(Sine(i) < 2) proved """ - return _nary_kind_builder(Kind.Sine, RealSort().cast(x)) + return _nary_kind_builder(Kind.SINE, RealSort().cast(x)) def Cosine(x): @@ -3113,7 +3113,7 @@ def Cosine(x): >>> prove(Cosine(i) < 2) proved """ - return _nary_kind_builder(Kind.Cosine, RealSort().cast(x)) + return _nary_kind_builder(Kind.COSINE, RealSort().cast(x)) def Tangent(x): @@ -3122,7 +3122,7 @@ def Tangent(x): >>> Tangent(Real('x')) Tangent(x) """ - return _nary_kind_builder(Kind.Tangent, RealSort().cast(x)) + return _nary_kind_builder(Kind.TANGENT, RealSort().cast(x)) def Arcsine(x): @@ -3131,7 +3131,7 @@ def Arcsine(x): >>> Arcsine(Real('x')) Arcsine(x) """ - return _nary_kind_builder(Kind.Arcsine, RealSort().cast(x)) + return _nary_kind_builder(Kind.ARCSINE, RealSort().cast(x)) def Arccosine(x): @@ -3140,7 +3140,7 @@ def Arccosine(x): >>> Arccosine(Real('x')) Arccosine(x) """ - return _nary_kind_builder(Kind.Arccosine, RealSort().cast(x)) + return _nary_kind_builder(Kind.ARCCOSINE, RealSort().cast(x)) def Arctangent(x): @@ -3149,7 +3149,7 @@ def Arctangent(x): >>> Arctangent(Real('x')) Arctangent(x) """ - return _nary_kind_builder(Kind.Arctangent, RealSort().cast(x)) + return _nary_kind_builder(Kind.ARCTANGENT, RealSort().cast(x)) def Secant(x): @@ -3158,7 +3158,7 @@ def Secant(x): >>> Secant(Real('x')) Secant(x) """ - return _nary_kind_builder(Kind.Secant, RealSort().cast(x)) + return _nary_kind_builder(Kind.SECANT, RealSort().cast(x)) def Cosecant(x): @@ -3167,7 +3167,7 @@ def Cosecant(x): >>> Cosecant(Real('x')) Cosecant(x) """ - return _nary_kind_builder(Kind.Cosecant, RealSort().cast(x)) + return _nary_kind_builder(Kind.COSECANT, RealSort().cast(x)) def Cotangent(x): @@ -3176,7 +3176,7 @@ def Cotangent(x): >>> Cotangent(Real('x')) Cotangent(x) """ - return _nary_kind_builder(Kind.Cotangent, RealSort().cast(x)) + return _nary_kind_builder(Kind.COTANGENT, RealSort().cast(x)) def Arcsecant(x): @@ -3185,7 +3185,7 @@ def Arcsecant(x): >>> Arcsecant(Real('x')) Arcsecant(x) """ - return _nary_kind_builder(Kind.Arcsecant, RealSort().cast(x)) + return _nary_kind_builder(Kind.ARCSECANT, RealSort().cast(x)) def Arccosecant(x): @@ -3194,7 +3194,7 @@ def Arccosecant(x): >>> Arccosecant(Real('x')) Arccosecant(x) """ - return _nary_kind_builder(Kind.Arccosecant, RealSort().cast(x)) + return _nary_kind_builder(Kind.ARCCOSECANT, RealSort().cast(x)) def Arccotangent(x): @@ -3203,7 +3203,7 @@ def Arccotangent(x): >>> Arccotangent(Real('x')) Arccotangent(x) """ - return _nary_kind_builder(Kind.Arccotangent, RealSort().cast(x)) + return _nary_kind_builder(Kind.ARCCOTANGENT, RealSort().cast(x)) ######################################### @@ -7035,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): @@ -7681,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): @@ -7754,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): diff --git a/test/pgms/example_exceptions.py b/test/pgms/example_exceptions.py index d8c758a..6800db7 100644 --- a/test/pgms/example_exceptions.py +++ b/test/pgms/example_exceptions.py @@ -1,4 +1,4 @@ -from cvc5_z3py_compat import * +from cvc5_pythonic_api import * if __name__ == '__main__': s = Solver() diff --git a/test/pgms/example_id.py b/test/pgms/example_id.py index 26158b2..bc365b2 100644 --- a/test/pgms/example_id.py +++ b/test/pgms/example_id.py @@ -1,4 +1,4 @@ -from cvc5_z3py_compat import * +from cvc5_pythonic_api import * if __name__ == '__main__': A = Set("A", SetSort(IntSort())) diff --git a/test/pgms/example_transcendentals.py b/test/pgms/example_transcendentals.py index 00b495f..f7e5a67 100644 --- a/test/pgms/example_transcendentals.py +++ b/test/pgms/example_transcendentals.py @@ -1,4 +1,4 @@ -from cvc5_z3py_compat import * +from cvc5_pythonic_api import * if __name__ == '__main__': x, y = Reals("x y") From fc431274c0b5ad6c9cf6cac8d18a8c5f971cc26a Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Mon, 4 Apr 2022 10:22:27 -0700 Subject: [PATCH 4/4] Apply suggestions from code review Co-authored-by: Gereon Kremer --- test/pgms/example_exceptions.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/pgms/example_exceptions.py b/test/pgms/example_exceptions.py index 6800db7..39ec33c 100644 --- a/test/pgms/example_exceptions.py +++ b/test/pgms/example_exceptions.py @@ -2,10 +2,10 @@ if __name__ == '__main__': s = Solver() - s.set(**{"produce-models": "true"}) + s.set("produce-models", True) try: # invalid option - s.set(**{"non-existing-option": "true"}) + s.set("non-existing-option", True) except: pass