diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-04-21 10:21:34 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-21 10:21:34 -0700 |
| commit | ae5ee4b07dc3d3c792e7fe7f382ff490dd28aca4 (patch) | |
| tree | a7c2ab8013f46dbea75fcd6e7da3fb83e2012b2f /examples/api/python/sets.py | |
| parent | 86aa9bc35ba9dc9a57913a2ffc71619c7657cc35 (diff) | |
Goodbye CVC4, hello cvc5! (#6371)
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
Diffstat (limited to 'examples/api/python/sets.py')
| -rw-r--r-- | examples/api/python/sets.py | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py index 01c14cb87..b41b2ad5a 100644 --- a/examples/api/python/sets.py +++ b/examples/api/python/sets.py @@ -15,11 +15,11 @@ # through the Python API. This is a direct translation of sets-new.cpp. ## -import pycvc4 -from pycvc4 import kinds +import pycvc5 +from pycvc5 import kinds if __name__ == "__main__": - slv = pycvc4.Solver() + slv = pycvc5.Solver() # Optionally, set the logic. We need at least UF for equality predicate, # integers (LIA) and sets (FS). @@ -48,7 +48,7 @@ if __name__ == "__main__": theorem = slv.mkTerm(kinds.Equal, lhs, rhs) - print("CVC4 reports: {} is {}".format(theorem, + print("cvc5 reports: {} is {}".format(theorem, slv.checkEntailed(theorem))) # Verify emptset is a subset of any set @@ -58,7 +58,7 @@ if __name__ == "__main__": theorem = slv.mkTerm(kinds.Subset, emptyset, A) - print("CVC4 reports: {} is {}".format(theorem, + print("cvc5 reports: {} is {}".format(theorem, slv.checkEntailed(theorem))) # Find me an element in 1, 2 intersection 2, 3, if there is one. @@ -80,7 +80,7 @@ if __name__ == "__main__": result = slv.checkSatAssuming(e) - print("CVC4 reports: {} is {}".format(e, result)) + print("cvc5 reports: {} is {}".format(e, result)) if result: print("For instance, {} is a member".format(slv.getValue(x))) |