diff options
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))) |