mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Leonardo de Moura 2013-06-13 13:45:55 -07:00
parent 40b1137b30 6184c5fdbc
commit 894fd8b967
51 changed files with 2127 additions and 1197 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_ast.cpp
View file

@ -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;

133
src/api/api_bv.cpp
View file

@ -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);
}

2
src/api/dotnet/Microsoft.Z3.csproj
View file

@ -399,4 +399,4 @@
<Target Name="AfterBuild">
</Target>
-->
</Project>
</Project>

46
src/api/ml/README-test-win
View file

@ -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.

46
src/api/ml/README-win
View file

@ -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!

6
src/api/ml/build-lib.cmd
View file

@ -1,3 +1,3 @@
@echo off
call .\compile_mlapi.cmd ..\include ..\bin ..\bin
@echo off
call .\compile_mlapi.cmd ..\include ..\bin ..\bin

38
src/api/ml/build-test.cmd
View file

@ -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= <ocaml_version
if %OCAML_VERSION% GEQ 3.11 (
set XCFLAGS=
) else (
set XCFLAGS=/nologo /MT /DWIN32
)
ocamlc -w A -ccopt "%XCFLAGS%" -o test_mlapi_byte.exe -I ..\..\ocaml z3.cma test_mlapi.ml
ocamlopt -w A -ccopt "%XCFLAGS%" -o test_mlapi.exe -I ..\..\ocaml z3.cmxa test_mlapi.ml
@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= <ocaml_version
if %OCAML_VERSION% GEQ 3.11 (
set XCFLAGS=
) else (
set XCFLAGS=/nologo /MT /DWIN32
)
ocamlc -w A -ccopt "%XCFLAGS%" -o test_mlapi_byte.exe -I ..\..\ocaml z3.cma test_mlapi.ml
ocamlopt -w A -ccopt "%XCFLAGS%" -o test_mlapi.exe -I ..\..\ocaml z3.cmxa test_mlapi.ml

10
src/api/ml/exec.cmd
View file

@ -1,5 +1,5 @@
@echo off
SETLOCAL
set PATH=..\..\bin;%PATH%
test_mlapi.exe
ENDLOCAL
@echo off
SETLOCAL
set PATH=..\..\bin;%PATH%
test_mlapi.exe
ENDLOCAL

14
src/ast/float_decl_plugin.cpp
View file

@ -255,7 +255,11 @@ func_decl * float_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_param
case OP_FLOAT_IS_ZERO: name = "isZero"; break;
case OP_FLOAT_IS_NZERO: name = "isNZero"; break;
case OP_FLOAT_IS_PZERO: name = "isPZero"; break;
case OP_FLOAT_IS_SIGN_MINUS: name = "isSignMinus"; break;
case OP_FLOAT_IS_SIGN_MINUS: name = "isSignMinus"; break;
case OP_FLOAT_IS_NAN: name = "isNaN"; break;
case OP_FLOAT_IS_INF: name = "isInfinite"; break;
case OP_FLOAT_IS_NORMAL: name = "isNormal"; break;
case OP_FLOAT_IS_SUBNORMAL: name = "isSubnormal"; break;
default:
UNREACHABLE();
break;
@ -415,6 +419,10 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_FLOAT_IS_NZERO:
case OP_FLOAT_IS_PZERO:
case OP_FLOAT_IS_SIGN_MINUS:
case OP_FLOAT_IS_NAN:
case OP_FLOAT_IS_INF:
case OP_FLOAT_IS_NORMAL:
case OP_FLOAT_IS_SUBNORMAL:
return mk_unary_rel_decl(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_ABS:
case OP_FLOAT_UMINUS:
@ -473,9 +481,13 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & 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));

12
src/ast/float_decl_plugin.h
View file

@ -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); }

44
src/ast/rewriter/float_rewriter.cpp
View file

@ -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)) {

4
src/ast/rewriter/float_rewriter.h
View file

@ -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);

1864
src/ast/rewriter/poly_rewriter_def.h
View file

File diff suppressed because it is too large Load diff

40
src/ast/simplifier/bv_simplifier_plugin.cpp
View file

@ -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

1
src/ast/simplifier/poly_simplifier_plugin.cpp
View file

@ -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;
}

2
src/cmd_context/README
View file

@ -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.
It is also provides the solver abstraction to plugin solvers in this kind of front-end.

2
src/math/euclid/README
View file

@ -1,2 +1,2 @@
Basic Euclidean solver for linear integer equations.
This solver generates "explanations".
This solver generates "explanations".

2
src/math/interval/README
View file

@ -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.
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.

2
src/math/polynomial/README
View file

@ -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.
Multivariate polynomial factorization does not work yet (polynomial_factorization.*), and it is disabled.

14
src/muz_qe/dl_base.h
View file

@ -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) {

30
src/muz_qe/dl_bmc_engine.cpp
View file

@ -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;
}

81
src/muz_qe/dl_check_table.cpp
View file

@ -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<table_join_fn> m_tocheck;
scoped_ptr<table_join_fn> 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<table_union_fn> m_tocheck;
scoped_ptr<table_union_fn> 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<table_transformer_fn> m_checker;
scoped_ptr<table_transformer_fn> 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<table_transformer_fn> m_checker;
scoped_ptr<table_transformer_fn> 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<table_transformer_fn> m_checker;
scoped_ptr<table_transformer_fn> 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<table_intersection_filter_fn> m_checker;
scoped_ptr<table_intersection_filter_fn> m_tocheck;

10
src/muz_qe/dl_check_table.h
View file

@ -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,

125
src/muz_qe/dl_compiler.cpp
View file

@ -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<expr> 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<sort> 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<sort> 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_index<ft_len; tail_index++) {
app * t = r->get_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();
}

2
src/muz_qe/dl_compiler.h
View file

@ -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);
/**

59
src/muz_qe/dl_instruction.cpp
View file

@ -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);

2
src/muz_qe/dl_instruction.h
View file

@ -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,

46
src/muz_qe/dl_relation_manager.cpp
View file

@ -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<relation_mutator_fn> m_filter;
@ -1387,6 +1394,45 @@ namespace datalog {
}
class relation_manager::default_table_filter_interpreted_and_project_fn
: public table_transformer_fn {
scoped_ptr<table_mutator_fn> m_filter;
scoped_ptr<table_transformer_fn> 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,

7
src/muz_qe/dl_relation_manager.h
View file

@ -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.

15
src/muz_qe/dl_table_relation.cpp
View file

@ -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<const table_relation &>(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<table_intersection_filter_fn> m_tfun;
public:

2
src/muz_qe/dl_table_relation.h
View file

@ -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,

3
src/muz_qe/fixedpoint_params.pyg
View file

@ -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'),
))

14
src/muz_qe/pdr_context.cpp
View file

@ -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));

171
src/muz_qe/pdr_generalizers.cpp
View file

@ -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

17
src/muz_qe/pdr_generalizers.h
View file

@ -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<func_decl, expr*> m_left;
obj_map<func_decl, expr*> 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:

4
src/muz_qe/qe_lite.cpp
View file

@ -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() {

2
src/muz_qe/rel_context.cpp
View file

@ -18,6 +18,8 @@ Revision History:
Extracted from dl_context
--*/
#include"rel_context.h"
#include"dl_context.h"
#include"dl_compiler.h"

20
src/sat/sat_clause_use_list.h
View file

@ -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;

27
src/sat/sat_simplifier.cpp
View file

@ -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;
}

4
src/sat/sat_simplifier.h
View file

@ -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;

30
src/shell/smtlib_frontend.cpp
View file

@ -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;
}

2
src/smt/database.smt
View file

@ -311,4 +311,4 @@
(= (?is (?select (?select (?asElems e) a) i)
(?elemtype (?typeof a))) 1)
:pats { (?select (?select (?asElems e) a) i) })
)
)

2
src/smt/theory_arith_core.h
View file

@ -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;

64
src/smt/theory_utvpi_def.h
View file

@ -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<typename Ext>
void theory_utvpi<Ext>::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<typename Ext>
void theory_utvpi<Ext>::init_model(model_generator & m) {
void theory_utvpi<Ext>::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(););
}

8
src/tactic/core/ctx_simplify_tactic.cpp
View file

@ -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));

243
src/tactic/fpa/fpa2bv_converter.cpp
View file

@ -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();

4
src/tactic/fpa/fpa2bv_converter.h
View file

@ -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);

20
src/tactic/fpa/fpa2bv_rewriter.h
View file

@ -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;

6
src/tactic/sls/sls_tactic.cpp
View file

@ -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<func_decl> & to_evaluate = m_tracker.get_unsat_constants(g);

10
src/util/bit_vector.cpp
View file

@ -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);
}

8
src/util/bit_vector.h
View file

@ -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),