diff options
Diffstat (limited to 'examples/api/python/combination.py')
| -rw-r--r-- | examples/api/python/combination.py | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py index 990149434..bceb7e738 100644 --- a/examples/api/python/combination.py +++ b/examples/api/python/combination.py @@ -17,7 +17,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind def prefixPrintGetValue(slv, t, level=0): print("slv.getValue({}): {}".format(t, slv.getValue(t))) @@ -51,18 +51,18 @@ if __name__ == "__main__": one = slv.mkInteger(1) # Terms - f_x = slv.mkTerm(kinds.ApplyUf, f, x) - f_y = slv.mkTerm(kinds.ApplyUf, f, y) - sum_ = slv.mkTerm(kinds.Plus, f_x, f_y) - p_0 = slv.mkTerm(kinds.ApplyUf, p, zero) - p_f_y = slv.mkTerm(kinds.ApplyUf, p, f_y) + f_x = slv.mkTerm(Kind.ApplyUf, f, x) + f_y = slv.mkTerm(Kind.ApplyUf, f, y) + sum_ = slv.mkTerm(Kind.Plus, f_x, f_y) + p_0 = slv.mkTerm(Kind.ApplyUf, p, zero) + p_f_y = slv.mkTerm(Kind.ApplyUf, p, f_y) # Construct the assertions - assertions = slv.mkTerm(kinds.And, + assertions = slv.mkTerm(Kind.And, [ - slv.mkTerm(kinds.Leq, zero, f_x), # 0 <= f(x) - slv.mkTerm(kinds.Leq, zero, f_y), # 0 <= f(y) - slv.mkTerm(kinds.Leq, sum_, one), # f(x) + f(y) <= 1 + slv.mkTerm(Kind.Leq, zero, f_x), # 0 <= f(x) + slv.mkTerm(Kind.Leq, zero, f_y), # 0 <= f(y) + slv.mkTerm(Kind.Leq, sum_, one), # f(x) + f(y) <= 1 p_0.notTerm(), # not p(0) p_f_y # p(f(y)) ]) @@ -71,7 +71,7 @@ if __name__ == "__main__": print("Given the following assertions:", assertions, "\n") print("Prove x /= y is entailed.\ncvc5: ", - slv.checkEntailed(slv.mkTerm(kinds.Distinct, x, y)), "\n") + slv.checkEntailed(slv.mkTerm(Kind.Distinct, x, y)), "\n") print("Call checkSat to show that the assertions are satisfiable") print("cvc5:", slv.checkSat(), "\n") |