From: yoni206 Date: Wed, 1 Dec 2021 01:38:45 +0000 (+0200) Subject: Translating API tests to Python — part 2 (#7651) X-Git-Tag: cvc5-1.0.0~746 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=24663f1c4baa2d60f27bd72c5654eaab9bd7ce01;p=cvc5.git Translating API tests to Python — part 2 (#7651) This PR translates the remaining cpp API tests to python. --- diff --git a/test/api/python/CMakeLists.txt b/test/api/python/CMakeLists.txt index e58ada545..966cfc06b 100644 --- a/test/api/python/CMakeLists.txt +++ b/test/api/python/CMakeLists.txt @@ -33,3 +33,7 @@ cvc5_add_python_api_test(pyapi_boilerplate boilerplate.py) cvc5_add_python_api_test(pyapi_issue4889 issue4889.py) cvc5_add_python_api_test(pyapi_issue5074 issue5074.py) cvc5_add_python_api_test(pyapi_issue6111 issue6111.py) +cvc5_add_python_api_test(pyapi_proj-issue306 proj-issue306.py) +cvc5_add_python_api_test(pyapi_reset_assertions reset_assertions.py) +cvc5_add_python_api_test(pyapi_sep_log_api sep_log_api.py) +cvc5_add_python_api_test(pyapi_two_solvers two_solvers.py) diff --git a/test/api/python/proj-issue306.py b/test/api/python/proj-issue306.py new file mode 100644 index 000000000..5d84f65b6 --- /dev/null +++ b/test/api/python/proj-issue306.py @@ -0,0 +1,31 @@ +############################################################################## +# Top contributors (to current version): +# Yoni Zohar +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################ +# +## + +import pycvc5 +from pycvc5 import kinds + +slv = pycvc5.Solver() +slv.setOption("check-proofs", "true") +slv.setOption("proof-check", "eager") +s1 = slv.getBooleanSort() +s3 = slv.getStringSort() +t1 = slv.mkConst(s3, "_x0") +t3 = slv.mkConst(s1, "_x2") +t11 = slv.mkString("") +t14 = slv.mkConst(s3, "_x11") +t42 = slv.mkTerm(kinds.Ite, t3, t14, t1) +t58 = slv.mkTerm(kinds.StringLeq, t14, t11) +t95 = slv.mkTerm(kinds.Equal, t14, t42) +slv.assertFormula(t95) +slv.checkSatAssuming([t58]) diff --git a/test/api/python/reset_assertions.py b/test/api/python/reset_assertions.py new file mode 100644 index 000000000..221f1c884 --- /dev/null +++ b/test/api/python/reset_assertions.py @@ -0,0 +1,44 @@ +############################################################################## +# Top contributors (to current version): +# Yoni Zohar +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################ +# +# A simple test for SolverEngine::resetAssertions() +# +# This program indirectly also tests some corner cases w.r.t. +# context-dependent datastructures: resetAssertions() pops the contexts to +# zero but some context-dependent datastructures are created at leevel 1, +# which the datastructure needs to handle properly problematic. +## + +import pycvc5 +from pycvc5 import kinds + +slv = pycvc5.Solver() +slv.setOption("incremental", "true") + +real = slv.getRealSort() +x = slv.mkConst(real, "x") +four = slv.mkInteger(4) +xEqFour = slv.mkTerm(kinds.Equal, x, four) +slv.assertFormula(xEqFour) +print(slv.checkSat()) + +slv.resetAssertions() + +elementType = slv.getIntegerSort() +indexType = slv.getIntegerSort() +arrayType = slv.mkArraySort(indexType, elementType) +array = slv.mkConst(arrayType, "array") +arrayAtFour = slv.mkTerm(kinds.Select, array, four) +ten = slv.mkInteger(10) +arrayAtFour_eq_ten = slv.mkTerm(kinds.Equal, arrayAtFour, ten) +slv.assertFormula(arrayAtFour_eq_ten) +print(slv.checkSat()) diff --git a/test/api/python/sep_log_api.py b/test/api/python/sep_log_api.py new file mode 100644 index 000000000..4e2fbb750 --- /dev/null +++ b/test/api/python/sep_log_api.py @@ -0,0 +1,232 @@ +############################################################################## +# Top contributors (to current version): +# Yoni Zohar +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################ +# +# Two tests to validate the use of the separation logic API. +# +# First test validates that we cannot use the API if not using separation +# logic. +# +# Second test validates that the expressions returned from the API are +# correct and can be interrogated. +## + +import pycvc5 +from pycvc5 import kinds + + +# Test function to validate that we *cannot* obtain the heap/nil expressions +# when *not* using the separation logic theory +def validate_exception(): + slv = pycvc5.Solver() + # Setup some options for cvc5 -- we explictly want to use a simplistic + # theory (e.g., QF_IDL) + slv.setLogic("QF_IDL") + slv.setOption("produce-models", "true") + slv.setOption("incremental", "false") + + # Our integer type + integer = slv.getIntegerSort() + + # we intentionally do not set the separation logic heap + + # Our SMT constants + x = slv.mkConst(integer, "x") + y = slv.mkConst(integer, "y") + + # y > x + y_gt_x = slv.mkTerm(kinds.Gt, y, x) + + # assert it + slv.assertFormula(y_gt_x) + + # check + r = slv.checkSat() + + # If this is UNSAT, we have an issue so bail-out + if not r.isSat(): + return False + + # We now try to obtain our separation logic expressions from the solver -- + # we want to validate that we get our expected exceptions. + + caught_on_heap = False + caught_on_nil = False + + # The exception message we expect to obtain + expected = \ + "Cannot obtain separation logic expressions if not using the separation " \ + "logic theory." + + # test the heap expression + try: + heap_expr = slv.getValueSepHeap() + except RuntimeError as e: + caught_on_heap = True + # Check we get the correct exception string + if str(e) != expected: + return False + + # test the nil expression + try: + nil_expr = slv.getValueSepNil() + except RuntimeError as e: + caught_on_nil = True + + # Check we get the correct exception string + if str(e) != expected: + return False + + if not caught_on_heap or not caught_on_nil: + return False + + # All tests pass! + return True + + +# Test function to demonstrate the use of, and validate the capability, of +# obtaining the heap/nil expressions when using separation logic. +def validate_getters(): + slv = pycvc5.Solver() + + # Setup some options for cvc5 + slv.setLogic("QF_ALL") + slv.setOption("produce-models", "true") + slv.setOption("incremental", "false") + + # Our integer type + integer = slv.getIntegerSort() + + #* Declare the separation logic heap types + slv.declareSepHeap(integer, integer) + + # A "random" constant + random_constant = slv.mkInteger(0xDEAD) + + # Another random constant + expr_nil_val = slv.mkInteger(0xFBAD) + + # Our nil term + nil = slv.mkSepNil(integer) + + # Our SMT constants + x = slv.mkConst(integer, "x") + y = slv.mkConst(integer, "y") + p1 = slv.mkConst(integer, "p1") + 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) + + # Points-to expressions + p1_to_x = slv.mkTerm(kinds.SepPto, p1, x) + p2_to_y = slv.mkTerm(kinds.SepPto, p2, y) + + # Heap -- the points-to have to be "starred"! + heap = slv.mkTerm(kinds.SepStar, p1_to_x, p2_to_y) + + # Constain "nil" to be something random + fix_nil = slv.mkTerm(kinds.Equal, nil, expr_nil_val) + + # Add it all to the solver! + slv.assertFormula(x_equal_const) + slv.assertFormula(y_gt_x) + slv.assertFormula(heap) + slv.assertFormula(fix_nil) + + # Incremental is disabled due to using separation logic, so don't query + # twice! + + r = (slv.checkSat()) + + # If this is UNSAT, we have an issue so bail-out + if not r.isSat(): + return False + + # Obtain our separation logic terms from the solver + heap_expr = slv.getValueSepHeap() + nil_expr = slv.getValueSepNil() + + # If the heap is not a separating conjunction, bail-out + if (heap_expr.getKind() != kinds.SepStar): + return False + + # If nil is not a direct equality, bail-out + if (nil_expr.getKind() != kinds.Equal): + return False + + # Obtain the values for our "pointers" + val_for_p1 = slv.getValue(p1) + val_for_p2 = slv.getValue(p2) + + # We need to make sure we find both pointers in the heap + checked_p1 = False + checked_p2 = False + + # Walk all the children + for child in heap_expr: + # If we don't have a PTO operator, bail-out + if (child.getKind() != kinds.SepPto): + return False + + # Find both sides of the PTO operator + addr = slv.getValue(child[0]) + value = slv.getValue(child[1]) + + # If the current address is the value for p1 + if (addr == val_for_p1): + checked_p1 = True + + # If it doesn't match the random constant, we have a problem + if value != random_constant: + return False + continue + + if (addr == val_for_p2): + checked_p2 = True + + # Our earlier constraint was that what p2 points to must be *greater* + # than the random constant -- if we get a value that is LTE, then + # something has gone wrong! + + if int(str(value)) <= int(str(random_constant)): + return False + continue + + # We should only have two addresses in heap, so if we haven't hit the + # "continue" for p1 or p2, then bail-out + + return True + + # If we complete the loop and we haven't validated both p1 and p2, then we + # have a problem + if (not checked_p1 or not checked_p2): + return False + + # We now get our value for what nil is + value_for_nil = slv.getValue(nil_expr[1]) + + # The value for nil from the solver should be the value we originally tied + # nil to + + if (value_for_nil != expr_nil_val): + return False + + # All tests pass! + return True + + +# check that we get an exception when we should +assert validate_exception() + +# check the getters +assert validate_getters() diff --git a/test/api/python/two_solvers.py b/test/api/python/two_solvers.py new file mode 100644 index 000000000..eb862d16c --- /dev/null +++ b/test/api/python/two_solvers.py @@ -0,0 +1,22 @@ +############################################################################## +# Top contributors (to current version): +# Yoni Zohar +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################ +# +# A simple test of multiple SmtEngines. +## + +import pycvc5 + +s1 = pycvc5.Solver() +s2 = pycvc5.Solver() +r1 = s1.checkEntailed(s1.mkBoolean(True)) +r2 = s2.checkEntailed(s2.mkBoolean(True)) +assert r1.isEntailed() and r2.isEntailed()