mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-03-08 14:32:30 +00:00
commit cfda8e9e03
25 changed files with 313 additions and 228 deletions
Download patch file Download diff file Expand all files Collapse all files

59
scripts/update_api.py
View file

@ -1612,14 +1612,27 @@ def generate_files(api_files,
java_package_name=None,
ml_output_dir=None):
"""
Scan the api files in ``api_files`` and emit
the relevant ``api_*.h`` and ``api_*.cpp`` files
for the api modules into the ``api_output_dir``
directory.
Scan the api files in ``api_files`` and emit the relevant API files into
the output directories specified. If an output directory is set to ``None``
then the files for that language binding or module are not emitted.
For the remaining arguments, if said argument is
not ``None`` the relevant files for that language
binding will be emitted to the specified directory.
The reason for this function interface is:
* The CMake build system needs to control where
files are emitted.
* The CMake build system needs to be able to choose
which API files are emitted.
* This function should be as decoupled from the Python
build system as much as possible but it must be possible
for the Python build system code to use this function.
Therefore we:
* Do not use the ``mk_util.is_*_enabled()`` functions
to determine if certain files should be or should not be emitted.
* Do not use the components declared in the Python build system
to determine the output directory paths.
"""
# FIXME: These should not be global
global log_h, log_c, exe_c, core_py
@ -1677,16 +1690,32 @@ def generate_files(api_files,
def main(args):
logging.basicConfig(level=logging.INFO)
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument("api_files", nargs="+",
parser.add_argument("api_files",
nargs="+",
help="API header files to generate files from")
parser.add_argument("--api_output_dir",
help="Directory to emit files for api module",
default=None)
parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None)
parser.add_argument("--dotnet-output-dir", dest="dotnet_output_dir", default=None)
parser.add_argument("--java-output-dir", dest="java_output_dir", default=None)
parser.add_argument("--java-package-name", dest="java_package_name", default=None)
parser.add_argument("--ml-output-dir", dest="ml_output_dir", default=None)
default=None,
help="Directory to emit files for api module. If not specified no files are emitted.")
parser.add_argument("--z3py-output-dir",
dest="z3py_output_dir",
default=None,
help="Directory to emit z3py files. If not specified no files are emitted.")
parser.add_argument("--dotnet-output-dir",
dest="dotnet_output_dir",
default=None,
help="Directory to emit dotnet files. If not specified no files are emitted.")
parser.add_argument("--java-output-dir",
dest="java_output_dir",
default=None,
help="Directory to emit Java files. If not specified no files are emitted.")
parser.add_argument("--java-package-name",
dest="java_package_name",
default=None,
help="Name to give the Java package (e.g. ``com.microsoft.z3``).")
parser.add_argument("--ml-output-dir",
dest="ml_output_dir",
default=None,
help="Directory to emit OCaml files. If not specified no files are emitted.")
pargs = parser.parse_args(args)
if pargs.java_output_dir:

1
src/cmd_context/cmd_context.cpp
View file

@ -1454,6 +1454,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
throw ex;
}
catch (z3_exception & ex) {
get_opt()->display_assignment(regular_stream());
throw cmd_exception(ex.msg());
}
if (was_pareto && r == l_false) {

3
src/muz/pdr/pdr_sym_mux.h
View file

@ -23,6 +23,7 @@ Revision History:
#include "ast.h"
#include "map.h"
#include "vector.h"
#include <vector>
class model_core;
@ -46,7 +47,7 @@ private:
mutable unsigned m_next_sym_suffix_idx;
mutable symbols m_used_suffixes;
/** Here we have default suffixes for each of the variants */
vector<std::string> m_suffixes;
std::vector<std::string> m_suffixes;
/**

3
src/opt/bcd2.cpp
View file

@ -233,8 +233,7 @@ namespace opt {
new_assignment.reset();
s().get_model(model);
for (unsigned i = 0; i < m_soft.size(); ++i) {
VERIFY(model->eval(m_soft[i], val));
new_assignment.push_back(m.is_true(val));
new_assignment.push_back(model->eval(m_soft[i], val) && m.is_true(val));
if (!new_assignment[i]) {
new_upper += m_weights[i];
}

2
src/opt/fu_malik.cpp
View file

@ -204,7 +204,7 @@ namespace opt {
m_assignment.reset();
for (unsigned i = 0; i < m_soft.size(); ++i) {
expr_ref val(m);
VERIFY(m_model->eval(m_soft[i], val));
if (!m_model->eval(m_soft[i], val)) return l_undef;
TRACE("opt", tout << val << "\n";);
m_assignment.push_back(m.is_true(val));
}

3
src/opt/maxhs.cpp
View file

@ -530,8 +530,7 @@ namespace opt {
bool is_true(model_ref& mdl, expr* e) {
expr_ref val(m);
VERIFY(mdl->eval(e, val));
return m.is_true(val);
return mdl->eval(e, val) && m.is_true(val);
}
bool is_active(unsigned i) const {

38
src/opt/maxres.cpp
View file

@ -82,6 +82,7 @@ private:
memset(this, 0, sizeof(*this));
}
};
unsigned m_index;
stats m_stats;
expr_ref_vector m_B;
expr_ref_vector m_asms;
@ -112,10 +113,11 @@ private:
typedef ptr_vector<expr> exprs;
public:
maxres(maxsat_context& c,
maxres(maxsat_context& c, unsigned index,
weights_t& ws, expr_ref_vector const& soft,
strategy_t st):
maxsmt_solver_base(c, ws, soft),
m_index(index),
m_B(m), m_asms(m), m_defs(m),
m_mus(c.get_solver(), m),
m_mss(c.get_solver(), m),
@ -189,7 +191,7 @@ public:
lbool mus_solver() {
lbool is_sat = l_true;
init();
if (!init()) return l_undef;
init_local();
trace();
while (m_lower < m_upper) {
@ -227,7 +229,7 @@ public:
}
lbool primal_dual_solver() {
init();
if (!init()) return l_undef;
init_local();
trace();
exprs cs;
@ -483,8 +485,9 @@ public:
if (m_csmodel) {
expr_ref val(m);
SASSERT(m_csmodel.get());
VERIFY(m_csmodel->eval(value, val));
m_csmodel->register_decl(to_app(def)->get_decl(), val);
if (m_csmodel->eval(value, val, true)) {
m_csmodel->register_decl(to_app(def)->get_decl(), val);
}
}
}
@ -724,17 +727,26 @@ public:
if (upper >= m_upper) {
return;
}
if (!m_c.verify_model(m_index, mdl, upper)) {
return;
}
m_model = mdl;
for (unsigned i = 0; i < m_soft.size(); ++i) {
m_assignment[i] = is_true(m_soft[i]);
}
DEBUG_CODE(verify_assignment(););
m_upper = upper;
trace();
add_upper_bound_block();
}
void add_upper_bound_block() {
@ -751,14 +763,12 @@ public:
bool is_true(model* mdl, expr* e) {
expr_ref tmp(m);
VERIFY(mdl->eval(e, tmp));
return m.is_true(tmp);
return mdl->eval(e, tmp, true) && m.is_true(tmp);
}
bool is_false(model* mdl, expr* e) {
expr_ref tmp(m);
VERIFY(mdl->eval(e, tmp));
return m.is_false(tmp);
return mdl->eval(e, tmp, true) && m.is_false(tmp);
}
bool is_true(expr* e) {
@ -870,12 +880,12 @@ public:
};
opt::maxsmt_solver_base* opt::mk_maxres(
maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) {
return alloc(maxres, c, ws, soft, maxres::s_primal);
maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) {
return alloc(maxres, c, id, ws, soft, maxres::s_primal);
}
opt::maxsmt_solver_base* opt::mk_primal_dual_maxres(
maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) {
return alloc(maxres, c, ws, soft, maxres::s_primal_dual);
maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) {
return alloc(maxres, c, id, ws, soft, maxres::s_primal_dual);
}

4
src/opt/maxres.h
View file

@ -22,9 +22,9 @@ Notes:
namespace opt {
maxsmt_solver_base* mk_maxres(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft);
maxsmt_solver_base* mk_maxres(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft);
maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft);
maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft);
};

34
src/opt/maxsmt.cpp
View file

@ -69,13 +69,13 @@ namespace opt {
s().assert_expr(tmp);
}
void maxsmt_solver_base::init() {
bool maxsmt_solver_base::init() {
m_lower.reset();
m_upper.reset();
m_assignment.reset();
for (unsigned i = 0; i < m_weights.size(); ++i) {
expr_ref val(m);
VERIFY(m_model->eval(m_soft[i], val));
if (!m_model->eval(m_soft[i], val)) return false;
m_assignment.push_back(m.is_true(val));
if (!m_assignment.back()) {
m_upper += m_weights[i];
@ -88,6 +88,7 @@ namespace opt {
tout << (m_assignment[i]?"T":"F");
}
tout << "\n";);
return true;
}
void maxsmt_solver_base::set_mus(bool f) {
@ -137,7 +138,8 @@ namespace opt {
//m_wth->reset_local();
}
smt::theory_wmaxsat& maxsmt_solver_base::scoped_ensure_theory::operator()() { return *m_wth; }
void maxsmt_solver_base::trace_bounds(char const * solver) {
IF_VERBOSE(1,
rational l = m_adjust_value(m_lower);
@ -148,8 +150,8 @@ namespace opt {
maxsmt::maxsmt(maxsat_context& c):
m(c.get_manager()), m_c(c),
maxsmt::maxsmt(maxsat_context& c, unsigned index):
m(c.get_manager()), m_c(c), m_index(index),
m_soft_constraints(m), m_answer(m) {}
lbool maxsmt::operator()() {
@ -159,10 +161,10 @@ namespace opt {
IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
TRACE("opt", tout << "maxsmt\n";);
if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres")) {
m_msolver = mk_maxres(m_c, m_weights, m_soft_constraints);
m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
}
else if (maxsat_engine == symbol("pd-maxres")) {
m_msolver = mk_primal_dual_maxres(m_c, m_weights, m_soft_constraints);
m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints);
}
else if (maxsat_engine == symbol("bcd2")) {
m_msolver = mk_bcd2(m_c, m_weights, m_soft_constraints);
@ -188,7 +190,13 @@ namespace opt {
if (m_msolver) {
m_msolver->updt_params(m_params);
m_msolver->set_adjust_value(m_adjust_value);
is_sat = (*m_msolver)();
is_sat = l_undef;
try {
is_sat = (*m_msolver)();
}
catch (z3_exception&) {
is_sat = l_undef;
}
if (is_sat != l_false) {
m_msolver->get_model(m_model, m_labels);
}
@ -205,6 +213,14 @@ namespace opt {
return is_sat;
}
void maxsmt::set_adjust_value(adjust_value& adj) {
m_adjust_value = adj;
if (m_msolver) {
m_msolver->set_adjust_value(m_adjust_value);
}
}
void maxsmt::verify_assignment() {
// TBD: have to use a different solver
// because we don't push local scope any longer.
@ -233,7 +249,7 @@ namespace opt {
rational r = m_upper;
if (m_msolver) {
rational q = m_msolver->get_upper();
if (q < r) r = q;
if (q < r) r = q;
}
return m_adjust_value(r);
}

7
src/opt/maxsmt.h
View file

@ -82,7 +82,7 @@ namespace opt {
void set_model() { s().get_model(m_model); s().get_labels(m_labels); }
virtual void updt_params(params_ref& p);
solver& s();
void init();
bool init();
void set_mus(bool f);
app* mk_fresh_bool(char const* name);
@ -111,6 +111,7 @@ namespace opt {
class maxsmt {
ast_manager& m;
maxsat_context& m_c;
unsigned m_index;
scoped_ptr<maxsmt_solver_base> m_msolver;
expr_ref_vector m_soft_constraints;
expr_ref_vector m_answer;
@ -122,11 +123,11 @@ namespace opt {
svector<symbol> m_labels;
params_ref m_params;
public:
maxsmt(maxsat_context& c);
maxsmt(maxsat_context& c, unsigned id);
lbool operator()();
void updt_params(params_ref& p);
void add(expr* f, rational const& w);
void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; }
void set_adjust_value(adjust_value& adj);
unsigned size() const { return m_soft_constraints.size(); }
expr* operator[](unsigned idx) const { return m_soft_constraints[idx]; }
rational weight(unsigned idx) const { return m_weights[idx]; }

11
src/opt/mss.cpp
View file

@ -73,8 +73,7 @@ namespace opt {
expr* n = core[j];
if (!core_lits.contains(n)) {
core_lits.insert(n);
VERIFY(m_model->eval(n, tmp));
if (m.is_true(tmp)) {
if (m_model->eval(n, tmp) && m.is_true(tmp)) {
add_mss(n);
}
else {
@ -86,8 +85,7 @@ namespace opt {
for (unsigned i = 0; i < literals.size(); ++i) {
expr* n = literals[i];
if (!core_lits.contains(n)) {
VERIFY(m_model->eval(n, tmp));
if (m.is_true(tmp)) {
if (m_model->eval(n, tmp) && m.is_true(tmp)) {
m_mss.push_back(n);
}
else {
@ -130,8 +128,7 @@ namespace opt {
if (m_mcs.contains(n)) {
continue; // remove from cores.
}
VERIFY(m_model->eval(n, tmp));
if (m.is_true(tmp)) {
if (m_model->eval(n, tmp) && m.is_true(tmp)) {
add_mss(n);
}
else {
@ -275,7 +272,7 @@ namespace opt {
expr_ref tmp(m);
for (unsigned i = 0; i < m_mss.size(); ++i) {
expr* n = m_mss[i];
VERIFY(m_model->eval(n, tmp));
if (!m_model->eval(n, tmp)) return true;
CTRACE("opt", !m.is_true(tmp), tout << mk_pp(n, m) << " |-> " << mk_pp(tmp, m) << "\n";);
SASSERT(!m.is_false(tmp));
}

80
src/opt/opt_context.cpp
View file

@ -203,7 +203,7 @@ namespace opt {
objective& obj = s.m_objectives[i];
m_objectives.push_back(obj);
if (obj.m_type == O_MAXSMT) {
add_maxsmt(obj.m_id);
add_maxsmt(obj.m_id, i);
}
}
m_hard_constraints.append(s.m_hard);
@ -311,7 +311,9 @@ namespace opt {
maxsmt& ms = *m_maxsmts.find(id);
if (scoped) get_solver().push();
lbool result = ms();
if (result != l_false && (ms.get_model(tmp, m_labels), tmp.get())) ms.get_model(m_model, m_labels);
if (result != l_false && (ms.get_model(tmp, m_labels), tmp.get())) {
ms.get_model(m_model, m_labels);
}
if (scoped) get_solver().pop(1);
if (result == l_true && committed) ms.commit_assignment();
return result;
@ -414,12 +416,16 @@ namespace opt {
case O_MINIMIZE:
is_ge = !is_ge;
case O_MAXIMIZE:
VERIFY(mdl->eval(obj.m_term, val) && is_numeral(val, k));
if (is_ge) {
result = mk_ge(obj.m_term, val);
if (mdl->eval(obj.m_term, val) && is_numeral(val, k)) {
if (is_ge) {
result = mk_ge(obj.m_term, val);
}
else {
result = mk_ge(val, obj.m_term);
}
}
else {
result = mk_ge(val, obj.m_term);
result = m.mk_true();
}
break;
case O_MAXSMT: {
@ -430,8 +436,7 @@ namespace opt {
for (unsigned i = 0; i < sz; ++i) {
terms.push_back(obj.m_terms[i]);
coeffs.push_back(obj.m_weights[i]);
VERIFY(mdl->eval(obj.m_terms[i], val));
if (m.is_true(val)) {
if (mdl->eval(obj.m_terms[i], val) && m.is_true(val)) {
k += obj.m_weights[i];
}
}
@ -469,8 +474,7 @@ namespace opt {
update_bound(false);
}
lbool context::execute_pareto() {
lbool context::execute_pareto() {
if (!m_pareto) {
set_pareto(alloc(gia_pareto, m, *this, m_solver.get(), m_params));
}
@ -642,8 +646,8 @@ namespace opt {
}
void context::add_maxsmt(symbol const& id) {
maxsmt* ms = alloc(maxsmt, *this);
void context::add_maxsmt(symbol const& id, unsigned index) {
maxsmt* ms = alloc(maxsmt, *this, index);
ms->updt_params(m_params);
#pragma omp critical (opt_context)
{
@ -708,7 +712,7 @@ namespace opt {
}
}
bool context::is_maximize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index) {
bool context::is_maximize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index) {
if (is_app(fml) && m_objective_fns.find(to_app(fml)->get_decl(), index) &&
m_objectives[index].m_type == O_MAXIMIZE) {
term = to_app(to_app(fml)->get_arg(0));
@ -718,7 +722,7 @@ namespace opt {
return false;
}
bool context::is_minimize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index) {
bool context::is_minimize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index) {
if (is_app(fml) && m_objective_fns.find(to_app(fml)->get_decl(), index) &&
m_objectives[index].m_type == O_MINIMIZE) {
term = to_app(to_app(fml)->get_arg(0));
@ -730,7 +734,7 @@ namespace opt {
bool context::is_maxsat(expr* fml, expr_ref_vector& terms,
vector<rational>& weights, rational& offset,
bool& neg, symbol& id, unsigned& index) {
bool& neg, symbol& id, expr_ref& orig_term, unsigned& index) {
if (!is_app(fml)) return false;
neg = false;
app* a = to_app(fml);
@ -752,7 +756,6 @@ namespace opt {
return true;
}
app_ref term(m);
expr* orig_term;
offset = rational::zero();
bool is_max = is_maximize(fml, term, orig_term, index);
bool is_min = !is_max && is_minimize(fml, term, orig_term, index);
@ -773,7 +776,7 @@ namespace opt {
}
}
TRACE("opt",
tout << "Convert minimization " << mk_pp(orig_term, m) << "\n";
tout << "Convert minimization " << orig_term << "\n";
tout << "to maxsat: " << term << "\n";
for (unsigned i = 0; i < weights.size(); ++i) {
tout << mk_pp(terms[i].get(), m) << ": " << weights[i] << "\n";
@ -781,7 +784,7 @@ namespace opt {
tout << "offset: " << offset << "\n";
);
std::ostringstream out;
out << mk_pp(orig_term, m) << ":" << index;
out << orig_term << ":" << index;
id = symbol(out.str().c_str());
return true;
}
@ -804,7 +807,7 @@ namespace opt {
}
neg = true;
std::ostringstream out;
out << mk_pp(orig_term, m) << ":" << index;
out << orig_term << ":" << index;
id = symbol(out.str().c_str());
return true;
}
@ -823,7 +826,7 @@ namespace opt {
}
neg = is_max;
std::ostringstream out;
out << mk_pp(orig_term, m) << ":" << index;
out << orig_term << ":" << index;
id = symbol(out.str().c_str());
return true;
}
@ -871,7 +874,7 @@ namespace opt {
tout << mk_pp(fmls[i], m) << "\n";
});
m_hard_constraints.reset();
expr* orig_term;
expr_ref orig_term(m);
for (unsigned i = 0; i < fmls.size(); ++i) {
expr* fml = fmls[i];
app_ref tr(m);
@ -881,7 +884,7 @@ namespace opt {
unsigned index;
symbol id;
bool neg;
if (is_maxsat(fml, terms, weights, offset, neg, id, index)) {
if (is_maxsat(fml, terms, weights, offset, neg, id, orig_term, index)) {
objective& obj = m_objectives[index];
if (obj.m_type != O_MAXSMT) {
@ -889,10 +892,11 @@ namespace opt {
obj.m_id = id;
obj.m_type = O_MAXSMT;
SASSERT(!m_maxsmts.contains(id));
add_maxsmt(id);
add_maxsmt(id, index);
}
mk_atomic(terms);
SASSERT(obj.m_id == id);
obj.m_term = to_app(orig_term);
obj.m_terms.reset();
obj.m_terms.append(terms);
obj.m_weights.reset();
@ -933,6 +937,32 @@ namespace opt {
}
}
bool context::verify_model(unsigned index, model* md, rational const& _v) {
rational r;
app_ref term = m_objectives[index].m_term;
rational v = m_objectives[index].m_adjust_value(_v);
expr_ref val(m);
model_ref mdl = md;
fix_model(mdl);
if (!mdl->eval(term, val)) {
TRACE("opt", tout << "Term does not evaluate " << term << "\n";);
return false;
}
if (!m_arith.is_numeral(val, r)) {
TRACE("opt", tout << "model does not evaluate objective to a value\n";);
return false;
}
if (r != v) {
TRACE("opt", tout << "Out of bounds: " << term << " " << val << " != " << v << "\n";);
return false;
}
else {
TRACE("opt", tout << "validated: " << term << " = " << val << "\n";);
}
return true;
}
void context::purify(app_ref& term) {
filter_model_converter_ref fm;
if (m_arith.is_add(term)) {
@ -1395,8 +1425,8 @@ namespace opt {
case O_MAXSMT: {
rational value(0);
for (unsigned i = 0; i < obj.m_terms.size(); ++i) {
VERIFY(m_model->eval(obj.m_terms[i], val));
if (!m.is_true(val)) {
bool evaluated = m_model->eval(obj.m_terms[i], val);
if (evaluated && !m.is_true(val)) {
value += obj.m_weights[i];
}
// TBD: check that optimal was not changed.

14
src/opt/opt_context.h
View file

@ -55,6 +55,8 @@ namespace opt {
virtual void get_base_model(model_ref& _m) = 0; // retrieve model from initial satisfiability call.
virtual smt::context& smt_context() = 0; // access SMT context for SMT based MaxSMT solver (wmax requires SMT core)
virtual unsigned num_objectives() = 0;
virtual bool verify_model(unsigned id, model* mdl, rational const& v) = 0;
virtual void set_model(model_ref& _m) = 0;
};
/**
@ -132,6 +134,7 @@ namespace opt {
bool set(ptr_vector<expr> & hard);
unsigned add(expr* soft, rational const& weight, symbol const& id);
unsigned add(app* obj, bool is_max);
unsigned get_index(symbol const& id) { return m_indices[id]; }
};
ast_manager& m;
@ -178,6 +181,7 @@ namespace opt {
virtual void set_hard_constraints(ptr_vector<expr> & hard);
virtual lbool optimize();
virtual bool print_model() const;
virtual void set_model(model_ref& _m) { m_model = _m; }
virtual void get_model(model_ref& _m);
virtual void fix_model(model_ref& _m);
virtual void collect_statistics(statistics& stats) const;
@ -219,6 +223,8 @@ namespace opt {
virtual void get_base_model(model_ref& _m);
virtual bool verify_model(unsigned id, model* mdl, rational const& v);
private:
void validate_feasibility(maxsmt& ms);
@ -236,11 +242,11 @@ namespace opt {
void import_scoped_state();
void normalize();
void internalize();
bool is_maximize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index);
bool is_minimize(expr* fml, app_ref& term, expr*& orig_term, unsigned& index);
bool is_maximize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index);
bool is_minimize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index);
bool is_maxsat(expr* fml, expr_ref_vector& terms,
vector<rational>& weights, rational& offset, bool& neg,
symbol& id, unsigned& index);
symbol& id, expr_ref& orig_term, unsigned& index);
void purify(app_ref& term);
app* purify(filter_model_converter_ref& fm, expr* e);
bool is_mul_const(expr* e);
@ -269,7 +275,7 @@ namespace opt {
void init_solver();
void update_solver();
void setup_arith_solver();
void add_maxsmt(symbol const& id);
void add_maxsmt(symbol const& id, unsigned index);
void set_simplify(tactic *simplify);
void set_pareto(pareto_base* p);
void clear_state();

3
src/opt/optsmt.cpp
View file

@ -156,8 +156,7 @@ namespace opt {
m_s->get_labels(m_labels);
for (unsigned i = 0; i < ors.size(); ++i) {
expr_ref tmp(m);
m_model->eval(ors[i].get(), tmp);
if (m.is_true(tmp)) {
if (m_model->eval(ors[i].get(), tmp) && m.is_true(tmp)) {
m_lower[i] = m_upper[i];
ors[i] = m.mk_false();
disj[i] = m.mk_false();

10
src/opt/pb_sls.cpp
View file

@ -139,8 +139,7 @@ namespace smt {
m_orig_model = mdl;
for (unsigned i = 0; i < m_var2decl.size(); ++i) {
expr_ref tmp(m);
VERIFY(mdl->eval(m_var2decl[i], tmp));
m_assignment[i] = m.is_true(tmp);
m_assignment[i] = mdl->eval(m_var2decl[i], tmp) && m.is_true(tmp);
}
}
@ -305,7 +304,9 @@ namespace smt {
if (!eval(m_clauses[i])) {
m_hard_false.insert(i);
expr_ref tmp(m);
VERIFY(m_orig_model->eval(m_orig_clauses[i].get(), tmp));
if (!m_orig_model->eval(m_orig_clauses[i].get(), tmp)) {
return;
}
IF_VERBOSE(0,
verbose_stream() << "original evaluation: " << tmp << "\n";
verbose_stream() << mk_pp(m_orig_clauses[i].get(), m) << "\n";
@ -487,8 +488,7 @@ namespace smt {
SASSERT(m_soft_occ.size() == var);
m_hard_occ.push_back(unsigned_vector());
m_soft_occ.push_back(unsigned_vector());
VERIFY(m_orig_model->eval(f, tmp));
m_assignment.push_back(m.is_true(tmp));
m_assignment.push_back(m_orig_model->eval(f, tmp) && m.is_true(tmp));
m_decl2var.insert(f, var);
m_var2decl.push_back(f);
}

4
src/sat/sat_mus.cpp
View file

@ -97,7 +97,7 @@ namespace sat {
break;
}
if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
IF_VERBOSE(1, verbose_stream() << "restart budget exceeded\n";);
IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";);
set_core();
return l_true;
}
@ -173,7 +173,7 @@ namespace sat {
lbool mus::qx(literal_set& assignment, literal_set& support, bool has_support) {
lbool is_sat = l_true;
if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
IF_VERBOSE(1, verbose_stream() << "restart budget exceeded\n";);
IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";);
return l_true;
}
if (has_support) {

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

@ -50,14 +50,14 @@ class inc_sat_solver : public solver {
expr_ref_vector m_core;
atom2bool_var m_map;
model_ref m_model;
model_converter_ref m_mc;
bit_blaster_rewriter m_bb_rewriter;
scoped_ptr<bit_blaster_rewriter> m_bb_rewriter;
tactic_ref m_preprocess;
unsigned m_num_scopes;
sat::literal_vector m_asms;
goal_ref_buffer m_subgoals;
proof_converter_ref m_pc;
model_converter_ref m_mc2;
model_converter_ref m_mc;
model_converter_ref m_mc0;
expr_dependency_ref m_dep_core;
svector<double> m_weights;
std::string m_unknown;
@ -72,29 +72,13 @@ public:
m_asmsf(m),
m_fmls_head(0),
m_core(m),
m_map(m),
m_bb_rewriter(m, p),
m_map(m),
m_num_scopes(0),
m_dep_core(m),
m_unknown("no reason given") {
m_params.set_bool("elim_vars", false);
m_solver.updt_params(m_params);
params_ref simp2_p = p;
simp2_p.set_bool("som", true);
simp2_p.set_bool("pull_cheap_ite", true);
simp2_p.set_bool("push_ite_bv", false);
simp2_p.set_bool("local_ctx", true);
simp2_p.set_uint("local_ctx_limit", 10000000);
simp2_p.set_bool("flat", true); // required by som
simp2_p.set_bool("hoist_mul", false); // required by som
simp2_p.set_bool("elim_and", true);
m_preprocess =
and_then(mk_card2bv_tactic(m, m_params),
using_params(mk_simplify_tactic(m), simp2_p),
mk_max_bv_sharing_tactic(m),
mk_bit_blaster_tactic(m, &m_bb_rewriter),
//mk_aig_tactic(),
using_params(mk_simplify_tactic(m), simp2_p));
init_preprocess();
}
virtual ~inc_sat_solver() {}
@ -179,14 +163,14 @@ public:
m_fmls_lim.push_back(m_fmls.size());
m_asms_lim.push_back(m_asmsf.size());
m_fmls_head_lim.push_back(m_fmls_head);
m_bb_rewriter.push();
m_bb_rewriter->push();
m_map.push();
}
virtual void pop(unsigned n) {
if (n > m_num_scopes) { // allow inc_sat_solver to
n = m_num_scopes; // take over for another solver.
}
m_bb_rewriter.pop(n);
m_bb_rewriter->pop(n);
m_map.pop(n);
SASSERT(n <= m_num_scopes);
m_solver.user_pop(n);
@ -269,30 +253,58 @@ public:
return m_asmsf[idx];
}
void init_preprocess() {
if (m_preprocess) {
m_preprocess->reset();
}
params_ref simp2_p = m_params;
m_bb_rewriter = alloc(bit_blaster_rewriter, m, m_params);
simp2_p.set_bool("som", true);
simp2_p.set_bool("pull_cheap_ite", true);
simp2_p.set_bool("push_ite_bv", false);
simp2_p.set_bool("local_ctx", true);
simp2_p.set_uint("local_ctx_limit", 10000000);
simp2_p.set_bool("flat", true); // required by som
simp2_p.set_bool("hoist_mul", false); // required by som
simp2_p.set_bool("elim_and", true);
m_preprocess =
and_then(mk_card2bv_tactic(m, m_params),
using_params(mk_simplify_tactic(m), simp2_p),
mk_max_bv_sharing_tactic(m),
mk_bit_blaster_tactic(m, m_bb_rewriter.get()),
//mk_aig_tactic(),
using_params(mk_simplify_tactic(m), simp2_p));
for (unsigned i = 0; i < m_num_scopes; ++i) {
m_bb_rewriter->push();
}
m_preprocess->reset();
}
private:
lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm) {
m_mc2.reset();
m_mc.reset();
m_pc.reset();
m_dep_core.reset();
m_subgoals.reset();
m_preprocess->reset();
init_preprocess();
SASSERT(g->models_enabled());
SASSERT(!g->proofs_enabled());
TRACE("sat", g->display(tout););
try {
(*m_preprocess)(g, m_subgoals, m_mc2, m_pc, m_dep_core);
(*m_preprocess)(g, m_subgoals, m_mc, m_pc, m_dep_core);
}
catch (tactic_exception & ex) {
IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
m_preprocess = 0;
m_bb_rewriter = 0;
return l_undef;
}
if (m_subgoals.size() != 1) {
IF_VERBOSE(0, verbose_stream() << "size of subgoals is not 1, it is: " << m_subgoals.size() << "\n";);
return l_undef;
}
CTRACE("sat", m_mc.get(), m_mc->display(tout); );
g = m_subgoals[0];
TRACE("sat", g->display_with_dependencies(tout););
m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true);
@ -416,24 +428,25 @@ private:
}
}
m_model = md;
if (m_mc || !m_bb_rewriter.const2bits().empty()) {
model_converter_ref mc = m_mc;
if (!m_bb_rewriter.const2bits().empty()) {
mc = concat(mc.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter.const2bits()));
}
(*mc)(m_model);
if (!m_bb_rewriter->const2bits().empty()) {
m_mc0 = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits()));
}
if (m_mc0) {
(*m_mc0)(m_model);
}
SASSERT(m_model);
DEBUG_CODE(
for (unsigned i = 0; i < m_fmls.size(); ++i) {
expr_ref tmp(m);
VERIFY(m_model->eval(m_fmls[i].get(), tmp, true));
CTRACE("sat", !m.is_true(tmp),
tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m)
<< " to " << tmp << "\n";
model_smt2_pp(tout, m, *(m_model.get()), 0););
SASSERT(m.is_true(tmp));
if (m_model->eval(m_fmls[i].get(), tmp, true)) {
CTRACE("sat", !m.is_true(tmp),
tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m)
<< " to " << tmp << "\n";
model_smt2_pp(tout, m, *(m_model.get()), 0););
SASSERT(m.is_true(tmp));
}
});
}
};

11
src/smt/tactic/smt_tactic.cpp
View file

@ -99,7 +99,7 @@ public:
m_ctx(0),
m_callback(0) {
updt_params_core(p);
TRACE("smt_tactic", tout << this << "\np: " << p << "\n";);
TRACE("smt_tactic", tout << "p: " << p << "\n";);
}
virtual tactic * translate(ast_manager & m) {
@ -120,13 +120,12 @@ public:
}
virtual void updt_params(params_ref const & p) {
TRACE("smt_tactic", tout << this << "\nupdt_params: " << p << "\n";);
TRACE("smt_tactic", tout << "updt_params: " << p << "\n";);
updt_params_core(p);
fparams().updt_params(p);
symbol logic = p.get_sym(symbol("logic"), symbol::null);
if (logic != symbol::null) {
if (m_ctx) m_ctx->set_logic(logic);
m_logic = logic;
m_logic = p.get_sym(symbol("logic"), m_logic);
if (m_logic != symbol::null && m_ctx) {
m_ctx->set_logic(m_logic);
}
SASSERT(p.get_bool("auto_config", fparams().m_auto_config) == fparams().m_auto_config);
}

52
src/smt/theory_bv.cpp
View file

@ -95,10 +95,9 @@ namespace smt {
enode * first_arg_enode = ctx.get_enode(first_arg);
get_var(first_arg_enode);
// numerals are not blasted into bit2bool, so we do this directly.
if (!ctx.b_internalized(n)) {
rational val;
unsigned sz;
VERIFY(m_util.is_numeral(first_arg, val, sz));
rational val;
unsigned sz;
if (!ctx.b_internalized(n) && m_util.is_numeral(first_arg, val, sz)) {
theory_var v = first_arg_enode->get_th_var(get_id());
app* owner = first_arg_enode->get_owner();
for (unsigned i = 0; i < sz; ++i) {
@ -113,29 +112,28 @@ namespace smt {
}
}
}
else {
enode * arg = ctx.get_enode(first_arg);
// The argument was already internalized, but it may not have a theory variable associated with it.
// For example, for ite-terms the method apply_sort_cnstr is not invoked.
// See comment in the then-branch.
theory_var v_arg = arg->get_th_var(get_id());
if (v_arg == null_theory_var) {
// The method get_var will create a theory variable for arg.
// As a side-effect the bits for arg will also be created.
get_var(arg);
SASSERT(ctx.b_internalized(n));
}
else {
SASSERT(v_arg != null_theory_var);
bool_var bv = ctx.mk_bool_var(n);
ctx.set_var_theory(bv, get_id());
bit_atom * a = new (get_region()) bit_atom();
insert_bv2a(bv, a);
m_trail_stack.push(mk_atom_trail(bv));
unsigned idx = n->get_decl()->get_parameter(0).get_int();
SASSERT(a->m_occs == 0);
a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
}
enode * arg = ctx.get_enode(first_arg);
// The argument was already internalized, but it may not have a theory variable associated with it.
// For example, for ite-terms the method apply_sort_cnstr is not invoked.
// See comment in the then-branch.
theory_var v_arg = arg->get_th_var(get_id());
if (v_arg == null_theory_var) {
// The method get_var will create a theory variable for arg.
// As a side-effect the bits for arg will also be created.
get_var(arg);
SASSERT(ctx.b_internalized(n));
}
else if (!ctx.b_internalized(n)) {
SASSERT(v_arg != null_theory_var);
bool_var bv = ctx.mk_bool_var(n);
ctx.set_var_theory(bv, get_id());
bit_atom * a = new (get_region()) bit_atom();
insert_bv2a(bv, a);
m_trail_stack.push(mk_atom_trail(bv));
unsigned idx = n->get_decl()->get_parameter(0).get_int();
SASSERT(a->m_occs == 0);
a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
}
}

2
src/solver/tactic2solver.cpp
View file

@ -128,8 +128,8 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
ast_manager & m = m_assertions.m();
m_result = alloc(simple_check_sat_result, m);
m_tactic->cleanup();
m_tactic->updt_params(m_params);
m_tactic->set_logic(m_logic);
m_tactic->updt_params(m_params); // parameters are allowed to overwrite logic.
goal_ref g = alloc(goal, m, m_produce_proofs, m_produce_models, m_produce_unsat_cores);
unsigned sz = m_assertions.size();

3
src/tactic/arith/lia2pb_tactic.cpp
View file

@ -272,8 +272,9 @@ class lia2pb_tactic : public tactic {
}
TRACE("lia2pb", tout << mk_ismt2_pp(x, m) << " -> " << dep << "\n";);
subst.insert(x, def, 0, dep);
if (m_produce_models)
if (m_produce_models) {
mc1->insert(to_app(x)->get_decl(), def);
}
}
}

62
src/tactic/extension_model_converter.cpp
View file

@ -25,25 +25,6 @@ Notes:
extension_model_converter::~extension_model_converter() {
}
struct extension_model_converter::set_eval {
extension_model_converter * m_owner;
model_evaluator * m_old;
set_eval(extension_model_converter * owner, model_evaluator * ev) {
m_owner = owner;
m_old = owner->m_eval;
#pragma omp critical (extension_model_converter)
{
owner->m_eval = ev;
}
}
~set_eval() {
#pragma omp critical (extension_model_converter)
{
m_owner->m_eval = m_old;
}
}
};
static void display_decls_info(std::ostream & out, model_ref & md) {
ast_manager & m = md->get_manager();
@ -68,36 +49,38 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) {
model_evaluator ev(*(md.get()));
ev.set_model_completion(true);
expr_ref val(m());
{
set_eval setter(this, &ev);
unsigned i = m_vars.size();
while (i > 0) {
--i;
expr * def = m_defs.get(i);
ev(def, val);
TRACE("extension_mc", tout << m_vars.get(i)->get_name() << " ->\n" << mk_ismt2_pp(def, m()) << "\n==>\n" << mk_ismt2_pp(val, m()) << "\n";);
func_decl * f = m_vars.get(i);
unsigned arity = f->get_arity();
if (arity == 0) {
md->register_decl(f, val);
}
else {
func_interp * new_fi = alloc(func_interp, m(), arity);
new_fi->set_else(val);
md->register_decl(f, new_fi);
}
unsigned i = m_vars.size();
while (i > 0) {
--i;
expr * def = m_defs.get(i);
ev(def, val);
TRACE("extension_mc", tout << m_vars.get(i)->get_name() << " ->\n" << mk_ismt2_pp(def, m()) << "\n==>\n" << mk_ismt2_pp(val, m()) << "\n";);
func_decl * f = m_vars.get(i);
unsigned arity = f->get_arity();
if (arity == 0) {
md->register_decl(f, val);
}
else {
func_interp * new_fi = alloc(func_interp, m(), arity);
new_fi->set_else(val);
md->register_decl(f, new_fi);
}
}
TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md););
}
void extension_model_converter::insert(func_decl * v, expr * def) {
m_vars.push_back(v);
m_defs.push_back(def);
}
void extension_model_converter::display(std::ostream & out) {
ast_manager & m = m_vars.get_manager();
out << "(extension-model-converter";
for (unsigned i = 0; i < m_vars.size(); i++) {
out << "\n (" << m_vars.get(i)->get_name() << " ";
unsigned indent = m_vars.get(i)->get_name().size() + 4;
out << mk_ismt2_pp(m_defs.get(i), m, indent) << ")";
out << mk_ismt2_pp(m_defs.get(i), m(), indent) << ")";
}
out << ")" << std::endl;
}
@ -108,6 +91,5 @@ model_converter * extension_model_converter::translate(ast_translation & transla
res->m_vars.push_back(translator(m_vars[i].get()));
for (unsigned i = 0; i < m_defs.size(); i++)
res->m_defs.push_back(translator(m_defs[i].get()));
// m_eval is a transient object. So, it doesn't need to be translated.
return res;
}

10
src/tactic/extension_model_converter.h
View file

@ -23,15 +23,12 @@ Notes:
#include"ast.h"
#include"model_converter.h"
class model_evaluator;
class extension_model_converter : public model_converter {
func_decl_ref_vector m_vars;
expr_ref_vector m_defs;
model_evaluator * m_eval;
struct set_eval;
public:
extension_model_converter(ast_manager & m):m_vars(m), m_defs(m), m_eval(0) {
extension_model_converter(ast_manager & m):m_vars(m), m_defs(m) {
}
virtual ~extension_model_converter();
@ -43,10 +40,7 @@ public:
virtual void display(std::ostream & out);
// register a variable that was eliminated
void insert(func_decl * v, expr * def) {
m_vars.push_back(v);
m_defs.push_back(def);
}
void insert(func_decl * v, expr * def);
virtual model_converter * translate(ast_translation & translator);
};

26
src/test/model_evaluator.cpp
View file

@ -26,13 +26,19 @@ void tst_model_evaluator() {
expr_ref vB0(m.mk_var(0, m.mk_bool_sort()), m);
expr_ref vB1(m.mk_var(1, m.mk_bool_sort()), m);
expr_ref vB2(m.mk_var(2, m.mk_bool_sort()), m);
expr_ref f01(m.mk_app(f, vI0, vB1), m);
expr_ref g01(m.mk_app(g, vI0, vB1), m);
expr_ref h01(m.mk_app(h, vI0, vB1), m);
expr* vI0p = vI0.get();
expr* vI1p = vI1.get();
expr* vB0p = vB0.get();
expr* vB1p = vB1.get();
expr* vB2p = vB2.get();
expr_ref f01(m.mk_app(f, vI0p, vB1p), m);
expr_ref g01(m.mk_app(g, vI0p, vB1p), m);
expr_ref h01(m.mk_app(h, vI0p, vB1p), m);
func_interp* fi = alloc(func_interp, m, 2);
func_interp* gi = alloc(func_interp, m, 2);
func_interp* hi = alloc(func_interp, m, 2);
hi->set_else(m.mk_ite(vB1, m.mk_app(f, vI0, vB1), m.mk_app(g, vI0, vB1)));
hi->set_else(m.mk_ite(vB1p, m.mk_app(f, vI0p, vB1p), m.mk_app(g, vI0p, vB1p)));
mdl.register_decl(h, hi);
@ -42,23 +48,23 @@ void tst_model_evaluator() {
{
symbol nI("N");
fi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0, m.mk_app(F, vI1, vB2))), vI0, a.mk_int(1)));
gi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0, m.mk_app(G, vI1, vB2))), a.mk_int(2), vI0));
fi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0p, m.mk_app(F, vI1p, vB2p))), vI0p, a.mk_int(1)));
gi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0p, m.mk_app(G, vI1p, vB2p))), a.mk_int(2), vI0p));
mdl.register_decl(g, gi);
mdl.register_decl(f, fi);
model_pp(std::cout, mdl);
e = m.mk_app(h, vI0, vB1);
e = m.mk_app(h, vI0p, vB1p);
eval(e, v);
std::cout << e << " " << v << "\n";
}
{
fi->set_else(m.mk_app(F, vI0, vB1));
gi->set_else(m.mk_app(G, vI0, vB1));
fi->set_else(m.mk_app(F, vI0p, vB1p));
gi->set_else(m.mk_app(G, vI0p, vB1p));
mdl.register_decl(g, gi);
mdl.register_decl(h, hi);
model_pp(std::cout, mdl);
e = m.mk_app(h, vI0, vB1);
e = m.mk_app(h, vI0p, vB1p);
eval(e, v);
std::cout << e << " " << v << "\n";
}

8
src/util/mpn.cpp
View file

@ -226,7 +226,7 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum,
mpn_sbuffer & n_denom) const
{
size_t d = 0;
while (((denom[lden-1] << d) & MASK_FIRST) == 0) d++;
while (lden > 0 && ((denom[lden-1] << d) & MASK_FIRST) == 0) d++;
SASSERT(d < DIGIT_BITS);
n_numer.resize(lnum+1);
@ -239,7 +239,8 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum,
for (size_t i = 0; i < lden; i++)
n_denom[i] = denom[i];
}
else {
else if (lnum != 0) {
SASSERT(lden > 0);
mpn_digit q = FIRST_BITS(d, numer[lnum-1]);
n_numer[lnum] = q;
for (size_t i = lnum-1; i > 0; i--)
@ -249,6 +250,9 @@ size_t mpn_manager::div_normalize(mpn_digit const * numer, size_t const lnum,
n_denom[i] = denom[i] << d | FIRST_BITS(d, denom[i-1]);
n_denom[0] = denom[0] << d;
}
else {
d = 0;
}
TRACE("mpn_norm", tout << "Normalized: n_numer="; display_raw(tout, n_numer.c_ptr(), n_numer.size());
tout << " n_denom="; display_raw(tout, n_denom.c_ptr(), n_denom.size()); tout << std::endl; );