load str decl plugin; recognize String sorted constants

src/ast/str_decl_plugin.cpp

@@ -66,6 +66,16 @@ app * str_decl_plugin::mk_string(const char * val) {
     return m_manager->mk_const(d);
 }
 
+void str_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
+    // TODO
+    // we would do something like:
+    // op_names.push_back(builtin_name("<=",OP_LE));
+}
+
+void str_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
+    sort_names.push_back(builtin_name("String", STRING_SORT));
+}
+
 bool str_recognizers::is_string(expr const * n, const char ** val) const {
     if (!is_app_of(n, m_afid, OP_STR))
             return false;

src/ast/str_decl_plugin.h

@@ -46,6 +46,10 @@ public:
                                          unsigned arity, sort * const * domain, sort * range);
 
     app * mk_string(const char * val);
+
+    virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
+
+    virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
     // TODO
 };
 

src/cmd_context/cmd_context.cpp

@@ -563,6 +563,10 @@ bool cmd_context::logic_has_fpa() const {
     return !has_logic() || m_logic == "QF_FP" || m_logic == "QF_FPBV";
 }
 
+bool cmd_context::logic_has_str() const {
+    return !has_logic() || m_logic == "QF_S";
+}
+
 bool cmd_context::logic_has_array_core(symbol const & s) const {
     return 
         s == "QF_AX" ||
@@ -605,6 +609,7 @@ void cmd_context::init_manager_core(bool new_manager) {
         register_plugin(symbol("datatype"), alloc(datatype_decl_plugin), logic_has_datatype());
         register_plugin(symbol("seq"),      alloc(seq_decl_plugin), logic_has_seq());
         register_plugin(symbol("fpa"),      alloc(fpa_decl_plugin), logic_has_fpa());
+        register_plugin(symbol("str"),      alloc(str_decl_plugin), logic_has_str());
     }
     else {
         // the manager was created by an external module
@@ -618,6 +623,7 @@ void cmd_context::init_manager_core(bool new_manager) {
         load_plugin(symbol("datatype"), logic_has_datatype(), fids);
         load_plugin(symbol("seq"),      logic_has_seq(), fids);
         load_plugin(symbol("fpa"),      logic_has_fpa(), fids);
+        load_plugin(symbol("str"),     logic_has_str(), fids);
         
         svector<family_id>::iterator it  = fids.begin();
         svector<family_id>::iterator end = fids.end();
@@ -671,7 +677,8 @@ bool cmd_context::supported_logic(symbol const & s) const {
         logic_has_arith_core(s) || logic_has_bv_core(s) || 
         logic_has_array_core(s) || logic_has_seq_core(s) ||
         logic_has_horn(s) ||
-        s == "QF_FP" || s == "QF_FPBV";
+        s == "QF_FP" || s == "QF_FPBV" ||
+        s == "QF_S";
 }
 
 bool cmd_context::set_logic(symbol const & s) {

src/cmd_context/cmd_context.h

@@ -242,6 +242,7 @@ protected:
     bool logic_has_array() const;
     bool logic_has_datatype() const;
     bool logic_has_fpa() const;
+    bool logic_has_str() const;
     bool supported_logic(symbol const & s) const;
 
     void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; }

src/smt/smt_setup.cpp

@@ -31,6 +31,7 @@ Revision History:
 #include"theory_dl.h"
 #include"theory_seq_empty.h"
 #include"theory_fpa.h"
+#include"theory_str.h"
 
 namespace smt {
 
@@ -117,6 +118,8 @@ namespace smt {
             setup_QF_FP();
         else if (m_logic == "QF_FPBV")
             setup_QF_FPBV();
+        else if (m_logic == "QF_S")
+            setup_QF_S();
         else
             setup_unknown();
     }
@@ -158,6 +161,8 @@ namespace smt {
                  setup_QF_BVRE();
             else if (m_logic == "QF_AUFLIA")
                 setup_QF_AUFLIA(st);
+            else if (m_logic == "QF_S")
+                setup_QF_S();
             else if (m_logic == "AUFLIA")
                 setup_AUFLIA(st);
             else if (m_logic == "AUFLIRA")
@@ -694,6 +699,11 @@ namespace smt {
         m_context.register_plugin(alloc(smt::theory_fpa, m_manager));
     }
 
+    void setup::setup_QF_S() {
+        setup_QF_LIA();
+        m_context.register_plugin(alloc(smt::theory_str, m_manager));
+    }
+
     bool is_arith(static_features const & st) {
         return st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0;
     }
@@ -800,6 +810,11 @@ namespace smt {
         m_context.register_plugin(alloc(theory_fpa, m_manager));
     }
 
+    void setup::setup_str() {
+        setup_arith();
+        m_context.register_plugin(alloc(theory_str, m_manager));
+    }
+
     void setup::setup_unknown() {
         setup_arith();
         setup_arrays();
@@ -808,6 +823,7 @@ namespace smt {
         setup_dl();
         setup_seq();
         setup_fpa();
+        setup_str();
     }
 
     void setup::setup_unknown(static_features & st) {
@@ -906,6 +922,8 @@ namespace smt {
             return;
         }
 
+        // TODO setup_str() by features
+
         setup_unknown();
     }
 

src/smt/smt_setup.h

@@ -77,6 +77,7 @@ namespace smt {
         void setup_QF_AUFLIA(static_features const & st);
         void setup_QF_FP();
         void setup_QF_FPBV();
+        void setup_QF_S();
         void setup_LRA();
         void setup_AUFLIA(bool simple_array = true);
         void setup_AUFLIA(static_features const & st);
@@ -98,6 +99,7 @@ namespace smt {
         void setup_i_arith();
         void setup_mi_arith();
         void setup_fpa();
+        void setup_str();
 
     public:
         setup(context & c, smt_params & params);

src/smt/theory_str.cpp

@@ -0,0 +1,97 @@
+/*++
+Module Name:
+
+    theory_str.cpp
+
+Abstract:
+
+    String Theory Plugin
+
+Author:
+
+    Murphy Berzish (mtrberzi) 2015-09-03
+
+Revision History:
+
+--*/
+#include"ast_smt2_pp.h"
+#include"smt_context.h"
+#include"theory_str.h"
+#include"smt_model_generator.h"
+
+namespace smt {
+
+theory_str::theory_str(ast_manager &m):
+        theory(m.mk_family_id("str"))
+{
+}
+
+theory_str::~theory_str() {
+}
+
+bool theory_str::internalize_atom(app * atom, bool gate_ctx) {
+    // TODO I have no idea if this is correct.
+    TRACE("t_str", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";);
+    SASSERT(atom->get_family_id() == get_family_id());
+
+    ast_manager & m = get_manager();
+    context & ctx = get_context();
+
+    if (ctx.b_internalized(atom))
+        return true;
+
+    unsigned num_args = atom->get_num_args();
+    for (unsigned i = 0; i < num_args; i++)
+        ctx.internalize(atom->get_arg(i), false);
+
+    literal l(ctx.mk_bool_var(atom));
+    ctx.set_var_theory(l.var(), get_id());
+
+    return true;
+}
+
+bool theory_str::internalize_term(app * term) {
+    // TODO I have no idea if this is correct either.
+    ast_manager & m = get_manager();
+    context & ctx = get_context();
+    TRACE("t_str", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";);
+    SASSERT(term->get_family_id() == get_family_id());
+    SASSERT(!ctx.e_internalized(term));
+
+    unsigned num_args = term->get_num_args();
+    for (unsigned i = 0; i < num_args; i++)
+        ctx.internalize(term->get_arg(i), false);
+
+    enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) :
+                                             ctx.mk_enode(term, false, false, true);
+
+    if (is_attached_to_var(e))
+        return false;
+
+    attach_new_th_var(e);
+
+    return true;
+}
+
+void theory_str::attach_new_th_var(enode * n) {
+    context & ctx = get_context();
+    theory_var v = mk_var(n);
+    ctx.attach_th_var(n, this, v);
+    TRACE("t_str_detail", tout << "new theory var: " << mk_ismt2_pp(n->get_owner(), get_manager()) << " := " << v << "\n";);
+}
+
+void theory_str::new_eq_eh(theory_var x, theory_var y) {
+    // TODO
+    TRACE("t_str", tout << "new eq: " << x << " = " << y << std::endl;);
+    TRACE("t_str_detail", tout << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " = " <<
+                                  mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;);
+}
+
+void theory_str::new_diseq_eh(theory_var x, theory_var y) {
+    // TODO
+    TRACE("t_str", tout << "new diseq: " << x << " != " << y << std::endl;);
+    TRACE("t_str_detail", tout << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " != " <<
+                                  mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;);
+}
+
+}; /* namespace smt */

src/smt/theory_str.h

@@ -0,0 +1,50 @@
+/*++
+Module Name:
+
+    theory_str.h
+
+Abstract:
+
+    String Theory Plugin
+
+Author:
+
+    Murphy Berzish (mtrberzi) 2015-09-03
+
+Revision History:
+
+--*/
+#ifndef _THEORY_STR_H_
+#define _THEORY_STR_H_
+
+#include"smt_theory.h"
+#include"trail.h"
+#include"th_rewriter.h"
+#include"value_factory.h"
+#include"smt_model_generator.h"
+
+namespace smt {
+
+    class str_value_factory : public value_factory {
+        // TODO
+    };
+
+    class theory_str : public theory {
+        // TODO
+    protected:
+        virtual bool internalize_atom(app * atom, bool gate_ctx);
+        virtual bool internalize_term(app * term);
+
+        virtual void new_eq_eh(theory_var, theory_var);
+        virtual void new_diseq_eh(theory_var, theory_var);
+        virtual theory* mk_fresh(context*) { return alloc(theory_str, get_manager()); }
+    public:
+        theory_str(ast_manager& m);
+        virtual ~theory_str();
+    protected:
+        void attach_new_th_var(enode * n);
+    };
+
+};
+
+#endif /* _THEORY_STR_H_ */