Support for separation logic. Enable cbqi by default for pure BV.

3 files changed, 33 insertions, 2 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 41428ed89..b3fe59b79 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1607,6 +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.getType() != type) {
           PARSER_STATE->parseError("Type ascription not satisfied.");
@@ -1911,6 +1915,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   | EMPTYSET_TOK
     { expr = MK_CONST( ::CVC4::EmptySet(Type())); }
 
+  | NILREF_TOK
+    { expr = MK_CONST( ::CVC4::NilRef(Type())); }
     // NOTE: Theory constants go here
   ;
 
@@ -2646,6 +2652,7 @@ FMFCARDVAL_TOK : 'fmf.card.val';
 INST_CLOSURE_TOK : 'inst-closure';
 
 EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
+NILREF_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SEP) }? 'sep.nil';
 // Other set theory operators are not
 // tokenized and handled directly when
 // processing a term
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 2da44152a..90fc11803 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -166,6 +166,18 @@ void Smt2::addFloatingPointOperators() {
   Parser::addOperator(kind::FLOATINGPOINT_TO_SBV);
 }
 
+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);
+  Parser::addOperator(kind::SEP_STAR);
+  Parser::addOperator(kind::SEP_PTO);
+  Parser::addOperator(kind::SEP_WAND);
+  Parser::addOperator(kind::EMP_STAR);
+}
 
 void Smt2::addTheory(Theory theory) {
   switch(theory) {
@@ -254,7 +266,11 @@ void Smt2::addTheory(Theory theory) {
     defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
     addFloatingPointOperators();
     break;
-
+    
+  case THEORY_SEP:
+    addSepOperators();
+    break;
+    
   default:
     std::stringstream ss;
     ss << "internal error: unsupported theory " << theory;
@@ -307,6 +323,8 @@ bool Smt2::isTheoryEnabled(Theory theory) const {
     return d_logic.isTheoryEnabled(theory::THEORY_UF);
   case THEORY_FP:
     return d_logic.isTheoryEnabled(theory::THEORY_FP);
+  case THEORY_SEP:
+    return d_logic.isTheoryEnabled(theory::THEORY_SEP);
   default:
     std::stringstream ss;
     ss << "internal error: unsupported theory " << theory;
@@ -415,6 +433,10 @@ void Smt2::setLogic(std::string name) {
     addTheory(THEORY_FP);
   }
 
+  if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) {
+    addTheory(THEORY_SEP);
+  }
+  
 }/* Smt2::setLogic() */
 
 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 1ae2c9dd7..b99e142ba 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -51,7 +51,8 @@ public:
     THEORY_SETS,
     THEORY_STRINGS,
     THEORY_UF,
-    THEORY_FP
+    THEORY_FP,
+    THEORY_SEP
   };
 
 private:
@@ -344,6 +345,7 @@ private:
 
   void addFloatingPointOperators();
 
+  void addSepOperators();
 };/* class Smt2 */
 
 }/* CVC4::parser namespace */