mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

isolated proto_model obsolete code

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-29 20:15:33 -07:00
parent 24efe18d3f
commit 759504880a
17 changed files with 68 additions and 78 deletions
Download patch file Download diff file Expand all files Collapse all files

206
src/model/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
src/model/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_ */

215
src/model/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
src/model/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_ */

67
src/model/func_interp.cpp
View file

@ -16,8 +16,6 @@ Revision History:
--*/
#include"func_interp.h"
#include"simplifier.h"
#include"basic_simplifier_plugin.h"
#include"var_subst.h"
#include"obj_hashtable.h"
#include"ast_pp.h"
@ -182,71 +180,6 @@ bool func_interp::eval_else(expr * const * args, expr_ref & result) const {
return true;
}
/**
\brief Store in r the result of applying args to this function.
Return true in case of success.
The function may fail if m_else == 0.
*/
bool func_interp::eval(simplifier & s, expr * const * args, expr_ref & result) {
bool actuals_are_values = true;
if (!m_entries.empty()) {
for (unsigned i = 0; actuals_are_values && i < m_arity; i++) {
actuals_are_values = m_manager.is_value(args[i]);
}
}
func_entry * entry = get_entry(args);
if (entry != 0) {
result = entry->get_result();
TRACE("func_interp", tout << "found entry for: ";
for(unsigned i = 0; i < m_arity; i++)
tout << mk_pp(args[i], m_manager) << " ";
tout << "\nresult: " << mk_pp(result, m_manager) << "\n";);
return true;
}
TRACE("func_interp", tout << "failed to find entry for: ";
for(unsigned i = 0; i < m_arity; i++)
tout << mk_pp(args[i], m_manager) << " ";
tout << "\nis partial: " << is_partial() << "\n";);
if (!eval_else(args, result)) {
TRACE("func_interp", tout << "function is partial, failed to evaluate\n";);
return false;
}
if (actuals_are_values && m_args_are_values) {
// cheap case... we are done
return true;
}
// build symbolic result... the actuals may be equal to the args of one of the entries.
basic_simplifier_plugin * bs = static_cast<basic_simplifier_plugin*>(s.get_plugin(m_manager.get_basic_family_id()));
ptr_vector<func_entry>::iterator it = m_entries.begin();
ptr_vector<func_entry>::iterator end = m_entries.end();
for (; it != end; ++it) {
func_entry * curr = *it;
SASSERT(!curr->eq_args(m_arity, args));
if (!actuals_are_values || !curr->args_are_values()) {
expr_ref_buffer eqs(m_manager);
unsigned i = m_arity;
while (i > 0) {
--i;
expr_ref new_eq(m_manager);
bs->mk_eq(curr->get_arg(i), args[i], new_eq);
eqs.push_back(new_eq);
}
SASSERT(eqs.size() == m_arity);
expr_ref new_cond(m_manager);
bs->mk_and(eqs.size(), eqs.c_ptr(), new_cond);
bs->mk_ite(new_cond, curr->get_result(), result, result);
}
}
return true;
}
/**
\brief Return the result with the maximal number of occurrencies in m_entries.
*/

9
src/model/func_interp.h
View file

@ -34,7 +34,6 @@ Revision History:
#include"ast_translation.h"
class func_interp;
class simplifier;
class func_entry {
bool m_args_are_values; //!< true if is_value(m_args[i]) is true for all i in [0, arity)
@ -50,10 +49,10 @@ class func_entry {
friend class func_interp;
void set_result(ast_manager & m, expr * r);
bool args_are_values() const { return m_args_are_values; }
public:
static func_entry * mk(ast_manager & m, unsigned arity, expr * const * args, expr * result);
bool args_are_values() const { return m_args_are_values; }
void deallocate(ast_manager & m, unsigned arity);
expr * get_result() const { return m_result; }
expr * get_arg(unsigned idx) const { return m_args[idx]; }
@ -81,6 +80,8 @@ public:
func_interp(ast_manager & m, unsigned arity);
~func_interp();
ast_manager & m () const { return m_manager; }
func_interp * copy() const;
unsigned get_arity() const { return m_arity; }
@ -88,8 +89,9 @@ public:
bool is_partial() const { return m_else == 0; }
// A function interpretation is said to be simple if m_else is ground.
bool is_simple() const { return is_partial() || is_ground(m_else); }
bool is_constant() const;
// Return true if all arguments of the function graph are values.
bool args_are_values() const { return m_args_are_values; }
expr * get_else() const { return m_else; }
void set_else(expr * e);
@ -98,7 +100,6 @@ public:
void insert_new_entry(expr * const * args, expr * r);
func_entry * get_entry(expr * const * args) const;
bool eval_else(expr * const * args, expr_ref & result) const;
bool eval(simplifier & s, expr * const * args, expr_ref & result);
unsigned num_entries() const { return m_entries.size(); }
func_entry const * const * get_entries() const { return m_entries.c_ptr(); }
func_entry const * get_entry(unsigned idx) const { return m_entries[idx]; }

37
src/model/model_params.cpp
View file

@ -1,37 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
model_params.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2007-08-23.
Revision History:
--*/
#include"model_params.h"
void model_params::register_params(ini_params & p) {
p.register_bool_param("MODEL_PARTIAL", m_model_partial, "enable/disable partial function interpretations", true);
p.register_bool_param("MODEL_HIDE_UNUSED_PARTITIONS", m_model_hide_unused_partitions, "hide unused partitions, some partitions are associated with internal terms/formulas created by Z3", true);
p.register_bool_param("MODEL_V1", m_model_v1_pp,
"use Z3 version 1.x pretty printer", true);
p.register_bool_param("MODEL_V2", m_model_v2_pp,
"use Z3 version 2.x (x <= 16) pretty printer", true);
p.register_bool_param("MODEL_COMPACT", m_model_compact,
"try to compact function graph (i.e., function interpretations that are lookup tables", true);
p.register_bool_param("MODEL_COMPLETION", m_model_completion,
"assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model", true);
p.register_bool_param("MODEL_DISPLAY_ARG_SORT", m_model_display_arg_sort,
"display the sort of each argument when printing function interpretations", true);
}

47
src/model/model_params.h
View file

@ -1,47 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
model_params.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2007-08-23.
Revision History:
--*/
#ifndef _MODEL_PARAMS_H_
#define _MODEL_PARAMS_H_
#include"ini_file.h"
struct model_params {
bool m_model_partial;
bool m_model_hide_unused_partitions;
bool m_model_compact;
bool m_model_v1_pp;
bool m_model_v2_pp;
bool m_model_completion;
bool m_model_display_arg_sort;
model_params():
m_model_partial(false),
m_model_hide_unused_partitions(true),
m_model_compact(false),
m_model_v1_pp(false),
m_model_v2_pp(false),
m_model_completion(false),
m_model_display_arg_sort(true) {
}
void register_params(ini_params & p);
};
#endif /* _MODEL_PARAMS_H_ */

52
src/model/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
src/model/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_ */

607
src/model/proto_model.cpp
View file

@ -1,607 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
proto_model.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2007-03-08.
Revision History:
--*/
#include"proto_model.h"
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include"var_subst.h"
#include"array_decl_plugin.h"
#include"well_sorted.h"
#include"used_symbols.h"
#include"model_v2_pp.h"
proto_model::proto_model(ast_manager & m, simplifier & s, model_params const & p):
model_core(m),
m_params(p),
m_asts(m),
m_simplifier(s),
m_afid(m.get_family_id(symbol("array"))) {
register_factory(alloc(basic_factory, m));
m_user_sort_factory = alloc(user_sort_factory, m);
register_factory(m_user_sort_factory);
}
void proto_model::reset_finterp() {
decl2finterp::iterator it = m_finterp.begin();
decl2finterp::iterator end = m_finterp.end();
for (; it != end; ++it) {
dealloc(it->m_value);
}
}
proto_model::~proto_model() {
reset_finterp();
}
void proto_model::register_decl(func_decl * d, expr * v) {
SASSERT(d->get_arity() == 0);
if (m_interp.contains(d)) {
DEBUG_CODE({
expr * old_v = 0;
m_interp.find(d, old_v);
SASSERT(old_v == v);
});
return;
}
SASSERT(!m_interp.contains(d));
m_decls.push_back(d);
m_asts.push_back(d);
m_asts.push_back(v);
m_interp.insert(d, v);
m_const_decls.push_back(d);
}
void proto_model::register_decl(func_decl * d, func_interp * fi, bool aux) {
SASSERT(d->get_arity() > 0);
SASSERT(!m_finterp.contains(d));
m_decls.push_back(d);
m_asts.push_back(d);
m_finterp.insert(d, fi);
m_func_decls.push_back(d);
if (aux)
m_aux_decls.insert(d);
}
/**
\brief Set new_fi as the new interpretation for f.
If f_aux != 0, then assign the old interpretation of f to f_aux.
If f_aux == 0, then delete the old interpretation of f.
f_aux is marked as a auxiliary declaration.
*/
void proto_model::reregister_decl(func_decl * f, func_interp * new_fi, func_decl * f_aux) {
func_interp * fi = get_func_interp(f);
if (fi == 0) {
register_decl(f, new_fi);
}
else {
if (f_aux != 0) {
register_decl(f_aux, fi);
m_aux_decls.insert(f_aux);
}
else {
dealloc(fi);
}
m_finterp.insert(f, new_fi);
}
}
expr * proto_model::mk_some_interp_for(func_decl * d) {
SASSERT(!has_interpretation(d));
expr * r = get_some_value(d->get_range()); // if t is a function, then it will be the constant function.
if (d->get_arity() == 0) {
register_decl(d, r);
}
else {
func_interp * new_fi = alloc(func_interp, m_manager, d->get_arity());
new_fi->set_else(r);
register_decl(d, new_fi);
}
return r;
}
/**
\brief Evaluate the expression e in the current model, and store the result in \c result.
It returns \c true if succeeded, and false otherwise. If the evaluation fails,
then r contains a term that is simplified as much as possible using the interpretations
available in the model.
When model_completion == true, if the model does not assign an interpretation to a
declaration it will build one for it. Moreover, partial functions will also be completed.
So, if model_completion == true, the evaluator never fails if it doesn't contain quantifiers.
*/
bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
bool is_ok = true;
SASSERT(is_well_sorted(m_manager, e));
TRACE("model_eval", tout << mk_pp(e, m_manager) << "\n";
tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";);
obj_map<expr, expr*> eval_cache;
expr_ref_vector trail(m_manager);
sbuffer<std::pair<expr*, expr*>, 128> todo;
ptr_buffer<expr> args;
expr * null = static_cast<expr*>(0);
todo.push_back(std::make_pair(e, null));
expr * a;
expr * expanded_a;
while (!todo.empty()) {
std::pair<expr *, expr *> & p = todo.back();
a = p.first;
expanded_a = p.second;
if (expanded_a != 0) {
expr * r = 0;
eval_cache.find(expanded_a, r);
SASSERT(r != 0);
todo.pop_back();
eval_cache.insert(a, r);
TRACE("model_eval",
tout << "orig:\n" << mk_pp(a, m_manager) << "\n";
tout << "after beta reduction:\n" << mk_pp(expanded_a, m_manager) << "\n";
tout << "new:\n" << mk_pp(r, m_manager) << "\n";);
}
else {
switch(a->get_kind()) {
case AST_APP: {
app * t = to_app(a);
bool visited = true;
args.reset();
unsigned num_args = t->get_num_args();
for (unsigned i = 0; i < num_args; ++i) {
expr * arg = 0;
if (!eval_cache.find(t->get_arg(i), arg)) {
visited = false;
todo.push_back(std::make_pair(t->get_arg(i), null));
}
else {
args.push_back(arg);
}
}
if (!visited) {
continue;
}
SASSERT(args.size() == t->get_num_args());
expr_ref new_t(m_manager);
func_decl * f = t->get_decl();
if (!has_interpretation(f)) {
// the model does not assign an interpretation to f.
SASSERT(new_t.get() == 0);
if (f->get_family_id() == null_family_id) {
if (model_completion) {
// create an interpretation for f.
new_t = mk_some_interp_for(f);
}
else {
is_ok = false;
}
}
if (new_t.get() == 0) {
// t is interpreted or model completion is disabled.
m_simplifier.mk_app(f, num_args, args.c_ptr(), new_t);
trail.push_back(new_t);
if (!is_app(new_t) || to_app(new_t)->get_decl() != f) {
// if the result is not of the form (f ...), then assume we must simplify it.
expr * new_new_t = 0;
if (!eval_cache.find(new_t.get(), new_new_t)) {
todo.back().second = new_t;
todo.push_back(std::make_pair(new_t, null));
continue;
}
else {
new_t = new_new_t;
}
}
}
}
else {
// the model has an interpretaion for f.
if (num_args == 0) {
// t is a constant
new_t = get_const_interp(f);
}
else {
// t is a function application
SASSERT(new_t.get() == 0);
// try to use function graph first
func_interp * fi = get_func_interp(f);
SASSERT(fi->get_arity() == num_args);
expr_ref r1(m_manager);
// fi may be partial...
if (!fi->eval(m_simplifier, args.c_ptr(), r1)) {
SASSERT(fi->is_partial()); // fi->eval only fails when fi is partial.
if (model_completion) {
expr * r = get_some_value(f->get_range());
fi->set_else(r);
SASSERT(!fi->is_partial());
new_t = r;
}
else {
// f is an uninterpreted function, there is no need to use m_simplifier.mk_app
new_t = m_manager.mk_app(f, num_args, args.c_ptr());
trail.push_back(new_t);
is_ok = false;
}
}
else {
SASSERT(r1);
trail.push_back(r1);
expr * r2 = 0;
if (!eval_cache.find(r1.get(), r2)) {
todo.back().second = r1;
todo.push_back(std::make_pair(r1, null));
continue;
}
else {
new_t = r2;
}
}
}
}
TRACE("model_eval",
tout << "orig:\n" << mk_pp(t, m_manager) << "\n";
tout << "new:\n" << mk_pp(new_t, m_manager) << "\n";);
todo.pop_back();
SASSERT(new_t.get() != 0);
eval_cache.insert(t, new_t);
break;
}
case AST_VAR:
SASSERT(a != 0);
eval_cache.insert(a, a);
todo.pop_back();
break;
case AST_QUANTIFIER:
is_ok = false; // evaluator does not handle quantifiers.
SASSERT(a != 0);
eval_cache.insert(a, a);
todo.pop_back();
break;
default:
UNREACHABLE();
break;
}
}
}
if (!eval_cache.find(e, a)) {
TRACE("model_eval", tout << "FAILED e: " << mk_bounded_pp(e, m_manager) << "\n";);
UNREACHABLE();
}
result = a;
TRACE("model_eval",
ast_ll_pp(tout << "original: ", m_manager, e);
ast_ll_pp(tout << "evaluated: ", m_manager, a);
ast_ll_pp(tout << "reduced: ", m_manager, result.get());
tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";
);
SASSERT(is_well_sorted(m_manager, result.get()));
return is_ok;
}
/**
\brief Replace uninterpreted constants occurring in fi->get_else()
by their interpretations.
*/
void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_aux_fs) {
if (fi->is_partial())
return;
expr * fi_else = fi->get_else();
TRACE("model_bug", tout << "cleaning up:\n" << mk_pp(fi_else, m_manager) << "\n";);
obj_map<expr, expr*> cache;
expr_ref_vector trail(m_manager);
ptr_buffer<expr, 128> todo;
ptr_buffer<expr> args;
todo.push_back(fi_else);
expr * a;
while (!todo.empty()) {
a = todo.back();
if (is_uninterp_const(a)) {
todo.pop_back();
func_decl * a_decl = to_app(a)->get_decl();
expr * ai = get_const_interp(a_decl);
if (ai == 0) {
ai = get_some_value(a_decl->get_range());
register_decl(a_decl, ai);
}
cache.insert(a, ai);
}
else {
switch(a->get_kind()) {
case AST_APP: {
app * t = to_app(a);
bool visited = true;
args.reset();
unsigned num_args = t->get_num_args();
for (unsigned i = 0; i < num_args; ++i) {
expr * arg = 0;
if (!cache.find(t->get_arg(i), arg)) {
visited = false;
todo.push_back(t->get_arg(i));
}
else {
args.push_back(arg);
}
}
if (!visited) {
continue;
}
func_decl * f = t->get_decl();
if (m_aux_decls.contains(f))
found_aux_fs.insert(f);
expr_ref new_t(m_manager);
m_simplifier.mk_app(f, num_args, args.c_ptr(), new_t);
if (t != new_t.get())
trail.push_back(new_t);
todo.pop_back();
cache.insert(t, new_t);
break;
}
default:
SASSERT(a != 0);
cache.insert(a, a);
todo.pop_back();
break;
}
}
}
if (!cache.find(fi_else, a)) {
UNREACHABLE();
}
fi->set_else(a);
}
void proto_model::remove_aux_decls_not_in_set(ptr_vector<func_decl> & decls, func_decl_set const & s) {
unsigned sz = decls.size();
unsigned i = 0;
unsigned j = 0;
for (; i < sz; i++) {
func_decl * f = decls[i];
if (!m_aux_decls.contains(f) || s.contains(f)) {
decls[j] = f;
j++;
}
}
decls.shrink(j);
}
/**
\brief Replace uninterpreted constants occurring in the func_interp's get_else()
by their interpretations.
*/
void proto_model::cleanup() {
func_decl_set found_aux_fs;
decl2finterp::iterator it = m_finterp.begin();
decl2finterp::iterator end = m_finterp.end();
for (; it != end; ++it) {
func_interp * fi = (*it).m_value;
cleanup_func_interp(fi, found_aux_fs);
}
// remove auxiliary declarations that are not used.
if (found_aux_fs.size() != m_aux_decls.size()) {
remove_aux_decls_not_in_set(m_decls, found_aux_fs);
remove_aux_decls_not_in_set(m_func_decls, found_aux_fs);
func_decl_set::iterator it2 = m_aux_decls.begin();
func_decl_set::iterator end2 = m_aux_decls.end();
for (; it2 != end2; ++it2) {
func_decl * faux = *it2;
if (!found_aux_fs.contains(faux)) {
TRACE("cleanup_bug", tout << "eliminating " << faux->get_name() << "\n";);
func_interp * fi = 0;
m_finterp.find(faux, fi);
SASSERT(fi != 0);
m_finterp.erase(faux);
dealloc(fi);
}
}
m_aux_decls.swap(found_aux_fs);
}
}
value_factory * proto_model::get_factory(family_id fid) {
return m_factories.get_plugin(fid);
}
void proto_model::freeze_universe(sort * s) {
SASSERT(m_manager.is_uninterp(s));
m_user_sort_factory->freeze_universe(s);
}
/**
\brief Return the known universe of an uninterpreted sort.
*/
obj_hashtable<expr> const & proto_model::get_known_universe(sort * s) const {
SASSERT(m_manager.is_uninterp(s));
return m_user_sort_factory->get_known_universe(s);
}
ptr_vector<expr> const & proto_model::get_universe(sort * s) const {
ptr_vector<expr> & tmp = const_cast<proto_model*>(this)->m_tmp;
tmp.reset();
obj_hashtable<expr> const & u = get_known_universe(s);
obj_hashtable<expr>::iterator it = u.begin();
obj_hashtable<expr>::iterator end = u.end();
for (; it != end; ++it)
tmp.push_back(*it);
return tmp;
}
unsigned proto_model::get_num_uninterpreted_sorts() const {
return m_user_sort_factory->get_num_sorts();
}
sort * proto_model::get_uninterpreted_sort(unsigned idx) const {
SASSERT(idx < get_num_uninterpreted_sorts());
return m_user_sort_factory->get_sort(idx);
}
/**
\brief Return true if the given sort is uninterpreted and has a finite interpretation
in the model.
*/
bool proto_model::is_finite(sort * s) const {
return m_manager.is_uninterp(s) && m_user_sort_factory->is_finite(s);
}
expr * proto_model::get_some_value(sort * s) {
family_id fid = s->get_family_id();
if (fid == null_family_id) {
return m_user_sort_factory->get_some_value(s);
}
value_factory * f = get_factory(fid);
if (f)
return f->get_some_value(s);
// there is no factory for the family id, then assume s is uninterpreted.
return m_user_sort_factory->get_some_value(s);
}
bool proto_model::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
family_id fid = s->get_family_id();
if (fid == null_family_id) {
return m_user_sort_factory->get_some_values(s, v1, v2);
}
value_factory * f = get_factory(fid);
if (f)
return f->get_some_values(s, v1, v2);
else
return false;
}
expr * proto_model::get_fresh_value(sort * s) {
family_id fid = s->get_family_id();
if (fid == null_family_id)
return m_user_sort_factory->get_fresh_value(s);
value_factory * f = get_factory(fid);
if (f)
return f->get_fresh_value(s);
else
// Use user_sort_factory if the theory has no support for model construnction.
// This is needed when dummy theories are used for arithmetic or arrays.
return m_user_sort_factory->get_fresh_value(s);
}
void proto_model::register_value(expr * n) {
sort * s = m_manager.get_sort(n);
family_id fid = s->get_family_id();
if (fid == null_family_id) {
m_user_sort_factory->register_value(n);
}
else {
value_factory * f = get_factory(fid);
if (f)
f->register_value(n);
}
}
bool proto_model::is_array_value(expr * v) const {
return is_app_of(v, m_afid, OP_AS_ARRAY);
}
void proto_model::compress() {
ptr_vector<func_decl>::iterator it = m_func_decls.begin();
ptr_vector<func_decl>::iterator end = m_func_decls.end();
for (; it != end; ++it) {
func_decl * f = *it;
func_interp * fi = get_func_interp(f);
SASSERT(fi != 0);
fi->compress();
}
}
/**
\brief Complete the interpretation fi of f if it is partial.
If f does not have an interpretation in the given model, then this is a noop.
*/
void proto_model::complete_partial_func(func_decl * f) {
func_interp * fi = get_func_interp(f);
if (fi && fi->is_partial()) {
expr * else_value = 0;
#if 0
// For UFBV benchmarks, setting the "else" to false is not a good idea.
// TODO: find a permanent solution. A possibility is to add another option.
if (m_manager.is_bool(f->get_range())) {
else_value = m_manager.mk_false();
}
else {
else_value = fi->get_max_occ_result();
if (else_value == 0)
else_value = get_some_value(f->get_range());
}
#else
else_value = fi->get_max_occ_result();
if (else_value == 0)
else_value = get_some_value(f->get_range());
#endif
fi->set_else(else_value);
}
}
/**
\brief Set the (else) field of function interpretations...
*/
void proto_model::complete_partial_funcs() {
if (m_params.m_model_partial)
return;
ptr_vector<func_decl>::iterator it = m_func_decls.begin();
ptr_vector<func_decl>::iterator end = m_func_decls.end();
for (; it != end; ++it)
complete_partial_func(*it);
}
model * proto_model::mk_model() {
TRACE("proto_model", tout << "mk_model\n"; model_v2_pp(tout, *this););
model * m = alloc(model, m_manager);
decl2expr::iterator it1 = m_interp.begin();
decl2expr::iterator end1 = m_interp.end();
for (; it1 != end1; ++it1) {
m->register_decl(it1->m_key, it1->m_value);
}
decl2finterp::iterator it2 = m_finterp.begin();
decl2finterp::iterator end2 = m_finterp.end();
for (; it2 != end2; ++it2) {
m->register_decl(it2->m_key, it2->m_value);
}
m_finterp.reset(); // m took the ownership of the func_interp's
unsigned sz = get_num_uninterpreted_sorts();
for (unsigned i = 0; i < sz; i++) {
sort * s = get_uninterpreted_sort(i);
TRACE("proto_model", tout << "copying uninterpreted sorts...\n" << mk_pp(s, m_manager) << "\n";);
ptr_buffer<expr> buf;
obj_hashtable<expr> const & u = get_known_universe(s);
obj_hashtable<expr>::iterator it = u.begin();
obj_hashtable<expr>::iterator end = u.end();
for (; it != end; ++it) {
buf.push_back(*it);
}
m->register_usort(s, buf.size(), buf.c_ptr());
}
return m;
}

119
src/model/proto_model.h
View file

@ -1,119 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
proto_model.h
Abstract:
This is the old model object.
smt::context used it during model construction and for
reporting the model for external consumers.
The whole value_factory "business" was due to model construction
and unnecessary for external consumers.
Future solvers will not use value_factory objects for
helping during model construction.
After smt::context finishes building the model, it is converted
into a new (light) model object.
Author:
Leonardo de Moura (leonardo) 2007-03-08.
Revision History:
--*/
#ifndef _PROTO_MODEL_H_
#define _PROTO_MODEL_H_
#include"model_core.h"
#include"model_params.h"
#include"value_factory.h"
#include"plugin_manager.h"
#include"simplifier.h"
#include"arith_decl_plugin.h"
#include"func_decl_dependencies.h"
#include"model.h"
class proto_model : public model_core {
model_params const & m_params;
ast_ref_vector m_asts;
plugin_manager<value_factory> m_factories;
user_sort_factory * m_user_sort_factory;
simplifier & m_simplifier;
family_id m_afid; //!< array family id: hack for displaying models in V1.x style
func_decl_set m_aux_decls;
ptr_vector<expr> m_tmp;
void reset_finterp();
expr * mk_some_interp_for(func_decl * d);
// Invariant: m_decls subset m_func_decls union m_const_decls union union m_value_decls
// Invariant: m_func_decls subset m_decls
// Invariant: m_const_decls subset m_decls
void remove_aux_decls_not_in_set(ptr_vector<func_decl> & decls, func_decl_set const & s);
void cleanup_func_interp(func_interp * fi, func_decl_set & found_aux_fs);
public:
proto_model(ast_manager & m, simplifier & s, model_params const & p);
virtual ~proto_model();
model_params const & get_model_params() const { return m_params; }
void register_factory(value_factory * f) { m_factories.register_plugin(f); }
bool eval(expr * e, expr_ref & result, bool model_completion = false);
bool is_array_value(expr * v) const;
value_factory * get_factory(family_id fid);
expr * get_some_value(sort * s);
bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2);
expr * get_fresh_value(sort * s);
void register_value(expr * n);
//
// Primitives for building models
//
void register_decl(func_decl * d, expr * v);
void register_decl(func_decl * f, func_interp * fi, bool aux = false);
void reregister_decl(func_decl * f, func_interp * new_fi, func_decl * f_aux);
void compress();
void cleanup();
//
// Primitives for building finite interpretations for uninterpreted sorts,
// and retrieving the known universe.
//
void freeze_universe(sort * s);
bool is_finite(sort * s) const;
obj_hashtable<expr> const & get_known_universe(sort * s) const;
virtual ptr_vector<expr> const & get_universe(sort * s) const;
virtual unsigned get_num_uninterpreted_sorts() const;
virtual sort * get_uninterpreted_sort(unsigned idx) const;
//
// Complete partial function interps
//
void complete_partial_func(func_decl * f);
void complete_partial_funcs();
//
// Create final model object.
// proto_model is corrupted after that.
model * mk_model();
};
typedef ref<proto_model> proto_model_ref;
#endif /* _PROTO_MODEL_H_ */

78
src/model/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
src/model/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_ */

117
src/model/value_factory.cpp
View file

@ -1,117 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
value_factory.cpp
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-10-28.
Revision History:
--*/
#include"value_factory.h"
value_factory::value_factory(ast_manager & m, family_id fid):
m_manager(m),
m_fid(fid) {
}
value_factory::~value_factory() {
}
basic_factory::basic_factory(ast_manager & m):
value_factory(m, m.get_basic_family_id()) {
}
expr * basic_factory::get_some_value(sort * s) {
if (m_manager.is_bool(s))
return m_manager.mk_false();
return 0;
}
bool basic_factory::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
if (m_manager.is_bool(s)) {
v1 = m_manager.mk_false();
v2 = m_manager.mk_true();
return true;
}
return false;
}
expr * basic_factory::get_fresh_value(sort * s) {
return 0;
}
user_sort_factory::user_sort_factory(ast_manager & m):
simple_factory<unsigned>(m, m.get_family_id("user-sort")) {
}
void user_sort_factory::freeze_universe(sort * s) {
if (!m_finite.contains(s)) {
value_set * set = 0;
m_sort2value_set.find(s, set);
if (!m_sort2value_set.find(s, set) || set->m_values.empty()) {
// we cannot freeze an empty universe.
get_some_value(s); // add one element to the universe...
}
SASSERT(m_sort2value_set.find(s, set) && set != 0 && !set->m_values.empty());
m_finite.insert(s);
}
}
obj_hashtable<expr> const & user_sort_factory::get_known_universe(sort * s) const {
value_set * set = 0;
if (m_sort2value_set.find(s, set)) {
return set->m_values;
}
return m_empty_universe;
}
expr * user_sort_factory::get_some_value(sort * s) {
if (is_finite(s)) {
value_set * set = 0;
m_sort2value_set.find(s, set);
SASSERT(set != 0);
SASSERT(!set->m_values.empty());
return *(set->m_values.begin());
}
return simple_factory<unsigned>::get_some_value(s);
}
bool user_sort_factory::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
if (is_finite(s)) {
value_set * set = 0;
if (m_sort2value_set.find(s, set) && set->m_values.size() >= 2) {
obj_hashtable<expr>::iterator it = set->m_values.begin();
v1 = *it;
++it;
v2 = *it;
return true;
}
return false;
}
return simple_factory<unsigned>::get_some_values(s, v1, v2);
}
expr * user_sort_factory::get_fresh_value(sort * s) {
if (is_finite(s))
return 0;
return simple_factory<unsigned>::get_fresh_value(s);
}
void user_sort_factory::register_value(expr * n) {
SASSERT(!is_finite(m_manager.get_sort(n)));
simple_factory<unsigned>::register_value(n);
}
app * user_sort_factory::mk_value_core(unsigned const & val, sort * s) {
return m_manager.mk_model_value(val, s);
}

257
src/model/value_factory.h
View file

@ -1,257 +0,0 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
value_factory.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-10-28.
Revision History:
--*/
#ifndef _VALUE_FACTORY_H_
#define _VALUE_FACTORY_H_
#include"ast.h"
#include"obj_hashtable.h"
/**
\brief Auxiliary object used during model construction.
*/
class value_factory {
protected:
ast_manager & m_manager;
family_id m_fid;
public:
value_factory(ast_manager & m, family_id fid);
virtual ~value_factory();
/**
\brief Return some value of the given sort. The result is always different from zero.
*/
virtual expr * get_some_value(sort * s) = 0;
/**
\brief Return two distinct values of the given sort. The results are stored in v1 and v2.
Return false if the intended interpretation of the given sort has only one element.
*/
virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) = 0;
/**
\brief Return a fresh value of the given sort.
Return 0 if it is not possible to do that (e.g., the sort is finite).
*/
virtual expr * get_fresh_value(sort * s) = 0;
/**
\brief Used to register that the given value was used in model construction.
So, get_fresh_value cannot return this value anymore.
*/
virtual void register_value(expr * n) = 0;
family_id get_family_id() const { return m_fid; }
};
class basic_factory : public value_factory {
public:
basic_factory(ast_manager & m);
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);
virtual void register_value(expr * n) { }
};
/**
\brief Template for value factories for numeric (and enumeration-like) sorts
*/
template<typename Number>
class simple_factory : public value_factory {
protected:
struct value_set {
obj_hashtable<expr> m_values;
Number m_next;
value_set():
m_next(0) {
}
};
typedef obj_map<sort, value_set *> sort2value_set;
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) {
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);
DEBUG_CODE({
value_set * set2 = 0;
SASSERT(m_sort2value_set.find(s, set2));
SASSERT(set == set2);
});
return set;
}
virtual app * mk_value_core(Number const & val, sort * s) = 0;
app * mk_value(Number const & val, sort * s, bool & is_new) {
value_set * set = get_value_set(s);
app * new_val = mk_value_core(val, s);
is_new = false;
if (!set->m_values.contains(new_val)) {
m_values.push_back(new_val);
set->m_values.insert(new_val);
is_new = true;
}
SASSERT(set->m_values.contains(new_val));
return new_val;
}
public:
simple_factory(ast_manager & m, family_id fid):
value_factory(m, fid),
m_values(m),
m_sorts(m) {
}
virtual ~simple_factory() {
std::for_each(m_sets.begin(), m_sets.end(), delete_proc<value_set>());
}
virtual expr * get_some_value(sort * s) {
value_set * set = 0;
expr * result = 0;
if (m_sort2value_set.find(s, set) && !set->m_values.empty())
result = *(set->m_values.begin());
else
result = mk_value(Number(0), s);
return result;
}
virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
value_set * set = 0;
if (m_sort2value_set.find(s, set)) {
switch (set->m_values.size()) {
case 0:
v1 = mk_value(Number(0), s);
v2 = mk_value(Number(1), s);
break;
case 1:
v1 = *(set->m_values.begin());
v2 = mk_value(Number(0), s);
if (v1 == v2)
v2 = mk_value(Number(1), s);
break;
default:
obj_hashtable<expr>::iterator it = set->m_values.begin();
v1 = *it;
++it;
v2 = *it;
break;
}
SASSERT(v1 != v2);
return true;
}
v1 = mk_value(Number(0), s);
v2 = mk_value(Number(1), s);
return true;
}
virtual expr * get_fresh_value(sort * s) {
value_set * set = get_value_set(s);
bool is_new = false;
expr * result = 0;
Number & next = set->m_next;
while (!is_new) {
result = mk_value(next, s, is_new);
next++;
}
SASSERT(result != 0);
return result;
}
virtual void register_value(expr * n) {
sort * s = this->m_manager.get_sort(n);
value_set * set = get_value_set(s);
if (!set->m_values.contains(n)) {
m_values.push_back(n);
set->m_values.insert(n);
}
}
virtual app * mk_value(Number const & val, sort * s) {
bool is_new;
return mk_value(val, s, is_new);
}
unsigned get_num_sorts() const { return m_sorts.size(); }
sort * get_sort(unsigned idx) const { return m_sorts.get(idx); }
};
/**
\brief Factory for creating values for uninterpreted sorts and user
declared (uninterpreted) sorts.
*/
class user_sort_factory : public simple_factory<unsigned> {
obj_hashtable<sort> m_finite; //!< set of sorts that are marked as finite.
obj_hashtable<expr> m_empty_universe;
virtual app * mk_value_core(unsigned const & val, sort * s);
public:
user_sort_factory(ast_manager & m);
virtual ~user_sort_factory() {}
/**
\brief Make the universe of \c s finite, by preventing new
elements to be added to its universe.
*/
void freeze_universe(sort * s);
/**
\brief Return true if the universe of \c s is frozen and finite.
*/
bool is_finite(sort * s) const {
return m_finite.contains(s);
}
/**
\brief Return the "known" universe of \c s. It doesn't matter whether
s is finite or not. If \c s is finite, then it is the whole universe.
*/
obj_hashtable<expr> const & get_known_universe(sort * s) const;
/**
\brief Return sorts with finite interpretations.
*/
obj_hashtable<sort> const & get_finite_sorts() const { return m_finite; }
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);
virtual void register_value(expr * n);
};
#endif /* _VALUE_FACTORY_H_ */