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

Reorganizing the code

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-20 20:53:33 -07:00
parent 6bdb009c3e
commit 2b8fb6c718
13 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

206
lib/array_factory.cpp
View file

@ -1,206 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
array_factory.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-10-28.
Revision History:
--*/
#include"array_factory.h"
#include"array_decl_plugin.h"
#include"proto_model.h"
#include"func_interp.h"
#include"ast_pp.h"
func_decl * mk_aux_decl_for_array_sort(ast_manager & m, sort * s) {
ptr_buffer<sort> domain;
sort * range = get_array_range(s);
unsigned arity = get_array_arity(s);
for (unsigned i = 0; i < arity; i++) {
domain.push_back(get_array_domain(s, i));
}
return m.mk_fresh_func_decl(symbol::null, symbol::null, arity, domain.c_ptr(), range);
}
array_factory::array_factory(ast_manager & m, proto_model & md):
struct_factory(m, m.get_family_id("array"), md) {
}
/**
\brieft Return as-array[f] where f is a fresh function symbol with the right domain and range for the array sort s.
Store in fi the function interpretation for f.
*/
expr * array_factory::mk_array_interp(sort * s, func_interp * & fi) {
func_decl * f = mk_aux_decl_for_array_sort(m_manager, s);
fi = alloc(func_interp, m_manager, get_array_arity(s));
m_model.register_decl(f, fi);
parameter p[1] = { parameter(f) };
expr * val = m_manager.mk_app(get_family_id(), OP_AS_ARRAY, 1, p);
register_value(val);
return val;
}
void array_factory::get_some_args_for(sort * s, ptr_buffer<expr> & args) {
unsigned arity = get_array_arity(s);
for (unsigned i = 0; i < arity; i++) {
sort * d = get_array_domain(s, i);
expr * a = m_model.get_some_value(d);
args.push_back(a);
}
}
expr * array_factory::get_some_value(sort * s) {
TRACE("array_factory", tout << mk_pp(s, m_manager) << "\n";);
value_set * set = 0;
if (m_sort2value_set.find(s, set) && !set->empty())
return *(set->begin());
func_interp * fi;
expr * val = mk_array_interp(s, fi);
ptr_buffer<expr> args;
get_some_args_for(s, args);
fi->insert_entry(args.c_ptr(), m_model.get_some_value(get_array_range(s)));
return val;
}
bool array_factory::mk_two_diff_values_for(sort * s) {
DEBUG_CODE({
value_set * set = 0;
SASSERT(!m_sort2value_set.find(s, set) || set->size() == 0);
});
expr_ref r1(m_manager);
expr_ref r2(m_manager);
sort * range = get_array_range(s);
if (!m_model.get_some_values(range, r1, r2))
return false; // failed... the range is probably unit.
ptr_buffer<expr> args;
get_some_args_for(s, args);
func_interp * fi1;
func_interp * fi2;
mk_array_interp(s, fi1);
mk_array_interp(s, fi2);
fi1->insert_entry(args.c_ptr(), r1);
fi2->insert_entry(args.c_ptr(), r2);
DEBUG_CODE({
value_set * set = 0;
SASSERT(m_sort2value_set.find(s, set) && set->size() == 2);
});
return true;
}
bool array_factory::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
value_set * set = 0;
if (!m_sort2value_set.find(s, set) || set->size() == 0) {
if (!mk_two_diff_values_for(s))
return false;
}
m_sort2value_set.find(s, set);
SASSERT(set != 0);
SASSERT(set->size() > 0);
if (set->size() == 1) {
v1 = *(set->begin());
v2 = get_fresh_value(s);
return v2.get() != 0;
}
else {
SASSERT(set->size() >= 2);
value_set::iterator it = set->begin();
v1 = *it;
++it;
v2 = *it;
return true;
}
}
//
// TODO: I have to check if the following procedure is really correct.
// I'm supporting partial arrays where the "else" can be set later by the model_finder or model classes.
// Projection functions may be also used.
//
// If projections are not used, then the following code should work if the "else" of a partial array
// is set with the result of some entry.
//
expr * array_factory::get_fresh_value(sort * s) {
value_set * set = get_value_set(s);
if (set->empty()) {
// easy case
return get_some_value(s);
}
sort * range = get_array_range(s);
expr * range_val = m_model.get_fresh_value(range);
if (range_val != 0) {
// easy case
func_interp * fi;
expr * val = mk_array_interp(s, fi);
ptr_buffer<expr> args;
get_some_args_for(s, args);
fi->insert_entry(args.c_ptr(), range_val);
return val;
}
else {
TRACE("array_factory_bug", tout << "array fresh value: using fresh index, range: " << mk_pp(range, m_manager) << "\n";);
expr_ref v1(m_manager);
expr_ref v2(m_manager);
if (m_model.get_some_values(range, v1, v2)) {
// Claim: A is fresh if A[i1] = v1 and A[i2] = v2 where i1 and i2 are fresh values,
// and v1 and v2 are distinct.
//
// Proof: let assume there is an Array A' such that A' = A.
// Then A[i1] == A'[i1] and A[i2] == A'[i2]. Since, i1 and i2 are fresh,
// A' does not have an entry for i1 or i2, So A'[i1] == A'[i2] == A'.m_else.
// Thus, A[i1] == A[i2] which is a contradiction since v1 != v2 and A[i1] = v1 and A[i2] = v2.
TRACE("array_factory_bug", tout << "v1: " << mk_pp(v1, m_manager) << " v2: " << mk_pp(v2, m_manager) << "\n";);
ptr_buffer<expr> args1;
ptr_buffer<expr> args2;
bool found = false;
unsigned arity = get_array_arity(s);
for (unsigned i = 0; i < arity; i++) {
sort * d = get_array_domain(s, i);
if (!found) {
expr * arg1 = m_model.get_fresh_value(d);
expr * arg2 = m_model.get_fresh_value(d);
if (arg1 != 0 && arg2 != 0) {
found = true;
args1.push_back(arg1);
args2.push_back(arg2);
continue;
}
}
expr * arg = m_model.get_some_value(d);
args1.push_back(arg);
args2.push_back(arg);
}
if (found) {
func_interp * fi;
expr * val = mk_array_interp(s, fi);
fi->insert_entry(args1.c_ptr(), v1);
fi->insert_entry(args2.c_ptr(), v2);
return val;
}
}
}
// TODO: use more expensive procedures to create a fresh array value.
// Example: track the values used in the domain.
// Remark: in the current implementation, this function
// will never fail, since if a type is finite, then
// type_pred will be applied and get_fresh_value will not
// need to be used.
// failed to create a fresh array value
TRACE("array_factory_bug", tout << "failed to build fresh array value\n";);
return 0;
}

45
lib/array_factory.h
View file

@ -1,45 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
array_factory.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-10-28.
Revision History:
--*/
#ifndef _ARRAY_FACTORY_H_
#define _ARRAY_FACTORY_H_
#include"struct_factory.h"
class func_interp;
func_decl * mk_aux_decl_for_array_sort(ast_manager & m, sort * s);
class array_factory : public struct_factory {
expr * mk_array_interp(sort * s, func_interp * & fi);
void get_some_args_for(sort * s, ptr_buffer<expr> & args);
bool mk_two_diff_values_for(sort * s);
public:
array_factory(ast_manager & m, proto_model & md);
virtual ~array_factory() {}
virtual expr * get_some_value(sort * s);
virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2);
virtual expr * get_fresh_value(sort * s);
};
#endif /* _ARRAY_FACTORY_H_ */

864
lib/array_simplifier_plugin.cpp
View file

@ -1,864 +0,0 @@
/*++
Copyright (c) 2008 Microsoft Corporation
Module Name:
array_simplifier_plugin.cpp
Abstract:
<abstract>
Author:
Nikolaj Bjorner (nbjorner) 2008-05-05
Revision History:
Notes TODO:
Examine quadratic cost of simplification vs. model-based procedure.
Parameterize cache replacement strategy.
Some parameters are hard-wired.
--*/
#include "array_simplifier_plugin.h"
#include "ast_ll_pp.h"
#include "ast_pp.h"
array_simplifier_plugin::array_simplifier_plugin(
ast_manager & m,
basic_simplifier_plugin& s,
simplifier& simp,
theory_array_params const& p) :
simplifier_plugin(symbol("array"),m),
m_util(m),
m_simp(s),
m_simplifier(simp),
m_params(p),
m_store_cache_size(0)
{}
array_simplifier_plugin::~array_simplifier_plugin() {
select_cache::iterator it = m_select_cache.begin();
select_cache::iterator end = m_select_cache.end();
for ( ; it != end; ++it) {
m_manager.dec_array_ref(it->m_key->size(), it->m_key->c_ptr());
m_manager.dec_ref(it->m_value);
dealloc(it->m_key);
}
store_cache::iterator it2 = m_store_cache.begin();
store_cache::iterator end2 = m_store_cache.end();
for (; it2 != end2; ++it2) {
m_manager.dec_ref(it->m_value);
dealloc(it->m_key);
}
}
bool array_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
if (!m_params.m_array_simplify)
return false;
set_reduce_invoked();
if (m_presimp)
return false;
#if _DEBUG
for (unsigned i = 0; i < num_args && i < f->get_arity(); ++i) {
SASSERT(m_manager.get_sort(args[i]) == f->get_domain(i));
}
#endif
TRACE("array_simplifier", {
tout << mk_pp(f, m_manager) << " ";
for (unsigned i = 0; i < num_args; ++i) {
tout << mk_pp(args[i], m_manager) << " ";
}
tout << "\n";
}
);
SASSERT(f->get_family_id() == m_fid);
switch(f->get_decl_kind()) {
case OP_SELECT:
mk_select(num_args, args, result);
break;
case OP_STORE:
mk_store(f, num_args, args, result);
break;
case OP_SET_UNION: {
sort* s = f->get_range();
expr_ref empty(m_manager);
mk_empty_set(s, empty);
switch(num_args) {
case 0:
result = empty;
break;
case 1:
result = args[0];
break;
default: {
result = args[0];
func_decl* f_or = m_manager.mk_or_decl();
for (unsigned i = 1; i < num_args; ++i) {
mk_map(f_or, result, args[i], result);
}
break;
}
}
break;
}
case OP_SET_INTERSECT: {
expr_ref full(m_manager);
mk_full_set(f->get_range(), full);
switch(num_args) {
case 0:
result = full;
break;
case 1:
result = args[0];
break;
default: {
result = args[0];
func_decl* f_and = m_manager.mk_and_decl();
for (unsigned i = 1; i < num_args; ++i) {
mk_map(f_and, result, args[i], result);
}
break;
}
}
TRACE("array_simplifier", tout << "sort " << mk_pp(result.get(), m_manager) << "\n";);
break;
}
case OP_SET_SUBSET: {
SASSERT(num_args == 2);
expr_ref diff(m_manager), emp(m_manager);
mk_set_difference(num_args, args, diff);
mk_empty_set(m_manager.get_sort(args[0]), emp);
m_simp.mk_eq(diff.get(), emp.get(), result);
break;
}
case OP_SET_COMPLEMENT: {
SASSERT(num_args == 1);
func_decl* f_not = m_manager.mk_not_decl();
mk_map(f_not, args[0], result);
break;
}
case OP_SET_DIFFERENCE: {
SASSERT(num_args == 2);
expr_ref r1(m_manager);
mk_map(m_manager.mk_not_decl(), args[1], r1);
mk_map(m_manager.mk_and_decl(), args[0], r1, result);
break;
}
case OP_ARRAY_MAP: {
SASSERT(f->get_num_parameters() == 1);
SASSERT(f->get_parameter(0).is_ast());
SASSERT(is_func_decl(f->get_parameter(0).get_ast()));
//
// map_d (store a j v) = (store (map_f a) v (d v))
//
if (num_args == 1 && is_store(args[0])) {
app* store_expr = to_app(args[0]);
unsigned num_args = store_expr->get_num_args();
SASSERT(num_args >= 3);
parameter p = f->get_parameter(0);
func_decl* d = to_func_decl(p.get_ast());
expr* a = store_expr->get_arg(0);
expr* v = store_expr->get_arg(num_args-1);
// expr*const* args = store_expr->get_args()+1;
expr_ref r1(m_manager), r2(m_manager);
ptr_vector<expr> new_args;
reduce(f, 1, &a, r1);
m_simplifier.mk_app(d, 1, &v, r2);
new_args.push_back(r1);
for (unsigned i = 1; i + 1 < num_args; ++i) {
new_args.push_back(store_expr->get_arg(i));
}
new_args.push_back(r2);
mk_store(store_expr->get_decl(), num_args, new_args.c_ptr(), result);
break;
}
//
// map_d (store a j v) (store b j w) = (store (map_f a b) j (d v w))
//
if (num_args > 1 && same_store(num_args, args)) {
app* store_expr1 = to_app(args[0]);
unsigned num_indices = store_expr1->get_num_args();
SASSERT(num_indices >= 3);
parameter p = f->get_parameter(0);
func_decl* d = to_func_decl(p.get_ast());
ptr_vector<expr> arrays;
ptr_vector<expr> values;
for (unsigned i = 0; i < num_args; ++i) {
arrays.push_back(to_app(args[i])->get_arg(0));
values.push_back(to_app(args[i])->get_arg(num_indices-1));
}
expr_ref r1(m_manager), r2(m_manager);
reduce(f, arrays.size(), arrays.c_ptr(), r1);
m_simplifier.mk_app(d, values.size(), values.c_ptr(), r2);
ptr_vector<expr> new_args;
new_args.push_back(r1);
for (unsigned i = 1; i + 1 < num_indices; ++i) {
new_args.push_back(store_expr1->get_arg(i));
}
new_args.push_back(r2);
mk_store(store_expr1->get_decl(), new_args.size(), new_args.c_ptr(), result);
break;
}
//
// map_d (const v) = (const (d v))
//
if (num_args == 1 && is_const_array(args[0])) {
app* const_expr = to_app(args[0]);
SASSERT(const_expr->get_num_args() == 1);
parameter p = f->get_parameter(0);
func_decl* d = to_func_decl(p.get_ast());
expr* v = const_expr->get_arg(0);
expr_ref r1(m_manager);
m_simplifier.mk_app(d, 1, &v, r1);
expr* arg = r1.get();
parameter param(f->get_range());
result = m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, &param, 1, &arg);
break;
}
//
// map_d (const v) (const w) = (const (d v w))
//
if (num_args > 1 && all_const_array(num_args, args)) {
parameter p = f->get_parameter(0);
func_decl* d = to_func_decl(p.get_ast());
ptr_vector<expr> values;
for (unsigned i = 0; i < num_args; ++i) {
values.push_back(to_app(args[i])->get_arg(0));
}
expr_ref r1(m_manager);
m_simplifier.mk_app(d, values.size(), values.c_ptr(), r1);
expr* arg = r1.get();
parameter param(f->get_range());
result = m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, &param, 1, &arg);
break;
}
result = m_manager.mk_app(f, num_args, args);
break;
}
default:
result = m_manager.mk_app(f, num_args, args);
break;
}
TRACE("array_simplifier",
tout << mk_pp(result.get(), m_manager) << "\n";);
return true;
}
bool array_simplifier_plugin::same_store(unsigned num_args, expr* const* args) const {
if (num_args == 0) {
return true;
}
if (!is_store(args[0])) {
return false;
}
SASSERT(to_app(args[0])->get_num_args() >= 3);
unsigned num_indices = to_app(args[0])->get_num_args() - 2;
for (unsigned i = 1; i < num_args; ++i) {
if (!is_store(args[i])) {
return false;
}
for (unsigned j = 1; j < num_indices + 1; ++j) {
if (to_app(args[0])->get_arg(j) != to_app(args[i])->get_arg(j)) {
return false;
}
}
}
return true;
}
bool array_simplifier_plugin::all_const_array(unsigned num_args, expr* const* args) const {
bool is_const = true;
for (unsigned i = 0; is_const && i < num_args; ++i) {
is_const = is_const_array(args[i]);
}
return is_const;
}
bool array_simplifier_plugin::all_values(unsigned num_args, expr* const* args) const {
for (unsigned i = 0; i < num_args; ++i) {
if (!m_manager.is_value(args[i])) {
return false;
}
}
return true;
}
bool array_simplifier_plugin::lex_lt(unsigned num_args, expr* const* args1, expr* const* args2) {
for (unsigned i = 0; i < num_args; ++i) {
TRACE("array_simplifier",
tout << mk_pp(args1[i], m_manager) << "\n";
tout << mk_pp(args2[i], m_manager) << "\n";
tout << args1[i]->get_id() << " " << args2[i]->get_id() << "\n";
);
if (args1[i]->get_id() < args2[i]->get_id()) return true;
if (args1[i]->get_id() > args2[i]->get_id()) return false;
}
return false;
}
void array_simplifier_plugin::get_stores(expr* n, unsigned& arity, expr*& m, ptr_vector<expr*const>& stores) {
while (is_store(n)) {
app* a = to_app(n);
SASSERT(a->get_num_args() > 2);
arity = a->get_num_args()-2;
n = a->get_arg(0);
stores.push_back(a->get_args()+1);
}
m = n;
}
lbool array_simplifier_plugin::eq_default(expr* def, unsigned arity, unsigned num_st, expr*const* const* st) {
for (unsigned i = 0; i < num_st; ++i) {
if (st[i][arity] == def) {
continue;
}
if (m_manager.is_value(st[i][arity]) && m_manager.is_value(def)) {
return l_false;
}
return l_undef;
}
return l_true;
}
bool array_simplifier_plugin::insert_table(expr* def, unsigned arity, unsigned num_st, expr*const* const* st, arg_table& table) {
for (unsigned i = 0; i < num_st; ++i ) {
for (unsigned j = 0; j < arity; ++j) {
if (!m_manager.is_value(st[i][j])) {
return false;
}
}
args_entry e(arity, st[i]);
table.insert_if_not_there(e);
}
return true;
}
lbool array_simplifier_plugin::eq_stores(expr* def, unsigned arity, unsigned num_st1, expr*const* const* st1, unsigned num_st2, expr*const* const* st2) {
if (num_st1 == 0) {
return eq_default(def, arity, num_st2, st2);
}
if (num_st2 == 0) {
return eq_default(def, arity, num_st1, st1);
}
arg_table table1, table2;
if (!insert_table(def, arity, num_st1, st1, table1)) {
return l_undef;
}
if (!insert_table(def, arity, num_st2, st2, table2)) {
return l_undef;
}
arg_table::iterator it = table1.begin();
arg_table::iterator end = table1.end();
for (; it != end; ++it) {
args_entry const & e1 = *it;
args_entry e2;
expr* v1 = e1.m_args[arity];
if (table2.find(e1, e2)) {
expr* v2 = e2.m_args[arity];
if (v1 == v2) {
table2.erase(e1);
continue;
}
if (m_manager.is_value(v1) && m_manager.is_value(v2)) {
return l_false;
}
return l_undef;
}
else if (m_manager.is_value(v1) && m_manager.is_value(def) && v1 != def) {
return l_false;
}
}
it = table2.begin();
end = table2.end();
for (; it != end; ++it) {
args_entry const & e = *it;
expr* v = e.m_args[arity];
if (m_manager.is_value(v) && m_manager.is_value(def) && v != def) {
return l_false;
}
}
if (!table2.empty() || !table1.empty()) {
return l_undef;
}
return l_true;
}
bool array_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) {
set_reduce_invoked();
expr* c1, *c2;
ptr_vector<expr*const> st1, st2;
unsigned arity = 0;
get_stores(lhs, arity, c1, st1);
get_stores(rhs, arity, c2, st2);
if (is_const_array(c1) && is_const_array(c2)) {
c1 = to_app(c1)->get_arg(0);
c2 = to_app(c2)->get_arg(0);
if (c1 == c2) {
lbool eq = eq_stores(c1, arity, st1.size(), st1.c_ptr(), st2.size(), st2.c_ptr());
TRACE("array_simplifier",
tout << mk_pp(lhs, m_manager) << " = "
<< mk_pp(rhs, m_manager) << " := " << eq << "\n";);
switch(eq) {
case l_false:
result = m_manager.mk_false();
return true;
case l_true:
result = m_manager.mk_true();
return true;
default:
return false;
}
}
else if (m_manager.is_value(c1) && m_manager.is_value(c2)) {
result = m_manager.mk_false();
return true;
}
}
return false;
}
bool array_simplifier_plugin::reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result) {
set_reduce_invoked();
return false;
}
array_simplifier_plugin::const_select_result
array_simplifier_plugin::mk_select_const(expr* m, app* index, expr_ref& result) {
store_info* info = 0;
expr* r = 0, *a = 0;
if (!is_store(m)) {
return NOT_CACHED;
}
if (!m_store_cache.find(m, info)) {
return NOT_CACHED;
}
if (info->m_map.find(index, r)) {
result = r;
return FOUND_VALUE;
}
a = info->m_default.get();
//
// Unfold and cache the store while searching for value of index.
//
while (is_store(a) && m_manager.is_value(to_app(a)->get_arg(1))) {
app* b = to_app(a);
app* c = to_app(b->get_arg(1));
if (!info->m_map.contains(c)) {
info->m_map.insert(c, b->get_arg(2));
m_manager.inc_ref(b->get_arg(2));
++m_store_cache_size;
}
a = b->get_arg(0);
info->m_default = a;
if (c == index) {
result = b->get_arg(2);
return FOUND_VALUE;
}
}
result = info->m_default.get();
return FOUND_DEFAULT;
}
void array_simplifier_plugin::cache_store(unsigned num_stores, expr* store_term)
{
if (num_stores <= m_const_store_threshold) {
return;
}
prune_store_cache();
if (!m_store_cache.contains(store_term)) {
store_info * info = alloc(store_info, m_manager, store_term);
m_manager.inc_ref(store_term);
m_store_cache.insert(store_term, info);
TRACE("cache_store", tout << m_store_cache.size() << "\n";);
++m_store_cache_size;
}
}
void array_simplifier_plugin::cache_select(unsigned num_args, expr * const * args, expr * result) {
ptr_vector<expr> * entry = alloc(ptr_vector<expr>);
entry->append(num_args, const_cast<expr**>(args));
const select_cache::key_data & kd = m_select_cache.insert_if_not_there(entry, result);
if (kd.m_key != entry) {
dealloc(entry);
return;
}
m_manager.inc_array_ref(num_args, args);
m_manager.inc_ref(result);
TRACE("cache_select", tout << m_select_cache.size() << "\n";);
}
void array_simplifier_plugin::prune_select_cache() {
if (m_select_cache.size() > m_select_cache_max_size) {
flush_select_cache();
}
}
void array_simplifier_plugin::prune_store_cache() {
if (m_store_cache_size > m_store_cache_max_size) {
flush_store_cache();
}
}
void array_simplifier_plugin::flush_select_cache() {
select_cache::iterator it = m_select_cache.begin();
select_cache::iterator end = m_select_cache.end();
for (; it != end; ++it) {
ptr_vector<expr> * e = (*it).m_key;
m_manager.dec_array_ref(e->size(), e->begin());
m_manager.dec_ref((*it).m_value);
dealloc(e);
}
m_select_cache.reset();
}
void array_simplifier_plugin::flush_store_cache() {
store_cache::iterator it = m_store_cache.begin();
store_cache::iterator end = m_store_cache.end();
for (; it != end; ++it) {
m_manager.dec_ref((*it).m_key);
const_map::iterator mit = (*it).m_value->m_map.begin();
const_map::iterator mend = (*it).m_value->m_map.end();
for (; mit != mend; ++mit) {
m_manager.dec_ref((*mit).m_value);
}
dealloc((*it).m_value);
}
m_store_cache.reset();
m_store_cache_size = 0;
}
void array_simplifier_plugin::flush_caches() {
flush_select_cache();
flush_store_cache();
}
void array_simplifier_plugin::mk_set_difference(unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(num_args == 2);
result = m_manager.mk_app(m_fid, OP_SET_DIFFERENCE, 0, 0, num_args, args);
}
void array_simplifier_plugin::mk_empty_set(sort* ty, expr_ref & result) {
parameter param(ty);
expr* args[1] = { m_manager.mk_false() };
result = m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, &param, 1, args);
}
void array_simplifier_plugin::mk_full_set(sort* ty, expr_ref & result) {
parameter param(ty);
expr* args[1] = { m_manager.mk_true() };
result = m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, &param, 1, args);
}
bool array_simplifier_plugin::same_args(unsigned num_args, expr * const * args1, expr * const * args2) {
for (unsigned i = 0; i < num_args; ++i) {
if (args1[i] != args2[i]) {
return false;
}
}
return true;
}
void array_simplifier_plugin::mk_store(func_decl* f, unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(num_args >= 3);
expr* arg0 = args[0];
expr* argn = args[num_args-1];
//
// store(store(a,i,v),i,w) = store(a,i,w)
//
if (is_store(arg0) &&
same_args(num_args-2, args+1, to_app(arg0)->get_args()+1)) {
expr_ref_buffer new_args(m_manager);
new_args.push_back(to_app(arg0)->get_arg(0));
for (unsigned i = 1; i < num_args; ++i) {
new_args.push_back(args[i]);
}
reduce(f, num_args, new_args.c_ptr(), result);
TRACE("array_simplifier", tout << mk_pp(result.get(), m_manager) << "\n";);
return;
}
//
// store(const(v),i,v) = const(v)
//
if (is_const_array(arg0) &&
to_app(arg0)->get_arg(0) == args[num_args-1]) {
result = arg0;
TRACE("array_simplifier", tout << mk_pp(result.get(), m_manager) << "\n";);
return;
}
//
// store(a, i, select(a, i)) = a
//
if (is_select(argn) &&
(to_app(argn)->get_num_args() == num_args - 1) &&
same_args(num_args-1, args, to_app(argn)->get_args())) {
TRACE("dummy_store", tout << "dummy store simplified mk_store(\n";
for (unsigned i = 0; i < num_args; i++) ast_ll_pp(tout, m_manager, args[i]);
tout << ") =====>\n";
ast_ll_pp(tout, m_manager, arg0););
result = arg0;
TRACE("array_simplifier", tout << mk_pp(result.get(), m_manager) << "\n";);
return;
}
//
// store(store(a,i,v),j,w) -> store(store(a,j,w),i,v)
// if i, j are values, i->get_id() < j->get_id()
//
if (m_params.m_array_canonize_simplify &&
is_store(arg0) &&
all_values(num_args-2, args+1) &&
all_values(num_args-2, to_app(arg0)->get_args()+1) &&
lex_lt(num_args-2, args+1, to_app(arg0)->get_args()+1)) {
expr* const* args2 = to_app(arg0)->get_args();
expr_ref_buffer new_args(m_manager);
new_args.push_back(args2[0]);
for (unsigned i = 1; i < num_args; ++i) {
new_args.push_back(args[i]);
}
reduce(f, num_args, new_args.c_ptr(), result);
new_args.reset();
new_args.push_back(result);
for (unsigned i = 1; i < num_args; ++i) {
new_args.push_back(args2[i]);
}
result = m_manager.mk_app(m_fid, OP_STORE, num_args, new_args.c_ptr());
TRACE("array_simplifier", tout << mk_pp(result.get(), m_manager) << "\n";);
return;
}
result = m_manager.mk_app(m_fid, OP_STORE, num_args, args);
TRACE("array_simplifier", tout << "default: " << mk_pp(result.get(), m_manager) << "\n";);
}
void array_simplifier_plugin::mk_select_as_array(unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(is_as_array(args[0]));
func_decl * f = get_as_array_func_decl(to_app(args[0]));
result = m_manager.mk_app(f, num_args - 1, args+1);
}
void array_simplifier_plugin::mk_select_as_array_tree(unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(is_as_array_tree(args[0]));
SASSERT(m_manager.is_ite(args[0]));
ptr_buffer<app, 32> todo;
obj_map<app, app *> cache;
app_ref_buffer trail(m_manager);
todo.push_back(to_app(args[0]));
while (!todo.empty()) {
app * curr = todo.back();
SASSERT(m_manager.is_ite(curr));
expr * branches[2] = {0, 0};
bool visited = true;
for (unsigned i = 0; i < 2; i++) {
expr * arg = curr->get_arg(i+1);
if (is_as_array(arg)) {
branches[i] = m_manager.mk_app(get_as_array_func_decl(to_app(arg)), num_args - 1, args+1);
}
else {
SASSERT(m_manager.is_ite(arg));
app * new_arg = 0;
if (!cache.find(to_app(arg), new_arg)) {
todo.push_back(to_app(arg));
visited = false;
}
else {
branches[i] = new_arg;
}
}
}
if (visited) {
todo.pop_back();
app * new_curr = m_manager.mk_ite(curr->get_arg(0), branches[0], branches[1]);
trail.push_back(new_curr);
cache.insert(curr, new_curr);
}
}
SASSERT(cache.contains(to_app(args[0])));
app * r = 0;
cache.find(to_app(args[0]), r);
result = r;
}
void array_simplifier_plugin::mk_select(unsigned num_args, expr * const * args, expr_ref & result) {
expr * r = 0;
if (is_as_array(args[0])) {
mk_select_as_array(num_args, args, result);
return;
}
if (is_as_array_tree(args[0])) {
mk_select_as_array_tree(num_args, args, result);
return;
}
bool is_const_select = num_args == 2 && m_manager.is_value(args[1]);
app* const_index = is_const_select?to_app(args[1]):0;
unsigned num_const_stores = 0;
expr_ref tmp(m_manager);
expr* args2[2];
if (is_const_select) {
switch(mk_select_const(args[0], const_index, tmp)) {
case NOT_CACHED:
break;
case FOUND_VALUE:
TRACE("mk_select", tout << "found value\n"; ast_ll_pp(tout, m_manager, tmp.get()); );
result = tmp.get();
// value of select is stored under result.
return;
case FOUND_DEFAULT:
args2[0] = tmp.get();
args2[1] = args[1];
args = args2;
is_const_select = false;
break;
}
}
SASSERT(num_args > 0);
ptr_vector<expr> & entry = m_tmp2;
entry.reset();
entry.append(num_args, args);
expr * entry0 = entry[0];
SASSERT(m_todo.empty());
m_todo.push_back(entry0);
while (!m_todo.empty()) {
expr * m = m_todo.back();
TRACE("array_simplifier", tout << mk_bounded_pp(m, m_manager) << "\n";);
if (is_store(m)) {
expr * nested_array = to_app(m)->get_arg(0);
expr * else_branch = 0;
entry[0] = nested_array;
if (is_const_select) {
if (m_manager.is_value(to_app(m)->get_arg(1))) {
app* const_index2 = to_app(to_app(m)->get_arg(1));
//
// we found the value, all other stores are different.
// there is no need to recurse.
//
if (const_index == const_index2) {
result = to_app(m)->get_arg(2);
cache_store(num_const_stores, args[0]);
m_todo.reset();
return;
}
++num_const_stores;
}
else {
is_const_select = false;
}
}
if (m_select_cache.find(&entry, else_branch)) {
expr_ref_buffer eqs(m_manager);
for (unsigned i = 1; i < num_args ; ++i) {
expr * a = args[i];
expr * b = to_app(m)->get_arg(i);
expr_ref eq(m_manager);
m_simp.mk_eq(a, b, eq);
eqs.push_back(eq.get());
}
expr_ref cond(m_manager);
m_simp.mk_and(eqs.size(), eqs.c_ptr(), cond);
expr * then_branch = to_app(m)->get_arg(num_args);
if (m_manager.is_true(cond.get())) {
result = then_branch;
}
else if (m_manager.is_false(cond.get())) {
result = else_branch;
}
else {
m_simp.mk_ite(cond.get(), then_branch, else_branch, result);
}
entry[0] = m;
cache_select(entry.size(), entry.c_ptr(), result.get());
m_todo.pop_back();
}
else {
m_todo.push_back(nested_array);
}
}
else if (is_const_array(m)) {
entry[0] = m;
cache_select(entry.size(), entry.c_ptr(), to_app(m)->get_arg(0));
m_todo.pop_back();
}
else {
entry[0] = m;
TRACE("array_simplifier", {
for (unsigned i = 0; i < entry.size(); ++i) {
tout << mk_bounded_pp(entry[i], m_manager) << ": "
<< mk_bounded_pp(m_manager.get_sort(entry[i]), m_manager) << "\n";
}}
);
r = m_manager.mk_app(m_fid, OP_SELECT, 0, 0, entry.size(), entry.c_ptr());
cache_select(entry.size(), entry.c_ptr(), r);
m_todo.pop_back();
}
}
cache_store(num_const_stores, args[0]);
entry[0] = entry0;
#ifdef Z3DEBUG
bool f =
#endif
m_select_cache.find(&entry, r);
SASSERT(f);
result = r;
prune_select_cache();
prune_store_cache();
TRACE("mk_select",
for (unsigned i = 0; i < num_args; i++) {
ast_ll_pp(tout, m_manager, args[i]); tout << "\n";
};
tout << "is_store: " << is_store(args[0]) << "\n";
ast_ll_pp(tout, m_manager, r););
}
void array_simplifier_plugin::mk_map(func_decl* f, expr* a, expr* b, expr_ref& result) {
expr* exprs[2] = { a, b };
parameter param(f);
result = m_manager.mk_app(m_fid, OP_ARRAY_MAP, 1, &param, 2, exprs );
}
void array_simplifier_plugin::mk_map(func_decl* f, expr* a, expr_ref& result) {
parameter param(f);
result = m_manager.mk_app(m_fid, OP_ARRAY_MAP, 1, &param, 1, &a );
}

154
lib/array_simplifier_plugin.h
View file

@ -1,154 +0,0 @@
/*++
Copyright (c) 2008 Microsoft Corporation
Module Name:
array_simplifier_plugin.h
Abstract:
<abstract>
Author:
Nikolaj Bjorner (nbjorner) 2008-05-05
Revision History:
--*/
#ifndef _ARRAY_SIMPLIFIER_PLUGIN_H_
#define _ARRAY_SIMPLIFIER_PLUGIN_H_
#include"ast.h"
#include"map.h"
#include"array_decl_plugin.h"
#include"simplifier_plugin.h"
#include"basic_simplifier_plugin.h"
#include"theory_array_params.h"
#include"simplifier.h"
#include"obj_hashtable.h"
#include"lbool.h"
class array_simplifier_plugin : public simplifier_plugin {
typedef ptr_vector<expr> entry;
struct entry_hash_proc {
unsigned operator()(ptr_vector<expr> * entry) const {
return get_exprs_hash(entry->size(), entry->begin(), 0xbeef1010);
}
};
struct entry_eq_proc {
bool operator()(ptr_vector<expr> * entry1, ptr_vector<expr> * entry2) const {
if (entry1->size() != entry2->size()) return false;
return compare_arrays(entry1->begin(), entry2->begin(), entry1->size());
}
};
typedef map<entry *, expr *, entry_hash_proc, entry_eq_proc> select_cache;
struct args_entry {
unsigned m_arity;
expr* const* m_args;
args_entry(unsigned a, expr* const* args) : m_arity(a), m_args(args) {}
args_entry() : m_arity(0), m_args(0) {}
};
struct args_entry_hash_proc {
unsigned operator()(args_entry const& e) const {
return get_exprs_hash(e.m_arity, e.m_args, 0xbeef1010);
}
};
struct args_entry_eq_proc {
bool operator()(args_entry const& e1, args_entry const& e2) const {
if (e1.m_arity != e2.m_arity) return false;
return compare_arrays(e1.m_args, e2.m_args, e1.m_arity);
}
};
typedef hashtable<args_entry, args_entry_hash_proc, args_entry_eq_proc> arg_table;
array_util m_util;
basic_simplifier_plugin& m_simp;
simplifier& m_simplifier;
theory_array_params const& m_params;
select_cache m_select_cache;
ptr_vector<expr> m_tmp;
ptr_vector<expr> m_tmp2;
ptr_vector<expr> m_todo;
static const unsigned m_select_cache_max_size = 100000;
typedef obj_map<expr, expr*> const_map;
class store_info {
store_info();
store_info(store_info const&);
public:
const_map m_map;
expr_ref m_default;
store_info(ast_manager& m, expr* d): m_default(d, m) {}
};
typedef obj_map<expr, store_info*> store_cache;
store_cache m_store_cache;
unsigned m_store_cache_size;
static const unsigned m_store_cache_max_size = 10000;
static const unsigned m_const_store_threshold = 5;
enum const_select_result {
NOT_CACHED,
FOUND_DEFAULT,
FOUND_VALUE
};
public:
array_simplifier_plugin(ast_manager & m, basic_simplifier_plugin& s, simplifier& simp, theory_array_params const& p);
virtual ~array_simplifier_plugin();
virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result);
virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result);
virtual void flush_caches();
private:
bool is_select(expr* n) const { return m_util.is_select(n); }
bool is_store(expr * n) const { return m_util.is_store(n); }
bool is_const_array(expr * n) const { return m_util.is_const(n); }
bool is_as_array(expr * n) const { return m_util.is_as_array(n); }
bool is_as_array_tree(expr * n) { return m_util.is_as_array_tree(n); }
func_decl * get_as_array_func_decl(app * n) const { return m_util.get_as_array_func_decl(n); }
void mk_select_as_array(unsigned num_args, expr * const * args, expr_ref & result);
void mk_select_as_array_tree(unsigned num_args, expr * const * args, expr_ref & result);
bool is_enumerated(expr* n, expr_ref& c, ptr_vector<expr>& keys, ptr_vector<expr>& vals);
const_select_result mk_select_const(expr* m, app* index, expr_ref& result);
void cache_store(unsigned num_stores, expr* nested_store);
void cache_select(unsigned num_args, expr * const * args, expr * result);
void prune_select_cache();
void prune_store_cache();
void flush_select_cache();
void flush_store_cache();
void mk_set_difference(unsigned num_args, expr * const * args, expr_ref & result);
void mk_empty_set(sort* ty, expr_ref & result);
void mk_full_set(sort* ty, expr_ref & result);
void mk_select(unsigned num_args, expr * const * args, expr_ref & result);
void mk_store(func_decl* f, unsigned num_args, expr * const * args, expr_ref & result);
void mk_map(func_decl* f, expr* a, expr* b, expr_ref & result);
void mk_map(func_decl* f, expr* a, expr_ref & result);
bool same_args(unsigned num_args, expr * const * args1, expr * const * args2);
void get_stores(expr* n, unsigned& arity, expr*& m, ptr_vector<expr*const>& stores);
lbool eq_default(expr* def, unsigned arity, unsigned num_st, expr*const* const* st);
bool insert_table(expr* def, unsigned arity, unsigned num_st, expr*const* const* st, arg_table& table);
lbool eq_stores(expr* def, unsigned arity, unsigned num_st1, expr*const* const* st1, unsigned num_st2, expr*const* const* st2);
bool same_store(unsigned num_args, expr* const* args) const;
bool all_const_array(unsigned num_args, expr* const* args) const;
bool all_values(unsigned num_args, expr* const* args) const;
bool lex_lt(unsigned num_args, expr* const* args1, expr* const* args2);
};
#endif /* _ARRAY_SIMPLIFIER_PLUGIN_H_ */

215
lib/datatype_factory.cpp
View file

@ -1,215 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
datatype_factory.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-11-06.
Revision History:
--*/
#include"datatype_factory.h"
#include"proto_model.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
datatype_factory::datatype_factory(ast_manager & m, proto_model & md):
struct_factory(m, m.get_family_id("datatype"), md),
m_util(m) {
}
expr * datatype_factory::get_some_value(sort * s) {
value_set * set = 0;
if (m_sort2value_set.find(s, set) && !set->empty())
return *(set->begin());
func_decl * c = m_util.get_non_rec_constructor(s);
ptr_vector<expr> args;
unsigned num = c->get_arity();
for (unsigned i = 0; i < num; i++) {
args.push_back(m_model.get_some_value(c->get_domain(i)));
}
expr * r = m_manager.mk_app(c, args.size(), args.c_ptr());
register_value(r);
TRACE("datatype_factory", tout << mk_pp(r, m_util.get_manager()) << "\n";);
return r;
}
/**
\brief Return the last fresh (or almost) fresh value of sort s.
*/
expr * datatype_factory::get_last_fresh_value(sort * s) {
expr * val = 0;
if (m_last_fresh_value.find(s, val))
return val;
value_set * set = get_value_set(s);
if (set->empty())
val = get_some_value(s);
else
val = *(set->begin());
if (m_util.is_recursive(s))
m_last_fresh_value.insert(s, val);
return val;
}
/**
\brief Create an almost fresh value. If s is recursive, then the result is not 0.
It also updates m_last_fresh_value
*/
expr * datatype_factory::get_almost_fresh_value(sort * s) {
value_set * set = get_value_set(s);
if (set->empty()) {
expr * val = get_some_value(s);
if (m_util.is_recursive(s))
m_last_fresh_value.insert(s, val);
return val;
}
// Traverse constructors, and try to invoke get_fresh_value of one of the arguments (if the argument is not a sibling datatype of s).
// If the argumet is a sibling datatype of s, then
// use get_last_fresh_value.
ptr_vector<func_decl> const * constructors = m_util.get_datatype_constructors(s);
ptr_vector<func_decl>::const_iterator it = constructors->begin();
ptr_vector<func_decl>::const_iterator end = constructors->end();
for (; it != end; ++it) {
func_decl * constructor = *it;
expr_ref_vector args(m_manager);
bool found_fresh_arg = false;
bool recursive = false;
unsigned num = constructor->get_arity();
for (unsigned i = 0; i < num; i++) {
sort * s_arg = constructor->get_domain(i);
if (!found_fresh_arg && (!m_util.is_datatype(s_arg) || !m_util.are_siblings(s, s_arg))) {
expr * new_arg = m_model.get_fresh_value(s_arg);
if (new_arg != 0) {
found_fresh_arg = true;
args.push_back(new_arg);
continue;
}
}
if (!found_fresh_arg && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) {
recursive = true;
expr * last_fresh = get_last_fresh_value(s_arg);
args.push_back(last_fresh);
}
else {
expr * some_arg = m_model.get_some_value(s_arg);
args.push_back(some_arg);
}
}
if (recursive || found_fresh_arg) {
expr * new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
SASSERT(!found_fresh_arg || !set->contains(new_value));
register_value(new_value);
if (m_util.is_recursive(s))
m_last_fresh_value.insert(s, new_value);
return new_value;
}
}
SASSERT(!m_util.is_recursive(s));
return 0;
}
expr * datatype_factory::get_fresh_value(sort * s) {
TRACE("datatype_factory", tout << "generating fresh value for: " << s->get_name() << "\n";);
value_set * set = get_value_set(s);
// Approach 0)
// if no value for s was generated so far, then used get_some_value
if (set->empty()) {
expr * val = get_some_value(s);
if (m_util.is_recursive(s))
m_last_fresh_value.insert(s, val);
TRACE("datatype_factory", tout << "0. result: " << mk_pp(val, m_manager) << "\n";);
return val;
}
// Approach 1)
// Traverse constructors, and try to invoke get_fresh_value of one of the
// arguments (if the argument is not a sibling datatype of s).
// Two datatypes are siblings if they were defined together in the same mutually recursive definition.
ptr_vector<func_decl> const * constructors = m_util.get_datatype_constructors(s);
ptr_vector<func_decl>::const_iterator it = constructors->begin();
ptr_vector<func_decl>::const_iterator end = constructors->end();
for (; it != end; ++it) {
func_decl * constructor = *it;
expr_ref_vector args(m_manager);
bool found_fresh_arg = false;
unsigned num = constructor->get_arity();
for (unsigned i = 0; i < num; i++) {
sort * s_arg = constructor->get_domain(i);
if (!found_fresh_arg && (!m_util.is_recursive(s) || !m_util.is_datatype(s_arg) || !m_util.are_siblings(s, s_arg))) {
expr * new_arg = m_model.get_fresh_value(s_arg);
if (new_arg != 0) {
found_fresh_arg = true;
args.push_back(new_arg);
continue;
}
}
expr * some_arg = m_model.get_some_value(s_arg);
args.push_back(some_arg);
}
expr_ref new_value(m_manager);
new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
CTRACE("datatype_factory", found_fresh_arg && set->contains(new_value), tout << mk_pp(new_value, m_manager) << "\n";);
SASSERT(!found_fresh_arg || !set->contains(new_value));
if (!set->contains(new_value)) {
register_value(new_value);
if (m_util.is_recursive(s))
m_last_fresh_value.insert(s, new_value);
TRACE("datatype_factory", tout << "1. result: " << mk_pp(new_value, m_manager) << "\n";);
return new_value;
}
}
// Approach 2)
// For recursive datatypes.
// search for constructor...
if (m_util.is_recursive(s)) {
while(true) {
TRACE("datatype_factory", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";);
ptr_vector<func_decl> const * constructors = m_util.get_datatype_constructors(s);
ptr_vector<func_decl>::const_iterator it = constructors->begin();
ptr_vector<func_decl>::const_iterator end = constructors->end();
for (; it != end; ++it) {
func_decl * constructor = *it;
expr_ref_vector args(m_manager);
bool found_sibling = false;
unsigned num = constructor->get_arity();
for (unsigned i = 0; i < num; i++) {
sort * s_arg = constructor->get_domain(i);
if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) {
found_sibling = true;
expr * maybe_new_arg = get_almost_fresh_value(s_arg);
args.push_back(maybe_new_arg);
}
else {
expr * some_arg = m_model.get_some_value(s_arg);
args.push_back(some_arg);
}
}
if (found_sibling) {
expr_ref new_value(m_manager);
new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
m_last_fresh_value.insert(s, new_value);
if (!set->contains(new_value)) {
register_value(new_value);
TRACE("datatype_factory", tout << "2. result: " << mk_pp(new_value, m_manager) << "\n";);
return new_value;
}
}
}
}
}
// Approach 3)
// for non-recursive datatypes.
// Search for value that was not created before.
SASSERT(!m_util.is_recursive(s));
return 0;
}

40
lib/datatype_factory.h
View file

@ -1,40 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
datatype_factory.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-11-06.
Revision History:
--*/
#ifndef _DATATYPE_FACTORY_H_
#define _DATATYPE_FACTORY_H_
#include"struct_factory.h"
#include"datatype_decl_plugin.h"
class datatype_factory : public struct_factory {
datatype_util m_util;
obj_map<sort, expr *> m_last_fresh_value;
expr * get_last_fresh_value(sort * s);
expr * get_almost_fresh_value(sort * s);
public:
datatype_factory(ast_manager & m, proto_model & md);
virtual ~datatype_factory() {}
virtual expr * get_some_value(sort * s);
virtual expr * get_fresh_value(sort * s);
};
#endif /* _DATATYPE_FACTORY_H_ */

52
lib/numeral_factory.cpp
View file

@ -1,52 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
numeral_factory.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-10-28.
Revision History:
--*/
#include"numeral_factory.h"
#include"ast_pp.h"
app * arith_factory::mk_value_core(rational const & val, sort * s) {
return m_util.mk_numeral(val, s);
}
arith_factory::arith_factory(ast_manager & m):
numeral_factory(m, m.get_family_id("arith")),
m_util(m) {
}
arith_factory::~arith_factory() {
}
app * arith_factory::mk_value(rational const & val, bool is_int) {
return numeral_factory::mk_value(val, is_int ? m_util.mk_int() : m_util.mk_real());
}
bv_factory::bv_factory(ast_manager & m):
numeral_factory(m, m.get_family_id("bv")),
m_util(m) {
}
bv_factory::~bv_factory() {
}
app * bv_factory::mk_value_core(rational const & val, sort * s) {
return m_util.mk_numeral(val, s);
}
app * bv_factory::mk_value(rational const & val, unsigned bv_size) {
return numeral_factory::mk_value(val, m_util.mk_sort(bv_size));
}

57
lib/numeral_factory.h
View file

@ -1,57 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
numeral_factory.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-10-28.
Revision History:
--*/
#ifndef _NUMERAL_FACTORY_H_
#define _NUMERAL_FACTORY_H_
#include"value_factory.h"
#include"arith_decl_plugin.h"
#include"bv_decl_plugin.h"
class numeral_factory : public simple_factory<rational> {
public:
numeral_factory(ast_manager & m, family_id fid):simple_factory<rational>(m, fid) {}
virtual ~numeral_factory() {}
};
class arith_factory : public numeral_factory {
arith_util m_util;
virtual app * mk_value_core(rational const & val, sort * s);
public:
arith_factory(ast_manager & m);
virtual ~arith_factory();
app * mk_value(rational const & val, bool is_int);
};
class bv_factory : public numeral_factory {
bv_util m_util;
virtual app * mk_value_core(rational const & val, sort * s);
public:
bv_factory(ast_manager & m);
virtual ~bv_factory();
app * mk_value(rational const & val, unsigned bv_size);
};
#endif /* _NUMERAL_FACTORY_H_ */

78
lib/struct_factory.cpp
View file

@ -1,78 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
struct_factory.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-11-06.
Revision History:
--*/
#include"struct_factory.h"
#include"proto_model.h"
struct_factory::value_set * struct_factory::get_value_set(sort * s) {
value_set * set = 0;
if (!m_sort2value_set.find(s, set)) {
set = alloc(value_set);
m_sort2value_set.insert(s, set);
m_sorts.push_back(s);
m_sets.push_back(set);
}
SASSERT(set != 0);
return set;
}
struct_factory::struct_factory(ast_manager & m, family_id fid, proto_model & md):
value_factory(m, fid),
m_model(md),
m_values(m),
m_sorts(m) {
}
struct_factory::~struct_factory() {
std::for_each(m_sets.begin(), m_sets.end(), delete_proc<value_set>());
}
void struct_factory::register_value(expr * new_value) {
sort * s = m_manager.get_sort(new_value);
value_set * set = get_value_set(s);
if (!set->contains(new_value)) {
m_values.push_back(new_value);
set->insert(new_value);
}
}
bool struct_factory::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
value_set * set = get_value_set(s);
switch (set->size()) {
case 0:
v1 = get_fresh_value(s);
v2 = get_fresh_value(s);
return v1 != 0 && v2 != 0;
case 1:
v1 = get_some_value(s);
v2 = get_fresh_value(s);
return v2 != 0;
default:
obj_hashtable<expr>::iterator it = set->begin();
v1 = *it;
++it;
v2 = *it;
return true;
}
}

56
lib/struct_factory.h
View file

@ -1,56 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
struct_factory.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-11-06.
Revision History:
--*/
#ifndef _STRUCT_FACTORY_H_
#define _STRUCT_FACTORY_H_
#include"value_factory.h"
#include"obj_hashtable.h"
class proto_model;
/**
\brief Abstract factory for structured values such as: arrays and algebraic datatypes.
*/
class struct_factory : public value_factory {
protected:
typedef obj_hashtable<expr> value_set;
typedef obj_map<sort, value_set *> sort2value_set;
proto_model & m_model;
sort2value_set m_sort2value_set;
expr_ref_vector m_values;
sort_ref_vector m_sorts;
ptr_vector<value_set> m_sets;
value_set * get_value_set(sort * s);
public:
struct_factory(ast_manager & m, family_id fid, proto_model & md);
virtual ~struct_factory();
virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2);
virtual void register_value(expr * array_value);
proto_model & get_model() { return m_model; }
};
#endif /* _STRUCT_FACTORY_H_ */