mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge remote-tracking branch 'upstream/master' into fix-length-testing
This commit is contained in:
commit
2ffffa9bed
|
@ -7,6 +7,19 @@
|
|||
# the C++ standard library in resulting in a link failure.
|
||||
project(Z3_C_EXAMPLE C CXX)
|
||||
cmake_minimum_required(VERSION 2.8.12)
|
||||
|
||||
# Set C version required to C99
|
||||
if ("${CMAKE_VERSION}" VERSION_LESS "3.1")
|
||||
if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR
|
||||
("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang"))
|
||||
set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -std=c99 ")
|
||||
endif()
|
||||
else()
|
||||
set(CMAKE_C_STANDARD_REQUIRED ON)
|
||||
set(CMAKE_C_STANDARD 99)
|
||||
set(CMAKE_C_EXTENSIONS OFF)
|
||||
endif()
|
||||
|
||||
find_package(Z3
|
||||
REQUIRED
|
||||
CONFIG
|
||||
|
|
|
@ -2769,80 +2769,279 @@ void fpa_example() {
|
|||
double_sort = Z3_mk_fpa_sort(ctx, 11, 53);
|
||||
rm_sort = Z3_mk_fpa_rounding_mode_sort(ctx);
|
||||
|
||||
// Show that there are x, y s.t. (x + y) = 42.0 (with rounding mode).
|
||||
s_rm = Z3_mk_string_symbol(ctx, "rm");
|
||||
rm = Z3_mk_const(ctx, s_rm, rm_sort);
|
||||
s_x = Z3_mk_string_symbol(ctx, "x");
|
||||
s_y = Z3_mk_string_symbol(ctx, "y");
|
||||
x = Z3_mk_const(ctx, s_x, double_sort);
|
||||
y = Z3_mk_const(ctx, s_y, double_sort);
|
||||
n = Z3_mk_fpa_numeral_double(ctx, 42.0, double_sort);
|
||||
|
||||
s_x_plus_y = Z3_mk_string_symbol(ctx, "x_plus_y");
|
||||
x_plus_y = Z3_mk_const(ctx, s_x_plus_y, double_sort);
|
||||
c1 = Z3_mk_eq(ctx, x_plus_y, Z3_mk_fpa_add(ctx, rm, x, y));
|
||||
|
||||
args[0] = c1;
|
||||
args[1] = Z3_mk_eq(ctx, x_plus_y, n);
|
||||
c2 = Z3_mk_and(ctx, 2, (Z3_ast*)&args);
|
||||
|
||||
args2[0] = c2;
|
||||
args2[1] = Z3_mk_not(ctx, Z3_mk_eq(ctx, rm, Z3_mk_fpa_rtz(ctx)));
|
||||
c3 = Z3_mk_and(ctx, 2, (Z3_ast*)&args2);
|
||||
|
||||
and_args[0] = Z3_mk_not(ctx, Z3_mk_fpa_is_zero(ctx, y));
|
||||
and_args[1] = Z3_mk_not(ctx, Z3_mk_fpa_is_nan(ctx, y));
|
||||
and_args[2] = Z3_mk_not(ctx, Z3_mk_fpa_is_infinite(ctx, y));
|
||||
args3[0] = c3;
|
||||
args3[1] = Z3_mk_and(ctx, 3, and_args);
|
||||
c4 = Z3_mk_and(ctx, 2, (Z3_ast*)&args3);
|
||||
|
||||
printf("c4: %s\n", Z3_ast_to_string(ctx, c4));
|
||||
Z3_solver_push(ctx, s);
|
||||
Z3_solver_assert(ctx, s, c4);
|
||||
check(ctx, s, Z3_L_TRUE);
|
||||
Z3_solver_pop(ctx, s, 1);
|
||||
|
||||
// Show that the following are equal:
|
||||
// (fp #b0 #b10000000001 #xc000000000000)
|
||||
// ((_ to_fp 11 53) #x401c000000000000))
|
||||
// ((_ to_fp 11 53) RTZ 1.75 2)))
|
||||
// ((_ to_fp 11 53) RTZ 7.0)))
|
||||
|
||||
Z3_solver_push(ctx, s);
|
||||
c1 = Z3_mk_fpa_fp(ctx,
|
||||
Z3_mk_numeral(ctx, "0", Z3_mk_bv_sort(ctx, 1)),
|
||||
Z3_mk_numeral(ctx, "1025", Z3_mk_bv_sort(ctx, 11)),
|
||||
// Show that there are x, y s.t. (x + y) = 42.0 (with rounding mode).
|
||||
s_rm = Z3_mk_string_symbol(ctx, "rm");
|
||||
rm = Z3_mk_const(ctx, s_rm, rm_sort);
|
||||
s_x = Z3_mk_string_symbol(ctx, "x");
|
||||
s_y = Z3_mk_string_symbol(ctx, "y");
|
||||
x = Z3_mk_const(ctx, s_x, double_sort);
|
||||
y = Z3_mk_const(ctx, s_y, double_sort);
|
||||
n = Z3_mk_fpa_numeral_double(ctx, 42.0, double_sort);
|
||||
|
||||
s_x_plus_y = Z3_mk_string_symbol(ctx, "x_plus_y");
|
||||
x_plus_y = Z3_mk_const(ctx, s_x_plus_y, double_sort);
|
||||
c1 = Z3_mk_eq(ctx, x_plus_y, Z3_mk_fpa_add(ctx, rm, x, y));
|
||||
|
||||
args[0] = c1;
|
||||
args[1] = Z3_mk_eq(ctx, x_plus_y, n);
|
||||
c2 = Z3_mk_and(ctx, 2, (Z3_ast*)&args);
|
||||
|
||||
args2[0] = c2;
|
||||
args2[1] = Z3_mk_not(ctx, Z3_mk_eq(ctx, rm, Z3_mk_fpa_rtz(ctx)));
|
||||
c3 = Z3_mk_and(ctx, 2, (Z3_ast*)&args2);
|
||||
|
||||
and_args[0] = Z3_mk_not(ctx, Z3_mk_fpa_is_zero(ctx, y));
|
||||
and_args[1] = Z3_mk_not(ctx, Z3_mk_fpa_is_nan(ctx, y));
|
||||
and_args[2] = Z3_mk_not(ctx, Z3_mk_fpa_is_infinite(ctx, y));
|
||||
args3[0] = c3;
|
||||
args3[1] = Z3_mk_and(ctx, 3, and_args);
|
||||
c4 = Z3_mk_and(ctx, 2, (Z3_ast*)&args3);
|
||||
|
||||
printf("c4: %s\n", Z3_ast_to_string(ctx, c4));
|
||||
Z3_solver_push(ctx, s);
|
||||
Z3_solver_assert(ctx, s, c4);
|
||||
check(ctx, s, Z3_L_TRUE);
|
||||
Z3_solver_pop(ctx, s, 1);
|
||||
|
||||
// Show that the following are equal:
|
||||
// (fp #b0 #b10000000001 #xc000000000000)
|
||||
// ((_ to_fp 11 53) #x401c000000000000))
|
||||
// ((_ to_fp 11 53) RTZ 1.75 2)))
|
||||
// ((_ to_fp 11 53) RTZ 7.0)))
|
||||
|
||||
Z3_solver_push(ctx, s);
|
||||
c1 = Z3_mk_fpa_fp(ctx,
|
||||
Z3_mk_numeral(ctx, "0", Z3_mk_bv_sort(ctx, 1)),
|
||||
Z3_mk_numeral(ctx, "1025", Z3_mk_bv_sort(ctx, 11)),
|
||||
Z3_mk_numeral(ctx, "3377699720527872", Z3_mk_bv_sort(ctx, 52)));
|
||||
c2 = Z3_mk_fpa_to_fp_bv(ctx,
|
||||
Z3_mk_numeral(ctx, "4619567317775286272", Z3_mk_bv_sort(ctx, 64)),
|
||||
Z3_mk_fpa_sort(ctx, 11, 53));
|
||||
c2 = Z3_mk_fpa_to_fp_bv(ctx,
|
||||
Z3_mk_numeral(ctx, "4619567317775286272", Z3_mk_bv_sort(ctx, 64)),
|
||||
Z3_mk_fpa_sort(ctx, 11, 53));
|
||||
c3 = Z3_mk_fpa_to_fp_int_real(ctx,
|
||||
Z3_mk_fpa_rtz(ctx),
|
||||
Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)), /* exponent */
|
||||
Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)), /* exponent */
|
||||
Z3_mk_numeral(ctx, "1.75", Z3_mk_real_sort(ctx)), /* significand */
|
||||
Z3_mk_fpa_sort(ctx, 11, 53));
|
||||
c4 = Z3_mk_fpa_to_fp_real(ctx,
|
||||
Z3_mk_fpa_rtz(ctx),
|
||||
Z3_mk_numeral(ctx, "7.0", Z3_mk_real_sort(ctx)),
|
||||
Z3_mk_fpa_sort(ctx, 11, 53));
|
||||
args3[0] = Z3_mk_eq(ctx, c1, c2);
|
||||
args3[1] = Z3_mk_eq(ctx, c1, c3);
|
||||
args3[2] = Z3_mk_eq(ctx, c1, c4);
|
||||
c5 = Z3_mk_and(ctx, 3, args3);
|
||||
|
||||
printf("c5: %s\n", Z3_ast_to_string(ctx, c5));
|
||||
Z3_solver_assert(ctx, s, c5);
|
||||
check(ctx, s, Z3_L_TRUE);
|
||||
Z3_solver_pop(ctx, s, 1);
|
||||
|
||||
Z3_mk_fpa_rtz(ctx),
|
||||
Z3_mk_numeral(ctx, "7.0", Z3_mk_real_sort(ctx)),
|
||||
Z3_mk_fpa_sort(ctx, 11, 53));
|
||||
args3[0] = Z3_mk_eq(ctx, c1, c2);
|
||||
args3[1] = Z3_mk_eq(ctx, c1, c3);
|
||||
args3[2] = Z3_mk_eq(ctx, c1, c4);
|
||||
c5 = Z3_mk_and(ctx, 3, args3);
|
||||
|
||||
printf("c5: %s\n", Z3_ast_to_string(ctx, c5));
|
||||
Z3_solver_assert(ctx, s, c5);
|
||||
check(ctx, s, Z3_L_TRUE);
|
||||
Z3_solver_pop(ctx, s, 1);
|
||||
|
||||
del_solver(ctx, s);
|
||||
Z3_del_context(ctx);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Demonstrates some basic features of model construction
|
||||
*/
|
||||
|
||||
void mk_model_example() {
|
||||
Z3_context ctx;
|
||||
Z3_model m;
|
||||
Z3_sort intSort;
|
||||
Z3_symbol aSymbol, bSymbol, cSymbol;
|
||||
Z3_func_decl aFuncDecl, bFuncDecl, cFuncDecl;
|
||||
Z3_ast aApp, bApp, cApp;
|
||||
Z3_sort int2intArraySort;
|
||||
Z3_ast zeroNumeral, oneNumeral, twoNumeral, threeNumeral, fourNumeral;
|
||||
Z3_sort arrayDomain[1];
|
||||
Z3_func_decl cAsFuncDecl;
|
||||
Z3_func_interp cAsFuncInterp;
|
||||
Z3_ast_vector zeroArgs;
|
||||
Z3_ast_vector oneArgs;
|
||||
Z3_ast cFuncDeclAsArray;
|
||||
Z3_string modelAsString;
|
||||
|
||||
printf("\nmk_model_example\n");
|
||||
ctx = mk_context();
|
||||
// Construct empty model
|
||||
m = Z3_mk_model(ctx);
|
||||
Z3_model_inc_ref(ctx, m);
|
||||
|
||||
// Create constants "a" and "b"
|
||||
intSort = Z3_mk_int_sort(ctx);
|
||||
aSymbol = Z3_mk_string_symbol(ctx, "a");
|
||||
aFuncDecl = Z3_mk_func_decl(ctx, aSymbol,
|
||||
/*domain_size=*/0,
|
||||
/*domain=*/NULL,
|
||||
/*range=*/intSort);
|
||||
aApp = Z3_mk_app(ctx, aFuncDecl,
|
||||
/*num_args=*/0,
|
||||
/*args=*/NULL);
|
||||
bSymbol = Z3_mk_string_symbol(ctx, "b");
|
||||
bFuncDecl = Z3_mk_func_decl(ctx, bSymbol,
|
||||
/*domain_size=*/0,
|
||||
/*domain=*/NULL,
|
||||
/*range=*/intSort);
|
||||
bApp = Z3_mk_app(ctx, bFuncDecl,
|
||||
/*num_args=*/0,
|
||||
/*args=*/NULL);
|
||||
|
||||
// Create array "c" that maps int to int.
|
||||
cSymbol = Z3_mk_string_symbol(ctx, "c");
|
||||
int2intArraySort = Z3_mk_array_sort(ctx,
|
||||
/*domain=*/intSort,
|
||||
/*range=*/intSort);
|
||||
cFuncDecl = Z3_mk_func_decl(ctx, cSymbol,
|
||||
/*domain_size=*/0,
|
||||
/*domain=*/NULL,
|
||||
/*range=*/int2intArraySort);
|
||||
cApp = Z3_mk_app(ctx, cFuncDecl,
|
||||
/*num_args=*/0,
|
||||
/*args=*/NULL);
|
||||
|
||||
// Create numerals to be used in model
|
||||
zeroNumeral = Z3_mk_int(ctx, 0, intSort);
|
||||
oneNumeral = Z3_mk_int(ctx, 1, intSort);
|
||||
twoNumeral = Z3_mk_int(ctx, 2, intSort);
|
||||
threeNumeral = Z3_mk_int(ctx, 3, intSort);
|
||||
fourNumeral = Z3_mk_int(ctx, 4, intSort);
|
||||
|
||||
// Add assignments to model
|
||||
// a == 1
|
||||
Z3_add_const_interp(ctx, m, aFuncDecl, oneNumeral);
|
||||
// b == 2
|
||||
Z3_add_const_interp(ctx, m, bFuncDecl, twoNumeral);
|
||||
|
||||
// Create a fresh function that represents
|
||||
// reading from array.
|
||||
arrayDomain[0] = intSort;
|
||||
cAsFuncDecl = Z3_mk_fresh_func_decl(ctx,
|
||||
/*prefix=*/"",
|
||||
/*domain_size*/ 1,
|
||||
/*domain=*/arrayDomain,
|
||||
/*sort=*/intSort);
|
||||
// Create function interpretation with default
|
||||
// value of "0".
|
||||
cAsFuncInterp =
|
||||
Z3_add_func_interp(ctx, m, cAsFuncDecl,
|
||||
/*default_value=*/zeroNumeral);
|
||||
Z3_func_interp_inc_ref(ctx, cAsFuncInterp);
|
||||
// Add [0] = 3
|
||||
zeroArgs = Z3_mk_ast_vector(ctx);
|
||||
Z3_ast_vector_inc_ref(ctx, zeroArgs);
|
||||
Z3_ast_vector_push(ctx, zeroArgs, zeroNumeral);
|
||||
Z3_func_interp_add_entry(ctx, cAsFuncInterp, zeroArgs, threeNumeral);
|
||||
// Add [1] = 4
|
||||
oneArgs = Z3_mk_ast_vector(ctx);
|
||||
Z3_ast_vector_inc_ref(ctx, oneArgs);
|
||||
Z3_ast_vector_push(ctx, oneArgs, oneNumeral);
|
||||
Z3_func_interp_add_entry(ctx, cAsFuncInterp, oneArgs, fourNumeral);
|
||||
|
||||
// Now use the `(_ as_array)` to associate
|
||||
// the `cAsFuncInterp` with the `cFuncDecl`
|
||||
// in the model
|
||||
cFuncDeclAsArray = Z3_mk_as_array(ctx, cAsFuncDecl);
|
||||
Z3_add_const_interp(ctx, m, cFuncDecl, cFuncDeclAsArray);
|
||||
|
||||
// Print the model
|
||||
modelAsString = Z3_model_to_string(ctx, m);
|
||||
printf("Model:\n%s\n", modelAsString);
|
||||
|
||||
// Check the interpretations we expect to be present
|
||||
// are.
|
||||
{
|
||||
Z3_func_decl expectedInterpretations[3] = {aFuncDecl, bFuncDecl, cFuncDecl};
|
||||
int index;
|
||||
for (index = 0;
|
||||
index < sizeof(expectedInterpretations) / sizeof(Z3_func_decl);
|
||||
++index) {
|
||||
Z3_func_decl d = expectedInterpretations[index];
|
||||
if (Z3_model_has_interp(ctx, m, d)) {
|
||||
printf("Found interpretation for \"%s\"\n",
|
||||
Z3_ast_to_string(ctx, Z3_func_decl_to_ast(ctx, d)));
|
||||
} else {
|
||||
printf("Missing interpretation");
|
||||
exit(1);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
{
|
||||
// Evaluate a + b under model
|
||||
Z3_ast addArgs[] = {aApp, bApp};
|
||||
Z3_ast aPlusB = Z3_mk_add(ctx,
|
||||
/*num_args=*/2,
|
||||
/*args=*/addArgs);
|
||||
Z3_ast aPlusBEval = NULL;
|
||||
Z3_bool aPlusBEvalSuccess =
|
||||
Z3_model_eval(ctx, m, aPlusB,
|
||||
/*model_completion=*/Z3_FALSE, &aPlusBEval);
|
||||
if (aPlusBEvalSuccess != Z3_TRUE) {
|
||||
printf("Failed to evaluate model\n");
|
||||
exit(1);
|
||||
}
|
||||
|
||||
{
|
||||
int aPlusBValue = 0;
|
||||
Z3_bool getAPlusBValueSuccess =
|
||||
Z3_get_numeral_int(ctx, aPlusBEval, &aPlusBValue);
|
||||
if (getAPlusBValueSuccess != Z3_TRUE) {
|
||||
printf("Failed to get integer value for a+b\n");
|
||||
exit(1);
|
||||
}
|
||||
printf("Evaluated a + b = %d\n", aPlusBValue);
|
||||
if (aPlusBValue != 3) {
|
||||
printf("a+b did not evaluate to expected value\n");
|
||||
exit(1);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
{
|
||||
// Evaluate c[0] + c[1] + c[2] under model
|
||||
Z3_ast c0 = Z3_mk_select(ctx, cApp, zeroNumeral);
|
||||
Z3_ast c1 = Z3_mk_select(ctx, cApp, oneNumeral);
|
||||
Z3_ast c2 = Z3_mk_select(ctx, cApp, twoNumeral);
|
||||
Z3_ast arrayAddArgs[] = {c0, c1, c2};
|
||||
Z3_ast arrayAdd = Z3_mk_add(ctx,
|
||||
/*num_args=*/3,
|
||||
/*args=*/arrayAddArgs);
|
||||
Z3_ast arrayAddEval = NULL;
|
||||
Z3_bool arrayAddEvalSuccess =
|
||||
Z3_model_eval(ctx, m, arrayAdd,
|
||||
/*model_completion=*/Z3_FALSE, &arrayAddEval);
|
||||
if (arrayAddEvalSuccess != Z3_TRUE) {
|
||||
printf("Failed to evaluate model\n");
|
||||
exit(1);
|
||||
}
|
||||
{
|
||||
int arrayAddValue = 0;
|
||||
Z3_bool getArrayAddValueSuccess =
|
||||
Z3_get_numeral_int(ctx, arrayAddEval, &arrayAddValue);
|
||||
if (getArrayAddValueSuccess != Z3_TRUE) {
|
||||
printf("Failed to get integer value for c[0] + c[1] + c[2]\n");
|
||||
exit(1);
|
||||
}
|
||||
printf("Evaluated c[0] + c[1] + c[2] = %d\n", arrayAddValue);
|
||||
if (arrayAddValue != 7) {
|
||||
printf("c[0] + c[1] + c[2] did not evaluate to expected value\n");
|
||||
exit(1);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
Z3_ast_vector_dec_ref(ctx, oneArgs);
|
||||
Z3_ast_vector_dec_ref(ctx, zeroArgs);
|
||||
Z3_func_interp_dec_ref(ctx, cAsFuncInterp);
|
||||
Z3_model_dec_ref(ctx, m);
|
||||
Z3_del_context(ctx);
|
||||
}
|
||||
|
||||
/*@}*/
|
||||
/*@}*/
|
||||
|
||||
|
||||
|
||||
int main() {
|
||||
#ifdef LOG_Z3_CALLS
|
||||
Z3_open_log("z3.log");
|
||||
|
@ -2886,5 +3085,6 @@ int main() {
|
|||
substitute_example();
|
||||
substitute_vars_example();
|
||||
fpa_example();
|
||||
mk_model_example();
|
||||
return 0;
|
||||
}
|
||||
|
|
|
@ -37,20 +37,20 @@ def init_project_def():
|
|||
add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic')
|
||||
add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic')
|
||||
add_lib('aig_tactic', ['tactic'], 'tactic/aig')
|
||||
add_lib('solver', ['model', 'tactic'])
|
||||
add_lib('proofs', ['rewriter', 'util'], 'ast/proofs')
|
||||
add_lib('solver', ['model', 'tactic', 'proofs'])
|
||||
add_lib('ackermannization', ['model', 'rewriter', 'ast', 'solver', 'tactic'], 'ackermannization')
|
||||
add_lib('interp', ['solver'])
|
||||
add_lib('cmd_context', ['solver', 'rewriter', 'interp'])
|
||||
add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
|
||||
add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
|
||||
add_lib('proof_checker', ['rewriter'], 'ast/proof_checker')
|
||||
add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa')
|
||||
add_lib('pattern', ['normal_forms', 'smt2parser', 'rewriter'], 'ast/pattern')
|
||||
add_lib('bit_blaster', ['rewriter', 'rewriter'], 'ast/rewriter/bit_blaster')
|
||||
add_lib('smt_params', ['ast', 'rewriter', 'pattern', 'bit_blaster'], 'smt/params')
|
||||
add_lib('proto_model', ['model', 'rewriter', 'smt_params'], 'smt/proto_model')
|
||||
add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model',
|
||||
'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util', 'fpa', 'lp'])
|
||||
'substitution', 'grobner', 'euclid', 'simplex', 'proofs', 'pattern', 'parser_util', 'fpa', 'lp'])
|
||||
add_lib('bv_tactics', ['tactic', 'bit_blaster', 'core_tactics'], 'tactic/bv')
|
||||
add_lib('fuzzing', ['ast'], 'test/fuzzing')
|
||||
add_lib('smt_tactic', ['smt'], 'smt/tactic')
|
||||
|
|
|
@ -67,7 +67,7 @@ add_subdirectory(interp)
|
|||
add_subdirectory(cmd_context)
|
||||
add_subdirectory(cmd_context/extra_cmds)
|
||||
add_subdirectory(parsers/smt2)
|
||||
add_subdirectory(ast/proof_checker)
|
||||
add_subdirectory(ast/proofs)
|
||||
add_subdirectory(ast/fpa)
|
||||
add_subdirectory(ast/macros)
|
||||
add_subdirectory(ast/pattern)
|
||||
|
|
|
@ -249,7 +249,7 @@ extern "C" {
|
|||
params_ref _p;
|
||||
_p.set_bool("proof", true); // this is currently useless
|
||||
|
||||
scoped_proof_mode spm(mk_c(c)->m(), PGM_FINE);
|
||||
scoped_proof_mode spm(mk_c(c)->m(), PGM_ENABLED);
|
||||
scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
|
||||
scoped_ptr<solver> m_solver((*sf)(mk_c(c)->m(), _p, true, true, true, ::symbol::null));
|
||||
m_solver.get()->updt_params(_p); // why do we have to do this?
|
||||
|
|
|
@ -255,8 +255,13 @@ extern "C" {
|
|||
LOG_Z3_add_const_interp(c, m, f, a);
|
||||
RESET_ERROR_CODE();
|
||||
func_decl* d = to_func_decl(f);
|
||||
model* mdl = to_model_ref(m);
|
||||
mdl->register_decl(d, to_expr(a));
|
||||
if (d->get_arity() != 0) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
}
|
||||
else {
|
||||
model* mdl = to_model_ref(m);
|
||||
mdl->register_decl(d, to_expr(a));
|
||||
}
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
|
|
|
@ -10,6 +10,7 @@ z3_add_component(ast
|
|||
ast_printer.cpp
|
||||
ast_smt2_pp.cpp
|
||||
ast_smt_pp.cpp
|
||||
ast_pp_dot.cpp
|
||||
ast_translation.cpp
|
||||
ast_util.cpp
|
||||
bv_decl_plugin.cpp
|
||||
|
|
109
src/ast/ast.cpp
109
src/ast/ast.cpp
|
@ -805,7 +805,6 @@ func_decl * basic_decl_plugin::mk_proof_decl(char const* name, basic_op_kind k,
|
|||
}
|
||||
|
||||
func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_parents) {
|
||||
SASSERT(k == PR_UNDEF || m_manager->proofs_enabled());
|
||||
switch (static_cast<basic_op_kind>(k)) {
|
||||
//
|
||||
// A description of the semantics of the proof
|
||||
|
@ -2626,7 +2625,7 @@ bool ast_manager::is_fully_interp(sort * s) const {
|
|||
// -----------------------------------
|
||||
|
||||
proof * ast_manager::mk_proof(family_id fid, decl_kind k, unsigned num_args, expr * const * args) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
return mk_app(fid, k, num_args, args);
|
||||
}
|
||||
|
@ -2662,8 +2661,7 @@ proof * ast_manager::mk_goal(expr * f) {
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_modus_ponens(proof * p1, proof * p2) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
if (!p1 || !p2) return nullptr;
|
||||
SASSERT(has_fact(p1));
|
||||
SASSERT(has_fact(p2));
|
||||
CTRACE("mk_modus_ponens", !(is_implies(get_fact(p2)) || is_iff(get_fact(p2)) || is_oeq(get_fact(p2))),
|
||||
|
@ -2684,14 +2682,10 @@ proof * ast_manager::mk_modus_ponens(proof * p1, proof * p2) {
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_reflexivity(expr * e) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
return mk_app(m_basic_family_id, PR_REFLEXIVITY, mk_eq(e, e));
|
||||
}
|
||||
|
||||
proof * ast_manager::mk_oeq_reflexivity(expr * e) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
return mk_app(m_basic_family_id, PR_REFLEXIVITY, mk_oeq(e, e));
|
||||
}
|
||||
|
||||
|
@ -2705,8 +2699,7 @@ proof * ast_manager::mk_commutativity(app * f) {
|
|||
\brief Given a proof of p, return a proof of (p <=> true)
|
||||
*/
|
||||
proof * ast_manager::mk_iff_true(proof * pr) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
if (!pr) return pr;
|
||||
SASSERT(has_fact(pr));
|
||||
SASSERT(is_bool(get_fact(pr)));
|
||||
return mk_app(m_basic_family_id, PR_IFF_TRUE, pr, mk_iff(get_fact(pr), mk_true()));
|
||||
|
@ -2716,8 +2709,7 @@ proof * ast_manager::mk_iff_true(proof * pr) {
|
|||
\brief Given a proof of (not p), return a proof of (p <=> false)
|
||||
*/
|
||||
proof * ast_manager::mk_iff_false(proof * pr) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
if (!pr) return pr;
|
||||
SASSERT(has_fact(pr));
|
||||
SASSERT(is_not(get_fact(pr)));
|
||||
expr * p = to_app(get_fact(pr))->get_arg(0);
|
||||
|
@ -2725,10 +2717,7 @@ proof * ast_manager::mk_iff_false(proof * pr) {
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_symmetry(proof * p) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
if (!p)
|
||||
return p;
|
||||
if (!p) return p;
|
||||
if (is_reflexivity(p))
|
||||
return p;
|
||||
if (is_symmetry(p))
|
||||
|
@ -2741,8 +2730,6 @@ proof * ast_manager::mk_symmetry(proof * p) {
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_transitivity(proof * p1, proof * p2) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
if (!p1)
|
||||
return p2;
|
||||
if (!p2)
|
||||
|
@ -2787,8 +2774,6 @@ proof * ast_manager::mk_transitivity(proof * p1, proof * p2, proof * p3, proof *
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
SASSERT(num_proofs > 0);
|
||||
proof * r = proofs[0];
|
||||
for (unsigned i = 1; i < num_proofs; i++)
|
||||
|
@ -2797,11 +2782,8 @@ proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs, expr * n1, expr * n2) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
if (fine_grain_proofs())
|
||||
return mk_transitivity(num_proofs, proofs);
|
||||
SASSERT(num_proofs > 0);
|
||||
if (num_proofs == 0)
|
||||
return nullptr;
|
||||
if (num_proofs == 1)
|
||||
return proofs[0];
|
||||
DEBUG_CODE({
|
||||
|
@ -2817,8 +2799,6 @@ proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_monotonicity(func_decl * R, app * f1, app * f2, unsigned num_proofs, proof * const * proofs) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
SASSERT(f1->get_num_args() == f2->get_num_args());
|
||||
SASSERT(f1->get_decl() == f2->get_decl());
|
||||
ptr_buffer<expr> args;
|
||||
|
@ -2828,8 +2808,6 @@ proof * ast_manager::mk_monotonicity(func_decl * R, app * f1, app * f2, unsigned
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_congruence(app * f1, app * f2, unsigned num_proofs, proof * const * proofs) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
SASSERT(get_sort(f1) == get_sort(f2));
|
||||
sort * s = get_sort(f1);
|
||||
sort * d[2] = { s, s };
|
||||
|
@ -2837,8 +2815,6 @@ proof * ast_manager::mk_congruence(app * f1, app * f2, unsigned num_proofs, proo
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_oeq_congruence(app * f1, app * f2, unsigned num_proofs, proof * const * proofs) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
SASSERT(get_sort(f1) == get_sort(f2));
|
||||
sort * s = get_sort(f1);
|
||||
sort * d[2] = { s, s };
|
||||
|
@ -2846,11 +2822,7 @@ proof * ast_manager::mk_oeq_congruence(app * f1, app * f2, unsigned num_proofs,
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_quant_intro(quantifier * q1, quantifier * q2, proof * p) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
if (!p) {
|
||||
return 0;
|
||||
}
|
||||
if (!p) return nullptr;
|
||||
SASSERT(q1->get_num_decls() == q2->get_num_decls());
|
||||
SASSERT(has_fact(p));
|
||||
SASSERT(is_iff(get_fact(p)));
|
||||
|
@ -2858,8 +2830,7 @@ proof * ast_manager::mk_quant_intro(quantifier * q1, quantifier * q2, proof * p)
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_oeq_quant_intro(quantifier * q1, quantifier * q2, proof * p) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
if (!p) return nullptr;
|
||||
SASSERT(q1->get_num_decls() == q2->get_num_decls());
|
||||
SASSERT(has_fact(p));
|
||||
SASSERT(is_oeq(get_fact(p)));
|
||||
|
@ -2867,25 +2838,26 @@ proof * ast_manager::mk_oeq_quant_intro(quantifier * q1, quantifier * q2, proof
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_distributivity(expr * s, expr * r) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
return mk_app(m_basic_family_id, PR_DISTRIBUTIVITY, mk_eq(s, r));
|
||||
}
|
||||
|
||||
proof * ast_manager::mk_rewrite(expr * s, expr * t) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
SASSERT(proofs_enabled());
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
return mk_app(m_basic_family_id, PR_REWRITE, mk_eq(s, t));
|
||||
}
|
||||
|
||||
proof * ast_manager::mk_oeq_rewrite(expr * s, expr * t) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
SASSERT(proofs_enabled());
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
return mk_app(m_basic_family_id, PR_REWRITE, mk_oeq(s, t));
|
||||
}
|
||||
|
||||
proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
SASSERT(proofs_enabled());
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
ptr_buffer<expr> args;
|
||||
args.append(num_proofs, (expr**) proofs);
|
||||
|
@ -2894,37 +2866,43 @@ proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, pr
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_pull_quant(expr * e, quantifier * q) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
SASSERT(proofs_enabled());
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
return mk_app(m_basic_family_id, PR_PULL_QUANT, mk_iff(e, q));
|
||||
}
|
||||
|
||||
proof * ast_manager::mk_pull_quant_star(expr * e, quantifier * q) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
SASSERT(proofs_enabled());
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
return mk_app(m_basic_family_id, PR_PULL_QUANT_STAR, mk_iff(e, q));
|
||||
}
|
||||
|
||||
proof * ast_manager::mk_push_quant(quantifier * q, expr * e) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
SASSERT(proofs_enabled());
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
return mk_app(m_basic_family_id, PR_PUSH_QUANT, mk_iff(q, e));
|
||||
}
|
||||
|
||||
proof * ast_manager::mk_elim_unused_vars(quantifier * q, expr * e) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
SASSERT(proofs_enabled());
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
return mk_app(m_basic_family_id, PR_ELIM_UNUSED_VARS, mk_iff(q, e));
|
||||
}
|
||||
|
||||
proof * ast_manager::mk_der(quantifier * q, expr * e) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
SASSERT(proofs_enabled());
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
return mk_app(m_basic_family_id, PR_DER, mk_iff(q, e));
|
||||
}
|
||||
|
||||
proof * ast_manager::mk_quant_inst(expr * not_q_or_i, unsigned num_bind, expr* const* binding) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
SASSERT(proofs_enabled());
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
vector<parameter> params;
|
||||
for (unsigned i = 0; i < num_bind; ++i) {
|
||||
|
@ -2959,7 +2937,8 @@ bool ast_manager::is_rewrite(expr const* e, expr*& r1, expr*& r2) const {
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_def_axiom(expr * ax) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
SASSERT(proofs_enabled());
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
return mk_app(m_basic_family_id, PR_DEF_AXIOM, ax);
|
||||
}
|
||||
|
@ -3001,7 +2980,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
|
|||
new_lits.push_back(lit);
|
||||
}
|
||||
DEBUG_CODE({
|
||||
for (unsigned i = 1; m_proof_mode == PGM_FINE && i < num_proofs; i++) {
|
||||
for (unsigned i = 1; proofs_enabled() && i < num_proofs; i++) {
|
||||
CTRACE("mk_unit_resolution_bug", !found.get(i, false),
|
||||
for (unsigned j = 0; j < num_proofs; j++) {
|
||||
if (j == i) tout << "Index " << i << " was not found:\n";
|
||||
|
@ -3080,14 +3059,11 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_hypothesis(expr * h) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
return mk_app(m_basic_family_id, PR_HYPOTHESIS, h);
|
||||
}
|
||||
|
||||
proof * ast_manager::mk_lemma(proof * p, expr * lemma) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
if (!p) return p;
|
||||
SASSERT(has_fact(p));
|
||||
CTRACE("mk_lemma", !is_false(get_fact(p)), tout << mk_ll_pp(p, *this) << "\n";);
|
||||
SASSERT(is_false(get_fact(p)));
|
||||
|
@ -3100,7 +3076,7 @@ proof * ast_manager::mk_def_intro(expr * new_def) {
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_apply_defs(expr * n, expr * def, unsigned num_proofs, proof * const * proofs) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
ptr_buffer<expr> args;
|
||||
args.append(num_proofs, (expr**) proofs);
|
||||
|
@ -3109,10 +3085,7 @@ proof * ast_manager::mk_apply_defs(expr * n, expr * def, unsigned num_proofs, pr
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_iff_oeq(proof * p) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
return m_undef_proof;
|
||||
if (!p)
|
||||
return p;
|
||||
if (!p) return p;
|
||||
|
||||
SASSERT(has_fact(p));
|
||||
SASSERT(is_iff(get_fact(p)) || is_oeq(get_fact(p)));
|
||||
|
@ -3136,7 +3109,7 @@ bool ast_manager::check_nnf_proof_parents(unsigned num_proofs, proof * const * p
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
check_nnf_proof_parents(num_proofs, proofs);
|
||||
ptr_buffer<expr> args;
|
||||
|
@ -3146,7 +3119,7 @@ proof * ast_manager::mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof *
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
check_nnf_proof_parents(num_proofs, proofs);
|
||||
ptr_buffer<expr> args;
|
||||
|
@ -3156,7 +3129,7 @@ proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof *
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
ptr_buffer<expr> args;
|
||||
args.append(num_proofs, (expr**) proofs);
|
||||
|
@ -3165,7 +3138,7 @@ proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_skolemization(expr * q, expr * e) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
SASSERT(is_bool(q));
|
||||
SASSERT(is_bool(e));
|
||||
|
@ -3173,7 +3146,7 @@ proof * ast_manager::mk_skolemization(expr * q, expr * e) {
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
ptr_buffer<expr> args;
|
||||
args.append(num_proofs, (expr**) proofs);
|
||||
|
@ -3182,7 +3155,7 @@ proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_and_elim(proof * p, unsigned i) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
SASSERT(has_fact(p));
|
||||
SASSERT(is_and(get_fact(p)));
|
||||
|
@ -3193,7 +3166,7 @@ proof * ast_manager::mk_and_elim(proof * p, unsigned i) {
|
|||
}
|
||||
|
||||
proof * ast_manager::mk_not_or_elim(proof * p, unsigned i) {
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
SASSERT(has_fact(p));
|
||||
SASSERT(is_not(get_fact(p)));
|
||||
|
@ -3216,7 +3189,7 @@ proof * ast_manager::mk_th_lemma(
|
|||
unsigned num_params, parameter const* params
|
||||
)
|
||||
{
|
||||
if (m_proof_mode == PGM_DISABLED)
|
||||
if (proofs_disabled())
|
||||
return m_undef_proof;
|
||||
|
||||
ptr_buffer<expr> args;
|
||||
|
|
|
@ -1396,8 +1396,7 @@ public:
|
|||
|
||||
enum proof_gen_mode {
|
||||
PGM_DISABLED,
|
||||
PGM_COARSE,
|
||||
PGM_FINE
|
||||
PGM_ENABLED
|
||||
};
|
||||
|
||||
// -----------------------------------
|
||||
|
@ -2088,15 +2087,14 @@ protected:
|
|||
proof * mk_proof(family_id fid, decl_kind k, expr * arg1, expr * arg2);
|
||||
proof * mk_proof(family_id fid, decl_kind k, expr * arg1, expr * arg2, expr * arg3);
|
||||
|
||||
proof * mk_undef_proof() const { return m_undef_proof; }
|
||||
|
||||
public:
|
||||
bool proofs_enabled() const { return m_proof_mode != PGM_DISABLED; }
|
||||
bool proofs_disabled() const { return m_proof_mode == PGM_DISABLED; }
|
||||
bool coarse_grain_proofs() const { return m_proof_mode == PGM_COARSE; }
|
||||
bool fine_grain_proofs() const { return m_proof_mode == PGM_FINE; }
|
||||
proof_gen_mode proof_mode() const { return m_proof_mode; }
|
||||
void toggle_proof_mode(proof_gen_mode m) { m_proof_mode = m; } // APIs for creating proof objects return [undef]
|
||||
|
||||
proof * mk_undef_proof() const { return m_undef_proof; }
|
||||
|
||||
bool is_proof(expr const * n) const { return is_app(n) && to_app(n)->get_decl()->get_range() == m_proof_sort; }
|
||||
|
||||
|
|
133
src/ast/ast_pp_dot.cpp
Normal file
133
src/ast/ast_pp_dot.cpp
Normal file
|
@ -0,0 +1,133 @@
|
|||
/*++
|
||||
|
||||
Abstract: Pretty-printer for proofs in Graphviz format
|
||||
|
||||
--*/
|
||||
|
||||
#include "util/util.h"
|
||||
#include "util/map.h"
|
||||
#include "ast/ast_pp_dot.h"
|
||||
|
||||
// string escaping for DOT
|
||||
std::string escape_dot(std::string const & s) {
|
||||
std::string res;
|
||||
res.reserve(s.size()); // preallocate
|
||||
for (auto c : s) {
|
||||
if (c == '\n')
|
||||
res.append("\\l");
|
||||
else
|
||||
res.push_back(c);
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
// map from proofs to unique IDs
|
||||
typedef obj_map<const expr, unsigned> expr2id;
|
||||
|
||||
// temporary structure for traversing the proof and printing it
|
||||
struct ast_pp_dot_st {
|
||||
ast_manager & m_manager;
|
||||
std::ostream & m_out;
|
||||
const ast_pp_dot * m_pp;
|
||||
unsigned m_next_id;
|
||||
expr2id m_id_map;
|
||||
obj_hashtable<const expr> m_printed;
|
||||
svector<const expr *> m_to_print;
|
||||
bool m_first;
|
||||
|
||||
ast_pp_dot_st(const ast_pp_dot * pp, std::ostream & out) :
|
||||
m_manager(pp->get_manager()),
|
||||
m_out(out),
|
||||
m_pp(pp),
|
||||
m_next_id(0),
|
||||
m_id_map(),
|
||||
m_printed(),
|
||||
m_to_print(),
|
||||
m_first(true) {}
|
||||
|
||||
~ast_pp_dot_st() {};
|
||||
|
||||
void push_term(const expr * a) { m_to_print.push_back(a); }
|
||||
|
||||
void pp_loop() {
|
||||
// DFS traversal
|
||||
while (!m_to_print.empty()) {
|
||||
const expr * a = m_to_print.back();
|
||||
m_to_print.pop_back();
|
||||
if (!m_printed.contains(a)) {
|
||||
m_printed.insert(a);
|
||||
if (m().is_proof(a))
|
||||
pp_step(to_app(a));
|
||||
else
|
||||
pp_atomic_step(a);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
private:
|
||||
|
||||
inline ast_manager & m() const { return m_manager; }
|
||||
|
||||
// label for an expression
|
||||
std::string label_of_expr(const expr * e) const {
|
||||
expr_ref er((expr*)e, m());
|
||||
std::ostringstream out;
|
||||
out << er << std::flush;
|
||||
return escape_dot(out.str());
|
||||
}
|
||||
|
||||
void pp_atomic_step(const expr * e) {
|
||||
unsigned id = get_id(e);
|
||||
m_out << "node_" << id << " [shape=box,color=\"yellow\",style=\"filled\",label=\"" << label_of_expr(e) << "\"] ;" << std::endl;
|
||||
}
|
||||
|
||||
void pp_step(const proof * p) {
|
||||
TRACE("pp_ast_dot_step", tout << " :kind " << p->get_kind() << " :num-args " << p->get_num_args() << "\n";);
|
||||
if (m().has_fact(p)) {
|
||||
// print result
|
||||
expr* p_res = m().get_fact(p); // result of proof step
|
||||
unsigned id = get_id(p);
|
||||
unsigned num_parents = m().get_num_parents(p);
|
||||
const char* color =
|
||||
m_first ? (m_first=false,"color=\"red\"") : num_parents==0 ? "color=\"yellow\"": "";
|
||||
m_out << "node_" << id <<
|
||||
" [shape=box,style=\"filled\",label=\"" << label_of_expr(p_res) << "\""
|
||||
<< color << "]" << std::endl;
|
||||
// now print edges to parents (except last one, which is the result)
|
||||
std::string label = p->get_decl()->get_name().str();
|
||||
for (unsigned i = 0 ; i < num_parents; ++i) {
|
||||
expr* parent = m().get_parent(p, i);
|
||||
// explore parent, also print a link to it
|
||||
push_term(to_app(parent));
|
||||
m_out << "node_" << id << " -> " << "node_" << get_id((expr*)parent)
|
||||
<< "[label=\"" << label << "\"];" << std::endl;;
|
||||
}
|
||||
} else {
|
||||
pp_atomic_step(p);
|
||||
}
|
||||
}
|
||||
|
||||
// find a unique ID for this proof
|
||||
unsigned get_id(const expr * e) {
|
||||
unsigned id = 0;
|
||||
if (!m_id_map.find(e, id)) {
|
||||
id = m_next_id++;
|
||||
m_id_map.insert(e, id);
|
||||
}
|
||||
return id;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
// main printer
|
||||
std::ostream & ast_pp_dot::pp(std::ostream & out) const {
|
||||
out << "digraph proof { " << std::endl;
|
||||
ast_pp_dot_st pp_st(this, out);
|
||||
pp_st.push_term(m_pr);
|
||||
pp_st.pp_loop();
|
||||
out << std::endl << " } " << std::endl << std::flush;
|
||||
return out;
|
||||
}
|
||||
|
||||
std::ostream &operator<<(std::ostream &out, const ast_pp_dot & p) { return p.pp(out); }
|
||||
|
24
src/ast/ast_pp_dot.h
Normal file
24
src/ast/ast_pp_dot.h
Normal file
|
@ -0,0 +1,24 @@
|
|||
/*++
|
||||
|
||||
Abstract: Pretty-printer for proofs in Graphviz format
|
||||
|
||||
--*/
|
||||
|
||||
#pragma once
|
||||
|
||||
#include <iostream>
|
||||
#include "ast_pp.h"
|
||||
|
||||
class ast_pp_dot {
|
||||
ast_manager & m_manager;
|
||||
proof * const m_pr;
|
||||
|
||||
public:
|
||||
ast_pp_dot(proof *pr, ast_manager &m) : m_manager(m), m_pr(pr) {}
|
||||
ast_pp_dot(proof_ref &e) : m_manager(e.m()), m_pr(e.get()) {}
|
||||
|
||||
std::ostream & pp(std::ostream & out) const;
|
||||
ast_manager & get_manager() const { return m_manager; }
|
||||
};
|
||||
|
||||
std::ostream &operator<<(std::ostream &out, const ast_pp_dot & p);
|
|
@ -44,6 +44,7 @@ format * smt2_pp_environment::pp_fdecl_name(symbol const & s, unsigned & len) co
|
|||
return mk_string(m, str.c_str());
|
||||
}
|
||||
else if (!s.bare_str()) {
|
||||
len = 4;
|
||||
return mk_string(m, "null");
|
||||
}
|
||||
else {
|
||||
|
|
|
@ -3076,8 +3076,6 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
|
|||
split_fp(x, sgn, e, s);
|
||||
mk_is_nan(x, x_is_nan);
|
||||
|
||||
sort * fp_srt = m.get_sort(x);
|
||||
|
||||
expr_ref unspec(m);
|
||||
mk_to_ieee_bv_unspecified(f, num, args, unspec);
|
||||
|
||||
|
|
|
@ -229,7 +229,7 @@ struct pull_quant::imp {
|
|||
proofs.push_back(m_manager.mk_pull_quant(arg, to_quantifier(new_arg)));
|
||||
}
|
||||
pull_quant1(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr(), r);
|
||||
if (m_manager.fine_grain_proofs()) {
|
||||
if (m_manager.proofs_enabled()) {
|
||||
app * r1 = m_manager.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr());
|
||||
proof * p1 = proofs.empty() ? 0 : m_manager.mk_congruence(to_app(n), r1, proofs.size(), proofs.c_ptr());
|
||||
proof * p2 = r1 == r ? 0 : m_manager.mk_pull_quant(r1, to_quantifier(r));
|
||||
|
@ -240,7 +240,7 @@ struct pull_quant::imp {
|
|||
expr_ref new_expr(m_manager);
|
||||
pull_quant1(to_quantifier(n)->get_expr(), new_expr);
|
||||
pull_quant1(to_quantifier(n), new_expr, r);
|
||||
if (m_manager.fine_grain_proofs()) {
|
||||
if (m_manager.proofs_enabled()) {
|
||||
quantifier * q1 = m_manager.update_quantifier(to_quantifier(n), new_expr);
|
||||
proof * p1 = 0;
|
||||
if (n != q1) {
|
||||
|
|
|
@ -606,7 +606,7 @@ bool pattern_inference_cfg::reduce_quantifier(
|
|||
result = m.update_quantifier_weight(tmp, new_weight);
|
||||
TRACE("pattern_inference", tout << "found patterns in database, weight: " << new_weight << "\n" << mk_pp(new_q, m) << "\n";);
|
||||
}
|
||||
if (m.fine_grain_proofs())
|
||||
if (m.proofs_enabled())
|
||||
result_pr = m.mk_rewrite(q, new_q);
|
||||
return true;
|
||||
}
|
||||
|
@ -671,7 +671,7 @@ bool pattern_inference_cfg::reduce_quantifier(
|
|||
quantifier_ref new_q(m.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_body), m);
|
||||
if (weight != q->get_weight())
|
||||
new_q = m.update_quantifier_weight(new_q, weight);
|
||||
if (m.fine_grain_proofs()) {
|
||||
if (m.proofs_enabled()) {
|
||||
proof* new_body_pr = m.mk_reflexivity(new_body);
|
||||
result_pr = m.mk_quant_intro(q, new_q, new_body_pr);
|
||||
}
|
||||
|
@ -689,7 +689,7 @@ bool pattern_inference_cfg::reduce_quantifier(
|
|||
warning_msg("pulled nested quantifier to be able to find an useable pattern (quantifier id: %s)", q->get_qid().str().c_str());
|
||||
}
|
||||
new_q = m.update_quantifier(result2, new_patterns.size(), (expr**) new_patterns.c_ptr(), result2->get_expr());
|
||||
if (m.fine_grain_proofs()) {
|
||||
if (m.proofs_enabled()) {
|
||||
result_pr = m.mk_transitivity(new_pr, m.mk_quant_intro(result2, new_q, m.mk_reflexivity(new_q->get_expr())));
|
||||
}
|
||||
TRACE("pattern_inference", tout << "pulled quantifier:\n" << mk_pp(new_q, m) << "\n";);
|
||||
|
|
|
@ -1,6 +1,7 @@
|
|||
z3_add_component(proof_checker
|
||||
z3_add_component(proofs
|
||||
SOURCES
|
||||
proof_checker.cpp
|
||||
proof_utils.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
rewriter
|
||||
)
|
||||
)
|
|
@ -4,10 +4,9 @@ Copyright (c) 2015 Microsoft Corporation
|
|||
|
||||
--*/
|
||||
|
||||
#include "ast/proof_checker/proof_checker.h"
|
||||
#include "ast/proofs/proof_checker.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
#include "ast/ast_pp.h"
|
||||
// include "spc_decl_plugin.h"
|
||||
#include "ast/ast_smt_pp.h"
|
||||
#include "ast/arith_decl_plugin.h"
|
||||
#include "ast/rewriter/th_rewriter.h"
|
|
@ -1,15 +1,343 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
Copyright (c) 2017 Arie Gurfinkel
|
||||
|
||||
Module Name:
|
||||
|
||||
proof_utils.cpp
|
||||
|
||||
Abstract:
|
||||
Utilities to traverse and manipulate proofs
|
||||
|
||||
Author:
|
||||
Bernhard Gleiss
|
||||
Arie Gurfinkel
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
|
||||
#include "muz/base/dl_util.h"
|
||||
#include "muz/base/proof_utils.h"
|
||||
#include "ast/ast_smt2_pp.h"
|
||||
#include "ast/ast_util.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/proofs/proof_utils.h"
|
||||
#include "ast/proofs/proof_checker.h"
|
||||
#include "ast/rewriter/var_subst.h"
|
||||
#include "util/container_util.h"
|
||||
|
||||
|
||||
proof_post_order::proof_post_order(proof* root, ast_manager& manager) : m(manager)
|
||||
{m_todo.push_back(root);}
|
||||
|
||||
bool proof_post_order::hasNext()
|
||||
{return !m_todo.empty();}
|
||||
|
||||
/*
|
||||
* iterative post-order depth-first search (DFS) through the proof DAG
|
||||
*/
|
||||
proof* proof_post_order::next()
|
||||
{
|
||||
while (!m_todo.empty()) {
|
||||
proof* currentNode = m_todo.back();
|
||||
|
||||
// if we haven't already visited the current unit
|
||||
if (!m_visited.is_marked(currentNode)) {
|
||||
bool existsUnvisitedParent = false;
|
||||
|
||||
// add unprocessed premises to stack for DFS.
|
||||
// If there is at least one unprocessed premise, don't compute the result
|
||||
// for currentProof now, but wait until those unprocessed premises are processed.
|
||||
for (unsigned i = 0; i < m.get_num_parents(currentNode); ++i) {
|
||||
SASSERT(m.is_proof(currentNode->get_arg(i)));
|
||||
proof* premise = to_app(currentNode->get_arg(i));
|
||||
|
||||
// if we haven't visited the current premise yet
|
||||
if (!m_visited.is_marked(premise)) {
|
||||
// add it to the stack
|
||||
m_todo.push_back(premise);
|
||||
existsUnvisitedParent = true;
|
||||
}
|
||||
}
|
||||
|
||||
// if we already visited all parent-inferences, we can visit the inference too
|
||||
if (!existsUnvisitedParent) {
|
||||
m_visited.mark(currentNode, true);
|
||||
m_todo.pop_back();
|
||||
return currentNode;
|
||||
}
|
||||
} else {
|
||||
m_todo.pop_back();
|
||||
}
|
||||
}
|
||||
// we have already iterated through all inferences
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
|
||||
class reduce_hypotheses {
|
||||
ast_manager &m;
|
||||
// tracking all created expressions
|
||||
expr_ref_vector m_pinned;
|
||||
|
||||
// cache for the transformation
|
||||
obj_map<proof, proof*> m_cache;
|
||||
|
||||
// map from unit literals to their hypotheses-free derivations
|
||||
obj_map<expr, proof*> m_units;
|
||||
|
||||
// -- all hypotheses in the the proof
|
||||
obj_hashtable<expr> m_hyps;
|
||||
|
||||
// marks hypothetical proofs
|
||||
ast_mark m_hypmark;
|
||||
|
||||
|
||||
// stack
|
||||
ptr_vector<proof> m_todo;
|
||||
|
||||
void reset()
|
||||
{
|
||||
m_cache.reset();
|
||||
m_units.reset();
|
||||
m_hyps.reset();
|
||||
m_hypmark.reset();
|
||||
m_pinned.reset();
|
||||
}
|
||||
|
||||
bool compute_mark1(proof *pr)
|
||||
{
|
||||
bool hyp_mark = false;
|
||||
// lemmas clear all hypotheses
|
||||
if (!m.is_lemma(pr)) {
|
||||
for (unsigned i = 0, sz = m.get_num_parents(pr); i < sz; ++i) {
|
||||
if (m_hypmark.is_marked(m.get_parent(pr, i))) {
|
||||
hyp_mark = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
m_hypmark.mark(pr, hyp_mark);
|
||||
return hyp_mark;
|
||||
}
|
||||
|
||||
void compute_marks(proof* pr) {
|
||||
proof *p;
|
||||
proof_post_order pit(pr, m);
|
||||
while (pit.hasNext()) {
|
||||
p = pit.next();
|
||||
if (m.is_hypothesis(p)) {
|
||||
m_hypmark.mark(p, true);
|
||||
m_hyps.insert(m.get_fact(p));
|
||||
}
|
||||
else {
|
||||
bool hyp_mark = compute_mark1(p);
|
||||
// collect units that are hyp-free and are used as hypotheses somewhere
|
||||
if (!hyp_mark && m.has_fact(p) && m_hyps.contains(m.get_fact(p))) {
|
||||
m_units.insert(m.get_fact(p), p);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
void find_units(proof *pr)
|
||||
{
|
||||
// optional. not implemented yet.
|
||||
}
|
||||
|
||||
void reduce(proof* pf, proof_ref &out)
|
||||
{
|
||||
proof *res = NULL;
|
||||
|
||||
m_todo.reset();
|
||||
m_todo.push_back(pf);
|
||||
ptr_buffer<proof> args;
|
||||
bool dirty = false;
|
||||
|
||||
while (!m_todo.empty()) {
|
||||
proof *p, *tmp, *pp;
|
||||
unsigned todo_sz;
|
||||
|
||||
p = m_todo.back();
|
||||
if (m_cache.find(p, tmp)) {
|
||||
res = tmp;
|
||||
m_todo.pop_back();
|
||||
continue;
|
||||
}
|
||||
|
||||
dirty = false;
|
||||
args.reset();
|
||||
todo_sz = m_todo.size();
|
||||
for (unsigned i = 0, sz = m.get_num_parents(p); i < sz; ++i) {
|
||||
pp = m.get_parent(p, i);
|
||||
if (m_cache.find(pp, tmp)) {
|
||||
args.push_back(tmp);
|
||||
dirty = dirty || pp != tmp;
|
||||
} else {
|
||||
m_todo.push_back(pp);
|
||||
}
|
||||
}
|
||||
|
||||
if (todo_sz < m_todo.size()) { continue; }
|
||||
else { m_todo.pop_back(); }
|
||||
|
||||
if (m.is_hypothesis(p)) {
|
||||
// hyp: replace by a corresponding unit
|
||||
if (m_units.find(m.get_fact(p), tmp)) {
|
||||
res = tmp;
|
||||
} else { res = p; }
|
||||
}
|
||||
|
||||
else if (!dirty) { res = p; }
|
||||
|
||||
else if (m.is_lemma(p)) {
|
||||
//lemma: reduce the premise; remove reduced consequences from conclusion
|
||||
SASSERT(args.size() == 1);
|
||||
res = mk_lemma_core(args.get(0), m.get_fact(p));
|
||||
compute_mark1(res);
|
||||
} else if (m.is_unit_resolution(p)) {
|
||||
// unit: reduce untis; reduce the first premise; rebuild unit resolution
|
||||
res = mk_unit_resolution_core(args.size(), args.c_ptr());
|
||||
compute_mark1(res);
|
||||
} else {
|
||||
// other: reduce all premises; reapply
|
||||
if (m.has_fact(p)) { args.push_back(to_app(m.get_fact(p))); }
|
||||
SASSERT(p->get_decl()->get_arity() == args.size());
|
||||
res = m.mk_app(p->get_decl(), args.size(), (expr * const*)args.c_ptr());
|
||||
m_pinned.push_back(res);
|
||||
compute_mark1(res);
|
||||
}
|
||||
|
||||
SASSERT(res);
|
||||
m_cache.insert(p, res);
|
||||
|
||||
if (m.has_fact(res) && m.is_false(m.get_fact(res))) { break; }
|
||||
}
|
||||
|
||||
out = res;
|
||||
}
|
||||
|
||||
// returns true if (hypothesis (not a)) would be reduced
|
||||
bool is_reduced(expr *a)
|
||||
{
|
||||
expr_ref e(m);
|
||||
if (m.is_not(a)) { e = to_app(a)->get_arg(0); }
|
||||
else { e = m.mk_not(a); }
|
||||
|
||||
return m_units.contains(e);
|
||||
}
|
||||
|
||||
proof *mk_lemma_core(proof *pf, expr *fact)
|
||||
{
|
||||
ptr_buffer<expr> args;
|
||||
expr_ref lemma(m);
|
||||
|
||||
if (m.is_or(fact)) {
|
||||
for (unsigned i = 0, sz = to_app(fact)->get_num_args(); i < sz; ++i) {
|
||||
expr *a = to_app(fact)->get_arg(i);
|
||||
if (!is_reduced(a))
|
||||
{ args.push_back(a); }
|
||||
}
|
||||
} else if (!is_reduced(fact))
|
||||
{ args.push_back(fact); }
|
||||
|
||||
|
||||
if (args.size() == 0) { return pf; }
|
||||
else if (args.size() == 1) {
|
||||
lemma = args.get(0);
|
||||
} else {
|
||||
lemma = m.mk_or(args.size(), args.c_ptr());
|
||||
}
|
||||
proof* res = m.mk_lemma(pf, lemma);
|
||||
m_pinned.push_back(res);
|
||||
|
||||
if (m_hyps.contains(lemma))
|
||||
{ m_units.insert(lemma, res); }
|
||||
return res;
|
||||
}
|
||||
|
||||
proof *mk_unit_resolution_core(unsigned num_args, proof* const *args)
|
||||
{
|
||||
|
||||
ptr_buffer<proof> pf_args;
|
||||
pf_args.push_back(args [0]);
|
||||
|
||||
app *cls_fact = to_app(m.get_fact(args[0]));
|
||||
ptr_buffer<expr> cls;
|
||||
if (m.is_or(cls_fact)) {
|
||||
for (unsigned i = 0, sz = cls_fact->get_num_args(); i < sz; ++i)
|
||||
{ cls.push_back(cls_fact->get_arg(i)); }
|
||||
} else { cls.push_back(cls_fact); }
|
||||
|
||||
// construct new resovent
|
||||
ptr_buffer<expr> new_fact_cls;
|
||||
bool found;
|
||||
// XXX quadratic
|
||||
for (unsigned i = 0, sz = cls.size(); i < sz; ++i) {
|
||||
found = false;
|
||||
for (unsigned j = 1; j < num_args; ++j) {
|
||||
if (m.is_complement(cls.get(i), m.get_fact(args [j]))) {
|
||||
found = true;
|
||||
pf_args.push_back(args [j]);
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (!found) {
|
||||
new_fact_cls.push_back(cls.get(i));
|
||||
}
|
||||
}
|
||||
|
||||
SASSERT(new_fact_cls.size() + pf_args.size() - 1 == cls.size());
|
||||
expr_ref new_fact(m);
|
||||
new_fact = mk_or(m, new_fact_cls.size(), new_fact_cls.c_ptr());
|
||||
|
||||
// create new proof step
|
||||
proof *res = m.mk_unit_resolution(pf_args.size(), pf_args.c_ptr(), new_fact);
|
||||
m_pinned.push_back(res);
|
||||
return res;
|
||||
}
|
||||
|
||||
// reduce all units, if any unit reduces to false return true and put its proof into out
|
||||
bool reduce_units(proof_ref &out)
|
||||
{
|
||||
proof_ref res(m);
|
||||
for (auto entry : m_units) {
|
||||
reduce(entry.get_value(), res);
|
||||
if (m.is_false(m.get_fact(res))) {
|
||||
out = res;
|
||||
return true;
|
||||
}
|
||||
res.reset();
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
public:
|
||||
reduce_hypotheses(ast_manager &m) : m(m), m_pinned(m) {}
|
||||
|
||||
|
||||
void operator()(proof_ref &pr)
|
||||
{
|
||||
compute_marks(pr);
|
||||
if (!reduce_units(pr)) {
|
||||
reduce(pr.get(), pr);
|
||||
}
|
||||
reset();
|
||||
}
|
||||
};
|
||||
|
||||
void reduce_hypotheses(proof_ref &pr) {
|
||||
ast_manager &m = pr.get_manager();
|
||||
class reduce_hypotheses hypred(m);
|
||||
hypred(pr);
|
||||
DEBUG_CODE(proof_checker pc(m);
|
||||
expr_ref_vector side(m);
|
||||
SASSERT(pc.check(pr, side));
|
||||
);
|
||||
}
|
||||
|
||||
|
||||
|
||||
#include "ast/ast_smt2_pp.h"
|
||||
|
||||
class reduce_hypotheses0 {
|
||||
typedef obj_hashtable<expr> expr_set;
|
||||
ast_manager& m;
|
||||
// reference for any expression created by the tranformation
|
||||
|
@ -85,7 +413,7 @@ class reduce_hypotheses {
|
|||
m_hyprefs.push_back(hyps);
|
||||
inherited = false;
|
||||
}
|
||||
datalog::set_union(*hyps, *hyps1);
|
||||
set_union(*hyps, *hyps1);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -137,7 +465,7 @@ class reduce_hypotheses {
|
|||
}
|
||||
|
||||
public:
|
||||
reduce_hypotheses(ast_manager& m): m(m), m_refs(m) {}
|
||||
reduce_hypotheses0(ast_manager& m): m(m), m_refs(m) {}
|
||||
|
||||
void operator()(proof_ref& pr) {
|
||||
proof_ref tmp(m);
|
||||
|
@ -416,7 +744,7 @@ public:
|
|||
|
||||
void proof_utils::reduce_hypotheses(proof_ref& pr) {
|
||||
ast_manager& m = pr.get_manager();
|
||||
class reduce_hypotheses reduce(m);
|
||||
class reduce_hypotheses0 reduce(m);
|
||||
reduce(pr);
|
||||
CTRACE("proof_utils", !is_closed(m, pr), tout << mk_pp(pr, m) << "\n";);
|
||||
}
|
238
src/ast/proofs/proof_utils.h
Normal file
238
src/ast/proofs/proof_utils.h
Normal file
|
@ -0,0 +1,238 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
proof_utils.h
|
||||
|
||||
Abstract:
|
||||
Utilities to traverse and manipulate proofs
|
||||
|
||||
Author:
|
||||
Bernhard Gleiss
|
||||
Arie Gurfinkel
|
||||
Nikolaj Bjorner
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef PROOF_UTILS_H_
|
||||
#define PROOF_UTILS_H_
|
||||
#include "ast/ast.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/rewriter/bool_rewriter.h"
|
||||
#include "ast/proofs/proof_checker.h"
|
||||
|
||||
/*
|
||||
* iterator, which traverses the proof in depth-first post-order.
|
||||
*/
|
||||
|
||||
class proof_post_order {
|
||||
public:
|
||||
proof_post_order(proof* refutation, ast_manager& manager);
|
||||
bool hasNext();
|
||||
proof* next();
|
||||
|
||||
private:
|
||||
ptr_vector<proof> m_todo;
|
||||
ast_mark m_visited; // the proof nodes we have already visited
|
||||
ast_manager& m;
|
||||
};
|
||||
|
||||
void reduce_hypotheses(proof_ref &pr);
|
||||
|
||||
|
||||
class proof_utils {
|
||||
public:
|
||||
/**
|
||||
\brief reduce the set of hypotheses used in the proof.
|
||||
*/
|
||||
static void reduce_hypotheses(proof_ref& pr);
|
||||
|
||||
/**
|
||||
\brief Check that a proof does not contain open hypotheses.
|
||||
*/
|
||||
static bool is_closed(ast_manager& m, proof* p);
|
||||
|
||||
/**
|
||||
\brief Permute unit resolution rule with th-lemma
|
||||
*/
|
||||
static void permute_unit_resolution(proof_ref& pr);
|
||||
|
||||
/**
|
||||
\brief Push instantiations created in hyper-resolutions up to leaves.
|
||||
This produces a "ground" proof where leaves are annotated by instantiations.
|
||||
*/
|
||||
static void push_instantiations_up(proof_ref& pr);
|
||||
|
||||
|
||||
};
|
||||
|
||||
class elim_aux_assertions {
|
||||
|
||||
static bool matches_fact(expr_ref_vector &args, expr* &match) {
|
||||
ast_manager &m = args.get_manager();
|
||||
expr *fact = args.back();
|
||||
for (unsigned i = 0, sz = args.size() - 1; i < sz; ++i) {
|
||||
expr *arg = args.get(i);
|
||||
if (m.is_proof(arg) &&
|
||||
m.has_fact(to_app(arg)) &&
|
||||
m.get_fact(to_app(arg)) == fact) {
|
||||
match = arg;
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
app_ref m_aux;
|
||||
public:
|
||||
elim_aux_assertions(app_ref aux) : m_aux(aux) {}
|
||||
|
||||
void mk_or_core(expr_ref_vector &args, expr_ref &res)
|
||||
{
|
||||
ast_manager &m = args.get_manager();
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0, sz = args.size(); i < sz; ++i) {
|
||||
if (m.is_false(args.get(i))) { continue; }
|
||||
if (i != j) { args [j] = args.get(i); }
|
||||
++j;
|
||||
}
|
||||
SASSERT(j >= 1);
|
||||
res = j > 1 ? m.mk_or(j, args.c_ptr()) : args.get(0);
|
||||
}
|
||||
|
||||
void mk_app(func_decl *decl, expr_ref_vector &args, expr_ref &res)
|
||||
{
|
||||
ast_manager &m = args.get_manager();
|
||||
bool_rewriter brwr(m);
|
||||
|
||||
if (m.is_or(decl))
|
||||
{ mk_or_core(args, res); }
|
||||
else if (m.is_iff(decl) && args.size() == 2)
|
||||
// avoiding simplifying equalities. In particular,
|
||||
// we don't want (= (not a) (not b)) to be reduced to (= a b)
|
||||
{ res = m.mk_iff(args.get(0), args.get(1)); }
|
||||
else
|
||||
{ brwr.mk_app(decl, args.size(), args.c_ptr(), res); }
|
||||
}
|
||||
|
||||
void operator()(ast_manager &m, proof *pr, proof_ref &res)
|
||||
{
|
||||
DEBUG_CODE(proof_checker pc(m);
|
||||
expr_ref_vector side(m);
|
||||
SASSERT(pc.check(pr, side));
|
||||
);
|
||||
obj_map<app, app*> cache;
|
||||
bool_rewriter brwr(m);
|
||||
|
||||
// for reference counting of new proofs
|
||||
app_ref_vector pinned(m);
|
||||
|
||||
ptr_vector<app> todo;
|
||||
todo.push_back(pr);
|
||||
|
||||
expr_ref not_aux(m);
|
||||
not_aux = m.mk_not(m_aux);
|
||||
|
||||
expr_ref_vector args(m);
|
||||
|
||||
while (!todo.empty()) {
|
||||
app *p, *r;
|
||||
expr *a;
|
||||
|
||||
p = todo.back();
|
||||
if (cache.find(pr, r)) {
|
||||
todo.pop_back();
|
||||
continue;
|
||||
}
|
||||
|
||||
SASSERT(!todo.empty() || pr == p);
|
||||
bool dirty = false;
|
||||
unsigned todo_sz = todo.size();
|
||||
args.reset();
|
||||
for (unsigned i = 0, sz = p->get_num_args(); i < sz; ++i) {
|
||||
expr* arg = p->get_arg(i);
|
||||
if (arg == m_aux.get()) {
|
||||
dirty = true;
|
||||
args.push_back(m.mk_true());
|
||||
} else if (arg == not_aux.get()) {
|
||||
dirty = true;
|
||||
args.push_back(m.mk_false());
|
||||
}
|
||||
// skip (asserted m_aux)
|
||||
else if (m.is_asserted(arg, a) && a == m_aux.get()) {
|
||||
dirty = true;
|
||||
}
|
||||
// skip (hypothesis m_aux)
|
||||
else if (m.is_hypothesis(arg, a) && a == m_aux.get()) {
|
||||
dirty = true;
|
||||
} else if (is_app(arg) && cache.find(to_app(arg), r)) {
|
||||
dirty |= (arg != r);
|
||||
args.push_back(r);
|
||||
} else if (is_app(arg))
|
||||
{ todo.push_back(to_app(arg)); }
|
||||
else
|
||||
// -- not an app
|
||||
{ args.push_back(arg); }
|
||||
|
||||
}
|
||||
if (todo_sz < todo.size()) {
|
||||
// -- process parents
|
||||
args.reset();
|
||||
continue;
|
||||
}
|
||||
|
||||
// ready to re-create
|
||||
app_ref newp(m);
|
||||
if (!dirty) { newp = p; }
|
||||
else if (m.is_unit_resolution(p)) {
|
||||
if (args.size() == 2)
|
||||
// unit resolution with m_aux that got collapsed to nothing
|
||||
{ newp = to_app(args.get(0)); }
|
||||
else {
|
||||
ptr_vector<proof> parents;
|
||||
for (unsigned i = 0, sz = args.size() - 1; i < sz; ++i)
|
||||
{ parents.push_back(to_app(args.get(i))); }
|
||||
SASSERT(parents.size() == args.size() - 1);
|
||||
newp = m.mk_unit_resolution(parents.size(), parents.c_ptr());
|
||||
// XXX the old and new facts should be
|
||||
// equivalent. The test here is much
|
||||
// stronger. It might need to be relaxed.
|
||||
SASSERT(m.get_fact(newp) == args.back());
|
||||
pinned.push_back(newp);
|
||||
}
|
||||
} else if (matches_fact(args, a)) {
|
||||
newp = to_app(a);
|
||||
} else {
|
||||
expr_ref papp(m);
|
||||
mk_app(p->get_decl(), args, papp);
|
||||
newp = to_app(papp.get());
|
||||
pinned.push_back(newp);
|
||||
}
|
||||
cache.insert(p, newp);
|
||||
todo.pop_back();
|
||||
CTRACE("virtual",
|
||||
p->get_decl_kind() == PR_TH_LEMMA &&
|
||||
p->get_decl()->get_parameter(0).get_symbol() == "arith" &&
|
||||
p->get_decl()->get_num_parameters() > 1 &&
|
||||
p->get_decl()->get_parameter(1).get_symbol() == "farkas",
|
||||
tout << "Old pf: " << mk_pp(p, m) << "\n"
|
||||
<< "New pf: " << mk_pp(newp, m) << "\n";);
|
||||
}
|
||||
|
||||
proof *r;
|
||||
VERIFY(cache.find(pr, r));
|
||||
|
||||
DEBUG_CODE(
|
||||
proof_checker pc(m);
|
||||
expr_ref_vector side(m);
|
||||
SASSERT(pc.check(r, side));
|
||||
);
|
||||
|
||||
res = r ;
|
||||
}
|
||||
};
|
||||
|
||||
#endif
|
|
@ -119,7 +119,6 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
|
|||
// BV -> float
|
||||
SASSERT(bvs1 == sbits + ebits);
|
||||
unsynch_mpz_manager & mpzm = m_fm.mpz_manager();
|
||||
unsynch_mpq_manager & mpqm = m_fm.mpq_manager();
|
||||
scoped_mpz sig(mpzm), exp(mpzm);
|
||||
|
||||
const mpz & sm1 = m_fm.m_powers2(sbits - 1);
|
||||
|
|
|
@ -37,7 +37,7 @@ public:
|
|||
|
||||
class scoped_proof : public scoped_proof_mode {
|
||||
public:
|
||||
scoped_proof(ast_manager& m): scoped_proof_mode(m, PGM_FINE) {}
|
||||
scoped_proof(ast_manager& m): scoped_proof_mode(m, PGM_ENABLED) {}
|
||||
};
|
||||
|
||||
class scoped_no_proof : public scoped_proof_mode {
|
||||
|
|
|
@ -20,6 +20,7 @@ Notes:
|
|||
#include "util/version.h"
|
||||
#include "ast/ast_smt_pp.h"
|
||||
#include "ast/ast_smt2_pp.h"
|
||||
#include "ast/ast_pp_dot.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/array_decl_plugin.h"
|
||||
#include "ast/pp.h"
|
||||
|
@ -202,6 +203,26 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
|
|||
}
|
||||
});
|
||||
|
||||
ATOMIC_CMD(get_proof_graph_cmd, "get-proof-graph", "retrieve proof and print it in graphviz", {
|
||||
if (!ctx.produce_proofs())
|
||||
throw cmd_exception("proof construction is not enabled, use command (set-option :produce-proofs true)");
|
||||
if (!ctx.has_manager() ||
|
||||
ctx.cs_state() != cmd_context::css_unsat)
|
||||
throw cmd_exception("proof is not available");
|
||||
proof_ref pr(ctx.m());
|
||||
pr = ctx.get_check_sat_result()->get_proof();
|
||||
if (pr == 0)
|
||||
throw cmd_exception("proof is not available");
|
||||
if (ctx.well_sorted_check_enabled() && !is_well_sorted(ctx.m(), pr)) {
|
||||
throw cmd_exception("proof is not well sorted");
|
||||
}
|
||||
|
||||
context_params& params = ctx.params();
|
||||
const std::string& file = params.m_dot_proof_file;
|
||||
std::ofstream out(file);
|
||||
out << ast_pp_dot(pr) << std::endl;
|
||||
});
|
||||
|
||||
static void print_core(cmd_context& ctx) {
|
||||
ptr_vector<expr> core;
|
||||
ctx.get_check_sat_result()->get_unsat_core(core);
|
||||
|
@ -840,6 +861,7 @@ void install_basic_cmds(cmd_context & ctx) {
|
|||
ctx.insert(alloc(get_assignment_cmd));
|
||||
ctx.insert(alloc(get_assertions_cmd));
|
||||
ctx.insert(alloc(get_proof_cmd));
|
||||
ctx.insert(alloc(get_proof_graph_cmd));
|
||||
ctx.insert(alloc(get_unsat_core_cmd));
|
||||
ctx.insert(alloc(set_option_cmd));
|
||||
ctx.insert(alloc(get_option_cmd));
|
||||
|
|
|
@ -1063,16 +1063,31 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
|
|||
if (fs.more_than_one())
|
||||
throw cmd_exception("ambiguous constant reference, more than one constant with the same sort, use a qualified expression (as <symbol> <sort>) to disumbiguate ", s);
|
||||
func_decl * f = fs.first();
|
||||
if (f == 0)
|
||||
if (f == 0) {
|
||||
throw cmd_exception("unknown constant ", s);
|
||||
}
|
||||
if (f->get_arity() != 0)
|
||||
throw cmd_exception("invalid function application, missing arguments ", s);
|
||||
result = m().mk_const(f);
|
||||
}
|
||||
else {
|
||||
func_decl * f = fs.find(m(), num_args, args, range);
|
||||
if (f == 0)
|
||||
throw cmd_exception("unknown constant ", s);
|
||||
if (f == 0) {
|
||||
std::ostringstream buffer;
|
||||
buffer << "unknown constant " << s << " ";
|
||||
buffer << " (";
|
||||
bool first = true;
|
||||
for (unsigned i = 0; i < num_args; ++i, first = false) {
|
||||
if (!first) buffer << " ";
|
||||
buffer << mk_pp(m().get_sort(args[i]), m());
|
||||
}
|
||||
buffer << ") ";
|
||||
if (range) buffer << mk_pp(range, m()) << " ";
|
||||
for (unsigned i = 0; i < fs.get_num_entries(); ++i) {
|
||||
buffer << "\ndeclared: " << mk_pp(fs.get_entry(i), m()) << " ";
|
||||
}
|
||||
throw cmd_exception(buffer.str().c_str());
|
||||
}
|
||||
if (well_sorted_check_enabled())
|
||||
m().check_sort(f, num_args, args);
|
||||
result = m().mk_app(f, num_args, args);
|
||||
|
|
|
@ -111,6 +111,9 @@ void context_params::set(char const * param, char const * value) {
|
|||
else if (p == "trace_file_name") {
|
||||
m_trace_file_name = value;
|
||||
}
|
||||
else if (p == "dot_proof_file") {
|
||||
m_dot_proof_file = value;
|
||||
}
|
||||
else if (p == "unsat_core") {
|
||||
set_bool(m_unsat_core, param, value);
|
||||
}
|
||||
|
@ -146,6 +149,7 @@ void context_params::updt_params(params_ref const & p) {
|
|||
m_dump_models = p.get_bool("dump_models", m_dump_models);
|
||||
m_trace = p.get_bool("trace", m_trace);
|
||||
m_trace_file_name = p.get_str("trace_file_name", "z3.log");
|
||||
m_dot_proof_file = p.get_str("dot_proof_file", "proof.dot");
|
||||
m_unsat_core = p.get_bool("unsat_core", m_unsat_core);
|
||||
m_debug_ref_count = p.get_bool("debug_ref_count", m_debug_ref_count);
|
||||
m_smtlib2_compliant = p.get_bool("smtlib2_compliant", m_smtlib2_compliant);
|
||||
|
@ -161,6 +165,7 @@ void context_params::collect_param_descrs(param_descrs & d) {
|
|||
d.insert("dump_models", CPK_BOOL, "dump models whenever check-sat returns sat", "false");
|
||||
d.insert("trace", CPK_BOOL, "trace generation for VCC", "false");
|
||||
d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log");
|
||||
d.insert("dot_proof_file", CPK_STRING, "file in which to output graphical proofs", "proof.dot");
|
||||
d.insert("debug_ref_count", CPK_BOOL, "debug support for AST reference counting", "false");
|
||||
d.insert("smtlib2_compliant", CPK_BOOL, "enable/disable SMT-LIB 2.0 compliance", "false");
|
||||
collect_solver_param_descrs(d);
|
||||
|
@ -192,7 +197,7 @@ void context_params::get_solver_params(ast_manager const & m, params_ref & p, bo
|
|||
|
||||
ast_manager * context_params::mk_ast_manager() {
|
||||
ast_manager * r = alloc(ast_manager,
|
||||
m_proof ? PGM_FINE : PGM_DISABLED,
|
||||
m_proof ? PGM_ENABLED : PGM_DISABLED,
|
||||
m_trace ? m_trace_file_name.c_str() : 0);
|
||||
if (m_smtlib2_compliant)
|
||||
r->enable_int_real_coercions(false);
|
||||
|
|
|
@ -30,6 +30,7 @@ class context_params {
|
|||
public:
|
||||
bool m_auto_config;
|
||||
bool m_proof;
|
||||
std::string m_dot_proof_file;
|
||||
bool m_interpolants;
|
||||
bool m_debug_ref_count;
|
||||
bool m_trace;
|
||||
|
|
|
@ -147,7 +147,7 @@ static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, par
|
|||
ast_manager &_m = ctx.m();
|
||||
// TODO: the following is a HACK to enable proofs in the old smt solver
|
||||
// When we stop using that solver, this hack can be removed
|
||||
scoped_proof_mode spm(_m,PGM_FINE);
|
||||
scoped_proof_mode spm(_m,PGM_ENABLED);
|
||||
ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
|
||||
p.set_bool("proof", true);
|
||||
scoped_ptr<solver> sp = (ctx.get_interpolating_solver_factory())(_m, p, true, models_enabled, false, ctx.get_logic());
|
||||
|
|
|
@ -57,12 +57,12 @@ typedef ast raw_ast;
|
|||
|
||||
/** Wrapper around an ast pointer */
|
||||
class ast_i {
|
||||
protected:
|
||||
protected:
|
||||
raw_ast *_ast;
|
||||
public:
|
||||
public:
|
||||
raw_ast * const &raw() const {return _ast;}
|
||||
ast_i(raw_ast *a){_ast = a;}
|
||||
|
||||
|
||||
ast_i(){_ast = 0;}
|
||||
bool eq(const ast_i &other) const {
|
||||
return _ast == other._ast;
|
||||
|
@ -86,19 +86,19 @@ class ast_i {
|
|||
/** Reference counting verison of above */
|
||||
class ast_r : public ast_i {
|
||||
ast_manager *_m;
|
||||
public:
|
||||
ast_r(ast_manager *m, raw_ast *a) : ast_i(a) {
|
||||
public:
|
||||
ast_r(ast_manager *m, raw_ast *a) : ast_i(a) {
|
||||
_m = m;
|
||||
m->inc_ref(a);
|
||||
}
|
||||
|
||||
|
||||
ast_r() {_m = 0;}
|
||||
|
||||
ast_r(const ast_r &other) : ast_i(other) {
|
||||
|
||||
ast_r(const ast_r &other) : ast_i(other) {
|
||||
_m = other._m;
|
||||
if (_m) _m->inc_ref(_ast);
|
||||
}
|
||||
|
||||
|
||||
ast_r &operator=(const ast_r &other) {
|
||||
if(_ast)
|
||||
_m->dec_ref(_ast);
|
||||
|
@ -107,12 +107,12 @@ class ast_r : public ast_i {
|
|||
if (_m) _m->inc_ref(_ast);
|
||||
return *this;
|
||||
}
|
||||
|
||||
~ast_r(){
|
||||
|
||||
~ast_r() {
|
||||
if(_ast)
|
||||
_m->dec_ref(_ast);
|
||||
}
|
||||
|
||||
|
||||
ast_manager *mgr() const {return _m;}
|
||||
|
||||
};
|
||||
|
|
|
@ -29,6 +29,7 @@
|
|||
#include "interp/iz3profiling.h"
|
||||
#include "interp/iz3interp.h"
|
||||
#include "interp/iz3proof_itp.h"
|
||||
#include "ast/ast_pp.h"
|
||||
|
||||
#include <assert.h>
|
||||
#include <algorithm>
|
||||
|
@ -1851,6 +1852,21 @@ public:
|
|||
}
|
||||
break;
|
||||
}
|
||||
case PR_TRANSITIVITY_STAR: {
|
||||
// assume the premises are x = y, y = z, z = u, u = v, ..
|
||||
|
||||
ast x = arg(conc(prem(proof,0)),0);
|
||||
ast y = arg(conc(prem(proof,0)),1);
|
||||
ast z = arg(conc(prem(proof,1)),1);
|
||||
res = iproof->make_transitivity(x,y,z,args[0],args[1]);
|
||||
|
||||
for (unsigned i = 2; i < nprems; ++i) {
|
||||
y = z;
|
||||
z = arg(conc(prem(proof,i)),1);
|
||||
res = iproof->make_transitivity(x,y,z,res,args[i]);
|
||||
}
|
||||
break;
|
||||
}
|
||||
case PR_QUANT_INTRO:
|
||||
case PR_MONOTONICITY:
|
||||
{
|
||||
|
@ -2029,6 +2045,7 @@ public:
|
|||
break;
|
||||
}
|
||||
default:
|
||||
IF_VERBOSE(0, verbose_stream() << "Unsupported proof rule: " << expr_ref((expr*)proof.raw(), *proof.mgr()) << "\n";);
|
||||
// pfgoto(proof);
|
||||
// SASSERT(0 && "translate_main: unsupported proof rule");
|
||||
throw unsupported();
|
||||
|
|
|
@ -36,7 +36,7 @@ class iz3translation : public iz3base {
|
|||
|
||||
/** This is thrown when the proof cannot be translated. */
|
||||
struct unsupported: public iz3_exception {
|
||||
unsupported(): iz3_exception("unsupported") {}
|
||||
unsupported(): iz3_exception("unsupported") { }
|
||||
};
|
||||
|
||||
static iz3translation *create(iz3mgr &mgr,
|
||||
|
|
|
@ -10,7 +10,6 @@ z3_add_component(muz
|
|||
dl_rule_transformer.cpp
|
||||
dl_util.cpp
|
||||
hnf.cpp
|
||||
proof_utils.cpp
|
||||
rule_properties.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
aig_tactic
|
||||
|
|
|
@ -53,7 +53,7 @@ Example from Boogie:
|
|||
|
||||
#include "muz/base/dl_boogie_proof.h"
|
||||
#include "model/model_pp.h"
|
||||
#include "muz/base/proof_utils.h"
|
||||
#include "ast/proofs/proof_utils.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/ast_util.h"
|
||||
|
||||
|
|
|
@ -462,7 +462,7 @@ namespace datalog {
|
|||
|
||||
void context::flush_add_rules() {
|
||||
datalog::rule_manager& rm = get_rule_manager();
|
||||
scoped_proof_mode _scp(m, generate_proof_trace()?PGM_FINE:PGM_DISABLED);
|
||||
scoped_proof_mode _scp(m, generate_proof_trace()?PGM_ENABLED:PGM_DISABLED);
|
||||
while (m_rule_fmls_head < m_rule_fmls.size()) {
|
||||
expr* fml = m_rule_fmls[m_rule_fmls_head].get();
|
||||
proof* p = generate_proof_trace()?m.mk_asserted(fml):0;
|
||||
|
|
|
@ -141,7 +141,7 @@ namespace datalog {
|
|||
|
||||
|
||||
void rule_manager::mk_rule(expr* fml, proof* p, rule_set& rules, symbol const& name) {
|
||||
scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED);
|
||||
scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_ENABLED:PGM_DISABLED);
|
||||
proof_ref pr(p, m);
|
||||
expr_ref fml1(m);
|
||||
bind_variables(fml, true, fml1);
|
||||
|
@ -343,7 +343,7 @@ namespace datalog {
|
|||
}
|
||||
TRACE("dl", tout << rule_expr << "\n";);
|
||||
|
||||
scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED);
|
||||
scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_ENABLED:PGM_DISABLED);
|
||||
proof_ref pr(m);
|
||||
if (m_ctx.generate_proof_trace()) {
|
||||
pr = m.mk_asserted(rule_expr);
|
||||
|
|
|
@ -11,7 +11,7 @@ Abstract:
|
|||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2010-05-20.
|
||||
Krystof Hoder 2010
|
||||
|
||||
Revision History:
|
||||
|
||||
|
@ -31,6 +31,7 @@ Revision History:
|
|||
#include "util/statistics.h"
|
||||
#include "util/stopwatch.h"
|
||||
#include "util/lbool.h"
|
||||
#include "util/container_util.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
@ -381,129 +382,6 @@ namespace datalog {
|
|||
*/
|
||||
void apply_subst(expr_ref_vector& tgt, expr_ref_vector const& sub);
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
// container functions
|
||||
//
|
||||
// -----------------------------------
|
||||
|
||||
template<class Set1, class Set2>
|
||||
void set_intersection(Set1 & tgt, const Set2 & src) {
|
||||
svector<typename Set1::data> to_remove;
|
||||
typename Set1::iterator vit = tgt.begin();
|
||||
typename Set1::iterator vend = tgt.end();
|
||||
for(;vit!=vend;++vit) {
|
||||
typename Set1::data itm=*vit;
|
||||
if(!src.contains(itm)) {
|
||||
to_remove.push_back(itm);
|
||||
}
|
||||
}
|
||||
while(!to_remove.empty()) {
|
||||
tgt.remove(to_remove.back());
|
||||
to_remove.pop_back();
|
||||
}
|
||||
}
|
||||
|
||||
template<class Set>
|
||||
void set_difference(Set & tgt, const Set & to_remove) {
|
||||
typename Set::iterator vit = to_remove.begin();
|
||||
typename Set::iterator vend = to_remove.end();
|
||||
for(;vit!=vend;++vit) {
|
||||
typename Set::data itm=*vit;
|
||||
tgt.remove(itm);
|
||||
}
|
||||
}
|
||||
|
||||
template<class Set1, class Set2>
|
||||
void set_union(Set1 & tgt, const Set2 & to_add) {
|
||||
typename Set2::iterator vit = to_add.begin();
|
||||
typename Set2::iterator vend = to_add.end();
|
||||
for(;vit!=vend;++vit) {
|
||||
typename Set1::data itm=*vit;
|
||||
tgt.insert(itm);
|
||||
}
|
||||
}
|
||||
|
||||
void idx_set_union(idx_set & tgt, const idx_set & src);
|
||||
|
||||
template<class T>
|
||||
void unite_disjoint_maps(T & tgt, const T & src) {
|
||||
typename T::iterator it = src.begin();
|
||||
typename T::iterator end = src.end();
|
||||
for(; it!=end; ++it) {
|
||||
SASSERT(!tgt.contains(it->m_key));
|
||||
tgt.insert(it->m_key, it->m_value);
|
||||
}
|
||||
}
|
||||
|
||||
template<class T, class U>
|
||||
void collect_map_range(T & acc, const U & map) {
|
||||
typename U::iterator it = map.begin();
|
||||
typename U::iterator end = map.end();
|
||||
for(; it!=end; ++it) {
|
||||
acc.push_back(it->m_value);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
template<class T>
|
||||
void print_container(const T & begin, const T & end, std::ostream & out) {
|
||||
T it = begin;
|
||||
out << "(";
|
||||
bool first = true;
|
||||
for(; it!=end; ++it) {
|
||||
if(first) { first = false; } else { out << ","; }
|
||||
out << (*it);
|
||||
}
|
||||
out << ")";
|
||||
}
|
||||
|
||||
template<class T>
|
||||
void print_container(const T & cont, std::ostream & out) {
|
||||
print_container(cont.begin(), cont.end(), out);
|
||||
}
|
||||
|
||||
template<class T, class M>
|
||||
void print_container(const ref_vector<T,M> & cont, std::ostream & out) {
|
||||
print_container(cont.c_ptr(), cont.c_ptr() + cont.size(), out);
|
||||
}
|
||||
|
||||
template<class T>
|
||||
void print_map(const T & cont, std::ostream & out) {
|
||||
typename T::iterator it = cont.begin();
|
||||
typename T::iterator end = cont.end();
|
||||
out << "(";
|
||||
bool first = true;
|
||||
for(; it!=end; ++it) {
|
||||
if(first) { first = false; } else { out << ","; }
|
||||
out << it->m_key << "->" << it->m_value;
|
||||
}
|
||||
out << ")";
|
||||
}
|
||||
|
||||
template<class It, class V>
|
||||
unsigned find_index(const It & begin, const It & end, const V & val) {
|
||||
unsigned idx = 0;
|
||||
It it = begin;
|
||||
for(; it!=end; it++, idx++) {
|
||||
if(*it==val) {
|
||||
return idx;
|
||||
}
|
||||
}
|
||||
return UINT_MAX;
|
||||
}
|
||||
|
||||
template<class T, class U>
|
||||
bool containers_equal(const T & begin1, const T & end1, const U & begin2, const U & end2) {
|
||||
T it1 = begin1;
|
||||
U it2 = begin2;
|
||||
for(; it1!=end1 && it2!=end2; ++it1, ++it2) {
|
||||
if(*it1!=*it2) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return it1==end1 && it2==end2;
|
||||
}
|
||||
|
||||
template<class T, class U>
|
||||
bool vectors_equal(const T & c1, const U & c2) {
|
||||
|
@ -521,6 +399,8 @@ namespace datalog {
|
|||
return true;
|
||||
}
|
||||
|
||||
void idx_set_union(idx_set & tgt, const idx_set & src);
|
||||
|
||||
template<class T>
|
||||
struct default_obj_chash {
|
||||
unsigned operator()(T const& cont, unsigned i) const {
|
||||
|
|
|
@ -1,48 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
proof_utils.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Utilities for transforming proofs.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2012-10-12.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef PROOF_UTILS_H_
|
||||
#define PROOF_UTILS_H_
|
||||
|
||||
class proof_utils {
|
||||
public:
|
||||
/**
|
||||
\brief reduce the set of hypotheses used in the proof.
|
||||
*/
|
||||
static void reduce_hypotheses(proof_ref& pr);
|
||||
|
||||
/**
|
||||
\brief Check that a proof does not contain open hypotheses.
|
||||
*/
|
||||
static bool is_closed(ast_manager& m, proof* p);
|
||||
|
||||
/**
|
||||
\brief Permute unit resolution rule with th-lemma
|
||||
*/
|
||||
static void permute_unit_resolution(proof_ref& pr);
|
||||
|
||||
/**
|
||||
\brief Push instantiations created in hyper-resolutions up to leaves.
|
||||
This produces a "ground" proof where leaves are annotated by instantiations.
|
||||
*/
|
||||
static void push_instantiations_up(proof_ref& pr);
|
||||
|
||||
|
||||
};
|
||||
|
||||
#endif
|
|
@ -41,9 +41,8 @@ Notes:
|
|||
#include "ast/ast_smt2_pp.h"
|
||||
#include "qe/qe_lite.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
#include "ast/proof_checker/proof_checker.h"
|
||||
#include "ast/proofs/proof_checker.h"
|
||||
#include "smt/smt_value_sort.h"
|
||||
#include "muz/base/proof_utils.h"
|
||||
#include "muz/base/dl_boogie_proof.h"
|
||||
#include "ast/scoped_proof.h"
|
||||
#include "tactic/core/blast_term_ite_tactic.h"
|
||||
|
@ -1825,7 +1824,7 @@ namespace pdr {
|
|||
m_core_generalizers.push_back(alloc(core_multi_generalizer, *this, 0));
|
||||
}
|
||||
if (!classify.is_bool()) {
|
||||
m.toggle_proof_mode(PGM_FINE);
|
||||
m.toggle_proof_mode(PGM_ENABLED);
|
||||
m_fparams.m_arith_bound_prop = BP_NONE;
|
||||
m_fparams.m_arith_auto_config_simplex = true;
|
||||
m_fparams.m_arith_propagate_eqs = false;
|
||||
|
|
|
@ -31,7 +31,7 @@ Revision History:
|
|||
#include "ast/rewriter/th_rewriter.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
#include "tactic/arith/arith_bounds_tactic.h"
|
||||
#include "muz/base/proof_utils.h"
|
||||
#include "ast/proofs/proof_utils.h"
|
||||
#include "ast/reg_decl_plugins.h"
|
||||
|
||||
|
||||
|
@ -372,7 +372,7 @@ namespace pdr {
|
|||
|
||||
farkas_learner::farkas_learner(smt_params& params, ast_manager& outer_mgr)
|
||||
: m_proof_params(get_proof_params(params)),
|
||||
m_pr(PGM_FINE),
|
||||
m_pr(PGM_ENABLED),
|
||||
m_constr(0),
|
||||
m_combine_farkas_coefficients(true),
|
||||
p2o(m_pr, outer_mgr),
|
||||
|
@ -733,8 +733,8 @@ namespace pdr {
|
|||
}
|
||||
else {
|
||||
expr_set* hyps3 = alloc(expr_set);
|
||||
datalog::set_union(*hyps3, *hyps);
|
||||
datalog::set_union(*hyps3, *hyps2);
|
||||
set_union(*hyps3, *hyps);
|
||||
set_union(*hyps3, *hyps2);
|
||||
hyps = hyps3;
|
||||
hyprefs.push_back(hyps);
|
||||
}
|
||||
|
@ -795,7 +795,7 @@ namespace pdr {
|
|||
case PR_LEMMA: {
|
||||
expr_set* hyps2 = alloc(expr_set);
|
||||
hyprefs.push_back(hyps2);
|
||||
datalog::set_union(*hyps2, *hyps);
|
||||
set_union(*hyps2, *hyps);
|
||||
hyps = hyps2;
|
||||
expr* fml = m.get_fact(p);
|
||||
hyps->remove(fml);
|
||||
|
|
|
@ -81,7 +81,7 @@ namespace pdr {
|
|||
m_gen(n, core0, uses_level1);
|
||||
new_cores.push_back(std::make_pair(core0, uses_level1));
|
||||
obj_hashtable<expr> core_exprs, core1_exprs;
|
||||
datalog::set_union(core_exprs, core0);
|
||||
set_union(core_exprs, core0);
|
||||
for (unsigned i = 0; i < old_core.size(); ++i) {
|
||||
expr* lit = old_core[i].get();
|
||||
if (core_exprs.contains(lit)) {
|
||||
|
@ -94,8 +94,8 @@ namespace pdr {
|
|||
if (core1.size() < old_core.size()) {
|
||||
new_cores.push_back(std::make_pair(core1, uses_level1));
|
||||
core1_exprs.reset();
|
||||
datalog::set_union(core1_exprs, core1);
|
||||
datalog::set_intersection(core_exprs, core1_exprs);
|
||||
set_union(core1_exprs, core1);
|
||||
set_intersection(core_exprs, core1_exprs);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
@ -7,7 +7,6 @@ z3_add_component(spacer
|
|||
spacer_farkas_learner.cpp
|
||||
spacer_generalizers.cpp
|
||||
spacer_manager.cpp
|
||||
spacer_marshal.cpp
|
||||
spacer_prop_solver.cpp
|
||||
spacer_smt_context_manager.cpp
|
||||
spacer_sym_mux.cpp
|
||||
|
@ -15,11 +14,9 @@ z3_add_component(spacer
|
|||
spacer_itp_solver.cpp
|
||||
spacer_virtual_solver.cpp
|
||||
spacer_legacy_mbp.cpp
|
||||
spacer_proof_utils.cpp
|
||||
spacer_unsat_core_learner.cpp
|
||||
spacer_unsat_core_plugin.cpp
|
||||
spacer_matrix.cpp
|
||||
spacer_min_cut.cpp
|
||||
spacer_antiunify.cpp
|
||||
spacer_mev_array.cpp
|
||||
spacer_qe_project.cpp
|
||||
|
|
|
@ -40,7 +40,7 @@ Notes:
|
|||
#include "ast/ast_smt2_pp.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
#include "ast/ast_util.h"
|
||||
#include "ast/proof_checker/proof_checker.h"
|
||||
#include "ast/proofs/proof_checker.h"
|
||||
#include "smt/smt_value_sort.h"
|
||||
#include "ast/scoped_proof.h"
|
||||
#include "muz/spacer/spacer_qe_project.h"
|
||||
|
@ -2139,7 +2139,7 @@ void context::reset_lemma_generalizers()
|
|||
void context::init_lemma_generalizers(datalog::rule_set& rules)
|
||||
{
|
||||
reset_lemma_generalizers();
|
||||
m.toggle_proof_mode(PGM_FINE);
|
||||
m.toggle_proof_mode(PGM_ENABLED);
|
||||
smt_params &fparams = m_pm.fparams ();
|
||||
if (!m_params.spacer_eq_prop ()) {
|
||||
fparams.m_arith_bound_prop = BP_NONE;
|
||||
|
|
|
@ -31,7 +31,7 @@ Revision History:
|
|||
#include "muz/spacer/spacer_farkas_learner.h"
|
||||
#include "ast/rewriter/th_rewriter.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
#include "muz/base/proof_utils.h"
|
||||
#include "ast/proofs/proof_utils.h"
|
||||
#include "ast/reg_decl_plugins.h"
|
||||
#include "smt/smt_farkas_util.h"
|
||||
|
||||
|
@ -231,8 +231,8 @@ void farkas_learner::get_lemmas(proof* root, expr_set const& bs, expr_ref_vector
|
|||
hyps = hyps2;
|
||||
} else {
|
||||
expr_set* hyps3 = alloc(expr_set);
|
||||
datalog::set_union(*hyps3, *hyps);
|
||||
datalog::set_union(*hyps3, *hyps2);
|
||||
set_union(*hyps3, *hyps);
|
||||
set_union(*hyps3, *hyps2);
|
||||
hyps = hyps3;
|
||||
hyprefs.push_back(hyps);
|
||||
}
|
||||
|
@ -291,7 +291,7 @@ void farkas_learner::get_lemmas(proof* root, expr_set const& bs, expr_ref_vector
|
|||
case PR_LEMMA: {
|
||||
expr_set* hyps2 = alloc(expr_set);
|
||||
hyprefs.push_back(hyps2);
|
||||
datalog::set_union(*hyps2, *hyps);
|
||||
set_union(*hyps2, *hyps);
|
||||
hyps = hyps2;
|
||||
expr* fml = m.get_fact(p);
|
||||
hyps->remove(fml);
|
||||
|
|
|
@ -134,8 +134,8 @@ public:
|
|||
{return m_solver.get_num_assumptions();}
|
||||
virtual expr * get_assumption(unsigned idx) const
|
||||
{return m_solver.get_assumption(idx);}
|
||||
virtual std::ostream &display(std::ostream &out) const
|
||||
{m_solver.display(out); return out;}
|
||||
virtual std::ostream &display(std::ostream &out, unsigned n, expr* const* es) const
|
||||
{ return m_solver.display(out, n, es); }
|
||||
|
||||
/* check_sat_result interface */
|
||||
|
||||
|
@ -170,7 +170,7 @@ public:
|
|||
public:
|
||||
scoped_bg(itp_solver &s) : m_s(s), m_bg_sz(m_s.get_num_bg()) {}
|
||||
~scoped_bg()
|
||||
{if(m_s.get_num_bg() > m_bg_sz) { m_s.pop_bg(m_s.get_num_bg() - m_bg_sz); }}
|
||||
{if (m_s.get_num_bg() > m_bg_sz) { m_s.pop_bg(m_s.get_num_bg() - m_bg_sz); }}
|
||||
};
|
||||
};
|
||||
}
|
||||
|
|
|
@ -23,9 +23,9 @@
|
|||
#include "ast/ast_smt2_pp.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
#include "ast/ast_util.h"
|
||||
#include "ast/proof_checker/proof_checker.h"
|
||||
#include "ast/proofs/proof_checker.h"
|
||||
#include "smt/smt_value_sort.h"
|
||||
#include "muz/base/proof_utils.h"
|
||||
#include "ast/proofs/proof_utils.h"
|
||||
#include "ast/scoped_proof.h"
|
||||
#include "muz/spacer/spacer_qe_project.h"
|
||||
#include "tactic/core/blast_term_ite_tactic.h"
|
||||
|
|
|
@ -1,289 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Arie Gurfinkel
|
||||
|
||||
Module Name:
|
||||
|
||||
spacer_min_cut.cpp
|
||||
|
||||
Abstract:
|
||||
min cut solver
|
||||
|
||||
Author:
|
||||
Bernhard Gleiss
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
#include "muz/spacer/spacer_min_cut.h"
|
||||
|
||||
namespace spacer {
|
||||
|
||||
spacer_min_cut::spacer_min_cut()
|
||||
{
|
||||
m_n = 2;
|
||||
|
||||
// push back two empty vectors for source and sink
|
||||
m_edges.push_back(vector<std::pair<unsigned, unsigned>>());
|
||||
m_edges.push_back(vector<std::pair<unsigned, unsigned>>());
|
||||
}
|
||||
|
||||
unsigned spacer_min_cut::new_node()
|
||||
{
|
||||
return m_n++;
|
||||
}
|
||||
|
||||
void spacer_min_cut::add_edge(unsigned int i, unsigned int j, unsigned int capacity)
|
||||
{
|
||||
if (i >= m_edges.size())
|
||||
{
|
||||
m_edges.resize(i + 1);
|
||||
}
|
||||
m_edges[i].insert(std::make_pair(j, 1));
|
||||
STRACE("spacer.mincut",
|
||||
verbose_stream() << "adding edge (" << i << "," << j << ")\n";
|
||||
);
|
||||
|
||||
}
|
||||
|
||||
void spacer_min_cut::compute_min_cut(vector<unsigned>& cut_nodes)
|
||||
{
|
||||
if (m_n == 2)
|
||||
{
|
||||
return;
|
||||
}
|
||||
|
||||
m_d.resize(m_n);
|
||||
m_pred.resize(m_n);
|
||||
|
||||
// compute initial distances and number of nodes
|
||||
compute_initial_distances();
|
||||
|
||||
unsigned i = 0;
|
||||
|
||||
while (m_d[0] < m_n)
|
||||
{
|
||||
unsigned j = get_admissible_edge(i);
|
||||
|
||||
if (j < m_n)
|
||||
{
|
||||
// advance(i)
|
||||
m_pred[j] = i;
|
||||
i = j;
|
||||
|
||||
// if i is the sink, augment path
|
||||
if (i == 1)
|
||||
{
|
||||
augment_path();
|
||||
i = 0;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
// retreat
|
||||
compute_distance(i);
|
||||
if (i != 0)
|
||||
{
|
||||
i = m_pred[i];
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// split nodes into reachable and unreachable ones
|
||||
vector<bool> reachable(m_n);
|
||||
compute_reachable_nodes(reachable);
|
||||
|
||||
// find all edges between reachable and unreachable nodes and for each such edge, add corresponding lemma to unsat-core
|
||||
compute_cut_and_add_lemmas(reachable, cut_nodes);
|
||||
}
|
||||
|
||||
void spacer_min_cut::compute_initial_distances()
|
||||
{
|
||||
vector<unsigned> todo;
|
||||
vector<bool> visited(m_n);
|
||||
|
||||
todo.push_back(0); // start at the source, since we do postorder traversel
|
||||
|
||||
while (!todo.empty())
|
||||
{
|
||||
unsigned current = todo.back();
|
||||
|
||||
// if we haven't already visited current
|
||||
if (!visited[current]) {
|
||||
bool existsUnvisitedParent = false;
|
||||
|
||||
// add unprocessed parents to stack for DFS. If there is at least one unprocessed parent, don't compute the result
|
||||
// for current now, but wait until those unprocessed parents are processed.
|
||||
for (unsigned i = 0, sz = m_edges[current].size(); i < sz; ++i)
|
||||
{
|
||||
unsigned parent = m_edges[current][i].first;
|
||||
|
||||
// if we haven't visited the current parent yet
|
||||
if(!visited[parent])
|
||||
{
|
||||
// add it to the stack
|
||||
todo.push_back(parent);
|
||||
existsUnvisitedParent = true;
|
||||
}
|
||||
}
|
||||
|
||||
// if we already visited all parents, we can visit current too
|
||||
if (!existsUnvisitedParent) {
|
||||
visited[current] = true;
|
||||
todo.pop_back();
|
||||
|
||||
compute_distance(current); // I.H. all parent distances are already computed
|
||||
}
|
||||
}
|
||||
else {
|
||||
todo.pop_back();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
unsigned spacer_min_cut::get_admissible_edge(unsigned i)
|
||||
{
|
||||
for (const auto& pair : m_edges[i])
|
||||
{
|
||||
if (pair.second > 0 && m_d[i] == m_d[pair.first] + 1)
|
||||
{
|
||||
return pair.first;
|
||||
}
|
||||
}
|
||||
return m_n; // no element found
|
||||
}
|
||||
|
||||
void spacer_min_cut::augment_path()
|
||||
{
|
||||
// find bottleneck capacity
|
||||
unsigned max = std::numeric_limits<unsigned int>::max();
|
||||
unsigned k = 1;
|
||||
while (k != 0)
|
||||
{
|
||||
unsigned l = m_pred[k];
|
||||
for (const auto& pair : m_edges[l])
|
||||
{
|
||||
if (pair.first == k)
|
||||
{
|
||||
if (max > pair.second)
|
||||
{
|
||||
max = pair.second;
|
||||
}
|
||||
}
|
||||
}
|
||||
k = l;
|
||||
}
|
||||
|
||||
k = 1;
|
||||
while (k != 0)
|
||||
{
|
||||
unsigned l = m_pred[k];
|
||||
|
||||
// decrease capacity
|
||||
for (auto& pair : m_edges[l])
|
||||
{
|
||||
if (pair.first == k)
|
||||
{
|
||||
pair.second -= max;
|
||||
}
|
||||
}
|
||||
// increase reverse flow
|
||||
bool already_exists = false;
|
||||
for (auto& pair : m_edges[k])
|
||||
{
|
||||
if (pair.first == l)
|
||||
{
|
||||
already_exists = true;
|
||||
pair.second += max;
|
||||
}
|
||||
}
|
||||
if (!already_exists)
|
||||
{
|
||||
m_edges[k].insert(std::make_pair(l, max));
|
||||
}
|
||||
k = l;
|
||||
}
|
||||
}
|
||||
|
||||
void spacer_min_cut::compute_distance(unsigned i)
|
||||
{
|
||||
if (i == 1) // sink node
|
||||
{
|
||||
m_d[1] = 0;
|
||||
}
|
||||
else
|
||||
{
|
||||
unsigned min = std::numeric_limits<unsigned int>::max();
|
||||
|
||||
// find edge (i,j) with positive residual capacity and smallest distance
|
||||
for (const auto& pair : m_edges[i])
|
||||
{
|
||||
if (pair.second > 0)
|
||||
{
|
||||
unsigned tmp = m_d[pair.first] + 1;
|
||||
if (tmp < min)
|
||||
{
|
||||
min = tmp;
|
||||
}
|
||||
}
|
||||
}
|
||||
m_d[i] = min;
|
||||
}
|
||||
}
|
||||
|
||||
void spacer_min_cut::compute_reachable_nodes(vector<bool>& reachable)
|
||||
{
|
||||
vector<unsigned> todo;
|
||||
|
||||
todo.push_back(0);
|
||||
while (!todo.empty())
|
||||
{
|
||||
unsigned current = todo.back();
|
||||
todo.pop_back();
|
||||
|
||||
if (!reachable[current])
|
||||
{
|
||||
reachable[current] = true;
|
||||
|
||||
for (const auto& pair : m_edges[current])
|
||||
{
|
||||
if (pair.second > 0)
|
||||
{
|
||||
todo.push_back(pair.first);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void spacer_min_cut::compute_cut_and_add_lemmas(vector<bool>& reachable, vector<unsigned>& cut_nodes)
|
||||
{
|
||||
vector<unsigned> todo;
|
||||
vector<bool> visited(m_n);
|
||||
|
||||
todo.push_back(0);
|
||||
while (!todo.empty())
|
||||
{
|
||||
unsigned current = todo.back();
|
||||
todo.pop_back();
|
||||
|
||||
if (!visited[current])
|
||||
{
|
||||
visited[current] = true;
|
||||
|
||||
for (const auto& pair : m_edges[current])
|
||||
{
|
||||
unsigned successor = pair.first;
|
||||
if (reachable[successor])
|
||||
{
|
||||
todo.push_back(successor);
|
||||
}
|
||||
else
|
||||
{
|
||||
cut_nodes.push_back(successor);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
|
@ -1,53 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Arie Gurfinkel
|
||||
|
||||
Module Name:
|
||||
|
||||
spacer_min_cut.h
|
||||
|
||||
Abstract:
|
||||
min cut solver
|
||||
|
||||
Author:
|
||||
Bernhard Gleiss
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef _SPACER_MIN_CUT_H_
|
||||
#define _SPACER_MIN_CUT_H_
|
||||
|
||||
#include "ast/ast.h"
|
||||
#include "util/vector.h"
|
||||
|
||||
namespace spacer {
|
||||
|
||||
class spacer_min_cut {
|
||||
public:
|
||||
spacer_min_cut();
|
||||
|
||||
unsigned new_node();
|
||||
void add_edge(unsigned i, unsigned j, unsigned capacity);
|
||||
void compute_min_cut(vector<unsigned>& cut_nodes);
|
||||
|
||||
private:
|
||||
|
||||
unsigned m_n; // number of vertices in the graph
|
||||
|
||||
vector<vector<std::pair<unsigned, unsigned> > > m_edges; // map from node to all outgoing edges together with their weights (also contains "reverse edges")
|
||||
vector<unsigned> m_d; // approximation of distance from node to sink in residual graph
|
||||
vector<unsigned> m_pred; // predecessor-information for reconstruction of augmenting path
|
||||
vector<expr*> m_node_to_formula; // maps each node to the corresponding formula in the original proof
|
||||
|
||||
void compute_initial_distances();
|
||||
unsigned get_admissible_edge(unsigned i);
|
||||
void augment_path();
|
||||
void compute_distance(unsigned i);
|
||||
void compute_reachable_nodes(vector<bool>& reachable);
|
||||
void compute_cut_and_add_lemmas(vector<bool>& reachable, vector<unsigned>& cut_nodes);
|
||||
};
|
||||
}
|
||||
|
||||
#endif
|
|
@ -1,332 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Arie Gurfinkel
|
||||
|
||||
Module Name:
|
||||
|
||||
spacer_proof_utils.cpp
|
||||
|
||||
Abstract:
|
||||
Utilities to traverse and manipulate proofs
|
||||
|
||||
Author:
|
||||
Bernhard Gleiss
|
||||
Arie Gurfinkel
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
|
||||
#include "muz/spacer/spacer_proof_utils.h"
|
||||
#include "ast/ast_util.h"
|
||||
#include "ast/ast_pp.h"
|
||||
|
||||
#include "ast/proof_checker/proof_checker.h"
|
||||
|
||||
namespace spacer {
|
||||
|
||||
ProofIteratorPostOrder::ProofIteratorPostOrder(proof* root, ast_manager& manager) : m(manager)
|
||||
{m_todo.push_back(root);}
|
||||
|
||||
bool ProofIteratorPostOrder::hasNext()
|
||||
{return !m_todo.empty();}
|
||||
|
||||
/*
|
||||
* iterative post-order depth-first search (DFS) through the proof DAG
|
||||
*/
|
||||
proof* ProofIteratorPostOrder::next()
|
||||
{
|
||||
while (!m_todo.empty()) {
|
||||
proof* currentNode = m_todo.back();
|
||||
|
||||
// if we haven't already visited the current unit
|
||||
if (!m_visited.is_marked(currentNode)) {
|
||||
bool existsUnvisitedParent = false;
|
||||
|
||||
// add unprocessed premises to stack for DFS. If there is at least one unprocessed premise, don't compute the result
|
||||
// for currentProof now, but wait until those unprocessed premises are processed.
|
||||
for (unsigned i = 0; i < m.get_num_parents(currentNode); ++i) {
|
||||
SASSERT(m.is_proof(currentNode->get_arg(i)));
|
||||
proof* premise = to_app(currentNode->get_arg(i));
|
||||
|
||||
// if we haven't visited the current premise yet
|
||||
if (!m_visited.is_marked(premise)) {
|
||||
// add it to the stack
|
||||
m_todo.push_back(premise);
|
||||
existsUnvisitedParent = true;
|
||||
}
|
||||
}
|
||||
|
||||
// if we already visited all parent-inferences, we can visit the inference too
|
||||
if (!existsUnvisitedParent) {
|
||||
m_visited.mark(currentNode, true);
|
||||
m_todo.pop_back();
|
||||
return currentNode;
|
||||
}
|
||||
} else {
|
||||
m_todo.pop_back();
|
||||
}
|
||||
}
|
||||
// we have already iterated through all inferences
|
||||
return NULL;
|
||||
}
|
||||
|
||||
|
||||
class reduce_hypotheses {
|
||||
ast_manager &m;
|
||||
// tracking all created expressions
|
||||
expr_ref_vector m_pinned;
|
||||
|
||||
// cache for the transformation
|
||||
obj_map<proof, proof*> m_cache;
|
||||
|
||||
// map from unit literals to their hypotheses-free derivations
|
||||
obj_map<expr, proof*> m_units;
|
||||
|
||||
// -- all hypotheses in the the proof
|
||||
obj_hashtable<expr> m_hyps;
|
||||
|
||||
// marks hypothetical proofs
|
||||
ast_mark m_hypmark;
|
||||
|
||||
|
||||
// stack
|
||||
ptr_vector<proof> m_todo;
|
||||
|
||||
void reset()
|
||||
{
|
||||
m_cache.reset();
|
||||
m_units.reset();
|
||||
m_hyps.reset();
|
||||
m_hypmark.reset();
|
||||
m_pinned.reset();
|
||||
}
|
||||
|
||||
bool compute_mark1(proof *pr)
|
||||
{
|
||||
bool hyp_mark = false;
|
||||
// lemmas clear all hypotheses
|
||||
if (!m.is_lemma(pr)) {
|
||||
for (unsigned i = 0, sz = m.get_num_parents(pr); i < sz; ++i) {
|
||||
if (m_hypmark.is_marked(m.get_parent(pr, i))) {
|
||||
hyp_mark = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
m_hypmark.mark(pr, hyp_mark);
|
||||
return hyp_mark;
|
||||
}
|
||||
|
||||
void compute_marks(proof* pr)
|
||||
{
|
||||
proof *p;
|
||||
ProofIteratorPostOrder pit(pr, m);
|
||||
while (pit.hasNext()) {
|
||||
p = pit.next();
|
||||
if (m.is_hypothesis(p)) {
|
||||
m_hypmark.mark(p, true);
|
||||
m_hyps.insert(m.get_fact(p));
|
||||
} else {
|
||||
bool hyp_mark = compute_mark1(p);
|
||||
// collect units that are hyp-free and are used as hypotheses somewhere
|
||||
if (!hyp_mark && m.has_fact(p) && m_hyps.contains(m.get_fact(p)))
|
||||
{ m_units.insert(m.get_fact(p), p); }
|
||||
}
|
||||
}
|
||||
}
|
||||
void find_units(proof *pr)
|
||||
{
|
||||
// optional. not implemented yet.
|
||||
}
|
||||
|
||||
void reduce(proof* pf, proof_ref &out)
|
||||
{
|
||||
proof *res = NULL;
|
||||
|
||||
m_todo.reset();
|
||||
m_todo.push_back(pf);
|
||||
ptr_buffer<proof> args;
|
||||
bool dirty = false;
|
||||
|
||||
while (!m_todo.empty()) {
|
||||
proof *p, *tmp, *pp;
|
||||
unsigned todo_sz;
|
||||
|
||||
p = m_todo.back();
|
||||
if (m_cache.find(p, tmp)) {
|
||||
res = tmp;
|
||||
m_todo.pop_back();
|
||||
continue;
|
||||
}
|
||||
|
||||
dirty = false;
|
||||
args.reset();
|
||||
todo_sz = m_todo.size();
|
||||
for (unsigned i = 0, sz = m.get_num_parents(p); i < sz; ++i) {
|
||||
pp = m.get_parent(p, i);
|
||||
if (m_cache.find(pp, tmp)) {
|
||||
args.push_back(tmp);
|
||||
dirty = dirty || pp != tmp;
|
||||
} else {
|
||||
m_todo.push_back(pp);
|
||||
}
|
||||
}
|
||||
|
||||
if (todo_sz < m_todo.size()) { continue; }
|
||||
else { m_todo.pop_back(); }
|
||||
|
||||
if (m.is_hypothesis(p)) {
|
||||
// hyp: replace by a corresponding unit
|
||||
if (m_units.find(m.get_fact(p), tmp)) {
|
||||
res = tmp;
|
||||
} else { res = p; }
|
||||
}
|
||||
|
||||
else if (!dirty) { res = p; }
|
||||
|
||||
else if (m.is_lemma(p)) {
|
||||
//lemma: reduce the premise; remove reduced consequences from conclusion
|
||||
SASSERT(args.size() == 1);
|
||||
res = mk_lemma_core(args.get(0), m.get_fact(p));
|
||||
compute_mark1(res);
|
||||
} else if (m.is_unit_resolution(p)) {
|
||||
// unit: reduce untis; reduce the first premise; rebuild unit resolution
|
||||
res = mk_unit_resolution_core(args.size(), args.c_ptr());
|
||||
compute_mark1(res);
|
||||
} else {
|
||||
// other: reduce all premises; reapply
|
||||
if (m.has_fact(p)) { args.push_back(to_app(m.get_fact(p))); }
|
||||
SASSERT(p->get_decl()->get_arity() == args.size());
|
||||
res = m.mk_app(p->get_decl(), args.size(), (expr * const*)args.c_ptr());
|
||||
m_pinned.push_back(res);
|
||||
compute_mark1(res);
|
||||
}
|
||||
|
||||
SASSERT(res);
|
||||
m_cache.insert(p, res);
|
||||
|
||||
if (m.has_fact(res) && m.is_false(m.get_fact(res))) { break; }
|
||||
}
|
||||
|
||||
out = res;
|
||||
}
|
||||
|
||||
// returns true if (hypothesis (not a)) would be reduced
|
||||
bool is_reduced(expr *a)
|
||||
{
|
||||
expr_ref e(m);
|
||||
if (m.is_not(a)) { e = to_app(a)->get_arg(0); }
|
||||
else { e = m.mk_not(a); }
|
||||
|
||||
return m_units.contains(e);
|
||||
}
|
||||
proof *mk_lemma_core(proof *pf, expr *fact)
|
||||
{
|
||||
ptr_buffer<expr> args;
|
||||
expr_ref lemma(m);
|
||||
|
||||
if (m.is_or(fact)) {
|
||||
for (unsigned i = 0, sz = to_app(fact)->get_num_args(); i < sz; ++i) {
|
||||
expr *a = to_app(fact)->get_arg(i);
|
||||
if (!is_reduced(a))
|
||||
{ args.push_back(a); }
|
||||
}
|
||||
} else if (!is_reduced(fact))
|
||||
{ args.push_back(fact); }
|
||||
|
||||
|
||||
if (args.size() == 0) { return pf; }
|
||||
else if (args.size() == 1) {
|
||||
lemma = args.get(0);
|
||||
} else {
|
||||
lemma = m.mk_or(args.size(), args.c_ptr());
|
||||
}
|
||||
proof* res = m.mk_lemma(pf, lemma);
|
||||
m_pinned.push_back(res);
|
||||
|
||||
if (m_hyps.contains(lemma))
|
||||
{ m_units.insert(lemma, res); }
|
||||
return res;
|
||||
}
|
||||
|
||||
proof *mk_unit_resolution_core(unsigned num_args, proof* const *args)
|
||||
{
|
||||
|
||||
ptr_buffer<proof> pf_args;
|
||||
pf_args.push_back(args [0]);
|
||||
|
||||
app *cls_fact = to_app(m.get_fact(args[0]));
|
||||
ptr_buffer<expr> cls;
|
||||
if (m.is_or(cls_fact)) {
|
||||
for (unsigned i = 0, sz = cls_fact->get_num_args(); i < sz; ++i)
|
||||
{ cls.push_back(cls_fact->get_arg(i)); }
|
||||
} else { cls.push_back(cls_fact); }
|
||||
|
||||
// construct new resovent
|
||||
ptr_buffer<expr> new_fact_cls;
|
||||
bool found;
|
||||
// XXX quadratic
|
||||
for (unsigned i = 0, sz = cls.size(); i < sz; ++i) {
|
||||
found = false;
|
||||
for (unsigned j = 1; j < num_args; ++j) {
|
||||
if (m.is_complement(cls.get(i), m.get_fact(args [j]))) {
|
||||
found = true;
|
||||
pf_args.push_back(args [j]);
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (!found) {
|
||||
new_fact_cls.push_back(cls.get(i));
|
||||
}
|
||||
}
|
||||
|
||||
SASSERT(new_fact_cls.size() + pf_args.size() - 1 == cls.size());
|
||||
expr_ref new_fact(m);
|
||||
new_fact = mk_or(m, new_fact_cls.size(), new_fact_cls.c_ptr());
|
||||
|
||||
// create new proof step
|
||||
proof *res = m.mk_unit_resolution(pf_args.size(), pf_args.c_ptr(), new_fact);
|
||||
m_pinned.push_back(res);
|
||||
return res;
|
||||
}
|
||||
|
||||
// reduce all units, if any unit reduces to false return true and put its proof into out
|
||||
bool reduce_units(proof_ref &out)
|
||||
{
|
||||
proof_ref res(m);
|
||||
for (auto entry : m_units) {
|
||||
reduce(entry.get_value(), res);
|
||||
if (m.is_false(m.get_fact(res))) {
|
||||
out = res;
|
||||
return true;
|
||||
}
|
||||
res.reset();
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
public:
|
||||
reduce_hypotheses(ast_manager &m) : m(m), m_pinned(m) {}
|
||||
|
||||
|
||||
void operator()(proof_ref &pr)
|
||||
{
|
||||
compute_marks(pr);
|
||||
if (!reduce_units(pr)) {
|
||||
reduce(pr.get(), pr);
|
||||
}
|
||||
reset();
|
||||
}
|
||||
};
|
||||
void reduce_hypotheses(proof_ref &pr)
|
||||
{
|
||||
ast_manager &m = pr.get_manager();
|
||||
class reduce_hypotheses hypred(m);
|
||||
hypred(pr);
|
||||
DEBUG_CODE(proof_checker pc(m);
|
||||
expr_ref_vector side(m);
|
||||
SASSERT(pc.check(pr, side));
|
||||
);
|
||||
}
|
||||
}
|
|
@ -1,43 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Arie Gurfinkel
|
||||
|
||||
Module Name:
|
||||
|
||||
spacer_proof_utils.cpp
|
||||
|
||||
Abstract:
|
||||
Utilities to traverse and manipulate proofs
|
||||
|
||||
Author:
|
||||
Bernhard Gleiss
|
||||
Arie Gurfinkel
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef _SPACER_PROOF_UTILS_H_
|
||||
#define _SPACER_PROOF_UTILS_H_
|
||||
#include "ast/ast.h"
|
||||
|
||||
namespace spacer {
|
||||
/*
|
||||
* iterator, which traverses the proof in depth-first post-order.
|
||||
*/
|
||||
class ProofIteratorPostOrder {
|
||||
public:
|
||||
ProofIteratorPostOrder(proof* refutation, ast_manager& manager);
|
||||
bool hasNext();
|
||||
proof* next();
|
||||
|
||||
private:
|
||||
ptr_vector<proof> m_todo;
|
||||
ast_mark m_visited; // the proof nodes we have already visited
|
||||
|
||||
ast_manager& m;
|
||||
};
|
||||
|
||||
|
||||
void reduce_hypotheses(proof_ref &pr);
|
||||
}
|
||||
#endif
|
|
@ -41,7 +41,7 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e
|
|||
// transform proof in order to get a proof which is better suited for unsat-core-extraction
|
||||
proof_ref pr(root, m);
|
||||
|
||||
spacer::reduce_hypotheses(pr);
|
||||
reduce_hypotheses(pr);
|
||||
STRACE("spacer.unsat_core_learner",
|
||||
verbose_stream() << "Reduced proof:\n" << mk_ismt2_pp(pr, m) << "\n";
|
||||
);
|
||||
|
@ -50,7 +50,7 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e
|
|||
collect_symbols_b(asserted_b);
|
||||
|
||||
// traverse proof
|
||||
ProofIteratorPostOrder it(root, m);
|
||||
proof_post_order it(root, m);
|
||||
while (it.hasNext())
|
||||
{
|
||||
proof* currentNode = it.next();
|
||||
|
@ -138,7 +138,7 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e
|
|||
std::unordered_map<unsigned, unsigned> id_to_small_id;
|
||||
unsigned counter = 0;
|
||||
|
||||
ProofIteratorPostOrder it2(root, m);
|
||||
proof_post_order it2(root, m);
|
||||
while (it2.hasNext())
|
||||
{
|
||||
proof* currentNode = it2.next();
|
||||
|
|
|
@ -20,7 +20,7 @@ Revision History:
|
|||
|
||||
#include "ast/ast.h"
|
||||
#include "muz/spacer/spacer_util.h"
|
||||
#include "muz/spacer/spacer_proof_utils.h"
|
||||
#include "ast/proofs/proof_utils.h"
|
||||
|
||||
namespace spacer {
|
||||
|
||||
|
|
|
@ -20,13 +20,13 @@ Revision History:
|
|||
|
||||
#include "ast/rewriter/bool_rewriter.h"
|
||||
#include "ast/arith_decl_plugin.h"
|
||||
#include "ast/proofs/proof_utils.h"
|
||||
|
||||
#include "solver/solver.h"
|
||||
|
||||
#include "smt/smt_farkas_util.h"
|
||||
#include "smt/smt_solver.h"
|
||||
|
||||
#include "muz/spacer/spacer_proof_utils.h"
|
||||
#include "muz/spacer/spacer_matrix.h"
|
||||
#include "muz/spacer/spacer_unsat_core_plugin.h"
|
||||
#include "muz/spacer/spacer_unsat_core_learner.h"
|
||||
|
@ -735,7 +735,7 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
|
|||
m_node_to_formula[node_other] = m.get_fact(i);
|
||||
m_node_to_formula[node_i] = m.get_fact(i);
|
||||
|
||||
m_min_cut.add_edge(node_other, node_i, 1);
|
||||
m_min_cut.add_edge(node_other, node_i);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -765,12 +765,12 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
|
|||
m_node_to_formula[node_j] = m.get_fact(j);
|
||||
m_node_to_formula[node_other] = m.get_fact(j);
|
||||
|
||||
m_min_cut.add_edge(node_j, node_other, 1);
|
||||
m_min_cut.add_edge(node_j, node_other);
|
||||
}
|
||||
}
|
||||
|
||||
// finally connect nodes
|
||||
m_min_cut.add_edge(node_i, node_j, 1);
|
||||
m_min_cut.add_edge(node_i, node_j);
|
||||
}
|
||||
|
||||
/*
|
||||
|
@ -779,7 +779,7 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
|
|||
*/
|
||||
void unsat_core_plugin_min_cut::finalize()
|
||||
{
|
||||
vector<unsigned int> cut_nodes;
|
||||
unsigned_vector cut_nodes;
|
||||
m_min_cut.compute_min_cut(cut_nodes);
|
||||
|
||||
for (unsigned cut_node : cut_nodes)
|
||||
|
|
|
@ -19,7 +19,7 @@ Revision History:
|
|||
#define _SPACER_UNSAT_CORE_PLUGIN_H_
|
||||
|
||||
#include "ast/ast.h"
|
||||
#include "muz/spacer/spacer_min_cut.h"
|
||||
#include "util/min_cut.h"
|
||||
|
||||
namespace spacer {
|
||||
|
||||
|
@ -109,7 +109,7 @@ private:
|
|||
|
||||
vector<expr*> m_node_to_formula; // maps each node to the corresponding formula in the original proof
|
||||
|
||||
spacer_min_cut m_min_cut;
|
||||
min_cut m_min_cut;
|
||||
};
|
||||
}
|
||||
#endif
|
||||
|
|
|
@ -72,73 +72,67 @@ namespace spacer {
|
|||
//
|
||||
|
||||
model_evaluator_util::model_evaluator_util(ast_manager& m) :
|
||||
m(m), m_mev(NULL)
|
||||
{ reset (NULL); }
|
||||
m(m), m_mev(nullptr) {
|
||||
reset (nullptr);
|
||||
}
|
||||
|
||||
model_evaluator_util::~model_evaluator_util() {reset (NULL);}
|
||||
|
||||
|
||||
void model_evaluator_util::reset(model* model)
|
||||
{
|
||||
void model_evaluator_util::reset(model* model) {
|
||||
if (m_mev) {
|
||||
dealloc(m_mev);
|
||||
m_mev = NULL;
|
||||
}
|
||||
m_model = model;
|
||||
if (!m_model) { return; }
|
||||
if (!m_model) { return; }
|
||||
m_mev = alloc(model_evaluator, *m_model);
|
||||
}
|
||||
|
||||
bool model_evaluator_util::eval(expr *e, expr_ref &result, bool model_completion)
|
||||
{
|
||||
|
||||
bool model_evaluator_util::eval(expr *e, expr_ref &result, bool model_completion) {
|
||||
m_mev->set_model_completion (model_completion);
|
||||
try {
|
||||
m_mev->operator() (e, result);
|
||||
return true;
|
||||
} catch (model_evaluator_exception &ex) {
|
||||
}
|
||||
catch (model_evaluator_exception &ex) {
|
||||
(void)ex;
|
||||
TRACE("spacer_model_evaluator", tout << ex.msg () << "\n";);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
bool model_evaluator_util::eval(const expr_ref_vector &v,
|
||||
expr_ref& res, bool model_completion)
|
||||
{
|
||||
expr_ref& res, bool model_completion) {
|
||||
expr_ref e(m);
|
||||
e = mk_and (v);
|
||||
return eval(e, res, model_completion);
|
||||
}
|
||||
|
||||
|
||||
bool model_evaluator_util::is_true(const expr_ref_vector &v)
|
||||
{
|
||||
|
||||
|
||||
bool model_evaluator_util::is_true(const expr_ref_vector &v) {
|
||||
expr_ref res(m);
|
||||
return eval (v, res, false) && m.is_true (res);
|
||||
}
|
||||
|
||||
bool model_evaluator_util::is_false(expr *x)
|
||||
{
|
||||
|
||||
bool model_evaluator_util::is_false(expr *x) {
|
||||
expr_ref res(m);
|
||||
return eval(x, res, false) && m.is_false (res);
|
||||
}
|
||||
bool model_evaluator_util::is_true(expr *x)
|
||||
{
|
||||
|
||||
bool model_evaluator_util::is_true(expr *x) {
|
||||
expr_ref res(m);
|
||||
return eval(x, res, false) && m.is_true (res);
|
||||
}
|
||||
|
||||
|
||||
void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml)
|
||||
{
|
||||
|
||||
void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) {
|
||||
ast_manager& m = fml.get_manager();
|
||||
expr_ref_vector conjs(m);
|
||||
flatten_and(fml, conjs);
|
||||
obj_map<expr, unsigned> diseqs;
|
||||
expr* n, *lhs, *rhs;
|
||||
for (unsigned i = 0; i < conjs.size(); ++i) {
|
||||
if (m.is_not(conjs[i].get(), n) &&
|
||||
m.is_eq(n, lhs, rhs)) {
|
||||
if (m.is_not(conjs[i].get(), n) && m.is_eq(n, lhs, rhs)) {
|
||||
if (!m.is_value(rhs)) {
|
||||
std::swap(lhs, rhs);
|
||||
}
|
||||
|
@ -155,14 +149,12 @@ void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml)
|
|||
expr_ref val(m), tmp(m);
|
||||
proof_ref pr(m);
|
||||
pr = m.mk_asserted(m.mk_true());
|
||||
obj_map<expr, unsigned>::iterator it = diseqs.begin();
|
||||
obj_map<expr, unsigned>::iterator end = diseqs.end();
|
||||
for (; it != end; ++it) {
|
||||
if (it->m_value >= threshold) {
|
||||
model.eval(it->m_key, val);
|
||||
sub.insert(it->m_key, val, pr);
|
||||
conjs.push_back(m.mk_eq(it->m_key, val));
|
||||
num_deleted += it->m_value;
|
||||
for (auto const& kv : diseqs) {
|
||||
if (kv.m_value >= threshold) {
|
||||
model.eval(kv.m_key, val);
|
||||
sub.insert(kv.m_key, val, pr);
|
||||
conjs.push_back(m.mk_eq(kv.m_key, val));
|
||||
num_deleted += kv.m_value;
|
||||
}
|
||||
}
|
||||
if (orig_size < conjs.size()) {
|
||||
|
@ -178,14 +170,17 @@ void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml)
|
|||
SASSERT(orig_size <= 1 + conjs.size());
|
||||
if (i + 1 == orig_size) {
|
||||
// no-op.
|
||||
} else if (orig_size <= conjs.size()) {
|
||||
}
|
||||
else if (orig_size <= conjs.size()) {
|
||||
// no-op
|
||||
} else {
|
||||
}
|
||||
else {
|
||||
SASSERT(orig_size == 1 + conjs.size());
|
||||
--orig_size;
|
||||
--i;
|
||||
}
|
||||
} else {
|
||||
}
|
||||
else {
|
||||
conjs[i] = tmp;
|
||||
}
|
||||
}
|
||||
|
@ -202,9 +197,8 @@ void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml)
|
|||
ast_manager& m;
|
||||
public:
|
||||
ite_hoister(ast_manager& m): m(m) {}
|
||||
|
||||
br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result)
|
||||
{
|
||||
|
||||
br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) {
|
||||
if (m.is_ite(f)) {
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
@ -233,13 +227,12 @@ void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml)
|
|||
struct ite_hoister_cfg: public default_rewriter_cfg {
|
||||
ite_hoister m_r;
|
||||
bool rewrite_patterns() const { return false; }
|
||||
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr)
|
||||
{
|
||||
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
|
||||
return m_r.mk_app_core(f, num, args, result);
|
||||
}
|
||||
ite_hoister_cfg(ast_manager & m, params_ref const & p):m_r(m) {}
|
||||
};
|
||||
|
||||
|
||||
class ite_hoister_star : public rewriter_tpl<ite_hoister_cfg> {
|
||||
ite_hoister_cfg m_cfg;
|
||||
public:
|
||||
|
@ -247,9 +240,8 @@ void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml)
|
|||
rewriter_tpl<ite_hoister_cfg>(m, false, m_cfg),
|
||||
m_cfg(m, p) {}
|
||||
};
|
||||
|
||||
void hoist_non_bool_if(expr_ref& fml)
|
||||
{
|
||||
|
||||
void hoist_non_bool_if(expr_ref& fml) {
|
||||
ast_manager& m = fml.get_manager();
|
||||
scoped_no_proof _sp(m);
|
||||
params_ref p;
|
||||
|
@ -266,8 +258,7 @@ void hoist_non_bool_if(expr_ref& fml)
|
|||
bool m_is_dl;
|
||||
bool m_test_for_utvpi;
|
||||
|
||||
bool is_numeric(expr* e) const
|
||||
{
|
||||
bool is_numeric(expr* e) const {
|
||||
if (a.is_numeral(e)) {
|
||||
return true;
|
||||
}
|
||||
|
@ -278,13 +269,11 @@ void hoist_non_bool_if(expr_ref& fml)
|
|||
return false;
|
||||
}
|
||||
|
||||
bool is_arith_expr(expr *e) const
|
||||
{
|
||||
bool is_arith_expr(expr *e) const {
|
||||
return is_app(e) && a.get_family_id() == to_app(e)->get_family_id();
|
||||
}
|
||||
|
||||
bool is_offset(expr* e) const
|
||||
{
|
||||
|
||||
bool is_offset(expr* e) const {
|
||||
if (a.is_numeral(e)) {
|
||||
return true;
|
||||
}
|
||||
|
@ -315,47 +304,44 @@ void hoist_non_bool_if(expr_ref& fml)
|
|||
return !is_arith_expr(e);
|
||||
}
|
||||
|
||||
bool is_minus_one(expr const * e) const
|
||||
{
|
||||
rational r;
|
||||
return a.is_numeral(e, r) && r.is_minus_one();
|
||||
bool is_minus_one(expr const * e) const {
|
||||
rational r;
|
||||
return a.is_numeral(e, r) && r.is_minus_one();
|
||||
}
|
||||
|
||||
bool test_ineq(expr* e) const
|
||||
{
|
||||
bool test_ineq(expr* e) const {
|
||||
SASSERT(a.is_le(e) || a.is_ge(e) || m.is_eq(e));
|
||||
SASSERT(to_app(e)->get_num_args() == 2);
|
||||
expr * lhs = to_app(e)->get_arg(0);
|
||||
expr * rhs = to_app(e)->get_arg(1);
|
||||
if (is_offset(lhs) && is_offset(rhs))
|
||||
{ return true; }
|
||||
{ return true; }
|
||||
if (!is_numeric(rhs))
|
||||
{ std::swap(lhs, rhs); }
|
||||
{ std::swap(lhs, rhs); }
|
||||
if (!is_numeric(rhs))
|
||||
{ return false; }
|
||||
{ return false; }
|
||||
// lhs can be 'x' or '(+ x (* -1 y))'
|
||||
if (is_offset(lhs))
|
||||
{ return true; }
|
||||
{ return true; }
|
||||
expr* arg1, *arg2;
|
||||
if (!a.is_add(lhs, arg1, arg2))
|
||||
{ return false; }
|
||||
{ return false; }
|
||||
// x
|
||||
if (m_test_for_utvpi) {
|
||||
return is_offset(arg1) && is_offset(arg2);
|
||||
}
|
||||
if (is_arith_expr(arg1))
|
||||
{ std::swap(arg1, arg2); }
|
||||
{ std::swap(arg1, arg2); }
|
||||
if (is_arith_expr(arg1))
|
||||
{ return false; }
|
||||
{ return false; }
|
||||
// arg2: (* -1 y)
|
||||
expr* m1, *m2;
|
||||
if (!a.is_mul(arg2, m1, m2))
|
||||
{ return false; }
|
||||
{ return false; }
|
||||
return is_minus_one(m1) && is_offset(m2);
|
||||
}
|
||||
|
||||
bool test_eq(expr* e) const
|
||||
{
|
||||
bool test_eq(expr* e) const {
|
||||
expr* lhs, *rhs;
|
||||
VERIFY(m.is_eq(e, lhs, rhs));
|
||||
if (!a.is_int_real(lhs)) {
|
||||
|
@ -370,9 +356,8 @@ void hoist_non_bool_if(expr_ref& fml)
|
|||
!a.is_mul(lhs) &&
|
||||
!a.is_mul(rhs);
|
||||
}
|
||||
|
||||
bool test_term(expr* e) const
|
||||
{
|
||||
|
||||
bool test_term(expr* e) const {
|
||||
if (m.is_bool(e)) {
|
||||
return true;
|
||||
}
|
||||
|
@ -490,7 +475,7 @@ bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls)
|
|||
* eliminate simple equalities using qe_lite
|
||||
* then, MBP for Booleans (substitute), reals (based on LW), ints (based on Cooper), and arrays
|
||||
*/
|
||||
void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml,
|
||||
void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml,
|
||||
const model_ref& M, bool reduce_all_selects, bool use_native_mbp,
|
||||
bool dont_sub)
|
||||
{
|
||||
|
|
|
@ -74,15 +74,6 @@ inline std::ostream& operator<<(std::ostream& out, pp_level const& p)
|
|||
}
|
||||
|
||||
|
||||
struct scoped_watch {
|
||||
stopwatch &m_sw;
|
||||
scoped_watch (stopwatch &sw, bool reset=false): m_sw(sw)
|
||||
{
|
||||
if(reset) { m_sw.reset(); }
|
||||
m_sw.start ();
|
||||
}
|
||||
~scoped_watch () {m_sw.stop ();}
|
||||
};
|
||||
|
||||
|
||||
typedef ptr_vector<app> app_vector;
|
||||
|
|
|
@ -23,7 +23,8 @@ Notes:
|
|||
#include "muz/spacer/spacer_util.h"
|
||||
#include "ast/rewriter/bool_rewriter.h"
|
||||
|
||||
#include "ast/proof_checker/proof_checker.h"
|
||||
#include "ast/proofs/proof_checker.h"
|
||||
#include "ast/proofs/proof_utils.h"
|
||||
|
||||
#include "ast/scoped_proof.h"
|
||||
|
||||
|
@ -64,172 +65,11 @@ virtual_solver::~virtual_solver()
|
|||
}
|
||||
|
||||
namespace {
|
||||
static bool matches_fact(expr_ref_vector &args, expr* &match)
|
||||
{
|
||||
ast_manager &m = args.get_manager();
|
||||
expr *fact = args.back();
|
||||
for (unsigned i = 0, sz = args.size() - 1; i < sz; ++i) {
|
||||
expr *arg = args.get(i);
|
||||
if (m.is_proof(arg) &&
|
||||
m.has_fact(to_app(arg)) &&
|
||||
m.get_fact(to_app(arg)) == fact) {
|
||||
match = arg;
|
||||
return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
class elim_aux_assertions {
|
||||
app_ref m_aux;
|
||||
public:
|
||||
elim_aux_assertions(app_ref aux) : m_aux(aux) {}
|
||||
// TBD: move to ast/proofs/elim_aux_assertions
|
||||
|
||||
void mk_or_core(expr_ref_vector &args, expr_ref &res)
|
||||
{
|
||||
ast_manager &m = args.get_manager();
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0, sz = args.size(); i < sz; ++i) {
|
||||
if (m.is_false(args.get(i))) { continue; }
|
||||
if (i != j) { args [j] = args.get(i); }
|
||||
++j;
|
||||
}
|
||||
SASSERT(j >= 1);
|
||||
res = j > 1 ? m.mk_or(j, args.c_ptr()) : args.get(0);
|
||||
}
|
||||
|
||||
void mk_app(func_decl *decl, expr_ref_vector &args, expr_ref &res)
|
||||
{
|
||||
ast_manager &m = args.get_manager();
|
||||
bool_rewriter brwr(m);
|
||||
|
||||
if (m.is_or(decl))
|
||||
{ mk_or_core(args, res); }
|
||||
else if (m.is_iff(decl) && args.size() == 2)
|
||||
// avoiding simplifying equalities. In particular,
|
||||
// we don't want (= (not a) (not b)) to be reduced to (= a b)
|
||||
{ res = m.mk_iff(args.get(0), args.get(1)); }
|
||||
else
|
||||
{ brwr.mk_app(decl, args.size(), args.c_ptr(), res); }
|
||||
}
|
||||
|
||||
void operator()(ast_manager &m, proof *pr, proof_ref &res)
|
||||
{
|
||||
DEBUG_CODE(proof_checker pc(m);
|
||||
expr_ref_vector side(m);
|
||||
SASSERT(pc.check(pr, side));
|
||||
);
|
||||
obj_map<app, app*> cache;
|
||||
bool_rewriter brwr(m);
|
||||
|
||||
// for reference counting of new proofs
|
||||
app_ref_vector pinned(m);
|
||||
|
||||
ptr_vector<app> todo;
|
||||
todo.push_back(pr);
|
||||
|
||||
expr_ref not_aux(m);
|
||||
not_aux = m.mk_not(m_aux);
|
||||
|
||||
expr_ref_vector args(m);
|
||||
|
||||
while (!todo.empty()) {
|
||||
app *p, *r;
|
||||
expr *a;
|
||||
|
||||
p = todo.back();
|
||||
if (cache.find(pr, r)) {
|
||||
todo.pop_back();
|
||||
continue;
|
||||
}
|
||||
|
||||
SASSERT(!todo.empty() || pr == p);
|
||||
bool dirty = false;
|
||||
unsigned todo_sz = todo.size();
|
||||
args.reset();
|
||||
for (unsigned i = 0, sz = p->get_num_args(); i < sz; ++i) {
|
||||
expr* arg = p->get_arg(i);
|
||||
if (arg == m_aux.get()) {
|
||||
dirty = true;
|
||||
args.push_back(m.mk_true());
|
||||
} else if (arg == not_aux.get()) {
|
||||
dirty = true;
|
||||
args.push_back(m.mk_false());
|
||||
}
|
||||
// skip (asserted m_aux)
|
||||
else if (m.is_asserted(arg, a) && a == m_aux.get()) {
|
||||
dirty = true;
|
||||
}
|
||||
// skip (hypothesis m_aux)
|
||||
else if (m.is_hypothesis(arg, a) && a == m_aux.get()) {
|
||||
dirty = true;
|
||||
} else if (is_app(arg) && cache.find(to_app(arg), r)) {
|
||||
dirty |= (arg != r);
|
||||
args.push_back(r);
|
||||
} else if (is_app(arg))
|
||||
{ todo.push_back(to_app(arg)); }
|
||||
else
|
||||
// -- not an app
|
||||
{ args.push_back(arg); }
|
||||
|
||||
}
|
||||
if (todo_sz < todo.size()) {
|
||||
// -- process parents
|
||||
args.reset();
|
||||
continue;
|
||||
}
|
||||
|
||||
// ready to re-create
|
||||
app_ref newp(m);
|
||||
if (!dirty) { newp = p; }
|
||||
else if (m.is_unit_resolution(p)) {
|
||||
if (args.size() == 2)
|
||||
// unit resolution with m_aux that got collapsed to nothing
|
||||
{ newp = to_app(args.get(0)); }
|
||||
else {
|
||||
ptr_vector<proof> parents;
|
||||
for (unsigned i = 0, sz = args.size() - 1; i < sz; ++i)
|
||||
{ parents.push_back(to_app(args.get(i))); }
|
||||
SASSERT(parents.size() == args.size() - 1);
|
||||
newp = m.mk_unit_resolution(parents.size(), parents.c_ptr());
|
||||
// XXX the old and new facts should be
|
||||
// equivalent. The test here is much
|
||||
// stronger. It might need to be relaxed.
|
||||
SASSERT(m.get_fact(newp) == args.back());
|
||||
pinned.push_back(newp);
|
||||
}
|
||||
} else if (matches_fact(args, a)) {
|
||||
newp = to_app(a);
|
||||
} else {
|
||||
expr_ref papp(m);
|
||||
mk_app(p->get_decl(), args, papp);
|
||||
newp = to_app(papp.get());
|
||||
pinned.push_back(newp);
|
||||
}
|
||||
cache.insert(p, newp);
|
||||
todo.pop_back();
|
||||
CTRACE("virtual",
|
||||
p->get_decl_kind() == PR_TH_LEMMA &&
|
||||
p->get_decl()->get_parameter(0).get_symbol() == "arith" &&
|
||||
p->get_decl()->get_num_parameters() > 1 &&
|
||||
p->get_decl()->get_parameter(1).get_symbol() == "farkas",
|
||||
tout << "Old pf: " << mk_pp(p, m) << "\n"
|
||||
<< "New pf: " << mk_pp(newp, m) << "\n";);
|
||||
}
|
||||
|
||||
proof *r;
|
||||
VERIFY(cache.find(pr, r));
|
||||
|
||||
DEBUG_CODE(
|
||||
proof_checker pc(m);
|
||||
expr_ref_vector side(m);
|
||||
SASSERT(pc.check(r, side));
|
||||
);
|
||||
|
||||
res = r ;
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
proof *virtual_solver::get_proof()
|
||||
|
@ -349,15 +189,16 @@ void virtual_solver::push_core()
|
|||
m_context.push();
|
||||
}
|
||||
}
|
||||
void virtual_solver::pop_core(unsigned n)
|
||||
{
|
||||
void virtual_solver::pop_core(unsigned n) {
|
||||
SASSERT(!m_pushed || get_scope_level() > 0);
|
||||
if (m_pushed) {
|
||||
SASSERT(!m_in_delay_scope);
|
||||
m_context.pop(n);
|
||||
m_pushed = get_scope_level() - n > 0;
|
||||
} else
|
||||
{ m_in_delay_scope = get_scope_level() - n > 0; }
|
||||
}
|
||||
else {
|
||||
m_in_delay_scope = get_scope_level() - n > 0;
|
||||
}
|
||||
}
|
||||
|
||||
void virtual_solver::get_unsat_core(ptr_vector<expr> &r)
|
||||
|
|
|
@ -92,7 +92,6 @@ public:
|
|||
virtual bool get_produce_models();
|
||||
virtual smt_params &fparams();
|
||||
virtual void reset();
|
||||
|
||||
virtual void set_progress_callback(progress_callback *callback)
|
||||
{UNREACHABLE();}
|
||||
|
||||
|
@ -134,6 +133,9 @@ private:
|
|||
|
||||
|
||||
void refresh();
|
||||
|
||||
smt_params &fparams() { return m_fparams; }
|
||||
|
||||
public:
|
||||
virtual_solver_factory(ast_manager &mgr, smt_params &fparams);
|
||||
virtual ~virtual_solver_factory();
|
||||
|
@ -144,7 +146,6 @@ public:
|
|||
void collect_param_descrs(param_descrs &r) { /* empty */ }
|
||||
void set_produce_models(bool f) { m_fparams.m_model = f; }
|
||||
bool get_produce_models() { return m_fparams.m_model; }
|
||||
smt_params &fparams() { return m_fparams; }
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
@ -315,14 +315,13 @@ public:
|
|||
|
||||
void found_optimum() {
|
||||
IF_VERBOSE(1, verbose_stream() << "found optimum\n";);
|
||||
rational upper(0);
|
||||
m_lower.reset();
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
m_assignment[i] = is_true(m_soft[i]);
|
||||
if (!m_assignment[i]) {
|
||||
upper += m_weights[i];
|
||||
m_lower += m_weights[i];
|
||||
}
|
||||
}
|
||||
SASSERT(upper == m_lower);
|
||||
m_upper = m_lower;
|
||||
m_found_feasible_optimum = true;
|
||||
}
|
||||
|
@ -397,10 +396,11 @@ public:
|
|||
void get_current_correction_set(model* mdl, exprs& cs) {
|
||||
cs.reset();
|
||||
if (!mdl) return;
|
||||
for (unsigned i = 0; i < m_asms.size(); ++i) {
|
||||
if (is_false(mdl, m_asms[i].get())) {
|
||||
cs.push_back(m_asms[i].get());
|
||||
for (expr* a : m_asms) {
|
||||
if (is_false(mdl, a)) {
|
||||
cs.push_back(a);
|
||||
}
|
||||
TRACE("opt", expr_ref tmp(m); mdl->eval(a, tmp, true); tout << mk_pp(a, m) << ": " << tmp << "\n";);
|
||||
}
|
||||
TRACE("opt", display_vec(tout << "new correction set: ", cs););
|
||||
}
|
||||
|
@ -509,6 +509,7 @@ public:
|
|||
trace();
|
||||
if (m_c.num_objectives() == 1 && m_pivot_on_cs && m_csmodel.get() && m_correction_set_size < core.size()) {
|
||||
exprs cs;
|
||||
TRACE("opt", tout << "cs " << m_correction_set_size << " " << core.size() << "\n";);
|
||||
get_current_correction_set(m_csmodel.get(), cs);
|
||||
m_correction_set_size = cs.size();
|
||||
if (m_correction_set_size < core.size()) {
|
||||
|
|
|
@ -819,7 +819,7 @@ namespace opt {
|
|||
bool is_max = is_maximize(fml, term, orig_term, index);
|
||||
bool is_min = !is_max && is_minimize(fml, term, orig_term, index);
|
||||
if (is_min && get_pb_sum(term, terms, weights, offset)) {
|
||||
TRACE("opt", tout << "try to convert minimization" << mk_pp(term, m) << "\n";);
|
||||
TRACE("opt", tout << "try to convert minimization\n" << mk_pp(term, m) << "\n";);
|
||||
// minimize 2*x + 3*y
|
||||
// <=>
|
||||
// (assert-soft (not x) 2)
|
||||
|
|
|
@ -47,8 +47,9 @@ namespace opt {
|
|||
m_dump_benchmarks(false),
|
||||
m_first(true),
|
||||
m_was_unknown(false) {
|
||||
solver::updt_params(p);
|
||||
m_params.updt_params(p);
|
||||
if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {
|
||||
if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {
|
||||
m_params.m_relevancy_lvl = 0;
|
||||
}
|
||||
// m_params.m_auto_config = false;
|
||||
|
|
|
@ -34,7 +34,7 @@ Revision History:
|
|||
namespace smtlib {
|
||||
|
||||
solver::solver():
|
||||
m_ast_manager(m_params.m_proof ? PGM_FINE : PGM_DISABLED,
|
||||
m_ast_manager(m_params.m_proof ? PGM_ENABLED : PGM_DISABLED,
|
||||
m_params.m_trace ? m_params.m_trace_file_name.c_str() : 0),
|
||||
m_ctx(0),
|
||||
m_error_code(0) {
|
||||
|
|
|
@ -1,5 +1,6 @@
|
|||
z3_add_component(smt2parser
|
||||
SOURCES
|
||||
marshal.cpp
|
||||
smt2parser.cpp
|
||||
smt2scanner.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
|
|
|
@ -2,14 +2,14 @@
|
|||
Copyright (c) 2017 Arie Gurfinkel
|
||||
Module Name:
|
||||
|
||||
spacer_marshal.cpp
|
||||
marshal.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
marshaling and unmarshaling of expressions
|
||||
|
||||
--*/
|
||||
#include "muz/spacer/spacer_marshal.h"
|
||||
#include "parsers/smt2/marshal.h"
|
||||
|
||||
#include <sstream>
|
||||
|
||||
|
@ -18,39 +18,33 @@ Abstract:
|
|||
#include "util/vector.h"
|
||||
#include "ast/ast_smt_pp.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/ast_util.h"
|
||||
|
||||
namespace spacer {
|
||||
std::ostream &marshal(std::ostream &os, expr_ref e, ast_manager &m)
|
||||
{
|
||||
std::ostream &marshal(std::ostream &os, expr_ref e, ast_manager &m) {
|
||||
ast_smt_pp pp(m);
|
||||
pp.display_smt2(os, e);
|
||||
return os;
|
||||
}
|
||||
|
||||
std::string marshal(expr_ref e, ast_manager &m)
|
||||
{
|
||||
std::string marshal(expr_ref e, ast_manager &m) {
|
||||
std::stringstream ss;
|
||||
marshal(ss, e, m);
|
||||
return ss.str();
|
||||
}
|
||||
|
||||
|
||||
expr_ref unmarshal(std::istream &is, ast_manager &m)
|
||||
{
|
||||
expr_ref unmarshal(std::istream &is, ast_manager &m) {
|
||||
cmd_context ctx(false, &m);
|
||||
ctx.set_ignore_check(true);
|
||||
if (!parse_smt2_commands(ctx, is)) { return expr_ref(0, m); }
|
||||
|
||||
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
|
||||
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
|
||||
if (it == end) { return expr_ref(m.mk_true(), m); }
|
||||
unsigned size = static_cast<unsigned>(end - it);
|
||||
return expr_ref(m.mk_and(size, it), m);
|
||||
return expr_ref(mk_and(m, size, it), m);
|
||||
}
|
||||
|
||||
expr_ref unmarshal(std::string s, ast_manager &m)
|
||||
{
|
||||
expr_ref unmarshal(std::string s, ast_manager &m) {
|
||||
std::istringstream is(s);
|
||||
return unmarshal(is, m);
|
||||
}
|
||||
}
|
|
@ -2,7 +2,7 @@
|
|||
Copyright (c) 2017 Arie Gurfinkel
|
||||
Module Name:
|
||||
|
||||
spacer_marshal.h
|
||||
marshal.h
|
||||
|
||||
Abstract:
|
||||
|
||||
|
@ -17,14 +17,11 @@ Abstract:
|
|||
|
||||
#include "ast/ast.h"
|
||||
|
||||
namespace spacer {
|
||||
std::ostream &marshal(std::ostream &os, expr_ref e, ast_manager &m);
|
||||
std::string marshal(expr_ref e, ast_manager &m);
|
||||
expr_ref unmarshal(std::string s, ast_manager &m);
|
||||
expr_ref unmarshal(std::istream &is, ast_manager &m);
|
||||
|
||||
|
||||
}
|
||||
|
||||
|
||||
#endif
|
|
@ -69,7 +69,7 @@ class inc_sat_solver : public solver {
|
|||
public:
|
||||
inc_sat_solver(ast_manager& m, params_ref const& p):
|
||||
m(m), m_solver(p, m.limit(), 0),
|
||||
m_params(p), m_optimize_model(false),
|
||||
m_optimize_model(false),
|
||||
m_fmls(m),
|
||||
m_asmsf(m),
|
||||
m_fmls_head(0),
|
||||
|
@ -79,7 +79,7 @@ public:
|
|||
m_dep_core(m),
|
||||
m_unknown("no reason given") {
|
||||
m_params.set_bool("elim_vars", false);
|
||||
m_solver.updt_params(m_params);
|
||||
updt_params(p);
|
||||
init_preprocess();
|
||||
}
|
||||
|
||||
|
@ -237,7 +237,7 @@ public:
|
|||
sat::solver::collect_param_descrs(r);
|
||||
}
|
||||
virtual void updt_params(params_ref const & p) {
|
||||
m_params = p;
|
||||
solver::updt_params(p);
|
||||
m_params.set_bool("elim_vars", false);
|
||||
m_solver.updt_params(m_params);
|
||||
m_optimize_model = m_params.get_bool("optimize_model", false);
|
||||
|
|
|
@ -75,7 +75,7 @@ z3_add_component(smt
|
|||
normal_forms
|
||||
parser_util
|
||||
pattern
|
||||
proof_checker
|
||||
proofs
|
||||
proto_model
|
||||
simplex
|
||||
substitution
|
||||
|
|
|
@ -101,14 +101,14 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_ex
|
|||
else if (m.is_and(e)) {
|
||||
for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
|
||||
expr* arg = to_app(e)->get_arg(i);
|
||||
proof_ref _pr(m.mk_and_elim(pr, i), m);
|
||||
proof_ref _pr(m.proofs_enabled() ? m.mk_and_elim(pr, i) : 0, m);
|
||||
push_assertion(arg, _pr, result);
|
||||
}
|
||||
}
|
||||
else if (m.is_not(e, e1) && m.is_or(e1)) {
|
||||
for (unsigned i = 0; i < to_app(e1)->get_num_args(); ++i) {
|
||||
expr* arg = to_app(e1)->get_arg(i);
|
||||
proof_ref _pr(m.mk_not_or_elim(pr, i), m);
|
||||
proof_ref _pr(m.proofs_enabled() ? m.mk_not_or_elim(pr, i) : 0, m);
|
||||
expr_ref narg(mk_not(m, arg), m);
|
||||
push_assertion(narg, _pr, result);
|
||||
}
|
||||
|
@ -163,7 +163,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
|
|||
}
|
||||
|
||||
void asserted_formulas::assert_expr(expr * e) {
|
||||
assert_expr(e, m.mk_asserted(e));
|
||||
assert_expr(e, m.proofs_enabled() ? m.mk_asserted(e) : nullptr);
|
||||
}
|
||||
|
||||
void asserted_formulas::get_assertions(ptr_vector<expr> & result) const {
|
||||
|
@ -365,7 +365,7 @@ void asserted_formulas::nnf_cnf() {
|
|||
CASSERT("well_sorted", is_well_sorted(m, n));
|
||||
apply_nnf(n, push_todo, push_todo_prs, r1, pr1);
|
||||
CASSERT("well_sorted",is_well_sorted(m, r1));
|
||||
pr = m.mk_modus_ponens(pr, pr1);
|
||||
pr = m.proofs_enabled() ? m.mk_modus_ponens(pr, pr1) : nullptr;
|
||||
push_todo.push_back(r1);
|
||||
push_todo_prs.push_back(pr);
|
||||
|
||||
|
@ -506,16 +506,16 @@ void asserted_formulas::update_substitution(expr* n, proof* pr) {
|
|||
}
|
||||
if (is_gt(rhs, lhs)) {
|
||||
TRACE("propagate_values", tout << "insert " << mk_pp(rhs, m) << " -> " << mk_pp(lhs, m) << "\n";);
|
||||
m_scoped_substitution.insert(rhs, lhs, m.mk_symmetry(pr));
|
||||
m_scoped_substitution.insert(rhs, lhs, m.proofs_enabled() ? m.mk_symmetry(pr) : nullptr);
|
||||
return;
|
||||
}
|
||||
TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";);
|
||||
}
|
||||
if (m.is_not(n, n1)) {
|
||||
m_scoped_substitution.insert(n1, m.mk_false(), m.mk_iff_false(pr));
|
||||
m_scoped_substitution.insert(n1, m.mk_false(), m.proofs_enabled() ? m.mk_iff_false(pr) : nullptr);
|
||||
}
|
||||
else {
|
||||
m_scoped_substitution.insert(n, m.mk_true(), m.mk_iff_true(pr));
|
||||
m_scoped_substitution.insert(n, m.mk_true(), m.proofs_enabled() ? m.mk_iff_true(pr) : nullptr);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -810,8 +810,6 @@ namespace smt {
|
|||
m_new_proofs.push_back(pr);
|
||||
return pr;
|
||||
}
|
||||
if (m_manager.coarse_grain_proofs())
|
||||
return pr;
|
||||
TRACE("norm_eq_proof",
|
||||
tout << "#" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";
|
||||
tout << mk_ll_pp(pr, m_manager, true, false););
|
||||
|
@ -1217,7 +1215,7 @@ namespace smt {
|
|||
mk_proof(rhs, c, prs2);
|
||||
while (!prs2.empty()) {
|
||||
proof * pr = prs2.back();
|
||||
if (m_manager.fine_grain_proofs()) {
|
||||
if (m_manager.proofs_enabled()) {
|
||||
pr = m_manager.mk_symmetry(pr);
|
||||
m_new_proofs.push_back(pr);
|
||||
prs1.push_back(pr);
|
||||
|
|
|
@ -23,7 +23,7 @@ Revision History:
|
|||
#include "ast/ast_ll_pp.h"
|
||||
#include "util/warning.h"
|
||||
#include "smt/smt_quick_checker.h"
|
||||
#include "ast/proof_checker/proof_checker.h"
|
||||
#include "ast/proofs/proof_checker.h"
|
||||
#include "ast/ast_util.h"
|
||||
#include "smt/uses_theory.h"
|
||||
#include "model/model.h"
|
||||
|
|
|
@ -129,7 +129,7 @@ namespace smt {
|
|||
|
||||
if (m_node1 != m_node1->get_root()) {
|
||||
proof * pr = cr.get_proof(m_node1, m_node1->get_root());
|
||||
if (pr && m.fine_grain_proofs())
|
||||
if (pr && m.proofs_enabled())
|
||||
pr = m.mk_symmetry(pr);
|
||||
prs.push_back(pr);
|
||||
if (!pr)
|
||||
|
|
|
@ -29,9 +29,8 @@ Notes:
|
|||
|
||||
namespace smt {
|
||||
|
||||
class solver : public solver_na2as {
|
||||
class smt_solver : public solver_na2as {
|
||||
smt_params m_smt_params;
|
||||
params_ref m_params;
|
||||
smt::kernel m_context;
|
||||
progress_callback * m_callback;
|
||||
symbol m_logic;
|
||||
|
@ -42,28 +41,24 @@ namespace smt {
|
|||
obj_map<expr, expr*> m_name2assertion;
|
||||
|
||||
public:
|
||||
solver(ast_manager & m, params_ref const & p, symbol const & l) :
|
||||
smt_solver(ast_manager & m, params_ref const & p, symbol const & l) :
|
||||
solver_na2as(m),
|
||||
m_smt_params(p),
|
||||
m_params(p),
|
||||
m_context(m, m_smt_params),
|
||||
m_minimizing_core(false),
|
||||
m_core_extend_patterns(false),
|
||||
m_core_extend_patterns_max_distance(UINT_MAX),
|
||||
m_core_extend_nonlocal_patterns(false) {
|
||||
m_core_extend_nonlocal_patterns(false) {
|
||||
m_logic = l;
|
||||
if (m_logic != symbol::null)
|
||||
m_context.set_logic(m_logic);
|
||||
smt_params_helper smth(p);
|
||||
m_core_extend_patterns = smth.core_extend_patterns();
|
||||
m_core_extend_patterns_max_distance = smth.core_extend_patterns_max_distance();
|
||||
m_core_extend_nonlocal_patterns = smth.core_extend_nonlocal_patterns();
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
virtual solver * translate(ast_manager & m, params_ref const & p) {
|
||||
ast_translation translator(get_manager(), m);
|
||||
|
||||
solver * result = alloc(solver, m, p, m_logic);
|
||||
smt_solver * result = alloc(smt_solver, m, p, m_logic);
|
||||
smt::kernel::copy(m_context, result->m_context);
|
||||
|
||||
for (auto & kv : m_name2assertion)
|
||||
|
@ -73,13 +68,13 @@ namespace smt {
|
|||
return result;
|
||||
}
|
||||
|
||||
virtual ~solver() {
|
||||
virtual ~smt_solver() {
|
||||
dec_ref_values(get_manager(), m_name2assertion);
|
||||
}
|
||||
|
||||
virtual void updt_params(params_ref const & p) {
|
||||
solver::updt_params(p);
|
||||
m_smt_params.updt_params(p);
|
||||
m_params.copy(p);
|
||||
m_context.updt_params(p);
|
||||
smt_params_helper smth(p);
|
||||
m_core_extend_patterns = smth.core_extend_patterns();
|
||||
|
@ -146,9 +141,9 @@ namespace smt {
|
|||
}
|
||||
|
||||
struct scoped_minimize_core {
|
||||
solver& s;
|
||||
smt_solver& s;
|
||||
expr_ref_vector m_assumptions;
|
||||
scoped_minimize_core(solver& s) : s(s), m_assumptions(s.m_assumptions) {
|
||||
scoped_minimize_core(smt_solver& s) : s(s), m_assumptions(s.m_assumptions) {
|
||||
s.m_minimizing_core = true;
|
||||
s.m_assumptions.reset();
|
||||
}
|
||||
|
@ -165,7 +160,7 @@ namespace smt {
|
|||
r.push_back(m_context.get_unsat_core_expr(i));
|
||||
}
|
||||
|
||||
if (m_minimizing_core && smt_params_helper(m_params).core_minimize()) {
|
||||
if (m_minimizing_core && smt_params_helper(get_params()).core_minimize()) {
|
||||
scoped_minimize_core scm(*this);
|
||||
mus mus(*this);
|
||||
mus.add_soft(r.size(), r.c_ptr());
|
||||
|
@ -346,22 +341,16 @@ namespace smt {
|
|||
|
||||
void add_nonlocal_pattern_literals_to_core(ptr_vector<expr> & core) {
|
||||
ast_manager & m = get_manager();
|
||||
|
||||
obj_map<expr, expr*>::iterator it = m_name2assertion.begin();
|
||||
obj_map<expr, expr*>::iterator end = m_name2assertion.end();
|
||||
for (unsigned i = 0; it != end; it++, i++) {
|
||||
expr_ref name(it->m_key, m);
|
||||
expr_ref assrtn(it->m_value, m);
|
||||
for (auto const& kv : m_name2assertion) {
|
||||
expr_ref name(kv.m_key, m);
|
||||
expr_ref assrtn(kv.m_value, m);
|
||||
|
||||
if (!core.contains(name)) {
|
||||
func_decl_set pattern_fds, body_fds;
|
||||
collect_pattern_fds(assrtn, pattern_fds);
|
||||
collect_body_func_decls(assrtn, body_fds);
|
||||
|
||||
func_decl_set::iterator pit = pattern_fds.begin();
|
||||
func_decl_set::iterator pend= pattern_fds.end();
|
||||
for (; pit != pend; pit++) {
|
||||
func_decl * fd = *pit;
|
||||
for (func_decl *fd : pattern_fds) {
|
||||
if (!body_fds.contains(fd)) {
|
||||
core.insert(name);
|
||||
break;
|
||||
|
@ -374,7 +363,7 @@ namespace smt {
|
|||
};
|
||||
|
||||
solver * mk_smt_solver(ast_manager & m, params_ref const & p, symbol const & logic) {
|
||||
return alloc(smt::solver, m, p, logic);
|
||||
return alloc(smt::smt_solver, m, p, logic);
|
||||
}
|
||||
|
||||
class smt_solver_factory : public solver_factory {
|
||||
|
|
|
@ -218,7 +218,6 @@ namespace smt {
|
|||
ast_manager & m = get_manager();
|
||||
ext_skolems = alloc(func_decl_ref_vector, m);
|
||||
for (unsigned i = 0; i < dimension; ++i) {
|
||||
sort * ext_sk_domain[2] = { s_array, s_array };
|
||||
func_decl * ext_sk_decl = util.mk_array_ext(s_array, i);
|
||||
ext_skolems->push_back(ext_sk_decl);
|
||||
}
|
||||
|
|
|
@ -190,13 +190,13 @@ namespace smt {
|
|||
|
||||
expr * theory_str::rewrite_implication(expr * premise, expr * conclusion) {
|
||||
ast_manager & m = get_manager();
|
||||
return m.mk_or(m.mk_not(premise), conclusion);
|
||||
return m.mk_or(mk_not(m, premise), conclusion);
|
||||
}
|
||||
|
||||
void theory_str::assert_implication(expr * premise, expr * conclusion) {
|
||||
ast_manager & m = get_manager();
|
||||
TRACE("str", tout << "asserting implication " << mk_ismt2_pp(premise, m) << " -> " << mk_ismt2_pp(conclusion, m) << std::endl;);
|
||||
expr_ref axiom(m.mk_or(m.mk_not(premise), conclusion), m);
|
||||
expr_ref axiom(m.mk_or(mk_not(m, premise), conclusion), m);
|
||||
assert_axiom(axiom);
|
||||
}
|
||||
|
||||
|
@ -545,7 +545,7 @@ namespace smt {
|
|||
context & ctx = get_context();
|
||||
ast_manager & m = get_manager();
|
||||
|
||||
expr_ref ax1(m.mk_not(ctx.mk_eq_atom(s, mk_string(""))), m);
|
||||
expr_ref ax1(mk_not(m, ctx.mk_eq_atom(s, mk_string(""))), m);
|
||||
assert_axiom(ax1);
|
||||
|
||||
{
|
||||
|
@ -557,7 +557,7 @@ namespace smt {
|
|||
SASSERT(zero);
|
||||
// build LHS > RHS and assert
|
||||
// we have to build !(LHS <= RHS) instead
|
||||
expr_ref lhs_gt_rhs(m.mk_not(m_autil.mk_le(len_str, zero)), m);
|
||||
expr_ref lhs_gt_rhs(mk_not(m, m_autil.mk_le(len_str, zero)), m);
|
||||
SASSERT(lhs_gt_rhs);
|
||||
assert_axiom(lhs_gt_rhs);
|
||||
}
|
||||
|
@ -592,7 +592,7 @@ namespace smt {
|
|||
SASSERT(zero);
|
||||
// build LHS > RHS and assert
|
||||
// we have to build !(LHS <= RHS) instead
|
||||
expr_ref lhs_gt_rhs(m.mk_not(m_autil.mk_le(len_str, zero)), m);
|
||||
expr_ref lhs_gt_rhs(mk_not(m, m_autil.mk_le(len_str, zero)), m);
|
||||
SASSERT(lhs_gt_rhs);
|
||||
assert_axiom(lhs_gt_rhs);
|
||||
}
|
||||
|
@ -1089,7 +1089,7 @@ namespace smt {
|
|||
m_autil.mk_ge(expr->get_arg(1), mk_int(0)),
|
||||
// REWRITE for arithmetic theory:
|
||||
// m_autil.mk_lt(expr->get_arg(1), mk_strlen(expr->get_arg(0)))
|
||||
m.mk_not(m_autil.mk_ge(m_autil.mk_add(expr->get_arg(1), m_autil.mk_mul(mk_int(-1), mk_strlen(expr->get_arg(0)))), mk_int(0)))
|
||||
mk_not(m, m_autil.mk_ge(m_autil.mk_add(expr->get_arg(1), m_autil.mk_mul(mk_int(-1), mk_strlen(expr->get_arg(0)))), mk_int(0)))
|
||||
), m);
|
||||
|
||||
expr_ref_vector and_item(m);
|
||||
|
@ -1130,7 +1130,7 @@ namespace smt {
|
|||
expr_ref_vector innerItems(m);
|
||||
innerItems.push_back(ctx.mk_eq_atom(expr->get_arg(1), mk_concat(ts0, ts1)));
|
||||
innerItems.push_back(ctx.mk_eq_atom(mk_strlen(ts0), mk_strlen(expr->get_arg(0))));
|
||||
innerItems.push_back(m.mk_ite(ctx.mk_eq_atom(ts0, expr->get_arg(0)), expr, m.mk_not(expr)));
|
||||
innerItems.push_back(m.mk_ite(ctx.mk_eq_atom(ts0, expr->get_arg(0)), expr, mk_not(m, expr)));
|
||||
expr_ref then1(m.mk_and(innerItems.size(), innerItems.c_ptr()), m);
|
||||
SASSERT(then1);
|
||||
|
||||
|
@ -1143,7 +1143,7 @@ namespace smt {
|
|||
, m);
|
||||
SASSERT(topLevelCond);
|
||||
|
||||
expr_ref finalAxiom(m.mk_ite(topLevelCond, then1, m.mk_not(expr)), m);
|
||||
expr_ref finalAxiom(m.mk_ite(topLevelCond, then1, mk_not(m, expr)), m);
|
||||
SASSERT(finalAxiom);
|
||||
assert_axiom(finalAxiom);
|
||||
}
|
||||
|
@ -1167,7 +1167,7 @@ namespace smt {
|
|||
expr_ref_vector innerItems(m);
|
||||
innerItems.push_back(ctx.mk_eq_atom(expr->get_arg(1), mk_concat(ts0, ts1)));
|
||||
innerItems.push_back(ctx.mk_eq_atom(mk_strlen(ts1), mk_strlen(expr->get_arg(0))));
|
||||
innerItems.push_back(m.mk_ite(ctx.mk_eq_atom(ts1, expr->get_arg(0)), expr, m.mk_not(expr)));
|
||||
innerItems.push_back(m.mk_ite(ctx.mk_eq_atom(ts1, expr->get_arg(0)), expr, mk_not(m, expr)));
|
||||
expr_ref then1(m.mk_and(innerItems.size(), innerItems.c_ptr()), m);
|
||||
SASSERT(then1);
|
||||
|
||||
|
@ -1180,7 +1180,7 @@ namespace smt {
|
|||
, m);
|
||||
SASSERT(topLevelCond);
|
||||
|
||||
expr_ref finalAxiom(m.mk_ite(topLevelCond, then1, m.mk_not(expr)), m);
|
||||
expr_ref finalAxiom(m.mk_ite(topLevelCond, then1, mk_not(m, expr)), m);
|
||||
SASSERT(finalAxiom);
|
||||
assert_axiom(finalAxiom);
|
||||
}
|
||||
|
@ -1204,7 +1204,7 @@ namespace smt {
|
|||
if (haystackStr.contains(needleStr)) {
|
||||
assert_axiom(ex);
|
||||
} else {
|
||||
assert_axiom(m.mk_not(ex));
|
||||
assert_axiom(mk_not(m, ex));
|
||||
}
|
||||
return;
|
||||
}
|
||||
|
@ -1265,7 +1265,7 @@ namespace smt {
|
|||
SASSERT(tmpLen);
|
||||
thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x3, x4)));
|
||||
thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen));
|
||||
thenItems.push_back(m.mk_not(mk_contains(x3, expr->get_arg(1))));
|
||||
thenItems.push_back(mk_not(m, mk_contains(x3, expr->get_arg(1))));
|
||||
expr_ref thenBranch(m.mk_and(thenItems.size(), thenItems.c_ptr()), m);
|
||||
SASSERT(thenBranch);
|
||||
|
||||
|
@ -1341,7 +1341,7 @@ namespace smt {
|
|||
|
||||
expr_ref ite1(m.mk_ite(
|
||||
//m_autil.mk_lt(expr->get_arg(2), zeroAst),
|
||||
m.mk_not(m_autil.mk_ge(expr->get_arg(2), zeroAst)),
|
||||
mk_not(m, m_autil.mk_ge(expr->get_arg(2), zeroAst)),
|
||||
ctx.mk_eq_atom(resAst, mk_indexof(expr->get_arg(0), expr->get_arg(1))),
|
||||
ite2
|
||||
), m);
|
||||
|
@ -1384,7 +1384,7 @@ namespace smt {
|
|||
thenItems.push_back(m_autil.mk_ge(indexAst, mk_int(0)));
|
||||
// args[0] = x1 . args[1] . x2
|
||||
// x1 doesn't contain args[1]
|
||||
thenItems.push_back(m.mk_not(mk_contains(x2, expr->get_arg(1))));
|
||||
thenItems.push_back(mk_not(m, mk_contains(x2, expr->get_arg(1))));
|
||||
thenItems.push_back(ctx.mk_eq_atom(indexAst, mk_strlen(x1)));
|
||||
|
||||
bool canSkip = false;
|
||||
|
@ -1402,7 +1402,7 @@ namespace smt {
|
|||
expr_ref tmpLen(m_autil.mk_add(indexAst, mk_int(1)), m);
|
||||
thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x3, x4)));
|
||||
thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen));
|
||||
thenItems.push_back(m.mk_not(mk_contains(x4, expr->get_arg(1))));
|
||||
thenItems.push_back(mk_not(m, mk_contains(x4, expr->get_arg(1))));
|
||||
}
|
||||
//----------------------------
|
||||
// else branch
|
||||
|
@ -1452,7 +1452,7 @@ namespace smt {
|
|||
argumentsValid_terms.push_back(m_autil.mk_ge(substrPos, zero));
|
||||
// pos < strlen(base)
|
||||
// --> pos + -1*strlen(base) < 0
|
||||
argumentsValid_terms.push_back(m.mk_not(m_autil.mk_ge(
|
||||
argumentsValid_terms.push_back(mk_not(m, m_autil.mk_ge(
|
||||
m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)),
|
||||
zero)));
|
||||
|
||||
|
@ -1473,7 +1473,7 @@ namespace smt {
|
|||
|
||||
// Case 1: pos < 0 or pos >= strlen(base) or len < 0
|
||||
// ==> (Substr ...) = ""
|
||||
expr_ref case1_premise(m.mk_not(argumentsValid), m);
|
||||
expr_ref case1_premise(mk_not(m, argumentsValid), m);
|
||||
SASSERT(case1_premise);
|
||||
ctx.internalize(case1_premise, false);
|
||||
expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m);
|
||||
|
@ -1505,7 +1505,7 @@ namespace smt {
|
|||
case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen));
|
||||
case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3));
|
||||
expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m);
|
||||
expr_ref case3(rewrite_implication(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m);
|
||||
expr_ref case3(rewrite_implication(m.mk_and(argumentsValid, mk_not(m, lenOutOfBounds)), case3_conclusion), m);
|
||||
SASSERT(case3);
|
||||
|
||||
ctx.internalize(case1, false);
|
||||
|
@ -1548,7 +1548,7 @@ namespace smt {
|
|||
argumentsValid_terms.push_back(m_autil.mk_ge(substrPos, zero));
|
||||
// pos < strlen(base)
|
||||
// --> pos + -1*strlen(base) < 0
|
||||
argumentsValid_terms.push_back(m.mk_not(m_autil.mk_ge(
|
||||
argumentsValid_terms.push_back(mk_not(m, m_autil.mk_ge(
|
||||
m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)),
|
||||
zero)));
|
||||
// len >= 0
|
||||
|
@ -1564,7 +1564,7 @@ namespace smt {
|
|||
|
||||
// Case 1: pos < 0 or pos >= strlen(base) or len < 0
|
||||
// ==> (Substr ...) = ""
|
||||
expr_ref case1_premise(m.mk_not(argumentsValid), m);
|
||||
expr_ref case1_premise(mk_not(m, argumentsValid), m);
|
||||
expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m);
|
||||
expr_ref case1(m.mk_implies(case1_premise, case1_conclusion), m);
|
||||
|
||||
|
@ -1589,7 +1589,7 @@ namespace smt {
|
|||
case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen));
|
||||
case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3));
|
||||
expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m);
|
||||
expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m);
|
||||
expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, mk_not(m, lenOutOfBounds)), case3_conclusion), m);
|
||||
|
||||
assert_axiom(case1);
|
||||
assert_axiom(case2);
|
||||
|
@ -1630,7 +1630,7 @@ namespace smt {
|
|||
expr_ref tmpLen(m_autil.mk_add(i1, mk_strlen(expr->get_arg(1)), mk_int(-1)), m);
|
||||
thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x3, x4)));
|
||||
thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen));
|
||||
thenItems.push_back(m.mk_not(mk_contains(x3, expr->get_arg(1))));
|
||||
thenItems.push_back(mk_not(m, mk_contains(x3, expr->get_arg(1))));
|
||||
thenItems.push_back(ctx.mk_eq_atom(result, mk_concat(x1, mk_concat(expr->get_arg(2), x2))));
|
||||
// -----------------------
|
||||
// false branch
|
||||
|
@ -1684,7 +1684,7 @@ namespace smt {
|
|||
expr_ref tl(mk_str_var("tl"), m);
|
||||
expr_ref conclusion1(ctx.mk_eq_atom(S, mk_concat(hd, tl)), m);
|
||||
expr_ref conclusion2(ctx.mk_eq_atom(mk_strlen(hd), m_autil.mk_numeral(rational::one(), true)), m);
|
||||
expr_ref conclusion3(m.mk_not(ctx.mk_eq_atom(hd, mk_string("0"))), m);
|
||||
expr_ref conclusion3(mk_not(m, ctx.mk_eq_atom(hd, mk_string("0"))), m);
|
||||
expr_ref conclusion(m.mk_and(conclusion1, conclusion2, conclusion3), m);
|
||||
SASSERT(premise);
|
||||
SASSERT(conclusion);
|
||||
|
@ -1708,7 +1708,7 @@ namespace smt {
|
|||
// axiom 1: N < 0 <==> (str.from-int N) = ""
|
||||
expr * N = ex->get_arg(0);
|
||||
{
|
||||
expr_ref axiom1_lhs(m.mk_not(m_autil.mk_ge(N, m_autil.mk_numeral(rational::zero(), true))), m);
|
||||
expr_ref axiom1_lhs(mk_not(m, m_autil.mk_ge(N, m_autil.mk_numeral(rational::zero(), true))), m);
|
||||
expr_ref axiom1_rhs(ctx.mk_eq_atom(ex, mk_string("")), m);
|
||||
expr_ref axiom1(ctx.mk_eq_atom(axiom1_lhs, axiom1_rhs), m);
|
||||
SASSERT(axiom1);
|
||||
|
@ -1947,7 +1947,7 @@ namespace smt {
|
|||
// inconsistency check: value
|
||||
if (!can_two_nodes_eq(eqc_nn1, eqc_nn2)) {
|
||||
TRACE("str", tout << "inconsistency detected: " << mk_pp(eqc_nn1, m) << " cannot be equal to " << mk_pp(eqc_nn2, m) << std::endl;);
|
||||
expr_ref to_assert(m.mk_not(ctx.mk_eq_atom(eqc_nn1, eqc_nn2)), m);
|
||||
expr_ref to_assert(mk_not(m, ctx.mk_eq_atom(eqc_nn1, eqc_nn2)), m);
|
||||
assert_axiom(to_assert);
|
||||
// this shouldn't use the integer theory at all, so we don't allow the option of quick-return
|
||||
return false;
|
||||
|
@ -2160,7 +2160,7 @@ namespace smt {
|
|||
expr_ref implyR11(ctx.mk_eq_atom(mk_strlen(arg1), mk_int(makeUpLenArg1)), m);
|
||||
assert_implication(implyL11, implyR11);
|
||||
} else {
|
||||
expr_ref neg(m.mk_not(implyL11), m);
|
||||
expr_ref neg(mk_not(m, implyL11), m);
|
||||
assert_axiom(neg);
|
||||
}
|
||||
}
|
||||
|
@ -2231,7 +2231,7 @@ namespace smt {
|
|||
expr_ref implyR11(ctx.mk_eq_atom(mk_strlen(arg0), mk_int(makeUpLenArg0)), m);
|
||||
assert_implication(implyL11, implyR11);
|
||||
} else {
|
||||
expr_ref neg(m.mk_not(implyL11), m);
|
||||
expr_ref neg(mk_not(m, implyL11), m);
|
||||
assert_axiom(neg);
|
||||
}
|
||||
}
|
||||
|
@ -2762,7 +2762,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
if (!can_two_nodes_eq(new_nn1, new_nn2)) {
|
||||
expr_ref detected(m.mk_not(ctx.mk_eq_atom(new_nn1, new_nn2)), m);
|
||||
expr_ref detected(mk_not(m, ctx.mk_eq_atom(new_nn1, new_nn2)), m);
|
||||
TRACE("str", tout << "inconsistency detected: " << mk_ismt2_pp(detected, m) << std::endl;);
|
||||
assert_axiom(detected);
|
||||
return;
|
||||
|
@ -5008,7 +5008,7 @@ namespace smt {
|
|||
implyR = boolVar;
|
||||
} else {
|
||||
//implyR = Z3_mk_eq(ctx, boolVar, Z3_mk_false(ctx));
|
||||
implyR = m.mk_not(boolVar);
|
||||
implyR = mk_not(m, boolVar);
|
||||
}
|
||||
} else {
|
||||
// ------------------------------------------------------------------------------------------------
|
||||
|
@ -5037,7 +5037,7 @@ namespace smt {
|
|||
litems.push_back(ctx.mk_eq_atom(substrAst, aConcat));
|
||||
}
|
||||
//implyR = Z3_mk_eq(ctx, boolVar, Z3_mk_false(ctx));
|
||||
implyR = m.mk_not(boolVar);
|
||||
implyR = mk_not(m, boolVar);
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
@ -5076,7 +5076,7 @@ namespace smt {
|
|||
implyR = boolVar;
|
||||
} else {
|
||||
// implyR = Z3_mk_eq(ctx, boolVar, Z3_mk_false(ctx));
|
||||
implyR = m.mk_not(boolVar);
|
||||
implyR = mk_not(m, boolVar);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -5146,7 +5146,7 @@ namespace smt {
|
|||
litems.push_back(ctx.mk_eq_atom(substrAst, aConcat));
|
||||
}
|
||||
expr_ref implyLHS(mk_and(litems), m);
|
||||
expr_ref implyR(m.mk_not(boolVar), m);
|
||||
expr_ref implyR(mk_not(m, boolVar), m);
|
||||
assert_implication(implyLHS, implyR);
|
||||
break;
|
||||
}
|
||||
|
@ -6515,7 +6515,7 @@ namespace smt {
|
|||
if (matchRes) {
|
||||
assert_implication(implyL, boolVar);
|
||||
} else {
|
||||
assert_implication(implyL, m.mk_not(boolVar));
|
||||
assert_implication(implyL, mk_not(m, boolVar));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -6603,7 +6603,7 @@ namespace smt {
|
|||
<< arg1_str << "\" + \"" << arg2_str <<
|
||||
"\" != \"" << const_str << "\"" << "\n";);
|
||||
expr_ref equality(ctx.mk_eq_atom(concat, str), m);
|
||||
expr_ref diseq(m.mk_not(equality), m);
|
||||
expr_ref diseq(mk_not(m, equality), m);
|
||||
assert_axiom(diseq);
|
||||
return;
|
||||
}
|
||||
|
@ -6621,7 +6621,7 @@ namespace smt {
|
|||
"\" is longer than \"" << const_str << "\","
|
||||
<< " so cannot be concatenated with anything to form it" << "\n";);
|
||||
expr_ref equality(ctx.mk_eq_atom(newConcat, str), m);
|
||||
expr_ref diseq(m.mk_not(equality), m);
|
||||
expr_ref diseq(mk_not(m, equality), m);
|
||||
assert_axiom(diseq);
|
||||
return;
|
||||
} else {
|
||||
|
@ -6635,7 +6635,7 @@ namespace smt {
|
|||
<< "actually \"" << arg2_str << "\""
|
||||
<< "\n";);
|
||||
expr_ref equality(ctx.mk_eq_atom(newConcat, str), m);
|
||||
expr_ref diseq(m.mk_not(equality), m);
|
||||
expr_ref diseq(mk_not(m, equality), m);
|
||||
assert_axiom(diseq);
|
||||
return;
|
||||
} else {
|
||||
|
|
|
@ -6,6 +6,7 @@ z3_add_component(solver
|
|||
smt_logics.cpp
|
||||
solver.cpp
|
||||
solver_na2as.cpp
|
||||
solver_pool.cpp
|
||||
solver2tactic.cpp
|
||||
tactic2solver.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
|
|
|
@ -147,6 +147,7 @@ public:
|
|||
}
|
||||
|
||||
virtual void updt_params(params_ref const & p) {
|
||||
solver::updt_params(p);
|
||||
m_solver1->updt_params(p);
|
||||
m_solver2->updt_params(p);
|
||||
updt_local_params(p);
|
||||
|
@ -280,8 +281,8 @@ public:
|
|||
return m_solver2->get_assumption(idx - c1);
|
||||
}
|
||||
|
||||
virtual std::ostream& display(std::ostream & out) const {
|
||||
return m_solver1->display(out);
|
||||
virtual std::ostream& display(std::ostream & out, unsigned n, expr* const* es) const {
|
||||
return m_solver1->display(out, n, es);
|
||||
}
|
||||
|
||||
virtual void collect_statistics(statistics & st) const {
|
||||
|
|
|
@ -34,11 +34,12 @@ expr * solver::get_assertion(unsigned idx) const {
|
|||
return 0;
|
||||
}
|
||||
|
||||
std::ostream& solver::display(std::ostream & out) const {
|
||||
std::ostream& solver::display(std::ostream & out, unsigned n, expr* const* assumptions) const {
|
||||
expr_ref_vector fmls(get_manager());
|
||||
get_assertions(fmls);
|
||||
ast_pp_util visitor(get_manager());
|
||||
visitor.collect(fmls);
|
||||
visitor.collect(n, assumptions);
|
||||
visitor.display_decls(out);
|
||||
visitor.display_asserts(out, fmls, true);
|
||||
return out;
|
||||
|
|
|
@ -43,6 +43,7 @@ public:
|
|||
- results based on check_sat_result API
|
||||
*/
|
||||
class solver : public check_sat_result {
|
||||
params_ref m_params;
|
||||
public:
|
||||
virtual ~solver() {}
|
||||
|
||||
|
@ -54,7 +55,12 @@ public:
|
|||
/**
|
||||
\brief Update the solver internal settings.
|
||||
*/
|
||||
virtual void updt_params(params_ref const & p) { }
|
||||
virtual void updt_params(params_ref const & p) { m_params.copy(p); }
|
||||
|
||||
/**
|
||||
\brief Retrieve set of parameters set on solver.
|
||||
*/
|
||||
virtual params_ref const& get_params() { return m_params; }
|
||||
|
||||
/**
|
||||
\brief Store in \c r a description of the configuration
|
||||
|
@ -175,7 +181,7 @@ public:
|
|||
/**
|
||||
\brief Display the content of this solver.
|
||||
*/
|
||||
virtual std::ostream& display(std::ostream & out) const;
|
||||
virtual std::ostream& display(std::ostream & out, unsigned n = 0, expr* const* assumptions = nullptr) const;
|
||||
|
||||
class scoped_push {
|
||||
solver& s;
|
||||
|
|
320
src/solver/solver_pool.cpp
Normal file
320
src/solver/solver_pool.cpp
Normal file
|
@ -0,0 +1,320 @@
|
|||
/**
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
solver_pool.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Maintain a pool of solvers
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
|
||||
#include "solver/solver_pool.h"
|
||||
#include "solver/solver_na2as.h"
|
||||
#include "ast/proofs/proof_utils.h"
|
||||
#include "ast/ast_util.h"
|
||||
|
||||
class pool_solver : public solver_na2as {
|
||||
solver_pool& m_pool;
|
||||
app_ref m_pred;
|
||||
proof_ref m_proof;
|
||||
ref<solver> m_base;
|
||||
expr_ref_vector m_assertions;
|
||||
unsigned m_head;
|
||||
expr_ref_vector m_flat;
|
||||
bool m_pushed;
|
||||
bool m_in_delayed_scope;
|
||||
unsigned m_dump_counter;
|
||||
|
||||
bool is_virtual() const { return !m.is_true(m_pred); }
|
||||
public:
|
||||
pool_solver(solver* b, solver_pool& pool, app_ref& pred):
|
||||
solver_na2as(pred.get_manager()),
|
||||
m_pool(pool),
|
||||
m_pred(pred),
|
||||
m_proof(m),
|
||||
m_base(b),
|
||||
m_assertions(m),
|
||||
m_head(0),
|
||||
m_flat(m),
|
||||
m_pushed(false),
|
||||
m_in_delayed_scope(false),
|
||||
m_dump_counter(0) {
|
||||
if (is_virtual()) {
|
||||
solver_na2as::assert_expr(m.mk_true(), pred);
|
||||
}
|
||||
}
|
||||
|
||||
virtual ~pool_solver() {
|
||||
if (m_pushed) pop(get_scope_level());
|
||||
if (is_virtual()) {
|
||||
m_pred = m.mk_not(m_pred);
|
||||
m_base->assert_expr(m_pred);
|
||||
}
|
||||
}
|
||||
|
||||
solver* base_solver() { return m_base.get(); }
|
||||
|
||||
virtual solver* translate(ast_manager& m, params_ref const& p) { UNREACHABLE(); return nullptr; }
|
||||
virtual void updt_params(params_ref const& p) { solver::updt_params(p); m_base->updt_params(p); }
|
||||
virtual void collect_param_descrs(param_descrs & r) { m_base->collect_param_descrs(r); }
|
||||
virtual void collect_statistics(statistics & st) const { m_base->collect_statistics(st); }
|
||||
|
||||
virtual void get_unsat_core(ptr_vector<expr> & r) {
|
||||
m_base->get_unsat_core(r);
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < r.size(); ++i)
|
||||
if (m_pred != r[i])
|
||||
r[j++] = r[i];
|
||||
r.shrink(j);
|
||||
}
|
||||
|
||||
virtual unsigned get_num_assumptions() const {
|
||||
unsigned sz = solver_na2as::get_num_assumptions();
|
||||
return is_virtual() ? sz - 1 : sz;
|
||||
}
|
||||
|
||||
virtual proof * get_proof() {
|
||||
scoped_watch _t_(m_pool.m_proof_watch);
|
||||
if (!m_proof.get()) {
|
||||
elim_aux_assertions pc(m_pred);
|
||||
m_proof = m_base->get_proof();
|
||||
pc(m, m_proof, m_proof);
|
||||
}
|
||||
return m_proof;
|
||||
}
|
||||
|
||||
void internalize_assertions() {
|
||||
SASSERT(!m_pushed || m_head == m_assertions.size());
|
||||
for (unsigned sz = m_assertions.size(); m_head < sz; ++m_head) {
|
||||
expr_ref f(m);
|
||||
f = m.mk_implies(m_pred, (m_assertions.get(m_head)));
|
||||
m_base->assert_expr(f);
|
||||
}
|
||||
}
|
||||
|
||||
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
|
||||
SASSERT(!m_pushed || get_scope_level() > 0);
|
||||
m_proof.reset();
|
||||
scoped_watch _t_(m_pool.m_check_watch);
|
||||
m_pool.m_stats.m_num_checks++;
|
||||
|
||||
stopwatch sw;
|
||||
sw.start();
|
||||
internalize_assertions();
|
||||
lbool res = m_base->check_sat(num_assumptions, assumptions);
|
||||
sw.stop();
|
||||
switch (res) {
|
||||
case l_true:
|
||||
m_pool.m_check_sat_watch.add(sw);
|
||||
m_pool.m_stats.m_num_sat_checks++;
|
||||
break;
|
||||
case l_undef:
|
||||
m_pool.m_check_undef_watch.add(sw);
|
||||
m_pool.m_stats.m_num_undef_checks++;
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
set_status(res);
|
||||
|
||||
if (false /*m_dump_benchmarks && sw.get_seconds() >= m_pool.fparams().m_dump_min_time*/) {
|
||||
std::stringstream file_name;
|
||||
file_name << "virt_solver";
|
||||
if (is_virtual()) { file_name << "_" << m_pred->get_decl()->get_name(); }
|
||||
file_name << "_" << (m_dump_counter++) << ".smt2";
|
||||
|
||||
std::ofstream out(file_name.str().c_str());
|
||||
if (!out) { verbose_stream() << "could not open file " << file_name.str() << " for output\n"; }
|
||||
|
||||
out << "(set-info :status ";
|
||||
switch (res) {
|
||||
case l_true: out << "sat"; break;
|
||||
case l_false: out << "unsat"; break;
|
||||
case l_undef: out << "unknown"; break;
|
||||
}
|
||||
out << ")\n";
|
||||
m_base->display(out, num_assumptions, assumptions);
|
||||
bool first = true;
|
||||
out << "(check-sat";
|
||||
for (unsigned i = 0; i < num_assumptions; ++i) {
|
||||
out << " " << mk_pp(assumptions[i], m);
|
||||
}
|
||||
out << ")";
|
||||
out << "(exit)\n";
|
||||
::statistics st;
|
||||
m_base->collect_statistics(st);
|
||||
st.update("time", sw.get_seconds());
|
||||
st.display_smt2(out);
|
||||
out.close();
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
virtual void push_core() {
|
||||
SASSERT(!m_pushed || get_scope_level() > 0);
|
||||
if (m_in_delayed_scope) {
|
||||
// second push
|
||||
internalize_assertions();
|
||||
m_base->push();
|
||||
m_pushed = true;
|
||||
m_in_delayed_scope = false;
|
||||
}
|
||||
|
||||
if (!m_pushed) {
|
||||
m_in_delayed_scope = true;
|
||||
}
|
||||
else {
|
||||
SASSERT(m_pushed);
|
||||
SASSERT(!m_in_delayed_scope);
|
||||
m_base->push();
|
||||
}
|
||||
}
|
||||
|
||||
virtual void pop_core(unsigned n) {
|
||||
SASSERT(!m_pushed || get_scope_level() > 0);
|
||||
if (m_pushed) {
|
||||
SASSERT(!m_in_delayed_scope);
|
||||
m_base->pop(n);
|
||||
m_pushed = get_scope_level() - n > 0;
|
||||
}
|
||||
else {
|
||||
m_in_delayed_scope = get_scope_level() - n > 0;
|
||||
}
|
||||
}
|
||||
|
||||
virtual void assert_expr(expr * e) {
|
||||
SASSERT(!m_pushed || get_scope_level() > 0);
|
||||
if (m.is_true(e)) return;
|
||||
if (m_in_delayed_scope) {
|
||||
internalize_assertions();
|
||||
m_base->push();
|
||||
m_pushed = true;
|
||||
m_in_delayed_scope = false;
|
||||
}
|
||||
|
||||
if (m_pushed) {
|
||||
m_base->assert_expr(e);
|
||||
}
|
||||
else {
|
||||
m_flat.push_back(e);
|
||||
flatten_and(m_flat);
|
||||
m_assertions.append(m_flat);
|
||||
m_flat.reset();
|
||||
}
|
||||
}
|
||||
|
||||
virtual void get_model(model_ref & _m) { m_base->get_model(_m); }
|
||||
|
||||
virtual expr * get_assumption(unsigned idx) const {
|
||||
return solver_na2as::get_assumption(idx + is_virtual());
|
||||
}
|
||||
|
||||
virtual std::string reason_unknown() const { return m_base->reason_unknown(); }
|
||||
virtual void set_reason_unknown(char const* msg) { return m_base->set_reason_unknown(msg); }
|
||||
virtual void get_labels(svector<symbol> & r) { return m_base->get_labels(r); }
|
||||
virtual void set_progress_callback(progress_callback * callback) { m_base->set_progress_callback(callback); }
|
||||
|
||||
virtual ast_manager& get_manager() const { return m_base->get_manager(); }
|
||||
|
||||
void refresh(solver* new_base) {
|
||||
SASSERT(!m_pushed);
|
||||
m_head = 0;
|
||||
m_base = new_base;
|
||||
}
|
||||
|
||||
void reset() {
|
||||
SASSERT(!m_pushed);
|
||||
m_head = 0;
|
||||
m_assertions.reset();
|
||||
m_pool.refresh(m_base.get());
|
||||
}
|
||||
};
|
||||
|
||||
solver_pool::solver_pool(solver* base_solver, unsigned num_solvers_per_pool):
|
||||
m_base_solver(base_solver),
|
||||
m_num_solvers_per_pool(num_solvers_per_pool),
|
||||
m_num_solvers_in_last_pool(0)
|
||||
{}
|
||||
|
||||
|
||||
ptr_vector<solver> solver_pool::get_base_solvers() const {
|
||||
ptr_vector<solver> solvers;
|
||||
for (solver* s0 : m_solvers) {
|
||||
pool_solver* s = dynamic_cast<pool_solver*>(s0);
|
||||
if (!solvers.contains(s->base_solver())) {
|
||||
solvers.push_back(s->base_solver());
|
||||
}
|
||||
}
|
||||
return solvers;
|
||||
}
|
||||
|
||||
void solver_pool::collect_statistics(statistics &st) const {
|
||||
ptr_vector<solver> solvers = get_base_solvers();
|
||||
for (solver* s : solvers) s->collect_statistics(st);
|
||||
st.update("time.pool_solver.smt.total", m_check_watch.get_seconds());
|
||||
st.update("time.pool_solver.smt.total.sat", m_check_sat_watch.get_seconds());
|
||||
st.update("time.pool_solver.smt.total.undef", m_check_undef_watch.get_seconds());
|
||||
st.update("time.pool_solver.proof", m_proof_watch.get_seconds());
|
||||
st.update("pool_solver.checks", m_stats.m_num_checks);
|
||||
st.update("pool_solver.checks.sat", m_stats.m_num_sat_checks);
|
||||
st.update("pool_solver.checks.undef", m_stats.m_num_undef_checks);
|
||||
}
|
||||
|
||||
void solver_pool::reset_statistics() {
|
||||
#if 0
|
||||
ptr_vector<solver> solvers = get_base_solvers();
|
||||
for (solver* s : solvers) {
|
||||
s->reset_statistics();
|
||||
}
|
||||
#endif
|
||||
m_stats.reset();
|
||||
m_check_sat_watch.reset();
|
||||
m_check_undef_watch.reset();
|
||||
m_check_watch.reset();
|
||||
m_proof_watch.reset();
|
||||
}
|
||||
|
||||
solver* solver_pool::mk_solver() {
|
||||
ref<solver> base_solver;
|
||||
ast_manager& m = m_base_solver->get_manager();
|
||||
if (m_solvers.empty() || m_num_solvers_in_last_pool == m_num_solvers_per_pool) {
|
||||
base_solver = m_base_solver->translate(m, m_base_solver->get_params());
|
||||
m_num_solvers_in_last_pool = 0;
|
||||
}
|
||||
else {
|
||||
base_solver = dynamic_cast<pool_solver*>(m_solvers.back())->base_solver();
|
||||
}
|
||||
m_num_solvers_in_last_pool++;
|
||||
std::stringstream name;
|
||||
name << "vsolver#" << m_solvers.size();
|
||||
app_ref pred(m.mk_const(symbol(name.str().c_str()), m.mk_bool_sort()), m);
|
||||
pool_solver* solver = alloc(pool_solver, base_solver.get(), *this, pred);
|
||||
m_solvers.push_back(solver);
|
||||
return solver;
|
||||
}
|
||||
|
||||
void solver_pool::reset_solver(solver* s) {
|
||||
pool_solver* ps = dynamic_cast<pool_solver*>(s);
|
||||
SASSERT(ps);
|
||||
if (ps) ps->reset();
|
||||
}
|
||||
|
||||
void solver_pool::refresh(solver* base_solver) {
|
||||
ast_manager& m = m_base_solver->get_manager();
|
||||
ref<solver> new_base = m_base_solver->translate(m, m_base_solver->get_params());
|
||||
for (solver* s0 : m_solvers) {
|
||||
pool_solver* s = dynamic_cast<pool_solver*>(s0);
|
||||
if (base_solver == s->base_solver()) {
|
||||
s->refresh(new_base.get());
|
||||
}
|
||||
}
|
||||
}
|
69
src/solver/solver_pool.h
Normal file
69
src/solver/solver_pool.h
Normal file
|
@ -0,0 +1,69 @@
|
|||
/**
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
solver_pool.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Maintain a pool of solvers
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner
|
||||
Arie Gurfinkel
|
||||
|
||||
Notes:
|
||||
|
||||
This is a revision of spacer_virtual_solver by Arie Gurfinkel
|
||||
|
||||
--*/
|
||||
#ifndef SOLVER_POOL_H_
|
||||
#define SOLVER_POOL_H_
|
||||
|
||||
#include "solver/solver.h"
|
||||
#include "util/stopwatch.h"
|
||||
|
||||
class pool_solver;
|
||||
|
||||
class solver_pool {
|
||||
|
||||
friend class pool_solver;
|
||||
|
||||
struct stats {
|
||||
unsigned m_num_checks;
|
||||
unsigned m_num_sat_checks;
|
||||
unsigned m_num_undef_checks;
|
||||
stats() { reset(); }
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
};
|
||||
|
||||
ref<solver> m_base_solver;
|
||||
unsigned m_num_solvers_per_pool;
|
||||
unsigned m_num_solvers_in_last_pool;
|
||||
sref_vector<solver> m_solvers;
|
||||
stats m_stats;
|
||||
|
||||
stopwatch m_check_watch;
|
||||
stopwatch m_check_sat_watch;
|
||||
stopwatch m_check_undef_watch;
|
||||
stopwatch m_proof_watch;
|
||||
|
||||
void refresh(solver* s);
|
||||
|
||||
ptr_vector<solver> get_base_solvers() const;
|
||||
|
||||
public:
|
||||
solver_pool(solver* base_solver, unsigned num_solvers_per_pool);
|
||||
|
||||
void collect_statistics(statistics &st) const;
|
||||
void reset_statistics();
|
||||
|
||||
solver* mk_solver();
|
||||
|
||||
void reset_solver(solver* s);
|
||||
};
|
||||
|
||||
|
||||
#endif
|
|
@ -37,7 +37,6 @@ class tactic2solver : public solver_na2as {
|
|||
ref<simple_check_sat_result> m_result;
|
||||
tactic_ref m_tactic;
|
||||
symbol m_logic;
|
||||
params_ref m_params;
|
||||
bool m_produce_models;
|
||||
bool m_produce_proofs;
|
||||
bool m_produce_unsat_cores;
|
||||
|
@ -85,7 +84,7 @@ tactic2solver::tactic2solver(ast_manager & m, tactic * t, params_ref const & p,
|
|||
|
||||
m_tactic = t;
|
||||
m_logic = logic;
|
||||
m_params = p;
|
||||
solver::updt_params(p);
|
||||
|
||||
m_produce_models = produce_models;
|
||||
m_produce_proofs = produce_proofs;
|
||||
|
@ -96,7 +95,7 @@ tactic2solver::~tactic2solver() {
|
|||
}
|
||||
|
||||
void tactic2solver::updt_params(params_ref const & p) {
|
||||
m_params.append(p);
|
||||
solver::updt_params(p);
|
||||
}
|
||||
|
||||
void tactic2solver::collect_param_descrs(param_descrs & r) {
|
||||
|
@ -129,7 +128,7 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
|
|||
m_result = alloc(simple_check_sat_result, m);
|
||||
m_tactic->cleanup();
|
||||
m_tactic->set_logic(m_logic);
|
||||
m_tactic->updt_params(m_params); // parameters are allowed to overwrite logic.
|
||||
m_tactic->updt_params(get_params()); // parameters are allowed to overwrite logic.
|
||||
goal_ref g = alloc(goal, m, m_produce_proofs, m_produce_models, m_produce_unsat_cores);
|
||||
|
||||
unsigned sz = m_assertions.size();
|
||||
|
|
|
@ -441,7 +441,7 @@ ptr_vector<expr> const & dom_simplify_tactic::tree(expr * e) {
|
|||
}
|
||||
|
||||
|
||||
// ----------------------
|
||||
// ---------------------
|
||||
// expr_substitution_simplifier
|
||||
|
||||
bool expr_substitution_simplifier::assert_expr(expr * t, bool sign) {
|
||||
|
|
|
@ -95,7 +95,6 @@ class dom_simplify_tactic : public tactic {
|
|||
expr_ref_vector m_trail, m_args;
|
||||
obj_map<expr, expr*> m_result;
|
||||
expr_dominators m_dominators;
|
||||
unsigned m_scope_level;
|
||||
unsigned m_depth;
|
||||
unsigned m_max_depth;
|
||||
ptr_vector<expr> m_empty;
|
||||
|
@ -128,8 +127,7 @@ public:
|
|||
dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()):
|
||||
m(m), m_simplifier(s), m_params(p),
|
||||
m_trail(m), m_args(m),
|
||||
m_dominators(m),
|
||||
m_scope_level(0), m_depth(0), m_max_depth(1024), m_forward(true) {}
|
||||
m_dominators(m), m_depth(0), m_max_depth(1024), m_forward(true) {}
|
||||
|
||||
|
||||
virtual ~dom_simplify_tactic();
|
||||
|
|
|
@ -33,7 +33,6 @@ Notes:
|
|||
|
||||
class bounded_int2bv_solver : public solver_na2as {
|
||||
ast_manager& m;
|
||||
params_ref m_params;
|
||||
mutable bv_util m_bv;
|
||||
mutable arith_util m_arith;
|
||||
mutable expr_ref_vector m_assertions;
|
||||
|
@ -53,7 +52,6 @@ public:
|
|||
bounded_int2bv_solver(ast_manager& m, params_ref const& p, solver* s):
|
||||
solver_na2as(m),
|
||||
m(m),
|
||||
m_params(p),
|
||||
m_bv(m),
|
||||
m_arith(m),
|
||||
m_assertions(m),
|
||||
|
@ -63,6 +61,7 @@ public:
|
|||
m_rewriter_ctx(m, p),
|
||||
m_rewriter(m, m_rewriter_ctx)
|
||||
{
|
||||
solver::updt_params(p);
|
||||
m_bounds.push_back(alloc(bound_manager, m));
|
||||
}
|
||||
|
||||
|
@ -131,7 +130,7 @@ public:
|
|||
return m_solver->check_sat(num_assumptions, assumptions);
|
||||
}
|
||||
|
||||
virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); }
|
||||
virtual void updt_params(params_ref const & p) { solver::updt_params(p); m_solver->updt_params(p); }
|
||||
virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }
|
||||
virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
|
||||
virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); }
|
||||
|
|
|
@ -33,7 +33,6 @@ Notes:
|
|||
|
||||
class enum2bv_solver : public solver_na2as {
|
||||
ast_manager& m;
|
||||
params_ref m_params;
|
||||
ref<solver> m_solver;
|
||||
enum2bv_rewriter m_rewriter;
|
||||
|
||||
|
@ -42,10 +41,10 @@ public:
|
|||
enum2bv_solver(ast_manager& m, params_ref const& p, solver* s):
|
||||
solver_na2as(m),
|
||||
m(m),
|
||||
m_params(p),
|
||||
m_solver(s),
|
||||
m_rewriter(m, p)
|
||||
{
|
||||
solver::updt_params(p);
|
||||
}
|
||||
|
||||
virtual ~enum2bv_solver() {}
|
||||
|
@ -78,7 +77,7 @@ public:
|
|||
return m_solver->check_sat(num_assumptions, assumptions);
|
||||
}
|
||||
|
||||
virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); }
|
||||
virtual void updt_params(params_ref const & p) { solver::updt_params(p); m_solver->updt_params(p); }
|
||||
virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }
|
||||
virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
|
||||
virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); }
|
||||
|
|
|
@ -26,7 +26,6 @@ Notes:
|
|||
|
||||
class pb2bv_solver : public solver_na2as {
|
||||
ast_manager& m;
|
||||
params_ref m_params;
|
||||
mutable expr_ref_vector m_assertions;
|
||||
mutable ref<solver> m_solver;
|
||||
mutable pb2bv_rewriter m_rewriter;
|
||||
|
@ -36,11 +35,11 @@ public:
|
|||
pb2bv_solver(ast_manager& m, params_ref const& p, solver* s):
|
||||
solver_na2as(m),
|
||||
m(m),
|
||||
m_params(p),
|
||||
m_assertions(m),
|
||||
m_solver(s),
|
||||
m_rewriter(m, p)
|
||||
{
|
||||
solver::updt_params(p);
|
||||
}
|
||||
|
||||
virtual ~pb2bv_solver() {}
|
||||
|
@ -70,7 +69,7 @@ public:
|
|||
return m_solver->check_sat(num_assumptions, assumptions);
|
||||
}
|
||||
|
||||
virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); }
|
||||
virtual void updt_params(params_ref const & p) { solver::updt_params(p); m_solver->updt_params(p); }
|
||||
virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); }
|
||||
virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); }
|
||||
virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); }
|
||||
|
|
|
@ -4,11 +4,11 @@ Copyright (c) 2015 Microsoft Corporation
|
|||
|
||||
--*/
|
||||
|
||||
#include "ast/proof_checker/proof_checker.h"
|
||||
#include "ast/proofs/proof_checker.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
|
||||
void tst_checker1() {
|
||||
ast_manager m(PGM_FINE);
|
||||
ast_manager m(PGM_ENABLED);
|
||||
expr_ref a(m);
|
||||
proof_ref p1(m), p2(m), p3(m), p4(m);
|
||||
expr_ref_vector side_conditions(m);
|
||||
|
|
|
@ -28,6 +28,7 @@ z3_add_component(util
|
|||
lbool.cpp
|
||||
luby.cpp
|
||||
memory_manager.cpp
|
||||
min_cut.cpp
|
||||
mpbq.cpp
|
||||
mpf.cpp
|
||||
mpff.cpp
|
||||
|
|
122
src/util/container_util.h
Normal file
122
src/util/container_util.h
Normal file
|
@ -0,0 +1,122 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
container_util.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Useful functions for containers
|
||||
|
||||
Author:
|
||||
|
||||
Krystof Hoder, Nikolaj Bjorner 2017-10-24
|
||||
|
||||
Revision History:
|
||||
|
||||
Extracted from dl_util.h
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef CONTAINER_UTIL_H_
|
||||
#define CONTAINER_UTIL_H_
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
// container functions
|
||||
//
|
||||
// -----------------------------------
|
||||
|
||||
template<class Set1, class Set2>
|
||||
void set_intersection(Set1 & tgt, const Set2 & src) {
|
||||
svector<typename Set1::data> to_remove;
|
||||
for (auto const& itm : tgt)
|
||||
if (!src.contains(itm))
|
||||
to_remove.push_back(itm);
|
||||
while (!to_remove.empty()) {
|
||||
tgt.remove(to_remove.back());
|
||||
to_remove.pop_back();
|
||||
}
|
||||
}
|
||||
|
||||
template<class Set>
|
||||
void set_difference(Set & tgt, const Set & to_remove) {
|
||||
for (auto const& itm : to_remove)
|
||||
tgt.remove(itm);
|
||||
}
|
||||
|
||||
template<class Set1, class Set2>
|
||||
void set_union(Set1 & tgt, const Set2 & to_add) {
|
||||
for (auto const& itm : to_add)
|
||||
tgt.insert(itm);
|
||||
}
|
||||
|
||||
template<class T>
|
||||
void unite_disjoint_maps(T & tgt, const T & src) {
|
||||
for (auto const& kv : src) {
|
||||
SASSERT(!tgt.contains(kv.m_key));
|
||||
tgt.insert(kv.m_key, kv.m_value);
|
||||
}
|
||||
}
|
||||
|
||||
template<class T, class U>
|
||||
void collect_map_range(T & acc, const U & map) {
|
||||
for (auto const& kv : map)
|
||||
acc.push_back(kv.m_value);
|
||||
}
|
||||
|
||||
|
||||
template<class T>
|
||||
void print_container(const T & begin, const T & end, std::ostream & out) {
|
||||
T it = begin;
|
||||
out << "(";
|
||||
bool first = true;
|
||||
for(; it!=end; ++it) {
|
||||
if(first) { first = false; } else { out << ","; }
|
||||
out << (*it);
|
||||
}
|
||||
out << ")";
|
||||
}
|
||||
|
||||
template<class T>
|
||||
void print_container(const T & cont, std::ostream & out) {
|
||||
print_container(cont.begin(), cont.end(), out);
|
||||
}
|
||||
|
||||
template<class T, class M>
|
||||
void print_container(const ref_vector<T,M> & cont, std::ostream & out) {
|
||||
print_container(cont.c_ptr(), cont.c_ptr() + cont.size(), out);
|
||||
}
|
||||
|
||||
template<class T>
|
||||
void print_map(const T & cont, std::ostream & out) {
|
||||
out << "(";
|
||||
bool first = true;
|
||||
for (auto const& kv : cont) {
|
||||
if (first) { first = false; } else { out << ","; }
|
||||
out << kv.m_key << "->" << kv.m_value;
|
||||
}
|
||||
out << ")";
|
||||
}
|
||||
|
||||
template<class It, class V>
|
||||
unsigned find_index(const It & begin, const It & end, const V & val) {
|
||||
It it = begin;
|
||||
for (unsigned idx = 0; it != end; it++, idx++) {
|
||||
if (*it == val) {
|
||||
return idx;
|
||||
}
|
||||
}
|
||||
return UINT_MAX;
|
||||
}
|
||||
|
||||
template<class T, class U>
|
||||
bool containers_equal(const T & begin1, const T & end1, const U & begin2, const U & end2) {
|
||||
T it1 = begin1;
|
||||
U it2 = begin2;
|
||||
for (; it1 != end1 && it2 != end2 && *it1 == *it2; ++it1, ++it2) {};
|
||||
return it1 == end1 && it2 == end2;
|
||||
}
|
||||
|
||||
#endif
|
232
src/util/min_cut.cpp
Normal file
232
src/util/min_cut.cpp
Normal file
|
@ -0,0 +1,232 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Arie Gurfinkel
|
||||
|
||||
Module Name:
|
||||
|
||||
min_cut.cpp
|
||||
|
||||
Abstract:
|
||||
min cut solver
|
||||
|
||||
Author:
|
||||
Bernhard Gleiss
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
#include "util/min_cut.h"
|
||||
#include "util/trace.h"
|
||||
|
||||
min_cut::min_cut() {
|
||||
// push back two empty vectors for source and sink
|
||||
m_edges.push_back(edge_vector());
|
||||
m_edges.push_back(edge_vector());
|
||||
}
|
||||
|
||||
unsigned min_cut::new_node() {
|
||||
m_edges.push_back(edge_vector());
|
||||
return m_edges.size() - 1;
|
||||
}
|
||||
|
||||
void min_cut::add_edge(unsigned int i, unsigned int j, unsigned capacity) {
|
||||
m_edges.reserve(i + 1);
|
||||
m_edges[i].push_back(edge(j, capacity));
|
||||
TRACE("spacer.mincut", tout << "adding edge (" << i << "," << j << ")\n";);
|
||||
}
|
||||
|
||||
void min_cut::compute_min_cut(unsigned_vector& cut_nodes) {
|
||||
if (m_edges.size() == 2) {
|
||||
return;
|
||||
}
|
||||
|
||||
m_d.resize(m_edges.size());
|
||||
m_pred.resize(m_edges.size());
|
||||
|
||||
// compute initial distances and number of nodes
|
||||
compute_initial_distances();
|
||||
|
||||
unsigned i = 0;
|
||||
|
||||
while (m_d[0] < m_edges.size()) {
|
||||
unsigned j = get_admissible_edge(i);
|
||||
|
||||
if (j < m_edges.size()) {
|
||||
// advance(i)
|
||||
m_pred[j] = i;
|
||||
i = j;
|
||||
|
||||
// if i is the sink, augment path
|
||||
if (i == 1) {
|
||||
augment_path();
|
||||
i = 0;
|
||||
}
|
||||
}
|
||||
else {
|
||||
// retreat
|
||||
compute_distance(i);
|
||||
if (i != 0) {
|
||||
i = m_pred[i];
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// split nodes into reachable and unreachable ones
|
||||
bool_vector reachable(m_edges.size());
|
||||
compute_reachable_nodes(reachable);
|
||||
|
||||
// find all edges between reachable and unreachable nodes and
|
||||
// for each such edge, add corresponding lemma to unsat-core
|
||||
compute_cut_and_add_lemmas(reachable, cut_nodes);
|
||||
}
|
||||
|
||||
void min_cut::compute_initial_distances() {
|
||||
unsigned_vector todo;
|
||||
bool_vector visited(m_edges.size());
|
||||
|
||||
todo.push_back(0); // start at the source, since we do postorder traversel
|
||||
|
||||
while (!todo.empty()) {
|
||||
unsigned current = todo.back();
|
||||
|
||||
// if we haven't already visited current
|
||||
if (!visited[current]) {
|
||||
bool exists_unvisited_parent = false;
|
||||
|
||||
// add unprocessed parents to stack for DFS. If there is at least
|
||||
// one unprocessed parent, don't compute the result
|
||||
// for current now, but wait until those unprocessed parents are processed
|
||||
for (auto const& edge : m_edges[current]) {
|
||||
unsigned parent = edge.node;
|
||||
|
||||
// if we haven't visited the current parent yet
|
||||
if (!visited[parent]) {
|
||||
// add it to the stack
|
||||
todo.push_back(parent);
|
||||
exists_unvisited_parent = true;
|
||||
}
|
||||
}
|
||||
|
||||
// if we already visited all parents, we can visit current too
|
||||
if (!exists_unvisited_parent) {
|
||||
visited[current] = true;
|
||||
todo.pop_back();
|
||||
|
||||
compute_distance(current); // I.H. all parent distances are already computed
|
||||
}
|
||||
}
|
||||
else {
|
||||
todo.pop_back();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
unsigned min_cut::get_admissible_edge(unsigned i) {
|
||||
for (const auto& edge : m_edges[i]) {
|
||||
if (edge.weight > 0 && m_d[i] == m_d[edge.node] + 1) {
|
||||
return edge.node;
|
||||
}
|
||||
}
|
||||
return m_edges.size(); // no element found
|
||||
}
|
||||
|
||||
void min_cut::augment_path() {
|
||||
// find bottleneck capacity
|
||||
unsigned max = std::numeric_limits<unsigned int>::max();
|
||||
unsigned k = 1;
|
||||
while (k != 0) {
|
||||
unsigned l = m_pred[k];
|
||||
for (const auto& edge : m_edges[l]) {
|
||||
if (edge.node == k) {
|
||||
max = std::min(max, edge.weight);
|
||||
}
|
||||
}
|
||||
k = l;
|
||||
}
|
||||
|
||||
k = 1;
|
||||
while (k != 0) {
|
||||
unsigned l = m_pred[k];
|
||||
|
||||
// decrease capacity
|
||||
for (auto& edge : m_edges[l]) {
|
||||
if (edge.node == k) {
|
||||
edge.weight -= max;
|
||||
}
|
||||
}
|
||||
// increase reverse flow
|
||||
bool already_exists = false;
|
||||
for (auto& edge : m_edges[k]) {
|
||||
if (edge.node == l) {
|
||||
already_exists = true;
|
||||
edge.weight += max;
|
||||
}
|
||||
}
|
||||
if (!already_exists) {
|
||||
m_edges[k].push_back(edge(1, max));
|
||||
}
|
||||
k = l;
|
||||
}
|
||||
}
|
||||
|
||||
void min_cut::compute_distance(unsigned i) {
|
||||
if (i == 1) { // sink node
|
||||
m_d[1] = 0;
|
||||
}
|
||||
else {
|
||||
unsigned min = std::numeric_limits<unsigned int>::max();
|
||||
|
||||
// find edge (i,j) with positive residual capacity and smallest distance
|
||||
for (const auto& edge : m_edges[i]) {
|
||||
if (edge.weight > 0) {
|
||||
min = std::min(min, m_d[edge.node] + 1);
|
||||
}
|
||||
}
|
||||
m_d[i] = min;
|
||||
}
|
||||
}
|
||||
|
||||
void min_cut::compute_reachable_nodes(bool_vector& reachable) {
|
||||
unsigned_vector todo;
|
||||
|
||||
todo.push_back(0);
|
||||
while (!todo.empty()) {
|
||||
unsigned current = todo.back();
|
||||
todo.pop_back();
|
||||
|
||||
if (!reachable[current]) {
|
||||
reachable[current] = true;
|
||||
|
||||
for (const auto& edge : m_edges[current]) {
|
||||
if (edge.weight > 0) {
|
||||
todo.push_back(edge.node);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void min_cut::compute_cut_and_add_lemmas(bool_vector& reachable, unsigned_vector& cut_nodes) {
|
||||
unsigned_vector todo;
|
||||
bool_vector visited(m_edges.size());
|
||||
|
||||
todo.push_back(0);
|
||||
while (!todo.empty()) {
|
||||
unsigned current = todo.back();
|
||||
todo.pop_back();
|
||||
|
||||
if (!visited[current]) {
|
||||
visited[current] = true;
|
||||
|
||||
for (const auto& edge : m_edges[current]) {
|
||||
unsigned successor = edge.node;
|
||||
if (reachable[successor]) {
|
||||
todo.push_back(successor);
|
||||
}
|
||||
else {
|
||||
cut_nodes.push_back(successor);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
63
src/util/min_cut.h
Normal file
63
src/util/min_cut.h
Normal file
|
@ -0,0 +1,63 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Arie Gurfinkel
|
||||
|
||||
Module Name:
|
||||
|
||||
min_cut.h
|
||||
|
||||
Abstract:
|
||||
min cut solver
|
||||
|
||||
Author:
|
||||
Bernhard Gleiss
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef MIN_CUT_H_
|
||||
#define MIN_CUT_H_
|
||||
|
||||
#include "util/vector.h"
|
||||
|
||||
|
||||
class min_cut {
|
||||
public:
|
||||
min_cut();
|
||||
|
||||
/*
|
||||
\brief create a node
|
||||
*/
|
||||
unsigned new_node();
|
||||
|
||||
/*
|
||||
\brief add an i -> j edge with (unit) capacity
|
||||
*/
|
||||
void add_edge(unsigned i, unsigned j, unsigned capacity = 1);
|
||||
|
||||
/*
|
||||
\brief produce a min cut between source node = 0 and target node = 1.
|
||||
NB. the function changes capacities on edges.
|
||||
*/
|
||||
void compute_min_cut(unsigned_vector& cut_nodes);
|
||||
|
||||
private:
|
||||
|
||||
typedef svector<bool> bool_vector;
|
||||
struct edge { unsigned node; unsigned weight; edge(unsigned n, unsigned w): node(n), weight(w) {} edge(): node(0), weight(0) {} };
|
||||
typedef svector<edge> edge_vector;
|
||||
|
||||
vector<edge_vector> m_edges; // map from node to all outgoing edges together with their weights (also contains "reverse edges")
|
||||
unsigned_vector m_d; // approximation of distance from node to sink in residual graph
|
||||
unsigned_vector m_pred; // predecessor-information for reconstruction of augmenting path
|
||||
|
||||
void compute_initial_distances();
|
||||
unsigned get_admissible_edge(unsigned i);
|
||||
void augment_path();
|
||||
void compute_distance(unsigned i);
|
||||
void compute_reachable_nodes(bool_vector& reachable);
|
||||
void compute_cut_and_add_lemmas(bool_vector& reachable, unsigned_vector& cut_nodes);
|
||||
};
|
||||
|
||||
#endif
|
|
@ -185,4 +185,15 @@ public:
|
|||
|
||||
#endif
|
||||
|
||||
struct scoped_watch {
|
||||
stopwatch &m_sw;
|
||||
scoped_watch (stopwatch &sw, bool reset=false): m_sw(sw) {
|
||||
if (reset) m_sw.reset();
|
||||
m_sw.start();
|
||||
}
|
||||
~scoped_watch() {
|
||||
m_sw.stop ();
|
||||
}
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
Loading…
Reference in a new issue