diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b38aa4e..14775b9 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.10.0" - uses: actions/checkout@v2 with: @@ -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 }} 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..e25a0a2 100644 --- a/cvc5_pythonic_api/cvc5_pythonic.py +++ b/cvc5_pythonic_api/cvc5_pythonic.py @@ -52,6 +52,8 @@ * Missing features: * 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 @@ -558,9 +560,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 @@ -1245,8 +1244,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) @@ -1429,6 +1426,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. @@ -1875,8 +1904,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 @@ -2617,8 +2644,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 @@ -4067,8 +4092,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: @@ -5494,7 +5517,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) @@ -6238,12 +6260,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) @@ -6789,13 +6821,36 @@ 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 + """ + if not isinstance(t, ExprRef): + raise TypeError("Can only evaluate `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 @@ -6857,12 +6912,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] @@ -6965,8 +7030,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) @@ -8633,7 +8696,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 @@ -9240,9 +9302,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)