Cleanup from last commit, treat sep.nil as variable kind.

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 84f674d2bb944efcd5327dad40c25adc49fb177f..ef74575f3de7cbb329966a5bda69769592b37402 100644 (file)
--- 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 04f2f4289d0137cd29279e893e0e0f730847a985..31c911736648c95d975959fecb68448dbdaa369c 100644 (file)
--- 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 0809a03318a56697cb00f38ee0467a0ddf6bd6e6..d2ac7e2a127c81cea62362f2b7a5540170ae6183 100644 (file)
--- 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 7d2b13e4c4998da7c7dfe17d3ffb669dea7b6c99..dcd7005f851879e0cc3317af593808da84344560 100644 (file)
--- 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 b3fe59b79890f2692d4b7a849c1fff92d66aa68b..29d3e45b6baac6124cca8333038b6f1e8d48b815 100644 (file)
--- 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 90fc118033637955168609c38b040b8806f6fd35..a46eae4754968a162809edcfd5e1cea35ed9c849 100644 (file)
--- 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 7b6bc8708f1b11455a71a78acff1239225f4d261..35e6f1a73076acbf927389d699b243e7640cbb39 100644 (file)
--- 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 04cac7ae56fcfed6591c938d84e794f1c0a01fea..89b0f054ac29d9266d960c375ea6e66c35493279 100644 (file)
--- 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 9f222431e4162220c0633e72936c24bb8e02348a..d3a5e178f2125c671d6d5a4292a49b39ba833d14 100644 (file)
--- 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 52418aefbafbca715b25740953e527bf084e9e2e..4ad615c1f983a16cee0d297af2ad261bdc56b96e 100644 (file)
--- 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 6fec57852ffe2dd8918ee012d6e6957466413101..836a04afad17034b8abbf23c01fac79dab500244 100644 (file)
--- 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 506cb77cd034fb389c8f33d7da5512a3019fabcd..852a36721e66b3799891cebc4cbc5a03f5def31d 100644 (file)
--- 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 ce0b20cbd5e6b7db7f83c13ad4d571a9a3106ee1..d58c2c13d310bae1b379a80cfa63a992379da7fc 100644 (file)
--- 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 f47941b0338d84778ea9af194a6c4d8ee0f9f61d..7d4eb303e5a227bdda9f010f1c6989e7e146ed0c 100644 (file)
--- 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 7b97862478eb43c07cadd495010452630e23bc17..e758002fa49e1dc0005e60a2110affe3dd2ef118 100644 (file)
--- 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 a617f94554938ae6d15420eb080f1bc5d3b191b0..f43a2aa7f6e55816a3149545bcabc64aeffaac51 100644 (file)
--- 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;