diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-12-14 13:35:53 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-14 13:35:53 -0600 |
| commit | e16ab44a2b4622bb5745633cbafd43a0023a518c (patch) | |
| tree | d980bdc3dc771abfc8101036d1e2aaebc8020134 /test/api/python/sep_log_api.py | |
| parent | ad34df900d79aad64558b354a866870715bfd007 (diff) | |
| parent | effb0d47ba5bfaebae17dcd06153489dccd90eff (diff) | |
Merge branch 'master' into cav22-stringscav22-strings
Diffstat (limited to 'test/api/python/sep_log_api.py')
| -rw-r--r-- | test/api/python/sep_log_api.py | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/test/api/python/sep_log_api.py b/test/api/python/sep_log_api.py index 4e2fbb750..8bbef42fa 100644 --- a/test/api/python/sep_log_api.py +++ b/test/api/python/sep_log_api.py @@ -20,7 +20,7 @@ ## import pycvc5 -from pycvc5 import kinds +from pycvc5 import Kind # Test function to validate that we *cannot* obtain the heap/nil expressions @@ -43,7 +43,7 @@ def validate_exception(): y = slv.mkConst(integer, "y") # y > x - y_gt_x = slv.mkTerm(kinds.Gt, y, x) + y_gt_x = slv.mkTerm(Kind.Gt, y, x) # assert it slv.assertFormula(y_gt_x) @@ -124,18 +124,18 @@ def validate_getters(): p2 = slv.mkConst(integer, "p2") # Constraints on x and y - x_equal_const = slv.mkTerm(kinds.Equal, x, random_constant) - y_gt_x = slv.mkTerm(kinds.Gt, y, x) + x_equal_const = slv.mkTerm(Kind.Equal, x, random_constant) + y_gt_x = slv.mkTerm(Kind.Gt, y, x) # Points-to expressions - p1_to_x = slv.mkTerm(kinds.SepPto, p1, x) - p2_to_y = slv.mkTerm(kinds.SepPto, p2, y) + p1_to_x = slv.mkTerm(Kind.SepPto, p1, x) + p2_to_y = slv.mkTerm(Kind.SepPto, p2, y) # Heap -- the points-to have to be "starred"! - heap = slv.mkTerm(kinds.SepStar, p1_to_x, p2_to_y) + heap = slv.mkTerm(Kind.SepStar, p1_to_x, p2_to_y) # Constain "nil" to be something random - fix_nil = slv.mkTerm(kinds.Equal, nil, expr_nil_val) + fix_nil = slv.mkTerm(Kind.Equal, nil, expr_nil_val) # Add it all to the solver! slv.assertFormula(x_equal_const) @@ -157,11 +157,11 @@ def validate_getters(): nil_expr = slv.getValueSepNil() # If the heap is not a separating conjunction, bail-out - if (heap_expr.getKind() != kinds.SepStar): + if (heap_expr.getKind() != Kind.SepStar): return False # If nil is not a direct equality, bail-out - if (nil_expr.getKind() != kinds.Equal): + if (nil_expr.getKind() != Kind.Equal): return False # Obtain the values for our "pointers" @@ -175,7 +175,7 @@ def validate_getters(): # Walk all the children for child in heap_expr: # If we don't have a PTO operator, bail-out - if (child.getKind() != kinds.SepPto): + if (child.getKind() != Kind.SepPto): return False # Find both sides of the PTO operator |