diff --git a/CMakeLists.txt b/CMakeLists.txt index c169be14d..df6d528b0 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -289,12 +289,13 @@ endif() ################################################################################ # Tracing ################################################################################ -option(ENABLE_TRACING OFF "Enable tracing") -if (ENABLE_TRACING) +option(ENABLE_TRACING_FOR_NON_DEBUG "Enable tracing in non-debug builds." OFF) +if (ENABLE_TRACING_FOR_NON_DEBUG) list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_TRACE") +else() + # Tracing is always enabled in debug builds + list(APPEND Z3_COMPONENT_CXX_DEFINES $<$:_TRACE>) endif() -# Should we always enable tracing when doing a debug build? -list(APPEND Z3_COMPONENT_CXX_DEFINES $<$:_TRACE>) ################################################################################ # Postion independent code diff --git a/README-CMake.md b/README-CMake.md index 47cc70332..47ec11a7c 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -266,7 +266,7 @@ The following useful options can be passed to CMake whilst configuring. * ``CMAKE_INSTALL_LIBDIR`` - STRING. The path to install z3 libraries (relative to ``CMAKE_INSTALL_PREFIX``), e.g. ``lib``. * ``CMAKE_INSTALL_PREFIX`` - STRING. The install prefix to use (e.g. ``/usr/local/``). * ``CMAKE_INSTALL_PYTHON_PKG_DIR`` - STRING. The path to install the z3 python bindings. This can be relative (to ``CMAKE_INSTALL_PREFIX``) or absolute. -* ``ENABLE_TRACING`` - BOOL. If set to ``TRUE`` enable tracing, if set to ``FALSE`` disable tracing. +* ``ENABLE_TRACING_FOR_NON_DEBUG`` - BOOL. If set to ``TRUE`` enable tracing in non-debug builds, if set to ``FALSE`` disable tracing in non-debug builds. Note in debug builds tracing is always enabled. * ``BUILD_LIBZ3_SHARED`` - BOOL. If set to ``TRUE`` build libz3 as a shared library otherwise build as a static library. * ``ENABLE_EXAMPLE_TARGETS`` - BOOL. If set to ``TRUE`` add the build targets for building the API examples. * ``USE_OPENMP`` - BOOL. If set to ``TRUE`` and OpenMP support is detected build with OpenMP support. diff --git a/doc/README b/doc/README index a81ed2856..e46554230 100644 --- a/doc/README +++ b/doc/README @@ -1,7 +1,7 @@ API documentation ----------------- -To generate the API documentation for the C, .NET and Python APIs, we must execute +To generate the API documentation for the C, C++, .NET, Java and Python APIs, we must execute python mk_api_doc.py diff --git a/examples/c/README b/examples/c/README index 5ea885519..4ca71e0f8 100644 --- a/examples/c/README +++ b/examples/c/README @@ -1,4 +1,4 @@ -Small example using the c++ bindings. +Small example using the C bindings. To build the example execute make examples in the build directory. diff --git a/examples/maxsat/README b/examples/maxsat/README index cf022d847..e5e4ba610 100644 --- a/examples/maxsat/README +++ b/examples/maxsat/README @@ -1,4 +1,4 @@ -Small example using the c++ bindings. +Small example using the C bindings. To build the example execute make examples in the build directory. diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 1c7ee4ab5..e6de3e8ea 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -28,6 +28,7 @@ CXX=getenv("CXX", None) CC=getenv("CC", None) CPPFLAGS=getenv("CPPFLAGS", "") CXXFLAGS=getenv("CXXFLAGS", "") +AR=getenv("AR", "ar") EXAMP_DEBUG_FLAG='' LDFLAGS=getenv("LDFLAGS", "") JNI_HOME=getenv("JNI_HOME", None) @@ -496,8 +497,8 @@ def is64(): def check_ar(): if is_verbose(): print("Testing ar...") - if which('ar') is None: - raise MKException('ar (archive tool) was not found') + if which(AR) is None: + raise MKException('%s (archive tool) was not found' % AR) def find_cxx_compiler(): global CXX, CXX_COMPILERS @@ -2365,7 +2366,7 @@ def mk_config(): config.write('CXX_OUT_FLAG=-o \n') config.write('OBJ_EXT=.o\n') config.write('LIB_EXT=.a\n') - config.write('AR=ar\n') + config.write('AR=%s\n' % AR) config.write('AR_FLAGS=rcs\n') config.write('AR_OUTFLAG=\n') config.write('EXE_EXT=\n') @@ -2386,6 +2387,7 @@ def mk_config(): print('Host platform: %s' % sysname) print('C++ Compiler: %s' % CXX) print('C Compiler : %s' % CC) + print('Archive Tool: %s' % AR) print('Arithmetic: %s' % ARITH) print('OpenMP: %s' % HAS_OMP) print('Prefix: %s' % PREFIX) diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp index 4f2ce81c5..f8f44b6d9 100644 --- a/src/qe/qe_arrays.cpp +++ b/src/qe/qe_arrays.cpp @@ -305,16 +305,23 @@ namespace qe { SASSERT(!contains_x(t)); if (s == m_var->x()) { - expr_ref result(s, m); + expr_ref result(t, m); expr_ref_vector args(m); sort* range = get_array_range(m.get_sort(s)); for (unsigned i = 0; i < idxs.size(); ++i) { - app_ref var(m); + app_ref var(m), sel(m); + expr_ref val(m); var = m.mk_fresh_const("value", range); vars.push_back(var); args.reset(); - args.push_back(result); + + args.push_back (s); args.append(idxs[i].m_values.size(), idxs[i].m_vars); + sel = a.mk_select (args.size (), args.c_ptr ()); + VERIFY (model.eval (sel, val)); + model.register_decl (var->get_decl (), val); + + args[0] = result; args.push_back(var); result = a.mk_store(args.size(), args.c_ptr()); } @@ -390,15 +397,15 @@ namespace qe { } lbool compare(expr* val1, expr* val2) { - if (val1 == val2) { - return l_true; - } + if (m.are_equal (val1, val2)) return l_true; + if (m.are_distinct (val1, val2)) return l_false; + if (is_uninterp(val1) || is_uninterp(val2)) { // TBD chase definition of nested array. return l_undef; } - return l_true; + return l_undef; } }; diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index c8ec34726..cb8546b6c 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -134,9 +134,7 @@ class mbp::impl { expr* e = lits[i].get(), *l, *r; if (m.is_eq(e, l, r) && reduce_eq(is_var, l, r, v, t)) { reduced = true; - lits[i] = lits.back(); - lits.pop_back(); - --i; + project_plugin::erase(lits, i); expr_safe_replace sub(m); sub.insert(v, t); is_rem.mark(v); @@ -148,12 +146,16 @@ class mbp::impl { } } if (reduced) { + unsigned j = 0; for (unsigned i = 0; i < vars.size(); ++i) { - if (is_rem.is_marked(vars[i].get())) { - vars[i] = vars.back(); - vars.pop_back(); + if (!is_rem.is_marked(vars[i].get())) { + if (i != j) { + vars[j] = vars[i].get(); + } + ++j; } } + vars.shrink(j); } return reduced; } @@ -333,9 +335,7 @@ public: sub(fmls[i].get(), tmp); rw(tmp); if (m.is_true(tmp)) { - fmls[i] = fmls.back(); - fmls.pop_back(); - --i; + project_plugin::erase(fmls, i); } else { fmls[i] = tmp; diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 0a5c40dbd..1b0555b22 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -500,40 +500,40 @@ namespace qe { } } - class kernel { - ast_manager& m; - smt_params m_smtp; - smt::kernel m_kernel; - - public: - kernel(ast_manager& m): - m(m), - m_kernel(m, m_smtp) - { - m_smtp.m_model = true; - m_smtp.m_relevancy_lvl = 0; - m_smtp.m_case_split_strategy = CS_ACTIVITY_WITH_CACHE; + class kernel { + ast_manager& m; + smt_params m_smtp; + smt::kernel m_kernel; + + public: + kernel(ast_manager& m): + m(m), + m_kernel(m, m_smtp) + { + m_smtp.m_model = true; + m_smtp.m_relevancy_lvl = 0; + m_smtp.m_case_split_strategy = CS_ACTIVITY_WITH_CACHE; + } + + smt::kernel& k() { return m_kernel; } + smt::kernel const& k() const { return m_kernel; } + + void assert_expr(expr* e) { + m_kernel.assert_expr(e); + } + + void get_core(expr_ref_vector& core) { + unsigned sz = m_kernel.get_unsat_core_size(); + core.reset(); + for (unsigned i = 0; i < sz; ++i) { + core.push_back(m_kernel.get_unsat_core_expr(i)); } - - smt::kernel& k() { return m_kernel; } - smt::kernel const& k() const { return m_kernel; } - - void assert_expr(expr* e) { - m_kernel.assert_expr(e); - } - - void get_core(expr_ref_vector& core) { - unsigned sz = m_kernel.get_unsat_core_size(); - core.reset(); - for (unsigned i = 0; i < sz; ++i) { - core.push_back(m_kernel.get_unsat_core_expr(i)); - } - TRACE("qe", tout << "core: " << core << "\n"; - m_kernel.display(tout); - tout << "\n"; - ); - } - }; + TRACE("qe", tout << "core: " << core << "\n"; + m_kernel.display(tout); + tout << "\n"; + ); + } + }; class qsat : public tactic { @@ -1168,6 +1168,7 @@ namespace qe { pred_abs m_pred_abs; qe::mbp m_mbp; kernel m_kernel; + vector m_vars; imp(ast_manager& m): m(m), @@ -1180,14 +1181,36 @@ namespace qe { m_fmls.push_back(e); } - lbool check(svector const& is_max, func_decl_ref_vector const& vars, app* t) { + lbool check(svector const& is_max, app_ref_vector const& vars, app* t) { // Assume this is the only call to check. expr_ref_vector defs(m); + app_ref_vector free_vars(m), vars1(m); expr_ref fml = mk_and(m_fmls); + m_pred_abs.get_free_vars(fml, free_vars); m_pred_abs.abstract_atoms(fml, defs); fml = m_pred_abs.mk_abstract(fml); m_kernel.assert_expr(mk_and(defs)); m_kernel.assert_expr(fml); + obj_hashtable var_set; + for (unsigned i = 0; i < vars.size(); ++i) { + var_set.insert(vars[i]); + } + for (unsigned i = 0; i < free_vars.size(); ++i) { + app* v = free_vars[i].get(); + if (!var_set.contains(v)) { + vars1.push_back(v); + } + } + bool is_m = is_max[0]; + for (unsigned i = 0; i < vars.size(); ++i) { + if (is_m != is_max[i]) { + m_vars.push_back(vars1); + vars1.reset(); + is_m = is_max[i]; + } + vars1.push_back(vars[i]); + } + // TBD return l_undef; @@ -1212,7 +1235,7 @@ namespace qe { } } - lbool min_max_opt::check(svector const& is_max, func_decl_ref_vector const& vars, app* t) { + lbool min_max_opt::check(svector const& is_max, app_ref_vector const& vars, app* t) { return m_imp->check(is_max, vars, t); } diff --git a/src/qe/qsat.h b/src/qe/qsat.h index 91b370294..5c6b80a04 100644 --- a/src/qe/qsat.h +++ b/src/qe/qsat.h @@ -121,7 +121,7 @@ namespace qe { ~min_max_opt(); void add(expr* e); void add(expr_ref_vector const& fmls); - lbool check(svector const& is_max, func_decl_ref_vector const& vars, app* t); + lbool check(svector const& is_max, app_ref_vector const& vars, app* t); }; diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index cfc037a68..036a09bb6 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -91,6 +91,25 @@ bool proto_model::is_select_of_model_value(expr* e) const { has_interpretation(array_util(m_manager).get_as_array_func_decl(to_app(to_app(e)->get_arg(0)))); } +bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { + m_eval.set_model_completion(model_completion); + try { + m_eval(e, result); +#if 0 + std::cout << mk_pp(e, m_manager) << "\n===>\n" << result << "\n"; +#endif + return true; + } + catch (model_evaluator_exception & ex) { + (void)ex; + TRACE("model_evaluator", tout << ex.msg() << "\n";); + return false; + } +} + + + + /** \brief Evaluate the expression e in the current model, and store the result in \c result. It returns \c true if succeeded, and false otherwise. If the evaluation fails, @@ -101,18 +120,7 @@ bool proto_model::is_select_of_model_value(expr* e) const { declaration it will build one for it. Moreover, partial functions will also be completed. So, if model_completion == true, the evaluator never fails if it doesn't contain quantifiers. */ -bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { - m_eval.set_model_completion(model_completion); - try { - m_eval(e, result); - return true; - } - catch (model_evaluator_exception & ex) { - (void)ex; - TRACE("model_evaluator", tout << ex.msg() << "\n";); - return false; - } -} + /** \brief Replace uninterpreted constants occurring in fi->get_else() @@ -429,3 +437,245 @@ model * proto_model::mk_model() { return m; } + + +#if 0 + +#include"simplifier.h" +#include"basic_simplifier_plugin.h" + +// Auxiliary function for computing fi(args[0], ..., args[fi.get_arity() - 1]). +// The result is stored in result. +// Return true if succeeded, and false otherwise. +// It uses the simplifier s during the computation. +bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & result) { + bool actuals_are_values = true; + + if (fi.num_entries() != 0) { + for (unsigned i = 0; actuals_are_values && i < fi.get_arity(); i++) { + actuals_are_values = fi.m().is_value(args[i]); + } + } + + func_entry * entry = fi.get_entry(args); + if (entry != 0) { + result = entry->get_result(); + return true; + } + + TRACE("func_interp", tout << "failed to find entry for: "; + for(unsigned i = 0; i < fi.get_arity(); i++) + tout << mk_pp(args[i], fi.m()) << " "; + tout << "\nis partial: " << fi.is_partial() << "\n";); + + if (!fi.eval_else(args, result)) { + return false; + } + + if (actuals_are_values && fi.args_are_values()) { + // cheap case... we are done + return true; + } + + // build symbolic result... the actuals may be equal to the args of one of the entries. + basic_simplifier_plugin * bs = static_cast(s.get_plugin(fi.m().get_basic_family_id())); + for (unsigned k = 0; k < fi.num_entries(); k++) { + func_entry const * curr = fi.get_entry(k); + SASSERT(!curr->eq_args(fi.m(), fi.get_arity(), args)); + if (!actuals_are_values || !curr->args_are_values()) { + expr_ref_buffer eqs(fi.m()); + unsigned i = fi.get_arity(); + while (i > 0) { + --i; + expr_ref new_eq(fi.m()); + bs->mk_eq(curr->get_arg(i), args[i], new_eq); + eqs.push_back(new_eq); + } + SASSERT(eqs.size() == fi.get_arity()); + expr_ref new_cond(fi.m()); + bs->mk_and(eqs.size(), eqs.c_ptr(), new_cond); + bs->mk_ite(new_cond, curr->get_result(), result, result); + } + } + return true; +} + + +bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { + bool is_ok = true; + SASSERT(is_well_sorted(m_manager, e)); + TRACE("model_eval", tout << mk_pp(e, m_manager) << "\n"; + tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";); + + obj_map eval_cache; + expr_ref_vector trail(m_manager); + sbuffer, 128> todo; + ptr_buffer args; + expr * null = static_cast(0); + todo.push_back(std::make_pair(e, null)); + + simplifier m_simplifier(m_manager); + + expr * a; + expr * expanded_a; + while (!todo.empty()) { + std::pair & p = todo.back(); + a = p.first; + expanded_a = p.second; + if (expanded_a != 0) { + expr * r = 0; + eval_cache.find(expanded_a, r); + SASSERT(r != 0); + todo.pop_back(); + eval_cache.insert(a, r); + TRACE("model_eval", + tout << "orig:\n" << mk_pp(a, m_manager) << "\n"; + tout << "after beta reduction:\n" << mk_pp(expanded_a, m_manager) << "\n"; + tout << "new:\n" << mk_pp(r, m_manager) << "\n";); + } + else { + switch(a->get_kind()) { + case AST_APP: { + app * t = to_app(a); + bool visited = true; + args.reset(); + unsigned num_args = t->get_num_args(); + for (unsigned i = 0; i < num_args; ++i) { + expr * arg = 0; + if (!eval_cache.find(t->get_arg(i), arg)) { + visited = false; + todo.push_back(std::make_pair(t->get_arg(i), null)); + } + else { + args.push_back(arg); + } + } + if (!visited) { + continue; + } + SASSERT(args.size() == t->get_num_args()); + expr_ref new_t(m_manager); + func_decl * f = t->get_decl(); + + if (!has_interpretation(f)) { + // the model does not assign an interpretation to f. + SASSERT(new_t.get() == 0); + if (f->get_family_id() == null_family_id) { + if (model_completion) { + // create an interpretation for f. + new_t = mk_some_interp_for(f); + } + else { + TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";); + is_ok = false; + } + } + if (new_t.get() == 0) { + // t is interpreted or model completion is disabled. + m_simplifier.mk_app(f, num_args, args.c_ptr(), new_t); + TRACE("model_eval", tout << mk_pp(t, m_manager) << " -> " << new_t << "\n";); + trail.push_back(new_t); + if (!is_app(new_t) || to_app(new_t)->get_decl() != f || is_select_of_model_value(new_t)) { + // if the result is not of the form (f ...), then assume we must simplify it. + expr * new_new_t = 0; + if (!eval_cache.find(new_t.get(), new_new_t)) { + todo.back().second = new_t; + todo.push_back(std::make_pair(new_t, null)); + continue; + } + else { + new_t = new_new_t; + } + } + } + } + else { + // the model has an interpretaion for f. + if (num_args == 0) { + // t is a constant + new_t = get_const_interp(f); + } + else { + // t is a function application + SASSERT(new_t.get() == 0); + // try to use function graph first + func_interp * fi = get_func_interp(f); + SASSERT(fi->get_arity() == num_args); + expr_ref r1(m_manager); + // fi may be partial... + if (!::eval(*fi, m_simplifier, args.c_ptr(), r1)) { + SASSERT(fi->is_partial()); // fi->eval only fails when fi is partial. + if (model_completion) { + expr * r = get_some_value(f->get_range()); + fi->set_else(r); + SASSERT(!fi->is_partial()); + new_t = r; + } + else { + // f is an uninterpreted function, there is no need to use m_simplifier.mk_app + new_t = m_manager.mk_app(f, num_args, args.c_ptr()); + trail.push_back(new_t); + TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";); + is_ok = false; + } + } + else { + SASSERT(r1); + trail.push_back(r1); + TRACE("model_eval", tout << mk_pp(a, m_manager) << "\nevaluates to: " << r1 << "\n";); + expr * r2 = 0; + if (!eval_cache.find(r1.get(), r2)) { + todo.back().second = r1; + todo.push_back(std::make_pair(r1, null)); + continue; + } + else { + new_t = r2; + } + } + } + } + TRACE("model_eval", + tout << "orig:\n" << mk_pp(t, m_manager) << "\n"; + tout << "new:\n" << mk_pp(new_t, m_manager) << "\n";); + todo.pop_back(); + SASSERT(new_t.get() != 0); + eval_cache.insert(t, new_t); + break; + } + case AST_VAR: + SASSERT(a != 0); + eval_cache.insert(a, a); + todo.pop_back(); + break; + case AST_QUANTIFIER: + TRACE("model_eval", tout << "found quantifier\n" << mk_pp(a, m_manager) << "\n";); + is_ok = false; // evaluator does not handle quantifiers. + SASSERT(a != 0); + eval_cache.insert(a, a); + todo.pop_back(); + break; + default: + UNREACHABLE(); + break; + } + } + } + + if (!eval_cache.find(e, a)) { + TRACE("model_eval", tout << "FAILED e: " << mk_bounded_pp(e, m_manager) << "\n";); + UNREACHABLE(); + } + + result = a; + std::cout << mk_pp(e, m_manager) << "\n===>\n" << result << "\n"; + TRACE("model_eval", + ast_ll_pp(tout << "original: ", m_manager, e); + ast_ll_pp(tout << "evaluated: ", m_manager, a); + ast_ll_pp(tout << "reduced: ", m_manager, result.get()); + tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n"; + ); + SASSERT(is_well_sorted(m_manager, result.get())); + return is_ok; +} +#endif diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index 72e1f1bc2..8f209b96b 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -1308,7 +1308,7 @@ namespace smt { if (!gcd_test()) return FC_CONTINUE; - if (m_params.m_arith_euclidean_solver) + if (m_params.m_arith_euclidean_solver || (0 == (1 + m_branch_cut_counter) % 80)) apply_euclidean_solver(); if (get_context().inconsistent()) diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp index 13a790e93..f501ed75a 100644 --- a/src/tactic/smtlogics/quant_tactics.cpp +++ b/src/tactic/smtlogics/quant_tactics.cpp @@ -22,6 +22,7 @@ Revision History: #include"solve_eqs_tactic.h" #include"elim_uncnstr_tactic.h" #include"qe_tactic.h" +#include"qe_lite.h" #include"qsat.h" #include"nlqsat.h" #include"ctx_simplify_tactic.h" @@ -61,6 +62,7 @@ static tactic * mk_no_solve_eq_preprocessor(ast_manager & m) { tactic * mk_ufnia_tactic(ast_manager & m, params_ref const & p) { tactic * st = and_then(mk_no_solve_eq_preprocessor(m), + mk_qe_lite_tactic(m, p), mk_smt_tactic()); st->updt_params(p); return st;