mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 13:53:39 +00:00
Code Activity

Merge pull request #1226 from NikolajBjorner/master

Browse source 
removing dependencies on simplifier, support SMTLIB2 parametric algebraic datatypes.
This is a breaking change. It introduces two substantial changes:
1. The legacy simplifier is removed. It was obsoleted with the introduction of the rewriter facilities, but many dependencies made it a major change to remove the legacy simplifier. All uses of the legacy simplifier have now been replaced by corresponding calls to the rewriter. It means that some normalization may behave differently. At this point, Z3 passes regressions and passes performance tests without regressing.
2. Algebraic datatypes in the form of SMT-LIB2.6 are now supported. These generalize the datatypes supported so far as parametric datatype constructors may be applied to different arguments within a recursive definition.
This commit is contained in:
Nikolaj Bjorner 2017-09-11 00:40:51 +03:00 • committed by GitHub
commit 77008dc411
198 changed files with 5392 additions and 12493 deletions
Download patch file Download diff file Expand all files Collapse all files

42
src/cmd_context/basic_cmds.cpp
View file

@ -15,21 +15,21 @@ Author:
Notes:
--*/
#include "cmd_context/cmd_context.h"
#include "util/gparams.h"
#include "util/env_params.h"
#include "util/version.h"
#include "ast/ast_smt_pp.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_pp.h"
#include "model/model_smt2_pp.h"
#include "ast/array_decl_plugin.h"
#include "ast/pp.h"
#include "ast/well_sorted.h"
#include "ast/pp_params.hpp"
#include "model/model_smt2_pp.h"
#include "cmd_context/cmd_context.h"
#include "cmd_context/cmd_util.h"
#include "cmd_context/simplify_cmd.h"
#include "cmd_context/eval_cmd.h"
#include "util/gparams.h"
#include "util/env_params.h"
#include "ast/well_sorted.h"
#include "ast/pp_params.hpp"
class help_cmd : public cmd {
svector<symbol> m_cmds;
@ -79,19 +79,15 @@ public:
}
// named_cmd_lt is not a total order for commands, but this is irrelevant for Linux x Windows behavior
std::sort(cmds.begin(), cmds.end(), named_cmd_lt());
vector<named_cmd>::const_iterator it2 = cmds.begin();
vector<named_cmd>::const_iterator end2 = cmds.end();
for (; it2 != end2; ++it2) {
display_cmd(ctx, it2->first, it2->second);
for (named_cmd const& nc : cmds) {
display_cmd(ctx, nc.first, nc.second);
}
}
else {
svector<symbol>::const_iterator it = m_cmds.begin();
svector<symbol>::const_iterator end = m_cmds.end();
for (; it != end; ++it) {
cmd * c = ctx.find_cmd(*it);
for (symbol const& s : m_cmds) {
cmd * c = ctx.find_cmd(s);
SASSERT(c);
display_cmd(ctx, *it, c);
display_cmd(ctx, s, c);
}
}
ctx.regular_stream() << "\"\n";
@ -136,11 +132,10 @@ ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", {
ctx.get_check_sat_result()->get_model(m);
ctx.regular_stream() << "(";
dictionary<macro_decls> const & macros = ctx.get_macros();
dictionary<macro_decls>::iterator it = macros.begin();
dictionary<macro_decls>::iterator end = macros.end();
for (bool first = true; it != end; ++it) {
symbol const & name = (*it).m_key;
macro_decls const & _m = (*it).m_value;
bool first = true;
for (auto const& kv : macros) {
symbol const & name = kv.m_key;
macro_decls const & _m = kv.m_value;
for (auto md : _m) {
if (md.m_domain.size() == 0 && ctx.m().is_bool(md.m_body)) {
expr_ref val(ctx.m());
@ -211,14 +206,13 @@ static void print_core(cmd_context& ctx) {
ptr_vector<expr> core;
ctx.get_check_sat_result()->get_unsat_core(core);
ctx.regular_stream() << "(";
ptr_vector<expr>::const_iterator it = core.begin();
ptr_vector<expr>::const_iterator end = core.end();
for (bool first = true; it != end; ++it) {
bool first = true;
for (expr* e : core) {
if (first)
first = false;
else
ctx.regular_stream() << " ";
ctx.regular_stream() << mk_ismt2_pp(*it, ctx.m());
ctx.regular_stream() << mk_ismt2_pp(e, ctx.m());
}
ctx.regular_stream() << ")" << std::endl;
}

133
src/cmd_context/cmd_context.cpp
View file

@ -18,7 +18,10 @@ Notes:
#include<signal.h>
#include "util/tptr.h"
#include "cmd_context/cmd_context.h"
#include "util/cancel_eh.h"
#include "util/scoped_ctrl_c.h"
#include "util/dec_ref_util.h"
#include "util/scoped_timer.h"
#include "ast/func_decl_dependencies.h"
#include "ast/arith_decl_plugin.h"
#include "ast/bv_decl_plugin.h"
@ -31,22 +34,19 @@ Notes:
#include "ast/rewriter/var_subst.h"
#include "ast/pp.h"
#include "ast/ast_smt2_pp.h"
#include "cmd_context/basic_cmds.h"
#include "util/cancel_eh.h"
#include "util/scoped_ctrl_c.h"
#include "util/dec_ref_util.h"
#include "ast/decl_collector.h"
#include "ast/well_sorted.h"
#include "model/model_evaluator.h"
#include "ast/for_each_expr.h"
#include "util/scoped_timer.h"
#include "cmd_context/interpolant_cmds.h"
#include "ast/rewriter/th_rewriter.h"
#include "model/model_evaluator.h"
#include "model/model_smt2_pp.h"
#include "model/model_v2_pp.h"
#include "model/model_params.hpp"
#include "ast/rewriter/th_rewriter.h"
#include "tactic/tactic_exception.h"
#include "solver/smt_logics.h"
#include "cmd_context/basic_cmds.h"
#include "cmd_context/interpolant_cmds.h"
#include "cmd_context/cmd_context.h"
func_decls::func_decls(ast_manager & m, func_decl * f):
m_decls(TAG(func_decl*, f, 0)) {
@ -61,11 +61,9 @@ void func_decls::finalize(ast_manager & m) {
else {
TRACE("func_decls", tout << "finalize...\n";);
func_decl_set * fs = UNTAG(func_decl_set *, m_decls);
func_decl_set::iterator it = fs->begin();
func_decl_set::iterator end = fs->end();
for (; it != end; ++it) {
TRACE("func_decls", tout << "dec_ref of " << (*it)->get_name() << " ref_count: " << (*it)->get_ref_count() << "\n";);
m.dec_ref(*it);
for (func_decl * f : *fs) {
TRACE("func_decls", tout << "dec_ref of " << f->get_name() << " ref_count: " << f->get_ref_count() << "\n";);
m.dec_ref(f);
}
dealloc(fs);
}
@ -161,10 +159,7 @@ bool func_decls::clash(func_decl * f) const {
if (GET_TAG(m_decls) == 0)
return false;
func_decl_set * fs = UNTAG(func_decl_set *, m_decls);
func_decl_set::iterator it = fs->begin();
func_decl_set::iterator end = fs->end();
for (; it != end; ++it) {
func_decl * g = *it;
for (func_decl * g : *fs) {
if (g == f)
continue;
if (g->get_arity() != f->get_arity())
@ -201,10 +196,7 @@ func_decl * func_decls::find(unsigned arity, sort * const * domain, sort * range
if (!more_than_one())
return first();
func_decl_set * fs = UNTAG(func_decl_set *, m_decls);
func_decl_set::iterator it = fs->begin();
func_decl_set::iterator end = fs->end();
for (; it != end; it++) {
func_decl * f = *it;
for (func_decl * f : *fs) {
if (range != 0 && f->get_range() != range)
continue;
if (f->get_arity() != arity)
@ -607,10 +599,8 @@ void cmd_context::register_builtin_sorts(decl_plugin * p) {
svector<builtin_name> names;
p->get_sort_names(names, m_logic);
family_id fid = p->get_family_id();
svector<builtin_name>::const_iterator it = names.begin();
svector<builtin_name>::const_iterator end = names.end();
for (; it != end; ++it) {
psort_decl * d = pm().mk_psort_builtin_decl((*it).m_name, fid, (*it).m_kind);
for (builtin_name const& n : names) {
psort_decl * d = pm().mk_psort_builtin_decl(n.m_name, fid, n.m_kind);
insert(d);
}
}
@ -619,17 +609,15 @@ void cmd_context::register_builtin_ops(decl_plugin * p) {
svector<builtin_name> names;
p->get_op_names(names, m_logic);
family_id fid = p->get_family_id();
svector<builtin_name>::const_iterator it = names.begin();
svector<builtin_name>::const_iterator end = names.end();
for (; it != end; ++it) {
if (m_builtin_decls.contains((*it).m_name)) {
builtin_decl & d = m_builtin_decls.find((*it).m_name);
builtin_decl * new_d = alloc(builtin_decl, fid, (*it).m_kind, d.m_next);
for (builtin_name const& n : names) {
if (m_builtin_decls.contains(n.m_name)) {
builtin_decl & d = m_builtin_decls.find(n.m_name);
builtin_decl * new_d = alloc(builtin_decl, fid, n.m_kind, d.m_next);
d.m_next = new_d;
m_extra_builtin_decls.push_back(new_d);
}
else {
m_builtin_decls.insert((*it).m_name, builtin_decl(fid, (*it).m_kind));
m_builtin_decls.insert(n.m_name, builtin_decl(fid, n.m_kind));
}
}
}
@ -686,8 +674,6 @@ bool cmd_context::logic_has_datatype() const {
void cmd_context::init_manager_core(bool new_manager) {
SASSERT(m_manager != 0);
SASSERT(m_pmanager != 0);
m_dt_eh = alloc(dt_eh, *this);
m_pmanager->set_new_datatype_eh(m_dt_eh.get());
if (new_manager) {
decl_plugin * basic = m_manager->get_plugin(m_manager->get_basic_family_id());
register_builtin_sorts(basic);
@ -715,16 +701,16 @@ void cmd_context::init_manager_core(bool new_manager) {
load_plugin(symbol("seq"), logic_has_seq(), fids);
load_plugin(symbol("fpa"), logic_has_fpa(), fids);
load_plugin(symbol("pb"), logic_has_pb(), fids);
svector<family_id>::iterator it = fids.begin();
svector<family_id>::iterator end = fids.end();
for (; it != end; ++it) {
decl_plugin * p = m_manager->get_plugin(*it);
for (family_id fid : fids) {
decl_plugin * p = m_manager->get_plugin(fid);
if (p) {
register_builtin_sorts(p);
register_builtin_ops(p);
}
}
}
m_dt_eh = alloc(dt_eh, *this);
m_pmanager->set_new_datatype_eh(m_dt_eh.get());
if (!has_logic()) {
// add list type only if the logic is not specified.
// it prevents clashes with builtin types.
@ -1170,11 +1156,8 @@ void cmd_context::erase_object_ref(symbol const & s) {
}
void cmd_context::reset_func_decls() {
dictionary<func_decls>::iterator it = m_func_decls.begin();
dictionary<func_decls>::iterator end = m_func_decls.end();
for (; it != end; ++it) {
func_decls fs = (*it).m_value;
fs.finalize(m());
for (auto & kv : m_func_decls) {
kv.m_value.finalize(m());
}
m_func_decls.reset();
m_func_decls_stack.reset();
@ -1182,10 +1165,8 @@ void cmd_context::reset_func_decls() {
}
void cmd_context::reset_psort_decls() {
dictionary<psort_decl*>::iterator it = m_psort_decls.begin();
dictionary<psort_decl*>::iterator end = m_psort_decls.end();
for (; it != end; ++it) {
psort_decl * p = (*it).m_value;
for (auto & kv : m_psort_decls) {
psort_decl * p = kv.m_value;
pm().dec_ref(p);
}
m_psort_decls.reset();
@ -1201,19 +1182,14 @@ void cmd_context::reset_macros() {
}
void cmd_context::reset_cmds() {
dictionary<cmd*>::iterator it = m_cmds.begin();
dictionary<cmd*>::iterator end = m_cmds.end();
for (; it != end; ++it) {
cmd * c = (*it).m_value;
c->reset(*this);
for (auto& kv : m_cmds) {
kv.m_value->reset(*this);
}
}
void cmd_context::finalize_cmds() {
dictionary<cmd*>::iterator it = m_cmds.begin();
dictionary<cmd*>::iterator end = m_cmds.end();
for (; it != end; ++it) {
cmd * c = (*it).m_value;
for (auto& kv : m_cmds) {
cmd * c = kv.m_value;
c->finalize(*this);
dealloc(c);
}
@ -1226,10 +1202,8 @@ void cmd_context::reset_user_tactics() {
}
void cmd_context::reset_object_refs() {
dictionary<object_ref*>::iterator it = m_object_refs.begin();
dictionary<object_ref*>::iterator end = m_object_refs.end();
for (; it != end; ++it) {
object_ref * r = (*it).m_value;
for (auto& kv : m_object_refs) {
object_ref * r = kv.m_value;
r->dec_ref(*this);
}
m_object_refs.reset();
@ -1564,10 +1538,8 @@ void cmd_context::reset_assertions() {
mk_solver();
}
restore_assertions(0);
svector<scope>::iterator it = m_scopes.begin();
svector<scope>::iterator end = m_scopes.end();
for (; it != end; ++it) {
it->m_assertions_lim = 0;
for (scope& s : m_scopes) {
s.m_assertions_lim = 0;
if (m_solver) m_solver->push();
}
}
@ -1799,10 +1771,7 @@ void cmd_context::set_solver_factory(solver_factory * f) {
mk_solver();
// assert formulas and create scopes in the new solver.
unsigned lim = 0;
svector<scope>::iterator it = m_scopes.begin();
svector<scope>::iterator end = m_scopes.end();
for (; it != end; ++it) {
scope & s = *it;
for (scope& s : m_scopes) {
for (unsigned i = lim; i < s.m_assertions_lim; i++) {
m_solver->assert_expr(m_assertions[i]);
}
@ -1839,11 +1808,9 @@ void cmd_context::display_statistics(bool show_total_time, double total_time) {
void cmd_context::display_assertions() {
if (!m_interactive_mode)
throw cmd_exception("command is only available in interactive mode, use command (set-option :interactive-mode true)");
std::vector<std::string>::const_iterator it = m_assertion_strings.begin();
std::vector<std::string>::const_iterator end = m_assertion_strings.end();
regular_stream() << "(";
for (bool first = true; it != end; ++it) {
std::string const & s = *it;
bool first = true;
for (std::string const& s : m_assertion_strings) {
if (first)
first = false;
else
@ -1919,10 +1886,8 @@ void cmd_context::display(std::ostream & out, func_decl * d, unsigned indent) co
}
void cmd_context::dump_assertions(std::ostream & out) const {
ptr_vector<expr>::const_iterator it = m_assertions.begin();
ptr_vector<expr>::const_iterator end = m_assertions.end();
for (; it != end; ++it) {
display(out, *it);
for (expr * e : m_assertions) {
display(out, e);
out << std::endl;
}
}
@ -1981,21 +1946,15 @@ cmd_context::dt_eh::~dt_eh() {
void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) {
TRACE("new_dt_eh", tout << "new datatype: "; m_owner.pm().display(tout, dt); tout << "\n";);
ptr_vector<func_decl> const * constructors = m_dt_util.get_datatype_constructors(dt);
unsigned num_constructors = constructors->size();
for (unsigned j = 0; j < num_constructors; j++) {
func_decl * c = constructors->get(j);
m_owner.insert(c);
for (func_decl * c : *m_dt_util.get_datatype_constructors(dt)) {
TRACE("new_dt_eh", tout << "new constructor: " << c->get_name() << "\n";);
m_owner.insert(c);
func_decl * r = m_dt_util.get_constructor_recognizer(c);
m_owner.insert(r);
TRACE("new_dt_eh", tout << "new recognizer: " << r->get_name() << "\n";);
ptr_vector<func_decl> const * accessors = m_dt_util.get_constructor_accessors(c);
unsigned num_accessors = accessors->size();
for (unsigned k = 0; k < num_accessors; k++) {
func_decl * a = accessors->get(k);
m_owner.insert(a);
for (func_decl * a : *m_dt_util.get_constructor_accessors(c)) {
TRACE("new_dt_eh", tout << "new accessor: " << a->get_name() << "\n";);
m_owner.insert(a);
}
}
if (m_owner.m_scopes.size() > 0) {

307
src/cmd_context/pdecl.cpp
View file

@ -39,15 +39,13 @@ public:
}
else {
SASSERT(m_const == 0);
obj_map<sort, void *>::iterator it = m_map.begin();
obj_map<sort, void *>::iterator end = m_map.end();
for (; it != end; ++it) {
m.m().dec_ref((*it).m_key);
for (auto kv : m_map) {
m.m().dec_ref(kv.m_key);
if (m_num_params == 1) {
m.m().dec_ref(static_cast<sort*>((*it).m_value));
m.m().dec_ref(static_cast<sort*>(kv.m_value));
}
else {
psort_inst_cache * child = static_cast<psort_inst_cache*>((*it).m_value);
psort_inst_cache * child = static_cast<psort_inst_cache*>(kv.m_value);
child->finalize(m);
child->~psort_inst_cache();
m.a().deallocate(sizeof(psort_inst_cache), child);
@ -172,9 +170,10 @@ public:
virtual char const * hcons_kind() const { return "psort_var"; }
virtual unsigned hcons_hash() const { return hash_u_u(m_num_params, m_idx); }
virtual bool hcons_eq(psort const * other) const {
if (other->hcons_kind() != hcons_kind())
return false;
return get_num_params() == other->get_num_params() && m_idx == static_cast<psort_var const *>(other)->m_idx;
return
other->hcons_kind() == hcons_kind() &&
get_num_params() == other->get_num_params() &&
m_idx == static_cast<psort_var const *>(other)->m_idx;
}
virtual void display(std::ostream & out) const {
out << "s_" << m_idx;
@ -268,8 +267,8 @@ public:
psort_decl::psort_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n):
pdecl(id, num_params),
m_psort_kind(PSORT_BASE),
m_name(n),
m_psort_kind(PSORT_BASE),
m_inst_cache(0) {
}
@ -294,27 +293,6 @@ sort * psort_decl::find(sort * const * s) {
return m_inst_cache->find(s);
}
#if 0
psort_dt_decl::psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager& m, symbol const& n):
psort_decl(id, num_params, m, n) {
}
void psort_dt_decl::finalize(pdecl_manager& m) {
psort_decl::finalize(m);
}
sort * psort_dt_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
UNREACHABLE();
return 0;
}
void psort_dt_decl::display(std::ostream & out) const {
out << get_name() << " " << get_num_params();
}
#endif
psort_user_decl::psort_user_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, psort * p) :
psort_decl(id, num_params, m, n),
m_def(p) {
@ -367,6 +345,27 @@ void psort_user_decl::display(std::ostream & out) const {
out << ")";
}
// -------------------
// psort_dt_decl
psort_dt_decl::psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n) :
psort_decl(id, num_params, m, n) {
m_psort_kind = PSORT_DT;
}
sort * psort_dt_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
SASSERT(n == m_num_params);
return m.instantiate_datatype(this, m_name, n, s);
}
void psort_dt_decl::display(std::ostream & out) const {
out << "(datatype-sort " << m_name << ")";
}
// -------------------
// psort_builtin_decl
psort_builtin_decl::psort_builtin_decl(unsigned id, pdecl_manager & m, symbol const & n, family_id fid, decl_kind k):
psort_decl(id, PSORT_DECL_VAR_PARAMS, m, n),
m_fid(fid),
@ -458,8 +457,8 @@ bool paccessor_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol
accessor_decl * paccessor_decl::instantiate_decl(pdecl_manager & m, sort * const * s) {
switch (m_type.kind()) {
case PTR_REC_REF: return mk_accessor_decl(m_name, type_ref(m_type.get_idx()));
case PTR_PSORT: return mk_accessor_decl(m_name, type_ref(m_type.get_psort()->instantiate(m, s)));
case PTR_REC_REF: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_idx()));
case PTR_PSORT: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_psort()->instantiate(m, s)));
default:
// missing refs must have been eliminated.
UNREACHABLE();
@ -488,20 +487,16 @@ void pconstructor_decl::finalize(pdecl_manager & m) {
}
bool pconstructor_decl::has_missing_refs(symbol & missing) const {
ptr_vector<paccessor_decl>::const_iterator it = m_accessors.begin();
ptr_vector<paccessor_decl>::const_iterator end = m_accessors.end();
for (; it != end; ++it) {
if ((*it)->has_missing_refs(missing))
for (paccessor_decl* a : m_accessors) {
if (a->has_missing_refs(missing))
return true;
}
return false;
}
bool pconstructor_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing) {
ptr_vector<paccessor_decl>::iterator it = m_accessors.begin();
ptr_vector<paccessor_decl>::iterator end = m_accessors.end();
for (; it != end; ++it) {
if (!(*it)->fix_missing_refs(symbol2idx, missing))
for (paccessor_decl* a : m_accessors) {
if (!a->fix_missing_refs(symbol2idx, missing))
return false;
}
return true;
@ -509,20 +504,16 @@ bool pconstructor_decl::fix_missing_refs(dictionary<int> const & symbol2idx, sym
constructor_decl * pconstructor_decl::instantiate_decl(pdecl_manager & m, sort * const * s) {
ptr_buffer<accessor_decl> as;
ptr_vector<paccessor_decl>::iterator it = m_accessors.begin();
ptr_vector<paccessor_decl>::iterator end = m_accessors.end();
for (; it != end; ++it)
as.push_back((*it)->instantiate_decl(m, s));
for (paccessor_decl* a : m_accessors)
as.push_back(a->instantiate_decl(m, s));
return mk_constructor_decl(m_name, m_recogniser_name, as.size(), as.c_ptr());
}
void pconstructor_decl::display(std::ostream & out, pdatatype_decl const * const * dts) const {
out << "(" << m_name;
ptr_vector<paccessor_decl>::const_iterator it = m_accessors.begin();
ptr_vector<paccessor_decl>::const_iterator end = m_accessors.end();
for (; it != end; ++it) {
for (paccessor_decl* a : m_accessors) {
out << " ";
(*it)->display(out, dts);
a->display(out, dts);
}
out << ")";
}
@ -541,23 +532,17 @@ void pdatatype_decl::finalize(pdecl_manager & m) {
}
bool pdatatype_decl::has_missing_refs(symbol & missing) const {
ptr_vector<pconstructor_decl>::const_iterator it = m_constructors.begin();
ptr_vector<pconstructor_decl>::const_iterator end = m_constructors.end();
for (; it != end; ++it) {
if ((*it)->has_missing_refs(missing))
for (auto c : m_constructors)
if (c->has_missing_refs(missing))
return true;
}
return false;
}
bool pdatatype_decl::has_duplicate_accessors(symbol & duplicated) const {
hashtable<symbol, symbol_hash_proc, symbol_eq_proc> names;
ptr_vector<pconstructor_decl>::const_iterator it = m_constructors.begin();
ptr_vector<pconstructor_decl>::const_iterator end = m_constructors.end();
for (; it != end; ++it) {
ptr_vector<paccessor_decl> const& acc = (*it)->m_accessors;
for (unsigned i = 0; i < acc.size(); ++i) {
symbol const& name = acc[i]->get_name();
for (auto c : m_constructors) {
for (auto a : c->m_accessors) {
symbol const& name = a->get_name();
if (names.contains(name)) {
duplicated = name;
return true;
@ -570,10 +555,8 @@ bool pdatatype_decl::has_duplicate_accessors(symbol & duplicated) const {
bool pdatatype_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing) {
ptr_vector<pconstructor_decl>::iterator it = m_constructors.begin();
ptr_vector<pconstructor_decl>::iterator end = m_constructors.end();
for (; it != end; ++it) {
if (!(*it)->fix_missing_refs(symbol2idx, missing))
for (auto c : m_constructors) {
if (!c->fix_missing_refs(symbol2idx, missing))
return false;
}
return true;
@ -581,12 +564,11 @@ bool pdatatype_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol
datatype_decl * pdatatype_decl::instantiate_decl(pdecl_manager & m, sort * const * s) {
ptr_buffer<constructor_decl> cs;
ptr_vector<pconstructor_decl>::iterator it = m_constructors.begin();
ptr_vector<pconstructor_decl>::iterator end = m_constructors.end();
for (; it != end; ++it) {
cs.push_back((*it)->instantiate_decl(m, s));
for (auto c : m_constructors) {
cs.push_back(c->instantiate_decl(m, s));
}
return mk_datatype_decl(m_name, cs.size(), cs.c_ptr());
datatype_util util(m.m());
return mk_datatype_decl(util, m_name, m_num_params, s, cs.size(), cs.c_ptr());
}
struct datatype_decl_buffer {
@ -594,67 +576,86 @@ struct datatype_decl_buffer {
~datatype_decl_buffer() { del_datatype_decls(m_buffer.size(), m_buffer.c_ptr()); }
};
sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
SASSERT(m_num_params == n);
sort * r = find(s);
if (r)
return r;
if (m_parent != 0) {
if (m_parent->instantiate(m, s)) {
r = find(s);
SASSERT(r);
return r;
sort * r = m.instantiate_datatype(this, m_name, n, s);
datatype_util util(m.m());
if (r && n > 0 && util.is_declared(r)) {
ast_mark mark;
datatype::def const& d = util.get_def(r);
mark.mark(r, true);
sort_ref_vector params(m.m(), n, s);
for (datatype::constructor* c : d) {
for (datatype::accessor* a : *c) {
sort* rng = a->range();
if (util.is_datatype(rng) && !mark.is_marked(rng) && m_parent) {
mark.mark(rng, true);
// TBD: search over more than just parents
for (pdatatype_decl* p : *m_parent) {
if (p->get_name() == rng->get_name()) {
ptr_vector<sort> ps;
func_decl_ref acc = a->instantiate(params);
for (unsigned j = 0; j < util.get_datatype_num_parameter_sorts(rng); ++j) {
ps.push_back(util.get_datatype_parameter_sort(acc->get_range(), j));
}
m.instantiate_datatype(p, p->get_name(), ps.size(), ps.c_ptr());
break;
}
}
}
}
}
}
else {
datatype_decl_buffer dts;
dts.m_buffer.push_back(instantiate_decl(m, s));
datatype_decl * d_ptr = dts.m_buffer[0];
sort_ref_vector sorts(m.m());
bool is_ok = m.get_dt_plugin()->mk_datatypes(1, &d_ptr, m_num_params, s, sorts);
TRACE("pdatatype_decl", tout << "instantiating " << m_name << " is_ok: " << is_ok << "\n";);
if (is_ok) {
r = sorts.get(0);
cache(m, s, r);
m.save_info(r, this, n, s);
m.notify_new_dt(r, this);
return r;
}
}
return 0;
return r;
}
void pdatatype_decl::display(std::ostream & out) const {
out << "(declare-datatype " << m_name;
display_sort_args(out, m_num_params);
ptr_vector<pconstructor_decl>::const_iterator it = m_constructors.begin();
ptr_vector<pconstructor_decl>::const_iterator end = m_constructors.end();
for (bool first = true; it != end; ++it) {
bool first = true;
for (auto c : m_constructors) {
if (!first)
out << " ";
if (m_parent) {
(*it)->display(out, m_parent->children());
c->display(out, m_parent->children());
}
else {
pdatatype_decl const * dts[1] = { this };
(*it)->display(out, dts);
c->display(out, dts);
}
first = false;
}
out << ")";
}
bool pdatatype_decl::commit(pdecl_manager& m) {
TRACE("datatype", tout << m_name << "\n";);
sort_ref_vector ps(m.m());
for (unsigned i = 0; i < m_num_params; ++i) {
ps.push_back(m.m().mk_uninterpreted_sort(symbol(i), 0, 0));
}
datatype_decl_buffer dts;
dts.m_buffer.push_back(instantiate_decl(m, ps.c_ptr()));
datatype_decl * d_ptr = dts.m_buffer[0];
sort_ref_vector sorts(m.m());
bool is_ok = m.get_dt_plugin()->mk_datatypes(1, &d_ptr, m_num_params, ps.c_ptr(), sorts);
if (is_ok && m_num_params == 0) {
m.notify_new_dt(sorts.get(0), this);
}
return is_ok;
}
pdatatypes_decl::pdatatypes_decl(unsigned id, unsigned num_params, pdecl_manager & m,
unsigned num_datatypes, pdatatype_decl * const * dts):
pdecl(id, num_params),
m_datatypes(num_datatypes, dts) {
m.inc_ref(num_datatypes, dts);
ptr_vector<pdatatype_decl>::iterator it = m_datatypes.begin();
ptr_vector<pdatatype_decl>::iterator end = m_datatypes.end();
for (; it != end; ++it) {
SASSERT((*it)->m_parent == 0);
(*it)->m_parent = this;
for (auto d : m_datatypes) {
SASSERT(d->m_parent == 0);
d->m_parent = this;
}
}
@ -665,38 +666,67 @@ void pdatatypes_decl::finalize(pdecl_manager & m) {
bool pdatatypes_decl::fix_missing_refs(symbol & missing) {
TRACE("fix_missing_refs", tout << "pdatatypes_decl::fix_missing_refs\n";);
dictionary<int> symbol2idx;
ptr_vector<pdatatype_decl>::iterator it = m_datatypes.begin();
ptr_vector<pdatatype_decl>::iterator end = m_datatypes.end();
for (unsigned idx = 0; it != end; ++it, ++idx)
symbol2idx.insert((*it)->get_name(), idx);
it = m_datatypes.begin();
for (unsigned idx = 0; it != end; ++it, ++idx) {
if (!(*it)->fix_missing_refs(symbol2idx, missing))
int idx = 0;
for (pdatatype_decl* d : m_datatypes)
symbol2idx.insert(d->get_name(), idx++);
for (pdatatype_decl* d : m_datatypes)
if (!d->fix_missing_refs(symbol2idx, missing))
return false;
}
return true;
}
sort* pdecl_manager::instantiate_datatype(psort_decl* p, symbol const& name, unsigned n, sort * const* s) {
TRACE("datatype", tout << name << " "; for (unsigned i = 0; i < n; ++i) tout << s[i]->get_name() << " "; tout << "\n";);
pdecl_manager& m = *this;
sort * r = p->find(s);
if (r)
return r;
buffer<parameter> ps;
ps.push_back(parameter(name));
for (unsigned i = 0; i < n; i++)
ps.push_back(parameter(s[i]));
datatype_util util(m.m());
r = m.m().mk_sort(util.get_family_id(), DATATYPE_SORT, ps.size(), ps.c_ptr());
p->cache(m, s, r);
m.save_info(r, p, n, s);
if (n > 0 && util.is_declared(r)) {
bool has_typevar = false;
// crude check ..
for (unsigned i = 0; !has_typevar && i < n; ++i) {
has_typevar = s[i]->get_name().is_numerical();
}
if (!has_typevar) {
m.notify_new_dt(r, p);
}
}
return r;
}
bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) {
UNREACHABLE();
return false;
}
bool pdatatypes_decl::commit(pdecl_manager& m) {
datatype_decl_buffer dts;
ptr_vector<pdatatype_decl>::iterator it = m_datatypes.begin();
ptr_vector<pdatatype_decl>::iterator end = m_datatypes.end();
for (; it != end; ++it) {
dts.m_buffer.push_back((*it)->instantiate_decl(m, s));
for (pdatatype_decl* d : m_datatypes) {
sort_ref_vector ps(m.m());
for (unsigned i = 0; i < d->get_num_params(); ++i) {
ps.push_back(m.m().mk_uninterpreted_sort(symbol(i), 0, 0));
}
dts.m_buffer.push_back(d->instantiate_decl(m, ps.c_ptr()));
}
sort_ref_vector sorts(m.m());
bool is_ok = m.get_dt_plugin()->mk_datatypes(dts.m_buffer.size(), dts.m_buffer.c_ptr(), m_num_params, s, sorts);
if (!is_ok)
return false;
it = m_datatypes.begin();
for (unsigned i = 0; it != end; ++it, ++i) {
sort * new_dt = sorts.get(i);
(*it)->cache(m, s, new_dt);
m.save_info(new_dt, *it, m_num_params, s);
m.notify_new_dt(new_dt, *it);
bool is_ok = m.get_dt_plugin()->mk_datatypes(m_datatypes.size(), dts.m_buffer.c_ptr(), 0, nullptr, sorts);
if (is_ok) {
for (unsigned i = 0; i < m_datatypes.size(); ++i) {
pdatatype_decl* d = m_datatypes[i];
if (d->get_num_params() == 0) {
m.notify_new_dt(sorts.get(i), this);
}
}
}
return true;
return is_ok;
}
struct pdecl_manager::sort_info {
@ -708,9 +738,7 @@ struct pdecl_manager::sort_info {
}
virtual ~sort_info() {}
virtual unsigned obj_size() const { return sizeof(sort_info); }
virtual void finalize(pdecl_manager & m) {
m.dec_ref(m_decl);
}
virtual void finalize(pdecl_manager & m) { m.dec_ref(m_decl); }
virtual void display(std::ostream & out, pdecl_manager const & m) const = 0;
virtual format * pp(pdecl_manager const & m) const = 0;
};
@ -810,6 +838,7 @@ void pdecl_manager::init_list() {
mk_pconstructor_decl(1, symbol("insert"), symbol("is-insert"), 2, as) };
m_list = mk_pdatatype_decl(1, symbol("List"), 2, cs);
inc_ref(m_list);
m_list->commit(*this);
}
pdecl_manager::pdecl_manager(ast_manager & m):
@ -841,9 +870,8 @@ psort * pdecl_manager::register_psort(psort * n) {
psort * r = m_table.insert_if_not_there(n);
if (r != n) {
del_decl_core(n);
return r;
}
return n;
return r;
}
psort * pdecl_manager::mk_psort_var(unsigned num_params, unsigned vidx) {
@ -862,6 +890,7 @@ pconstructor_decl * pdecl_manager::mk_pconstructor_decl(unsigned num_params,
}
pdatatype_decl * pdecl_manager::mk_pdatatype_decl(unsigned num_params, symbol const & s, unsigned num, pconstructor_decl * const * cs) {
TRACE("datatype", tout << s << " has " << num_params << " parameters\n";);
return new (a().allocate(sizeof(pdatatype_decl))) pdatatype_decl(m_id_gen.mk(), num_params, *this,
s, num, cs);
}
@ -888,10 +917,10 @@ psort_decl * pdecl_manager::mk_psort_user_decl(unsigned num_params, symbol const
return new (a().allocate(sizeof(psort_user_decl))) psort_user_decl(m_id_gen.mk(), num_params, *this, n, def);
}
psort_decl * pdecl_manager::mk_psort_dt_decl(unsigned num_params, symbol const & n) {
return new (a().allocate(sizeof(psort_dt_decl))) psort_dt_decl(m_id_gen.mk(), num_params, *this, n);
}
//psort_decl * pdecl_manager::mk_psort_dt_decl(unsigned num_params, symbol const & n) {
// return new (a().allocate(sizeof(psort_dt_decl))) psort_dt_decl(m_id_gen.mk(), num_params, *this, n);
//}
psort_decl * pdecl_manager::mk_psort_builtin_decl(symbol const & n, family_id fid, decl_kind k) {
return new (a().allocate(sizeof(psort_builtin_decl))) psort_builtin_decl(m_id_gen.mk(), *this, n, fid, k);
@ -968,11 +997,9 @@ void pdecl_manager::save_info(sort * s, psort_decl * d, unsigned num_indices, un
}
void pdecl_manager::reset_sort_info() {
obj_map<sort, sort_info *>::iterator it = m_sort2info.begin();
obj_map<sort, sort_info *>::iterator end = m_sort2info.end();
for (; it != end; ++it) {
sort * s = (*it).m_key;
sort_info * info = (*it).m_value;
for (auto kv : m_sort2info) {
sort * s = kv.m_key;
sort_info * info = kv.m_value;
m().dec_ref(s);
unsigned sz = info->obj_size();
info->finalize(*this);

21
src/cmd_context/pdecl.h
View file

@ -23,6 +23,7 @@ Revision History:
#include "util/obj_hashtable.h"
#include "util/dictionary.h"
#include "ast/format.h"
#include "ast/datatype_decl_plugin.h"
class pdecl_manager;
@ -86,7 +87,7 @@ typedef ptr_hashtable<psort, psort_hash_proc, psort_eq_proc> psort_table;
#define PSORT_DECL_VAR_PARAMS UINT_MAX
typedef enum { PSORT_BASE = 0, PSORT_USER, PSORT_BUILTIN } psort_decl_kind;
typedef enum { PSORT_BASE = 0, PSORT_USER, PSORT_BUILTIN, PSORT_DT } psort_decl_kind;
class psort_decl : public pdecl {
protected:
@ -110,6 +111,7 @@ public:
virtual void reset_cache(pdecl_manager& m);
bool is_user_decl() const { return m_psort_kind == PSORT_USER; }
bool is_builtin_decl() const { return m_psort_kind == PSORT_BUILTIN; }
bool is_dt_decl() const { return m_psort_kind == PSORT_DT; }
};
class psort_user_decl : public psort_decl {
@ -124,7 +126,7 @@ public:
virtual sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s);
virtual void display(std::ostream & out) const;
};
class psort_builtin_decl : public psort_decl {
protected:
friend class pdecl_manager;
@ -139,24 +141,17 @@ public:
virtual void display(std::ostream & out) const;
};
#if 0
class psort_dt_decl : public psort_decl {
protected:
friend class pdecl_manager;
psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n);
virtual size_t obj_size() const { return sizeof(psort_dt_decl); }
virtual void finalize(pdecl_manager & m);
virtual ~psort_dt_decl() {}
public:
virtual sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s);
virtual void display(std::ostream & out) const;
};
#endif
class datatype_decl_plugin;
class datatype_decl;
class constructor_decl;
class accessor_decl;
class pdatatypes_decl;
class pdatatype_decl;
@ -246,6 +241,7 @@ public:
virtual void display(std::ostream & out) const;
bool has_missing_refs(symbol & missing) const;
bool has_duplicate_accessors(symbol & repeated) const;
bool commit(pdecl_manager& m);
};
/**
@ -263,6 +259,10 @@ class pdatatypes_decl : public pdecl {
virtual ~pdatatypes_decl() {}
public:
pdatatype_decl const * const * children() const { return m_datatypes.c_ptr(); }
pdatatype_decl * const * begin() const { return m_datatypes.begin(); }
pdatatype_decl * const * end() const { return m_datatypes.end(); }
// commit declaration
bool commit(pdecl_manager& m);
};
class new_datatype_eh {
@ -305,7 +305,7 @@ public:
psort * mk_psort_var(unsigned num_params, unsigned vidx);
psort * mk_psort_app(unsigned num_params, psort_decl * d, unsigned num_args, psort * const * args);
psort * mk_psort_app(psort_decl * d);
// psort_decl * mk_psort_dt_decl(unsigned num_params, symbol const & n);
psort_decl * mk_psort_dt_decl(unsigned num_params, symbol const & n);
psort_decl * mk_psort_user_decl(unsigned num_params, symbol const & n, psort * def);
psort_decl * mk_psort_builtin_decl(symbol const & n, family_id fid, decl_kind k);
paccessor_decl * mk_paccessor_decl(unsigned num_params, symbol const & s, ptype const & p);
@ -314,6 +314,7 @@ public:
pdatatypes_decl * mk_pdatatypes_decl(unsigned num_params, unsigned num, pdatatype_decl * const * dts);
pdatatype_decl * mk_plist_decl() { if (!m_list) init_list(); return m_list; }
bool fix_missing_refs(pdatatypes_decl * s, symbol & missing) { return s->fix_missing_refs(missing); }
sort * instantiate_datatype(psort_decl* p, symbol const& name, unsigned n, sort * const* s);
sort * instantiate(psort * s, unsigned num, sort * const * args);
void lazy_dec_ref(pdecl * p) { p->dec_ref(); if (p->get_ref_count() == 0) m_to_delete.push_back(p); }

6
src/cmd_context/tactic_cmds.cpp
View file

@ -258,11 +258,9 @@ public:
result->m_core.append(core_elems.size(), core_elems.c_ptr());
if (p.get_bool("print_unsat_core", false)) {
ctx.regular_stream() << "(unsat-core";
ptr_vector<expr>::const_iterator it = core_elems.begin();
ptr_vector<expr>::const_iterator end = core_elems.end();
for (; it != end; ++it) {
for (expr * e : core_elems) {
ctx.regular_stream() << " ";
ctx.display(ctx.regular_stream(), *it);
ctx.display(ctx.regular_stream(), e);
}
ctx.regular_stream() << ")" << std::endl;
}