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.
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;
*/
Term getQuantifierEliminationDisjunct(api::Term q) const;
+ /**
+ * When using separation logic, this sets the location sort and the
+ * datatype sort to the given ones. This method should be invoked exactly
+ * once, before any separation logic constraints are provided.
+ * @param locSort The location sort of the heap
+ * @param dataSort The data sort of the heap
+ */
+ void declareSeparationHeap(api::Sort locSort, api::Sort dataSort) const;
+
/**
* When using separation logic, obtain the term for the heap.
* @return The term for the heap
vector[Term] getUnsatCore() except +
Term getValue(Term term) except +
vector[Term] getValue(const vector[Term]& terms) except +
+ void declareSeparationHeap(Sort locSort, Sort dataSort) except +
Term getSeparationHeap() except +
Term getSeparationNilTerm() except +
void pop(uint32_t nscopes) except +
term.cterm = self.csolver.getSeparationHeap()
return term
+ def declareSeparationHeap(self, Sort locType, Sort dataType):
+ self.csolver.declareSeparationHeap(locType.csort, dataType.csort)
+
def getSeparationNilTerm(self):
cdef Term term = Term(self)
term.cterm = self.csolver.getSeparationNilTerm()
@declarations {
std::vector<api::DatatypeDecl> dts;
CVC4::api::Term e, e2;
- CVC4::api::Sort t;
+ CVC4::api::Sort t, s;
std::string name;
std::vector<std::string> names;
std::vector<CVC4::api::Term> terms;
}
| DECLARE_HEAP LPAREN_TOK
sortSymbol[t, CHECK_DECLARED]
- sortSymbol[t, CHECK_DECLARED]
- // We currently do nothing with the type information declared for the heap.
- { cmd->reset(new EmptyCommand()); }
+ sortSymbol[s, CHECK_DECLARED]
+ { cmd->reset(new DeclareHeapCommand(t, s)); }
RPAREN_TOK
| BLOCK_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
{ cmd->reset(new BlockModelCommand()); }
printUnknownCommand(out, "comment");
}
+void Printer::toStreamCmdDeclareHeap(std::ostream& out,
+ TypeNode locType,
+ TypeNode dataType) const
+{
+ printUnknownCommand(out, "declare-heap");
+}
+
void Printer::toStreamCmdCommandSequence(
std::ostream& out, const std::vector<Command*>& sequence) const
{
/** Print comment command */
virtual void toStreamCmdComment(std::ostream& out,
const std::string& comment) const;
+ /** Declare heap command */
+ virtual void toStreamCmdDeclareHeap(std::ostream& out,
+ TypeNode locType,
+ TypeNode dataType) const;
/** Print command sequence command */
virtual void toStreamCmdCommandSequence(
out << "(set-info :notes \"" << s << "\")" << std::endl;
}
+void Smt2Printer::toStreamCmdDeclareHeap(std::ostream& out,
+ TypeNode locType,
+ TypeNode dataType) const
+{
+ out << "(declare-heap (" << locType << " " << dataType << "))" << std::endl;
+}
+
void Smt2Printer::toStreamCmdEmpty(std::ostream& out,
const std::string& name) const
{
void toStreamCmdComment(std::ostream& out,
const std::string& comment) const override;
+ /** Print declare-heap command */
+ void toStreamCmdDeclareHeap(std::ostream& out,
+ TypeNode locType,
+ TypeNode dataType) const override;
+
/** Print command sequence command */
void toStreamCmdCommandSequence(
std::ostream& out, const std::vector<Command*>& sequence) const override;
formals,
api::termVectorToNodes(d_formulas));
}
+/* -------------------------------------------------------------------------- */
+/* class DeclareHeapCommand */
+/* -------------------------------------------------------------------------- */
+DeclareHeapCommand::DeclareHeapCommand(api::Sort locSort, api::Sort dataSort)
+ : d_locSort(locSort), d_dataSort(dataSort)
+{
+}
+
+api::Sort DeclareHeapCommand::getLocationSort() const { return d_locSort; }
+api::Sort DeclareHeapCommand::getDataSort() const { return d_dataSort; }
+
+void DeclareHeapCommand::invoke(api::Solver* solver)
+{
+ solver->declareSeparationHeap(d_locSort, d_dataSort);
+}
+
+Command* DeclareHeapCommand::clone() const
+{
+ return new DeclareHeapCommand(d_locSort, d_dataSort);
+}
+
+std::string DeclareHeapCommand::getCommandName() const
+{
+ return "declare-heap";
+}
+
+void DeclareHeapCommand::toStream(std::ostream& out,
+ int toDepth,
+ size_t dag,
+ OutputLanguage language) const
+{
+ Printer::getPrinter(language)->toStreamCmdDeclareHeap(
+ out, d_locSort.getTypeNode(), d_dataSort.getTypeNode());
+}
/* -------------------------------------------------------------------------- */
-/* class SetUserAttribute */
+/* class SetUserAttributeCommand */
/* -------------------------------------------------------------------------- */
SetUserAttributeCommand::SetUserAttributeCommand(
void toStream(
std::ostream& out,
int toDepth = -1,
-
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class DefineNamedFunctionCommand */
bool d_global;
}; /* class DefineFunctionRecCommand */
+/**
+ * In separation logic inputs, which is an extension of smt2 inputs, this
+ * corresponds to the command:
+ * (declare-heap (T U))
+ * where T is the location sort and U is the data sort.
+ */
+class CVC4_PUBLIC DeclareHeapCommand : public Command
+{
+ public:
+ DeclareHeapCommand(api::Sort locSort, api::Sort dataSort);
+ api::Sort getLocationSort() const;
+ api::Sort getDataSort() const;
+ void invoke(api::Solver* solver) override;
+ Command* clone() const override;
+ std::string getCommandName() const override;
+ void toStream(
+ std::ostream& out,
+ int toDepth = -1,
+ size_t dag = 1,
+ OutputLanguage language = language::output::LANG_AUTO) const override;
+
+ protected:
+ /** The location sort */
+ api::Sort d_locSort;
+ /** The data sort */
+ api::Sort d_dataSort;
+};
+
/**
* The command when an attribute is set by a user. In SMT-LIBv2 this is done
* via the syntax (! expr :attr)
#include "theory/logic_info.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/rewriter.h"
+#include "theory/smt_engine_subsolver.h"
#include "theory/theory_engine.h"
#include "util/hash.h"
#include "util/random.h"
return eassertsProc;
}
+void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
+{
+ if (!d_logic.isTheoryEnabled(THEORY_SEP))
+ {
+ const char* msg =
+ "Cannot declare heap if not using the separation logic theory.";
+ throw RecoverableModalException(msg);
+ }
+ SmtScope smts(this);
+ finishInit();
+ TheoryEngine* te = getTheoryEngine();
+ te->declareSepHeap(locT, dataT);
+}
+
+bool SmtEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT)
+{
+ SmtScope smts(this);
+ finishInit();
+ TheoryEngine* te = getTheoryEngine();
+ return te->getSepHeapTypes(locT, dataT);
+}
+
Node SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
UnsatCore core = getUnsatCore();
- SmtEngine coreChecker(d_exprManager, &d_options);
- coreChecker.setIsInternalSubsolver();
- coreChecker.setLogic(getLogicInfo());
- coreChecker.getOptions().set(options::checkUnsatCores, false);
+ // initialize the core checker
+ std::unique_ptr<SmtEngine> coreChecker;
+ initializeSubsolver(coreChecker);
+ coreChecker->getOptions().set(options::checkUnsatCores, false);
+
+ // set up separation logic heap if necessary
+ TypeNode sepLocType, sepDataType;
+ if (getSepHeapTypes(sepLocType, sepDataType))
+ {
+ coreChecker->declareSepHeap(sepLocType, sepDataType);
+ }
Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl;
for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
Node assertionAfterExpansion = expandDefinitions(*i);
Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
<< ", expanded to " << assertionAfterExpansion << "\n";
- coreChecker.assertFormula(assertionAfterExpansion);
+ coreChecker->assertFormula(assertionAfterExpansion);
}
Result r;
try {
- r = coreChecker.checkSat();
+ r = coreChecker->checkSat();
} catch(...) {
throw;
}
*/
Result blockModelValues(const std::vector<Node>& exprs);
+ /**
+ * Declare heap. For smt2 inputs, this is called when the command
+ * (declare-heap (locT datat)) is invoked by the user. This sets locT as the
+ * location type and dataT is the data type for the heap. This command should
+ * be executed only once, and must be invoked before solving separation logic
+ * inputs.
+ */
+ void declareSepHeap(TypeNode locT, TypeNode dataT);
+
+ /**
+ * Get the separation heap types, which extracts which types were passed to
+ * the method above.
+ *
+ * @return true if the separation logic heap types have been declared.
+ */
+ bool getSepHeapTypes(TypeNode& locT, TypeNode& dataT);
+
/** When using separation logic, obtain the expression for the heap. */
Node getSepHeapExpr();
}
}
+void TheorySep::declareSepHeap(TypeNode locT, TypeNode dataT)
+{
+ if (!d_type_ref.isNull())
+ {
+ TypeNode te1 = d_loc_to_data_type.begin()->first;
+ std::stringstream ss;
+ ss << "ERROR: cannot declare heap types for separation logic more than "
+ "once. We are declaring heap of type ";
+ ss << locT << " -> " << dataT << ", but we already have ";
+ ss << d_type_ref << " -> " << d_type_data;
+ throw LogicException(ss.str());
+ }
+ Node nullAtom;
+ registerRefDataTypes(locT, dataT, nullAtom);
+}
+
TheoryRewriter* TheorySep::getTheoryRewriter() { return &d_rewriter; }
bool TheorySep::needsEqualityEngine(EeSetupInfo& esi)
void TheorySep::presolve() {
Trace("sep-pp") << "Presolving" << std::endl;
- //TODO: cleanup if incremental?
}
}
void TheorySep::registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom ){
- //separation logic is effectively enabled when we find at least one spatial constraint occurs in the input
- if( options::incrementalSolving() ){
- std::stringstream ss;
- ss << "ERROR: cannot use separation logic in incremental mode." << std::endl;
- throw LogicException(ss.str());
- }
- std::map< TypeNode, TypeNode >::iterator itt = d_loc_to_data_type.find( tn1 );
- if( itt==d_loc_to_data_type.end() ){
- if( !d_loc_to_data_type.empty() ){
- TypeNode te1 = d_loc_to_data_type.begin()->first;
+ if (!d_type_ref.isNull())
+ {
+ Assert(!atom.isNull());
+ // already declared, ensure compatible
+ if ((!tn1.isNull() && !tn1.isComparableTo(d_type_ref))
+ || (!tn2.isNull() && !tn2.isComparableTo(d_type_data)))
+ {
std::stringstream ss;
- ss << "ERROR: specifying heap constraints for two different types : " << tn1 << " -> " << tn2 << " and " << te1 << " -> " << d_loc_to_data_type[te1] << std::endl;
- throw LogicException(ss.str());
- Assert(false);
- }
- if( tn2.isNull() ){
- Trace("sep-type") << "Sep: assume location type " << tn1 << " (from " << atom << ")" << std::endl;
- }else{
- Trace("sep-type") << "Sep: assume location type " << tn1 << " is associated with data type " << tn2 << " (from " << atom << ")" << std::endl;
- }
- d_loc_to_data_type[tn1] = tn2;
- //for now, we only allow heap constraints of one type
- d_type_ref = tn1;
- d_type_data = tn2;
- d_bound_kind[tn1] = bound_default;
- }else{
- if( !tn2.isNull() ){
- if( itt->second!=tn2 ){
- if( itt->second.isNull() ){
- Trace("sep-type") << "Sep: assume location type " << tn1 << " is associated with data type " << tn2 << " (from " << atom << ")" << std::endl;
- //now we know data type
- d_loc_to_data_type[tn1] = tn2;
- d_type_data = tn2;
- }else{
- std::stringstream ss;
- ss << "ERROR: location type " << tn1 << " is already associated with data type " << itt->second << ", offending atom is " << atom << " with data type " << tn2 << std::endl;
- throw LogicException(ss.str());
- Assert(false);
- }
- }
+ ss << "ERROR: the separation logic heap type has already been set to "
+ << d_type_ref << " -> " << d_type_data
+ << " but we have a constraint that uses different heap types, "
+ "offending atom is "
+ << atom << " with associated heap type " << tn1 << " -> " << tn2
+ << std::endl;
}
+ return;
+ }
+ // if not declared yet, and we have a separation logic constraint, throw
+ // an error.
+ if (!atom.isNull())
+ {
+ std::stringstream ss;
+ // error, heap not declared
+ ss << "ERROR: the type of the separation logic heap has not been declared "
+ "(e.g. via a declare-heap command), and we have a separation logic "
+ "constraint "
+ << atom << std::endl;
+ throw LogicException(ss.str());
}
+ // otherwise set it
+ Trace("sep-type") << "Sep: assume location type " << tn1
+ << " is associated with data type " << tn2 << std::endl;
+ d_loc_to_data_type[tn1] = tn2;
+ // for now, we only allow heap constraints of one type
+ d_type_ref = tn1;
+ d_type_data = tn2;
+ d_bound_kind[tn1] = bound_default;
}
void TheorySep::initializeBounds() {
ProofNodeManager* pnm = nullptr);
~TheorySep();
+ /**
+ * Declare heap. For smt2 inputs, this is called when the command
+ * (declare-heap (locT datat)) is invoked by the user. This sets locT as the
+ * location type and dataT is the data type for the heap. This command can be
+ * executed once only, and must be invoked before solving separation logic
+ * inputs.
+ */
+ void declareSepHeap(TypeNode locT, TypeNode dataT) override;
+
//--------------------------------- initialization
/** get the official theory rewriter of this theory */
TheoryRewriter* getTheoryRewriter() override;
//get global reference/data type
TypeNode getReferenceType( Node n );
TypeNode getDataType( Node n );
- void registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom );
+ /**
+ * This is called either when:
+ * (A) a declare-heap command is issued with tn1/tn2, and atom is null, or
+ * (B) an atom specifying the heap type tn1/tn2 is registered to this theory.
+ * We set the heap type if we are are case (A), and check whether the
+ * heap type is consistent in the case of (B).
+ */
+ void registerRefDataTypes(TypeNode tn1, TypeNode tn2, Node atom);
//get location/data type
//get the base label for the spatial assertion
Node getBaseLabel( TypeNode tn );
smte.reset(new SmtEngine(nm->toExprManager(), &smtCurr->getOptions()));
smte->setIsInternalSubsolver();
smte->setLogic(smtCurr->getLogicInfo());
+ // set the options
if (needsTimeout)
{
smte->setTimeLimit(timeout);
}
- smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
}
Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
/**
* This function initializes the smt engine smte to check the satisfiability
- * of the argument "query".
+ * of the argument "query". It takes the logic and options of the current
+ * SMT engine in scope.
+ *
+ * Notice this method intentionally does not fully initialize smte. This means
+ * that the options of smte can still be modified after it is returned by
+ * this method.
+ *
+ * Notice that some aspects of subsolvers are not incoporated by this call.
+ * For example, the type of separation logic heaps is not set on smte, even
+ * if the current SMT engine has declared a separation logic heap.
*
* @param smte The smt engine pointer to initialize
* @param needsTimeout Whether we would like to set a timeout
return d_logicInfo;
}
+ /**
+ * Set separation logic heap. This is called when the location and data
+ * types for separation logic are determined. This should be called at
+ * most once, before solving.
+ *
+ * This currently should be overridden by the separation logic theory only.
+ */
+ virtual void declareSepHeap(TypeNode locT, TypeNode dataT) {}
+
/**
* The theory that owns the uninterpreted sort.
*/
const LogicInfo& TheoryEngine::getLogicInfo() const { return d_logicInfo; }
+bool TheoryEngine::getSepHeapTypes(TypeNode& locType, TypeNode& dataType) const
+{
+ if (d_sepLocType.isNull())
+ {
+ return false;
+ }
+ locType = d_sepLocType;
+ dataType = d_sepDataType;
+ return true;
+}
+
+void TheoryEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
+{
+ Theory* tsep = theoryOf(THEORY_SEP);
+ if (tsep == nullptr)
+ {
+ Assert(false) << "TheoryEngine::declareSepHeap called without the "
+ "separation logic theory enabled";
+ return;
+ }
+
+ // Definition of the statement that is to be run by every theory
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+ theoryOf(THEORY)->declareSepHeap(locT, dataT);
+
+ // notify each theory using the statement above
+ CVC4_FOR_EACH_THEORY;
+
+ // remember the types we have set
+ d_sepLocType = locT;
+ d_sepDataType = dataT;
+}
+
theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
Assert(a.getType().isComparableTo(b.getType()));
return d_sharedSolver->getEqualityStatus(a, b);
* the cost of walking the DAG on registration, etc.
*/
const LogicInfo& d_logicInfo;
+ /** The separation logic location and data types */
+ TypeNode d_sepLocType;
+ TypeNode d_sepDataType;
/** Reference to the output manager of the smt engine */
OutputManager& d_outMgr;
}
/** get the logic info used by this theory engine */
const LogicInfo& getLogicInfo() const;
+ /** get the separation logic heap types */
+ bool getSepHeapTypes(TypeNode& locType, TypeNode& dataType) const;
+
+ /**
+ * Declare heap. This is used for separation logics to set the location
+ * and data types. It should be called only once, and before any separation
+ * logic constraints are asserted to this theory engine.
+ */
+ void declareSepHeap(TypeNode locT, TypeNode dataT);
+
/**
* Returns the equality status of the two terms, from the theory
* that owns the domain type. The types of a and b must be the same.
/* Our integer type */
Sort integer = slv.getIntegerSort();
+ /** we intentionally do not set the separation logic heap */
+
/* Our SMT constants */
Term x = slv.mkConst(integer, "x");
Term y = slv.mkConst(integer, "y");
/* Our integer type */
Sort integer = slv.getIntegerSort();
+ /** Declare the separation logic heap types */
+ slv.declareSeparationHeap(integer, integer);
+
/* A "random" constant */
Term random_constant = slv.mkInteger(0xDEADBEEF);
(set-logic QF_ALL_SUPPORTED)
(set-info :status unsat)
+(declare-heap (Int Int))
+
(declare-const w Int)
(declare-const w1 Int)
(declare-const w2 Int)
(set-info :status unsat)
(declare-sort Loc 0)
(declare-const l Loc)
+(declare-heap (Loc Loc))
(assert (sep (not (_ emp Loc Loc)) (not (_ emp Loc Loc))))
(assert (pto l l))
(check-sat)
; COMMAND-LINE: --quiet
; EXPECT: sat
(set-logic ALL)
+(declare-heap (Int Int))
(assert (_ emp Int Int))
(check-sat)
; COMMAND-LINE: --no-check-models
; EXPECT: sat
(set-logic QF_SEP_LIA)
+(declare-heap (Int Int))
(assert (not (_ emp Int Int)))
(check-sat)
(declare-sort U 0)
(declare-fun f (U) U)
(declare-fun a () U)
+(declare-heap (U Int))
(assert (= (as sep.nil U) (f a)))
(set-logic QF_ALL_SUPPORTED)
(set-info :status sat)
(declare-fun x () Int)
+(declare-heap (Int Int))
(assert (sep (= x 0) (not (= x 5))))
(set-logic QF_ALL_SUPPORTED)
(set-info :status unsat)
+(declare-heap (Int Int))
(declare-const x Int)
(set-logic QF_ALL_SUPPORTED)
(set-info :status unsat)
+(declare-heap (Int Int))
(declare-const x Int)
(set-logic QF_ALL_SUPPORTED)
(set-info :status unsat)
+(declare-heap (Int Int))
(declare-const x Int)
(declare-const y Int)
(set-logic QF_ALL_SUPPORTED)
(set-info :status unsat)
+(declare-heap (Int Int))
(declare-const x Int)
(declare-const y Int)
(set-logic QF_ALL_SUPPORTED)
(set-info :status unsat)
-
(declare-sort U 0)
+(declare-heap (U U))
+
(declare-fun x () U)
(declare-fun y () U)
(declare-fun a () U)
(set-logic QF_ALL_SUPPORTED)
(set-option :produce-models true)
(set-info :status sat)
+(declare-heap (Int Int))
(declare-fun x () Int)
; works
; COMMAND-LINE: --no-check-models --sep-pre-skolem-emp
; EXPECT: sat
(set-logic QF_ALL_SUPPORTED)
+(declare-heap (Int Int))
(assert (not (_ emp Int Int)))
(check-sat)
(declare-const loc0 Loc)
(declare-datatypes ((Node 0)) (((node (data Int) (left Loc) (right Loc)))))
+(declare-heap (Loc Node))
(declare-fun data0 () Node)
; COMMAND-LINE: --no-check-models
; EXPECT: sat
(set-logic QF_ALL_SUPPORTED)
+(declare-heap (Int Int))
(assert (wand (_ emp Int Int) (_ emp Int Int)))
(check-sat)
(set-logic QF_ALL_SUPPORTED)
(set-info :status unsat)
+(declare-heap (Int Int))
(declare-const x Int)
(declare-const y Int)
; EXPECT: sat
(set-logic QF_ALL_SUPPORTED)
(set-info :status sat)
+(declare-heap (Int Int))
(declare-const x Int)
(declare-const a Int)
(set-logic QF_ALL_SUPPORTED)
(declare-sort Loc 0)
+(declare-heap (Loc Loc))
(declare-const w Loc)
(declare-const u1 Loc)
(set-info :status unsat)
(declare-sort U 0)
(declare-fun u () U)
+(declare-heap (U U))
(assert (sep (not (_ emp U U)) (not (_ emp U U))))
(set-logic ALL_SUPPORTED)
(declare-sort Loc 0)
(declare-const l Loc)
+(declare-heap (Loc Loc))
(assert (not (_ emp Loc Loc)))
(assert (forall ((x Loc) (y Loc)) (not (pto x y))))
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(declare-sort U 0)
+(declare-heap (U Int))
(declare-fun u1 () U)
(declare-fun u2 () U)
(assert (not (= u1 u2)))
; EXPECT: sat
(set-logic QF_ALL_SUPPORTED)
(set-info :status sat)
+(declare-heap (Int Int))
(declare-const x Int)
(declare-const a Int)
(set-logic QF_ALL_SUPPORTED)
(set-info :status unsat)
+(declare-heap (Int Int))
(declare-const x1 Int)
(declare-const x2 Int)
; EXPECT: unsat
(set-logic ALL_SUPPORTED)
(set-info :status unsat)
+(declare-heap (Int Int))
(declare-const u Int)
(set-logic QF_ALL_SUPPORTED)
(set-info :status unsat)
+(declare-heap (Int Int))
(declare-const x Int)
(declare-const y Int)
(set-logic QF_ALL_SUPPORTED)
(set-info :status unsat)
+(declare-heap (Int Int))
(declare-const x Int)
(declare-const y Int)
(set-logic QF_SEP_LIA)
(set-info :status unsat)
+(declare-heap (Int Int))
(declare-const x1 Int)
(declare-const x2 Int)
(declare-sort Loc 0)
(declare-const l Loc)
(declare-const x Loc)
+(declare-heap (Loc Loc))
(assert (wand (pto x x) false))
(assert (forall ((x Loc) (y Loc)) (not (pto x y))))
; EXPECT: sat
(set-logic QF_ALL_SUPPORTED)
(set-info :status sat)
+(declare-heap (Int Int))
(declare-const x Int)
(declare-const y Int)
(set-logic QF_ALL_SUPPORTED)
(set-info :status unsat)
+(declare-heap (Int Int))
(declare-const x Int)
(declare-const y Int)
; EXPECT: sat
(set-logic QF_ALL_SUPPORTED)
(set-info :status sat)
+(declare-heap (Int Int))
(declare-const x Int)
(declare-const y Int)
; EXPECT: sat
(set-logic QF_ALL_SUPPORTED)
(set-info :status sat)
+(declare-heap (Int Int))
(declare-const x Int)
(declare-const y Int)
; EXPECT: sat
(set-logic QF_ALL_SUPPORTED)
(set-info :status sat)
+(declare-heap (Int Int))
(declare-const x Int)
(declare-const y Int)
; EXPECT: sat
(set-logic QF_ALL_SUPPORTED)
(set-info :status sat)
+(declare-heap (Int Int))
(declare-const x Int)
(declare-const y Int)
(set-logic QF_ALL_SUPPORTED)
(set-info :status unsat)
+(declare-heap (Int Int))
(declare-const x Int)
(declare-const y Int)
(set-logic QF_ALL_SUPPORTED)
(set-info :status sat)
(declare-sort U 0)
+(declare-heap (U U))
(declare-fun x () U)
(declare-fun y () U)
(declare-fun a () U)
; EXPECT: sat
(set-logic QF_ALL_SUPPORTED)
(set-info :status sat)
+(declare-heap (Int Int))
(declare-const x Int)
(declare-const y Int)
(set-logic QF_ALL_SUPPORTED)
(set-info :status unsat)
+(declare-heap (Int Int))
(declare-const x Int)
(declare-const y Int)
; EXPECT: unsat
(set-logic QF_ALL_SUPPORTED)
(set-info :status unsat)
+(declare-heap (Int Int))
(declare-const x Int)
(declare-const y Int)
; COMMAND-LINE: --no-check-models
; EXPECT: sat
(set-logic QF_ALL_SUPPORTED)
+(declare-heap (Int Int))
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun u () Int)
; EXPECT: sat
(set-logic QF_ALL_SUPPORTED)
(set-info :status sat)
+(declare-heap (Int Int))
(declare-fun x () Int)
(assert (wand (pto x x) false))
(check-sat)
; COMMAND-LINE: --no-check-models
; EXPECT: sat
(set-logic QF_ALL_SUPPORTED)
+(declare-heap (Int Int))
(declare-fun x () Int)
(assert (wand (_ emp Int Int) (pto x 3)))
(check-sat)
; EXPECT: sat
(set-logic QF_ALL_SUPPORTED)
(set-info :status sat)
+(declare-heap (Int Int))
(declare-fun x () Int)
(assert (wand (pto x 1) (_ emp Int Int)))
(check-sat)
; COMMAND-LINE: --no-check-models
; EXPECT: sat
(set-logic QF_ALL_SUPPORTED)
+(declare-heap (Int Int))
(declare-fun x () Int)
(assert (wand (pto x 1) (pto x 1)))
(check-sat)
; EXPECT: sat
(set-logic QF_ALL_SUPPORTED)
(set-info :status sat)
+(declare-heap (Int Int))
(declare-fun x () Int)
(assert (wand (pto x 1) (pto x 3)))
(check-sat)
; EXPECT: unsat
(set-logic QF_ALL_SUPPORTED)
(declare-fun x () Int)
+(declare-heap (Int Int))
(assert (wand (pto x 1) (pto x 3)))
(assert (_ emp Int Int))
(check-sat)
void testGetValue3();
void testGetQuantifierElimination();
void testGetQuantifierEliminationDisjunct();
+ void testDeclareSeparationHeap();
void testGetSeparationHeapTerm1();
void testGetSeparationHeapTerm2();
void testGetSeparationHeapTerm3();
TS_ASSERT_THROWS_NOTHING(d_solver->getQuantifierEliminationDisjunct(forall));
}
+void SolverBlack::testDeclareSeparationHeap()
+{
+ d_solver->setLogic("ALL_SUPPORTED");
+ Sort integer = d_solver->getIntegerSort();
+ TS_ASSERT_THROWS_NOTHING(d_solver->declareSeparationHeap(integer, integer));
+ // cannot declare separation logic heap more than once
+ TS_ASSERT_THROWS(d_solver->declareSeparationHeap(integer, integer),
+ CVC4ApiException&);
+}
+
namespace {
/**
* Helper function for testGetSeparation{Heap,Nil}TermX. Asserts and checks
void checkSimpleSeparationConstraints(Solver* solver)
{
Sort integer = solver->getIntegerSort();
+ // declare the separation heap
+ solver->declareSeparationHeap(integer, integer);
Term x = solver->mkConst(integer, "x");
Term p = solver->mkConst(integer, "p");
Term heap = solver->mkTerm(Kind::SEP_PTO, p, x);
projects / cvc5.git / commitdiff