Adding support for sort U in QF_UF.

3 files changed, 18 insertions, 1 deletions

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index e2949286a..9b18eeb5a 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -208,6 +208,15 @@ AntlrParser::newSorts(const std::vector<std::string>& names) {
   return types;
 }
 
+void
+AntlrParser::setLogic(const std::string& name) {
+  if( name == "QF_UF" ) {
+    newSort("U");
+  } else {
+    Unhandled("setLogic: " + name);
+  }
+}
+
 const BooleanType* AntlrParser::booleanType() {
   return d_exprManager->booleanType(); 
 }
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index 8f1f3fa1d..e68405eb9 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -65,6 +65,13 @@ public:
   void setExpressionManager(ExprManager* expr_manager);
 
   /**
+   * Sets the logic for the current benchmark. Declares any logic symbols.
+   *
+   * @param name the name of the logic (e.g., QF_UF, AUFLIA)
+   */
+  void setLogic(const std::string& name);
+
+  /**
    * Parse a command.
    * @return a command
    */
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index be6f6cf83..301859a37 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -96,7 +96,8 @@ benchAttribute returns [Command* smt_command = 0]
   SetBenchmarkStatusCommand::BenchmarkStatus b_status = SetBenchmarkStatusCommand::SMT_UNKNOWN;
 }
   : LOGIC_ATTR logic = identifier
-    { smt_command = new SetBenchmarkLogicCommand(logic);   }
+    { setLogic(logic);
+      smt_command = new SetBenchmarkLogicCommand(logic);   }
   | ASSUMPTION_ATTR formula = annotatedFormula
     { smt_command = new AssertCommand(formula);   }
   | FORMULA_ATTR formula = annotatedFormula