mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

add Length function to theory of strings

Browse source
This commit is contained in:
Murphy Berzish 2015-09-07 16:13:48 -04:00
parent 7f0d9157ac
commit dc86385e7f
4 changed files with 62 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ast/str_decl_plugin.cpp
View file

@ -33,6 +33,9 @@ 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);
DEC_REF(m_concat_decl);
DEC_REF(m_length_decl);
DEC_REF(m_int_sort);
}
void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
@ -41,11 +44,19 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
m->inc_ref(m_str_decl);
sort * s = m_str_decl;
m_arith_fid = m_manager->mk_family_id("arith");
m_int_sort = m_manager->mk_sort(m_arith_fid, INT_SORT);
SASSERT(m_int_sort != 0); // arith_decl_plugin must be installed before str_decl_plugin.
m_manager->inc_ref(m_int_sort);
sort * i = m_int_sort;
#define MK_OP(FIELD, NAME, KIND, SORT) \
FIELD = m->mk_func_decl(symbol(NAME), SORT, SORT, SORT, func_decl_info(id, KIND)); \
m->inc_ref(FIELD)
MK_OP(m_concat_decl, "Concat", OP_STRCAT, s);
m_length_decl = m->mk_func_decl(symbol("Length"), s, i); m_manager->inc_ref(m_length_decl);
}
decl_plugin * str_decl_plugin::mk_fresh() {
@ -62,6 +73,7 @@ sort * str_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
func_decl * str_decl_plugin::mk_func_decl(decl_kind k) {
switch(k) {
case OP_STRCAT: return m_concat_decl;
case OP_STRLEN: return m_length_decl;
default: return 0;
}
}
@ -88,6 +100,7 @@ app * str_decl_plugin::mk_string(const char * val) {
void str_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
op_names.push_back(builtin_name("Concat", OP_STRCAT));
op_names.push_back(builtin_name("Length", OP_STRLEN));
}
void str_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {

6
src/ast/str_decl_plugin.h
View file

@ -18,6 +18,7 @@ Revision History:
#define _STR_DECL_PLUGIN_H_
#include"ast.h"
#include"arith_decl_plugin.h"
enum str_sort_kind {
STRING_SORT,
@ -27,6 +28,7 @@ enum str_op_kind {
OP_STR, /* string constants */
//
OP_STRCAT,
OP_STRLEN,
LAST_STR_OP
};
@ -35,7 +37,11 @@ protected:
symbol m_strv_sym;
sort * m_str_decl;
sort * m_int_sort;
family_id m_arith_fid;
func_decl * m_concat_decl;
func_decl * m_length_decl;
virtual void set_manager(ast_manager * m, family_id id);

37
src/smt/theory_str.cpp
View file

@ -31,7 +31,7 @@ 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";);
TRACE("t_str", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << std::endl;);
SASSERT(atom->get_family_id() == get_family_id());
ast_manager & m = get_manager();
@ -54,7 +54,7 @@ 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";);
TRACE("t_str", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << std::endl;);
SASSERT(term->get_family_id() == get_family_id());
SASSERT(!ctx.e_internalized(term));
@ -80,6 +80,20 @@ void theory_str::attach_new_th_var(enode * n) {
TRACE("t_str_detail", tout << "new theory var: " << mk_ismt2_pp(n->get_owner(), get_manager()) << " := " << v << "\n";);
}
void theory_str::init_search_eh() {
ast_manager & m = get_manager();
context & ctx = get_context();
TRACE("t_str",
tout << "search started, assignments are:" << std::endl;
expr_ref_vector assignment(m);
ctx.get_assignments(assignment);
for (expr_ref_vector::iterator i = assignment.begin(); i != assignment.end(); ++i) {
expr * ex = *i;
tout << mk_ismt2_pp(ex, m) << std::endl;
}
);
}
void theory_str::new_eq_eh(theory_var x, theory_var y) {
// TODO
TRACE("t_str", tout << "new eq: " << x << " = " << y << std::endl;);
@ -94,4 +108,23 @@ void theory_str::new_diseq_eh(theory_var x, theory_var y) {
mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;);
}
void theory_str::relevant_eh(app * n) {
TRACE("t_str", tout << "relevant: " << mk_ismt2_pp(n, get_manager()) << "\n";);
}
void theory_str::assign_eh(bool_var v, bool is_true) {
context & ctx = get_context();
TRACE("t_str", tout << "assert: v" << v << " #" << ctx.bool_var2expr(v)->get_id() << " is_true: " << is_true << "\n";);
}
void theory_str::push_scope_eh() {
TRACE("t_str", tout << "push" << std::endl;);
}
final_check_status theory_str::final_check_eh() {
// TODO
TRACE("t_str", tout << "final check" << std::endl;);
return FC_DONE;
}
}; /* namespace smt */

8
src/smt/theory_str.h
View file

@ -38,6 +38,14 @@ namespace smt {
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()); }
virtual void init_search_eh();
virtual void relevant_eh(app * n);
virtual void assign_eh(bool_var v, bool is_true);
virtual void push_scope_eh();
virtual final_check_status final_check_eh();
public:
theory_str(ast_manager& m);
virtual ~theory_str();