From 69dc74923908206f0a568ee89fd6cc1c8392802c Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Sat, 17 Nov 2018 21:02:00 +0700 Subject: [PATCH 01/10] Fix missing word in doc comment. --- src/api/z3_api.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index e1359949d..be463b1b0 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5579,7 +5579,7 @@ extern "C" { \brief Convert a goal into a DIMACS formatted string. The goal must be in CNF. You can convert a goal to CNF by applying the tseitin-cnf tactic. Bit-vectors are not automatically - converted to Booleans either, so the caller intends to + converted to Booleans either, so if the caller intends to preserve satisfiability, it should apply bit-blasting tactics. Quantifiers and theory atoms will not be encoded. From 9ec59fdb9338bd91ac0487d6b2fea8d6ba402ae7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 17 Nov 2018 15:04:25 -0800 Subject: [PATCH 02/10] fix #1934 Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 4 +- src/opt/maxres.cpp | 117 +++++++++++++++++++------------- src/opt/opt_context.cpp | 14 ++-- src/solver/check_sat_result.cpp | 1 + 4 files changed, 83 insertions(+), 53 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 88d7d7246..261890922 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -456,7 +456,9 @@ def check_dotnet(): raise MKException('Failed testing gacutil. Set environment variable GACUTIL with the path to gacutil.') def check_dotnet_core(): - # TBD: check DOTNET + # r = exec_cmd([DOTNET]) + # if r != 0: + # raise ... pass def check_ml(): diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 0b5f20db8..7f8b8ba91 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -108,6 +108,7 @@ private: bool m_pivot_on_cs; // prefer smaller correction set to core. bool m_dump_benchmarks; // display benchmarks (into wcnf format) + std::string m_trace_id; typedef ptr_vector exprs; @@ -152,6 +153,14 @@ public: (m.is_not(l, l) && is_uninterp_const(l)); } + void add(expr_ref_vector const& es) { + for (expr* e : es) add(e); + } + + void add(expr* e) { + s().assert_expr(e); + } + void add_soft(expr* e, rational const& w) { TRACE("opt", tout << mk_pp(e, m) << " |-> " << w << "\n";); expr_ref asum(m), fml(m); @@ -168,7 +177,7 @@ public: else { asum = mk_fresh_bool("soft"); fml = m.mk_iff(asum, e); - s().assert_expr(fml); + add(fml); } new_assumption(asum, w); } @@ -194,11 +203,8 @@ public: if (is_sat != l_true) return is_sat; while (m_lower < m_upper) { TRACE("opt_verbose", - display_vec(tout, m_asms); - s().display(tout); - tout << "\n"; - display(tout); - ); + s().display(tout << m_asms << "\n") << "\n"; + display(tout);); is_sat = check_sat_hill_climb(m_asms); if (m.canceled()) { return l_undef; @@ -206,8 +212,7 @@ public: switch (is_sat) { case l_true: CTRACE("opt", !m_model->is_true(m_asms), - tout << *m_model; - tout << "assumptions: "; + tout << *m_model << "assumptions: "; for (expr* a : m_asms) tout << mk_pp(a, m) << " -> " << (*m_model)(a) << " "; tout << "\n";); SASSERT(m_model->is_true(m_asms)); @@ -320,6 +325,7 @@ public: void found_optimum() { IF_VERBOSE(1, verbose_stream() << "found optimum\n";); + verify_assumptions(); m_lower.reset(); for (soft& s : m_soft) { s.is_true = m_model->is_true(s.s); @@ -348,7 +354,14 @@ public: st.update("maxres-correction-sets", m_stats.m_num_cs); } - lbool get_cores(vector& cores) { + struct weighted_core { + exprs m_core; + rational m_weight; + weighted_core(exprs const& c, rational const& w): + m_core(c), m_weight(w) {} + }; + + lbool get_cores(vector& cores) { // assume m_s is unsat. lbool is_sat = l_false; cores.reset(); @@ -361,7 +374,7 @@ public: get_mus_model(mdl); is_sat = minimize_core(_core); core.append(_core.size(), _core.c_ptr()); - // verify_core(core); + verify_core(core); ++m_stats.m_num_cores; if (is_sat != l_true) { IF_VERBOSE(100, verbose_stream() << "(opt.maxres minimization failed)\n";); @@ -373,13 +386,16 @@ public: m_lower = m_upper; return l_true; } + + // 1. remove all core literals from m_asms // 2. re-add literals of higher weight than min-weight. // 3. 'core' stores the core literals that are // re-encoded as assumptions, afterwards + cores.push_back(weighted_core(core, core_weight(core))); + remove_soft(core, m_asms); - split_core(core); - cores.push_back(core); + split_core(core); if (core.size() >= m_max_core_size) break; if (cores.size() >= m_max_num_cores) break; @@ -456,7 +472,7 @@ public: } lbool process_unsat() { - vector cores; + vector cores; lbool is_sat = get_cores(cores); if (is_sat != l_true) { return is_sat; @@ -478,9 +494,9 @@ public: return result; } - void process_unsat(vector const& cores) { + void process_unsat(vector const& cores) { for (auto const & c : cores) { - process_unsat(c); + process_unsat(c.m_core, c.m_weight); } } @@ -491,16 +507,15 @@ public: } } - void process_unsat(exprs const& core) { + void process_unsat(exprs const& core, rational w) { IF_VERBOSE(3, verbose_stream() << "(maxres cs model valid: " << (m_csmodel.get() != nullptr) << " cs size:" << m_correction_set_size << " core: " << core.size() << ")\n";); expr_ref fml(m); SASSERT(!core.empty()); - rational w = core_weight(core); TRACE("opt", display_vec(tout << "minimized core: ", core);); - IF_VERBOSE(10, display_vec(verbose_stream() << "core: ", core);); + IF_VERBOSE(10, display_vec(verbose_stream() << "core: ", core);); max_resolve(core, w); fml = mk_not(m, mk_and(m, core.size(), core.c_ptr())); - s().assert_expr(fml); + add(fml); m_lower += w; if (m_st == s_primal_dual) { m_lower = std::min(m_lower, m_upper); @@ -636,10 +651,10 @@ public: else { dd = mk_fresh_bool("d"); fml = m.mk_implies(dd, d); - s().assert_expr(fml); + add(fml); m_defs.push_back(fml); fml = m.mk_implies(dd, b_i); - s().assert_expr(fml); + add(fml); m_defs.push_back(fml); fml = m.mk_and(d, b_i); update_model(dd, fml); @@ -650,7 +665,7 @@ public: fml = m.mk_implies(asum, cls); update_model(asum, cls); new_assumption(asum, w); - s().assert_expr(fml); + add(fml); m_defs.push_back(fml); } } @@ -682,7 +697,7 @@ public: d = mk_fresh_bool("d"); fml = m.mk_implies(d, cls); update_model(d, cls); - s().assert_expr(fml); + add(fml); m_defs.push_back(fml); } @@ -691,10 +706,10 @@ public: } asum = mk_fresh_bool("a"); fml = m.mk_implies(asum, b_i1); - s().assert_expr(fml); + add(fml); m_defs.push_back(fml); fml = m.mk_implies(asum, cls); - s().assert_expr(fml); + add(fml); m_defs.push_back(fml); new_assumption(asum, w); @@ -702,7 +717,7 @@ public: update_model(asum, fml); } fml = m.mk_or(cs.size(), cs.c_ptr()); - s().assert_expr(fml); + add(fml); } void update_assignment(model_ref & mdl) { @@ -747,7 +762,7 @@ public: s.is_true = m_model->is_true(s.s); } - // DEBUG_CODE(verify_assignment();); + verify_assignment(); m_upper = upper; @@ -768,7 +783,7 @@ public: } fml = u.mk_lt(nsoft.size(), weights.c_ptr(), nsoft.c_ptr(), m_upper); TRACE("opt", tout << "block upper bound " << fml << "\n";);; - s().assert_expr(fml); + add(fml); } void remove_soft(exprs const& core, expr_ref_vector& asms) { @@ -819,40 +834,50 @@ public: void commit_assignment() override { if (m_found_feasible_optimum) { TRACE("opt", tout << "Committing feasible solution\n" << m_defs << " " << m_asms;); - s().assert_expr(m_defs); - s().assert_expr(m_asms); + add(m_defs); + add(m_asms); } // else: there is only a single assignment to these soft constraints. } void verify_core(exprs const& core) { - IF_VERBOSE(3, verbose_stream() << "verify core\n";); - ref smt_solver = mk_smt_solver(m, m_params, symbol()); - smt_solver->assert_expr(s().get_assertions()); - smt_solver->assert_expr(core); - lbool is_sat = smt_solver->check_sat(0, nullptr); - if (is_sat == l_true) { - IF_VERBOSE(0, verbose_stream() << "not a core\n";); - } + if (!gparams::get_ref().get_bool("model_validate", false)) return; + IF_VERBOSE(3, verbose_stream() << "verify core " << s().check_sat(core.size(), core.c_ptr()) << "\n";); + ref _solver = mk_smt_solver(m, m_params, symbol()); + _solver->assert_expr(s().get_assertions()); + _solver->assert_expr(core); + lbool is_sat = _solver->check_sat(0, nullptr); + IF_VERBOSE(0, verbose_stream() << "core status (l_false:) " << is_sat << "\n"); + VERIFY(is_sat == l_false); + } + + void verify_assumptions() { + if (!gparams::get_ref().get_bool("model_validate", false)) return; + IF_VERBOSE(1, verbose_stream() << "verify assumptions\n";); + ref _solver = mk_smt_solver(m, m_params, symbol()); + _solver->assert_expr(s().get_assertions()); + _solver->assert_expr(m_asms); + lbool is_sat = _solver->check_sat(0, nullptr); + IF_VERBOSE(1, verbose_stream() << "assignment status (l_true) " << is_sat << "\n";); + VERIFY(is_sat == l_true); } void verify_assignment() { + if (!gparams::get_ref().get_bool("model_validate", false)) return; IF_VERBOSE(1, verbose_stream() << "verify assignment\n";); - ref smt_solver = mk_smt_solver(m, m_params, symbol()); - smt_solver->assert_expr(s().get_assertions()); + ref _solver = mk_smt_solver(m, m_params, symbol()); + _solver->assert_expr(s().get_assertions()); expr_ref n(m); for (soft& s : m_soft) { n = s.s; if (!s.is_true) { n = mk_not(m, n); } - smt_solver->assert_expr(n); + _solver->assert_expr(n); } - lbool is_sat = smt_solver->check_sat(0, nullptr); - if (is_sat == l_false) { - IF_VERBOSE(0, verbose_stream() << "assignment is infeasible\n";); - } - IF_VERBOSE(1, verbose_stream() << "verified\n";); + lbool is_sat = _solver->check_sat(0, nullptr); + IF_VERBOSE(1, verbose_stream() << "assignment status (l_true) " << is_sat << "\n"); + VERIFY(is_sat == l_true); } }; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index d9c3457fa..29246c6f5 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -284,7 +284,9 @@ namespace opt { symbol pri = optp.priority(); IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n"); + lbool is_sat = s.check_sat(asms.size(),asms.c_ptr()); + TRACE("opt", s.display(tout << "initial search result: " << is_sat << "\n");); if (is_sat != l_false) { s.get_model(m_model); @@ -1555,7 +1557,6 @@ namespace opt { } void context::validate_model() { - return; if (!gparams::get_ref().get_bool("model_validate", false)) return; expr_ref_vector fmls(m); get_hard_constraints(fmls); @@ -1565,11 +1566,12 @@ namespace opt { mdl->set_model_completion(true); for (expr * f : fmls) { if (!mdl->is_true(f)) { - //IF_VERBOSE(0, m_fm->display(verbose_stream() << "fm\n")); - IF_VERBOSE(0, m_model_converter->display(verbose_stream() << "mc\n")); - IF_VERBOSE(0, verbose_stream() << "Failed to validate " << mk_pp(f, m) << "\n" << tmp << "\n"); - IF_VERBOSE(0, model_smt2_pp(verbose_stream(), m, *mdl, 0)); - IF_VERBOSE(11, verbose_stream() << to_string_internal() << "\n"); + IF_VERBOSE(0, + verbose_stream() << "Failed to validate " << mk_pp(f, m) << "\n" << tmp << "\n"; + m_fm->display(verbose_stream() << "fm\n"); + m_model_converter->display(verbose_stream() << "mc\n"); + model_smt2_pp(verbose_stream(), m, *mdl, 0); + verbose_stream() << to_string_internal() << "\n"); exit(0); } } diff --git a/src/solver/check_sat_result.cpp b/src/solver/check_sat_result.cpp index 28e6afeca..7431618df 100644 --- a/src/solver/check_sat_result.cpp +++ b/src/solver/check_sat_result.cpp @@ -36,6 +36,7 @@ void check_sat_result::set_reason_unknown(event_handler& eh) { } } + simple_check_sat_result::simple_check_sat_result(ast_manager & m): m_core(m), m_proof(m) { From e98da4320b6febeac1a38c435f8d03d35fea69f0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 17 Nov 2018 15:08:52 -0800 Subject: [PATCH 03/10] make dotnet core optional for mk_win_dist Signed-off-by: Nikolaj Bjorner --- scripts/mk_win_dist.py | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 10865676d..41229e438 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -25,6 +25,7 @@ VERBOSE=True DIST_DIR='dist' FORCE_MK=False DOTNET_ENABLED=True +DOTNET_CORE_ENABLED=False DOTNET_KEY_FILE=None JAVA_ENABLED=True GIT_HASH=False @@ -62,6 +63,7 @@ def display_help(): print(" -b , --build= subdirectory where x86 and x64 Z3 versions will be built (default: build-dist).") print(" -f, --force force script to regenerate Makefiles.") print(" --nodotnet do not include .NET bindings in the binary distribution files.") + print(" --dotnetcore build for dotnet core.") print(" --dotnet-key= sign the .NET assembly with the private key in .") print(" --nojava do not include Java bindings in the binary distribution files.") print(" --nopython do not include Python bindings in the binary distribution files.") @@ -72,7 +74,7 @@ def display_help(): # Parse configuration option for mk_make script def parse_options(): - global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE, PYTHON_ENABLED, X86ONLY, X64ONLY + global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, PYTHON_ENABLED, X86ONLY, X64ONLY path = BUILD_DIR options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 'help', @@ -80,6 +82,7 @@ def parse_options(): 'force', 'nojava', 'nodotnet', + 'dotnetcore', 'dotnet-key=', 'githash', 'nopython', @@ -99,6 +102,8 @@ def parse_options(): FORCE_MK = True elif opt == '--nodotnet': DOTNET_ENABLED = False + elif opt == '--dotnetcore': + DOTNET_CORE_ENABLED = True elif opt == '--nopython': PYTHON_ENABLED = False elif opt == '--dotnet-key': @@ -124,7 +129,11 @@ def mk_build_dir(path, x64): if not check_build_dir(path) or FORCE_MK: parallel = '--parallel=' + MAKEJOBS opts = ["python", os.path.join('scripts', 'mk_make.py'), parallel, "-b", path] - if DOTNET_ENABLED: + if DOTNET_CORE_ENABLED: + opts.append('--dotnetcore') + if not DOTNET_KEY_FILE is None: + opts.append('--dotnet-key=' + DOTNET_KEY_FILE) + elif DOTNET_ENABLED: opts.append('--dotnet') if not DOTNET_KEY_FILE is None: opts.append('--dotnet-key=' + DOTNET_KEY_FILE) @@ -208,7 +217,10 @@ def mk_dist_dir(x64): build_path = BUILD_X86_DIR dist_path = os.path.join(DIST_DIR, get_z3_name(x64)) mk_dir(dist_path) - mk_util.DOTNET_CORE_ENABLED = DOTNET_ENABLED + if DOTNET_CORE_ENABLED: + mk_util.DOTNET_CORE_ENABLED = True + else: + mk_util.DOTNET_CORE_ENABLED = DOTNET_ENABLED mk_util.DOTNET_KEY_FILE = DOTNET_KEY_FILE mk_util.JAVA_ENABLED = JAVA_ENABLED mk_util.PYTHON_ENABLED = PYTHON_ENABLED From d45b8a3ac83ef49d5b46f32b26bac1f3dd1acfbf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 17 Nov 2018 15:24:54 -0800 Subject: [PATCH 04/10] fix debug build, add access to numerics from model Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/Context.cs | 20 ++++++++++++++++++++ src/api/dotnet/Model.cs | 8 ++++++++ src/opt/maxres.cpp | 2 +- 3 files changed, 29 insertions(+), 1 deletion(-) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index ac11022c1..a941f8e86 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -931,6 +931,26 @@ namespace Microsoft.Z3 return new BoolExpr(this, Native.Z3_mk_xor(nCtx, t1.NativeObject, t2.NativeObject)); } + /// + /// Create an expression representing t1 xor t2 xor t3 ... . + /// + public BoolExpr MkXor(IEnumerable ts) + { + Debug.Assert(ts != null); + Debug.Assert(ts.All(a => a != null)); + CheckContextMatch(ts); + BoolExpr r = null; + foreach (var t in ts) { + if (r == null) + r = t; + else + r = MkXor(r, t); + } + if (r == null) + r = MkTrue(); + return r; + } + /// /// Create an expression representing t[0] and t[1] and .... /// diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs index c24516c22..c0cb091b0 100644 --- a/src/api/dotnet/Model.cs +++ b/src/api/dotnet/Model.cs @@ -238,6 +238,14 @@ namespace Microsoft.Z3 return Eval(t, completion); } + /// + /// Evaluate expression to a double, assuming it is a numeral already. + /// + public double Double(Expr t) { + var r = Eval(t, true); + return Native.Z3_get_numeral_double(Context.nCtx, r.NativeObject); + } + /// /// The number of uninterpreted sorts that the model has an interpretation for. /// diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 7f8b8ba91..98e6531ea 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -405,7 +405,7 @@ public: TRACE("opt", tout << "sat: " << is_sat << " num cores: " << cores.size() << "\n"; - for (auto const& c : cores) display_vec(tout, c); + for (auto const& c : cores) display_vec(tout, c.m_core); tout << "num assumptions: " << m_asms.size() << "\n";); return is_sat; From 141cd687ffe36f3f94b4de6b7e56eb2f07cbcb03 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 17 Nov 2018 15:37:36 -0800 Subject: [PATCH 05/10] disable validation in builds Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 6 +++--- src/opt/opt_context.cpp | 1 + 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 98e6531ea..75a42886c 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -841,7 +841,7 @@ public: } void verify_core(exprs const& core) { - if (!gparams::get_ref().get_bool("model_validate", false)) return; + return; IF_VERBOSE(3, verbose_stream() << "verify core " << s().check_sat(core.size(), core.c_ptr()) << "\n";); ref _solver = mk_smt_solver(m, m_params, symbol()); _solver->assert_expr(s().get_assertions()); @@ -852,7 +852,7 @@ public: } void verify_assumptions() { - if (!gparams::get_ref().get_bool("model_validate", false)) return; + return; IF_VERBOSE(1, verbose_stream() << "verify assumptions\n";); ref _solver = mk_smt_solver(m, m_params, symbol()); _solver->assert_expr(s().get_assertions()); @@ -863,7 +863,7 @@ public: } void verify_assignment() { - if (!gparams::get_ref().get_bool("model_validate", false)) return; + return; IF_VERBOSE(1, verbose_stream() << "verify assignment\n";); ref _solver = mk_smt_solver(m, m_params, symbol()); _solver->assert_expr(s().get_assertions()); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 29246c6f5..a6f3d8152 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1557,6 +1557,7 @@ namespace opt { } void context::validate_model() { + return; if (!gparams::get_ref().get_bool("model_validate", false)) return; expr_ref_vector fmls(m); get_hard_constraints(fmls); From 1603075189b2298dfbad2db8271663f898c49f6c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 17 Nov 2018 15:46:06 -0800 Subject: [PATCH 06/10] add empty/full to java #1944 Signed-off-by: Nikolaj Bjorner --- src/api/java/Context.java | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 08d20dfb2..ede494598 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2173,6 +2173,22 @@ public class Context implements AutoCloseable { { checkContextMatch(t); return (ReExpr) Expr.create(this, Native.mkReIntersect(nCtx(), t.length, AST.arrayToNative(t))); + } + + /** + * Create the empty regular expression. + */ + public ReExpr mkEmptyRe(Sort s) + { + return (ReExpr) Expr.create(this, Native.mkReEmpty(nCtx(), s.getNativeObject())); + } + + /** + * Create the full regular expression. + */ + public ReExpr mkFullRe(Sort s) + { + return (ReExpr) Expr.create(this, Native.mkReFull(nCtx(), s.getNativeObject())); } /** From d400929d9a05423f7ed06c7d75fb4e55e3f13eec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Nov 2018 08:56:30 -0800 Subject: [PATCH 07/10] fix #1945 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_core.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 4ca4928d0..f3a3e9238 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -503,7 +503,7 @@ namespace smt { tout << "lower: " << lower << "\n"; tout << "upper: " << upper << "\n";); - mk_axiom(eqz, eq, true); + mk_axiom(eqz, eq, false); mk_axiom(eqz, lower, false); mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor)); rational k; From fb1287155e28a675d0783e4a24d1483126cd80b1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Nov 2018 08:59:27 -0800 Subject: [PATCH 08/10] fix windows build_dist setting Signed-off-by: Nikolaj Bjorner --- scripts/mk_win_dist.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 41229e438..e61a7714c 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -220,7 +220,7 @@ def mk_dist_dir(x64): if DOTNET_CORE_ENABLED: mk_util.DOTNET_CORE_ENABLED = True else: - mk_util.DOTNET_CORE_ENABLED = DOTNET_ENABLED + mk_util.DOTNET_ENABLED = DOTNET_ENABLED mk_util.DOTNET_KEY_FILE = DOTNET_KEY_FILE mk_util.JAVA_ENABLED = JAVA_ENABLED mk_util.PYTHON_ENABLED = PYTHON_ENABLED From 6ef2557e2a96657c85dee84397e4fdfa5027fe0d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Nov 2018 09:34:33 -0800 Subject: [PATCH 09/10] investigate #1946 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 4 + src/tactic/bv/bit_blaster_model_converter.cpp | 6 +- src/util/params.cpp | 101 ++++++++---------- 3 files changed, 50 insertions(+), 61 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index f68b908e2..70dcb158e 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6164,6 +6164,10 @@ class ModelRef(Z3PPObject): def __deepcopy__(self): return self.translate(self.ctx) +def Model(ctx = None): + ctx = _get_ctx(ctx) + return ModelRef(Z3_mk_model(ctx.ref()), ctx) + def is_as_array(n): """Return true if n is a Z3 expression of the form (_ as-array f).""" return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast()) diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp index 5474700c3..be6ea8b7a 100644 --- a/src/tactic/bv/bit_blaster_model_converter.cpp +++ b/src/tactic/bv/bit_blaster_model_converter.cpp @@ -72,10 +72,8 @@ struct bit_blaster_model_converter : public model_converter { } TRACE("blaster_mc", tout << "bits that should not be included in the model:\n"; - obj_hashtable::iterator it = bits.begin(); - obj_hashtable::iterator end = bits.end(); - for (; it != end; ++it) { - tout << (*it)->get_name() << " "; + for (func_decl* f : bits) { + tout << f->get_name() << " "; } tout << "\n";); diff --git a/src/util/params.cpp b/src/util/params.cpp index d7e05cb00..43f53514a 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -161,19 +161,15 @@ struct param_descrs::imp { void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const { svector names; - dictionary::iterator it = m_info.begin(); - dictionary::iterator end = m_info.end(); - for (; it != end; ++it) { - names.push_back(it->m_key); + for (auto const& kv : m_info) { + names.push_back(kv.m_key); } std::sort(names.begin(), names.end(), lt()); - svector::iterator it2 = names.begin(); - svector::iterator end2 = names.end(); - for (; it2 != end2; ++it2) { + for (symbol const& name : names) { for (unsigned i = 0; i < indent; i++) out << " "; if (smt2_style) out << ':'; - char const * s = it2->bare_str(); + char const * s = name.bare_str(); unsigned n = static_cast(strlen(s)); for (unsigned i = 0; i < n; i++) { if (smt2_style && s[i] == '_') @@ -186,7 +182,7 @@ struct param_descrs::imp { out << s[i]; } info d; - m_info.find(*it2, d); + m_info.find(name, d); SASSERT(d.m_descr); out << " (" << d.m_kind << ")"; if (include_descr) @@ -198,10 +194,8 @@ struct param_descrs::imp { } void copy(param_descrs & other) { - dictionary::iterator it = other.m_imp->m_info.begin(); - dictionary::iterator end = other.m_imp->m_info.end(); - for (; it != end; ++it) { - insert(it->m_key, it->m_value.m_kind, it->m_value.m_descr, it->m_value.m_default, it->m_value.m_module); + for (auto const& kv : other.m_imp->m_info) { + insert(kv.m_key, kv.m_value.m_kind, kv.m_value.m_descr, kv.m_value.m_default, kv.m_value.m_module); } } @@ -346,24 +340,22 @@ public: void reset(symbol const & k); void reset(char const * k); - void validate(param_descrs const & p) { - svector::iterator it = m_entries.begin(); - svector::iterator end = m_entries.end(); + void validate(param_descrs const & p) { symbol suffix, prefix; - for (; it != end; ++it) { - param_kind expected = p.get_kind_in_module(it->first); + for (params::entry& e : m_entries) { + param_kind expected = p.get_kind_in_module(e.first); if (expected == CPK_INVALID) { std::stringstream strm; - strm << "unknown parameter '" << it->first.str() << "'\n"; + strm << "unknown parameter '" << e.first.str() << "'\n"; strm << "Legal parameters are:\n"; p.display(strm, 2, false, false); throw default_exception(strm.str()); } - if (it->second.m_kind != expected && - !(it->second.m_kind == CPK_UINT && expected == CPK_NUMERAL)) { + if (e.second.m_kind != expected && + !(e.second.m_kind == CPK_UINT && expected == CPK_NUMERAL)) { std::stringstream strm; - strm << "Parameter " << it->first.str() << " was given argument of type "; - strm << it->second.m_kind << ", expected " << expected; + strm << "Parameter " << e.first.str() << " was given argument of type "; + strm << e.second.m_kind << ", expected " << expected; throw default_exception(strm.str()); } } @@ -405,28 +397,26 @@ public: void display(std::ostream & out) const { out << "(params"; - svector::const_iterator it = m_entries.begin(); - svector::const_iterator end = m_entries.end(); - for (; it != end; ++it) { - out << " " << it->first; - switch (it->second.m_kind) { + for (params::entry const& e : m_entries) { + out << " " << e.first; + switch (e.second.m_kind) { case CPK_BOOL: - out << " " << (it->second.m_bool_value?"true":"false"); + out << " " << (e.second.m_bool_value?"true":"false"); break; case CPK_UINT: - out << " " <second.m_uint_value; + out << " " <second.m_double_value; + out << " " << e.second.m_double_value; break; case CPK_NUMERAL: - out << " " << *(it->second.m_rat_value); + out << " " << *(e.second.m_rat_value); break; case CPK_SYMBOL: - out << " " << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value); + out << " " << symbol::mk_symbol_from_c_ptr(e.second.m_sym_value); break; case CPK_STRING: - out << " " << it->second.m_str_value; + out << " " << e.second.m_str_value; break; default: UNREACHABLE(); @@ -437,31 +427,29 @@ public: } void display_smt2(std::ostream & out, char const* module, param_descrs& descrs) const { - svector::const_iterator it = m_entries.begin(); - svector::const_iterator end = m_entries.end(); - for (; it != end; ++it) { - if (!descrs.contains(it->first)) continue; + for (params::entry const& e : m_entries) { + if (!descrs.contains(e.first)) continue; out << "(set-option :"; out << module << "."; - out << it->first; - switch (it->second.m_kind) { + out << e.first; + switch (e.second.m_kind) { case CPK_BOOL: - out << " " << (it->second.m_bool_value?"true":"false"); + out << " " << (e.second.m_bool_value?"true":"false"); break; case CPK_UINT: - out << " " <second.m_uint_value; + out << " " <second.m_double_value; + out << " " << e.second.m_double_value; break; case CPK_NUMERAL: - out << " " << *(it->second.m_rat_value); + out << " " << *(e.second.m_rat_value); break; case CPK_SYMBOL: - out << " " << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value); + out << " " << symbol::mk_symbol_from_c_ptr(e.second.m_sym_value); break; case CPK_STRING: - out << " " << it->second.m_str_value; + out << " " << e.second.m_str_value; break; default: UNREACHABLE(); @@ -472,29 +460,27 @@ public: } void display(std::ostream & out, symbol const & k) const { - svector::const_iterator it = m_entries.begin(); - svector::const_iterator end = m_entries.end(); - for (; it != end; ++it) { - if (it->first != k) + for (params::entry const& e : m_entries) { + if (e.first != k) continue; - switch (it->second.m_kind) { + switch (e.second.m_kind) { case CPK_BOOL: - out << (it->second.m_bool_value?"true":"false"); + out << (e.second.m_bool_value?"true":"false"); return; case CPK_UINT: - out << it->second.m_uint_value; + out << e.second.m_uint_value; return; case CPK_DOUBLE: - out << it->second.m_double_value; + out << e.second.m_double_value; return; case CPK_NUMERAL: - out << *(it->second.m_rat_value); + out << *(e.second.m_rat_value); return; case CPK_SYMBOL: - out << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value); + out << symbol::mk_symbol_from_c_ptr(e.second.m_sym_value); return; case CPK_STRING: - out << it->second.m_str_value; + out << e.second.m_str_value; return; default: out << "internal"; @@ -786,6 +772,7 @@ void params::del_values() { return false; \ } + bool params::contains(symbol const & k) const { CONTAINS(k); } From a9e6d83c6e746480811b80467a33281a2e554e21 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Nov 2018 10:40:08 -0800 Subject: [PATCH 10/10] std::cout -> out Signed-off-by: Nikolaj Bjorner --- src/solver/solver.h | 2 ++ src/util/gparams.cpp | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/solver/solver.h b/src/solver/solver.h index 5329161cd..7437a5a08 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -146,6 +146,8 @@ public: lbool check_sat(app_ref_vector const& asms) { return check_sat(asms.size(), (expr* const*)asms.c_ptr()); } + lbool check_sat() { return check_sat(0, nullptr); } + /** \brief Check satisfiability modulo a cube and a clause. diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 4ba3b3b5c..9ab3123a2 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -520,7 +520,7 @@ public: try { symbol m, p; normalize(name, m, p); - std::cout << name << " " << m << " " << p << "\n"; + out << name << " " << m << " " << p << "\n"; param_descrs * d; if (m == symbol::null) { d = &get_param_descrs();