diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp index 3bd81970d..b6ec25c46 100644 --- a/src/ast/str_decl_plugin.cpp +++ b/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 & 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 & 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; diff --git a/src/ast/str_decl_plugin.h b/src/ast/str_decl_plugin.h index 57829d542..854431366 100644 --- a/src/ast/str_decl_plugin.h +++ b/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 & op_names, symbol const & logic); + + virtual void get_sort_names(svector & sort_names, symbol const & logic); // TODO }; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 77cbfe132..a7db2f16c 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/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::iterator it = fids.begin(); svector::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) { diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index f9e50e611..37dccab8a 100644 --- a/src/cmd_context/cmd_context.h +++ b/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; } diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index e6d21a1e2..5e4af91fd 100644 --- a/src/smt/smt_setup.cpp +++ b/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(); } diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index 6cbcb9602..6beb0b239 100644 --- a/src/smt/smt_setup.h +++ b/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); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp new file mode 100644 index 000000000..bc1b59551 --- /dev/null +++ b/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 */ diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h new file mode 100644 index 000000000..7bb5b5148 --- /dev/null +++ b/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_ */