mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

fix compilation errors

Browse source
This commit is contained in:
Murphy Berzish 2015-09-30 05:21:16 -04:00
parent ed7b343822
commit e2901fff1e
2 changed files with 14 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/smt/theory_str.cpp
View file

@ -903,8 +903,8 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
ast_manager & mgr = get_manager(); ast_manager & mgr = get_manager();
context & ctx = get_context(); context & ctx = get_context();
TRACE("t_str_detail", tout << "process_concat_eq TYPE 1" << std::endl TRACE("t_str_detail", tout << "process_concat_eq TYPE 1" << std::endl
<< "concatAst1 = " << mk_ismt2_pp(concatAst1, m) << std::endl << "concatAst1 = " << mk_ismt2_pp(concatAst1, mgr) << std::endl
<< "concatAst2 = " << mk_ismt2_pp(concatAst2, m) << std::endl; << "concatAst2 = " << mk_ismt2_pp(concatAst2, mgr) << std::endl;
); );
if (!is_concat(to_app(concatAst1))) { if (!is_concat(to_app(concatAst1))) {
@ -1041,8 +1041,8 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
option++; option++;
add_cut_info_merge(t2, sLevel, x); add_cut_info_merge(t2, ctx.get_scope_level(), x);
add_cut_info_merge(t2, sLevel, n); add_cut_info_merge(t2, ctx.get_scope_level(), n);
} else { } else {
loopDetected = true; loopDetected = true;
TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;); TRACE("t_str", tout << "AVOID LOOP: SKIPPED" << std::endl;);
@ -1064,8 +1064,8 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
} else { } else {
and_item[0] = mgr.mk_or(option, or_item); and_item[0] = mgr.mk_or(option, or_item);
} }
expr_ref premise(ctx.mk_eq_atom(concatAst1, concatAst2), m); expr_ref premise(ctx.mk_eq_atom(concatAst1, concatAst2), mgr);
expr_ref conclusion(mgr.mk_and(pos, and_item), m); expr_ref conclusion(mgr.mk_and(pos, and_item), mgr);
assert_implication(premise, conclusion); assert_implication(premise, conclusion);
} else { } else {
TRACE("t_str", tout << "STOP: no split option found for two EQ concats." << std::endl;); TRACE("t_str", tout << "STOP: no split option found for two EQ concats." << std::endl;);
@ -1078,7 +1078,7 @@ bool theory_str::is_concat_eq_type2(expr * concatAst1, expr * concatAst2) {
return false; return false;
} }
void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) {
} }
@ -1087,7 +1087,7 @@ bool theory_str::is_concat_eq_type3(expr * concatAst1, expr * concatAst2) {
return false; return false;
} }
void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) {
} }
@ -1096,7 +1096,7 @@ bool theory_str::is_concat_eq_type4(expr * concatAst1, expr * concatAst2) {
return false; return false;
} }
void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { void theory_str::process_concat_eq_type4(expr * concatAst1, expr * concatAst2) {
} }
@ -1105,7 +1105,7 @@ bool theory_str::is_concat_eq_type5(expr * concatAst1, expr * concatAst2) {
return false; return false;
} }
void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { void theory_str::process_concat_eq_type5(expr * concatAst1, expr * concatAst2) {
} }
@ -1114,7 +1114,7 @@ bool theory_str::is_concat_eq_type6(expr * concatAst1, expr * concatAst2) {
return false; return false;
} }
void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) {
} }

5
src/smt/theory_str.h
View file

@ -24,6 +24,7 @@ Revision History:
#include"smt_model_generator.h" #include"smt_model_generator.h"
#include"arith_decl_plugin.h" #include"arith_decl_plugin.h"
#include<set> #include<set>
#include<stack>
namespace smt { namespace smt {
@ -71,8 +72,8 @@ namespace smt {
int tmpXorVarCount; int tmpXorVarCount;
std::map<std::pair<expr*, expr*>, std::map<int, expr*> > varForBreakConcat; std::map<std::pair<expr*, expr*>, std::map<int, expr*> > varForBreakConcat;
bool avoidLoopCut = true; bool avoidLoopCut;
bool loopDetected = false; bool loopDetected;
std::map<expr*, std::stack<T_cut *> > cut_var_map; std::map<expr*, std::stack<T_cut *> > cut_var_map;
protected: protected:
void assert_axiom(expr * e); void assert_axiom(expr * e);