mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

integrated unstable changes

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-22 11:16:37 -08:00
commit 8bea5a3625
33 changed files with 1807 additions and 1197 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/api/api_arith.cpp
View file

@ -101,27 +101,14 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0);
}
if (mk_c(c)->fparams().m_pre_simplify_expr) {
// Do not use logging here... the function is implemented using API primitives
Z3_ast m1 = Z3_mk_int(c, -1, Z3_get_sort(c, args[0]));
Z3_ast args1[2] = { args[0], 0 };
for (unsigned i = 1; i < num_args; ++i) {
Z3_ast args2[3] = { m1, args[i] };
args1[1] = Z3_mk_mul(c, 2, args2);
args1[0] = Z3_mk_add(c, 2, args1);
}
RETURN_Z3(args1[0]);
}
else {
expr* r = to_expr(args[0]);
for (unsigned i = 1; i < num_args; ++i) {
expr* args1[2] = { r, to_expr(args[i]) };
r = mk_c(c)->m().mk_app(mk_c(c)->get_arith_fid(), OP_SUB, 0, 0, 2, args1);
check_sorts(c, r);
}
mk_c(c)->save_ast_trail(r);
RETURN_Z3(of_expr(r));
expr* r = to_expr(args[0]);
for (unsigned i = 1; i < num_args; ++i) {
expr* args1[2] = { r, to_expr(args[i]) };
r = mk_c(c)->m().mk_app(mk_c(c)->get_arith_fid(), OP_SUB, 0, 0, 2, args1);
check_sorts(c, r);
}
mk_c(c)->save_ast_trail(r);
RETURN_Z3(of_expr(r));
Z3_CATCH_RETURN(0);
}
@ -129,12 +116,6 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_unary_minus(c, n);
RESET_ERROR_CODE();
if (mk_c(c)->fparams().m_pre_simplify_expr) {
Z3_ast m1 = Z3_mk_int(c, -1, Z3_get_sort(c, n));
Z3_ast args[2] = { m1, n };
Z3_ast r = Z3_mk_mul(c, 2, args);
RETURN_Z3(r);
}
MK_UNARY_BODY(Z3_mk_unary_minus, mk_c(c)->get_arith_fid(), OP_UMINUS, SKIP);
Z3_CATCH_RETURN(0);
}

12
src/api/api_bv.cpp
View file

@ -280,12 +280,6 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_TRY;
LOG_Z3_mk_bvsub(c, n1, n2);
RESET_ERROR_CODE();
// TODO: Do we really need this pre_simplifier hack?
if (mk_c(c)->fparams().m_pre_simplify_expr) {
Z3_ast m1 = Z3_mk_int(c, -1, Z3_get_sort(c, n2));
Z3_ast r = Z3_mk_bvadd(c, n1, Z3_mk_bvmul(c, m1, n2));
RETURN_Z3(r);
}
MK_BINARY_BODY(Z3_mk_bvsub, mk_c(c)->get_bv_fid(), OP_BSUB, SKIP);
Z3_CATCH_RETURN(0);
}
@ -294,12 +288,6 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_TRY;
LOG_Z3_mk_bvneg(c, n);
RESET_ERROR_CODE();
// TODO: Do we really need this pre_simplifier hack?
if (mk_c(c)->fparams().m_pre_simplify_expr) {
Z3_ast m1 = Z3_mk_int(c, -1, Z3_get_sort(c, n));
Z3_ast r = Z3_mk_bvmul(c, m1, n);
RETURN_Z3(r);
}
MK_UNARY_BODY(Z3_mk_bvneg, mk_c(c)->get_bv_fid(), OP_BNEG, SKIP);
Z3_CATCH_RETURN(0);
}

4
src/api/java/README Normal file
View file

@ -0,0 +1,4 @@
Java bindings
-------------
This is currently "working in progress".

2
src/api/z3_api.h
View file

@ -1860,7 +1860,7 @@ BEGIN_MLAPI_EXCLUDE
\param c logical context.
\param num_sorts number of datatype sorts.
\param sort_names names of datatype sorts.
\param sorts array of datattype sorts.
\param sorts array of datatype sorts.
\param constructor_lists list of constructors, one list per sort.
def_API('Z3_mk_datatypes', VOID, (_in(CONTEXT), _in(UINT), _in_array(1, SYMBOL), _out_array(1, SORT), _inout_array(1, CONSTRUCTOR_LIST)))

436
src/ast/rewriter/bit_blaster/eager_bit_blaster.cpp
View file

@ -1,436 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
eager_bit_blaster.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-10-02.
Revision History:
--*/
#include"ast_ll_pp.h"
#include"eager_bit_blaster.h"
eager_bit_blaster::basic_plugin::basic_plugin(ast_manager & m, eager_bit_blaster::bv_plugin & p, basic_simplifier_plugin & s):
simplifier_plugin(symbol("basic"), m),
m_main(p),
m_s(s) {
}
eager_bit_blaster::basic_plugin::~basic_plugin() {
}
bool eager_bit_blaster::basic_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
if (f->get_decl_kind() == OP_ITE) {
SASSERT(num_args == 3);
return m_main.reduce_ite(args[0], args[1], args[2], result);
}
else if (f->get_decl_kind() == OP_NOT) {
// the internalizer assumes there is not double negation (not (not x))
SASSERT(num_args == 1);
m_s.mk_not(args[0], result);
return true;
}
return false;
}
eager_bit_blaster::bv_plugin::bv_plugin(ast_manager & m, bit_blaster_params const & p):
simplifier_plugin(symbol("bv"), m),
m_util(m),
m_bb(m, p),
m_s(m) {
}
eager_bit_blaster::bv_plugin::~bv_plugin() {
}
void eager_bit_blaster::bv_plugin::get_bits(expr * n, expr_ref_vector & out_bits) {
rational val;
unsigned bv_size;
if (m_util.is_numeral(n, val, bv_size)) {
TRACE("eager_bb_bug", tout << "bv_size: " << bv_size << "\n";);
m_bb.num2bits(val, bv_size, out_bits);
SASSERT(out_bits.size() == bv_size);
}
else if (m_util.is_mkbv(n)) {
out_bits.append(to_app(n)->get_num_args(), to_app(n)->get_args());
}
else {
unsigned bv_size = m_util.get_bv_size(n);
for (unsigned i = 0; i < bv_size; i++) {
parameter p(i);
out_bits.push_back(m_manager.mk_app(get_family_id(), OP_BIT2BOOL, 1, &p, 1, &n));
}
SASSERT(bv_size == out_bits.size());
}
}
inline app * eager_bit_blaster::bv_plugin::mk_mkbv(expr_ref_vector const & bits) {
#ifdef Z3DEBUG
for (unsigned i = 0; i < bits.size(); i++) {
expr * b = bits.get(i);
SASSERT(!m_manager.is_not(b) || !m_manager.is_not(to_app(b)->get_arg(0)));
}
#endif
return m_manager.mk_app(get_family_id(), OP_MKBV, bits.size(), bits.c_ptr());
}
#define MK_UNARY_REDUCE(OP, BB_OP) \
void eager_bit_blaster::bv_plugin::OP(expr * arg, expr_ref & result) { \
expr_ref_vector bits(m_manager); \
get_bits(arg, bits); \
expr_ref_vector out_bits(m_manager); \
m_bb.BB_OP(bits.size(), bits.c_ptr(), out_bits); \
result = mk_mkbv(out_bits); \
}
#define MK_BIN_REDUCE(OP, BB_OP) \
void eager_bit_blaster::bv_plugin::OP(expr * arg1, expr * arg2, expr_ref & result) { \
expr_ref_vector bits1(m_manager); \
expr_ref_vector bits2(m_manager); \
get_bits(arg1, bits1); \
get_bits(arg2, bits2); \
expr_ref_vector out_bits(m_manager); \
m_bb.BB_OP(bits1.size(), bits1.c_ptr(), bits2.c_ptr(), out_bits); \
result = mk_mkbv(out_bits); \
}
#define MK_BIN_AC_FLAT_REDUCE(OP, BIN_OP, S_OP, BB_OP) \
MK_BIN_REDUCE(BIN_OP, BB_OP); \
void eager_bit_blaster::bv_plugin::OP(unsigned num_args, expr * const * args, expr_ref & result) { \
SASSERT(num_args > 0); \
if (num_args == 2) { \
BIN_OP(args[0], args[1], result); \
return; \
} \
\
ptr_buffer<expr_ref_vector> args_bits; \
for (unsigned i = 0; i < num_args; i++) { \
expr_ref_vector * bits = alloc(expr_ref_vector, m_manager); \
get_bits(args[i], *bits); \
args_bits.push_back(bits); \
} \
\
unsigned bv_size = m_util.get_bv_size(args[0]); \
expr_ref_vector new_bits(m_manager); \
for (unsigned i = 0; i < bv_size; i++) { \
expr_ref_vector arg_bits(m_manager); \
for (unsigned j = 0; j < num_args; j++) \
arg_bits.push_back(args_bits[j]->get(i)); \
expr_ref new_bit(m_manager); \
m_s.S_OP(arg_bits.size(), arg_bits.c_ptr(), new_bit); \
new_bits.push_back(new_bit); \
} \
result = mk_mkbv(new_bits); \
std::for_each(args_bits.begin(), args_bits.end(), delete_proc<expr_ref_vector>()); \
}
#define MK_BIN_AC_REDUCE(OP, BIN_OP, BB_OP) \
MK_BIN_REDUCE(BIN_OP, BB_OP); \
void eager_bit_blaster::bv_plugin::OP(unsigned num_args, expr * const * args, expr_ref & result) { \
SASSERT(num_args > 0); \
result = args[0]; \
for (unsigned i = 1; i < num_args; i++) { \
expr_ref new_result(m_manager); \
BIN_OP(result.get(), args[i], new_result); \
result = new_result; \
} \
}
#define MK_BIN_PRED_REDUCE(OP, BB_OP) \
void eager_bit_blaster::bv_plugin::OP(expr * arg1, expr * arg2, expr_ref & result) { \
expr_ref_vector bits1(m_manager); \
expr_ref_vector bits2(m_manager); \
get_bits(arg1, bits1); \
get_bits(arg2, bits2); \
m_bb.BB_OP(bits1.size(), bits1.c_ptr(), bits2.c_ptr(), result); \
}
#define MK_PARAMETRIC_UNARY_REDUCE(OP, BB_OP) \
void eager_bit_blaster::bv_plugin::OP(expr * arg, unsigned n, expr_ref & result) { \
expr_ref_vector bits(m_manager); \
get_bits(arg, bits); \
expr_ref_vector out_bits(m_manager); \
m_bb.BB_OP(bits.size(), bits.c_ptr(), n, out_bits); \
result = mk_mkbv(out_bits); \
}
MK_UNARY_REDUCE(reduce_not, mk_not);
MK_BIN_AC_FLAT_REDUCE(reduce_or, reduce_bin_or, mk_or, mk_or);
MK_BIN_AC_FLAT_REDUCE(reduce_and, reduce_bin_and, mk_and, mk_and);
MK_BIN_AC_FLAT_REDUCE(reduce_nor, reduce_bin_nor, mk_nor, mk_nor);
MK_BIN_AC_FLAT_REDUCE(reduce_nand, reduce_bin_nand, mk_nand, mk_nand);
MK_BIN_REDUCE(reduce_xor, mk_xor);
MK_BIN_REDUCE(reduce_xnor, mk_xnor);
MK_UNARY_REDUCE(reduce_neg, mk_neg);
MK_BIN_AC_REDUCE(reduce_add, reduce_bin_add, mk_adder);
MK_BIN_AC_REDUCE(reduce_mul, reduce_bin_mul, mk_multiplier);
MK_BIN_PRED_REDUCE(reduce_sle, mk_sle);
MK_BIN_PRED_REDUCE(reduce_ule, mk_ule);
MK_PARAMETRIC_UNARY_REDUCE(reduce_rotate_left, mk_rotate_left);
MK_PARAMETRIC_UNARY_REDUCE(reduce_rotate_right, mk_rotate_right);
MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
MK_PARAMETRIC_UNARY_REDUCE(reduce_zero_extend, mk_zero_extend);
MK_UNARY_REDUCE(reduce_redor, mk_redor);
MK_UNARY_REDUCE(reduce_redand, mk_redand);
MK_BIN_REDUCE(reduce_shl, mk_shl);
MK_BIN_REDUCE(reduce_ashr, mk_ashr);
MK_BIN_REDUCE(reduce_lshr, mk_lshr);
MK_BIN_REDUCE(reduce_comp, mk_comp);
MK_BIN_REDUCE(reduce_udiv, mk_udiv);
MK_BIN_REDUCE(reduce_urem, mk_urem);
MK_BIN_REDUCE(reduce_sdiv, mk_sdiv);
MK_BIN_REDUCE(reduce_srem, mk_srem);
MK_BIN_REDUCE(reduce_smod, mk_smod);
void eager_bit_blaster::bv_plugin::reduce_extract(unsigned start, unsigned end, expr * arg, expr_ref & result) {
expr_ref_vector bits(m_manager);
get_bits(arg, bits);
expr_ref_vector out_bits(m_manager);
for (unsigned i = start; i <= end; ++i)
out_bits.push_back(bits.get(i));
result = mk_mkbv(out_bits);
}
void eager_bit_blaster::bv_plugin::reduce_concat(unsigned num_args, expr * const * args, expr_ref & result) {
expr_ref_vector out_bits(m_manager);
unsigned i = num_args;
while (i > 0) {
i--;
expr_ref_vector bits(m_manager);
get_bits(args[i], bits);
out_bits.append(bits.size(), bits.c_ptr());
}
result = mk_mkbv(out_bits);
}
bool eager_bit_blaster::bv_plugin::reduce_ite(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
sort * s = m_manager.get_sort(arg2);
if (!m_util.is_bv_sort(s))
return false;
expr_ref_vector bits1(m_manager);
expr_ref_vector bits2(m_manager);
get_bits(arg2, bits1);
get_bits(arg3, bits2);
SASSERT(bits1.size() == bits2.size());
expr_ref_vector out_bits(m_manager);
unsigned bv_size = bits1.size();
for (unsigned i = 0; i < bv_size; i++) {
expr_ref new_bit(m_manager);
m_s.mk_ite(arg1, bits1.get(i), bits2.get(i), new_bit);
out_bits.push_back(new_bit);
}
result = mk_mkbv(out_bits);
return true;
}
bool eager_bit_blaster::bv_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
bv_op_kind k = static_cast<bv_op_kind>(f->get_decl_kind());
switch (k) {
case OP_BNOT:
SASSERT(num_args == 1);
reduce_not(args[0], result);
return true;
case OP_BOR:
reduce_or(num_args, args, result);
return true;
case OP_BAND:
reduce_and(num_args, args, result);
return true;
case OP_BNOR:
reduce_nor(num_args, args, result);
return true;
case OP_BNAND:
reduce_nand(num_args, args, result);
return true;
case OP_BXOR:
SASSERT(num_args == 2);
reduce_xor(args[0], args[1], result);
return true;
case OP_BXNOR:
SASSERT(num_args == 2);
reduce_xnor(args[0], args[1], result);
return true;
case OP_BNEG:
SASSERT(num_args == 1);
reduce_neg(args[0], result);
return true;
case OP_BADD:
reduce_add(num_args, args, result);
return true;
case OP_BMUL:
reduce_mul(num_args, args, result);
return true;
case OP_BIT1:
case OP_BIT0:
case OP_BSUB:
// I'm assuming the expressions were simplified before invoking this method.
UNREACHABLE();
return false;
case OP_BSDIV:
case OP_BUDIV:
case OP_BSREM:
case OP_BUREM:
case OP_BSMOD:
// I'm assuming the expressions were simplified before invoking this method.
UNREACHABLE();
return false;
case OP_BSDIV0:
case OP_BUDIV0:
case OP_BSREM0:
case OP_BUREM0:
case OP_BSMOD0:
// do nothing... these are uninterpreted
return true;
case OP_BSDIV_I:
SASSERT(num_args == 2);
reduce_sdiv(args[0], args[1], result);
return true;
case OP_BUDIV_I:
SASSERT(num_args == 2);
reduce_udiv(args[0], args[1], result);
return true;
case OP_BSREM_I:
SASSERT(num_args == 2);
reduce_srem(args[0], args[1], result);
return true;
case OP_BUREM_I:
SASSERT(num_args == 2);
reduce_urem(args[0], args[1], result);
return true;
case OP_BSMOD_I:
SASSERT(num_args == 2);
reduce_smod(args[0], args[1], result);
return true;
case OP_ULEQ:
SASSERT(num_args == 2);
reduce_ule(args[0], args[1], result);
return true;
case OP_SLEQ:
SASSERT(num_args == 2);
reduce_sle(args[0], args[1], result);
return true;
case OP_UGEQ:
case OP_SGEQ:
case OP_ULT:
case OP_SLT:
case OP_UGT:
case OP_SGT:
// I'm assuming the expressions were simplified before invoking this method.
UNREACHABLE();
return false;
case OP_EXTRACT:
SASSERT(num_args == 1);
reduce_extract(f->get_parameter(1).get_int(), f->get_parameter(0).get_int(), args[0], result);
return true;
case OP_CONCAT:
reduce_concat(num_args, args, result);
return true;
case OP_SIGN_EXT:
SASSERT(num_args == 1);
reduce_sign_extend(args[0], f->get_parameter(0).get_int(), result);
return true;
case OP_ZERO_EXT:
SASSERT(num_args == 1);
reduce_zero_extend(args[0], f->get_parameter(0).get_int(), result);
return true;
case OP_REPEAT:
UNREACHABLE();
return false;
case OP_BREDOR:
SASSERT(num_args == 1);
reduce_redor(args[0], result);
return true;
case OP_BREDAND:
SASSERT(num_args == 1);
reduce_redand(args[0], result);
return true;
case OP_BCOMP:
SASSERT(num_args == 2);
reduce_comp(args[0], args[1], result);
return true;
case OP_BSHL:
SASSERT(num_args == 2);
reduce_shl(args[0], args[1], result);
return true;
case OP_BLSHR:
SASSERT(num_args == 2);
reduce_lshr(args[0], args[1], result);
return true;
case OP_BASHR:
SASSERT(num_args == 2);
reduce_ashr(args[0], args[1], result);
return true;
case OP_ROTATE_LEFT:
SASSERT(num_args == 1);
reduce_rotate_left(args[0], f->get_parameter(0).get_int(), result);
return true;
case OP_ROTATE_RIGHT:
SASSERT(num_args == 1);
reduce_rotate_right(args[0], f->get_parameter(0).get_int(), result);
return true;
default:
return false;
}
}
bool eager_bit_blaster::bv_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) {
TRACE("eager_bb_eq", tout << mk_ll_pp(lhs, m_manager) << "\n" << mk_ll_pp(rhs, m_manager) << "\n";);
SASSERT(m_util.get_bv_size(lhs) == m_util.get_bv_size(rhs));
expr_ref_vector bits1(m_manager);
expr_ref_vector bits2(m_manager);
get_bits(lhs, bits1);
get_bits(rhs, bits2);
SASSERT(bits1.size() == bits2.size());
m_bb.mk_eq(bits1.size(), bits1.c_ptr(), bits2.c_ptr(), result);
return true;
}
bool eager_bit_blaster::bv_plugin::reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result) {
if (num_args <= 1) {
result = m_manager.mk_true();
}
if (num_args == 2) {
expr_ref tmp(m_manager);
reduce_eq(args[0], args[1], tmp);
m_s.mk_not(tmp, result);
}
else {
expr_ref_vector new_args(m_manager);
for (unsigned i = 0; i < num_args - 1; i++) {
expr * a1 = args[i];
for (unsigned j = i + 1; j < num_args; j++) {
expr * a2 = args[j];
expr_ref tmp1(m_manager);
reduce_eq(a1, a2, tmp1);
expr_ref tmp2(m_manager);
m_s.mk_not(tmp1, tmp2);
new_args.push_back(tmp2);
}
}
m_s.mk_and(new_args.size(), new_args.c_ptr(), result);
}
return true;
}
eager_bit_blaster::eager_bit_blaster(ast_manager & m, bit_blaster_params const & p):
m_simplifier(m) {
m_simplifier.enable_ac_support(false);
bv_plugin * bv_p = alloc(bv_plugin, m, p);
m_simplifier.register_plugin(bv_p);
m_simplifier.register_plugin(alloc(basic_plugin, m, *bv_p, bv_p->get_basic_simplifier()));
}
void eager_bit_blaster::operator()(expr * s, expr_ref & r, proof_ref & p) {
m_simplifier.operator()(s, r, p);
}

107
src/ast/rewriter/bit_blaster/eager_bit_blaster.h
View file

@ -1,107 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
eager_bit_blaster.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-10-02.
Revision History:
--*/
#ifndef _EAGER_BIT_BLASTER_H_
#define _EAGER_BIT_BLASTER_H_
#include"bv_decl_plugin.h"
#include"bit_blaster.h"
#include"simplifier.h"
#include"basic_simplifier_plugin.h"
class eager_bit_blaster {
class bv_plugin : public simplifier_plugin {
bv_util m_util;
bit_blaster m_bb;
basic_simplifier_plugin m_s;
void get_bits(expr * n, expr_ref_vector & out_bits);
app * mk_mkbv(expr_ref_vector const & bits);
void reduce_not(expr * arg, expr_ref & result);
void reduce_bin_or(expr * arg1, expr * arg2, expr_ref & result);
void reduce_or(unsigned num_args, expr * const * args, expr_ref & result);
void reduce_bin_and(expr * arg1, expr * arg2, expr_ref & result);
void reduce_and(unsigned num_args, expr * const * args, expr_ref & result);
void reduce_bin_nor(expr * arg1, expr * arg2, expr_ref & result);
void reduce_nor(unsigned num_args, expr * const * args, expr_ref & result);
void reduce_bin_nand(expr * arg1, expr * arg2, expr_ref & result);
void reduce_nand(unsigned num_args, expr * const * args, expr_ref & result);
void reduce_xor(expr * arg1, expr * arg2, expr_ref & result);
void reduce_xnor(expr * arg1, expr * arg2, expr_ref & result);
void reduce_neg(expr * arg, expr_ref & result);
void reduce_bin_add(expr * arg1, expr * arg2, expr_ref & result);
void reduce_add(unsigned num_args, expr * const * args, expr_ref & result);
void reduce_bin_mul(expr * arg1, expr * arg2, expr_ref & result);
void reduce_mul(unsigned num_args, expr * const * args, expr_ref & result);
void reduce_sdiv(expr * arg1, expr * arg2, expr_ref & result);
void reduce_udiv(expr * arg1, expr * arg2, expr_ref & result);
void reduce_srem(expr * arg1, expr * arg2, expr_ref & result);
void reduce_urem(expr * arg1, expr * arg2, expr_ref & result);
void reduce_smod(expr * arg1, expr * arg2, expr_ref & result);
void reduce_sle(expr * arg1, expr * arg2, expr_ref & result);
void reduce_ule(expr * arg1, expr * arg2, expr_ref & result);
void reduce_concat(unsigned num_args, expr * const * args, expr_ref & result);
void reduce_extract(unsigned start, unsigned end, expr * arg, expr_ref & result);
void reduce_redor(expr * arg, expr_ref & result);
void reduce_redand(expr * arg, expr_ref & result);
void reduce_comp(expr * arg1, expr * arg2, expr_ref & result);
void reduce_shl(expr * arg1, expr * arg2, expr_ref & result);
void reduce_ashr(expr * arg1, expr * arg2, expr_ref & result);
void reduce_lshr(expr * arg1, expr * arg2, expr_ref & result);
void reduce_rotate_left(expr * arg, unsigned n, expr_ref & result);
void reduce_rotate_right(expr * arg, unsigned n, expr_ref & result);
void reduce_sign_extend(expr * arg, unsigned n, expr_ref & result);
void reduce_zero_extend(expr * arg, unsigned n, expr_ref & result);
public:
bv_plugin(ast_manager & m, bit_blaster_params const & p);
virtual ~bv_plugin();
virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result);
virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result);
basic_simplifier_plugin & get_basic_simplifier() { return m_s; }
bool reduce_ite(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
};
/**
\brief Plugin for handling the term-ite.
*/
class basic_plugin : public simplifier_plugin {
bv_plugin & m_main;
basic_simplifier_plugin & m_s;
public:
basic_plugin(ast_manager & m, bv_plugin & p, basic_simplifier_plugin & s);
virtual ~basic_plugin();
virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
};
simplifier m_simplifier;
public:
eager_bit_blaster(ast_manager & m, bit_blaster_params const & p);
void operator()(expr * s, expr_ref & r, proof_ref & p);
};
#endif /* _EAGER_BIT_BLASTER_H_ */

3
src/front_end_params/bit_blaster_params.h
View file

@ -22,16 +22,13 @@ Revision History:
#include"ini_file.h"
struct bit_blaster_params {
bool m_bb_eager;
bool m_bb_ext_gates;
bool m_bb_quantifiers;
bit_blaster_params():
m_bb_eager(false),
m_bb_ext_gates(false),
m_bb_quantifiers(false) {
}
void register_params(ini_params & p) {
p.register_bool_param("BB_EAGER", m_bb_eager, "eager bit blasting");
p.register_bool_param("BB_EXT_GATES", m_bb_ext_gates, "use extended gates during bit-blasting");
p.register_bool_param("BB_QUANTIFIERS", m_bb_quantifiers, "convert bit-vectors to Booleans in quantifiers");
}

4
src/front_end_params/front_end_params.cpp
View file

@ -21,12 +21,9 @@ Revision History:
void front_end_params::register_params(ini_params & p) {
p.register_param_vector(m_param_vector.get());
preprocessor_params::register_params(p);
spc_params::register_params(p);
smt_params::register_params(p);
parser_params::register_params(p);
arith_simplifier_params::register_params(p);
p.register_int_param("ENGINE", 0, 2, reinterpret_cast<int&>(m_engine), "0: SMT solver, 1: Superposition prover, 2: EPR solver, true");
z3_solver_params::register_params(p);
model_params::register_params(p);
p.register_bool_param("AT_LABELS_CEX", m_at_labels_cex,
"only use labels that contain '@' when building multiple counterexamples");
@ -43,7 +40,6 @@ void front_end_params::register_params(ini_params & p) {
p.register_int_param("PROOF_MODE", 0, 2, reinterpret_cast<int&>(m_proof_mode), "select proof generation mode: 0 - disabled, 1 - coarse grain, 2 - fine grain");
p.register_bool_param("TRACE", m_trace, "enable tracing for the Axiom Profiler tool");
p.register_string_param("TRACE_FILE_NAME", m_trace_file_name, "tracing file name");
p.register_bool_param("IGNORE_SETPARAMETER", m_ignore_setparameter, "ignore (SETPARAMETER ...) commands in Simplify format input");
p.register_bool_param("ASYNC_COMMANDS", m_async_commands, "enable/disable support for asynchronous commands in the Simplify front-end.");
p.register_bool_param("DISPLAY_CONFIG", m_display_config, "display configuration used by Z3");

16
src/front_end_params/front_end_params.h
View file

@ -22,25 +22,16 @@ Revision History:
#include"ini_file.h"
#include"ast.h"
#include"preprocessor_params.h"
#include"spc_params.h"
#include"smt_params.h"
#include"pp_params.h"
#include"parser_params.h"
#include"arith_simplifier_params.h"
#include"z3_solver_params.h"
#include"model_params.h"
enum engine {
ENG_SMT,
ENG_SPC,
ENG_EPR
};
struct front_end_params : public preprocessor_params, public spc_params, public smt_params, public parser_params,
public arith_simplifier_params, public z3_solver_params, public model_params
struct front_end_params : public preprocessor_params, public smt_params, public parser_params,
public arith_simplifier_params, public model_params
{
ref<param_vector> m_param_vector;
engine m_engine;
bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples.
bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.
bool m_default_qid;
@ -65,7 +56,6 @@ struct front_end_params : public preprocessor_params, public spc_params, public
bool m_trace;
std::string m_trace_file_name;
std::fstream* m_trace_stream;
bool m_ignore_setparameter;
bool m_async_commands;
bool m_display_config;
bool m_user_theory_preprocess_axioms;
@ -74,7 +64,6 @@ struct front_end_params : public preprocessor_params, public spc_params, public
front_end_params():
m_param_vector(alloc(param_vector, this)),
m_engine(ENG_SMT),
m_at_labels_cex(false),
m_check_at_labels(false),
m_default_qid(false),
@ -107,7 +96,6 @@ struct front_end_params : public preprocessor_params, public spc_params, public
m_trace(false),
m_trace_file_name("z3.log"),
m_trace_stream(NULL),
m_ignore_setparameter(false),
m_async_commands(true),
m_display_config(false),
m_user_theory_preprocess_axioms(false),

27
src/front_end_params/order_params.cpp
View file

@ -1,27 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
order_params.cpp
Abstract:
Term ordering parameters.
Author:
Leonardo de Moura (leonardo) 2008-01-28.
Revision History:
--*/
#include"order_params.h"
void order_params::register_params(ini_params & p) {
p.register_symbol_list_param("PRECEDENCE", m_order_precedence, "describe a (partial) precedence for the term ordering used in the Superposition Calculus module. The precedence is lists of function symbols. Example: PRECEDENCE=\"(f, g, h)\"");
p.register_symbol_list_param("PRECEDENCE_GEN", m_order_precedence_gen, "describe how a total precedence order is generated. The generator is a sequence of simple (partial) orders with an optional '-' (indicating the next (partial) order should be inverted). The available simple (partial) orders are: user (the order specified by precedence); arity; interpreted (interpreted function symbols are considered smaller); definition (defined function symbols are considered bigger); frequency; arbitrary (total arbitrary order generated by Z3). Example: PRECEDENCE_GEN=\"user interpreted - arity arbitraty\"");
p.register_symbol_nat_list_param("ORDER_WEIGHTS", m_order_weights, "describe a (partial) assignment of weights to function symbols for term orderings (e.g., KBO). The assigment is a list of pairs of the form f:n where f is a string and n is a natural. Example: WEIGHTS=\"(f:1, g:2, h:3)\"");
p.register_unsigned_param("ORDER_VAR_WEIGHT", m_order_var_weight, "weight of variables in term orderings (e.g., KBO)");
p.register_int_param("ORDER", 0, 1, reinterpret_cast<int&>(m_order_kind), "Term ordering: 0 - KBO, 1 - LPO");
}

44
src/front_end_params/order_params.h
View file

@ -1,44 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
order_params.h
Abstract:
Term ordering parameters.
Author:
Leonardo de Moura (leonardo) 2008-01-28.
Revision History:
--*/
#ifndef _ORDER_PARAMS_H_
#define _ORDER_PARAMS_H_
#include"ini_file.h"
enum order_kind {
ORD_KBO,
ORD_LPO
};
struct order_params {
svector<symbol> m_order_precedence;
svector<symbol> m_order_precedence_gen;
svector<symbol_nat_pair> m_order_weights;
unsigned m_order_var_weight;
order_kind m_order_kind;
order_params():
m_order_var_weight(1),
m_order_kind(ORD_KBO) {
}
void register_params(ini_params & p);
};
#endif /* _ORDER_PARAMS_H_ */

37
src/front_end_params/spc_params.cpp
View file

@ -1,37 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
spc_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-02-08.
Revision History:
--*/
#include"spc_params.h"
void spc_params::register_params(ini_params & p) {
order_params::register_params(p);
p.register_unsigned_param("SPC_MIN_FUNC_FREQ_SUBSUMPTION_INDEX",m_min_func_freq_subsumption_index,
"minimal number of occurrences (in clauses) for a function symbol to be considered for subsumption indexing.");
p.register_unsigned_param("SPC_MAX_SUBSUMPTION_INDEX_FEATURES", m_max_subsumption_index_features,
"maximum number of features to be used for subsumption index.");
p.register_unsigned_param("SPC_INITIAL_SUBSUMPTION_INDEX_OPT", m_initial_subsumption_index_opt,
"after how many processed clauses the subsumption index is optimized.");
p.register_double_param("SPC_FACTOR_SUBSUMPTION_INDEX_OPT", m_factor_subsumption_index_opt,
"after each optimization the threshold for optimization is increased by this factor. See INITIAL_SUBSUMPTION_INDEX_OPT.");
p.register_bool_param("SPC_BS", m_backward_subsumption, "Enable/disable backward subsumption in the superposition engine");
p.register_bool_param("SPC_ES", m_equality_subsumption, "Enable/disable equality resolution in the superposition engine");
p.register_unsigned_param("SPC_NUM_ITERATIONS", m_spc_num_iterations);
p.register_bool_param("SPC_TRACE", m_spc_trace);
}

49
src/front_end_params/spc_params.h
View file

@ -1,49 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
spc_params.h
Abstract:
Parameters for the Superposition Calculus Engine
Author:
Leonardo de Moura (leonardo) 2008-02-08.
Revision History:
--*/
#ifndef _SPC_PARAMS_H_
#define _SPC_PARAMS_H_
#include"order_params.h"
struct spc_params : public order_params {
unsigned m_min_func_freq_subsumption_index;
unsigned m_max_subsumption_index_features;
unsigned m_initial_subsumption_index_opt;
double m_factor_subsumption_index_opt;
bool m_backward_subsumption;
bool m_equality_subsumption;
unsigned m_spc_num_iterations;
bool m_spc_trace;
spc_params():
m_min_func_freq_subsumption_index(100),
m_max_subsumption_index_features(32),
m_initial_subsumption_index_opt(1000),
m_factor_subsumption_index_opt(1.5),
m_backward_subsumption(true),
m_equality_subsumption(true),
m_spc_num_iterations(1000),
m_spc_trace(false) {
}
void register_params(ini_params & p);
};
#endif /* _SPC_PARAMS_H_ */

30
src/front_end_params/z3_solver_params.cpp
View file

@ -1,30 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
z3_solver_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2007-06-11.
Revision History:
--*/
#include"z3_solver_params.h"
void z3_solver_params::register_params(ini_params & p) {
p.register_bool_param("Z3_SOLVER_LL_PP", m_ast_ll_pp, "pretty print asserted constraints using low-level printer (Z3 input format specific)");
p.register_bool_param("Z3_SOLVER_SMT_PP", m_ast_smt_pp, "pretty print asserted constraints using SMT printer (Z3 input format specific)");
p.register_bool_param("PRE_SIMPLIFY_EXPR", m_pre_simplify_expr, "pre-simplify expressions when created over the API (example: -x -> (* -1 x))");
p.register_string_param("SMTLIB_TRACE_PATH", m_smtlib_trace_path, "path for converting Z3 formulas to SMTLIB benchmarks");
p.register_string_param("SMTLIB_SOURCE_INFO", m_smtlib_source_info, "additional source info to add to SMTLIB benchmark");
p.register_string_param("SMTLIB_CATEGORY", m_smtlib_category, "additional category info to add to SMTLIB benchmark");
}

44
src/front_end_params/z3_solver_params.h
View file

@ -1,44 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
z3_solver_params.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2007-06-11.
Revision History:
--*/
#ifndef _Z3_SOLVER_PARAMS_H_
#define _Z3_SOLVER_PARAMS_H_
#include"ini_file.h"
struct z3_solver_params {
bool m_ast_ll_pp;
bool m_ast_smt_pp;
bool m_pre_simplify_expr;
std::string m_smtlib_trace_path;
std::string m_smtlib_source_info;
std::string m_smtlib_category;
z3_solver_params():
m_ast_ll_pp(false),
m_ast_smt_pp(false),
m_pre_simplify_expr(false),
m_smtlib_trace_path(""),
m_smtlib_source_info(""),
m_smtlib_category("")
{}
void register_params(ini_params & p);
};
#endif /* _Z3_SOLVER_PARAMS_H_ */

97
src/muz_qe/dl_mk_extract_quantifiers.cpp Normal file
View file

@ -0,0 +1,97 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
dl_mk_extract_quantifiers.cpp
Abstract:
Remove universal quantifiers over interpreted predicates in the body.
Author:
Nikolaj Bjorner (nbjorner) 2012-11-21
Revision History:
--*/
#include"dl_mk_extract_quantifiers.h"
#include"ast_pp.h"
namespace datalog {
mk_extract_quantifiers::mk_extract_quantifiers(context & ctx) :
rule_transformer::plugin(101, false),
m_ctx(ctx),
m(ctx.get_manager()),
rm(ctx.get_rule_manager())
{}
mk_extract_quantifiers::~mk_extract_quantifiers() {
for (unsigned i = 0; i < m_refs.size(); ++i) {
dealloc(m_refs[i]);
}
m_quantifiers.reset();
m_refs.reset();
}
void mk_extract_quantifiers::extract(rule& r, rule_set& new_rules) {
app_ref_vector tail(m);
svector<bool> neg_tail;
quantifier_ref_vector quantifiers(m);
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size();
for (unsigned i = 0; i < utsz; ++i) {
tail.push_back(r.get_tail(i));
neg_tail.push_back(r.is_neg_tail(i));
}
for (unsigned i = utsz; i < tsz; ++i) {
SASSERT(!r.is_neg_tail(i));
app* t = r.get_tail(i);
expr_ref_vector conjs(m);
datalog::flatten_and(t, conjs);
for (unsigned j = 0; j < conjs.size(); ++j) {
expr* e = conjs[j].get();
quantifier* q = 0;
if (rule_manager::is_forall(m, e, q)) {
quantifiers.push_back(q);
}
else {
tail.push_back(is_app(e)?to_app(e):m.mk_eq(e, m.mk_true()));
neg_tail.push_back(false);
}
}
}
if (quantifiers.empty()) {
new_rules.add_rule(&r);
}
else {
rule* new_rule = rm.mk(r.get_head(), tail.size(), tail.c_ptr(), neg_tail.c_ptr(), r.name(), false);
new_rules.add_rule(new_rule);
quantifier_ref_vector* qs = alloc(quantifier_ref_vector, quantifiers);
m_quantifiers.insert(new_rule, qs);
m_refs.push_back(qs);
}
}
rule_set * mk_extract_quantifiers::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) {
m_quantifiers.reset();
rule_set* rules = alloc(rule_set, m_ctx);
rule_set::iterator it = source.begin(), end = source.end();
for (; it != end; ++it) {
extract(**it, *rules);
}
if (m_quantifiers.empty()) {
dealloc(rules);
rules = 0;
}
return rules;
}
};

59
src/muz_qe/dl_mk_extract_quantifiers.h Normal file
View file

@ -0,0 +1,59 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
dl_mk_extract_quantifiers.h
Abstract:
Remove universal quantifiers over interpreted predicates in the body.
Author:
Nikolaj Bjorner (nbjorner) 2012-11-21
Revision History:
--*/
#ifndef _DL_MK_EXTRACT_QUANTIFIERS_H_
#define _DL_MK_EXTRACT_QUANTIFIERS_H_
#include"dl_context.h"
#include"dl_rule_set.h"
#include"dl_rule_transformer.h"
namespace datalog {
/**
\brief Extract universal quantifiers from rules.
*/
class mk_extract_quantifiers : public rule_transformer::plugin {
context& m_ctx;
ast_manager& m;
rule_manager& rm;
ptr_vector<quantifier_ref_vector> m_refs;
obj_map<rule const, quantifier_ref_vector*> m_quantifiers;
void extract(rule& r, rule_set& new_rules);
public:
/**
\brief Create rule transformer that extracts universal quantifiers (over recursive predicates).
*/
mk_extract_quantifiers(context & ctx);
virtual ~mk_extract_quantifiers();
rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc);
obj_map<rule const, quantifier_ref_vector*>& quantifiers() { return m_quantifiers; }
bool has_quantifiers() const { return !m_quantifiers.empty(); }
};
};
#endif /* _DL_MK_EXTRACT_QUANTIFIERS_H_ */

48
src/muz_qe/pdr_context.cpp
View file

@ -65,10 +65,6 @@ namespace pdr {
m_reachable(pm, pm.get_params()) {}
pred_transformer::~pred_transformer() {
qinst_map::iterator it = m_rule2qinst.begin(), end = m_rule2qinst.end();
for (; it != end; ++it) {
dealloc(it->m_value);
}
rule2inst::iterator it2 = m_rule2inst.begin(), end2 = m_rule2inst.end();
for (; it2 != end2; ++it2) {
dealloc(it2->m_value);
@ -556,7 +552,6 @@ namespace pdr {
// positions the variables occur are made equivalent with these.
expr_ref_vector conj(m);
app_ref_vector& var_reprs = *(alloc(app_ref_vector, m));
qinst* qi = 0;
ptr_vector<app> aux_vars;
unsigned ut_size = rule.get_uninterpreted_tail_size();
@ -581,19 +576,6 @@ namespace pdr {
for (unsigned i = 0; i < tail.size(); ++i) {
expr_ref tmp(m);
var_subst(m, false)(tail[i].get(), var_reprs.size(), (expr*const*)var_reprs.c_ptr(), tmp);
quantifier* q;
if (datalog::rule_manager::is_forall(m, tmp, q)) {
if (!qi) {
qi = alloc(qinst, m);
}
//
// The contract is to instantiate q with
// sufficient witnesses to validate body.
//
qi->quantifiers.push_back(q);
tmp = m.mk_true();
}
conj.push_back(tmp);
TRACE("pdr", tout << mk_pp(tail[i].get(), m) << "\n" << mk_pp(tmp, m) << "\n";);
SASSERT(is_ground(tmp));
@ -607,12 +589,10 @@ namespace pdr {
TRACE("pdr", tout << mk_pp(fml, m) << "\n";);
SASSERT(is_ground(fml));
if (m.is_false(fml)) {
dealloc(qi);
qi = 0;
// no-op.
}
else {
if (ut_size == 0 && !qi) {
if (ut_size == 0) {
init = m.mk_or(init, fml);
}
transitions.push_back(fml);
@ -620,9 +600,6 @@ namespace pdr {
m_rule2transition.insert(&rule, fml.get());
rules.push_back(&rule);
}
if (qi) {
m_rule2qinst.insert(&rule, qi);
}
m_rule2inst.insert(&rule,&var_reprs);
m_rule2vars.insert(&rule, aux_vars);
}
@ -1119,7 +1096,6 @@ namespace pdr {
m_params(params),
m(m),
m_context(0),
m_quantifier_inst(*this, m),
m_pm(m_fparams, m_params, m),
m_query_pred(m),
m_query(0),
@ -1491,7 +1467,6 @@ namespace pdr {
UNREACHABLE();
}
catch (model_exception) {
check_quantifiers();
IF_VERBOSE(1, verbose_stream() << "\n"; m_search.display(verbose_stream()););
m_last_result = l_true;
validate();
@ -1605,24 +1580,6 @@ namespace pdr {
}
}
//
// Check that quantifiers are satisfied in the produced model.
//
void context::check_quantifiers() {
if (has_quantifiers()) {
m_quantifier_inst.model_check(m_search.get_root());
}
}
bool context::has_quantifiers() const {
decl2rel const& dr = get_pred_transformers();
decl2rel::iterator it = dr.begin(), end = dr.end();
for (; it != end; ++it) {
pred_transformer* pt = it->m_value;
if (pt->has_quantifiers()) return true;
}
return false;
}
//
// Pick a potential counter example state.
@ -1832,8 +1789,7 @@ namespace pdr {
for (unsigned i = 0; i < sig_size; ++i) {
vars.push_back(m.mk_const(m_pm.o2n(pt.sig(i), 0)));
}
ptr_vector<app> aux_vars;
pt.get_aux_vars(r, aux_vars);
ptr_vector<app>& aux_vars = pt.get_aux_vars(r);
vars.append(aux_vars.size(), aux_vars.c_ptr());
scoped_ptr<expr_replacer> rep;

17
src/muz_qe/pdr_context.h
View file

@ -29,7 +29,6 @@ Revision History:
#include "dl_base.h"
#include "pdr_prop_solver.h"
#include "pdr_reachable_cache.h"
#include "pdr_quantifiers.h"
namespace datalog {
class rule_set;
@ -42,7 +41,6 @@ namespace pdr {
class model_node;
class context;
typedef obj_map<datalog::rule const, qinst*> qinst_map;
typedef obj_map<datalog::rule const, app_ref_vector*> rule2inst;
typedef obj_map<func_decl, pred_transformer*> decl2rel;
@ -78,7 +76,6 @@ namespace pdr {
obj_map<expr, unsigned> m_prop2level; // map property to level where it occurs.
obj_map<expr, datalog::rule const*> m_tag2rule; // map tag predicate to rule.
rule2expr m_rule2tag; // map rule to predicate tag.
qinst_map m_rule2qinst; // map tag to quantifier instantiation.
rule2inst m_rule2inst; // map rules to instantiations of indices
rule2expr m_rule2transition; // map rules to transition
rule2apps m_rule2vars; // map rule to auxiliary variables
@ -99,7 +96,6 @@ namespace pdr {
void init_rule(decl2rel const& pts, datalog::rule const& rule, expr_ref& init,
ptr_vector<datalog::rule const>& rules, expr_ref_vector& transition);
void init_atom(decl2rel const& pts, app * atom, app_ref_vector& var_reprs, expr_ref_vector& conj, unsigned tail_idx);
void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector<app>& aux_vars);
void simplify_formulas(tactic& tac, expr_ref_vector& fmls);
@ -122,8 +118,6 @@ namespace pdr {
func_decl* const* sig() { init_sig(); return m_sig.c_ptr(); }
expr* transition() const { return m_transition; }
expr* initial_state() const { return m_initial_state; }
bool has_quantifiers() const { return !m_rule2qinst.empty(); }
qinst* get_quantifiers(datalog::rule const* r) const { qinst* q = 0; m_rule2qinst.find(r, q); return q; }
expr* rule2tag(datalog::rule const* r) { return m_rule2tag.find(r); }
unsigned get_num_levels() { return m_levels.size(); }
expr_ref get_cover_delta(func_decl* p_orig, int level);
@ -140,7 +134,7 @@ namespace pdr {
void find_predecessors(model_core const& model, ptr_vector<func_decl>& preds) const;
datalog::rule const& find_rule(model_core const& model) const;
expr* get_transition(datalog::rule const& r) { return m_rule2transition.find(&r); }
void get_aux_vars(datalog::rule const& r, ptr_vector<app>& vs) { m_rule2vars.find(&r, vs); }
ptr_vector<app>& get_aux_vars(datalog::rule const& r) { return m_rule2vars.find(&r); }
bool propagate_to_next_level(unsigned level);
void add_property(expr * lemma, unsigned lvl); // add property 'p' to state at level.
@ -166,6 +160,8 @@ namespace pdr {
void inherit_properties(pred_transformer& other);
void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector<app>& aux_vars);
};
@ -292,7 +288,6 @@ namespace pdr {
params_ref const& m_params;
ast_manager& m;
datalog::context* m_context;
quantifier_model_checker m_quantifier_inst;
manager m_pm;
decl2rel m_rels; // Map from relation predicate to fp-operator.
func_decl_ref m_query_pred;
@ -309,8 +304,6 @@ namespace pdr {
// Functions used by search.
void solve_impl();
bool check_reachability(unsigned level);
void check_quantifiers();
bool has_quantifiers() const;
void propagate(unsigned max_prop_lvl);
void close_node(model_node& n);
void check_pre_closed(model_node& n);
@ -396,8 +389,6 @@ namespace pdr {
void set_axioms(expr* axioms) { m_pm.set_background(axioms); }
void refine(qi& q, datalog::rule_set& rules) { m_quantifier_inst.refine(q, rules); }
unsigned get_num_levels(func_decl* p);
expr_ref get_cover_delta(int level, func_decl* p_orig, func_decl* p);
@ -408,6 +399,8 @@ namespace pdr {
proof_ref get_proof() const;
model_node& get_root() const { return m_search.get_root(); }
};
};

23
src/muz_qe/pdr_dl_interface.cpp
View file

@ -25,6 +25,7 @@ Revision History:
#include "dl_mk_rule_inliner.h"
#include "dl_rule.h"
#include "dl_rule_transformer.h"
#include "dl_mk_extract_quantifiers.h"
#include "smt2parser.h"
#include "pdr_context.h"
#include "pdr_dl_interface.h"
@ -32,6 +33,7 @@ Revision History:
#include "dl_mk_slice.h"
#include "dl_mk_unfold.h"
#include "dl_mk_coalesce.h"
#include "pdr_quantifiers.h"
using namespace pdr;
@ -144,6 +146,12 @@ lbool dl_interface::query(expr * query) {
--num_unfolds;
}
}
// remove universal quantifiers from body.
datalog::mk_extract_quantifiers* extract_quantifiers = alloc(datalog::mk_extract_quantifiers, m_ctx);
datalog::rule_transformer extract_q_tr(m_ctx);
extract_q_tr.register_plugin(extract_quantifiers);
m_ctx.transform_rules(extract_q_tr, mc, pc);
IF_VERBOSE(2, m_ctx.display_rules(verbose_stream()););
m_pdr_rules.add_rules(m_ctx.get_rules());
@ -151,6 +159,7 @@ lbool dl_interface::query(expr * query) {
m_ctx.reopen();
m_ctx.replace_rules(old_rules);
quantifier_model_checker quantifier_mc(*m_context, m, extract_quantifiers->quantifiers(), m_pdr_rules);
m_context->set_proof_converter(pc);
m_context->set_model_converter(mc);
@ -163,14 +172,20 @@ lbool dl_interface::query(expr * query) {
return l_false;
}
lbool result;
while (true) {
try {
return m_context->solve();
result = m_context->solve();
if (result == l_true && extract_quantifiers->has_quantifiers()) {
if (quantifier_mc.check()) {
return l_true;
}
// else continue
}
catch (pdr::qi& q) {
m_context->refine(q, m_pdr_rules);
else {
return result;
}
}
}
expr_ref dl_interface::get_cover_delta(int level, func_decl* pred_orig) {

420
src/muz_qe/pdr_quantifiers.cpp
View file

@ -115,166 +115,21 @@ namespace pdr {
var_subst vs(m, false);
vs(q->get_expr(), binding.size(), binding.c_ptr(), e);
(*rep)(e);
m_rules.push_back(m_current_rule);
m_apps.push_back(to_app(e));
m_instantiated_rules.push_back(m_current_rule);
m_instantiations.push_back(to_app(e));
TRACE("pdr", tout << mk_pp(e, m) << "\n";);
}
void quantifier_model_checker::model_check(model_node& root) {
m_apps.reset();
m_rules.reset();
ptr_vector<model_node> nodes;
get_nodes(root, nodes);
for (unsigned i = nodes.size(); i > 0; ) {
--i;
model_check_node(*nodes[i]);
}
if (m_apps.empty()) {
return;
}
qi q(m);
for (unsigned i = 0; i < m_apps.size(); ++i) {
q.add(m_rules[i], m_apps[i].get());
}
throw q;
}
// As & not Body_i is satisfiable
// then instantiate with model for parameters to Body_i
bool quantifier_model_checker::find_instantiations(qinst& qi, unsigned level) {
bool quantifier_model_checker::find_instantiations(quantifier_ref_vector const& qs, unsigned level) {
return
find_instantiations_proof_based(qi, level); // ||
// find_instantiations_qe_based(qi, level);
find_instantiations_proof_based(qs, level); // ||
// find_instantiations_qe_based(qs, level);
}
bool quantifier_model_checker::find_instantiations_model_based(qinst& qi, unsigned level) {
bool found_instance = false;
expr_ref C(m);
front_end_params fparams;
smt::kernel solver(m, fparams);
solver.assert_expr(m_A);
for (unsigned i = 0; i < m_Bs.size(); ++i) {
expr_ref_vector fresh_vars(m);
quantifier* q = qi.quantifiers[i].get();
for (unsigned j = 0; j < q->get_num_decls(); ++j) {
fresh_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j)));
}
var_subst varsubst(m, false);
varsubst(m_Bs[i].get(), fresh_vars.size(), fresh_vars.c_ptr(), C);
TRACE("pdr", tout << "updated propagation formula: " << mk_pp(C,m) << "\n";);
solver.push();
// TBD: what to do with the different tags when unfolding the same predicate twice?
solver.assert_expr(m.mk_not(C));
lbool result = solver.check();
if (result == l_true) {
found_instance = true;
model_ref mr;
solver.get_model(mr);
TRACE("pdr", model_smt2_pp(tout, m, *mr, 0););
expr_ref_vector insts(m);
for (unsigned j = 0; j < fresh_vars.size(); ++j) {
expr* interp = mr->get_const_interp(to_app(fresh_vars[j].get())->get_decl());
if (interp) {
insts.push_back(interp);
}
else {
insts.push_back(fresh_vars[j].get());
}
TRACE("pdr", tout << mk_pp(insts.back(), m) << "\n";);
}
add_binding(q, insts);
}
solver.pop(1);
}
return found_instance;
}
//
// Build:
//
// A & forall x . B1 & forall y . B2 & ...
// =
// not exists x y . (!A or !B1 or !B2 or ...)
//
// Find an instance that satisfies formula.
// (or find all instances?)
//
bool quantifier_model_checker::find_instantiations_qe_based(qinst& qi, unsigned level) {
expr_ref_vector fmls(m), conjs(m), fresh_vars(m);
app_ref_vector all_vars(m);
expr_ref C(m);
qe::def_vector defs(m);
front_end_params fparams;
qe::expr_quant_elim qe(m, fparams);
for (unsigned i = 0; i < m_Bs.size(); ++i) {
quantifier* q = qi.quantifiers[i].get();
unsigned num_decls = q->get_num_decls();
unsigned offset = all_vars.size();
for (unsigned j = 0; j < num_decls; ++j) {
all_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j)));
}
var_subst varsubst(m, false);
varsubst(m_Bs[i].get(), num_decls, (expr**)(all_vars.c_ptr() + offset), C);
fmls.push_back(C);
}
conjs.push_back(m_A);
conjs.push_back(m.mk_not(m.mk_and(fmls.size(), fmls.c_ptr())));
// add previous instances.
expr* r = m.mk_and(m_Bs.size(), m_Bs.c_ptr());
m_trail.push_back(r);
expr* inst;
if (!m_bound.find(m_current_rule, r, inst)) {
TRACE("pdr", tout << "did not find: " << mk_pp(r, m) << "\n";);
m_trail.push_back(r);
inst = m.mk_true();
m_bound.insert(m_current_rule, r, inst);
}
else {
TRACE("pdr", tout << "blocking: " << mk_pp(inst, m) << "\n";);
conjs.push_back(inst);
}
C = m.mk_and(conjs.size(), conjs.c_ptr());
lbool result = qe.first_elim(all_vars.size(), all_vars.c_ptr(), C, defs);
TRACE("pdr", tout << mk_pp(C.get(), m) << "\n" << result << "\n";);
if (result != l_true) {
return false;
}
inst = m.mk_and(inst, m.mk_not(C));
m_trail.push_back(inst);
m_bound.insert(m_current_rule, r, inst);
TRACE("pdr",
tout << "Instantiating\n";
for (unsigned i = 0; i < defs.size(); ++i) {
tout << defs.var(i)->get_name() << " " << mk_pp(defs.def(i), m) << "\n";
}
);
expr_substitution sub(m);
for (unsigned i = 0; i < defs.size(); ++i) {
sub.insert(m.mk_const(defs.var(i)), defs.def(i));
}
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
rep->set_substitution(&sub);
for (unsigned i = 0; i < all_vars.size(); ++i) {
expr_ref tmp(all_vars[i].get(), m);
(*rep)(tmp);
all_vars[i] = to_app(tmp);
}
unsigned offset = 0;
for (unsigned i = 0; i < m_Bs.size(); ++i) {
quantifier* q = qi.quantifiers[i].get();
unsigned num_decls = q->get_num_decls();
expr_ref_vector new_binding(m);
for (unsigned j = 0; j < num_decls; ++j) {
new_binding.push_back(all_vars[offset+j].get());
}
offset += num_decls;
add_binding(q, new_binding);
}
return true;
}
class collect_insts {
ast_manager& m;
@ -322,7 +177,7 @@ namespace pdr {
};
bool quantifier_model_checker::find_instantiations_proof_based(qinst& qi, unsigned level) {
bool quantifier_model_checker::find_instantiations_proof_based(quantifier_ref_vector const& qs, unsigned level) {
bool found_instance = false;
TRACE("pdr", tout << mk_pp(m_A,m) << "\n";);
@ -336,7 +191,7 @@ namespace pdr {
expr_ref C(m);
fmls.push_back(tr(m_A.get()));
for (unsigned i = 0; i < m_Bs.size(); ++i) {
C = m.update_quantifier(qi.quantifiers[i].get(), m_Bs[i].get());
C = m.update_quantifier(qs[i], m_Bs[i].get());
fmls.push_back(tr(C.get()));
}
TRACE("pdr",
@ -355,8 +210,8 @@ namespace pdr {
}
map<symbol, quantifier*, symbol_hash_proc, symbol_eq_proc> qid_map;
quantifier* q;
for (unsigned i = 0; i < qi.quantifiers.size(); ++i) {
q = qi.quantifiers[i].get();
for (unsigned i = 0; i < qs.size(); ++i) {
q = qs[i];
qid_map.insert(q->get_qid(), q);
}
@ -391,7 +246,7 @@ namespace pdr {
if (collector.size() == 0) {
// Try to create dummy instances.
for (unsigned i = 0; i < m_Bs.size(); ++i) {
q = qi.quantifiers[i].get();
q = qs[i];
expr_ref_vector binding(m);
for (unsigned j = 0; j < q->get_num_decls(); ++j) {
binding.push_back(m.mk_fresh_const("B", q->get_decl_sort(j)));
@ -403,7 +258,6 @@ namespace pdr {
return found_instance;
}
void quantifier_model_checker::model_check_node(model_node& node) {
TRACE("pdr", node.display(tout, 0););
pred_transformer& pt = node.pt();
@ -411,9 +265,6 @@ namespace pdr {
expr_ref A(m), B(m), C(m);
expr_ref_vector As(m);
m_Bs.reset();
if (!pt.has_quantifiers()) {
return;
}
//
// nodes from leaves that are repeated
// inside the search tree don't have models.
@ -427,10 +278,12 @@ namespace pdr {
if (!m_current_rule) {
return;
}
qinst* qi = pt.get_quantifiers(m_current_rule);
if (!qi) {
quantifier_ref_vector* qis = 0;
m_quantifiers.find(m_current_rule, qis);
if (!qis) {
return;
}
}
unsigned level = node.level();
unsigned previous_level = (level == 0)?0:(level-1);
@ -440,42 +293,69 @@ namespace pdr {
m_A = pm.mk_and(As);
// Add quantifiers:
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
for (unsigned j = 0; j < qi->quantifiers.size(); ++j) {
quantifier* q = qi->quantifiers[j].get();
app* a = to_app(q->get_expr());
func_decl* f = a->get_decl();
pred_transformer& pt2 = m_ctx.get_pred_transformer(f);
B = pt2.get_formulas(previous_level, true);
TRACE("pdr", tout << mk_pp(B, m) << "\n";);
expr_substitution sub(m);
for (unsigned i = 0; i < a->get_num_args(); ++i) {
expr* v = m.mk_const(pm.o2n(pt2.sig(i),0));
sub.insert(v, a->get_arg(i));
{
datalog::scoped_no_proof _no_proof(m);
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
for (unsigned j = 0; j < qis->size(); ++j) {
quantifier* q = (*qis)[j].get();
app* a = to_app(q->get_expr());
func_decl* f = a->get_decl();
pred_transformer& pt2 = m_ctx.get_pred_transformer(f);
B = pt2.get_formulas(previous_level, true);
expr_substitution sub(m);
expr_ref_vector refs(m);
for (unsigned i = 0; i < a->get_num_args(); ++i) {
expr* v = m.mk_const(pm.o2n(pt2.sig(i),0));
sub.insert(v, a->get_arg(i));
refs.push_back(v);
}
rep->set_substitution(&sub);
(*rep)(B);
app_ref_vector& inst = pt.get_inst(m_current_rule);
ptr_vector<app>& aux_vars = pt.get_aux_vars(*m_current_rule);
pt.ground_free_vars(B, inst, aux_vars);
var_subst vs(m, false);
vs(B, inst.size(), (expr*const*)inst.c_ptr(), B);
m_Bs.push_back(B);
}
rep->set_substitution(&sub);
// TBD: exclude previous bindings here.
(*rep)(B);
m_Bs.push_back(B);
TRACE("pdr",
tout << mk_pp(q, m) << "\n";
tout << "propagation formula: " << mk_pp(B, m) << "\n";);
}
find_instantiations(*qi, level);
TRACE("pdr",
tout << "A:\n" << mk_pp(m_A, m) << "\n";
tout << "B:\n";
for (unsigned i = 0; i < m_Bs.size(); ++i) {
tout << mk_pp((*qis)[i].get(), m) << "\n" << mk_pp(m_Bs[i].get(), m) << "\n";
}
);
find_instantiations(*qis, level);
}
void quantifier_model_checker::refine(qi& q, datalog::rule_set& rules) {
bool quantifier_model_checker::model_check(model_node& root) {
m_instantiations.reset();
m_instantiated_rules.reset();
ptr_vector<model_node> nodes;
get_nodes(root, nodes);
for (unsigned i = nodes.size(); i > 0; ) {
--i;
model_check_node(*nodes[i]);
}
return m_instantiations.empty();
}
void quantifier_model_checker::refine() {
IF_VERBOSE(1, verbose_stream() << "instantiating quantifiers\n";);
datalog::rule_manager& rule_m = rules.get_rule_manager();
datalog::rule_set new_rules(rules.get_context());
datalog::rule_set::iterator it = rules.begin(), end = rules.end();
datalog::rule_manager& rule_m = m_rules.get_rule_manager();
datalog::rule_set new_rules(m_rules.get_context());
datalog::rule_set::iterator it = m_rules.begin(), end = m_rules.end();
for (; it != end; ++it) {
datalog::rule* r = *it;
app_ref_vector body(m);
for (unsigned i = 0; i < q.size(); ++i) {
if (r == q.get_rule(i)) {
body.push_back(q.get_app(i));
expr_ref_vector body(m);
for (unsigned i = 0; i < m_instantiations.size(); ++i) {
if (r == m_instantiated_rules[i]) {
body.push_back(m_instantiations[i].get());
}
}
if (body.empty()) {
@ -485,19 +365,165 @@ namespace pdr {
for (unsigned i = 0; i < r->get_tail_size(); ++i) {
body.push_back(r->get_tail(i));
}
quantifier_ref_vector* qs = 0;
m_quantifiers.find(r, qs);
m_quantifiers.remove(r);
datalog::rule_ref_vector rules(rule_m);
expr_ref rule(m.mk_implies(m.mk_and(body.size(), (expr*const*)body.c_ptr()), r->get_head()), m);
expr_ref rule(m.mk_implies(m.mk_and(body.size(), body.c_ptr()), r->get_head()), m);
rule_m.mk_rule(rule, rules, r->name());
for (unsigned i = 0; i < rules.size(); ++i) {
new_rules.add_rule(rules[i].get());
m_quantifiers.insert(rules[i].get(), qs);
}
}
}
new_rules.close();
rules.reset();
rules.add_rules(new_rules);
rules.close();
m_ctx.update_rules(rules);
TRACE("pdr", rules.display(tout););
m_rules.reset();
m_rules.add_rules(new_rules);
m_rules.close();
m_ctx.update_rules(m_rules);
TRACE("pdr", m_rules.display(tout););
}
bool quantifier_model_checker::check() {
if (model_check(m_ctx.get_root())) {
return true;
}
refine();
return false;
}
};
#if 0
//
// Build:
//
// A & forall x . B1 & forall y . B2 & ...
// =
// not exists x y . (!A or !B1 or !B2 or ...)
//
// Find an instance that satisfies formula.
// (or find all instances?)
//
bool quantifier_model_checker::find_instantiations_qe_based(quantifier_ref_vector const& qs, unsigned level) {
expr_ref_vector fmls(m), conjs(m), fresh_vars(m);
app_ref_vector all_vars(m);
expr_ref C(m);
qe::def_vector defs(m);
front_end_params fparams;
qe::expr_quant_elim qe(m, fparams);
for (unsigned i = 0; i < m_Bs.size(); ++i) {
quantifier* q = qs[i];
unsigned num_decls = q->get_num_decls();
unsigned offset = all_vars.size();
for (unsigned j = 0; j < num_decls; ++j) {
all_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j)));
}
var_subst varsubst(m, false);
varsubst(m_Bs[i].get(), num_decls, (expr**)(all_vars.c_ptr() + offset), C);
fmls.push_back(C);
}
conjs.push_back(m_A);
conjs.push_back(m.mk_not(m.mk_and(fmls.size(), fmls.c_ptr())));
// add previous instances.
expr* r = m.mk_and(m_Bs.size(), m_Bs.c_ptr());
m_trail.push_back(r);
expr* inst;
if (!m_bound.find(m_current_rule, r, inst)) {
TRACE("pdr", tout << "did not find: " << mk_pp(r, m) << "\n";);
m_trail.push_back(r);Newton Sanches
inst = m.mk_true();
m_bound.insert(m_current_rule, r, inst);
}
else {
TRACE("pdr", tout << "blocking: " << mk_pp(inst, m) << "\n";);
conjs.push_back(inst);
}
C = m.mk_and(conjs.size(), conjs.c_ptr());
lbool result = qe.first_elim(all_vars.size(), all_vars.c_ptr(), C, defs);
TRACE("pdr", tout << mk_pp(C.get(), m) << "\n" << result << "\n";);
if (result != l_true) {
return false;
}
inst = m.mk_and(inst, m.mk_not(C));
m_trail.push_back(inst);
m_bound.insert(m_current_rule, r, inst);
TRACE("pdr",
tout << "Instantiating\n";
for (unsigned i = 0; i < defs.size(); ++i) {
tout << defs.var(i)->get_name() << " " << mk_pp(defs.def(i), m) << "\n";
}
);
expr_substitution sub(m);
for (unsigned i = 0; i < defs.size(); ++i) {
sub.insert(m.mk_const(defs.var(i)), defs.def(i));
}
scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
rep->set_substitution(&sub);
for (unsigned i = 0; i < all_vars.size(); ++i) {
expr_ref tmp(all_vars[i].get(), m);
(*rep)(tmp);
all_vars[i] = to_app(tmp);
}
unsigned offset = 0;
for (unsigned i = 0; i < m_Bs.size(); ++i) {
quantifier* q = qs[i];
unsigned num_decls = q->get_num_decls();
expr_ref_vector new_binding(m);
for (unsigned j = 0; j < num_decls; ++j) {
new_binding.push_back(all_vars[offset+j].get());
}
offset += num_decls;
add_binding(q, new_binding);
}
return true;
}
bool quantifier_model_checker::find_instantiations_model_based(quantifier_ref_vector const& qs, unsigned level) {
bool found_instance = false;
expr_ref C(m);
front_end_params fparams;
smt::kernel solver(m, fparams);
solver.assert_expr(m_A);
for (unsigned i = 0; i < m_Bs.size(); ++i) {
expr_ref_vector fresh_vars(m);
quantifier* q = qs[i];
for (unsigned j = 0; j < q->get_num_decls(); ++j) {
fresh_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j)));
}
var_subst varsubst(m, false);
varsubst(m_Bs[i].get(), fresh_vars.size(), fresh_vars.c_ptr(), C);
TRACE("pdr", tout << "updated propagation formula: " << mk_pp(C,m) << "\n";);
solver.push();
// TBD: what to do with the different tags when unfolding the same predicate twice?
solver.assert_expr(m.mk_not(C));
lbool result = solver.check();
if (result == l_true) {
found_instance = true;
model_ref mr;
solver.get_model(mr);
TRACE("pdr", model_smt2_pp(tout, m, *mr, 0););
expr_ref_vector insts(m);
for (unsigned j = 0; j < fresh_vars.size(); ++j) {
expr* interp = mr->get_const_interp(to_app(fresh_vars[j].get())->get_decl());
if (interp) {
insts.push_back(interp);
}
else {
insts.push_back(fresh_vars[j].get());
}
TRACE("pdr", tout << mk_pp(insts.back(), m) << "\n";);
}
add_binding(q, insts);
}
solver.pop(1);
}
return found_instance;
}
#endif

63
src/muz_qe/pdr_quantifiers.h
View file

@ -33,52 +33,31 @@ namespace pdr {
class model_node;
class pred_transformer;
class context;
struct qinst {
quantifier_ref_vector quantifiers; // quantifiers in rule body.
func_decl_ref_vector predicates; // predicates in order of bindings.
expr_ref_vector bindings; // the actual instantiations of the predicates
qinst(ast_manager& m): quantifiers(m), predicates(m), bindings(m) {}
};
class qi {
ptr_vector<datalog::rule const> m_rules;
app_ref_vector m_apps;
public:
qi(ast_manager& m) : m_apps(m) {}
void add(datalog::rule const* r, app* a) {
m_rules.push_back(r);
m_apps.push_back(a);
}
unsigned size() const { return m_rules.size(); }
datalog::rule const* get_rule(unsigned i) const { return m_rules[i]; }
app* get_app(unsigned i) const { return m_apps[i]; }
};
class quantifier_model_checker {
context& m_ctx;
ast_manager& m;
obj_pair_map<datalog::rule const, expr, expr*> m_bound;
obj_map<datalog::rule const, quantifier_ref_vector*>& m_quantifiers;
datalog::rule_set& m_rules;
expr_ref_vector m_trail;
expr_ref m_A;
expr_ref_vector m_Bs;
pred_transformer* m_current_pt;
datalog::rule const* m_current_rule;
model_node* m_current_node;
ptr_vector<datalog::rule const> m_rules;
app_ref_vector m_apps;
app_ref_vector m_instantiations;
ptr_vector<datalog::rule const> m_instantiated_rules;
void model_check_node(model_node& node);
bool find_instantiations(qinst& qi, unsigned level);
bool find_instantiations(quantifier_ref_vector const& qs, unsigned level);
bool find_instantiations_model_based(qinst& qi, unsigned level);
bool find_instantiations_model_based(quantifier_ref_vector const& qs, unsigned level);
bool find_instantiations_proof_based(qinst& qi, unsigned level);
bool find_instantiations_proof_based(quantifier_ref_vector const& qs, unsigned level);
bool find_instantiations_qe_based(qinst& qi, unsigned level);
bool find_instantiations_qe_based(quantifier_ref_vector const& qs, unsigned level);
void add_binding(quantifier* q, expr_ref_vector& binding);
@ -88,12 +67,8 @@ namespace pdr {
void generalize_binding(expr_ref_vector const& binding, unsigned idx, expr_ref_vector& new_binding, vector<expr_ref_vector>& bindings);
public:
quantifier_model_checker(context& ctx, ast_manager& m):
m_ctx(ctx),
m(m), m_trail(m), m_A(m), m_Bs(m),
m_current_pt(0), m_current_rule(0),
m_current_node(0), m_apps(m) {}
void refine();
/**
\brief model check a potential model against quantifiers in bodies of rules.
@ -102,9 +77,23 @@ namespace pdr {
'false' and a set of instantiations that contradict the current model.
*/
void model_check(model_node& root);
bool model_check(model_node& root);
void refine(qi& q, datalog::rule_set& rules);
public:
quantifier_model_checker(
context& ctx,
ast_manager& m,
obj_map<datalog::rule const, quantifier_ref_vector*>& quantifiers,
datalog::rule_set& rules) :
m_ctx(ctx),
m(m),
m_quantifiers(quantifiers),
m_rules(rules),
m_trail(m), m_A(m), m_Bs(m),
m_current_pt(0), m_current_rule(0),
m_current_node(0), m_instantiations(m) {}
bool check();
};
};

7
src/smt/asserted_formulas.cpp
View file

@ -40,7 +40,6 @@ Revision History:
#include"der.h"
#include"elim_bounds.h"
#include"warning.h"
#include"eager_bit_blaster.h"
#include"bit2int.h"
#include"distribute_forall.h"
#include"quasi_macros.h"
@ -340,13 +339,9 @@ void asserted_formulas::reduce() {
INVOKE(m_params.m_quasi_macros && has_quantifiers(), apply_quasi_macros());
INVOKE(m_params.m_simplify_bit2int, apply_bit2int());
INVOKE(m_params.m_eliminate_bounds && has_quantifiers(), cheap_quant_fourier_motzkin());
INVOKE(!m_params.m_bb_eager && has_quantifiers() && m_params.m_ematching, infer_patterns());
INVOKE(m_params.m_max_bv_sharing && has_bv(), max_bv_sharing());
INVOKE(m_params.m_bb_quantifiers, elim_bvs_from_quantifiers());
INVOKE(m_params.m_bb_eager, apply_eager_bit_blaster());
INVOKE(m_params.m_bb_eager && m_params.m_nnf_cnf, nnf_cnf()); // bit-blaster destroys CNF
INVOKE(m_params.m_bb_quantifiers && m_params.m_der && has_quantifiers(), apply_der()); // bit-vector elimination + bit-blasting creates new opportunities for der.
INVOKE(m_params.m_bb_eager && has_quantifiers() && m_params.m_ematching, infer_patterns());
// temporary HACK: make sure that arith & bv are list-assoc
// this may destroy some simplification steps such as max_bv_sharing
reduce_asserted_formulas();
@ -1434,8 +1429,6 @@ bool asserted_formulas::quant_elim() {
return false;
}
MK_SIMPLIFIER(apply_eager_bit_blaster, eager_bit_blaster functor(m_manager, m_params), "eager_bb", "eager bit blasting", false);
MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m_manager), "bv_elim", "eliminate bit-vectors from quantifiers", true);
#define LIFT_ITE(NAME, FUNCTOR, MSG) \

1
src/smt/asserted_formulas.h
View file

@ -94,7 +94,6 @@ class asserted_formulas {
void apply_demodulators();
void apply_quasi_macros();
void nnf_cnf();
bool apply_eager_bit_blaster();
void infer_patterns();
void eliminate_term_ite();
void reduce_and_solve();