summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/expr_manager_template.cpp5
-rw-r--r--src/expr/expr_manager_template.h5
-rw-r--r--src/expr/node_manager.cpp14
-rw-r--r--src/expr/node_manager.h6
-rw-r--r--src/parser/smt2/Smt2.g8
-rw-r--r--src/parser/smt2/smt2.cpp6
-rw-r--r--src/printer/smt2/smt2_printer.cpp42
-rw-r--r--src/theory/logic_info.cpp7
-rw-r--r--src/theory/quantifiers/term_database.cpp2
-rw-r--r--src/theory/sep/kinds12
-rw-r--r--src/theory/sep/theory_sep.cpp72
-rw-r--r--src/theory/sep/theory_sep.h4
-rw-r--r--src/theory/sep/theory_sep_rewriter.cpp20
-rw-r--r--src/theory/sep/theory_sep_type_rules.h28
-rw-r--r--src/theory/term_registration_visitor.cpp2
-rw-r--r--src/theory/theory_model.cpp2
16 files changed, 132 insertions, 103 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 84f674d2b..ef74575f3 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -941,6 +941,11 @@ Expr ExprManager::mkBoundVar(Type type) {
return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode));
}
+Expr ExprManager::mkSepNil(Type type) {
+ NodeManagerScope nms(d_nodeManager);
+ return Expr(this, d_nodeManager->mkSepNilPtr(*type.d_typeNode));
+}
+
Expr ExprManager::mkAssociative(Kind kind,
const std::vector<Expr>& children) {
PrettyCheckArgument(
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 04f2f4289..31c911736 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -545,6 +545,11 @@ public:
* @param type the type for the new bound variable
*/
Expr mkBoundVar(Type type);
+
+ /**
+ * Create a (nameless) new nil reference for separation logic of type
+ */
+ Expr mkSepNil(Type type);
/** Get a reference to the statistics registry for this ExprManager */
Statistics getStatistics() const throw();
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 0809a0331..d2ac7e2a1 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -681,6 +681,20 @@ Node NodeManager::mkInstConstant(const TypeNode& type) {
return n;
}
+Node NodeManager::mkSepNil(const TypeNode& type) {
+ Node n = NodeBuilder<0>(this, kind::SEP_NIL);
+ n.setAttribute(TypeAttr(), type);
+ n.setAttribute(TypeCheckedAttr(), true);
+ return n;
+}
+
+Node* NodeManager::mkSepNilPtr(const TypeNode& type) {
+ Node* n = NodeBuilder<0>(this, kind::SEP_NIL).constructNodePtr();
+ setAttribute(*n, TypeAttr(), type);
+ setAttribute(*n, TypeCheckedAttr(), true);
+ return n;
+}
+
Node NodeManager::mkAbstractValue(const TypeNode& type) {
Node n = mkConst(AbstractValue(++d_abstractValueCount));
n.setAttribute(TypeAttr(), type);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 7d2b13e4c..dcd7005f8 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -332,7 +332,7 @@ class NodeManager {
/** Create a variable with the given type. */
Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
-
+
public:
explicit NodeManager(ExprManager* exprManager);
@@ -486,6 +486,10 @@ public:
/** Create a instantiation constant with the given type. */
Node mkInstConstant(const TypeNode& type);
+
+ /** Create nil reference for separation logic with the given type. */
+ Node mkSepNil(const TypeNode& type);
+ Node* mkSepNilPtr(const TypeNode& type);
/** Make a new abstract value with the given type. */
Node mkAbstractValue(const TypeNode& type);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index b3fe59b79..29d3e45b6 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1607,10 +1607,10 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
Debug("parser") << "Empty set encountered: " << f << " "
<< f2 << " " << type << std::endl;
expr = MK_CONST( ::CVC4::EmptySet(type) );
- } else if(f.getKind() == CVC4::kind::NIL_REF) {
- //hack: We don't want the nil reference to be a constant: for instance, it could be of type Int but is not a const rational.
- // However, the expression has 0 children. So we convert to (sep_nil tmp) here.
- expr = MK_EXPR(CVC4::kind::SEP_NIL, PARSER_STATE->mkBoundVar("__tmp",type) );
+ } else if(f.getKind() == CVC4::kind::SEP_NIL_REF) {
+ //We don't want the nil reference to be a constant: for instance, it could be of type Int but is not a const rational.
+ //However, the expression has 0 children. So we convert to a SEP_NIL variable.
+ expr = EXPR_MANAGER->mkSepNil(type);
} else {
if(f.getType() != type) {
PARSER_STATE->parseError("Type ascription not satisfied.");
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 90fc11803..a46eae475 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -167,16 +167,14 @@ void Smt2::addFloatingPointOperators() {
}
void Smt2::addSepOperators() {
- //addOperator(kind::SEP_NIL, "sep.nil");
addOperator(kind::SEP_STAR, "sep");
addOperator(kind::SEP_PTO, "pto");
addOperator(kind::SEP_WAND, "wand");
- addOperator(kind::EMP_STAR, "emp");
- //Parser::addOperator(kind::SEP_NIL);
+ addOperator(kind::SEP_EMP, "emp");
Parser::addOperator(kind::SEP_STAR);
Parser::addOperator(kind::SEP_PTO);
Parser::addOperator(kind::SEP_WAND);
- Parser::addOperator(kind::EMP_STAR);
+ Parser::addOperator(kind::SEP_EMP);
}
void Smt2::addTheory(Theory theory) {
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 7b6bc8708..35e6f1a73 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -117,21 +117,26 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
// variable
if(n.isVar()) {
- string s;
- if(n.getAttribute(expr::VarNameAttr(), s)) {
- out << maybeQuoteSymbol(s);
- } else {
- if(n.getKind() == kind::VARIABLE) {
- out << "var_";
+ if( n.getKind() == kind::SEP_NIL ){
+ out << "(as sep.nil " << n.getType() << ")";
+ return;
+ }else{
+ string s;
+ if(n.getAttribute(expr::VarNameAttr(), s)) {
+ out << maybeQuoteSymbol(s);
} else {
- out << n.getKind() << '_';
+ if(n.getKind() == kind::VARIABLE) {
+ out << "var_";
+ } else {
+ out << n.getKind() << '_';
+ }
+ out << n.getId();
+ }
+ if(types) {
+ // print the whole type, but not *its* type
+ out << ":";
+ n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5);
}
- out << n.getId();
- }
- if(types) {
- // print the whole type, but not *its* type
- out << ":";
- n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5);
}
return;
@@ -291,7 +296,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
case kind::EMPTYSET:
out << "(as emptyset " << n.getConst<EmptySet>().getType() << ")";
break;
-
+
default:
// fall back on whatever operator<< does on underlying type; we
// might luck out and be SMT-LIB v2 compliant
@@ -319,11 +324,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
return;
}
- if( n.getKind() == kind::SEP_NIL ){
- out << "sep.nil";
- return;
- }
-
bool stillNeedToPrintParams = true;
bool forceBinary = false; // force N-ary to binary when outputing children
// operator
@@ -588,7 +588,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
break;
//separation
- case kind::EMP_STAR:
+ case kind::SEP_EMP:
case kind::SEP_PTO:
case kind::SEP_STAR:
case kind::SEP_WAND:out << smtKindString(k) << " "; break;
@@ -868,7 +868,7 @@ static string smtKindString(Kind k) throw() {
case kind::SEP_STAR: return "sep";
case kind::SEP_PTO: return "pto";
case kind::SEP_WAND: return "wand";
- case kind::EMP_STAR: return "emp";
+ case kind::SEP_EMP: return "emp";
default:
; /* fall through */
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 04cac7ae5..89b0f054a 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -270,7 +270,7 @@ std::string LogicInfo::getLogicString() const {
if(d_theories[THEORY_FP]) {
ss << "FP";
++seen;
- }
+ }
if(d_theories[THEORY_DATATYPES]) {
ss << "DT";
++seen;
@@ -296,7 +296,10 @@ std::string LogicInfo::getLogicString() const {
ss << "FS";
++seen;
}
-
+ if(d_theories[THEORY_SEP]) {
+ ss << "SEP";
+ ++seen;
+ }
if(seen != d_sharingTheories) {
Unhandled("can't extract a logic string from LogicInfo; at least one "
"active theory is unknown to LogicInfo::getLogicString() !");
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 9f222431e..d3a5e178f 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1925,7 +1925,7 @@ bool TermDb::containsUninterpretedConstant( Node n ) {
bool ret = false;
if( n.getKind()==UNINTERPRETED_CONSTANT ){
ret = true;
- }else if( n.getKind()!=SEP_NIL ){ //sep.nil has dummy argument FIXME
+ }else{
for( unsigned i=0; i<n.getNumChildren(); i++ ){
if( containsUninterpretedConstant( n[i] ) ){
ret = true;
diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds
index 52418aefb..4ad615c1f 100644
--- a/src/theory/sep/kinds
+++ b/src/theory/sep/kinds
@@ -11,7 +11,7 @@ properties polite stable-infinite parametric
properties check propagate presolve getNextDecisionRequest
# constants
-constant NIL_REF \
+constant SEP_NIL_REF \
::CVC4::NilRef \
::CVC4::NilRefHashFunction \
"expr/sepconst.h" \
@@ -19,16 +19,16 @@ constant NIL_REF \
rewriter ::CVC4::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter.h"
-operator SEP_NIL 1 "separation nil"
-operator EMP_STAR 1 "separation empty heap"
+variable SEP_NIL "separation nil"
+
+operator SEP_EMP 1 "separation empty heap"
operator SEP_PTO 2 "points to relation"
operator SEP_STAR 2: "separation star"
operator SEP_WAND 2 "separation magic wand"
operator SEP_LABEL 2 "separation label"
-typerule NIL_REF ::CVC4::theory::sep::NilRefTypeRule
-typerule SEP_NIL ::CVC4::theory::sep::SepNilTypeRule
-typerule EMP_STAR ::CVC4::theory::sep::EmpStarTypeRule
+typerule SEP_NIL_REF ::CVC4::theory::sep::SepNilRefTypeRule
+typerule SEP_EMP ::CVC4::theory::sep::SepEmpTypeRule
typerule SEP_PTO ::CVC4::theory::sep::SepPtoTypeRule
typerule SEP_STAR ::CVC4::theory::sep::SepStarTypeRule
typerule SEP_WAND ::CVC4::theory::sep::SepWandTypeRule
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 6fec57852..836a04afa 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -78,10 +78,10 @@ Node TheorySep::mkAnd( std::vector< TNode >& assumptions ) {
Node TheorySep::ppRewrite(TNode term) {
-/*
Trace("sep-pp") << "ppRewrite : " << term << std::endl;
+/*
Node s_atom = term.getKind()==kind::NOT ? term[0] : term;
- if( s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::EMP_STAR ){
+ if( s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::SEP_EMP ){
//get the reference type (will compute d_type_references)
int card = 0;
TypeNode tn = getReferenceType( s_atom, card );
@@ -102,7 +102,7 @@ void TheorySep::processAssertions( std::vector< Node >& assertions ) {
void TheorySep::processAssertion( Node n, std::map< Node, bool >& visited ) {
if( visited.find( n )==visited.end() ){
visited[n] = true;
- if( n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::EMP_STAR ){
+ if( n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_EMP ){
//get the reference type (will compute d_type_references)
int card = 0;
TypeNode tn = getReferenceType( n, card );
@@ -159,8 +159,41 @@ void TheorySep::explain(TNode literal, std::vector<TNode>& assumptions) {
}
}
-void TheorySep::preRegisterTerm(TNode node){
+void TheorySep::preRegisterTermRec(TNode t, std::map< TNode, bool >& visited ) {
+ if( visited.find( t )==visited.end() ){
+ visited[t] = true;
+ Trace("sep-prereg-debug") << "Preregister : " << t << std::endl;
+ if( t.getKind()==kind::SEP_NIL ){
+ Trace("sep-prereg") << "Preregister nil : " << t << std::endl;
+ //per type, all nil variable references are equal
+ TypeNode tn = t.getType();
+ std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn );
+ if( it==d_nil_ref.end() ){
+ Trace("sep-prereg") << "...set as reference." << std::endl;
+ d_nil_ref[tn] = t;
+ }else{
+ Node nr = it->second;
+ Trace("sep-prereg") << "...reference is " << nr << "." << std::endl;
+ if( t!=nr ){
+ if( d_reduce.find( t )==d_reduce.end() ){
+ d_reduce.insert( t );
+ Node lem = NodeManager::currentNM()->mkNode( tn.isBoolean() ? kind::IFF : kind::EQUAL, t, nr );
+ Trace("sep-lemma") << "Sep::Lemma: nil ref eq : " << lem << std::endl;
+ d_out->lemma( lem );
+ }
+ }
+ }
+ }else{
+ for( unsigned i=0; i<t.getNumChildren(); i++ ){
+ preRegisterTermRec( t[i], visited );
+ }
+ }
+ }
+}
+void TheorySep::preRegisterTerm(TNode term){
+ std::map< TNode, bool > visited;
+ preRegisterTermRec( term, visited );
}
@@ -241,16 +274,15 @@ void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel )
if( fullModel ){
for( std::map< TypeNode, Node >::iterator it = d_base_label.begin(); it != d_base_label.end(); ++it ){
+ Trace("sep-model") << "; Model for heap, type = " << it->first << " : " << std::endl;
computeLabelModel( it->second, d_tmodel );
- //, (label = " << it->second << ")
- Trace("sep-model") << "Model for heap, type = " << it->first << " : " << std::endl;
if( d_label_model[it->second].d_heap_locs_model.empty() ){
- Trace("sep-model") << " [empty]" << std::endl;
+ Trace("sep-model") << "; [empty]" << std::endl;
}else{
for( unsigned j=0; j<d_label_model[it->second].d_heap_locs_model.size(); j++ ){
Assert( d_label_model[it->second].d_heap_locs_model[j].getKind()==kind::SINGLETON );
Node l = d_label_model[it->second].d_heap_locs_model[j][0];
- Trace("sep-model") << " " << l << " -> ";
+ Trace("sep-model") << "; " << l << " -> ";
if( d_pto_model[l].isNull() ){
Trace("sep-model") << "_";
}else{
@@ -261,7 +293,7 @@ void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel )
}
Node nil = getNilRef( it->first );
Node vnil = d_valuation.getModel()->getRepresentative( nil );
- Trace("sep-model") << "sep.nil = " << vnil << std::endl;
+ Trace("sep-model") << "; sep.nil = " << vnil << std::endl;
Trace("sep-model") << std::endl;
}
}
@@ -302,7 +334,7 @@ void TheorySep::check(Effort e) {
bool polarity = fact.getKind() != kind::NOT;
TNode atom = polarity ? fact : fact[0];
- if( atom.getKind()==kind::EMP_STAR ){
+ if( atom.getKind()==kind::SEP_EMP ){
TypeNode tn = atom[0].getType();
if( d_emp_arg.find( tn )==d_emp_arg.end() ){
d_emp_arg[tn] = atom[0];
@@ -312,7 +344,7 @@ void TheorySep::check(Effort e) {
}
TNode s_atom = atom.getKind()==kind::SEP_LABEL ? atom[0] : atom;
TNode s_lbl = atom.getKind()==kind::SEP_LABEL ? atom[1] : TNode::null();
- bool is_spatial = s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::EMP_STAR;
+ bool is_spatial = s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::SEP_EMP;
if( is_spatial && s_lbl.isNull() ){
if( d_reduce.find( fact )==d_reduce.end() ){
Trace("sep-lemma-debug") << "Reducing unlabelled assertion " << atom << std::endl;
@@ -807,7 +839,7 @@ TheorySep::HeapAssertInfo * TheorySep::getOrMakeEqcInfo( Node n, bool doMake ) {
TypeNode TheorySep::getReferenceType( Node atom, int& card, int index ) {
Trace("sep-type") << "getReference type " << atom << " " << index << std::endl;
- Assert( atom.getKind()==kind::SEP_PTO || atom.getKind()==kind::SEP_STAR || atom.getKind()==kind::SEP_WAND || atom.getKind()==kind::EMP_STAR || index!=-1 );
+ Assert( atom.getKind()==kind::SEP_PTO || atom.getKind()==kind::SEP_STAR || atom.getKind()==kind::SEP_WAND || atom.getKind()==kind::SEP_EMP || index!=-1 );
std::map< int, TypeNode >::iterator it = d_reference_type[atom].find( index );
if( it==d_reference_type[atom].end() ){
card = 0;
@@ -890,7 +922,7 @@ TypeNode TheorySep::getReferenceType2( Node atom, int& card, int index, Node n,
visited[n] = card;
return tn1;
//return n[1].getType();
- }else if( n.getKind()==kind::EMP_STAR ){
+ }else if( n.getKind()==kind::SEP_EMP ){
card = 1;
visited[n] = card;
return n[0].getType();
@@ -998,8 +1030,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
Node TheorySep::getNilRef( TypeNode tn ) {
std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn );
if( it==d_nil_ref.end() ){
- TypeEnumerator te(tn);
- Node nil = NodeManager::currentNM()->mkNode( kind::SEP_NIL, *te );
+ Node nil = NodeManager::currentNM()->mkSepNil( tn );
d_nil_ref[tn] = nil;
return nil;
}else{
@@ -1047,7 +1078,7 @@ Node TheorySep::getLabel( Node atom, int child, Node lbl ) {
Node TheorySep::applyLabel( Node n, Node lbl, std::map< Node, Node >& visited ) {
Assert( n.getKind()!=kind::SEP_LABEL );
- if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_PTO || n.getKind()==kind::EMP_STAR ){
+ if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_EMP ){
return NodeManager::currentNM()->mkNode( kind::SEP_LABEL, n, lbl );
}else if( !n.getType().isBoolean() || n.getNumChildren()==0 ){
return n;
@@ -1084,7 +1115,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
return Node::null();
}else{
if( Trace.isOn("sep-inst") ){
- if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_PTO || n.getKind()==kind::EMP_STAR ){
+ if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_EMP ){
for( unsigned j=0; j<ind; j++ ){ Trace("sep-inst") << " "; }
Trace("sep-inst") << n << "[" << lbl << "] :: " << lbl_v << std::endl;
}
@@ -1154,7 +1185,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
Node ret = children.empty() ? NodeManager::currentNM()->mkConst( true ) : ( children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children ) );
Trace("sep-inst-debug") << "Return " << ret << std::endl;
return ret;
- }else if( n.getKind()==kind::EMP_STAR ){
+ }else if( n.getKind()==kind::SEP_EMP ){
//return NodeManager::currentNM()->mkConst( lbl_v.getKind()==kind::EMPTYSET );
return lbl_v.eqNode( NodeManager::currentNM()->mkConst(EmptySet(lbl_v.getType().toType())) );
}else{
@@ -1225,8 +1256,8 @@ void TheorySep::computeLabelModel( Node lbl, std::map< Node, Node >& tmodel ) {
if( !d_label_model[lbl].d_computed ){
d_label_model[lbl].d_computed = true;
- //Node v_val = d_valuation.getModelValue( s_lbl );
- //hack FIXME
+ //we must get the value of lbl from the model: this is being run at last call, after the model is constructed
+ //Assert(...); TODO
Node v_val = d_valuation.getModel()->getRepresentative( lbl );
Trace("sep-process") << "Model value (from valuation) for " << lbl << " : " << v_val << std::endl;
if( v_val.getKind()!=kind::EMPTYSET ){
@@ -1297,6 +1328,7 @@ bool TheorySep::areDisequal( Node a, Node b ){
return false;
}
+
void TheorySep::eqNotifyPreMerge(TNode t1, TNode t2) {
}
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 506cb77cd..852a36721 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -86,9 +86,10 @@ class TheorySep : public Theory {
/** Explain why this literal is true by adding assumptions */
void explain(TNode literal, std::vector<TNode>& assumptions);
+ void preRegisterTermRec(TNode t, std::map< TNode, bool >& visited );
public:
- void preRegisterTerm(TNode n);
+ void preRegisterTerm(TNode t);
void propagate(Effort e);
Node explain(TNode n);
@@ -274,7 +275,6 @@ private:
bool hasTerm( Node a );
bool areEqual( Node a, Node b );
bool areDisequal( Node a, Node b );
- /** called when two equivalence classes will merge */
void eqNotifyPreMerge(TNode t1, TNode t2);
void eqNotifyPostMerge(TNode t1, TNode t2);
diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp
index ce0b20cbd..d58c2c13d 100644
--- a/src/theory/sep/theory_sep_rewriter.cpp
+++ b/src/theory/sep/theory_sep_rewriter.cpp
@@ -25,7 +25,7 @@ namespace sep {
void TheorySepRewriter::getStarChildren( Node n, std::vector< Node >& s_children, std::vector< Node >& ns_children ){
Assert( n.getKind()==kind::SEP_STAR );
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( n[i].getKind()==kind::EMP_STAR ){
+ if( n[i].getKind()==kind::SEP_EMP ){
s_children.push_back( n[i] );
}else if( n[i].getKind()==kind::SEP_STAR ){
getStarChildren( n[i], s_children, ns_children );
@@ -41,7 +41,7 @@ void TheorySepRewriter::getStarChildren( Node n, std::vector< Node >& s_children
//remove empty star
std::vector< Node > temp_s_children2;
for( unsigned i=0; i<temp_s_children.size(); i++ ){
- if( temp_s_children[i].getKind()!=kind::EMP_STAR ){
+ if( temp_s_children[i].getKind()!=kind::SEP_EMP ){
temp_s_children2.push_back( temp_s_children[i] );
}
}
@@ -87,7 +87,7 @@ void TheorySepRewriter::getAndChildren( Node n, std::vector< Node >& s_children,
bool TheorySepRewriter::isSpatial( Node n, std::map< Node, bool >& visited ) {
if( visited.find( n )==visited.end() ){
visited[n] = true;
- if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_PTO || n.getKind()==kind::EMP_STAR || n.getKind()==kind::SEP_LABEL ){
+ if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_EMP || n.getKind()==kind::SEP_LABEL ){
return true;
}else if( n.getType().isBoolean() ){
for( unsigned i=0; i<n.getNumChildren(); i++ ){
@@ -104,14 +104,6 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) {
Trace("sep-postrewrite") << "Sep::postRewrite start " << node << std::endl;
Node retNode = node;
switch (node.getKind()) {
- case kind::SEP_NIL: {
- TypeEnumerator te(node[0].getType());
- Node n = *te;
- if( n!=node[0] ){
- retNode = NodeManager::currentNM()->mkNode( kind::SEP_NIL, n );
- }
- break;
- }
case kind::SEP_LABEL: {
if( node[0].getKind()==kind::SEP_PTO ){
Node s = NodeManager::currentNM()->mkNode( kind::SINGLETON, node[0][0] );
@@ -121,7 +113,7 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) {
retNode = NodeManager::currentNM()->mkNode( kind::AND, c1, c2 );
}
}
- if( node[0].getKind()==kind::EMP_STAR ){
+ if( node[0].getKind()==kind::SEP_EMP ){
retNode = node[1].eqNode( NodeManager::currentNM()->mkConst(EmptySet(node[1].getType().toType())) );
}
break;
@@ -177,9 +169,9 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) {
/*
RewriteResponse TheorySepRewriter::preRewrite(TNode node) {
- if( node.getKind()==kind::EMP_STAR ){
+ if( node.getKind()==kind::SEP_EMP ){
Trace("sep-prerewrite") << "Sep::preRewrite emp star " << std::endl;
- return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkNode( kind::EMP_STAR, NodeManager::currentNM()->mkConst( true ) ) );
+ return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkNode( kind::SEP_EMP, NodeManager::currentNM()->mkConst( true ) ) );
}else{
Trace("sep-prerewrite") << "Sep::preRewrite returning " << node << std::endl;
return RewriteResponse(REWRITE_DONE, node);
diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h
index f47941b03..7d4eb303e 100644
--- a/src/theory/sep/theory_sep_type_rules.h
+++ b/src/theory/sep/theory_sep_type_rules.h
@@ -25,7 +25,7 @@ namespace CVC4 {
namespace theory {
namespace sep {
-class NilRefTypeRule {
+class SepNilRefTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
throw (TypeCheckingExceptionPrivate, AssertionException) {
@@ -33,18 +33,11 @@ public:
}
};
-class SepNilTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- throw (TypeCheckingExceptionPrivate, AssertionException) {
- return n[0].getType(check);
- }
-};
-
-class EmpStarTypeRule {
+class SepEmpTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::SEP_EMP);
return nodeManager->booleanType();
}
};
@@ -55,14 +48,7 @@ struct SepPtoTypeRule {
Assert(n.getKind() == kind::SEP_PTO);
if( check ) {
TypeNode refType = n[0].getType(check);
- //SEP-POLY
- //if(!refType.isRef()) {
- // throw TypeCheckingExceptionPrivate(n, "pto applied to non-reference term");
- //}
TypeNode ptType = n[1].getType(check);
- //if(!ptType.isComparableTo(refType.getRefConstituentType())){
- // throw TypeCheckingExceptionPrivate(n, "pto maps reference to term of different type");
- //}
}
return nodeManager->booleanType();
}
@@ -102,14 +88,6 @@ struct SepWandTypeRule {
}
};/* struct SepWandTypeRule */
-class EmpStarInternalTypeRule {
-public:
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- throw (TypeCheckingExceptionPrivate, AssertionException) {
- return nodeManager->booleanType();
- }
-};/* struct EmpStarInternalTypeRule */
-
struct SepLabelTypeRule {
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
throw (TypeCheckingExceptionPrivate, AssertionException) {
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 7b9786247..e758002fa 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -38,7 +38,6 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
if( ( parent.getKind() == kind::FORALL ||
parent.getKind() == kind::EXISTS ||
parent.getKind() == kind::REWRITE_RULE ||
- parent.getKind() == kind::SEP_NIL ||
parent.getKind() == kind::SEP_STAR ||
parent.getKind() == kind::SEP_WAND ||
( parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean() )
@@ -183,7 +182,6 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
if( ( parent.getKind() == kind::FORALL ||
parent.getKind() == kind::EXISTS ||
parent.getKind() == kind::REWRITE_RULE ||
- parent.getKind() == kind::SEP_NIL ||
parent.getKind() == kind::SEP_STAR ||
parent.getKind() == kind::SEP_WAND ||
( parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean() )
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index a617f9455..f43a2aa7f 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -1015,7 +1015,7 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node
retNode = NodeManager::currentNM()->mkNode( r.getKind(), children );
if (childrenConst) {
retNode = Rewriter::rewrite(retNode);
- Assert(retNode.getKind()==kind::APPLY_UF || retNode.getKind()==kind::REGEXP_RANGE || retNode.getKind()==kind::SEP_NIL || retNode.isConst());
+ Assert(retNode.getKind()==kind::APPLY_UF || retNode.getKind()==kind::REGEXP_RANGE || retNode.isConst());
}
}
d_normalizedCache[r] = retNode;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback