diff --git a/examples/python/example.py b/examples/python/example.py
index 761ae10be..b93ed6abf 100644
--- a/examples/python/example.py
+++ b/examples/python/example.py
@@ -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).
diff --git a/scripts/mk_nuget_release.py b/scripts/mk_nuget_release.py
index ba0d44c3e..db7a1af64 100644
--- a/scripts/mk_nuget_release.py
+++ b/scripts/mk_nuget_release.py
@@ -85,7 +85,12 @@ def create_nuget_spec():
Microsoft.Z3
%s
Microsoft
- Z3 is a satisfiability modulo theories solver from Microsoft Research.
+
+Z3 is a satisfiability modulo theories solver from Microsoft Research.
+
+Linux Dependencies:
+ libgomp.so.1 installed
+
Copyright Microsoft Corporation. All rights reserved.
smt constraint solver theorem prover
https://raw.githubusercontent.com/Z3Prover/z3/master/package/icon.jpg
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 1f2f40941..a974e8b78 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -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);
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 4d3e5d312..2d406e0b4 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -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
}
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index fe0d4a13e..796e83535 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -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;
diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg
index f72bafbd8..623eefea3 100644
--- a/src/opt/opt_params.pyg
+++ b/src/opt/opt_params.pyg
@@ -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)'),
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 7feb8f615..4a35acd02 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -31,6 +31,7 @@ Notes:
#include
#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);
}
}
diff --git a/src/opt/optsmt.h b/src/opt/optsmt.h
index 6db7eaadf..c9aa4f41d 100644
--- a/src/opt/optsmt.h
+++ b/src/opt/optsmt.h
@@ -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 m_lower;
vector m_upper;
@@ -40,8 +43,8 @@ namespace opt {
svector m_labels;
sref_vector 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);
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index 93c172bf1..7fdfbf9aa 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -311,7 +311,7 @@ namespace smt {
bool_var var = antecedent.var();
unsigned lvl = m_ctx.get_assign_level(var);
SASSERT(var < static_cast(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);
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 3c601f400..f9df954fa 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -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;
}
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 4eb997c2e..72cc2404c 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -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";
}
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index 6aa49efae..e907b4462 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -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);
diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h
index 010e78cb3..67cf5cfee 100644
--- a/src/smt/theory_datatype.h
+++ b/src/smt/theory_datatype.h
@@ -73,7 +73,7 @@ namespace smt {
void sign_recognizer_conflict(enode * c, enode * r);
typedef enum { ENTER, EXIT } stack_op;
- typedef map, ptr_eq > parent_tbl;
+ typedef obj_map parent_tbl;
typedef std::pair stack_entry;
ptr_vector 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);