4 files changed, 24 insertions, 20 deletions

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 066cb3aed..6eb269bca 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -32,6 +32,7 @@
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::parser;
+using namespace CVC4::kind;
 
 namespace CVC4 {
 namespace parser {
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); }
   ;
 
 /**
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 84796f093..85b6c9865 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -124,6 +124,9 @@ Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
 Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
                              string filename) {
   istream* input = new ifstream(filename.c_str());
+  if(!*input) {
+    throw Exception("file does not exist or is unreadable: " + filename);
+  }
   return getNewParser(em, lang, input, filename, true);
 }
 
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index 39cadd47f..be6f6cf83 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -117,7 +117,7 @@ benchAttribute returns [Command* smt_command = 0]
 annotatedFormula returns [CVC4::Expr formula]
 {
   Debug("parser") << "annotated formula: " << LT(1)->getText() << endl;
-  Kind kind = UNDEFINED_KIND;
+  Kind kind = CVC4::kind::UNDEFINED_KIND;
   vector<Expr> args; 
 }
   : /* a built-in operator application */
@@ -136,7 +136,7 @@ annotatedFormula returns [CVC4::Expr formula]
     { args.push_back(f); }
     annotatedFormulas[args] RPAREN
     // TODO: check arity
-    { formula = mkExpr(CVC4::APPLY,args); }
+    { formula = mkExpr(CVC4::kind::APPLY,args); }
 
   | /* An ite expression */
     LPAREN (ITE | IF_THEN_ELSE) 
@@ -145,7 +145,7 @@ annotatedFormula returns [CVC4::Expr formula]
     trueExpr = annotatedFormula
     falseExpr = annotatedFormula
     RPAREN
-    { formula = mkExpr(CVC4::ITE, test, trueExpr, falseExpr); }
+    { formula = mkExpr(CVC4::kind::ITE, test, trueExpr, falseExpr); }
 
   | /* a variable */
     { std::string name; }
@@ -178,13 +178,13 @@ builtinOp returns [CVC4::Kind kind]
 {
   Debug("parser") << "builtin: " << LT(1)->getText() << endl;
 }
-  : NOT      { kind = CVC4::NOT;     }
-  | IMPLIES  { kind = CVC4::IMPLIES; }
-  | AND      { kind = CVC4::AND;     }
-  | OR       { kind = CVC4::OR;      }
-  | XOR      { kind = CVC4::XOR;     }
-  | IFF      { kind = CVC4::IFF;     }
-  | EQUAL    { kind = CVC4::EQUAL;   }
+  : NOT      { kind = CVC4::kind::NOT;     }
+  | IMPLIES  { kind = CVC4::kind::IMPLIES; }
+  | AND      { kind = CVC4::kind::AND;     }
+  | OR       { kind = CVC4::kind::OR;      }
+  | XOR      { kind = CVC4::kind::XOR;     }
+  | IFF      { kind = CVC4::kind::IFF;     }
+  | EQUAL    { kind = CVC4::kind::EQUAL;   }
     /* TODO: lt, gt, plus, minus, etc. */
   ;