4 files changed, 36 insertions, 40 deletions
diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index 3ea6dc940..f081f493f 100644
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -2,7 +2,9 @@ AM_CPPFLAGS = \
 	-D__BUILDING_CVC4PARSERLIB \
 	-I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES)
 AM_CXXFLAGS = -Wall -fvisibility=hidden
+
 # Compile generated C files using C++ compiler
+AM_CFLAGS = $(AM_CXXFLAGS)
 CC=$(CXX)
 
 noinst_LTLIBRARIES = libparsersmt.la
@@ -30,17 +32,17 @@ BUILT_SOURCES = $(ANTLR_STUFF)
 dist-hook: $(ANTLR_STUFF)
 MAINTAINERCLEANFILES = $(ANTLR_STUFF)
 maintainer-clean-local:
-	-rmdir @srcdir@/generated
-	-rm -f @srcdir@/stamp-generated
+	-$(AM_V_at)rmdir @srcdir@/generated
+	-$(AM_V_at)rm -f @srcdir@/stamp-generated
 
 @srcdir@/stamp-generated:
-	mkdir -p @srcdir@/generated
-	touch @srcdir@/stamp-generated
+	$(AM_V_at)mkdir -p @srcdir@/generated
+	$(AM_V_at)touch @srcdir@/stamp-generated
 
 # antlr doesn't overwrite output files, it just leaves them.  So we have to delete them first.
 @srcdir@/generated/SmtLexer.h: Smt.g @srcdir@/stamp-generated
-	-rm -f $(ANTLR_STUFF)
-	$(ANTLR) -o "@srcdir@/generated" "@srcdir@/Smt.g"
+	-$(AM_V_at)rm -f $(ANTLR_STUFF)
+	$(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/Smt.g"
 
 # These don't actually depend on SmtLexer.h, but if we're doing parallel
 # make and the lexer needs to be rebuilt, we have to keep the rules
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 789e01670..48a0eddef 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -74,6 +74,8 @@ using namespace CVC4::parser;
 #define EXPR_MANAGER ANTLR_INPUT->getExprManager()
 #undef MK_EXPR
 #define MK_EXPR EXPR_MANAGER->mkExpr
+#undef MK_CONST
+#define MK_CONST EXPR_MANAGER->mkConst
 }
 
 /**
@@ -206,8 +208,8 @@ annotatedFormula[CVC4::Expr& expr]
     { expr = ANTLR_INPUT->getVariable(name); }
 
     /* constants */
-  | TRUE_TOK          { expr = MK_EXPR(CVC4::kind::TRUE); }
-  | FALSE_TOK         { expr = MK_EXPR(CVC4::kind::FALSE); }
+  | TRUE_TOK          { expr = MK_CONST(true); }
+  | FALSE_TOK         { expr = MK_CONST(false); }
     /* TODO: let, flet, quantifiers, arithmetic constants */
   ;
 
diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp
index db4d89860..cd62eec39 100644
--- a/src/parser/smt/smt_input.cpp
+++ b/src/parser/smt/smt_input.cpp
@@ -1,10 +1,3 @@
-/*
- * smt_parser.cpp
- *
- *  Created on: Mar 5, 2010
- *      Author: chris
- */
-
 #include <antlr3.h>
 
 #include "expr/expr_manager.h"
@@ -65,6 +58,5 @@ Expr SmtInput::doParseExpr() throw (ParserException) {
   return d_pSmtParser->parseExpr(d_pSmtParser);
 }
 
-} // namespace parser
-
-} // namespace CVC4
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h
index 4795edc91..3e295d18a 100644
--- a/src/parser/smt/smt_input.h
+++ b/src/parser/smt/smt_input.h
@@ -1,12 +1,7 @@
-/*
- * smt_parser.h
- *
- *  Created on: Mar 5, 2010
- *      Author: chris
- */
+#include "cvc4parser_public.h"
 
-#ifndef SMT_PARSER_H_
-#define SMT_PARSER_H_
+#ifndef __CVC4__PARSER__SMT_INPUT_H
+#define __CVC4__PARSER__SMT_INPUT_H
 
 #include "parser/antlr_input.h"
 #include "parser/smt/generated/SmtLexer.h"
@@ -32,7 +27,8 @@ class SmtInput : public AntlrInput {
 
 public:
 
-  /** Create a file input.
+  /**
+   * Create a file input.
    *
    * @param exprManager the manager to use when building expressions from the input
    * @param filename the path of the file to read
@@ -41,7 +37,8 @@ public:
    */
   SmtInput(ExprManager* exprManager, const std::string& filename, bool useMmap);
 
-  /** Create a string input.
+  /**
+   * Create a string input.
    *
    * @param exprManager the manager to use when building expressions from the input
    * @param input the string to read
@@ -49,20 +46,22 @@ public:
    */
   SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name);
 
-  /* Destructor. Frees the lexer and the parser. */
+  /** Destructor. Frees the lexer and the parser. */
   ~SmtInput();
 
 protected:
 
-  /** Parse a command from the input. Returns <code>NULL</code> if there is
-   * no command there to parse.
+  /**
+   * Parse a command from the input. Returns <code>NULL</code> if
+   * there is no command there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
    */
   Command* doParseCommand() throw(ParserException);
 
-  /** Parse an expression from the input. Returns a null <code>Expr</code>
-   * if there is no expression there to parse.
+  /**
+   * Parse an expression from the input. Returns a null
+   * <code>Expr</code> if there is no expression there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
    */
@@ -70,14 +69,15 @@ protected:
 
 private:
 
-  /** Initialize the class. Called from the constructors once the input stream
-   * is initialized. */
+  /**
+   * Initialize the class. Called from the constructors once the input
+   * stream is initialized.
+   */
   void init();
 
-}; // class SmtInput
-
-} // namespace parser
+};/* class SmtInput */
 
-} // namespace CVC4
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
 
-#endif /* SMT_PARSER_H_ */
+#endif /* __CVC4__PARSER__SMT_INPUT_H */