diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-06 09:39:03 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-06 09:39:20 -0600 |
| commit | d73fdfe7e1fe071670a7e5f843c7609db290b63e (patch) | |
| tree | ff8ad52565f6a149689668f74957292486b2eeab /src/parser/smt2 | |
| parent | 5f096cbd59afa98e8b3c7e7e7aa0b6df3c7e01b0 (diff) | |
Support for set compliment and universe set. Simplify approach for sep.nil nodes.
Diffstat (limited to 'src/parser/smt2')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 12 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 1 |
2 files changed, 11 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 735c2b2f1..92becbc68 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1775,7 +1775,9 @@ 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::SEP_NIL_REF) { + } else if(f.getKind() == CVC4::kind::UNIVERSE_SET) { + expr = EXPR_MANAGER->mkUniqueVar(type, kind::UNIVERSE_SET); + } else if(f.getKind() == CVC4::kind::SEP_NIL) { //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. @@ -2095,8 +2097,13 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | EMPTYSET_TOK { expr = MK_CONST( ::CVC4::EmptySet(Type())); } + | UNIVSET_TOK + { //booleanType is placeholder here since we don't have type info without type annotation + expr = EXPR_MANAGER->mkUniqueVar(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET); } + | NILREF_TOK - { expr = MK_CONST( ::CVC4::NilRef(Type())); } + { //booleanType is placeholder here since we don't have type info without type annotation + expr = EXPR_MANAGER->mkUniqueVar(EXPR_MANAGER->booleanType(), kind::SEP_NIL); } // NOTE: Theory constants go here ; @@ -2874,6 +2881,7 @@ FMFCARDVAL_TOK : 'fmf.card.val'; INST_CLOSURE_TOK : 'inst-closure'; EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset'; +UNIVSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'univset'; NILREF_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SEP) }? 'sep.nil'; // Other set theory operators are not // tokenized and handled directly when diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e1b824ba3..88b2479ea 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -236,6 +236,7 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::SINGLETON, "singleton"); addOperator(kind::INSERT, "insert"); addOperator(kind::CARD, "card"); + addOperator(kind::COMPLIMENT, "compliment"); break; case THEORY_DATATYPES: |