mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-25 04:26:00 +00:00
Code Activity

add theory name; add debug info for freeVar_map

Browse source
This commit is contained in:
Murphy Berzish 2016-05-07 17:47:50 -04:00
parent 6dfc2dd910
commit bcaad06061
2 changed files with 9 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/theory_str.cpp
View file

@ -2655,6 +2655,7 @@ void theory_str::init_search_eh() {
* might not get a chance to see. * might not get a chance to see.
*/ */
/*
expr_ref_vector assignments(m); expr_ref_vector assignments(m);
ctx.get_assignments(assignments); ctx.get_assignments(assignments);
for (expr_ref_vector::iterator i = assignments.begin(); i != assignments.end(); ++i) { for (expr_ref_vector::iterator i = assignments.begin(); i != assignments.end(); ++i) {
@ -2676,6 +2677,7 @@ void theory_str::init_search_eh() {
<< ": expr ignored" << std::endl;); << ": expr ignored" << std::endl;);
} }
} }
*/
TRACE("t_str", tout << "search started" << std::endl;); TRACE("t_str", tout << "search started" << std::endl;);
search_started = true; search_started = true;
@ -2686,16 +2688,12 @@ void theory_str::new_eq_eh(theory_var x, theory_var y) {
TRACE("t_str", tout << "new eq: " << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " = " << TRACE("t_str", tout << "new eq: " << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " = " <<
mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;); mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;);
handle_equality(get_enode(x)->get_owner(), get_enode(y)->get_owner()); handle_equality(get_enode(x)->get_owner(), get_enode(y)->get_owner());
TRACE("t_str_dump_assign", dump_assignments(););
} }
void theory_str::new_diseq_eh(theory_var x, theory_var y) { void theory_str::new_diseq_eh(theory_var x, theory_var y) {
//TRACE("t_str_detail", tout << "new diseq: v#" << x << " != v#" << y << std::endl;); //TRACE("t_str_detail", tout << "new diseq: v#" << x << " != v#" << y << std::endl;);
TRACE("t_str", tout << "new diseq: " << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " != " << TRACE("t_str", tout << "new diseq: " << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " != " <<
mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;); mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;);
TRACE("t_str_dump_assign", dump_assignments(););
} }
void theory_str::relevant_eh(app * n) { void theory_str::relevant_eh(app * n) {
@ -3523,6 +3521,11 @@ final_check_status theory_str::final_check_eh() {
for (std::set<expr*>::iterator itx = free_variables.begin(); itx != free_variables.end(); ++itx) { for (std::set<expr*>::iterator itx = free_variables.begin(); itx != free_variables.end(); ++itx) {
tout << mk_ismt2_pp(*itx, m) << std::endl; tout << mk_ismt2_pp(*itx, m) << std::endl;
} }
tout << "freeVar_map has the following entries:" << std::endl;
for (std::map<expr*, int>::iterator fvIt = freeVar_map.begin(); fvIt != freeVar_map.end(); fvIt++) {
expr * var = fvIt->first;
tout << mk_ismt2_pp(var, m) << std::endl;
}
); );
// ----------------------------------------------------------- // -----------------------------------------------------------

2
src/smt/theory_str.h
View file

@ -205,6 +205,8 @@ namespace smt {
public: public:
theory_str(ast_manager & m); theory_str(ast_manager & m);
virtual ~theory_str(); virtual ~theory_str();
virtual char const * get_name() const { return "strings"; }
protected: protected:
virtual bool internalize_atom(app * atom, bool gate_ctx); virtual bool internalize_atom(app * atom, bool gate_ctx);
virtual bool internalize_term(app * term); virtual bool internalize_term(app * term);