diff options
| author | makaimann <makaim@stanford.edu> | 2020-06-04 15:18:35 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-04 15:18:35 -0700 |
| commit | 6c608754e8058098e410e208d0b6cc0f586b79ca (patch) | |
| tree | 6e1f58c09e6dd08eab04ec43acebd796d7cf8c99 /examples/api/python/bitvectors.py | |
| parent | f0169b253759632aee0d21db916fe68702c66116 (diff) | |
Wrap Result in Python API (#4473)
This PR would change the Python API to wrap the C++ Result class instead of translating it to a pure Python class. This is more convenient because there are several possibilities other than sat/unsat/unknown. Furthermore, this PR updates the bitvectors.py example which had an incorrect function name "checkEntailment" and adds a floating point example contributed by Eva Darulova.
Diffstat (limited to 'examples/api/python/bitvectors.py')
| -rwxr-xr-x | examples/api/python/bitvectors.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py index 8e4e1b682..f12e79541 100755 --- a/examples/api/python/bitvectors.py +++ b/examples/api/python/bitvectors.py @@ -84,7 +84,7 @@ if __name__ == "__main__": print("Checking entailment assuming:", new_x_eq_new_x_) print("Expect ENTAILED.") - print("CVC4:", slv.checkEntailment(new_x_eq_new_x_)) + print("CVC4:", slv.checkEntailed(new_x_eq_new_x_)) print("Popping context.") slv.pop() |