From f238720b768ad9262dc7976c907672383195afe7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 27 Jun 2013 09:19:23 -0700 Subject: [PATCH 1/4] Cherry-pick goodies from mcsat branch Signed-off-by: Leonardo de Moura --- src/ast/ast_util.cpp | 53 ++++++++++++++++++++++++++++++++++++++++++++ src/ast/ast_util.h | 31 ++++++++++++++++++++++++++ 2 files changed, 84 insertions(+) diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp index 8b0b3fa04..d77deca01 100644 --- a/src/ast/ast_util.cpp +++ b/src/ast/ast_util.cpp @@ -1,3 +1,21 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + ast_util.cpp + +Abstract: + + Helper functions + +Author: + + Leonardo de Moura (leonardo) 2007-06-08. + +Revision History: + +--*/ #include "ast_util.h" app * mk_list_assoc_app(ast_manager & m, func_decl * f, unsigned num_args, expr * const * args) { @@ -138,3 +156,38 @@ expr * get_clause_literal(ast_manager & m, expr * cls, unsigned idx) { SASSERT(m.is_or(cls)); return to_app(cls)->get_arg(idx); } + +expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args) { + if (num_args == 0) + return m.mk_true(); + else if (num_args == 1) + return args[0]; + else + return m.mk_and(num_args, args); +} + +expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args) { + if (num_args == 0) + return m.mk_false(); + else if (num_args == 1) + return args[0]; + else + return m.mk_or(num_args, args); +} + +expr * mk_not(ast_manager & m, expr * arg) { + expr * atom; + if (m.is_not(arg, atom)) + return atom; + else + return m.mk_not(arg); +} + +expr * expand_distinct(ast_manager & m, unsigned num_args, expr * const * args) { + expr_ref_buffer new_diseqs(m); + for (unsigned i = 0; i < num_args; i++) { + for (unsigned j = i + 1; j < num_args; j++) + new_diseqs.push_back(m.mk_not(m.mk_eq(args[i], args[j]))); + } + return mk_and(m, new_diseqs.size(), new_diseqs.c_ptr()); +} diff --git a/src/ast/ast_util.h b/src/ast/ast_util.h index c7f54da01..1e813b1b0 100644 --- a/src/ast/ast_util.h +++ b/src/ast/ast_util.h @@ -95,5 +95,36 @@ bool is_clause(ast_manager & m, expr * n); unsigned get_clause_num_literals(ast_manager & m, expr * cls); expr * get_clause_literal(ast_manager & m, expr * cls, unsigned idx); +// ----------------------------------- +// +// Goodies for creating Boolean expressions +// +// ----------------------------------- + +/** + Return (and args[0] ... args[num_args-1]) if num_args >= 2 + Return args[0] if num_args == 1 + Return true if num_args == 0 + */ +expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args); + +/** + Return (or args[0] ... args[num_args-1]) if num_args >= 2 + Return args[0] if num_args == 1 + Return false if num_args == 0 + */ +expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args); + +/** + Return a if arg = (not a) + Retur (not arg) otherwise + */ +expr * mk_not(ast_manager & m, expr * arg); + +/** + Return the expression (and (not (= args[0] args[1])) (not (= args[0] args[2])) ... (not (= args[num_args-2] args[num_args-1]))) +*/ +expr * expand_distinct(ast_manager & m, unsigned num_args, expr * const * args); + #endif /* _AST_UTIL_H_ */ From 5b7201a911a0e5f0e4efabc143ebac4be6e41c13 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 27 Jun 2013 09:30:25 -0700 Subject: [PATCH 2/4] Fix minor problem Signed-off-by: Leonardo de Moura --- src/smt/tactic/ctx_solver_simplify_tactic.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index 5668ca455..63c14f297 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -23,7 +23,7 @@ Notes: #include"smt_kernel.h" #include"ast_pp.h" #include"mk_simplified_app.h" - +#include"ast_util.h" class ctx_solver_simplify_tactic : public tactic { ast_manager& m; @@ -104,7 +104,7 @@ protected: return; ptr_vector fmls; g.get_formulas(fmls); - fml = m.mk_and(fmls.size(), fmls.c_ptr()); + fml = mk_and(m, fmls.size(), fmls.c_ptr()); m_solver.push(); reduce(fml); m_solver.pop(1); @@ -119,7 +119,7 @@ protected: { m_solver.push(); expr_ref fml1(m); - fml1 = m.mk_and(fmls.size(), fmls.c_ptr()); + fml1 = mk_and(m, fmls.size(), fmls.c_ptr()); fml1 = m.mk_iff(fml, fml1); fml1 = m.mk_not(fml1); m_solver.assert_expr(fml1); From 619bd91ddb30c6b6283409be567336ee390e692d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Jun 2013 11:59:40 -0500 Subject: [PATCH 3/4] fix bug in ctx-solver-simplify reported @ http://z3.codeplex.com/workitem/51 Signed-off-by: Nikolaj Bjorner --- src/smt/tactic/ctx_solver_simplify_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index 5668ca455..626cb6d22 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -218,7 +218,7 @@ protected: else if (m.is_bool(arg)) { res = local_simplify(a, n, id, i); TRACE("ctx_solver_simplify_tactic", - tout << "Already cached: " << path_r.first << " " << mk_pp(res, m) << "\n";); + tout << "Already cached: " << path_r.first << " " << mk_pp(arg, m) << " |-> " << mk_pp(res, m) << "\n";); args.push_back(res); } else { @@ -327,7 +327,7 @@ protected: tmp = m.mk_eq(result, n); m_solver.assert_expr(tmp); if (!simplify_bool(n2, result)) { - result = a; + result = a->get_arg(index); } m_solver.pop(1); return result; From 4f72e1d5289b5afce868377a286e7f325f65e0f0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 28 Jun 2013 12:14:14 +0100 Subject: [PATCH 4/4] FPA: avoid compiler warnings. Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_converter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 234c343b8..ff24d1ceb 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -2437,7 +2437,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & t = m_bv_util.mk_bv_sub(t, lz); t = m_bv_util.mk_bv_sub(t, m_bv_util.mk_sign_extend(2, e_min)); expr_ref TINY(m); - TINY = m_bv_util.mk_sle(t, m_bv_util.mk_numeral(-1, ebits+2)); + TINY = m_bv_util.mk_sle(t, m_bv_util.mk_numeral((unsigned)-1, ebits+2)); TRACE("fpa2bv_dbg", tout << "TINY = " << mk_ismt2_pp(TINY, m) << std::endl;); SASSERT(is_well_sorted(m, TINY)); @@ -2481,7 +2481,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & m_simp.mk_ite(sigma_le_cap, sigma_neg, sigma_cap, sigma_neg_capped); dbg_decouple("fpa2bv_rnd_sigma_neg", sigma_neg); dbg_decouple("fpa2bv_rnd_sigma_neg_capped", sigma_neg_capped); - sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral(-1, sigma_size)); + sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral((unsigned)-1, sigma_size)); dbg_decouple("fpa2bv_rnd_sigma_lt_zero", sigma_lt_zero); sig_ext = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_size));