mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity

fixing #2217

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-04-05 03:06:41 -07:00
parent dfd327f287
commit f1a2e875b5
4 changed files with 19 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/api/python/z3/z3.py
View file

@ -10379,3 +10379,10 @@ def Range(lo, hi, ctx = None):
# Special Relations
def PartialOrder(n, s):
ctx = s.ctx
return FuncDeclRef(Z3_mk_partial_order(ctx, n, s.ast), ctx)
def TreeOrder(n, s):
ctx = s.ctx
return FuncDeclRef(Z3_mk_tree_order(ctx, n, s.ast), ctx)

6
src/ast/datatype_decl_plugin.cpp
View file

@ -290,6 +290,7 @@ namespace datatype {
obj_map<sort, sort_size> S;
for (unsigned i = 0; i + 1 < num_parameters; ++i) {
sort* r = to_sort(parameters[i + 1].get_ast());
TRACE("datatype", tout << "inserting " << mk_ismt2_pp(r, *m_manager) << " " << r->get_num_elements() << "\n";);
S.insert(d->params()[i], r->get_num_elements());
}
sort_size ts = d->sort_size()->eval(S);
@ -693,7 +694,7 @@ namespace datatype {
}
param_size::size* util::get_sort_size(sort_ref_vector const& params, sort* s) {
if (params.empty()) {
if (params.empty() && !is_datatype(s)) {
return param_size::size::mk_offset(s->get_num_elements());
}
if (is_datatype(s)) {
@ -742,6 +743,7 @@ namespace datatype {
map<symbol, status, symbol_hash_proc, symbol_eq_proc> already_found;
map<symbol, param_size::size*, symbol_hash_proc, symbol_eq_proc> szs;
TRACE("datatype", for (auto const& s : names) tout << s << " "; tout << "\n";);
svector<symbol> todo(names);
status st;
while (!todo.empty()) {
@ -780,6 +782,7 @@ namespace datatype {
todo.pop_back();
already_found.insert(s, BLACK);
if (is_infinite) {
TRACE("datatype", tout << "infinite " << s << "\n";);
d.set_sort_size(param_size::size::mk_offset(sort_size::mk_infinite()));
continue;
}
@ -792,6 +795,7 @@ namespace datatype {
}
s_add.push_back(param_size::size::mk_times(s_mul));
}
TRACE("datatype", tout << "set sort size " << s << "\n";);
d.set_sort_size(param_size::size::mk_plus(s_add));
}
}

1
src/smt/smt_context.h
View file

@ -923,7 +923,6 @@ namespace smt {
failure m_last_search_failure;
ptr_vector<theory> m_incomplete_theories; //!< theories that failed to produce a model
bool m_searching;
bool m_propagating;
unsigned m_num_conflicts;
unsigned m_num_conflicts_since_restart;
unsigned m_num_conflicts_since_lemma_gc;

8
src/smt/theory_datatype.cpp
View file

@ -372,7 +372,13 @@ namespace smt {
//
// If the theory variable is not created for 'a', then a wrong model will be generated.
TRACE("datatype", tout << "apply_sort_cnstr: #" << n->get_owner_id() << "\n";);
TRACE("datatype_bug", tout << "apply_sort_cnstr:\n" << mk_pp(n->get_owner(), get_manager()) << "\n";);
TRACE("datatype_bug",
tout << "apply_sort_cnstr:\n" << mk_pp(n->get_owner(), get_manager()) << " ";
tout << m_util.is_datatype(s) << " ";
if (m_util.is_datatype(s)) tout << "is-infinite: " << s->is_infinite() << " ";
if (m_util.is_datatype(s)) tout << "attached: " << is_attached_to_var(n) << " ";
tout << "\n";
);
if ((get_context().has_quantifiers() || (m_util.is_datatype(s) && !s->is_infinite())) && !is_attached_to_var(n)) {
mk_var(n);
}