mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-01-18 18:09:22 -08:00
commit 1efbc25b3b
13 changed files with 73 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

2
examples/python/example.py
View file

@ -2,7 +2,7 @@
# The Z3 Python API requires libz3.dll/.so/.dylib in the
# PATH/LD_LIBRARY_PATH/DYLD_LIBRARY_PATH
# environment variable and the PYTHON_PATH environment variable
# environment variable and the PYTHONPATH environment variable
# needs to point to the `python' directory that contains `z3/z3.py'
# (which is at bin/python in our binary releases).

7
scripts/mk_nuget_release.py
View file

@ -85,7 +85,12 @@ def create_nuget_spec():
<id>Microsoft.Z3</id>
<version>%s</version>
<authors>Microsoft</authors>
<description>Z3 is a satisfiability modulo theories solver from Microsoft Research.</description>
<description>
Z3 is a satisfiability modulo theories solver from Microsoft Research.
Linux Dependencies:
libgomp.so.1 installed
</description>
<copyright>Copyright Microsoft Corporation. All rights reserved.</copyright>
<tags>smt constraint solver theorem prover</tags>
<iconUrl>https://raw.githubusercontent.com/Z3Prover/z3/master/package/icon.jpg</iconUrl>

1
src/ast/ast.cpp
View file

@ -2138,7 +2138,6 @@ app * ast_manager::mk_app_core(func_decl * decl, unsigned num_args, expr * const
app * new_node = nullptr;
unsigned sz = app::get_obj_size(num_args);
void * mem = allocate_node(sz);
try {
if (m_int_real_coercions && coercion_needed(decl, num_args, args)) {
expr_ref_buffer new_args(*this);

17
src/opt/opt_context.cpp
View file

@ -125,7 +125,7 @@ namespace opt {
m_solver(nullptr),
m_pareto1(false),
m_box_index(UINT_MAX),
m_optsmt(m),
m_optsmt(m, *this),
m_scoped_state(m),
m_fm(alloc(generic_model_converter, m, "opt")),
m_model_fixed(),
@ -357,6 +357,17 @@ namespace opt {
}
}
void context::set_model(model_ref& m) {
m_model = m;
opt_params optp(m_params);
if (optp.dump_models()) {
model_ref md = m->copy();
fix_model(md);
std::cout << *md << "\n";
}
}
void context::get_model_core(model_ref& mdl) {
mdl = m_model;
fix_model(mdl);
@ -1062,6 +1073,9 @@ namespace opt {
void context::model_updated(model* md) {
model_ref mdl = md;
set_model(mdl);
#if 0
opt_params optp(m_params);
symbol prefix = optp.solution_prefix();
if (prefix == symbol::null || prefix == symbol("")) return;
@ -1074,6 +1088,7 @@ namespace opt {
out << *mdl;
out.close();
}
#endif
}

2
src/opt/opt_context.h
View file

@ -189,7 +189,7 @@ namespace opt {
bool empty() override { return m_scoped_state.m_objectives.empty(); }
void set_hard_constraints(expr_ref_vector const& hard) override;
lbool optimize(expr_ref_vector const& asms) override;
void set_model(model_ref& _m) override { m_model = _m; }
void set_model(model_ref& _m) override;
void get_model_core(model_ref& _m) override;
void get_box_model(model_ref& _m, unsigned index) override;
void fix_model(model_ref& _m) override;

1
src/opt/opt_params.pyg
View file

@ -5,6 +5,7 @@ def_module_params('opt',
('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"),
('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', 'box'"),
('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
('dump_models', BOOL, False, 'display intermediary models to stdout'),
('solution_prefix', SYMBOL, '', "path prefix to dump intermediary, but non-optimal, solutions"),
('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
('rlimit', UINT, 0, 'resource limit (0 means no limit)'),

5
src/opt/optsmt.cpp
View file

@ -31,6 +31,7 @@ Notes:
#include <typeinfo>
#include "opt/optsmt.h"
#include "opt/opt_solver.h"
#include "opt/opt_context.h"
#include "ast/arith_decl_plugin.h"
#include "smt/theory_arith.h"
#include "ast/ast_pp.h"
@ -362,12 +363,14 @@ namespace opt {
verbose_stream() << "(optsmt lower bound: " << v << ")\n";
else
verbose_stream() << "(optsmt upper bound: " << (-v) << ")\n";
);
);
expr_ref tmp(m);
for (unsigned i = idx+1; i < m_vars.size(); ++i) {
m_s->maximize_objective(i, tmp);
m_lower[i] = m_s->saved_objective_value(i);
}
m_context.set_model(m_model);
}
}

7
src/opt/optsmt.h
View file

@ -27,8 +27,11 @@ namespace opt {
Returns an optimal assignment to objective functions.
*/
class context;
class optsmt {
ast_manager& m;
context& m_context;
opt_solver* m_s;
vector<inf_eps> m_lower;
vector<inf_eps> m_upper;
@ -40,8 +43,8 @@ namespace opt {
svector<symbol> m_labels;
sref_vector<model> m_models;
public:
optsmt(ast_manager& m):
m(m), m_s(nullptr), m_objs(m), m_lower_fmls(m) {}
optsmt(ast_manager& m, context& ctx):
m(m), m_context(ctx), m_s(nullptr), m_objs(m), m_lower_fmls(m) {}
void setup(opt_solver& solver);

8
src/smt/smt_conflict_resolution.cpp
View file

@ -311,7 +311,7 @@ namespace smt {
bool_var var = antecedent.var();
unsigned lvl = m_ctx.get_assign_level(var);
SASSERT(var < static_cast<int>(m_ctx.get_num_bool_vars()));
TRACE("conflict", tout << "processing antecedent (level " << lvl << "):";
TRACE("conflict_", tout << "processing antecedent (level " << lvl << "):";
m_ctx.display_literal(tout, antecedent);
m_ctx.display_detailed_literal(tout << " ", antecedent) << "\n";);
@ -429,7 +429,7 @@ namespace smt {
void conflict_resolution::finalize_resolve(b_justification conflict, literal not_l) {
unmark_justifications(0);
TRACE("conflict", m_ctx.display_literals(tout << "before minimization:\n", m_lemma) << "\n";);
TRACE("conflict", m_ctx.display_literals(tout << "before minimization:\n", m_lemma) << "\n" << m_lemma << "\n";);
TRACE("conflict_verbose",m_ctx.display_literals_verbose(tout << "before minimization:\n", m_lemma) << "\n";);
@ -484,7 +484,7 @@ namespace smt {
unsigned num_marks = 0;
if (not_l != null_literal) {
TRACE("conflict", tout << "not_l: "; m_ctx.display_literal_verbose(tout, not_l); tout << "\n";);
TRACE("conflict", tout << "not_l: "; m_ctx.display_literal_verbose(tout, not_l) << "\n";);
process_antecedent(not_l, num_marks);
}
@ -497,7 +497,7 @@ namespace smt {
}
TRACE("conflict", tout << "processing consequent id: " << idx << " lit: " << consequent << " "; m_ctx.display_literal(tout, consequent);
m_ctx.display_literal_verbose(tout, consequent) << "\n";
m_ctx.display_literal_verbose(tout << " ", consequent) << "\n";
tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << " level: " << m_ctx.get_assign_level(consequent) << "\n";
);
SASSERT(js != null_b_justification);

1
src/smt/smt_context.cpp
View file

@ -3918,6 +3918,7 @@ namespace smt {
conflict_lvl > m_search_lvl + 1 &&
!m_manager.proofs_enabled() &&
m_units_to_reassert.size() < m_fparams.m_delay_units_threshold;
if (delay_forced_restart) {
new_lvl = conflict_lvl - 1;
}

2
src/smt/smt_context_pp.cpp
View file

@ -263,7 +263,7 @@ namespace smt {
for (unsigned i = 0; i < sz; i++) {
expr * n = m_b_internalized_stack.get(i);
bool_var v = get_bool_var_of_id(n->get_id());
out << "(#" << n->get_id() << " -> p!" << v << ") ";
out << "(#" << n->get_id() << " -> " << literal(v, false) << ") ";
}
out << "\n";
}

49
src/smt/theory_datatype.cpp
View file

@ -455,33 +455,46 @@ namespace smt {
return d->m_constructor;
}
void theory_datatype::explain_is_child(enode* parent, enode* child) {
enode * parentc = oc_get_cstor(parent);
if (parent != parentc) {
m_used_eqs.push_back(enode_pair(parent, parentc));
}
// collect equalities on all children that may have been used.
bool found = false;
for (enode * arg : enode::args(parentc)) {
// found an argument which is equal to root
if (arg->get_root() == child->get_root()) {
if (arg != child) {
m_used_eqs.push_back(enode_pair(arg, child));
}
found = true;
}
}
VERIFY(found);
}
// explain the cycle root -> ... -> app -> root
void theory_datatype::occurs_check_explain(enode * app, enode * root) {
TRACE("datatype", tout << "occurs_check_explain " << mk_bounded_pp(app->get_owner(), get_manager()) << " <-> " << mk_bounded_pp(root->get_owner(), get_manager()) << "\n";);
enode* app_parent = nullptr;
// first: explain that root=v, given that app=cstor(...,v,...)
for (enode * arg : enode::args(oc_get_cstor(app))) {
// found an argument which is equal to root
if (arg->get_root() == root->get_root()) {
if (arg != root)
m_used_eqs.push_back(enode_pair(arg, root));
break;
}
}
explain_is_child(app, root);
// now explain app=cstor(..,v,..) where v=root, and recurse with parent of app
while (app->get_root() != root->get_root()) {
enode * app_cstor = oc_get_cstor(app);
if (app != app_cstor)
m_used_eqs.push_back(enode_pair(app, app_cstor));
app_parent = m_parent[app->get_root()];
app = app_parent;
enode* parent_app = m_parent[app->get_root()];
explain_is_child(parent_app, app);
SASSERT(is_constructor(parent_app));
app = parent_app;
}
SASSERT(app->get_root() == root->get_root());
if (app != root)
if (app != root) {
m_used_eqs.push_back(enode_pair(app, root));
}
TRACE("datatype",
tout << "occurs_check\n";
@ -706,11 +719,11 @@ namespace smt {
sort * s = recognizer->get_decl()->get_domain(0);
if (d->m_recognizers.empty()) {
SASSERT(m_util.is_datatype(s));
d->m_recognizers.resize(m_util.get_datatype_num_constructors(s));
d->m_recognizers.resize(m_util.get_datatype_num_constructors(s), nullptr);
}
SASSERT(d->m_recognizers.size() == m_util.get_datatype_num_constructors(s));
unsigned c_idx = m_util.get_recognizer_constructor_idx(recognizer->get_decl());
if (d->m_recognizers[c_idx] == 0) {
if (d->m_recognizers[c_idx] == nullptr) {
lbool val = ctx.get_assignment(recognizer);
TRACE("datatype", tout << "adding recognizer to v" << v << " rec: #" << recognizer->get_owner_id() << " val: " << val << "\n";);
if (val == l_true) {
@ -782,7 +795,7 @@ namespace smt {
region & reg = ctx.get_region();
TRACE("datatype_conflict", tout << mk_ismt2_pp(recognizer->get_owner(), get_manager()) << "\n";
for (literal l : lits) {
ctx.display_detailed_literal(tout, l); tout << "\n";
ctx.display_detailed_literal(tout, l) << "\n";
}
for (auto const& p : eqs) {
tout << enode_eq_pp(p, ctx);

3
src/smt/theory_datatype.h
View file

@ -73,7 +73,7 @@ namespace smt {
void sign_recognizer_conflict(enode * c, enode * r);
typedef enum { ENTER, EXIT } stack_op;
typedef map<enode*, enode*, obj_ptr_hash<enode>, ptr_eq<enode> > parent_tbl;
typedef obj_map<enode, enode*> parent_tbl;
typedef std::pair<stack_op, enode*> stack_entry;
ptr_vector<enode> m_to_unmark;
@ -102,6 +102,7 @@ namespace smt {
bool occurs_check(enode * n);
bool occurs_check_enter(enode * n);
void occurs_check_explain(enode * top, enode * root);
void explain_is_child(enode* parent, enode* child);
void mk_split(theory_var v);