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

Merge pull request #8 from Z3Prover/master

Browse source 
merge with Z3Prover/z3
This commit is contained in:
trinhmt 2018-06-27 18:10:54 +08:00 • committed by GitHub
commit 54a9482716
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
145 changed files with 2605 additions and 1588 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/cached_var_subst.cpp
View file

@ -63,7 +63,7 @@ void cached_var_subst::operator()(quantifier * qa, unsigned num_bindings, smt::e
SASSERT(entry->get_data().m_value == 0);
try {
m_proc(qa->get_expr(), new_key->m_num_bindings, new_key->m_bindings, result);
result = m_proc(qa->get_expr(), new_key->m_num_bindings, new_key->m_bindings);
}
catch (...) {
// CMW: The var_subst reducer was interrupted and m_instances is

46
src/smt/fingerprints.cpp
View file

@ -20,9 +20,10 @@ Revision History:
namespace smt {
fingerprint::fingerprint(region & r, void * d, unsigned d_h, unsigned n, enode * const * args):
fingerprint::fingerprint(region & r, void * d, unsigned d_h, expr* def, unsigned n, enode * const * args):
m_data(d),
m_data_hash(d_h),
m_def(def),
m_num_args(n),
m_args(nullptr) {
m_args = new (r) enode*[n];
@ -50,8 +51,18 @@ namespace smt {
m_dummy.m_args = m_tmp.c_ptr();
return &m_dummy;
}
std::ostream& operator<<(std::ostream& out, fingerprint const& f) {
out << f.get_data_hash() << " " << " num_args " << f.get_num_args() << " ";
for (enode const * arg : f) {
out << " " << arg->get_owner_id();
}
out << "\n";
return out;
}
fingerprint * fingerprint_set::insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args) {
fingerprint * fingerprint_set::insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def) {
fingerprint * d = mk_dummy(data, data_hash, num_args, args);
if (m_set.contains(d))
return nullptr;
@ -66,11 +77,10 @@ namespace smt {
tout << "\n";);
return nullptr;
}
TRACE("fingerprint_bug", tout << "2) inserting: " << data_hash << " num_args: " << num_args;
for (unsigned i = 0; i < num_args; i++) tout << " " << args[i]->get_owner_id();
tout << "\n";);
fingerprint * f = new (m_region) fingerprint(m_region, data, data_hash, num_args, d->m_args);
TRACE("fingerprint_bug", tout << "2) inserting: " << *d;);
fingerprint * f = new (m_region) fingerprint(m_region, data, data_hash, def, num_args, d->m_args);
m_fingerprints.push_back(f);
m_defs.push_back(def);
m_set.insert(f);
return f;
}
@ -89,6 +99,7 @@ namespace smt {
void fingerprint_set::reset() {
m_set.reset();
m_fingerprints.reset();
m_defs.reset();
}
void fingerprint_set::push_scope() {
@ -104,20 +115,15 @@ namespace smt {
for (unsigned i = old_size; i < size; i++)
m_set.erase(m_fingerprints[i]);
m_fingerprints.shrink(old_size);
m_defs.shrink(old_size);
m_scopes.shrink(new_lvl);
}
void fingerprint_set::display(std::ostream & out) const {
out << "fingerprints:\n";
SASSERT(m_set.size() == m_fingerprints.size());
ptr_vector<fingerprint>::const_iterator it = m_fingerprints.begin();
ptr_vector<fingerprint>::const_iterator end = m_fingerprints.end();
for (; it != end; ++it) {
fingerprint const * f = *it;
out << f->get_data() << " #" << f->get_data_hash();
for (unsigned i = 0; i < f->get_num_args(); i++)
out << " #" << f->get_arg(i)->get_owner_id();
out << "\n";
for (fingerprint const * f : m_fingerprints) {
out << f->get_data() << " " << *f;
}
}
@ -126,10 +132,7 @@ namespace smt {
\brief Slow function for checking if there is a fingerprint congruent to (data args[0] ... args[num_args-1])
*/
bool fingerprint_set::slow_contains(void const * data, unsigned data_hash, unsigned num_args, enode * const * args) const {
ptr_vector<fingerprint>::const_iterator it = m_fingerprints.begin();
ptr_vector<fingerprint>::const_iterator end = m_fingerprints.end();
for (; it != end; ++it) {
fingerprint const * f = *it;
for (fingerprint const* f : m_fingerprints) {
if (f->get_data() != data)
continue;
if (f->get_num_args() != num_args)
@ -139,12 +142,7 @@ namespace smt {
if (f->get_arg(i)->get_root() != args[i]->get_root())
break;
if (i == num_args) {
TRACE("missing_instance_detail", tout << "found instance data: " << data << "=" << f->get_data() << " hash: " << f->get_data_hash();
for (unsigned i = 0; i < num_args; i++) {
tout << " " << f->get_arg(i)->get_owner_id() << ":" << f->get_arg(i)->get_root()->get_owner_id() << "="
<< args[i]->get_owner_id() << ":" << args[i]->get_root()->get_owner_id();
}
tout << "\n";);
TRACE("missing_instance_detail", tout << "found instance data: " << data << "=" << *f;);
return true;
}
}

13
src/smt/fingerprints.h
View file

@ -20,6 +20,7 @@ Revision History:
#define FINGERPRINTS_H_
#include "smt/smt_enode.h"
#include "util/util.h"
namespace smt {
@ -27,18 +28,23 @@ namespace smt {
protected:
void * m_data;
unsigned m_data_hash;
expr* m_def;
unsigned m_num_args;
enode * * m_args;
friend class fingerprint_set;
fingerprint() {}
public:
fingerprint(region & r, void * d, unsigned d_hash, unsigned n, enode * const * args);
fingerprint(region & r, void * d, unsigned d_hash, expr* def, unsigned n, enode * const * args);
void * get_data() const { return m_data; }
expr * get_def() const { return m_def; }
unsigned get_data_hash() const { return m_data_hash; }
unsigned get_num_args() const { return m_num_args; }
enode * const * get_args() const { return m_args; }
enode * get_arg(unsigned idx) const { SASSERT(idx < m_num_args); return m_args[idx]; }
enode * const * begin() const { return m_args; }
enode * const * end() const { return begin() + get_num_args(); }
friend std::ostream& operator<<(std::ostream& out, fingerprint const& f);
};
class fingerprint_set {
@ -60,6 +66,7 @@ namespace smt {
region & m_region;
set m_set;
ptr_vector<fingerprint> m_fingerprints;
expr_ref_vector m_defs;
unsigned_vector m_scopes;
ptr_vector<enode> m_tmp;
fingerprint m_dummy;
@ -67,8 +74,8 @@ namespace smt {
fingerprint * mk_dummy(void * data, unsigned data_hash, unsigned num_args, enode * const * args);
public:
fingerprint_set(region & r):m_region(r) {}
fingerprint * insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args);
fingerprint_set(ast_manager& m, region & r): m_region(r), m_defs(m) {}
fingerprint * insert(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def);
unsigned size() const { return m_fingerprints.size(); }
bool contains(void * data, unsigned data_hash, unsigned num_args, enode * const * args);
void reset();

83
src/smt/mam.cpp
View file

@ -16,15 +16,16 @@ Author:
Revision History:
--*/
#include "smt/mam.h"
#include "smt/smt_context.h"
#include <algorithm>
#include "util/pool.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "util/trail.h"
#include "util/stopwatch.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_smt2_pp.h"
#include<algorithm>
#include "smt/mam.h"
#include "smt/smt_context.h"
// #define _PROFILE_MAM
@ -569,9 +570,8 @@ namespace smt {
if (m_context) {
ast_manager & m = m_context->get_manager();
out << "patterns:\n";
for (expr* p : m_patterns) {
out << mk_pp(p, m) << "\n";
}
for (app* a : m_patterns)
out << mk_pp(a, m) << "\n";
}
#endif
out << "function: " << m_root_lbl->get_name();
@ -1482,8 +1482,8 @@ namespace smt {
}
if (num_instr > SIMPLE_SEQ_THRESHOLD || (curr != nullptr && curr->m_opcode == CHOOSE))
simple = false;
for (unsigned reg : m_to_reset)
m_registers[reg] = 0;
for (unsigned r : m_to_reset)
m_registers[r] = 0;
return weight;
}
@ -1998,19 +1998,19 @@ namespace smt {
TRACE("trigger_bug", tout << "execute for code tree:\n"; t->display(tout););
init(t);
if (t->filter_candidates()) {
for (enode * app : t->get_candidates()) {
for (enode* app : t->get_candidates()) {
if (!app->is_marked() && app->is_cgr()) {
execute_core(t, app);
app->set_mark();
}
}
for (enode * app : t->get_candidates()) {
for (enode* app : t->get_candidates()) {
if (app->is_marked())
app->unset_mark();
}
}
else {
for (enode * app : t->get_candidates()) {
for (enode* app : t->get_candidates()) {
TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";);
if (app->is_cgr()) {
TRACE("trigger_bug", tout << "is_cgr\n";);
@ -2797,7 +2797,7 @@ namespace smt {
void display_trees(std::ostream & out, const ptr_vector<code_tree> & trees) {
unsigned lbl = 0;
for (code_tree* tree : trees) {
for (code_tree * tree : trees) {
if (tree) {
out << "tree for f" << lbl << "\n";
out << *tree;
@ -3143,10 +3143,7 @@ namespace smt {
m_trail_stack.push(set_bitvector_trail<mam_impl>(m_is_clbl, lbl_id));
SASSERT(m_is_clbl[lbl_id]);
unsigned h = m_lbl_hasher(lbl);
enode_vector::const_iterator it = m_context.begin_enodes_of(lbl);
enode_vector::const_iterator end = m_context.end_enodes_of(lbl);
for (; it != end; ++it) {
enode * app = *it;
for (enode* app : m_context.enodes_of(lbl)) {
if (m_context.is_relevant(app)) {
update_lbls(app, h);
TRACE("mam_bug", tout << "updating labels of: #" << app->get_owner_id() << "\n";
@ -3188,10 +3185,7 @@ namespace smt {
SASSERT(m_is_plbl[lbl_id]);
SASSERT(is_plbl(lbl));
unsigned h = m_lbl_hasher(lbl);
enode_vector::const_iterator it = m_context.begin_enodes_of(lbl);
enode_vector::const_iterator end = m_context.end_enodes_of(lbl);
for (; it != end; ++it) {
enode * app = *it;
for (enode * app : m_context.enodes_of(lbl)) {
if (m_context.is_relevant(app))
update_children_plbls(app, h);
}
@ -3677,18 +3671,12 @@ namespace smt {
approx_set & plbls = r1->get_plbls();
approx_set & clbls = r2->get_lbls();
if (!plbls.empty() && !clbls.empty()) {
approx_set::iterator it1 = plbls.begin();
approx_set::iterator end1 = plbls.end();
for (; it1 != end1; ++it1) {
for (unsigned plbl1 : plbls) {
if (m_context.get_cancel_flag()) {
break;
}
unsigned plbl1 = *it1;
SASSERT(plbls.may_contain(plbl1));
approx_set::iterator it2 = clbls.begin();
approx_set::iterator end2 = clbls.end();
for (; it2 != end2; ++it2) {
unsigned lbl2 = *it2;
for (unsigned lbl2 : clbls) {
SASSERT(clbls.may_contain(lbl2));
collect_parents(r1, m_pc[plbl1][lbl2]);
}
@ -3699,14 +3687,12 @@ namespace smt {
void match_new_patterns() {
TRACE("mam_new_pat", tout << "matching new patterns:\n";);
m_tmp_trees_to_delete.reset();
svector<qp_pair>::iterator it1 = m_new_patterns.begin();
svector<qp_pair>::iterator end1 = m_new_patterns.end();
for (; it1 != end1; ++it1) {
for (auto const& kv : m_new_patterns) {
if (m_context.get_cancel_flag()) {
break;
}
quantifier * qa = it1->first;
app * mp = it1->second;
quantifier * qa = kv.first;
app * mp = kv.second;
SASSERT(m_ast_manager.is_pattern(mp));
app * p = to_app(mp->get_arg(0));
func_decl * lbl = p->get_decl();
@ -3723,19 +3709,13 @@ namespace smt {
}
}
ptr_vector<func_decl>::iterator it2 = m_tmp_trees_to_delete.begin();
ptr_vector<func_decl>::iterator end2 = m_tmp_trees_to_delete.end();
for (; it2 != end2; ++it2) {
func_decl * lbl = *it2;
for (func_decl * lbl : m_tmp_trees_to_delete) {
unsigned lbl_id = lbl->get_decl_id();
code_tree * tmp_tree = m_tmp_trees[lbl_id];
SASSERT(tmp_tree != 0);
SASSERT(m_context.get_num_enodes_of(lbl) > 0);
m_interpreter.init(tmp_tree);
enode_vector::const_iterator it3 = m_context.begin_enodes_of(lbl);
enode_vector::const_iterator end3 = m_context.end_enodes_of(lbl);
for (; it3 != end3; ++it3) {
enode * app = *it3;
for (enode * app : m_context.enodes_of(lbl)) {
if (m_context.is_relevant(app))
m_interpreter.execute_core(tmp_tree, app);
}
@ -3824,10 +3804,7 @@ namespace smt {
void pop_scope(unsigned num_scopes) override {
if (!m_to_match.empty()) {
ptr_vector<code_tree>::iterator it = m_to_match.begin();
ptr_vector<code_tree>::iterator end = m_to_match.end();
for (; it != end; ++it) {
code_tree * t = *it;
for (code_tree* t : m_to_match) {
t->reset_candidates();
}
m_to_match.reset();
@ -3860,10 +3837,7 @@ namespace smt {
void match() override {
TRACE("trigger_bug", tout << "match\n"; display(tout););
ptr_vector<code_tree>::iterator it = m_to_match.begin();
ptr_vector<code_tree>::iterator end = m_to_match.end();
for (; it != end; ++it) {
code_tree * t = *it;
for (code_tree* t : m_to_match) {
SASSERT(t->has_candidates());
m_interpreter.execute(t);
t->reset_candidates();
@ -3884,10 +3858,7 @@ namespace smt {
if (t) {
m_interpreter.init(t);
func_decl * lbl = t->get_root_lbl();
enode_vector::const_iterator it2 = m_context.begin_enodes_of(lbl);
enode_vector::const_iterator end2 = m_context.end_enodes_of(lbl);
for (; it2 != end2; ++it2) {
enode * curr = *it2;
for (enode * curr : m_context.enodes_of(lbl)) {
if (use_irrelevant || m_context.is_relevant(curr))
m_interpreter.execute_core(t, curr);
}
@ -3924,7 +3895,7 @@ namespace smt {
#endif
unsigned min_gen, max_gen;
m_interpreter.get_min_max_top_generation(min_gen, max_gen);
m_context.add_instance(qa, pat, num_bindings, bindings, max_generation, min_gen, max_gen, used_enodes);
m_context.add_instance(qa, pat, num_bindings, bindings, nullptr, max_generation, min_gen, max_gen, used_enodes);
}
bool is_shared(enode * n) const override {

4
src/smt/params/theory_array_params.h
View file

@ -40,6 +40,7 @@ struct theory_array_params {
bool m_array_always_prop_upward;
bool m_array_lazy_ieq;
unsigned m_array_lazy_ieq_delay;
bool m_array_fake_support; // fake support for all array operations to pretend they are satisfiable.
theory_array_params():
m_array_canonize_simplify(false),
@ -52,7 +53,8 @@ struct theory_array_params {
m_array_cg(false),
m_array_always_prop_upward(true), // UPWARDs filter is broken... TODO: fix it
m_array_lazy_ieq(false),
m_array_lazy_ieq_delay(10) {
m_array_lazy_ieq_delay(10),
m_array_fake_support(false) {
}

14
src/smt/proto_model/array_factory.cpp
View file

@ -17,11 +17,11 @@ Revision History:
--*/
#include "smt/proto_model/array_factory.h"
#include "ast/array_decl_plugin.h"
#include "smt/proto_model/proto_model.h"
#include "model/func_interp.h"
#include "ast/ast_pp.h"
#include "model/func_interp.h"
#include "smt/proto_model/array_factory.h"
#include "smt/proto_model/proto_model.h"
func_decl * mk_aux_decl_for_array_sort(ast_manager & m, sort * s) {
ptr_buffer<sort> domain;
@ -67,9 +67,13 @@ expr * array_factory::get_some_value(sort * s) {
return *(set->begin());
func_interp * fi;
expr * val = mk_array_interp(s, fi);
#if 0
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)));
#else
fi->set_else(m_model.get_some_value(get_array_range(s)));
#endif
return val;
}
@ -143,9 +147,13 @@ expr * array_factory::get_fresh_value(sort * s) {
// easy case
func_interp * fi;
expr * val = mk_array_interp(s, fi);
#if 0
ptr_buffer<expr> args;
get_some_args_for(s, args);
fi->insert_entry(args.c_ptr(), range_val);
#else
fi->set_else(range_val);
#endif
return val;
}
else {

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

@ -18,13 +18,15 @@ Revision History:
--*/
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/rewriter/var_subst.h"
#include "ast/well_sorted.h"
#include "ast/used_symbols.h"
#include "ast/for_each_expr.h"
#include "ast/rewriter/var_subst.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_eval(*this),
@ -75,7 +77,7 @@ expr * proto_model::mk_some_interp_for(func_decl * d) {
register_decl(d, r);
}
else {
func_interp * new_fi = alloc(func_interp, m_manager, d->get_arity());
func_interp * new_fi = alloc(func_interp, m, d->get_arity());
new_fi->set_else(r);
register_decl(d, new_fi);
}
@ -86,6 +88,7 @@ expr * proto_model::mk_some_interp_for(func_decl * d) {
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);
TRACE("model_evaluator", model_v2_pp(tout, *this, true););
try {
m_eval(e, result);
return true;
@ -120,10 +123,10 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au
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";);
TRACE("model_bug", tout << "cleaning up:\n" << mk_pp(fi_else, m) << "\n";);
obj_map<expr, expr*> cache;
expr_ref_vector trail(m_manager);
expr_ref_vector trail(m);
ptr_buffer<expr, 128> todo;
ptr_buffer<expr> args;
todo.push_back(fi_else);
@ -165,7 +168,7 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au
TRACE("model_bug", tout << f->get_name() << "\n";);
found_aux_fs.insert(f);
}
expr_ref new_t(m_manager);
expr_ref new_t(m);
new_t = m_rewrite.mk_app(f, args.size(), args.c_ptr());
if (t != new_t.get())
trail.push_back(new_t);
@ -235,7 +238,7 @@ value_factory * proto_model::get_factory(family_id fid) {
}
void proto_model::freeze_universe(sort * s) {
SASSERT(m_manager.is_uninterp(s));
SASSERT(m.is_uninterp(s));
m_user_sort_factory->freeze_universe(s);
}
@ -270,11 +273,11 @@ sort * proto_model::get_uninterpreted_sort(unsigned idx) const {
in the model.
*/
bool proto_model::is_finite(sort * s) const {
return m_manager.is_uninterp(s) && m_user_sort_factory->is_finite(s);
return m.is_uninterp(s) && m_user_sort_factory->is_finite(s);
}
expr * proto_model::get_some_value(sort * s) {
if (m_manager.is_uninterp(s)) {
if (m.is_uninterp(s)) {
return m_user_sort_factory->get_some_value(s);
}
else {
@ -288,7 +291,7 @@ expr * proto_model::get_some_value(sort * s) {
}
bool proto_model::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
if (m_manager.is_uninterp(s)) {
if (m.is_uninterp(s)) {
return m_user_sort_factory->get_some_values(s, v1, v2);
}
else {
@ -302,7 +305,7 @@ bool proto_model::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
}
expr * proto_model::get_fresh_value(sort * s) {
if (m_manager.is_uninterp(s)) {
if (m.is_uninterp(s)) {
return m_user_sort_factory->get_fresh_value(s);
}
else {
@ -318,8 +321,8 @@ expr * proto_model::get_fresh_value(sort * s) {
}
void proto_model::register_value(expr * n) {
sort * s = m_manager.get_sort(n);
if (m_manager.is_uninterp(s)) {
sort * s = m.get_sort(n);
if (m.is_uninterp(s)) {
m_user_sort_factory->register_value(n);
}
else {
@ -374,15 +377,15 @@ void proto_model::complete_partial_funcs(bool use_fresh) {
model * proto_model::mk_model() {
TRACE("proto_model", model_v2_pp(tout << "mk_model\n", *this););
model * m = alloc(model, m_manager);
model * mdl = alloc(model, m);
for (auto const& kv : m_interp) {
m->register_decl(kv.m_key, kv.m_value);
mdl->register_decl(kv.m_key, kv.m_value);
}
for (auto const& kv : m_finterp) {
m->register_decl(kv.m_key, kv.m_value);
m_manager.dec_ref(kv.m_key);
mdl->register_decl(kv.m_key, kv.m_value);
m.dec_ref(kv.m_key);
}
m_finterp.reset(); // m took the ownership of the func_interp's
@ -390,10 +393,11 @@ model * proto_model::mk_model() {
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";);
TRACE("proto_model", tout << "copying uninterpreted sorts...\n" << mk_pp(s, m) << "\n";);
ptr_vector<expr> const& buf = get_universe(s);
m->register_usort(s, buf.size(), buf.c_ptr());
mdl->register_usort(s, buf.size(), buf.c_ptr());
}
return m;
return mdl;
}

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

@ -38,6 +38,7 @@ Revision History:
#include "util/params.h"
#include "ast/rewriter/th_rewriter.h"
class proto_model : public model_core {
plugin_manager<value_factory> m_factories;
user_sort_factory * m_user_sort_factory;

30
src/smt/qi_queue.cpp
View file

@ -148,7 +148,7 @@ namespace smt {
}
void qi_queue::instantiate() {
unsigned since_last_check = 0;
unsigned since_last_check = 0;
for (entry & curr : m_new_entries) {
fingerprint * f = curr.m_qb;
quantifier * qa = static_cast<quantifier*>(f->get_data());
@ -169,7 +169,6 @@ namespace smt {
// Periodically check if we didn't run out of time/memory.
if (since_last_check++ > 100) {
if (m_context.resource_limits_exceeded()) {
// verbose_stream() << "EXCEEDED...\n";
break;
}
since_last_check = 0;
@ -182,16 +181,7 @@ namespace smt {
void qi_queue::display_instance_profile(fingerprint * f, quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned proof_id, unsigned generation) {
if (m_manager.has_trace_stream()) {
m_manager.trace_stream() << "[instance] ";
#if 1
m_manager.trace_stream() << static_cast<void*>(f);
#else
for (unsigned i = 0; i < num_bindings; i++) {
// I don't want to use mk_pp because it creates expressions for pretty printing.
// This nasty side-effect may change the behavior of Z3.
m_manager.trace_stream() << " #" << bindings[i]->get_owner_id();
}
#endif
if (m_manager.proofs_enabled())
m_manager.trace_stream() << " #" << proof_id;
m_manager.trace_stream() << " ; " << generation;
@ -208,10 +198,7 @@ namespace smt {
ent.m_instantiated = true;
TRACE("qi_queue_profile",
tout << q->get_qid() << ", gen: " << generation;
for (unsigned i = 0; i < num_bindings; i++) tout << " #" << bindings[i]->get_owner_id();
tout << "\n";);
TRACE("qi_queue_profile", tout << q->get_qid() << ", gen: " << generation << " " << *f;);
if (m_checker.is_sat(q->get_expr(), num_bindings, bindings)) {
TRACE("checker", tout << "instance already satisfied\n";);
@ -288,6 +275,9 @@ namespace smt {
unsigned gen = get_new_gen(q, generation, ent.m_cost);
display_instance_profile(f, q, num_bindings, bindings, proof_id, gen);
m_context.internalize_instance(lemma, pr1, gen);
if (f->get_def()) {
m_context.internalize(f->get_def(), true);
}
TRACE_CODE({
static unsigned num_useless = 0;
if (m_manager.is_or(lemma)) {
@ -412,10 +402,7 @@ namespace smt {
void qi_queue::display_delayed_instances_stats(std::ostream & out) const {
obj_map<quantifier, delayed_qa_info> qa2info;
ptr_vector<quantifier> qas;
svector<entry>::const_iterator it = m_delayed_entries.begin();
svector<entry>::const_iterator end = m_delayed_entries.end();
for (; it != end; ++it) {
entry const & e = *it;
for (entry const & e : m_delayed_entries) {
if (e.m_instantiated)
continue;
quantifier * qa = static_cast<quantifier*>(e.m_qb->get_data());
@ -433,10 +420,7 @@ namespace smt {
}
qa2info.insert(qa, info);
}
ptr_vector<quantifier>::iterator it2 = qas.begin();
ptr_vector<quantifier>::iterator end2 = qas.end();
for (; it2 != end2; ++it2) {
quantifier * qa = *it2;
for (quantifier * qa : qas) {
delayed_qa_info info;
qa2info.find(qa, info);
out << qa->get_qid() << ": " << info.m_num << " [" << info.m_min_cost << ", " << info.m_max_cost << "]\n";

12
src/smt/smt_context.cpp
View file

@ -53,7 +53,7 @@ namespace smt {
m_flushing(false),
m_progress_callback(nullptr),
m_next_progress_sample(0),
m_fingerprints(m_region),
m_fingerprints(m, m_region),
m_b_internalized_stack(m),
m_e_internalized_stack(m),
m_final_check_idx(0),
@ -1785,9 +1785,9 @@ namespace smt {
return m_fingerprints.contains(q, q->get_id(), num_bindings, bindings);
}
bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation,
bool context::add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation,
unsigned min_top_generation, unsigned max_top_generation, ptr_vector<enode> & used_enodes) {
return m_qmanager->add_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_top_generation, used_enodes);
return m_qmanager->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_top_generation, used_enodes);
}
void context::rescale_bool_var_activity() {
@ -2932,7 +2932,7 @@ namespace smt {
void context::assert_expr_core(expr * e, proof * pr) {
if (get_cancel_flag()) return;
SASSERT(is_well_sorted(m_manager, e));
TRACE("begin_assert_expr", tout << mk_pp(e, m_manager) << "\n";);
TRACE("begin_assert_expr", tout << this << " " << mk_pp(e, m_manager) << "\n";);
TRACE("begin_assert_expr_ll", tout << mk_ll_pp(e, m_manager) << "\n";);
pop_to_base_lvl();
if (pr == nullptr)
@ -4401,9 +4401,9 @@ namespace smt {
for (unsigned i = 0; !get_cancel_flag() && i < m_asserted_formulas.get_num_formulas(); ++i) {
expr* e = m_asserted_formulas.get_formula(i);
if (is_quantifier(e)) {
TRACE("context", tout << mk_pp(e, m) << "\n";);
quantifier* q = to_quantifier(e);
if (!m.is_rec_fun_def(q)) continue;
TRACE("context", tout << mk_pp(e, m) << "\n";);
SASSERT(q->get_num_patterns() == 2);
expr* fn = to_app(q->get_pattern(0))->get_arg(0);
expr* body = to_app(q->get_pattern(1))->get_arg(0);
@ -4417,7 +4417,7 @@ namespace smt {
expr_ref bodyr(m);
var_subst sub(m, true);
TRACE("context", tout << expr_ref(q, m) << " " << subst << "\n";);
sub(body, subst.size(), subst.c_ptr(), bodyr);
bodyr = sub(body, subst.size(), subst.c_ptr());
func_decl* f = to_app(fn)->get_decl();
func_interp* fi = alloc(func_interp, m, f->get_arity());
fi->set_else(bodyr);

18
src/smt/smt_context.h
View file

@ -116,6 +116,7 @@ namespace smt {
plugin_manager<theory> m_theories; // mapping from theory_id -> theory
ptr_vector<theory> m_theory_set; // set of theories for fast traversal
vector<enode_vector> m_decl2enodes; // decl -> enode (for decls with arity > 0)
enode_vector m_empty_vector;
cg_table m_cg_table;
dyn_ack_manager m_dyn_ack_manager;
struct new_eq {
@ -456,6 +457,8 @@ namespace smt {
theory * get_theory(theory_id th_id) const {
return m_theories.get_plugin(th_id);
}
ptr_vector<theory> const& theories() const { return m_theories.plugins(); }
ptr_vector<theory>::const_iterator begin_theories() const {
return m_theories.begin();
@ -517,6 +520,11 @@ namespace smt {
return id < m_decl2enodes.size() ? m_decl2enodes[id].size() : 0;
}
enode_vector const& enodes_of(func_decl const * d) const {
unsigned id = d->get_decl_id();
return id < m_decl2enodes.size() ? m_decl2enodes[id] : m_empty_vector;
}
enode_vector::const_iterator begin_enodes_of(func_decl const * decl) const {
unsigned id = decl->get_decl_id();
return id < m_decl2enodes.size() ? m_decl2enodes[id].begin() : nullptr;
@ -527,6 +535,8 @@ namespace smt {
return id < m_decl2enodes.size() ? m_decl2enodes[id].end() : nullptr;
}
ptr_vector<enode> const& enodes() const { return m_enodes; }
ptr_vector<enode>::const_iterator begin_enodes() const {
return m_enodes.begin();
}
@ -553,8 +563,8 @@ namespace smt {
return m_asserted_formulas.has_quantifiers();
}
fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args) {
return m_fingerprints.insert(data, data_hash, num_args, args);
fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def = 0) {
return m_fingerprints.insert(data, data_hash, num_args, args, def);
}
theory_id get_var_theory(bool_var v) const {
@ -736,6 +746,8 @@ namespace smt {
void internalize_quantifier(quantifier * q, bool gate_ctx);
void internalize_lambda(quantifier * q);
void internalize_formula_core(app * n, bool gate_ctx);
void set_merge_tf(enode * n, bool_var v, bool is_new_var);
@ -957,7 +969,7 @@ namespace smt {
bool contains_instance(quantifier * q, unsigned num_bindings, enode * const * bindings);
bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation,
bool add_instance(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, expr* def, unsigned max_generation,
unsigned min_top_generation, unsigned max_top_generation, ptr_vector<enode> & used_enodes);
void set_global_generation(unsigned generation) { m_generation = generation; }

30
src/smt/smt_internalizer.cpp
View file

@ -329,6 +329,9 @@ namespace smt {
SASSERT(is_quantifier(n) || is_app(n));
internalize_formula(n, gate_ctx);
}
else if (is_lambda(n)) {
internalize_lambda(to_quantifier(n));
}
else {
SASSERT(is_app(n));
SASSERT(!gate_ctx);
@ -514,7 +517,7 @@ namespace smt {
CTRACE("internalize_quantifier_zero", q->get_weight() == 0, tout << mk_pp(q, m_manager) << "\n";);
SASSERT(gate_ctx); // limitation of the current implementation
SASSERT(!b_internalized(q));
SASSERT(q->is_forall());
SASSERT(is_forall(q));
SASSERT(check_patterns(q));
bool_var v = mk_bool_var(q);
unsigned generation = m_generation;
@ -528,6 +531,31 @@ namespace smt {
m_qmanager->add(q, generation);
}
void context::internalize_lambda(quantifier * q) {
UNREACHABLE();
#if 0
TRACE("internalize_quantifier", tout << mk_pp(q, m_manager) << "\n";);
SASSERT(is_lambda(q));
app_ref lam_name(m_manager.mk_fresh_const("lambda", m_manager.get_sort(q)), m_manager);
enode * e = mk_enode(lam_name, true, false, false);
expr_ref eq(m_manager), lam_app(m_manager);
expr_ref_vector vars(m_manager);
vars.push_back(lam_name);
unsigned sz = q->get_num_decls();
for (unsigned i = 0; i < sz; ++i) {
vars.push_back(m_manager.mk_var(sz - i - 1, q->get_decl_sort(i)));
}
array_util autil(m_manager);
lam_app = autil.mk_select(vars.size(), vars.c_ptr());
eq = m_manager.mk_eq(lam_app, q->get_expr());
quantifier_ref fa(m_manager);
expr * patterns[1] = { m_manager.mk_pattern(lam_name) };
fa = m_manager.mk_forall(sz, q->get_decl_sorts(), q->get_decl_names(), eq, 0, m_manager.lambda_def_qid(), symbol::null, 1, patterns);
internalize_quantifier(fa, true);
#endif
}
/**
\brief Internalize gates and (uninterpreted and equality) predicates.
*/

256
src/smt/smt_model_checker.cpp
View file

@ -15,12 +15,19 @@ Author:
Revision History:
- to support lambdas/array models:
binding sk -> (as-array k!0)
then include definition for k!0 as part of binding.
Binding instance can be a pointer into m_pinned expressions.
--*/
#include "ast/normal_forms/pull_quant.h"
#include "ast/for_each_expr.h"
#include "ast/rewriter/var_subst.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/ast_pp.h"
#include "ast/array_decl_plugin.h"
#include "ast/ast_smt2_pp.h"
#include "smt/smt_model_checker.h"
#include "smt/smt_context.h"
@ -53,8 +60,8 @@ namespace smt {
}
void model_checker::set_qm(quantifier_manager & qm) {
SASSERT(m_qm == 0);
SASSERT(m_context == 0);
SASSERT(m_qm == nullptr);
SASSERT(m_context == nullptr);
m_qm = &qm;
m_context = &(m_qm->get_context());
}
@ -63,6 +70,13 @@ namespace smt {
\brief Return a term in the context that evaluates to val.
*/
expr * model_checker::get_term_from_ctx(expr * val) {
init_value2expr();
expr * t = nullptr;
m_value2expr.find(val, t);
return t;
}
void model_checker::init_value2expr() {
if (m_value2expr.empty()) {
// populate m_value2expr
for (auto const& kv : *m_root2value) {
@ -72,9 +86,28 @@ namespace smt {
m_value2expr.insert(val, n->get_owner());
}
}
expr * t = nullptr;
m_value2expr.find(val, t);
return t;
}
expr_ref model_checker::replace_value_from_ctx(expr * e) {
init_value2expr();
struct beta_reducer_cfg : default_rewriter_cfg {
model_checker& mc;
beta_reducer_cfg(model_checker& mc):mc(mc) {}
bool get_subst(expr * e, expr* & t, proof *& pr) {
t = nullptr; pr = nullptr;
mc.m_value2expr.find(e, t);
return t != nullptr;
}
};
struct beta_reducer : public rewriter_tpl<beta_reducer_cfg> {
beta_reducer_cfg m_cfg;
beta_reducer(model_checker& m):
rewriter_tpl<beta_reducer_cfg>(m.m, false, m_cfg), m_cfg(m) {}
};
beta_reducer br(*this);
expr_ref result(m);
br(e, result);
return result;
}
/**
@ -94,8 +127,6 @@ namespace smt {
m_aux_context->assert_expr(fml);
}
#define PP_DEPTH 8
/**
\brief Assert the negation of q after applying the interpretation in m_curr_model to the uninterpreted symbols in q.
@ -122,9 +153,8 @@ namespace smt {
}
}
expr_ref sk_body(m);
var_subst s(m);
s(tmp, subst_args.size(), subst_args.c_ptr(), sk_body);
expr_ref sk_body = s(tmp, subst_args.size(), subst_args.c_ptr());
expr_ref r(m);
r = m.mk_not(sk_body);
TRACE("model_checker", tout << "mk_neg_q_m:\n" << mk_ismt2_pp(r, m) << "\n";);
@ -132,37 +162,35 @@ namespace smt {
}
bool model_checker::add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv) {
if (cex == nullptr) {
if (cex == nullptr || sks.empty()) {
TRACE("model_checker", tout << "no model is available\n";);
return false;
}
array_util autil(m);
unsigned num_decls = q->get_num_decls();
// Remark: sks were created for the flat version of q.
SASSERT(sks.size() >= num_decls);
expr_ref_vector bindings(m);
expr_ref_vector bindings(m), defs(m);
expr_ref def(m);
bindings.resize(num_decls);
unsigned max_generation = 0;
for (unsigned i = 0; i < num_decls; i++) {
expr * sk = sks.get(num_decls - i - 1);
func_decl * sk_d = to_app(sk)->get_decl();
expr_ref sk_value(m);
sk_value = cex->get_const_interp(sk_d);
if (sk_value == 0) {
sk_value = cex->get_some_value(sk_d->get_range());
if (sk_value == 0) {
TRACE("model_checker", tout << "Could not get value for " << sk_d->get_name() << "\n";);
return false; // get_some_value failed... giving up
}
TRACE("model_checker", tout << "Got some value " << sk_value << "\n";);
expr_ref sk_value(cex->get_some_const_interp(sk_d), m);
if (!sk_value) {
TRACE("model_checker", tout << "Could not get value for " << sk_d->get_name() << "\n";);
return false; // get_some_value failed... giving up
}
TRACE("model_checker", tout << "Got some value " << sk_value << "\n";);
if (use_inv) {
unsigned sk_term_gen;
expr * sk_term = m_model_finder.get_inv(q, i, sk_value, sk_term_gen);
if (sk_term != nullptr) {
TRACE("model_checker", tout << "Found inverse " << mk_pp(sk_term, m) << "\n";);
SASSERT(!m.is_model_value(sk_term));
if (sk_term_gen > max_generation)
max_generation = sk_term_gen;
max_generation = std::max(sk_term_gen, max_generation);
sk_value = sk_term;
}
else {
@ -180,39 +208,48 @@ namespace smt {
TRACE("model_checker", tout << "value is private to model: " << sk_value << "\n";);
return false;
}
func_decl * f = nullptr;
if (autil.is_as_array(sk_value, f) && cex->get_func_interp(f)) {
expr_ref body(cex->get_func_interp(f)->get_interp(), m);
ptr_vector<sort> sorts(f->get_arity(), f->get_domain());
svector<symbol> names;
for (unsigned i = 0; i < f->get_arity(); ++i) {
names.push_back(symbol(i));
}
defined_names dn(m);
body = replace_value_from_ctx(body);
body = m.mk_lambda(sorts.size(), sorts.c_ptr(), names.c_ptr(), body);
// sk_value = m.mk_fresh_const(0, m.get_sort(sk_value)); // get rid of as-array
body = dn.mk_definition(body, to_app(sk_value));
defs.push_back(body);
}
bindings.set(num_decls - i - 1, sk_value);
}
TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: ";
for (unsigned i = 0; i < num_decls; i++) {
tout << mk_ismt2_pp(bindings[i].get(), m) << " ";
}
tout << "\n";);
TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: " << bindings << "\n" << defs << "\n";);
if (!defs.empty()) def = mk_and(defs);
max_generation = std::max(m_qm->get_generation(q), max_generation);
add_instance(q, bindings, max_generation);
add_instance(q, bindings, max_generation, def.get());
return true;
}
void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) {
void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation, expr* def) {
SASSERT(q->get_num_decls() == bindings.size());
for (expr* b : bindings)
m_pinned_exprs.push_back(b);
unsigned offset = m_pinned_exprs.size();
m_pinned_exprs.append(bindings);
m_pinned_exprs.push_back(q);
void * mem = m_new_instances_region.allocate(instance::get_obj_size(q->get_num_decls()));
instance * new_inst = new (mem) instance(q, bindings.c_ptr(), max_generation);
m_new_instances.push_back(new_inst);
m_pinned_exprs.push_back(def);
m_new_instances.push_back(instance(q, offset, def, max_generation));
}
void model_checker::operator()(expr *n) {
if (m.is_model_value(n) || m_autil.is_as_array(n)) {
if (m.is_model_value(n) /*|| m_autil.is_as_array(n)*/) {
throw is_model_value();
}
}
bool model_checker::contains_model_value(expr* n) {
if (m.is_model_value(n) || m_autil.is_as_array(n)) {
if (m.is_model_value(n) /*|| m_autil.is_as_array(n)*/) {
return true;
}
if (is_app(n) && to_app(n)->get_num_args() == 0) {
@ -230,16 +267,13 @@ namespace smt {
bool model_checker::add_blocking_clause(model * cex, expr_ref_vector & sks) {
SASSERT(cex != 0);
SASSERT(cex != nullptr);
expr_ref_buffer diseqs(m);
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);
if (sk_value == 0) {
sk_value = cex->get_some_value(sk_d->get_range());
if (sk_value == 0)
return false; // get_some_value failed... aborting add_blocking_clause
expr_ref sk_value(cex->get_some_const_interp(sk_d), m);
if (!sk_value) {
return false; // get_some_value failed... aborting add_blocking_clause
}
diseqs.push_back(m.mk_not(m.mk_eq(sk, sk_value)));
}
@ -250,40 +284,43 @@ namespace smt {
return true;
}
struct scoped_ctx_push {
context* c;
scoped_ctx_push(context* c): c(c) { c->push(); }
~scoped_ctx_push() { c->pop(1); }
};
/**
\brief Return true if q is satisfied by m_curr_model.
*/
bool model_checker::check(quantifier * q) {
SASSERT(!m_aux_context->relevancy());
m_aux_context->push();
scoped_ctx_push _push(m_aux_context.get());
quantifier * flat_q = get_flat_quantifier(q);
TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" <<
mk_ismt2_pp(flat_q->get_expr(), m) << "\n";);
TRACE("model_checker", tout << "model checking:\n" << expr_ref(q->get_expr(), m) << "\n" << expr_ref(flat_q->get_expr(), m) << "\n";);
expr_ref_vector sks(m);
assert_neg_q_m(flat_q, sks);
TRACE("model_checker", tout << "skolems:\n";
for (expr* sk : sks) {
tout << mk_ismt2_pp(sk, m) << " " << mk_pp(m.get_sort(sk), m) << "\n";
});
TRACE("model_checker", tout << "skolems:\n" << sks << "\n";);
flet<bool> l(m_aux_context->get_fparams().m_array_fake_support, true);
lbool r = m_aux_context->check();
TRACE("model_checker", tout << "[complete] model-checker result: " << to_sat_str(r) << "\n";);
if (r != l_true) {
m_aux_context->pop(1);
if (r != l_true) {
return r == l_false; // quantifier is satisfied by m_curr_model
}
model_ref complete_cex;
m_aux_context->get_model(complete_cex);
// try to find new instances using instantiation sets.
m_model_finder.restrict_sks_to_inst_set(m_aux_context.get(), q, sks);
unsigned num_new_instances = 0;
while (true) {
flet<bool> l(m_aux_context->get_fparams().m_array_fake_support, true);
lbool r = m_aux_context->check();
TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";);
if (r != l_true)
@ -307,7 +344,6 @@ namespace smt {
add_instance(q, complete_cex.get(), sks, false);
}
m_aux_context->pop(1);
return false;
}
@ -317,33 +353,29 @@ namespace smt {
expr* fn = to_app(q->get_pattern(0))->get_arg(0);
SASSERT(is_app(fn));
func_decl* f = to_app(fn)->get_decl();
enode_vector::const_iterator it = m_context->begin_enodes_of(f);
enode_vector::const_iterator end = m_context->end_enodes_of(f);
bool is_undef = false;
expr_ref_vector args(m);
unsigned num_decls = q->get_num_decls();
args.resize(num_decls, nullptr);
var_subst sub(m);
expr_ref tmp(m), result(m);
for (; it != end; ++it) {
if (m_context->is_relevant(*it)) {
app* e = (*it)->get_owner();
for (enode* n : m_context->enodes_of(f)) {
if (m_context->is_relevant(n)) {
app* e = n->get_owner();
SASSERT(e->get_num_args() == num_decls);
for (unsigned i = 0; i < num_decls; ++i) {
args[i] = e->get_arg(i);
}
sub(q->get_expr(), num_decls, args.c_ptr(), tmp);
tmp = sub(q->get_expr(), num_decls, args.c_ptr());
m_curr_model->eval(tmp, result, true);
if (strict_rec_fun ? !m.is_true(result) : m.is_false(result)) {
add_instance(q, args, 0);
add_instance(q, args, 0, nullptr);
return false;
}
TRACE("model_checker", tout << tmp << "\nevaluates to:\n" << result << "\n";);
// if (!m.is_true(result)) is_undef = true;
TRACE("model_checker", tout << tmp << "\nevaluates to:\n" << result << "\n";);
}
}
return !is_undef;
return true;
}
void model_checker::init_aux_context() {
@ -359,7 +391,7 @@ namespace smt {
}
bool model_checker::check(proto_model * md, obj_map<enode, app *> const & root2value) {
SASSERT(md != 0);
SASSERT(md != nullptr);
m_root2value = &root2value;
@ -390,7 +422,6 @@ namespace smt {
check_quantifiers(false, found_relevant, num_failures);
if (found_relevant)
m_iteration_idx++;
@ -415,35 +446,47 @@ namespace smt {
return num_failures == 0;
}
//
// (repeated from defined_names.cpp)
// NB. The pattern for lambdas is incomplete.
// consider store(a, i, v) == \lambda j . if i = j then v else a[j]
// the instantiation rules for store(a, i, v) are:
// sotre(a, i, v)[j] = if i = j then v else a[j] with patterns {a[j], store(a, i, v)} { store(a, i, v)[j] }
// The first pattern is not included.
// TBD use a model-based scheme for exracting instantiations instead of
// using multi-patterns.
//
void model_checker::check_quantifiers(bool strict_rec_fun, bool& found_relevant, unsigned& num_failures) {
ptr_vector<quantifier>::const_iterator it = m_qm->begin_quantifiers();
ptr_vector<quantifier>::const_iterator end = m_qm->end_quantifiers();
for (; it != end; ++it) {
quantifier * q = *it;
if(!m_qm->mbqi_enabled(q)) continue;
for (quantifier * q : *m_qm) {
if (!(m_qm->mbqi_enabled(q) &&
m_context->is_relevant(q) &&
m_context->get_assignment(q) == l_true &&
!m.is_lambda_def(q))) {
continue;
}
TRACE("model_checker",
tout << "Check: " << mk_pp(q, m) << "\n";
tout << m_context->get_assignment(q) << "\n";);
if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) {
if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) {
verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n";
}
found_relevant = true;
if (m.is_rec_fun_def(q)) {
if (!check_rec_fun(q, strict_rec_fun)) {
TRACE("model_checker", tout << "checking recursive function failed\n";);
num_failures++;
}
}
else if (!check(q)) {
if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) {
IF_VERBOSE(0, verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n");
}
TRACE("model_checker", tout << "checking quantifier " << mk_pp(q, m) << " failed\n";);
if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) {
verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n";
}
found_relevant = true;
if (m.is_rec_fun_def(q)) {
if (!check_rec_fun(q, strict_rec_fun)) {
TRACE("model_checker", tout << "checking recursive function failed\n";);
num_failures++;
}
}
else if (!check(q)) {
if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) {
IF_VERBOSE(0, verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n");
}
TRACE("model_checker", tout << "checking quantifier " << mk_pp(q, m) << " failed\n";);
num_failures++;
}
}
}
@ -466,7 +509,6 @@ namespace smt {
void model_checker::reset_new_instances() {
m_pinned_exprs.reset();
m_new_instances.reset();
m_new_instances_region.reset();
}
void model_checker::reset() {
@ -477,32 +519,30 @@ namespace smt {
TRACE("model_checker_bug_detail", tout << "assert_new_instances, inconsistent: " << m_context->inconsistent() << "\n";);
ptr_buffer<enode> bindings;
ptr_vector<enode> dummy;
for (instance* inst : m_new_instances) {
quantifier * q = inst->m_q;
for (instance const& inst : m_new_instances) {
quantifier * q = inst.m_q;
if (m_context->b_internalized(q)) {
bindings.reset();
unsigned num_decls = q->get_num_decls();
unsigned gen = inst->m_generation;
unsigned gen = inst.m_generation;
unsigned offset = inst.m_bindings_offset;
for (unsigned i = 0; i < num_decls; i++) {
expr * b = inst->m_bindings[i];
expr * b = m_pinned_exprs.get(offset + i);
if (!m_context->e_internalized(b)) {
TRACE("model_checker_bug_detail", tout << "internalizing b:\n" << mk_pp(b, m) << "\n";);
TRACE("model_checker", tout << "internalizing b:\n" << mk_pp(b, m) << "\n";);
m_context->internalize(b, false, gen);
}
bindings.push_back(m_context->get_enode(b));
}
if (inst.m_def) {
m_context->internalize_assertion(inst.m_def, 0, gen);
}
TRACE("model_checker_bug_detail", tout << "instantiating... q:\n" << mk_pp(q, m) << "\n";
tout << "inconsistent: " << m_context->inconsistent() << "\n";
tout << "bindings:\n";
for (unsigned i = 0; i < num_decls; i++) {
expr * b = inst->m_bindings[i];
tout << mk_pp(b, m) << "\n";
});
TRACE("model_checker_instance",
expr_ref inst_expr(m);
instantiate(m, q, inst->m_bindings, inst_expr);
tout << "(assert " << mk_ismt2_pp(inst_expr, m) << ")\n";);
m_context->add_instance(q, nullptr, num_decls, bindings.c_ptr(), gen, gen, gen, dummy);
tout << "bindings:\n" << expr_ref_vector(m, num_decls, m_pinned_exprs.c_ptr() + offset) << "\n";);
m_context->add_instance(q, nullptr, num_decls, bindings.c_ptr(), inst.m_def, gen, gen, gen, dummy);
TRACE("model_checker_bug_detail", tout << "after instantiating, inconsistent: " << m_context->inconsistent() << "\n";);
}
}

19
src/smt/smt_model_checker.h
View file

@ -21,12 +21,12 @@ Revision History:
#ifndef SMT_MODEL_CHECKER_H_
#define SMT_MODEL_CHECKER_H_
#include "util/obj_hashtable.h"
#include "ast/ast.h"
#include "ast/array_decl_plugin.h"
#include "util/obj_hashtable.h"
#include "ast/normal_forms/defined_names.h"
#include "smt/params/qi_params.h"
#include "smt/params/smt_params.h"
#include "util/region.h"
class proto_model;
class model;
@ -56,7 +56,9 @@ namespace smt {
friend class instantiation_set;
void init_aux_context();
void init_value2expr();
expr * get_term_from_ctx(expr * val);
expr_ref replace_value_from_ctx(expr * e);
void restrict_to_universe(expr * sk, obj_hashtable<expr> const & universe);
void assert_neg_q_m(quantifier * q, expr_ref_vector & sks);
bool add_blocking_clause(model * cex, expr_ref_vector & sks);
@ -67,15 +69,12 @@ namespace smt {
struct instance {
quantifier * m_q;
unsigned m_generation;
expr * m_bindings[0];
static unsigned get_obj_size(unsigned num_bindings) { return sizeof(instance) + num_bindings * sizeof(expr*); }
instance(quantifier * q, expr * const * bindings, unsigned gen):m_q(q), m_generation(gen) {
memcpy(m_bindings, bindings, q->get_num_decls() * sizeof(expr*));
}
expr * m_def;
unsigned m_bindings_offset;
instance(quantifier * q, unsigned offset, expr* def, unsigned gen):m_q(q), m_generation(gen), m_def(def), m_bindings_offset(offset) {}
};
region m_new_instances_region;
ptr_vector<instance> m_new_instances;
svector<instance> m_new_instances;
expr_ref_vector m_pinned_exprs;
bool add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv);
void reset_new_instances();
@ -86,7 +85,7 @@ namespace smt {
struct is_model_value {};
expr_mark m_visited;
bool contains_model_value(expr * e);
void add_instance(quantifier * q, expr_ref_vector const & bindings, unsigned max_generation);
void add_instance(quantifier * q, expr_ref_vector const & bindings, unsigned max_generation, expr * def);
public:
model_checker(ast_manager & m, qi_params const & p, model_finder & mf);

246
src/smt/smt_model_finder.cpp
View file

@ -76,16 +76,16 @@ namespace smt {
\brief Instantiation sets are the S_{k,j} sets in the Complete quantifier instantiation paper.
*/
class instantiation_set {
ast_manager & m_manager;
ast_manager & m;
obj_map<expr, unsigned> m_elems; // and the associated generation
obj_map<expr, expr *> m_inv;
expr_mark m_visited;
public:
instantiation_set(ast_manager & m):m_manager(m) {}
instantiation_set(ast_manager & m):m(m) {}
~instantiation_set() {
for (auto const& kv : m_elems) {
m_manager.dec_ref(kv.m_key);
m.dec_ref(kv.m_key);
}
m_elems.reset();
}
@ -95,10 +95,10 @@ namespace smt {
void insert(expr * n, unsigned generation) {
if (m_elems.contains(n) || contains_model_value(n))
return;
TRACE("model_finder", tout << mk_pp(n, m_manager) << "\n";);
m_manager.inc_ref(n);
TRACE("model_finder", tout << mk_pp(n, m) << "\n";);
m.inc_ref(n);
m_elems.insert(n, generation);
SASSERT(!m_manager.is_model_value(n));
SASSERT(!m.is_model_value(n));
}
void remove(expr * n) {
@ -106,16 +106,16 @@ namespace smt {
SASSERT(m_elems.contains(n));
SASSERT(m_inv.empty());
m_elems.erase(n);
m_manager.dec_ref(n);
m.dec_ref(n);
}
void display(std::ostream & out) const {
for (auto const& kv : m_elems) {
out << mk_bounded_pp(kv.m_key, m_manager) << " [" << kv.m_value << "]\n";
out << mk_bounded_pp(kv.m_key, m) << " [" << kv.m_value << "]\n";
}
out << "inverse:\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";
out << mk_bounded_pp(kv.m_key, m) << " -> " << mk_bounded_pp(kv.m_value, m) << "\n";
}
}
@ -138,7 +138,7 @@ namespace smt {
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";);
TRACE("model_finder", tout << mk_pp(t, m) << " " << mk_pp(t_val, m) << "\n";);
expr * old_t = nullptr;
if (m_inv.find(t_val, old_t)) {
@ -161,13 +161,13 @@ namespace smt {
struct is_model_value {};
void operator()(expr *n) {
if (m_manager.is_model_value(n)) {
if (m.is_model_value(n)) {
throw is_model_value();
}
}
bool contains_model_value(expr* n) {
if (m_manager.is_model_value(n)) {
if (m.is_model_value(n)) {
return true;
}
if (is_app(n) && to_app(n)->get_num_args() == 0) {
@ -393,6 +393,7 @@ namespace smt {
ast_manager & m;
arith_util m_arith;
bv_util m_bv;
array_util m_array;
ptr_vector<node> m_nodes;
unsigned m_next_node_id;
key2node m_uvars;
@ -427,16 +428,16 @@ namespace smt {
m_eval_cache_range.reset();
}
node * mk_node(key2node & m, ast * n, unsigned i, sort * s) {
node * mk_node(key2node & map, ast * n, unsigned i, sort * s) {
node * r = nullptr;
ast_idx_pair k(n, i);
if (m.find(k, r)) {
if (map.find(k, r)) {
SASSERT(r->get_sort() == s);
return r;
}
r = alloc(node, m_next_node_id, s);
m_next_node_id++;
m.insert(k, r);
map.insert(k, r);
m_nodes.push_back(r);
return r;
}
@ -468,6 +469,7 @@ namespace smt {
m(m),
m_arith(m),
m_bv(m),
m_array(m),
m_next_node_id(0),
m_context(nullptr),
m_ks(m),
@ -651,6 +653,7 @@ namespace smt {
a set of values.
*/
app * get_k_for(sort * s) {
TRACE("model_finder", tout << sort_ref(s, m) << "\n";);
SASSERT(is_infinite(s));
app * r = nullptr;
if (m_sort2k.find(s, r))
@ -709,6 +712,7 @@ namespace smt {
}
void set_projection_else(node * n) {
TRACE("model_finder", n->display(tout, m););
SASSERT(n->is_root());
SASSERT(!n->is_mono_proj());
instantiation_set const * s = n->get_instantiation_set();
@ -856,7 +860,6 @@ namespace smt {
bool is_signed = n->is_signed_proj();
unsigned sz = values.size();
SASSERT(sz > 0);
func_decl * p = m.mk_fresh_func_decl(1, &s, s);
expr * pi = values[sz - 1];
expr_ref var(m);
var = m.mk_var(0, s);
@ -872,11 +875,14 @@ namespace smt {
}
func_interp * rpi = alloc(func_interp, m, 1);
rpi->set_else(pi);
func_decl * p = m.mk_fresh_func_decl(1, &s, s);
TRACE("model_finder", tout << expr_ref(pi, m) << "\n";);
m_model->register_aux_decl(p, rpi);
n->set_proj(p);
}
void mk_simple_proj(node * n) {
TRACE("model_finder", n->display(tout, m););
set_projection_else(n);
ptr_buffer<expr> values;
get_instantiation_set_values(n, values);
@ -887,7 +893,7 @@ namespace smt {
if (n->get_else()) {
expr * else_val = eval(n->get_else(), true);
pi->set_else(else_val);
}
}
for (expr * v : values) {
pi->insert_new_entry(&v, v);
}
@ -972,9 +978,8 @@ namespace smt {
}
}
expr_ref_vector trail(m);
for (unsigned i = 0; i < need_fresh.size(); ++i) {
for (node * n : need_fresh) {
expr * e;
node* n = need_fresh[i];
sort* s = n->get_sort();
if (!sort2elems.find(s, e)) {
e = m.mk_fresh_const("elem", s);
@ -1173,10 +1178,7 @@ namespace smt {
void populate_inst_sets(quantifier * q, auf_solver & s, context * ctx) override {
node * A_f_i = s.get_A_f_i(m_f, m_arg_i);
enode_vector::const_iterator it = ctx->begin_enodes_of(m_f);
enode_vector::const_iterator end = ctx->end_enodes_of(m_f);
for (; it != end; it++) {
enode * n = *it;
for (enode * n : ctx->enodes_of(m_f)) {
if (ctx->is_relevant(n)) {
// Remark: it is incorrect to use
// n->get_arg(m_arg_i)->get_root()
@ -1203,10 +1205,7 @@ namespace smt {
instantiation_set * s = uvar_inst_sets[m_var_j];
SASSERT(s != 0);
enode_vector::const_iterator it = ctx->begin_enodes_of(m_f);
enode_vector::const_iterator end = ctx->end_enodes_of(m_f);
for (; it != end; it++) {
enode * n = *it;
for (enode * n : ctx->enodes_of(m_f)) {
if (ctx->is_relevant(n)) {
enode * e_arg = n->get_arg(m_arg_i);
expr * arg = e_arg->get_owner();
@ -1255,10 +1254,7 @@ namespace smt {
// there is no finite fixpoint... we just copy the i-th arguments of A_f_i - m_offset
// hope for the best...
node * S_j = s.get_uvar(q, m_var_j);
enode_vector::const_iterator it = ctx->begin_enodes_of(m_f);
enode_vector::const_iterator end = ctx->end_enodes_of(m_f);
for (; it != end; it++) {
enode * n = *it;
for (enode * n : ctx->enodes_of(m_f)) {
if (ctx->is_relevant(n)) {
arith_rewriter arith_rw(ctx->get_manager());
bv_util bv(ctx->get_manager());
@ -1375,7 +1371,7 @@ namespace smt {
class select_var : public qinfo {
protected:
ast_manager & m_manager;
ast_manager & m;
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;
@ -1384,6 +1380,7 @@ namespace smt {
app * get_array() const { return to_app(m_select->get_arg(0)); }
func_decl * get_array_func_decl(app * ground_array, auf_solver & s) {
TRACE("model_evaluator", tout << expr_ref(ground_array, m) << "\n";);
expr * ground_array_interp = s.eval(ground_array, false);
if (ground_array_interp != nullptr && m_array.is_as_array(ground_array_interp))
return m_array.get_as_array_func_decl(ground_array_interp);
@ -1391,7 +1388,7 @@ namespace smt {
}
public:
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) {}
select_var(ast_manager & m, app * s, unsigned i, unsigned j):m(m), m_array(m), m_select(s), m_arg_i(i), m_var_j(j) {}
~select_var() override {}
char const * get_kind() const override {
@ -1406,7 +1403,7 @@ namespace smt {
}
void display(std::ostream & out) const override {
out << "(" << mk_bounded_pp(m_select, m_manager) << ":" << m_arg_i << " -> v!" << m_var_j << ")";
out << "(" << mk_bounded_pp(m_select, m) << ":" << m_arg_i << " -> v!" << m_var_j << ")";
}
void process_auf(quantifier * q, auf_solver & s, context * ctx) override {
@ -1415,7 +1412,7 @@ namespace smt {
TRACE("select_var",
tout << "enodes matching: "; display(tout); tout << "\n";
for (enode* n : arrays) {
tout << "#" << n->get_owner()->get_id() << "\n" << mk_pp(n->get_owner(), m_manager) << "\n";
tout << "#" << n->get_owner()->get_id() << "\n" << mk_pp(n->get_owner(), m) << "\n";
});
node * n1 = s.get_uvar(q, m_var_j);
for (enode* n : arrays) {
@ -1574,10 +1571,7 @@ namespace smt {
// For uninterpreted sorts, we add all terms in the context.
// See Section 4.1 in the paper "Complete Quantifier Instantiation"
node * S_q_i = slv.get_uvar(q, m_var_i);
ptr_vector<enode>::const_iterator it = ctx->begin_enodes();
ptr_vector<enode>::const_iterator end = ctx->end_enodes();
for (; it != end; ++it) {
enode * n = *it;
for (enode * n : ctx->enodes()) {
if (ctx->is_relevant(n) && get_sort(n->get_owner()) == s) {
S_q_i->insert(n->get_owner(), n->get_generation());
}
@ -1623,7 +1617,7 @@ namespace smt {
class cond_macro {
protected:
ast_manager & m_manager;
ast_manager & m;
func_decl * m_f;
expr * m_def;
expr * m_cond;
@ -1633,7 +1627,7 @@ namespace smt {
unsigned m_weight;
public:
cond_macro(ast_manager & m, func_decl * f, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, unsigned weight):
m_manager(m),
m(m),
m_f(f),
m_def(def),
m_cond(cond),
@ -1641,14 +1635,14 @@ namespace smt {
m_satisfy_atom(satisfy_atom),
m_hint(hint),
m_weight(weight) {
m_manager.inc_ref(m_def);
m_manager.inc_ref(m_cond);
m.inc_ref(m_def);
m.inc_ref(m_cond);
SASSERT(!m_hint || m_cond == 0);
}
~cond_macro() {
m_manager.dec_ref(m_def);
m_manager.dec_ref(m_cond);
m.dec_ref(m_def);
m.dec_ref(m_cond);
}
func_decl * get_f() const { return m_f; }
@ -1657,7 +1651,7 @@ namespace smt {
expr * get_cond() const { return m_cond; }
bool is_unconditional() const { return m_cond == nullptr || m_manager.is_true(m_cond); }
bool is_unconditional() const { return m_cond == nullptr || m.is_true(m_cond); }
bool satisfy_atom() const { return m_satisfy_atom; }
@ -1668,11 +1662,11 @@ namespace smt {
}
void display(std::ostream & out) const {
out << "[" << m_f->get_name() << " -> " << mk_bounded_pp(m_def, m_manager, 6);
out << "[" << m_f->get_name() << " -> " << mk_bounded_pp(m_def, m, 6);
if (m_hint)
out << " *hint*";
else
out << " when " << mk_bounded_pp(m_cond, m_manager, 6);
out << " when " << mk_bounded_pp(m_cond, m, 6);
out << "] weight: " << m_weight;
}
@ -1739,7 +1733,7 @@ namespace smt {
m_has_x_eq_y(false),
m_the_one(nullptr),
m_uvar_inst_sets(nullptr) {
if (has_quantifiers(q->get_expr())) {
if (has_quantifiers(q->get_expr()) && !m.is_lambda_def(q)) {
static bool displayed_flat_msg = false;
if (!displayed_flat_msg) {
// [Leo]: This warning message is not useful.
@ -1758,7 +1752,7 @@ namespace smt {
}
CTRACE("model_finder_bug", has_quantifiers(m_flat_q->get_expr()),
tout << mk_pp(q, m) << "\n" << mk_pp(m_flat_q, m) << "\n";);
SASSERT(!has_quantifiers(m_flat_q->get_expr()));
SASSERT(m.is_lambda_def(q) || !has_quantifiers(m_flat_q->get_expr()));
}
~quantifier_info() {
@ -1787,7 +1781,6 @@ namespace smt {
ptr_vector<cond_macro> const& macros() const { return m_cond_macros; }
void set_the_one(func_decl * m) {
m_the_one = m;
}
@ -1880,7 +1873,7 @@ namespace smt {
*/
class quantifier_analyzer {
model_finder& m_mf;
ast_manager & m_manager;
ast_manager & m;
macro_util m_mutil;
array_util m_array_util;
arith_util m_arith_util;
@ -1909,7 +1902,7 @@ namespace smt {
bool is_var_plus_ground(expr * n, var * & v, expr_ref & t) {
bool inv;
TRACE("is_var_plus_ground", tout << mk_pp(n, m_manager) << "\n";
TRACE("is_var_plus_ground", tout << mk_pp(n, m) << "\n";
tout << "is_var_plus_ground: " << is_var_plus_ground(n, inv, v, t) << "\n";
tout << "inv: " << inv << "\n";);
return is_var_plus_ground(n, inv, v, t) && !inv;
@ -1953,7 +1946,7 @@ namespace smt {
bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t, bool & inv) {
inv = false; // true if invert the sign
TRACE("is_var_and_ground", tout << "is_var_and_ground: " << mk_ismt2_pp(lhs, m_manager) << " " << mk_ismt2_pp(rhs, m_manager) << "\n";);
TRACE("is_var_and_ground", tout << "is_var_and_ground: " << mk_ismt2_pp(lhs, m) << " " << mk_ismt2_pp(rhs, m) << "\n";);
if (is_var(lhs) && is_ground(rhs)) {
v = to_var(lhs);
t = rhs;
@ -1967,7 +1960,7 @@ namespace smt {
return true;
}
else {
expr_ref tmp(m_manager);
expr_ref tmp(m);
if (is_var_plus_ground(lhs, inv, v, tmp) && is_ground(rhs)) {
if (inv)
mk_sub(tmp, rhs, t);
@ -1994,7 +1987,7 @@ namespace smt {
bool is_x_eq_t_atom(expr * n, var * & v, expr_ref & t) {
if (!is_app(n))
return false;
if (m_manager.is_eq(n))
if (m.is_eq(n))
return is_var_and_ground(to_app(n)->get_arg(0), to_app(n)->get_arg(1), v, t);
return false;
}
@ -2030,7 +2023,7 @@ namespace smt {
}
bool is_x_eq_y_atom(expr * n, var * & v1, var * & v2) {
return m_manager.is_eq(n) && is_var_and_var(to_app(n)->get_arg(0), to_app(n)->get_arg(1), v1, v2);
return m.is_eq(n) && is_var_and_var(to_app(n)->get_arg(0), to_app(n)->get_arg(1), v1, v2);
}
bool is_x_gle_y_atom(expr * n, var * & v1, var * & v2) {
@ -2042,28 +2035,28 @@ namespace smt {
return false;
if (sign) {
bool r = is_le_ge(atom) && is_var_and_ground(to_app(atom)->get_arg(0), to_app(atom)->get_arg(1), v, t);
CTRACE("is_x_gle_t", r, tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m_manager) << "\n--->\n"
<< mk_ismt2_pp(v, m_manager) << " " << mk_ismt2_pp(t, m_manager) << "\n";
CTRACE("is_x_gle_t", r, tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m) << "\n--->\n"
<< mk_ismt2_pp(v, m) << " " << mk_ismt2_pp(t, m) << "\n";
tout << "sign: " << sign << "\n";);
return r;
}
else {
if (is_le_ge(atom)) {
expr_ref tmp(m_manager);
expr_ref tmp(m);
bool le = is_le(atom);
bool inv = false;
if (is_var_and_ground(to_app(atom)->get_arg(0), to_app(atom)->get_arg(1), v, tmp, inv)) {
if (inv)
le = !le;
sort * s = m_manager.get_sort(tmp);
expr_ref one(m_manager);
sort * s = m.get_sort(tmp);
expr_ref one(m);
one = mk_one(s);
if (le)
mk_add(tmp, one, t);
else
mk_sub(tmp, one, t);
TRACE("is_x_gle_t", tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m_manager) << "\n--->\n"
<< mk_ismt2_pp(v, m_manager) << " " << mk_ismt2_pp(t, m_manager) << "\n";
TRACE("is_x_gle_t", tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m) << "\n--->\n"
<< mk_ismt2_pp(v, m) << " " << mk_ismt2_pp(t, m) << "\n";
tout << "sign: " << sign << "\n";);
return true;
}
@ -2113,9 +2106,9 @@ namespace smt {
}
var * v;
expr_ref k(m_manager);
expr_ref k(m);
if (is_var_plus_ground(arg, v, k)) {
insert_qinfo(alloc(f_var_plus_offset, m_manager, t->get_decl(), i, v->get_idx(), k.get()));
insert_qinfo(alloc(f_var_plus_offset, m, t->get_decl(), i, v->get_idx(), k.get()));
continue;
}
@ -2157,7 +2150,7 @@ namespace smt {
for (unsigned i = 1; i < num_args; i++) {
expr * arg = t->get_arg(i);
if (is_var(arg)) {
insert_qinfo(alloc(select_var, m_manager, t, i, to_var(arg)->get_idx()));
insert_qinfo(alloc(select_var, m, t, i, to_var(arg)->get_idx()));
}
else {
SASSERT(is_ground(arg));
@ -2174,7 +2167,7 @@ namespace smt {
void process_app(app * t) {
SASSERT(!is_ground(t));
if (t->get_family_id() != m_manager.get_basic_family_id()) {
if (t->get_family_id() != m.get_basic_family_id()) {
m_info->m_ng_decls.insert(t->get_decl());
}
@ -2191,7 +2184,7 @@ namespace smt {
expr * curr = m_ttodo.back();
m_ttodo.pop_back();
if (m_manager.is_bool(curr)) {
if (m.is_bool(curr)) {
// formula nested in a term.
visit_formula(curr, POS);
visit_formula(curr, NEG);
@ -2212,30 +2205,30 @@ namespace smt {
}
void process_literal(expr * atom, bool sign) {
CTRACE("model_finder_bug", is_ground(atom), tout << mk_pp(atom, m_manager) << "\n";);
CTRACE("model_finder_bug", is_ground(atom), tout << mk_pp(atom, m) << "\n";);
SASSERT(!is_ground(atom));
SASSERT(m_manager.is_bool(atom));
SASSERT(m.is_bool(atom));
if (is_var(atom)) {
if (sign) {
// atom (not X) can be viewed as X != true
insert_qinfo(alloc(x_neq_t, m_manager, to_var(atom)->get_idx(), m_manager.mk_true()));
insert_qinfo(alloc(x_neq_t, m, to_var(atom)->get_idx(), m.mk_true()));
}
else {
// atom X can be viewed as X != false
insert_qinfo(alloc(x_neq_t, m_manager, to_var(atom)->get_idx(), m_manager.mk_false()));
insert_qinfo(alloc(x_neq_t, m, to_var(atom)->get_idx(), m.mk_false()));
}
return;
}
if (is_app(atom)) {
var * v, * v1, * v2;
expr_ref t(m_manager);
expr_ref t(m);
if (is_x_eq_t_atom(atom, v, t)) {
if (sign)
insert_qinfo(alloc(x_neq_t, m_manager, v->get_idx(), t));
insert_qinfo(alloc(x_neq_t, m, v->get_idx(), t));
else
insert_qinfo(alloc(x_eq_t, m_manager, v->get_idx(), t));
insert_qinfo(alloc(x_eq_t, m, v->get_idx(), t));
}
else if (is_x_eq_y_atom(atom, v1, v2)) {
if (sign)
@ -2252,7 +2245,7 @@ namespace smt {
insert_qinfo(alloc(x_leq_y, v1->get_idx(), v2->get_idx()));
}
else if (is_x_gle_t_atom(atom, sign, v, t)) {
insert_qinfo(alloc(x_gle_t, m_manager, v->get_idx(), t));
insert_qinfo(alloc(x_gle_t, m, v->get_idx(), t));
}
else {
process_app(to_app(atom));
@ -2299,7 +2292,7 @@ namespace smt {
polarity pol = e.second;
m_ftodo.pop_back();
if (is_app(curr)) {
if (to_app(curr)->get_family_id() == m_manager.get_basic_family_id() && m_manager.is_bool(curr)) {
if (to_app(curr)->get_family_id() == m.get_basic_family_id() && m.is_bool(curr)) {
switch (static_cast<basic_op_kind>(to_app(curr)->get_decl_kind())) {
case OP_IMPLIES:
case OP_XOR:
@ -2316,7 +2309,7 @@ namespace smt {
process_ite(to_app(curr), pol);
break;
case OP_EQ:
if (m_manager.is_bool(to_app(curr)->get_arg(0))) {
if (m.is_bool(to_app(curr)->get_arg(0))) {
process_iff(to_app(curr));
}
else {
@ -2333,7 +2326,7 @@ namespace smt {
}
}
else if (is_var(curr)) {
SASSERT(m_manager.is_bool(curr));
SASSERT(m.is_bool(curr));
process_literal(curr, pol);
}
else {
@ -2344,32 +2337,32 @@ namespace smt {
}
void process_formula(expr * n) {
SASSERT(m_manager.is_bool(n));
SASSERT(m.is_bool(n));
visit_formula(n, POS);
}
void process_clause(expr * cls) {
SASSERT(is_clause(m_manager, cls));
unsigned num_lits = get_clause_num_literals(m_manager, cls);
SASSERT(is_clause(m, cls));
unsigned num_lits = get_clause_num_literals(m, cls);
for (unsigned i = 0; i < num_lits; i++) {
expr * lit = get_clause_literal(m_manager, cls, i);
SASSERT(is_literal(m_manager, lit));
expr * lit = get_clause_literal(m, cls, i);
SASSERT(is_literal(m, lit));
expr * atom;
bool sign;
get_literal_atom_sign(m_manager, lit, atom, sign);
get_literal_atom_sign(m, lit, atom, sign);
if (!is_ground(atom))
process_literal(atom, sign);
}
}
void collect_macro_candidates(quantifier * q) {
macro_util::macro_candidates candidates(m_manager);
macro_util::macro_candidates candidates(m);
m_mutil.collect_macro_candidates(q, candidates);
unsigned num_candidates = candidates.size();
for (unsigned i = 0; i < num_candidates; i++) {
cond_macro * m = alloc(cond_macro, m_manager, candidates.get_f(i), candidates.get_def(i), candidates.get_cond(i),
cond_macro * mc = alloc(cond_macro, m, candidates.get_f(i), candidates.get_def(i), candidates.get_cond(i),
candidates.ineq(i), candidates.satisfy_atom(i), candidates.hint(i), q->get_weight());
m_info->insert_macro(m);
m_info->insert_macro(mc);
}
}
@ -2377,7 +2370,7 @@ namespace smt {
public:
quantifier_analyzer(model_finder& mf, ast_manager & m):
m_mf(mf),
m_manager(m),
m(m),
m_mutil(m),
m_array_util(m),
m_arith_util(m),
@ -2389,13 +2382,14 @@ namespace smt {
void operator()(quantifier_info * d) {
m_info = d;
quantifier * q = d->get_flat_q();
if (m.is_lambda_def(q)) return;
expr * e = q->get_expr();
SASSERT(!has_quantifiers(e));
reset_cache();
SASSERT(m_ttodo.empty());
SASSERT(m_ftodo.empty());
if (is_clause(m_manager, e)) {
if (is_clause(m, e)) {
process_clause(e);
}
else {
@ -2419,7 +2413,7 @@ namespace smt {
*/
class base_macro_solver {
protected:
ast_manager & m_manager;
ast_manager & m;
obj_map<quantifier, quantifier_info *> const & m_q2info;
proto_model * m_model;
@ -2434,18 +2428,18 @@ namespace smt {
SASSERT(f_else != 0);
func_interp * fi = m_model->get_func_interp(f);
if (fi == nullptr) {
fi = alloc(func_interp, m_manager, f->get_arity());
fi = alloc(func_interp, m, f->get_arity());
m_model->register_decl(f, fi);
}
fi->set_else(f_else);
TRACE("model_finder", tout << f->get_name() << " " << mk_pp(f_else, m_manager) << "\n";);
TRACE("model_finder", tout << f->get_name() << " " << mk_pp(f_else, m) << "\n";);
}
virtual bool process(ptr_vector<quantifier> const & qs, ptr_vector<quantifier> & new_qs, ptr_vector<quantifier> & residue) = 0;
public:
base_macro_solver(ast_manager & m, obj_map<quantifier, quantifier_info *> const & q2i):
m_manager(m),
m(m),
m_q2info(q2i),
m_model(nullptr) {
}
@ -2647,7 +2641,7 @@ namespace smt {
bool is_candidate(quantifier * q) const {
quantifier_info * qi = get_qinfo(q);
for (cond_macro * m : qi->macros()) {
for (cond_macro* m : qi->macros()) {
if (m->satisfy_atom() && !m_forbidden.contains(m->get_f()))
return true;
}
@ -2708,7 +2702,7 @@ namespace smt {
void display_qcandidates(std::ostream & out, ptr_vector<quantifier> const & qcandidates) const {
for (quantifier * q : qcandidates) {
out << q->get_qid() << " ->\n" << mk_pp(q, m_manager) << "\n";
out << q->get_qid() << " ->\n" << mk_pp(q, m) << "\n";
quantifier_info * qi = get_qinfo(q);
qi->display(out);
out << "------\n";
@ -2724,7 +2718,7 @@ namespace smt {
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);
out << f->get_name() << " " << mk_pp(def, m) << " ->\n"; display_quantifier_set(out, s);
}
}
@ -2846,7 +2840,7 @@ namespace smt {
m_satisfied.push_scope();
m_residue.push_scope();
TRACE("model_finder", tout << f->get_name() << " " << mk_pp(def, m_manager) << "\n";);
TRACE("model_finder", tout << f->get_name() << " " << mk_pp(def, m) << "\n";);
m_fs.insert(f, def);
if (update_satisfied_residue(f, def)) {
@ -3023,7 +3017,7 @@ namespace smt {
qi_params const * m_qi_params;
bool add_macro(func_decl * f, expr * f_else) {
TRACE("model_finder", tout << "trying to add macro for " << f->get_name() << "\n" << mk_pp(f_else, m_manager) << "\n";);
TRACE("model_finder", tout << "trying to add macro for " << f->get_name() << "\n" << mk_pp(f_else, m) << "\n";);
func_decl_set * s = m_dependencies.mk_func_decl_set();
m_dependencies.collect_ng_func_decls(f_else, s);
if (!m_dependencies.insert(f, s)) {
@ -3092,23 +3086,23 @@ namespace smt {
}
void process(func_decl * f, ptr_vector<quantifier> const & qs, obj_hashtable<quantifier> & removed) {
expr_ref fi_else(m_manager);
expr_ref fi_else(m);
ptr_buffer<quantifier> to_remove;
for (quantifier * q : qs) {
if (removed.contains(q))
continue;
cond_macro * m = get_macro_for(f, q);
if (!m)
cond_macro * cm = get_macro_for(f, q);
if (!cm)
continue;
SASSERT(!m->is_hint());
if (m->is_unconditional())
SASSERT(!cm->is_hint());
if (cm->is_unconditional())
return; // f is part of a full macro... ignoring it.
to_remove.push_back(q);
if (fi_else.get() == nullptr) {
fi_else = m->get_def();
fi_else = cm->get_def();
}
else {
fi_else = m_manager.mk_ite(m->get_cond(), m->get_def(), fi_else);
fi_else = m.mk_ite(cm->get_cond(), cm->get_def(), fi_else);
}
}
if (fi_else.get() != nullptr && add_macro(f, fi_else)) {
@ -3166,7 +3160,7 @@ namespace smt {
// -----------------------------------
model_finder::model_finder(ast_manager & m):
m_manager(m),
m(m),
m_context(nullptr),
m_analyzer(alloc(quantifier_analyzer, *this, m)),
m_auf_solver(alloc(auf_solver, m)),
@ -3206,8 +3200,8 @@ namespace smt {
}
void model_finder::register_quantifier(quantifier * q) {
TRACE("model_finder", tout << "registering:\n" << mk_pp(q, m_manager) << "\n";);
quantifier_info * new_info = alloc(quantifier_info, *this, m_manager, q);
TRACE("model_finder", tout << "registering:\n" << mk_pp(q, m) << "\n";);
quantifier_info * new_info = alloc(quantifier_info, *this, m, q);
m_q2info.insert(q, new_info);
m_quantifiers.push_back(q);
m_analyzer->operator()(new_info);
@ -3261,9 +3255,9 @@ namespace smt {
}
}
void model_finder::process_auf(ptr_vector<quantifier> const & qs, proto_model * m) {
void model_finder::process_auf(ptr_vector<quantifier> const & qs, proto_model * mdl) {
m_auf_solver->reset();
m_auf_solver->set_model(m);
m_auf_solver->set_model(mdl);
for (quantifier * q : qs) {
quantifier_info * qi = get_quantifier_info(q);
@ -3280,7 +3274,7 @@ namespace smt {
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";
tout << "#" << fq->get_id() << " ->\n" << mk_pp(fq, m) << "\n";
}
m_auf_solver->display_nodes(tout););
}
@ -3310,11 +3304,8 @@ namespace smt {
\brief Clean leftovers from previous invocations to fix_model.
*/
void model_finder::cleanup_quantifier_infos(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_info * qi = get_quantifier_info(*it);
qi->reset_the_one();
for (quantifier* q : qs) {
get_quantifier_info(q)->reset_the_one();
}
}
@ -3356,7 +3347,7 @@ namespace smt {
quantifier * flat_q = get_flat_quantifier(q);
SASSERT(flat_q->get_num_decls() >= q->get_num_decls());
instantiation_set const * r = m_auf_solver->get_uvar_inst_set(flat_q, flat_q->get_num_decls() - q->get_num_decls() + i);
TRACE("model_finder", tout << "q: #" << q->get_id() << "\n" << mk_pp(q,m_manager) << "\nflat_q: " << mk_pp(flat_q, m_manager)
TRACE("model_finder", tout << "q: #" << q->get_id() << "\n" << mk_pp(q,m) << "\nflat_q: " << mk_pp(flat_q, m)
<< "\ni: " << i << " " << flat_q->get_num_decls() - q->get_num_decls() + i << "\n";);
if (r != nullptr)
return r;
@ -3365,7 +3356,6 @@ namespace smt {
quantifier_info * qinfo = get_quantifier_info(q);
SASSERT(qinfo);
SASSERT(qinfo->get_the_one() != 0);
return qinfo->get_macro_based_inst_set(i, m_context, *(m_auf_solver.get()));
}
@ -3415,15 +3405,13 @@ namespace smt {
if (inv.empty())
continue; // nothing to do
ptr_buffer<expr> eqs;
obj_map<expr, expr *>::iterator it = inv.begin();
obj_map<expr, expr *>::iterator end = inv.end();
for (; it != end; ++it) {
expr * val = (*it).m_key;
eqs.push_back(m_manager.mk_eq(sk, val));
for (auto const& kv : inv) {
expr * val = kv.m_key;
eqs.push_back(m.mk_eq(sk, val));
}
expr_ref new_cnstr(m_manager);
new_cnstr = m_manager.mk_or(eqs.size(), eqs.c_ptr());
TRACE("model_finder", tout << "assert_restriction:\n" << mk_pp(new_cnstr, m_manager) << "\n";);
expr_ref new_cnstr(m);
new_cnstr = m.mk_or(eqs.size(), eqs.c_ptr());
TRACE("model_finder", tout << "assert_restriction:\n" << mk_pp(new_cnstr, m) << "\n";);
aux_ctx->assert_expr(new_cnstr);
asserted_something = true;
}
@ -3435,7 +3423,7 @@ namespace smt {
if (sz > 0) {
for (unsigned i = 0; i < sz; i++) {
expr * c = m_new_constraints.get(i);
TRACE("model_finder_bug_detail", tout << "asserting new constraint: " << mk_pp(c, m_manager) << "\n";);
TRACE("model_finder_bug_detail", tout << "asserting new constraint: " << mk_pp(c, m) << "\n";);
m_context->internalize(c, true);
literal l(m_context->get_literal(c));
m_context->mark_as_relevant(l);

2
src/smt/smt_model_finder.h
View file

@ -74,7 +74,7 @@ namespace smt {
typedef mf::non_auf_macro_solver non_auf_macro_solver;
typedef mf::instantiation_set instantiation_set;
ast_manager & m_manager;
ast_manager & m;
context * m_context;
scoped_ptr<quantifier_analyzer> m_analyzer;
scoped_ptr<auf_solver> m_auf_solver;

52
src/smt/smt_model_generator.cpp
View file

@ -24,6 +24,7 @@ Revision History:
#include "smt/smt_context.h"
#include "smt/smt_model_generator.h"
#include "smt/proto_model/proto_model.h"
#include "model/model_v2_pp.h"
namespace smt {
@ -51,11 +52,9 @@ namespace smt {
SASSERT(!m_model);
// PARAM-TODO smt_params ---> params_ref
m_model = alloc(proto_model, m_manager); // , m_context->get_fparams());
ptr_vector<theory>::const_iterator it = m_context->begin_theories();
ptr_vector<theory>::const_iterator end = m_context->end_theories();
for (; it != end; ++it) {
TRACE("model", tout << "init_model for theory: " << (*it)->get_name() << "\n";);
(*it)->init_model(*this);
for (theory* th : m_context->theories()) {
TRACE("model_generator_bug", tout << "init_model for theory: " << th->get_name() << "\n";);
th->init_model(*this);
}
}
@ -82,10 +81,7 @@ namespace smt {
*/
void model_generator::mk_value_procs(obj_map<enode, model_value_proc *> & root2proc, ptr_vector<enode> & roots,
ptr_vector<model_value_proc> & procs) {
ptr_vector<enode>::const_iterator it = m_context->begin_enodes();
ptr_vector<enode>::const_iterator end = m_context->end_enodes();
for (; it != end; ++it) {
enode * r = *it;
for (enode * r : m_context->enodes()) {
if (r == r->get_root() && m_context->is_relevant(r)) {
roots.push_back(r);
sort * s = m_manager.get_sort(r->get_owner());
@ -201,10 +197,7 @@ namespace smt {
SASSERT(proc);
buffer<model_value_dependency> dependencies;
proc->get_dependencies(dependencies);
buffer<model_value_dependency>::const_iterator it = dependencies.begin();
buffer<model_value_dependency>::const_iterator end = dependencies.end();
for (; it != end; ++it) {
model_value_dependency const & dep = *it;
for (model_value_dependency const& dep : dependencies) {
visit_child(dep, colors, todo, visited);
TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " -> ";
if (dep.is_fresh_value()) tout << "fresh!" << dep.get_value()->get_idx();
@ -308,10 +301,7 @@ namespace smt {
mk_value_procs(root2proc, roots, procs);
top_sort_sources(roots, root2proc, sources);
TRACE("sorted_sources",
svector<source>::const_iterator it = sources.begin();
svector<source>::const_iterator end = sources.end();
for (; it != end; ++it) {
source const & curr = *it;
for (source const& curr : sources) {
if (curr.is_fresh_value()) {
tout << "fresh!" << curr.get_value()->get_idx() << " " << mk_pp(curr.get_value()->get_sort(), m_manager) << "\n";
}
@ -326,11 +316,7 @@ namespace smt {
tout << " is_fresh: " << proc->is_fresh() << "\n";
}
});
svector<source>::const_iterator it = sources.begin();
svector<source>::const_iterator end = sources.end();
for (; it != end; ++it) {
source const & curr = *it;
for (source const& curr : sources) {
if (curr.is_fresh_value()) {
sort * s = curr.get_value()->get_sort();
TRACE("model_fresh_bug", tout << "mk fresh!" << curr.get_value()->get_idx() << " : " << mk_pp(s, m_manager) << "\n";);
@ -349,10 +335,7 @@ namespace smt {
VERIFY(root2proc.find(n, proc));
SASSERT(proc);
proc->get_dependencies(dependencies);
buffer<model_value_dependency>::const_iterator it2 = dependencies.begin();
buffer<model_value_dependency>::const_iterator end2 = dependencies.end();
for (; it2 != end2; ++it2) {
model_value_dependency const & d = *it2;
for (model_value_dependency const& d : dependencies) {
if (d.is_fresh_value()) {
CTRACE("mg_top_sort", !d.get_value()->get_value(),
tout << "#" << n->get_owner_id() << " -> ";
@ -381,10 +364,7 @@ namespace smt {
m_extra_fresh_values.reset();
// send model
ptr_vector<enode>::const_iterator it3 = m_context->begin_enodes();
ptr_vector<enode>::const_iterator end3 = m_context->end_enodes();
for (; it3 != end3; ++it3) {
enode * n = *it3;
for (enode * n : m_context->enodes()) {
if (is_uninterp_const(n->get_owner()) && m_context->is_relevant(n)) {
func_decl * d = n->get_owner()->get_decl();
TRACE("mg_top_sort", tout << d->get_name() << " " << (m_hidden_ufs.contains(d)?"hidden":"visible") << "\n";);
@ -484,17 +464,12 @@ namespace smt {
}
void model_generator::finalize_theory_models() {
ptr_vector<theory>::const_iterator it = m_context->begin_theories();
ptr_vector<theory>::const_iterator end = m_context->end_theories();
for (; it != end; ++it)
(*it)->finalize_model(*this);
for (theory* th : m_context->theories())
th->finalize_model(*this);
}
void model_generator::register_existing_model_values() {
ptr_vector<enode>::const_iterator it = m_context->begin_enodes();
ptr_vector<enode>::const_iterator end = m_context->end_enodes();
for (; it != end; ++it) {
enode * r = *it;
for (enode * r : m_context->enodes()) {
if (r == r->get_root() && m_context->is_relevant(r)) {
expr * n = r->get_owner();
if (m_manager.is_model_value(n)) {
@ -531,6 +506,7 @@ namespace smt {
mk_func_interps();
finalize_theory_models();
register_macros();
TRACE("model", model_v2_pp(tout, *m_model, true););
return m_model;
}

10
src/smt/smt_quantifier.cpp
View file

@ -107,6 +107,7 @@ namespace smt {
bool add_instance(quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
expr* def,
unsigned max_generation,
unsigned min_top_generation,
unsigned max_top_generation,
@ -116,7 +117,7 @@ namespace smt {
return false;
}
get_stat(q)->update_max_generation(max_generation);
fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings);
fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings, def);
if (f) {
if (has_trace_stream()) {
std::ostream & out = trace_stream();
@ -291,16 +292,17 @@ namespace smt {
bool quantifier_manager::add_instance(quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
expr* def,
unsigned max_generation,
unsigned min_top_generation,
unsigned max_top_generation,
ptr_vector<enode> & used_enodes) {
return m_imp->add_instance(q, pat, num_bindings, bindings, max_generation, min_top_generation, max_generation, used_enodes);
return m_imp->add_instance(q, pat, num_bindings, bindings, def, max_generation, min_top_generation, max_generation, used_enodes);
}
bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation) {
bool quantifier_manager::add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, expr* def, unsigned generation) {
ptr_vector<enode> tmp;
return add_instance(q, nullptr, num_bindings, bindings, generation, generation, generation, tmp);
return add_instance(q, nullptr, num_bindings, bindings, def, generation, generation, generation, tmp);
}
void quantifier_manager::init_search_eh() {

5
src/smt/smt_quantifier.h
View file

@ -54,11 +54,12 @@ namespace smt {
bool add_instance(quantifier * q, app * pat,
unsigned num_bindings,
enode * const * bindings,
expr* def,
unsigned max_generation,
unsigned min_top_generation,
unsigned max_top_generation,
ptr_vector<enode> & used_enodes);
bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned generation = 0);
bool add_instance(quantifier * q, unsigned num_bindings, enode * const * bindings, expr* def, unsigned generation = 0);
void init_search_eh();
void assign_eh(quantifier * q);
@ -91,6 +92,8 @@ namespace smt {
ptr_vector<quantifier>::const_iterator begin_quantifiers() const;
ptr_vector<quantifier>::const_iterator end_quantifiers() const;
ptr_vector<quantifier>::const_iterator begin() const { return begin_quantifiers(); }
ptr_vector<quantifier>::const_iterator end() const { return end_quantifiers(); }
unsigned num_quantifiers() const;
};

35
src/smt/smt_quick_checker.cpp
View file

@ -51,10 +51,7 @@ namespace smt {
bool quick_checker::collector::check_arg(enode * n, func_decl * f, unsigned i) {
if (!f || !m_conservative)
return true;
enode_vector::const_iterator it = m_context.begin_enodes_of(f);
enode_vector::const_iterator end = m_context.end_enodes_of(f);
for (; it != end; ++it) {
enode * curr = *it;
for (enode * curr : m_context.enodes_of(f)) {
if (m_context.is_relevant(curr) && curr->is_cgr() && i < curr->get_num_args() && curr->get_arg(i)->get_root() == n->get_root())
return true;
}
@ -76,10 +73,7 @@ namespace smt {
if (s.empty())
continue;
ns.reset();
enode_vector::const_iterator it = m_context.begin_enodes_of(f);
enode_vector::const_iterator end = m_context.end_enodes_of(f);
for (; it != end; ++it) {
enode * curr = *it;
for (enode * curr : m_context.enodes_of(f)) {
if (m_context.is_relevant(curr) && curr->is_cgr() && check_arg(curr, p, i) && j < curr->get_num_args()) {
enode * arg = curr->get_arg(j)->get_root();
// intersection
@ -93,10 +87,7 @@ namespace smt {
else {
m_already_found[idx] = true;
enode_set & s = m_candidates[idx];
enode_vector::const_iterator it = m_context.begin_enodes_of(f);
enode_vector::const_iterator end = m_context.end_enodes_of(f);
for (; it != end; ++it) {
enode * curr = *it;
for (enode * curr : m_context.enodes_of(f)) {
if (m_context.is_relevant(curr) && curr->is_cgr() && check_arg(curr, p, i) && j < curr->get_num_args()) {
enode * arg = curr->get_arg(j)->get_root();
s.insert(arg);
@ -133,10 +124,7 @@ namespace smt {
enode_vector & v = candidates[i];
v.reset();
enode_set & s = m_candidates[i];
enode_set::iterator it = s.begin();
enode_set::iterator end = s.end();
for (; it != end; ++it) {
enode * curr = *it;
for (enode * curr : s) {
v.push_back(curr);
}
}
@ -145,10 +133,8 @@ namespace smt {
for (unsigned i = 0; i < m_num_vars; i++) {
tout << "var " << i << ":";
enode_vector & v = candidates[i];
enode_vector::iterator it = v.begin();
enode_vector::iterator end = v.end();
for (; it != end; ++it)
tout << " #" << (*it)->get_owner_id();
for (enode * n : v)
tout << " #" << n->get_owner_id();
tout << "\n";
});
}
@ -226,10 +212,8 @@ namespace smt {
tout << "candidates:\n";
for (unsigned i = 0; i < m_num_bindings; i++) {
enode_vector & v = m_candidate_vectors[i];
enode_vector::iterator it = v.begin();
enode_vector::iterator end = v.end();
for (; it != end; ++it)
tout << "#" << (*it)->get_owner_id() << " ";
for (enode * n : v)
tout << "#" << n->get_owner_id() << " ";
tout << "\n";
});
bool result = false;
@ -251,7 +235,8 @@ namespace smt {
TRACE("quick_checker_sizes", tout << "found new candidate\n";
for (unsigned i = 0; i < m_num_bindings; i++) tout << "#" << m_bindings[i]->get_owner_id() << " "; tout << "\n";);
unsigned max_generation = get_max_generation(m_num_bindings, m_bindings.c_ptr());
if (m_context.add_instance(q, nullptr /* no pattern was used */, m_num_bindings, m_bindings.c_ptr(), max_generation,
if (m_context.add_instance(q, nullptr /* no pattern was used */, m_num_bindings, m_bindings.c_ptr(), nullptr,
max_generation,
0, // min_top_generation is only available for instances created by the MAM
0, // max_top_generation is only available for instances created by the MAM
empty_used_enodes))

2
src/smt/theory_array.cpp
View file

@ -383,7 +383,7 @@ namespace smt {
}
}
TRACE("array", tout << "m_found_unsupported_op: " << m_found_unsupported_op << " " << r << "\n";);
if (r == FC_DONE && m_found_unsupported_op)
if (r == FC_DONE && m_found_unsupported_op && !get_context().get_fparams().m_array_fake_support)
r = FC_GIVEUP;
return r;
}

8
src/smt/theory_array_base.cpp
View file

@ -33,8 +33,12 @@ namespace smt {
}
void theory_array_base::found_unsupported_op(expr * n) {
TRACE("array", tout << mk_ll_pp(n, get_manager()) << "\n";);
if (!m_found_unsupported_op) {
if (!get_context().get_fparams().m_array_fake_support && !m_found_unsupported_op) {
//array_util autil(get_manager());
//func_decl* f = 0;
//if (autil.is_as_array(n, f) && f->is_skolem()) return;
TRACE("array", tout << mk_ll_pp(n, get_manager()) << "\n";);
get_context().push_trail(value_trail<context, bool>(m_found_unsupported_op));
m_found_unsupported_op = true;
}

148
src/smt/theory_array_full.cpp
View file

@ -17,13 +17,13 @@ Revision History:
--*/
#include "smt/smt_context.h"
#include "smt/theory_array_full.h"
#include "util/stats.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "ast/ast_util.h"
#include "ast/ast_smt2_pp.h"
#include "util/stats.h"
#include "smt/smt_context.h"
#include "smt/theory_array_full.h"
namespace smt {
@ -54,11 +54,9 @@ namespace smt {
set_prop_upward(v,d);
d_full->m_maps.push_back(s);
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d_full->m_maps));
ptr_vector<enode>::iterator it = d->m_parent_selects.begin();
ptr_vector<enode>::iterator end = d->m_parent_selects.end();
for (; it != end; ++it) {
SASSERT(is_select(*it));
instantiate_select_map_axiom(*it, s);
for (enode* n : d->m_parent_selects) {
SASSERT(is_select(n));
instantiate_select_map_axiom(n, s);
}
set_prop_upward(s);
}
@ -67,15 +65,10 @@ namespace smt {
bool result = false;
var_data * d = m_var_data[v];
var_data_full * d_full = m_var_data_full[v];
unsigned num_maps = d_full->m_parent_maps.size();
unsigned num_selects = d->m_parent_selects.size();
for (unsigned i = 0; i < num_maps; ++i) {
for (unsigned j = 0; j < num_selects; ++j) {
if (instantiate_select_map_axiom(d->m_parent_selects[j], d_full->m_parent_maps[i])) {
result = true;
}
}
}
for (enode* pm : d_full->m_parent_maps)
for (enode* ps : d->m_parent_selects)
if (instantiate_select_map_axiom(ps, pm))
result = true;
return result;
}
@ -91,11 +84,9 @@ namespace smt {
d_full->m_parent_maps.push_back(s);
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d_full->m_parent_maps));
if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
ptr_vector<enode>::iterator it = d->m_parent_selects.begin();
ptr_vector<enode>::iterator end = d->m_parent_selects.end();
for (; it != end; ++it) {
if (!m_params.m_array_cg || (*it)->is_cgr()) {
instantiate_select_map_axiom(*it, s);
for (enode * n : d->m_parent_selects) {
if (!m_params.m_array_cg || n->is_cgr()) {
instantiate_select_map_axiom(n, s);
}
}
}
@ -118,20 +109,14 @@ namespace smt {
instantiate_axiom_map_for(v);
}
var_data_full * d2 = m_var_data_full[v];
ptr_vector<enode>::iterator it = d->m_stores.begin();
ptr_vector<enode>::iterator end = d->m_stores.end();
for (; it != end; ++it) {
set_prop_upward(*it);
for (enode * n : d->m_stores) {
set_prop_upward(n);
}
it = d2->m_maps.begin();
end = d2->m_maps.end();
for (; it != end; ++it) {
set_prop_upward(*it);
for (enode * n : d2->m_maps) {
set_prop_upward(n);
}
it = d2->m_consts.begin();
end = d2->m_consts.end();
for (; it != end; ++it) {
set_prop_upward(*it);
for (enode * n : d2->m_consts) {
set_prop_upward(n);
}
}
}
@ -180,12 +165,9 @@ namespace smt {
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(consts));
consts.push_back(cnst);
instantiate_default_const_axiom(cnst);
ptr_vector<enode>::iterator it = d->m_parent_selects.begin();
ptr_vector<enode>::iterator end = d->m_parent_selects.end();
for (; it != end; ++it) {
SASSERT(is_select(*it));
instantiate_select_const_axiom(*it, cnst);
for (enode * n : d->m_parent_selects) {
SASSERT(is_select(n));
instantiate_select_const_axiom(n, cnst);
}
}
@ -199,12 +181,9 @@ namespace smt {
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(as_arrays));
as_arrays.push_back(arr);
instantiate_default_as_array_axiom(arr);
ptr_vector<enode>::iterator it = d->m_parent_selects.begin();
ptr_vector<enode>::iterator end = d->m_parent_selects.end();
for (; it != end; ++it) {
SASSERT(is_select(*it));
instantiate_select_as_array_axiom(*it, arr);
for (enode * n : d->m_parent_selects) {
SASSERT(is_select(n));
instantiate_select_as_array_axiom(n, arr);
}
}
@ -257,6 +236,10 @@ namespace smt {
}
bool theory_array_full::internalize_term(app * n) {
context & ctx = get_context();
if (ctx.e_internalized(n)) {
return true;
}
TRACE("array", tout << mk_pp(n, get_manager()) << "\n";);
if (is_store(n) || is_select(n)) {
@ -272,11 +255,10 @@ namespace smt {
if (!internalize_term_core(n)) {
return true;
}
context & ctx = get_context();
if (is_map(n) || is_array_ext(n)) {
for (unsigned i = 0; i < n->get_num_args(); ++i) {
enode* arg = ctx.get_enode(n->get_arg(i));
for (expr* e : *n) {
enode* arg = ctx.get_enode(e);
if (!is_attached_to_var(arg)) {
mk_var(arg);
}
@ -300,8 +282,8 @@ namespace smt {
add_parent_default(v_arg);
}
else if (is_map(n)) {
for (unsigned i = 0; i < n->get_num_args(); ++i) {
enode* arg = ctx.get_enode(n->get_arg(i));
for (expr* e : *n) {
enode* arg = ctx.get_enode(e);
theory_var v_arg = arg->get_th_var(get_id());
add_parent_map(v_arg, node);
}
@ -334,27 +316,17 @@ namespace smt {
// v1 is the new root
SASSERT(v1 == find(v1));
var_data_full * d2 = m_var_data_full[v2];
ptr_vector<enode>::iterator it, end;
it = d2->m_maps.begin();
end = d2->m_maps.end();
for (; it != end; ++it) {
add_map(v1, *it);
for (enode * n : d2->m_maps) {
add_map(v1, n);
}
it = d2->m_parent_maps.begin();
end = d2->m_parent_maps.end();
for (; it != end; ++it) {
add_parent_map(v1, *it);
for (enode * n : d2->m_parent_maps) {
add_parent_map(v1, n);
}
it = d2->m_consts.begin();
end = d2->m_consts.end();
for (; it != end; ++it) {
add_const(v1, *it);
for (enode * n : d2->m_consts) {
add_const(v1, n);
}
it = d2->m_as_arrays.begin();
end = d2->m_as_arrays.end();
for (; it != end; ++it) {
add_as_array(v1, *it);
for (enode * n : d2->m_as_arrays) {
add_as_array(v1, n);
}
TRACE("array",
tout << mk_pp(get_enode(v1)->get_owner(), get_manager()) << "\n";
@ -367,21 +339,13 @@ namespace smt {
SASSERT(v != null_theory_var);
v = find(v);
var_data* d = m_var_data[v];
ptr_vector<enode>::iterator it, end;
it = d->m_stores.begin();
end = d->m_stores.end();
for(; it != end; ++it) {
enode * store = *it;
for (enode * store : d->m_stores) {
SASSERT(is_store(store));
instantiate_default_store_axiom(store);
}
if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
it = d->m_parent_stores.begin();
end = d->m_parent_stores.end();
for (; it != end; ++it) {
enode* store = *it;
for (enode * store : d->m_parent_stores) {
SASSERT(is_store(store));
if (!m_params.m_array_cg || store->is_cgr()) {
instantiate_default_store_axiom(store);
@ -399,23 +363,15 @@ namespace smt {
v = find(v);
var_data_full* d_full = m_var_data_full[v];
var_data* d = m_var_data[v];
ptr_vector<enode>::iterator it = d_full->m_consts.begin();
ptr_vector<enode>::iterator end = d_full->m_consts.end();
for (; it != end; ++it) {
instantiate_select_const_axiom(s, *it);
for (enode * n : d_full->m_consts) {
instantiate_select_const_axiom(s, n);
}
it = d_full->m_maps.begin();
end = d_full->m_maps.end();
for (; it != end; ++it) {
enode* map = *it;
for (enode * map : d_full->m_maps) {
SASSERT(is_map(map));
instantiate_select_map_axiom(s, map);
}
if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
it = d_full->m_parent_maps.begin();
end = d_full->m_parent_maps.end();
for (; it != end; ++it) {
enode* map = *it;
for (enode * map : d_full->m_parent_maps) {
SASSERT(is_map(map));
if (!m_params.m_array_cg || map->is_cgr()) {
instantiate_select_map_axiom(s, map);
@ -437,7 +393,7 @@ namespace smt {
enode * arg = ctx.get_enode(n->get_arg(0));
theory_var v = arg->get_th_var(get_id());
SASSERT(v != null_theory_var);
add_parent_select(find(v), node);
add_parent_select(find(v), node);
}
else if (is_default(n)) {
enode * arg = ctx.get_enode(n->get_arg(0));
@ -577,7 +533,14 @@ namespace smt {
return try_assign_eq(val, def);
}
/**
* instantiate f(ep1,ep2,..,ep_n) = default(as-array f)
* it is disabled to avoid as-array terms during search.
*/
bool theory_array_full::instantiate_default_as_array_axiom(enode* arr) {
return false;
#if 0
context& ctx = get_context();
if (!ctx.add_fingerprint(this, 0, 1, &arr)) {
return false;
@ -595,6 +558,7 @@ namespace smt {
ctx.internalize(def, false);
ctx.internalize(val.get(), false);
return try_assign_eq(val.get(), def);
#endif
}
bool theory_array_full::has_large_domain(app* array_term) {

34
src/smt/theory_fpa.cpp
View file

@ -843,14 +843,12 @@ namespace smt {
context & ctx = get_context();
bool first = true;
ptr_vector<enode>::const_iterator it = ctx.begin_enodes();
ptr_vector<enode>::const_iterator end = ctx.end_enodes();
for (; it != end; it++) {
theory_var v = (*it)->get_th_var(get_family_id());
for (enode* n : ctx.enodes()) {
theory_var v = n->get_th_var(get_family_id());
if (v != -1) {
if (first) out << "fpa theory variables:" << std::endl;
out << v << " -> " <<
mk_ismt2_pp((*it)->get_owner(), m) << std::endl;
mk_ismt2_pp(n->get_owner(), m) << std::endl;
first = false;
}
}
@ -858,30 +856,24 @@ namespace smt {
if (first) return;
out << "bv theory variables:" << std::endl;
it = ctx.begin_enodes();
end = ctx.end_enodes();
for (; it != end; it++) {
theory_var v = (*it)->get_th_var(m_bv_util.get_family_id());
for (enode * n : ctx.enodes()) {
theory_var v = n->get_th_var(m_bv_util.get_family_id());
if (v != -1) out << v << " -> " <<
mk_ismt2_pp((*it)->get_owner(), m) << std::endl;
mk_ismt2_pp(n->get_owner(), m) << std::endl;
}
out << "arith theory variables:" << std::endl;
it = ctx.begin_enodes();
end = ctx.end_enodes();
for (; it != end; it++) {
theory_var v = (*it)->get_th_var(m_arith_util.get_family_id());
for (enode* n : ctx.enodes()) {
theory_var v = n->get_th_var(m_arith_util.get_family_id());
if (v != -1) out << v << " -> " <<
mk_ismt2_pp((*it)->get_owner(), m) << std::endl;
mk_ismt2_pp(n->get_owner(), m) << std::endl;
}
out << "equivalence classes:\n";
it = ctx.begin_enodes();
end = ctx.end_enodes();
for (; it != end; ++it) {
expr * n = (*it)->get_owner();
expr * r = (*it)->get_root()->get_owner();
out << r->get_id() << " --> " << mk_ismt2_pp(n, m) << std::endl;
for (enode * n : ctx.enodes()) {
expr * e = n->get_owner();
expr * r = n->get_root()->get_owner();
out << r->get_id() << " --> " << mk_ismt2_pp(e, m) << std::endl;
}
}
};