diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index c4b5c97d7..6855f6209 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1070,6 +1070,10 @@ extern "C" { case OP_BV2INT: return Z3_OP_BV2INT; case OP_CARRY: return Z3_OP_CARRY; case OP_XOR3: return Z3_OP_XOR3; + case OP_BSMUL_NO_OVFL: + case OP_BUMUL_NO_OVFL: + case OP_BSMUL_NO_UDFL: + return Z3_OP_UNINTERPRETED; default: UNREACHABLE(); return Z3_OP_UNINTERPRETED; diff --git a/src/api/api_bv.cpp b/src/api/api_bv.cpp index 8126c8e2a..07d4fda18 100644 --- a/src/api/api_bv.cpp +++ b/src/api/api_bv.cpp @@ -121,10 +121,20 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ unsigned sz = Z3_get_bv_sort_size(c, s); rational max_bound = power(rational(2), sz); Z3_ast bound = Z3_mk_numeral(c, max_bound.to_string().c_str(), int_s); - Z3_ast pred = Z3_mk_bvslt(c, n, Z3_mk_int(c, 0, s)); + Z3_inc_ref(c, bound); + Z3_ast zero = Z3_mk_int(c, 0, s); + Z3_inc_ref(c, zero); + Z3_ast pred = Z3_mk_bvslt(c, n, zero); + Z3_inc_ref(c, pred); // if n <_sigend 0 then r - s^sz else r Z3_ast args[2] = { r, bound }; - Z3_ast res = Z3_mk_ite(c, pred, Z3_mk_sub(c, 2, args), r); + Z3_ast sub = Z3_mk_sub(c, 2, args); + Z3_inc_ref(c, sub); + Z3_ast res = Z3_mk_ite(c, pred, sub, r); + Z3_dec_ref(c, bound); + Z3_dec_ref(c, pred); + Z3_dec_ref(c, sub); + Z3_dec_ref(c, zero); RETURN_Z3(res); } else { @@ -156,7 +166,14 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } - return Z3_mk_bvshl(c, Z3_mk_int64(c, 1, s), Z3_mk_int64(c, sz - 1, s)); + Z3_ast x = Z3_mk_int64(c, 1, s); + Z3_inc_ref(c, x); + Z3_ast y = Z3_mk_int64(c, sz - 1, s); + Z3_inc_ref(c, y); + Z3_ast result = Z3_mk_bvshl(c, x, y); + Z3_dec_ref(c, x); + Z3_dec_ref(c, y); + return result; Z3_CATCH_RETURN(0); } @@ -177,17 +194,40 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ RESET_ERROR_CODE(); if (is_signed) { Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1)); + Z3_inc_ref(c, zero); Z3_ast r = Z3_mk_bvadd(c, t1, t2); - Z3_ast args[2] = { Z3_mk_bvslt(c, zero, t1), Z3_mk_bvslt(c, zero, t2) }; + Z3_inc_ref(c, r); + Z3_ast l1 = Z3_mk_bvslt(c, zero, t1); + Z3_inc_ref(c, l1); + Z3_ast l2 = Z3_mk_bvslt(c, zero, t2); + Z3_inc_ref(c, l2); + Z3_ast args[2] = { l1, l2 }; Z3_ast args_pos = Z3_mk_and(c, 2, args); - return Z3_mk_implies(c, args_pos, Z3_mk_bvslt(c, zero, r)); + Z3_inc_ref(c, args_pos); + Z3_ast result = Z3_mk_implies(c, args_pos, Z3_mk_bvslt(c, zero, r)); + Z3_dec_ref(c, r); + Z3_dec_ref(c, l1); + Z3_dec_ref(c, l2); + Z3_dec_ref(c, args_pos); + Z3_dec_ref(c, zero); + return result; } else { unsigned sz = Z3_get_bv_sort_size(c, Z3_get_sort(c, t1)); t1 = Z3_mk_zero_ext(c, 1, t1); + Z3_inc_ref(c, t1); t2 = Z3_mk_zero_ext(c, 1, t2); + Z3_inc_ref(c, t2); Z3_ast r = Z3_mk_bvadd(c, t1, t2); - return Z3_mk_eq(c, Z3_mk_extract(c, sz, sz, r), Z3_mk_int(c, 0, Z3_mk_bv_sort(c, 1))); + Z3_inc_ref(c, r); + Z3_ast ex = Z3_mk_extract(c, sz, sz, r); + Z3_inc_ref(c, ex); + Z3_ast result = Z3_mk_eq(c, ex, Z3_mk_int(c, 0, Z3_mk_bv_sort(c, 1))); + Z3_dec_ref(c, t1); + Z3_dec_ref(c, t2); + Z3_dec_ref(c, ex); + Z3_dec_ref(c, r); + return result; } Z3_CATCH_RETURN(0); } @@ -197,10 +237,26 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_TRY; RESET_ERROR_CODE(); Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1)); + Z3_inc_ref(c, zero); Z3_ast r = Z3_mk_bvadd(c, t1, t2); - Z3_ast args[2] = { Z3_mk_bvslt(c, t1, zero), Z3_mk_bvslt(c, t2, zero) }; + Z3_inc_ref(c, r); + Z3_ast l1 = Z3_mk_bvslt(c, t1, zero); + Z3_inc_ref(c, l1); + Z3_ast l2 = Z3_mk_bvslt(c, t2, zero); + Z3_inc_ref(c, l2); + Z3_ast args[2] = { l1, l2 }; Z3_ast args_neg = Z3_mk_and(c, 2, args); - return Z3_mk_implies(c, args_neg, Z3_mk_bvslt(c, r, zero)); + Z3_inc_ref(c, args_neg); + Z3_ast lt = Z3_mk_bvslt(c, r, zero); + Z3_inc_ref(c, lt); + Z3_ast result = Z3_mk_implies(c, args_neg, lt); + Z3_dec_ref(c, lt); + Z3_dec_ref(c, l1); + Z3_dec_ref(c, l2); + Z3_dec_ref(c, r); + Z3_dec_ref(c, args_neg); + Z3_dec_ref(c, zero); + return result; Z3_CATCH_RETURN(0); } @@ -208,12 +264,28 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_ast Z3_API Z3_mk_bvsub_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) { Z3_TRY; RESET_ERROR_CODE(); - Z3_sort s = Z3_get_sort(c, t2); Z3_ast minus_t2 = Z3_mk_bvneg(c, t2); + Z3_inc_ref(c, minus_t2); + Z3_sort s = Z3_get_sort(c, t2); Z3_ast min = Z3_mk_bvsmin(c, s); - return Z3_mk_ite(c, Z3_mk_eq(c, t2, min), - Z3_mk_bvslt(c, t1, Z3_mk_int(c, 0, s)), - Z3_mk_bvadd_no_overflow(c, t1, minus_t2, true)); + Z3_inc_ref(c, min); + Z3_ast x = Z3_mk_eq(c, t2, min); + Z3_inc_ref(c, x); + Z3_ast zero = Z3_mk_int(c, 0, s); + Z3_inc_ref(c, zero); + Z3_ast y = Z3_mk_bvslt(c, t1, zero); + Z3_inc_ref(c, y); + Z3_ast z = Z3_mk_bvadd_no_overflow(c, t1, minus_t2, true); + Z3_inc_ref(c, z); + Z3_ast result = Z3_mk_ite(c, x, y, z); + mk_c(c)->save_ast_trail(to_app(result)); + Z3_dec_ref(c, minus_t2); + Z3_dec_ref(c, min); + Z3_dec_ref(c, x); + Z3_dec_ref(c, y); + Z3_dec_ref(c, z); + Z3_dec_ref(c, zero); + return result; Z3_CATCH_RETURN(0); } @@ -222,10 +294,19 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ RESET_ERROR_CODE(); if (is_signed) { Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1)); - if (Z3_get_error_code(c) != Z3_OK) return 0; + Z3_inc_ref(c, zero); Z3_ast minus_t2 = Z3_mk_bvneg(c, t2); - if (Z3_get_error_code(c) != Z3_OK) return 0; - return Z3_mk_implies(c, Z3_mk_bvslt(c, zero, t2), Z3_mk_bvadd_no_underflow(c, t1, minus_t2)); + Z3_inc_ref(c, minus_t2); + Z3_ast x = Z3_mk_bvslt(c, zero, t2); + Z3_inc_ref(c, x); + Z3_ast y = Z3_mk_bvadd_no_underflow(c, t1, minus_t2); + Z3_inc_ref(c, y); + Z3_ast result = Z3_mk_implies(c, x, y); + Z3_dec_ref(c, zero); + Z3_dec_ref(c, minus_t2); + Z3_dec_ref(c, x); + Z3_dec_ref(c, y); + return result; } else { return Z3_mk_bvule(c, t2, t1); @@ -267,12 +348,24 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_TRY; RESET_ERROR_CODE(); Z3_sort s = Z3_get_sort(c, t1); - if (Z3_get_error_code(c) != Z3_OK) return 0; Z3_ast min = Z3_mk_bvmsb(c, s); - if (Z3_get_error_code(c) != Z3_OK) return 0; - Z3_ast args[2] = { Z3_mk_eq(c, t1, min), - Z3_mk_eq(c, t2, Z3_mk_int(c, -1, s)) }; - return Z3_mk_not(c, Z3_mk_and(c, 2, args)); + Z3_inc_ref(c, min); + Z3_ast x = Z3_mk_eq(c, t1, min); + Z3_inc_ref(c, x); + Z3_ast y = Z3_mk_int(c, -1, s); + Z3_inc_ref(c, y); + Z3_ast z = Z3_mk_eq(c, t2, y); + Z3_inc_ref(c, z); + Z3_ast args[2] = { x, z }; + Z3_ast u = Z3_mk_and(c, 2, args); + Z3_inc_ref(c, u); + Z3_ast result = Z3_mk_not(c, u); + Z3_dec_ref(c, min); + Z3_dec_ref(c, x); + Z3_dec_ref(c, y); + Z3_dec_ref(c, z); + Z3_dec_ref(c, u); + return result; Z3_CATCH_RETURN(0); } 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= & op_names, symbol co op_names.push_back(builtin_name("<=", OP_FLOAT_LE)); op_names.push_back(builtin_name(">=", OP_FLOAT_GE)); + op_names.push_back(builtin_name("isNaN", OP_FLOAT_IS_NAN)); + op_names.push_back(builtin_name("isInfinite", OP_FLOAT_IS_INF)); op_names.push_back(builtin_name("isZero", OP_FLOAT_IS_ZERO)); op_names.push_back(builtin_name("isNZero", OP_FLOAT_IS_NZERO)); op_names.push_back(builtin_name("isPZero", OP_FLOAT_IS_PZERO)); + op_names.push_back(builtin_name("isNormal", OP_FLOAT_IS_NORMAL)); + op_names.push_back(builtin_name("isSubnormal", OP_FLOAT_IS_SUBNORMAL)); op_names.push_back(builtin_name("isSignMinus", OP_FLOAT_IS_SIGN_MINUS)); op_names.push_back(builtin_name("min", OP_FLOAT_MIN)); diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index 4ec17addf..f1b60a91b 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -61,9 +61,13 @@ enum float_op_kind { OP_FLOAT_GT, OP_FLOAT_LE, OP_FLOAT_GE, + OP_FLOAT_IS_NAN, + OP_FLOAT_IS_INF, OP_FLOAT_IS_ZERO, - OP_FLOAT_IS_NZERO, + OP_FLOAT_IS_NORMAL, + OP_FLOAT_IS_SUBNORMAL, OP_FLOAT_IS_PZERO, + OP_FLOAT_IS_NZERO, OP_FLOAT_IS_SIGN_MINUS, OP_TO_FLOAT, @@ -223,7 +227,7 @@ public: app * mk_rem(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_REM, arg1, arg2); } app * mk_max(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_MAX, arg1, arg2); } app * mk_min(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_MIN, arg1, arg2); } - app * mk_abs(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_ABS, arg1, arg2); } + app * mk_abs(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_ABS, arg1); } app * mk_sqrt(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_SQRT, arg1, arg2); } app * mk_round(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_ROUND_TO_INTEGRAL, arg1, arg2); } app * mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4) { @@ -237,7 +241,11 @@ public: app * mk_le(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_LE, arg1, arg2); } app * mk_ge(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_GE, arg1, arg2); } + app * mk_is_nan(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NAN, arg1); } + app * mk_is_inf(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_INF, arg1); } app * mk_is_zero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_ZERO, arg1); } + app * mk_is_normal(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NORMAL, arg1); } + app * mk_is_subnormal(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SUBNORMAL, arg1); } app * mk_is_nzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NZERO, arg1); } app * mk_is_pzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_PZERO, arg1); } app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SIGN_MINUS, arg1); } diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index b43f07b65..015bce0ed 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -58,6 +58,10 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_FLOAT_IS_ZERO: SASSERT(num_args == 1); st = mk_is_zero(args[0], result); break; case OP_FLOAT_IS_NZERO: SASSERT(num_args == 1); st = mk_is_nzero(args[0], result); break; case OP_FLOAT_IS_PZERO: SASSERT(num_args == 1); st = mk_is_pzero(args[0], result); break; + case OP_FLOAT_IS_NAN: SASSERT(num_args == 1); st = mk_is_nan(args[0], result); break; + case OP_FLOAT_IS_INF: SASSERT(num_args == 1); st = mk_is_inf(args[0], result); break; + case OP_FLOAT_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break; + case OP_FLOAT_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break; case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break; case OP_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break; } @@ -428,6 +432,46 @@ br_status float_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) { return BR_FAILED; } +br_status float_rewriter::mk_is_nan(expr * arg1, expr_ref & result) { + scoped_mpf v(m_util.fm()); + if (m_util.is_value(arg1, v)) { + result = (m_util.fm().is_nan(v)) ? m().mk_true() : m().mk_false(); + return BR_DONE; + } + + return BR_FAILED; +} + +br_status float_rewriter::mk_is_inf(expr * arg1, expr_ref & result) { + scoped_mpf v(m_util.fm()); + if (m_util.is_value(arg1, v)) { + result = (m_util.fm().is_inf(v)) ? m().mk_true() : m().mk_false(); + return BR_DONE; + } + + return BR_FAILED; +} + +br_status float_rewriter::mk_is_normal(expr * arg1, expr_ref & result) { + scoped_mpf v(m_util.fm()); + if (m_util.is_value(arg1, v)) { + result = (m_util.fm().is_normal(v)) ? m().mk_true() : m().mk_false(); + return BR_DONE; + } + + return BR_FAILED; +} + +br_status float_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) { + scoped_mpf v(m_util.fm()); + if (m_util.is_value(arg1, v)) { + result = (m_util.fm().is_denormal(v)) ? m().mk_true() : m().mk_false(); + return BR_DONE; + } + + return BR_FAILED; +} + br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) { scoped_mpf v(m_util.fm()); if (m_util.is_value(arg1, v)) { diff --git a/src/ast/rewriter/float_rewriter.h b/src/ast/rewriter/float_rewriter.h index 7c86a5bc3..4a0879d4b 100644 --- a/src/ast/rewriter/float_rewriter.h +++ b/src/ast/rewriter/float_rewriter.h @@ -66,6 +66,10 @@ public: br_status mk_is_zero(expr * arg1, expr_ref & result); br_status mk_is_nzero(expr * arg1, expr_ref & result); br_status mk_is_pzero(expr * arg1, expr_ref & result); + br_status mk_is_nan(expr * arg1, expr_ref & result); + br_status mk_is_inf(expr * arg1, expr_ref & result); + br_status mk_is_normal(expr * arg1, expr_ref & result); + br_status mk_is_subnormal(expr * arg1, expr_ref & result); br_status mk_is_sign_minus(expr * arg1, expr_ref & result); br_status mk_to_ieee_bv(expr * arg1, expr_ref & result); diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index 290144c75..036221f96 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -1,932 +1,932 @@ -/*++ -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()); -} +/*++ +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/ast/simplifier/bv_simplifier_plugin.cpp b/src/ast/simplifier/bv_simplifier_plugin.cpp index 3ef55baba..8ee353a76 100644 --- a/src/ast/simplifier/bv_simplifier_plugin.cpp +++ b/src/ast/simplifier/bv_simplifier_plugin.cpp @@ -636,7 +636,31 @@ bool bv_simplifier_plugin::try_mk_extract(unsigned high, unsigned low, expr * ar if (!all_found) { return false; } - result = m_manager.mk_app(m_fid, a->get_decl_kind(), new_args.size(), new_args.c_ptr()); + // We should not use mk_app because it does not guarantee that the result would be in simplified form. + // result = m_manager.mk_app(m_fid, a->get_decl_kind(), new_args.size(), new_args.c_ptr()); + if (is_app_of(a, m_fid, OP_BAND)) + mk_bv_and(new_args.size(), new_args.c_ptr(), result); + else if (is_app_of(a, m_fid, OP_BOR)) + mk_bv_or(new_args.size(), new_args.c_ptr(), result); + else if (is_app_of(a, m_fid, OP_BXOR)) + mk_bv_xor(new_args.size(), new_args.c_ptr(), result); + else if (is_app_of(a, m_fid, OP_BNOR)) + mk_bv_nor(new_args.size(), new_args.c_ptr(), result); + else if (is_app_of(a, m_fid, OP_BNAND)) + mk_bv_nand(new_args.size(), new_args.c_ptr(), result); + else if (is_app_of(a, m_fid, OP_BNOT)) { + SASSERT(new_args.size() == 1); + mk_bv_not(new_args[0], result); + } + else if (is_app_of(a, m_fid, OP_BADD)) + mk_add(new_args.size(), new_args.c_ptr(), result); + else if (is_app_of(a, m_fid, OP_BMUL)) + mk_mul(new_args.size(), new_args.c_ptr(), result); + else if (is_app_of(a, m_fid, OP_BSUB)) + mk_sub(new_args.size(), new_args.c_ptr(), result); + else { + UNREACHABLE(); + } return true; } else if (m_manager.is_ite(a)) { @@ -747,16 +771,16 @@ void bv_simplifier_plugin::mk_bv_eq(expr* a1, expr* a2, expr_ref& result) { expr * arg1 = *it1; expr * arg2 = *it2; TRACE("expr_bv_util", tout << "low1: " << low1 << " low2: " << low2 << "\n"; - ast_ll_pp(tout, m_manager, arg1); - ast_ll_pp(tout, m_manager, arg2);); + tout << mk_pp(arg1, m_manager) << "\n"; + tout << mk_pp(arg2, m_manager) << "\n";); unsigned sz1 = get_bv_size(arg1); unsigned sz2 = get_bv_size(arg2); SASSERT(low1 < sz1 && low2 < sz2); unsigned rsz1 = sz1 - low1; unsigned rsz2 = sz2 - low2; TRACE("expr_bv_util", tout << "rsz1: " << rsz1 << " rsz2: " << rsz2 << "\n"; - ast_ll_pp(tout, m_manager, arg1); ast_ll_pp(tout, m_manager, arg2);); - + tout << mk_pp(arg1, m_manager) << "\n"; + tout << mk_pp(arg2, m_manager) << "\n";); if (rsz1 == rsz2) { mk_extract(sz1 - 1, low1, arg1, lhs); @@ -826,9 +850,9 @@ void bv_simplifier_plugin::mk_eq_core(expr * arg1, expr * arg2, expr_ref & resul } m_bsimp.mk_and(tmps.size(), tmps.c_ptr(), result); TRACE("mk_eq_bb", - ast_ll_pp(tout, m_manager, arg1); - ast_ll_pp(tout, m_manager, arg2); - ast_ll_pp(tout, m_manager, result);); + tout << mk_pp(arg1, m_manager) << "\n"; + tout << mk_pp(arg2, m_manager) << "\n"; + tout << mk_pp(result, m_manager) << "\n";); return; } #endif diff --git a/src/ast/simplifier/poly_simplifier_plugin.cpp b/src/ast/simplifier/poly_simplifier_plugin.cpp index 402b078a8..d64123e7b 100644 --- a/src/ast/simplifier/poly_simplifier_plugin.cpp +++ b/src/ast/simplifier/poly_simplifier_plugin.cpp @@ -285,6 +285,7 @@ bool poly_simplifier_plugin::merge_monomials(bool inv, expr * n1, expr * n2, exp else result = m_manager.mk_app(m_fid, m_MUL, mk_numeral(k1), b); } + TRACE("merge_monomials", tout << mk_pp(n1, m_manager) << "\n" << mk_pp(n2, m_manager) << "\n" << mk_pp(result, m_manager) << "\n";); return true; } 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_base.h b/src/muz_qe/dl_base.h index 491bb261d..200ce2d83 100644 --- a/src/muz_qe/dl_base.h +++ b/src/muz_qe/dl_base.h @@ -331,6 +331,10 @@ namespace datalog { virtual mutator_fn * mk_filter_interpreted_fn(const base_object & t, app * condition) { return 0; } + virtual transformer_fn * mk_filter_interpreted_and_project_fn(const base_object & t, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) + { return 0; } + virtual transformer_fn * mk_select_equal_and_project_fn(const base_object & t, const element & value, unsigned col) { return 0; } @@ -454,8 +458,8 @@ namespace datalog { class convenient_join_fn : public join_fn { signature m_result_sig; protected: - const unsigned_vector m_cols1; - const unsigned_vector m_cols2; + unsigned_vector m_cols1; + unsigned_vector m_cols2; convenient_join_fn(const signature & o1_sig, const signature & o2_sig, unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) @@ -470,8 +474,8 @@ namespace datalog { class convenient_join_project_fn : public join_fn { signature m_result_sig; protected: - const unsigned_vector m_cols1; - const unsigned_vector m_cols2; + unsigned_vector m_cols1; + unsigned_vector m_cols2; //it is non-const because it needs to be modified in sparse_table version of the join_project operator unsigned_vector m_removed_cols; @@ -498,7 +502,7 @@ namespace datalog { class convenient_project_fn : public convenient_transformer_fn { protected: - const unsigned_vector m_removed_cols; + unsigned_vector m_removed_cols; convenient_project_fn(const signature & orig_sig, unsigned col_cnt, const unsigned * removed_cols) : m_removed_cols(col_cnt, removed_cols) { diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp index c313f7d7b..8e9fb510e 100644 --- a/src/muz_qe/dl_bmc_engine.cpp +++ b/src/muz_qe/dl_bmc_engine.cpp @@ -297,6 +297,7 @@ namespace datalog { r->to_formula(fml); r2 = r; rm.substitute(r2, sub.size(), sub.c_ptr()); + proof_ref p(m); if (r0) { VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get())); expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true); @@ -306,7 +307,10 @@ namespace datalog { r1->to_formula(concl); scoped_proof _sp(m); - proof* p = r->get_proof(); + p = r->get_proof(); + if (!p) { + p = m.mk_asserted(fml); + } proof* premises[2] = { pr, p }; positions.push_back(std::make_pair(0, 1)); @@ -319,13 +323,17 @@ namespace datalog { else { r2->to_formula(concl); scoped_proof _sp(m); - proof* p = r->get_proof(); + p = r->get_proof(); + if (!p) { + p = m.mk_asserted(fml); + } if (sub.empty()) { pr = p; } else { substs.push_back(sub); - pr = m.mk_hyper_resolve(1, &p, concl, positions, substs); + proof* ps[1] = { p }; + pr = m.mk_hyper_resolve(1, ps, concl, positions, substs); } r0 = r2; } @@ -1211,6 +1219,15 @@ namespace datalog { r->to_formula(fml); r2 = r; rm.substitute(r2, sub.size(), sub.c_ptr()); + proof_ref p(m); + { + scoped_proof _sp(m); + p = r->get_proof(); + if (!p) { + p = m.mk_asserted(fml); + } + } + if (r0) { VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get())); expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true); @@ -1218,9 +1235,8 @@ namespace datalog { apply_subst(sub, sub2); unifier.apply(*r0.get(), 0, *r2.get(), r1); r1->to_formula(concl); - scoped_proof _sp(m); - proof* p = r->get_proof(); + scoped_proof _sp(m); proof* premises[2] = { pr, p }; positions.push_back(std::make_pair(0, 1)); @@ -1233,13 +1249,13 @@ namespace datalog { else { r2->to_formula(concl); scoped_proof _sp(m); - proof* p = r->get_proof(); if (sub.empty()) { pr = p; } else { substs.push_back(sub); - pr = m.mk_hyper_resolve(1, &p, concl, positions, substs); + proof * ps[1] = { p }; + pr = m.mk_hyper_resolve(1, ps, concl, positions, substs); } r0 = r2; } diff --git a/src/muz_qe/dl_check_table.cpp b/src/muz_qe/dl_check_table.cpp index 5081654b5..ea4003e5f 100644 --- a/src/muz_qe/dl_check_table.cpp +++ b/src/muz_qe/dl_check_table.cpp @@ -82,6 +82,34 @@ namespace datalog { return alloc(join_fn, *this, t1, t2, col_cnt, cols1, cols2); } + class check_table_plugin::join_project_fn : public table_join_fn { + scoped_ptr m_tocheck; + scoped_ptr m_checker; + public: + join_project_fn(check_table_plugin& p, const table_base & t1, const table_base & t2, + unsigned col_cnt, const unsigned * cols1, const unsigned * cols2, + unsigned removed_col_cnt, const unsigned * removed_cols) { + m_tocheck = p.get_manager().mk_join_project_fn(tocheck(t1), tocheck(t2), col_cnt, cols1, cols2, removed_col_cnt, removed_cols); + m_checker = p.get_manager().mk_join_project_fn(checker(t1), checker(t2), col_cnt, cols1, cols2, removed_col_cnt, removed_cols); + } + + virtual table_base* operator()(const table_base & t1, const table_base & t2) { + table_base* ttocheck = (*m_tocheck)(tocheck(t1), tocheck(t2)); + table_base* tchecker = (*m_checker)(checker(t1), checker(t2)); + check_table* result = alloc(check_table, get(t1).get_plugin(), ttocheck->get_signature(), ttocheck, tchecker); + return result; + } + }; + + table_join_fn * check_table_plugin::mk_join_project_fn(const table_base & t1, const table_base & t2, + unsigned col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, + const unsigned * removed_cols) { + if (!check_kind(t1) || !check_kind(t2)) { + return 0; + } + return alloc(join_project_fn, *this, t1, t2, col_cnt, cols1, cols2, removed_col_cnt, removed_cols); + } + class check_table_plugin::union_fn : public table_union_fn { scoped_ptr m_tocheck; scoped_ptr m_checker; @@ -120,7 +148,6 @@ namespace datalog { } table_base* operator()(table_base const& src) { - IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";); table_base* tchecker = (*m_checker)(checker(src)); table_base* ttocheck = (*m_tocheck)(tocheck(src)); check_table* result = alloc(check_table, get(src).get_plugin(), tchecker->get_signature(), ttocheck, tchecker); @@ -135,6 +162,31 @@ namespace datalog { return alloc(project_fn, *this, t, col_cnt, removed_cols); } + class check_table_plugin::select_equal_and_project_fn : public table_transformer_fn { + scoped_ptr m_checker; + scoped_ptr m_tocheck; + public: + select_equal_and_project_fn(check_table_plugin& p, const table_base & t, const table_element & value, unsigned col) { + m_checker = p.get_manager().mk_select_equal_and_project_fn(checker(t), value, col); + m_tocheck = p.get_manager().mk_select_equal_and_project_fn(tocheck(t), value, col); + } + + table_base* operator()(table_base const& src) { + table_base* tchecker = (*m_checker)(checker(src)); + table_base* ttocheck = (*m_tocheck)(tocheck(src)); + check_table* result = alloc(check_table, get(src).get_plugin(), tchecker->get_signature(), ttocheck, tchecker); + return result; + } + }; + + table_transformer_fn * check_table_plugin::mk_select_equal_and_project_fn(const table_base & t, + const table_element & value, unsigned col) { + if (!check_kind(t)) { + return 0; + } + return alloc(select_equal_and_project_fn, *this, t, value, col); + } + class check_table_plugin::rename_fn : public table_transformer_fn { scoped_ptr m_checker; scoped_ptr m_tocheck; @@ -233,6 +285,33 @@ namespace datalog { return 0; } + class check_table_plugin::filter_interpreted_and_project_fn : public table_transformer_fn { + scoped_ptr m_checker; + scoped_ptr m_tocheck; + public: + filter_interpreted_and_project_fn(check_table_plugin& p, const table_base & t, app * condition, + unsigned removed_col_cnt, const unsigned * removed_cols) + { + m_checker = p.get_manager().mk_filter_interpreted_and_project_fn(checker(t), condition, removed_col_cnt, removed_cols); + m_tocheck = p.get_manager().mk_filter_interpreted_and_project_fn(tocheck(t), condition, removed_col_cnt, removed_cols); + } + + table_base* operator()(table_base const& src) { + table_base* tchecker = (*m_checker)(checker(src)); + table_base* ttocheck = (*m_tocheck)(tocheck(src)); + check_table* result = alloc(check_table, get(src).get_plugin(), ttocheck->get_signature(), ttocheck, tchecker); + return result; + } + }; + + table_transformer_fn * check_table_plugin::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 alloc(filter_interpreted_and_project_fn, *this, t, condition, removed_col_cnt, removed_cols); + } + return 0; + } + class check_table_plugin::filter_by_negation_fn : public table_intersection_filter_fn { scoped_ptr m_checker; scoped_ptr m_tocheck; diff --git a/src/muz_qe/dl_check_table.h b/src/muz_qe/dl_check_table.h index 40a3d5207..e4f439590 100644 --- a/src/muz_qe/dl_check_table.h +++ b/src/muz_qe/dl_check_table.h @@ -35,13 +35,16 @@ namespace datalog { unsigned m_count; protected: class join_fn; + class join_project_fn; class union_fn; class transformer_fn; class rename_fn; class project_fn; + class select_equal_and_project_fn; class filter_equal_fn; class filter_identical_fn; class filter_interpreted_fn; + class filter_interpreted_and_project_fn; class filter_by_negation_fn; public: @@ -54,10 +57,15 @@ namespace datalog { virtual table_join_fn * mk_join_fn(const table_base & t1, const table_base & t2, unsigned col_cnt, const unsigned * cols1, const unsigned * cols2); + virtual table_join_fn * mk_join_project_fn(const table_base & t1, const table_base & t2, + unsigned col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, + const unsigned * removed_cols); virtual table_union_fn * mk_union_fn(const table_base & tgt, const table_base & src, const table_base * delta); virtual table_transformer_fn * mk_project_fn(const table_base & t, unsigned col_cnt, const unsigned * removed_cols); + virtual table_transformer_fn * mk_select_equal_and_project_fn(const table_base & t, + const table_element & value, unsigned col); virtual table_transformer_fn * mk_rename_fn(const table_base & t, unsigned permutation_cycle_len, const unsigned * permutation_cycle); virtual table_mutator_fn * mk_filter_identical_fn(const table_base & t, unsigned col_cnt, @@ -65,6 +73,8 @@ namespace datalog { virtual table_mutator_fn * mk_filter_equal_fn(const table_base & t, const table_element & value, unsigned col); virtual table_mutator_fn * mk_filter_interpreted_fn(const table_base & t, app * condition); + virtual table_transformer_fn * mk_filter_interpreted_and_project_fn(const table_base & t, + app * condition, unsigned removed_col_cnt, const unsigned * 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, diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp index 05a0d24b2..3f16d0dab 100644 --- a/src/muz_qe/dl_compiler.cpp +++ b/src/muz_qe/dl_compiler.cpp @@ -73,6 +73,18 @@ namespace datalog { vars.get_cols2(), removed_cols.size(), removed_cols.c_ptr(), result)); } + void compiler::make_filter_interpreted_and_project(reg_idx src, app_ref & cond, + const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc) { + SASSERT(!removed_cols.empty()); + relation_signature res_sig; + relation_signature::from_project(m_reg_signatures[src], removed_cols.size(), + removed_cols.c_ptr(), res_sig); + result = get_fresh_register(res_sig); + + acc.push_back(instruction::mk_filter_interpreted_and_project(src, cond, + removed_cols.size(), removed_cols.c_ptr(), result)); + } + void compiler::make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col, reg_idx & result, instruction_block & acc) { relation_signature res_sig; @@ -619,6 +631,116 @@ namespace datalog { } // enforce interpreted tail predicates + unsigned ft_len = r->get_tail_size(); // full tail + ptr_vector tail; + for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) { + tail.push_back(r->get_tail(tail_index)); + } + + if (!tail.empty()) { + app_ref filter_cond(tail.size() == 1 ? to_app(tail.back()) : m.mk_and(tail.size(), tail.c_ptr()), m); + ptr_vector filter_vars; + get_free_vars(filter_cond, filter_vars); + + // create binding + expr_ref_vector binding(m); + binding.resize(filter_vars.size()+1); + + for (unsigned v = 0; v < filter_vars.size(); ++v) { + if (!filter_vars[v]) + continue; + + int2ints::entry * entry = var_indexes.find_core(v); + unsigned src_col; + if (entry) { + src_col = entry->get_data().m_value.back(); + } else { + // we have an unbound variable, so we add an unbound column for it + relation_sort unbound_sort = filter_vars[v]; + + reg_idx new_reg; + bool new_dealloc; + make_add_unbound_column(r, 0, head_pred, filtered_res, unbound_sort, new_reg, new_dealloc, acc); + if (dealloc) + make_dealloc_non_void(filtered_res, acc); + dealloc = new_dealloc; + filtered_res = new_reg; + + src_col = single_res_expr.size(); + single_res_expr.push_back(m.mk_var(v, unbound_sort)); + + entry = var_indexes.insert_if_not_there2(v, unsigned_vector()); + entry->get_data().m_value.push_back(src_col); + } + relation_sort var_sort = m_reg_signatures[filtered_res][src_col]; + binding[filter_vars.size()-v] = m.mk_var(src_col, var_sort); + } + + // check if there are any columns to remove + unsigned_vector remove_columns; + { + unsigned_vector var_idx_to_remove; + ptr_vector vars; + get_free_vars(r->get_head(), vars); + for (int2ints::iterator I = var_indexes.begin(), E = var_indexes.end(); + I != E; ++I) { + unsigned var_idx = I->m_key; + if (!vars.get(var_idx, 0)) { + unsigned_vector & cols = I->m_value; + for (unsigned i = 0; i < cols.size(); ++i) { + remove_columns.push_back(cols[i]); + } + var_idx_to_remove.push_back(var_idx); + } + } + + for (unsigned i = 0; i < var_idx_to_remove.size(); ++i) { + var_indexes.remove(var_idx_to_remove[i]); + } + + // update column idx for after projection state + if (!remove_columns.empty()) { + unsigned_vector offsets; + offsets.resize(single_res_expr.size(), 0); + + for (unsigned i = 0; i < remove_columns.size(); ++i) { + for (unsigned col = remove_columns[i]; col < offsets.size(); ++col) { + ++offsets[col]; + } + } + + for (int2ints::iterator I = var_indexes.begin(), E = var_indexes.end(); + I != E; ++I) { + unsigned_vector & cols = I->m_value; + for (unsigned i = 0; i < cols.size(); ++i) { + cols[i] -= offsets[cols[i]]; + } + } + } + } + + expr_ref renamed(m); + m_context.get_var_subst()(filter_cond, binding.size(), binding.c_ptr(), renamed); + app_ref app_renamed(to_app(renamed), m); + if (remove_columns.empty()) { + if (!dealloc) + make_clone(filtered_res, filtered_res, acc); + acc.push_back(instruction::mk_filter_interpreted(filtered_res, app_renamed)); + } else { + reg_idx new_reg; + std::sort(remove_columns.begin(), remove_columns.end()); + make_filter_interpreted_and_project(filtered_res, app_renamed, remove_columns, new_reg, acc); + if (dealloc) + make_dealloc_non_void(filtered_res, acc); + filtered_res = new_reg; + } + dealloc = true; + } + +#if 0 + // this version is potentially better for non-symbolic tables, + // since it constraints each unbound column at a time (reducing the + // size of intermediate results). unsigned ft_len=r->get_tail_size(); //full tail for(unsigned tail_index=ut_len; tail_indexget_tail(tail_index); @@ -686,6 +808,7 @@ namespace datalog { acc.push_back(instruction::mk_filter_interpreted(filtered_res, app_renamed)); dealloc = true; } +#endif { //put together the columns of head relation @@ -737,7 +860,7 @@ namespace datalog { make_dealloc_non_void(new_head_reg, acc); } - finish: +// finish: m_instruction_observer.finish_rule(); } diff --git a/src/muz_qe/dl_compiler.h b/src/muz_qe/dl_compiler.h index 78b4623de..e0f9af424 100644 --- a/src/muz_qe/dl_compiler.h +++ b/src/muz_qe/dl_compiler.h @@ -145,6 +145,8 @@ namespace datalog { instruction_block & acc); void make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars, const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc); + void make_filter_interpreted_and_project(reg_idx src, app_ref & cond, + const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc); void make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col, reg_idx & result, instruction_block & acc); /** diff --git a/src/muz_qe/dl_instruction.cpp b/src/muz_qe/dl_instruction.cpp index b103d743e..637d9a17f 100644 --- a/src/muz_qe/dl_instruction.cpp +++ b/src/muz_qe/dl_instruction.cpp @@ -526,6 +526,64 @@ namespace datalog { return alloc(instr_filter_interpreted, reg, condition); } + class instr_filter_interpreted_and_project : public instruction { + reg_idx m_src; + app_ref m_cond; + unsigned_vector m_cols; + reg_idx m_res; + public: + instr_filter_interpreted_and_project(reg_idx src, app_ref & condition, + unsigned col_cnt, const unsigned * removed_cols, reg_idx result) + : m_src(src), m_cond(condition), m_cols(col_cnt, removed_cols), + m_res(result) {} + + virtual bool perform(execution_context & ctx) { + if (!ctx.reg(m_src)) { + ctx.make_empty(m_res); + return true; + } + + relation_transformer_fn * fn; + relation_base & reg = *ctx.reg(m_src); + if (!find_fn(reg, fn)) { + fn = reg.get_manager().mk_filter_interpreted_and_project_fn(reg, m_cond, m_cols.size(), m_cols.c_ptr()); + if (!fn) { + throw default_exception( + "trying to perform unsupported filter_interpreted_and_project operation on a relation of kind %s", + reg.get_plugin().get_name().bare_str()); + } + store_fn(reg, fn); + } + + ctx.set_reg(m_res, (*fn)(reg)); + + if (ctx.eager_emptiness_checking() && ctx.reg(m_res)->empty()) { + ctx.make_empty(m_res); + } + return true; + } + + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + out << "filter_interpreted_and_project " << m_src << " into " << m_res; + out << " using " << mk_pp(m_cond, m_cond.get_manager()); + out << " deleting columns "; + print_container(m_cols, out); + } + + virtual void make_annotations(execution_context & ctx) { + std::stringstream s; + std::string a = "rel_src"; + ctx.get_register_annotation(m_src, a); + s << "filter_interpreted_and_project " << mk_pp(m_cond, m_cond.get_manager()); + ctx.set_register_annotation(m_res, s.str()); + } + }; + + instruction * instruction::mk_filter_interpreted_and_project(reg_idx reg, app_ref & condition, + unsigned col_cnt, const unsigned * removed_cols, reg_idx result) { + return alloc(instr_filter_interpreted_and_project, reg, condition, col_cnt, removed_cols, result); + } + class instr_union : public instruction { reg_idx m_src; @@ -592,6 +650,7 @@ namespace datalog { } } + SASSERT(r_src.get_signature().size() == r_tgt.get_signature().size()); TRACE("dl_verbose", r_tgt.display(tout <<"pre-union:");); (*fn)(r_tgt, r_src, r_delta); diff --git a/src/muz_qe/dl_instruction.h b/src/muz_qe/dl_instruction.h index ae6310ba6..97622c6f3 100644 --- a/src/muz_qe/dl_instruction.h +++ b/src/muz_qe/dl_instruction.h @@ -260,6 +260,8 @@ namespace datalog { static instruction * mk_filter_equal(ast_manager & m, reg_idx reg, const relation_element & value, unsigned col); static instruction * mk_filter_identical(reg_idx reg, unsigned col_cnt, const unsigned * identical_cols); static instruction * mk_filter_interpreted(reg_idx reg, app_ref & condition); + static instruction * mk_filter_interpreted_and_project(reg_idx src, app_ref & condition, + unsigned col_cnt, const unsigned * removed_cols, reg_idx result); static instruction * mk_union(reg_idx src, reg_idx tgt, reg_idx delta); static instruction * mk_widen(reg_idx src, reg_idx tgt, reg_idx delta); static instruction * mk_projection(reg_idx src, unsigned col_cnt, const unsigned * removed_cols, diff --git a/src/muz_qe/dl_relation_manager.cpp b/src/muz_qe/dl_relation_manager.cpp index 986a1f2c4..ce20961f1 100644 --- a/src/muz_qe/dl_relation_manager.cpp +++ b/src/muz_qe/dl_relation_manager.cpp @@ -720,6 +720,13 @@ namespace datalog { return t.get_plugin().mk_filter_interpreted_fn(t, condition); } + relation_transformer_fn * relation_manager::mk_filter_interpreted_and_project_fn(const relation_base & t, + app * condition, + unsigned removed_col_cnt, + const unsigned * removed_cols) { + return t.get_plugin().mk_filter_interpreted_and_project_fn(t, condition, removed_col_cnt, removed_cols); + } + class relation_manager::default_relation_select_equal_and_project_fn : public relation_transformer_fn { scoped_ptr m_filter; @@ -1387,6 +1394,45 @@ namespace datalog { } + class relation_manager::default_table_filter_interpreted_and_project_fn + : public table_transformer_fn { + scoped_ptr m_filter; + scoped_ptr m_project; + app_ref m_condition; + unsigned_vector m_removed_cols; + public: + default_table_filter_interpreted_and_project_fn(context & ctx, table_mutator_fn * filter, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) + : m_filter(filter), m_condition(condition, ctx.get_manager()), + m_removed_cols(removed_col_cnt, removed_cols) {} + + virtual table_base* operator()(const table_base & tb) { + table_base *t2 = tb.clone(); + (*m_filter)(*t2); + if (!m_project) { + relation_manager & rmgr = t2->get_plugin().get_manager(); + m_project = rmgr.mk_project_fn(*t2, m_removed_cols.size(), m_removed_cols.c_ptr()); + if (!m_project) { + throw default_exception("projection does not exist"); + } + } + return (*m_project)(*t2); + } + }; + + table_transformer_fn * relation_manager::mk_filter_interpreted_and_project_fn(const table_base & t, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) { + table_transformer_fn * res = t.get_plugin().mk_filter_interpreted_and_project_fn(t, condition, removed_col_cnt, removed_cols); + if (res) + return res; + + table_mutator_fn * filter = mk_filter_interpreted_fn(t, condition); + SASSERT(filter); + res = alloc(default_table_filter_interpreted_and_project_fn, get_context(), filter, condition, removed_col_cnt, removed_cols); + return res; + } + + table_intersection_filter_fn * relation_manager::mk_filter_by_intersection_fn(const table_base & t, const table_base & src, unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * src_cols) { table_intersection_filter_fn * res = t.get_plugin().mk_filter_by_negation_fn(t, src, joined_col_cnt, diff --git a/src/muz_qe/dl_relation_manager.h b/src/muz_qe/dl_relation_manager.h index f22ae7923..ccdba2783 100644 --- a/src/muz_qe/dl_relation_manager.h +++ b/src/muz_qe/dl_relation_manager.h @@ -55,6 +55,7 @@ namespace datalog { class default_table_filter_equal_fn; class default_table_filter_identical_fn; class default_table_filter_interpreted_fn; + class default_table_filter_interpreted_and_project_fn; class default_table_negation_filter_fn; class default_table_filter_not_equal_fn; class default_table_select_equal_and_project_fn; @@ -350,6 +351,9 @@ namespace datalog { relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition); + relation_transformer_fn * mk_filter_interpreted_and_project_fn(const relation_base & t, app * condition, + unsigned removed_col_cnt, const unsigned * removed_cols); + /** \brief Operations that returns all rows of \c t for which is column \c col equal to \c value with the column \c col removed. @@ -522,6 +526,9 @@ namespace datalog { table_mutator_fn * mk_filter_interpreted_fn(const table_base & t, app * condition); + table_transformer_fn * mk_filter_interpreted_and_project_fn(const table_base & t, app * condition, + unsigned removed_col_cnt, const unsigned * removed_cols); + /** \brief Operations that returns all rows of \c t for which is column \c col equal to \c value with the column \c col removed. diff --git a/src/muz_qe/dl_table_relation.cpp b/src/muz_qe/dl_table_relation.cpp index fc661366d..3c30c58bb 100644 --- a/src/muz_qe/dl_table_relation.cpp +++ b/src/muz_qe/dl_table_relation.cpp @@ -354,6 +354,21 @@ namespace datalog { return alloc(tr_mutator_fn, tfun); } + relation_transformer_fn * table_relation_plugin::mk_filter_interpreted_and_project_fn(const relation_base & t, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) { + if (!t.from_table()) + return 0; + + const table_relation & tr = static_cast(t); + table_transformer_fn * tfun = get_manager().mk_filter_interpreted_and_project_fn(tr.get_table(), + condition, removed_col_cnt, removed_cols); + SASSERT(tfun); + + relation_signature sig; + relation_signature::from_project(t.get_signature(), removed_col_cnt, removed_cols, sig); + return alloc(tr_transformer_fn, sig, tfun); + } + class table_relation_plugin::tr_intersection_filter_fn : public relation_intersection_filter_fn { scoped_ptr m_tfun; public: diff --git a/src/muz_qe/dl_table_relation.h b/src/muz_qe/dl_table_relation.h index 12f0d4eaa..f86143c0f 100644 --- a/src/muz_qe/dl_table_relation.h +++ b/src/muz_qe/dl_table_relation.h @@ -71,6 +71,8 @@ namespace datalog { virtual relation_mutator_fn * mk_filter_equal_fn(const relation_base & t, const relation_element & value, unsigned col); virtual relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition); + virtual relation_transformer_fn * mk_filter_interpreted_and_project_fn(const relation_base & t, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols); virtual relation_intersection_filter_fn * mk_filter_by_intersection_fn(const relation_base & t, const relation_base & src, unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * src_cols); virtual relation_intersection_filter_fn * mk_filter_by_negation_fn(const relation_base & t, diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg index c2d33cb05..c2996dd8f 100644 --- a/src/muz_qe/fixedpoint_params.pyg +++ b/src/muz_qe/fixedpoint_params.pyg @@ -48,6 +48,7 @@ def_module_params('fixedpoint', ('use_multicore_generalizer', BOOL, False, "PDR: extract multiple cores for blocking states"), ('use_inductive_generalizer', BOOL, True, "PDR: generalize lemmas using induction strengthening"), ('use_arith_inductive_generalizer', BOOL, False, "PDR: generalize lemmas using arithmetic heuristics for induction strengthening"), + ('use_convex_hull_generalizer', BOOL, False, "PDR: generalize using convex hulls of lemmas"), ('cache_mode', UINT, 0, "PDR: use no (0), symbolic (1) or explicit cache (2) for model search"), ('inductive_reachability_check', BOOL, False, "PDR: assume negation of the cube on the previous level when " "checking for reachability (not only during cube weakening)"), @@ -60,7 +61,7 @@ def_module_params('fixedpoint', ('print_answer', BOOL, False, 'print answer instance(s) to query'), ('print_certificate', BOOL, False, 'print certificate for reachability or non-reachability'), ('print_statistics', BOOL, False, 'print statistics'), - ('use_utvpi', BOOL, False, 'experimental use UTVPI strategy'), + ('use_utvpi', BOOL, True, 'PDR: Enable UTVPI strategy'), ('tab_selection', SYMBOL, 'weight', 'selection method for tabular strategy: weight (default), first, var-use'), ('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'), )) diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index dcfbcca2b..1c49e0c83 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1561,15 +1561,19 @@ 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 (m_params.use_convex_hull_generalizer()) { + m_core_generalizers.push_back(alloc(core_convex_hull_generalizer, *this)); } 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/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp index 1b8ea22f9..800a21eaf 100644 --- a/src/muz_qe/pdr_generalizers.cpp +++ b/src/muz_qe/pdr_generalizers.cpp @@ -147,6 +147,177 @@ namespace pdr { } + core_convex_hull_generalizer::core_convex_hull_generalizer(context& ctx): + core_generalizer(ctx), + m(ctx.get_manager()), + a(m), + m_sigma(m), + m_trail(m) { + m_sigma.push_back(m.mk_fresh_const("sigma", a.mk_real())); + m_sigma.push_back(m.mk_fresh_const("sigma", a.mk_real())); + } + + void core_convex_hull_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) { + manager& pm = n.pt().get_pdr_manager(); + expr_ref_vector conv1(m), conv2(m), core1(m), core2(m), eqs(m); + if (core.empty()) { + return; + } + if (!m_left.contains(n.pt().head())) { + expr_ref left(m), right(m); + m_left.insert(n.pt().head(), 0); + unsigned sz = n.pt().sig_size(); + for (unsigned i = 0; i < sz; ++i) { + func_decl* fn0 = n.pt().sig(i); + sort* srt = fn0->get_range(); + if (a.is_int_real(srt)) { + func_decl* fn1 = pm.o2n(fn0, 0); + left = m.mk_fresh_const(fn1->get_name().str().c_str(), srt); + right = m.mk_fresh_const(fn1->get_name().str().c_str(), srt); + m_left.insert(fn1, left); + m_right.insert(fn1, right); + m_trail.push_back(left); + m_trail.push_back(right); + } + } + } + unsigned sz = n.pt().sig_size(); + for (unsigned i = 0; i < sz; ++i) { + expr* left, *right; + func_decl* fn0 = n.pt().sig(i); + func_decl* fn1 = pm.o2n(fn0, 0); + if (m_left.find(fn1, left) && m_right.find(fn1, right)) { + eqs.push_back(m.mk_eq(m.mk_const(fn1), a.mk_add(left, right))); + } + } + if (!mk_convex(core, 0, conv1)) { + IF_VERBOSE(0, verbose_stream() << "Non-convex: " << mk_pp(pm.mk_and(core), m) << "\n";); + return; + } + conv1.append(eqs); + conv1.push_back(a.mk_gt(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real()))); + conv1.push_back(a.mk_gt(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real()))); + conv1.push_back(m.mk_eq(a.mk_numeral(rational(1), a.mk_real()), a.mk_add(m_sigma[0].get(), m_sigma[1].get()))); + expr_ref fml = n.pt().get_formulas(n.level(), false); + expr_ref_vector fmls(m); + datalog::flatten_and(fml, fmls); + for (unsigned i = 0; i < fmls.size(); ++i) { + fml = m.mk_not(fmls[i].get()); + core2.reset(); + datalog::flatten_and(fml, core2); + if (!mk_convex(core2, 1, conv2)) { + IF_VERBOSE(0, verbose_stream() << "Non-convex: " << mk_pp(pm.mk_and(core2), m) << "\n";); + continue; + } + conv2.append(conv1); + expr_ref state = pm.mk_and(conv2); + TRACE("pdr", tout << "Check:\n" << mk_pp(state, m) << "\n"; + tout << "New formula:\n" << mk_pp(pm.mk_and(core), m) << "\n"; + tout << "Old formula:\n" << mk_pp(fml, m) << "\n"; + + ); + model_node nd(0, state, n.pt(), n.level()); + if (l_false == n.pt().is_reachable(nd, &conv2, uses_level)) { + TRACE("pdr", + tout << mk_pp(state, m) << "\n"; + tout << "Generalized to:\n" << mk_pp(pm.mk_and(conv2), m) << "\n";); + IF_VERBOSE(0, + verbose_stream() << mk_pp(state, m) << "\n"; + verbose_stream() << "Generalized to:\n" << mk_pp(pm.mk_and(conv2), m) << "\n";); + core.reset(); + core.append(conv2); + } + } + } + + bool core_convex_hull_generalizer::mk_convex(expr_ref_vector const& core, unsigned index, expr_ref_vector& conv) { + conv.reset(); + for (unsigned i = 0; i < core.size(); ++i) { + mk_convex(core[i], index, conv); + } + return !conv.empty(); + } + + void core_convex_hull_generalizer::mk_convex(expr* fml, unsigned index, expr_ref_vector& conv) { + expr_ref result(m), r1(m), r2(m); + expr* e1, *e2; + bool is_not = m.is_not(fml, fml); + if (a.is_le(fml, e1, e2) && mk_convex(e1, index, false, r1) && mk_convex(e2, index, false, r2)) { + result = a.mk_le(r1, r2); + } + else if (a.is_ge(fml, e1, e2) && mk_convex(e1, index, false, r1) && mk_convex(e2, index, false, r2)) { + result = a.mk_ge(r1, r2); + } + else if (a.is_gt(fml, e1, e2) && mk_convex(e1, index, false, r1) && mk_convex(e2, index, false, r2)) { + result = a.mk_gt(r1, r2); + } + else if (a.is_lt(fml, e1, e2) && mk_convex(e1, index, false, r1) && mk_convex(e2, index, false, r2)) { + result = a.mk_lt(r1, r2); + } + else if (m.is_eq(fml, e1, e2) && a.is_int_real(e1) && mk_convex(e1, index, false, r1) && mk_convex(e2, index, false, r2)) { + result = m.mk_eq(r1, r2); + } + else { + TRACE("pdr", tout << "Did not handle " << mk_pp(fml, m) << "\n";); + return; + } + if (is_not) { + result = m.mk_not(result); + } + conv.push_back(result); + } + + + bool core_convex_hull_generalizer::translate(func_decl* f, unsigned index, expr_ref& result) { + expr* tmp; + if (index == 0 && m_left.find(f, tmp)) { + result = tmp; + return true; + } + if (index == 1 && m_right.find(f, tmp)) { + result = tmp; + return true; + } + return false; + } + + + bool core_convex_hull_generalizer::mk_convex(expr* term, unsigned index, bool is_mul, expr_ref& result) { + if (!is_app(term)) { + return false; + } + app* app = to_app(term); + expr* e1, *e2; + expr_ref r1(m), r2(m); + if (translate(app->get_decl(), index, result)) { + return true; + } + if (a.is_add(term, e1, e2) && mk_convex(e1, index, is_mul, r1) && mk_convex(e2, index, is_mul, r2)) { + result = a.mk_add(r1, r2); + return true; + } + if (a.is_sub(term, e1, e2) && mk_convex(e1, index, is_mul, r1) && mk_convex(e2, index, is_mul, r2)) { + result = a.mk_sub(r1, r2); + return true; + } + if (a.is_mul(term, e1, e2) && mk_convex(e1, index, true, r1) && mk_convex(e2, index, true, r2)) { + result = a.mk_mul(r1, r2); + return true; + } + if (a.is_numeral(term)) { + if (is_mul) { + result = term; + } + else { + result = a.mk_mul(m_sigma[index].get(), term); + } + return true; + } + IF_VERBOSE(0, verbose_stream() << "Not handled: " << mk_pp(term, m) << "\n";); + return false; + } + + // --------------------------------- // core_arith_inductive_generalizer // NB. this is trying out some ideas for generalization in diff --git a/src/muz_qe/pdr_generalizers.h b/src/muz_qe/pdr_generalizers.h index 03bd89c4d..a4be9d1fa 100644 --- a/src/muz_qe/pdr_generalizers.h +++ b/src/muz_qe/pdr_generalizers.h @@ -73,6 +73,23 @@ namespace pdr { virtual void collect_statistics(statistics& st) const; }; + class core_convex_hull_generalizer : public core_generalizer { + ast_manager& m; + arith_util a; + expr_ref_vector m_sigma; + expr_ref_vector m_trail; + obj_map m_left; + obj_map m_right; + bool mk_convex(expr_ref_vector const& core, unsigned index, expr_ref_vector& conv); + void mk_convex(expr* fml, unsigned index, expr_ref_vector& conv); + bool mk_convex(expr* term, unsigned index, bool is_mul, expr_ref& result); + bool translate(func_decl* fn, unsigned index, expr_ref& result); + public: + core_convex_hull_generalizer(context& ctx); + virtual ~core_convex_hull_generalizer() {} + virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level); + }; + class core_multi_generalizer : public core_generalizer { core_bool_inductive_generalizer m_gen; public: diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp index 50c3347ee..f840f19d6 100644 --- a/src/muz_qe/qe_lite.cpp +++ b/src/muz_qe/qe_lite.cpp @@ -1417,6 +1417,7 @@ namespace fm { fm(ast_manager & _m): m(_m), + m_is_variable(0), m_allocator("fm-elim"), m_util(m), m_bvar2expr(m), @@ -1424,6 +1425,9 @@ namespace fm { m_new_fmls(m), m_inconsistent_core(m) { m_cancel = false; + updt_params(); + m_counter = 0; + m_inconsistent = false; } ~fm() { diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp index 63e8ba700..7aade28e2 100644 --- a/src/muz_qe/rel_context.cpp +++ b/src/muz_qe/rel_context.cpp @@ -18,6 +18,8 @@ Revision History: Extracted from dl_context --*/ + + #include"rel_context.h" #include"dl_context.h" #include"dl_compiler.h" diff --git a/src/sat/sat_clause_use_list.h b/src/sat/sat_clause_use_list.h index ccf4b4a5b..0859439d5 100644 --- a/src/sat/sat_clause_use_list.h +++ b/src/sat/sat_clause_use_list.h @@ -20,6 +20,7 @@ Revision History: #define _SAT_CLAUSE_USE_LIST_H_ #include"sat_types.h" +#include"trace.h" namespace sat { @@ -35,6 +36,7 @@ namespace sat { #endif public: clause_use_list() { + STRACE("clause_use_list_bug", tout << "[cul_created] " << this << "\n";); #ifdef LAZY_USE_LIST m_size = 0; #endif @@ -51,22 +53,33 @@ namespace sat { bool empty() const { return size() == 0; } void insert(clause & c) { - SASSERT(!m_clauses.contains(&c)); SASSERT(!c.was_removed()); + STRACE("clause_use_list_bug", tout << "[cul_insert] " << this << " " << &c << "\n";); + SASSERT(!m_clauses.contains(&c)); + SASSERT(!c.was_removed()); m_clauses.push_back(&c); #ifdef LAZY_USE_LIST m_size++; #endif } + void erase_not_removed(clause & c) { + STRACE("clause_use_list_bug", tout << "[cul_erase_not_removed] " << this << " " << &c << "\n";); #ifdef LAZY_USE_LIST - SASSERT(m_clauses.contains(&c)); SASSERT(!c.was_removed()); m_clauses.erase(&c); m_size--; + SASSERT(m_clauses.contains(&c)); + SASSERT(!c.was_removed()); + m_clauses.erase(&c); + m_size--; #else m_clauses.erase(&c); #endif } + void erase(clause & c) { + STRACE("clause_use_list_bug", tout << "[cul_erase] " << this << " " << &c << "\n";); #ifdef LAZY_USE_LIST - SASSERT(m_clauses.contains(&c)); SASSERT(c.was_removed()); m_size--; + SASSERT(m_clauses.contains(&c)); + SASSERT(c.was_removed()); + m_size--; #else m_clauses.erase(&c); #endif @@ -80,6 +93,7 @@ namespace sat { } bool check_invariant() const; + // iterate & compress class iterator { clause_vector & m_clauses; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 47c4b6150..ba0c67235 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -146,8 +146,11 @@ namespace sat { m_need_cleanup = false; m_use_list.init(s.num_vars()); init_visited(); - if (learned) + bool learned_in_use_lists = false; + if (learned) { register_clauses(s.m_learned); + learned_in_use_lists = true; + } register_clauses(s.m_clauses); if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls)) @@ -179,7 +182,7 @@ namespace sat { if (!m_need_cleanup) { if (vars_eliminated) { // must remove learned clauses with eliminated variables - cleanup_clauses(s.m_learned, true, true); + cleanup_clauses(s.m_learned, true, true, learned_in_use_lists); } CASSERT("sat_solver", s.check_invariant()); TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout);); @@ -187,8 +190,8 @@ namespace sat { return; } cleanup_watches(); - cleanup_clauses(s.m_learned, true, vars_eliminated); - cleanup_clauses(s.m_clauses, false, vars_eliminated); + cleanup_clauses(s.m_learned, true, vars_eliminated, learned_in_use_lists); + cleanup_clauses(s.m_clauses, false, vars_eliminated, true); TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout);); CASSERT("sat_solver", s.check_invariant()); free_memory(); @@ -221,7 +224,7 @@ namespace sat { } } - void simplifier::cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated) { + void simplifier::cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists) { clause_vector::iterator it = cs.begin(); clause_vector::iterator it2 = it; clause_vector::iterator end = cs.end(); @@ -245,7 +248,7 @@ namespace sat { } } - if (cleanup_clause(c)) { + if (cleanup_clause(c, in_use_lists)) { s.del_clause(c); continue; } @@ -516,7 +519,7 @@ namespace sat { Return true if the clause is satisfied */ - bool simplifier::cleanup_clause(clause & c) { + bool simplifier::cleanup_clause(clause & c, bool in_use_list) { bool r = false; unsigned sz = c.size(); unsigned j = 0; @@ -529,7 +532,11 @@ namespace sat { break; case l_false: m_need_cleanup = true; - m_use_list.get(l).erase_not_removed(c); + if (in_use_list && !c.frozen()) { + // Remark: if in_use_list is false, then the given clause was not added to the use lists. + // Remark: frozen clauses are not added to the use lists. + m_use_list.get(l).erase_not_removed(c); + } break; case l_true: r = true; @@ -611,7 +618,7 @@ namespace sat { clause_use_list & occurs = m_use_list.get(l); occurs.erase_not_removed(c); m_sub_counter -= occurs.size()/2; - if (cleanup_clause(c)) { + if (cleanup_clause(c, true /* clause is in the use lists */)) { // clause was satisfied TRACE("elim_lit", tout << "clause was satisfied\n";); remove_clause(c); @@ -806,7 +813,7 @@ namespace sat { m_sub_counter--; TRACE("subsumption", tout << "next: " << c << "\n";); if (s.m_trail.size() > m_last_sub_trail_sz) { - if (cleanup_clause(c)) { + if (cleanup_clause(c, true /* clause is in the use_lists */)) { remove_clause(c); continue; } diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 44e2f0dee..96d346598 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -125,7 +125,7 @@ namespace sat { void collect_subsumed0(clause const & c1, clause_vector & out); void back_subsumption0(clause & c1); - bool cleanup_clause(clause & c); + bool cleanup_clause(clause & c, bool in_use_list); bool cleanup_clause(literal_vector & c); void propagate_unit(literal l); void elim_lit(clause & c, literal l); @@ -136,7 +136,7 @@ namespace sat { void subsume(); void cleanup_watches(); - void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated); + void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists); bool is_external(bool_var v) const; bool was_eliminated(bool_var v) const; diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index ef0b4ad6b..b5d8635da 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/src/shell/smtlib_frontend.cpp @@ -54,13 +54,19 @@ static void display_statistics() { } static void on_timeout() { - display_statistics(); - exit(0); + #pragma omp critical (g_display_stats) + { + display_statistics(); + exit(0); + } } static void on_ctrl_c(int) { signal (SIGINT, SIG_DFL); - display_statistics(); + #pragma omp critical (g_display_stats) + { + display_statistics(); + } raise(SIGINT); } @@ -83,9 +89,12 @@ unsigned read_smtlib_file(char const * benchmark_file) { } } - display_statistics(); - register_on_timeout_proc(0); - g_solver = 0; + #pragma omp critical (g_display_stats) + { + display_statistics(); + register_on_timeout_proc(0); + g_solver = 0; + } return solver.get_error_code(); } @@ -103,7 +112,6 @@ unsigned read_smtlib2_commands(char const * file_name) { install_subpaving_cmds(ctx); g_cmd_context = &ctx; - register_on_timeout_proc(on_timeout); signal(SIGINT, on_ctrl_c); bool result = true; @@ -119,8 +127,12 @@ unsigned read_smtlib2_commands(char const * file_name) { result = parse_smt2_commands(ctx, std::cin, true); } - display_statistics(); - g_cmd_context = 0; + + #pragma omp critical (g_display_stats) + { + display_statistics(); + g_cmd_context = 0; + } return result ? 0 : 1; } 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_arith_core.h b/src/smt/theory_arith_core.h index fafe73a79..195d78e25 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -408,7 +408,7 @@ namespace smt { mk_axiom(eqz, upper); rational k; if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) && - k.is_pos() && k < rational(512)) { + k.is_pos() && k < rational(8)) { rational j(0); #if 1 literal_buffer lits; diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h index 6c85e40b9..8463eb17f 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,17 +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) { enode* e = get_enode(i); @@ -720,22 +733,19 @@ namespace smt { } th_var v1 = to_var(i); th_var v2 = neg(v1); - TRACE("utvpi", tout << "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); + break; + } } + TRACE("utvpi", + tout << "Disparity: " << v1 << "\n"; for (unsigned j = 0; j < zero_v.size(); ++j) { tout << "decrement: " << zero_v[j] << "\n"; }); @@ -745,10 +755,9 @@ 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";); todo.push_back(k); } - } + } } SASSERT(m_graph.is_feasible()); DEBUG_CODE( @@ -764,10 +773,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();); } diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 2c2afab6f..71f4771a9 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -21,7 +21,7 @@ Notes: #include"goal_num_occurs.h" #include"cooperate.h" #include"ast_ll_pp.h" -#include"ast_smt2_pp.h" +#include"ast_pp.h" struct ctx_simplify_tactic::imp { struct cached_result { @@ -105,6 +105,7 @@ struct ctx_simplify_tactic::imp { } bool shared(expr * t) const { + TRACE("ctx_simplify_tactic_bug", tout << mk_pp(t, m) << "\n";); return t->get_ref_count() > 1 && m_occs.get_num_occs(t) > 1; } @@ -242,12 +243,13 @@ struct ctx_simplify_tactic::imp { } void assert_expr(expr * t, bool sign) { + expr * p = t; if (m.is_not(t)) { t = to_app(t)->get_arg(0); sign = !sign; } bool mk_scope = true; - if (shared(t)) { + if (shared(t) || shared(p)) { push(); mk_scope = false; assert_eq_core(t, sign ? m.mk_false() : m.mk_true()); @@ -457,7 +459,7 @@ struct ctx_simplify_tactic::imp { if (visit.is_marked(s)) { continue; } - visit.mark(s, true); + visit.mark(s, true); ++sz; for (unsigned i = 0; is_app(s) && i < to_app(s)->get_num_args(); ++i) { todo.push_back(to_app(s)->get_arg(i)); diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 363cf1df8..dd40e8453 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1022,13 +1022,15 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, split(x, x_sgn, x_sig, x_exp); split(y, y_sgn, y_sig, y_exp); - expr_ref c1(m), c2(m), y_is_nan(m), x_is_nzero(m), y_is_zero(m), c2_and(m); - mk_is_nan(x, c1); - mk_is_nan(y, y_is_nan); - mk_is_nzero(x, x_is_nzero); + expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), c1_and(m); + mk_is_zero(x, x_is_zero); mk_is_zero(y, y_is_zero); - m_simp.mk_and(x_is_nzero, y_is_zero, c2_and); - m_simp.mk_or(y_is_nan, c2_and, c2); + m_simp.mk_and(x_is_zero, y_is_zero, c1_and); + mk_is_nan(x, x_is_nan); + m_simp.mk_or(x_is_nan, c1_and, c1); + + mk_is_nan(y, y_is_nan); + c2 = y_is_nan; expr_ref c3(m); mk_float_lt(f, num, args, c3); @@ -1063,13 +1065,15 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, split(x, x_sgn, x_sig, x_exp); split(y, y_sgn, y_sig, y_exp); - expr_ref c1(m), c2(m), y_is_nan(m), y_is_nzero(m), x_is_zero(m), xy_is_zero(m); - mk_is_nan(x, c1); - mk_is_nan(y, y_is_nan); - mk_is_nzero(y, y_is_nzero); + expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), y_is_zero(m), x_is_zero(m), c1_and(m); + mk_is_zero(y, y_is_zero); mk_is_zero(x, x_is_zero); - m_simp.mk_and(y_is_nzero, x_is_zero, xy_is_zero); - m_simp.mk_or(y_is_nan, xy_is_zero, c2); + m_simp.mk_and(y_is_zero, x_is_zero, c1_and); + mk_is_nan(x, x_is_nan); + m_simp.mk_or(x_is_nan, c1_and, c1); + + mk_is_nan(y, y_is_nan); + c2 = y_is_nan; expr_ref c3(m); mk_float_gt(f, num, args, c3); @@ -1111,20 +1115,23 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar mk_minus_inf(f, ninf); mk_plus_inf(f, pinf); - expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m); - expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m); - expr_ref z_is_nan(m), z_is_zero(m), z_is_pos(m), z_is_inf(m); + expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_neg(m), x_is_inf(m); + expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_neg(m), y_is_inf(m); + expr_ref z_is_nan(m), z_is_zero(m), z_is_pos(m), z_is_neg(m), z_is_inf(m); mk_is_nan(x, x_is_nan); mk_is_zero(x, x_is_zero); mk_is_pos(x, x_is_pos); + mk_is_neg(x, x_is_neg); mk_is_inf(x, x_is_inf); mk_is_nan(y, y_is_nan); mk_is_zero(y, y_is_zero); mk_is_pos(y, y_is_pos); + mk_is_neg(y, y_is_neg); mk_is_inf(y, y_is_inf); mk_is_nan(z, z_is_nan); mk_is_zero(z, z_is_zero); mk_is_pos(z, z_is_pos); + mk_is_neg(z, z_is_neg); mk_is_inf(z, z_is_inf); dbg_decouple("fpa2bv_fma_x_is_nan", x_is_nan); @@ -1140,42 +1147,56 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar dbg_decouple("fpa2bv_fma_z_is_pos", z_is_pos); dbg_decouple("fpa2bv_fma_z_is_inf", z_is_inf); - expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m); - expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m); + expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m), c7(m); + expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m), v8(m); - // (x is NaN) || (y is NaN) -> NaN - m_simp.mk_or(x_is_nan, y_is_nan, c1); + expr_ref inf_xor(m), inf_cond(m); + m_simp.mk_xor(x_is_neg, y_is_neg, inf_xor); + m_simp.mk_xor(inf_xor, z_is_neg, inf_xor); + m_simp.mk_and(z_is_inf, inf_xor, inf_cond); + + // (x is NaN) || (y is NaN) || (z is Nan) -> NaN + m_simp.mk_or(x_is_nan, y_is_nan, z_is_nan, c1); v1 = nan; // (x is +oo) -> if (y is 0) then NaN else inf with y's sign. mk_is_pinf(x, c2); - expr_ref y_sgn_inf(m); + expr_ref y_sgn_inf(m), inf_or(m); mk_ite(y_is_pos, pinf, ninf, y_sgn_inf); - mk_ite(y_is_zero, nan, y_sgn_inf, v2); + m_simp.mk_or(y_is_zero, inf_cond, inf_or); + mk_ite(inf_or, nan, y_sgn_inf, v2); // (y is +oo) -> if (x is 0) then NaN else inf with x's sign. mk_is_pinf(y, c3); expr_ref x_sgn_inf(m); mk_ite(x_is_pos, pinf, ninf, x_sgn_inf); - mk_ite(x_is_zero, nan, x_sgn_inf, v3); + m_simp.mk_or(x_is_zero, inf_cond, inf_or); + mk_ite(inf_or, nan, x_sgn_inf, v3); // (x is -oo) -> if (y is 0) then NaN else inf with -y's sign. mk_is_ninf(x, c4); expr_ref neg_y_sgn_inf(m); mk_ite(y_is_pos, ninf, pinf, neg_y_sgn_inf); - mk_ite(y_is_zero, nan, neg_y_sgn_inf, v4); + m_simp.mk_or(y_is_zero, inf_cond, inf_or); + mk_ite(inf_or, nan, neg_y_sgn_inf, v4); // (y is -oo) -> if (x is 0) then NaN else inf with -x's sign. mk_is_ninf(y, c5); expr_ref neg_x_sgn_inf(m); mk_ite(x_is_pos, ninf, pinf, neg_x_sgn_inf); - mk_ite(x_is_zero, nan, neg_x_sgn_inf, v5); + m_simp.mk_or(x_is_zero, inf_cond, inf_or); + mk_ite(inf_or, nan, neg_x_sgn_inf, v5); + + // z is +-INF -> Z. + mk_is_inf(z, c6); + v6 = z; // (x is 0) || (y is 0) -> x but with sign = x.sign ^ y.sign - m_simp.mk_or(x_is_zero, y_is_zero, c6); + m_simp.mk_or(x_is_zero, y_is_zero, c7); expr_ref sign_xor(m); m_simp.mk_xor(x_is_pos, y_is_pos, sign_xor); - mk_ite(sign_xor, nzero, pzero, v6); + mk_ite(sign_xor, nzero, pzero, v7); + // else comes the fused multiplication. unsigned ebits = m_util.get_ebits(f->get_range()); @@ -1190,54 +1211,57 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar expr_ref c_sgn(m), c_sig(m), c_exp(m), c_lz(m); unpack(x, a_sgn, a_sig, a_exp, a_lz, true); unpack(y, b_sgn, b_sig, b_exp, b_lz, true); - unpack(z, c_sgn, c_sig, c_exp, c_lz, false); + unpack(z, c_sgn, c_sig, c_exp, c_lz, true); - expr_ref a_lz_ext(m), b_lz_ext(m); + expr_ref a_lz_ext(m), b_lz_ext(m), c_lz_ext(m); a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz); b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz); + c_lz_ext = m_bv_util.mk_zero_extend(2, c_lz); expr_ref a_sig_ext(m), b_sig_ext(m); a_sig_ext = m_bv_util.mk_zero_extend(sbits, a_sig); b_sig_ext = m_bv_util.mk_zero_extend(sbits, b_sig); - expr_ref a_exp_ext(m), b_exp_ext(m); + expr_ref a_exp_ext(m), b_exp_ext(m), c_exp_ext(m); a_exp_ext = m_bv_util.mk_sign_extend(2, a_exp); b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp); + c_exp_ext = m_bv_util.mk_sign_extend(2, c_exp); expr_ref mul_sgn(m), mul_sig(m), mul_exp(m); expr * signs[2] = { a_sgn, b_sgn }; - mul_sgn = m_bv_util.mk_bv_xor(2, signs); + mul_sgn = m_bv_util.mk_bv_xor(2, signs); dbg_decouple("fpa2bv_fma_mul_sgn", mul_sgn); - mul_exp = m_bv_util.mk_bv_sub( - m_bv_util.mk_bv_add(a_exp_ext, b_exp_ext), - m_bv_util.mk_bv_add(a_lz_ext, b_lz_ext)); + mul_exp = m_bv_util.mk_bv_add(m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext), + m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext)); + dbg_decouple("fpa2bv_fma_mul_exp", mul_exp); mul_sig = m_bv_util.mk_bv_mul(a_sig_ext, b_sig_ext); - dbg_decouple("fpa2bv_fma_mul_sig", mul_sig); SASSERT(m_bv_util.get_bv_size(mul_sig) == 2*sbits); + SASSERT(m_bv_util.get_bv_size(mul_exp) == ebits + 2); - // The result in `product' represents a number of the form 1.*** (unpacked) - // (product = mul_sgn/mul_sig/mul_exp and c_sgn/c_sig/c_exp is unpacked w/o normalization). + // The product has the form [-1][0].[2*sbits - 2]. + + // Extend c + c_sig = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits-1))); - // extend c. - c_sig = m_bv_util.mk_concat(c_sig, m_bv_util.mk_numeral(0, sbits)); - c_exp = m_bv_util.mk_sign_extend(2, c_exp); + SASSERT(m_bv_util.get_bv_size(mul_sig) == 2 * sbits); + SASSERT(m_bv_util.get_bv_size(c_sig) == 2 * sbits); expr_ref swap_cond(m); - swap_cond = m_bv_util.mk_sle(mul_exp, c_exp); + swap_cond = m_bv_util.mk_sle(mul_exp, c_exp_ext); SASSERT(is_well_sorted(m, swap_cond)); expr_ref e_sgn(m), e_sig(m), e_exp(m), f_sgn(m), f_sig(m), f_exp(m); m_simp.mk_ite(swap_cond, c_sgn, mul_sgn, e_sgn); m_simp.mk_ite(swap_cond, c_sig, mul_sig, e_sig); // has 2 * sbits - m_simp.mk_ite(swap_cond, c_exp, mul_exp, e_exp); // has ebits + 2 + m_simp.mk_ite(swap_cond, c_exp_ext, mul_exp, e_exp); // has ebits + 2 m_simp.mk_ite(swap_cond, mul_sgn, c_sgn, f_sgn); m_simp.mk_ite(swap_cond, mul_sig, c_sig, f_sig); // has 2 * sbits - m_simp.mk_ite(swap_cond, mul_exp, c_exp, f_exp); // has ebits + 2 + m_simp.mk_ite(swap_cond, mul_exp, c_exp_ext, f_exp); // has ebits + 2 SASSERT(is_well_sorted(m, e_sgn)); SASSERT(is_well_sorted(m, e_sig)); @@ -1247,26 +1271,94 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar SASSERT(is_well_sorted(m, f_exp)); expr_ref res_sgn(m), res_sig(m), res_exp(m); - add_core(2 * sbits, ebits + 2, rm, - e_sgn, e_sig, e_exp, f_sgn, f_sig, f_exp, - res_sgn, res_sig, res_exp); + + expr_ref exp_delta(m); + exp_delta = m_bv_util.mk_bv_sub(e_exp, f_exp); + dbg_decouple("fpa2bv_fma_add_exp_delta", exp_delta); - // Note: res_sig is now 2 * sbits + 4, i.e., `sbits' too much, which should go into a sticky bit. - unsigned sig_size = m_bv_util.get_bv_size(res_sig); - SASSERT(sig_size == (2*sbits+4)); + // cap the delta + expr_ref cap(m), cap_le_delta(m); + cap = m_bv_util.mk_numeral(sbits+3, ebits+2); + cap_le_delta = m_bv_util.mk_ule(exp_delta, cap); + m_simp.mk_ite(cap_le_delta, cap, exp_delta, exp_delta); + SASSERT(m_bv_util.get_bv_size(exp_delta) == ebits+2); + dbg_decouple("fpa2bv_fma_add_exp_delta_capped", exp_delta); + + // Alignment shift with sticky bit computation. + expr_ref big_f_sig(m); + big_f_sig = m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits+4)); + SASSERT(is_well_sorted(m, big_f_sig)); - // Note: res_exp is 2 bits too wide. - unsigned exp_size = m_bv_util.get_bv_size(res_exp); - SASSERT(exp_size == ebits+4); - res_exp = m_bv_util.mk_extract(ebits+1, 0, res_exp); + expr_ref shifted_big(m), shifted_f_sig(m), sticky_raw(m); + shifted_big = m_bv_util.mk_bv_lshr(big_f_sig, m_bv_util.mk_concat(m_bv_util.mk_numeral(0, (2*(sbits+4))-(ebits+2)), exp_delta)); + shifted_f_sig = m_bv_util.mk_extract((2*(sbits+4)-1), (sbits+4), shifted_big); + SASSERT(is_well_sorted(m, shifted_f_sig)); - expr_ref sticky(m); - sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sbits, 0, res_sig)); - res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(2*sbits+3, sbits+1, res_sig), sticky); + sticky_raw = m_bv_util.mk_extract(sbits+3, 0, shifted_big); + expr_ref sticky(m), sticky_eq(m), nil_sbit4(m), one_sbit4(m); + nil_sbit4 = m_bv_util.mk_numeral(0, sbits+4); + one_sbit4 = m_bv_util.mk_numeral(1, sbits+4); + m_simp.mk_eq(sticky_raw, nil_sbit4, sticky_eq); + m_simp.mk_ite(sticky_eq, nil_sbit4, one_sbit4, sticky); + SASSERT(is_well_sorted(m, sticky)); + + expr * or_args[2] = { shifted_f_sig, sticky }; + shifted_f_sig = m_bv_util.mk_bv_or(2, or_args); + SASSERT(is_well_sorted(m, shifted_f_sig)); - sig_size = m_bv_util.get_bv_size(res_sig); - SASSERT(sig_size == sbits+4); + expr_ref eq_sgn(m); + m_simp.mk_eq(e_sgn, f_sgn, eq_sgn); + + // two extra bits for catching the overflow. + e_sig = m_bv_util.mk_zero_extend(2, e_sig); + shifted_f_sig = m_bv_util.mk_zero_extend(2, shifted_f_sig); + SASSERT(m_bv_util.get_bv_size(e_sig) == sbits+6); + SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == sbits+6); + + dbg_decouple("fpa2bv_fma_add_e_sig", e_sig); + dbg_decouple("fpa2bv_fma_add_shifted_f_sig", shifted_f_sig); + + expr_ref sum(m); + m_simp.mk_ite(eq_sgn, + m_bv_util.mk_bv_add(e_sig, shifted_f_sig), // ADD LZ + m_bv_util.mk_bv_sub(e_sig, shifted_f_sig), + sum); + + SASSERT(is_well_sorted(m, sum)); + + dbg_decouple("fpa2bv_fma_add_sum", sum); + + expr_ref sign_bv(m), n_sum(m); + sign_bv = m_bv_util.mk_extract(sbits+4, sbits+4, sum); + n_sum = m_bv_util.mk_bv_neg(sum); + + dbg_decouple("fpa2bv_fma_add_sign_bv", sign_bv); + dbg_decouple("fpa2bv_fma_add_n_sum", n_sum); + + family_id bvfid = m_bv_util.get_fid(); + + expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m); + expr_ref not_e_sgn(m), not_f_sgn(m), not_sign_bv(m); + not_e_sgn = m_bv_util.mk_bv_not(e_sgn); + not_f_sgn = m_bv_util.mk_bv_not(f_sgn); + not_sign_bv = m_bv_util.mk_bv_not(sign_bv); + res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_e_sgn, e_sgn, sign_bv); + res_sgn_c2 = m.mk_app(bvfid, OP_BAND, e_sgn, not_f_sgn, not_sign_bv); + res_sgn_c3 = m.mk_app(bvfid, OP_BAND, e_sgn, f_sgn); + expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 }; + res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args); + + expr_ref res_sig_eq(m), sig_abs(m), one_1(m); + one_1 = m_bv_util.mk_numeral(1, 1); + m_simp.mk_eq(sign_bv, one_1, res_sig_eq); + m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs); + + dbg_decouple("fpa2bv_fma_add_sig_abs", sig_abs); + + res_sig = m_bv_util.mk_extract(sbits+3, 0, sig_abs); + res_exp = m_bv_util.mk_bv_sub(e_exp, c_lz_ext); + expr_ref is_zero_sig(m), nil_sbits4(m); nil_sbits4 = m_bv_util.mk_numeral(0, sbits+4); m_simp.mk_eq(res_sig, nil_sbits4, is_zero_sig); @@ -1281,10 +1373,11 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar expr_ref rounded(m); round(f->get_range(), rm, res_sgn, res_sig, res_exp, rounded); - mk_ite(is_zero_sig, zero_case, rounded, v7); + mk_ite(is_zero_sig, zero_case, rounded, v8); // And finally, we tie them together. - mk_ite(c6, v6, v7, result); + mk_ite(c7, v7, v8, result); + mk_ite(c6, v6, result, result); mk_ite(c5, v5, result, result); mk_ite(c4, v4, result, result); mk_ite(c3, v3, result, result); @@ -1293,7 +1386,7 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar SASSERT(is_well_sorted(m, result)); - TRACE("fpa2bv_mul", tout << "MUL = " << mk_ismt2_pp(result, m) << std::endl; ); + TRACE("fpa2bv_fma_", tout << "FMA = " << mk_ismt2_pp(result, m) << std::endl; ); } void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { @@ -1528,6 +1621,26 @@ void fpa2bv_converter::mk_is_pzero(func_decl * f, unsigned num, expr * const * a m_simp.mk_and(a0_is_pos, a0_is_zero, result); } +void fpa2bv_converter::mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + mk_is_nan(args[0], result); +} + +void fpa2bv_converter::mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + mk_is_inf(args[0], result); +} + +void fpa2bv_converter::mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + mk_is_normal(args[0], result); +} + +void fpa2bv_converter::mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + mk_is_denormal(args[0], result); +} + void fpa2bv_converter::mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); mk_is_neg(args[0], result); @@ -2571,9 +2684,13 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { sz = bv_mdl->get_num_functions(); for (unsigned i = 0; i < sz; i++) { - func_decl * c = bv_mdl->get_function(i); - if (!seen.contains(c)) - float_mdl->register_decl(c, bv_mdl->get_const_interp(c)); + func_decl * f = bv_mdl->get_function(i); + if (!seen.contains(f)) + { + TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl; ); + func_interp * val = bv_mdl->get_func_interp(f); + float_mdl->register_decl(f, val); + } } sz = bv_mdl->get_num_uninterpreted_sorts(); diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h index 2a68342f8..821618bae 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/src/tactic/fpa/fpa2bv_converter.h @@ -116,6 +116,10 @@ public: void mk_is_nzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_pzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h index 3398874f5..24e275c0d 100644 --- a/src/tactic/fpa/fpa2bv_rewriter.h +++ b/src/tactic/fpa/fpa2bv_rewriter.h @@ -29,9 +29,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { ast_manager & m_manager; expr_ref_vector m_out; fpa2bv_converter & m_conv; - sort_ref_vector m_bindings; - expr_ref_vector m_mappings; - + sort_ref_vector m_bindings; unsigned long long m_max_memory; unsigned m_max_steps; @@ -42,8 +40,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { m_manager(m), m_out(m), m_conv(c), - m_bindings(m), - m_mappings(m) { + m_bindings(m) { updt_params(p); // We need to make sure that the mananger has the BV plugin loaded. symbol s_bv("bv"); @@ -135,6 +132,10 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FLOAT_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_NZERO: m_conv.mk_is_nzero(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_PZERO: m_conv.mk_is_pzero(f, num, args, result); return BR_DONE; + case OP_FLOAT_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE; + case OP_FLOAT_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE; + case OP_FLOAT_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE; + case OP_FLOAT_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE; case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE; case OP_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; @@ -177,7 +178,6 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { new_bindings.push_back(q->get_decl_sort(i)); SASSERT(new_bindings.size() == q->get_num_decls()); m_bindings.append(new_bindings); - m_mappings.resize(m_bindings.size(), 0); } return true; } @@ -215,8 +215,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(), old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns); result_pr = 0; - m_bindings.shrink(old_sz); - m_mappings.shrink(old_sz); + m_bindings.shrink(old_sz); TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " << mk_ismt2_pp(old_q->get_expr(), m()) << std::endl << " new body: " << mk_ismt2_pp(new_body, m()) << std::endl; @@ -243,10 +242,9 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { new_exp); } else - new_exp = m().mk_var(t->get_idx(), s); - m_mappings[inx] = new_exp; + new_exp = m().mk_var(t->get_idx(), s); - result = m_mappings[inx].get(); + result = new_exp; result_pr = 0; TRACE("fpa2bv", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;); return true; diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index f49ce8422..69e1c8bc3 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -1370,7 +1370,7 @@ class sls_tactic : public tactic { void updt_params(params_ref const & p) { m_produce_models = p.get_bool("produce_models", false); - m_max_restarts = p.get_uint("sls_restarts", -1); + m_max_restarts = p.get_uint("sls_restarts", (unsigned)-1); m_tracker.set_random_seed(p.get_uint("random_seed", 0)); m_plateau_limit = p.get_uint("plateau_limit", 100); } @@ -1612,7 +1612,7 @@ class sls_tactic : public tactic { lbool search(goal_ref const & g) { lbool res = l_undef; double score = 0.0, old_score = 0.0; - unsigned new_const = -1, new_bit = 0; + unsigned new_const = (unsigned)-1, new_bit = 0; mpz new_value; move_type move; @@ -1631,7 +1631,7 @@ class sls_tactic : public tactic { checkpoint(); old_score = score; - new_const = -1; + new_const = (unsigned)-1; ptr_vector & to_evaluate = m_tracker.get_unsat_constants(g); diff --git a/src/util/bit_vector.cpp b/src/util/bit_vector.cpp index 0d67f1f79..6885b93e8 100644 --- a/src/util/bit_vector.cpp +++ b/src/util/bit_vector.cpp @@ -22,6 +22,8 @@ Revision History: #define DEFAULT_CAPACITY 2 +#define MK_MASK(_num_bits_) ((1U << _num_bits_) - 1) + void bit_vector::expand_to(unsigned new_capacity) { unsigned * new_data = alloc_svect(unsigned, new_capacity); memset(new_data, 0, new_capacity * sizeof(unsigned)); @@ -51,7 +53,7 @@ void bit_vector::resize(unsigned new_size, bool val) { unsigned ewidx = num_words(new_size); unsigned * begin = m_data + bwidx; unsigned pos = m_num_bits % 32; - unsigned mask = (1 << pos) - 1; + unsigned mask = MK_MASK(pos); int cval; if (val) { @@ -128,7 +130,7 @@ bool bit_vector::operator==(bit_vector const & source) const { return false; } unsigned bit_rest = source.m_num_bits % 32; - unsigned mask = (1 << bit_rest) - 1; + unsigned mask = MK_MASK(bit_rest); if (mask == 0) mask = UINT_MAX; return (m_data[i] & mask) == (source.m_data[i] & mask); } @@ -149,7 +151,7 @@ bit_vector & bit_vector::operator|=(bit_vector const & source) { unsigned i = 0; for (i = 0; i < n2 - 1; i++) m_data[i] |= source.m_data[i]; - unsigned mask = (1 << bit_rest) - 1; + unsigned mask = MK_MASK(bit_rest); m_data[i] |= source.m_data[i] & mask; } return *this; @@ -175,7 +177,7 @@ bit_vector & bit_vector::operator&=(bit_vector const & source) { else { for (i = 0; i < n2 - 1; i++) m_data[i] &= source.m_data[i]; - unsigned mask = (1 << bit_rest) - 1; + unsigned mask = MK_MASK(bit_rest); m_data[i] &= (source.m_data[i] & mask); } diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h index 2c641c5a6..0ccdeae9e 100644 --- a/src/util/bit_vector.h +++ b/src/util/bit_vector.h @@ -28,6 +28,7 @@ COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); #define BV_DEFAULT_CAPACITY 2 class bit_vector { +protected: unsigned m_num_bits; unsigned m_capacity; //!< in words unsigned * m_data; @@ -64,6 +65,13 @@ public: m_data(0) { } + bit_vector(unsigned reserve_num_bits) : + m_num_bits(0), + m_capacity(num_words(reserve_num_bits)), + m_data(alloc_svect(unsigned, m_capacity)) { + memset(m_data, 0, m_capacity * sizeof(unsigned)); + } + bit_vector(bit_vector const & source): m_num_bits(source.m_num_bits), m_capacity(source.m_capacity),