diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-12 16:47:12 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-12 16:47:12 -0500 |
| commit | 75db964b0c56f1a3b04b77c33d226c4d9cd0ca54 (patch) | |
| tree | c30f7f17ae963e3f51cef111b2d549eacff1a852 /src/parser | |
| parent | e6e02c32c58f9e5edde2dd85fc7b19ef001eea03 (diff) | |
Add nullary operator metakind.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 4 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 8 |
2 files changed, 6 insertions, 6 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index a5d5febe9..2dc74afdb 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1839,7 +1839,7 @@ postfixTerm[CVC4::Expr& f] } 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); + f = EXPR_MANAGER->mkNullaryOperator(t, kind::UNIVERSE_SET); } else { if(f.getType() != t) { PARSER_STATE->parseError("Type ascription not satisfied."); @@ -2075,7 +2075,7 @@ simpleTerm[CVC4::Expr& f] { f = MK_CONST(EmptySet(Type())); } | UNIVSET_TOK { //booleanType is placeholder - f = EXPR_MANAGER->mkUniqueVar(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET); + f = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET); } /* finite set literal */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 33674770d..740e35ba4 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1868,12 +1868,12 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] << f2 << " " << type << std::endl; expr = MK_CONST( ::CVC4::EmptySet(type) ); } else if(f.getKind() == CVC4::kind::UNIVERSE_SET) { - expr = EXPR_MANAGER->mkUniqueVar(type, kind::UNIVERSE_SET); + expr = EXPR_MANAGER->mkNullaryOperator(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. - expr = EXPR_MANAGER->mkUniqueVar(type, kind::SEP_NIL); + expr = EXPR_MANAGER->mkNullaryOperator(type, kind::SEP_NIL); } else { if(f.getType() != type) { PARSER_STATE->parseError("Type ascription not satisfied."); @@ -2304,11 +2304,11 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | 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); } + expr = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET); } | NILREF_TOK { //booleanType is placeholder here since we don't have type info without type annotation - expr = EXPR_MANAGER->mkUniqueVar(EXPR_MANAGER->booleanType(), kind::SEP_NIL); } + expr = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->booleanType(), kind::SEP_NIL); } // NOTE: Theory constants go here ; |