mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-01 20:01:20 +00:00
Code Activity

tune for unit test, delay initialize re-solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-13 11:49:33 -07:00
parent f2bee7f16a
commit 1e143971c3
4 changed files with 9 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/seq_rewriter.h
View file

@ -89,6 +89,7 @@ public:
~re2automaton(); ~re2automaton();
eautomaton* operator()(expr* e); eautomaton* operator()(expr* e);
void set_solver(expr_solver* solver); void set_solver(expr_solver* solver);
bool has_solver() const { return m_solver; }
eautomaton* mk_product(eautomaton *a1, eautomaton *a2); eautomaton* mk_product(eautomaton *a1, eautomaton *a2);
}; };

6
src/smt/theory_seq.cpp
View file

@ -238,8 +238,7 @@ theory_seq::~theory_seq() {
} }
void theory_seq::init(context* ctx) { void theory_seq::init(context* ctx) {
theory::init(ctx); theory::init(ctx);
m_mk_aut.set_solver(alloc(seq_expr_solver, m, get_context().get_fparams()));
} }
final_check_status theory_seq::final_check_eh() { final_check_status theory_seq::final_check_eh() {
@ -4168,6 +4167,9 @@ eautomaton* theory_seq::get_automaton(expr* re) {
if (m_re2aut.find(re, result)) { if (m_re2aut.find(re, result)) {
return result; return result;
} }
if (!m_mk_aut.has_solver()) {
m_mk_aut.set_solver(alloc(seq_expr_solver, m, get_context().get_fparams()));
}
result = m_mk_aut(re); result = m_mk_aut(re);
if (result) { if (result) {
display_expr disp(m); display_expr disp(m);

6
src/test/get_implied_equalities.cpp
View file

@ -75,9 +75,9 @@ static void tst_get_implied_equalities1() {
} }
static void tst_get_implied_equalities2() { static void tst_get_implied_equalities2() {
enable_trace("after_search"); //enable_trace("after_search");
enable_trace("get_implied_equalities"); //enable_trace("get_implied_equalities");
enable_trace("implied_equalities"); //enable_trace("implied_equalities");
Z3_config cfg = Z3_mk_config(); Z3_config cfg = Z3_mk_config();
Z3_context ctx = Z3_mk_context(cfg); Z3_context ctx = Z3_mk_context(cfg);
Z3_del_config(cfg); Z3_del_config(cfg);

2
src/test/sat_local_search.cpp
View file

@ -7,7 +7,6 @@
static bool build_instance(char const * filename, sat::solver& s, sat::local_search& local_search) static bool build_instance(char const * filename, sat::solver& s, sat::local_search& local_search)
{ {
char line[16383]; char line[16383];
int cur_term;
// for temperally storage // for temperally storage
std::ifstream infile(filename); std::ifstream infile(filename);
@ -18,6 +17,7 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea
} }
infile.getline(line, 16383); infile.getline(line, 16383);
#ifdef _WINDOWS #ifdef _WINDOWS
int cur_term;
int num_vars = 0, num_constraints = 0; int num_vars = 0, num_constraints = 0;
sscanf_s(line, "%d %d", &num_vars, &num_constraints); sscanf_s(line, "%d %d", &num_vars, &num_constraints);
//std::cout << "number of variables: " << num_vars << '\n'; //std::cout << "number of variables: " << num_vars << '\n';