mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Merge pull request #1222 from NikolajBjorner/master

Browse source 
bug fixes and revision of proto_model
This commit is contained in:
Nikolaj Bjorner 2017-08-21 17:19:27 -07:00 committed by GitHub
parent ed5058d225 2c8e9aeb9c
commit 26afdd92c9
15 changed files with 313 additions and 714 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/array_decl_plugin.cpp
View file

@ -556,9 +556,9 @@ bool array_decl_plugin::is_fully_interp(sort const * s) const {
return m_manager->is_fully_interp(get_array_range(s));
}
func_decl * array_recognizers::get_as_array_func_decl(app * n) const {
func_decl * array_recognizers::get_as_array_func_decl(expr * n) const {
SASSERT(is_as_array(n));
return to_func_decl(n->get_decl()->get_parameter(0).get_ast());
return to_func_decl(to_app(n)->get_decl()->get_parameter(0).get_ast());
}
array_util::array_util(ast_manager& m):

2
src/ast/array_decl_plugin.h
View file

@ -148,7 +148,7 @@ public:
bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); }
bool is_map(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_MAP); }
bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); }
func_decl * get_as_array_func_decl(app * n) const;
func_decl * get_as_array_func_decl(expr * n) const;
};
class array_util : public array_recognizers {

10
src/ast/rewriter/seq_rewriter.cpp
View file

@ -864,11 +864,11 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
expr_ref_vector as(m()), bs(m());
if (a1 != b1 && isc1 && isc2) {
TRACE("seq", tout << s1 << " " << s2 << "\n";);
if (s1.length() <= s2.length()) {
if (s1.prefixof(s2)) {
if (a == a1) {
result = m().mk_true();
TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";);
return BR_DONE;
}
m_util.str.get_concat(a, as);
@ -878,10 +878,12 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
bs[0] = m_util.str.mk_string(s2);
result = m_util.str.mk_prefix(m_util.str.mk_concat(as.size()-1, as.c_ptr()+1),
m_util.str.mk_concat(bs.size(), bs.c_ptr()));
TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";);
return BR_REWRITE_FULL;
}
else {
result = m().mk_false();
TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";);
return BR_DONE;
}
}
@ -889,6 +891,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
if (s2.prefixof(s1)) {
if (b == b1) {
result = m().mk_false();
TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";);
return BR_DONE;
}
m_util.str.get_concat(a, as);
@ -898,10 +901,12 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
as[0] = m_util.str.mk_string(s1);
result = m_util.str.mk_prefix(m_util.str.mk_concat(as.size(), as.c_ptr()),
m_util.str.mk_concat(bs.size()-1, bs.c_ptr()+1));
TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";);
return BR_REWRITE_FULL;
}
else {
result = m().mk_false();
TRACE("seq", tout << s1 << " " << s2 << " " << result << "\n";);
return BR_DONE;
}
}
@ -930,9 +935,6 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
if (i == as.size()) {
result = mk_and(eqs);
TRACE("seq", tout << result << "\n";);
if (m().is_true(result)) {
return BR_DONE;
}
return BR_REWRITE3;
}
SASSERT(i < as.size());

6
src/model/model_core.cpp
View file

@ -90,11 +90,11 @@ void model_core::register_decl(func_decl * d, func_interp * fi) {
void model_core::unregister_decl(func_decl * d) {
decl2expr::obj_map_entry * ec = m_interp.find_core(d);
if (ec && ec->get_data().m_value != 0) {
m_manager.dec_ref(ec->get_data().m_key);
m_manager.dec_ref(ec->get_data().m_value);
m_manager.dec_ref(ec->get_data().m_key);
m_manager.dec_ref(ec->get_data().m_value);
m_interp.remove(d);
m_const_decls.erase(d);
return;
return;
}
decl2finterp::obj_map_entry * ef = m_finterp.find_core(d);

2
src/muz/spacer/spacer_generalizers.cpp
View file

@ -133,7 +133,7 @@ void unsat_core_generalizer::operator()(lemma_ref &lemma)
unsigned uses_level;
expr_ref_vector core(m);
VERIFY(pt.is_invariant(lemma->level(), lemma->get_expr(), uses_level, &core));
VERIFY(pt.is_invariant(old_level, lemma->get_expr(), uses_level, &core));
CTRACE("spacer", old_sz > core.size(),
tout << "unsat core reduced lemma from: "

2
src/muz/spacer/spacer_qe_project.cpp
View file

@ -98,7 +98,7 @@ peq::peq (app* p, ast_manager& m):
m_eq (m),
m_arr_u (m)
{
SASSERT (is_partial_eq (p));
VERIFY (is_partial_eq (p));
SASSERT (m_arr_u.is_array (m_lhs) &&
m_arr_u.is_array (m_rhs) &&
m_eq_proc (m.get_sort (m_lhs), m.get_sort (m_rhs)));

3
src/smt/mam.cpp
View file

@ -2080,16 +2080,15 @@ namespace smt {
*/
enode_vector * interpreter::mk_depth1_vector(enode * n, func_decl * f, unsigned i) {
enode_vector * v = mk_enode_vector();
unsigned num_args = n->get_num_args();
n = n->get_root();
enode_vector::const_iterator it = n->begin_parents();
enode_vector::const_iterator end = n->end_parents();
for (; it != end; ++it) {
enode * p = *it;
if (p->get_decl() == f &&
i < p->get_num_args() &&
m_context.is_relevant(p) &&
p->is_cgr() &&
i < p->get_num_args() &&
p->get_arg(i)->get_root() == n) {
v->push_back(p);
}

16
src/smt/proto_model/datatype_factory.cpp
View file

@ -19,7 +19,6 @@ Revision History:
#include "smt/proto_model/datatype_factory.h"
#include "smt/proto_model/proto_model.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/expr_functors.h"
datatype_factory::datatype_factory(ast_manager & m, proto_model & md):
@ -90,10 +89,7 @@ expr * datatype_factory::get_almost_fresh_value(sort * 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;
for (func_decl * constructor : *constructors) {
expr_ref_vector args(m_manager);
bool found_fresh_arg = false;
bool recursive = false;
@ -156,10 +152,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
// 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;
for (func_decl * constructor : *constructors) {
expr_ref_vector args(m_manager);
bool found_fresh_arg = false;
unsigned num = constructor->get_arity();
@ -197,10 +190,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
++num_iterations;
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;
for (func_decl * constructor : *constructors) {
expr_ref_vector args(m_manager);
bool found_sibling = false;
unsigned num = constructor->get_arity();

340
src/smt/proto_model/proto_model.cpp
View file

@ -10,41 +10,40 @@ Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2007-03-08.
Revision History:
--*/
#include "smt/proto_model/proto_model.h"
#include "model/model_params.hpp"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/rewriter/var_subst.h"
#include "ast/array_decl_plugin.h"
#include "ast/well_sorted.h"
#include "ast/used_symbols.h"
#include "model/model_params.hpp"
#include "model/model_v2_pp.h"
#include "smt/proto_model/proto_model.h"
proto_model::proto_model(ast_manager & m, params_ref const & p):
model_core(m),
m_afid(m.mk_family_id(symbol("array"))),
m_eval(*this),
m_rewrite(m) {
register_factory(alloc(basic_factory, m));
m_user_sort_factory = alloc(user_sort_factory, m);
register_factory(m_user_sort_factory);
m_model_partial = model_params(p).partial();
}
void proto_model::register_aux_decl(func_decl * d, func_interp * fi) {
model_core::register_decl(d, fi);
m_aux_decls.insert(d);
}
void proto_model::register_aux_decl(func_decl * d) {
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.
@ -84,21 +83,11 @@ expr * proto_model::mk_some_interp_for(func_decl * d) {
}
bool proto_model::is_select_of_model_value(expr* e) const {
return
is_app_of(e, m_afid, OP_SELECT) &&
is_as_array(to_app(e)->get_arg(0)) &&
has_interpretation(array_util(m_manager).get_as_array_func_decl(to_app(to_app(e)->get_arg(0))));
}
bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
m_eval.set_model_completion(model_completion);
m_eval.set_expand_array_equalities(false);
try {
m_eval(e, result);
#if 0
std::cout << mk_pp(e, m_manager) << "\n===>\n" << result << "\n";
#endif
return true;
}
catch (model_evaluator_exception & ex) {
@ -158,12 +147,11 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au
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) {
for (expr* t_arg : *t) {
expr * arg = 0;
if (!cache.find(t->get_arg(i), arg)) {
if (!cache.find(t_arg, arg)) {
visited = false;
todo.push_back(t->get_arg(i));
todo.push_back(t_arg);
}
else {
args.push_back(arg);
@ -176,7 +164,7 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au
if (m_aux_decls.contains(f))
found_aux_fs.insert(f);
expr_ref new_t(m_manager);
new_t = m_rewrite.mk_app(f, num_args, args.c_ptr());
new_t = m_rewrite.mk_app(f, args.size(), args.c_ptr());
if (t != new_t.get())
trail.push_back(new_t);
todo.pop_back();
@ -220,10 +208,8 @@ void proto_model::remove_aux_decls_not_in_set(ptr_vector<func_decl> & decls, fun
*/
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;
for (auto const& kv : m_finterp) {
func_interp * fi = kv.m_value;
cleanup_func_interp(fi, found_aux_fs);
}
@ -232,18 +218,10 @@ void proto_model::cleanup() {
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;
for (func_decl* faux : m_aux_decls) {
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);
m_manager.dec_ref(faux);
dealloc(fi);
unregister_decl(faux);
}
}
m_aux_decls.swap(found_aux_fs);
@ -270,10 +248,9 @@ 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);
for (expr * e : u) {
tmp.push_back(e);
}
return tmp;
}
@ -351,15 +328,8 @@ void proto_model::register_value(expr * n) {
}
}
bool proto_model::is_as_array(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;
for (func_decl* f : m_func_decls) {
func_interp * fi = get_func_interp(f);
SASSERT(fi != 0);
fi->compress();
@ -373,23 +343,9 @@ void proto_model::compress() {
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();
expr * 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);
}
}
@ -412,17 +368,13 @@ 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);
for (auto const& kv : m_interp) {
m->register_decl(kv.m_key, kv.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_manager.dec_ref(it2->m_key);
for (auto const& kv : m_finterp) {
m->register_decl(kv.m_key, kv.m_value);
m_manager.dec_ref(kv.m_key);
}
m_finterp.reset(); // m took the ownership of the func_interp's
@ -437,245 +389,3 @@ model * proto_model::mk_model() {
return m;
}
#if 0
#include "ast/simplifier/simplifier.h"
#include "ast/simplifier/basic_simplifier_plugin.h"
// Auxiliary function for computing fi(args[0], ..., args[fi.get_arity() - 1]).
// The result is stored in result.
// Return true if succeeded, and false otherwise.
// It uses the simplifier s during the computation.
bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & result) {
bool actuals_are_values = true;
if (fi.num_entries() != 0) {
for (unsigned i = 0; actuals_are_values && i < fi.get_arity(); i++) {
actuals_are_values = fi.m().is_value(args[i]);
}
}
func_entry * entry = fi.get_entry(args);
if (entry != 0) {
result = entry->get_result();
return true;
}
TRACE("func_interp", tout << "failed to find entry for: ";
for(unsigned i = 0; i < fi.get_arity(); i++)
tout << mk_pp(args[i], fi.m()) << " ";
tout << "\nis partial: " << fi.is_partial() << "\n";);
if (!fi.eval_else(args, result)) {
return false;
}
if (actuals_are_values && fi.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(fi.m().get_basic_family_id()));
for (unsigned k = 0; k < fi.num_entries(); k++) {
func_entry const * curr = fi.get_entry(k);
SASSERT(!curr->eq_args(fi.m(), fi.get_arity(), args));
if (!actuals_are_values || !curr->args_are_values()) {
expr_ref_buffer eqs(fi.m());
unsigned i = fi.get_arity();
while (i > 0) {
--i;
expr_ref new_eq(fi.m());
bs->mk_eq(curr->get_arg(i), args[i], new_eq);
eqs.push_back(new_eq);
}
SASSERT(eqs.size() == fi.get_arity());
expr_ref new_cond(fi.m());
bs->mk_and(eqs.size(), eqs.c_ptr(), new_cond);
bs->mk_ite(new_cond, curr->get_result(), result, result);
}
}
return true;
}
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));
simplifier m_simplifier(m_manager);
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 {
TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";);
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);
TRACE("model_eval", tout << mk_pp(t, m_manager) << " -> " << new_t << "\n";);
trail.push_back(new_t);
if (!is_app(new_t) || to_app(new_t)->get_decl() != f || is_select_of_model_value(new_t)) {
// 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 (!::eval(*fi, 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);
TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";);
is_ok = false;
}
}
else {
SASSERT(r1);
trail.push_back(r1);
TRACE("model_eval", tout << mk_pp(a, m_manager) << "\nevaluates to: " << r1 << "\n";);
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:
TRACE("model_eval", tout << "found quantifier\n" << mk_pp(a, m_manager) << "\n";);
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;
std::cout << mk_pp(e, m_manager) << "\n===>\n" << result << "\n";
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;
}
#endif

4
src/smt/proto_model/proto_model.h
View file

@ -41,7 +41,6 @@ Revision History:
class proto_model : public model_core {
plugin_manager<value_factory> m_factories;
user_sort_factory * m_user_sort_factory;
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;
model_evaluator m_eval;
@ -58,7 +57,6 @@ class proto_model : public model_core {
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);
bool is_select_of_model_value(expr* e) const;
public:
proto_model(ast_manager & m, params_ref const & p = params_ref());
@ -68,7 +66,6 @@ public:
bool eval(expr * e, expr_ref & result, bool model_completion = false);
bool is_as_array(expr * v) const;
value_factory * get_factory(family_id fid);
@ -84,6 +81,7 @@ public:
// Primitives for building models
//
void register_aux_decl(func_decl * f, func_interp * fi);
void register_aux_decl(func_decl * f);
void reregister_decl(func_decl * f, func_interp * new_fi, func_decl * f_aux);
void compress();
void cleanup();

39
src/smt/smt_model_checker.cpp
View file

@ -17,16 +17,15 @@ Revision History:
--*/
#include "smt/smt_model_checker.h"
#include "smt/smt_context.h"
#include "smt/smt_model_finder.h"
#include "ast/normal_forms/pull_quant.h"
#include "ast/for_each_expr.h"
#include "ast/rewriter/var_subst.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "model/model_pp.h"
#include "ast/ast_smt2_pp.h"
#include "smt/smt_model_checker.h"
#include "smt/smt_context.h"
#include "smt/smt_model_finder.h"
#include "model/model_pp.h"
namespace smt {
@ -65,11 +64,9 @@ namespace smt {
expr * model_checker::get_term_from_ctx(expr * val) {
if (m_value2expr.empty()) {
// populate m_value2expr
obj_map<enode, app *>::iterator it = m_root2value->begin();
obj_map<enode, app *>::iterator end = m_root2value->end();
for (; it != end; ++it) {
enode * n = (*it).m_key;
expr * val = (*it).m_value;
for (auto const& kv : *m_root2value) {
enode * n = kv.m_key;
expr * val = kv.m_value;
n = n->get_eq_enode_with_min_gen();
m_value2expr.insert(val, n->get_owner());
}
@ -89,10 +86,7 @@ namespace smt {
void model_checker::restrict_to_universe(expr * sk, obj_hashtable<expr> const & universe) {
SASSERT(!universe.empty());
ptr_buffer<expr> eqs;
obj_hashtable<expr>::iterator it = universe.begin();
obj_hashtable<expr>::iterator end = universe.end();
for (; it != end; ++it) {
expr * e = *it;
for (expr * e : universe) {
eqs.push_back(m.mk_eq(sk, e));
}
expr_ref fml(m.mk_or(eqs.size(), eqs.c_ptr()), m);
@ -201,9 +195,8 @@ namespace smt {
void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) {
SASSERT(q->get_num_decls() == bindings.size());
for (unsigned i = 0; i < bindings.size(); i++)
m_pinned_exprs.push_back(bindings[i]);
for (expr* b : bindings)
m_pinned_exprs.push_back(b);
m_pinned_exprs.push_back(q);
void * mem = m_new_instances_region.allocate(instance::get_obj_size(q->get_num_decls()));
@ -237,10 +230,8 @@ namespace smt {
bool model_checker::add_blocking_clause(model * cex, expr_ref_vector & sks) {
SASSERT(cex != 0);
unsigned num_sks = sks.size();
expr_ref_buffer diseqs(m);
for (unsigned i = 0; i < num_sks; i++) {
expr * sk = sks.get(i);
for (expr * sk : sks) {
func_decl * sk_d = to_app(sk)->get_decl();
expr_ref sk_value(m);
sk_value = cex->get_const_interp(sk_d);
@ -272,8 +263,7 @@ namespace smt {
assert_neg_q_m(flat_q, sks);
TRACE("model_checker", tout << "skolems:\n";
for (unsigned i = 0; i < sks.size(); i++) {
expr * sk = sks.get(i);
for (expr* sk : sks) {
tout << mk_ismt2_pp(sk, m) << " " << mk_pp(m.get_sort(sk), m) << "\n";
});
@ -486,10 +476,7 @@ namespace smt {
TRACE("model_checker_bug_detail", tout << "assert_new_instances, inconsistent: " << m_context->inconsistent() << "\n";);
ptr_buffer<enode> bindings;
ptr_vector<enode> dummy;
ptr_vector<instance>::iterator it = m_new_instances.begin();
ptr_vector<instance>::iterator end = m_new_instances.end();
for (; it != end; ++it) {
instance * inst = *it;
for (instance* inst : m_new_instances) {
quantifier * q = inst->m_q;
if (m_context->b_internalized(q)) {
bindings.reset();

495
src/smt/smt_model_finder.cpp
View file

@ -16,8 +16,8 @@ Author:
Revision History:
--*/
#include "smt/smt_model_finder.h"
#include "smt/smt_context.h"
#include "util/cooperate.h"
#include "util/backtrackable_set.h"
#include "ast/ast_util.h"
#include "ast/macros/macro_util.h"
#include "ast/arith_decl_plugin.h"
@ -27,14 +27,14 @@ Revision History:
#include "ast/simplifier/bv_simplifier_plugin.h"
#include "ast/normal_forms/pull_quant.h"
#include "ast/rewriter/var_subst.h"
#include "util/backtrackable_set.h"
#include "ast/for_each_expr.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/well_sorted.h"
#include "model/model_pp.h"
#include "ast/ast_smt2_pp.h"
#include "util/cooperate.h"
#include "model/model_pp.h"
#include "smt/smt_model_finder.h"
#include "smt/smt_context.h"
#include "tactic/tactic_exception.h"
namespace smt {
@ -56,11 +56,9 @@ namespace smt {
v1.swap(v2);
return;
}
typename ptr_vector<T>::iterator it = v2.begin();
typename ptr_vector<T>::iterator end = v2.end();
for (; it != end; ++it) {
if (!v1.contains(*it))
v1.push_back(*it);
for (T* t : v2) {
if (!v1.contains(t))
v1.push_back(t);
}
v2.finalize();
}
@ -88,10 +86,8 @@ namespace smt {
instantiation_set(ast_manager & m):m_manager(m) {}
~instantiation_set() {
obj_map<expr, unsigned>::iterator it = m_elems.begin();
obj_map<expr, unsigned>::iterator end = m_elems.end();
for (; it != end; ++it) {
m_manager.dec_ref((*it).m_key);
for (auto const& kv : m_elems) {
m_manager.dec_ref(kv.m_key);
}
m_elems.reset();
}
@ -116,16 +112,12 @@ namespace smt {
}
void display(std::ostream & out) const {
obj_map<expr, unsigned>::iterator it = m_elems.begin();
obj_map<expr, unsigned>::iterator end = m_elems.end();
for (; it != end; ++it) {
out << mk_bounded_pp((*it).m_key, m_manager) << " [" << (*it).m_value << "]\n";
for (auto const& kv : m_elems) {
out << mk_bounded_pp(kv.m_key, m_manager) << " [" << kv.m_value << "]\n";
}
out << "inverse:\n";
obj_map<expr, expr *>::iterator it2 = m_inv.begin();
obj_map<expr, expr *>::iterator end2 = m_inv.end();
for (; it2 != end2; ++it2) {
out << mk_bounded_pp((*it2).m_key, m_manager) << " -> " << mk_bounded_pp((*it2).m_value, m_manager) << "\n";
for (auto const& kv : m_inv) {
out << mk_bounded_pp(kv.m_key, m_manager) << " -> " << mk_bounded_pp(kv.m_value, m_manager) << "\n";
}
}
@ -142,12 +134,10 @@ namespace smt {
}
void mk_inverse(evaluator & ev) {
obj_map<expr, unsigned>::iterator it = m_elems.begin();
obj_map<expr, unsigned>::iterator end = m_elems.end();
for (; it != end; ++it) {
expr * t = (*it).m_key;
for (auto const& kv : m_elems) {
expr * t = kv.m_key;
SASSERT(!contains_model_value(t));
unsigned gen = (*it).m_value;
unsigned gen = kv.m_value;
expr * t_val = ev.eval(t, true);
if (!t_val) break;
TRACE("model_finder", tout << mk_pp(t, m_manager) << " " << mk_pp(t_val, m_manager) << "\n";);
@ -329,17 +319,13 @@ namespace smt {
out << "root node ------\n";
out << "@" << m_id << " mono: " << m_mono_proj << " signed: " << m_signed_proj << ", sort: " << mk_pp(m_sort, m) << "\n";
out << "avoid-set: ";
ptr_vector<node>::const_iterator it1 = m_avoid_set.begin();
ptr_vector<node>::const_iterator end1 = m_avoid_set.end();
for (; it1 != end1; ++it1) {
out << "@" << (*it1)->get_root()->get_id() << " ";
for (node* n : m_avoid_set) {
out << "@" << n->get_root()->get_id() << " ";
}
out << "\n";
out << "exceptions: ";
ptr_vector<expr>::const_iterator it2 = m_exceptions.begin();
ptr_vector<expr>::const_iterator end2 = m_exceptions.end();
for (; it2 != end2; ++it2) {
out << mk_bounded_pp((*it2), m) << " ";
for (expr * e : m_exceptions) {
out << mk_bounded_pp(e, m) << " ";
}
out << "\n";
if (m_else)
@ -368,10 +354,8 @@ namespace smt {
// return true if m_avoid_set.contains(this)
bool must_avoid_itself() const {
node * r = get_root();
ptr_vector<node>::const_iterator it = m_avoid_set.begin();
ptr_vector<node>::const_iterator end = m_avoid_set.end();
for (; it != end; ++it) {
if (r == (*it)->get_root())
for (node* n : m_avoid_set) {
if (r == n->get_root())
return true;
}
return false;
@ -460,23 +444,19 @@ namespace smt {
}
void display_key2node(std::ostream & out, key2node const & m) const {
key2node::iterator it = m.begin();
key2node::iterator end = m.end();
for (; it != end; ++it) {
ast * a = (*it).m_key.first;
unsigned i = (*it).m_key.second;
node * n = (*it).m_value;
for (auto const& kv : m) {
ast * a = kv.m_key.first;
unsigned i = kv.m_key.second;
node * n = kv.m_value;
out << "#" << a->get_id() << ":" << i << " -> @" << n->get_id() << "\n";
}
}
void display_A_f_is(std::ostream & out) const {
key2node::iterator it = m_A_f_is.begin();
key2node::iterator end = m_A_f_is.end();
for (; it != end; ++it) {
func_decl * f = static_cast<func_decl*>((*it).m_key.first);
unsigned i = (*it).m_key.second;
node * n = (*it).m_value;
for (auto const& kv : m_A_f_is) {
func_decl * f = static_cast<func_decl*>(kv.m_key.first);
unsigned i = kv.m_key.second;
node * n = kv.m_value;
out << f->get_name() << ":" << i << " -> @" << n->get_id() << "\n";
}
}
@ -556,10 +536,7 @@ namespace smt {
}
void mk_instantiation_sets() {
ptr_vector<node>::const_iterator it = m_nodes.begin();
ptr_vector<node>::const_iterator end = m_nodes.end();
for (; it != end; ++it) {
node * curr = *it;
for (node* curr : m_nodes) {
if (curr->is_root()) {
curr->mk_instantiation_set(m_manager);
}
@ -569,22 +546,19 @@ namespace smt {
// For each instantiation_set, reemove entries that do not evaluate to values.
void cleanup_instantiation_sets() {
ptr_vector<expr> to_delete;
ptr_vector<node>::const_iterator it = m_nodes.begin();
ptr_vector<node>::const_iterator end = m_nodes.end();
for (; it != end; ++it) {
node * curr = *it;
for (node * curr : m_nodes) {
if (curr->is_root()) {
instantiation_set * s = curr->get_instantiation_set();
to_delete.reset();
obj_map<expr, unsigned> const & elems = s->get_elems();
for (obj_map<expr, unsigned>::iterator it = elems.begin(); it != elems.end(); it++) {
expr * n = it->m_key;
for (auto const& kv : elems) {
expr * n = kv.m_key;
expr * n_val = eval(n, true);
if (!n_val || !m_manager.is_value(n_val))
to_delete.push_back(n);
}
for (ptr_vector<expr>::iterator it = to_delete.begin(); it != to_delete.end(); it++) {
s->remove(*it);
for (expr* e : to_delete) {
s->remove(e);
}
}
}
@ -592,11 +566,9 @@ namespace smt {
void display_nodes(std::ostream & out) const {
display_key2node(out, m_uvars);
display_A_f_is(out);
ptr_vector<node>::const_iterator it = m_nodes.begin();
ptr_vector<node>::const_iterator end = m_nodes.end();
for (; it != end; ++it) {
(*it)->display(out, m_manager);
display_A_f_is(out);
for (node* n : m_nodes) {
n->display(out, m_manager);
}
}
@ -628,18 +600,14 @@ namespace smt {
ptr_vector<expr> const & exceptions = n->get_exceptions();
ptr_vector<node> const & avoid_set = n->get_avoid_set();
ptr_vector<expr>::const_iterator it1 = exceptions.begin();
ptr_vector<expr>::const_iterator end1 = exceptions.end();
for (; it1 != end1; ++it1) {
expr * val = eval(*it1, true);
for (expr* e : exceptions) {
expr * val = eval(e, true);
SASSERT(val != 0);
r.push_back(val);
}
ptr_vector<node>::const_iterator it2 = avoid_set.begin();
ptr_vector<node>::const_iterator end2 = avoid_set.end();
for (; it2 != end2; ++it2) {
node * n = (*it2)->get_root();
for (node* a : avoid_set) {
node * n = a->get_root();
if (!n->is_mono_proj() && n->get_else() != 0) {
expr * val = eval(n->get_else(), true);
SASSERT(val != 0);
@ -661,20 +629,19 @@ namespace smt {
expr * t_result = 0;
unsigned gen_result = UINT_MAX;
obj_map<expr, unsigned>::iterator it1 = elems.begin();
obj_map<expr, unsigned>::iterator end1 = elems.end();
for (; it1 != end1; ++it1) {
expr * t = (*it1).m_key;
unsigned gen = (*it1).m_value;
for (auto const& kv : elems) {
expr * t = kv.m_key;
unsigned gen = kv.m_value;
expr * t_val = eval(t, true);
SASSERT(t_val != 0);
ptr_buffer<expr>::const_iterator it2 = ex_vals.begin();
ptr_buffer<expr>::const_iterator end2 = ex_vals.end();
for (; it2 != end2; ++it2) {
if (!m_manager.are_distinct(t_val, *it2))
bool found = false;
for (expr* v : ex_vals) {
if (!m_manager.are_distinct(t_val, v)) {
found = true;
break;
}
}
if (it2 == end2 && (t_result == 0 || gen < gen_result)) {
if (!found && (t_result == 0 || gen < gen_result)) {
t_result = t;
gen_result = gen;
}
@ -699,6 +666,7 @@ namespace smt {
if (m_sort2k.find(s, r))
return r;
r = m_manager.mk_fresh_const("k", s);
m_model->register_aux_decl(r->get_decl());
m_sort2k.insert(s, r);
m_ks.push_back(r);
return r;
@ -734,14 +702,11 @@ namespace smt {
*/
bool assert_k_diseq_exceptions(app * k, ptr_vector<expr> const & exceptions) {
TRACE("assert_k_diseq_exceptions", tout << "assert_k_diseq_exceptions, " << "k: " << mk_pp(k, m_manager) << "\nexceptions:\n";
for (unsigned i = 0; i < exceptions.size(); i++) tout << mk_pp(exceptions[i], m_manager) << "\n";);
for (expr * e : exceptions) tout << mk_pp(e, m_manager) << "\n";);
expr * k_interp = get_k_interp(k);
if (k_interp == 0)
return false;
ptr_vector<expr>::const_iterator it = exceptions.begin();
ptr_vector<expr>::const_iterator end = exceptions.end();
for (; it != end; ++it) {
expr * ex = *it;
for (expr * ex : exceptions) {
expr * ex_val = eval(ex, true);
if (!m_manager.are_distinct(k_interp, ex_val)) {
SASSERT(m_new_constraints);
@ -806,10 +771,7 @@ namespace smt {
expr_ref one(m_manager);
one = ps->mk_one();
ptr_vector<expr> const & exceptions = n->get_exceptions();
ptr_vector<expr>::const_iterator it = exceptions.begin();
ptr_vector<expr>::const_iterator end = exceptions.end();
for (; it != end; ++it) {
expr * e = *it;
for (expr * e : exceptions) {
expr_ref e_plus_1(m_manager);
expr_ref e_minus_1(m_manager);
TRACE("mf_simp_bug", tout << "e:\n" << mk_ismt2_pp(e, m_manager) << "\none:\n" << mk_ismt2_pp(one, m_manager) << "\n";);
@ -825,10 +787,8 @@ namespace smt {
instantiation_set const * s = n->get_instantiation_set();
obj_hashtable<expr> already_found;
obj_map<expr, unsigned> const & elems = s->get_elems();
obj_map<expr, unsigned>::iterator it = elems.begin();
obj_map<expr, unsigned>::iterator end = elems.end();
for (; it != end; ++it) {
expr * t = (*it).m_key;
for (auto const& kv : elems) {
expr * t = kv.m_key;
expr * t_val = eval(t, true);
if (t_val && !already_found.contains(t_val)) {
values.push_back(t_val);
@ -836,10 +796,7 @@ namespace smt {
}
}
TRACE("model_finder_bug", tout << "values for the instantiation_set of @" << n->get_id() << "\n";
ptr_buffer<expr>::const_iterator it = values.begin();
ptr_buffer<expr>::const_iterator end = values.end();
for (; it != end; ++it) {
expr * v = *it;
for (expr * v : values) {
tout << mk_pp(v, m_manager) << "\n";
});
}
@ -941,10 +898,7 @@ namespace smt {
}
void mk_projections() {
ptr_vector<node>::const_iterator it = m_root_nodes.begin();
ptr_vector<node>::const_iterator end = m_root_nodes.end();
for (; it != end; ++it) {
node * n = *it;
for (node * n : m_root_nodes) {
SASSERT(n->is_root());
if (n->is_mono_proj())
mk_mono_proj(n);
@ -957,10 +911,8 @@ namespace smt {
\brief Store in r the partial functions that have A_f_i nodes.
*/
void collect_partial_funcs(func_decl_set & r) {
key2node::iterator it = m_A_f_is.begin();
key2node::iterator end = m_A_f_is.end();
for (; it != end; ++it) {
func_decl * f = to_func_decl((*it).m_key.first);
for (auto const& kv : m_A_f_is) {
func_decl * f = to_func_decl(kv.m_key.first);
if (!r.contains(f)) {
func_interp * fi = m_model->get_func_interp(f);
if (fi == 0) {
@ -983,10 +935,7 @@ namespace smt {
for more details.
*/
void mk_sorts_finite() {
ptr_vector<node>::const_iterator it = m_root_nodes.begin();
ptr_vector<node>::const_iterator end = m_root_nodes.end();
for (; it != end; ++it) {
node * n = *it;
for (node * n : m_root_nodes) {
SASSERT(n->is_root());
sort * s = n->get_sort();
if (m_manager.is_uninterp(s) &&
@ -998,13 +947,10 @@ namespace smt {
}
}
void add_elem_to_empty_inst_sets() {
ptr_vector<node>::const_iterator it = m_root_nodes.begin();
ptr_vector<node>::const_iterator end = m_root_nodes.end();
void add_elem_to_empty_inst_sets() {
obj_map<sort, expr*> sort2elems;
ptr_vector<node> need_fresh;
for (; it != end; ++it) {
node * n = *it;
for (node * n : m_root_nodes) {
SASSERT(n->is_root());
instantiation_set const * s = n->get_instantiation_set();
TRACE("model_finder", s->display(tout););
@ -1047,10 +993,7 @@ namespace smt {
*/
void collect_root_nodes() {
m_root_nodes.reset();
ptr_vector<node>::const_iterator it = m_nodes.begin();
ptr_vector<node>::const_iterator end = m_nodes.end();
for (; it != end; ++it) {
node * n = *it;
for (node * n : m_nodes) {
if (n->is_root())
m_root_nodes.push_back(n);
}
@ -1085,10 +1028,7 @@ namespace smt {
collected in the beginning of fix_model().
*/
void complete_partial_funcs(func_decl_set const & partial_funcs) {
func_decl_set::iterator it = partial_funcs.begin();
func_decl_set::iterator end = partial_funcs.end();
for (; it != end; ++it) {
func_decl * f = *it;
for (func_decl * f : partial_funcs) {
// Complete the current interpretation
m_model->complete_partial_func(f);
@ -1129,10 +1069,7 @@ namespace smt {
}
void mk_inverses() {
ptr_vector<node>::const_iterator it = m_root_nodes.begin();
ptr_vector<node>::const_iterator end = m_root_nodes.end();
for (; it != end; ++it) {
node * n = *it;
for (node * n : m_root_nodes) {
SASSERT(n->is_root());
mk_inverse(n);
}
@ -1360,16 +1297,14 @@ namespace smt {
ps = bs;
instantiation_set const * from_s = from->get_instantiation_set();
obj_map<expr, unsigned> const & elems_s = from_s->get_elems();
obj_map<expr, unsigned>::iterator it = elems_s.begin();
obj_map<expr, unsigned>::iterator end = elems_s.end();
for (; it != end; ++it) {
expr * n = (*it).m_key;
for (auto const& kv : elems_s) {
expr * n = kv.m_key;
expr_ref n_k(m_offset.get_manager());
if (PLUS)
ps->mk_add(n, m_offset, n_k);
else
ps->mk_sub(n, m_offset, n_k);
to->insert(n_k, (*it).m_value);
to->insert(n_k, kv.m_value);
}
}
@ -1414,10 +1349,7 @@ namespace smt {
app * nested_array = to_app(auf_arr->get_arg(0));
ptr_buffer<enode> nested_arrays;
get_auf_arrays(nested_array, ctx, nested_arrays);
ptr_buffer<enode>::const_iterator it = nested_arrays.begin();
ptr_buffer<enode>::const_iterator end = nested_arrays.end();
for (; it != end; ++it) {
enode * curr = *it;
for (enode * curr : nested_arrays) {
enode_vector::iterator it2 = curr->begin_parents();
enode_vector::iterator end2 = curr->end_parents();
for (; it2 != end2; ++it2) {
@ -1433,6 +1365,7 @@ namespace smt {
class select_var : public qinfo {
protected:
ast_manager & m_manager;
array_util m_array;
app * m_select; // It must satisfy is_auf_select... see bool is_auf_select(expr * t) const
unsigned m_arg_i;
unsigned m_var_j;
@ -1441,13 +1374,13 @@ namespace smt {
func_decl * get_array_func_decl(app * ground_array, auf_solver & s) {
expr * ground_array_interp = s.eval(ground_array, false);
if (ground_array_interp != 0 && s.get_model()->is_as_array(ground_array_interp))
return to_func_decl(to_app(ground_array_interp)->get_decl()->get_parameter(0).get_ast());
if (ground_array_interp != 0 && m_array.is_as_array(ground_array_interp))
return m_array.get_as_array_func_decl(ground_array_interp);
return 0;
}
public:
select_var(ast_manager & m, app * s, unsigned i, unsigned j):m_manager(m), m_select(s), m_arg_i(i), m_var_j(j) {}
select_var(ast_manager & m, app * s, unsigned i, unsigned j):m_manager(m), m_array(m), m_select(s), m_arg_i(i), m_var_j(j) {}
virtual ~select_var() {}
virtual char const * get_kind() const {
@ -1470,16 +1403,12 @@ namespace smt {
get_auf_arrays(get_array(), ctx, arrays);
TRACE("select_var",
tout << "enodes matching: "; display(tout); tout << "\n";
ptr_buffer<enode>::const_iterator it = arrays.begin();
ptr_buffer<enode>::const_iterator end = arrays.end();
for (; it != end; ++it) {
tout << "#" << (*it)->get_owner()->get_id() << "\n" << mk_pp((*it)->get_owner(), m_manager) << "\n";
for (enode* n : arrays) {
tout << "#" << n->get_owner()->get_id() << "\n" << mk_pp(n->get_owner(), m_manager) << "\n";
});
node * n1 = s.get_uvar(q, m_var_j);
ptr_buffer<enode>::const_iterator it = arrays.begin();
ptr_buffer<enode>::const_iterator end = arrays.end();
for (; it != end; ++it) {
app * ground_array = (*it)->get_owner();
for (enode* n : arrays) {
app * ground_array = n->get_owner();
func_decl * f = get_array_func_decl(ground_array, s);
if (f) {
SASSERT(m_arg_i >= 1);
@ -1492,10 +1421,7 @@ namespace smt {
virtual void populate_inst_sets(quantifier * q, auf_solver & s, context * ctx) {
ptr_buffer<enode> arrays;
get_auf_arrays(get_array(), ctx, arrays);
ptr_buffer<enode>::const_iterator it = arrays.begin();
ptr_buffer<enode>::const_iterator end = arrays.end();
for (; it != end; ++it) {
enode * curr = (*it);
for (enode * curr : arrays) {
app * ground_array = curr->get_owner();
func_decl * f = get_array_func_decl(ground_array, s);
if (f) {
@ -1778,11 +1704,9 @@ namespace smt {
void insert_qinfo(qinfo * qi) {
// I'm assuming the number of qinfo's per quantifier is small. So, the linear search is not a big deal.
scoped_ptr<qinfo> q(qi);
ptr_vector<qinfo>::iterator it = m_qinfo_vect.begin();
ptr_vector<qinfo>::iterator end = m_qinfo_vect.end();
for (; it != end; ++it) {
for (qinfo* qi2 : m_qinfo_vect) {
checkpoint();
if (qi->is_equal(*it)) {
if (qi->is_equal(qi2)) {
return;
}
}
@ -1876,22 +1800,16 @@ namespace smt {
out << "IS_AUF: " << m_is_auf << ", has x=y: " << m_has_x_eq_y << "\n";
out << "unary function fragment: " << unary_function_fragment() << "\n";
out << "ng decls: ";
func_decl_set::iterator it1 = m_ng_decls.begin();
func_decl_set::iterator end1 = m_ng_decls.end();
for (; it1 != end1; ++it1) {
out << (*it1)->get_name() << " ";
for (func_decl * f : m_ng_decls) {
out << f->get_name() << " ";
}
out << "\ninfo bits:\n";
ptr_vector<qinfo>::const_iterator it2 = m_qinfo_vect.begin();
ptr_vector<qinfo>::const_iterator end2 = m_qinfo_vect.end();
for (; it2 != end2; ++it2) {
out << " "; (*it2)->display(out); out << "\n";
for (qinfo* qi : m_qinfo_vect) {
out << " "; qi->display(out); out << "\n";
}
out << "\nmacros:\n";
ptr_vector<cond_macro>::const_iterator it3 = m_cond_macros.begin();
ptr_vector<cond_macro>::const_iterator end3 = m_cond_macros.end();
for (; it3 != end3; ++it3) {
out << " "; (*it3)->display(out); out << "\n";
for (cond_macro* cm : m_cond_macros) {
out << " "; cm->display(out); out << "\n";
}
}
@ -1900,23 +1818,19 @@ namespace smt {
// make sure a node exists for each variable.
s.get_uvar(m_flat_q, i);
}
ptr_vector<qinfo>::const_iterator it = m_qinfo_vect.begin();
ptr_vector<qinfo>::const_iterator end = m_qinfo_vect.end();
for (; it != end; ++it) {
(*it)->process_auf(m_flat_q, s, ctx);
for (qinfo * qi : m_qinfo_vect) {
qi->process_auf(m_flat_q, s, ctx);
}
}
void populate_inst_sets(auf_solver & s, context * ctx) {
ptr_vector<qinfo>::const_iterator it = m_qinfo_vect.begin();
ptr_vector<qinfo>::const_iterator end = m_qinfo_vect.end();
for (; it != end; ++it)
(*it)->populate_inst_sets(m_flat_q, s, ctx);
for (qinfo * qi : m_qinfo_vect) {
qi->populate_inst_sets(m_flat_q, s, ctx);
}
// second pass
it = m_qinfo_vect.begin();
for (; it != end; ++it) {
for (qinfo * qi : m_qinfo_vect) {
checkpoint();
(*it)->populate_inst_sets2(m_flat_q, s, ctx);
qi->populate_inst_sets2(m_flat_q, s, ctx);
}
}
@ -1929,14 +1843,9 @@ namespace smt {
if (m_uvar_inst_sets != 0)
return;
m_uvar_inst_sets = alloc(ptr_vector<instantiation_set>);
ptr_vector<qinfo>::const_iterator it = m_qinfo_vect.begin();
ptr_vector<qinfo>::const_iterator end = m_qinfo_vect.end();
for (; it != end; ++it)
(*it)->populate_inst_sets(m_flat_q, m_the_one, *m_uvar_inst_sets, ctx);
ptr_vector<instantiation_set>::iterator it2 = m_uvar_inst_sets->begin();
ptr_vector<instantiation_set>::iterator end2 = m_uvar_inst_sets->end();
for (; it2 != end2; ++it2) {
instantiation_set * s = *it2;
for (qinfo* qi : m_qinfo_vect)
qi->populate_inst_sets(m_flat_q, m_the_one, *m_uvar_inst_sets, ctx);
for (instantiation_set * s : *m_uvar_inst_sets) {
if (s != 0)
s->mk_inverse(ev);
}
@ -2230,9 +2139,7 @@ namespace smt {
expr * a = to_app(t)->get_arg(0);
if (!is_ground(a) && !is_auf_select(a))
return false;
unsigned num_args = to_app(t)->get_num_args();
for (unsigned i = 1; i < num_args; i++) {
expr * arg = to_app(t)->get_arg(i);
for (expr * arg : *to_app(t)) {
if (!is_ground(arg) && !is_var(arg))
return false;
}
@ -2258,9 +2165,9 @@ namespace smt {
}
}
else {
unsigned num_args = t->get_num_args();
for (unsigned i = 0; i < num_args; i++)
visit_term(t->get_arg(i));
for (expr * arg : *t) {
visit_term(arg);
}
}
}
@ -2577,10 +2484,7 @@ namespace smt {
\brief Return true if \c f is in (qs\{q})
*/
bool contains(func_decl * f, ptr_vector<quantifier> const & qs, quantifier * q) {
ptr_vector<quantifier>::const_iterator it = qs.begin();
ptr_vector<quantifier>::const_iterator end = qs.end();
for (; it != end; ++it) {
quantifier * other = *it;
for (quantifier * other : qs) {
if (q == other)
continue;
quantifier_info * other_qi = get_qinfo(other);
@ -2619,13 +2523,11 @@ namespace smt {
virtual bool process(ptr_vector<quantifier> const & qs, ptr_vector<quantifier> & new_qs, ptr_vector<quantifier> & residue) {
bool removed = false;
ptr_vector<quantifier>::const_iterator it = qs.begin();
ptr_vector<quantifier>::const_iterator end = qs.end();
for (; it != end; ++it) {
if (process(*it, qs))
for (quantifier* q : qs) {
if (process(q, qs))
removed = true;
else
new_qs.push_back(*it);
new_qs.push_back(q);
}
return removed;
}
@ -2774,20 +2676,15 @@ namespace smt {
void register_decls_as_forbidden(quantifier * q) {
quantifier_info * qi = get_qinfo(q);
func_decl_set const & ng_decls = qi->get_ng_decls();
func_decl_set::iterator it = ng_decls.begin();
func_decl_set::iterator end = ng_decls.end();
for (; it != end; ++it) {
m_forbidden.insert(*it);
for (func_decl* f : ng_decls) {
m_forbidden.insert(f);
}
}
void preprocess(ptr_vector<quantifier> const & qs, ptr_vector<quantifier> & qcandidates, ptr_vector<quantifier> & non_qcandidates) {
ptr_vector<quantifier> curr(qs);
while (true) {
ptr_vector<quantifier>::iterator it = curr.begin();
ptr_vector<quantifier>::iterator end = curr.end();
for (; it != end; ++it) {
quantifier * q = *it;
for (quantifier * q : curr) {
if (is_candidate(q)) {
qcandidates.push_back(q);
}
@ -2805,16 +2702,10 @@ namespace smt {
}
void mk_q_f_defs(ptr_vector<quantifier> const & qs) {
ptr_vector<quantifier>::const_iterator it = qs.begin();
ptr_vector<quantifier>::const_iterator end = qs.end();
for (; it != end; ++it) {
quantifier * q = *it;
for (quantifier * q : qs) {
quantifier_info * qi = get_qinfo(q);
func_decl_set const & ng_decls = qi->get_ng_decls();
func_decl_set::iterator it2 = ng_decls.begin();
func_decl_set::iterator end2 = ng_decls.end();
for (; it2 != end2; ++it2) {
func_decl * f = *it2;
for (func_decl* f : ng_decls) {
if (!m_forbidden.contains(f))
insert_q_f(q, f);
}
@ -2831,40 +2722,30 @@ namespace smt {
}
static void display_quantifier_set(std::ostream & out, quantifier_set const * s) {
quantifier_set::iterator it = s->begin();
quantifier_set::iterator end = s->end();
for (; it != end; ++it) {
quantifier * q = *it;
for (quantifier* q : *s) {
out << q->get_qid() << " ";
}
out << "\n";
}
void display_qcandidates(std::ostream & out, ptr_vector<quantifier> const & qcandidates) const {
ptr_vector<quantifier>::const_iterator it1 = qcandidates.begin();
ptr_vector<quantifier>::const_iterator end1 = qcandidates.end();
for (; it1 != end1; ++it1) {
quantifier * q = *it1;
for (quantifier * q : qcandidates) {
out << q->get_qid() << " ->\n" << mk_pp(q, m_manager) << "\n";
quantifier_info * qi = get_qinfo(q);
qi->display(out);
out << "------\n";
}
out << "Sets Q_f\n";
q_f::iterator it2 = m_q_f.begin();
q_f::iterator end2 = m_q_f.end();
for (; it2 != end2; ++it2) {
func_decl * f = (*it2).m_key;
quantifier_set * s = (*it2).m_value;
for (auto const& kv : m_q_f) {
func_decl * f = kv.m_key;
quantifier_set * s = kv.m_value;
out << f->get_name() << " -> "; display_quantifier_set(out, s);
}
out << "Sets Q_{f = def}\n";
q_f_def::iterator it3 = m_q_f_def.begin();
q_f_def::iterator end3 = m_q_f_def.end();
for (; it3 != end3; ++it3) {
func_decl * f = (*it3).get_key1();
expr * def = (*it3).get_key2();
quantifier_set * s = (*it3).get_value();
for (auto const& kv : m_q_f_def) {
func_decl * f = kv.get_key1();
expr * def = kv.get_key2();
quantifier_set * s = kv.get_value();
out << f->get_name() << " " << mk_pp(def, m_manager) << " ->\n"; display_quantifier_set(out, s);
}
}
@ -2899,32 +2780,23 @@ namespace smt {
void display_search_state(std::ostream & out) const {
out << "fs:\n";
f2def::iterator it3 = m_fs.begin();
f2def::iterator end3 = m_fs.end();
for (; it3 != end3; ++it3) {
out << (*it3).m_key->get_name() << " ";
for (auto const& kv : m_fs) {
out << kv.m_key->get_name() << " ";
}
out << "\nsatisfied:\n";
qsset::iterator it = m_satisfied.begin();
qsset::iterator end = m_satisfied.end();
for (; it != end; ++it) {
out << (*it)->get_qid() << " ";
for (auto q : m_satisfied) {
out << q->get_qid() << " ";
}
out << "\nresidue:\n";
qset::iterator it2 = m_residue.begin();
qset::iterator end2 = m_residue.end();
for (; it2 != end2; ++it2) {
out << (*it2)->get_qid() << " ";
for (auto q : m_residue) {
out << q->get_qid() << " ";
}
out << "\n";
}
bool check_satisfied_residue_invariant() {
DEBUG_CODE(
qsset::iterator it = m_satisfied.begin();
qsset::iterator end = m_satisfied.end();
for (; it != end; ++it) {
quantifier * q = *it;
for (quantifier * q : m_satisfied) {
SASSERT(!m_residue.contains(q));
quantifier_info * qi = get_qinfo(q);
SASSERT(qi != 0);
@ -2939,10 +2811,7 @@ namespace smt {
SASSERT(check_satisfied_residue_invariant());
quantifier_set * q_f = get_q_f(f);
quantifier_set * q_f_def = get_q_f_def(f, def);
quantifier_set::iterator it = q_f_def->begin();
quantifier_set::iterator end = q_f_def->end();
for (; it != end; ++it) {
quantifier * q = *it;
for (quantifier * q : *q_f_def) {
if (!m_satisfied.contains(q)) {
useful = true;
m_residue.erase(q);
@ -2954,10 +2823,7 @@ namespace smt {
}
if (!useful)
return false;
it = q_f->begin();
end = q_f->end();
for (; it != end; ++it) {
quantifier * q = *it;
for (quantifier * q : *q_f) {
if (!m_satisfied.contains(q)) {
m_residue.insert(q);
}
@ -2971,10 +2837,7 @@ namespace smt {
The candidates must not be elements of m_fs.
*/
void get_candidates_from_residue(func_decl_set & candidates) {
qset::iterator it = m_residue.begin();
qset::iterator end = m_residue.end();
for (; it != end; ++it) {
quantifier * q = *it;
for (quantifier * q : m_residue) {
quantifier_info * qi = get_qinfo(q);
quantifier_info::macro_iterator it2 = qi->begin_macros();
@ -3003,10 +2866,7 @@ namespace smt {
display_search_state(tout););
expr_set * s = get_f_defs(f);
expr_set::iterator it = s->begin();
expr_set::iterator end = s->end();
for (; it != end; ++it) {
expr * def = *it;
for (expr * def : *s) {
SASSERT(!m_fs.contains(f));
@ -3041,17 +2901,13 @@ namespace smt {
get_candidates_from_residue(candidates);
TRACE("model_finder_hint", tout << "candidates from residue:\n";
func_decl_set::iterator it = candidates.begin();
func_decl_set::iterator end = candidates.end();
for (; it != end; ++it) {
tout << (*it)->get_name() << " ";
for (func_decl * f : candidates) {
tout << f->get_name() << " ";
}
tout << "\n";);
func_decl_set::iterator it = candidates.begin();
func_decl_set::iterator end = candidates.end();
for (; it != end; ++it) {
greedy(*it, depth);
for (func_decl* f : candidates) {
greedy(f, depth);
}
}
@ -3071,10 +2927,7 @@ namespace smt {
\brief Copy the quantifiers from qcandidates to new_qs that are not in m_satisfied.
*/
void copy_non_satisfied(ptr_vector<quantifier> const & qcandidates, ptr_vector<quantifier> & new_qs) {
ptr_vector<quantifier>::const_iterator it = qcandidates.begin();
ptr_vector<quantifier>::const_iterator end = qcandidates.end();
for (; it != end; ++it) {
quantifier * q = *it;
for (quantifier * q : qcandidates) {
if (!m_satisfied.contains(q))
new_qs.push_back(q);
}
@ -3085,11 +2938,9 @@ namespace smt {
quantifiers in m_satisfied.
*/
void set_interp() {
f2def::iterator it = m_fs.begin();
f2def::iterator end = m_fs.end();
for (; it != end; ++it) {
func_decl * f = (*it).m_key;
expr * def = (*it).m_value;
for (auto const& kv : m_fs) {
func_decl * f = kv.m_key;
expr * def = kv.m_value;
set_else_interp(f, def);
}
}
@ -3113,10 +2964,7 @@ namespace smt {
}
mk_q_f_defs(qcandidates);
TRACE("model_finder_hint", tout << "starting hint-solver search using:\n"; display_qcandidates(tout, qcandidates););
func_decl_set::iterator it = m_candidates.begin();
func_decl_set::iterator end = m_candidates.end();
for (; it != end; ++it) {
func_decl * f = *it;
for (func_decl * f : m_candidates) {
try {
process(f);
}
@ -3195,10 +3043,7 @@ namespace smt {
typedef std::pair<cond_macro *, quantifier *> mq_pair;
void collect_candidates(ptr_vector<quantifier> const & qs, obj_map<func_decl, mq_pair> & full_macros, func_decl_set & cond_macros) {
ptr_vector<quantifier>::const_iterator it = qs.begin();
ptr_vector<quantifier>::const_iterator end = qs.end();
for (; it != end; ++it) {
quantifier * q = *it;
for (quantifier * q : qs) {
quantifier_info * qi = get_qinfo(q);
quantifier_info::macro_iterator it2 = qi->begin_macros();
quantifier_info::macro_iterator end2 = qi->end_macros();
@ -3221,12 +3066,10 @@ namespace smt {
}
void process_full_macros(obj_map<func_decl, mq_pair> const & full_macros, obj_hashtable<quantifier> & removed) {
obj_map<func_decl, mq_pair>::iterator it = full_macros.begin();
obj_map<func_decl, mq_pair>::iterator end = full_macros.end();
for (; it != end; ++it) {
func_decl * f = (*it).m_key;
cond_macro * m = (*it).m_value.first;
quantifier * q = (*it).m_value.second;
for (auto const& kv : full_macros) {
func_decl * f = kv.m_key;
cond_macro * m = kv.m_value.first;
quantifier * q = kv.m_value.second;
SASSERT(m->is_unconditional());
if (add_macro(f, m->get_def())) {
get_qinfo(q)->set_the_one(f);
@ -3238,10 +3081,7 @@ namespace smt {
void process(func_decl * f, ptr_vector<quantifier> const & qs, obj_hashtable<quantifier> & removed) {
expr_ref fi_else(m_manager);
ptr_buffer<quantifier> to_remove;
ptr_vector<quantifier>::const_iterator it = qs.begin();
ptr_vector<quantifier>::const_iterator end = qs.end();
for (; it != end; ++it) {
quantifier * q = *it;
for (quantifier * q : qs) {
if (removed.contains(q))
continue;
cond_macro * m = get_macro_for(f, q);
@ -3259,20 +3099,16 @@ namespace smt {
}
}
if (fi_else.get() != 0 && add_macro(f, fi_else)) {
ptr_buffer<quantifier>::iterator it2 = to_remove.begin();
ptr_buffer<quantifier>::iterator end2 = to_remove.end();
for (; it2 != end2; ++it2) {
get_qinfo(*it2)->set_the_one(f);
removed.insert(*it2);
for (quantifier * q : to_remove) {
get_qinfo(q)->set_the_one(f);
removed.insert(q);
}
}
}
void process_cond_macros(func_decl_set const & cond_macros, ptr_vector<quantifier> const & qs, obj_hashtable<quantifier> & removed) {
func_decl_set::iterator it = cond_macros.begin();
func_decl_set::iterator end = cond_macros.end();
for (; it != end; ++it) {
process(*it, qs, removed);
for (func_decl * f : cond_macros) {
process(f, qs, removed);
}
}
@ -3287,10 +3123,7 @@ namespace smt {
process_full_macros(full_macros, removed);
process_cond_macros(cond_macros, qs, removed);
ptr_vector<quantifier>::const_iterator it = qs.begin();
ptr_vector<quantifier>::const_iterator end = qs.end();
for (; it != end; ++it) {
quantifier * q = *it;
for (quantifier * q : qs) {
if (removed.contains(q))
continue;
new_qs.push_back(q);
@ -3409,10 +3242,7 @@ namespace smt {
}
void model_finder::collect_relevant_quantifiers(ptr_vector<quantifier> & qs) const {
ptr_vector<quantifier>::const_iterator it = m_quantifiers.begin();
ptr_vector<quantifier>::const_iterator end = m_quantifiers.end();
for (; it != end; ++it) {
quantifier * q = *it;
for (quantifier * q : m_quantifiers) {
if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true)
qs.push_back(q);
}
@ -3422,26 +3252,19 @@ namespace smt {
m_auf_solver->reset();
m_auf_solver->set_model(m);
ptr_vector<quantifier>::const_iterator it = qs.begin();
ptr_vector<quantifier>::const_iterator end = qs.end();
for (; it != end; ++it) {
quantifier * q = *it;
for (quantifier * q : qs) {
quantifier_info * qi = get_quantifier_info(q);
qi->process_auf(*(m_auf_solver.get()), m_context);
}
m_auf_solver->mk_instantiation_sets();
it = qs.begin();
for (; it != end; ++it) {
quantifier * q = *it;
for (quantifier * q : qs) {
quantifier_info * qi = get_quantifier_info(q);
qi->populate_inst_sets(*(m_auf_solver.get()), m_context);
}
m_auf_solver->fix_model(m_new_constraints);
TRACE("model_finder",
ptr_vector<quantifier>::const_iterator it = qs.begin();
ptr_vector<quantifier>::const_iterator end = qs.end();
for (; it != end; ++it) {
quantifier * q = *it;
for (quantifier * q : qs) {
quantifier_info * qi = get_quantifier_info(q);
quantifier * fq = qi->get_flat_q();
tout << "#" << fq->get_id() << " ->\n" << mk_pp(fq, m_manager) << "\n";

5
src/smt/theory_fpa.cpp
View file

@ -237,8 +237,9 @@ namespace smt {
if (m_fpa_util.is_fp(e)) {
expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) };
res = m_bv_util.mk_concat(3, cargs);
m_th_rw((expr_ref&)res);
expr_ref tmp(m_bv_util.mk_concat(3, cargs), m);
m_th_rw(tmp);
res = to_app(tmp);
}
else {
sort * es = m.get_sort(e);

14
src/smt/theory_seq.cpp
View file

@ -427,7 +427,7 @@ bool theory_seq::branch_unit_variable() {
break;
}
}
CTRACE("seq", result, "branch unit variable";);
CTRACE("seq", result, tout << "branch unit variable";);
return result;
}
@ -3224,26 +3224,32 @@ void theory_seq::add_indexof_axiom(expr* i) {
/*
let r = replace(a, s, t)
a = "" => s = "" or r = a
contains(a, s) or r = a
s = "" => r = t+a
tightest_prefix(s, x)
(contains(a, s) -> r = xty & a = xsy) &
(!contains(a, s) -> r = a)
*/
void theory_seq::add_replace_axiom(expr* r) {
context& ctx = get_context();
expr* a = 0, *s = 0, *t = 0;
VERIFY(m_util.str.is_replace(r, a, s, t));
expr_ref x = mk_skolem(m_indexof_left, a, s);
expr_ref y = mk_skolem(m_indexof_right, a, s);
expr_ref xty = mk_concat(x, t, y);
expr_ref xsy = mk_concat(x, s, y);
literal a_emp = mk_eq_empty(a, true);
literal s_emp = mk_eq_empty(s, true);
literal cnt = mk_literal(m_util.str.mk_contains(a, s));
literal a_emp = mk_eq_empty(a);
literal s_emp = mk_eq_empty(s);
add_axiom(~a_emp, s_emp, mk_seq_eq(r, a));
add_axiom(cnt, mk_seq_eq(r, a));
add_axiom(~s_emp, mk_seq_eq(r, mk_concat(t, a)));
add_axiom(~cnt, a_emp, s_emp, mk_seq_eq(a, xsy));
add_axiom(~cnt, a_emp, s_emp, mk_seq_eq(r, xty));
ctx.force_phase(cnt);
tightest_prefix(s, x);
}
@ -3546,7 +3552,7 @@ bool theory_seq::get_length(expr* e, rational& val) const {
}
}
}
CTRACE("seq", !val.is_int(), "length is not an integer\n";);
CTRACE("seq", !val.is_int(), tout << "length is not an integer\n";);
return val.is_int();
}

85
src/smt/theory_str.cpp
View file

@ -185,6 +185,7 @@ namespace smt {
m_trail.push_back(e);
//TRACE("str", tout << "done asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;);
}
expr * theory_str::rewrite_implication(expr * premise, expr * conclusion) {
@ -1449,6 +1450,7 @@ namespace smt {
argumentsValid_terms.push_back(m.mk_not(m_autil.mk_ge(
m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)),
zero)));
// len >= 0
argumentsValid_terms.push_back(m_autil.mk_ge(substrLen, zero));
@ -1488,6 +1490,7 @@ namespace smt {
// Case 3: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) < strlen(base)
// ==> base = t2.t3.t4 AND len(t2) = pos AND len(t3) = len AND (Substr ...) = t3
expr_ref t2(mk_str_var("t2"), m);
expr_ref t3(mk_str_var("t3"), m);
expr_ref t4(mk_str_var("t4"), m);
@ -1509,6 +1512,86 @@ namespace smt {
assert_axiom(finalAxiom);
}
#if 0
// rewrite
// requires to add th_rewriter to assert_axiom to enforce normal form.
void theory_str::instantiate_axiom_Substr(enode * e) {
context & ctx = get_context();
ast_manager & m = get_manager();
expr* substrBase = 0;
expr* substrPos = 0;
expr* substrLen = 0;
app * expr = e->get_owner();
if (axiomatized_terms.contains(expr)) {
TRACE("str", tout << "already set up Substr axiom for " << mk_pp(expr, m) << std::endl;);
return;
}
axiomatized_terms.insert(expr);
TRACE("str", tout << "instantiate Substr axiom for " << mk_pp(expr, m) << std::endl;);
VERIFY(u.str.is_extract(expr, substrBase, substrPos, substrLen));
expr_ref zero(m_autil.mk_numeral(rational::zero(), true), m);
expr_ref minusOne(m_autil.mk_numeral(rational::minus_one(), true), m);
SASSERT(zero);
SASSERT(minusOne);
expr_ref_vector argumentsValid_terms(m);
// pos >= 0
argumentsValid_terms.push_back(m_autil.mk_ge(substrPos, zero));
// pos < strlen(base)
// --> pos + -1*strlen(base) < 0
argumentsValid_terms.push_back(m.mk_not(m_autil.mk_ge(
m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)),
zero)));
// len >= 0
argumentsValid_terms.push_back(m_autil.mk_ge(substrLen, zero));
// (pos+len) >= strlen(base)
// --> pos + len + -1*strlen(base) >= 0
expr_ref lenOutOfBounds(m_autil.mk_ge(
m_autil.mk_add(substrPos, substrLen, m_autil.mk_mul(minusOne, mk_strlen(substrBase))),
zero), m);
expr_ref argumentsValid = mk_and(argumentsValid_terms);
// Case 1: pos < 0 or pos >= strlen(base) or len < 0
// ==> (Substr ...) = ""
expr_ref case1_premise(m.mk_not(argumentsValid), m);
expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m);
expr_ref case1(m.mk_implies(case1_premise, case1_conclusion), m);
// Case 2: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) >= strlen(base)
// ==> base = t0.t1 AND len(t0) = pos AND (Substr ...) = t1
expr_ref t0(mk_str_var("t0"), m);
expr_ref t1(mk_str_var("t1"), m);
expr_ref case2_conclusion(m.mk_and(
ctx.mk_eq_atom(substrBase, mk_concat(t0,t1)),
ctx.mk_eq_atom(mk_strlen(t0), substrPos),
ctx.mk_eq_atom(expr, t1)), m);
expr_ref case2(m.mk_implies(m.mk_and(argumentsValid, lenOutOfBounds), case2_conclusion), m);
// Case 3: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) < strlen(base)
// ==> base = t2.t3.t4 AND len(t2) = pos AND len(t3) = len AND (Substr ...) = t3
expr_ref t2(mk_str_var("t2"), m);
expr_ref t3(mk_str_var("t3"), m);
expr_ref t4(mk_str_var("t4"), m);
expr_ref_vector case3_conclusion_terms(m);
case3_conclusion_terms.push_back(ctx.mk_eq_atom(substrBase, mk_concat(t2, mk_concat(t3, t4))));
case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t2), substrPos));
case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen));
case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3));
expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m);
expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m);
assert_axiom(case1);
assert_axiom(case2);
assert_axiom(case3);
}
#endif
void theory_str::instantiate_axiom_Replace(enode * e) {
context & ctx = get_context();
ast_manager & m = get_manager();
@ -8484,7 +8567,7 @@ namespace smt {
} else {
TRACE("str", tout << "integer theory has no assignment for " << mk_pp(a, m) << std::endl;);
expr_ref is_zero(ctx.mk_eq_atom(a, m_autil.mk_int(0)), m);
literal is_zero_l = mk_literal(is_zero);
/* literal is_zero_l = */ mk_literal(is_zero);
axiomAdd = true;
TRACE("str", ctx.display(tout););
// NOT_IMPLEMENTED_YET();