From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Tue, 9 Mar 2010 23:10:13 +0000 (+0000)
Subject: Adding support for sort U in QF_UF.
X-Git-Tag: cvc5-1.0.0~9191
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4ab7098ce928d69183d604e6b49b283f2f1283a6;p=cvc5.git

Adding support for sort U in QF_UF.
---

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
@@ -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 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