mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

move display method to before first SAT call

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-21 18:29:36 -07:00
parent a78fc031bc
commit da0c12cdba
3 changed files with 16 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/opt/maxres.cpp
View file

@ -186,7 +186,6 @@ public:
init();
init_local();
trace();
display();
while (m_lower < m_upper) {
TRACE("opt",
display_vec(tout, m_asms);
@ -220,7 +219,6 @@ public:
init();
init_local();
trace();
display();
exprs cs;
while (m_lower < m_upper) {
lbool is_sat = check_sat_hill_climb(m_asms);
@ -253,14 +251,6 @@ public:
return l_true;
}
void display() {
if (m_dump_benchmarks && m_c.sat_enabled()) {
unsigned sz = m_soft.size();
inc_sat_display(verbose_stream(), s(), sz,
m_soft.c_ptr(), m_weights.c_ptr());
}
}
lbool check_sat_hill_climb(expr_ref_vector& asms1) {
expr_ref_vector asms(asms1);

15
src/opt/opt_context.cpp
View file

@ -41,6 +41,7 @@ Notes:
#include "ast_smt_pp.h"
#include "filter_model_converter.h"
#include "ast_pp_util.h"
#include "inc_sat_solver.h"
namespace opt {
@ -220,7 +221,7 @@ namespace opt {
TRACE("opt", tout << "Hard constraint: " << mk_ismt2_pp(m_hard_constraints[i].get(), m) << std::endl;);
s.assert_expr(m_hard_constraints[i].get());
}
display_benchmark();
IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";);
lbool is_sat = s.check_sat(0,0);
TRACE("opt", tout << "initial search result: " << is_sat << "\n";);
@ -1069,6 +1070,18 @@ namespace opt {
}
}
void context::display_benchmark() {
if (opt_params(m_params).dump_benchmarks() &&
sat_enabled() &&
m_objectives.size() == 1 &&
m_objectives[0].m_type == O_MAXSMT
) {
objective& o = m_objectives[0];
unsigned sz = o.m_terms.size();
inc_sat_display(verbose_stream(), get_solver(), sz, o.m_terms.c_ptr(), o.m_weights.c_ptr());
}
}
void context::display(std::ostream& out) {
display_assignment(out);
}

2
src/opt/opt_context.h
View file

@ -280,6 +280,8 @@ namespace opt {
void validate_lex();
void display_benchmark();
// pareto
void yield();