From: Andres Noetzli Date: Sat, 27 Jun 2020 07:12:26 +0000 (-0700) Subject: Add API for retrieving separation heap/nil term (#4663) X-Git-Tag: cvc5-1.0.0~3171 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fa833542f0e96187b3a02c4e15ec33ba45428b62;p=cvc5.git 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. --- diff --git a/NEWS b/NEWS index 60ff9dbc8..f5f9bc03a 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,12 @@ This file contains a summary of important user-visible changes. +Changes since 1.8 +================= + +Improvements: +* New API: Added functions to retrieve the heap/nil term when using separation + logic. + Changes since 1.7 ================= diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index cebba9b5e..0c8de5291 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -33,6 +33,9 @@ #include "api/cvc4cpp.h" +#include +#include + #include "base/check.h" #include "base/configuration.h" #include "expr/expr.h" @@ -49,13 +52,11 @@ #include "smt/model.h" #include "smt/smt_engine.h" #include "theory/logic_info.h" +#include "theory/theory_model.h" #include "util/random.h" #include "util/result.h" #include "util/utility.h" -#include -#include - namespace CVC4 { namespace api { @@ -4673,6 +4674,56 @@ std::vector Solver::getValue(const std::vector& terms) const CVC4_API_SOLVER_TRY_CATCH_END; } +Term Solver::getSeparationHeap() const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_CHECK( + d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) + << "Cannot obtain separation logic expressions if not using the " + "separation logic theory."; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + CVC4_API_CHECK(CVC4::options::produceModels()) + << "Cannot get separation heap term unless model generation is enabled " + "(try --produce-models)"; + CVC4_API_CHECK(d_smtEngine->getSmtMode() + != SmtEngine::SmtMode::SMT_MODE_UNSAT) + << "Cannot get separtion heap term when in unsat mode."; + + theory::TheoryModel* m = + d_smtEngine->getAvailableModel("get separation logic heap and nil"); + Expr heap, nil; + bool hasHeapModel = m->getHeapModel(heap, nil); + CVC4_API_CHECK(hasHeapModel) + << "Failed to obtain heap term from theory model."; + return Term(this, d_smtEngine->getSepHeapExpr()); + CVC4_API_SOLVER_TRY_CATCH_END; +} + +Term Solver::getSeparationNilTerm() const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_CHECK( + d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) + << "Cannot obtain separation logic expressions if not using the " + "separation logic theory."; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + CVC4_API_CHECK(CVC4::options::produceModels()) + << "Cannot get separation nil term unless model generation is enabled " + "(try --produce-models)"; + CVC4_API_CHECK(d_smtEngine->getSmtMode() + != SmtEngine::SmtMode::SMT_MODE_UNSAT) + << "Cannot get separtion nil term when in unsat mode."; + + theory::TheoryModel* m = + d_smtEngine->getAvailableModel("get separation logic heap and nil"); + Expr heap, nil; + bool hasHeapModel = m->getHeapModel(heap, nil); + CVC4_API_CHECK(hasHeapModel) + << "Failed to obtain nil term from theory model."; + return Term(this, nil); + CVC4_API_SOLVER_TRY_CATCH_END; +} + /** * ( pop ) */ diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 049cf6709..828dc6f65 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -3003,6 +3003,18 @@ class CVC4_PUBLIC Solver */ std::vector getValue(const std::vector& terms) const; + /** + * When using separation logic, obtain the term for the heap. + * @return The term for the heap + */ + Term getSeparationHeap() const; + + /** + * When using separation logic, obtain the term for nil. + * @return The term for nil + */ + Term getSeparationNilTerm() const; + /** * Pop (a) level(s) from the assertion stack. * SMT-LIB: ( pop ) diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index eb4254560..ee05709b7 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -197,6 +197,8 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": vector[Term] getUnsatCore() except + Term getValue(Term term) except + vector[Term] getValue(const vector[Term]& terms) except + + Term getSeparationHeap() except + + Term getSeparationNilTerm() except + void pop(uint32_t nscopes) except + void printModel(ostream& out) void push(uint32_t nscopes) except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index 5abbfb113..ab174ef0d 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -917,6 +917,16 @@ cdef class Solver: term.cterm = self.csolver.getValue(t.cterm) return term + def getSeparationHeap(self): + cdef Term term = Term() + term.cterm = self.csolver.getSeparationHeap() + return term + + def getSeparationNilTerm(self): + cdef Term term = Term() + term.cterm = self.csolver.getSeparationNilTerm() + return term + def pop(self, nscopes=1): self.csolver.pop(nscopes) 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; } diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 6faab6075..f080f5348 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -106,6 +106,22 @@ class SolverBlack : public CxxTest::TestSuite void testGetValue1(); void testGetValue2(); void testGetValue3(); + void testGetSeparationHeapTerm1(); + void testGetSeparationHeapTerm2(); + void testGetSeparationHeapTerm3(); + void testGetSeparationHeapTerm4(); + void testGetSeparationHeapTerm5(); + void testGetSeparationNilTerm1(); + void testGetSeparationNilTerm2(); + void testGetSeparationNilTerm3(); + void testGetSeparationNilTerm4(); + void testGetSeparationNilTerm5(); + + /** + * When using separation logic, obtain the term for nil. + * @return The term for nil + */ + Term getSeparationNilTerm() const; void testPush1(); void testPush2(); @@ -1493,6 +1509,124 @@ void SolverBlack::testGetValue3() TS_ASSERT_THROWS(slv.getValue(x), CVC4ApiException&); } +namespace { +/** + * Helper function for testGetSeparation{Heap,Nil}TermX. Asserts and checks + * some simple separation logic constraints. + */ +void checkSimpleSeparationConstraints(Solver* solver) +{ + Sort integer = solver->getIntegerSort(); + Term x = solver->mkConst(integer, "x"); + Term p = solver->mkConst(integer, "p"); + Term heap = solver->mkTerm(Kind::SEP_PTO, p, x); + solver->assertFormula(heap); + Term nil = solver->mkSepNil(integer); + solver->assertFormula(nil.eqTerm(solver->mkReal(5))); + solver->checkSat(); +} +} // namespace + +void SolverBlack::testGetSeparationHeapTerm1() +{ + d_solver->setLogic("QF_BV"); + d_solver->setOption("incremental", "false"); + d_solver->setOption("produce-models", "true"); + Term t = d_solver->mkTrue(); + d_solver->assertFormula(t); + TS_ASSERT_THROWS(d_solver->getSeparationHeap(), CVC4ApiException&); +} + +void SolverBlack::testGetSeparationHeapTerm2() +{ + d_solver->setLogic("ALL_SUPPORTED"); + d_solver->setOption("incremental", "false"); + d_solver->setOption("produce-models", "false"); + checkSimpleSeparationConstraints(d_solver.get()); + TS_ASSERT_THROWS(d_solver->getSeparationHeap(), CVC4ApiException&); +} + +void SolverBlack::testGetSeparationHeapTerm3() +{ + d_solver->setLogic("ALL_SUPPORTED"); + d_solver->setOption("incremental", "false"); + d_solver->setOption("produce-models", "true"); + Term t = d_solver->mkFalse(); + d_solver->assertFormula(t); + d_solver->checkSat(); + TS_ASSERT_THROWS(d_solver->getSeparationHeap(), CVC4ApiException&); +} + +void SolverBlack::testGetSeparationHeapTerm4() +{ + d_solver->setLogic("ALL_SUPPORTED"); + d_solver->setOption("incremental", "false"); + d_solver->setOption("produce-models", "true"); + Term t = d_solver->mkTrue(); + d_solver->assertFormula(t); + d_solver->checkSat(); + TS_ASSERT_THROWS(d_solver->getSeparationHeap(), CVC4ApiException&); +} + +void SolverBlack::testGetSeparationHeapTerm5() +{ + d_solver->setLogic("ALL_SUPPORTED"); + d_solver->setOption("incremental", "false"); + d_solver->setOption("produce-models", "true"); + checkSimpleSeparationConstraints(d_solver.get()); + TS_ASSERT_THROWS_NOTHING(d_solver->getSeparationHeap()); +} + +void SolverBlack::testGetSeparationNilTerm1() +{ + d_solver->setLogic("QF_BV"); + d_solver->setOption("incremental", "false"); + d_solver->setOption("produce-models", "true"); + Term t = d_solver->mkTrue(); + d_solver->assertFormula(t); + TS_ASSERT_THROWS(d_solver->getSeparationNilTerm(), CVC4ApiException&); +} + +void SolverBlack::testGetSeparationNilTerm2() +{ + d_solver->setLogic("ALL_SUPPORTED"); + d_solver->setOption("incremental", "false"); + d_solver->setOption("produce-models", "false"); + checkSimpleSeparationConstraints(d_solver.get()); + TS_ASSERT_THROWS(d_solver->getSeparationNilTerm(), CVC4ApiException&); +} + +void SolverBlack::testGetSeparationNilTerm3() +{ + d_solver->setLogic("ALL_SUPPORTED"); + d_solver->setOption("incremental", "false"); + d_solver->setOption("produce-models", "true"); + Term t = d_solver->mkFalse(); + d_solver->assertFormula(t); + d_solver->checkSat(); + TS_ASSERT_THROWS(d_solver->getSeparationNilTerm(), CVC4ApiException&); +} + +void SolverBlack::testGetSeparationNilTerm4() +{ + d_solver->setLogic("ALL_SUPPORTED"); + d_solver->setOption("incremental", "false"); + d_solver->setOption("produce-models", "true"); + Term t = d_solver->mkTrue(); + d_solver->assertFormula(t); + d_solver->checkSat(); + TS_ASSERT_THROWS(d_solver->getSeparationNilTerm(), CVC4ApiException&); +} + +void SolverBlack::testGetSeparationNilTerm5() +{ + d_solver->setLogic("ALL_SUPPORTED"); + d_solver->setOption("incremental", "false"); + d_solver->setOption("produce-models", "true"); + checkSimpleSeparationConstraints(d_solver.get()); + TS_ASSERT_THROWS_NOTHING(d_solver->getSeparationNilTerm()); +} + void SolverBlack::testPush1() { d_solver->setOption("incremental", "true");