mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

Removed (some) dead parameters. Added doxygen documentation for the whole code base.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-22 10:06:24 -08:00
parent 66b02eb88d
commit 5e7436cb50
19 changed files with 1105 additions and 845 deletions
Download patch file Download diff file Expand all files Collapse all files

15
doc/README
View file

@ -7,5 +7,16 @@ To generate the API documentation for the C, .NET and Python APIs, we must execu
We must have doxygen installed in our system. We must have doxygen installed in our system.
The documentation will be stored in the subdirectory './html'. The documentation will be stored in the subdirectory './api/html'.
The main file is './html/index.html' The main file is './api/html/index.html'
Code documentation
------------------
To generate documentation for the Z3 code, we must execute
doxygen z3code.dox
The documentation will be store in the subdirectory './code/html'.
The main file is './code/html/index.html'

2
doc/update_website.cmd
View file

@ -1,4 +1,4 @@
REM Script for updating the website containing the Z3 API documentation. REM Script for updating the website containing the Z3 API documentation.
REM You must be inside the Microsoft network to execute this script, and REM You must be inside the Microsoft network to execute this script, and
REM robocopy must be in your PATH. REM robocopy must be in your PATH.
robocopy /S html \\research\root\web\external\en-us\UM\redmond\projects\z3 robocopy /S api\html \\research\root\web\external\en-us\UM\redmond\projects\z3

2
doc/z3.dox
View file

@ -38,7 +38,7 @@ PROJECT_NUMBER =
# If a relative path is entered, it will be relative to the location # If a relative path is entered, it will be relative to the location
# where doxygen was started. If left blank the current directory will be used. # where doxygen was started. If left blank the current directory will be used.
OUTPUT_DIRECTORY = . OUTPUT_DIRECTORY = api
# If the CREATE_SUBDIRS tag is set to YES, then doxygen will create # If the CREATE_SUBDIRS tag is set to YES, then doxygen will create
# 4096 sub-directories (in 2 levels) under the output directory of each output # 4096 sub-directories (in 2 levels) under the output directory of each output

1081
doc/z3code.dox Normal file
View file

File diff suppressed because it is too large Load diff

33
src/api/api_arith.cpp
View file

@ -101,27 +101,14 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
if (mk_c(c)->fparams().m_pre_simplify_expr) { expr* r = to_expr(args[0]);
// Do not use logging here... the function is implemented using API primitives for (unsigned i = 1; i < num_args; ++i) {
Z3_ast m1 = Z3_mk_int(c, -1, Z3_get_sort(c, args[0])); expr* args1[2] = { r, to_expr(args[i]) };
Z3_ast args1[2] = { args[0], 0 }; r = mk_c(c)->m().mk_app(mk_c(c)->get_arith_fid(), OP_SUB, 0, 0, 2, args1);
for (unsigned i = 1; i < num_args; ++i) { check_sorts(c, r);
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));
} }
mk_c(c)->save_ast_trail(r);
RETURN_Z3(of_expr(r));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -129,12 +116,6 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_mk_unary_minus(c, n); LOG_Z3_mk_unary_minus(c, n);
RESET_ERROR_CODE(); 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); MK_UNARY_BODY(Z3_mk_unary_minus, mk_c(c)->get_arith_fid(), OP_UMINUS, SKIP);
Z3_CATCH_RETURN(0); 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; Z3_TRY;
LOG_Z3_mk_bvsub(c, n1, n2); LOG_Z3_mk_bvsub(c, n1, n2);
RESET_ERROR_CODE(); 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); MK_BINARY_BODY(Z3_mk_bvsub, mk_c(c)->get_bv_fid(), OP_BSUB, SKIP);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -294,12 +288,6 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_TRY; Z3_TRY;
LOG_Z3_mk_bvneg(c, n); LOG_Z3_mk_bvneg(c, n);
RESET_ERROR_CODE(); 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); MK_UNARY_BODY(Z3_mk_bvneg, mk_c(c)->get_bv_fid(), OP_BNEG, SKIP);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }

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" #include"ini_file.h"
struct bit_blaster_params { struct bit_blaster_params {
bool m_bb_eager;
bool m_bb_ext_gates; bool m_bb_ext_gates;
bool m_bb_quantifiers; bool m_bb_quantifiers;
bit_blaster_params(): bit_blaster_params():
m_bb_eager(false),
m_bb_ext_gates(false), m_bb_ext_gates(false),
m_bb_quantifiers(false) { m_bb_quantifiers(false) {
} }
void register_params(ini_params & p) { 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_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"); 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) { void front_end_params::register_params(ini_params & p) {
p.register_param_vector(m_param_vector.get()); p.register_param_vector(m_param_vector.get());
preprocessor_params::register_params(p); preprocessor_params::register_params(p);
spc_params::register_params(p);
smt_params::register_params(p); smt_params::register_params(p);
parser_params::register_params(p); parser_params::register_params(p);
arith_simplifier_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); model_params::register_params(p);
p.register_unsigned_param("MAX_COUNTEREXAMPLES", m_max_num_cex, p.register_unsigned_param("MAX_COUNTEREXAMPLES", m_max_num_cex,
"set the maximum number of counterexamples when using Simplify front end"); "set the maximum number of counterexamples when using Simplify front end");
@ -45,7 +42,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_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_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_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("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"); 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"ini_file.h"
#include"ast.h" #include"ast.h"
#include"preprocessor_params.h" #include"preprocessor_params.h"
#include"spc_params.h"
#include"smt_params.h" #include"smt_params.h"
#include"pp_params.h" #include"pp_params.h"
#include"parser_params.h" #include"parser_params.h"
#include"arith_simplifier_params.h" #include"arith_simplifier_params.h"
#include"z3_solver_params.h"
#include"model_params.h" #include"model_params.h"
enum engine { struct front_end_params : public preprocessor_params, public smt_params, public parser_params,
ENG_SMT, public arith_simplifier_params, public model_params
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
{ {
ref<param_vector> m_param_vector; ref<param_vector> m_param_vector;
engine m_engine;
unsigned m_max_num_cex; // maximum number of counterexamples unsigned m_max_num_cex; // maximum number of counterexamples
bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples. 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_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.
@ -66,7 +57,6 @@ struct front_end_params : public preprocessor_params, public spc_params, public
bool m_trace; bool m_trace;
std::string m_trace_file_name; std::string m_trace_file_name;
std::fstream* m_trace_stream; std::fstream* m_trace_stream;
bool m_ignore_setparameter;
bool m_async_commands; bool m_async_commands;
bool m_display_config; bool m_display_config;
bool m_user_theory_preprocess_axioms; bool m_user_theory_preprocess_axioms;
@ -75,7 +65,6 @@ struct front_end_params : public preprocessor_params, public spc_params, public
front_end_params(): front_end_params():
m_param_vector(alloc(param_vector, this)), m_param_vector(alloc(param_vector, this)),
m_engine(ENG_SMT),
m_max_num_cex(1), m_max_num_cex(1),
m_at_labels_cex(false), m_at_labels_cex(false),
m_check_at_labels(false), m_check_at_labels(false),
@ -109,7 +98,6 @@ struct front_end_params : public preprocessor_params, public spc_params, public
m_trace(false), m_trace(false),
m_trace_file_name("z3.log"), m_trace_file_name("z3.log"),
m_trace_stream(NULL), m_trace_stream(NULL),
m_ignore_setparameter(false),
m_async_commands(true), m_async_commands(true),
m_display_config(false), m_display_config(false),
m_user_theory_preprocess_axioms(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_ */

7
src/smt/asserted_formulas.cpp
View file

@ -40,7 +40,6 @@ Revision History:
#include"der.h" #include"der.h"
#include"elim_bounds.h" #include"elim_bounds.h"
#include"warning.h" #include"warning.h"
#include"eager_bit_blaster.h"
#include"bit2int.h" #include"bit2int.h"
#include"distribute_forall.h" #include"distribute_forall.h"
#include"quasi_macros.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_quasi_macros && has_quantifiers(), apply_quasi_macros());
INVOKE(m_params.m_simplify_bit2int, apply_bit2int()); INVOKE(m_params.m_simplify_bit2int, apply_bit2int());
INVOKE(m_params.m_eliminate_bounds && has_quantifiers(), cheap_quant_fourier_motzkin()); 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_max_bv_sharing && has_bv(), max_bv_sharing());
INVOKE(m_params.m_bb_quantifiers, elim_bvs_from_quantifiers()); 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_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 // temporary HACK: make sure that arith & bv are list-assoc
// this may destroy some simplification steps such as max_bv_sharing // this may destroy some simplification steps such as max_bv_sharing
reduce_asserted_formulas(); reduce_asserted_formulas();
@ -1434,8 +1429,6 @@ bool asserted_formulas::quant_elim() {
return false; 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); 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) \ #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_demodulators();
void apply_quasi_macros(); void apply_quasi_macros();
void nnf_cnf(); void nnf_cnf();
bool apply_eager_bit_blaster();
void infer_patterns(); void infer_patterns();
void eliminate_term_ite(); void eliminate_term_ite();
void reduce_and_solve(); void reduce_and_solve();