parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...

1 files changed, 19 insertions, 6 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 1c02aa482..0faf9bebf 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -208,11 +208,17 @@ public:
   Expr getVariable(const std::string& var_name);
 
   /**
-   * Returns a sort, given a name
+   * Returns a sort, given a name.
    */
   Type getSort(const std::string& sort_name);
 
   /**
+   * Returns a sort, given a name and args.
+   */
+  Type getSort(const std::string& sort_name,
+               const std::vector<Type>& params);
+
+  /**
    * Checks if a symbol has been declared.
    * @param name the symbol name
    * @param type the symbol type
@@ -267,8 +273,10 @@ public:
   /** Create a new CVC4 variable expression of the given type. */
   Expr mkVar(const std::string& name, const Type& type);
 
-  /** Create a set of new CVC4 variable expressions of the given
-   type. */
+  /**
+   * Create a set of new CVC4 variable expressions of the given
+   * type.
+   */
   const std::vector<Expr>
   mkVars(const std::vector<std::string> names, const Type& type);
 
@@ -278,13 +286,18 @@ public:
   /** Create a new type definition. */
   void defineType(const std::string& name, const Type& type);
 
+  /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */
+  void defineParameterizedType(const std::string& name,
+                               const std::vector<Type>& params,
+                               const Type& type);
+
   /**
-   * Creates a new sort with the given name.
+   * Creates a new sort with the given name and arity.
    */
-  Type mkSort(const std::string& name);
+  Type mkSort(const std::string& name, size_t arity = 0);
 
   /**
-   * Creates a new sorts with the given names.
+   * Creates new sorts with the given names (all of arity 0).
    */
   const std::vector<Type>
   mkSorts(const std::vector<std::string>& names);