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

fix #1908

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-30 14:15:29 -05:00
parent 5d06fa2347
commit 3c1c3d5987
12 changed files with 103 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/ast/array_decl_plugin.cpp
View file

@ -253,7 +253,10 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) {
if (!parameters[i].is_ast() ||
!is_sort(parameters[i].get_ast()) ||
!m_manager->compatible_sorts(domain[i+1], to_sort(parameters[i].get_ast()))) {
m_manager->raise_exception("domain sort and parameter do not match");
std::stringstream strm;
strm << "domain sort " << sort_ref(domain[i+1], *m_manager) << " and parameter ";
strm << parameter_pp(parameters[i], *m_manager) << " do not match";
m_manager->raise_exception(strm.str().c_str());
UNREACHABLE();
return nullptr;
}
@ -292,8 +295,12 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) {
m_manager->raise_exception("expecting sort parameter");
return nullptr;
}
if (!m_manager->compatible_sorts(to_sort(parameters[i].get_ast()), domain[i+1])) {
m_manager->raise_exception("domain sort and parameter do not match");
sort* srt1 = to_sort(parameters[i].get_ast());
sort* srt2 = domain[i+1];
if (!m_manager->compatible_sorts(srt1, srt2)) {
std::stringstream strm;
strm << "domain sort " << sort_ref(srt2, *m_manager) << " and parameter sort " << sort_ref(srt2, *m_manager) << " do not match";
m_manager->raise_exception(strm.str());
UNREACHABLE();
return nullptr;
}
@ -326,13 +333,13 @@ bool array_decl_plugin::check_set_arguments(unsigned arity, sort * const * domai
if (domain[i] != domain[0]) {
std::ostringstream buffer;
buffer << "arguments " << 1 << " and " << (i+1) << " have different sorts";
m_manager->raise_exception(buffer.str().c_str());
m_manager->raise_exception(buffer.str());
return false;
}
if (domain[i]->get_family_id() != m_family_id) {
std::ostringstream buffer;
buffer << "argument " << (i+1) << " is not of array sort";
m_manager->raise_exception(buffer.str().c_str());
m_manager->raise_exception(buffer.str());
return false;
}
}
@ -517,6 +524,7 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
void array_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol const & logic) {
sort_names.push_back(builtin_name(ARRAY_SORT_STR, ARRAY_SORT));
sort_names.push_back(builtin_name("=>", ARRAY_SORT));
// TBD: this could easily break users even though it is already used in CVC4:
// sort_names.push_back(builtin_name("Set", _SET_SORT));
}

10
src/ast/ast.cpp
View file

@ -1542,6 +1542,16 @@ void ast_manager::raise_exception(char const * msg) {
}
std::ostream& ast_manager::display(std::ostream& out, parameter const& p) {
switch (p.get_kind()) {
case parameter::PARAM_AST:
return out << mk_pp(p.get_ast(), *this);
default:
return p.display(out);
}
return out;
}
void ast_manager::copy_families_plugins(ast_manager const & from) {
TRACE("copy_families_plugins",
tout << "target:\n";

13
src/ast/ast.h
View file

@ -1558,6 +1558,9 @@ public:
// Equivalent to throw ast_exception(msg)
Z3_NORETURN void raise_exception(char const * msg);
Z3_NORETURN void raise_exception(std::string const& msg) { raise_exception(msg.c_str()); }
std::ostream& display(std::ostream& out, parameter const& p);
bool is_format_manager() const { return m_format_manager == nullptr; }
@ -2569,6 +2572,16 @@ public:
void operator()(AST * n) { m_manager.inc_ref(n); }
};
struct parameter_pp {
parameter const& p;
ast_manager& m;
parameter_pp(parameter const& p, ast_manager& m): p(p), m(m) {}
};
inline std::ostream& operator<<(std::ostream& out, parameter_pp const& pp) {
return pp.m.display(out, pp.p);
}
#endif /* AST_H_ */

4
src/ast/rewriter/seq_rewriter.cpp
View file

@ -859,10 +859,6 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu
result = m_util.str.mk_concat(c, a);
return BR_REWRITE1;
}
if (m_util.str.is_string(a, s1) && s1.length() == 0) {
result = a;
return BR_DONE;
}
return BR_FAILED;
}

1
src/sat/sat_config.cpp
View file

@ -86,6 +86,7 @@ namespace sat {
m_local_search_mode = local_search_mode::gsat;
else
m_local_search_mode = local_search_mode::wsat;
m_local_search_dbg_flips = p.local_search_dbg_flips();
m_unit_walk = p.unit_walk();
m_unit_walk_threads = p.unit_walk_threads();
m_lookahead_simplify = p.lookahead_simplify();

1
src/sat/sat_config.h
View file

@ -105,6 +105,7 @@ namespace sat {
unsigned m_local_search_threads;
bool m_local_search;
local_search_mode m_local_search_mode;
bool m_local_search_dbg_flips;
unsigned m_unit_walk_threads;
bool m_unit_walk;
bool m_lookahead_simplify;

18
src/sat/sat_local_search.cpp
View file

@ -553,6 +553,7 @@ namespace sat {
PROGRESS(tries, total_flips);
for (tries = 1; !m_unsat_stack.empty() && m_limit.inc(); ++tries) {
++m_stats.m_num_restarts;
for (step = 0; step < m_max_steps && !m_unsat_stack.empty(); ++step) {
pick_flip_walksat();
if (m_unsat_stack.size() < m_best_unsat) {
@ -622,7 +623,6 @@ namespace sat {
break;
}
// remove unit clauses from assumptions.
m_constraints.shrink(num_constraints() - sz);
@ -779,8 +779,11 @@ namespace sat {
}
void local_search::flip_walksat(bool_var flipvar) {
++m_stats.m_num_flips;
VERIFY(!is_unit(flipvar));
m_vars[flipvar].m_value = !cur_solution(flipvar);
m_vars[flipvar].m_flips++;
m_vars[flipvar].m_slow_break.update(abs(m_vars[flipvar].m_slack_score));
bool flip_is_true = cur_solution(flipvar);
coeff_vector const& truep = m_vars[flipvar].m_watch[flip_is_true];
@ -1062,6 +1065,19 @@ namespace sat {
return out << "v" << v << " := " << (vi.m_value?"true":"false") << " bias: " << vi.m_bias << "\n";
}
void local_search::collect_statistics(statistics& st) const {
if (m_config.dbg_flips()) {
unsigned i = 0;
for (var_info const& vi : m_vars) {
IF_VERBOSE(0, verbose_stream() << "flips: " << i << " " << vi.m_flips << " " << vi.m_slow_break << "\n");
++i;
}
}
st.update("local-search-flips", m_stats.m_num_flips);
st.update("local-search-restarts", m_stats.m_num_restarts);
}
bool local_search::check_goodvar() {
unsigned g = 0;
for (unsigned v = 0; v < num_vars(); ++v) {

24
src/sat/sat_local_search.h
View file

@ -23,6 +23,8 @@
#include "sat/sat_types.h"
#include "sat/sat_config.h"
#include "util/rlimit.h"
#include "util/ema.h"
#include "util/statistics.h"
namespace sat {
@ -33,18 +35,21 @@ namespace sat {
int m_best_known_value;
local_search_mode m_mode;
bool m_phase_sticky;
bool m_dbg_flips;
public:
local_search_config() {
m_random_seed = 0;
m_best_known_value = INT_MAX;
m_mode = local_search_mode::wsat;
m_phase_sticky = false;
m_dbg_flips = false;
}
unsigned random_seed() const { return m_random_seed; }
unsigned best_known_value() const { return m_best_known_value; }
local_search_mode mode() const { return m_mode; }
bool phase_sticky() const { return m_phase_sticky; }
bool dbg_flips() const { return m_dbg_flips; }
void set_random_seed(unsigned s) { m_random_seed = s; }
void set_best_known_value(unsigned v) { m_best_known_value = v; }
@ -53,6 +58,7 @@ namespace sat {
m_mode = cfg.m_local_search_mode;
m_random_seed = cfg.m_random_seed;
m_phase_sticky = cfg.m_phase_sticky;
m_dbg_flips = cfg.m_local_search_dbg_flips;
}
};
@ -74,6 +80,13 @@ namespace sat {
int coefficient; // non-zero integer
ob_term(bool_var v, int c): var_id(v), coefficient(c) {}
};
struct stats {
unsigned m_num_flips;
unsigned m_num_restarts;
void reset() { memset(this, 0, sizeof(*this)); }
stats() { reset(); }
};
struct var_info {
bool m_value; // current solution
@ -89,6 +102,8 @@ namespace sat {
bool_var_vector m_neighbors; // neighborhood variables
coeff_vector m_watch[2];
literal_vector m_bin[2];
unsigned m_flips;
ema m_slow_break;
var_info():
m_value(true),
m_bias(50),
@ -97,7 +112,9 @@ namespace sat {
m_in_goodvar_stack(false),
m_score(0),
m_slack_score(0),
m_cscc(0)
m_cscc(0),
m_flips(0),
m_slow_break(1e-5)
{}
};
@ -115,6 +132,8 @@ namespace sat {
literal const* end() const { return m_literals.end(); }
};
stats m_stats;
local_search_config m_config;
// objective function: maximize
@ -145,7 +164,6 @@ namespace sat {
inline void set_best_unsat();
/* TBD: other scores */
vector<constraint> m_constraints;
@ -293,6 +311,8 @@ namespace sat {
model& get_model() { return m_model; }
void collect_statistics(statistics& st) const;
};
}

1
src/sat/sat_params.pyg
View file

@ -48,6 +48,7 @@ def_module_params('sat',
('local_search', BOOL, False, 'use local search instead of CDCL'),
('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'),
('local_search_dbg_flips', BOOL, False, 'write debug information for number of flips'),
('unit_walk', BOOL, False, 'use unit-walk search instead of CDCL'),
('unit_walk_threads', UINT, 0, 'number of unit-walk search threads to find satisfiable solution'),
('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'),

25
src/sat/sat_solver.cpp
View file

@ -68,6 +68,7 @@ namespace sat {
m_simplifications = 0;
m_ext = nullptr;
m_cuber = nullptr;
m_local_search = nullptr;
m_mc.set_solver(this);
}
@ -764,9 +765,9 @@ namespace sat {
m_not_l = not_l;
}
void solver::assign_core(literal l, justification j) {
void solver::assign_core(literal l, unsigned lvl, justification j) {
SASSERT(value(l) == l_undef);
TRACE("sat_assign_core", tout << l << " " << j << " level: " << scope_lvl() << "\n";);
TRACE("sat_assign_core", tout << l << " " << j << " level: " << lvl << "\n";);
if (at_base_lvl()) {
if (m_config.m_drat) m_drat.add(l, !j.is_none());
j = justification(); // erase justification for level 0
@ -774,7 +775,7 @@ namespace sat {
m_assignment[l.index()] = l_true;
m_assignment[(~l).index()] = l_false;
bool_var v = l.var();
m_level[v] = scope_lvl();
m_level[v] = lvl;
m_justification[v] = j;
m_phase[v] = static_cast<phase>(l.sign());
m_assigned_since_gc[v] = true;
@ -882,7 +883,7 @@ namespace sat {
return false;
case l_undef:
m_stats.m_bin_propagate++;
assign_core(l1, justification(not_l));
assign_core(l1, scope_lvl(), justification(not_l));
break;
case l_true:
break; // skip
@ -897,11 +898,11 @@ namespace sat {
val2 = value(l2);
if (val1 == l_false && val2 == l_undef) {
m_stats.m_ter_propagate++;
assign_core(l2, justification(l1, not_l));
assign_core(l2, scope_lvl(), justification(l1, not_l));
}
else if (val1 == l_undef && val2 == l_false) {
m_stats.m_ter_propagate++;
assign_core(l1, justification(l2, not_l));
assign_core(l1, scope_lvl(), justification(l2, not_l));
}
else if (val1 == l_false && val2 == l_false) {
CONFLICT_CLEANUP();
@ -964,7 +965,7 @@ namespace sat {
it2++;
m_stats.m_propagate++;
c.mark_used();
assign_core(c[0], justification(cls_off));
assign_core(c[0], scope_lvl(), justification(cls_off));
#ifdef UPDATE_GLUE
if (update && c.is_learned() && c.glue() > 2) {
unsigned glue;
@ -1042,7 +1043,7 @@ namespace sat {
literal l(v, false);
if (mdl[v] != l_true) l.neg();
push();
assign_core(l, justification());
assign_core(l, scope_lvl(), justification());
}
mk_model();
break;
@ -1160,13 +1161,16 @@ namespace sat {
lbool solver::do_local_search(unsigned num_lits, literal const* lits) {
scoped_limits scoped_rl(rlimit());
local_search srch;
SASSERT(!m_local_search);
m_local_search = alloc(local_search);
local_search& srch = *m_local_search;
srch.config().set_config(m_config);
srch.import(*this, false);
scoped_rl.push_child(&srch.rlimit());
lbool r = srch.check(num_lits, lits, nullptr);
m_model = srch.get_model();
// srch.collect_statistics(m_aux_stats);
m_local_search = nullptr;
dealloc(&srch);
return r;
}
@ -3379,6 +3383,7 @@ namespace sat {
m_asymm_branch.collect_statistics(st);
m_probing.collect_statistics(st);
if (m_ext) m_ext->collect_statistics(st);
if (m_local_search) m_local_search->collect_statistics(st);
st.copy(m_aux_stats);
}

5
src/sat/sat_solver.h
View file

@ -163,6 +163,7 @@ namespace sat {
bool m_par_syncing_clauses;
class lookahead* m_cuber;
class local_search* m_local_search;
statistics m_aux_stats;
@ -305,11 +306,11 @@ namespace sat {
TRACE("sat_assign", tout << l << " previous value: " << value(l) << "\n";);
switch (value(l)) {
case l_false: set_conflict(j, ~l); break;
case l_undef: assign_core(l, j); break;
case l_undef: assign_core(l, scope_lvl(), j); break;
case l_true: return;
}
}
void assign_core(literal l, justification jst);
void assign_core(literal l, unsigned lvl, justification jst);
void set_conflict(justification c, literal not_l);
void set_conflict(justification c) { set_conflict(c, null_literal); }
lbool status(clause const & c) const;

14
src/shell/dimacs_frontend.cpp
View file

@ -178,21 +178,21 @@ unsigned read_dimacs(char const * file_name) {
std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl;
exit(ERR_OPEN_FILE);
}
parse_dimacs(in, solver);
parse_dimacs(in, *g_solver);
}
else {
parse_dimacs(std::cin, solver);
parse_dimacs(std::cin, *g_solver);
}
IF_VERBOSE(20, solver.display_status(verbose_stream()););
IF_VERBOSE(20, g_solver->display_status(verbose_stream()););
lbool r;
vector<sat::literal_vector> tracking_clauses;
sat::solver solver2(p, limit);
if (p.get_bool("dimacs.core", false)) {
g_solver = &solver2;
sat::solver solver2( p, limit);
if (p.get_bool("dimacs.core", false)) {
sat::literal_vector assumptions;
track_clauses(solver, solver2, assumptions, tracking_clauses);
r = g_solver->check(assumptions.size(), assumptions.c_ptr());
g_solver = &solver2;
r = solver2.check(assumptions.size(), assumptions.c_ptr());
}
else {
r = g_solver->check();