diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-06-17 15:55:56 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-06-17 15:57:28 -0500 |
commit | 1a2547995acc5a98c8969e628ac5e1c45b0efe94 (patch) | |
tree | 0d9abd19ba7b3b742da3e745da00c0457237f84b /src/parser | |
parent | 0348b525a951a8709f9dc4b5757ce0bcb48a9472 (diff) |
Support for separation logic. Enable cbqi by default for pure BV.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 7 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 24 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 4 |
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 */ |