Since ~1 year ago, we insist that the location and data types of the separation logic heap are set upfront, analogous to the set-logic command. This means that the separation logic empty heap constraint does not need to be annotated with its types.
This makes SEP_EMP a nullary Boolean operator instead of binary predicate (taking dummy arguments whose types specify the heap type). It changes the smt2 extended syntax from (_ emp T1 T2) to sep.emp.
Term Solver::mkTermFromKind(Kind kind) const
{
- CVC5_API_KIND_CHECK_EXPECTED(
- kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
+ CVC5_API_KIND_CHECK_EXPECTED(kind == PI || kind == REGEXP_EMPTY
+ || kind == REGEXP_SIGMA || kind == SEP_EMP,
+ kind)
<< "PI or REGEXP_EMPTY or REGEXP_SIGMA";
//////// all checks before this line
Node res;
+ cvc5::Kind k = extToIntKind(kind);
if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
{
- cvc5::Kind k = extToIntKind(kind);
Assert(isDefinedIntKind(k));
res = d_nodeMgr->mkNode(k, std::vector<Node>());
}
+ else if (kind == SEP_EMP)
+ {
+ res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->booleanType(), k);
+ }
else
{
Assert(kind == PI);
- res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), cvc5::kind::PI);
+ res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), k);
}
(void)res.getType(true); /* kick off type checking */
increment_term_stats(kind);
*/
SEP_NIL,
/**
- * Separation logic empty heap.
- *
- * Parameters:
- * - 1: Term of the same sort as the sort of the location of the heap
- * that is constrained to be empty
- * - 2: Term of the same sort as the data sort of the heap that is
- * that is constrained to be empty
+ * Separation logic empty heap constraint
*
* Create with:
- * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const`
- * - `Solver::mkTerm(Kind kind, const std::vector<Term>& children) const`
+ * - `Solver::mkTerm(Kind kind) const`
*/
SEP_EMP,
/**
// Constants using indexed identifiers, e.g. (_ +oo 8 24) (positive infinity
// as a 32-bit floating-point constant)
| LPAREN_TOK INDEX_TOK
- ( EMP_TOK
- sortSymbol[type,CHECK_DECLARED]
- sortSymbol[type2,CHECK_DECLARED]
- {
- // Empty heap constant in seperation logic
- api::Term v1 = SOLVER->mkConst(api::Sort(type), "_emp1");
- api::Term v2 = SOLVER->mkConst(api::Sort(type2), "_emp2");
- atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2);
- }
- | CHAR_TOK HEX_LITERAL
+ ( CHAR_TOK HEX_LITERAL
{
std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
atomTerm = PARSER_STATE->mkCharConstant(hexStr);
EXISTS_TOK : 'exists';
FORALL_TOK : 'forall';
-EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp';
CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char';
TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple';
TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_select';
// the Boolean sort is a placeholder here since we don't have type info
// without type annotation
defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort()));
+ defineVar("sep.emp", d_solver->mkTerm(api::SEP_EMP));
addSepOperators();
}
#include "expr/node.h"
#include "expr/skolem_manager.h"
#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
+#include "theory/theory_engine.h"
namespace cvc5 {
namespace preprocessing {
namespace {
-Node preSkolemEmp(Node n,
- bool pol,
- std::map<bool, std::map<Node, Node>>& visited)
+Node preSkolemEmp(TypeNode locType,
+ TypeNode dataType,
+ Node n,
+ bool pol,
+ std::map<bool, std::map<Node, Node>>& visited)
{
std::map<Node, Node>::iterator it = visited[pol].find(n);
if (it == visited[pol].end())
{
if (!pol)
{
- TypeNode tnx = n[0].getType();
- TypeNode tny = n[1].getType();
Node x =
- sm->mkDummySkolem("ex", tnx, "skolem location for negated emp");
- Node y = sm->mkDummySkolem("ey", tny, "skolem data for negated emp");
+ sm->mkDummySkolem("ex", locType, "skolem location for negated emp");
+ Node y =
+ sm->mkDummySkolem("ey", dataType, "skolem data for negated emp");
return nm
->mkNode(kind::SEP_STAR,
nm->mkNode(kind::SEP_PTO, x, y),
Node nc = n[i];
if (newHasPol)
{
- nc = preSkolemEmp(n[i], newPol, visited);
+ nc = preSkolemEmp(locType, dataType, n[i], newPol, visited);
childChanged = childChanged || nc != n[i];
}
children.push_back(nc);
PreprocessingPassResult SepSkolemEmp::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
+ TypeNode locType, dataType;
+ if (!d_preprocContext->getTheoryEngine()->getSepHeapTypes(locType, dataType))
+ {
+ Warning() << "SepSkolemEmp::applyInternal: failed to get separation logic "
+ "heap types during preprocessing"
+ << std::endl;
+ return PreprocessingPassResult::NO_CONFLICT;
+ }
std::map<bool, std::map<Node, Node>> visited;
for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
{
Node prev = (*assertionsToPreprocess)[i];
bool pol = true;
- Node next = preSkolemEmp(prev, pol, visited);
+ Node next = preSkolemEmp(locType, dataType, prev, pol, visited);
if (next != prev)
{
assertionsToPreprocess->replace(i, rewrite(next));
nullaryoperator SEP_NIL "separation nil"
-operator SEP_EMP 2 "separation empty heap"
+nullaryoperator SEP_EMP "separation logic empty heap constraint"
operator SEP_PTO 2 "points to relation"
operator SEP_STAR 2: "separation star"
operator SEP_WAND 2 "separation magic wand"
ss << d_type_ref << " -> " << d_type_data;
throw LogicException(ss.str());
}
- Node nullAtom;
- registerRefDataTypes(locT, dataT, nullAtom);
+ // otherwise set it
+ Trace("sep-type") << "Sep: assume location type " << locT
+ << " is associated with data type " << dataT << std::endl;
+ d_loc_to_data_type[locT] = dataT;
+ // for now, we only allow heap constraints of one type
+ d_type_ref = locT;
+ d_type_data = dataT;
+ d_bound_kind[locT] = bound_default;
}
TheoryRewriter* TheorySep::getTheoryRewriter() { return &d_rewriter; }
Kind k = n.getKind();
if (k == SEP_PTO || k == SEP_EMP || k == SEP_STAR || k == SEP_WAND)
{
- registerRefDataTypesAtom(n);
+ ensureHeapTypesFor(n);
}
}
void TheorySep::postProcessModel( TheoryModel* m ){
Trace("sep-model") << "Printing model for TheorySep..." << std::endl;
+ NodeManager* nm = NodeManager::currentNM();
std::vector< Node > sep_children;
Node m_neq;
Node m_heap;
}
Node nil = getNilRef( it->first );
Node vnil = d_valuation.getModel()->getRepresentative( nil );
- m_neq = NodeManager::currentNM()->mkNode( kind::EQUAL, nil, vnil );
+ m_neq = nm->mkNode(kind::EQUAL, nil, vnil);
Trace("sep-model") << "sep.nil = " << vnil << std::endl;
Trace("sep-model") << std::endl;
if( sep_children.empty() ){
TypeEnumerator te_domain( it->first );
TypeEnumerator te_range( d_loc_to_data_type[it->first] );
- m_heap = NodeManager::currentNM()->mkNode( kind::SEP_EMP, *te_domain, *te_range );
+ TypeNode boolType = nm->booleanType();
+ m_heap = nm->mkNullaryOperator(boolType, kind::SEP_EMP);
}else if( sep_children.size()==1 ){
m_heap = sep_children[0];
}else{
- m_heap = NodeManager::currentNM()->mkNode( kind::SEP_STAR, sep_children );
+ m_heap = nm->mkNode(kind::SEP_STAR, sep_children);
}
m->setHeapModel( m_heap, m_neq );
}
Trace("sep-lemma-debug")
<< "Reducing unlabelled assertion " << atom << std::endl;
// introduce top-level label, add iff
- TypeNode refType = getReferenceType(satom);
+ TypeNode refType = getReferenceType();
Trace("sep-lemma-debug")
<< "...reference type is : " << refType << std::endl;
Node b_lbl = getBaseLabel(refType);
{
std::vector<Node> children;
std::vector<Node> c_lems;
- TypeNode tn = getReferenceType(satom);
+ TypeNode tn = getReferenceType();
if (d_reference_bound_max.find(tn) != d_reference_bound_max.end())
{
c_lems.push_back(nm->mkNode(SUBSET, slbl, d_reference_bound_max[tn]));
}
else
{
- Node kl = sm->mkDummySkolem("loc", getReferenceType(satom));
- Node kd = sm->mkDummySkolem("data", getDataType(satom));
+ Node kl = sm->mkDummySkolem("loc", getReferenceType());
+ Node kd = sm->mkDummySkolem("data", getDataType());
Node econc = nm->mkNode(
SEP_LABEL,
nm->mkNode(SEP_STAR, nm->mkNode(SEP_PTO, kl, kd), d_true),
continue;
}
needAddLemma = true;
- TypeNode tn = getReferenceType(satom);
+ TypeNode tn = getReferenceType();
tn = nm->mkSetType(tn);
// tn = nm->mkSetType(nm->mkRefType(tn));
Node o_b_lbl_mval = d_label_model[slbl].getValue(tn);
}
//for now, assume all constraints are for the same heap type (ensured by logic exceptions thrown in computeReferenceType2)
-TypeNode TheorySep::getReferenceType( Node n ) {
+TypeNode TheorySep::getReferenceType() const
+{
Assert(!d_type_ref.isNull());
return d_type_ref;
}
-TypeNode TheorySep::getDataType( Node n ) {
+TypeNode TheorySep::getDataType() const
+{
Assert(!d_type_data.isNull());
return d_type_data;
}
if( it==visited[index].end() ){
Trace("sep-pp-debug") << "process assertion : " << n << ", index = " << index << std::endl;
if( n.getKind()==kind::SEP_EMP ){
- registerRefDataTypesAtom(n);
+ ensureHeapTypesFor(n);
if( hasPol && pol ){
references[index][n].clear();
references_strict[index][n] = true;
card = 1;
}
}else if( n.getKind()==kind::SEP_PTO ){
- registerRefDataTypesAtom(n);
+ ensureHeapTypesFor(n);
if( quantifiers::TermUtil::hasBoundVarAttr( n[0] ) ){
TypeNode tn1 = n[0].getType();
if( d_bound_kind[tn1]!=bound_strict && d_bound_kind[tn1]!=bound_invalid ){
}
if( !underSpatial && ( !references[index][n].empty() || card>0 ) ){
- TypeNode tn = getReferenceType( n );
+ TypeNode tn = getReferenceType();
Assert(!tn.isNull());
// add references to overall type
unsigned bt = d_bound_kind[tn];
return card;
}
-void TheorySep::registerRefDataTypesAtom(Node atom)
-{
- TypeNode tn1;
- TypeNode tn2;
- Kind k = atom.getKind();
- if (k == SEP_PTO || k == SEP_EMP)
- {
- tn1 = atom[0].getType();
- tn2 = atom[1].getType();
- }
- else
- {
- Assert(k == SEP_STAR || k == SEP_WAND);
- }
- registerRefDataTypes(tn1, tn2, atom);
-}
-
-void TheorySep::registerRefDataTypes(TypeNode tn1, TypeNode tn2, Node atom)
+void TheorySep::ensureHeapTypesFor(Node atom) const
{
- if (!d_type_ref.isNull())
+ Assert(!atom.isNull());
+ if (!d_type_ref.isNull() && !d_type_data.isNull())
{
- Assert(!atom.isNull());
- // already declared, ensure compatible
- if ((!tn1.isNull() && !tn1.isComparableTo(d_type_ref))
- || (!tn2.isNull() && !tn2.isComparableTo(d_type_data)))
+ if (atom.getKind() == SEP_PTO)
{
- std::stringstream ss;
- 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;
+ TypeNode tn1 = atom[0].getType();
+ TypeNode tn2 = atom[1].getType();
+ // already declared, ensure compatible
+ if ((!tn1.isNull() && !tn1.isComparableTo(d_type_ref))
+ || (!tn2.isNull() && !tn2.isComparableTo(d_type_data)))
+ {
+ std::stringstream ss;
+ 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())
+ else
{
+ // if not declared yet, and we have a separation logic constraint, throw
+ // an error.
std::stringstream ss;
// error, heap not declared
ss << "ERROR: the type of the separation logic heap has not been declared "
<< 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() {
if( it==d_label_map[atom][lbl].end() ){
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
- TypeNode refType = getReferenceType( atom );
+ TypeNode refType = getReferenceType();
std::stringstream ss;
ss << "__Lc" << child;
TypeNode ltn = NodeManager::currentNM()->mkSetType(refType);
std::map< Node, HeapAssertInfo * > d_eqc_info;
HeapAssertInfo * getOrMakeEqcInfo( Node n, bool doMake = false );
- //get global reference/data type
- TypeNode getReferenceType( Node n );
- TypeNode getDataType( Node n );
/**
- * Register reference data types for atom. Calls the method below for
- * the appropriate types.
+ * Ensure that reference and data types have been set to something that is
+ * non-null, and compatible with separation logic constraint atom.
*/
- void registerRefDataTypesAtom(Node atom);
+ void ensureHeapTypesFor(Node atom) const;
+ // get global reference/data type
+ TypeNode getReferenceType() const;
+ TypeNode getDataType() const;
/**
* This is called either when:
* (A) a declare-heap command is issued with tn1/tn2, and atom is null, or
;-----------------
(assert (pto w (as sep.nil Int)))
-(assert (not (and (sep (and (_ emp Int Int) (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true))))
+(assert (not (and (sep (and sep.emp (= w2 (as sep.nil Int))) (pto w w1)) (sep (pto w w2) true))))
(check-sat)
;(get-model)
(declare-sort Loc 0)
(declare-const l Loc)
(declare-heap (Loc Loc))
-(assert (sep (not (_ emp Loc Loc)) (not (_ emp Loc Loc))))
+(assert (sep (not sep.emp) (not sep.emp)))
(assert (pto l l))
(check-sat)
-; COMMAND-LINE: --quiet
+; COMMAND-LINE: --no-check-models
; EXPECT: sat
(set-logic ALL)
(declare-heap (Int Int))
-(assert (_ emp Int Int))
+(assert sep.emp)
(check-sat)
; EXPECT: sat
(set-logic QF_SEP_LIA)
(declare-heap (Int Int))
-(assert (not (_ emp Int Int)))
+(assert (not sep.emp))
(check-sat)
(declare-fun a () U)
(declare-fun b () U)
-(assert (_ emp U U))
+(assert sep.emp)
(assert (sep (pto x a) (pto y b)))
(check-sat)
; EXPECT: sat
(set-logic QF_ALL)
(declare-heap (Int Int))
-(assert (not (_ emp Int Int)))
+(assert (not sep.emp))
(check-sat)
(declare-const r Loc)
(define-fun ten-tree0 ((x Loc) (d Int)) Bool
-(or (and (_ emp Loc Node) (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and (_ emp Loc Node) (= l (as sep.nil Loc))) (and (_ emp Loc Node) (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10)))))
+(or (and sep.emp (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and sep.emp (= l (as sep.nil Loc))) (and sep.emp (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10)))))
(declare-const dy Int)
(declare-const y Loc)
(declare-const z Loc)
(define-fun ord-tree0 ((x Loc) (d Int)) Bool
-(or (and (_ emp Loc Node) (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and (_ emp Loc Node) (= y (as sep.nil Loc))) (and (_ emp Loc Node) (= z (as sep.nil Loc)))) (<= dy d) (<= d dz))))
+(or (and sep.emp (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and sep.emp (= y (as sep.nil Loc))) (and sep.emp (= z (as sep.nil Loc)))) (<= dy d) (<= d dz))))
;------- f -------
(assert (= y (as sep.nil Loc)))
; EXPECT: sat
(set-logic QF_ALL)
(declare-heap (Int Int))
-(assert (wand (_ emp Int Int) (_ emp Int Int)))
+(assert (wand sep.emp sep.emp))
(check-sat)
(declare-fun u () U)
(declare-heap (U U))
-(assert (sep (not (_ emp U U)) (not (_ emp U U))))
+(assert (sep (not sep.emp) (not sep.emp)))
(assert (forall ((x U) (y U)) (= x y)))
(declare-const l Loc)
(declare-heap (Loc Loc))
-(assert (not (_ emp Loc Loc)))
+(assert (not sep.emp))
(assert (forall ((x Loc) (y Loc)) (not (pto x y))))
(declare-fun u1 () U)
(declare-fun u2 () U)
(assert (not (= u1 u2)))
-(assert (forall ((x U)) (=> (not (= x (as sep.nil U))) (sep (not (_ emp U Int)) (pto x 0)))))
+(assert (forall ((x U)) (=> (not (= x (as sep.nil U))) (sep (not sep.emp) (pto x 0)))))
; satisfiable with heap of size 2, model of U of size 3
(check-sat)
(declare-const u Int)
-(assert (_ emp Int Int))
+(assert sep.emp)
(assert
(forall ((y Int))
(declare-const c Int)
(assert (and
- (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) (not (_ emp Int Int)) ))
+ (not (sep (not (pto x a)) (not (pto y b)) (not (sep (pto x a) (pto y b))) (not sep.emp) ))
(sep (pto x a) (pto y b))
)
)
(declare-fun u () Int)
(declare-fun v () Int)
(assert (wand (pto x u) (pto y v)))
-(assert (_ emp Int Int))
+(assert sep.emp)
(check-sat)
(set-logic QF_ALL)
(declare-heap (Int Int))
(declare-fun x () Int)
-(assert (wand (_ emp Int Int) (pto x 3)))
+(assert (wand sep.emp (pto x 3)))
(check-sat)
(set-info :status sat)
(declare-heap (Int Int))
(declare-fun x () Int)
-(assert (wand (pto x 1) (_ emp Int Int)))
+(assert (wand (pto x 1) sep.emp))
(check-sat)
(declare-fun x () Int)
(declare-heap (Int Int))
(assert (wand (pto x 1) (pto x 3)))
-(assert (_ emp Int Int))
+(assert sep.emp)
(check-sat)
projects / cvc5.git / commitdiff