diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj index 8f6e34517..9eb9eb660 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj +++ b/src/api/dotnet/Microsoft.Z3.csproj @@ -399,4 +399,4 @@ --> - \ No newline at end of file + diff --git a/src/api/ml/README-test-win b/src/api/ml/README-test-win index d9be0174b..0e8b73ccd 100644 --- a/src/api/ml/README-test-win +++ b/src/api/ml/README-test-win @@ -1,23 +1,23 @@ -This directory contains scripts to build the test application using -OCaml. You also need CamlIDL to be able to generate the OCaml API. - -- To download OCaml: - http://caml.inria.fr/ocaml/ - -- To download CamlIDL: - http://forge.ocamlcore.org/projects/camlidl/ - -- One must build the OCaml library before compiling the example. - Go to directory ../ocaml - -- Use 'build-test.cmd' to build the test application using the OCaml compiler. - -Remark: The OCaml and C compiler tool chains must be configured in your environment. -Running from the Visual Studio Command Prompt configures the Microsoft C compiler. - -- The script 'exec.cmd' adds the bin directory to the path. So, - test_mlapi.exe can find z3.dll. - - - - +This directory contains scripts to build the test application using +OCaml. You also need CamlIDL to be able to generate the OCaml API. + +- To download OCaml: + http://caml.inria.fr/ocaml/ + +- To download CamlIDL: + http://forge.ocamlcore.org/projects/camlidl/ + +- One must build the OCaml library before compiling the example. + Go to directory ../ocaml + +- Use 'build-test.cmd' to build the test application using the OCaml compiler. + +Remark: The OCaml and C compiler tool chains must be configured in your environment. +Running from the Visual Studio Command Prompt configures the Microsoft C compiler. + +- The script 'exec.cmd' adds the bin directory to the path. So, + test_mlapi.exe can find z3.dll. + + + + diff --git a/src/api/ml/README-win b/src/api/ml/README-win index 91d2faa4f..82ddc2652 100644 --- a/src/api/ml/README-win +++ b/src/api/ml/README-win @@ -1,23 +1,23 @@ -The OCaml API for Z3 was tested using OCaml 3.12.1. -You also need CamlIDL to be able to generate the OCaml API. - -- To download OCaml: - http://caml.inria.fr/ocaml/ - -- To download CamlIDL: - http://forge.ocamlcore.org/projects/camlidl/ - -- To build the OCaml API for Z3: - .\build-lib.cmd - -Remark: The OCaml and C compiler tool chains must be configured in your environment. -Running from the Visual Studio Command Prompt configures the Microsoft C compiler. - -Remark: Building the OCaml API copies some pathnames into files, -so the OCaml API must be recompiled if the Z3 library files are moved. - -See ..\examples\ocaml\build-test.cmd for an example of how to compile and link with Z3. - -Acknowledgements: -The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg. -Many thanks to them! +The OCaml API for Z3 was tested using OCaml 3.12.1. +You also need CamlIDL to be able to generate the OCaml API. + +- To download OCaml: + http://caml.inria.fr/ocaml/ + +- To download CamlIDL: + http://forge.ocamlcore.org/projects/camlidl/ + +- To build the OCaml API for Z3: + .\build-lib.cmd + +Remark: The OCaml and C compiler tool chains must be configured in your environment. +Running from the Visual Studio Command Prompt configures the Microsoft C compiler. + +Remark: Building the OCaml API copies some pathnames into files, +so the OCaml API must be recompiled if the Z3 library files are moved. + +See ..\examples\ocaml\build-test.cmd for an example of how to compile and link with Z3. + +Acknowledgements: +The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg. +Many thanks to them! diff --git a/src/api/ml/build-lib.cmd b/src/api/ml/build-lib.cmd index 93d667a34..7cf1bbcbd 100755 --- a/src/api/ml/build-lib.cmd +++ b/src/api/ml/build-lib.cmd @@ -1,3 +1,3 @@ -@echo off - -call .\compile_mlapi.cmd ..\include ..\bin ..\bin +@echo off + +call .\compile_mlapi.cmd ..\include ..\bin ..\bin diff --git a/src/api/ml/build-test.cmd b/src/api/ml/build-test.cmd index 7b80dc795..13a752dbb 100755 --- a/src/api/ml/build-test.cmd +++ b/src/api/ml/build-test.cmd @@ -1,19 +1,19 @@ -@echo off - -if not exist ..\..\ocaml\z3.cmxa ( - echo "YOU MUST BUILD OCAML API! Go to directory ..\ocaml" - goto :EOF -) - -REM ocaml (>= 3.11) calls the linker through flexlink -ocamlc -version >> ocaml_version -set /p OCAML_VERSION= = 3.11) calls the linker through flexlink +ocamlc -version >> ocaml_version +set /p OCAML_VERSION= -char const * poly_rewriter::g_ste_blowup_msg = "sum of monomials blowup"; - - -template -void poly_rewriter::updt_params(params_ref const & _p) { - poly_rewriter_params p(_p); - m_flat = p.flat(); - m_som = p.som(); - m_hoist_mul = p.hoist_mul(); - m_hoist_cmul = p.hoist_cmul(); - m_som_blowup = p.som_blowup(); -} - -template -void poly_rewriter::get_param_descrs(param_descrs & r) { - poly_rewriter_params::collect_param_descrs(r); -} - -template -expr * poly_rewriter::mk_add_app(unsigned num_args, expr * const * args) { - switch (num_args) { - case 0: return mk_numeral(numeral(0)); - case 1: return args[0]; - default: return m().mk_app(get_fid(), add_decl_kind(), num_args, args); - } -} - -// t = (^ x y) --> return x, and set k = y if k is an integer >= 1 -// Otherwise return t and set k = 1 -template -expr * poly_rewriter::get_power_body(expr * t, rational & k) { - if (!is_power(t)) { - k = rational(1); - return t; - } - if (is_numeral(to_app(t)->get_arg(1), k) && k.is_int() && k > rational(1)) { - return to_app(t)->get_arg(0); - } - k = rational(1); - return t; -} - -template -expr * poly_rewriter::mk_mul_app(unsigned num_args, expr * const * args) { - switch (num_args) { - case 0: - return mk_numeral(numeral(1)); - case 1: - return args[0]; - default: - if (use_power()) { - rational k_prev; - expr * prev = get_power_body(args[0], k_prev); - rational k; - ptr_buffer new_args; -#define PUSH_POWER() { \ - if (k_prev.is_one()) { \ - new_args.push_back(prev); \ - } \ - else { \ - expr * pargs[2] = { prev, mk_numeral(k_prev) }; \ - new_args.push_back(m().mk_app(get_fid(), power_decl_kind(), 2, pargs)); \ - } \ - } - - for (unsigned i = 1; i < num_args; i++) { - expr * arg = get_power_body(args[i], k); - if (arg == prev) { - k_prev += k; - } - else { - PUSH_POWER(); - prev = arg; - k_prev = k; - } - } - PUSH_POWER(); - SASSERT(new_args.size() > 0); - if (new_args.size() == 1) { - return new_args[0]; - } - else { - return m().mk_app(get_fid(), mul_decl_kind(), new_args.size(), new_args.c_ptr()); - } - } - else { - return m().mk_app(get_fid(), mul_decl_kind(), num_args, args); - } - } -} - -template -expr * poly_rewriter::mk_mul_app(numeral const & c, expr * arg) { - if (c.is_one()) { - return arg; - } - else { - expr * new_args[2] = { mk_numeral(c), arg }; - return mk_mul_app(2, new_args); - } -} - -template -br_status poly_rewriter::mk_flat_mul_core(unsigned num_args, expr * const * args, expr_ref & result) { - SASSERT(num_args >= 2); - // only try to apply flattening if it is not already in one of the flat monomial forms - // - (* c x) - // - (* c (* x_1 ... x_n)) - if (num_args != 2 || !is_numeral(args[0]) || (is_mul(args[1]) && is_numeral(to_app(args[1])->get_arg(0)))) { - unsigned i; - for (i = 0; i < num_args; i++) { - if (is_mul(args[i])) - break; - } - if (i < num_args) { - // input has nested monomials. - ptr_buffer flat_args; - // we need the todo buffer to handle: (* (* c (* x_1 ... x_n)) (* d (* y_1 ... y_n))) - ptr_buffer todo; - flat_args.append(i, args); - for (unsigned j = i; j < num_args; j++) { - if (is_mul(args[j])) { - todo.push_back(args[j]); - while (!todo.empty()) { - expr * curr = todo.back(); - todo.pop_back(); - if (is_mul(curr)) { - unsigned k = to_app(curr)->get_num_args(); - while (k > 0) { - --k; - todo.push_back(to_app(curr)->get_arg(k)); - } - } - else { - flat_args.push_back(curr); - } - } - } - else { - flat_args.push_back(args[j]); - } - } - TRACE("poly_rewriter", - tout << "flat mul:\n"; - for (unsigned i = 0; i < num_args; i++) tout << mk_bounded_pp(args[i], m()) << "\n"; - tout << "---->\n"; - for (unsigned i = 0; i < flat_args.size(); i++) tout << mk_bounded_pp(flat_args[i], m()) << "\n";); - br_status st = mk_nflat_mul_core(flat_args.size(), flat_args.c_ptr(), result); - if (st == BR_FAILED) { - result = mk_mul_app(flat_args.size(), flat_args.c_ptr()); - return BR_DONE; - } - return st; - } - } - return mk_nflat_mul_core(num_args, args, result); -} - - -template -struct poly_rewriter::mon_pw_lt { - poly_rewriter & m_owner; - mon_pw_lt(poly_rewriter & o):m_owner(o) {} - - bool operator()(expr * n1, expr * n2) const { - rational k; - return lt(m_owner.get_power_body(n1, k), - m_owner.get_power_body(n2, k)); - } -}; - - -template -br_status poly_rewriter::mk_nflat_mul_core(unsigned num_args, expr * const * args, expr_ref & result) { - SASSERT(num_args >= 2); - // cheap case - numeral a; - if (num_args == 2 && is_numeral(args[0], a) && !a.is_one() && !a.is_zero() && - (is_var(args[1]) || to_app(args[1])->get_decl()->get_family_id() != get_fid())) - return BR_FAILED; - numeral c(1); - unsigned num_coeffs = 0; - unsigned num_add = 0; - expr * var = 0; - for (unsigned i = 0; i < num_args; i++) { - expr * arg = args[i]; - if (is_numeral(arg, a)) { - num_coeffs++; - c *= a; - } - else { - var = arg; - if (is_add(arg)) - num_add++; - } - } - - normalize(c); - // (* c_1 ... c_n) --> c_1*...*c_n - if (num_coeffs == num_args) { - result = mk_numeral(c); - return BR_DONE; - } - - // (* s ... 0 ... r) --> 0 - if (c.is_zero()) { - result = mk_numeral(c); - return BR_DONE; - } - - if (num_coeffs == num_args - 1) { - SASSERT(var != 0); - // (* c_1 ... c_n x) --> x if c_1*...*c_n == 1 - if (c.is_one()) { - result = var; - return BR_DONE; - } - - numeral c_prime; - if (is_mul(var)) { - // apply basic simplification even when flattening is not enabled. - // (* c1 (* c2 x)) --> (* c1*c2 x) - if (to_app(var)->get_num_args() == 2 && is_numeral(to_app(var)->get_arg(0), c_prime)) { - c *= c_prime; - normalize(c); - result = mk_mul_app(c, to_app(var)->get_arg(1)); - return BR_REWRITE1; - } - else { - // var is a power-product - return BR_FAILED; - } - } - - if (num_add == 0 || m_hoist_cmul) { - SASSERT(!is_add(var) || m_hoist_cmul); - if (num_args == 2 && args[1] == var) { - DEBUG_CODE({ - numeral c_prime; - SASSERT(is_numeral(args[0], c_prime) && c == c_prime); - }); - // it is already simplified - return BR_FAILED; - } - - // (* c_1 ... c_n x) --> (* c_1*...*c_n x) - result = mk_mul_app(c, var); - return BR_DONE; - } - else { - SASSERT(is_add(var)); - // (* c_1 ... c_n (+ t_1 ... t_m)) --> (+ (* c_1*...*c_n t_1) ... (* c_1*...*c_n t_m)) - ptr_buffer new_add_args; - unsigned num = to_app(var)->get_num_args(); - for (unsigned i = 0; i < num; i++) { - new_add_args.push_back(mk_mul_app(c, to_app(var)->get_arg(i))); - } - result = mk_add_app(new_add_args.size(), new_add_args.c_ptr()); - TRACE("mul_bug", tout << "result: " << mk_bounded_pp(result, m(),5) << "\n";); - return BR_REWRITE2; - } - } - - SASSERT(num_coeffs <= num_args - 2); - - if (!m_som || num_add == 0) { - ptr_buffer new_args; - expr * prev = 0; - bool ordered = true; - for (unsigned i = 0; i < num_args; i++) { - expr * curr = args[i]; - if (is_numeral(curr)) - continue; - if (prev != 0 && lt(curr, prev)) - ordered = false; - new_args.push_back(curr); - prev = curr; - } - TRACE("poly_rewriter", - for (unsigned i = 0; i < new_args.size(); i++) { - if (i > 0) - tout << (lt(new_args[i-1], new_args[i]) ? " < " : " !< "); - tout << mk_ismt2_pp(new_args[i], m()); - } - tout << "\nordered: " << ordered << "\n";); - if (ordered && num_coeffs == 0 && !use_power()) - return BR_FAILED; - if (!ordered) { - if (use_power()) - std::sort(new_args.begin(), new_args.end(), mon_pw_lt(*this)); - else - std::sort(new_args.begin(), new_args.end(), ast_to_lt()); - TRACE("poly_rewriter", - tout << "after sorting:\n"; - for (unsigned i = 0; i < new_args.size(); i++) { - if (i > 0) - tout << (lt(new_args[i-1], new_args[i]) ? " < " : " !< "); - tout << mk_ismt2_pp(new_args[i], m()); - } - tout << "\n";); - } - SASSERT(new_args.size() >= 2); - result = mk_mul_app(new_args.size(), new_args.c_ptr()); - result = mk_mul_app(c, result); - TRACE("poly_rewriter", tout << "mk_nflat_mul_core result:\n" << mk_ismt2_pp(result, m()) << "\n";); - return BR_DONE; - } - - SASSERT(m_som && num_add > 0); - - sbuffer szs; - sbuffer it; - sbuffer sums; - for (unsigned i = 0; i < num_args; i ++) { - it.push_back(0); - expr * arg = args[i]; - if (is_add(arg)) { - sums.push_back(const_cast(to_app(arg)->get_args())); - szs.push_back(to_app(arg)->get_num_args()); - } - else { - sums.push_back(const_cast(args + i)); - szs.push_back(1); - SASSERT(sums.back()[0] == arg); - } - } - expr_ref_buffer sum(m()); // must be ref_buffer because we may throw an exception - ptr_buffer m_args; - TRACE("som", tout << "starting som...\n";); - do { - TRACE("som", for (unsigned i = 0; i < it.size(); i++) tout << it[i] << " "; - tout << "\n";); - if (sum.size() > m_som_blowup) - throw rewriter_exception(g_ste_blowup_msg); - m_args.reset(); - for (unsigned i = 0; i < num_args; i++) { - expr * const * v = sums[i]; - expr * arg = v[it[i]]; - m_args.push_back(arg); - } - sum.push_back(mk_mul_app(m_args.size(), m_args.c_ptr())); - } - while (product_iterator_next(szs.size(), szs.c_ptr(), it.c_ptr())); - result = mk_add_app(sum.size(), sum.c_ptr()); - return BR_REWRITE2; -} - -template -br_status poly_rewriter::mk_flat_add_core(unsigned num_args, expr * const * args, expr_ref & result) { - unsigned i; - for (i = 0; i < num_args; i++) { - if (is_add(args[i])) - break; - } - if (i < num_args) { - // has nested ADDs - ptr_buffer flat_args; - flat_args.append(i, args); - for (; i < num_args; i++) { - expr * arg = args[i]; - // Remark: all rewrites are depth 1. - if (is_add(arg)) { - unsigned num = to_app(arg)->get_num_args(); - for (unsigned j = 0; j < num; j++) - flat_args.push_back(to_app(arg)->get_arg(j)); - } - else { - flat_args.push_back(arg); - } - } - br_status st = mk_nflat_add_core(flat_args.size(), flat_args.c_ptr(), result); - if (st == BR_FAILED) { - result = mk_add_app(flat_args.size(), flat_args.c_ptr()); - return BR_DONE; - } - return st; - } - return mk_nflat_add_core(num_args, args, result); -} - -template -inline expr * poly_rewriter::get_power_product(expr * t) { - if (is_mul(t) && to_app(t)->get_num_args() == 2 && is_numeral(to_app(t)->get_arg(0))) - return to_app(t)->get_arg(1); - return t; -} - -template -inline expr * poly_rewriter::get_power_product(expr * t, numeral & a) { - if (is_mul(t) && to_app(t)->get_num_args() == 2 && is_numeral(to_app(t)->get_arg(0), a)) - return to_app(t)->get_arg(1); - a = numeral(1); - return t; -} - -template -bool poly_rewriter::is_mul(expr * t, numeral & c, expr * & pp) { - if (!is_mul(t) || to_app(t)->get_num_args() != 2) - return false; - if (!is_numeral(to_app(t)->get_arg(0), c)) - return false; - pp = to_app(t)->get_arg(1); - return true; -} - -template -struct poly_rewriter::hoist_cmul_lt { - poly_rewriter & m_r; - hoist_cmul_lt(poly_rewriter & r):m_r(r) {} - - bool operator()(expr * t1, expr * t2) const { - expr * pp1, * pp2; - numeral c1, c2; - bool is_mul1 = m_r.is_mul(t1, c1, pp1); - bool is_mul2 = m_r.is_mul(t2, c2, pp2); - if (!is_mul1 && is_mul2) - return true; - if (is_mul1 && !is_mul2) - return false; - if (!is_mul1 && !is_mul2) - return t1->get_id() < t2->get_id(); - if (c1 < c2) - return true; - if (c1 > c2) - return false; - return pp1->get_id() < pp2->get_id(); - } -}; - -template -void poly_rewriter::hoist_cmul(expr_ref_buffer & args) { - unsigned sz = args.size(); - std::sort(args.c_ptr(), args.c_ptr() + sz, hoist_cmul_lt(*this)); - numeral c, c_prime; - ptr_buffer pps; - expr * pp, * pp_prime; - unsigned j = 0; - unsigned i = 0; - while (i < sz) { - expr * mon = args[i]; - if (is_mul(mon, c, pp) && i < sz - 1) { - expr * mon_prime = args[i+1]; - if (is_mul(mon_prime, c_prime, pp_prime) && c == c_prime) { - // found target - pps.reset(); - pps.push_back(pp); - pps.push_back(pp_prime); - i += 2; - while (i < sz && is_mul(args[i], c_prime, pp_prime) && c == c_prime) { - pps.push_back(pp_prime); - i++; - } - SASSERT(is_numeral(to_app(mon)->get_arg(0), c_prime) && c == c_prime); - expr * mul_args[2] = { to_app(mon)->get_arg(0), mk_add_app(pps.size(), pps.c_ptr()) }; - args.set(j, mk_mul_app(2, mul_args)); - j++; - continue; - } - } - args.set(j, mon); - j++; - i++; - } - args.resize(j); -} - -template -br_status poly_rewriter::mk_nflat_add_core(unsigned num_args, expr * const * args, expr_ref & result) { - SASSERT(num_args >= 2); - numeral c; - unsigned num_coeffs = 0; - numeral a; - expr_fast_mark1 visited; // visited.is_marked(power_product) if the power_product occurs in args - expr_fast_mark2 multiple; // multiple.is_marked(power_product) if power_product occurs more than once - bool has_multiple = false; - expr * prev = 0; - bool ordered = true; - for (unsigned i = 0; i < num_args; i++) { - expr * arg = args[i]; - if (is_numeral(arg, a)) { - num_coeffs++; - c += a; - } - else { - // arg is not a numeral - if (m_sort_sums && ordered) { - if (prev != 0 && lt(arg, prev)) - ordered = false; - prev = arg; - } - } - - arg = get_power_product(arg); - if (visited.is_marked(arg)) { - multiple.mark(arg); - has_multiple = true; - } - else { - visited.mark(arg); - } - } - normalize(c); - SASSERT(m_sort_sums || ordered); - TRACE("sort_sums", - tout << "ordered: " << ordered << "\n"; - for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";); - - if (has_multiple) { - // expensive case - buffer coeffs; - m_expr2pos.reset(); - // compute the coefficient of power products that occur multiple times. - for (unsigned i = 0; i < num_args; i++) { - expr * arg = args[i]; - if (is_numeral(arg)) - continue; - expr * pp = get_power_product(arg, a); - if (!multiple.is_marked(pp)) - continue; - unsigned pos; - if (m_expr2pos.find(pp, pos)) { - coeffs[pos] += a; - } - else { - m_expr2pos.insert(pp, coeffs.size()); - coeffs.push_back(a); - } - } - expr_ref_buffer new_args(m()); - if (!c.is_zero()) { - new_args.push_back(mk_numeral(c)); - } - // copy power products with non zero coefficients to new_args - visited.reset(); - for (unsigned i = 0; i < num_args; i++) { - expr * arg = args[i]; - if (is_numeral(arg)) - continue; - expr * pp = get_power_product(arg); - if (!multiple.is_marked(pp)) { - new_args.push_back(arg); - } - else if (!visited.is_marked(pp)) { - visited.mark(pp); - unsigned pos = UINT_MAX; - m_expr2pos.find(pp, pos); - SASSERT(pos != UINT_MAX); - a = coeffs[pos]; - normalize(a); - if (!a.is_zero()) - new_args.push_back(mk_mul_app(a, pp)); - } - } - if (m_hoist_cmul) { - hoist_cmul(new_args); - } - else if (m_sort_sums) { - TRACE("sort_sums_bug", tout << "new_args.size(): " << new_args.size() << "\n";); - if (c.is_zero()) - std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), ast_to_lt()); - else - std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size(), ast_to_lt()); - } - result = mk_add_app(new_args.size(), new_args.c_ptr()); - if (hoist_multiplication(result)) { - return BR_REWRITE_FULL; - } - return BR_DONE; - } - else { - SASSERT(!has_multiple); - if (ordered && !m_hoist_mul && !m_hoist_cmul) { - if (num_coeffs == 0) - return BR_FAILED; - if (num_coeffs == 1 && is_numeral(args[0], a) && !a.is_zero()) - return BR_FAILED; - } - expr_ref_buffer new_args(m()); - if (!c.is_zero()) - new_args.push_back(mk_numeral(c)); - for (unsigned i = 0; i < num_args; i++) { - expr * arg = args[i]; - if (is_numeral(arg)) - continue; - new_args.push_back(arg); - } - if (m_hoist_cmul) { - hoist_cmul(new_args); - } - else if (!ordered) { - if (c.is_zero()) - std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), ast_to_lt()); - else - std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size(), ast_to_lt()); - } - result = mk_add_app(new_args.size(), new_args.c_ptr()); - if (hoist_multiplication(result)) { - return BR_REWRITE_FULL; - } - return BR_DONE; - } -} - - -template -br_status poly_rewriter::mk_uminus(expr * arg, expr_ref & result) { - numeral a; - set_curr_sort(m().get_sort(arg)); - if (is_numeral(arg, a)) { - a.neg(); - normalize(a); - result = mk_numeral(a); - return BR_DONE; - } - else { - result = mk_mul_app(numeral(-1), arg); - return BR_REWRITE1; - } -} - -template -br_status poly_rewriter::mk_sub(unsigned num_args, expr * const * args, expr_ref & result) { - SASSERT(num_args > 0); - if (num_args == 1) { - result = args[0]; - return BR_DONE; - } - set_curr_sort(m().get_sort(args[0])); - expr * minus_one = mk_numeral(numeral(-1)); - ptr_buffer new_args; - new_args.push_back(args[0]); - for (unsigned i = 1; i < num_args; i++) { - expr * aux_args[2] = { minus_one, args[i] }; - new_args.push_back(mk_mul_app(2, aux_args)); - } - result = mk_add_app(new_args.size(), new_args.c_ptr()); - return BR_REWRITE2; -} - -/** - \brief Cancel/Combine monomials that occur is the left and right hand sides. - - \remark If move = true, then all non-constant monomials are moved to the left-hand-side. -*/ -template -br_status poly_rewriter::cancel_monomials(expr * lhs, expr * rhs, bool move, expr_ref & lhs_result, expr_ref & rhs_result) { - set_curr_sort(m().get_sort(lhs)); - unsigned lhs_sz; - expr * const * lhs_monomials = get_monomials(lhs, lhs_sz); - unsigned rhs_sz; - expr * const * rhs_monomials = get_monomials(rhs, rhs_sz); - - expr_fast_mark1 visited; // visited.is_marked(power_product) if the power_product occurs in lhs or rhs - expr_fast_mark2 multiple; // multiple.is_marked(power_product) if power_product occurs more than once - bool has_multiple = false; - - numeral c(0); - numeral a; - unsigned num_coeffs = 0; - - for (unsigned i = 0; i < lhs_sz; i++) { - expr * arg = lhs_monomials[i]; - if (is_numeral(arg, a)) { - c += a; - num_coeffs++; - } - else { - visited.mark(get_power_product(arg)); - } - } - - if (move && num_coeffs == 0 && is_numeral(rhs)) - return BR_FAILED; - - for (unsigned i = 0; i < rhs_sz; i++) { - expr * arg = rhs_monomials[i]; - if (is_numeral(arg, a)) { - c -= a; - num_coeffs++; - } - else { - expr * pp = get_power_product(arg); - if (visited.is_marked(pp)) { - multiple.mark(pp); - has_multiple = true; - } - } - } - - normalize(c); - - if (!has_multiple && num_coeffs <= 1) { - if (move) { - if (is_numeral(rhs)) - return BR_FAILED; - } - else { - if (num_coeffs == 0 || is_numeral(rhs)) - return BR_FAILED; - } - } - - buffer coeffs; - m_expr2pos.reset(); - for (unsigned i = 0; i < lhs_sz; i++) { - expr * arg = lhs_monomials[i]; - if (is_numeral(arg)) - continue; - expr * pp = get_power_product(arg, a); - if (!multiple.is_marked(pp)) - continue; - unsigned pos; - if (m_expr2pos.find(pp, pos)) { - coeffs[pos] += a; - } - else { - m_expr2pos.insert(pp, coeffs.size()); - coeffs.push_back(a); - } - } - - for (unsigned i = 0; i < rhs_sz; i++) { - expr * arg = rhs_monomials[i]; - if (is_numeral(arg)) - continue; - expr * pp = get_power_product(arg, a); - if (!multiple.is_marked(pp)) - continue; - unsigned pos = UINT_MAX; - m_expr2pos.find(pp, pos); - SASSERT(pos != UINT_MAX); - coeffs[pos] -= a; - } - - - ptr_buffer new_lhs_monomials; - new_lhs_monomials.push_back(0); // save space for coefficient if needed - // copy power products with non zero coefficients to new_lhs_monomials - visited.reset(); - for (unsigned i = 0; i < lhs_sz; i++) { - expr * arg = lhs_monomials[i]; - if (is_numeral(arg)) - continue; - expr * pp = get_power_product(arg); - if (!multiple.is_marked(pp)) { - new_lhs_monomials.push_back(arg); - } - else if (!visited.is_marked(pp)) { - visited.mark(pp); - unsigned pos = UINT_MAX; - m_expr2pos.find(pp, pos); - SASSERT(pos != UINT_MAX); - a = coeffs[pos]; - if (!a.is_zero()) - new_lhs_monomials.push_back(mk_mul_app(a, pp)); - } - } - - ptr_buffer new_rhs_monomials; - new_rhs_monomials.push_back(0); // save space for coefficient if needed - for (unsigned i = 0; i < rhs_sz; i++) { - expr * arg = rhs_monomials[i]; - if (is_numeral(arg)) - continue; - expr * pp = get_power_product(arg, a); - if (!multiple.is_marked(pp)) { - if (move) { - if (!a.is_zero()) { - if (a.is_minus_one()) { - new_lhs_monomials.push_back(pp); - } - else { - a.neg(); - SASSERT(!a.is_one()); - expr * args[2] = { mk_numeral(a), pp }; - new_lhs_monomials.push_back(mk_mul_app(2, args)); - } - } - } - else { - new_rhs_monomials.push_back(arg); - } - } - } - - bool c_at_rhs = false; - if (move) { - if (m_sort_sums) { - // + 1 to skip coefficient - std::sort(new_lhs_monomials.begin() + 1, new_lhs_monomials.end(), ast_to_lt()); - } - c_at_rhs = true; - } - else if (new_rhs_monomials.size() == 1) { // rhs is empty - c_at_rhs = true; - } - else if (new_lhs_monomials.size() > 1) { - c_at_rhs = true; - } - - if (c_at_rhs) { - c.neg(); - normalize(c); - new_rhs_monomials[0] = mk_numeral(c); - lhs_result = mk_add_app(new_lhs_monomials.size() - 1, new_lhs_monomials.c_ptr() + 1); - rhs_result = mk_add_app(new_rhs_monomials.size(), new_rhs_monomials.c_ptr()); - } - else { - new_lhs_monomials[0] = mk_numeral(c); - lhs_result = mk_add_app(new_lhs_monomials.size(), new_lhs_monomials.c_ptr()); - rhs_result = mk_add_app(new_rhs_monomials.size() - 1, new_rhs_monomials.c_ptr() + 1); - } - return BR_DONE; -} - -#define TO_BUFFER(_tester_, _buffer_, _e_) \ - _buffer_.push_back(_e_); \ - for (unsigned _i = 0; _i < _buffer_.size(); ) { \ - expr* _e = _buffer_[_i]; \ - if (_tester_(_e)) { \ - app* a = to_app(_e); \ - _buffer_[_i] = a->get_arg(0); \ - for (unsigned _j = 1; _j < a->get_num_args(); ++_j) { \ - _buffer_.push_back(a->get_arg(_j)); \ - } \ - } \ - else { \ - ++_i; \ - } \ - } \ - -template -bool poly_rewriter::hoist_multiplication(expr_ref& som) { - if (!m_hoist_mul) { - return false; - } - ptr_buffer adds, muls; - TO_BUFFER(is_add, adds, som); - buffer valid(adds.size(), true); - obj_map mul_map; - unsigned j; - bool change = false; - for (unsigned k = 0; k < adds.size(); ++k) { - expr* e = adds[k]; - muls.reset(); - TO_BUFFER(is_mul, muls, e); - for (unsigned i = 0; i < muls.size(); ++i) { - e = muls[i]; - if (is_numeral(e)) { - continue; - } - if (mul_map.find(e, j) && valid[j] && j != k) { - m_curr_sort = m().get_sort(adds[k]); - adds[j] = merge_muls(adds[j], adds[k]); - adds[k] = mk_numeral(rational(0)); - valid[j] = false; - valid[k] = false; - change = true; - break; - } - else { - mul_map.insert(e, k); - } - } - } - if (!change) { - return false; - } - - som = mk_add_app(adds.size(), adds.c_ptr()); - - - return true; -} - -template -expr* poly_rewriter::merge_muls(expr* x, expr* y) { - ptr_buffer m1, m2; - TO_BUFFER(is_mul, m1, x); - TO_BUFFER(is_mul, m2, y); - unsigned k = 0; - for (unsigned i = 0; i < m1.size(); ++i) { - x = m1[i]; - bool found = false; - unsigned j; - for (j = k; j < m2.size(); ++j) { - found = m2[j] == x; - if (found) break; - } - if (found) { - std::swap(m1[i],m1[k]); - std::swap(m2[j],m2[k]); - ++k; - } - } - m_curr_sort = m().get_sort(x); - SASSERT(k > 0); - SASSERT(m1.size() >= k); - SASSERT(m2.size() >= k); - expr* args[2] = { mk_mul_app(m1.size()-k, m1.c_ptr()+k), - mk_mul_app(m2.size()-k, m2.c_ptr()+k) }; - if (k == m1.size()) { - m1.push_back(0); - } - m1[k] = mk_add_app(2, args); - return mk_mul_app(k+1, m1.c_ptr()); -} +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + poly_rewriter_def.h + +Abstract: + + Basic rewriting rules for Polynomials. + +Author: + + Leonardo (leonardo) 2011-04-08 + +Notes: + +--*/ +#include"poly_rewriter.h" +#include"poly_rewriter_params.hpp" +#include"ast_lt.h" +#include"ast_ll_pp.h" +#include"ast_smt2_pp.h" + +template +char const * poly_rewriter::g_ste_blowup_msg = "sum of monomials blowup"; + + +template +void poly_rewriter::updt_params(params_ref const & _p) { + poly_rewriter_params p(_p); + m_flat = p.flat(); + m_som = p.som(); + m_hoist_mul = p.hoist_mul(); + m_hoist_cmul = p.hoist_cmul(); + m_som_blowup = p.som_blowup(); +} + +template +void poly_rewriter::get_param_descrs(param_descrs & r) { + poly_rewriter_params::collect_param_descrs(r); +} + +template +expr * poly_rewriter::mk_add_app(unsigned num_args, expr * const * args) { + switch (num_args) { + case 0: return mk_numeral(numeral(0)); + case 1: return args[0]; + default: return m().mk_app(get_fid(), add_decl_kind(), num_args, args); + } +} + +// t = (^ x y) --> return x, and set k = y if k is an integer >= 1 +// Otherwise return t and set k = 1 +template +expr * poly_rewriter::get_power_body(expr * t, rational & k) { + if (!is_power(t)) { + k = rational(1); + return t; + } + if (is_numeral(to_app(t)->get_arg(1), k) && k.is_int() && k > rational(1)) { + return to_app(t)->get_arg(0); + } + k = rational(1); + return t; +} + +template +expr * poly_rewriter::mk_mul_app(unsigned num_args, expr * const * args) { + switch (num_args) { + case 0: + return mk_numeral(numeral(1)); + case 1: + return args[0]; + default: + if (use_power()) { + rational k_prev; + expr * prev = get_power_body(args[0], k_prev); + rational k; + ptr_buffer new_args; +#define PUSH_POWER() { \ + if (k_prev.is_one()) { \ + new_args.push_back(prev); \ + } \ + else { \ + expr * pargs[2] = { prev, mk_numeral(k_prev) }; \ + new_args.push_back(m().mk_app(get_fid(), power_decl_kind(), 2, pargs)); \ + } \ + } + + for (unsigned i = 1; i < num_args; i++) { + expr * arg = get_power_body(args[i], k); + if (arg == prev) { + k_prev += k; + } + else { + PUSH_POWER(); + prev = arg; + k_prev = k; + } + } + PUSH_POWER(); + SASSERT(new_args.size() > 0); + if (new_args.size() == 1) { + return new_args[0]; + } + else { + return m().mk_app(get_fid(), mul_decl_kind(), new_args.size(), new_args.c_ptr()); + } + } + else { + return m().mk_app(get_fid(), mul_decl_kind(), num_args, args); + } + } +} + +template +expr * poly_rewriter::mk_mul_app(numeral const & c, expr * arg) { + if (c.is_one()) { + return arg; + } + else { + expr * new_args[2] = { mk_numeral(c), arg }; + return mk_mul_app(2, new_args); + } +} + +template +br_status poly_rewriter::mk_flat_mul_core(unsigned num_args, expr * const * args, expr_ref & result) { + SASSERT(num_args >= 2); + // only try to apply flattening if it is not already in one of the flat monomial forms + // - (* c x) + // - (* c (* x_1 ... x_n)) + if (num_args != 2 || !is_numeral(args[0]) || (is_mul(args[1]) && is_numeral(to_app(args[1])->get_arg(0)))) { + unsigned i; + for (i = 0; i < num_args; i++) { + if (is_mul(args[i])) + break; + } + if (i < num_args) { + // input has nested monomials. + ptr_buffer flat_args; + // we need the todo buffer to handle: (* (* c (* x_1 ... x_n)) (* d (* y_1 ... y_n))) + ptr_buffer todo; + flat_args.append(i, args); + for (unsigned j = i; j < num_args; j++) { + if (is_mul(args[j])) { + todo.push_back(args[j]); + while (!todo.empty()) { + expr * curr = todo.back(); + todo.pop_back(); + if (is_mul(curr)) { + unsigned k = to_app(curr)->get_num_args(); + while (k > 0) { + --k; + todo.push_back(to_app(curr)->get_arg(k)); + } + } + else { + flat_args.push_back(curr); + } + } + } + else { + flat_args.push_back(args[j]); + } + } + TRACE("poly_rewriter", + tout << "flat mul:\n"; + for (unsigned i = 0; i < num_args; i++) tout << mk_bounded_pp(args[i], m()) << "\n"; + tout << "---->\n"; + for (unsigned i = 0; i < flat_args.size(); i++) tout << mk_bounded_pp(flat_args[i], m()) << "\n";); + br_status st = mk_nflat_mul_core(flat_args.size(), flat_args.c_ptr(), result); + if (st == BR_FAILED) { + result = mk_mul_app(flat_args.size(), flat_args.c_ptr()); + return BR_DONE; + } + return st; + } + } + return mk_nflat_mul_core(num_args, args, result); +} + + +template +struct poly_rewriter::mon_pw_lt { + poly_rewriter & m_owner; + mon_pw_lt(poly_rewriter & o):m_owner(o) {} + + bool operator()(expr * n1, expr * n2) const { + rational k; + return lt(m_owner.get_power_body(n1, k), + m_owner.get_power_body(n2, k)); + } +}; + + +template +br_status poly_rewriter::mk_nflat_mul_core(unsigned num_args, expr * const * args, expr_ref & result) { + SASSERT(num_args >= 2); + // cheap case + numeral a; + if (num_args == 2 && is_numeral(args[0], a) && !a.is_one() && !a.is_zero() && + (is_var(args[1]) || to_app(args[1])->get_decl()->get_family_id() != get_fid())) + return BR_FAILED; + numeral c(1); + unsigned num_coeffs = 0; + unsigned num_add = 0; + expr * var = 0; + for (unsigned i = 0; i < num_args; i++) { + expr * arg = args[i]; + if (is_numeral(arg, a)) { + num_coeffs++; + c *= a; + } + else { + var = arg; + if (is_add(arg)) + num_add++; + } + } + + normalize(c); + // (* c_1 ... c_n) --> c_1*...*c_n + if (num_coeffs == num_args) { + result = mk_numeral(c); + return BR_DONE; + } + + // (* s ... 0 ... r) --> 0 + if (c.is_zero()) { + result = mk_numeral(c); + return BR_DONE; + } + + if (num_coeffs == num_args - 1) { + SASSERT(var != 0); + // (* c_1 ... c_n x) --> x if c_1*...*c_n == 1 + if (c.is_one()) { + result = var; + return BR_DONE; + } + + numeral c_prime; + if (is_mul(var)) { + // apply basic simplification even when flattening is not enabled. + // (* c1 (* c2 x)) --> (* c1*c2 x) + if (to_app(var)->get_num_args() == 2 && is_numeral(to_app(var)->get_arg(0), c_prime)) { + c *= c_prime; + normalize(c); + result = mk_mul_app(c, to_app(var)->get_arg(1)); + return BR_REWRITE1; + } + else { + // var is a power-product + return BR_FAILED; + } + } + + if (num_add == 0 || m_hoist_cmul) { + SASSERT(!is_add(var) || m_hoist_cmul); + if (num_args == 2 && args[1] == var) { + DEBUG_CODE({ + numeral c_prime; + SASSERT(is_numeral(args[0], c_prime) && c == c_prime); + }); + // it is already simplified + return BR_FAILED; + } + + // (* c_1 ... c_n x) --> (* c_1*...*c_n x) + result = mk_mul_app(c, var); + return BR_DONE; + } + else { + SASSERT(is_add(var)); + // (* c_1 ... c_n (+ t_1 ... t_m)) --> (+ (* c_1*...*c_n t_1) ... (* c_1*...*c_n t_m)) + ptr_buffer new_add_args; + unsigned num = to_app(var)->get_num_args(); + for (unsigned i = 0; i < num; i++) { + new_add_args.push_back(mk_mul_app(c, to_app(var)->get_arg(i))); + } + result = mk_add_app(new_add_args.size(), new_add_args.c_ptr()); + TRACE("mul_bug", tout << "result: " << mk_bounded_pp(result, m(),5) << "\n";); + return BR_REWRITE2; + } + } + + SASSERT(num_coeffs <= num_args - 2); + + if (!m_som || num_add == 0) { + ptr_buffer new_args; + expr * prev = 0; + bool ordered = true; + for (unsigned i = 0; i < num_args; i++) { + expr * curr = args[i]; + if (is_numeral(curr)) + continue; + if (prev != 0 && lt(curr, prev)) + ordered = false; + new_args.push_back(curr); + prev = curr; + } + TRACE("poly_rewriter", + for (unsigned i = 0; i < new_args.size(); i++) { + if (i > 0) + tout << (lt(new_args[i-1], new_args[i]) ? " < " : " !< "); + tout << mk_ismt2_pp(new_args[i], m()); + } + tout << "\nordered: " << ordered << "\n";); + if (ordered && num_coeffs == 0 && !use_power()) + return BR_FAILED; + if (!ordered) { + if (use_power()) + std::sort(new_args.begin(), new_args.end(), mon_pw_lt(*this)); + else + std::sort(new_args.begin(), new_args.end(), ast_to_lt()); + TRACE("poly_rewriter", + tout << "after sorting:\n"; + for (unsigned i = 0; i < new_args.size(); i++) { + if (i > 0) + tout << (lt(new_args[i-1], new_args[i]) ? " < " : " !< "); + tout << mk_ismt2_pp(new_args[i], m()); + } + tout << "\n";); + } + SASSERT(new_args.size() >= 2); + result = mk_mul_app(new_args.size(), new_args.c_ptr()); + result = mk_mul_app(c, result); + TRACE("poly_rewriter", tout << "mk_nflat_mul_core result:\n" << mk_ismt2_pp(result, m()) << "\n";); + return BR_DONE; + } + + SASSERT(m_som && num_add > 0); + + sbuffer szs; + sbuffer it; + sbuffer sums; + for (unsigned i = 0; i < num_args; i ++) { + it.push_back(0); + expr * arg = args[i]; + if (is_add(arg)) { + sums.push_back(const_cast(to_app(arg)->get_args())); + szs.push_back(to_app(arg)->get_num_args()); + } + else { + sums.push_back(const_cast(args + i)); + szs.push_back(1); + SASSERT(sums.back()[0] == arg); + } + } + expr_ref_buffer sum(m()); // must be ref_buffer because we may throw an exception + ptr_buffer m_args; + TRACE("som", tout << "starting som...\n";); + do { + TRACE("som", for (unsigned i = 0; i < it.size(); i++) tout << it[i] << " "; + tout << "\n";); + if (sum.size() > m_som_blowup) + throw rewriter_exception(g_ste_blowup_msg); + m_args.reset(); + for (unsigned i = 0; i < num_args; i++) { + expr * const * v = sums[i]; + expr * arg = v[it[i]]; + m_args.push_back(arg); + } + sum.push_back(mk_mul_app(m_args.size(), m_args.c_ptr())); + } + while (product_iterator_next(szs.size(), szs.c_ptr(), it.c_ptr())); + result = mk_add_app(sum.size(), sum.c_ptr()); + return BR_REWRITE2; +} + +template +br_status poly_rewriter::mk_flat_add_core(unsigned num_args, expr * const * args, expr_ref & result) { + unsigned i; + for (i = 0; i < num_args; i++) { + if (is_add(args[i])) + break; + } + if (i < num_args) { + // has nested ADDs + ptr_buffer flat_args; + flat_args.append(i, args); + for (; i < num_args; i++) { + expr * arg = args[i]; + // Remark: all rewrites are depth 1. + if (is_add(arg)) { + unsigned num = to_app(arg)->get_num_args(); + for (unsigned j = 0; j < num; j++) + flat_args.push_back(to_app(arg)->get_arg(j)); + } + else { + flat_args.push_back(arg); + } + } + br_status st = mk_nflat_add_core(flat_args.size(), flat_args.c_ptr(), result); + if (st == BR_FAILED) { + result = mk_add_app(flat_args.size(), flat_args.c_ptr()); + return BR_DONE; + } + return st; + } + return mk_nflat_add_core(num_args, args, result); +} + +template +inline expr * poly_rewriter::get_power_product(expr * t) { + if (is_mul(t) && to_app(t)->get_num_args() == 2 && is_numeral(to_app(t)->get_arg(0))) + return to_app(t)->get_arg(1); + return t; +} + +template +inline expr * poly_rewriter::get_power_product(expr * t, numeral & a) { + if (is_mul(t) && to_app(t)->get_num_args() == 2 && is_numeral(to_app(t)->get_arg(0), a)) + return to_app(t)->get_arg(1); + a = numeral(1); + return t; +} + +template +bool poly_rewriter::is_mul(expr * t, numeral & c, expr * & pp) { + if (!is_mul(t) || to_app(t)->get_num_args() != 2) + return false; + if (!is_numeral(to_app(t)->get_arg(0), c)) + return false; + pp = to_app(t)->get_arg(1); + return true; +} + +template +struct poly_rewriter::hoist_cmul_lt { + poly_rewriter & m_r; + hoist_cmul_lt(poly_rewriter & r):m_r(r) {} + + bool operator()(expr * t1, expr * t2) const { + expr * pp1, * pp2; + numeral c1, c2; + bool is_mul1 = m_r.is_mul(t1, c1, pp1); + bool is_mul2 = m_r.is_mul(t2, c2, pp2); + if (!is_mul1 && is_mul2) + return true; + if (is_mul1 && !is_mul2) + return false; + if (!is_mul1 && !is_mul2) + return t1->get_id() < t2->get_id(); + if (c1 < c2) + return true; + if (c1 > c2) + return false; + return pp1->get_id() < pp2->get_id(); + } +}; + +template +void poly_rewriter::hoist_cmul(expr_ref_buffer & args) { + unsigned sz = args.size(); + std::sort(args.c_ptr(), args.c_ptr() + sz, hoist_cmul_lt(*this)); + numeral c, c_prime; + ptr_buffer pps; + expr * pp, * pp_prime; + unsigned j = 0; + unsigned i = 0; + while (i < sz) { + expr * mon = args[i]; + if (is_mul(mon, c, pp) && i < sz - 1) { + expr * mon_prime = args[i+1]; + if (is_mul(mon_prime, c_prime, pp_prime) && c == c_prime) { + // found target + pps.reset(); + pps.push_back(pp); + pps.push_back(pp_prime); + i += 2; + while (i < sz && is_mul(args[i], c_prime, pp_prime) && c == c_prime) { + pps.push_back(pp_prime); + i++; + } + SASSERT(is_numeral(to_app(mon)->get_arg(0), c_prime) && c == c_prime); + expr * mul_args[2] = { to_app(mon)->get_arg(0), mk_add_app(pps.size(), pps.c_ptr()) }; + args.set(j, mk_mul_app(2, mul_args)); + j++; + continue; + } + } + args.set(j, mon); + j++; + i++; + } + args.resize(j); +} + +template +br_status poly_rewriter::mk_nflat_add_core(unsigned num_args, expr * const * args, expr_ref & result) { + SASSERT(num_args >= 2); + numeral c; + unsigned num_coeffs = 0; + numeral a; + expr_fast_mark1 visited; // visited.is_marked(power_product) if the power_product occurs in args + expr_fast_mark2 multiple; // multiple.is_marked(power_product) if power_product occurs more than once + bool has_multiple = false; + expr * prev = 0; + bool ordered = true; + for (unsigned i = 0; i < num_args; i++) { + expr * arg = args[i]; + if (is_numeral(arg, a)) { + num_coeffs++; + c += a; + } + else { + // arg is not a numeral + if (m_sort_sums && ordered) { + if (prev != 0 && lt(arg, prev)) + ordered = false; + prev = arg; + } + } + + arg = get_power_product(arg); + if (visited.is_marked(arg)) { + multiple.mark(arg); + has_multiple = true; + } + else { + visited.mark(arg); + } + } + normalize(c); + SASSERT(m_sort_sums || ordered); + TRACE("sort_sums", + tout << "ordered: " << ordered << "\n"; + for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";); + + if (has_multiple) { + // expensive case + buffer coeffs; + m_expr2pos.reset(); + // compute the coefficient of power products that occur multiple times. + for (unsigned i = 0; i < num_args; i++) { + expr * arg = args[i]; + if (is_numeral(arg)) + continue; + expr * pp = get_power_product(arg, a); + if (!multiple.is_marked(pp)) + continue; + unsigned pos; + if (m_expr2pos.find(pp, pos)) { + coeffs[pos] += a; + } + else { + m_expr2pos.insert(pp, coeffs.size()); + coeffs.push_back(a); + } + } + expr_ref_buffer new_args(m()); + if (!c.is_zero()) { + new_args.push_back(mk_numeral(c)); + } + // copy power products with non zero coefficients to new_args + visited.reset(); + for (unsigned i = 0; i < num_args; i++) { + expr * arg = args[i]; + if (is_numeral(arg)) + continue; + expr * pp = get_power_product(arg); + if (!multiple.is_marked(pp)) { + new_args.push_back(arg); + } + else if (!visited.is_marked(pp)) { + visited.mark(pp); + unsigned pos = UINT_MAX; + m_expr2pos.find(pp, pos); + SASSERT(pos != UINT_MAX); + a = coeffs[pos]; + normalize(a); + if (!a.is_zero()) + new_args.push_back(mk_mul_app(a, pp)); + } + } + if (m_hoist_cmul) { + hoist_cmul(new_args); + } + else if (m_sort_sums) { + TRACE("sort_sums_bug", tout << "new_args.size(): " << new_args.size() << "\n";); + if (c.is_zero()) + std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), ast_to_lt()); + else + std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size(), ast_to_lt()); + } + result = mk_add_app(new_args.size(), new_args.c_ptr()); + if (hoist_multiplication(result)) { + return BR_REWRITE_FULL; + } + return BR_DONE; + } + else { + SASSERT(!has_multiple); + if (ordered && !m_hoist_mul && !m_hoist_cmul) { + if (num_coeffs == 0) + return BR_FAILED; + if (num_coeffs == 1 && is_numeral(args[0], a) && !a.is_zero()) + return BR_FAILED; + } + expr_ref_buffer new_args(m()); + if (!c.is_zero()) + new_args.push_back(mk_numeral(c)); + for (unsigned i = 0; i < num_args; i++) { + expr * arg = args[i]; + if (is_numeral(arg)) + continue; + new_args.push_back(arg); + } + if (m_hoist_cmul) { + hoist_cmul(new_args); + } + else if (!ordered) { + if (c.is_zero()) + std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), ast_to_lt()); + else + std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size(), ast_to_lt()); + } + result = mk_add_app(new_args.size(), new_args.c_ptr()); + if (hoist_multiplication(result)) { + return BR_REWRITE_FULL; + } + return BR_DONE; + } +} + + +template +br_status poly_rewriter::mk_uminus(expr * arg, expr_ref & result) { + numeral a; + set_curr_sort(m().get_sort(arg)); + if (is_numeral(arg, a)) { + a.neg(); + normalize(a); + result = mk_numeral(a); + return BR_DONE; + } + else { + result = mk_mul_app(numeral(-1), arg); + return BR_REWRITE1; + } +} + +template +br_status poly_rewriter::mk_sub(unsigned num_args, expr * const * args, expr_ref & result) { + SASSERT(num_args > 0); + if (num_args == 1) { + result = args[0]; + return BR_DONE; + } + set_curr_sort(m().get_sort(args[0])); + expr * minus_one = mk_numeral(numeral(-1)); + ptr_buffer new_args; + new_args.push_back(args[0]); + for (unsigned i = 1; i < num_args; i++) { + expr * aux_args[2] = { minus_one, args[i] }; + new_args.push_back(mk_mul_app(2, aux_args)); + } + result = mk_add_app(new_args.size(), new_args.c_ptr()); + return BR_REWRITE2; +} + +/** + \brief Cancel/Combine monomials that occur is the left and right hand sides. + + \remark If move = true, then all non-constant monomials are moved to the left-hand-side. +*/ +template +br_status poly_rewriter::cancel_monomials(expr * lhs, expr * rhs, bool move, expr_ref & lhs_result, expr_ref & rhs_result) { + set_curr_sort(m().get_sort(lhs)); + unsigned lhs_sz; + expr * const * lhs_monomials = get_monomials(lhs, lhs_sz); + unsigned rhs_sz; + expr * const * rhs_monomials = get_monomials(rhs, rhs_sz); + + expr_fast_mark1 visited; // visited.is_marked(power_product) if the power_product occurs in lhs or rhs + expr_fast_mark2 multiple; // multiple.is_marked(power_product) if power_product occurs more than once + bool has_multiple = false; + + numeral c(0); + numeral a; + unsigned num_coeffs = 0; + + for (unsigned i = 0; i < lhs_sz; i++) { + expr * arg = lhs_monomials[i]; + if (is_numeral(arg, a)) { + c += a; + num_coeffs++; + } + else { + visited.mark(get_power_product(arg)); + } + } + + if (move && num_coeffs == 0 && is_numeral(rhs)) + return BR_FAILED; + + for (unsigned i = 0; i < rhs_sz; i++) { + expr * arg = rhs_monomials[i]; + if (is_numeral(arg, a)) { + c -= a; + num_coeffs++; + } + else { + expr * pp = get_power_product(arg); + if (visited.is_marked(pp)) { + multiple.mark(pp); + has_multiple = true; + } + } + } + + normalize(c); + + if (!has_multiple && num_coeffs <= 1) { + if (move) { + if (is_numeral(rhs)) + return BR_FAILED; + } + else { + if (num_coeffs == 0 || is_numeral(rhs)) + return BR_FAILED; + } + } + + buffer coeffs; + m_expr2pos.reset(); + for (unsigned i = 0; i < lhs_sz; i++) { + expr * arg = lhs_monomials[i]; + if (is_numeral(arg)) + continue; + expr * pp = get_power_product(arg, a); + if (!multiple.is_marked(pp)) + continue; + unsigned pos; + if (m_expr2pos.find(pp, pos)) { + coeffs[pos] += a; + } + else { + m_expr2pos.insert(pp, coeffs.size()); + coeffs.push_back(a); + } + } + + for (unsigned i = 0; i < rhs_sz; i++) { + expr * arg = rhs_monomials[i]; + if (is_numeral(arg)) + continue; + expr * pp = get_power_product(arg, a); + if (!multiple.is_marked(pp)) + continue; + unsigned pos = UINT_MAX; + m_expr2pos.find(pp, pos); + SASSERT(pos != UINT_MAX); + coeffs[pos] -= a; + } + + + ptr_buffer new_lhs_monomials; + new_lhs_monomials.push_back(0); // save space for coefficient if needed + // copy power products with non zero coefficients to new_lhs_monomials + visited.reset(); + for (unsigned i = 0; i < lhs_sz; i++) { + expr * arg = lhs_monomials[i]; + if (is_numeral(arg)) + continue; + expr * pp = get_power_product(arg); + if (!multiple.is_marked(pp)) { + new_lhs_monomials.push_back(arg); + } + else if (!visited.is_marked(pp)) { + visited.mark(pp); + unsigned pos = UINT_MAX; + m_expr2pos.find(pp, pos); + SASSERT(pos != UINT_MAX); + a = coeffs[pos]; + if (!a.is_zero()) + new_lhs_monomials.push_back(mk_mul_app(a, pp)); + } + } + + ptr_buffer new_rhs_monomials; + new_rhs_monomials.push_back(0); // save space for coefficient if needed + for (unsigned i = 0; i < rhs_sz; i++) { + expr * arg = rhs_monomials[i]; + if (is_numeral(arg)) + continue; + expr * pp = get_power_product(arg, a); + if (!multiple.is_marked(pp)) { + if (move) { + if (!a.is_zero()) { + if (a.is_minus_one()) { + new_lhs_monomials.push_back(pp); + } + else { + a.neg(); + SASSERT(!a.is_one()); + expr * args[2] = { mk_numeral(a), pp }; + new_lhs_monomials.push_back(mk_mul_app(2, args)); + } + } + } + else { + new_rhs_monomials.push_back(arg); + } + } + } + + bool c_at_rhs = false; + if (move) { + if (m_sort_sums) { + // + 1 to skip coefficient + std::sort(new_lhs_monomials.begin() + 1, new_lhs_monomials.end(), ast_to_lt()); + } + c_at_rhs = true; + } + else if (new_rhs_monomials.size() == 1) { // rhs is empty + c_at_rhs = true; + } + else if (new_lhs_monomials.size() > 1) { + c_at_rhs = true; + } + + if (c_at_rhs) { + c.neg(); + normalize(c); + new_rhs_monomials[0] = mk_numeral(c); + lhs_result = mk_add_app(new_lhs_monomials.size() - 1, new_lhs_monomials.c_ptr() + 1); + rhs_result = mk_add_app(new_rhs_monomials.size(), new_rhs_monomials.c_ptr()); + } + else { + new_lhs_monomials[0] = mk_numeral(c); + lhs_result = mk_add_app(new_lhs_monomials.size(), new_lhs_monomials.c_ptr()); + rhs_result = mk_add_app(new_rhs_monomials.size() - 1, new_rhs_monomials.c_ptr() + 1); + } + return BR_DONE; +} + +#define TO_BUFFER(_tester_, _buffer_, _e_) \ + _buffer_.push_back(_e_); \ + for (unsigned _i = 0; _i < _buffer_.size(); ) { \ + expr* _e = _buffer_[_i]; \ + if (_tester_(_e)) { \ + app* a = to_app(_e); \ + _buffer_[_i] = a->get_arg(0); \ + for (unsigned _j = 1; _j < a->get_num_args(); ++_j) { \ + _buffer_.push_back(a->get_arg(_j)); \ + } \ + } \ + else { \ + ++_i; \ + } \ + } \ + +template +bool poly_rewriter::hoist_multiplication(expr_ref& som) { + if (!m_hoist_mul) { + return false; + } + ptr_buffer adds, muls; + TO_BUFFER(is_add, adds, som); + buffer valid(adds.size(), true); + obj_map mul_map; + unsigned j; + bool change = false; + for (unsigned k = 0; k < adds.size(); ++k) { + expr* e = adds[k]; + muls.reset(); + TO_BUFFER(is_mul, muls, e); + for (unsigned i = 0; i < muls.size(); ++i) { + e = muls[i]; + if (is_numeral(e)) { + continue; + } + if (mul_map.find(e, j) && valid[j] && j != k) { + m_curr_sort = m().get_sort(adds[k]); + adds[j] = merge_muls(adds[j], adds[k]); + adds[k] = mk_numeral(rational(0)); + valid[j] = false; + valid[k] = false; + change = true; + break; + } + else { + mul_map.insert(e, k); + } + } + } + if (!change) { + return false; + } + + som = mk_add_app(adds.size(), adds.c_ptr()); + + + return true; +} + +template +expr* poly_rewriter::merge_muls(expr* x, expr* y) { + ptr_buffer m1, m2; + TO_BUFFER(is_mul, m1, x); + TO_BUFFER(is_mul, m2, y); + unsigned k = 0; + for (unsigned i = 0; i < m1.size(); ++i) { + x = m1[i]; + bool found = false; + unsigned j; + for (j = k; j < m2.size(); ++j) { + found = m2[j] == x; + if (found) break; + } + if (found) { + std::swap(m1[i],m1[k]); + std::swap(m2[j],m2[k]); + ++k; + } + } + m_curr_sort = m().get_sort(x); + SASSERT(k > 0); + SASSERT(m1.size() >= k); + SASSERT(m2.size() >= k); + expr* args[2] = { mk_mul_app(m1.size()-k, m1.c_ptr()+k), + mk_mul_app(m2.size()-k, m2.c_ptr()+k) }; + if (k == m1.size()) { + m1.push_back(0); + } + m1[k] = mk_add_app(2, args); + return mk_mul_app(k+1, m1.c_ptr()); +} diff --git a/src/cmd_context/README b/src/cmd_context/README index c44a00690..feb3abd20 100644 --- a/src/cmd_context/README +++ b/src/cmd_context/README @@ -1,2 +1,2 @@ Command context provides the infrastructure for executing commands in front-ends such as SMT-LIB 2.0. -It is also provides the solver abstraction to plugin solvers in this kind of front-end. \ No newline at end of file +It is also provides the solver abstraction to plugin solvers in this kind of front-end. diff --git a/src/math/euclid/README b/src/math/euclid/README index 7235cd76f..17d408fc9 100644 --- a/src/math/euclid/README +++ b/src/math/euclid/README @@ -1,2 +1,2 @@ Basic Euclidean solver for linear integer equations. -This solver generates "explanations". \ No newline at end of file +This solver generates "explanations". diff --git a/src/math/interval/README b/src/math/interval/README index 75aa2e9c6..06ca1ea7a 100644 --- a/src/math/interval/README +++ b/src/math/interval/README @@ -1,2 +1,2 @@ Template for interval arithmetic. The template can be instantiated using different numeral (integers/mpz, rationals/mpq, floating-point/mpf, etc) packages. -The class im_default_config defines a default configuration for the template that uses rationals. It also shows what is the expected signature used by the template. \ No newline at end of file +The class im_default_config defines a default configuration for the template that uses rationals. It also shows what is the expected signature used by the template. diff --git a/src/math/polynomial/README b/src/math/polynomial/README index 5d079eea0..2d2f9f0a0 100644 --- a/src/math/polynomial/README +++ b/src/math/polynomial/README @@ -1,3 +1,3 @@ Polynomial manipulation package. It contains support for univariate (upolynomial.*) and multivariate polynomials (polynomial.*). -Multivariate polynomial factorization does not work yet (polynomial_factorization.*), and it is disabled. \ No newline at end of file +Multivariate polynomial factorization does not work yet (polynomial_factorization.*), and it is disabled. diff --git a/src/muz_qe/dl_hassel_common.cpp b/src/muz_qe/dl_hassel_common.cpp deleted file mode 100755 index 6201868ca..000000000 --- a/src/muz_qe/dl_hassel_common.cpp +++ /dev/null @@ -1,434 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - dl_hassel_common.cpp - -Abstract: - - - -Revision History: - ---*/ - -#include "dl_hassel_common.h" -#include "dl_context.h" - -#include - -namespace datalog { - - static void formula_to_dnf_aux(app *and, unsigned idx, std::set& conjexpr, std::set& toplevel, ast_manager& m) { - if (idx == and->get_num_args()) { - std::vector v(conjexpr.begin(), conjexpr.end()); - toplevel.insert(m.mk_and((unsigned)v.size(), &v[0])); - return; - } - - expr *e = and->get_arg(idx); - if (is_app(e) && to_app(e)->get_decl_kind() == OP_OR) { - app *or = to_app(e); - // quick subsumption test: if any of the elements of the OR is already ANDed, then we skip this OR - for (unsigned i = 0; i < or->get_num_args(); ++i) { - if (conjexpr.count(or->get_arg(i))) { - formula_to_dnf_aux(and, idx+1, conjexpr, toplevel, m); - return; - } - } - - for (unsigned i = 0; i < or->get_num_args(); ++i) { - std::set conjexpr2(conjexpr); - conjexpr2.insert(or->get_arg(i)); - formula_to_dnf_aux(and, idx+1, conjexpr2, toplevel, m); - } - } else { - conjexpr.insert(e); - formula_to_dnf_aux(and, idx+1, conjexpr, toplevel, m); - } - } - - expr_ref formula_to_dnf(expr_ref f) { - app *a = to_app(f); - SASSERT(a->get_decl_kind() == OP_AND); - std::set toplevel, conjexpr; - formula_to_dnf_aux(a, 0, conjexpr, toplevel, f.m()); - - if (toplevel.size() > 1) { - std::vector v(toplevel.begin(), toplevel.end()); - return expr_ref(f.m().mk_or((unsigned)v.size(), &v[0]), f.m()); - } else { - return expr_ref(*toplevel.begin(), f.m()); - } - } - - bool bit_vector::contains(const bit_vector & other) const { - unsigned n = num_words(); - if (n == 0) - return true; - - for (unsigned i = 0; i < n - 1; ++i) { - if ((m_data[i] & other.m_data[i]) != other.m_data[i]) - return false; - } - unsigned bit_rest = m_num_bits % 32; - unsigned mask = (1 << bit_rest) - 1; - if (mask == 0) mask = UINT_MAX; - unsigned other_data = other.m_data[n-1] & mask; - return (m_data[n-1] & other_data) == other_data; - } - - bool bit_vector::contains(const bit_vector & other, unsigned idx) const { - // TODO: optimize this to avoid copy - return slice(idx, other.size()).contains(other); - } - - bool bit_vector::contains_consecutive_zeros() const { - unsigned n = num_words(); - if (n == 0) - return false; - - for (unsigned i = 0; i < n - 1; ++i) { - if ((((m_data[i] << 1) | m_data[i]) & 0xAAAAAAAA) != 0xAAAAAAAA) - return true; - } - unsigned bit_rest = m_num_bits % 32; - unsigned mask = (1 << bit_rest) - 1; - if (mask == 0) mask = UINT_MAX; - mask &= 0xAAAAAAAA; - return ((((m_data[n-1] << 1) | m_data[n-1]) & mask) != mask); - } - - bit_vector bit_vector::slice(unsigned idx, unsigned length) const { - bit_vector Res(length); - // TODO: optimize w/ memcpy when possible - for (unsigned i = idx; i < idx + length; ++i) { - Res.push_back(get(i)); - } - SASSERT(Res.size() == length); - return Res; - } - - void bit_vector::append(const bit_vector & other) { - if (other.empty()) - return; - - if ((m_num_bits % 32) == 0) { - unsigned prev_num_bits = m_num_bits; - resize(m_num_bits + other.m_num_bits); - memcpy(&get_bit_word(prev_num_bits), other.m_data, other.num_words() * sizeof(unsigned)); - return; - } - - // TODO: optimize the other cases. - for (unsigned i = 0; i < other.m_num_bits; ++i) { - push_back(other.get(i)); - } - } - - uint64 bit_vector::to_number(unsigned idx, unsigned length) const { - SASSERT(length <= 64); - uint64 r = 0; - for (unsigned i = 0; i < length; ++i) { - r = (r << 1) | (uint64)get(idx+i); - } - return r; - } - - bool bit_vector::operator<(bit_vector const & other) const { - SASSERT(m_num_bits == other.m_num_bits); - unsigned n = num_words(); - if (n == 0) - return false; - - for (unsigned i = 0; i < n - 1; ++i) { - if (m_data[i] > other.m_data[i]) - return false; - if (m_data[i] < other.m_data[i]) - return true; - } - - unsigned bit_rest = m_num_bits % 32; - unsigned mask = (1 << bit_rest) - 1; - if (mask == 0) mask = UINT_MAX; - return (m_data[n-1] & mask) < (other.m_data[n-1] & mask); - } - - table_information::table_information(table_plugin & p, const table_signature& sig) : - m_column_info(sig.size()+1), - m_bv_util(p.get_context().get_manager()), - m_decl_util(p.get_context().get_manager()) { - - unsigned column = 0; - for (unsigned i = 0; i < sig.size(); ++i) { - unsigned num_bits = uint64_log2(sig[i]); - SASSERT(num_bits == 64 || (1ULL << num_bits) == sig[i]); - m_column_info[i] = column; - column += num_bits; - } - m_column_info[sig.size()] = column; - } - - void table_information::expand_column_vector(unsigned_vector& v, const table_information *other) const { - unsigned_vector orig; - orig.swap(v); - - for (unsigned i = 0; i < orig.size(); ++i) { - unsigned col, limit; - if (orig[i] < get_num_cols()) { - col = column_idx(orig[i]); - limit = col + column_num_bits(orig[i]); - } else { - unsigned idx = orig[i] - get_num_cols(); - col = get_num_bits() + other->column_idx(idx); - limit = col + other->column_num_bits(idx); - } - - for (; col < limit; ++col) { - v.push_back(col); - } - } - } - - void table_information::display(std::ostream & out) const { - out << '<'; - for (unsigned i = 0; i < get_num_cols(); ++i) { - if (i > 0) - out << ", "; - out << column_num_bits(i); - } - out << ">\n"; - } - - ternary_bitvector::ternary_bitvector(unsigned size, bool full) : - bit_vector() { - resize(size, full); - } - - ternary_bitvector::ternary_bitvector(uint64 n, unsigned num_bits) : - bit_vector(2 * num_bits) { - append_number(n, num_bits); - } - - ternary_bitvector::ternary_bitvector(const table_fact& f, const table_information& t) : - bit_vector(2 * t.get_num_bits()) { - for (unsigned i = 0; i < f.size(); ++i) { - SASSERT(t.column_idx(i) == size()); - append_number(f[i], t.column_num_bits(i)); - } - SASSERT(size() == t.get_num_bits()); - } - - void ternary_bitvector::fill1() { - memset(m_data, 0xFF, m_capacity * sizeof(unsigned)); - } - - unsigned ternary_bitvector::get(unsigned idx) const { - idx *= 2; - return (bit_vector::get(idx) << 1) | (unsigned)bit_vector::get(idx+1); - } - - void ternary_bitvector::set(unsigned idx, unsigned val) { - SASSERT(val == BIT_0 || val == BIT_1 || val == BIT_x); - idx *= 2; - bit_vector::set(idx, (val >> 1) != 0); - bit_vector::set(idx+1, (val & 1) != 0); - } - - void ternary_bitvector::push_back(unsigned val) { - SASSERT(val == BIT_0 || val == BIT_1 || val == BIT_x); - bit_vector::push_back((val >> 1) != 0); - bit_vector::push_back((val & 1) != 0); - } - - void ternary_bitvector::append_number(uint64 n, unsigned num_bits) { - SASSERT(num_bits <= 64); - for (int bit = num_bits-1; bit >= 0; --bit) { - if (n & (1ULL << bit)) { - push_back(BIT_1); - } else { - push_back(BIT_0); - } - } - } - - void ternary_bitvector::mk_idx_eq(unsigned idx, ternary_bitvector& val) { - for (unsigned i = 0; i < val.size(); ++i) { - set(idx+i, val.get(i)); - } - } - - ternary_bitvector ternary_bitvector::and(const ternary_bitvector& other) const{ - ternary_bitvector result(*this); - result &= other; - return result; - } - - void ternary_bitvector::neg(union_ternary_bitvector& result) const { - ternary_bitvector negated; - negated.resize(size()); - - for (unsigned i = 0; i < size(); ++i) { - switch (get(i)) { - case BIT_0: - negated.fill1(); - negated.set(i, BIT_1); - break; - case BIT_1: - negated.fill1(); - negated.set(i, BIT_0); - break; - default: - continue; - } - result.add_fact(negated); - } - } - - static void join_fix_eqs(ternary_bitvector& TBV, unsigned idx, unsigned col2_offset, - const unsigned_vector& cols1, const unsigned_vector& cols2, - union_ternary_bitvector& result) { - if (idx == cols1.size()) { - result.add_fact(TBV); - return; - } - - unsigned idx1 = cols1[idx]; - unsigned idx2 = cols2[idx] + col2_offset; - unsigned v1 = TBV.get(idx1); - unsigned v2 = TBV.get(idx2); - - if (v1 == BIT_x) { - if (v2 == BIT_x) { - // both x: duplicate row - ternary_bitvector TBV2(TBV); - TBV2.set(idx1, BIT_0); - TBV2.set(idx2, BIT_0); - join_fix_eqs(TBV2, idx+1, col2_offset, cols1, cols2, result); - - TBV.set(idx1, BIT_1); - TBV.set(idx2, BIT_1); - } else { - TBV.set(idx1, v2); - } - } else if (v2 == BIT_x) { - TBV.set(idx2, v1); - } else if (v1 != v2) { - // columns don't match - return; - } - join_fix_eqs(TBV, idx+1, col2_offset, cols1, cols2, result); - } - - void ternary_bitvector::join(const ternary_bitvector& other, - const unsigned_vector& cols1, - const unsigned_vector& cols2, - union_ternary_bitvector& result) const { - ternary_bitvector TBV(*this); - TBV.append(other); - join_fix_eqs(TBV, 0, size(), cols1, cols2, result); - } - - bool ternary_bitvector::project(const unsigned_vector& delcols, ternary_bitvector& result) const { - unsigned *rm_cols = delcols.c_ptr(); - - for (unsigned i = 0; i < size(); ++i) { - if (*rm_cols == i) { - ++rm_cols; - continue; - } - result.push_back(get(i)); - } - return true; - } - - static void copy_column(ternary_bitvector& CopyTo, const ternary_bitvector& CopyFrom, - unsigned col_dst, unsigned col_src, const table_information& src_table, - const table_information& dst_table) { - unsigned idx_dst = dst_table.column_idx(col_dst); - unsigned idx_src = src_table.column_idx(col_src); - unsigned num_bits = dst_table.column_num_bits(col_dst); - SASSERT(num_bits == src_table.column_num_bits(col_src)); - - for (unsigned i = 0; i < num_bits; ++i) { - CopyTo.set(idx_dst+i, CopyFrom.get(idx_src+i)); - } - } - - void ternary_bitvector::rename(const unsigned_vector& cyclecols, - const unsigned_vector& out_of_cycle_cols, - const table_information& src_table, - const table_information& dst_table, - ternary_bitvector& result) const { - result.resize(dst_table.get_num_bits()); - - for (unsigned i = 1; i < cyclecols.size(); ++i) { - copy_column(result, *this, cyclecols[i-1], cyclecols[i], src_table, dst_table); - } - copy_column(result, *this, cyclecols[cyclecols.size()-1], cyclecols[0], src_table, dst_table); - - for (unsigned i = 0; i < out_of_cycle_cols.size(); ++i) { - unsigned col = out_of_cycle_cols[i]; - copy_column(result, *this, col, col, src_table, dst_table); - } - } - - unsigned ternary_bitvector::size_in_bytes() const { - return sizeof(*this) + m_capacity; - } - - void ternary_bitvector::display(std::ostream & out) const { - for (unsigned i = 0; i < size(); ++i) { - switch (get(i)) { - case BIT_0: - out << '0'; - break; - case BIT_1: - out << '1'; - break; - case BIT_x: - out << 'x'; - break; - default: - UNREACHABLE(); - } - } - } - -#if Z3DEBUG - void ternary_bitvector::expand(std::set & BVs) const { - bit_vector BV(m_num_bits); - expand(BVs, BV, 0); - } - - void ternary_bitvector::expand(std::set & BVs, bit_vector &BV, unsigned idx) const { - if (idx == size()) { - BVs.insert(BV); - return; - } - - switch (get(idx)) { - case BIT_0: - BV.push_back(false); - expand(BVs, BV, idx+1); - break; - case BIT_1: - BV.push_back(true); - expand(BVs, BV, idx+1); - break; - case BIT_x: { // x: duplicate - bit_vector BV2(BV); - BV.push_back(false); - BV2.push_back(true); - expand(BVs, BV, idx+1); - expand(BVs, BV2, idx+1); - } - break; - default: - UNREACHABLE(); - } - } -#endif - -} diff --git a/src/muz_qe/dl_hassel_common.h b/src/muz_qe/dl_hassel_common.h deleted file mode 100755 index 7c1d1e614..000000000 --- a/src/muz_qe/dl_hassel_common.h +++ /dev/null @@ -1,1079 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - dl_hassel_common.h - -Abstract: - - - -Revision History: - ---*/ - -#ifndef _DL_HASSEL_COMMON_H_ -#define _DL_HASSEL_COMMON_H_ - -#include "bit_vector.h" -#include "dl_base.h" -#include "bv_decl_plugin.h" -#include "union_find.h" -#include -#include - -#define BIT_0 ((0<<1)|1) -#define BIT_1 ((1<<1)|0) -#define BIT_x ((1<<1)|1) - -namespace datalog { - - expr_ref formula_to_dnf(expr_ref f); - - class bit_vector : public ::bit_vector { - public: - bit_vector() : ::bit_vector() {} - bit_vector(unsigned bits) : ::bit_vector(bits) {} - - bool contains(const bit_vector & other) const; - bool contains(const bit_vector & other, unsigned idx) const; - bool contains_consecutive_zeros() const; - - bit_vector slice(unsigned idx, unsigned length) const; - void append(const bit_vector & other); - - uint64 to_number(unsigned idx, unsigned length) const; - - // for std::less operations - bool operator<(bit_vector const & other) const; - }; - - - class table_information { - unsigned_vector m_column_info; - bv_util m_bv_util; - dl_decl_util m_decl_util; - - public: - table_information(table_plugin & p, const table_signature& sig); - - unsigned get_num_bits() const { - return m_column_info.back(); - } - - unsigned get_num_cols() const { - return m_column_info.size()-1; - } - - unsigned column_idx(unsigned col) const { - return m_column_info[col]; - } - - unsigned column_num_bits(unsigned col) const { - return m_column_info[col+1] - m_column_info[col]; - } - - void expand_column_vector(unsigned_vector& v, const table_information *other = 0) const; - - void display(std::ostream & out) const; - - const bv_util& get_bv_util() const { return m_bv_util; } - const dl_decl_util& get_decl_util() const { return m_decl_util; } - }; - - - template class union_ternary_bitvector; - - - class ternary_bitvector : private bit_vector { - public: - ternary_bitvector() : bit_vector() {} - ternary_bitvector(unsigned size) : bit_vector(2 * size) {} - - ternary_bitvector(unsigned size, bool full); - ternary_bitvector(uint64 n, unsigned num_bits); - ternary_bitvector(const table_fact& f, const table_information& t); - - void swap(ternary_bitvector& other) { - SASSERT(size() == other.size()); - bit_vector::swap(other); - } - - void resize(unsigned new_size, bool val = false) { - bit_vector::resize(2 * new_size, val); - } - - void reset() { - m_num_bits = 0; - } - - unsigned size() const { - SASSERT((m_num_bits % 2) == 0); - return m_num_bits/2; - } - - void fill1(); - - void append(const ternary_bitvector & other) { bit_vector::append(other); } - bool contains(const ternary_bitvector & other) const { return bit_vector::contains(other); } - - bool is_empty() const { return contains_consecutive_zeros(); } - - unsigned get(unsigned idx) const; - void set(unsigned idx, unsigned val); - void push_back(unsigned val); - void append_number(uint64 n, unsigned num_bits); - void mk_idx_eq(unsigned idx, ternary_bitvector& val); - - ternary_bitvector and(const ternary_bitvector& other) const; - void neg(union_ternary_bitvector& result) const; - - void join(const ternary_bitvector& other, const unsigned_vector& cols1, - const unsigned_vector& cols2, union_ternary_bitvector& result) const; - - bool project(const unsigned_vector& delcols, ternary_bitvector& result) const; - - void rename(const unsigned_vector& cyclecols, const unsigned_vector& out_of_cycle_cols, - const table_information& src_table, const table_information& dst_table, - ternary_bitvector& result) const; - - static bool has_subtract() { return false; } - void subtract(const union_ternary_bitvector& other, - union_ternary_bitvector& result) const { UNREACHABLE(); } - - void display(std::ostream & out) const; - unsigned size_in_bytes() const; - -#if Z3DEBUG - void expand(std::set & BVs) const; -#endif - - private: -#if Z3DEBUG - void expand(std::set & BVs, bit_vector &BV, unsigned idx) const; -#endif - }; - - - template - class union_ternary_bitvector { - typedef std::list union_t; - - union_t m_bitvectors; - unsigned m_bv_size; //!< number of ternary bits - - public: - union_ternary_bitvector(unsigned bv_size) : m_bv_size(bv_size) {} - - union_ternary_bitvector(unsigned bv_size, bool full) : m_bv_size(bv_size) { - if (full) - mk_full(); - } - - union_ternary_bitvector and(const union_ternary_bitvector & Other) const { - if (empty()) - return *this; - if (Other.empty()) - return Other; - - union_ternary_bitvector Ret(m_bv_size); - - for (const_iterator I = begin(), E = end(); I != E; ++I) { - for (const_iterator II = Other.begin(), EE = Other.end(); II != EE; ++II) { - T row(I->and(*II)); - if (!row.is_empty()) - Ret.add_fact(row); - } - } - return Ret; - } - - union_ternary_bitvector or(const union_ternary_bitvector & Other) const { - if (empty()) - return Other; - if (Other.empty()) - return *this; - - union_ternary_bitvector Ret(*this); - Ret.add_facts(Other); - return Ret; - } - - union_ternary_bitvector neg() const { - union_ternary_bitvector Ret(m_bv_size); - Ret.mk_full(); - - union_ternary_bitvector negated(m_bv_size); - for (const_iterator I = begin(), E = end(); I != E; ++I) { - negated.reset(); - I->neg(negated); - Ret.swap(Ret.and(negated)); - } - return Ret; - } - - void subtract(const union_ternary_bitvector& other) { - if (!T::has_subtract()) { - swap(this->and(other.neg())); - return; - } - - union_ternary_bitvector subtracted(m_bv_size); - for (const_iterator I = begin(), E = end(); I != E; ++I) { - I->subtract(other, subtracted); - } - swap(subtracted); - } - -#if 0 - union_ternary_bitvector gc() const { - // Simple subsumption-based cleaning. - union_ternary_bitvector Ret(m_bv_size); - for (union_t::const_reverse_iterator I = m_bitvectors.rbegin(), E = m_bitvectors.rend(); I != E; ++I) { - Ret.add_fact(*I); - } - return Ret; - } -#endif - - void join(const union_ternary_bitvector& other, const unsigned_vector& cols1, - const unsigned_vector& cols2, union_ternary_bitvector& result) const { - for (const_iterator I = begin(), E = end(); I != E; ++I) { - for (const_iterator II = other.begin(), EE = other.end(); II != EE; ++II) { - I->join(*II, cols1, cols2, result); - } - } - } - - void rename(const unsigned_vector& cyclecols, const unsigned_vector& out_of_cycle_cols, - const table_information& src_table, const table_information& dst_table, - union_ternary_bitvector& result) const { - T row(m_bv_size); - for (const_iterator I = begin(), E = end(); I != E; ++I) { - row.reset(); - I->rename(cyclecols, out_of_cycle_cols, src_table, dst_table, row); - result.add_new_fact(row); - } - } - - void project(const unsigned_vector& delcols, union_ternary_bitvector& result) const { - unsigned new_size = m_bv_size - (delcols.size()-1); - T row(new_size); - - for (const_iterator I = begin(), E = end(); I != E; ++I) { - row.reset(); - if (I->project(delcols, row)) { - SASSERT(!row.is_empty()); - result.add_fact(row); - } - } - } - - private: - typedef union_find<> subset_ints; - - // returns 1 if row should be removed, 0 otherwise - static int fix_single_bit(T & BV, unsigned idx, unsigned value, const subset_ints& equalities) { - unsigned root = equalities.find(idx); - idx = root; - do { - unsigned bitval = BV.get(idx); - if (bitval == BIT_x) { - BV.set(idx, value); - } else if (bitval != value) { - return 1; - } - idx = equalities.next(idx); - } while (idx != root); - return 0; - } - - static int fix_single_bit(T & BV1, unsigned idx1, T & BV2, unsigned idx2, - subset_ints& equalities, bool discard_col) { - unsigned A = BV1.get(idx1); - unsigned B = BV2.get(idx2); - - if (A == BIT_x) { - if (B == BIT_x) { - // Both are don't cares. - /////// FIXME::: don't duplicate rows with diff table - if (!discard_col) - return 2; // duplicate row - equalities.merge(idx1, idx2); - return 0; - } else { - // only A is don't care. - return fix_single_bit(BV1, idx1, B, equalities); - } - } else if (B == BIT_x) { - // Only B is don't care. - return fix_single_bit(BV2, idx2, A, equalities); - } else if (A == B) { - return 0; - } else { - return 1; // remove row - } - } - - void fix_eq_bits(unsigned idx1, const T *BV, unsigned idx2, unsigned length, - subset_ints& equalities, const bit_vector& discard_cols) { - for (unsigned i = 0; i < length; ++i) { - for (union_t::iterator I = m_bitvectors.begin(), E = m_bitvectors.end(); I != E; ) { - T *eqBV = BV ? const_cast(BV) : &*I; - bool discard_col = discard_cols.get(idx1+i) || (!BV && discard_cols.get(idx2+i)); - - switch (fix_single_bit(*I, idx1+i, *eqBV, idx2+i, equalities, discard_col)) { - case 1: - // remove row - I = m_bitvectors.erase(I); - break; - - case 2: { - // duplicate row - T BV2(*I); - I->set(idx1+i, BIT_0); - I->set(idx2+i, BIT_0); - - BV2.set(idx1+i, BIT_1); - BV2.set(idx2+i, BIT_1); - m_bitvectors.insert(I, BV2); - ++I; - break;} - - default: - // bits fixed - ++I; - } - } - } - } - - /// make bits of table [idx,idx+max_length] equal to e sliced starting at idx2 - unsigned fix_eq_bits(unsigned idx, const expr *e, unsigned idx2, unsigned max_length, - const table_information& t, subset_ints& equalities, - const bit_vector & discard_cols) { - const bv_util& bvu = t.get_bv_util(); - const dl_decl_util& dutil = t.get_decl_util(); - - rational n; - unsigned bv_size; - if (bvu.is_numeral(e, n, bv_size)) { - T num(n.get_int64(), bv_size); - SASSERT(idx2 < bv_size); - max_length = std::min(max_length, bv_size - idx2); - fix_eq_bits(idx, &num, idx2, max_length, equalities, discard_cols); - return idx + max_length; - } - - uint64 num; - if (dutil.is_numeral(e, num)) { - T num_bv(num, max_length); - fix_eq_bits(idx, &num_bv, idx2, max_length, equalities, discard_cols); - return idx + max_length; - } - - if (bvu.is_concat(e)) { - const app *a = to_app(e); - - // skip the first elements of the concat if e.g. we have a top level extract - unsigned i = 0; - for (; i < a->get_num_args(); ++i) { - unsigned arg_size = bvu.get_bv_size(a->get_arg(i)); - if (idx2 < arg_size) - break; - idx2 -= arg_size; - } - - SASSERT(i < a->get_num_args()); - for (; max_length > 0 && i < a->get_num_args(); ++i) { - unsigned idx0 = idx; - idx = fix_eq_bits(idx, a->get_arg(i), idx2, max_length, t, equalities, discard_cols); - idx2 = 0; - SASSERT((idx - idx0) <= max_length); - max_length = max_length - (idx - idx0); - } - return idx; - } - - unsigned low, high; - expr *e2; - if (bvu.is_extract(e, low, high, e2)) { - SASSERT(low <= high); - unsigned size = bvu.get_bv_size(e2); - unsigned offset = size - (high+1) + idx2; - SASSERT(idx2 < (high-low+1)); - max_length = std::min(max_length, high - low + 1 - idx2); - return fix_eq_bits(idx, e2, offset, max_length, t, equalities, discard_cols); - } - - if (e->get_kind() == AST_VAR) { - unsigned idx_var = idx2 + t.column_idx(to_var(e)->get_idx()); - SASSERT(idx2 < t.column_num_bits(to_var(e)->get_idx())); - max_length = std::min(max_length, t.column_num_bits(to_var(e)->get_idx()) - idx2); - fix_eq_bits(idx, 0, idx_var, max_length, equalities, discard_cols); - return idx + max_length; - } - - NOT_IMPLEMENTED_YET(); - return 0; - } - - void filter(const expr *e, subset_ints& equalities, const bit_vector& discard_cols, - const table_information& t) { - switch (e->get_kind()) { - case AST_APP: { - const app *app = to_app(e); - switch (app->get_decl_kind()) { - case OP_AND: - for (unsigned i = 0; i < app->get_num_args(); ++i) { - filter(app->get_arg(i), equalities, discard_cols, t); - } - return; - - case OP_EQ: { - const expr *a = app->get_arg(0); - const var *v; - unsigned vidx = 0; - unsigned length; - - unsigned low, high; - expr *e2; - if (is_var(a)) { - v = to_var(a); - length = t.column_num_bits(v->get_idx()); - } else if (t.get_bv_util().is_extract(a, low, high, e2)) { - vidx = t.get_bv_util().get_bv_size(e2) - high - 1; - length = high - low + 1; - SASSERT(is_var(e2)); - v = to_var(e2); - } else { - NOT_IMPLEMENTED_YET(); - } - vidx += t.column_idx(v->get_idx()); - - unsigned final_idx = fix_eq_bits(vidx, app->get_arg(1), 0, length, t, equalities, discard_cols); - SASSERT(final_idx == vidx + length); - (void)final_idx; - return;} - - case OP_FALSE: - reset(); - return; - - case OP_NOT: { - union_ternary_bitvector sub(m_bv_size, true); - sub.filter(app->get_arg(0), equalities, discard_cols, t); - this->subtract(sub); - return;} - - case OP_OR: { - union_ternary_bitvector orig(m_bv_size); - swap(orig); - for (unsigned i = 0; i < app->get_num_args(); ++i) { - union_ternary_bitvector tmp(orig); - subset_ints eqs(equalities); - tmp.filter(app->get_arg(i), eqs, discard_cols, t); - add_facts(tmp); - } - return;} - - case OP_TRUE: - return; - - default: - std::cerr << "app decl: " << app->get_decl()->get_name() << " (" << app->get_decl_kind() << ")\n"; - NOT_IMPLEMENTED_YET(); - } - break;} - - case AST_VAR: { - // boolean var must be true (10) - SASSERT(t.column_num_bits(to_var(e)->get_idx()) == 1); - unsigned idx = t.column_idx(to_var(e)->get_idx()); - ternary_bitvector BV(1); - BV.push_back(BIT_1); - T BV2(BV); - fix_eq_bits(idx, &BV2, 0, 2, equalities, discard_cols); - return;} - - default: - break; - } - std::cerr << "expr kind: " << get_ast_kind_name(e->get_kind()) << '\n'; - NOT_IMPLEMENTED_YET(); - } - - public: - void filter(const expr *cond, const bit_vector& discard_cols, const table_information& table) { - // datastructure to store equalities with columns that will be projected out - union_find_default_ctx union_ctx; - subset_ints equalities(union_ctx); - for (unsigned i = 0, e = discard_cols.size(); i < e; ++i) { - equalities.mk_var(); - } - - filter(cond, equalities, discard_cols, table); - } - - bool contains(const T & fact) const { - for (const_iterator I = begin(), E = end(); I != E; ++I) { - if (I->contains(fact)) - return true; - } - return false; - } - - bool contains(const union_ternary_bitvector & other) const { - for (const_iterator I = other.begin(), E = other.end(); I != E; ++I) { - for (const_iterator II = begin(), EE = end(); II != EE; ++II) { - if (II->contains(*I)) - goto next_iter; - } - return false; -next_iter: ; - } - return true; - } - - unsigned num_disjs() const { - return (unsigned)m_bitvectors.size(); - } - - unsigned num_bytes() const { - unsigned size = sizeof(*this); - for (const_iterator I = begin(), E = end(); I != E; ++I) { - size += I->size_in_bytes(); - } - return size; - } - -#if Z3DEBUG - void expand(std::set & BVs) const { - for (const_iterator I = begin(), E = end(); I != E; ++I) { - I->expand(BVs); - } - } -#endif - - void add_facts(const union_ternary_bitvector & Other, union_ternary_bitvector *Delta = 0) { - for (const_iterator I = Other.begin(), E = Other.end(); I != E; ++I) { - if (add_fact(*I) && Delta) - Delta->add_fact(*I); - } - } - - bool add_fact(const T & fact) { - if (contains(fact)) - return false; - add_new_fact(fact); - return true; - } - - void add_new_fact(const T & fact) { - SASSERT(m_bv_size == fact.size()); - - // TODO: optimize sequence (karnaugh maps??) - // At least join 1-bit different BVs - m_bitvectors.push_back(fact); - } - - void mk_full() { - reset(); - add_new_fact(T(m_bv_size, true)); - } - - typedef typename union_t::const_iterator const_iterator; - - const_iterator begin() const { return m_bitvectors.begin(); } - const_iterator end() const { return m_bitvectors.end(); } - - bool empty() const { return m_bitvectors.empty(); } - void reset() { m_bitvectors.clear(); } - - void swap(union_ternary_bitvector& other) { - SASSERT(m_bv_size == other.m_bv_size); - m_bitvectors.swap(other.m_bitvectors); - } - - void display(std::ostream & out) const { - out << '#' << num_disjs() << " (bv" << m_bv_size << ") "; - - bool first = true; - for (const_iterator I = begin(), E = end(); I != E; ++I) { - if (!first) - out << " \\/ "; - first = false; - I->display(out); - } - out << '\n'; - } - }; - - - template - class common_hassel_table_plugin : public table_plugin { - public: - common_hassel_table_plugin(symbol &s, relation_manager & manager) : - table_plugin(s, manager) { } - - virtual table_base * mk_empty(const table_signature & s) { - return alloc(T, *this, s); - } - - virtual table_base * mk_full(func_decl* p, const table_signature & s) { - T *t = static_cast(mk_empty(s)); - t->mk_full(); - return t; - } - - virtual bool can_handle_signature(const table_signature & s) { - return s.functional_columns() == 0; - } - - private: - ast_manager& get_ast_manager() { return get_context().get_manager(); } - - class join_fn : public convenient_table_join_fn { - public: - join_fn(const T & t1, const T & t2, unsigned col_cnt, const unsigned *cols1, const unsigned *cols2) - : convenient_table_join_fn(t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2) { - t1.expand_column_vector(m_cols1); - t2.expand_column_vector(m_cols2); - } - - virtual table_base * operator()(const table_base & tb1, const table_base & tb2) { - const T & T1 = static_cast(tb1); - const T & T2 = static_cast(tb2); - T * Res = static_cast(T1.get_plugin().mk_empty(get_result_signature())); - T1.m_bitsets.join(T2.m_bitsets, m_cols1, m_cols2, Res->m_bitsets); - TRACE("dl_hassel", tout << "final size: " << Res->get_size_estimate_rows() << '\n';); - return Res; - } - }; - - public: - virtual table_join_fn * mk_join_fn(const table_base & t1, const table_base & t2, - unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) { - if (!check_kind(t1) || !check_kind(t2)) - return 0; - return alloc(join_fn, static_cast(t1), static_cast(t2), col_cnt, cols1, cols2); - } - - private: - class union_fn : public table_union_fn { - public: - virtual void operator()(table_base & tgt0, const table_base & src0, table_base * delta0) { - T & tgt = static_cast(tgt0); - const T & src = static_cast(src0); - T * delta = static_cast(delta0); - tgt.m_bitsets.add_facts(src.m_bitsets, delta ? &delta->m_bitsets : 0); - TRACE("dl_hassel", tout << "final size: " << tgt.get_size_estimate_rows() << '\n';); - } - }; - - public: - virtual table_union_fn * mk_union_fn(const table_base & tgt, const table_base & src, - const table_base * delta) { - if (!check_kind(tgt) || !check_kind(src)) - return 0; - return alloc(union_fn); - } - - private: - class project_fn : public convenient_table_project_fn { - public: - project_fn(const T & t, unsigned removed_col_cnt, const unsigned * removed_cols) - : convenient_table_project_fn(t.get_signature(), removed_col_cnt, removed_cols) { - t.expand_column_vector(m_removed_cols); - m_removed_cols.push_back(UINT_MAX); - } - - virtual table_base * operator()(const table_base & tb) { - const T & t = static_cast(tb); - T * res = static_cast(t.get_plugin().mk_empty(get_result_signature())); - t.m_bitsets.project(m_removed_cols, res->m_bitsets); - TRACE("dl_hassel", tout << "final size: " << res->get_size_estimate_rows() << '\n';); - return res; - } - }; - - public: - virtual table_transformer_fn * mk_project_fn(const table_base & t, unsigned col_cnt, - const unsigned * removed_cols) { - if (!check_kind(t)) - return 0; - return alloc(project_fn, static_cast(t), col_cnt, removed_cols); - } - - private: - class rename_fn : public convenient_table_rename_fn { - unsigned_vector m_out_of_cycle; - public: - rename_fn(const table_signature & orig_sig, unsigned permutation_cycle_len, const unsigned * permutation_cycle) - : convenient_table_rename_fn(orig_sig, permutation_cycle_len, permutation_cycle) { - SASSERT(permutation_cycle_len >= 2); - idx_set cycle_cols; - for (unsigned i = 0; i < permutation_cycle_len; ++i) { - cycle_cols.insert(permutation_cycle[i]); - } - for (unsigned i = 0; i < orig_sig.size(); ++i) { - if (!cycle_cols.contains(i)) - m_out_of_cycle.push_back(i); - } - } - - virtual table_base * operator()(const table_base & tb) { - const T & t = static_cast(tb); - T * res = static_cast(t.get_plugin().mk_empty(get_result_signature())); - t.m_bitsets.rename(m_cycle, m_out_of_cycle, t, *res, res->m_bitsets); - TRACE("dl_hassel", tout << "final size: " << res->get_size_estimate_rows() << '\n';); - return res; - } - }; - - public: - virtual table_transformer_fn * mk_rename_fn(const table_base & t, unsigned permutation_cycle_len, - const unsigned * permutation_cycle) { - if (!check_kind(t)) - return 0; - return alloc(rename_fn, t.get_signature(), permutation_cycle_len, permutation_cycle); - } - - private: - class filter_equal_fn : public table_mutator_fn { - typename T::bitset_t m_filter; - public: - filter_equal_fn(const T & t, const table_element val, unsigned col) : - m_filter(t.get_num_bits()) { - ternary_bitvector filter_row(t.get_num_bits(), true); - ternary_bitvector column(val, t.column_num_bits(col)); - filter_row.mk_idx_eq(t.column_idx(col), column); - m_filter.add_new_fact(filter_row); - } - - virtual void operator()(table_base & tb) { - T & t = static_cast(tb); - t.m_bitsets.swap(m_filter.and(t.m_bitsets)); - TRACE("dl_hassel", tout << "final size: " << t.get_size_estimate_rows() << '\n';); - } - }; - - public: - virtual table_mutator_fn * mk_filter_equal_fn(const table_base & t, const table_element & value, - unsigned col) { - if (!check_kind(t)) - return 0; - return alloc(filter_equal_fn, static_cast(t), value, col); - } - - private: - static bool cond_is_guard(const expr *e, const table_information& t) { - switch (e->get_kind()) { - case AST_APP: { - const app *app = to_app(e); - switch (app->get_decl_kind()) { - case OP_AND: - case OP_OR: - case OP_NOT: - for (unsigned i = 0; i < app->get_num_args(); ++i) { - if (!cond_is_guard(app->get_arg(i), t)) - return false; - } - return true; - - case OP_EQ: { - const expr *a = app->get_arg(0), *b = app->get_arg(1); - - // column equality is not succinctly representable with TBVs - if (is_var(a) && is_var(b)) - return false; - - // (= var (concat var foo)) - if (t.get_bv_util().is_concat(b)) - return false; - - return true;} - - case OP_FALSE: - case OP_TRUE: - return true; - - default: - return false; - } - break;} - - case AST_VAR: - return true; - - default: - break; - } - return false; - } - - static void split_cond_guard(app *cond, expr_ref& guard, expr_ref& leftover, const table_information& t) { - expr_ref_vector guards(guard.m()); - expr_ref_vector leftovers(leftover.m()); - - if (is_app(cond) && to_app(cond)->get_decl_kind() == OP_AND) { - app *a = to_app(cond); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - expr *arg = a->get_arg(i); - if (cond_is_guard(arg, t)) { - guards.push_back(arg); - } else { - leftovers.push_back(arg); - } - } - } else if (cond_is_guard(cond, t)) { - guard = cond; - return; - } else { - leftover = cond; - return; - } - - if (guards.size() > 1) { - guard = formula_to_dnf(expr_ref(guard.m().mk_and(guards.size(), guards.c_ptr()), guard.m())); - } else if (guards.size() == 1) { - guard = guards.get(0); - } - - if (leftovers.size() > 1) { - leftover = formula_to_dnf(expr_ref(leftover.m().mk_and(leftovers.size(), leftovers.c_ptr()), leftover.m())); - } else if (leftovers.size() == 1) { - leftover = leftovers.get(0); - } - } - - class filter_fn : public table_mutator_fn { - expr_ref m_condition; - typename T::bitset_t m_filter; - bit_vector m_empty_bv; - public: - filter_fn(const T & t, ast_manager& m, app *condition) : - m_condition(m), m_filter(t.get_num_bits(), true) { - m_empty_bv.resize(t.get_num_bits(), false); - - expr_ref guard(m); - split_cond_guard(condition, guard, m_condition, t); - if (guard) - m_filter.filter(guard, m_empty_bv, t); - } - - virtual void operator()(table_base & tb) { - T & t = static_cast(tb); - // first apply guard and then run the interpreter on the leftover - t.m_bitsets.swap(m_filter.and(t.m_bitsets)); - if (m_condition) - t.m_bitsets.filter(m_condition, m_empty_bv, t); - TRACE("dl_hassel", tout << "final size: " << t.get_size_estimate_rows() << '\n';); - } - }; - - public: - virtual table_mutator_fn * mk_filter_interpreted_fn(const table_base & t, app * condition) { - if (!check_kind(t)) - return 0; - TRACE("dl_hassel", tout << mk_pp(condition, get_ast_manager()) << '\n';); - return alloc(filter_fn, static_cast(t), get_ast_manager(), condition); - } - - private: - class filter_proj_fn : public convenient_table_project_fn { - expr_ref m_condition; - typename T::bitset_t m_filter; - bit_vector m_col_list; // map: col idx -> bool (whether the column is to be removed) - public: - filter_proj_fn(const T & t, ast_manager& m, app *condition, - unsigned col_cnt, const unsigned * removed_cols) : - convenient_table_project_fn(t.get_signature(), col_cnt, removed_cols), - m_condition(m), m_filter(t.get_num_bits(), true) { - t.expand_column_vector(m_removed_cols); - - m_col_list.resize(t.get_num_bits(), false); - for (unsigned i = 0; i < m_removed_cols.size(); ++i) { - m_col_list.set(m_removed_cols[i]); - } - m_removed_cols.push_back(UINT_MAX); - - expr_ref guard(m); - split_cond_guard(condition, guard, m_condition, t); - if (guard) - m_filter.filter(guard, m_col_list, t); - } - - virtual table_base* operator()(const table_base & tb) { - const T & t = static_cast(tb); - // first apply guard and then run the interpreter on the leftover - typename T::bitset_t filtered(t.get_num_bits()); - filtered.swap(m_filter.and(t.m_bitsets)); - if (m_condition) - filtered.filter(m_condition, m_col_list, t); - - T * res = static_cast(t.get_plugin().mk_empty(get_result_signature())); - filtered.project(m_removed_cols, res->m_bitsets); - TRACE("dl_hassel", tout << "final size: " << res->get_size_estimate_rows() << '\n';); - return res; - } - }; - - public: - virtual table_transformer_fn * mk_filter_interpreted_and_project_fn(const table_base & t, app * condition, - unsigned removed_col_cnt, const unsigned * removed_cols) { - if (!check_kind(t)) - return 0; - TRACE("dl_hassel", tout << mk_pp(condition, get_ast_manager()) << '\n';); - return alloc(filter_proj_fn, static_cast(t), get_ast_manager(), - condition, removed_col_cnt, removed_cols); - } - - - virtual table_intersection_filter_fn * mk_filter_by_negation_fn(const table_base & t, - const table_base & negated_obj, unsigned joined_col_cnt, const unsigned * t_cols, - const unsigned * negated_cols) { - NOT_IMPLEMENTED_YET(); - } - }; - - template - class common_hassel_table : public table_base, public table_information { - public: - typedef T bitset_t; - - common_hassel_table(table_plugin & p, const table_signature & sig) : - table_base(p, sig), table_information(p, sig), m_bitsets(get_num_bits()) { } - - virtual table_base * complement(func_decl* p, const table_element * func_columns = 0) const { - SASSERT(!func_columns); - - if (empty()) - return get_plugin().mk_full(p, get_signature()); - - common_hassel_table *res = static_cast(get_plugin().mk_empty(get_signature())); - res->m_bitsets.swap(m_bitsets.neg()); - return res; - } - - virtual void add_fact(const table_fact & f) { - m_bitsets.add_fact(ternary_bitvector(f, *this)); - } - - virtual void add_new_fact(const table_fact & f) { - m_bitsets.add_new_fact(ternary_bitvector(f, *this)); - } - - virtual void remove_fact(table_element const* fact) { - NOT_IMPLEMENTED_YET(); - } - - virtual void reset() { - m_bitsets.reset(); - } - - void mk_full() { - m_bitsets.mk_full(); - } - - virtual table_base * clone() const { - common_hassel_table *res = static_cast(get_plugin().mk_empty(get_signature())); - res->m_bitsets = m_bitsets; - return res; - } - - virtual bool contains_fact(const table_fact & f) { - return m_bitsets.contains(ternary_bitvector(f, *this)); - } - - virtual bool empty() const { - return m_bitsets.empty(); - } - -#if Z3DEBUG - class our_iterator_core : public iterator_core { - class our_row : public row_interface { - const our_iterator_core & m_parent; - const table_information& m_table; - public: - our_row(const common_hassel_table & t, const our_iterator_core & parent) : - row_interface(t), m_parent(parent), m_table(t) {} - - virtual table_element operator[](unsigned col) const { - return m_parent.it->to_number(m_table.column_idx(col), m_table.column_num_bits(col)); - } - }; - - our_row m_row_obj; - std::set BVs; - std::set::iterator it; - - public: - our_iterator_core(const common_hassel_table & t, bool finished) : - m_row_obj(t, *this) { - if (finished) { - it = BVs.end(); - return; - } - t.m_bitsets.expand(BVs); - it = BVs.begin(); - } - - virtual bool is_finished() const { - return it == BVs.end(); - } - - virtual row_interface & operator*() { - SASSERT(!is_finished()); - return m_row_obj; - } - - virtual void operator++() { - SASSERT(!is_finished()); - ++it; - } - }; -#endif - - virtual iterator begin() const { -#if Z3DEBUG - return mk_iterator(alloc(our_iterator_core, *this, false)); -#else - SASSERT(0 && "begin() disabled"); - return mk_iterator(0); -#endif - } - - virtual iterator end() const { -#if Z3DEBUG - return mk_iterator(alloc(our_iterator_core, *this, true)); -#else - SASSERT(0 && "end() disabled"); - return mk_iterator(0); -#endif - } - - virtual void display(std::ostream & out) const { - table_information::display(out); - m_bitsets.display(out); - } - - virtual void to_formula(relation_signature const& sig, expr_ref& fml) const { - // TODO - } - - virtual unsigned get_size_estimate_rows() const { - return m_bitsets.num_disjs(); - } - - virtual unsigned get_size_estimate_bytes() const { - return m_bitsets.num_bytes(); - } - - T m_bitsets; - }; - -} - -#endif diff --git a/src/muz_qe/dl_hassel_diff_table.cpp b/src/muz_qe/dl_hassel_diff_table.cpp deleted file mode 100755 index 3ddcb3bbe..000000000 --- a/src/muz_qe/dl_hassel_diff_table.cpp +++ /dev/null @@ -1,219 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - dl_hassel_diff_table.cpp - -Abstract: - - - -Revision History: - ---*/ - -#include "ast_printer.h" -#include "dl_context.h" -#include "dl_util.h" -#include "dl_hassel_diff_table.h" - - -namespace datalog { - - ternary_diff_bitvector::ternary_diff_bitvector(unsigned size, bool full) : - m_pos(size, full), m_neg(size) { } - - ternary_diff_bitvector::ternary_diff_bitvector(uint64 n, unsigned num_bits) : - m_pos(n, num_bits), m_neg(num_bits) { } - - ternary_diff_bitvector::ternary_diff_bitvector(const ternary_bitvector & tbv) : - m_pos(tbv), m_neg(tbv.size()) { } - - bool ternary_diff_bitvector::contains(const ternary_diff_bitvector & other) const { - return m_pos.contains(other.m_pos) && other.m_neg.contains(m_neg); - } - - bool ternary_diff_bitvector::is_empty() const { - if (m_pos.is_empty()) - return true; - - return m_neg.contains(m_pos); - } - - ternary_diff_bitvector ternary_diff_bitvector::and(const ternary_diff_bitvector& other) const { - ternary_diff_bitvector result(m_pos.and(other.m_pos)); - result.m_neg.swap(m_neg.or(other.m_neg)); - return result; - } - - void ternary_diff_bitvector::neg(union_ternary_bitvector& result) const { - // not(A\B) <-> (T\A) U B - ternary_diff_bitvector negated(size(), true); - negated.m_neg.add_new_fact(m_pos); - result.add_fact(negated); - - for (union_ternary_bitvector::const_iterator I = m_neg.begin(), - E = m_neg.end(); I != E; ++I) { - result.add_fact(*I); - } - } - - void ternary_diff_bitvector::subtract(const union_ternary_bitvector& other, - union_ternary_bitvector& result) const { - ternary_diff_bitvector newfact(*this); - for (union_ternary_bitvector::const_iterator I = other.begin(), - E = other.end(); I != E; ++I) { - if (!I->m_neg.empty()) { - NOT_IMPLEMENTED_YET(); - } - newfact.m_neg.add_fact(I->m_pos); - } - - if (!newfact.is_empty()) - result.add_fact(newfact); - } - - void ternary_diff_bitvector::join(const ternary_diff_bitvector& other, - const unsigned_vector& cols1, - const unsigned_vector& cols2, - union_ternary_bitvector& result) const { - unsigned new_size = size() + other.size(); - ternary_diff_bitvector res(new_size); - - res.m_pos = m_pos; - res.m_pos.append(other.m_pos); - - for (unsigned i = 0; i < cols1.size(); ++i) { - unsigned idx1 = cols1[i]; - unsigned idx2 = size() + cols2[i]; - unsigned v1 = res.m_pos.get(idx1); - unsigned v2 = res.m_pos.get(idx2); - - if (v1 == BIT_x) { - if (v2 == BIT_x) { - // add to subtracted TBVs: 1xx0 and 0xx1 - { - ternary_bitvector r(new_size, true); - r.set(idx1, BIT_0); - r.set(idx2, BIT_1); - res.m_neg.add_new_fact(r); - } - { - ternary_bitvector r(new_size, true); - r.set(idx1, BIT_1); - r.set(idx2, BIT_0); - res.m_neg.add_new_fact(r); - } - } else { - res.m_pos.set(idx1, v2); - } - } else if (v2 == BIT_x) { - res.m_pos.set(idx2, v1); - } else if (v1 != v2) { - // columns don't match - return; - } - } - - // handle subtracted TBVs: 1010 -> 1010xxx - if (!m_neg.empty()) { - ternary_bitvector padding(other.size(), true); - for (union_ternary_bitvector::const_iterator I = m_neg.begin(), - E = m_neg.end(); I != E; ++I) { - ternary_bitvector BV(*I); - BV.append(padding); - res.m_neg.add_new_fact(BV); - } - } - - if (!other.m_neg.empty()) { - ternary_bitvector padding(size(), true); - for (union_ternary_bitvector::const_iterator I = other.m_neg.begin(), - E = other.m_neg.end(); I != E; ++I) { - ternary_bitvector BV(padding); - BV.append(*I); - res.m_neg.add_new_fact(BV); - } - } - - result.add_fact(res); - } - - bool ternary_diff_bitvector::project(const unsigned_vector& delcols, ternary_diff_bitvector& result) const { - m_pos.project(delcols, result.m_pos); - if (m_neg.empty()) - return true; - - ternary_bitvector newneg; - for (union_ternary_bitvector::const_iterator I = m_neg.begin(), - E = m_neg.end(); I != E; ++I) { - for (unsigned i = 0; i < delcols.size()-1; ++i) { - unsigned idx = delcols[i]; - if (I->get(idx) != BIT_x && m_pos.get(idx) == BIT_x) - goto skip_row; - } - newneg.reset(); - I->project(delcols, newneg); - result.m_neg.add_fact(newneg); -skip_row: ; - } - return !result.is_empty(); - } - - void ternary_diff_bitvector::rename(const unsigned_vector& cyclecols, - const unsigned_vector& out_of_cycle_cols, - const table_information& src_table, - const table_information& dst_table, - ternary_diff_bitvector& result) const { - m_pos.rename(cyclecols, out_of_cycle_cols, src_table, dst_table, result.m_pos); - m_neg.rename(cyclecols, out_of_cycle_cols, src_table, dst_table, result.m_neg); - } - - unsigned ternary_diff_bitvector::get(unsigned idx) { - return m_pos.get(idx); - } - - void ternary_diff_bitvector::set(unsigned idx, unsigned val) { - m_pos.set(idx, val); - } - - void ternary_diff_bitvector::swap(ternary_diff_bitvector & other) { - m_pos.swap(other.m_pos); - m_neg.swap(other.m_neg); - } - - void ternary_diff_bitvector::reset() { - m_pos.reset(); - m_neg.reset(); - } - - void ternary_diff_bitvector::display(std::ostream & out) const { - m_pos.display(out); - if (!m_neg.empty()) { - out << " \\ "; - if (m_neg.num_disjs() > 1) out << '('; - m_neg.display(out); - if (m_neg.num_disjs() > 1) out << ')'; - } - } - - unsigned ternary_diff_bitvector::size_in_bytes() const { - return m_pos.size_in_bytes() + m_neg.num_bytes(); - } - -#if Z3DEBUG - void ternary_diff_bitvector::expand(std::set & BVs) const { - m_pos.expand(BVs); - SASSERT(!BVs.empty()); - - std::set NegBVs; - m_neg.expand(NegBVs); - BVs.erase(NegBVs.begin(), NegBVs.end()); - } -#endif - - hassel_diff_table_plugin::hassel_diff_table_plugin(relation_manager & manager) - : common_hassel_table_plugin(symbol("hassel_diff"), manager) {} - -} diff --git a/src/muz_qe/dl_hassel_diff_table.h b/src/muz_qe/dl_hassel_diff_table.h deleted file mode 100755 index 07340c7e8..000000000 --- a/src/muz_qe/dl_hassel_diff_table.h +++ /dev/null @@ -1,87 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - dl_hassel_diff_table.h - -Abstract: - - - -Revision History: - ---*/ - -#ifndef _DL_HASSEL_DIFF_TABLE_H_ -#define _DL_HASSEL_DIFF_TABLE_H_ - -#include "dl_hassel_common.h" - -namespace datalog { - - class hassel_diff_table; - - class ternary_diff_bitvector { - // pos \ (neg0 \/ ... \/ negn) - ternary_bitvector m_pos; - union_ternary_bitvector m_neg; - - public: - ternary_diff_bitvector() : m_pos(), m_neg(0) {} - ternary_diff_bitvector(unsigned size) : m_pos(size), m_neg(size) {} - ternary_diff_bitvector(unsigned size, bool full); - ternary_diff_bitvector(uint64 n, unsigned num_bits); - ternary_diff_bitvector(const ternary_bitvector & tbv); - - bool contains(const ternary_diff_bitvector & other) const; - bool is_empty() const; - - ternary_diff_bitvector and(const ternary_diff_bitvector& other) const; - void neg(union_ternary_bitvector& result) const; - - static bool has_subtract() { return true; } - void subtract(const union_ternary_bitvector& other, - union_ternary_bitvector& result) const; - - void join(const ternary_diff_bitvector& other, const unsigned_vector& cols1, - const unsigned_vector& cols2, union_ternary_bitvector& result) const; - - bool project(const unsigned_vector& delcols, ternary_diff_bitvector& result) const; - - void rename(const unsigned_vector& cyclecols, const unsigned_vector& out_of_cycle_cols, - const table_information& src_table, const table_information& dst_table, - ternary_diff_bitvector& result) const; - - unsigned get(unsigned idx); - void set(unsigned idx, unsigned val); - - void swap(ternary_diff_bitvector & other); - void reset(); - - unsigned size() const { return m_pos.size(); } - - void display(std::ostream & out) const; - unsigned size_in_bytes() const; - -#if Z3DEBUG - void expand(std::set & BVs) const; -#endif - }; - - typedef union_ternary_bitvector union_ternary_diff_bitvector; - - class hassel_diff_table : public common_hassel_table { - public: - hassel_diff_table(table_plugin & p, const table_signature & sig) : - common_hassel_table(p, sig) {} - }; - - class hassel_diff_table_plugin : public common_hassel_table_plugin { - public: - hassel_diff_table_plugin(relation_manager & manager); - }; - -} - -#endif diff --git a/src/muz_qe/dl_hassel_table.cpp b/src/muz_qe/dl_hassel_table.cpp deleted file mode 100644 index 6ec28df87..000000000 --- a/src/muz_qe/dl_hassel_table.cpp +++ /dev/null @@ -1,27 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - dl_hassel_table.cpp - -Abstract: - - - -Revision History: - ---*/ - -#include "ast_printer.h" -#include "dl_context.h" -#include "dl_util.h" -#include "dl_hassel_table.h" - - -namespace datalog { - - hassel_table_plugin::hassel_table_plugin(relation_manager & manager) - : common_hassel_table_plugin(symbol("hassel"), manager) {} - -} diff --git a/src/muz_qe/dl_hassel_table.h b/src/muz_qe/dl_hassel_table.h deleted file mode 100644 index 6c4e9c1fe..000000000 --- a/src/muz_qe/dl_hassel_table.h +++ /dev/null @@ -1,39 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - dl_hassel_table.h - -Abstract: - - - -Revision History: - ---*/ - -#ifndef _DL_HASSEL_TABLE_H_ -#define _DL_HASSEL_TABLE_H_ - -#include "dl_hassel_common.h" - -namespace datalog { - - class hassel_table; - typedef union_ternary_bitvector union_ternary_bitvectors; - - class hassel_table : public common_hassel_table { - public: - hassel_table(table_plugin & p, const table_signature & sig) : - common_hassel_table(p, sig) {} - }; - - class hassel_table_plugin : public common_hassel_table_plugin { - public: - hassel_table_plugin(relation_manager & manager); - }; - -} - -#endif diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index dcfbcca2b..76f744325 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1561,15 +1561,16 @@ namespace pdr { m_fparams.m_arith_auto_config_simplex = true; m_fparams.m_arith_propagate_eqs = false; m_fparams.m_arith_eager_eq_axioms = false; - if (classify.is_utvpi() && m_params.use_utvpi()) { + if (classify.is_dl()) { + m_fparams.m_arith_mode = AS_DIFF_LOGIC; + m_fparams.m_arith_expand_eqs = true; + } + else if (classify.is_utvpi() && m_params.use_utvpi()) { IF_VERBOSE(1, verbose_stream() << "UTVPI\n";); m_fparams.m_arith_mode = AS_UTVPI; m_fparams.m_arith_expand_eqs = true; } - else if (classify.is_dl()) { - m_fparams.m_arith_mode = AS_DIFF_LOGIC; - m_fparams.m_arith_expand_eqs = true; - } + } if (!use_mc && m_params.use_inductive_generalizer()) { m_core_generalizers.push_back(alloc(core_bool_inductive_generalizer, *this, 0)); diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp index 3d61c04f0..7aade28e2 100644 --- a/src/muz_qe/rel_context.cpp +++ b/src/muz_qe/rel_context.cpp @@ -19,7 +19,6 @@ Revision History: --*/ -#define Z3_HASSEL_TABLE #include"rel_context.h" #include"dl_context.h" @@ -33,10 +32,6 @@ Revision History: #include"dl_mk_karr_invariants.h" #include"dl_finite_product_relation.h" #include"dl_sparse_table.h" -#ifdef Z3_HASSEL_TABLE -# include"dl_hassel_table.h" -# include"dl_hassel_diff_table.h" -#endif #include"dl_table.h" #include"dl_table_relation.h" #include"aig_exporter.h" @@ -94,10 +89,6 @@ namespace datalog { get_rmanager().register_plugin(alloc(bitvector_table_plugin, get_rmanager())); get_rmanager().register_plugin(alloc(equivalence_table_plugin, get_rmanager())); -#ifdef Z3_HASSEL_TABLE - get_rmanager().register_plugin(alloc(hassel_table_plugin, get_rmanager())); - get_rmanager().register_plugin(alloc(hassel_diff_table_plugin, get_rmanager())); -#endif // register plugins for builtin relations diff --git a/src/smt/database.smt b/src/smt/database.smt index 186dd9b95..2f5e5e1c9 100644 --- a/src/smt/database.smt +++ b/src/smt/database.smt @@ -311,4 +311,4 @@ (= (?is (?select (?select (?asElems e) a) i) (?elemtype (?typeof a))) 1) :pats { (?select (?select (?asElems e) a) i) }) - ) \ No newline at end of file + ) diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index 6c85e40b9..498a2a172 100644 --- a/src/smt/theory_utvpi_def.h +++ b/src/smt/theory_utvpi_def.h @@ -418,9 +418,6 @@ namespace smt { return FC_GIVEUP; } else { - m_graph.set_to_zero(to_var(m_zero_int), to_var(m_zero_real)); - m_graph.set_to_zero(neg(to_var(m_zero_int)), neg(to_var(m_zero_real))); - m_graph.set_to_zero(to_var(m_zero_int), neg(to_var(m_zero_int))); return FC_DONE; } } @@ -691,16 +688,33 @@ namespace smt { \brief adjust values for variables in the difference graph such that for variables of integer sort it is the case that x^+ - x^- is even. - The informal justification for the procedure enforce_parity is that - the graph does not contain a strongly connected component where - x^+ and x+- are connected. They can be independently changed. - Since we would like variables representing 0 (zero) map to 0, - we selectively update the subgraph that can be updated without - changing the value of zero (which should be 0). + The informal justification for the procedure enforce_parity relies + on a set of properties: + 1. the graph does not contain a strongly connected component where + x^+ and x+- are connected. They can be independently changed. + This is checked prior to enforce_parity. + 2. When x^+ - x^- is odd, the values are adjusted by first + decrementing the value of x^+, provided x^- is not 0-dependent. + Otherwise decrement x^-. + x^- is "0-dependent" if there is a set of tight + inequalities from x^+ to x^-. + 3. The affinity to x^+ (the same component of x^+) ensures that + the parity is broken only a finite number of times when + traversing that component. Namely, suppose that the parity of y + gets broken when fixing 'x'. Then first note that 'y' cannot + be equal to 'x'. If it were, then we have a state where: + parity(x^+) != parity(x^-) and + parity(y^+) == parity(y^-) + but x^+ and y^+ are tightly connected and x^- and y^- are + also tightly connected using two copies of the same inequalities. + This is a contradiction. + Thus, 'y' cannot be equal to 'x' if 'y's parity gets broken when + repairing 'x'. + */ template void theory_utvpi::enforce_parity() { - unsigned_vector todo; + unsigned_vector todo; unsigned sz = get_num_vars(); for (unsigned i = 0; i < sz; ++i) { @@ -712,6 +726,8 @@ namespace smt { if (todo.empty()) { return; } + IF_VERBOSE(2, verbose_stream() << "disparity: " << todo.size() << "\n";); + unsigned iter = 0; while (!todo.empty()) { unsigned i = todo.back(); todo.pop_back(); @@ -720,21 +736,17 @@ namespace smt { } th_var v1 = to_var(i); th_var v2 = neg(v1); - TRACE("utvpi", tout << "disparity: " << v1 << "\n";); + + // IF_VERBOSE(1, verbose_stream() << "disparity: " << v1 << "\n";); int_vector zero_v; m_graph.compute_zero_succ(v1, zero_v); - bool found0 = false; - for (unsigned j = 0; !found0 && j < zero_v.size(); ++j) { - found0 = - (to_var(m_zero_int) == zero_v[j]) || - (neg(to_var(m_zero_int)) == zero_v[j]); - } - // variables that are tightly connected - // to 0 should not have their values changed. - if (found0) { - zero_v.reset(); - m_graph.compute_zero_succ(v2, zero_v); + for (unsigned j = 0; j < zero_v.size(); ++j) { + if (zero_v[j] == v2) { + zero_v.reset(); + m_graph.compute_zero_succ(v2, zero_v); + } } + TRACE("utvpi", for (unsigned j = 0; j < zero_v.size(); ++j) { tout << "decrement: " << zero_v[j] << "\n"; @@ -745,10 +757,23 @@ namespace smt { m_graph.acc_assignment(v, numeral(-1)); th_var k = from_var(v); if (!is_parity_ok(k)) { - TRACE("utvpi", tout << "new disparity: " << k << "\n";); + // IF_VERBOSE(1, verbose_stream() << "new disparity: " << k << "\n";); todo.push_back(k); } - } + } + if (iter >= 10000) { + IF_VERBOSE(1, + verbose_stream() << "decrement: "; + for (unsigned j = 0; j < zero_v.size(); ++j) { + rational r = m_graph.get_assignment(zero_v[j]).get_rational(); + verbose_stream() << zero_v[j] << " (" << r << ") "; + } + verbose_stream() << "\n";); + if (!is_parity_ok(i)) { + IF_VERBOSE(1, verbose_stream() << "Parity not fixed\n";); + } + } + ++iter; } SASSERT(m_graph.is_feasible()); DEBUG_CODE( @@ -764,10 +789,13 @@ namespace smt { // models: template - void theory_utvpi::init_model(model_generator & m) { + void theory_utvpi::init_model(model_generator & m) { m_factory = alloc(arith_factory, get_manager()); m.register_factory(m_factory); enforce_parity(); + m_graph.set_to_zero(to_var(m_zero_int), to_var(m_zero_real)); + m_graph.set_to_zero(neg(to_var(m_zero_int)), neg(to_var(m_zero_real))); + m_graph.set_to_zero(to_var(m_zero_int), neg(to_var(m_zero_int))); compute_delta(); DEBUG_CODE(validate_model();); }