From ce339d1473201bc0db36b2304c42f27661b11930 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Thu, 12 Dec 2024 10:07:40 -0800 Subject: [PATCH 1/8] fix tests --- .github/workflows/ci.yml | 2 +- Makefile | 4 +-- cvc5_pythonic_api/cvc5_pythonic.py | 44 ++++++++++++++++++++++-------- 3 files changed, 35 insertions(+), 15 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b38aa4e..4aa1ff3 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -18,7 +18,7 @@ jobs: with: options: "--check --verbose" src: "cvc5_pythonic_api" - version: "23.7.0" + version: "24" - uses: actions/checkout@v2 with: diff --git a/Makefile b/Makefile index 6ecca50..cb36a00 100644 --- a/Makefile +++ b/Makefile @@ -7,10 +7,10 @@ check: pyright ./cvc5_pythonic_api fmt: - black --required-version 23.7.0 ./cvc5_pythonic_api + black --required-version 24 ./cvc5_pythonic_api check-fmt: - black --check --verbose --required-version 23.7.0 ./cvc5_pythonic_api + black --check --verbose --required-version 24 ./cvc5_pythonic_api coverage: coverage run test_unit.py && coverage report && coverage html diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py index 8810692..e91c3a0 100644 --- a/cvc5_pythonic_api/cvc5_pythonic.py +++ b/cvc5_pythonic_api/cvc5_pythonic.py @@ -6238,12 +6238,22 @@ def proof(self): [a + 2 == 0, a == 0], (EQ_RESOLVE: False, (ASSUME: a == 0, [a == 0]), - (MACRO_SR_EQ_INTRO: (a == 0) == False, - [a == 0, 7, 12], - (EQ_RESOLVE: a == -2, - (ASSUME: a + 2 == 0, [a + 2 == 0]), - (MACRO_SR_EQ_INTRO: (a + 2 == 0) == (a == -2), - [a + 2 == 0, 7, 12])))))) + (TRANS: (a == 0) == False, + (CONG: (a == 0) == (-2 == 0), + [5], + (EQ_RESOLVE: a == -2, + (ASSUME: a + 2 == 0, [a + 2 == 0]), + (TRANS: (a + 2 == 0) == (a == -2), + (CONG: (a + 2 == 0) == (2 + a == 0), + [5], + (TRUST_THEORY_REWRITE: a + 2 == 2 + a, + [a + 2 == 2 + a, 3, 7]), + (REFL: 0 == 0, [0])), + (TRUST_THEORY_REWRITE: (2 + a == 0) == (a == -2), + [(2 + a == 0) == (a == -2), 3, 7]))), + (REFL: 0 == 0, [0])), + (TRUST_THEORY_REWRITE: (-2 == 0) == False, + [(-2 == 0) == False, 3, 7]))))) """ p = self.solver.getProof()[0] return ProofRef(self, p) @@ -6857,12 +6867,22 @@ def getChildren(self): >>> p (EQ_RESOLVE: False, (ASSUME: a == 0, [a == 0]), - (MACRO_SR_EQ_INTRO: (a == 0) == False, - [a == 0, 7, 12], - (EQ_RESOLVE: a == -2, - (ASSUME: a + 2 == 0, [a + 2 == 0]), - (MACRO_SR_EQ_INTRO: (a + 2 == 0) == (a == -2), - [a + 2 == 0, 7, 12])))) + (TRANS: (a == 0) == False, + (CONG: (a == 0) == (-2 == 0), + [5], + (EQ_RESOLVE: a == -2, + (ASSUME: a + 2 == 0, [a + 2 == 0]), + (TRANS: (a + 2 == 0) == (a == -2), + (CONG: (a + 2 == 0) == (2 + a == 0), + [5], + (TRUST_THEORY_REWRITE: a + 2 == 2 + a, + [a + 2 == 2 + a, 3, 7]), + (REFL: 0 == 0, [0])), + (TRUST_THEORY_REWRITE: (2 + a == 0) == (a == -2), + [(2 + a == 0) == (a == -2), 3, 7]))), + (REFL: 0 == 0, [0])), + (TRUST_THEORY_REWRITE: (-2 == 0) == False, + [(-2 == 0) == False, 3, 7]))) """ children = self.proof.getChildren() return [ProofRef(self.solver, cp) for cp in children] From 3ae864b1bc858482681283825054f1e2839f002c Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Thu, 12 Dec 2024 10:12:23 -0800 Subject: [PATCH 2/8] add bool operator overloads: &, |, ^, ~ --- cvc5_pythonic_api/cvc5_pythonic.py | 32 ++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py index e91c3a0..682c765 100644 --- a/cvc5_pythonic_api/cvc5_pythonic.py +++ b/cvc5_pythonic_api/cvc5_pythonic.py @@ -1429,6 +1429,38 @@ def __mul__(self, other): return 0 return If(self, other, 0) + def __and__(self, other): + """Create the SMT and expression `self & other`. + + >>> solve(Bool("x") & Bool("y")) + [x = True, y = True] + """ + return And(self, other) + + def __or__(self, other): + """Create the SMT or expression `self | other`. + + >>> solve(Bool("x") | Bool("y"), Not(Bool("x"))) + [x = False, y = True] + """ + return Or(self, other) + + def __xor__(self, other): + """Create the SMT xor expression `self ^ other`. + + >>> solve(Bool("x") ^ Bool("y"), Not(Bool("x"))) + [x = False, y = True] + """ + return Xor(self, other) + + def __invert__(self): + """Create the SMT not expression `~self`. + + >>> solve(~Bool("x")) + [x = False] + """ + return Not(self) + def is_bool(a): """Return `True` if `a` is an SMT Boolean expression. From 2e7072dd2ff10cbfabfc6f8613eb00a9a5765afd Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Thu, 12 Dec 2024 10:19:52 -0800 Subject: [PATCH 3/8] document missing Model function --- cvc5_pythonic_api/cvc5_pythonic.py | 1 + 1 file changed, 1 insertion(+) diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py index 682c765..f93137e 100644 --- a/cvc5_pythonic_api/cvc5_pythonic.py +++ b/cvc5_pythonic_api/cvc5_pythonic.py @@ -52,6 +52,7 @@ * Missing features: * Patterns * Models for uninterpreted sorts + * The `Model` function * Pseudo-boolean counting constraints * AtMost, AtLeast, PbLe, PbGe, PbEq * HTML integration From dfc6363147ee0ab6c99e984afde02a9f25329d0f Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Thu, 12 Dec 2024 10:21:42 -0800 Subject: [PATCH 4/8] black version in CI --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4aa1ff3..b736bba 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -18,7 +18,7 @@ jobs: with: options: "--check --verbose" src: "cvc5_pythonic_api" - version: "24" + version: "24.10.0" - uses: actions/checkout@v2 with: From 78883678f096dfde976b33839c5da485e0046653 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Thu, 12 Dec 2024 10:28:46 -0800 Subject: [PATCH 5/8] gpl cvc5 --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b736bba..14775b9 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -56,7 +56,7 @@ jobs: - name: Build cvc5 run: | cd cvc5/ - ./configure.sh production --auto-download --python-bindings --cocoa + ./configure.sh production --auto-download --python-bindings --cocoa --gpl cd build/ make -j${{ env.num_proc }} From 4dc6a3e4bec40486aff3c925ff7aa0d85323b3f6 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Thu, 12 Dec 2024 18:36:50 -0800 Subject: [PATCH 6/8] Remove unnecessary context equivalence assertions. Our terms (unlike z3's) are context-free. --- cvc5_pythonic_api/cvc5_pythonic.py | 24 +++++------------------- 1 file changed, 5 insertions(+), 19 deletions(-) diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py index f93137e..f88b31a 100644 --- a/cvc5_pythonic_api/cvc5_pythonic.py +++ b/cvc5_pythonic_api/cvc5_pythonic.py @@ -559,9 +559,6 @@ def _ctx_from_ast_arg_list(args, default_ctx=None): if is_ast(a): if ctx is None: ctx = a.ctx - else: - if debugging(): - _assert(ctx == a.ctx, "Context mismatch") if ctx is None: ctx = default_ctx return ctx @@ -1246,8 +1243,6 @@ def If(a, b, c, ctx=None): s = BoolSort(ctx) a = s.cast(a) b, c = _coerce_exprs(b, c, ctx) - if debugging(): - _assert(a.ctx == b.ctx, "Context mismatch") return _to_expr_ref(ctx.solver.mkTerm(Kind.ITE, a.ast, b.ast, c.ast), ctx) @@ -1908,8 +1903,6 @@ def cast(self, val): String """ if is_expr(val): - if debugging(): - _assert(self.ctx == val.ctx, "Context mismatch") val_s = val.sort() if self.eq(val_s): return val @@ -2650,8 +2643,6 @@ def cast(self, val): failed """ if is_expr(val): - if debugging(): - _assert(self.ctx == val.ctx, "Context mismatch") val_s = val.sort() if self.eq(val_s): return val @@ -4100,8 +4091,6 @@ def cast(self, val): '#b00000000000000000000000000001010' """ if is_expr(val): - if debugging(): - _assert(self.ctx == val.ctx, "Context mismatch") # Idea: use sign_extend if sort of val is a bitvector of smaller size return val else: @@ -5527,7 +5516,6 @@ def ArraySort(*sig): if debugging(): for s in sig: _assert(is_sort(s), "SMT sort expected") - _assert(s.ctx == r.ctx, "Context mismatch") ctx = d.ctx if len(sig) == 2: return ArraySortRef(ctx.solver.mkArraySort(d.ast, r.ast), ctx) @@ -6832,7 +6820,11 @@ def decls(self): def evaluate(t): - """Evaluates the given term (assuming it is constant!)""" + """Evaluates the given term (assuming it is constant!) + + >>> evaluate(evaluate(BitVecVal(1, 8) + BitVecVal(2, 8)) + BitVecVal(3, 8)) + 6 + """ s = Solver() s.check() m = s.model() @@ -7018,8 +7010,6 @@ def cast(self, val): '(fp #b0 #b01111111 #b00000000000000000000000)' """ if is_expr(val): - if debugging(): - _assert(self.ctx == val.ctx, "Context mismatch") return val else: return FPVal(val, None, self, self.ctx) @@ -8686,7 +8676,6 @@ def CreateDatatypes(*ds): _assert( all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes" ) - _assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch") _assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected") ctx = ds[0].ctx s = ctx.solver @@ -9293,9 +9282,6 @@ def cast(self, val): '#f10m31' """ if is_expr(val): - if debugging(): - _assert(self.ctx == val.ctx, "Context mismatch") - # Idea: use sign_extend if sort of val is a bitvector of smaller size return val else: return FiniteFieldVal(val, self) From 78348eb7e17e871d72d788ea5586e2913fc0e9bb Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Fri, 13 Dec 2024 14:37:44 -0800 Subject: [PATCH 7/8] Add DummyModel --- cvc5_pythonic_api/cvc5_pythonic.py | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py index f88b31a..43a536c 100644 --- a/cvc5_pythonic_api/cvc5_pythonic.py +++ b/cvc5_pythonic_api/cvc5_pythonic.py @@ -53,6 +53,7 @@ * Patterns * Models for uninterpreted sorts * The `Model` function + * In our API, this function returns an object whose only method is `evaluate`. * Pseudo-boolean counting constraints * AtMost, AtLeast, PbLe, PbGe, PbEq * HTML integration @@ -6825,12 +6826,31 @@ def evaluate(t): >>> evaluate(evaluate(BitVecVal(1, 8) + BitVecVal(2, 8)) + BitVecVal(3, 8)) 6 """ + if not isinstance(t, ExprRef): + raise TypeError("Can only evaluation `ExprRef`s") s = Solver() s.check() m = s.model() return m[t] +class EmptyModel: + def evaluate(self, t): + return evaluate(t) + + +def Model(ctx=None): + """Return an object for evaluating terms. + + We recommend using the standalone `evaluate` function for this instead, + but we also provide this function and its return object for z3 compatibility. + + >>> Model().evaluate(BitVecVal(1, 8) + BitVecVal(2, 8)) + 3 + """ + return EmptyModel() + + class ProofRef: """A proof tree where every proof reference corresponds to the root step of a proof. The branches of the root step are the From 3013c7972f4df5c0aa1e2b8b8c3d33657ed8f4b8 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Mon, 6 Jan 2025 11:05:45 -0800 Subject: [PATCH 8/8] fix typo; thanks Haniel! --- cvc5_pythonic_api/cvc5_pythonic.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py index 43a536c..e25a0a2 100644 --- a/cvc5_pythonic_api/cvc5_pythonic.py +++ b/cvc5_pythonic_api/cvc5_pythonic.py @@ -6827,7 +6827,7 @@ def evaluate(t): 6 """ if not isinstance(t, ExprRef): - raise TypeError("Can only evaluation `ExprRef`s") + raise TypeError("Can only evaluate `ExprRef`s") s = Solver() s.check() m = s.model()