From c2757f0440c5d5b841e05c60d1fd93dc9ee3763a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 10 Nov 2020 07:43:19 -0600 Subject: Add proper support for the declare-heap command for separation logic (#5405) This adds proper support for the (declare-heap (T U)) command, which declares the type of the heap in separation logic. This command is part of the standard for separation logic. This previous was handled in an ad-hoc way where the type of the heap would be inferred on demand. This was a poor solution and has led to a number of issues related to when the heap is inferred. Fixes #5343, fixes #4926. Work towards CVC4/cvc4-wishues#22. --- src/api/cvc4cpp.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'src/api/cvc4cpp.cpp') diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index c0e6bad5f..566bcc3c7 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -5194,6 +5194,17 @@ Term Solver::getQuantifierEliminationDisjunct(api::Term q) const CVC4_API_SOLVER_TRY_CATCH_END; } +void Solver::declareSeparationHeap(api::Sort locSort, api::Sort dataSort) 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."; + d_smtEngine->declareSepHeap(locSort.getTypeNode(), dataSort.getTypeNode()); + CVC4_API_SOLVER_TRY_CATCH_END; +} + Term Solver::getSeparationHeap() const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; -- cgit v1.2.3