From fa833542f0e96187b3a02c4e15ec33ba45428b62 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sat, 27 Jun 2020 00:12:26 -0700 Subject: Add API for retrieving separation heap/nil term (#4663) This commit extends the API to support the retrieval of heap/nil term when separation logic is used and changes the corresponding system test accordingly. This commit is in preparation of making the constructor of `ExprManager` private. --- test/system/sep_log_api.cpp | 117 ++++++++++++++++++++------------------------ 1 file changed, 54 insertions(+), 63 deletions(-) (limited to 'test/system') diff --git a/test/system/sep_log_api.cpp b/test/system/sep_log_api.cpp index c4244d7cb..9341310a3 100644 --- a/test/system/sep_log_api.cpp +++ b/test/system/sep_log_api.cpp @@ -22,10 +22,9 @@ #include #include -#include "expr/expr.h" -#include "smt/smt_engine.h" +#include "api/cvc4cpp.h" -using namespace CVC4; +using namespace CVC4::api; using namespace std; /** @@ -34,33 +33,31 @@ using namespace std; */ int validate_exception(void) { - ExprManager em; - Options opts; - SmtEngine smt(&em); + Solver slv; /* * Setup some options for CVC4 -- we explictly want to use a simplistic * theory (e.g., QF_IDL) */ - smt.setLogic("QF_IDL"); - smt.setOption("produce-models", SExpr("true")); - smt.setOption("incremental", SExpr("false")); + slv.setLogic("QF_IDL"); + slv.setOption("produce-models", "true"); + slv.setOption("incremental", "false"); /* Our integer type */ - Type integer(em.integerType()); + Sort integer = slv.getIntegerSort(); /* Our SMT constants */ - Expr x(em.mkVar("x", integer)); - Expr y(em.mkVar("y", integer)); + Term x = slv.mkConst(integer, "x"); + Term y = slv.mkConst(integer, "y"); /* y > x */ - Expr y_gt_x(em.mkExpr(kind::GT, y, x)); + Term y_gt_x(slv.mkTerm(Kind::GT, y, x)); /* assert it */ - smt.assertFormula(y_gt_x); + slv.assertFormula(y_gt_x); /* check */ - Result r(smt.checkSat()); + Result r(slv.checkSat()); /* If this is UNSAT, we have an issue; so bail-out */ if (!r.isSat()) @@ -83,9 +80,9 @@ int validate_exception(void) /* test the heap expression */ try { - Expr heap_expr(smt.getSepHeapExpr()); + Term heap_expr = slv.getSeparationHeap(); } - catch (const CVC4::RecoverableModalException& e) + catch (const CVC4ApiException& e) { caught_on_heap = true; @@ -99,9 +96,9 @@ int validate_exception(void) /* test the nil expression */ try { - Expr nil_expr(smt.getSepNilExpr()); + Term nil_expr = slv.getSeparationNilTerm(); } - catch (const CVC4::RecoverableModalException& e) + catch (const CVC4ApiException& e) { caught_on_nil = true; @@ -127,60 +124,56 @@ int validate_exception(void) */ int validate_getters(void) { - ExprManager em; - Options opts; - SmtEngine smt(&em); + Solver slv; /* Setup some options for CVC4 */ - smt.setLogic("QF_ALL_SUPPORTED"); - smt.setOption("produce-models", SExpr("true")); - smt.setOption("incremental", SExpr("false")); + slv.setLogic("QF_ALL_SUPPORTED"); + slv.setOption("produce-models", "true"); + slv.setOption("incremental", "false"); /* Our integer type */ - Type integer(em.integerType()); + Sort integer = slv.getIntegerSort(); /* A "random" constant */ - Rational val_for_random_constant(Rational(0xDEADBEEF)); - Expr random_constant(em.mkConst(val_for_random_constant)); + Term random_constant = slv.mkReal(0xDEADBEEF); /* Another random constant */ - Rational val_for_expr_nil_val(Rational(0xFBADBEEF)); - Expr expr_nil_val(em.mkConst(val_for_expr_nil_val)); + Term expr_nil_val = slv.mkReal(0xFBADBEEF); /* Our nil term */ - Expr nil(em.mkNullaryOperator(integer, kind::SEP_NIL)); + Term nil = slv.mkSepNil(integer); /* Our SMT constants */ - Expr x(em.mkVar("x", integer)); - Expr y(em.mkVar("y", integer)); - Expr p1(em.mkVar("p1", integer)); - Expr p2(em.mkVar("p2", integer)); + Term x = slv.mkConst(integer, "x"); + Term y = slv.mkConst(integer, "y"); + Term p1 = slv.mkConst(integer, "p1"); + Term p2 = slv.mkConst(integer, "p2"); /* Constraints on x and y */ - Expr x_equal_const(em.mkExpr(kind::EQUAL, x, random_constant)); - Expr y_gt_x(em.mkExpr(kind::GT, y, x)); + Term x_equal_const = slv.mkTerm(Kind::EQUAL, x, random_constant); + Term y_gt_x = slv.mkTerm(Kind::GT, y, x); /* Points-to expressions */ - Expr p1_to_x(em.mkExpr(kind::SEP_PTO, p1, x)); - Expr p2_to_y(em.mkExpr(kind::SEP_PTO, p2, y)); + Term p1_to_x = slv.mkTerm(Kind::SEP_PTO, p1, x); + Term p2_to_y = slv.mkTerm(Kind::SEP_PTO, p2, y); /* Heap -- the points-to have to be "starred"! */ - Expr heap(em.mkExpr(kind::SEP_STAR, p1_to_x, p2_to_y)); + Term heap = slv.mkTerm(Kind::SEP_STAR, p1_to_x, p2_to_y); /* Constain "nil" to be something random */ - Expr fix_nil(em.mkExpr(kind::EQUAL, nil, expr_nil_val)); + Term fix_nil = slv.mkTerm(Kind::EQUAL, nil, expr_nil_val); /* Add it all to the solver! */ - smt.assertFormula(x_equal_const); - smt.assertFormula(y_gt_x); - smt.assertFormula(heap); - smt.assertFormula(fix_nil); + 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! */ - Result r(smt.checkSat()); + Result r(slv.checkSat()); /* If this is UNSAT, we have an issue; so bail-out */ if (!r.isSat()) @@ -189,43 +182,41 @@ int validate_getters(void) } /* Obtain our separation logic terms from the solver */ - Expr heap_expr(smt.getSepHeapExpr()); - Expr nil_expr(smt.getSepNilExpr()); + Term heap_expr = slv.getSeparationHeap(); + Term nil_expr = slv.getSeparationNilTerm(); /* If the heap is not a separating conjunction, bail-out */ - if (heap_expr.getKind() != kind::SEP_STAR) + if (heap_expr.getKind() != Kind::SEP_STAR) { return -1; } /* If nil is not a direct equality, bail-out */ - if (nil_expr.getKind() != kind::EQUAL) + if (nil_expr.getKind() != Kind::EQUAL) { return -1; } /* Obtain the values for our "pointers" */ - Rational val_for_p1(smt.getValue(p1).getConst()); - Rational val_for_p2(smt.getValue(p2).getConst()); + Term val_for_p1 = slv.getValue(p1); + Term val_for_p2 = slv.getValue(p2); /* We need to make sure we find both pointers in the heap */ bool checked_p1(false); bool checked_p2(false); /* Walk all the children */ - for (Expr child : heap_expr.getChildren()) + for (const Term& child : heap_expr) { /* If we don't have a PTO operator, bail-out */ - if (child.getKind() != kind::SEP_PTO) + if (child.getKind() != Kind::SEP_PTO) { return -1; } /* Find both sides of the PTO operator */ - Rational addr( - smt.getValue(child.getChildren().at(0)).getConst()); - Rational value( - smt.getValue(child.getChildren().at(1)).getConst()); + Term addr = slv.getValue(child[0]); + Term value = slv.getValue(child[1]); /* If the current address is the value for p1 */ if (addr == val_for_p1) @@ -233,7 +224,7 @@ int validate_getters(void) checked_p1 = true; /* If it doesn't match the random constant, we have a problem */ - if (value != val_for_random_constant) + if (value != random_constant) { return -1; } @@ -250,7 +241,8 @@ int validate_getters(void) * than the random constant -- if we get a value that is LTE, then * something has gone wrong! */ - if (value <= val_for_random_constant) + if (std::stoll(value.toString()) + <= std::stoll(random_constant.toString())) { return -1; } @@ -274,14 +266,13 @@ int validate_getters(void) } /* We now get our value for what nil is */ - Rational value_for_nil = - smt.getValue(nil_expr.getChildren().at(1)).getConst(); + Term 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 != val_for_expr_nil_val) + if (value_for_nil != expr_nil_val) { return -1; } -- cgit v1.2.3