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

checkpoint

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-21 14:39:59 -07:00
parent cf47f6ce60
commit ae400c4b2a
42 changed files with 1 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

314
lib/assertion_stack.cpp
View file

@ -1,314 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
assertion_stack.cpp
Abstract:
Assertion stacks
Author:
Leonardo de Moura (leonardo) 2012-02-17
Revision History:
--*/
#include"assertion_stack.h"
#include"well_sorted.h"
#include"ast_smt2_pp.h"
#include"ref_util.h"
assertion_stack::assertion_stack(ast_manager & m, bool models_enabled, bool core_enabled):
m_manager(m),
m_forbidden(m),
m_csubst(m, core_enabled),
m_fsubst(m, core_enabled) {
init(m.proofs_enabled(), models_enabled, core_enabled);
}
assertion_stack::assertion_stack(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled):
m_manager(m),
m_forbidden(m),
m_csubst(m, core_enabled, proofs_enabled),
m_fsubst(m, core_enabled, proofs_enabled) {
init(proofs_enabled, models_enabled, core_enabled);
}
void assertion_stack::init(bool proofs_enabled, bool models_enabled, bool core_enabled) {
m_ref_count = 0;
m_models_enabled = models_enabled;
m_proofs_enabled = proofs_enabled;
m_core_enabled = core_enabled;
m_inconsistent = false;
m_form_qhead = 0;
}
assertion_stack::~assertion_stack() {
reset();
}
void assertion_stack::reset() {
m_inconsistent = false;
m_form_qhead = 0;
m_mc_qhead = 0;
dec_ref_collection_values(m_manager, m_forms);
dec_ref_collection_values(m_manager, m_proofs);
dec_ref_collection_values(m_manager, m_deps);
m_forbidden_set.reset();
m_forbidden.reset();
m_csubst.reset();
m_fsubst.reset();
m_mc.reset();
m_scopes.reset();
}
void assertion_stack::expand(expr * f, proof * pr, expr_dependency * dep, expr_ref & new_f, proof_ref & new_pr, expr_dependency_ref & new_dep) {
// TODO: expand definitions
new_f = f;
new_pr = pr;
new_dep = dep;
}
void assertion_stack::push_back(expr * f, proof * pr, expr_dependency * d) {
if (m().is_true(f))
return;
if (m().is_false(f)) {
m_inconsistent = true;
}
else {
SASSERT(!m_inconsistent);
}
m().inc_ref(f);
m_forms.push_back(f);
if (proofs_enabled()) {
m().inc_ref(pr);
m_proofs.push_back(pr);
}
if (unsat_core_enabled()) {
m().inc_ref(d);
m_deps.push_back(d);
}
}
void assertion_stack::quick_process(bool save_first, expr * & f, expr_dependency * d) {
if (!m().is_and(f) && !(m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))) {
if (!save_first) {
push_back(f, 0, d);
}
return;
}
typedef std::pair<expr *, bool> expr_pol;
sbuffer<expr_pol, 64> todo;
todo.push_back(expr_pol(f, true));
while (!todo.empty()) {
if (m_inconsistent)
return;
expr_pol p = todo.back();
expr * curr = p.first;
bool pol = p.second;
todo.pop_back();
if (pol && m().is_and(curr)) {
app * t = to_app(curr);
unsigned i = t->get_num_args();
while (i > 0) {
--i;
todo.push_back(expr_pol(t->get_arg(i), true));
}
}
else if (!pol && m().is_or(curr)) {
app * t = to_app(curr);
unsigned i = t->get_num_args();
while (i > 0) {
--i;
todo.push_back(expr_pol(t->get_arg(i), false));
}
}
else if (m().is_not(curr)) {
todo.push_back(expr_pol(to_app(curr)->get_arg(0), !pol));
}
else {
if (!pol)
curr = m().mk_not(curr);
if (save_first) {
f = curr;
save_first = false;
}
else {
push_back(curr, 0, d);
}
}
}
}
void assertion_stack::process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) {
unsigned num = f->get_num_args();
for (unsigned i = 0; i < num; i++) {
if (m_inconsistent)
return;
slow_process(save_first && i == 0, f->get_arg(i), m().mk_and_elim(pr, i), d, out_f, out_pr);
}
}
void assertion_stack::process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) {
unsigned num = f->get_num_args();
for (unsigned i = 0; i < num; i++) {
if (m_inconsistent)
return;
expr * child = f->get_arg(i);
if (m().is_not(child)) {
expr * not_child = to_app(child)->get_arg(0);
slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr);
}
else {
expr_ref not_child(m());
not_child = m().mk_not(child);
slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr);
}
}
}
void assertion_stack::slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) {
if (m().is_and(f))
process_and(save_first, to_app(f), pr, d, out_f, out_pr);
else if (m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))
process_not_or(save_first, to_app(to_app(f)->get_arg(0)), pr, d, out_f, out_pr);
else if (save_first) {
out_f = f;
out_pr = pr;
}
else {
push_back(f, pr, d);
}
}
void assertion_stack::slow_process(expr * f, proof * pr, expr_dependency * d) {
expr_ref out_f(m());
proof_ref out_pr(m());
slow_process(false, f, pr, d, out_f, out_pr);
}
void assertion_stack::assert_expr(expr * f, proof * pr, expr_dependency * d) {
SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
if (m_inconsistent)
return;
expr_ref new_f(m()); proof_ref new_pr(m()); expr_dependency_ref new_d(m());
expand(f, pr, d, new_f, new_pr, new_d);
if (proofs_enabled())
slow_process(f, pr, d);
else
quick_process(false, f, d);
}
#ifdef Z3DEBUG
// bool assertion_stack::is_expanded(expr * f) {
// }
#endif
void assertion_stack::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
SASSERT(i >= m_form_qhead);
SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
if (m_inconsistent)
return;
if (proofs_enabled()) {
expr_ref out_f(m());
proof_ref out_pr(m());
slow_process(true, f, pr, d, out_f, out_pr);
if (!m_inconsistent) {
if (m().is_false(out_f)) {
push_back(out_f, out_pr, d);
}
else {
m().inc_ref(out_f);
m().dec_ref(m_forms[i]);
m_forms[i] = out_f;
m().inc_ref(out_pr);
m().dec_ref(m_proofs[i]);
m_proofs[i] = out_pr;
if (unsat_core_enabled()) {
m().inc_ref(d);
m().dec_ref(m_deps[i]);
m_deps[i] = d;
}
}
}
}
else {
quick_process(true, f, d);
if (!m_inconsistent) {
if (m().is_false(f)) {
push_back(f, 0, d);
}
else {
m().inc_ref(f);
m().dec_ref(m_forms[i]);
m_forms[i] = f;
if (unsat_core_enabled()) {
m().inc_ref(d);
m().dec_ref(m_deps[i]);
m_deps[i] = d;
}
}
}
}
}
void assertion_stack::expand_and_update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
SASSERT(i >= m_form_qhead);
SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
if (m_inconsistent)
return;
expr_ref new_f(m()); proof_ref new_pr(m()); expr_dependency_ref new_d(m());
expand(f, pr, d, new_f, new_pr, new_d);
update(i, new_f, new_pr, new_d);
}
void assertion_stack::push() {
}
void assertion_stack::pop(unsigned num_scopes) {
}
void assertion_stack::commit() {
}
void assertion_stack::add_filter(func_decl * f) const {
}
void assertion_stack::add_definition(app * c, expr * def, proof * pr, expr_dependency * dep) {
}
void assertion_stack::add_definition(func_decl * f, quantifier * q, proof * pr, expr_dependency * dep) {
}
void assertion_stack::convert(model_ref & m) {
}
void assertion_stack::display(std::ostream & out) const {
out << "(assertion-stack";
unsigned sz = size();
for (unsigned i = 0; i < sz; i++) {
out << "\n ";
if (i == m_form_qhead)
out << "==>\n";
out << mk_ismt2_pp(form(i), m(), 2);
}
out << ")" << std::endl;
}
bool assertion_stack::is_well_sorted() const {
unsigned sz = size();
for (unsigned i = 0; i < sz; i++) {
expr * t = form(i);
if (!::is_well_sorted(m(), t))
return false;
}
return true;
}

141
lib/assertion_stack.h
View file

@ -1,141 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
assertion_stack.h
Abstract:
It should be viewed as the "goal" object for incremental solvers.
The main difference is the support of push/pop operations. Like a
goal, an assertion_stack contains expressions, their proofs (if
proof generation is enabled), and dependencies (if unsat core
generation is enabled).
The assertions on the stack are grouped by scope levels. Scoped
levels are created using push, and removed using pop.
Assertions may be "committed". Whenever a push is executed, all
"uncommitted" assertions are automatically committed.
Only uncommitted assertions can be simplified/reduced.
An assertion set has a limited model converter that only supports
definitions (for variable/function elimination) and filters (for fresh
symbols introduced by tactics).
Some tactics support assertion_stacks and can be applied to them.
However, a tactic can only access the assertions on the top level.
The assertion stack also informs the tactic which declarations
can't be eliminated since they occur in the already committed part.
Author:
Leonardo de Moura (leonardo) 2012-02-17
Revision History:
--*/
#ifndef _ASSERTION_STACK_H_
#define _ASSERTION_STACK_H_
#include"ast.h"
#include"model.h"
#include"expr_substitution.h"
#include"macro_substitution.h"
class assertion_stack {
ast_manager & m_manager;
unsigned m_ref_count;
bool m_models_enabled; // model generation is enabled.
bool m_proofs_enabled; // proof production is enabled. m_manager.proofs_enabled() must be true if m_proofs_enabled == true
bool m_core_enabled; // unsat core extraction is enabled.
bool m_inconsistent;
ptr_vector<expr> m_forms;
ptr_vector<proof> m_proofs;
ptr_vector<expr_dependency> m_deps;
unsigned m_form_qhead; // position of first uncommitted assertion
unsigned m_mc_qhead;
// Set of declarations that can't be eliminated
obj_hashtable<func_decl> m_forbidden_set;
func_decl_ref_vector m_forbidden;
// Limited model converter support, it supports only extensions
// and filters.
// It should be viewed as combination of extension_model_converter and
// filter_model_converter for goals.
expr_substitution m_csubst; // substitution for eliminated constants
macro_substitution m_fsubst; // substitution for eliminated functions
// Model converter is just a sequence of tagged pointers.
// Tag 0 (extension) func_decl was eliminated, and its definition is in m_vsubst or m_fsubst.
// Tag 1 (filter) func_decl was introduced by tactic, and must be removed from model.
ptr_vector<func_decl> m_mc;
struct scope {
unsigned m_forms_lim;
unsigned m_forbidden_vars_lim;
unsigned m_mc_lim;
bool m_inconsistent_old;
};
svector<scope> m_scopes;
void init(bool proofs_enabled, bool models_enabled, bool core_enabled);
void expand(expr * f, proof * pr, expr_dependency * dep, expr_ref & new_f, proof_ref & new_pr, expr_dependency_ref & new_dep);
void push_back(expr * f, proof * pr, expr_dependency * d);
void quick_process(bool save_first, expr * & f, expr_dependency * d);
void process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
void process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
void slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
void slow_process(expr * f, proof * pr, expr_dependency * d);
public:
assertion_stack(ast_manager & m, bool models_enabled = true, bool core_enabled = true);
assertion_stack(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled);
~assertion_stack();
void reset();
void inc_ref() { ++m_ref_count; }
void dec_ref() { --m_ref_count; if (m_ref_count == 0) dealloc(this); }
ast_manager & m() const { return m_manager; }
bool models_enabled() const { return m_models_enabled; }
bool proofs_enabled() const { return m_proofs_enabled; }
bool unsat_core_enabled() const { return m_core_enabled; }
bool inconsistent() const { return m_inconsistent; }
unsigned size() const { return m_forms.size(); }
unsigned qhead() const { return m_form_qhead; }
expr * form(unsigned i) const { return m_forms[i]; }
proof * pr(unsigned i) const { return proofs_enabled() ? static_cast<proof*>(m_proofs[i]) : 0; }
expr_dependency * dep(unsigned i) const { return unsat_core_enabled() ? m_deps[i] : 0; }
void assert_expr(expr * f, proof * pr, expr_dependency * d);
void assert_expr(expr * f) {
assert_expr(f, proofs_enabled() ? m().mk_asserted(f) : 0, 0);
}
void update(unsigned i, expr * f, proof * pr = 0, expr_dependency * dep = 0);
void expand_and_update(unsigned i, expr * f, proof * pr = 0, expr_dependency * d = 0);
void commit();
void push();
void pop(unsigned num_scopes);
unsigned scope_lvl() const { return m_scopes.size(); }
bool is_well_sorted() const;
bool is_forbidden(func_decl * f) const { return m_forbidden_set.contains(f); }
void add_filter(func_decl * f) const;
void add_definition(app * c, expr * def, proof * pr, expr_dependency * dep);
void add_definition(func_decl * f, quantifier * q, proof * pr, expr_dependency * dep);
void convert(model_ref & m);
void display(std::ostream & out) const;
};
#endif

604
lib/bv2int_rewriter.cpp
View file

@ -1,604 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
bv2int_rewriter.cpp
Abstract:
Basic rewriting rules for bv2int propagation.
Author:
Nikolaj (nbjorner) 2011-05-05
Notes:
--*/
#include "bv2int_rewriter.h"
#include "rewriter_def.h"
#include "ast_pp.h"
void bv2int_rewriter_ctx::update_params(params_ref const& p) {
m_max_size = p.get_uint(":max-bv-size", UINT_MAX);
}
struct lt_rational {
bool operator()(rational const& a, rational const& b) const { return a < b; }
};
void bv2int_rewriter_ctx::collect_power2(goal const& s) {
ast_manager& m = m_trail.get_manager();
arith_util arith(m);
bv_util bv(m);
for (unsigned j = 0; j < s.size(); ++j) {
expr* f = s.form(j);
if (!m.is_or(f)) continue;
unsigned sz = to_app(f)->get_num_args();
expr* x, *y, *v = 0;
rational n;
vector<rational> bounds;
bool is_int, ok = true;
for (unsigned i = 0; ok && i < sz; ++i) {
expr* e = to_app(f)->get_arg(i);
if (!m.is_eq(e, x, y)) {
ok = false;
break;
}
if (arith.is_numeral(y, n, is_int) && is_int &&
(x == v || v == 0)) {
v = x;
bounds.push_back(n);
}
else if (arith.is_numeral(x, n, is_int) && is_int &&
(y == v || v == 0)) {
v = y;
bounds.push_back(n);
}
else {
ok = false;
break;
}
}
if (!ok || !v) continue;
SASSERT(!bounds.empty());
lt_rational lt;
// lt is a total order on rationals.
std::sort(bounds.begin(), bounds.end(), lt);
rational p(1);
unsigned num_bits = 0;
for (unsigned i = 0; ok && i < bounds.size(); ++i) {
ok = (p == bounds[i]);
p *= rational(2);
++num_bits;
}
if (!ok) continue;
unsigned log2 = 0;
for (unsigned i = 1; i <= num_bits; i *= 2) ++log2;
if(log2 == 0) continue;
expr* logx = m.mk_fresh_const("log2_v", bv.mk_sort(log2));
logx = bv.mk_zero_extend(num_bits - log2, logx);
m_trail.push_back(logx);
TRACE("bv2int_rewriter", tout << mk_pp(v, m) << " |-> " << mk_pp(logx, m) << "\n";);
m_power2.insert(v, logx);
}
}
bool bv2int_rewriter_ctx::is_power2(expr* x, expr*& log_x) {
return m_power2.find(x, log_x);
}
bv2int_rewriter::bv2int_rewriter(ast_manager & m, bv2int_rewriter_ctx& ctx)
:m_manager(m), m_ctx(ctx), m_bv(m), m_arith(m) {
}
br_status bv2int_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
if(f->get_family_id() == m_arith.get_family_id()) {
switch (f->get_decl_kind()) {
case OP_NUM: return BR_FAILED;
case OP_LE: SASSERT(num_args == 2); return mk_le(args[0], args[1], result);
case OP_GE: SASSERT(num_args == 2); return mk_ge(args[0], args[1], result);
case OP_LT: SASSERT(num_args == 2); return mk_lt(args[0], args[1], result);
case OP_GT: SASSERT(num_args == 2); return mk_gt(args[0], args[1], result);
case OP_ADD: return mk_add(num_args, args, result);
case OP_MUL: return mk_mul(num_args, args, result);
case OP_SUB: return mk_sub(num_args, args, result);
case OP_DIV: return BR_FAILED;
case OP_IDIV: SASSERT(num_args == 2); return mk_idiv(args[0], args[1], result);
case OP_MOD: SASSERT(num_args == 2); return mk_mod(args[0], args[1], result);
case OP_REM: SASSERT(num_args == 2); return mk_rem(args[0], args[1], result);
case OP_UMINUS: SASSERT(num_args == 1); return mk_uminus(args[0], result);
case OP_TO_REAL: return BR_FAILED;
case OP_TO_INT: return BR_FAILED;
case OP_IS_INT: return BR_FAILED;
default:
return BR_FAILED;
}
}
if (f->get_family_id() == m().get_basic_family_id()) {
switch (f->get_decl_kind()) {
case OP_EQ: SASSERT(num_args == 2); return mk_eq(args[0], args[1], result);
case OP_ITE: SASSERT(num_args == 3); return mk_ite(args[0], args[1], args[2], result);
default: return BR_FAILED;
}
}
return BR_FAILED;
}
br_status bv2int_rewriter::mk_le(expr * s, expr * t, expr_ref & result) {
expr_ref s1(m()), t1(m()), s2(m()), t2(m());
if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
align_sizes(s1, t1, false);
result = m_bv.mk_ule(s1, t1);
return BR_DONE;
}
if (is_bv2int_diff(s, s1, s2) && is_bv2int_diff(t, t1, t2)) {
// s1 - s2 <= t1 - t2
// <=>
// s1 + t2 <= t1 + s2
//
s1 = mk_bv_add(s1, t2, false);
t1 = mk_bv_add(t1, s2, false);
align_sizes(s1, t1, false);
result = m_bv.mk_ule(s1, t1);
return BR_DONE;
}
if (is_sbv2int(s, s1) && is_sbv2int(t, t1)) {
align_sizes(s1, t1, true);
result = m_bv.mk_sle(s1, t1);
return BR_DONE;
}
return BR_FAILED;
}
br_status bv2int_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) {
result = m().mk_not(m_arith.mk_le(arg2, arg1));
return BR_REWRITE2;
}
br_status bv2int_rewriter::mk_ge(expr * arg1, expr * arg2, expr_ref & result) {
return mk_le(arg2, arg1, result);
}
br_status bv2int_rewriter::mk_gt(expr * arg1, expr * arg2, expr_ref & result) {
result = m().mk_not(m_arith.mk_le(arg1, arg2));
return BR_REWRITE2;
}
br_status bv2int_rewriter::mk_ite(expr* c, expr* s, expr* t, expr_ref& result) {
expr_ref s1(m()), t1(m());
if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
align_sizes(s1, t1, false);
result = m_bv.mk_bv2int(m().mk_ite(c, s1, t1));
return BR_DONE;
}
if (is_sbv2int(s, s1) && is_sbv2int(t, t1)) {
align_sizes(s1, t1, true);
result = mk_sbv2int(m().mk_ite(c, s1, t1));
return BR_DONE;
}
return BR_FAILED;
}
br_status bv2int_rewriter::mk_eq(expr * s, expr * t, expr_ref & result) {
expr_ref s1(m()), t1(m()), s2(m()), t2(m());
if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
align_sizes(s1, t1, false);
result = m().mk_eq(s1, t1);
return BR_DONE;
}
if (is_bv2int_diff(s, s1, s2) && is_bv2int_diff(t, t1, t2)) {
s1 = mk_bv_add(s1, t2, false);
t1 = mk_bv_add(s2, t1, false);
align_sizes(s1, t1, false);
result = m().mk_eq(s1, t1);
return BR_DONE;
}
if (is_sbv2int(s, s1) && is_sbv2int(t, t1)) {
align_sizes(s1, t1, true);
result = m().mk_eq(s1, t1);
return BR_DONE;
}
return BR_FAILED;
}
br_status bv2int_rewriter::mk_idiv(expr * arg1, expr * arg2, expr_ref & result) {
// TBD
return BR_FAILED;
}
br_status bv2int_rewriter::mk_mod(expr * s, expr * t, expr_ref & result) {
expr_ref s1(m()), s2(m()), t1(m());
if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
align_sizes(s1, t1, false);
result = m_bv.mk_bv2int(m_bv.mk_bv_urem(s1, t1));
return BR_DONE;
}
//
// (s1 - s2) mod t1 = (s1 + (t1 - (s2 mod t1))) mod t1
//
if (is_bv2int_diff(s, s1, s2) && is_bv2int(t, t1)) {
expr_ref u1(m());
align_sizes(s1, t1, false);
u1 = m_bv.mk_bv_urem(s1, t1);
u1 = m_bv.mk_bv_sub(t1, u1);
u1 = mk_bv_add(s1, u1, false);
align_sizes(u1, t1, false);
result = m_bv.mk_bv2int(m_bv.mk_bv_urem(u1, t1));
return BR_DONE;
}
#if 0
// TBD: check semantics
if (is_sbv2int(s, s1) && is_sbv2int(t, t1)) {
align_sizes(s1, t1, true);
result = mk_sbv2int(m_bv.mk_bv_srem(s1, t1));
return BR_DONE;
}
#endif
return BR_FAILED;
}
br_status bv2int_rewriter::mk_rem(expr * arg1, expr * arg2, expr_ref & result) {
// TBD
return BR_FAILED;
}
br_status bv2int_rewriter::mk_uminus(expr * s, expr_ref & result) {
expr_ref s1(m()), s2(m());
if (is_bv2int_diff(s, s1, s2)) {
result = m_arith.mk_sub(m_bv.mk_bv2int(s2), m_bv.mk_bv2int(s1));
return BR_DONE;
}
if (is_sbv2int(s, s1)) {
result = mk_sbv2int(m_bv.mk_bv_neg(s1));
return BR_DONE;
}
return BR_FAILED;
}
br_status bv2int_rewriter::mk_add(unsigned num_args, expr * const* args, expr_ref& result) {
br_status r = BR_DONE;
SASSERT(num_args > 0);
result = args[0];
for (unsigned i = 1; r == BR_DONE && i < num_args; ++i) {
r = mk_add(result, args[i], result);
}
return r;
}
void bv2int_rewriter::align_sizes(expr_ref& s, expr_ref& t, bool is_signed) {
unsigned sz1 = m_bv.get_bv_size(s);
unsigned sz2 = m_bv.get_bv_size(t);
if (sz1 > sz2 && is_signed) {
t = mk_extend(sz1-sz2, t, true);
}
if (sz1 > sz2 && !is_signed) {
t = mk_extend(sz1-sz2, t, false);
}
if (sz1 < sz2 && is_signed) {
s = mk_extend(sz2-sz1, s, true);
}
if (sz1 < sz2 && !is_signed) {
s = mk_extend(sz2-sz1, s, false);
}
}
bool bv2int_rewriter::is_zero(expr* n) {
rational r;
unsigned sz;
return m_bv.is_numeral(n, r, sz) && r.is_zero();
}
expr* bv2int_rewriter::mk_bv_add(expr* s, expr* t, bool is_signed) {
SASSERT(m_bv.is_bv(s));
SASSERT(m_bv.is_bv(t));
if (is_zero(s)) {
return t;
}
if (is_zero(t)) {
return s;
}
expr_ref s1(s, m()), t1(t, m());
align_sizes(s1, t1, is_signed);
s1 = mk_extend(1, s1, is_signed);
t1 = mk_extend(1, t1, is_signed);
return m_bv.mk_bv_add(s1, t1);
}
br_status bv2int_rewriter::mk_add(expr* s, expr* t, expr_ref& result) {
expr_ref s1(m()), t1(m()), s2(m()), t2(m());
if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
result = m_bv.mk_bv2int(mk_bv_add(s1, t1, false));
return BR_DONE;
}
if (is_bv2int_diff(s, s1, s2) && is_bv2int_diff(t, t1, t2)) {
// s1 - s2 + t1 - t2
// =
// s1 + t1 - (s2 + t2)
//
t1 = m_bv.mk_bv2int(mk_bv_add(s1, t1, false));
t2 = m_bv.mk_bv2int(mk_bv_add(s2, t2, false));
result = m_arith.mk_sub(t1, t2);
return BR_DONE;
}
if (is_sbv2int(s, s1) && is_sbv2int(t, t1)) {
result = mk_sbv2int(mk_bv_add(s1, t1, true));
return BR_DONE;
}
return BR_FAILED;
}
br_status bv2int_rewriter::mk_mul(unsigned num_args, expr * const* args, expr_ref& result) {
br_status r = BR_DONE;
SASSERT(num_args > 0);
result = args[0];
for (unsigned i = 1; r == BR_DONE && i < num_args; ++i) {
r = mk_mul(result, args[i], result);
}
return r;
}
expr* bv2int_rewriter::mk_bv_mul(expr* s, expr* t, bool is_signed) {
SASSERT(m_bv.is_bv(s));
SASSERT(m_bv.is_bv(t));
if (is_zero(s)) {
return s;
}
if (is_zero(t)) {
return t;
}
rational r;
unsigned sz;
if (m_bv.is_numeral(s, r, sz) && r.is_one()) {
return t;
}
if (m_bv.is_numeral(t, r, sz) && r.is_one()) {
return s;
}
expr_ref s1(s, m()), t1(t, m());
align_sizes(s1, t1, is_signed);
unsigned n = m_bv.get_bv_size(t1);
unsigned max_bits = m_ctx.get_max_num_bits();
bool add_side_conds = 2*n > max_bits;
if (n >= max_bits) {
//
}
else if (2*n > max_bits) {
s1 = mk_extend(max_bits-n, s1, is_signed);
t1 = mk_extend(max_bits-n, t1, is_signed);
}
else {
s1 = mk_extend(n, s1, is_signed);
t1 = mk_extend(n, t1, is_signed);
}
if (add_side_conds) {
if (is_signed) {
m_ctx.add_side_condition(m_bv.mk_bvsmul_no_ovfl(s1, t1));
m_ctx.add_side_condition(m_bv.mk_bvsmul_no_udfl(s1, t1));
}
else {
m_ctx.add_side_condition(m_bv.mk_bvumul_no_ovfl(s1, t1));
}
}
return m_bv.mk_bv_mul(s1, t1);
}
br_status bv2int_rewriter::mk_mul(expr* s, expr* t, expr_ref& result) {
expr_ref s1(m()), s2(m()), t1(m()), t2(m());
if ((is_shl1(s, s1) && is_bv2int(t, t1)) ||
(is_shl1(t, s1) && is_bv2int(s, t1))) {
unsigned n = m_bv.get_bv_size(s1);
unsigned m = m_bv.get_bv_size(t1);
s1 = mk_extend(m, s1, false);
t1 = mk_extend(n, t1, false);
result = m_bv.mk_bv2int(m_bv.mk_bv_shl(t1, s1));
return BR_DONE;
}
if (is_bv2int(s, s1) && is_bv2int(t, t1)) {
result = m_bv.mk_bv2int(mk_bv_mul(s1, t1, false));
return BR_DONE;
}
if ((is_bv2int(s, s1) && is_bv2int_diff(t, t1, t2)) ||
(is_bv2int(t, s1) && is_bv2int_diff(s, t1, t2))) {
t1 = m_bv.mk_bv2int(mk_bv_mul(s1, t1, false));
t2 = m_bv.mk_bv2int(mk_bv_mul(s1, t2, false));
result = m_arith.mk_sub(t1, t2);
return BR_DONE;
}
if (is_sbv2int(s, s1) && is_sbv2int(t, t1)) {
result = mk_sbv2int(mk_bv_mul(s1, t1, true));
return BR_DONE;
}
return BR_FAILED;
}
br_status bv2int_rewriter::mk_sub(unsigned num_args, expr * const* args, expr_ref& result) {
br_status r = BR_DONE;
SASSERT(num_args > 0);
result = args[0];
for (unsigned i = 1; r == BR_DONE && i < num_args; ++i) {
r = mk_sub(result, args[i], result);
}
return r;
}
br_status bv2int_rewriter::mk_sub(expr* s, expr* t, expr_ref& result) {
expr_ref s1(m()), t1(m()), s2(m()), t2(m());
if (is_bv2int_diff(s, s1, s2) && is_bv2int_diff(t, t1, t2)) {
// s1 - s2 - (t1 - t2)
// =
// s1 + t2 - (t1 + s2)
//
s1 = m_bv.mk_bv2int(mk_bv_add(s1, t2, false));
s2 = m_bv.mk_bv2int(mk_bv_add(s2, t1, false));
result = m_arith.mk_sub(s1, s2);
return BR_DONE;
}
if (is_sbv2int(s, s1) && is_sbv2int(t, t1)) {
align_sizes(s1, t1, true);
s1 = m_bv.mk_sign_extend(1, s1);
t1 = m_bv.mk_sign_extend(1, t1);
result = mk_sbv2int(m_bv.mk_bv_sub(s1, t1));
return BR_DONE;
}
return BR_FAILED;
}
bool bv2int_rewriter::is_bv2int(expr* n, expr_ref& s) {
rational k;
bool is_int;
if (m_bv.is_bv2int(n)) {
s = to_app(n)->get_arg(0);
return true;
}
if (m_arith.is_numeral(n, k, is_int) && is_int && !k.is_neg()) {
unsigned sz = k.get_num_bits();
s = m_bv.mk_numeral(k, m_bv.mk_sort(sz));
return true;
}
return false;
}
bool bv2int_rewriter::is_shl1(expr* n, expr_ref& s) {
expr* s1, *s2;
rational r;
unsigned bv_size;
if(m_bv.is_bv2int(n, s2) &&
m_bv.is_bv_shl(s2, s1, s2) &&
m_bv.is_numeral(s1, r, bv_size) &&
r.is_one()) {
s = s2;
return true;
}
return false;
}
bool bv2int_rewriter::is_bv2int_diff(expr* n, expr_ref& s, expr_ref& t) {
if (is_bv2int(n, s)) {
t = m_bv.mk_numeral(0, 1);
return true;
}
rational k;
bool is_int;
if (m_arith.is_numeral(n, k, is_int) && is_int) {
SASSERT(k.is_neg());
k.neg();
unsigned sz = k.get_num_bits();
t = m_bv.mk_numeral(k, m_bv.mk_sort(sz));
s = m_bv.mk_numeral(0, 1);
return true;
}
//
// bv2int(a) - bv2int(b)
//
expr *e1, *e2;
if (m_arith.is_sub(n, e1, e2) &&
is_bv2int(e1, s) &&
is_bv2int(e2, t)) {
return true;
}
return false;
}
bool bv2int_rewriter::is_sbv2int(expr* n, expr_ref& s) {
if (is_bv2int(n, s)) {
s = m_bv.mk_zero_extend(1, s);
return true;
}
expr_ref u1(m()), u2(m());
if (is_bv2int_diff(n, u1, u2)) {
align_sizes(u1, u2, false);
u1 = mk_extend(1, u1, false);
u2 = mk_extend(1, u2, false);
s = m_bv.mk_bv_sub(u1, u2);
return true;
}
// ite(bv1 == b[n-1:n-1], bv2int(b[0:n-2]) - 2^{n-1}, bv2int(b[0:n-2]))
expr* c, *t, *e1, *c1, *c2, *c3, *t1, *t2, *e2, *e3;
rational k;
bool is_int;
unsigned lo, hi, lo1, hi1, sz;
if (m().is_ite(n, c, t, e1) &&
m().is_eq(c, c1, c2) &&
m_bv.is_numeral(c1, k, sz) && k.is_one() && sz == 1 &&
m_bv.is_extract(c2, lo, hi, c3) &&
lo == hi && lo == m_bv.get_bv_size(c3) - 1 &&
m_arith.is_sub(t, t1, t2) &&
e1 == t1 &&
m_bv.is_bv2int(e1, e2) &&
m_bv.is_extract(e2, lo1, hi1, e3) &&
lo1 == 0 && hi1 == hi-1 &&
m_arith.is_numeral(t2, k, is_int) && is_int &&
k == m_bv.power_of_two(hi)
) {
s = e3;
return true;
}
#if 0
// bv2int(b[0:n-2]) - ite(bv1 == b[n-1:n-1], 2^{n-1}, 0)
if (m().is_sub(n, e1, e2) &&
m_bv.is_bv2int(e1, e3) &&
m_bv.is_extract(e3, lo, hi, e4) &&
lo == 0 && hi == m_bv.get_bv_size(e4) - 2 &&
m().is_ite(e2, t1, t2, t3) &&
m().is_eq(t1, c1, c2) &&
m_bv.is_numeral(c1, k, sz) && k.is_one() && sz == 1 &&
m_bv.is_extract(c2, lo1, hi1, c3) && lo1 == h1 + 1 && hi1 == lo1 &&
c3 == e4 &&
m_arith.is_numeral(t2, )) {
}
#endif
return false;
}
expr* bv2int_rewriter::mk_sbv2int(expr* b) {
//
// ite(bit1 = b[n-1:n-1], bv2int(b[0:n-2]) - 2^{n-1}, bv2int(b[0:n-2]))
//
expr* bv1 = m_bv.mk_numeral(1, 1);
unsigned n = m_bv.get_bv_size(b);
expr* c = m().mk_eq(bv1, m_bv.mk_extract(n-1, n-1, b));
expr* e = m_bv.mk_bv2int(m_bv.mk_extract(n-2, 0, b));
expr* t = m_arith.mk_sub(e, m_arith.mk_numeral(power(rational(2), n-1), true));
return m().mk_ite(c, t, e);
}
expr* bv2int_rewriter::mk_extend(unsigned sz, expr* b, bool is_signed) {
if (sz == 0) {
return b;
}
rational r;
unsigned bv_sz;
if (is_signed) {
return m_bv.mk_sign_extend(sz, b);
}
else if (m_bv.is_numeral(b, r, bv_sz)) {
return m_bv.mk_numeral(r, bv_sz + sz);
}
else {
return m_bv.mk_zero_extend(sz, b);
}
}
template class rewriter_tpl<bv2int_rewriter_cfg>;

120
lib/bv2int_rewriter.h
View file

@ -1,120 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
bv2int_rewriter.h
Abstract:
Basic rewriting rules for bv2int propagation.
Author:
Nikolaj (nbjorner) 2011-05-05
Notes:
--*/
#ifndef _BV2INT_REWRITER_H_
#define _BV2INT_REWRITER_H_
#include"ast.h"
#include"rewriter.h"
#include"bv_decl_plugin.h"
#include"arith_decl_plugin.h"
#include"params.h"
#include"goal.h"
class bv2int_rewriter_ctx {
unsigned m_max_size;
expr_ref_vector m_side_conditions;
obj_map<expr, expr*> m_power2;
expr_ref_vector m_trail;
public:
bv2int_rewriter_ctx(ast_manager& m, params_ref const& p) :
m_side_conditions(m), m_trail(m) { update_params(p); }
void reset() { m_side_conditions.reset(); m_trail.reset(); m_power2.reset(); }
void add_side_condition(expr* e) { m_side_conditions.push_back(e); }
unsigned num_side_conditions() const { return m_side_conditions.size(); }
expr* const* side_conditions() const { return m_side_conditions.c_ptr(); }
unsigned get_max_num_bits() const { return m_max_size; }
void collect_power2(goal const & s);
bool is_power2(expr* x, expr*& log_x);
obj_map<expr, expr*> const& power2() const { return m_power2; }
private:
void update_params(params_ref const& p);
};
class bv2int_rewriter {
ast_manager & m_manager;
bv2int_rewriter_ctx& m_ctx;
bv_util m_bv;
arith_util m_arith;
public:
bv2int_rewriter(ast_manager & m, bv2int_rewriter_ctx& ctx);
ast_manager & m() const { return m_manager; }
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
void mk_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
if (mk_app_core(f, num_args, args, result) == BR_FAILED)
result = m().mk_app(f, num_args, args);
}
private:
br_status mk_eq(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_ite(expr* c, expr* s, expr* t, expr_ref& result);
br_status mk_le(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_lt(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_ge(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_gt(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_idiv(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_mod(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_rem(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_add(unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_mul(unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_sub(unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_add(expr* s, expr* t, expr_ref& result);
br_status mk_mul(expr* s, expr* t, expr_ref& result);
br_status mk_sub(expr* s, expr* t, expr_ref& result);
br_status mk_uminus(expr* e, expr_ref & result);
bool is_bv2int(expr* e, expr_ref& s);
bool is_sbv2int(expr* e, expr_ref& s);
bool is_bv2int_diff(expr* e, expr_ref& s, expr_ref& t);
bool is_zero(expr* e);
bool is_shl1(expr* e, expr_ref& s);
expr* mk_bv_add(expr* s, expr* t, bool is_signed);
expr* mk_bv_mul(expr* s, expr* t, bool is_signed);
expr* mk_sbv2int(expr* s);
expr* mk_extend(unsigned sz, expr* b, bool is_signed);
void align_sizes(expr_ref& s, expr_ref& t, bool is_signed);
};
struct bv2int_rewriter_cfg : public default_rewriter_cfg {
bv2int_rewriter m_r;
bool rewrite_patterns() const { return false; }
bool flat_assoc(func_decl * f) const { return false; }
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0;
return m_r.mk_app_core(f, num, args, result);
}
bv2int_rewriter_cfg(ast_manager & m, bv2int_rewriter_ctx& ctx):m_r(m, ctx) {}
};
class bv2int_rewriter_star : public rewriter_tpl<bv2int_rewriter_cfg> {
bv2int_rewriter_cfg m_cfg;
public:
bv2int_rewriter_star(ast_manager & m, bv2int_rewriter_ctx& ctx):
rewriter_tpl<bv2int_rewriter_cfg>(m, false, m_cfg),
m_cfg(m, ctx) {}
};
#endif

695
lib/bv2real_rewriter.cpp
View file

@ -1,695 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
bv2real_rewriter.cpp
Abstract:
Basic rewriting rules for bv2real propagation.
Author:
Nikolaj (nbjorner) 2011-08-05
Notes:
--*/
#include"bv2real_rewriter.h"
#include"rewriter_def.h"
#include"ast_pp.h"
#include"for_each_expr.h"
bv2real_util::bv2real_util(ast_manager& m, rational const& default_root, rational const& default_divisor, unsigned max_num_bits) :
m_manager(m),
m_arith(m),
m_bv(m),
m_decls(m),
m_pos_le(m),
m_pos_lt(m),
m_side_conditions(m),
m_default_root(default_root),
m_default_divisor(default_divisor),
m_max_divisor(rational(2)*default_divisor),
m_max_num_bits(max_num_bits) {
sort* real = m_arith.mk_real();
sort* domain[2] = { real, real };
m_pos_lt = m.mk_fresh_func_decl("<","",2,domain,m.mk_bool_sort());
m_pos_le = m.mk_fresh_func_decl("<=","",2,domain,m.mk_bool_sort());
m_decls.push_back(m_pos_lt);
m_decls.push_back(m_pos_le);
}
bool bv2real_util::is_bv2real(func_decl* f) const {
return m_decl2sig.contains(f);
}
bool bv2real_util::is_bv2real(func_decl* f, unsigned num_args, expr* const* args,
expr*& m, expr*& n, rational& d, rational& r) const {
bvr_sig sig;
if (!m_decl2sig.find(f, sig)) {
return false;
}
SASSERT(num_args == 2);
m = args[0];
n = args[1];
d = sig.m_d;
r = sig.m_r;
SASSERT(sig.m_d.is_int() && sig.m_d.is_pos());
SASSERT(sig.m_r.is_int() && sig.m_r.is_pos());
SASSERT(m_bv.get_bv_size(m) == sig.m_msz);
SASSERT(m_bv.get_bv_size(n) == sig.m_nsz);
return true;
}
bool bv2real_util::is_bv2real(expr* e, expr*& m, expr*& n, rational& d, rational& r) const {
if (!is_app(e)) return false;
func_decl* f = to_app(e)->get_decl();
return is_bv2real(f, to_app(e)->get_num_args(), to_app(e)->get_args(), m, n, d, r);
}
class bv2real_util::contains_bv2real_proc {
bv2real_util const& m_util;
public:
class found {};
contains_bv2real_proc(bv2real_util const& u): m_util(u) {}
void operator()(app* a) {
if (m_util.is_bv2real(a->get_decl())) {
throw found();
}
}
void operator()(var*) {}
void operator()(quantifier*) {}
};
bool bv2real_util::contains_bv2real(expr* e) const {
contains_bv2real_proc p(*this);
try {
for_each_expr(p, e);
}
catch (contains_bv2real_proc::found) {
return true;
}
return false;
}
bool bv2real_util::mk_bv2real(expr* _s, expr* _t, rational& d, rational& r, expr_ref& result) {
expr_ref s(_s,m()), t(_t,m());
if (align_divisor(s, t, d)) {
result = mk_bv2real_c(s, t, d, r);
return true;
}
else {
return false;
}
}
expr* bv2real_util::mk_bv2real_c(expr* s, expr* t, rational const& d, rational const& r) {
bvr_sig sig;
sig.m_msz = m_bv.get_bv_size(s);
sig.m_nsz = m_bv.get_bv_size(t);
sig.m_d = d;
sig.m_r = r;
func_decl* f;
if (!m_sig2decl.find(sig, f)) {
sort* domain[2] = { m_manager.get_sort(s), m_manager.get_sort(t) };
sort* real = m_arith.mk_real();
f = m_manager.mk_fresh_func_decl("bv2real", "", 2, domain, real);
m_decls.push_back(f);
m_sig2decl.insert(sig, f);
m_decl2sig.insert(f, sig);
}
return m_manager.mk_app(f, s, t);
}
void bv2real_util::mk_bv2real_reduced(expr* s, expr* t, rational const& d, rational const& r, expr_ref & result) {
expr_ref s1(m()), t1(m()), r1(m());
rational num;
mk_sbv2real(s, s1);
mk_sbv2real(t, t1);
mk_div(s1, d, s1);
mk_div(t1, d, t1);
r1 = a().mk_power(a().mk_numeral(r, false), a().mk_numeral(rational(1,2),false));
t1 = a().mk_mul(t1, r1);
result = a().mk_add(s1, t1);
}
void bv2real_util::mk_div(expr* e, rational const& d, expr_ref& result) {
result = a().mk_div(e, a().mk_numeral(rational(d), false));
}
void bv2real_util::mk_sbv2real(expr* e, expr_ref& result) {
rational r;
unsigned bv_size = m_bv.get_bv_size(e);
rational bsize = power(rational(2), bv_size);
expr_ref bvr(a().mk_to_real(m_bv.mk_bv2int(e)), m());
expr_ref c(m_bv.mk_sle(m_bv.mk_numeral(rational(0), bv_size), e), m());
result = m().mk_ite(c, bvr, a().mk_sub(bvr, a().mk_numeral(bsize, false)));
}
expr* bv2real_util::mk_bv_mul(rational const& n, expr* t) {
if (n.is_one()) return t;
expr* s = mk_sbv(n);
return mk_bv_mul(s, t);
}
void bv2real_util::align_divisors(expr_ref& s1, expr_ref& s2, expr_ref& t1, expr_ref& t2, rational& d1, rational& d2) {
if (d1 == d2) {
return;
}
// s/d1 ~ t/d2 <=> lcm*s/d1 ~ lcm*t/d2 <=> (lcm/d1)*s ~ (lcm/d2)*t
// s/d1 ~ t/d2 <=> s/gcd*d1' ~ t/gcd*d2' <=> d2'*s/lcm ~ d1'*t/lcm
rational g = gcd(d1,d2);
rational l = lcm(d1,d2);
rational d1g = d1/g;
rational d2g = d2/g;
s1 = mk_bv_mul(d2g, s1);
s2 = mk_bv_mul(d2g, s2);
t1 = mk_bv_mul(d1g, t1);
t2 = mk_bv_mul(d1g, t2);
d1 = l;
d2 = l;
}
expr* bv2real_util::mk_bv_mul(expr* s, expr* t) {
SASSERT(m_bv.is_bv(s));
SASSERT(m_bv.is_bv(t));
if (is_zero(s)) {
return s;
}
if (is_zero(t)) {
return t;
}
expr_ref s1(s, m()), t1(t, m());
align_sizes(s1, t1);
unsigned n = m_bv.get_bv_size(t1);
unsigned max_bits = get_max_num_bits();
bool add_side_conds = 2*n > max_bits;
if (n >= max_bits) {
// nothing
}
else if (2*n > max_bits) {
s1 = mk_extend(max_bits-n, s1);
t1 = mk_extend(max_bits-n, t1);
}
else {
s1 = mk_extend(n, s1);
t1 = mk_extend(n, t1);
}
if (add_side_conds) {
add_side_condition(m_bv.mk_bvsmul_no_ovfl(s1, t1));
add_side_condition(m_bv.mk_bvsmul_no_udfl(s1, t1));
}
return m_bv.mk_bv_mul(s1, t1);
}
bool bv2real_util::is_zero(expr* n) {
rational r;
unsigned sz;
return m_bv.is_numeral(n, r, sz) && r.is_zero();
}
expr* bv2real_util::mk_bv_add(expr* s, expr* t) {
SASSERT(m_bv.is_bv(s));
SASSERT(m_bv.is_bv(t));
if (is_zero(s)) {
return t;
}
if (is_zero(t)) {
return s;
}
expr_ref s1(s, m()), t1(t, m());
align_sizes(s1, t1);
s1 = mk_extend(1, s1);
t1 = mk_extend(1, t1);
return m_bv.mk_bv_add(s1, t1);
}
void bv2real_util::align_sizes(expr_ref& s, expr_ref& t) {
unsigned sz1 = m_bv.get_bv_size(s);
unsigned sz2 = m_bv.get_bv_size(t);
if (sz1 > sz2) {
t = mk_extend(sz1-sz2, t);
}
else if (sz1 < sz2) {
s = mk_extend(sz2-sz1, s);
}
}
expr* bv2real_util::mk_sbv(rational const& n) {
SASSERT(n.is_int());
if (n.is_neg()) {
rational m = abs(n);
unsigned nb = m.get_num_bits();
return m_bv.mk_bv_neg(m_bv.mk_numeral(m, nb+1));
}
else {
unsigned nb = n.get_num_bits();
return m_bv.mk_numeral(n, nb+1);
}
}
expr* bv2real_util::mk_bv_sub(expr* s, expr* t) {
expr_ref s1(s, m()), t1(t, m());
align_sizes(s1, t1);
s1 = mk_extend(1, s1);
t1 = mk_extend(1, t1);
return m_bv.mk_bv_sub(s1, t1);
}
expr* bv2real_util::mk_extend(unsigned sz, expr* b) {
if (sz == 0) {
return b;
}
rational r;
unsigned bv_sz;
if (m_bv.is_numeral(b, r, bv_sz) &&
power(rational(2),bv_sz-1) > r) {
return m_bv.mk_numeral(r, bv_sz + sz);
}
return m_bv.mk_sign_extend(sz, b);
}
bool bv2real_util::is_bv2real(expr* n, expr_ref& s, expr_ref& t, rational& d, rational& r) {
expr* _s, *_t;
if (is_bv2real(n, _s, _t, d, r)) {
s = _s;
t = _t;
return true;
}
rational k;
bool is_int;
if (m_arith.is_numeral(n, k, is_int) && !is_int) {
d = denominator(k);
r = default_root();
s = mk_sbv(numerator(k));
t = mk_sbv(rational(0));
return true;
}
return false;
}
bool bv2real_util::align_divisor(expr_ref& s, expr_ref& t, rational& d) {
if (d > max_divisor()) {
//
// if divisor is over threshold, then divide s and t
// add side condition that s, t are divisible.
//
rational overflow = d / max_divisor();
if (!overflow.is_int()) return false;
if (!mk_is_divisible_by(s, overflow)) return false;
if (!mk_is_divisible_by(t, overflow)) return false;
d = max_divisor();
}
return true;
}
bool bv2real_util::mk_is_divisible_by(expr_ref& s, rational const& _overflow) {
rational overflow(_overflow);
SASSERT(overflow.is_int());
SASSERT(overflow.is_pos());
SASSERT(!overflow.is_one());
TRACE("bv2real_rewriter",
tout << mk_pp(s, m()) << " " << overflow << "\n";);
unsigned power2 = 0;
while ((overflow % rational(2)) == rational(0)) {
power2++;
overflow = div(overflow, rational(2));
}
if (power2 > 0) {
unsigned sz = m_bv.get_bv_size(s);
if (sz <= power2) {
add_side_condition(m().mk_eq(s, m_bv.mk_numeral(rational(0), sz)));
s = m_bv.mk_numeral(rational(0), 1);
}
else {
expr* s1 = m_bv.mk_extract(power2-1, 0, s);
add_side_condition(m().mk_eq(s1, m_bv.mk_numeral(rational(0), power2)));
s = m_bv.mk_extract(sz-1, power2, s);
}
}
TRACE("bv2real_rewriter",
tout << mk_pp(s, m()) << " " << overflow << "\n";);
return overflow.is_one();
}
// ---------------------------------------------------------------------
// bv2real_rewriter
bv2real_rewriter::bv2real_rewriter(ast_manager& m, bv2real_util& util):
m_manager(m),
m_util(util),
m_bv(m),
m_arith(m)
{}
br_status bv2real_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
TRACE("bv2real_rewriter",
tout << mk_pp(f, m()) << " ";
for (unsigned i = 0; i < num_args; ++i) {
tout << mk_pp(args[i], m()) << " ";
}
tout << "\n";);
if(f->get_family_id() == m_arith.get_family_id()) {
switch (f->get_decl_kind()) {
case OP_NUM: return BR_FAILED;
case OP_LE: SASSERT(num_args == 2); return mk_le(args[0], args[1], result);
case OP_GE: SASSERT(num_args == 2); return mk_ge(args[0], args[1], result);
case OP_LT: SASSERT(num_args == 2); return mk_lt(args[0], args[1], result);
case OP_GT: SASSERT(num_args == 2); return mk_gt(args[0], args[1], result);
case OP_ADD: return mk_add(num_args, args, result);
case OP_MUL: return mk_mul(num_args, args, result);
case OP_SUB: return mk_sub(num_args, args, result);
case OP_DIV: SASSERT(num_args == 2); return mk_div(args[0], args[1], result);
case OP_IDIV: return BR_FAILED;
case OP_MOD: return BR_FAILED;
case OP_REM: return BR_FAILED;
case OP_UMINUS: SASSERT(num_args == 1); return mk_uminus(args[0], result);
case OP_TO_REAL: return BR_FAILED; // TBD
case OP_TO_INT: return BR_FAILED; // TBD
case OP_IS_INT: return BR_FAILED; // TBD
default: return BR_FAILED;
}
}
if (f->get_family_id() == m().get_basic_family_id()) {
switch (f->get_decl_kind()) {
case OP_EQ: SASSERT(num_args == 2); return mk_eq(args[0], args[1], result);
case OP_ITE: SASSERT(num_args == 3); return mk_ite(args[0], args[1], args[2], result);
default: return BR_FAILED;
}
}
if (u().is_pos_ltf(f)) {
SASSERT(num_args == 2);
return mk_lt_pos(args[0], args[1], result);
}
if (u().is_pos_lef(f)) {
SASSERT(num_args == 2);
return mk_le_pos(args[0], args[1], result);
}
return BR_FAILED;
}
bool bv2real_rewriter::mk_le(expr* s, expr* t, bool is_pos, bool is_neg, expr_ref& result) {
expr_ref s1(m()), s2(m()), t1(m()), t2(m());
rational d1, d2, r1, r2;
SASSERT(is_pos || is_neg);
if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) &&
r1 == r2 && r1 == rational(2)) {
//
// (s1 + s2*sqrt(2))/d1 <= (t1 + t2*sqrt(2))/d2
// <=>
//
// let s1 = s1*d2-t1*d1, t2 = s2*d2-t2*d1
//
//
// s1 + s2*sqrt(2) <= 0
// <=
// s1 + s2*approx(sign(s2),sqrt(2)) <= 0
// or (s1 = 0 & s2 = 0)
//
// If s2 is negative use an under-approximation for sqrt(r).
// If s2 is positive use an over-approximation for sqrt(r).
// e.g., r = 2, then 5/4 and 3/2 are under/over approximations.
// Then s1 + s2*approx(sign(s2), r) <= 0 => s1 + s2*sqrt(r) <= 0
u().align_divisors(s1, s2, t1, t2, d1, d2);
s1 = u().mk_bv_sub(s1, t1);
s2 = u().mk_bv_sub(s2, t2);
unsigned s2_size = m_bv.get_bv_size(s2);
expr_ref le_proxy(m().mk_fresh_const("le_proxy",m().mk_bool_sort()), m());
u().add_aux_decl(to_app(le_proxy)->get_decl());
expr_ref gt_proxy(m().mk_not(le_proxy), m());
expr_ref s2_is_nonpos(m_bv.mk_sle(s2, m_bv.mk_numeral(rational(0), s2_size)), m());
expr_ref under(u().mk_bv_add(u().mk_bv_mul(rational(4), s1), u().mk_bv_mul(rational(5), s2)), m());
expr_ref z1(m_bv.mk_numeral(rational(0), m_bv.get_bv_size(under)), m());
expr_ref le_under(m_bv.mk_sle(under, z1), m());
expr_ref over(u().mk_bv_add(u().mk_bv_mul(rational(2), s1), u().mk_bv_mul(rational(3), s2)), m());
expr_ref z2(m_bv.mk_numeral(rational(0), m_bv.get_bv_size(over)), m());
expr_ref le_over(m_bv.mk_sle(over, z2), m());
// predicate may occur in positive polarity.
if (is_pos) {
// s1 + s2*sqrt(2) <= 0 <== s2 <= 0 & s1 + s2*(5/4) <= 0; 4*s1 + 5*s2 <= 0
expr* e1 = m().mk_implies(m().mk_and(le_proxy, s2_is_nonpos), le_under);
// s1 + s2*sqrt(2) <= 0 <== s2 > 0 & s1 + s2*(3/2); 0 <=> 2*s1 + 3*s2 <= 0
expr* e2 = m().mk_implies(m().mk_and(le_proxy, m().mk_not(s2_is_nonpos)), le_over);
u().add_side_condition(e1);
u().add_side_condition(e2);
}
// predicate may occur in negative polarity.
if (is_neg) {
// s1 + s2*sqrt(2) > 0 <== s2 > 0 & s1 + s2*(5/4) > 0; 4*s1 + 5*s2 > 0
expr* e3 = m().mk_implies(m().mk_and(gt_proxy, m().mk_not(s2_is_nonpos)), m().mk_not(le_under));
// s1 + s2*sqrt(2) > 0 <== s2 <= 0 & s1 + s2*(3/2) > 0 <=> 2*s1 + 3*s2 > 0
expr* e4 = m().mk_implies(m().mk_and(gt_proxy, s2_is_nonpos), m().mk_not(le_over));
u().add_side_condition(e3);
u().add_side_condition(e4);
}
TRACE("bv2real_rewriter", tout << "mk_le\n";);
if (is_pos) {
result = le_proxy;
}
else {
result = gt_proxy;
}
return true;
}
return false;
}
br_status bv2real_rewriter::mk_le_pos(expr * s, expr * t, expr_ref & result) {
if (mk_le(s, t, true, false, result)) {
return BR_DONE;
}
return BR_FAILED;
}
br_status bv2real_rewriter::mk_lt_pos(expr * s, expr * t, expr_ref & result) {
if (mk_le(t, s, false, true, result)) {
return BR_DONE;
}
return BR_FAILED;
}
br_status bv2real_rewriter::mk_le(expr * s, expr * t, expr_ref & result) {
expr_ref s1(m()), s2(m()), t1(m()), t2(m());
rational d1, d2, r1, r2;
if (mk_le(s, t, true, true, result)) {
return BR_DONE;
}
if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) {
//
// somewhat expensive approach without having
// polarity information for sound approximation.
//
// Convert to:
// t1 + t2*sqrt(r) >= 0
// then to:
//
// (t1 >= 0 && t2 <= 0 => t1^2 >= t2^2*r)
// (t1 <= 0 && t2 >= 0 => t1^2 <= t2^2*r)
// (t1 >= 0 || t2 >= 0)
//
// A cheaper approach is to approximate > under the assumption
// that > occurs in positive polarity.
// then if t2 is negative use an over-approximation for sqrt(r)
// if t2 is positive use an under-approximation for sqrt(r).
// e.g., r = 2, then 5/4 and 3/2 are under/over approximations.
// Then t1 + t2*approx(sign(t2), r) > 0 => t1 + t2*sqrt(r) > 0
//
u().align_divisors(s1, s2, t1, t2, d1, d2);
t1 = u().mk_bv_sub(t1, s1);
t2 = u().mk_bv_sub(t2, s2);
expr_ref z1(m()), z2(m());
z1 = m_bv.mk_numeral(rational(0), m_bv.get_bv_size(t1));
z2 = m_bv.mk_numeral(rational(0), m_bv.get_bv_size(t2));
expr* gz1 = m_bv.mk_sle(z1, t1);
expr* lz1 = m_bv.mk_sle(t1, z1);
expr* gz2 = m_bv.mk_sle(z2, t2);
expr* lz2 = m_bv.mk_sle(t2, z2);
expr_ref t12(u().mk_bv_mul(t1, t1), m());
expr_ref t22(u().mk_bv_mul(r1, u().mk_bv_mul(t2, t2)), m());
u().align_sizes(t12, t22);
expr* ge = m_bv.mk_sle(t22, t12);
expr* le = m_bv.mk_sle(t12, t22);
expr* e1 = m().mk_or(gz1, gz2);
expr* e2 = m().mk_or(m().mk_not(gz1), m().mk_not(lz2), ge);
expr* e3 = m().mk_or(m().mk_not(gz2), m().mk_not(lz1), le);
result = m().mk_and(e1, e2, e3);
TRACE("bv2real_rewriter", tout << "\n";);
return BR_DONE;
}
return BR_FAILED;
}
br_status bv2real_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) {
result = m().mk_not(m_arith.mk_le(arg2, arg1));
return BR_REWRITE2;
}
br_status bv2real_rewriter::mk_ge(expr * arg1, expr * arg2, expr_ref & result) {
return mk_le(arg2, arg1, result);
}
br_status bv2real_rewriter::mk_gt(expr * arg1, expr * arg2, expr_ref & result) {
result = m().mk_not(m_arith.mk_le(arg1, arg2));
return BR_REWRITE2;
}
br_status bv2real_rewriter::mk_ite(expr* c, expr* s, expr* t, expr_ref& result) {
expr_ref s1(m()), s2(m()), t1(m()), t2(m());
rational d1, d2, r1, r2;
if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) {
u().align_divisors(s1, s2, t1, t2, d1, d2);
u().align_sizes(s1, t1);
u().align_sizes(s2, t2);
if (u().mk_bv2real(m().mk_ite(c, s1, t1), m().mk_ite(c, s2, t2), d1, r1, result)) {
return BR_DONE;
}
}
return BR_FAILED;
}
br_status bv2real_rewriter::mk_eq(expr * s, expr * t, expr_ref & result) {
expr_ref s1(m()), s2(m()), t1(m()), t2(m());
rational d1, d2, r1, r2;
if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) {
u().align_divisors(s1, s2, t1, t2, d1, d2);
u().align_sizes(s1, t1);
u().align_sizes(s2, t2);
result = m().mk_and(m().mk_eq(s1, t1), m().mk_eq(s2, t2));
return BR_DONE;
}
return BR_FAILED;
}
br_status bv2real_rewriter::mk_uminus(expr * s, expr_ref & result) {
expr_ref s1(m()), s2(m());
rational d1, r1;
if (u().is_bv2real(s, s1, s2, d1, r1)) {
s1 = u().mk_extend(1, s1);
s2 = u().mk_extend(1, s2);
if (u().mk_bv2real(m_bv.mk_bv_neg(s1), m_bv.mk_bv_neg(s2), d1, r1, result)) {
return BR_DONE;
}
}
return BR_FAILED;
}
br_status bv2real_rewriter::mk_add(unsigned num_args, expr * const* args, expr_ref& result) {
br_status r = BR_DONE;
SASSERT(num_args > 0);
result = args[0];
for (unsigned i = 1; r == BR_DONE && i < num_args; ++i) {
r = mk_add(result, args[i], result);
}
return r;
}
br_status bv2real_rewriter::mk_add(expr* s, expr* t, expr_ref& result) {
expr_ref s1(m()), s2(m()), t1(m()), t2(m());
rational d1, d2, r1, r2;
if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) {
u().align_divisors(s1, s2, t1, t2, d1, d2);
if (u().mk_bv2real(u().mk_bv_add(s1, t1), u().mk_bv_add(t2, s2), d1, r1, result)) {
return BR_DONE;
}
}
return BR_FAILED;
}
br_status bv2real_rewriter::mk_mul(unsigned num_args, expr * const* args, expr_ref& result) {
br_status r = BR_DONE;
SASSERT(num_args > 0);
result = args[0];
for (unsigned i = 1; r == BR_DONE && i < num_args; ++i) {
r = mk_mul(result, args[i], result);
}
return r;
}
br_status bv2real_rewriter::mk_div(expr* s, expr* t, expr_ref& result) {
return BR_FAILED;
}
br_status bv2real_rewriter::mk_mul(expr* s, expr* t, expr_ref& result) {
// TBD: optimize
expr_ref s1(m()), t1(m()), s2(m()), t2(m());
rational d1, d2, r1, r2;
if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) {
// s1*t1 + r1*(s2*t2) + (s1*t2 + s2*t2)*r1
expr_ref u1(m()), u2(m());
u1 = u().mk_bv_add(u().mk_bv_mul(s1, t1), u().mk_bv_mul(r1, u().mk_bv_mul(t2, s2)));
u2 = u().mk_bv_add(u().mk_bv_mul(s1, t2), u().mk_bv_mul(s2, t1));
rational tmp = d1*d2;
if (u().mk_bv2real(u1, u2, tmp, r1, result)) {
return BR_DONE;
}
}
return BR_FAILED;
}
br_status bv2real_rewriter::mk_sub(unsigned num_args, expr * const* args, expr_ref& result) {
br_status r = BR_DONE;
SASSERT(num_args > 0);
result = args[0];
for (unsigned i = 1; r == BR_DONE && i < num_args; ++i) {
r = mk_sub(result, args[i], result);
}
return r;
}
br_status bv2real_rewriter::mk_sub(expr* s, expr* t, expr_ref& result) {
expr_ref s1(m()), s2(m()), t1(m()), t2(m());
rational d1, d2, r1, r2;
if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) {
u().align_divisors(s1, s2, t1, t2, d1, d2);
if (u().mk_bv2real(u().mk_bv_sub(s1, t1), u().mk_bv_sub(s2, t2), d1, r1, result)) {
return BR_DONE;
}
}
return BR_FAILED;
}
template class rewriter_tpl<bv2real_rewriter_cfg>;
br_status bv2real_elim_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
expr* m, *n;
rational d, r;
if (m_util.is_bv2real(f, num_args, args, m, n, d, r)) {
m_util.mk_bv2real_reduced(m, n, d, r, result);
return BR_REWRITE_FULL;
}
return BR_FAILED;
}
template class rewriter_tpl<bv2real_elim_rewriter_cfg>;

233
lib/bv2real_rewriter.h
View file

@ -1,233 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
bv2real_rewriter.h
Abstract:
Basic rewriting rules for bv2real propagation.
Author:
Nikolaj (nbjorner) 2011-08-05
Notes:
--*/
#ifndef _BV2REAL_REWRITER_H_
#define _BV2REAL_REWRITER_H_
#include"ast.h"
#include"rewriter.h"
#include"bv_decl_plugin.h"
#include"arith_decl_plugin.h"
//
// bv2real[d,r](n,m) has interpretation:
// sbv2int(n)/d + sbv2int(m)/d*sqrt(r)
// where
// sbv2int is signed bit-vector 2 integer.
//
class bv2real_util {
struct bvr_sig {
unsigned m_msz, m_nsz;
rational m_d, m_r;
};
struct bvr_eq {
bool operator()(bvr_sig const& x, bvr_sig const& y) const {
return
x.m_msz == y.m_msz &&
x.m_nsz == y.m_nsz &&
x.m_d == y.m_d &&
x.m_r == y.m_r;
}
};
struct bvr_hash {
unsigned operator()(bvr_sig const& x) const {
unsigned a[3] = { x.m_msz, x.m_nsz, x.m_d.hash() };
return string_hash((char const*)a, 12, x.m_r.hash());
}
};
ast_manager& m_manager;
arith_util m_arith;
bv_util m_bv;
func_decl_ref_vector m_decls;
func_decl_ref m_pos_le;
func_decl_ref m_pos_lt;
expr_ref_vector m_side_conditions;
map<bvr_sig, func_decl*, bvr_hash, bvr_eq> m_sig2decl;
obj_map<func_decl, bvr_sig> m_decl2sig;
rational m_default_root;
rational m_default_divisor;
rational m_max_divisor;
unsigned m_max_num_bits;
class contains_bv2real_proc;
public:
bv2real_util(ast_manager& m, rational const& default_root, rational const& default_divisor, unsigned max_num_bits);
void reset() { m_side_conditions.reset(); }
bool is_bv2real(func_decl* f) const;
bool is_bv2real(func_decl* f, unsigned num_args, expr* const* args,
expr*& m, expr*& n, rational& d, rational& r) const;
bool is_bv2real(expr* e, expr*& n, expr*& m, rational& d, rational& r) const;
bool is_bv2real(expr* e, expr*& n, expr*& m, rational& d);
bool contains_bv2real(expr* e) const;
bool mk_bv2real(expr* s, expr* t, rational& d, rational& r, expr_ref& result);
expr* mk_bv2real_c(expr* s, expr* t, rational const& d, rational const& r);
expr* mk_bv2real(expr* n, expr* m) { return mk_bv2real_c(n, m, default_divisor(), default_root()); }
void mk_bv2real_reduced(expr* s, expr* t, expr_ref & result) { mk_bv2real_reduced(s, t, default_divisor(), default_root(), result); }
void mk_bv2real_reduced(expr* s, expr* t, rational const& d, rational const& r, expr_ref & result);
//
// Positive polarity comparison operators.
// Translation of positive polarity comparison requires fewer clauses.
//
bool is_pos_ltf(func_decl* f) const { return f == m_pos_lt; }
bool is_pos_lef(func_decl* f) const { return f == m_pos_le; }
bool is_pos_lt(expr const* e) const { return is_app(e) && is_pos_ltf(to_app(e)->get_decl()); }
bool is_pos_le(expr const* e) const { return is_app(e) && is_pos_lef(to_app(e)->get_decl()); }
MATCH_BINARY(is_pos_lt);
MATCH_BINARY(is_pos_le);
expr* mk_pos_lt(expr* s, expr* t) { return m().mk_app(m_pos_lt, s, t); }
expr* mk_pos_le(expr* s, expr* t) { return m().mk_app(m_pos_le, s, t); }
rational const& default_root() const { return m_default_root; }
rational const& default_divisor() const { return m_default_divisor; }
rational const& max_divisor() const { return m_max_divisor; }
unsigned get_max_num_bits() const { return m_max_num_bits; }
void add_side_condition(expr* e) { m_side_conditions.push_back(e); }
unsigned num_side_conditions() const { return m_side_conditions.size(); }
expr* const* side_conditions() const { return m_side_conditions.c_ptr(); }
bool is_zero(expr* e);
expr* mk_bv_add(expr* s, expr* t);
expr* mk_bv_sub(expr* s, expr* t);
expr* mk_bv_mul(expr* s, expr* t);
expr* mk_bv_mul(rational const& n, expr* t);
expr* mk_extend(unsigned sz, expr* b);
expr* mk_sbv(rational const& n);
void align_sizes(expr_ref& s, expr_ref& t);
void align_divisors(expr_ref& s1, expr_ref& s2, expr_ref& t1, expr_ref& t2, rational& d1, rational& d2);
bool is_bv2real(expr* n, expr_ref& s, expr_ref& t, rational& d, rational& r);
bool align_divisor(expr_ref& s, expr_ref& t, rational& d);
bool mk_is_divisible_by(expr_ref& s, rational const& _overflow);
void add_aux_decl(func_decl* f) { m_decls.push_back(f); }
unsigned num_aux_decls() const { return m_decls.size(); }
func_decl* get_aux_decl(unsigned i) const { return m_decls[i]; }
private:
ast_manager & m() const { return m_manager; }
arith_util & a() { return m_arith; }
void mk_div(expr* e, rational const& d, expr_ref& result);
void mk_sbv2real(expr* e, expr_ref& result);
};
class bv2real_rewriter {
ast_manager & m_manager;
bv2real_util& m_util;
bv_util m_bv;
arith_util m_arith;
public:
bv2real_rewriter(ast_manager & m, bv2real_util& util);
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
private:
ast_manager & m() const { return m_manager; }
arith_util & a() { return m_arith; }
bv2real_util& u() { return m_util; }
br_status mk_eq(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_ite(expr* c, expr* s, expr* t, expr_ref& result);
bool mk_le(expr* s, expr* t, bool is_pos, bool is_neg, expr_ref& result);
br_status mk_le(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_lt(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_le_pos(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_lt_pos(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_ge(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_gt(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_add(unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_mul(unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_sub(unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_div(expr* s, expr* t, expr_ref& result);
br_status mk_add(expr* s, expr* t, expr_ref& result);
br_status mk_mul(expr* s, expr* t, expr_ref& result);
br_status mk_sub(expr* s, expr* t, expr_ref& result);
br_status mk_uminus(expr* e, expr_ref & result);
};
struct bv2real_rewriter_cfg : public default_rewriter_cfg {
bv2real_rewriter m_r;
bool rewrite_patterns() const { return false; }
bool flat_assoc(func_decl * f) const { return false; }
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0;
return m_r.mk_app_core(f, num, args, result);
}
bv2real_rewriter_cfg(ast_manager & m, bv2real_util& u):m_r(m, u) {}
};
class bv2real_rewriter_star : public rewriter_tpl<bv2real_rewriter_cfg> {
bv2real_rewriter_cfg m_cfg;
public:
bv2real_rewriter_star(ast_manager & m, bv2real_util& u):
rewriter_tpl<bv2real_rewriter_cfg>(m, false, m_cfg),
m_cfg(m, u) {}
};
/**
\brief replace le(bv2real(a),bv2real(b)) by under-approximation.
*/
class bv2real_elim_rewriter {
bv2real_util& m_util;
public:
bv2real_elim_rewriter(bv2real_util& util) : m_util(util) {}
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
};
struct bv2real_elim_rewriter_cfg : public default_rewriter_cfg {
bv2real_elim_rewriter m_r;
bool rewrite_patterns() const { return false; }
bool flat_assoc(func_decl * f) const { return false; }
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0;
return m_r.mk_app_core(f, num, args, result);
}
bv2real_elim_rewriter_cfg(bv2real_util& u):m_r(u) {}
};
class bv2real_elim_rewriter_star : public rewriter_tpl<bv2real_elim_rewriter_cfg> {
bv2real_elim_rewriter_cfg m_cfg;
public:
bv2real_elim_rewriter_star(ast_manager & m, bv2real_util& u):
rewriter_tpl<bv2real_elim_rewriter_cfg>(m, false, m_cfg),
m_cfg(u) {}
};
#endif

712
lib/cofactor_elim_term_ite.cpp
View file

@ -1,712 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
cofactor_elim_term_ite.cpp
Abstract:
Eliminate term if-then-else's using cofactors.
Author:
Leonardo de Moura (leonardo) 2011-06-05.
Revision History:
--*/
#include"cofactor_elim_term_ite.h"
#include"mk_simplified_app.h"
#include"rewriter_def.h"
#include"cooperate.h"
#include"for_each_expr.h"
#include"ast_smt2_pp.h"
#include"ast_ll_pp.h"
#include"tactic.h"
struct cofactor_elim_term_ite::imp {
ast_manager & m;
params_ref m_params;
unsigned long long m_max_memory;
volatile bool m_cancel;
void checkpoint() {
cooperate("cofactor ite");
if (memory::get_allocation_size() > m_max_memory)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
if (m_cancel)
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
}
// Collect atoms that contain term if-then-else
struct analyzer {
struct frame {
expr * m_t;
unsigned m_first:1;
unsigned m_form_ctx:1;
frame(expr * t, bool form_ctx):m_t(t), m_first(true), m_form_ctx(form_ctx) {}
};
ast_manager & m;
imp & m_owner;
obj_hashtable<expr> m_candidates;
expr_fast_mark1 m_processed;
expr_fast_mark2 m_has_term_ite;
svector<frame> m_frame_stack;
analyzer(ast_manager & _m, imp & owner):m(_m), m_owner(owner) {}
void push_frame(expr * t, bool form_ctx) {
m_frame_stack.push_back(frame(t, form_ctx && m.is_bool(t)));
}
void visit(expr * t, bool form_ctx, bool & visited) {
if (!m_processed.is_marked(t)) {
visited = false;
push_frame(t, form_ctx);
}
}
void save_candidate(expr * t, bool form_ctx) {
if (!form_ctx)
return;
if (!m.is_bool(t))
return;
if (!m_has_term_ite.is_marked(t))
return;
if (!is_app(t))
return;
if (to_app(t)->get_family_id() == m.get_basic_family_id()) {
switch (to_app(t)->get_decl_kind()) {
case OP_OR:
case OP_AND:
case OP_NOT:
case OP_XOR:
case OP_IMPLIES:
case OP_TRUE:
case OP_FALSE:
case OP_ITE:
case OP_IFF:
return;
case OP_EQ:
case OP_DISTINCT:
if (m.is_bool(to_app(t)->get_arg(0)))
return;
break;
default:
break;
}
}
// it is an atom in a formula context (i.e., it is not nested inside a term),
// and it contains a term if-then-else.
m_candidates.insert(t);
}
void operator()(expr * t) {
SASSERT(m.is_bool(t));
push_frame(t, true);
SASSERT(!m_frame_stack.empty());
while (!m_frame_stack.empty()) {
frame & fr = m_frame_stack.back();
expr * t = fr.m_t;
bool form_ctx = fr.m_form_ctx;
TRACE("cofactor_ite_analyzer", tout << "processing, form_ctx: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
m_owner.checkpoint();
if (m_processed.is_marked(t)) {
save_candidate(t, form_ctx);
m_frame_stack.pop_back();
continue;
}
if (m.is_term_ite(t)) {
m_has_term_ite.mark(t);
m_processed.mark(t);
m_frame_stack.pop_back();
continue;
}
if (fr.m_first) {
fr.m_first = false;
bool visited = true;
if (is_app(t)) {
unsigned num_args = to_app(t)->get_num_args();
for (unsigned i = 0; i < num_args; i++)
visit(to_app(t)->get_arg(i), form_ctx, visited);
}
// ignoring quantifiers
if (!visited)
continue;
}
if (is_app(t)) {
unsigned num_args = to_app(t)->get_num_args();
unsigned i;
for (i = 0; i < num_args; i++) {
if (m_has_term_ite.is_marked(to_app(t)->get_arg(i)))
break;
}
if (i < num_args) {
m_has_term_ite.mark(t);
TRACE("cofactor_ite_analyzer", tout << "saving candidate: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
save_candidate(t, form_ctx);
}
}
else {
SASSERT(is_quantifier(t) || is_var(t));
// ignoring quantifiers... they are treated as black boxes.
}
m_processed.mark(t);
m_frame_stack.pop_back();
}
m_processed.reset();
m_has_term_ite.reset();
}
};
expr * get_first(expr * t) {
typedef std::pair<expr *, unsigned> frame;
expr_fast_mark1 visited;
sbuffer<frame> stack;
stack.push_back(frame(t, 0));
while (!stack.empty()) {
start:
checkpoint();
frame & fr = stack.back();
expr * curr = fr.first;
if (m.is_term_ite(curr))
return to_app(curr)->get_arg(0);
switch (curr->get_kind()) {
case AST_VAR:
case AST_QUANTIFIER:
// ignore quantifiers
stack.pop_back();
break;
case AST_APP: {
unsigned num_args = to_app(curr)->get_num_args();
while (fr.second < num_args) {
expr * arg = to_app(curr)->get_arg(fr.second);
fr.second++;
if (arg->get_ref_count() > 1) {
if (visited.is_marked(arg))
continue;
visited.mark(arg);
}
switch (arg->get_kind()) {
case AST_VAR:
case AST_QUANTIFIER:
// ingore quantifiers
break;
case AST_APP:
if (to_app(arg)->get_num_args() > 0) {
stack.push_back(frame(arg, 0));
goto start;
}
break;
default:
UNREACHABLE();
break;
}
}
stack.pop_back();
break;
}
default:
UNREACHABLE();
break;
}
}
return 0;
}
/**
\brief Fuctor for selecting the term if-then-else condition with the most number of occurrences.
*/
expr * get_best(expr * t) {
typedef std::pair<expr *, unsigned> frame;
obj_map<expr, unsigned> occs;
expr_fast_mark1 visited;
sbuffer<frame> stack;
stack.push_back(frame(t, 0));
while (!stack.empty()) {
start:
checkpoint();
frame & fr = stack.back();
expr * curr = fr.first;
switch (curr->get_kind()) {
case AST_VAR:
case AST_QUANTIFIER:
// ignore quantifiers
stack.pop_back();
break;
case AST_APP: {
unsigned num_args = to_app(curr)->get_num_args();
bool is_term_ite = m.is_term_ite(curr);
while (fr.second < num_args) {
expr * arg = to_app(curr)->get_arg(fr.second);
if (fr.second == 0 && is_term_ite) {
unsigned num = 0;
if (occs.find(arg, num))
occs.insert(arg, num+1);
else
occs.insert(arg, 1);
}
fr.second++;
if (arg->get_ref_count() > 1) {
if (visited.is_marked(arg))
continue;
visited.mark(arg);
}
switch (arg->get_kind()) {
case AST_VAR:
case AST_QUANTIFIER:
// ingore quantifiers
break;
case AST_APP:
if (to_app(arg)->get_num_args() > 0) {
stack.push_back(frame(arg, 0));
goto start;
}
break;
default:
UNREACHABLE();
break;
}
}
stack.pop_back();
break;
}
default:
UNREACHABLE();
break;
}
}
expr * best = 0;
unsigned best_occs = 0;
obj_map<expr, unsigned>::iterator it = occs.begin();
obj_map<expr, unsigned>::iterator end = occs.end();
for (; it != end; ++it) {
if ((!best) ||
(get_depth(it->m_key) < get_depth(best)) ||
(get_depth(it->m_key) == get_depth(best) && it->m_value > best_occs) ||
// break ties by giving preference to equalities
(get_depth(it->m_key) == get_depth(best) && it->m_value == best_occs && m.is_eq(it->m_key) && !m.is_eq(best))) {
best = it->m_key;
best_occs = it->m_value;
}
}
visited.reset();
CTRACE("cofactor_ite_get_best", best != 0, tout << "best num-occs: " << best_occs << "\n" << mk_ismt2_pp(best, m) << "\n";);
return best;
}
void updt_params(params_ref const & p) {
m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
}
void set_cancel(bool f) {
m_cancel = f;
}
struct cofactor_rw_cfg : public default_rewriter_cfg {
ast_manager & m;
imp & m_owner;
obj_hashtable<expr> * m_has_term_ite;
mk_simplified_app m_mk_app;
expr * m_atom;
bool m_sign;
expr * m_term;
app * m_value;
bool m_strict_lower;
app * m_lower;
bool m_strict_upper;
app * m_upper;
cofactor_rw_cfg(ast_manager & _m, imp & owner, obj_hashtable<expr> * has_term_ite = 0):
m(_m),
m_owner(owner),
m_has_term_ite(has_term_ite),
m_mk_app(m, owner.m_params) {
}
bool max_steps_exceeded(unsigned num_steps) const {
m_owner.checkpoint();
return false;
}
bool pre_visit(expr * t) {
return true;
}
void set_cofactor_atom(expr * t) {
if (m.is_not(t)) {
m_atom = to_app(t)->get_arg(0);
m_sign = true;
m_term = 0;
// TODO: bounds
}
else {
m_atom = t;
m_sign = false;
m_term = 0;
expr * lhs;
expr * rhs;
if (m.is_eq(t, lhs, rhs)) {
if (m.is_value(lhs)) {
m_term = rhs;
m_value = to_app(lhs);
TRACE("set_cofactor_atom", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
}
else if (m.is_value(rhs)) {
m_term = lhs;
m_value = to_app(rhs);
TRACE("set_cofactor_atom", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
}
}
// TODO: bounds
}
}
bool rewrite_patterns() const { return false; }
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0;
return m_mk_app.mk_core(f, num, args, result);
}
bool get_subst(expr * s, expr * & t, proof * & pr) {
pr = 0;
if (s == m_atom) {
t = m_sign ? m.mk_false() : m.mk_true();
return true;
}
if (s == m_term && m_value != 0) {
t = m_value;
return true;
}
// TODO: handle simple bounds
// Example: s is of the form (<= s 10) and m_term == s, and m_upper is 9
// then rewrite to true.
return false;
}
};
struct cofactor_rw : rewriter_tpl<cofactor_rw_cfg> {
cofactor_rw_cfg m_cfg;
public:
cofactor_rw(ast_manager & m, imp & owner, obj_hashtable<expr> * has_term_ite = 0):
rewriter_tpl<cofactor_rw_cfg>(m, false, m_cfg),
m_cfg(m, owner, has_term_ite) {
}
void set_cofactor_atom(expr * t) {
m_cfg.set_cofactor_atom(t);
reset();
}
};
struct main_rw_cfg : public default_rewriter_cfg {
ast_manager & m;
imp & m_owner;
cofactor_rw m_cofactor;
obj_hashtable<expr> const & m_candidates;
obj_map<expr, expr*> m_cache;
expr_ref_vector m_cache_domain;
main_rw_cfg(ast_manager & _m, imp & owner, obj_hashtable<expr> & candidates):
m(_m),
m_owner(owner),
m_cofactor(m, m_owner),
m_candidates(candidates),
m_cache_domain(_m) {
}
bool max_steps_exceeded(unsigned num_steps) const {
m_owner.checkpoint();
return false;
}
bool pre_visit(expr * t) {
return m.is_bool(t) && !is_quantifier(t);
}
bool get_subst(expr * s, expr * & t, proof * & t_pr) {
if (m_candidates.contains(s)) {
t_pr = 0;
if (m_cache.find(s, t))
return true;
unsigned step = 0;
TRACE("cofactor_ite", tout << "cofactor target:\n" << mk_ismt2_pp(s, m) << "\n";);
expr_ref curr(m);
curr = s;
while (true) {
// expr * c = m_owner.get_best(curr);
expr * c = m_owner.get_first(curr);
if (c == 0) {
m_cache.insert(s, curr);
m_cache_domain.push_back(curr);
t = curr.get();
return true;
}
step++;
expr_ref pos_cofactor(m);
expr_ref neg_cofactor(m);
m_cofactor.set_cofactor_atom(c);
m_cofactor(curr, pos_cofactor);
expr_ref neg_c(m);
neg_c = m.is_not(c) ? to_app(c)->get_arg(0) : m.mk_not(c);
m_cofactor.set_cofactor_atom(neg_c);
m_cofactor(curr, neg_cofactor);
curr = m.mk_ite(c, pos_cofactor, neg_cofactor);
TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
}
}
return false;
}
};
struct main_rw : rewriter_tpl<main_rw_cfg> {
main_rw_cfg m_cfg;
public:
main_rw(ast_manager & m, imp & owner, obj_hashtable<expr> & candidates):
rewriter_tpl<main_rw_cfg>(m, false, m_cfg),
m_cfg(m, owner, candidates) {
}
};
struct bottom_up_elim {
typedef std::pair<expr*, bool> frame;
ast_manager & m;
imp & m_owner;
obj_map<expr, expr*> m_cache;
expr_ref_vector m_cache_domain;
obj_hashtable<expr> m_has_term_ite;
svector<frame> m_frames;
cofactor_rw m_cofactor;
bottom_up_elim(ast_manager & _m, imp & owner):
m(_m),
m_owner(owner),
m_cache_domain(m),
m_cofactor(m, owner, &m_has_term_ite) {
}
bool is_atom(expr * t) const {
if (!m.is_bool(t))
return false;
if (!is_app(t))
return false;
if (to_app(t)->get_family_id() == m.get_basic_family_id()) {
switch (to_app(t)->get_decl_kind()) {
case OP_EQ:
case OP_DISTINCT:
if (m.is_bool(to_app(t)->get_arg(0)))
return false;
else
return true;
default:
return false;
}
}
return true;
}
void cofactor(expr * t, expr_ref & r) {
unsigned step = 0;
TRACE("cofactor_ite", tout << "cofactor target:\n" << mk_ismt2_pp(t, m) << "\n";);
expr_ref curr(m);
curr = t;
while (true) {
expr * c = m_owner.get_best(curr);
// expr * c = m_owner.get_first(curr);
if (c == 0) {
r = curr.get();
return;
}
step++;
expr_ref pos_cofactor(m);
expr_ref neg_cofactor(m);
m_cofactor.set_cofactor_atom(c);
m_cofactor(curr, pos_cofactor);
expr_ref neg_c(m);
neg_c = m.is_not(c) ? to_app(c)->get_arg(0) : m.mk_not(c);
m_cofactor.set_cofactor_atom(neg_c);
m_cofactor(curr, neg_cofactor);
if (pos_cofactor == neg_cofactor) {
curr = pos_cofactor;
TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
continue;
}
if (m.is_true(pos_cofactor) && m.is_false(neg_cofactor)) {
curr = c;
TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
continue;
}
if (m.is_false(pos_cofactor) && m.is_true(neg_cofactor)) {
curr = neg_c;
TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
continue;
}
curr = m.mk_ite(c, pos_cofactor, neg_cofactor);
TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
}
}
void visit(expr * t, bool & visited) {
if (!m_cache.contains(t)) {
m_frames.push_back(frame(t, true));
visited = false;
}
}
void operator()(expr * t, expr_ref & r) {
ptr_vector<expr> new_args;
m_frames.push_back(frame(t, true));
while (!m_frames.empty()) {
m_owner.checkpoint();
frame & fr = m_frames.back();
expr * t = fr.first;
TRACE("cofactor_bug", tout << "processing: " << t->get_id() << " :first " << fr.second << "\n";);
if (!is_app(t)) {
m_cache.insert(t, t);
m_frames.pop_back();
continue;
}
if (m_cache.contains(t)) {
m_frames.pop_back();
continue;
}
if (fr.second) {
fr.second = false;
bool visited = true;
unsigned i = to_app(t)->get_num_args();
while (i > 0) {
--i;
expr * arg = to_app(t)->get_arg(i);
visit(arg, visited);
}
if (!visited)
continue;
}
new_args.reset();
bool has_new_args = false;
bool has_term_ite = false;
unsigned num = to_app(t)->get_num_args();
for (unsigned i = 0; i < num; i++) {
expr * arg = to_app(t)->get_arg(i);
expr * new_arg = 0;
TRACE("cofactor_bug", tout << "collecting child: " << arg->get_id() << "\n";);
m_cache.find(arg, new_arg);
SASSERT(new_arg != 0);
if (new_arg != arg)
has_new_args = true;
if (m_has_term_ite.contains(new_arg))
has_term_ite = true;
new_args.push_back(new_arg);
}
if (m.is_term_ite(t))
has_term_ite = true;
expr_ref new_t(m);
if (has_new_args)
new_t = m.mk_app(to_app(t)->get_decl(), num, new_args.c_ptr());
else
new_t = t;
if (has_term_ite && is_atom(new_t)) {
// update new_t
expr_ref new_new_t(m);
m_has_term_ite.insert(new_t);
cofactor(new_t, new_new_t);
m_has_term_ite.erase(new_t);
new_t = new_new_t;
has_term_ite = false;
}
if (has_term_ite)
m_has_term_ite.insert(new_t);
SASSERT(new_t.get() != 0);
TRACE("cofactor_bug", tout << "caching: " << t->get_id() << "\n";);
#if 0
counter ++;
verbose_stream() << counter << "\n";
#endif
m_cache.insert(t, new_t);
m_cache_domain.push_back(new_t);
m_frames.pop_back();
}
expr * result = 0;
m_cache.find(t, result);
r = result;
}
};
imp(ast_manager & _m, params_ref const & p):
m(_m),
m_params(p) {
m_cancel = false;
updt_params(p);
}
void operator()(expr * t, expr_ref & r) {
#if 0
analyzer proc(m, *this);
proc(t);
main_rw rw(m, *this, proc.m_candidates);
rw(t, r);
#else
bottom_up_elim proc(m, *this);
proc(t, r);
#endif
}
};
cofactor_elim_term_ite::cofactor_elim_term_ite(ast_manager & m, params_ref const & p):
m_imp(alloc(imp, m, p)),
m_params(p) {
}
cofactor_elim_term_ite::~cofactor_elim_term_ite() {
imp * d = m_imp;
#pragma omp critical (cofactor_elim_term_ite)
{
m_imp = 0;
}
dealloc(d);
}
void cofactor_elim_term_ite::updt_params(params_ref const & p) {
m_imp->updt_params(p);
}
void cofactor_elim_term_ite::get_param_descrs(param_descrs & r) {
}
void cofactor_elim_term_ite::operator()(expr * t, expr_ref & r) {
m_imp->operator()(t, r);
}
void cofactor_elim_term_ite::set_cancel(bool f) {
#pragma omp critical (cofactor_elim_term_ite)
{
if (m_imp)
m_imp->set_cancel(f);
}
}
void cofactor_elim_term_ite::cleanup() {
ast_manager & m = m_imp->m;
#pragma omp critical (cofactor_elim_term_ite)
{
dealloc(m_imp);
m_imp = alloc(imp, m, m_params);
}
}

44
lib/cofactor_elim_term_ite.h
View file

@ -1,44 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
cofactor_elim_term_ite.h
Abstract:
Eliminate (ground) term if-then-else's using cofactors.
Author:
Leonardo de Moura (leonardo) 2011-06-05.
Revision History:
--*/
#ifndef _COFACTOR_ELIM_TERM_ITE_H_
#define _COFACTOR_ELIM_TERM_ITE_H_
#include"ast.h"
#include"params.h"
class cofactor_elim_term_ite {
struct imp;
imp * m_imp;
params_ref m_params;
public:
cofactor_elim_term_ite(ast_manager & m, params_ref const & p = params_ref());
virtual ~cofactor_elim_term_ite();
void updt_params(params_ref const & p);
static void get_param_descrs(param_descrs & r);
void operator()(expr * t, expr_ref & r);
void cancel() { set_cancel(true); }
void reset_cancel() { set_cancel(false); }
void set_cancel(bool f);
void cleanup();
};
#endif

82
lib/cofactor_term_ite_tactic.cpp
View file

@ -1,82 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
cofactor_term_ite_tactic.cpp
Abstract:
Wrap cofactor_elim_term_ite as a tactic.
Eliminate (ground) term if-then-else's using cofactors.
Author:
Leonardo de Moura (leonardo) 2012-02-20.
Revision History:
--*/
#include"tactical.h"
#include"cofactor_elim_term_ite.h"
/**
\brief Wrapper for applying cofactor_elim_term_ite in an assertion set.
*/
class cofactor_term_ite_tactic : public tactic {
params_ref m_params;
cofactor_elim_term_ite m_elim_ite;
void process(goal & g) {
ast_manager & m = g.m();
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
if (g.inconsistent())
break;
expr * f = g.form(i);
expr_ref new_f(m);
m_elim_ite(f, new_f);
g.update(i, new_f);
}
}
public:
cofactor_term_ite_tactic(ast_manager & m, params_ref const & p):
m_params(p),
m_elim_ite(m, p) {
}
virtual tactic * translate(ast_manager & m) {
return alloc(cofactor_term_ite_tactic, m, m_params);
}
virtual ~cofactor_term_ite_tactic() {}
virtual void updt_params(params_ref const & p) { m_params = p; m_elim_ite.updt_params(p); }
static void get_param_descrs(param_descrs & r) { cofactor_elim_term_ite::get_param_descrs(r); }
virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
SASSERT(g->is_well_sorted());
fail_if_proof_generation("cofactor-term-ite", g);
fail_if_unsat_core_generation("cofactor-term-ite", g);
tactic_report report("cofactor-term-ite", *g);
mc = 0; pc = 0; core = 0;
process(*(g.get()));
g->inc_depth();
result.push_back(g.get());
TRACE("cofactor-term-ite", g->display(tout););
SASSERT(g->is_well_sorted());
}
virtual void cleanup() { return m_elim_ite.cleanup(); }
virtual void set_cancel(bool f) { m_elim_ite.set_cancel(f); }
};
tactic * mk_cofactor_term_ite_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(cofactor_term_ite_tactic, m, p));
}

29
lib/cofactor_term_ite_tactic.h
View file

@ -1,29 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
cofactor_term_ite_tactic.h
Abstract:
Wrap cofactor_elim_term_ite as a tactic.
Eliminate (ground) term if-then-else's using cofactors.
Author:
Leonardo de Moura (leonardo) 2012-02-20.
Revision History:
--*/
#ifndef _COFACTOR_TERM_ITE_TACTIC_H_
#define _COFACTOR_TERM_ITE_TACTIC_H_
#include"params.h"
class ast_manager;
class tactic;
tactic * mk_cofactor_term_ite_tactic(ast_manager & m, params_ref const & p = params_ref());
#endif

1509
lib/datalog_parser.cpp
View file

File diff suppressed because it is too large Load diff

48
lib/datalog_parser.h
View file

@ -1,48 +0,0 @@
/*++
Copyright (c) 2010 Microsoft Corporation
Module Name:
datalog_parser.h
Abstract:
Parser for Datalogish files
Author:
Nikolaj Bjorner (nbjorner) 2010-5-17
Revision History:
--*/
#ifndef _DATALOG_PARSER_H_
#define _DATALOG_PARSER_H_
#include "ast.h"
#include "dl_context.h"
namespace datalog {
class parser {
public:
static parser * create(context& ctx, ast_manager & ast_manager);
virtual ~parser() {}
virtual bool parse_file(char const * path) = 0;
virtual bool parse_string(char const * string) = 0;
};
class wpa_parser {
public:
static wpa_parser * create(context& ctx, ast_manager & ast_manager);
virtual ~wpa_parser() {}
virtual bool parse_directory(char const * path) = 0;
};
};
#endif

383
lib/dbg_cmds.cpp
View file

@ -1,383 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
dbg_cmds.cpp
Abstract:
SMT2 front-end commands for debugging purposes.
Author:
Leonardo (leonardo) 2011-04-01
Notes:
--*/
#include<iomanip>
#include"cmd_context.h"
#include"cmd_util.h"
#include"rewriter.h"
#include"shared_occs.h"
#include"for_each_expr.h"
#include"rewriter.h"
#include"bool_rewriter.h"
#include"ast_lt.h"
#include"simplify_cmd.h"
#include"ast_smt2_pp.h"
#include"bound_manager.h"
#include"used_vars.h"
#include"var_subst.h"
#ifndef _EXTERNAL_RELEASE
BINARY_SYM_CMD(get_quantifier_body_cmd,
"dbg-get-qbody",
"<symbol> <quantifier>",
"store the body of the quantifier in the global variable <symbol>",
CPK_EXPR,
expr *, {
if (!is_quantifier(arg))
throw cmd_exception("invalid command, term must be a quantifier");
store_expr_ref(ctx, m_sym, to_quantifier(arg)->get_expr());
});
BINARY_SYM_CMD(set_cmd,
"dbg-set",
"<symbol> <term>",
"store <term> in the global variable <symbol>",
CPK_EXPR,
expr *, {
store_expr_ref(ctx, m_sym, arg);
});
UNARY_CMD(pp_var_cmd, "dbg-pp-var", "<symbol>", "pretty print a global variable that references an AST", CPK_SYMBOL, symbol const &, {
expr * t = get_expr_ref(ctx, arg);
SASSERT(t != 0);
ctx.display(ctx.regular_stream(), t);
ctx.regular_stream() << std::endl;
});
BINARY_SYM_CMD(shift_vars_cmd,
"dbg-shift-vars",
"<symbol> <uint>",
"shift the free variables by <uint> in the term referenced by the global variable <symbol>, the result is stored in <symbol>",
CPK_UINT,
unsigned, {
expr * t = get_expr_ref(ctx, m_sym);
expr_ref r(ctx.m());
var_shifter s(ctx.m());
s(t, arg, r);
store_expr_ref(ctx, m_sym, r.get());
});
UNARY_CMD(pp_shared_cmd, "dbg-pp-shared", "<term>", "display shared subterms of the given term", CPK_EXPR, expr *, {
shared_occs s(ctx.m());
s(arg);
ctx.regular_stream() << "(shared";
shared_occs::iterator it = s.begin_shared();
shared_occs::iterator end = s.end_shared();
for (; it != end; ++it) {
expr * curr = *it;
ctx.regular_stream() << std::endl << " ";
ctx.display(ctx.regular_stream(), curr, 2);
}
ctx.regular_stream() << ")" << std::endl;
});
UNARY_CMD(num_shared_cmd, "dbg-num-shared", "<term>", "return the number of shared subterms", CPK_EXPR, expr *, {
shared_occs s(ctx.m());
s(arg);
ctx.regular_stream() << s.num_shared() << std::endl;
});
UNARY_CMD(size_cmd, "dbg-size", "<term>", "return the size of the given term", CPK_EXPR, expr *, {
ctx.regular_stream() << get_num_exprs(arg) << std::endl;
});
class subst_cmd : public cmd {
unsigned m_idx;
expr * m_source;
symbol m_target;
ptr_vector<expr> m_subst;
public:
subst_cmd():cmd("dbg-subst") {}
virtual char const * get_usage() const { return "<symbol> (<symbol>*) <symbol>"; }
virtual char const * get_descr() const { return "substitute the free variables in the AST referenced by <symbol> using the ASTs referenced by <symbol>*"; }
virtual unsigned get_arity() const { return 3; }
virtual void prepare(cmd_context & ctx) { m_idx = 0; m_source = 0; }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
if (m_idx == 1) return CPK_SYMBOL_LIST;
return CPK_SYMBOL;
}
virtual void set_next_arg(cmd_context & ctx, symbol const & s) {
if (m_idx == 0) {
m_source = get_expr_ref(ctx, s);
}
else {
m_target = s;
}
m_idx++;
}
virtual void set_next_arg(cmd_context & ctx, unsigned num, symbol const * s) {
m_subst.reset();
unsigned i = num;
while (i > 0) {
--i;
m_subst.push_back(get_expr_ref(ctx, s[i]));
}
m_idx++;
}
virtual void execute(cmd_context & ctx) {
expr_ref r(ctx.m());
beta_reducer p(ctx.m());
p(m_source, m_subst.size(), m_subst.c_ptr(), r);
store_expr_ref(ctx, m_target, r.get());
}
};
UNARY_CMD(bool_rewriter_cmd, "dbg-bool-rewriter", "<term>", "apply the Boolean rewriter to the given term", CPK_EXPR, expr *, {
expr_ref t(ctx.m());
params_ref p;
p.set_bool(":flat", false);
SASSERT(p.get_bool(":flat", true) == false);
bool_rewriter_star r(ctx.m(), p);
r(arg, t);
ctx.display(ctx.regular_stream(), t);
ctx.regular_stream() << std::endl;
});
UNARY_CMD(bool_frewriter_cmd, "dbg-bool-flat-rewriter", "<term>", "apply the Boolean (flattening) rewriter to the given term", CPK_EXPR, expr *, {
expr_ref t(ctx.m());
{
params_ref p;
p.set_bool(":flat", true);
bool_rewriter_star r(ctx.m(), p);
r(arg, t);
}
ctx.display(ctx.regular_stream(), t);
ctx.regular_stream() << std::endl;
});
UNARY_CMD(elim_and_cmd, "dbg-elim-and", "<term>", "apply the Boolean rewriter (eliminating AND operator and flattening) to the given term", CPK_EXPR, expr *, {
expr_ref t(ctx.m());
{
params_ref p;
p.set_bool(":flat", true);
p.set_bool(":elim-and", true);
bool_rewriter_star r(ctx.m(), p);
r(arg, t);
}
ctx.display(ctx.regular_stream(), t);
ctx.regular_stream() << std::endl;
});
class lt_cmd : public cmd {
expr * m_t1;
expr * m_t2;
public:
lt_cmd():cmd("dbg-lt") {}
virtual char const * get_usage() const { return "<term> <term>"; }
virtual char const * get_descr(cmd_context & ctx) const { return "return true if the first term is smaller than the second one in the internal Z3 total order on terms."; }
virtual unsigned get_arity() const { return 2; }
virtual void prepare(cmd_context & ctx) { m_t1 = 0; }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_EXPR; }
virtual void set_next_arg(cmd_context & ctx, expr * arg) {
if (m_t1 == 0)
m_t1 = arg;
else
m_t2 = arg;
}
virtual void execute(cmd_context & ctx) {
bool r = lt(m_t1, m_t2);
ctx.regular_stream() << (r ? "true" : "false") << std::endl;
}
};
UNARY_CMD(some_value_cmd, "dbg-some-value", "<sort>", "retrieve some value of the given sort", CPK_SORT, sort *, {
ast_manager & m = ctx.m();
expr_ref val(m);
val = m.get_some_value(arg);
ctx.display(ctx.regular_stream(), val);
ctx.regular_stream() << std::endl;
});
void tst_params(cmd_context & ctx) {
params_ref p1;
params_ref p2;
p1.set_uint(":val", 100);
p2 = p1;
SASSERT(p2.get_uint(":val", 0) == 100);
p2.set_uint(":val", 200);
SASSERT(p2.get_uint(":val", 0) == 200);
SASSERT(p1.get_uint(":val", 0) == 100);
p2 = p1;
SASSERT(p2.get_uint(":val", 0) == 100);
SASSERT(p1.get_uint(":val", 0) == 100);
ctx.regular_stream() << "worked" << std::endl;
}
ATOMIC_CMD(params_cmd, "dbg-params", "test parameters", tst_params(ctx););
UNARY_CMD(translator_cmd, "dbg-translator", "<term>", "test AST translator", CPK_EXPR, expr *, {
ast_manager & m = ctx.m();
scoped_ptr<ast_manager> m2 = alloc(ast_manager, m.proof_mode());
ast_translation proc(m, *m2);
expr_ref s(m);
expr_ref t(*m2);
s = arg;
t = proc(s.get());
ctx.regular_stream() << mk_ismt2_pp(s, m) << "\n--->\n" << mk_ismt2_pp(t, *m2) << std::endl;
});
UNARY_CMD(sexpr_cmd, "dbg-sexpr", "<sexpr>", "display an s-expr", CPK_SEXPR, sexpr *, {
arg->display(ctx.regular_stream());
ctx.regular_stream() << std::endl;
});
static void tst_bound_manager(cmd_context & ctx) {
ast_manager & m = ctx.m();
assertion_set s(m);
assert_exprs_from(ctx, s);
bound_manager bc(m);
bc(s);
bc.display(ctx.regular_stream());
}
#define GUARDED_CODE(CODE) try { CODE } catch (z3_error & ex) { throw ex; } catch (z3_exception & ex) { ctx.regular_stream() << "(error \"" << escaped(ex.msg()) << "\")" << std::endl; }
ATOMIC_CMD(bounds_cmd, "dbg-bounds", "test bound manager", GUARDED_CODE(tst_bound_manager(ctx);));
UNARY_CMD(set_next_id, "dbg-set-next-id", "<unsigned>", "set the next expression id to be at least the given value", CPK_UINT, unsigned, {
ctx.m().set_next_expr_id(arg);
});
UNARY_CMD(used_vars_cmd, "dbg-used-vars", "<expr>", "test used_vars functor", CPK_EXPR, expr *, {
used_vars proc;
if (is_quantifier(arg))
arg = to_quantifier(arg)->get_expr();
proc(arg);
ctx.regular_stream() << "(vars";
for (unsigned i = 0; i < proc.get_max_found_var_idx_plus_1(); i++) {
sort * s = proc.get(i);
ctx.regular_stream() << "\n (" << std::left << std::setw(6) << i << " ";
if (s != 0)
ctx.display(ctx.regular_stream(), s, 10);
else
ctx.regular_stream() << "<not-used>";
ctx.regular_stream() << ")";
}
ctx.regular_stream() << ")" << std::endl;
});
UNARY_CMD(elim_unused_vars_cmd, "dbg-elim-unused-vars", "<expr>", "eliminate unused vars from a quantifier", CPK_EXPR, expr *, {
if (!is_quantifier(arg)) {
ctx.display(ctx.regular_stream(), arg);
return;
}
expr_ref r(ctx.m());
elim_unused_vars(ctx.m(), to_quantifier(arg), r);
SASSERT(!is_quantifier(r) || !to_quantifier(r)->may_have_unused_vars());
ctx.display(ctx.regular_stream(), r);
ctx.regular_stream() << std::endl;
});
class instantiate_cmd_core : public cmd {
protected:
quantifier * m_q;
ptr_vector<expr> m_args;
public:
instantiate_cmd_core(char const * name):cmd(name) {}
virtual char const * get_usage() const { return "<quantifier> (<symbol>*)"; }
virtual char const * get_descr() const { return "instantiate the quantifier using the given expressions."; }
virtual unsigned get_arity() const { return 2; }
virtual void prepare(cmd_context & ctx) { m_q = 0; m_args.reset(); }
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
if (m_q == 0) return CPK_EXPR;
else return CPK_EXPR_LIST;
}
virtual void set_next_arg(cmd_context & ctx, expr * s) {
if (!is_quantifier(s))
throw cmd_exception("invalid command, quantifier expected.");
m_q = to_quantifier(s);
}
virtual void set_next_arg(cmd_context & ctx, unsigned num, expr * const * ts) {
if (num != m_q->get_num_decls())
throw cmd_exception("invalid command, mismatch between the number of quantified variables and the number of arguments.");
unsigned i = num;
while (i > 0) {
--i;
sort * s = ctx.m().get_sort(ts[i]);
if (s != m_q->get_decl_sort(i)) {
std::ostringstream buffer;
buffer << "invalid command, sort mismatch at position " << i;
throw cmd_exception(buffer.str());
}
}
m_args.append(num, ts);
}
virtual void execute(cmd_context & ctx) {
expr_ref r(ctx.m());
instantiate(ctx.m(), m_q, m_args.c_ptr(), r);
ctx.display(ctx.regular_stream(), r);
ctx.regular_stream() << std::endl;
}
};
class instantiate_cmd : public instantiate_cmd_core {
public:
instantiate_cmd():instantiate_cmd_core("dbg-instantiate") {}
};
class instantiate_nested_cmd : public instantiate_cmd_core {
public:
instantiate_nested_cmd():instantiate_cmd_core("dbg-instantiate-nested") {}
virtual char const * get_descr() const { return "instantiate the quantifier nested in the outermost quantifier, this command is used to test the instantiation procedure with quantifiers that contain free variables."; }
virtual void set_next_arg(cmd_context & ctx, expr * s) {
instantiate_cmd_core::set_next_arg(ctx, s);
if (!is_quantifier(m_q->get_expr()))
throw cmd_exception("invalid command, nested quantifier expected");
m_q = to_quantifier(m_q->get_expr());
}
};
#endif
void install_dbg_cmds(cmd_context & ctx) {
#ifndef _EXTERNAL_RELEASE
ctx.insert(alloc(get_quantifier_body_cmd));
ctx.insert(alloc(set_cmd));
ctx.insert(alloc(pp_var_cmd));
ctx.insert(alloc(shift_vars_cmd));
ctx.insert(alloc(pp_shared_cmd));
ctx.insert(alloc(num_shared_cmd));
ctx.insert(alloc(size_cmd));
ctx.insert(alloc(subst_cmd));
ctx.insert(alloc(bool_rewriter_cmd));
ctx.insert(alloc(bool_frewriter_cmd));
ctx.insert(alloc(elim_and_cmd));
install_simplify_cmd(ctx, "dbg-th-rewriter");
ctx.insert(alloc(lt_cmd));
ctx.insert(alloc(some_value_cmd));
ctx.insert(alloc(params_cmd));
ctx.insert(alloc(translator_cmd));
ctx.insert(alloc(sexpr_cmd));
ctx.insert(alloc(bounds_cmd));
ctx.insert(alloc(used_vars_cmd));
ctx.insert(alloc(elim_unused_vars_cmd));
ctx.insert(alloc(instantiate_cmd));
ctx.insert(alloc(instantiate_nested_cmd));
ctx.insert(alloc(set_next_id));
#endif
}

25
lib/dbg_cmds.h
View file

@ -1,25 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
dbg_cmds.h
Abstract:
SMT2 front-end commands for debugging purposes.
Author:
Leonardo (leonardo) 2011-04-01
Notes:
--*/
#ifndef _DBG_CMDS_H_
#define _DBG_CMDS_H_
class cmd_context;
void install_dbg_cmds(cmd_context & ctx);
#endif

232
lib/elim_distinct.cpp
View file

@ -1,232 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
elim_distinct.cpp
Abstract:
Replace one distinct(t0, ..., tn) with (t0 = 0 and ... and tn = n)
when the sort of t0...tn is uninterpreted.
Author:
Leonardo de Moura (leonardo) 2011-04-28
Revision History:
--*/
#include"elim_distinct.h"
#include"assertion_set.h"
#include"model_converter.h"
#include"arith_decl_plugin.h"
#include"rewriter_def.h"
#include"critical_flet.h"
struct elim_distinct::imp {
struct mc : public model_converter {
ast_ref_vector m_asts;
sort * m_usort;
obj_map<func_decl, func_decl *> m_inv_map;
public:
mc(ast_manager & m):m_asts(m) {
}
};
struct u2i_cfg : public default_rewriter_cfg {
arith_util m_autil;
ast_ref_vector m_asts;
sort * m_usort;
sort * m_int_sort;
obj_map<func_decl, func_decl *> m_f2f;
ast_manager & m() const { return m_asts.get_manager(); }
bool must_remap(func_decl * f) const {
if (f->get_range() == m_usort)
return true;
for (unsigned i = 0; i < f->get_arity(); i++) {
if (f->get_domain(i) == m_usort)
return true;
}
return false;
}
sort * remap(sort * s) {
return (s == m_usort) ? m_int_sort : s;
}
func_decl * remap(func_decl * f) {
ptr_buffer<sort> new_domain;
sort * new_range = remap(f->get_range());
for (unsigned i = 0; i < f->get_arity(); i++)
new_domain.push_back(remap(f->get_domain(i)));
func_decl * new_f = m().mk_func_decl(f->get_name(), new_domain.size(), new_domain.c_ptr(), new_range);
m_asts.push_back(new_f);
m_asts.push_back(f);
m_f2f.insert(f, new_f);
return new_f;
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0;
func_decl * new_f;
if (m_f2f.find(f, new_f)) {
result = m().mk_app(new_f, num, args);
return BR_DONE;
}
if (!must_remap(f))
return BR_FAILED;
if (m().is_eq(f)) {
result = m().mk_eq(args[0], args[1]);
return BR_DONE;
}
if (m().is_ite(f)) {
result = m().mk_ite(args[0], args[1], args[2]);
return BR_DONE;
}
if (f->get_family_id() != null_family_id || f->get_info() != 0) {
throw elim_distinct_exception("uninterpreted sort is used in interpreted function symbol");
}
new_f = remap(f);
result = m().mk_app(new_f, num, args);
return BR_DONE;
}
bool reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
throw elim_distinct_exception("elim-distinct tactic does not support quantifiers");
}
u2i_cfg(ast_manager & m, sort * u):
m_autil(m),
m_asts(m),
m_usort(u) {
m_asts.push_back(u);
m_int_sort = m_autil.mk_int();
m_asts.push_back(m_int_sort);
}
};
class u2i : public rewriter_tpl<u2i_cfg> {
u2i_cfg m_cfg;
public:
u2i(ast_manager & m, sort * u):
rewriter_tpl<u2i_cfg>(m, false, m_cfg),
m_cfg(m, u) {
if (m.proofs_enabled())
throw elim_distinct_exception("elim-distinct tactic does not support proof generation");
}
arith_util & autil() { return cfg().m_autil; }
};
ast_manager & m_manager;
u2i * m_u2i;
imp(ast_manager & m):m_manager(m), m_u2i(0) {}
ast_manager & m() const { return m_manager; }
bool is_distinct(expr * t) {
if (!m().is_distinct(t))
return false;
if (to_app(t)->get_num_args() == 0)
return false;
return m().is_uninterp(m().get_sort(to_app(t)->get_arg(0)));
}
model_converter * operator()(assertion_set & s, app * d) {
if (d && !is_distinct(d))
d = 0;
app * r = 0;
unsigned sz = s.size();
for (unsigned i = 0; i < sz; i++) {
expr * curr = s.form(i);
if (curr == d)
break;
if (is_distinct(curr)) {
if (!r || to_app(curr)->get_num_args() > r->get_num_args())
r = to_app(curr);
}
}
if (d != 0)
r = d;
if (r == 0)
return 0;
sort * u = m().get_sort(to_app(r)->get_arg(0));
u2i conv(m(), u);
{
critical_flet<u2i*> l1(m_u2i, &conv);
expr_ref new_curr(m());
for (unsigned i = 0; i < sz; i++) {
expr * curr = s.form(i);
if (curr == r) {
unsigned num = r->get_num_args();
for (unsigned j = 0; j < num; j++) {
expr * arg = r->get_arg(j);
conv(arg, new_curr);
expr * eq = m().mk_eq(new_curr, conv.autil().mk_numeral(rational(j), true));
s.assert_expr(eq);
}
new_curr = m().mk_true();
}
else {
conv(curr, new_curr);
}
s.update(i, new_curr);
}
}
// TODO: create model converter
return 0;
}
void cancel() {
// Remark: m_u2i is protected by the omp global critical section.
// If this is a performance problem, then replace critical_flet by a custom flet that uses a different
// section name
#pragma omp critical (critical_flet)
{
if (m_u2i)
m_u2i->cancel();
}
}
};
template class rewriter_tpl<elim_distinct::imp::u2i_cfg>;
elim_distinct::elim_distinct(ast_manager & m) {
m_imp = alloc(imp, m);
}
elim_distinct::~elim_distinct() {
dealloc(m_imp);
}
model_converter * elim_distinct::operator()(assertion_set & s, app * d) {
return m_imp->operator()(s, d);
}
void elim_distinct::cancel() {
m_imp->cancel();
}
void elim_distinct::reset() {
cleanup();
}
void elim_distinct::cleanup() {
ast_manager & m = m_imp->m();
dealloc(m_imp);
m_imp = alloc(imp, m);
}

54
lib/elim_distinct.h
View file

@ -1,54 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
elim_distinct.h
Abstract:
Replace one distinct(t0, ..., tn) with (t0 = 0 and ... and tn = n)
when the sort of t0...tn is uninterpreted.
Author:
Leonardo de Moura (leonardo) 2011-04-28
Revision History:
--*/
#ifndef _ELIM_DISTINCT_H_
#define _ELIM_DISTINCT_H_
#include"assertion_set.h"
class model_converter;
class ast_manager;
class assertion_set;
class elim_distinct_exception : public default_exception {
public:
elim_distinct_exception(char const * msg):default_exception(msg) {}
};
class elim_distinct {
struct imp;
imp * m_imp;
public:
elim_distinct(ast_manager & m);
~elim_distinct();
/**
\brief It throws an elim_distinct_exception if the strategy failed.
If d == 0, then search for the biggest distinct(t0, ..., tn) in the assertion set.
if d != 0, then succeed only if d is in the assertion set.
*/
model_converter * operator()(assertion_set & s, app * d);
void cancel();
void reset();
void cleanup();
};
#endif

174
lib/elim_term_ite_strategy.cpp
View file

@ -1,174 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
elim_term_ite_strategy.cpp
Abstract:
Eliminate term if-then-else by adding
new fresh auxiliary variables.
Author:
Leonardo (leonardo) 2011-06-15
Notes:
--*/
#include"elim_term_ite_strategy.h"
#include"defined_names.h"
#include"rewriter_def.h"
#include"filter_model_converter.h"
#include"cooperate.h"
struct elim_term_ite_strategy::imp {
struct rw_cfg : public default_rewriter_cfg {
ast_manager & m;
defined_names m_defined_names;
ref<filter_model_converter> m_mc;
assertion_set * m_set;
unsigned long long m_max_memory; // in bytes
bool m_produce_models;
unsigned m_num_fresh;
bool max_steps_exceeded(unsigned num_steps) const {
cooperate("elim term ite");
if (memory::get_allocation_size() > m_max_memory)
throw elim_term_ite_exception(STE_MAX_MEMORY_MSG);
return false;
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
if (!m.is_term_ite(f))
return BR_FAILED;
expr_ref new_ite(m);
new_ite = m.mk_app(f, num, args);
expr_ref new_def(m);
proof_ref new_def_pr(m);
app_ref _result(m);
if (m_defined_names.mk_name(new_ite, new_def, new_def_pr, _result, result_pr)) {
m_set->assert_expr(new_def, new_def_pr);
m_num_fresh++;
if (m_produce_models) {
if (!m_mc)
m_mc = alloc(filter_model_converter, m);
m_mc->insert(_result->get_decl());
}
}
result = _result.get();
return BR_DONE;
}
rw_cfg(ast_manager & _m, params_ref const & p):
m(_m),
m_defined_names(m, 0 /* don't use prefix */) {
updt_params(p);
m_set = 0;
m_num_fresh = 0;
}
void updt_params(params_ref const & p) {
m_max_memory = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
m_produce_models = p.get_bool(":produce-models", false);
}
};
struct rw : public rewriter_tpl<rw_cfg> {
rw_cfg m_cfg;
rw(ast_manager & m, params_ref const & p):
rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg),
m_cfg(m, p) {
}
};
ast_manager & m;
rw m_rw;
imp(ast_manager & _m, params_ref const & p):
m(_m),
m_rw(m, p) {
}
void set_cancel(bool f) {
m_rw.set_cancel(f);
}
void updt_params(params_ref const & p) {
m_rw.cfg().updt_params(p);
}
void operator()(assertion_set & s, model_converter_ref & mc) {
mc = 0;
if (s.inconsistent())
return;
{
as_st_report report("elim-term-ite", s);
m_rw.m_cfg.m_num_fresh = 0;
m_rw.m_cfg.m_set = &s;
expr_ref new_curr(m);
proof_ref new_pr(m);
unsigned size = s.size();
for (unsigned idx = 0; idx < size; idx++) {
expr * curr = s.form(idx);
m_rw(curr, new_curr, new_pr);
if (m.proofs_enabled()) {
proof * pr = s.pr(idx);
new_pr = m.mk_modus_ponens(pr, new_pr);
}
s.update(idx, new_curr, new_pr);
}
mc = m_rw.m_cfg.m_mc.get();
}
report_st_progress(":elim-term-ite-consts", m_rw.m_cfg.m_num_fresh);
}
};
elim_term_ite_strategy::elim_term_ite_strategy(ast_manager & m, params_ref const & p):
m_params(p) {
m_imp = alloc(imp, m, p);
}
elim_term_ite_strategy::~elim_term_ite_strategy() {
dealloc(m_imp);
}
void elim_term_ite_strategy::updt_params(params_ref const & p) {
m_params = p;
m_imp->updt_params(p);
}
void elim_term_ite_strategy::get_param_descrs(param_descrs & r) {
insert_max_memory(r);
insert_produce_models(r);
}
void elim_term_ite_strategy::operator()(assertion_set & s, model_converter_ref & mc) {
m_imp->operator()(s, mc);
}
void elim_term_ite_strategy::set_cancel(bool f) {
if (m_imp)
m_imp->set_cancel(f);
}
void elim_term_ite_strategy::cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
#pragma omp critical (as_st_cancel)
{
d = m_imp;
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (as_st_cancel)
{
m_imp = d;
}
}

53
lib/elim_term_ite_strategy.h
View file

@ -1,53 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
elim_term_ite_strategy.h
Abstract:
Eliminate term if-then-else by adding
new fresh auxiliary variables.
Author:
Leonardo (leonardo) 2011-06-15
Notes:
--*/
#ifndef _ELIM_TERM_ITE_STRATEGY_H_
#define _ELIM_TERM_ITE_STRATEGY_H_
#include"strategy_exception.h"
#include"model_converter.h"
#include"params.h"
#include"assertion_set_strategy.h"
class assertion_set;
MK_ST_EXCEPTION(elim_term_ite_exception);
class elim_term_ite_strategy : public assertion_set_strategy {
struct imp;
imp * m_imp;
params_ref m_params;
public:
elim_term_ite_strategy(ast_manager & m, params_ref const & p = params_ref());
virtual ~elim_term_ite_strategy();
virtual void updt_params(params_ref const & p);
static void get_param_descrs(param_descrs & r);
virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
virtual void operator()(assertion_set & s, model_converter_ref & mc);
virtual void cleanup();
virtual void set_cancel(bool f);
};
inline as_st * mk_elim_term_ite(ast_manager & m, params_ref const & p = params_ref()) {
return clean(alloc(elim_term_ite_strategy, m, p));
}
#endif

32
lib/parameters.h
View file

@ -1,32 +0,0 @@
/*++
Copyright (c) 2007 Microsoft Corporation
Module Name:
parameters.h
Abstract:
Settings and parameters supplied to pre-processing and solver
modules.
Author:
Leonardo de Moura (leonardo) 2006-10-18.
Nikolaj Bjorner (nbjorner) 2007-02-15
Revision History:
2007-02-15, nbjorner.
Hoisted out from simplify_parser.h and core_theory_types.h
in order to share functionality with SMTLIB and other
front-ends without bringing in the simplifier and core_theory.
--*/
#ifndef _PARAMETERS_H_
#define _PARAMETERS_H_
#include"sat_params.h"
#include"core_theory_params.h"
#include"front_end_params.h"
#endif

37
lib/pattern_inference_params.cpp
View file

@ -1,37 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
pattern_inference_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-03-24.
Revision History:
--*/
#include"pattern_inference_params.h"
void pattern_inference_params::register_params(ini_params & p) {
p.register_unsigned_param("PI_MAX_MULTI_PATTERNS", m_pi_max_multi_patterns,
"when patterns are not provided, the prover uses a heuristic to infer them. This option sets the threshold on the number of extra multi-patterns that can be created. By default, the prover creates at most one multi-pattern when there is no unary pattern");
p.register_bool_param("PI_BLOCK_LOOOP_PATTERNS", m_pi_block_loop_patterns,
"block looping patterns during pattern inference");
p.register_int_param("PI_ARITH", 0, 2, reinterpret_cast<int&>(m_pi_arith),
"0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms.");
p.register_bool_param("PI_USE_DATABASE", m_pi_use_database);
p.register_unsigned_param("PI_ARITH_WEIGHT", m_pi_arith_weight, "default weight for quantifiers where the only available pattern has nested arithmetic terms.");
p.register_unsigned_param("PI_NON_NESTED_ARITH_WEIGHT", m_pi_non_nested_arith_weight, "default weight for quantifiers where the only available pattern has non nested arithmetic terms.");
p.register_bool_param("PI_PULL_QUANTIFIERS", m_pi_pull_quantifiers, "pull nested quantifiers, if no pattern was found.");
p.register_int_param("PI_NOPAT_WEIGHT", m_pi_nopat_weight, "set weight of quantifiers without patterns, if negative the weight is not changed.");
p.register_bool_param("PI_AVOID_SKOLEMS", m_pi_avoid_skolems);
p.register_bool_param("PI_WARNINGS", m_pi_warnings, "enable/disable warning messages in the pattern inference module.");
}

241
lib/polynomial_cmds.cpp
View file

@ -1,241 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
polynomial_cmds.cpp
Abstract:
Commands for debugging polynomial module.
Author:
Leonardo (leonardo) 2011-12-23
Notes:
--*/
#include<sstream>
#include"cmd_context.h"
#include"cmd_util.h"
#include"scoped_timer.h"
#include"scoped_ctrl_c.h"
#include"cancel_eh.h"
#include"ast_smt2_pp.h"
#include"expr2polynomial.h"
#include"parametric_cmd.h"
#include"mpq.h"
#include"algebraic_numbers.h"
#include"pp.h"
#include"pp_params.h"
#include"polynomial_var2value.h"
#include"expr2var.h"
static void to_poly(cmd_context & ctx, expr * t) {
polynomial::numeral_manager nm;
polynomial::manager pm(nm);
default_expr2polynomial expr2poly(ctx.m(), pm);
polynomial::polynomial_ref p(pm);
polynomial::scoped_numeral d(nm);
if (!expr2poly.to_polynomial(t, p, d)) {
throw cmd_exception("expression is not a polynomial");
}
expr_ref r(ctx.m());
expr2poly.to_expr(p, true, r);
if (!nm.is_one(d))
ctx.regular_stream() << "(* " << nm.to_string(d) << " ";
ctx.display(ctx.regular_stream(), r);
if (!nm.is_one(d))
ctx.regular_stream() << ")";
ctx.regular_stream() << std::endl;
}
static void factor(cmd_context & ctx, expr * t, polynomial::factor_params const & ps) {
polynomial::numeral_manager nm;
polynomial::manager pm(nm);
default_expr2polynomial expr2poly(ctx.m(), pm);
polynomial::polynomial_ref p(pm);
polynomial::scoped_numeral d(nm);
if (!expr2poly.to_polynomial(t, p, d)) {
throw cmd_exception("expression is not a polynomial");
}
polynomial::factors fs(pm);
factor(p, fs, ps);
ctx.regular_stream() << "(factors";
rational f0(fs.get_constant());
f0 = f0 / rational(d);
ctx.regular_stream() << std::endl << f0;
unsigned num_factors = fs.distinct_factors();
expr_ref f(ctx.m());
for (unsigned i = 0; i < num_factors; i++) {
ctx.regular_stream() << std::endl;
if (fs.get_degree(i) > 1)
ctx.regular_stream() << "(^ ";
expr2poly.to_expr(fs[i], true, f);
ctx.display(ctx.regular_stream(), f);
if (fs.get_degree(i) > 1)
ctx.regular_stream() << " " << fs.get_degree(i) << ")";
}
ctx.regular_stream() << ")" << std::endl;
}
class poly_isolate_roots_cmd : public cmd {
struct context {
arith_util m_util;
unsynch_mpq_manager m_qm;
polynomial::manager m_pm;
algebraic_numbers::manager m_am;
polynomial_ref m_p;
default_expr2polynomial m_expr2poly;
polynomial::var m_var;
typedef polynomial::simple_var2value<algebraic_numbers::manager> x2v;
x2v m_x2v;
context(ast_manager & m):
m_util(m),
m_pm(m_qm),
m_am(m_qm),
m_p(m_pm),
m_expr2poly(m, m_pm),
m_var(polynomial::null_var),
m_x2v(m_am) {
}
void set_next_arg(cmd_context & ctx, expr * arg) {
if (m_p.get() == 0) {
scoped_mpz d(m_qm);
if (!m_expr2poly.to_polynomial(arg, m_p, d))
throw cmd_exception("expression is not a polynomial");
}
else if (m_var == polynomial::null_var) {
if (!m_expr2poly.is_var(arg))
throw cmd_exception("invalid assignment, argument is not a variable in the given polynomial");
m_var = m_expr2poly.get_mapping().to_var(arg);
}
else {
rational k;
scoped_anum v(m_am);
if (m_util.is_numeral(arg, k)) {
m_am.set(v, k.to_mpq());
}
else if (m_util.is_irrational_algebraic_numeral(arg)) {
m_am.set(v, m_util.to_irrational_algebraic_numeral(arg));
}
else {
throw cmd_exception("invalid assignment, argument is not a value");
}
m_x2v.push_back(m_var, v);
m_var = polynomial::null_var;
}
}
void execute(cmd_context & ctx) {
if (m_p.get() == 0)
throw cmd_exception("polynomial expected");
polynomial::var_vector xs;
m_pm.vars(m_p, xs);
unsigned num_assigned = 0;
for (unsigned i = 0; i < xs.size(); i++) {
if (m_x2v.contains(xs[i]))
num_assigned++;
}
if (num_assigned != xs.size() && num_assigned + 1 != xs.size())
throw cmd_exception("given assignment is not sufficient to make the given polynomial univariate");
scoped_anum_vector rs(m_am);
m_am.isolate_roots(m_p, m_x2v, rs);
ctx.regular_stream() << "(roots";
for (unsigned i = 0; i < rs.size(); i++) {
ctx.regular_stream() << std::endl;
if (!get_pp_default_params().m_pp_decimal)
m_am.display_root_smt2(ctx.regular_stream(), rs[i]);
else
m_am.display_decimal(ctx.regular_stream(), rs[i]);
}
ctx.regular_stream() << ")" << std::endl;
}
};
scoped_ptr<context> m_ctx;
public:
poly_isolate_roots_cmd(char const * name = "poly/isolate-roots"):cmd(name), m_ctx(0) {}
virtual char const * get_usage() const { return "<term> (<term> <value>)*"; }
virtual char const * get_descr(cmd_context & ctx) const { return "isolate the roots a multivariate polynomial modulo an assignment"; }
virtual unsigned get_arity() const { return VAR_ARITY; }
virtual void prepare(cmd_context & ctx) {
m_ctx = alloc(context, ctx.m());
}
virtual void finalize(cmd_context & ctx) {
m_ctx = 0;
}
virtual void failure_cleanup(cmd_context & ctx) {
m_ctx = 0;
}
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
return CPK_EXPR;
}
virtual void set_next_arg(cmd_context & ctx, expr * arg) {
m_ctx->set_next_arg(ctx, arg);
}
virtual void execute(cmd_context & ctx) {
m_ctx->execute(ctx);
m_ctx = 0;
}
};
UNARY_CMD(to_poly_cmd, "to-poly", "<term>", "convert expression into sum-of-monomials form", CPK_EXPR, expr *, to_poly(ctx, arg););
class poly_factor_cmd : public parametric_cmd {
expr * m_target;
public:
poly_factor_cmd(char const * name = "poly/factor"):parametric_cmd(name) {}
virtual char const * get_usage() const { return "<term> (<keyword> <value>)*"; }
virtual char const * get_main_descr() const {
return "factor a polynomial";
}
virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
polynomial::factor_params::get_param_descrs(p);
}
virtual void prepare(cmd_context & ctx) {
parametric_cmd::prepare(ctx);
m_target = 0;
}
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
if (m_target == 0) return CPK_EXPR;
return parametric_cmd::next_arg_kind(ctx);
}
virtual void set_next_arg(cmd_context & ctx, expr * arg) {
m_target = arg;
}
virtual void execute(cmd_context & ctx) {
polynomial::factor_params ps;
ps.updt_params(m_params);
factor(ctx, m_target, ps);
}
};
void install_polynomial_cmds(cmd_context & ctx) {
#ifndef _EXTERNAL_RELEASE
ctx.insert(alloc(to_poly_cmd));
ctx.insert(alloc(poly_factor_cmd));
ctx.insert(alloc(poly_isolate_roots_cmd));
#endif
}

24
lib/polynomial_cmds.h
View file

@ -1,24 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
polynomial_cmds.h
Abstract:
Commands for debugging polynomial module.
Author:
Leonardo (leonardo) 2011-12-23
Notes:
--*/
#ifndef _POLYNOMIAL_CMDS_H_
#define _POLYNOMIAL_CMDS_H_
class cmd_context;
void install_polynomial_cmds(cmd_context & ctx);
#endif

521
lib/reduce_args.cpp
View file

@ -1,521 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
reduce_args.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2010-04-06.
Revision History:
--*/
#include"reduce_args.h"
#include"cooperate.h"
#include"ast_smt2_pp.h"
#include"map.h"
#include"rewriter_def.h"
#include"elim_var_model_converter.h"
#include"filter_model_converter.h"
struct reduce_args::imp {
ast_manager & m_manager;
bool m_produce_models;
volatile bool m_cancel;
ast_manager & m() const { return m_manager; }
imp(ast_manager & m, params_ref const & p):
m_manager(m) {
updt_params(p);
m_cancel = false;
}
void updt_params(params_ref const & p) {
m_produce_models = p.get_bool(":produce-models", false);
}
void set_cancel(bool f) {
m_cancel = f;
}
void checkpoint() {
if (m_cancel)
throw reduce_args_exception(STE_CANCELED_MSG);
cooperate("reduce-args");
}
struct find_non_candidates_proc {
ast_manager & m_manager;
obj_hashtable<func_decl> & m_non_cadidates;
find_non_candidates_proc(ast_manager & m, obj_hashtable<func_decl> & non_cadidates):
m_manager(m),
m_non_cadidates(non_cadidates) {
}
void operator()(var * n) {}
void operator()(quantifier * n) {}
void operator()(app * n) {
if (n->get_num_args() == 0)
return; // ignore constants
func_decl * d = n->get_decl();
if (d->get_family_id() != null_family_id)
return; // ignore interpreted symbols
if (m_non_cadidates.contains(d))
return; // it is already in the set.
unsigned j = n->get_num_args();
while (j > 0) {
--j;
if (m_manager.is_value(n->get_arg(j)))
return;
}
m_non_cadidates.insert(d);
}
};
/**
\brief Populate the table non_cadidates with function declarations \c f
such that there is a function application (f t1 ... tn) where t1 ... tn are not values.
*/
void find_non_candidates(assertion_set const & s, obj_hashtable<func_decl> & non_candidates) {
non_candidates.reset();
find_non_candidates_proc proc(m_manager, non_candidates);
expr_fast_mark1 visited;
unsigned sz = s.size();
for (unsigned i = 0; i < sz; i++) {
checkpoint();
quick_for_each_expr(proc, visited, s.form(i));
}
TRACE("reduce_args", tout << "non_candidates:\n";
obj_hashtable<func_decl>::iterator it = non_candidates.begin();
obj_hashtable<func_decl>::iterator end = non_candidates.end();
for (; it != end; ++it) {
func_decl * d = *it;
tout << d->get_name() << "\n";
});
}
struct populate_decl2args_proc {
ast_manager & m_manager;
obj_hashtable<func_decl> & m_non_cadidates;
obj_map<func_decl, bit_vector> & m_decl2args;
populate_decl2args_proc(ast_manager & m, obj_hashtable<func_decl> & nc, obj_map<func_decl, bit_vector> & d):
m_manager(m), m_non_cadidates(nc), m_decl2args(d) {}
void operator()(var * n) {}
void operator()(quantifier * n) {}
void operator()(app * n) {
if (n->get_num_args() == 0)
return; // ignore constants
func_decl * d = n->get_decl();
if (d->get_family_id() != null_family_id)
return; // ignore interpreted symbols
if (m_non_cadidates.contains(d))
return; // declaration is not a candidate
unsigned j = n->get_num_args();
obj_map<func_decl, bit_vector>::iterator it = m_decl2args.find_iterator(d);
if (it == m_decl2args.end()) {
m_decl2args.insert(d, bit_vector());
it = m_decl2args.find_iterator(d);
SASSERT(it != m_decl2args.end());
it->m_value.reserve(j);
while (j > 0) {
--j;
it->m_value.set(j, m_manager.is_value(n->get_arg(j)));
}
} else {
SASSERT(j == it->m_value.size());
while (j > 0) {
--j;
it->m_value.set(j, it->m_value.get(j) && m_manager.is_value(n->get_arg(j)));
}
}
}
};
void populate_decl2args(assertion_set const & s,
obj_hashtable<func_decl> & non_candidates,
obj_map<func_decl, bit_vector> & decl2args) {
expr_fast_mark1 visited;
decl2args.reset();
populate_decl2args_proc proc(m_manager, non_candidates, decl2args);
unsigned sz = s.size();
for (unsigned i = 0; i < sz; i++) {
checkpoint();
quick_for_each_expr(proc, visited, s.form(i));
}
// Remove all cases where the simplification is not applicable.
ptr_buffer<func_decl> bad_decls;
obj_map<func_decl, bit_vector>::iterator it = decl2args.begin();
obj_map<func_decl, bit_vector>::iterator end = decl2args.end();
for (; it != end; it++) {
bool is_zero = true;
for (unsigned i = 0; i < it->m_value.size() && is_zero ; i++) {
if (it->m_value.get(i))
is_zero = false;
}
if (is_zero)
bad_decls.push_back(it->m_key);
}
ptr_buffer<func_decl>::iterator it2 = bad_decls.begin();
ptr_buffer<func_decl>::iterator end2 = bad_decls.end();
for (; it2 != end2; ++it2)
decl2args.erase(*it2);
TRACE("reduce_args", tout << "decl2args:" << std::endl;
for (obj_map<func_decl, bit_vector>::iterator it = decl2args.begin() ; it != decl2args.end() ; it++) {
tout << it->m_key->get_name() << ": ";
for (unsigned i = 0 ; i < it->m_value.size() ; i++)
tout << (it->m_value.get(i) ? "1" : "0");
tout << std::endl;
});
}
struct arg2func_hash_proc {
bit_vector const & m_bv;
arg2func_hash_proc(bit_vector const & bv):m_bv(bv) {}
unsigned operator()(app const * n) const {
// compute the hash-code using only the arguments where m_bv is true.
unsigned a = 0x9e3779b9;
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
if (!m_bv.get(i))
continue; // ignore argument
a = hash_u_u(a, n->get_arg(i)->get_id());
}
return a;
}
};
struct arg2func_eq_proc {
bit_vector const & m_bv;
arg2func_eq_proc(bit_vector const & bv):m_bv(bv) {}
bool operator()(app const * n1, app const * n2) const {
// compare only the arguments where m_bv is true
SASSERT(n1->get_num_args() == n2->get_num_args());
unsigned num_args = n1->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
if (!m_bv.get(i))
continue; // ignore argument
if (n1->get_arg(i) != n2->get_arg(i))
return false;
}
return true;
}
};
typedef map<app *, func_decl *, arg2func_hash_proc, arg2func_eq_proc> arg2func;
typedef obj_map<func_decl, arg2func *> decl2arg2func_map;
struct reduce_args_ctx {
ast_manager & m_manager;
decl2arg2func_map m_decl2arg2funcs;
reduce_args_ctx(ast_manager & m): m_manager(m) {
}
~reduce_args_ctx() {
obj_map<func_decl, arg2func *>::iterator it = m_decl2arg2funcs.begin();
obj_map<func_decl, arg2func *>::iterator end = m_decl2arg2funcs.end();
for (; it != end; ++it) {
arg2func * map = it->m_value;
arg2func::iterator it2 = map->begin();
arg2func::iterator end2 = map->end();
for (; it2 != end2; ++it2) {
m_manager.dec_ref(it2->m_key);
m_manager.dec_ref(it2->m_value);
}
dealloc(map);
}
}
};
struct populate_decl2arg_set_proc {
ast_manager & m_manager;
obj_map<func_decl, bit_vector> & m_decl2args;
decl2arg2func_map & m_decl2arg2funcs;
populate_decl2arg_set_proc(ast_manager & m,
obj_map<func_decl, bit_vector> & d,
decl2arg2func_map & ds):
m_manager(m), m_decl2args(d), m_decl2arg2funcs(ds) {}
void operator()(var * n) {}
void operator()(quantifier * n) {}
void operator()(app * n) {
if (n->get_num_args() == 0)
return; // ignore constants
func_decl * d = n->get_decl();
if (d->get_family_id() != null_family_id)
return; // ignore interpreted symbols
obj_map<func_decl, bit_vector>::iterator it = m_decl2args.find_iterator(d);
if (it == m_decl2args.end())
return; // not reducing the arguments of this declaration
bit_vector & bv = it->m_value;
arg2func * map = 0;
decl2arg2func_map::iterator it2 = m_decl2arg2funcs.find_iterator(d);
if (it2 == m_decl2arg2funcs.end()) {
map = alloc(arg2func, arg2func_hash_proc(bv), arg2func_eq_proc(bv));
m_decl2arg2funcs.insert(d, map);
}
else {
map = it2->m_value;
}
if (!map->contains(n)) {
// create fresh symbol...
ptr_buffer<sort> domain;
unsigned arity = d->get_arity();
for (unsigned i = 0; i < arity; i++) {
if (!bv.get(i))
domain.push_back(d->get_domain(i));
}
func_decl * new_d = m_manager.mk_fresh_func_decl(d->get_name(), symbol::null, domain.size(), domain.c_ptr(), d->get_range());
map->insert(n, new_d);
m_manager.inc_ref(n);
m_manager.inc_ref(new_d);
}
}
};
void populate_decl2arg_set(assertion_set const & s,
obj_map<func_decl, bit_vector> & decl2args,
decl2arg2func_map & decl2arg2funcs) {
expr_fast_mark1 visited;
populate_decl2arg_set_proc proc(m_manager, decl2args, decl2arg2funcs);
unsigned sz = s.size();
for (unsigned i = 0; i < sz; i++) {
checkpoint();
quick_for_each_expr(proc, visited, s.form(i));
}
}
struct reduce_args_rw_cfg : public default_rewriter_cfg {
ast_manager & m;
imp & m_owner;
obj_map<func_decl, bit_vector> & m_decl2args;
decl2arg2func_map & m_decl2arg2funcs;
reduce_args_rw_cfg(imp & owner, obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs):
m(owner.m_manager),
m_owner(owner),
m_decl2args(decl2args),
m_decl2arg2funcs(decl2arg2funcs) {
}
bool max_steps_exceeded(unsigned num_steps) const {
m_owner.checkpoint();
return false;
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0;
if (f->get_arity() == 0)
return BR_FAILED; // ignore constants
if (f->get_family_id() != null_family_id)
return BR_FAILED; // ignore interpreted symbols
decl2arg2func_map::iterator it = m_decl2arg2funcs.find_iterator(f);
if (it == m_decl2arg2funcs.end())
return BR_FAILED;
SASSERT(m_decl2args.contains(f));
bit_vector & bv = m_decl2args.find(f);
arg2func * map = it->m_value;
app_ref tmp(m);
tmp = m.mk_app(f, num, args);
CTRACE("reduce_args", !map->contains(tmp),
tout << "map does not contain tmp f: " << f->get_name() << "\n";
tout << mk_ismt2_pp(tmp, m) << "\n";
arg2func::iterator it = map->begin();
arg2func::iterator end = map->end();
for (; it != end; ++it) {
tout << mk_ismt2_pp(it->m_key, m) << "\n---> " << it->m_value->get_name() << "\n";
});
SASSERT(map->contains(tmp));
func_decl * new_f = map->find(tmp);
ptr_buffer<expr> new_args;
for (unsigned i = 0; i < num; i++) {
if (!bv.get(i))
new_args.push_back(args[i]);
}
result = m.mk_app(new_f, new_args.size(), new_args.c_ptr());
return BR_DONE;
}
};
struct reduce_args_rw : rewriter_tpl<reduce_args_rw_cfg> {
reduce_args_rw_cfg m_cfg;
public:
reduce_args_rw(imp & owner, obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs):
rewriter_tpl<reduce_args_rw_cfg>(owner.m_manager, false, m_cfg),
m_cfg(owner, decl2args, decl2arg2funcs) {
}
};
model_converter * mk_mc(obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs) {
ptr_buffer<expr> new_args;
var_ref_vector new_vars(m_manager);
ptr_buffer<expr> new_eqs;
elim_var_model_converter * e_mc = alloc(elim_var_model_converter, m_manager);
filter_model_converter * f_mc = alloc(filter_model_converter, m_manager);
decl2arg2func_map::iterator it = decl2arg2funcs.begin();
decl2arg2func_map::iterator end = decl2arg2funcs.end();
for (; it != end; ++it) {
func_decl * f = it->m_key;
arg2func * map = it->m_value;
expr * def = 0;
SASSERT(decl2args.contains(f));
bit_vector & bv = decl2args.find(f);
new_vars.reset();
new_args.reset();
for (unsigned i = 0; i < f->get_arity(); i++) {
new_vars.push_back(m_manager.mk_var(i, f->get_domain(i)));
if (!bv.get(i))
new_args.push_back(new_vars.back());
}
arg2func::iterator it2 = map->begin();
arg2func::iterator end2 = map->end();
for (; it2 != end2; ++it2) {
app * t = it2->m_key;
func_decl * new_def = it2->m_value;
f_mc->insert(new_def);
SASSERT(new_def->get_arity() == new_args.size());
app * new_t = m_manager.mk_app(new_def, new_args.size(), new_args.c_ptr());
if (def == 0) {
def = new_t;
}
else {
new_eqs.reset();
for (unsigned i = 0; i < f->get_arity(); i++) {
if (bv.get(i))
new_eqs.push_back(m_manager.mk_eq(new_vars.get(i), t->get_arg(i)));
}
SASSERT(new_eqs.size() > 0);
expr * cond;
if (new_eqs.size() == 1)
cond = new_eqs[0];
else
cond = m_manager.mk_and(new_eqs.size(), new_eqs.c_ptr());
def = m_manager.mk_ite(cond, new_t, def);
}
}
SASSERT(def);
e_mc->insert(f, def);
}
return concat(f_mc, e_mc);
}
void operator()(assertion_set & s, model_converter_ref & mc) {
mc = 0;
if (s.inconsistent())
return;
if (m().proofs_enabled())
throw reduce_args_exception("reduce-args does not support proofs");
as_st_report report("reduce-args", s);
TRACE("reduce_args", s.display(tout););
obj_hashtable<func_decl> non_candidates;
obj_map<func_decl, bit_vector> decl2args;
find_non_candidates(s, non_candidates);
populate_decl2args(s, non_candidates, decl2args);
if (decl2args.empty())
return;
ptr_vector<arg2func> arg2funcs;
reduce_args_ctx ctx(m_manager);
populate_decl2arg_set(s, decl2args, ctx.m_decl2arg2funcs);
reduce_args_rw rw(*this, decl2args, ctx.m_decl2arg2funcs);
unsigned sz = s.size();
for (unsigned i = 0; i < sz; i++) {
if (s.inconsistent())
break;
expr * f = s.form(i);
expr_ref new_f(m_manager);
rw(f, new_f);
s.update(i, new_f);
}
report_st_progress(":reduced-funcs", decl2args.size());
if (m_produce_models)
mc = mk_mc(decl2args, ctx.m_decl2arg2funcs);
TRACE("reduce_args", s.display(tout); if (mc) mc->display(tout););
}
};
reduce_args::reduce_args(ast_manager & m, params_ref const & p):
m_params(p) {
m_imp = alloc(imp, m, p);
}
reduce_args::~reduce_args() {
dealloc(m_imp);
}
ast_manager & reduce_args::m() const {
return m_imp->m();
}
void reduce_args::updt_params(params_ref const & p) {
m_params = p;
m_imp->updt_params(p);
}
void reduce_args::get_param_descrs(param_descrs & r) {
insert_produce_models(r);
}
void reduce_args::operator()(assertion_set & s, model_converter_ref & mc) {
m_imp->operator()(s, mc);
}
void reduce_args::set_cancel(bool f) {
if (m_imp)
m_imp->set_cancel(f);
}
void reduce_args::cleanup() {
ast_manager & m = m_imp->m();
imp * d = m_imp;
#pragma omp critical (as_st_cancel)
{
m_imp = 0;
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (as_st_cancel)
{
m_imp = d;
}
}
void reduce_args::collect_statistics(statistics & st) const {
}
void reduce_args::reset_statistics() {
}
as_st * mk_reduce_args(ast_manager & m, params_ref const & p) {
return clean(alloc(reduce_args, m, p));
}

92
lib/reduce_args.h
View file

@ -1,92 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
reduce_args.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2010-04-05.
Revision History:
Make it a strategy 2011-07-26.
--*/
#ifndef _REDUCE_ARGS_H_
#define _REDUCE_ARGS_H_
#include"assertion_set_strategy.h"
MK_ST_EXCEPTION(reduce_args_exception);
/**
\brief Reduce the number of arguments in function applications.
Example, suppose we have a function f with 2 arguments.
There are 1000 applications of this function, but the first argument is always "a", "b" or "c".
Thus, we replace the f(t1, t2)
with
f_a(t2) if t1 = a
f_b(t2) if t2 = b
f_c(t2) if t2 = c
Since f_a, f_b, f_c are new symbols, satisfiability is preserved.
This transformation is very similar in spirit to the Ackermman's reduction.
This transformation should work in the following way:
1- Create a mapping decl2arg_map from declarations to tuples of booleans, an entry [f -> (true, false, true)]
means that f is a declaration with 3 arguments where the first and third arguments are always values.
2- Traverse the formula and populate the mapping.
For each function application f(t1, ..., tn) do
a) Create a boolean tuple (is_value(t1), ..., is_value(tn)) and do
the logical-and with the tuple that is already in the mapping. If there is no such tuple
in the mapping, we just add a new entry.
If all entries are false-tuples, then there is nothing to be done. The transformation is not applicable.
Now, we create a mapping decl2new_decl from (decl, val_1, ..., val_n) to decls. Note that, n may be different for each entry,
but it is the same for the same declaration.
For example, suppose we have [f -> (true, false, true)] in decl2arg_map, and applications f(1, a, 2), f(1, b, 2), f(1, b, 3), f(2, b, 3), f(2, c, 3) in the formula.
Then, decl2arg_map would contain
(f, 1, 2) -> f_1_2
(f, 1, 3) -> f_1_3
(f, 2, 3) -> f_2_3
where f_1_2, f_1_3 and f_2_3 are new function symbols.
Using the new map, we can replace the occurrences of f.
*/
class reduce_args : public assertion_set_strategy {
struct imp;
imp * m_imp;
params_ref m_params;
public:
reduce_args(ast_manager & m, params_ref const & p = params_ref());
virtual ~reduce_args();
ast_manager & m () const;
virtual void updt_params(params_ref const & p);
static void get_param_descrs(param_descrs & r);
virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
virtual void operator()(assertion_set & s, model_converter_ref & mc);
virtual void cleanup();
virtual void collect_statistics(statistics & st) const;
virtual void reset_statistics();
protected:
virtual void set_cancel(bool f);
};
as_st * mk_reduce_args(ast_manager & m, params_ref const & p = params_ref());
#endif /* _REDUCE_ARGS_H_ */

257
lib/shallow_context_simplifier.cpp
View file

@ -1,257 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
shallow_context_simplifier.h
Abstract:
Depth 1 context simplifier.
Author:
Leonardo de Moura (leonardo) 2011-04-28
Revision History:
--*/
#include"shallow_context_simplifier.h"
#include"assertion_set_util.h"
#include"expr_substitution.h"
#include"th_rewriter.h"
#include"ast_smt2_pp.h"
#include"assertion_set_util.h"
struct shallow_context_simplifier::imp {
ast_manager & m_manager;
th_rewriter m_r;
expr_substitution m_subst;
assertion_set * m_set;
as_shared_occs m_occs;
unsigned m_idx;
unsigned m_num_steps;
unsigned m_max_rounds;
bool m_modified;
imp(ast_manager & m, params_ref const & p):
m_manager(m),
m_r(m, p),
m_subst(m),
m_set(0),
m_occs(m, true /* track atoms */) {
m_r.set_substitution(&m_subst);
updt_params_core(p);
}
void updt_params_core(params_ref const & p) {
m_max_rounds = p.get_uint(":max-rounds", 4);
}
void updt_params(params_ref const & p) {
m_r.updt_params(p);
updt_params_core(p);
}
ast_manager & m() const { return m_manager; }
void set_cancel(bool f) {
m_r.set_cancel(f);
}
void reset() {
m_subst.reset();
m_set = 0;
m_num_steps = 0;
}
void push_result(expr * new_curr, proof * new_pr) {
if (m().proofs_enabled()) {
proof * pr = m_set->pr(m_idx);
new_pr = m().mk_modus_ponens(pr, new_pr);
}
m_set->update(m_idx, new_curr, new_pr);
if (is_shared(new_curr)) {
m_subst.insert(new_curr, m().mk_true(), m().mk_iff_true(new_pr));
}
expr * atom;
if (is_shared_neg(new_curr, atom)) {
m_subst.insert(atom, m().mk_false(), m().mk_iff_false(new_pr));
}
expr * lhs, * value;
if (is_shared_eq(new_curr, lhs, value)) {
TRACE("shallow_context_simplifier_bug", tout << "found eq:\n" << mk_ismt2_pp(new_curr, m()) << "\n";);
m_subst.insert(lhs, value, new_pr);
}
}
void process_current() {
expr * curr = m_set->form(m_idx);
expr_ref new_curr(m());
proof_ref new_pr(m());
if (!m_subst.empty()) {
m_r(curr, new_curr, new_pr);
m_num_steps += m_r.get_num_steps();
}
else {
new_curr = curr;
if (m().proofs_enabled())
new_pr = m().mk_reflexivity(curr);
}
TRACE("shallow_context_simplifier_bug", tout << mk_ismt2_pp(curr, m()) << "\n---->\n" << mk_ismt2_pp(new_curr, m()) << "\n";);
push_result(new_curr, new_pr);
if (new_curr != curr)
m_modified = true;
}
void operator()(assertion_set & s) {
SASSERT(is_well_sorted(s));
as_st_report report("shallow-context-simplifier", s);
m_num_steps = 0;
if (s.inconsistent())
return;
SASSERT(m_set == 0);
bool forward = true;
m_set = &s;
m_occs(*m_set);
TRACE("shallow_context_simplifier_bug", m_occs.display(tout, m()); );
unsigned size = s.size();
m_idx = 0;
m_modified = false;
expr_ref new_curr(m());
proof_ref new_pr(m());
unsigned round = 0;
while (true) {
TRACE("shallow_context_simplifier_round", s.display(tout););
if (forward) {
for (; m_idx < size; m_idx++) {
process_current();
if (m_set->inconsistent())
goto end;
}
if (m_subst.empty() && !m_modified)
goto end;
m_occs(*m_set);
m_idx = m_set->size();
forward = false;
m_subst.reset();
m_r.set_substitution(&m_subst); // reset, but keep substitution
}
else {
while (m_idx > 0) {
m_idx--;
process_current();
if (m_set->inconsistent())
goto end;
}
if (!m_modified)
goto end;
m_subst.reset();
m_r.set_substitution(&m_subst); // reset, but keep substitution
m_modified = false;
m_occs(*m_set);
m_idx = 0;
size = m_set->size();
forward = true;
}
round++;
if (round >= m_max_rounds)
break;
IF_VERBOSE(100, verbose_stream() << "starting new round, assertion-set size: " << m_set->num_exprs() << std::endl;);
TRACE("shallow_context_simplifier", tout << "round finished\n"; m_set->display(tout); tout << "\n";);
}
end:
m_set = 0;
SASSERT(is_well_sorted(s));
}
bool is_shared(expr * t) {
return m_occs.is_shared(t);
}
bool is_shared_neg(expr * t, expr * & atom) {
if (!m().is_not(t))
return false;
atom = to_app(t)->get_arg(0);
return is_shared(atom);
}
bool is_shared_eq(expr * t, expr * & lhs, expr * & value) {
if (!m().is_eq(t))
return false;
expr * arg1 = to_app(t)->get_arg(0);
expr * arg2 = to_app(t)->get_arg(1);
if (m().is_value(arg1) && is_shared(arg2)) {
lhs = arg2;
value = arg1;
return true;
}
if (m().is_value(arg2) && is_shared(arg1)) {
lhs = arg1;
value = arg2;
return true;
}
return false;
}
unsigned get_num_steps() const { return m_num_steps; }
};
shallow_context_simplifier::shallow_context_simplifier(ast_manager & m, params_ref const & p):
m_params(p) {
m_imp = alloc(imp, m, p);
}
shallow_context_simplifier::~shallow_context_simplifier() {
dealloc(m_imp);
}
void shallow_context_simplifier::updt_params(params_ref const & p) {
m_params = p;
m_imp->updt_params(p);
}
void shallow_context_simplifier::get_param_descrs(param_descrs & r) {
th_rewriter::get_param_descrs(r);
r.insert(":max-rounds", CPK_UINT, "(default: 2) maximum number of rounds.");
}
void shallow_context_simplifier::operator()(assertion_set & s) {
m_imp->operator()(s);
}
void shallow_context_simplifier::set_cancel(bool f) {
if (m_imp)
m_imp->set_cancel(f);
}
void shallow_context_simplifier::cleanup() {
ast_manager & m = m_imp->m();
imp * d = m_imp;
#pragma omp critical (as_st_cancel)
{
m_imp = 0;
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (as_st_cancel)
{
m_imp = d;
}
}
unsigned shallow_context_simplifier::get_num_steps() const {
return m_imp->get_num_steps();
}

59
lib/shallow_context_simplifier.h
View file

@ -1,59 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
shallow_context_simplifier.h
Abstract:
Depth 1 context simplifier.
Author:
Leonardo de Moura (leonardo) 2011-04-28
Revision History:
--*/
#ifndef _SHALLOW_CONTEXT_SIMPLIFIER_H_
#define _SHALLOW_CONTEXT_SIMPLIFIER_H_
#include"assertion_set_strategy.h"
class shallow_context_simplifier : public assertion_set_strategy {
struct imp;
imp * m_imp;
params_ref m_params;
public:
shallow_context_simplifier(ast_manager & m, params_ref const & p = params_ref());
virtual ~shallow_context_simplifier();
virtual void updt_params(params_ref const & p);
static void get_param_descrs(param_descrs & r);
virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
void operator()(assertion_set & s);
virtual void operator()(assertion_set & s, model_converter_ref & mc) {
operator()(s);
mc = 0;
}
virtual void cleanup();
unsigned get_num_steps() const;
protected:
virtual void set_cancel(bool f);
};
inline as_st * mk_shallow_simplifier(ast_manager & m, params_ref const & p = params_ref()) {
return clean(alloc(shallow_context_simplifier, m, p));
}
inline as_st * mk_constant_propagation(ast_manager & m, params_ref const & p = params_ref()) {
return mk_shallow_simplifier(m, p);
}
#endif

46
lib/smt_classifier.h
View file

@ -1,46 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
smt_classifier.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-06-24.
Revision History:
--*/
#ifndef _SMT_CLASSIFIER_H_
#define _SMT_CLASSIFIER_H_
#include"static_features.h"
namespace smt {
class classifier {
context & m_context;
ast_manager & m_manager;
static_features m_static_features;
symbol m_logic;
public:
classifier(context & c);
/**
\brief Give a hint by specifying the logic used to describe a problem.
*/
void set_logic(symbol & s);
/**
\brief Setup the logical context for solving the following formulas.
*/
void setup(unsigned num_formulas, expr * const * fs);
};
};
#endif /* _SMT_CLASSIFIER_H_ */

218
lib/smt_formula_compiler.cpp
View file

@ -1,218 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
smt_formula_compiler.cpp
Abstract:
Auxiliary class for smt::solver
Convert Exprs into Internal data-structures.
Author:
Leonardo de Moura (leonardo) 2011-06-25.
Revision History:
This was an experiment to rewrite Z3 kernel.
It will be deleted after we finish revamping Z3 kernel.
--*/
#include"smt_formula_compiler.h"
#include"smt_solver_exp.h"
#include"assertion_set_util.h"
#include"assertion_set2sat.h"
#include"for_each_expr.h"
namespace smt {
formula_compiler::formula_compiler(solver_exp & _s, params_ref const & p):
s(_s),
m_a_util(s.m),
m_normalizer(s.m),
m_elim_ite(s.m) {
updt_params(p);
params_ref s_p;
s_p.set_bool(":elim-and", true);
s_p.set_bool(":blast-distinct", true);
s_p.set_bool(":eq2ineq", true);
s_p.set_bool(":arith-lhs", true);
s_p.set_bool(":gcd-rounding", true);
s_p.set_bool(":sort-sums", true);
s_p.set_bool(":som", true);
m_normalizer.updt_params(s_p);
}
formula_compiler::~formula_compiler() {
}
// mark theory axioms: literals that do not occur in the boolean structure
void formula_compiler::mark_axioms(assertion_set const & s, expr_fast_mark2 & axioms) {
ast_manager & m = s.m();
unsigned sz = s.size();
for (unsigned i = 0; i < sz; i++) {
expr * f = s.form(i);
while (m.is_not(f, f));
if (!is_app(f) || to_app(f)->get_family_id() != m.get_basic_family_id()) {
axioms.mark(f);
continue;
}
SASSERT(is_app(f));
SASSERT(to_app(f)->get_family_id() == m.get_basic_family_id());
switch (to_app(f)->get_decl_kind()) {
case OP_OR:
case OP_IFF:
break;
case OP_ITE:
SASSERT(m.is_bool(to_app(f)->get_arg(1)));
break;
case OP_EQ:
if (!m.is_bool(to_app(f)->get_arg(1)))
axioms.mark(f);
break;
case OP_AND:
case OP_XOR:
case OP_IMPLIES:
case OP_DISTINCT:
UNREACHABLE();
break;
default:
break;
}
}
}
struct unmark_axioms_proc {
expr_fast_mark2 & m_axioms;
unmark_axioms_proc(expr_fast_mark2 & axioms):m_axioms(axioms) {}
void operator()(quantifier *) {}
void operator()(var *) {}
void operator()(app * t) {
m_axioms.reset_mark(t);
}
};
/**
\brief Unmark atoms that occur in the boolean structure.
*/
void formula_compiler::unmark_nested_atoms(assertion_set const & s, expr_fast_mark2 & axioms) {
ast_manager & m = s.m();
expr_fast_mark1 visited;
unmark_axioms_proc proc(axioms);
unsigned sz = s.size();
for (unsigned i = 0; i < sz; i++) {
expr * f = s.form(i);
while (m.is_not(f, f));
if (axioms.is_marked(f))
continue;
quick_for_each_expr(proc, visited, f);
}
}
void formula_compiler::assert_axiom(expr * f, bool neg) {
if (is_app(f)) {
if (to_app(f)->get_family_id() == m_a_util.get_family_id())
s.m_arith.assert_axiom(f, neg);
}
}
void formula_compiler::register_atom(expr * f, sat::bool_var p) {
if (is_app(f)) {
if (to_app(f)->get_family_id() == m_a_util.get_family_id())
s.m_arith.mk_atom(f, p);
}
}
void formula_compiler::compile_formulas(assertion_set const & assertions) {
ast_manager & m = assertions.m();
expr_fast_mark2 axioms;
mark_axioms(assertions, axioms);
unmark_nested_atoms(assertions, axioms);
ptr_vector<expr> formulas;
// send axioms to theories, and save formulas to compile
unsigned sz = assertions.size();
for (unsigned i = 0; i < sz; i++) {
expr * f = assertions.form(i);
bool neg = false;
while (m.is_not(f, f))
neg = !neg;
if (axioms.is_marked(f)) {
assert_axiom(f, neg);
}
else {
formulas.push_back(f);
}
}
// compile formulas into sat::solver
m_to_sat(m, formulas.size(), formulas.c_ptr(), s.m_params, *(s.m_sat), s.m_atom2bvar);
// register atoms nested in the boolean structure in the theories
atom2bool_var::recent_iterator it = s.m_atom2bvar.begin_recent();
atom2bool_var::recent_iterator end = s.m_atom2bvar.end_recent();
for (; it != end; ++it) {
expr * atom = *it;
register_atom(atom, s.m_atom2bvar.to_bool_var(atom));
}
s.m_atom2bvar.reset_recent();
}
void formula_compiler::normalize() {
// make sure that the assertions are in the right format.
m_normalizer(s.m_assertions);
m_normalizer.cleanup();
}
void formula_compiler::elim_term_ite() {
if (has_term_ite(s.m_assertions)) {
model_converter_ref mc;
m_elim_ite(s.m_assertions, mc);
s.m_mc = concat(s.m_mc.get(), mc.get());
m_elim_ite.cleanup();
}
}
void formula_compiler::operator()() {
if (s.m_assertions.inconsistent())
return;
// normalization
elim_term_ite();
normalize();
TRACE("before_formula_compiler", s.m_assertions.display(tout););
s.init();
compile_formulas(s.m_assertions);
s.m_arith.preprocess();
TRACE("after_formula_compiler", s.display_state(tout););
}
void formula_compiler::updt_params(params_ref const & p) {
// TODO
}
void formula_compiler::collect_param_descrs(param_descrs & d) {
// TODO
}
void formula_compiler::collect_statistics(statistics & st) {
// TODO
}
void formula_compiler::reset_statistics() {
// TODO
}
void formula_compiler::set_cancel(bool f) {
m_normalizer.set_cancel(f);
m_elim_ite.set_cancel(f);
m_to_sat.set_cancel(f);
}
};

63
lib/smt_formula_compiler.h
View file

@ -1,63 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
smt_formula_compiler.h
Abstract:
Auxiliary class for smt::solver
Convert Exprs into Internal data-structures.
Author:
Leonardo de Moura (leonardo) 2011-06-25.
Revision History:
--*/
#ifndef _SMT_FORMULA_COMPILER_H_
#define _SMT_FORMULA_COMPILER_H_
#include"smt_solver_types.h"
#include"assertion_set_rewriter.h"
#include"elim_term_ite_strategy.h"
#include"arith_decl_plugin.h"
#include"assertion_set2sat.h"
namespace smt {
class formula_compiler {
solver_exp & s;
arith_util m_a_util;
assertion_set_rewriter m_normalizer;
elim_term_ite_strategy m_elim_ite;
assertion_set2sat m_to_sat;
void normalize();
void elim_term_ite();
void mark_axioms(assertion_set const & s, expr_fast_mark2 & axioms);
void unmark_nested_atoms(assertion_set const & s, expr_fast_mark2 & axioms);
void assert_axiom(expr * f, bool neg);
void register_atom(expr * f, sat::bool_var p);
void compile_formulas(assertion_set const & assertions);
public:
formula_compiler(solver_exp & s, params_ref const & p);
~formula_compiler();
void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d);
void operator()();
void set_cancel(bool f);
void collect_statistics(statistics & st);
void reset_statistics();
};
};
#endif

232
lib/smt_solver_exp.cpp
View file

@ -1,232 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
smt_solver_exp.cpp
Abstract:
SMT solver using strategies and search on top of sat::solver
This solver uses assertion_set strategies during restarts.
It also uses the sat::solver to handle the Boolean structure of the problem.
Author:
Leonardo de Moura (leonardo) 2011-06-25.
Revision History:
This was an experiment to rewrite Z3 kernel.
It will be deleted after we finish revamping Z3 kernel.
--*/
#include"smt_solver_exp.h"
#include"sat_solver.h"
#include"ast_translation.h"
#include"model.h"
namespace smt {
void solver_exp::bridge::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r) {
}
void solver_exp::bridge::asserted(sat::literal l) {
}
sat::check_result solver_exp::bridge::check() {
return sat::CR_DONE;
}
void solver_exp::bridge::push() {
}
void solver_exp::bridge::pop(unsigned n) {
}
void solver_exp::bridge::simplify() {
}
void solver_exp::bridge::clauses_modifed() {
}
lbool solver_exp::bridge::get_phase(sat::bool_var v) {
return l_undef;
}
solver_exp::solver_exp(ast_manager & ext_mng, params_ref const & p):
m_ext_mng(ext_mng),
m(ext_mng, true /* disable proof gen */),
m_compiler(*this, p),
m_assertions(m),
m_atom2bvar(m),
m_arith(m, p),
m_bridge(*this) {
updt_params_core(p);
m_cancel = false;
}
solver_exp::~solver_exp() {
}
void solver_exp::updt_params_core(params_ref const & p) {
m_params = p;
}
void solver_exp::updt_params(params_ref const & p) {
updt_params_core(p);
m_arith.updt_params(p);
if (m_sat)
m_sat->updt_params(p);
}
void solver_exp::collect_param_descrs(param_descrs & d) {
// TODO
}
void solver_exp::set_cancel(bool f) {
m_cancel = f;
#pragma omp critical (smt_solver_exp)
{
if (m_sat) {
m_sat->set_cancel(f);
}
}
m_arith.set_cancel(f);
m_compiler.set_cancel(f);
}
void solver_exp::init() {
m_atom2bvar.reset();
if (m_sat)
m_sat->collect_statistics(m_stats);
#pragma omp critical (smt_solver_exp)
{
m_sat = alloc(sat::solver, m_params, &m_bridge);
}
m_arith.collect_statistics(m_stats);
m_arith.reset();
set_cancel(m_cancel);
}
void solver_exp::assert_expr_core(expr * t, ast_translation & translator) {
expr * new_t = translator(t);
m_assertions.assert_expr(new_t);
}
/**
\brief Assert an expression t (owned by the external manager)
*/
void solver_exp::assert_expr(expr * t) {
ast_translation translator(m_ext_mng, m, false);
assert_expr_core(t, translator);
}
/**
\brief Assert an assertion set s (owned by the external manager)
*/
void solver_exp::assert_set(assertion_set const & s) {
SASSERT(&(s.m()) == &m_ext_mng);
ast_translation translator(m_ext_mng, m, false);
unsigned sz = s.size();
for (unsigned i = 0; i < sz; i++) {
assert_expr_core(s.form(i), translator);
}
}
void solver_exp::assert_goal(goal const & g) {
SASSERT(&(g.m()) == &m_ext_mng);
ast_translation translator(m_ext_mng, m, false);
unsigned sz = g.size();
for (unsigned i = 0; i < sz; i++) {
assert_expr_core(g.form(i), translator);
}
}
/**
\brief Store in r the current set of assertions.
r is (owned) by the external assertion set
*/
void solver_exp::get_assertions(assertion_set & r) {
SASSERT(&(r.m()) == &m_ext_mng);
ast_translation translator(m, m_ext_mng, false);
unsigned sz = m_assertions.size();
for (unsigned i = 0; i < sz; i++) {
expr * f = m_assertions.form(i);
r.assert_expr(translator(f));
}
}
void solver_exp::get_model_converter(model_converter_ref & mc) {
ast_translation translator(m, m_ext_mng, false);
if (m_mc)
mc = m_mc->translate(translator);
else
mc = 0;
}
// -----------------------
//
// Search
//
// -----------------------
lbool solver_exp::check() {
compile();
lbool r = m_arith.check();
if (r == l_false)
return r;
if (m_sat->num_vars() == 0 && r == l_true) {
model_ref md = alloc(model, m);
m_arith.mk_model(md.get());
if (m_mc)
(*m_mc)(md);
ast_translation translator(m, m_ext_mng, false);
m_model = md->translate(translator);
return l_true;
}
return l_undef;
}
void solver_exp::compile() {
m_compiler();
}
// -----------------------
//
// Pretty Printing
//
// -----------------------
void solver_exp::display(std::ostream & out) const {
m_assertions.display(out);
}
void solver_exp::display_state(std::ostream & out) const {
if (m_sat) m_sat->display(out);
m_arith.display(out);
}
// -----------------------
//
// Statistics
//
// -----------------------
void solver_exp::collect_statistics(statistics & st) const {
solver_exp * _this = const_cast<solver_exp*>(this);
if (m_sat) {
m_sat->collect_statistics(_this->m_stats);
m_sat->reset_statistics();
}
m_arith.collect_statistics(_this->m_stats);
_this->m_arith.reset_statistics();
st.copy(m_stats);
}
void solver_exp::reset_statistics() {
m_stats.reset();
}
};

130
lib/smt_solver_exp.h
View file

@ -1,130 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
smt_solver_exp.h
Abstract:
SMT solver using strategies and search on top of sat::solver
This solver uses assertion_set strategies during restarts.
It also uses the sat::solver to handle the Boolean structure of the problem.
Author:
Leonardo de Moura (leonardo) 2011-06-25.
Revision History:
This was an experiment to rewrite Z3 kernel.
It will be deleted after we finish revamping Z3 kernel.
--*/
#ifndef _SMT_SOLVER_EXP_H_
#define _SMT_SOLVER_EXP_H_
#include"smt_solver_types.h"
#include"model.h"
#include"model_converter.h"
#include"smt_formula_compiler.h"
#include"smt_arith.h"
#include"sat_extension.h"
#include"goal.h"
namespace smt {
class solver_exp {
friend class formula_compiler;
struct bridge : public sat::extension {
solver_exp & s;
bridge(solver_exp & _s):s(_s) {}
virtual void propagate(sat::literal l, sat::ext_constraint_idx idx, bool & keep) {}
virtual void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r);
virtual void asserted(sat::literal l);
virtual sat::check_result check();
virtual void push();
virtual void pop(unsigned n);
virtual void simplify();
virtual void clauses_modifed();
virtual lbool get_phase(sat::bool_var v);
};
// External ASTs are coming from m_ext_mng
ast_manager & m_ext_mng;
// The ASTs are translated into the internal manager for the following reasons:
// 1. We can run multiple smt::solver_exps in parallel with minimal synchronization
// 2. Minimize gaps in the AST ids.
ast_manager m; // internal manager
params_ref m_params;
formula_compiler m_compiler;
// Set of asserted expressions.
// This assertion set belongs to ast_manager m.
assertion_set m_assertions;
model_ref m_model;
model_converter_ref m_mc; // chain of model converters
atom2bool_var m_atom2bvar;
scoped_ptr<sat::solver> m_sat;
arith m_arith;
bridge m_bridge;
statistics m_stats;
volatile bool m_cancel;
void updt_params_core(params_ref const & p);
void assert_expr_core(expr * t, ast_translation & translator);
void init();
void compile();
public:
solver_exp(ast_manager & ext_mng, params_ref const & p);
~solver_exp();
void updt_params(params_ref const & p);
void collect_param_descrs(param_descrs & d);
void set_cancel(bool f);
void assert_expr(expr * t);
void assert_set(assertion_set const & s);
void assert_goal(goal const & g);
void get_assertions(assertion_set & r);
// -----------------------
//
// Search
//
// -----------------------
public:
lbool check();
void get_model(model_ref & m) const { m = m_model.get(); }
void get_model_converter(model_converter_ref & mc);
// -----------------------
//
// Pretty Printing
//
// -----------------------
public:
void display(std::ostream & out) const;
void display_state(std::ostream & out) const;
// -----------------------
//
// Statistics
//
// -----------------------
public:
void collect_statistics(statistics & st) const;
void reset_statistics();
};
};
#endif

96
lib/smt_solver_strategy.cpp
View file

@ -1,96 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
sat_solver_strategy.cpp
Abstract:
Strategy for using the SMT solver.
Author:
Leonardo (leonardo) 2011-06-25
Notes:
--*/
#include"smt_solver_strategy.h"
#include"smt_solver_exp.h"
smt_solver_strategy::smt_solver_strategy(ast_manager & _m, params_ref const & p):
m(_m),
m_params(p) {
}
smt_solver_strategy::~smt_solver_strategy() {
}
void smt_solver_strategy::init_solver() {
smt::solver_exp * new_solver = alloc(smt::solver_exp, m, m_params);
#pragma omp critical (as_st_cancel)
{
m_solver = new_solver;
}
}
void smt_solver_strategy::updt_params(params_ref const & p) {
m_params = p;
}
void smt_solver_strategy::get_param_descrs(param_descrs & r) {
// TODO
}
void smt_solver_strategy::operator()(assertion_set & s, model_converter_ref & mc) {
if (s.m().proofs_enabled())
throw smt_solver_exception("smt quick solver does not support proof generation");
mc = 0;
s.elim_redundancies();
if (s.inconsistent())
return;
init_solver();
m_solver->assert_set(s);
s.reset();
lbool r = m_solver->check();
m_solver->collect_statistics(m_stats);
if (r == l_false) {
s.assert_expr(m.mk_false());
}
else if (r == l_true) {
model_ref md;
m_solver->get_model(md);
mc = model2model_converter(md.get());
}
else {
// recover simplified assertion set
m_solver->get_assertions(s);
m_solver->get_model_converter(mc);
}
}
void smt_solver_strategy::cleanup() {
if (m_solver)
m_solver->collect_statistics(m_stats);
#pragma omp critical (as_st_cancel)
{
m_solver = 0;
}
}
void smt_solver_strategy::set_cancel(bool f) {
if (m_solver)
m_solver->set_cancel(f);
}
void smt_solver_strategy::reset_statistics() {
m_stats.reset();
}
void smt_solver_strategy::collect_statistics(statistics & st) const {
st.copy(m_stats);
}

55
lib/smt_solver_strategy.h
View file

@ -1,55 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
smt_solver_strategy.h
Abstract:
Strategy for using the SAT solver.
Author:
Leonardo (leonardo) 2011-06-25
Notes:
--*/
#ifndef _SMT_SOLVER_STRATEGY_H_
#define _SMT_SOLVER_STRATEGY_H_
#include"assertion_set_strategy.h"
namespace smt { class solver_exp; };
class smt_solver_strategy : public assertion_set_strategy {
struct imp;
ast_manager & m;
params_ref m_params;
statistics m_stats;
scoped_ptr<smt::solver_exp> m_solver;
void init_solver();
public:
smt_solver_strategy(ast_manager & m, params_ref const & p = params_ref());
virtual ~smt_solver_strategy();
virtual void updt_params(params_ref const & p);
static void get_param_descrs(param_descrs & r);
virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
virtual void operator()(assertion_set & s, model_converter_ref & mc);
virtual void cleanup();
virtual void collect_statistics(statistics & st) const;
virtual void reset_statistics();
protected:
virtual void set_cancel(bool f);
};
inline as_st * mk_smt2_solver(ast_manager & m, params_ref const & p = params_ref()) {
return clean(alloc(smt_solver_strategy, m, p));
}
#endif

47
lib/smt_solver_types.h
View file

@ -1,47 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
smt_solver_types.h
Abstract:
Auxiliary definitions for smt::solver class.
Author:
Leonardo de Moura (leonardo) 2011-06-25.
Revision History:
This was an experiment to rewrite Z3 kernel.
It will be deleted after we finish revamping Z3 kernel.
--*/
#ifndef _SMT_SOLVER_TYPES_H_
#define _SMT_SOLVER_TYPES_H_
#include"assertion_set.h"
#include"strategy_exception.h"
#include"params.h"
#include"statistics.h"
#include"lbool.h"
#include"sat_types.h"
class ast_translation;
namespace sat {
class solver;
};
namespace smt {
class solver_exp;
class formula_compiler;
typedef unsigned atom_id;
typedef unsigned_vector atom_id_vector;
const atom_id null_atom_id = sat::null_bool_var;
};
MK_ST_EXCEPTION(smt_solver_exception);
#endif

26
lib/st_cmds.h
View file

@ -1,26 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
st_cmds.h
Abstract:
Commands for testing strategies.
Author:
Leonardo de Moura (leonardo) 2011-04-27
Revision History:
--*/
#ifndef _ST_CMD_H_
#define _ST_CMD_H_
class cmd_context;
void install_st_cmds(cmd_context & ctx);
#endif

56
lib/subpaving_cmds.cpp
View file

@ -1,56 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_cmds.cpp
Abstract:
Commands for debugging subpaving module.
Author:
Leonardo (leonardo) 2012-08-09
Notes:
--*/
#include<sstream>
#include"cmd_context.h"
#include"cmd_util.h"
#include"expr2subpaving.h"
#include"th_rewriter.h"
#include"ast_smt2_pp.h"
#include"expr2var.h"
static void to_subpaving(cmd_context & ctx, expr * t) {
ast_manager & m = ctx.m();
unsynch_mpq_manager qm;
scoped_ptr<subpaving::context> s;
s = subpaving::mk_mpq_context(qm);
expr2var e2v(m);
expr2subpaving e2s(m, *s, &e2v);
params_ref p;
p.set_bool(":mul-to-power", true);
th_rewriter simp(m, p);
expr_ref t_s(m);
simp(t, t_s);
scoped_mpz n(qm), d(qm);
ctx.regular_stream() << mk_ismt2_pp(t_s, m) << "\n=======>" << std::endl;
subpaving::var x = e2s.internalize_term(t_s, n, d);
expr2var::iterator it = e2v.begin();
expr2var::iterator end = e2v.end();
for (; it != end; ++it) {
ctx.regular_stream() << "x" << it->m_value << " := " << mk_ismt2_pp(it->m_key, m) << "\n";
}
s->display_constraints(ctx.regular_stream());
ctx.regular_stream() << n << "/" << d << " x" << x << "\n";
}
UNARY_CMD(to_subpaving_cmd, "to-subpaving", "<expr>", "internalize expression into subpaving module", CPK_EXPR, expr *, to_subpaving(ctx, arg););
void install_subpaving_cmds(cmd_context & ctx) {
#ifndef _EXTERNAL_RELEASE
ctx.insert(alloc(to_subpaving_cmd));
#endif
}

21
lib/subpaving_cmds.h
View file

@ -1,21 +0,0 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
subpaving_cmds.h
Abstract:
Commands for debugging subpaving module.
Author:
Leonardo (leonardo) 2012-08-09
Notes:
--*/
class cmd_context;
void install_subpaving_cmds(cmd_context & ctx);

656
lib/symmetry_reduce_tactic.cpp
View file

@ -1,656 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
symmetry_reduce.cpp
Abstract:
Add symmetry breaking predicates to goals.
Author:
Nikolaj (nbjorner) 2011-05-31
Notes:
This is a straight-forward and literal
adaption of the algorithms proposed for veriT.
--*/
#include"tactical.h"
#include"for_each_expr.h"
#include"map.h"
#include"expr_replacer.h"
#include"rewriter_def.h"
#include"ast_pp.h"
class symmetry_reduce_tactic : public tactic {
class imp;
imp * m_imp;
public:
symmetry_reduce_tactic(ast_manager & m);
virtual tactic * translate(ast_manager & m) {
return alloc(symmetry_reduce_tactic, m);
}
virtual ~symmetry_reduce_tactic();
virtual void operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core);
virtual void cleanup();
};
class ac_rewriter {
ast_manager& m_manager;
public:
ac_rewriter(ast_manager& m): m_manager(m) {}
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
if ((f->is_associative() && f->is_commutative()) ||
m_manager.is_distinct(f)) {
ptr_buffer<expr> buffer;
buffer.append(num_args, args);
std::sort(buffer.begin(), buffer.end(), ast_lt_proc());
bool change = false;
for (unsigned i = 0; !change && i < num_args; ++i) {
change = (args[i] != buffer[i]);
}
if (change) {
result = m().mk_app(f, num_args, buffer.begin());
return BR_DONE;
}
}
else if (f->is_commutative() && num_args == 2 && args[0]->get_id() > args[1]->get_id()) {
expr* args2[2] = { args[1], args[0] };
result = m().mk_app(f, num_args, args2);
return BR_DONE;
}
return BR_FAILED;
}
void mk_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
if (mk_app_core(f, num_args, args, result) == BR_FAILED)
result = m().mk_app(f, num_args, args);
}
private:
ast_manager& m() const { return m_manager; }
};
struct ac_rewriter_cfg : public default_rewriter_cfg {
ac_rewriter m_r;
bool rewrite_patterns() const { return false; }
bool flat_assoc(func_decl * f) const { return false; }
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0;
return m_r.mk_app_core(f, num, args, result);
}
ac_rewriter_cfg(ast_manager & m):m_r(m) {}
};
class ac_rewriter_star : public rewriter_tpl<ac_rewriter_cfg> {
ac_rewriter_cfg m_cfg;
public:
ac_rewriter_star(ast_manager & m):
rewriter_tpl<ac_rewriter_cfg>(m, false, m_cfg),
m_cfg(m) {}
};
template class rewriter_tpl<ac_rewriter_cfg>;
class symmetry_reduce_tactic::imp {
typedef ptr_vector<app> permutation;
typedef vector<permutation> permutations;
typedef ptr_vector<app> term_set;
typedef obj_map<app, unsigned> app_map;
typedef u_map<ptr_vector<app> > inv_app_map;
ast_manager& m_manager;
ac_rewriter_star m_rewriter;
scoped_ptr<expr_replacer> m_replace;
ast_manager& m() const { return m_manager; }
public:
imp(ast_manager& m) : m_manager(m), m_rewriter(m) {
m_replace = mk_default_expr_replacer(m);
}
~imp() {}
void operator()(goal & g) {
if (g.inconsistent())
return;
tactic_report report("symmetry-reduce", g);
vector<ptr_vector<app> > P;
expr_ref fml(m());
to_formula(g, fml);
app_map occs;
compute_occurrences(fml, occs);
find_candidate_permutations(fml, occs, P);
if (P.empty()) {
return;
}
term_set T, cts;
unsigned num_sym_break_preds = 0;
for (unsigned i = 0; i < P.size(); ++i) {
term_set& consts = P[i];
if (invariant_by_permutations(fml, consts)) {
cts.reset();
select_terms(fml, consts, T);
while (!T.empty() && cts.size() < consts.size()) {
app* t = select_most_promising_term(fml, T, cts, consts, occs);
T.erase(t);
compute_used_in(t, cts, consts);
app* c = select_const(consts, cts);
if (!c) break;
cts.push_back(c);
expr* mem = mk_member(t, cts);
g.assert_expr(mem);
num_sym_break_preds++;
TRACE("symmetry_reduce", tout << "member predicate: " << mk_pp(mem, m()) << "\n";);
fml = m().mk_and(fml.get(), mem);
normalize(fml);
}
}
}
report_tactic_progress(":num-symmetry-breaking ", num_sym_break_preds);
}
private:
void to_formula(goal const & g, expr_ref& fml) {
ptr_vector<expr> conjs;
for (unsigned i = 0; i < g.size(); ++i) {
conjs.push_back(g.form(i));
}
fml = m().mk_and(conjs.size(), conjs.c_ptr());
normalize(fml);
}
// find candidate permutations
void find_candidate_permutations(expr* fml, app_map const& occs, permutations& P) {
app_map coloring;
app_map depth;
inv_app_map inv_color;
unsigned num_occs;
compute_sort_colors(fml, coloring);
compute_max_depth(fml, depth);
merge_colors(occs, coloring);
merge_colors(depth, coloring);
// compute_siblings(fml, coloring);
compute_inv_app(coloring, inv_color);
inv_app_map::iterator it = inv_color.begin(), end = inv_color.end();
for (; it != end; ++it) {
if (it->m_value.size() < 2) {
continue;
}
VERIFY(occs.find(it->m_value[0], num_occs));
if (num_occs < 2) {
continue;
}
bool is_const = true;
for (unsigned j = 0; is_const && j < it->m_value.size(); ++j) {
is_const = it->m_value[j]->get_num_args() == 0;
}
if (!is_const) {
continue;
}
P.push_back(it->m_value);
TRACE("symmetry_reduce",
for (unsigned i = 0; i < it->m_value.size(); ++i) {
tout << mk_pp(it->m_value[i], m()) << " ";
}
tout << "\n";);
}
}
//
// refine coloring by taking most specific generalization.
// a |-> c1, b |-> c2 <c1,c2> |-> c
//
struct u_pair {
unsigned m_first;
unsigned m_second;
u_pair(unsigned f, unsigned s) : m_first(f), m_second(s) {}
u_pair(): m_first(0), m_second(0) {}
struct hash {
unsigned operator()(u_pair const& p) const {
return mk_mix(p.m_first, p.m_second, 23);
}
};
struct eq {
bool operator()(u_pair const& p, u_pair const& q) const {
return p.m_first == q.m_first && p.m_second == q.m_second;
}
};
};
typedef map<u_pair, unsigned, u_pair::hash, u_pair::eq> pair_map;
bool merge_colors(app_map const& colors1, app_map& colors2) {
pair_map recolor;
unsigned num_colors = 0, v1, v2, w, old_max = 0;
app_map::iterator it = colors2.begin(), end = colors2.end();
for (; it != end; ++it) {
app* a = it->m_key;
v1 = it->m_value;
VERIFY(colors1.find(a, v2));
if (recolor.find(u_pair(v1, v2), w)) {
it->m_value = w;
}
else {
it->m_value = num_colors;
recolor.insert(u_pair(v1, v2), num_colors++);
}
if (v1 > old_max) old_max = v1;
}
return num_colors > old_max + 1;
}
class sort_colors {
ast_manager& m_manager;
app_map& m_app2sortid;
obj_map<sort,unsigned> m_sort2id;
unsigned m_max_id;
public:
sort_colors(ast_manager& m, app_map& app2sort):
m_manager(m), m_app2sortid(app2sort), m_max_id(0) {}
void operator()(app* n) {
sort* s = m_manager.get_sort(n);
unsigned id;
if (!m_sort2id.find(s, id)) {
id = m_max_id++;
m_sort2id.insert(s, id);
}
m_app2sortid.insert(n, id);
}
void operator()(quantifier * n) {}
void operator()(var * n) {}
};
void compute_sort_colors(expr* fml, app_map& app2sortId) {
app2sortId.reset();
sort_colors sc(m(), app2sortId);
for_each_expr(sc, fml);
}
void compute_inv_app(app_map const& map, inv_app_map& inv_map) {
app_map::iterator it = map.begin(), end = map.end();
for (; it != end; ++it) {
app* t = it->m_key;
unsigned n = it->m_value;
if (is_uninterpreted(t)) {
inv_app_map::entry* e = inv_map.insert_if_not_there2(n, ptr_vector<app>());
e->get_data().m_value.push_back(t);
}
}
}
bool is_uninterpreted(app* t) const {
return t->get_family_id() == null_family_id;
}
// compute maximal depth of terms.
void compute_max_depth(expr* e, app_map& depth) {
ptr_vector<expr> todo;
unsigned_vector depths;
unsigned d, d1;
todo.push_back(e);
depths.push_back(0);
while (!todo.empty()) {
e = todo.back();
d = depths.back();
todo.pop_back();
depths.pop_back();
if (is_var(e)) {
// nothing
}
else if (is_quantifier(e)) {
todo.push_back(to_quantifier(e)->get_expr());
depths.push_back(d+1);
}
else if (is_app(e)) {
app* a = to_app(e);
if (depth.find(a, d1) && d <= d1) {
continue;
}
depth.insert(a, d);
++d;
for (unsigned i = 0; i < a->get_num_args(); ++i) {
todo.push_back(a->get_arg(i));
depths.push_back(d);
}
}
else {
UNREACHABLE();
}
}
}
// color nodes according to the function symbols they appear in
typedef obj_hashtable<func_decl> fun_set;
typedef obj_map<app, fun_set*> app_parents;
class parents {
app_parents m_use_funs;
public:
parents() {}
app_parents const& get_parents() { return m_use_funs; }
void operator()(app* n) {
func_decl* f;
unsigned sz = n->get_num_args();
for (unsigned i = 0; i < sz; ++i) {
expr* e = n->get_arg(i);
if (is_app(e)) {
app_parents::obj_map_entry* entry = m_use_funs.insert_if_not_there2(to_app(e), 0);
if (!entry->get_data().m_value) entry->get_data().m_value = alloc(fun_set);
entry->get_data().m_value->insert(f);
}
}
}
void operator()(quantifier *n) {}
void operator()(var* n) {}
};
void compute_parents(expr* e, app_map& parents) {
}
typedef hashtable<unsigned, u_hash, u_eq> uint_set;
typedef obj_map<app, uint_set*> app_siblings;;
class siblings {
app_map const& m_colors;
app_siblings m_sibs;
public:
siblings(app_map const& colors): m_colors(colors) {}
app_siblings const& get() { return m_sibs; }
void operator()(app* n) {
unsigned sz = n->get_num_args();
for (unsigned i = 0; i < sz; ++i) {
expr* e = n->get_arg(i);
if (!is_app(e)) continue;
app_siblings::obj_map_entry* entry = m_sibs.insert_if_not_there2(to_app(e), 0);
if (!entry->get_data().get_value()) entry->get_data().m_value = alloc(uint_set);
for (unsigned j = 0; j < sz; ++j) {
expr* f = n->get_arg(j);
if (is_app(f) && i != j) {
unsigned c1 = 0;
m_colors.find(to_app(f), c1);
entry->get_data().m_value->insert(c1);
}
}
}
}
void operator()(quantifier *n) {}
void operator()(var* n) {}
};
// refine coloring by taking colors of siblings into account.
bool compute_siblings_rec(expr* e, app_map& colors) {
siblings sibs(colors);
app_map colors1;
for_each_expr(sibs, e);
app_siblings const& s = sibs.get();
app_siblings::iterator it = s.begin(), end = s.end();
for (; it != end; ++it) {
app* a = it->m_key;
uint_set* set = it->m_value;
uint_set::iterator it2 = set->begin(), end2 = set->end();
unsigned c = 0;
for(; it2 != end2; ++it2) {
c += 1 + *it2;
}
colors1.insert(a, c);
dealloc(set);
}
if (is_app(e)) {
colors1.insert(to_app(e), 0);
}
return merge_colors(colors1, colors);
}
void compute_siblings(expr* fml, app_map& colors) {
while(compute_siblings_rec(fml, colors));
}
// check if assertion set is invariant under the current permutation
bool invariant_by_permutations(expr* fml, permutation& p) {
SASSERT(p.size() >= 2);
bool result = check_swap(fml, p[0], p[1]) && check_cycle(fml, p);
TRACE("symmetry_reduce",
if (result) {
tout << "Symmetric: ";
}
else {
tout << "Not symmetric: ";
}
for (unsigned i = 0; i < p.size(); ++i) {
tout << mk_pp(p[i], m()) << " ";
}
tout << "\n";);
return result;
}
bool check_swap(expr* fml, app* t1, app* t2) {
expr_substitution sub(m());
sub.insert(t1, t2);
sub.insert(t2, t1);
m_replace->set_substitution(&sub);
return check_substitution(fml);
}
bool check_cycle(expr* fml, permutation& p) {
expr_substitution sub(m());
for (unsigned i = 0; i + 1 < p.size(); ++i) {
sub.insert(p[i], p[i+1]);
}
sub.insert(p[p.size()-1], p[0]);
m_replace->set_substitution(&sub);
return check_substitution(fml);
}
bool check_substitution(expr* t) {
expr_ref r(m());
(*m_replace)(t, r);
normalize(r);
return t == r.get();
}
void normalize(expr_ref& r) {
proof_ref pr(m());
expr_ref result(m());
m_rewriter(r.get(), result, pr);
r = result;
}
// select terms that are range restricted by set p.
void select_terms(expr* fml, term_set const& p, term_set& T) {
T.reset();
ptr_vector<expr> todo;
todo.push_back(fml);
app* t = 0;
while (!todo.empty()) {
fml = todo.back();
todo.pop_back();
if (m().is_and(fml)) {
todo.append(to_app(fml)->get_num_args(), to_app(fml)->get_args());
}
else if (is_range_restriction(fml, p, t)) {
T.push_back(t);
}
}
}
bool is_range_restriction(expr* form, term_set const& C, app*& t) {
if (!m().is_or(form)) return false;
unsigned sz = to_app(form)->get_num_args();
t = 0;
for (unsigned i = 0; i < sz; ++i) {
expr* e = to_app(form)->get_arg(i);
expr* e1, *e2;
if (!m().is_eq(e, e1, e2)) return false;
if (!is_app(e1) || !is_app(e2)) return false;
app* a1 = to_app(e1), *a2 = to_app(e2);
if (C.contains(a1) && (t == 0 || t == a2)) {
t = a2;
}
else if (C.contains(a2) && (t == 0 || t == a1)) {
t = a1;
}
else {
return false;
}
}
return t != 0;
}
// select the most promising term among T.
// terms with the largest number of occurrences have higher weight.
// terms that have fewest terms among C as subterms are preferred.
class num_occurrences {
app_map& m_occs;
public:
num_occurrences(app_map& occs): m_occs(occs) {}
void operator()(app* n) {
app_map::obj_map_entry* e;
m_occs.insert_if_not_there2(n, 0);
unsigned sz = n->get_num_args();
for (unsigned i = 0; i < sz; ++i) {
expr* arg = n->get_arg(i);
if (is_app(arg)) {
e = m_occs.insert_if_not_there2(to_app(arg), 0);
e->get_data().m_value++;
}
}
}
void operator()(quantifier * n) {}
void operator()(var * n) {}
};
void compute_occurrences(expr* fml, app_map& occs) {
occs.reset();
num_occurrences num_occ(occs);
for_each_expr(num_occ, fml);
}
app* select_most_promising_term(
expr* fml, term_set const& T,
term_set& cts, term_set const& consts, app_map const& occs) {
SASSERT(!T.empty());
app* t = T[0];
unsigned weight, weight1;
VERIFY(occs.find(t, weight));
unsigned cts_delta = compute_cts_delta(t, cts, consts);
TRACE("symmetry_reduce", tout << mk_pp(t, m()) << " " << weight << " " << cts_delta << "\n";);
for (unsigned i = 1; i < T.size(); ++i) {
app* t1 = T[i];
VERIFY(occs.find(t1, weight1));
if (weight1 < weight && t->get_num_args() <= t1->get_num_args()) {
continue;
}
unsigned cts_delta1 = compute_cts_delta(t1, cts, consts);
TRACE("symmetry_reduce", tout << mk_pp(t1, m()) << " " << weight1 << " " << cts_delta1 << "\n";);
if ((t->get_num_args() == t1->get_num_args() && (weight1 > weight || cts_delta1 < cts_delta)) ||
t->get_num_args() > t1->get_num_args()) {
cts_delta = cts_delta1;
weight = weight1;
t = t1;
}
}
return t;
}
// add to cts subterms of t that are members of consts.
class member_of {
term_set const& m_S;
term_set& m_r;
public:
member_of(term_set const& S, term_set& r) : m_S(S), m_r(r) {}
void operator()(app* n) {
if (m_S.contains(n) && !m_r.contains(n)) {
m_r.push_back(n);
}
}
void operator()(quantifier * n) {}
void operator()(var * n) {}
};
void compute_used_in(app* t, term_set& cts, term_set const& consts) {
member_of mem(consts, cts);
for_each_expr(mem, t);
TRACE("symmetry_reduce",
tout << "Term: " << mk_pp(t, m()) << "\n";
tout << "Support set: ";
for (unsigned i = 0; i < consts.size(); ++i) {
tout << mk_pp(consts[i], m()) << " ";
}
tout << "\n";
tout << "Constants: ";
for (unsigned i = 0; i < cts.size(); ++i) {
tout << mk_pp(cts[i], m()) << " ";
}
tout << "\n";
);
}
unsigned compute_cts_delta(app* t, term_set& cts, term_set const& consts) {
unsigned cts_size = cts.size();
if (cts_size == consts.size()) {
return 0;
}
compute_used_in(t, cts, consts);
unsigned cts_delta = cts.size() - cts_size;
cts.resize(cts_size);
return cts_delta;
}
// select element in A not in B
app* select_const(term_set const& A, term_set const& B) {
unsigned j;
for (j = 0; j < A.size() && B.contains(A[j]); ++j);
return (j == A.size())?0:A[j];
}
app* mk_member(app* t, term_set const& C) {
expr_ref_vector eqs(m());
for (unsigned i = 0; i < C.size(); ++i) {
eqs.push_back(m().mk_eq(t, C[i]));
}
return m().mk_or(eqs.size(), eqs.c_ptr());
}
};
symmetry_reduce_tactic::symmetry_reduce_tactic(ast_manager & m) {
m_imp = alloc(imp, m);
}
symmetry_reduce_tactic::~symmetry_reduce_tactic() {
dealloc(m_imp);
}
void symmetry_reduce_tactic::operator()(goal_ref const & g,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
fail_if_proof_generation("symmetry_reduce", g);
fail_if_unsat_core_generation("symmetry_reduce", g);
mc = 0; pc = 0; core = 0; result.reset();
(*m_imp)(*(g.get()));
g->inc_depth();
result.push_back(g.get());
}
void symmetry_reduce_tactic::cleanup() {
// no-op.
}
tactic * mk_symmetry_reduce_tactic(ast_manager & m, params_ref const & p) {
return alloc(symmetry_reduce_tactic, m);
}

28
lib/symmetry_reduce_tactic.h
View file

@ -1,28 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
symmetry_reduce.h
Abstract:
Add symmetry breaking predicates to assertion sets.
Author:
Nikolaj (nbjorner) 2011-05-31
Notes:
--*/
#ifndef _SYMMETRY_REDUCE_TACTIC_H_
#define _SYMMETRY_REDUCE_TACTIC_H_
#include"params.h"
class ast_manager;
class tactic;
tactic * mk_symmetry_reduce_tactic(ast_manager & m, params_ref const & p);
#endif