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/cvc | |
| parent | 5f096cbd59afa98e8b3c7e7e7aa0b6df3c7e01b0 (diff) | |
Support for set compliment and universe set. Simplify approach for sep.nil nodes.
Diffstat (limited to 'src/parser/cvc')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 3a8f3a794..0655359a9 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -245,6 +245,7 @@ tokens { SETS_CARD_TOK = 'CARD'; FMF_CARD_TOK = 'HAS_CARD'; + UNIVSET_TOK = 'UNIVERSE'; // these are parsed by special NUMBER_OR_RANGEOP rule, below DECIMAL_LITERAL; @@ -440,6 +441,7 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em, Expr rhs = createPrecedenceTree(parser, em, expressions, operators, pivot + 1, stopIndex); switch(k) { + case kind::NOT : if(lhs.getType().isSet()) { k = kind::COMPLIMENT; } break; case kind::LEQ : if(lhs.getType().isSet()) { k = kind::SUBSET; } break; case kind::MINUS : if(lhs.getType().isSet()) { k = kind::SETMINUS; } break; case kind::BITVECTOR_AND: if(lhs.getType().isSet()) { k = kind::INTERSECTION; } break; @@ -1832,6 +1834,8 @@ postfixTerm[CVC4::Expr& f] f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v); } else if(f.getKind() == CVC4::kind::EMPTYSET && t.isSet()) { f = MK_CONST(CVC4::EmptySet(t)); + } else if(f.getKind() == CVC4::kind::UNIVERSE_SET && t.isSet()) { + f = EXPR_MANAGER->mkUniqueVar(t, kind::UNIVERSE_SET); } else { if(f.getType() != t) { PARSER_STATE->parseError("Type ascription not satisfied."); @@ -2065,6 +2069,10 @@ simpleTerm[CVC4::Expr& f] /* empty set literal */ | LBRACE RBRACE { f = MK_CONST(EmptySet(Type())); } + | UNIVSET_TOK + { //booleanType is placeholder + f = EXPR_MANAGER->mkUniqueVar(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET); + } /* finite set literal */ | LBRACE formula[f] { args.push_back(f); } |