From d3afdc957b384de058fcf6bc7eb05d3efbe2199f Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 21 Mar 2016 19:33:50 +0000 Subject: [PATCH 1/8] [CMake] Fix issue #522 Previously tracing could be disabled and was not enabled by default in a debug build. This isn't desirable but I had avoided fixing it because enabling tracing in debug mode would be confusing because ``ENABLE_TRACING`` could be set to off but tracing would be enabled anyway. I have resolved this by renaming the option from ``ENABLE_TRACING`` to ``ENABLE_TRACING_FOR_NON_DEBUG``. The semantics of the optiona are now that it will enable tracing in non-debug builds. I have also added code to ensure that tracing is always enabled in debug builds. Whilst I was here I also fixed how ``option()`` was being used. The default value and comment were in the wrong order. --- CMakeLists.txt | 8 +++++--- README-CMake.md | 2 +- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index d33f352e1..c3dec71d6 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -289,12 +289,14 @@ 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 indepdent 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. From 7bb085a565b38a450e5520143f4fc23e91327b88 Mon Sep 17 00:00:00 2001 From: Bobby Powers Date: Tue, 22 Mar 2016 10:42:00 -0400 Subject: [PATCH 2/8] build: allow overriding of 'ar' in mk_config This will still use 'ar' if AR isn't set in the environment, but lets us override the default archive tool at configure time. Just like CC and CXX, this doesn't apply to a ./configure for Windows. --- scripts/mk_util.py | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) 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) From fd6fe87c5d9cd059c33a847274aef42af552730b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 Mar 2016 15:41:21 -0700 Subject: [PATCH 3/8] enable qe-lite for UFNIA benchmarks Signed-off-by: Nikolaj Bjorner --- src/qe/qsat.cpp | 93 ++++++++++++++++---------- src/qe/qsat.h | 2 +- src/smt/theory_arith_int.h | 2 +- src/tactic/smtlogics/quant_tactics.cpp | 2 + 4 files changed, 62 insertions(+), 37 deletions(-) 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/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; From 5c2969c0f09f5f4c19a773d40de7fa328fd7cc46 Mon Sep 17 00:00:00 2001 From: Takeshi Abe Date: Wed, 23 Mar 2016 12:51:41 +0900 Subject: [PATCH 4/8] Fix typo --- examples/c/README | 2 +- examples/maxsat/README | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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. From 749e1a1fb186865ff4b6fdb31afbcc7d4329a918 Mon Sep 17 00:00:00 2001 From: Bohao Zhang Date: Wed, 23 Mar 2016 16:14:38 +0100 Subject: [PATCH 5/8] Clean up README mentioning C++ and Java. --- doc/README | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From ec681d7565fd5def93ce08b8de450041655a620d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Mar 2016 10:19:16 -0700 Subject: [PATCH 6/8] some of Arie's fixes Signed-off-by: Nikolaj Bjorner --- src/qe/qe_arrays.cpp | 2 +- src/qe/qe_mbp.cpp | 18 +- src/smt/proto_model/proto_model.cpp | 274 ++++++++++++++++++++++++++-- 3 files changed, 272 insertions(+), 22 deletions(-) diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp index 4f2ce81c5..88b0290d5 100644 --- a/src/qe/qe_arrays.cpp +++ b/src/qe/qe_arrays.cpp @@ -305,7 +305,7 @@ 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) { 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/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 From ee125b4fe3e33f0062ab525da3640038f89b6237 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 23 Mar 2016 19:05:21 -0400 Subject: [PATCH 7/8] extend model with the value of a fresh variable --- src/qe/qe_arrays.cpp | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp index 88b0290d5..162a4fb78 100644 --- a/src/qe/qe_arrays.cpp +++ b/src/qe/qe_arrays.cpp @@ -309,12 +309,19 @@ namespace qe { 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()); } @@ -398,6 +405,7 @@ namespace qe { // TBD chase definition of nested array. return l_undef; } + // AG: Shouldn't this be l_false return l_true; } }; From 4e7b6b6586ee6c223086ca81d0586b4d414f30fd Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 23 Mar 2016 19:20:27 -0400 Subject: [PATCH 8/8] proposed fix to compare --- src/qe/qe_arrays.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp index 162a4fb78..f8f44b6d9 100644 --- a/src/qe/qe_arrays.cpp +++ b/src/qe/qe_arrays.cpp @@ -397,16 +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; } - // AG: Shouldn't this be l_false - return l_true; + return l_undef; } };