mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Add support for abs (absolute value) function in theory arith (it is part of the SMT-LIB 2.0 standard)

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-02-03 15:28:56 -08:00
parent 490905e320
commit c4f762028f
6 changed files with 31 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/ast/arith_decl_plugin.cpp
View file

@ -194,6 +194,9 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
MK_OP(m_r_power_decl, "^", OP_POWER, r);
MK_OP(m_i_power_decl, "^", OP_POWER, i);
MK_UNARY(m_i_abs_decl, "abs", OP_ABS, i);
MK_UNARY(m_r_abs_decl, "abs", OP_ABS, r);
MK_UNARY(m_sin_decl, "sin", OP_SIN, r);
MK_UNARY(m_cos_decl, "cos", OP_COS, r);
MK_UNARY(m_tan_decl, "tan", OP_TAN, r);
@ -263,6 +266,8 @@ arith_decl_plugin::arith_decl_plugin():
m_is_int_decl(0),
m_r_power_decl(0),
m_i_power_decl(0),
m_r_abs_decl(0),
m_i_abs_decl(0),
m_sin_decl(0),
m_cos_decl(0),
m_tan_decl(0),
@ -320,6 +325,8 @@ void arith_decl_plugin::finalize() {
DEC_REF(m_is_int_decl);
DEC_REF(m_i_power_decl);
DEC_REF(m_r_power_decl);
DEC_REF(m_i_abs_decl);
DEC_REF(m_r_abs_decl);
DEC_REF(m_sin_decl);
DEC_REF(m_cos_decl);
DEC_REF(m_tan_decl);
@ -372,6 +379,7 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) {
case OP_TO_INT: return m_to_int_decl;
case OP_IS_INT: return m_is_int_decl;
case OP_POWER: return is_real ? m_r_power_decl : m_i_power_decl;
case OP_ABS: return is_real ? m_r_abs_decl : m_i_abs_decl;
case OP_SIN: return m_sin_decl;
case OP_COS: return m_cos_decl;
case OP_TAN: return m_tan_decl;
@ -538,6 +546,7 @@ void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
op_names.push_back(builtin_name("to_real",OP_TO_REAL));
op_names.push_back(builtin_name("to_int",OP_TO_INT));
op_names.push_back(builtin_name("is_int",OP_IS_INT));
op_names.push_back(builtin_name("abs", OP_ABS));
if (logic == symbol::null) {
op_names.push_back(builtin_name("^", OP_POWER));
op_names.push_back(builtin_name("sin", OP_SIN));

4
src/ast/arith_decl_plugin.h
View file

@ -51,6 +51,7 @@ enum arith_op_kind {
OP_TO_REAL,
OP_TO_INT,
OP_IS_INT,
OP_ABS,
OP_POWER,
// hyperbolic and trigonometric functions
OP_SIN,
@ -121,6 +122,9 @@ protected:
func_decl * m_r_power_decl;
func_decl * m_i_power_decl;
func_decl * m_r_abs_decl;
func_decl * m_i_abs_decl;
func_decl * m_sin_decl;
func_decl * m_cos_decl;
func_decl * m_tan_decl;

6
src/ast/rewriter/arith_rewriter.cpp
View file

@ -70,6 +70,7 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
case OP_TO_INT: SASSERT(num_args == 1); st = mk_to_int_core(args[0], result); break;
case OP_IS_INT: SASSERT(num_args == 1); st = mk_is_int(args[0], result); break;
case OP_POWER: SASSERT(num_args == 2); st = mk_power_core(args[0], args[1], result); break;
case OP_ABS: SASSERT(num_args == 1); st = mk_abs_core(args[0], result); break;
case OP_SIN: SASSERT(num_args == 1); st = mk_sin_core(args[0], result); break;
case OP_COS: SASSERT(num_args == 1); st = mk_cos_core(args[0], result); break;
case OP_TAN: SASSERT(num_args == 1); st = mk_tan_core(args[0], result); break;
@ -1024,6 +1025,11 @@ br_status arith_rewriter::mk_is_int(expr * arg, expr_ref & result) {
}
}
br_status arith_rewriter::mk_abs_core(expr * arg, expr_ref & result) {
result = m().mk_ite(m_util.mk_ge(arg, m_util.mk_numeral(rational(0), m_util.is_int(arg))), arg, m_util.mk_uminus(arg));
return BR_REWRITE2;
}
void arith_rewriter::set_cancel(bool f) {
m_util.set_cancel(f);
}

2
src/ast/rewriter/arith_rewriter.h
View file

@ -131,6 +131,8 @@ public:
}
void mk_gt(expr * arg1, expr * arg2, expr_ref & result) { mk_gt_core(arg1, arg2, result); }
br_status mk_abs_core(expr * arg, expr_ref & result);
br_status mk_div_core(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_idiv_core(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_mod_core(expr * arg1, expr * arg2, expr_ref & result);

9
src/ast/simplifier/arith_simplifier_plugin.cpp
View file

@ -404,6 +404,7 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co
case OP_TO_INT: SASSERT(num_args == 1); mk_to_int(args[0], result); break;
case OP_IS_INT: SASSERT(num_args == 1); mk_is_int(args[0], result); break;
case OP_POWER: return false;
case OP_ABS: SASSERT(num_args == 1); mk_abs(args[0], result); break;
case OP_IRRATIONAL_ALGEBRAIC_NUM: return false;
default:
UNREACHABLE();
@ -413,6 +414,14 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co
return true;
}
void arith_simplifier_plugin::mk_abs(expr * arg, expr_ref & result) {
expr_ref c(m_manager);
expr_ref m_arg(m_manager);
mk_uminus(arg, m_arg);
mk_ge(arg, m_util.mk_numeral(rational(0), m_util.is_int(arg)), c);
m_bsimp.mk_ite(c, arg, m_arg, result);
}
bool arith_simplifier_plugin::is_arith_term(expr * n) const {
return n->get_kind() == AST_APP && to_app(n)->get_family_id() == m_fid;
}

1
src/ast/simplifier/arith_simplifier_plugin.h
View file

@ -82,6 +82,7 @@ public:
void mk_to_real(expr * arg, expr_ref & result);
void mk_to_int(expr * arg, expr_ref & result);
void mk_is_int(expr * arg, expr_ref & result);
void mk_abs(expr * arg, expr_ref & result);
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);