Skip to content

Commit

Permalink
Rename z3 to pythonic api (#80)
Browse files Browse the repository at this point in the history
A lot of the naming still suggests that this is somehow part of z3. While we incorporate code from z3 (and still acknowledge this), we now call everything cvc5_pythonic_api.
  • Loading branch information
nafur authored Apr 2, 2022
1 parent cbc2e18 commit a35b49e
Show file tree
Hide file tree
Showing 26 changed files with 78 additions and 119 deletions.
8 changes: 4 additions & 4 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -29,8 +29,8 @@ jobs:
uses: actions/cache@v2
with:
path: ccache-dir
key: cvc5-z3py-compat-ccache-${{ github.sha }}
restore-keys: cvc5-z3py-compat-ccache-
key: cvc5-pythonic-api-ccache-${{ github.sha }}
restore-keys: cvc5-pythonic-api-ccache-

- name: Configure ccache
shell: bash
Expand All @@ -45,7 +45,7 @@ jobs:
uses: actions/cache@v2
with:
path: cvc5/build/deps
key: cvc5-z3py-compat-deps-${{ hashFiles('cvc5/cmake/**') }}-${{ hashFiles('.github/**') }}
key: cvc5-pythonic-api-deps-${{ hashFiles('cvc5/cmake/**') }}-${{ hashFiles('.github/**') }}

- name: Build cvc5
run: |
Expand All @@ -54,7 +54,7 @@ jobs:
cd build/
make -j${{ env.num_proc }}
- name: Test z3py compatibility API
- name: Test cvc5 pythonic API
run: |
make test
env:
Expand Down
6 changes: 3 additions & 3 deletions LICENSE.txt
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
cvc5_z3py_compat is copyright (C) 2021 by its authors and contributors and
cvc5_pythonic_api is copyright (C) 2021 by its authors and contributors and
their institutional affiliations. All rights reserved.

The source code of cvc5_z3py_compat is open and available to students,
The source code of cvc5_pythonic_api is open and available to students,
researchers, software companies, and everyone else to study, to modify, and to
redistribute original or modified versions; distribution is under the terms of
the modified BSD license (reproduced below). Note that the underlying
software, cvc5, includes it own license and restrictions. See
https://github.com/cvc5/cvc5 for details. Note that cvc5_z3py_compat includes
https://github.com/cvc5/cvc5 for details. Note that cvc5_pythonic_api includes
source from Z3Py; see `license/z3.txt` for its license.

Redistribution and use in source and binary forms, with or without
Expand Down
8 changes: 4 additions & 4 deletions Makefile
Original file line number Diff line number Diff line change
@@ -1,13 +1,13 @@
.PHONY: test check fmt coverage

test:
./z3doc_test.py && ./z3test.py
./test_doc.py && ./test_unit.py

check:
pyright ./cvc5_z3py_compat
pyright ./cvc5_pythonic_api

fmt:
black ./cvc5_z3py_compat
black ./cvc5_pythonic_api

coverage:
coverage run z3test.py && coverage report && coverage html
coverage run test_unit.py && coverage report && coverage html
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# cvc5's Z3Py compatibility layer
# cvc5's pythonic API

## Development requirements

Expand Down
File renamed without changes.
1 change: 1 addition & 0 deletions cvc5_pythonic_api/__init__.py
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
from .cvc5_pythonic import *
20 changes: 10 additions & 10 deletions cvc5_z3py_compat/z3.py → cvc5_pythonic_api/cvc5_pythonic.py
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@
"""
cvc5 is an SMT solver.
This is its (as much as possible) Z3-compatible python interface.
This is its pythonic API that is (as much as possible) Z3-compatible.
Several online tutorials for Z3Py are available at:
http://rise4fun.com/Z3Py/tutorial/guide
Expand Down Expand Up @@ -68,7 +68,7 @@
* as expected
* Some pretty printing
"""
from .z3printer import *
from .cvc5_pythonic_printer import *
from fractions import Fraction
from decimal import Decimal
import ctypes
Expand Down Expand Up @@ -7060,7 +7060,7 @@ def fpToFP(a1, a2=None, a3=None, ctx=None):
elif is_fprm(a1) and is_bv(a2) and is_fp_sort(a3):
return fpSignedToFP(a1, a2, a3, ctx)
else:
raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.")
raise SMTException("Unsupported combination of arguments for conversion to floating-point term.")


def fpBVToFP(v, sort, ctx=None):
Expand Down Expand Up @@ -7250,13 +7250,13 @@ def _valid_accessor(acc):


class Datatype:
"""Helper class for declaring Z3 datatypes.
"""Helper class for declaring datatypes.
>>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> # List is now a Z3 declaration
>>> # List is now a declaration
>>> List.nil
nil
>>> List.cons(10, List.nil)
Expand Down Expand Up @@ -7413,7 +7413,7 @@ def CreateDatatypes(*ds):
ftype = uninterp_sorts[ftype.name]
else:
if debugging():
_assert(is_sort(ftype), "Z3 sort expected")
_assert(is_sort(ftype), "sort expected")
ftype = ftype.ast
con.addSelector(fname, ftype)
decl.addConstructor(con)
Expand Down Expand Up @@ -7447,13 +7447,13 @@ def __init__(self, ast, ctx=None):
self.dt = ast.getDatatype()

def num_constructors(self):
"""Return the number of constructors in the given Z3 datatype.
"""Return the number of constructors in the given datatype.
>>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> # List is now a Z3 declaration
>>> # List is now a declaration
>>> List.num_constructors()
2
"""
Expand All @@ -7466,7 +7466,7 @@ def constructor(self, idx):
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> # List is now a Z3 declaration
>>> # List is now a declaration
>>> List.num_constructors()
2
>>> List.constructor(0)
Expand Down Expand Up @@ -7703,7 +7703,7 @@ class DatatypeRef(ExprRef):

def sort(self):
"""Return the datatype sort of the datatype expression `self`."""
return DatatypeSortRef(self.as_ast(), self.ctx)
return DatatypeSortRef(self.as_ast().getSort(), self.ctx)


def TupleSort(name, sorts, ctx=None):
Expand Down
Loading

0 comments on commit a35b49e

Please sign in to comment.