mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
5e6fa5ee6f
|
@ -87,6 +87,7 @@ namespace datalog {
|
|||
for (func_decl_set::iterator I = output_preds.begin(),
|
||||
E = output_preds.end(); I != E; ++I) {
|
||||
func_decl* sym = *I;
|
||||
TRACE("dl", tout << sym->get_name() << "\n";);
|
||||
const rule_vector& output_rules = m_rules.get_predicate_rules(sym);
|
||||
for (unsigned i = 0; i < output_rules.size(); ++i) {
|
||||
m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value.init_down(m_context, output_rules[i]);
|
||||
|
|
|
@ -738,6 +738,7 @@ namespace pdr {
|
|||
// model_node
|
||||
|
||||
void model_node::set_closed() {
|
||||
TRACE("pdr", tout << state() << "\n";);
|
||||
pt().close(state());
|
||||
m_closed = true;
|
||||
}
|
||||
|
@ -928,7 +929,7 @@ namespace pdr {
|
|||
model_node* p = n.parent();
|
||||
while (p) {
|
||||
if (p->state() == n.state()) {
|
||||
TRACE("pdr", tout << "repeated\n";);
|
||||
TRACE("pdr", tout << n.state() << "repeated\n";);
|
||||
return true;
|
||||
}
|
||||
p = p->parent();
|
||||
|
@ -1018,6 +1019,11 @@ namespace pdr {
|
|||
SASSERT(n1->children().empty());
|
||||
enqueue_leaf(n1);
|
||||
}
|
||||
|
||||
if (!nodes.empty() && n.get_model_ptr() && backtrack) {
|
||||
model_ref mr(n.get_model_ptr());
|
||||
nodes[0]->set_model(mr);
|
||||
}
|
||||
if (nodes.empty()) {
|
||||
cache(n).remove(n.state());
|
||||
}
|
||||
|
@ -1149,17 +1155,21 @@ namespace pdr {
|
|||
ast_manager& m = n->pt().get_manager();
|
||||
if (!n->get_model_ptr()) {
|
||||
if (models.find(n->state(), md)) {
|
||||
TRACE("pdr", tout << mk_pp(n->state(), m) << "\n";);
|
||||
TRACE("pdr", tout << n->state() << "\n";);
|
||||
model_ref mr(md);
|
||||
n->set_model(mr);
|
||||
datalog::rule const* rule = rules.find(n->state());
|
||||
n->set_rule(rule);
|
||||
}
|
||||
else {
|
||||
TRACE("pdr", tout << "no model for " << n->state() << "\n";);
|
||||
IF_VERBOSE(1, n->display(verbose_stream() << "no model:\n", 0);
|
||||
verbose_stream() << mk_pp(n->state(), m) << "\n";);
|
||||
verbose_stream() << n->state() << "\n";);
|
||||
}
|
||||
}
|
||||
else {
|
||||
TRACE("pdr", tout << n->state() << "\n";);
|
||||
}
|
||||
todo.pop_back();
|
||||
todo.append(n->children().size(), n->children().c_ptr());
|
||||
}
|
||||
|
@ -2027,11 +2037,11 @@ namespace pdr {
|
|||
switch (expand_state(n, cube, uses_level)) {
|
||||
case l_true:
|
||||
if (n.level() == 0) {
|
||||
TRACE("pdr", tout << "reachable at level 0\n";);
|
||||
TRACE("pdr", n.display(tout << "reachable at level 0\n", 0););
|
||||
close_node(n);
|
||||
}
|
||||
else {
|
||||
TRACE("pdr", tout << "node: " << &n << "\n";);
|
||||
TRACE("pdr", n.display(tout, 0););
|
||||
create_children(n);
|
||||
}
|
||||
break;
|
||||
|
|
|
@ -240,7 +240,7 @@ namespace pdr {
|
|||
void check_pre_closed();
|
||||
void set_closed();
|
||||
void set_open();
|
||||
void set_pre_closed() { m_closed = true; }
|
||||
void set_pre_closed() { TRACE("pdr", tout << state() << "\n";); m_closed = true; }
|
||||
void reset() { m_children.reset(); }
|
||||
|
||||
void set_rule(datalog::rule const* r) { m_rule = r; }
|
||||
|
|
|
@ -41,6 +41,9 @@ namespace datalog {
|
|||
bool new_tail = false;
|
||||
bool contained = true;
|
||||
for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) {
|
||||
if (m_context.has_facts(r->get_decl(i))) {
|
||||
return 0;
|
||||
}
|
||||
if (r->is_neg_tail(i)) {
|
||||
if (!engine.get_fact(r->get_decl(i)).is_reachable()) {
|
||||
if (!new_tail) {
|
||||
|
|
|
@ -154,7 +154,7 @@ namespace opt {
|
|||
m_soft_constraints(m), m_answer(m) {}
|
||||
|
||||
lbool maxsmt::operator()() {
|
||||
lbool is_sat;
|
||||
lbool is_sat = l_undef;
|
||||
m_msolver = 0;
|
||||
symbol const& maxsat_engine = m_c.maxsat_engine();
|
||||
IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
|
||||
|
|
Loading…
Reference in a new issue