Adding support for sort U in QF_UF.

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index e2949286a2939d4469a0941929363e5abb2d5988..9b18eeb5a788acfbb2f5392e628f2daf11ad08d2 100644 (file)
--- 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 8f1f3fa1dd71225f27788265b188242735d4692d..e68405eb9dce15a8fadc3ea03de19494d5fdd059 100644 (file)
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -64,6 +64,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 be6f6cf83313746b5dbf2ef7120bd4523ca7cbfc..301859a376dca5ee2ed94e47822ca9ee696f467a 100644 (file)
--- 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