Improve syntax for fmf cardinality constraints (#7556)

[cvc5.git] / src / parser / smt2 / smt2.h

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 2dd4bf66370fd2c765ebad59eee42abd7dbc8474..58a20cb2790a1f974c7b926e4a4afcebd5e28eaf 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -50,7 +50,7 @@ class Smt2 : public Parser
   bool d_seenSetLogic;
 
   LogicInfo d_logic;
-  std::unordered_map<std::string, api::Kind> operatorKindMap;
+  std::unordered_map<std::string, api::Kind> d_operatorKindMap;
   /**
    * Maps indexed symbols to the kind of the operator (e.g. "extract" to
    * BITVECTOR_EXTRACT).
@@ -105,6 +105,10 @@ class Smt2 : public Parser
    * @return true if higher-order support is enabled, false otherwise
    */
   bool isHoEnabled() const;
+  /**
+   * @return true if cardinality constraints are enabled, false otherwise
+   */
+  bool hasCardinalityConstraints() const;
 
   bool logicIsSet() override;
 
@@ -121,15 +125,13 @@ class Smt2 : public Parser
                               const std::vector<uint64_t>& numerals);
 
   /**
-   * Creates an indexed operator term, e.g. (_ extract 5 0).
+   * Creates an indexed operator kind, e.g. BITVECTOR_EXTRACT for "extract".
    *
    * @param name The name of the operator (e.g. "extract")
-   * @param numerals The parameters for the operator (e.g. [5, 0])
-   * @return The operator term corresponding to the indexed operator or a parse
+   * @return The kind corresponding to the indexed operator or a parse
    *         error if the name is not valid.
    */
-  api::Op mkIndexedOp(const std::string& name,
-                      const std::vector<uint64_t>& numerals);
+  api::Kind getIndexedOpKind(const std::string& name);
 
   /**
    * Returns the expression that name should be interpreted as.
@@ -205,7 +207,8 @@ class Smt2 : public Parser
    * @param name the name of the logic (e.g., QF_UF, AUFLIA)
    * @param fromCommand should be set to true if the request originates from a
    *                    set-logic command and false otherwise
-   * @return the command corresponding to setting the logic
+   * @return the command corresponding to setting the logic (if fromCommand
+   * is true), and nullptr otherwise.
    */
   Command* setLogic(std::string name, bool fromCommand = true);
 
@@ -229,12 +232,10 @@ class Smt2 : public Parser
    */
   bool v2_6(bool exact = false) const
   {
-    return language::isInputLang_smt2_6(getLanguage(), exact);
+    return d_solver->getOption("input-language") == "LANG_SMTLIB_V2_6";
   }
   /** Are we using a sygus language? */
   bool sygus() const;
-  /** Are we using the sygus version 2.0 format? */
-  bool sygus_v2() const;
 
   /**
    * Returns true if the language that we are parsing (SMT-LIB version >=2.5
@@ -414,8 +415,6 @@ class Smt2 : public Parser
 
   void addSepOperators();
 
-  InputLanguage getLanguage() const;
-
   /**
    * Utility function to create a conjunction of expressions.
    *