mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

aligning simplifier and rewriter for regression tests

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-04 09:28:40 -07:00
parent a3dba5b2f9
commit f12a4f04fd
12 changed files with 125 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/api/api_datatype.cpp
View file

@ -51,7 +51,7 @@ extern "C" {
constructor_decl* constrs[1] = { mk_constructor_decl(to_symbol(name), recognizer, acc.size(), acc.c_ptr()) };
{
datatype_decl * dt = mk_datatype_decl(to_symbol(name), 1, constrs);
datatype_decl * dt = mk_datatype_decl(dt_util, to_symbol(name), 1, constrs);
bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, 0, 0, tuples);
del_datatype_decl(dt);
@ -113,7 +113,7 @@ extern "C" {
{
datatype_decl * dt = mk_datatype_decl(to_symbol(name), n, constrs.c_ptr());
datatype_decl * dt = mk_datatype_decl(dt_util, to_symbol(name), n, constrs.c_ptr());
bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &dt, 0, 0, sorts);
del_datatype_decl(dt);
@ -160,6 +160,7 @@ extern "C" {
LOG_Z3_mk_list_sort(c, name, elem_sort, nil_decl, is_nil_decl, cons_decl, is_cons_decl, head_decl, tail_decl);
RESET_ERROR_CODE();
ast_manager& m = mk_c(c)->m();
datatype_util& dt_util = mk_c(c)->dtutil();
mk_c(c)->reset_last_result();
datatype_util data_util(m);
accessor_decl* head_tail[2] = {
@ -174,7 +175,7 @@ extern "C" {
sort_ref_vector sorts(m);
{
datatype_decl * decl = mk_datatype_decl(to_symbol(name), 2, constrs);
datatype_decl * decl = mk_datatype_decl(dt_util, to_symbol(name), 2, constrs);
bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &decl, 0, 0, sorts);
del_datatype_decl(decl);
@ -316,6 +317,7 @@ extern "C" {
Z3_symbol name,
unsigned num_constructors,
Z3_constructor constructors[]) {
datatype_util& dt_util = mk_c(c)->dtutil();
ptr_vector<constructor_decl> constrs;
for (unsigned i = 0; i < num_constructors; ++i) {
constructor* cn = reinterpret_cast<constructor*>(constructors[i]);
@ -330,7 +332,7 @@ extern "C" {
}
constrs.push_back(mk_constructor_decl(cn->m_name, cn->m_tester, acc.size(), acc.c_ptr()));
}
return mk_datatype_decl(to_symbol(name), num_constructors, constrs.c_ptr());
return mk_datatype_decl(dt_util, to_symbol(name), num_constructors, constrs.c_ptr());
}
Z3_sort Z3_API Z3_mk_datatype(Z3_context c,

2
src/ast/datatype_decl_plugin.cpp
View file

@ -95,7 +95,7 @@ public:
ptr_vector<constructor_decl> const & get_constructors() const { return m_constructors; }
};
datatype_decl * mk_datatype_decl(symbol const & n, unsigned num_constructors, constructor_decl * const * cs) {
datatype_decl * mk_datatype_decl(datatype_util&, symbol const & n, unsigned num_constructors, constructor_decl * const * cs) {
return alloc(datatype_decl, n, num_constructors, cs);
}

12
src/ast/datatype_decl_plugin.h
View file

@ -16,7 +16,7 @@ Author:
Revision History:
--*/
// define DATATYPE_V2
//define DATATYPE_V2
#ifdef DATATYPE_V2
#include "ast/datatype_decl_plugin2.h"
#else
@ -79,14 +79,14 @@ class datatype_decl;
class datatype_util;
accessor_decl * mk_accessor_decl(symbol const & n, type_ref const & t);
void del_accessor_decl(accessor_decl * d);
void del_accessor_decls(unsigned num, accessor_decl * const * as);
//void del_accessor_decl(accessor_decl * d);
//void del_accessor_decls(unsigned num, accessor_decl * const * as);
// Remark: the constructor becomes the owner of the accessor_decls
constructor_decl * mk_constructor_decl(symbol const & n, symbol const & r, unsigned num_accessors, accessor_decl * const * acs);
void del_constructor_decl(constructor_decl * d);
void del_constructor_decls(unsigned num, constructor_decl * const * cs);
//void del_constructor_decl(constructor_decl * d);
//void del_constructor_decls(unsigned num, constructor_decl * const * cs);
// Remark: the datatype becomes the owner of the constructor_decls
datatype_decl * mk_datatype_decl(symbol const & n, unsigned num_constructors, constructor_decl * const * cs);
datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_constructors, constructor_decl * const * cs);
void del_datatype_decl(datatype_decl * d);
void del_datatype_decls(unsigned num, datatype_decl * const * ds);

64
src/ast/datatype_decl_plugin2.cpp
View file

@ -1,5 +1,5 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Copyright (c) 2017 Microsoft Corporation
Module Name:
@ -11,18 +11,21 @@ Abstract:
Author:
Leonardo de Moura (leonardo) 2008-01-10.
Nikolaj Bjorner (nbjorner) 2017-9-1
Revision History:
--*/
#include "ast/datatype_decl_plugin.h"
#ifdef DATATYPE_V2
#include "util/warning.h"
#include "ast/datatype_decl_plugin2.h"
#include "ast/array_decl_plugin.h"
#include "ast/ast_smt2_pp.h"
#ifdef DATATYPE_V2
namespace datatype {
void accessor::fix_range(sort_ref_vector const& dts) {
@ -57,6 +60,7 @@ namespace datatype {
util& constructor::u() const { return m_def->u(); }
func_decl_ref constructor::instantiate(sort_ref_vector const& ps) const {
ast_manager& m = ps.get_manager();
sort_ref_vector domain(m);
for (accessor const* a : accessors()) {
domain.push_back(a->instantiate(ps)->get_range());
@ -281,6 +285,11 @@ namespace datatype {
}
}
def* plugin::mk(symbol const& name, unsigned n, sort * const * params) {
ast_manager& m = *m_manager;
return alloc(def, m, u(), name, m_class_id, n, params);
}
def& plugin::add(symbol const& name, unsigned n, sort * const * params) {
ast_manager& m = *m_manager;
def* d = 0;
@ -313,6 +322,21 @@ namespace datatype {
u().compute_datatype_size_functions(m_def_block);
}
bool plugin::mk_datatypes(unsigned num_datatypes, def * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts) {
begin_def_block();
for (unsigned i = 0; i < num_datatypes; ++i) {
if (m_defs.find(datatypes[i]->name(), d)) dealloc(d);
m_defs.insert(datatypes[i]->name(), datatypes[i]);
m_def_block.push_back(datatypes[i]->name());
}
end_def_block();
sort_ref_vector ps(*m_manager);
for (symbol const& s : m_def_block) {
new_sorts.push_back(m_defs[s]->instantiate(ps));
}
return true;
}
void plugin::del(symbol const& s) {
def* d = 0;
if (m_defs.find(s, d)) dealloc(d);
@ -705,7 +729,7 @@ namespace datatype {
return d;
}
func_decl * util::get_recognizer_constructor(func_decl * recognizer) {
func_decl * util::get_recognizer_constructor(func_decl * recognizer) const {
SASSERT(is_recognizer(recognizer));
return to_func_decl(recognizer->get_parameter(0).get_ast());
}
@ -856,6 +880,22 @@ namespace datatype {
return 0;
}
unsigned util::get_constructor_idx(func_decl * f) const {
unsigned idx = 0;
def const& d = get_def(f->get_range());
for (constructor* c : d) {
if (c->name() == f->get_name()) {
return idx;
}
++idx;
}
UNREACHABLE();
return 0;
}
unsigned util::get_recognizer_constructor_idx(func_decl * f) const {
return get_constructor_idx(get_recognizer_constructor(f));
}
/**
\brief Two datatype sorts s1 and s2 are siblings if they were
@ -870,6 +910,12 @@ namespace datatype {
}
}
unsigned util::get_datatype_num_constructors(sort * ty) {
def const& d = get_def(ty->get_name());
return d.constructors().size();
}
void util::display_datatype(sort *s0, std::ostream& strm) {
ast_mark mark;
ptr_buffer<sort> todo;
@ -902,4 +948,14 @@ namespace datatype {
}
}
}
datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_constructors, constructor_decl * const * cs) {
datatype::decl::plugin* p = u.get_plugin();
datatype::def( d = p->mk(n, 0, 0);
for (unsigned i = 0; i < num_constructors; ++i) {
d->add(cs[i]);
}
return d;
}
#endif

45
src/ast/datatype_decl_plugin2.h
View file

@ -1,5 +1,5 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Copyright (c) 2017 Microsoft Corporation
Module Name:
@ -11,10 +11,13 @@ Abstract:
Author:
Leonardo de Moura (leonardo) 2008-01-09.
Nikolaj Bjorner (nbjorner) 2017-9-1
Revision History:
rewritten to support SMTLIB-2.6 parameters from
Leonardo de Moura (leonardo) 2008-01-09.
--*/
#ifndef DATATYPE_DECL_PLUGIN2_H_
#define DATATYPE_DECL_PLUGIN2_H_
@ -74,12 +77,11 @@ namespace datatype {
};
class constructor {
ast_manager& m;
symbol m_name;
ptr_vector<accessor> m_accessors;
def* m_def;
public:
constructor(ast_manager& m, symbol n): m(m), m_name(n) {}
constructor(symbol n): m_name(n) {}
~constructor();
void add(accessor* a) { m_accessors.push_back(a); a->attach(this); }
symbol const& name() const { return m_name; }
@ -262,8 +264,12 @@ namespace datatype {
def& add(symbol const& name, unsigned n, sort * const * params);
def* mk(symbol const& name, unsigned n, sort * const * params);
void del(symbol const& d);
bool mk_datatypes(unsigned num_datatypes, def * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts);
def const& get_def(sort* s) const { return *(m_defs[datatype_name(s)]); }
def& get_def(symbol const& s) { return *(m_defs[s]); }
@ -299,9 +305,7 @@ namespace datatype {
family_id m_family_id;
mutable decl::plugin* m_plugin;
func_decl * get_constructor(sort * ty, unsigned c_id) const;
obj_map<sort, ptr_vector<func_decl> *> m_datatype2constructors;
obj_map<sort, func_decl *> m_datatype2nonrec_constructor;
obj_map<func_decl, ptr_vector<func_decl> *> m_constructor2accessors;
@ -310,14 +314,13 @@ namespace datatype {
obj_map<func_decl, func_decl *> m_accessor2constructor;
obj_map<sort, bool> m_is_recursive;
obj_map<sort, bool> m_is_enum;
mutable obj_map<sort, bool> m_is_fully_interp;
mutable obj_map<sort, bool> m_is_fully_interp;
mutable ast_ref_vector m_asts;
ptr_vector<ptr_vector<func_decl> > m_vectors;
unsigned m_start;
mutable ptr_vector<sort> m_fully_interp_trail;
mutable ptr_vector<sort> m_fully_interp_trail;
func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
func_decl * get_constructor(sort * ty, unsigned c_id);
friend class decl::plugin;
@ -353,7 +356,7 @@ namespace datatype {
func_decl * get_constructor_recognizer(func_decl * constructor);
ptr_vector<func_decl> const & get_constructor_accessors(func_decl * constructor);
func_decl * get_accessor_constructor(func_decl * accessor);
func_decl * get_recognizer_constructor(func_decl * recognizer);
func_decl * get_recognizer_constructor(func_decl * recognizer) const;
family_id get_family_id() const { return m_family_id; }
bool are_siblings(sort * s1, sort * s2);
bool is_func_decl(op_kind k, unsigned num_params, parameter const* params, func_decl* f);
@ -362,11 +365,12 @@ namespace datatype {
void display_datatype(sort *s, std::ostream& strm);
bool is_fully_interp(sort * s) const;
sort_ref_vector datatype_params(sort * s) const;
unsigned get_constructor_idx(func_decl * f) const;
unsigned get_recognizer_constructor_idx(func_decl * f) const;
};
};
#ifdef DATATYPE_V2
typedef datatype::accessor accessor_decl;
typedef datatype::constructor constructor_decl;
typedef datatype::def datatype_decl;
@ -394,7 +398,22 @@ inline accessor_decl * mk_accessor_decl(symbol const & n, type_ref const & t) {
return alloc(accessor_decl, n, t.get_sort());
}
}
#endif
inline constructor_decl * mk_constructor_decl(symbol const & n, symbol const & r, unsigned num_accessors, accessor_decl * * acs) {
constructor_decl* c = alloc(constructor_decl, n);
for (unsigned i = 0; i < num_accessors; ++i) {
c->add(acs[i]);
}
return c;
}
// Remark: the datatype becomes the owner of the constructor_decls
datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_constructors, constructor_decl * const * cs);
inline void del_datatype_decl(datatype_decl * d) {}
inline void del_datatype_decls(unsigned num, datatype_decl * const * ds) {}
#endif /* DATATYPE_DECL_PLUGIN_H_ */

4
src/ast/rewriter/arith_rewriter.cpp
View file

@ -455,7 +455,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
st = BR_DONE;
}
}
if (is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) {
if (m_arith_lhs && is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) {
a2.neg();
new_arg2 = m_util.mk_numeral(a2, m_util.is_int(new_arg1));
switch (kind) {
@ -523,7 +523,7 @@ expr_ref arith_rewriter::neg_monomial(expr* e) const {
}
else {
args.push_back(m_util.mk_numeral(rational(-1), m_util.is_int(e)));
args.append(to_app(e)->get_num_args(), to_app(e)->get_args());
args.push_back(e);
}
}
else {

1
src/ast/rewriter/poly_rewriter.h
View file

@ -36,6 +36,7 @@ protected:
bool m_sort_sums;
bool m_hoist_mul;
bool m_hoist_cmul;
bool m_ast_order;
bool is_numeral(expr * n) const { return Config::is_numeral(n); }
bool is_numeral(expr * n, numeral & r) const { return Config::is_numeral(n, r); }

7
src/ast/rewriter/poly_rewriter_def.h
View file

@ -18,7 +18,8 @@ Notes:
--*/
#include "ast/rewriter/poly_rewriter.h"
#include "ast/rewriter/poly_rewriter_params.hpp"
// include "ast/ast_lt.h"
#include "ast/rewriter/arith_rewriter_params.hpp"
#include "ast/ast_lt.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_smt2_pp.h"
@ -33,6 +34,8 @@ void poly_rewriter<Config>::updt_params(params_ref const & _p) {
m_som_blowup = p.som_blowup();
if (!m_flat) m_som = false;
if (m_som) m_hoist_mul = false;
arith_rewriter_params ap(_p);
m_ast_order = !ap.arith_ineq_lhs();
}
template<typename Config>
@ -485,6 +488,8 @@ void poly_rewriter<Config>::hoist_cmul(expr_ref_buffer & args) {
template<typename Config>
bool poly_rewriter<Config>::mon_lt::operator()(expr* e1, expr * e2) const {
if (rw.m_ast_order)
return lt(e1,e2);
return ordinal(e1) < ordinal(e2);
}

7
src/cmd_context/pdecl.cpp
View file

@ -566,7 +566,8 @@ datatype_decl * pdatatype_decl::instantiate_decl(pdecl_manager & m, sort * const
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, cs.size(), cs.c_ptr());
}
struct datatype_decl_buffer {
@ -679,9 +680,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;
};

9
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;
@ -139,10 +140,10 @@ public:
virtual void display(std::ostream & out) const;
};
class datatype_decl_plugin;
class datatype_decl;
class constructor_decl;
class accessor_decl;
//class datatype_decl_plugin;
//class datatype_decl;
//class constructor_decl;
//class accessor_decl;
class pdatatypes_decl;
class pdatatype_decl;

4
src/muz/bmc/dl_bmc_engine.cpp
View file

@ -979,7 +979,7 @@ namespace datalog {
symbol is_name(_name.str().c_str());
cnstrs.push_back(mk_constructor_decl(name, is_name, accs.size(), accs.c_ptr()));
}
dts.push_back(mk_datatype_decl(pred->get_name(), cnstrs.size(), cnstrs.c_ptr()));
dts.push_back(mk_datatype_decl(dtu, pred->get_name(), cnstrs.size(), cnstrs.c_ptr()));
}
@ -1027,7 +1027,7 @@ namespace datalog {
accs.push_back(mk_accessor_decl(name, tr));
cnstrs.push_back(mk_constructor_decl(name, is_name, accs.size(), accs.c_ptr()));
}
dts.push_back(mk_datatype_decl(symbol("Path"), cnstrs.size(), cnstrs.c_ptr()));
dts.push_back(mk_datatype_decl(dtu, symbol("Path"), cnstrs.size(), cnstrs.c_ptr()));
VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), 0, 0, new_sorts));
m_path_sort = new_sorts[0].get();
}

3
src/test/get_consequences.cpp
View file

@ -65,9 +65,8 @@ void test2() {
constructor_decl* G = mk_constructor_decl(symbol("G"), symbol("is-G"), 0, 0);
constructor_decl* B = mk_constructor_decl(symbol("B"), symbol("is-B"), 0, 0);
constructor_decl* constrs[3] = { R, G, B };
datatype_decl * enum_sort = mk_datatype_decl(symbol("RGB"), 3, constrs);
datatype_decl * enum_sort = mk_datatype_decl(dtutil, symbol("RGB"), 3, constrs);
VERIFY(dt.mk_datatypes(1, &enum_sort, 0, 0, new_sorts));
del_constructor_decls(3, constrs);
sort* rgb = new_sorts[0].get();
expr_ref x = mk_const(m, "x", rgb), y = mk_const(m, "y", rgb), z = mk_const(m, "z", rgb);