create and register string theory plugin

the parser gets a little bit further now!
rejects input with "unexpected character"

.gitignore

@@ -75,5 +75,6 @@ src/api/ml/z3.mllib
 doc/api
 doc/code
 # reference code for z3str2
+Z3-str
 Z3-str/**
 

src/ast/ast.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include<sstream>
+#include<cstring>
 #include"ast.h"
 #include"ast_pp.h"
 #include"ast_ll_pp.h"
@@ -58,6 +59,7 @@ parameter& parameter::operator=(parameter const& other) {
     case PARAM_SYMBOL: new (m_symbol) symbol(other.get_symbol()); break;
     case PARAM_RATIONAL: new (m_rational) rational(other.get_rational()); break;
     case PARAM_DOUBLE: m_dval = other.m_dval; break;
+    case PARAM_STRING: m_string = other.m_string; break;
     case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break;
     default:
         UNREACHABLE();
@@ -90,6 +92,7 @@ bool parameter::operator==(parameter const & p) const {
     case PARAM_SYMBOL: return get_symbol() == p.get_symbol();
     case PARAM_RATIONAL: return get_rational() == p.get_rational();
     case PARAM_DOUBLE: return m_dval == p.m_dval;
+    case PARAM_STRING: return (m_string == NULL && p.m_string == NULL) || strcmp(m_string, p.m_string)==0;
     case PARAM_EXTERNAL: return m_ext_id == p.m_ext_id;
     default: UNREACHABLE(); return false;
     }
@@ -103,6 +106,7 @@ unsigned parameter::hash() const {
     case PARAM_SYMBOL:   b = get_symbol().hash(); break;
     case PARAM_RATIONAL: b = get_rational().hash(); break;
     case PARAM_DOUBLE:   b = static_cast<unsigned>(m_dval); break;
+    case PARAM_STRING:   /* TODO */ b = 42; break;
     case PARAM_EXTERNAL: b = m_ext_id; break;
     }
     return (b << 2) | m_kind;
@@ -115,6 +119,7 @@ std::ostream& parameter::display(std::ostream& out) const {
     case PARAM_RATIONAL: return out << get_rational();
     case PARAM_AST:      return out << "#" << get_ast()->get_id();
     case PARAM_DOUBLE:   return out << m_dval;
+    case PARAM_STRING:   return out << m_string;
     case PARAM_EXTERNAL: return out << "@" << m_ext_id;
     default:
         UNREACHABLE();

src/ast/ast.h

@@ -86,6 +86,7 @@ public:
         PARAM_SYMBOL,
         PARAM_RATIONAL,
         PARAM_DOUBLE,
+        PARAM_STRING,
         // PARAM_EXTERNAL is used for handling decl_plugin specific parameters.
         // For example, it is used for handling mpf numbers in float_decl_plugin,
         // and irrational algebraic numbers in arith_decl_plugin.
@@ -104,6 +105,7 @@ private:
         char         m_symbol[sizeof(symbol)];      // for PARAM_SYMBOL
         char         m_rational[sizeof(rational)];  // for PARAM_RATIONAL
         double       m_dval;   // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin)
+        const char*  m_string; // for PARAM_STRING
         unsigned     m_ext_id; // for PARAM_EXTERNAL
     };
 
@@ -116,6 +118,7 @@ public:
     explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL) { new (m_symbol) symbol(s); }
     explicit parameter(rational const & r): m_kind(PARAM_RATIONAL) { new (m_rational) rational(r); }
     explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {}
+    explicit parameter(const char *s):m_kind(PARAM_STRING), m_string(s) {}
     explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}
     parameter(parameter const&);
 
@@ -129,6 +132,7 @@ public:
     bool is_symbol() const { return m_kind == PARAM_SYMBOL; }
     bool is_rational() const { return m_kind == PARAM_RATIONAL; }
     bool is_double() const { return m_kind == PARAM_DOUBLE; }
+    bool is_string() const { return m_kind == PARAM_STRING; }
     bool is_external() const { return m_kind == PARAM_EXTERNAL; }
     
     bool is_int(int & i) const { return is_int() && (i = get_int(), true); }
@@ -136,6 +140,7 @@ public:
     bool is_symbol(symbol & s) const { return is_symbol() && (s = get_symbol(), true); }
     bool is_rational(rational & r) const { return is_rational() && (r = get_rational(), true); }
     bool is_double(double & d) const { return is_double() && (d = get_double(), true); }
+    // TODO is_string(char*)
     bool is_external(unsigned & id) const { return is_external() && (id = get_ext_id(), true); }
 
     /**
@@ -155,6 +160,7 @@ public:
     symbol const & get_symbol() const { SASSERT(is_symbol()); return *(reinterpret_cast<const symbol *>(m_symbol)); }
     rational const & get_rational() const { SASSERT(is_rational()); return *(reinterpret_cast<const rational *>(m_rational)); }
     double get_double() const { SASSERT(is_double()); return m_dval; }
+    const char * get_string() const { SASSERT(is_string()); return m_string; }
     unsigned get_ext_id() const { SASSERT(is_external()); return m_ext_id; }
 
     bool operator==(parameter const & p) const;

src/ast/reg_decl_plugins.cpp

@@ -25,6 +25,7 @@ Revision History:
 #include"dl_decl_plugin.h"
 #include"seq_decl_plugin.h"
 #include"fpa_decl_plugin.h"
+#include"str_decl_plugin.h"
 
 void reg_decl_plugins(ast_manager & m) {
     if (!m.get_plugin(m.mk_family_id(symbol("arith")))) {
@@ -48,4 +49,7 @@ void reg_decl_plugins(ast_manager & m) {
     if (!m.get_plugin(m.mk_family_id(symbol("fpa")))) {
         m.register_plugin(symbol("fpa"), alloc(fpa_decl_plugin));
     }
+    if (!m.get_plugin(m.mk_family_id(symbol("str")))) {
+        m.register_plugin(symbol("str"), alloc(str_decl_plugin));
+    }
 }

src/ast/str_decl_plugin.cpp

@@ -0,0 +1,74 @@
+/*++
+Module Name:
+
+    str_decl_plugin.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Murphy Berzish (mtrberzi) 2015-09-02.
+
+Revision History:
+
+--*/
+#include<sstream>
+#include"str_decl_plugin.h"
+#include"string_buffer.h"
+#include"warning.h"
+#include"ast_pp.h"
+#include"ast_smt2_pp.h"
+
+str_decl_plugin::str_decl_plugin():
+    m_strv_sym("String"),
+    m_str_decl(0){
+}
+
+str_decl_plugin::~str_decl_plugin(){
+}
+
+void str_decl_plugin::finalize(void) {
+    #define DEC_REF(decl) if (decl) { m_manager->dec_ref(decl); } ((void) 0)
+    DEC_REF(m_str_decl);
+}
+
+void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
+    decl_plugin::set_manager(m, id);
+    m_str_decl = m->mk_sort(symbol("String"), sort_info(id, STRING_SORT));
+    m->inc_ref(m_str_decl);
+    sort * s = m_str_decl;
+    /* TODO mk_pred, etc. */
+}
+
+decl_plugin * str_decl_plugin::mk_fresh() {
+    return alloc(str_decl_plugin);
+}
+
+sort * str_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
+    switch (k) {
+    case STRING_SORT: return m_str_decl;
+    default: return 0;
+    }
+}
+
+func_decl * str_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
+                                         unsigned arity, sort * const * domain, sort * range) {
+    /* TODO */
+    m_manager->raise_exception("str_decl_plugin::mk_func_decl() not yet implemented"); return 0;
+}
+
+app * str_decl_plugin::mk_string(const char * val) {
+    parameter p[1] = {parameter(val)};
+    func_decl * d;
+    d = m_manager->mk_const_decl(m_strv_sym, m_str_decl, func_decl_info(m_family_id, OP_STR, 1, p));
+    return m_manager->mk_const(d);
+}
+
+str_util::str_util(ast_manager &m) :
+    str_recognizers(m.mk_family_id(symbol("str"))),
+    m_manager(m) {
+    SASSERT(m.has_plugin(symbol("str")));
+    m_plugin = static_cast<str_decl_plugin*>(m.get_plugin(m.mk_family_id(symbol("str"))));
+}

src/ast/str_decl_plugin.h

@@ -0,0 +1,75 @@
+/*++
+Module Name:
+
+    str_decl_plugin.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Murphy Berzish (mtrberzi) 2015-09-02.
+
+Revision History:
+
+--*/
+#ifndef _STR_DECL_PLUGIN_H_
+#define _STR_DECL_PLUGIN_H_
+
+#include"ast.h"
+
+enum str_sort_kind {
+   STRING_SORT,
+};
+
+enum str_op_kind {
+    OP_STR, /* string constants */
+
+    LAST_STR_OP
+};
+
+class str_decl_plugin : public decl_plugin {
+protected:
+    symbol m_strv_sym;
+    sort * m_str_decl;
+
+    virtual void set_manager(ast_manager * m, family_id id);
+public:
+    str_decl_plugin();
+    virtual ~str_decl_plugin();
+    virtual void finalize();
+
+    virtual decl_plugin * mk_fresh();
+    virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
+    virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
+                                         unsigned arity, sort * const * domain, sort * range);
+
+    app * mk_string(const char * val);
+    // TODO
+};
+
+class str_recognizers {
+    family_id m_afid;
+public:
+    str_recognizers(family_id fid):m_afid(fid) {}
+    family_id get_fid() const { return m_afid; }
+    family_id get_family_id() const { return get_fid(); }
+    // TODO
+};
+
+class str_util : public str_recognizers {
+    ast_manager & m_manager;
+    str_decl_plugin * m_plugin;
+public:
+    str_util(ast_manager & m);
+    ast_manager & get_manager() const { return m_manager; }
+    str_decl_plugin & plugin() { return *m_plugin; }
+
+    app * mk_string(const char * val) {
+        return m_plugin->mk_string(val);
+    }
+    // TODO
+};
+
+#endif /* _STR_DECL_PLUGIN_H_ */

src/parsers/smt2/smt2parser.cpp

@@ -22,6 +22,7 @@ Revision History:
 #include"datatype_decl_plugin.h"
 #include"bv_decl_plugin.h"
 #include"arith_decl_plugin.h"
+#include"str_decl_plugin.h"
 #include"ast_pp.h"
 #include"well_sorted.h"
 #include"pattern_validation.h"
@@ -64,6 +65,7 @@ namespace smt2 {
 
         scoped_ptr<bv_util>               m_bv_util;
         scoped_ptr<arith_util>            m_arith_util;
+        scoped_ptr<str_util>              m_str_util;
         scoped_ptr<pattern_validator>     m_pattern_validator;
         scoped_ptr<var_shifter>           m_var_shifter;
 
@@ -272,6 +274,12 @@ namespace smt2 {
             return *(m_bv_util.get());
         }
 
+        str_util & strutil() {
+            if (m_str_util.get() == 0)
+                m_str_util = alloc(str_util, m());
+            return *(m_str_util.get());
+        }
+
         pattern_validator & pat_validator() {
             if (m_pattern_validator.get() == 0) {
                 m_pattern_validator = alloc(pattern_validator, m());
@@ -1054,6 +1062,13 @@ namespace smt2 {
             next();
         }
 
+        void parse_string() {
+            SASSERT(curr() == scanner::STRING_TOKEN);
+            TRACE("parse_string", tout << "new string constant: " << m_scanner.get_string() << "\n";);
+            expr_stack().push_back(strutil().mk_string(m_scanner.get_string()));
+            next();
+        }
+
         void push_pattern_frame() {
             // TODO: It seems the only reliable way to parse patterns is:
             // Parse as an S-Expr, then try to convert it to an useful pattern.
@@ -1713,6 +1728,9 @@ namespace smt2 {
                         case scanner::BV_TOKEN:
                             parse_bv_numeral();
                             break;
+                        case scanner::STRING_TOKEN:
+                            parse_string();
+                            break;
                         case scanner::LEFT_PAREN:
                             push_expr_frame(m_num_expr_frames == 0 ? 0 : static_cast<expr_frame*>(m_stack.top()));
                             break;