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
=================
#include "api/cvc4cpp.h"
+#include <cstring>
+#include <sstream>
+
#include "base/check.h"
#include "base/configuration.h"
#include "expr/expr.h"
#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 <cstring>
-#include <sstream>
-
namespace CVC4 {
namespace api {
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 <numeral> )
*/
*/
std::vector<Term> getValue(const std::vector<Term>& 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 <numeral> )
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 +
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)
#include <iostream>
#include <sstream>
-#include "expr/expr.h"
-#include "smt/smt_engine.h"
+#include "api/cvc4cpp.h"
-using namespace CVC4;
+using namespace CVC4::api;
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())
/* 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;
/* 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;
*/
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())
}
/* 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<CVC4::Rational>());
- Rational val_for_p2(smt.getValue(p2).getConst<CVC4::Rational>());
+ 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<CVC4::Rational>());
- Rational value(
- smt.getValue(child.getChildren().at(1)).getConst<CVC4::Rational>());
+ 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)
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;
}
* 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;
}
}
/* We now get our value for what nil is */
- Rational value_for_nil =
- smt.getValue(nil_expr.getChildren().at(1)).getConst<CVC4::Rational>();
+ 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;
}
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();
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");
projects / cvc5.git / commitdiff