mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Alcides Fonseca 2019-01-25 14:45:22 +00:00
commit 83717a9c86
50 changed files with 1091 additions and 614 deletions
Download patch file Download diff file Expand all files Collapse all files

66
src/api/api_solver.cpp
View file

@ -163,12 +163,46 @@ extern "C" {
to_solver_ref(s)->set_model_converter(ctx->get_model_converter());
}
static void solver_from_dimacs_stream(Z3_context c, Z3_solver s, std::istream& is) {
init_solver(c, s);
ast_manager& m = to_solver_ref(s)->get_manager();
std::stringstream err;
sat::solver solver(to_solver_ref(s)->get_params(), m.limit());
if (!parse_dimacs(is, err, solver)) {
SET_ERROR_CODE(Z3_PARSER_ERROR, err.str().c_str());
return;
}
sat2goal s2g;
ref<sat2goal::mc> mc;
atom2bool_var a2b(m);
for (unsigned v = 0; v < solver.num_vars(); ++v) {
a2b.insert(m.mk_const(symbol(v), m.mk_bool_sort()), v);
}
goal g(m);
s2g(solver, a2b, to_solver_ref(s)->get_params(), g, mc);
for (unsigned i = 0; i < g.size(); ++i) {
to_solver_ref(s)->assert_expr(g.form(i));
}
}
// DIMACS files start with "p cnf" and number of variables/clauses.
// This is not legal SMT syntax, so use the DIMACS parser.
static bool is_dimacs_string(Z3_string c_str) {
std::cout << c_str << "\n";
return c_str[0] == 'p' && c_str[1] == ' ' && c_str[2] == 'c';
}
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string c_str) {
Z3_TRY;
LOG_Z3_solver_from_string(c, s, c_str);
std::string str(c_str);
std::istringstream is(str);
solver_from_stream(c, s, is);
if (is_dimacs_string(c_str)) {
solver_from_dimacs_stream(c, s, is);
}
else {
solver_from_stream(c, s, is);
}
Z3_CATCH;
}
@ -182,24 +216,7 @@ extern "C" {
SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR, nullptr);
}
else if (ext && (std::string("dimacs") == ext || std::string("cnf") == ext)) {
ast_manager& m = to_solver_ref(s)->get_manager();
std::stringstream err;
sat::solver solver(to_solver_ref(s)->get_params(), m.limit());
if (!parse_dimacs(is, err, solver)) {
SET_ERROR_CODE(Z3_PARSER_ERROR, err.str().c_str());
return;
}
sat2goal s2g;
ref<sat2goal::mc> mc;
atom2bool_var a2b(m);
for (unsigned v = 0; v < solver.num_vars(); ++v) {
a2b.insert(m.mk_const(symbol(v), m.mk_bool_sort()), v);
}
goal g(m);
s2g(solver, a2b, to_solver_ref(s)->get_params(), g, mc);
for (unsigned i = 0; i < g.size(); ++i) {
to_solver_ref(s)->assert_expr(g.form(i));
}
solver_from_dimacs_stream(c, s, is);
}
else {
solver_from_stream(c, s, is);
@ -532,6 +549,17 @@ extern "C" {
Z3_CATCH_RETURN("");
}
Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s) {
Z3_TRY;
LOG_Z3_solver_to_string(c, s);
RESET_ERROR_CODE();
init_solver(c, s);
std::ostringstream buffer;
to_solver_ref(s)->display_dimacs(buffer);
return mk_c(c)->mk_external_string(buffer.str());
Z3_CATCH_RETURN("");
}
Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c,
Z3_solver s,

18
src/api/c++/z3++.h
View file

@ -518,6 +518,12 @@ namespace z3 {
sort(context & c, Z3_ast a):ast(c, a) {}
sort(sort const & s):ast(s) {}
operator Z3_sort() const { return reinterpret_cast<Z3_sort>(m_ast); }
/**
\brief retrieve unique identifier for func_decl.
*/
unsigned id() const { unsigned r = Z3_get_sort_id(ctx(), *this); check_error(); return r; }
/**
\brief Return true if this sort and \c s are equal.
*/
@ -615,6 +621,11 @@ namespace z3 {
operator Z3_func_decl() const { return reinterpret_cast<Z3_func_decl>(m_ast); }
func_decl & operator=(func_decl const & s) { return static_cast<func_decl&>(ast::operator=(s)); }
/**
\brief retrieve unique identifier for func_decl.
*/
unsigned id() const { unsigned r = Z3_get_func_decl_id(ctx(), *this); check_error(); return r; }
unsigned arity() const { return Z3_get_arity(ctx(), *this); }
sort domain(unsigned i) const { assert(i < arity()); Z3_sort r = Z3_get_domain(ctx(), *this, i); check_error(); return sort(ctx(), r); }
sort range() const { Z3_sort r = Z3_get_range(ctx(), *this); check_error(); return sort(ctx(), r); }
@ -771,6 +782,11 @@ namespace z3 {
return std::string(Z3_get_numeral_decimal_string(ctx(), m_ast, precision));
}
/**
\brief retrieve unique identifier for expression.
*/
unsigned id() const { unsigned r = Z3_get_ast_id(ctx(), m_ast); check_error(); return r; }
/**
\brief Return int value of numeral, throw if result cannot fit in
machine int
@ -2240,6 +2256,8 @@ namespace z3 {
fml));
}
std::string dimacs() const { return std::string(Z3_solver_to_dimacs_string(ctx(), m_solver)); }
param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); }

4
src/api/python/z3/z3.py
View file

@ -6800,6 +6800,10 @@ class Solver(Z3PPObject):
"""
return Z3_solver_to_string(self.ctx.ref(), self.solver)
def dimacs(self):
"""Return a textual representation of the solver in DIMACS format."""
return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver)
def to_smt2(self):
"""return SMTLIB2 formatted benchmark for solver's assertions"""
es = self.assertions()

8
src/api/z3_api.h
View file

@ -6368,6 +6368,14 @@ extern "C" {
*/
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s);
/**
\brief Convert a solver into a DIMACS formatted string.
\sa Z3_goal_to_diamcs_string for requirements.
def_API('Z3_solver_to_dimacs_string', STRING, (_in(CONTEXT), _in(SOLVER)))
*/
Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s);
/*@}*/
/** @name Statistics */

1
src/ast/CMakeLists.txt
View file

@ -17,6 +17,7 @@ z3_add_component(ast
csp_decl_plugin.cpp
datatype_decl_plugin.cpp
decl_collector.cpp
display_dimacs.cpp
dl_decl_plugin.cpp
expr2polynomial.cpp
expr2var.cpp

81
src/ast/display_dimacs.cpp Normal file
View file

@ -0,0 +1,81 @@
/*++
Copyright (c) 2019 Microsoft Corporation
Module Name:
display_dimacs.h
Abstract:
Display expressions in DIMACS format.
Author:
Nikolaj Bjorner (nbjorner0 2019-01-24
Revision History:
--*/
#include "ast.h"
#include "display_dimacs.h"
std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls) {
ast_manager& m = fmls.m();
unsigned_vector expr2var;
ptr_vector<expr> exprs;
unsigned num_vars = 0;
unsigned num_cls = fmls.size();
for (expr * f : fmls) {
unsigned num_lits;
expr * const * lits;
if (m.is_or(f)) {
num_lits = to_app(f)->get_num_args();
lits = to_app(f)->get_args();
}
else {
num_lits = 1;
lits = &f;
}
for (unsigned j = 0; j < num_lits; j++) {
expr * l = lits[j];
if (m.is_not(l))
l = to_app(l)->get_arg(0);
if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) {
num_vars++;
expr2var.setx(l->get_id(), num_vars, UINT_MAX);
exprs.setx(l->get_id(), l, nullptr);
}
}
}
out << "p cnf " << num_vars << " " << num_cls << "\n";
for (expr* f : fmls) {
unsigned num_lits;
expr * const * lits;
if (m.is_or(f)) {
num_lits = to_app(f)->get_num_args();
lits = to_app(f)->get_args();
}
else {
num_lits = 1;
lits = &f;
}
for (unsigned j = 0; j < num_lits; j++) {
expr * l = lits[j];
if (m.is_not(l)) {
out << "-";
l = to_app(l)->get_arg(0);
}
SASSERT(exprs[l->get_id()]);
out << expr2var[l->get_id()] << " ";
}
out << "0\n";
}
for (expr* e : exprs) {
if (e && is_app(e)) {
symbol const& n = to_app(e)->get_decl()->get_name();
out << "c " << expr2var[e->get_id()] << " " << n << "\n";
}
}
return out;
}

26
src/ast/display_dimacs.h Normal file
View file

@ -0,0 +1,26 @@
/*++
Copyright (c) 2019 Microsoft Corporation
Module Name:
display_dimacs.h
Abstract:
Display expressions in DIMACS format.
Author:
Nikolaj Bjorner (nbjorner0 2019-01-24
Revision History:
--*/
#ifndef DISPLAY_DIMACS_H_
#define DISPLAY_DIMACS_H_
#include "ast.h"
std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls);
#endif /* DISPLAY_DIMACS_H__ */

2
src/ast/rewriter/arith_rewriter.cpp
View file

@ -907,7 +907,7 @@ expr_ref arith_rewriter::remove_divisor(expr* arg, expr* num, expr* den) {
m_util.mk_idiv(zero, zero),
m().mk_ite(m_util.mk_ge(arg, zero),
d,
m_util.mk_uminus(nd))),
nd)),
m());
}

791
src/muz/spacer/spacer_iuc_solver.cpp
View file

@ -27,443 +27,426 @@ Notes:
#include "muz/spacer/spacer_iuc_proof.h"
namespace spacer {
void iuc_solver::push ()
{
m_defs.push_back (def_manager (*this));
m_solver.push ();
}
void iuc_solver::pop (unsigned n)
{
m_solver.pop (n);
unsigned lvl = m_defs.size ();
SASSERT (n <= lvl);
unsigned new_lvl = lvl-n;
while (m_defs.size() > new_lvl) {
m_num_proxies -= m_defs.back ().m_defs.size ();
m_defs.pop_back ();
void iuc_solver::push () {
m_defs.push_back (def_manager (*this));
m_solver.push ();
}
}
app* iuc_solver::fresh_proxy ()
{
if (m_num_proxies == m_proxies.size()) {
std::stringstream name;
name << "spacer_proxy!" << m_proxies.size ();
app_ref res(m);
res = m.mk_const (symbol (name.str ().c_str ()),
m.mk_bool_sort ());
m_proxies.push_back (res);
// -- add the new proxy to proxy eliminator
proof_ref pr(m);
pr = m.mk_asserted (m.mk_true ());
m_elim_proxies_sub.insert (res, m.mk_true (), pr);
void iuc_solver::pop (unsigned n) {
m_solver.pop (n);
unsigned lvl = m_defs.size ();
SASSERT (n <= lvl);
unsigned new_lvl = lvl-n;
while (m_defs.size() > new_lvl) {
m_num_proxies -= m_defs.back ().m_defs.size ();
m_defs.pop_back ();
}
}
return m_proxies.get (m_num_proxies++);
}
app* iuc_solver::mk_proxy (expr *v)
{
{
app* iuc_solver::fresh_proxy () {
if (m_num_proxies == m_proxies.size()) {
std::stringstream name;
name << "spacer_proxy!" << m_proxies.size ();
app_ref res(m);
res = m.mk_const (symbol (name.str ().c_str ()),
m.mk_bool_sort ());
m_proxies.push_back (res);
// -- add the new proxy to proxy eliminator
proof_ref pr(m);
pr = m.mk_asserted (m.mk_true ());
m_elim_proxies_sub.insert (res, m.mk_true (), pr);
}
return m_proxies.get (m_num_proxies++);
}
app* iuc_solver::mk_proxy (expr *v) {
expr *e = v;
m.is_not (v, e);
if (is_uninterp_const(e)) { return to_app(v); }
if (is_uninterp_const(e)) {
return to_app(v);
}
def_manager &def = !m_defs.empty() ? m_defs.back () : m_base_defs;
return def.mk_proxy (v);
}
def_manager &def = !m_defs.empty() ? m_defs.back () : m_base_defs;
return def.mk_proxy (v);
}
bool iuc_solver::mk_proxies (expr_ref_vector &v, unsigned from)
{
bool dirty = false;
for (unsigned i = from, sz = v.size(); i < sz; ++i) {
app *p = mk_proxy (v.get (i));
dirty |= (v.get (i) != p);
v[i] = p;
bool iuc_solver::mk_proxies (expr_ref_vector &v, unsigned from) {
bool dirty = false;
for (unsigned i = from, sz = v.size(); i < sz; ++i) {
app *p = mk_proxy (v.get (i));
dirty |= (v.get (i) != p);
v[i] = p;
}
return dirty;
}
return dirty;
}
void iuc_solver::push_bg (expr *e)
{
if (m_assumptions.size () > m_first_assumption)
{ m_assumptions.shrink(m_first_assumption); }
m_assumptions.push_back (e);
m_first_assumption = m_assumptions.size ();
}
void iuc_solver::pop_bg (unsigned n)
{
if (n == 0) { return; }
if (m_assumptions.size () > m_first_assumption) {
void iuc_solver::push_bg (expr *e) {
if (m_assumptions.size () > m_first_assumption) {
m_assumptions.shrink(m_first_assumption);
}
m_assumptions.push_back (e);
m_first_assumption = m_assumptions.size ();
}
void iuc_solver::pop_bg (unsigned n) {
if (n == 0) return;
if (m_assumptions.size () > m_first_assumption) {
m_assumptions.shrink(m_first_assumption);
}
m_first_assumption = m_first_assumption > n ? m_first_assumption - n : 0;
m_assumptions.shrink (m_first_assumption);
}
unsigned iuc_solver::get_num_bg () {
return m_first_assumption;
}
lbool iuc_solver::check_sat_core (unsigned num_assumptions, expr * const *assumptions) {
// -- remove any old assumptions
m_assumptions.shrink(m_first_assumption);
// -- replace theory literals in background assumptions with proxies
mk_proxies (m_assumptions);
// -- in case mk_proxies added new literals, they are all background
m_first_assumption = m_assumptions.size ();
m_assumptions.append (num_assumptions, assumptions);
m_is_proxied = mk_proxies (m_assumptions, m_first_assumption);
return set_status (m_solver.check_sat (m_assumptions));
}
m_first_assumption = m_first_assumption > n ? m_first_assumption - n : 0;
m_assumptions.shrink (m_first_assumption);
}
lbool iuc_solver::check_sat_cc(const expr_ref_vector &cube,
vector<expr_ref_vector> const & clauses) {
if (clauses.empty())
return check_sat(cube.size(), cube.c_ptr());
// -- remove any old assumptions
m_assumptions.shrink(m_first_assumption);
// -- replace theory literals in background assumptions with proxies
mk_proxies(m_assumptions);
// -- in case mk_proxies added new literals, they are all background
m_first_assumption = m_assumptions.size();
m_assumptions.append(cube);
m_is_proxied = mk_proxies(m_assumptions, m_first_assumption);
return set_status (m_solver.check_sat_cc(m_assumptions, clauses));
}
unsigned iuc_solver::get_num_bg () {return m_first_assumption;}
lbool iuc_solver::check_sat (unsigned num_assumptions, expr * const *assumptions)
{
// -- remove any old assumptions
m_assumptions.shrink(m_first_assumption);
// -- replace theory literals in background assumptions with proxies
mk_proxies (m_assumptions);
// -- in case mk_proxies added new literals, they are all background
m_first_assumption = m_assumptions.size ();
m_assumptions.append (num_assumptions, assumptions);
m_is_proxied = mk_proxies (m_assumptions, m_first_assumption);
return set_status (m_solver.check_sat (m_assumptions));
}
lbool iuc_solver::check_sat_cc(const expr_ref_vector &cube,
vector<expr_ref_vector> const & clauses) {
if (clauses.empty())
return check_sat(cube.size(), cube.c_ptr());
// -- remove any old assumptions
m_assumptions.shrink(m_first_assumption);
// -- replace theory literals in background assumptions with proxies
mk_proxies(m_assumptions);
// -- in case mk_proxies added new literals, they are all background
m_first_assumption = m_assumptions.size();
m_assumptions.append(cube);
m_is_proxied = mk_proxies(m_assumptions, m_first_assumption);
return set_status (m_solver.check_sat_cc(m_assumptions, clauses));
}
app* iuc_solver::def_manager::mk_proxy (expr *v)
{
app* r;
if (m_expr2proxy.find(v, r))
return r;
ast_manager &m = m_parent.m;
app* proxy = m_parent.fresh_proxy ();
app* def = m.mk_or (m.mk_not (proxy), v);
m_defs.push_back (def);
m_expr2proxy.insert (v, proxy);
m_proxy2def.insert (proxy, def);
m_parent.assert_expr (def);
return proxy;
}
bool iuc_solver::def_manager::is_proxy (app *k, app_ref &def)
{
app *r = nullptr;
bool found = m_proxy2def.find (k, r);
def = r;
return found;
}
void iuc_solver::def_manager::reset ()
{
m_expr2proxy.reset ();
m_proxy2def.reset ();
m_defs.reset ();
}
bool iuc_solver::def_manager::is_proxy_def (expr *v)
{
// XXX This might not be the most robust way to check
return m_defs.contains (v);
}
bool iuc_solver::is_proxy(expr *e, app_ref &def)
{
if (!is_uninterp_const(e))
return false;
app* a = to_app (e);
for (int i = m_defs.size (); i-- > 0; )
if (m_defs[i].is_proxy (a, def))
return true;
return m_base_defs.is_proxy (a, def);
}
void iuc_solver::collect_statistics (statistics &st) const
{
m_solver.collect_statistics (st);
st.update ("time.iuc_solver.get_iuc", m_iuc_sw.get_seconds());
st.update ("time.iuc_solver.get_iuc.hyp_reduce1", m_hyp_reduce1_sw.get_seconds());
st.update ("time.iuc_solver.get_iuc.hyp_reduce2", m_hyp_reduce2_sw.get_seconds());
st.update ("time.iuc_solver.get_iuc.learn_core", m_learn_core_sw.get_seconds());
st.update("iuc_solver.num_proxies", m_proxies.size());
}
void iuc_solver::reset_statistics ()
{
m_iuc_sw.reset();
m_hyp_reduce1_sw.reset();
m_hyp_reduce2_sw.reset();
m_learn_core_sw.reset();
}
void iuc_solver::get_unsat_core (expr_ref_vector &core) {
m_solver.get_unsat_core (core);
undo_proxies_in_core (core);
}
void iuc_solver::undo_proxies_in_core (expr_ref_vector &r)
{
app_ref e(m);
expr_fast_mark1 bg;
for (unsigned i = 0; i < m_first_assumption; ++i) {
bg.mark(m_assumptions.get(i));
app* iuc_solver::def_manager::mk_proxy (expr *v) {
app* r;
if (m_expr2proxy.find(v, r))
return r;
ast_manager &m = m_parent.m;
app* proxy = m_parent.fresh_proxy ();
app* def = m.mk_or (m.mk_not (proxy), v);
m_defs.push_back (def);
m_expr2proxy.insert (v, proxy);
m_proxy2def.insert (proxy, def);
m_parent.assert_expr (def);
return proxy;
}
// expand proxies
unsigned j = 0;
for (expr* rr : r) {
// skip background assumptions
if (bg.is_marked(rr))
continue;
bool iuc_solver::def_manager::is_proxy (app *k, app_ref &def) {
app *r = nullptr;
bool found = m_proxy2def.find (k, r);
def = r;
return found;
}
void iuc_solver::def_manager::reset () {
m_expr2proxy.reset ();
m_proxy2def.reset ();
m_defs.reset ();
}
// -- undo proxies, but only if they were introduced in check_sat
if (m_is_proxied && is_proxy(rr, e)) {
SASSERT (m.is_or (e));
r[j++] = e->get_arg (1);
bool iuc_solver::def_manager::is_proxy_def (expr *v) {
// XXX This might not be the most robust way to check
return m_defs.contains (v);
}
bool iuc_solver::is_proxy(expr *e, app_ref &def) {
if (!is_uninterp_const(e))
return false;
app* a = to_app (e);
for (int i = m_defs.size (); i-- > 0; )
if (m_defs[i].is_proxy (a, def))
return true;
return m_base_defs.is_proxy (a, def);
}
void iuc_solver::collect_statistics (statistics &st) const {
m_solver.collect_statistics (st);
st.update ("time.iuc_solver.get_iuc", m_iuc_sw.get_seconds());
st.update ("time.iuc_solver.get_iuc.hyp_reduce1", m_hyp_reduce1_sw.get_seconds());
st.update ("time.iuc_solver.get_iuc.hyp_reduce2", m_hyp_reduce2_sw.get_seconds());
st.update ("time.iuc_solver.get_iuc.learn_core", m_learn_core_sw.get_seconds());
st.update("iuc_solver.num_proxies", m_proxies.size());
}
void iuc_solver::reset_statistics () {
m_iuc_sw.reset();
m_hyp_reduce1_sw.reset();
m_hyp_reduce2_sw.reset();
m_learn_core_sw.reset();
}
void iuc_solver::get_unsat_core (expr_ref_vector &core) {
m_solver.get_unsat_core (core);
undo_proxies_in_core (core);
}
void iuc_solver::undo_proxies_in_core (expr_ref_vector &r) {
app_ref e(m);
expr_fast_mark1 bg;
for (unsigned i = 0; i < m_first_assumption; ++i) {
bg.mark(m_assumptions.get(i));
}
// expand proxies
unsigned j = 0;
for (expr* rr : r) {
// skip background assumptions
if (bg.is_marked(rr))
continue;
// -- undo proxies, but only if they were introduced in check_sat
if (m_is_proxied && is_proxy(rr, e)) {
SASSERT (m.is_or (e));
r[j++] = e->get_arg (1);
}
else {
r[j++] = rr;
}
}
r.shrink (j);
}
void iuc_solver::undo_proxies (expr_ref_vector &r) {
app_ref e(m);
// expand proxies
for (unsigned i = 0, sz = r.size (); i < sz; ++i)
if (is_proxy(r.get(i), e)) {
SASSERT (m.is_or (e));
r[i] = e->get_arg (1);
}
}
void iuc_solver::elim_proxies (expr_ref_vector &v) {
expr_ref f = mk_and (v);
scoped_ptr<expr_replacer> rep = mk_expr_simp_replacer (m);
rep->set_substitution (&m_elim_proxies_sub);
(*rep)(f);
v.reset();
flatten_and(f, v);
}
void iuc_solver::get_iuc(expr_ref_vector &core) {
scoped_watch _t_ (m_iuc_sw);
typedef obj_hashtable<expr> expr_set;
expr_set core_lits;
for (unsigned i = m_first_assumption, sz = m_assumptions.size(); i < sz; ++i) {
expr *a = m_assumptions.get (i);
app_ref def(m);
if (is_proxy(a, def)) { core_lits.insert(def.get()); }
core_lits.insert (a);
}
if (m_iuc == 0) {
// ORIGINAL PDR CODE
// AG: deprecated
proof_ref pr(m);
pr = get_proof ();
farkas_learner learner_old;
learner_old.set_split_literals(m_split_literals);
learner_old.get_lemmas (pr, core_lits, core);
elim_proxies (core);
simplify_bounds (core); // XXX potentially redundant
}
else {
r[j++] = rr;
}
}
r.shrink (j);
}
void iuc_solver::undo_proxies (expr_ref_vector &r)
{
app_ref e(m);
// expand proxies
for (unsigned i = 0, sz = r.size (); i < sz; ++i)
if (is_proxy(r.get(i), e)) {
SASSERT (m.is_or (e));
r[i] = e->get_arg (1);
}
}
void iuc_solver::elim_proxies (expr_ref_vector &v)
{
expr_ref f = mk_and (v);
scoped_ptr<expr_replacer> rep = mk_expr_simp_replacer (m);
rep->set_substitution (&m_elim_proxies_sub);
(*rep)(f);
v.reset();
flatten_and(f, v);
}
void iuc_solver::get_iuc(expr_ref_vector &core)
{
scoped_watch _t_ (m_iuc_sw);
typedef obj_hashtable<expr> expr_set;
expr_set core_lits;
for (unsigned i = m_first_assumption, sz = m_assumptions.size(); i < sz; ++i) {
expr *a = m_assumptions.get (i);
app_ref def(m);
if (is_proxy(a, def)) { core_lits.insert(def.get()); }
core_lits.insert (a);
}
if (m_iuc == 0) {
// ORIGINAL PDR CODE
// AG: deprecated
proof_ref pr(m);
pr = get_proof ();
farkas_learner learner_old;
learner_old.set_split_literals(m_split_literals);
learner_old.get_lemmas (pr, core_lits, core);
elim_proxies (core);
simplify_bounds (core); // XXX potentially redundant
}
else {
// NEW IUC
proof_ref res(get_proof(), m);
// -- old hypothesis reducer while the new one is broken
if (m_old_hyp_reducer) {
scoped_watch _t_ (m_hyp_reduce1_sw);
// AG: deprecated
// pre-process proof in order to get a proof which is
// better suited for unsat-core-extraction
if (m_print_farkas_stats) {
iuc_proof iuc_before(m, res.get(), core_lits);
verbose_stream() << "\nOld reduce_hypotheses. Before:";
iuc_before.dump_farkas_stats();
// NEW IUC
proof_ref res(get_proof(), m);
// -- old hypothesis reducer while the new one is broken
if (m_old_hyp_reducer) {
scoped_watch _t_ (m_hyp_reduce1_sw);
// AG: deprecated
// pre-process proof in order to get a proof which is
// better suited for unsat-core-extraction
if (m_print_farkas_stats) {
iuc_proof iuc_before(m, res.get(), core_lits);
verbose_stream() << "\nOld reduce_hypotheses. Before:";
iuc_before.dump_farkas_stats();
}
proof_utils::reduce_hypotheses(res);
proof_utils::permute_unit_resolution(res);
if (m_print_farkas_stats) {
iuc_proof iuc_after(m, res.get(), core_lits);
verbose_stream() << "Old reduce_hypothesis. After:";
iuc_after.dump_farkas_stats();
}
}
proof_utils::reduce_hypotheses(res);
proof_utils::permute_unit_resolution(res);
if (m_print_farkas_stats) {
iuc_proof iuc_after(m, res.get(), core_lits);
verbose_stream() << "Old reduce_hypothesis. After:";
iuc_after.dump_farkas_stats();
}
}
// -- new hypothesis reducer
else
{
// -- new hypothesis reducer
else
{
#if 0
static unsigned bcnt = 0;
static unsigned bcnt = 0;
{
bcnt++;
TRACE("spacer", tout << "Dumping pf bcnt: " << bcnt << "\n";);
if (bcnt == 123) {
std::ofstream ofs;
ofs.open("/tmp/bpf_" + std::to_string(bcnt) + ".dot");
iuc_proof iuc_pf_before(m, res.get(), core_lits);
iuc_pf_before.display_dot(ofs);
ofs.close();
proof_checker pc(m);
expr_ref_vector side(m);
ENSURE(pc.check(res, side));
}
}
#endif
scoped_watch _t_ (m_hyp_reduce2_sw);
// pre-process proof for better iuc extraction
if (m_print_farkas_stats) {
iuc_proof iuc_before(m, res.get(), core_lits);
verbose_stream() << "\n New hypothesis_reducer. Before:";
iuc_before.dump_farkas_stats();
}
proof_ref pr1(m);
{
scoped_watch _t_ (m_hyp_reduce1_sw);
theory_axiom_reducer ta_reducer(m);
pr1 = ta_reducer.reduce (res.get());
}
proof_ref pr2(m);
{
scoped_watch _t_ (m_hyp_reduce2_sw);
hypothesis_reducer hyp_reducer(m);
pr2 = hyp_reducer.reduce(pr1);
}
res = pr2;
if (m_print_farkas_stats) {
iuc_proof iuc_after(m, res.get(), core_lits);
verbose_stream() << "New hypothesis_reducer. After:";
iuc_after.dump_farkas_stats();
}
}
iuc_proof iuc_pf(m, res, core_lits);
#if 0
static unsigned cnt = 0;
{
bcnt++;
TRACE("spacer", tout << "Dumping pf bcnt: " << bcnt << "\n";);
if (bcnt == 123) {
cnt++;
TRACE("spacer", tout << "Dumping pf cnt: " << cnt << "\n";);
if (cnt == 123) {
std::ofstream ofs;
ofs.open("/tmp/bpf_" + std::to_string(bcnt) + ".dot");
iuc_proof iuc_pf_before(m, res.get(), core_lits);
iuc_pf_before.display_dot(ofs);
ofs.open("/tmp/pf_" + std::to_string(cnt) + ".dot");
iuc_pf.display_dot(ofs);
ofs.close();
proof_checker pc(m);
expr_ref_vector side(m);
ENSURE(pc.check(res, side));
}
}
#endif
scoped_watch _t_ (m_hyp_reduce2_sw);
// pre-process proof for better iuc extraction
if (m_print_farkas_stats) {
iuc_proof iuc_before(m, res.get(), core_lits);
verbose_stream() << "\n New hypothesis_reducer. Before:";
iuc_before.dump_farkas_stats();
unsat_core_learner learner(m, iuc_pf);
unsat_core_plugin* plugin;
// -- register iuc plugins
switch (m_iuc_arith) {
case 0:
case 1:
plugin =
alloc(unsat_core_plugin_farkas_lemma,
learner, m_split_literals,
(m_iuc_arith == 1) /* use constants from A */);
learner.register_plugin(plugin);
break;
case 2:
SASSERT(false && "Broken");
plugin = alloc(unsat_core_plugin_farkas_lemma_optimized, learner, m);
learner.register_plugin(plugin);
break;
case 3:
plugin = alloc(unsat_core_plugin_farkas_lemma_bounded, learner, m);
learner.register_plugin(plugin);
break;
default:
UNREACHABLE();
break;
}
proof_ref pr1(m);
switch (m_iuc) {
case 1:
// -- iuc based on the lowest cut in the proof
plugin = alloc(unsat_core_plugin_lemma, learner);
learner.register_plugin(plugin);
break;
case 2:
// -- iuc based on the smallest cut in the proof
plugin = alloc(unsat_core_plugin_min_cut, learner, m);
learner.register_plugin(plugin);
break;
default:
UNREACHABLE();
break;
}
{
scoped_watch _t_ (m_hyp_reduce1_sw);
theory_axiom_reducer ta_reducer(m);
pr1 = ta_reducer.reduce (res.get());
}
proof_ref pr2(m);
{
scoped_watch _t_ (m_hyp_reduce2_sw);
hypothesis_reducer hyp_reducer(m);
pr2 = hyp_reducer.reduce(pr1);
}
res = pr2;
if (m_print_farkas_stats) {
iuc_proof iuc_after(m, res.get(), core_lits);
verbose_stream() << "New hypothesis_reducer. After:";
iuc_after.dump_farkas_stats();
scoped_watch _t_ (m_learn_core_sw);
// compute interpolating unsat core
learner.compute_unsat_core(core);
}
elim_proxies (core);
// AG: this should be taken care of by minimizing the iuc cut
simplify_bounds (core);
}
iuc_proof iuc_pf(m, res, core_lits);
#if 0
static unsigned cnt = 0;
{
cnt++;
TRACE("spacer", tout << "Dumping pf cnt: " << cnt << "\n";);
if (cnt == 123) {
std::ofstream ofs;
ofs.open("/tmp/pf_" + std::to_string(cnt) + ".dot");
iuc_pf.display_dot(ofs);
ofs.close();
proof_checker pc(m);
expr_ref_vector side(m);
ENSURE(pc.check(res, side));
}
}
#endif
unsat_core_learner learner(m, iuc_pf);
unsat_core_plugin* plugin;
// -- register iuc plugins
switch (m_iuc_arith) {
case 0:
case 1:
plugin =
alloc(unsat_core_plugin_farkas_lemma,
learner, m_split_literals,
(m_iuc_arith == 1) /* use constants from A */);
learner.register_plugin(plugin);
break;
case 2:
SASSERT(false && "Broken");
plugin = alloc(unsat_core_plugin_farkas_lemma_optimized, learner, m);
learner.register_plugin(plugin);
break;
case 3:
plugin = alloc(unsat_core_plugin_farkas_lemma_bounded, learner, m);
learner.register_plugin(plugin);
break;
default:
UNREACHABLE();
break;
}
switch (m_iuc) {
case 1:
// -- iuc based on the lowest cut in the proof
plugin = alloc(unsat_core_plugin_lemma, learner);
learner.register_plugin(plugin);
break;
case 2:
// -- iuc based on the smallest cut in the proof
plugin = alloc(unsat_core_plugin_min_cut, learner, m);
learner.register_plugin(plugin);
break;
default:
UNREACHABLE();
break;
}
{
scoped_watch _t_ (m_learn_core_sw);
// compute interpolating unsat core
learner.compute_unsat_core(core);
}
elim_proxies (core);
// AG: this should be taken care of by minimizing the iuc cut
simplify_bounds (core);
IF_VERBOSE(2,
verbose_stream () << "IUC Core:\n" << core << "\n";);
}
IF_VERBOSE(2,
verbose_stream () << "IUC Core:\n" << core << "\n";);
}
void iuc_solver::refresh ()
{
// only refresh in non-pushed state
SASSERT (m_defs.empty());
expr_ref_vector assertions (m);
for (unsigned i = 0, e = m_solver.get_num_assertions(); i < e; ++i) {
expr* a = m_solver.get_assertion (i);
if (!m_base_defs.is_proxy_def(a)) { assertions.push_back(a); }
void iuc_solver::refresh () {
// only refresh in non-pushed state
SASSERT (m_defs.empty());
expr_ref_vector assertions (m);
for (unsigned i = 0, e = m_solver.get_num_assertions(); i < e; ++i) {
expr* a = m_solver.get_assertion (i);
if (!m_base_defs.is_proxy_def(a)) { assertions.push_back(a); }
}
m_base_defs.reset ();
NOT_IMPLEMENTED_YET ();
// solver interface does not have a reset method. need to introduce it somewhere.
// m_solver.reset ();
for (unsigned i = 0, e = assertions.size (); i < e; ++i)
{ m_solver.assert_expr(assertions.get(i)); }
}
m_base_defs.reset ();
NOT_IMPLEMENTED_YET ();
// solver interface does not have a reset method. need to introduce it somewhere.
// m_solver.reset ();
for (unsigned i = 0, e = assertions.size (); i < e; ++i)
{ m_solver.assert_expr(assertions.get(i)); }
}
}

2
src/muz/spacer/spacer_iuc_solver.h
View file

@ -127,7 +127,7 @@ public:
void pop(unsigned n) override;
unsigned get_scope_level() const override { return m_solver.get_scope_level(); }
lbool check_sat(unsigned num_assumptions, expr * const *assumptions) override;
lbool check_sat_core(unsigned num_assumptions, expr * const *assumptions) override;
lbool check_sat_cc(const expr_ref_vector &cube, vector<expr_ref_vector> const & clauses) override;
void set_progress_callback(progress_callback *callback) override {
m_solver.set_progress_callback(callback);

1
src/opt/CMakeLists.txt
View file

@ -1,5 +1,6 @@
z3_add_component(opt
SOURCES
maxlex.cpp
maxres.cpp
maxsmt.cpp
opt_cmds.cpp

272
src/opt/maxlex.cpp Normal file
View file

@ -0,0 +1,272 @@
/*++
Copyright (c) 2019 Microsoft Corporation
Module Name:
maxlex.cpp
Abstract:
MaxLex solves weighted max-sat problems where weights impose lexicographic order.
MaxSAT is particularly easy for this class:
In order of highest weight, check if soft constraint can be satisfied.
If so, assert it, otherwise assert the negation and record whether the soft
constraint is true or false in the solution.
Author:
Nikolaj Bjorner (nbjorner) 2019-25-1
--*/
#include "opt/opt_context.h"
#include "opt/maxsmt.h"
#include "opt/maxlex.h"
namespace opt {
bool is_maxlex(weights_t & _ws) {
// disable for now
#if true
return false;
#else
vector<rational> ws(_ws);
std::sort(ws.begin(), ws.end());
ws.reverse();
rational sum(0);
for (rational const& w : ws) {
sum += w;
}
for (rational const& w : ws) {
if (sum > w + w) return false;
sum -= w;
}
return true;
#endif
}
class maxlex : public maxsmt_solver_base {
struct cmp_soft {
bool operator()(soft const& s1, soft const& s2) const {
return s1.weight > s2.weight;
}
};
ast_manager& m;
maxsat_context& m_c;
void update_assignment() {
model_ref mdl;
s().get_model(mdl);
if (mdl) {
m_model = mdl;
m_c.model_updated(mdl.get());
update_assignment(mdl);
}
}
void assert_value(soft& soft) {
switch (soft.value) {
case l_true:
s().assert_expr(soft.s);
break;
case l_false:
s().assert_expr(expr_ref(m.mk_not(soft.s), m));
break;
default:
break;
}
}
void set_value(soft& soft, lbool v) {
soft.set_value(v);
assert_value(soft);
}
void update_assignment(model_ref & mdl) {
bool prefix_defined = true;
for (auto & soft : m_soft) {
if (!prefix_defined) {
set_value(soft, l_undef);
continue;
}
switch (soft.value) {
case l_undef:
prefix_defined = mdl->is_true(soft.s);
set_value(soft, prefix_defined ? l_true : l_undef);
break;
case l_true:
break;
case l_false:
break;
}
}
update_bounds();
}
void update_bounds() {
m_lower.reset();
m_upper.reset();
bool prefix_defined = true;
for (auto & soft : m_soft) {
if (!prefix_defined) {
m_upper += soft.weight;
continue;
}
switch (soft.value) {
case l_undef:
prefix_defined = false;
m_upper += soft.weight;
break;
case l_true:
break;
case l_false:
m_lower += soft.weight;
m_upper += soft.weight;
break;
}
}
trace_bounds("maxlex");
}
void init() {
model_ref mdl;
s().get_model(mdl);
update_assignment(mdl);
}
lbool maxlex1() {
for (auto & soft : m_soft) {
if (soft.value == l_true) {
continue;
}
SASSERT(soft.value() == l_undef);
expr* a = soft.s;
lbool is_sat = s().check_sat(1, &a);
switch (is_sat) {
case l_false:
set_value(soft, l_false);
update_bounds();
break;
case l_true:
update_assignment();
SASSERT(soft.value == l_true);
break;
case l_undef:
return l_undef;
}
}
return l_true;
}
// try two literals per round.
// doesn't seem to make a difference based on sample test.
lbool maxlex2() {
unsigned sz = m_soft.size();
for (unsigned i = 0; i < sz; ++i) {
auto& soft = m_soft[i];
if (soft.value != l_undef) {
continue;
}
SASSERT(soft.value() == l_undef);
if (i + 1 == sz) {
expr* a = soft.s;
lbool is_sat = s().check_sat(1, &a);
switch (is_sat) {
case l_false:
set_value(soft, l_false);
update_bounds();
break;
case l_true:
update_assignment();
SASSERT(soft.value == l_true);
break;
case l_undef:
return l_undef;
}
}
else {
auto& soft2 = m_soft[i+1];
expr_ref_vector core(m);
expr* a = soft.s;
expr* b = soft2.s;
expr* asms[2] = { a, b };
lbool is_sat = s().check_sat(2, asms);
switch (is_sat) {
case l_true:
update_assignment();
SASSERT(soft.value == l_true);
SASSERT(soft2.value == l_true);
break;
case l_false:
s().get_unsat_core(core);
if (core.contains(b)) {
expr_ref not_b(mk_not(m, b), m);
asms[1] = not_b;
switch (s().check_sat(2, asms)) {
case l_true:
// a, b is unsat, a, not b is sat.
set_value(soft2, l_false);
update_assignment();
SASSERT(soft.value == l_true);
SASSERT(soft2.value == l_false);
break;
case l_false:
// a, b is unsat, a, not b is unsat -> a is unsat
// b is unsat, a, not b is unsat -> not a, not b
set_value(soft, l_false);
if (!core.contains(a)) {
set_value(soft2, l_false);
}
update_bounds();
break;
case l_undef:
return l_undef;
}
}
else {
set_value(soft, l_false);
update_bounds();
}
break;
case l_undef:
return l_undef;
}
}
}
return l_true;
}
public:
maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& s):
maxsmt_solver_base(c, ws, s),
m(c.get_manager()),
m_c(c) {
// ensure that soft constraints are sorted with largest soft constraints first.
cmp_soft cmp;
std::sort(m_soft.begin(), m_soft.end(), cmp);
}
lbool operator()() override {
init();
return maxlex1();
}
void commit_assignment() override {
for (auto & soft : m_soft) {
if (soft.value == l_undef) {
return;
}
assert_value(soft);
}
}
};
maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft) {
return alloc(maxlex, c, id, ws, soft);
}
}

32
src/opt/maxlex.h Normal file
View file

@ -0,0 +1,32 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
maxlex.h
Abstract:
MaxLex solves weighted max-sat problems where weights impose lexicographic order.
Author:
Nikolaj Bjorner (nbjorner) 2019-25-1
Notes:
--*/
#ifndef MAXLEX_H_
#define MAXLEX_H_
namespace opt {
bool is_maxlex(weights_t & ws);
maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft);
};
#endif

8
src/opt/maxres.cpp
View file

@ -329,8 +329,8 @@ public:
verify_assumptions();
m_lower.reset();
for (soft& s : m_soft) {
s.is_true = m_model->is_true(s.s);
if (!s.is_true) {
s.set_value(m_model->is_true(s.s));
if (!s.is_true()) {
m_lower += s.weight;
}
}
@ -764,7 +764,7 @@ public:
TRACE("opt", tout << "updated upper: " << upper << "\nmodel\n" << *m_model;);
for (soft& s : m_soft) {
s.is_true = m_model->is_true(s.s);
s.set_value(m_model->is_true(s.s));
}
verify_assignment();
@ -878,7 +878,7 @@ public:
expr_ref n(m);
for (soft& s : m_soft) {
n = s.s;
if (!s.is_true) {
if (!s.is_true()) {
n = mk_not(m, n);
}
_solver->assert_expr(n);

22
src/opt/maxsmt.cpp
View file

@ -18,17 +18,18 @@ Notes:
--*/
#include <typeinfo>
#include "util/uint_set.h"
#include "ast/ast_pp.h"
#include "ast/ast_util.h"
#include "ast/pb_decl_plugin.h"
#include "opt/maxsmt.h"
#include "opt/maxres.h"
#include "opt/maxlex.h"
#include "opt/wmax.h"
#include "opt/opt_params.hpp"
#include "ast/ast_pp.h"
#include "util/uint_set.h"
#include "opt/opt_context.h"
#include "smt/theory_wmaxsat.h"
#include "smt/theory_pb.h"
#include "ast/ast_util.h"
#include "ast/pb_decl_plugin.h"
namespace opt {
@ -61,7 +62,7 @@ namespace opt {
rational k(0), cost(0);
vector<rational> weights;
for (soft const& s : m_soft) {
if (s.is_true) {
if (s.is_true()) {
k += s.weight;
}
else {
@ -80,13 +81,13 @@ namespace opt {
m_lower.reset();
m_upper.reset();
for (soft& s : m_soft) {
s.is_true = m.is_true(s.s);
if (!s.is_true) m_upper += s.weight;
s.set_value(m.is_true(s.s));
if (!s.is_true()) m_upper += s.weight;
}
TRACE("opt",
tout << "upper: " << m_upper << " assignments: ";
for (soft& s : m_soft) tout << (s.is_true?"T":"F");
for (soft& s : m_soft) tout << (s.is_true()?"T":"F");
tout << "\n";);
return true;
}
@ -234,7 +235,10 @@ namespace opt {
symbol const& maxsat_engine = m_c.maxsat_engine();
IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
TRACE("opt_verbose", s().display(tout << "maxsmt\n") << "\n";);
if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {
if (is_maxlex(m_weights)) {
m_msolver = mk_maxlex(m_c, m_index, m_weights, m_soft_constraints);
}
else if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {
m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
}
else if (maxsat_engine == symbol("pd-maxres")) {

13
src/opt/maxsmt.h
View file

@ -59,10 +59,13 @@ namespace opt {
struct soft {
expr_ref s;
rational weight;
bool is_true;
soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), is_true(t) {}
soft(soft const& other):s(other.s), weight(other.weight), is_true(other.is_true) {}
soft& operator=(soft const& other) { s = other.s; weight = other.weight; is_true = other.is_true; return *this; }
lbool value;
void set_value(bool t) { value = t?l_true:l_undef; }
void set_value(lbool t) { value = t; }
bool is_true() const { return value == l_true; }
soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), value(t?l_true:l_undef) {}
soft(soft const& other):s(other.s), weight(other.weight), value(other.value) {}
soft& operator=(soft const& other) { s = other.s; weight = other.weight; value = other.value; return *this; }
};
ast_manager& m;
maxsat_context& m_c;
@ -84,7 +87,7 @@ namespace opt {
~maxsmt_solver_base() override {}
rational get_lower() const override { return m_lower; }
rational get_upper() const override { return m_upper; }
bool get_assignment(unsigned index) const override { return m_soft[index].is_true; }
bool get_assignment(unsigned index) const override { return m_soft[index].is_true(); }
void collect_statistics(statistics& st) const override { }
void get_model(model_ref& mdl, svector<symbol>& labels) override { mdl = m_model.get(); labels = m_labels;}
virtual void commit_assignment();

2
src/opt/opt_solver.cpp
View file

@ -158,7 +158,7 @@ namespace opt {
return m_dump_benchmarks;
}
lbool opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
lbool opt_solver::check_sat_core2(unsigned num_assumptions, expr * const * assumptions) {
TRACE("opt_verbose", {
tout << "context size: " << m_context.size() << "\n";
for (unsigned i = 0; i < m_context.size(); ++i) {

2
src/opt/opt_solver.h
View file

@ -95,7 +95,7 @@ namespace opt {
void assert_expr_core(expr * t) override;
void push_core() override;
void pop_core(unsigned n) override;
lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override;
lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override;
void get_unsat_core(expr_ref_vector & r) override;
void get_model_core(model_ref & _m) override;
proof * get_proof() override;

2
src/opt/sortmax.cpp
View file

@ -114,7 +114,7 @@ namespace opt {
}
void update_assignment() {
for (soft& s : m_soft) s.is_true = is_true(s.s);
for (soft& s : m_soft) s.set_value(is_true(s.s));
}
bool is_true(expr* e) {

2
src/opt/wmax.cpp
View file

@ -122,7 +122,7 @@ namespace opt {
}
void update_assignment() {
for (soft& s : m_soft) s.is_true = is_true(s.s);
for (soft& s : m_soft) s.set_value(is_true(s.s));
}
struct compare_asm {

5
src/sat/ba_solver.cpp
View file

@ -2837,7 +2837,7 @@ namespace sat {
void ba_solver::simplify() {
if (!s().at_base_lvl()) s().pop_to_base_level();
unsigned trail_sz;
unsigned trail_sz, count = 0;
do {
trail_sz = s().init_trail_size();
m_simplify_change = false;
@ -2855,8 +2855,9 @@ namespace sat {
cleanup_clauses();
cleanup_constraints();
update_pure();
++count;
}
while (m_simplify_change || trail_sz < s().init_trail_size());
while (count < 10 && (m_simplify_change || trail_sz < s().init_trail_size()));
IF_VERBOSE(1, verbose_stream() << "(ba.simplify"
<< " :vars " << s().num_vars() - trail_sz

24
src/sat/sat_big.cpp
View file

@ -164,22 +164,23 @@ namespace sat {
DEBUG_CODE(for (unsigned i = 0; i < num_lits; ++i) { VERIFY(m_left[i] < m_right[i]);});
}
// svector<std::pair<literal, literal>> big::s_del_bin;
bool big::in_del(literal u, literal v) const {
if (u.index() > v.index()) std::swap(u, v);
return m_del_bin.contains(std::make_pair(u, v));
return m_del_bin[u.index()].contains(v);
}
void big::add_del(literal u, literal v) {
if (u.index() > v.index()) std::swap(u, v);
m_del_bin.push_back(std::make_pair(u, v));
m_del_bin[u.index()].push_back(v);
}
unsigned big::reduce_tr(solver& s) {
unsigned idx = 0;
unsigned elim = 0;
m_del_bin.reset();
m_del_bin.reserve(s.m_watches.size());
for (watch_list & wlist : s.m_watches) {
if (s.inconsistent()) break;
literal u = to_literal(idx++);
@ -210,23 +211,6 @@ namespace sat {
}
wlist.set_end(itprev);
}
#if 0
s_del_bin.append(m_del_bin);
IF_VERBOSE(1,
display(verbose_stream() << "Learned: " << learned() << ":");
verbose_stream() << "del-bin\n";
for (auto p : m_del_bin) {
verbose_stream() << p.first << " " << p.second << "\n";
if (safe_reach(~p.first, p.second)) {
display_path(verbose_stream(), ~p.first, p.second) << " " << "\n";
}
else {
display_path(verbose_stream(), ~p.second, p.first) << " " << "\n";
}
}
);
#endif
s.propagate(false);
return elim;
}

2
src/sat/sat_big.h
View file

@ -36,7 +36,7 @@ namespace sat {
bool m_learned;
bool m_include_cardinality;
svector<std::pair<literal, literal>> m_del_bin;
vector<svector<literal> > m_del_bin;
void init_dfs_num();

8
src/sat/sat_scc.cpp
View file

@ -244,10 +244,10 @@ namespace sat {
}
void scc::reduce_tr() {
unsigned quota = 0, num_reduced = 0;
while ((num_reduced = reduce_tr(false)) > quota) { quota = std::max(100u, num_reduced / 2); }
quota = 0;
while ((num_reduced = reduce_tr(true)) > quota) { quota = std::max(100u, num_reduced / 2); }
unsigned quota = 0, num_reduced = 0, count = 0;
while ((num_reduced = reduce_tr(false)) > quota && count++ < 10) { quota = std::max(100u, num_reduced / 2); }
quota = 0; count = 0;
while ((num_reduced = reduce_tr(true)) > quota && count++ < 10) { quota = std::max(100u, num_reduced / 2); }
}
void scc::collect_statistics(statistics & st) const {

36
src/sat/sat_simplifier.cpp
View file

@ -1014,6 +1014,9 @@ namespace sat {
svector<bool> m_in_intersection;
unsigned m_ala_qhead;
clause_wrapper m_clause;
unsigned m_ala_cost;
unsigned m_ala_benefit;
unsigned m_ala_max_cost;
blocked_clause_elim(simplifier & _s, unsigned limit, model_converter & _mc, use_list & l,
vector<watch_list> & wlist):
@ -1021,8 +1024,11 @@ namespace sat {
m_counter(limit),
m_mc(_mc),
m_queue(l, wlist),
m_clause(null_literal, null_literal) {
m_clause(null_literal, null_literal),
m_ala_cost(0),
m_ala_benefit(0) {
m_in_intersection.resize(s.s.num_vars() * 2, false);
m_ala_max_cost = (s.s.m_clauses.size() * s.m_num_calls)/5;
}
void insert(literal l) {
@ -1034,6 +1040,10 @@ namespace sat {
return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v) && s.value(v) == l_undef;
}
bool reached_max_cost() {
return m_ala_benefit <= m_ala_cost * 100 && m_ala_cost > m_ala_max_cost;
}
enum elim_type {
bce_t,
cce_t,
@ -1296,13 +1306,15 @@ namespace sat {
*/
bool add_ala() {
unsigned init_size = m_covered_clause.size();
for (; m_ala_qhead < m_covered_clause.size() && m_ala_qhead < 5*init_size; ++m_ala_qhead) {
for (; m_ala_qhead < m_covered_clause.size() && m_ala_qhead < 5*init_size && !reached_max_cost(); ++m_ala_qhead) {
++m_ala_cost;
literal l = m_covered_clause[m_ala_qhead];
for (watched & w : s.get_wlist(~l)) {
if (w.is_binary_non_learned_clause()) {
literal lit = w.get_literal();
if (revisit_binary(l, lit)) continue;
if (s.is_marked(lit)) {
++m_ala_benefit;
return true;
}
if (!s.is_marked(~lit)) {
@ -1333,6 +1345,7 @@ namespace sat {
}
if (!ok) continue;
if (lit1 == null_literal) {
++m_ala_benefit;
return true;
}
m_covered_clause.push_back(~lit1);
@ -1504,7 +1517,9 @@ namespace sat {
template<elim_type et>
void cce_binary() {
while (!m_queue.empty() && m_counter >= 0) {
m_ala_cost = 0;
m_ala_benefit = 0;
while (!m_queue.empty() && m_counter >= 0 && !reached_max_cost()) {
s.checkpoint();
process_cce_binary<et>(m_queue.next());
}
@ -1516,7 +1531,7 @@ namespace sat {
watch_list & wlist = s.get_wlist(~l);
m_counter -= wlist.size();
model_converter::kind k;
for (watched & w : wlist) {
for (watched& w : wlist) {
if (!w.is_binary_non_learned_clause()) continue;
if (!select_clause<et>(2)) continue;
literal l2 = w.get_literal();
@ -1543,9 +1558,13 @@ namespace sat {
template<elim_type et>
void cce_clauses() {
literal blocked;
m_ala_cost = 0;
m_ala_benefit = 0;
model_converter::kind k;
for (clause* cp : s.s.m_clauses) {
clause& c = *cp;
unsigned start = s.s.m_rand();
unsigned sz = s.s.m_clauses.size();
for (unsigned i = 0; i < sz; ++i) {
clause& c = *s.s.m_clauses[(i + start) % sz];
if (c.was_removed() || c.is_learned()) continue;
if (!select_clause<et>(c.size())) continue;
elim_type r = cce<et>(c, blocked, k);
@ -1563,7 +1582,10 @@ namespace sat {
break;
}
s.checkpoint();
}
if (reached_max_cost()) {
break;
}
}
}
void inc_bc(elim_type et) {

2
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -166,7 +166,7 @@ public:
(m.is_not(e, e) && is_uninterp_const(e));
}
lbool check_sat(unsigned sz, expr * const * assumptions) override {
lbool check_sat_core(unsigned sz, expr * const * assumptions) override {
m_solver.pop_to_base_level();
m_core.reset();
if (m_solver.inconsistent()) return l_false;

1
src/sat/tactic/goal2sat.cpp
View file

@ -82,7 +82,6 @@ struct goal2sat::imp {
m_is_lemma(false) {
updt_params(p);
m_true = sat::null_bool_var;
mk_true();
}
void updt_params(params_ref const & p) {

2
src/smt/smt_solver.cpp
View file

@ -185,7 +185,7 @@ namespace smt {
m_context.pop(n);
}
lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override {
lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override {
TRACE("solver_na2as", tout << "smt_solver::check_sat_core: " << num_assumptions << "\n";);
return m_context.check(num_assumptions, assumptions);
}

16
src/smt/theory_lra.cpp
View file

@ -483,22 +483,6 @@ class theory_lra::imp {
if (ctx().relevancy()) ctx().add_relevancy_dependency(n, mod);
}
else if (a.is_mod(n, n1, n2)) {
bool is_num = a.is_numeral(n2, r) && !r.is_zero();
if (!is_num) {
found_not_handled(n);
}
#if 0
else {
app_ref div(a.mk_idiv(n1, n2), m);
mk_enode(div);
theory_var w = mk_var(div);
theory_var u = mk_var(n1);
// add axioms:
// u = v + r*w
// abs(r) > v >= 0
assert_idiv_mod_axioms(u, v, w, r);
}
#endif
if (!ctx().relevancy()) mk_idiv_mod_axioms(n1, n2);
}
else if (a.is_rem(n, n1, n2)) {

2
src/solver/CMakeLists.txt
View file

@ -16,5 +16,7 @@ z3_add_component(solver
PYG_FILES
combined_solver_params.pyg
parallel_params.pyg
PYG_FILES
solver_params.pyg
)

10
src/solver/combined_solver.cpp
View file

@ -218,7 +218,7 @@ public:
return l_undef;
}
lbool check_sat(unsigned num_assumptions, expr * const * assumptions) override {
lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override {
m_check_sat_executed = true;
m_use_solver1_results = false;
@ -227,13 +227,13 @@ public:
m_ignore_solver1) {
// must use incremental solver
switch_inc_mode();
return m_solver2->check_sat(num_assumptions, assumptions);
return m_solver2->check_sat_core(num_assumptions, assumptions);
}
if (m_inc_mode) {
if (m_inc_timeout == UINT_MAX) {
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 2 (without a timeout)\")\n";);
lbool r = m_solver2->check_sat(num_assumptions, assumptions);
lbool r = m_solver2->check_sat_core(num_assumptions, assumptions);
if (r != l_undef || !use_solver1_when_undef() || get_manager().canceled()) {
return r;
}
@ -244,7 +244,7 @@ public:
lbool r = l_undef;
try {
scoped_timer timer(m_inc_timeout, &eh);
r = m_solver2->check_sat(num_assumptions, assumptions);
r = m_solver2->check_sat_core(num_assumptions, assumptions);
}
catch (z3_exception&) {
if (!eh.m_canceled) {
@ -260,7 +260,7 @@ public:
IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 1\")\n";);
m_use_solver1_results = true;
return m_solver1->check_sat(num_assumptions, assumptions);
return m_solver1->check_sat_core(num_assumptions, assumptions);
}
void set_progress_callback(progress_callback * callback) override {

2
src/solver/parallel_tactic.cpp
View file

@ -213,7 +213,7 @@ class parallel_tactic : public tactic {
solver_state* clone() {
SASSERT(!m_cubes.empty());
ast_manager& m = m_solver->get_manager();
ast_manager* new_m = alloc(ast_manager, m, m.proof_mode());
ast_manager* new_m = alloc(ast_manager, m, true);
ast_translation tr(m, *new_m);
solver* s = m_solver.get()->translate(*new_m, m_params);
solver_state* st = alloc(solver_state, new_m, s, m_params);

49
src/solver/solver.cpp
View file

@ -3,7 +3,7 @@ Copyright (c) 2011 Microsoft Corporation
Module Name:
solver.h
solver.cpp
Abstract:
@ -21,25 +21,25 @@ Notes:
#include "ast/ast_util.h"
#include "ast/ast_pp.h"
#include "ast/ast_pp_util.h"
#include "ast/display_dimacs.h"
#include "tactic/model_converter.h"
#include "solver/solver.h"
#include "solver/solver_params.hpp"
#include "model/model_evaluator.h"
unsigned solver::get_num_assertions() const {
NOT_IMPLEMENTED_YET();
UNREACHABLE();
return 0;
}
expr * solver::get_assertion(unsigned idx) const {
NOT_IMPLEMENTED_YET();
UNREACHABLE();
return nullptr;
}
std::ostream& solver::display(std::ostream & out, unsigned n, expr* const* assumptions) const {
expr_ref_vector fmls(get_manager());
stopwatch sw;
sw.start();
get_assertions(fmls);
ast_pp_util visitor(get_manager());
model_converter_ref mc = get_model_converter();
@ -57,6 +57,12 @@ std::ostream& solver::display(std::ostream & out, unsigned n, expr* const* assum
return out;
}
std::ostream& solver::display_dimacs(std::ostream& out) const {
expr_ref_vector fmls(get_manager());
get_assertions(fmls);
return ::display_dimacs(out, fmls);
}
void solver::get_assertions(expr_ref_vector& fmls) const {
unsigned sz = get_num_assertions();
for (unsigned i = 0; i < sz; ++i) {
@ -232,12 +238,16 @@ void solver::collect_param_descrs(param_descrs & r) {
void solver::reset_params(params_ref const & p) {
m_params = p;
m_enforce_model_conversion = m_params.get_bool("solver.enforce_model_conversion", false);
solver_params sp(m_params);
m_enforce_model_conversion = sp.enforce_model_conversion();
m_cancel_backup_file = sp.cancel_backup_file();
}
void solver::updt_params(params_ref const & p) {
m_params.copy(p);
m_enforce_model_conversion = m_params.get_bool("solver.enforce_model_conversion", false);
solver_params sp(m_params);
m_enforce_model_conversion = sp.enforce_model_conversion();
m_cancel_backup_file = sp.cancel_backup_file();
}
@ -309,3 +319,28 @@ expr_ref_vector solver::get_non_units(ast_manager& m) {
}
return result;
}
lbool solver::check_sat(unsigned num_assumptions, expr * const * assumptions) {
lbool r = l_undef;
try {
r = check_sat_core(num_assumptions, assumptions);
}
catch (...) {
if (get_manager().canceled()) {
dump_state(num_assumptions, assumptions);
}
throw;
}
if (r == l_undef && get_manager().canceled()) {
dump_state(num_assumptions, assumptions);
}
return r;
}
void solver::dump_state(unsigned sz, expr* const* assumptions) {
std::string file = m_cancel_backup_file.str();
if (file != "") {
std::ofstream ous(file);
display(ous, sz, assumptions);
}
}

16
src/solver/solver.h
View file

@ -44,8 +44,9 @@ public:
- results based on check_sat_result API
*/
class solver : public check_sat_result {
params_ref m_params;
bool m_enforce_model_conversion;
params_ref m_params;
bool m_enforce_model_conversion;
symbol m_cancel_backup_file;
public:
solver(): m_enforce_model_conversion(false) {}
~solver() override {}
@ -140,7 +141,8 @@ public:
If it is unsatisfiable, and unsat-core generation is enabled. Then, the unsat-core is a subset of these assumptions.
*/
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0;
lbool check_sat(unsigned num_assumptions, expr * const * assumptions);
lbool check_sat(expr_ref_vector const& asms) { return check_sat(asms.size(), asms.c_ptr()); }
@ -227,6 +229,11 @@ public:
*/
virtual std::ostream& display(std::ostream & out, unsigned n = 0, expr* const* assumptions = nullptr) const;
/**
\brief Display the content of this solver in DIMACS format
*/
std::ostream& display_dimacs(std::ostream & out) const;
/**
\brief expose model converter when solver produces partially reduced set of assertions.
*/
@ -249,14 +256,17 @@ public:
void disable_pop() { m_nopop = true; }
};
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) = 0;
protected:
virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences);
void dump_state(unsigned sz, expr* const* assumptions);
bool is_literal(ast_manager& m, expr* e);
};
typedef ref<solver> solver_ref;

4
src/solver/solver_na2as.cpp
View file

@ -61,10 +61,10 @@ struct append_assumptions {
}
};
lbool solver_na2as::check_sat(unsigned num_assumptions, expr * const * assumptions) {
lbool solver_na2as::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
append_assumptions app(m_assumptions, num_assumptions, assumptions);
TRACE("solver_na2as", display(tout););
return check_sat_core(m_assumptions.size(), m_assumptions.c_ptr());
return check_sat_core2(m_assumptions.size(), m_assumptions.c_ptr());
}
lbool solver_na2as::check_sat_cc(const expr_ref_vector &assumptions, vector<expr_ref_vector> const &clauses) {

5
src/solver/solver_na2as.h
View file

@ -35,10 +35,9 @@ public:
~solver_na2as() override;
void assert_expr_core2(expr * t, expr * a) override;
// virtual void assert_expr_core(expr * t) = 0;
// Subclasses of solver_na2as should redefine the following *_core methods instead of these ones.
lbool check_sat(unsigned num_assumptions, expr * const * assumptions) override;
lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override;
lbool check_sat_cc(const expr_ref_vector &assumptions, vector<expr_ref_vector> const &clauses) override;
void push() override;
void pop(unsigned n) override;
@ -49,7 +48,7 @@ public:
lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) override;
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) override;
protected:
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) = 0;
virtual lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) = 0;
virtual lbool check_sat_cc_core(const expr_ref_vector &assumptions, vector<expr_ref_vector> const &clauses) { NOT_IMPLEMENTED_YET(); }
virtual void push_core() = 0;
virtual void pop_core(unsigned n) = 0;

8
src/solver/solver_params.pyg Normal file
View file

@ -0,0 +1,8 @@
def_module_params('solver',
description='solver parameters',
export=True,
params=(('enforce_model_conversion', BOOL, False, "apply model transformation on new assertions"),
('cancel_backup_file', SYMBOL, '', "file to save partial search state if search is canceled"),
))

2
src/solver/solver_pool.cpp
View file

@ -119,7 +119,7 @@ public:
}
}
lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override {
lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override {
SASSERT(!m_pushed || get_scope_level() > 0);
m_proof.reset();
scoped_watch _t_(m_pool.m_check_watch);

4
src/solver/tactic2solver.cpp
View file

@ -62,7 +62,7 @@ public:
void push_core() override;
void pop_core(unsigned n) override;
lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override;
lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override;
void collect_statistics(statistics & st) const override;
void get_unsat_core(expr_ref_vector & r) override;
@ -136,7 +136,7 @@ void tactic2solver::pop_core(unsigned n) {
m_result = nullptr;
}
lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * assumptions) {
if (m_tactic.get() == nullptr)
return l_false;
ast_manager & m = m_assertions.m();

2
src/tactic/CMakeLists.txt
View file

@ -22,4 +22,6 @@ z3_add_component(tactic
probe.h
sine_filter.h
tactic.h
PYG_FILES
tactic_params.pyg
)

13
src/tactic/core/blast_term_ite_tactic.cpp
View file

@ -16,11 +16,12 @@ Author:
Notes:
--*/
#include "tactic/tactical.h"
#include "util/cooperate.h"
#include "ast/normal_forms/defined_names.h"
#include "ast/rewriter/rewriter_def.h"
#include "util/cooperate.h"
#include "ast/scoped_proof.h"
#include "tactic/tactical.h"
#include "tactic/tactic_params.hpp"
@ -50,9 +51,10 @@ class blast_term_ite_tactic : public tactic {
}
void updt_params(params_ref const & p) {
tactic_params tp(p);
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_max_steps = p.get_uint("max_steps", UINT_MAX);
m_max_inflation = p.get_uint("max_inflation", UINT_MAX); // multiplicative factor of initial term size.
m_max_steps = p.get_uint("max_steps", tp.blast_term_ite_max_steps());
m_max_inflation = p.get_uint("max_inflation", tp.blast_term_ite_max_inflation()); // multiplicative factor of initial term size.
}
@ -182,8 +184,7 @@ public:
void collect_param_descrs(param_descrs & r) override {
insert_max_memory(r);
insert_max_steps(r);
r.insert("max_args", CPK_UINT,
"(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic.");
r.insert("max_inflation", CPK_UINT, "(default: infinity) multiplicative factor of initial term size.");
}
void operator()(goal_ref const & in, goal_ref_buffer & result) override {

6
src/tactic/core/propagate_values_tactic.cpp
View file

@ -23,6 +23,7 @@ Revision History:
#include "ast/ast_smt2_pp.h"
#include "ast/expr_substitution.h"
#include "tactic/goal_shared_occs.h"
#include "tactic/tactic_params.hpp"
namespace {
class propagate_values_tactic : public tactic {
@ -37,7 +38,8 @@ class propagate_values_tactic : public tactic {
params_ref m_params;
void updt_params_core(params_ref const & p) {
m_max_rounds = p.get_uint("max_rounds", 4);
tactic_params tp(p);
m_max_rounds = p.get_uint("max_rounds", tp.propagate_values_max_rounds());
}
bool is_shared(expr * t) {
@ -215,7 +217,7 @@ public:
void collect_param_descrs(param_descrs & r) override {
th_rewriter::get_param_descrs(r);
r.insert("max_rounds", CPK_UINT, "(default: 2) maximum number of rounds.");
r.insert("max_rounds", CPK_UINT, "(default: 4) maximum number of rounds.");
}
void operator()(goal_ref const & in, goal_ref_buffer & result) override {

29
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -25,6 +25,7 @@ Revision History:
#include "tactic/goal_shared_occs.h"
#include "tactic/tactical.h"
#include "tactic/generic_model_converter.h"
#include "tactic/tactic_params.hpp"
class solve_eqs_tactic : public tactic {
struct imp {
@ -40,6 +41,7 @@ class solve_eqs_tactic : public tactic {
bool m_theory_solver;
bool m_ite_solver;
unsigned m_max_occs;
bool m_context_solve;
scoped_ptr<expr_substitution> m_subst;
scoped_ptr<expr_substitution> m_norm_subst;
expr_sparse_mark m_candidate_vars;
@ -72,9 +74,11 @@ class solve_eqs_tactic : public tactic {
ast_manager & m() const { return m_manager; }
void updt_params(params_ref const & p) {
m_ite_solver = p.get_bool("ite_solver", true);
m_theory_solver = p.get_bool("theory_solver", true);
m_max_occs = p.get_uint("solve_eqs_max_occs", UINT_MAX);
tactic_params tp(p);
m_ite_solver = p.get_bool("ite_solver", tp.solve_eqs_ite_solver());
m_theory_solver = p.get_bool("theory_solver", tp.solve_eqs_theory_solver());
m_max_occs = p.get_uint("solve_eqs_max_occs", tp.solve_eqs_max_occs());
m_context_solve = p.get_bool("context_solve", tp.solve_eqs_context_solve());
}
void checkpoint() {
@ -555,7 +559,7 @@ class solve_eqs_tactic : public tactic {
insert_solution(g, idx, arg, var, def, pr);
}
else {
IF_VERBOSE(0,
IF_VERBOSE(10000,
verbose_stream() << "eq not solved " << mk_pp(arg, m()) << "\n";
verbose_stream() << is_uninterp_const(lhs) << " " << !m_candidate_vars.is_marked(lhs) << " "
<< !occurs(lhs, rhs) << " " << check_occs(lhs) << "\n";);
@ -726,7 +730,7 @@ class solve_eqs_tactic : public tactic {
++idx;
}
IF_VERBOSE(10,
IF_VERBOSE(10000,
verbose_stream() << "ordered vars: ";
for (app* v : m_ordered_vars) verbose_stream() << mk_pp(v, m()) << " ";
verbose_stream() << "\n";);
@ -811,12 +815,6 @@ class solve_eqs_tactic : public tactic {
}
m_r->operator()(f, new_f, new_pr, new_dep);
#if 0
pb_util pb(m());
if (pb.is_ge(f) && f != new_f) {
IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(f, m()) << "\n--->\n" << mk_ismt2_pp(new_f, m()) << "\n");
}
#endif
TRACE("solve_eqs_subst", tout << mk_ismt2_pp(f, m()) << "\n--->\n" << mk_ismt2_pp(new_f, m()) << "\n";);
m_num_steps += m_r->get_num_steps() + 1;
@ -922,8 +920,9 @@ class solve_eqs_tactic : public tactic {
while (true) {
collect_num_occs(*g);
collect(*g);
// TBD Disabled until tested more:
// collect_hoist(*g);
if (m_context_solve) {
collect_hoist(*g);
}
if (m_subst->empty())
break;
sort_vars();
@ -941,7 +940,6 @@ class solve_eqs_tactic : public tactic {
g->inc_depth();
g->add(mc.get());
result.push_back(g.get());
//IF_VERBOSE(0, g->display(verbose_stream()));
TRACE("solve_eqs", g->display(tout););
SASSERT(g->is_well_sorted());
}
@ -968,10 +966,11 @@ public:
m_imp->updt_params(p);
}
void collect_param_descrs(param_descrs & r) override {
void collect_param_descrs(param_descrs & r) override {
r.insert("solve_eqs_max_occs", CPK_UINT, "(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations.");
r.insert("theory_solver", CPK_BOOL, "(default: true) use theory solvers.");
r.insert("ite_solver", CPK_BOOL, "(default: true) use if-then-else solver.");
r.insert("context_solve", CPK_BOOL, "(default: false) solve equalities under disjunctions.");
}
void operator()(goal_ref const & in,

4
src/tactic/fd_solver/bounded_int2bv_solver.cpp
View file

@ -137,9 +137,9 @@ public:
}
}
lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override {
lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override {
flush_assertions();
return m_solver->check_sat(num_assumptions, assumptions);
return m_solver->check_sat_core(num_assumptions, assumptions);
}
void updt_params(params_ref const & p) override { solver::updt_params(p); m_solver->updt_params(p); }

4
src/tactic/fd_solver/enum2bv_solver.cpp
View file

@ -78,9 +78,9 @@ public:
m_rewriter.pop(n);
}
lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override {
lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override {
m_solver->updt_params(get_params());
return m_solver->check_sat(num_assumptions, assumptions);
return m_solver->check_sat_core(num_assumptions, assumptions);
}
void updt_params(params_ref const & p) override { solver::updt_params(p); m_solver->updt_params(p); }

4
src/tactic/fd_solver/pb2bv_solver.cpp
View file

@ -75,9 +75,9 @@ public:
m_rewriter.pop(n);
}
lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override {
lbool check_sat_core2(unsigned num_assumptions, expr * const * assumptions) override {
flush_assertions();
return m_solver->check_sat(num_assumptions, assumptions);
return m_solver->check_sat_core(num_assumptions, assumptions);
}
void updt_params(params_ref const & p) override { solver::updt_params(p); m_rewriter.updt_params(p); m_solver->updt_params(p); }

65
src/tactic/goal.cpp
View file

@ -20,6 +20,7 @@ Revision History:
#include "ast/ast_smt2_pp.h"
#include "ast/for_each_expr.h"
#include "ast/well_sorted.h"
#include "ast/display_dimacs.h"
#include "tactic/goal.h"
goal::precision goal::mk_union(precision p1, precision p2) {
@ -262,14 +263,14 @@ void goal::assert_expr(expr * f, expr_dependency * d) {
assert_expr(f, proofs_enabled() ? m().mk_asserted(f) : nullptr, d);
}
void goal::get_formulas(ptr_vector<expr> & result) {
void goal::get_formulas(ptr_vector<expr> & result) const {
unsigned sz = size();
for (unsigned i = 0; i < sz; i++) {
result.push_back(form(i));
}
}
void goal::get_formulas(expr_ref_vector & result) {
void goal::get_formulas(expr_ref_vector & result) const {
unsigned sz = size();
for (unsigned i = 0; i < sz; i++) {
result.push_back(form(i));
@ -434,63 +435,9 @@ void goal::display_ll(std::ostream & out) const {
\brief Assumes that the formula is already in CNF.
*/
void goal::display_dimacs(std::ostream & out) const {
unsigned_vector expr2var;
ptr_vector<expr> exprs;
unsigned num_vars = 0;
unsigned num_cls = size();
for (unsigned i = 0; i < num_cls; i++) {
expr * f = form(i);
unsigned num_lits;
expr * const * lits;
if (m().is_or(f)) {
num_lits = to_app(f)->get_num_args();
lits = to_app(f)->get_args();
}
else {
num_lits = 1;
lits = &f;
}
for (unsigned j = 0; j < num_lits; j++) {
expr * l = lits[j];
if (m().is_not(l))
l = to_app(l)->get_arg(0);
if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) {
num_vars++;
expr2var.setx(l->get_id(), num_vars, UINT_MAX);
exprs.setx(l->get_id(), l, nullptr);
}
}
}
out << "p cnf " << num_vars << " " << num_cls << "\n";
for (unsigned i = 0; i < num_cls; i++) {
expr * f = form(i);
unsigned num_lits;
expr * const * lits;
if (m().is_or(f)) {
num_lits = to_app(f)->get_num_args();
lits = to_app(f)->get_args();
}
else {
num_lits = 1;
lits = &f;
}
for (unsigned j = 0; j < num_lits; j++) {
expr * l = lits[j];
if (m().is_not(l)) {
out << "-";
l = to_app(l)->get_arg(0);
}
SASSERT(exprs[l->get_id()]);
out << expr2var[l->get_id()] << " ";
}
out << "0\n";
}
for (expr* e : exprs) {
if (e && is_app(e)) {
symbol const& n = to_app(e)->get_decl()->get_name();
out << "c " << expr2var[e->get_id()] << " " << n << "\n";
}
}
expr_ref_vector fmls(m());
get_formulas(fmls);
::display_dimacs(out, fmls);
}
unsigned goal::num_exprs() const {

4
src/tactic/goal.h
View file

@ -126,8 +126,8 @@ public:
void update(unsigned i, expr * f, proof * pr = nullptr, expr_dependency * dep = nullptr);
void get_formulas(ptr_vector<expr> & result);
void get_formulas(expr_ref_vector & result);
void get_formulas(ptr_vector<expr> & result) const;
void get_formulas(expr_ref_vector & result) const;
void elim_true();
void elim_redundancies();

20
src/tactic/tactic_params.pyg Normal file
View file

@ -0,0 +1,20 @@
def_module_params('tactic',
description='tactic parameters',
export=True,
params=(('solve_eqs.context_solve', BOOL, False, "solve equalities within disjunctions."),
('solve_eqs.theory_solver', BOOL, True, "use theory solvers."),
('solve_eqs.ite_solver', BOOL, True, "use if-then-else solvers."),
('solve_eqs.max_occs', UINT, UINT_MAX, "maximum number of occurrences for considering a variable for gaussian eliminations."),
('blast_term_ite.max_inflation', UINT, UINT_MAX, "multiplicative factor of initial term size."),
('blast_term_ite.max_steps', UINT, UINT_MAX, "maximal number of steps allowed for tactic."),
('propagate_values.max_rounds', UINT, 4, "maximal number of rounds to propagate values."),
# ('aig.per_assertion', BOOL, True, "process one assertion at a time"),
# ('add_bounds.lower, INT, -2, "lower bound to be added to unbounded variables."),
# ('add_bounds.upper, INT, 2, "upper bound to be added to unbounded variables."),
# ('fm.real_only', BOOL, True, "consider only real variables for FM"),
# ('fm.occ', BOOL, False, "consider inequalities occurring in clauses for FM."),
# ('fm.limit', UINT, 5000000, "maximal number of constraints, monomials, clauses visited during FM."),
# etc: lia2card, factor, nla2bv, normalize_bounds, pb2bv, purify_arith, bit_blaster, bv_bounds
))

1
src/util/chashtable.h
View file

@ -32,6 +32,7 @@ Revision History:
#include "util/debug.h"
#include "util/trace.h"
#include "util/tptr.h"
#include "util/util.h"
#ifdef Z3DEBUG
#include "util/hashtable.h"
#endif