diff options
Diffstat (limited to 'src/parser/cvc')
-rw-r--r-- | src/parser/cvc/cvc_parser.g | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index bfdc4c0f2..9492b36d9 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -216,7 +216,7 @@ iffFormula returns [CVC4::Expr f] } : f = impliesFormula ( IFF e = iffFormula - { f = mkExpr(CVC4::IFF, f, e); } + { f = mkExpr(CVC4::kind::IFF, f, e); } )? ; @@ -230,7 +230,7 @@ impliesFormula returns [CVC4::Expr f] } : f = orFormula ( IMPLIES e = impliesFormula - { f = mkExpr(CVC4::IMPLIES, f, e); } + { f = mkExpr(CVC4::kind::IMPLIES, f, e); } )? ; @@ -246,7 +246,7 @@ orFormula returns [CVC4::Expr f] : e = xorFormula { exprs.push_back(e); } ( OR e = xorFormula { exprs.push_back(e); } )* { - f = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]); + f = (exprs.size() > 1 ? mkExpr(CVC4::kind::OR, exprs) : exprs[0]); } ; @@ -260,7 +260,7 @@ xorFormula returns [CVC4::Expr f] } : f = andFormula ( XOR e = andFormula - { f = mkExpr(CVC4::XOR,f, e); } + { f = mkExpr(CVC4::kind::XOR,f, e); } )* ; @@ -276,7 +276,7 @@ andFormula returns [CVC4::Expr f] : e = notFormula { exprs.push_back(e); } ( AND e = notFormula { exprs.push_back(e); } )* { - f = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]); + f = (exprs.size() > 1 ? mkExpr(CVC4::kind::AND, exprs) : exprs[0]); } ; @@ -290,7 +290,7 @@ notFormula returns [CVC4::Expr f] } : /* negation */ NOT f = notFormula - { f = mkExpr(CVC4::NOT, f); } + { f = mkExpr(CVC4::kind::NOT, f); } | /* a boolean atom */ f = predFormula ; @@ -302,7 +302,7 @@ predFormula returns [CVC4::Expr f] : { Expr e; } f = term (EQUAL e = term - { f = mkExpr(CVC4::EQUAL, f, e); } + { f = mkExpr(CVC4::kind::EQUAL, f, e); } )? ; // TODO: lt, gt, etc. @@ -323,7 +323,7 @@ term returns [CVC4::Expr t] LPAREN formulaList[args] RPAREN // TODO: check arity - { t = mkExpr(CVC4::APPLY, args); } + { t = mkExpr(CVC4::kind::APPLY, args); } | /* if-then-else */ t = iteTerm @@ -352,7 +352,7 @@ iteTerm returns [CVC4::Expr t] THEN iteThen = formula iteElse = iteElseTerm ENDIF - { t = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); } + { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); } ; /** @@ -367,7 +367,7 @@ iteElseTerm returns [CVC4::Expr t] | ELSEIF iteCondition = formula THEN iteThen = formula iteElse = iteElseTerm - { t = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); } + { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); } ; /** |