mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

fix #2791

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-08 11:09:02 +03:00
parent 5da0902dd4
commit e6dc557c68
2 changed files with 31 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/datatype_decl_plugin.cpp
View file

@ -953,6 +953,8 @@ namespace datatype {
m_asts.push_back(ty); m_asts.push_back(ty);
m_vectors.push_back(r); m_vectors.push_back(r);
m_datatype2constructors.insert(ty, r); m_datatype2constructors.insert(ty, r);
if (!is_declared(ty))
m.raise_exception("datatype constructors have not been created");
def const& d = get_def(ty); def const& d = get_def(ty);
for (constructor const* c : d) { for (constructor const* c : d) {
func_decl_ref f = c->instantiate(ty); func_decl_ref f = c->instantiate(ty);

33
src/qe/nlqsat.cpp
View file

@ -251,7 +251,6 @@ namespace qe {
stats m_stats; stats m_stats;
statistics m_st; statistics m_st;
obj_hashtable<expr> m_free_vars; obj_hashtable<expr> m_free_vars;
obj_hashtable<expr> m_aux_vars;
expr_ref_vector m_answer; expr_ref_vector m_answer;
expr_safe_replace m_answer_simplify; expr_safe_replace m_answer_simplify;
expr_ref_vector m_trail; expr_ref_vector m_trail;
@ -661,7 +660,6 @@ namespace qe {
m_st.reset(); m_st.reset();
s.m_solver.collect_statistics(m_st); s.m_solver.collect_statistics(m_st);
m_free_vars.reset(); m_free_vars.reset();
m_aux_vars.reset();
m_answer.reset(); m_answer.reset();
m_answer_simplify.reset(); m_answer_simplify.reset();
m_trail.reset(); m_trail.reset();
@ -779,7 +777,7 @@ namespace qe {
for (auto const& kv : s.m_t2x) { for (auto const& kv : s.m_t2x) {
nlsat::var x = kv.m_value; nlsat::var x = kv.m_value;
expr * t = kv.m_key; expr * t = kv.m_key;
if (!is_uninterp_const(t) || !m_free_vars.contains(t) || m_aux_vars.contains(t)) if (!is_uninterp_const(t) || !m_free_vars.contains(t))
continue; continue;
expr * v; expr * v;
try { try {
@ -797,7 +795,7 @@ namespace qe {
for (auto const& kv : s.m_a2b) { for (auto const& kv : s.m_a2b) {
expr * a = kv.m_key; expr * a = kv.m_key;
nlsat::bool_var b = kv.m_value; nlsat::bool_var b = kv.m_value;
if (a == nullptr || !is_uninterp_const(a) || b == s.m_is_true.var() || !m_free_vars.contains(a) || m_aux_vars.contains(a)) if (a == nullptr || !is_uninterp_const(a) || b == s.m_is_true.var() || !m_free_vars.contains(a))
continue; continue;
lbool val = s.m_bmodel0.get(b, l_undef); lbool val = s.m_bmodel0.get(b, l_undef);
if (val == l_undef) if (val == l_undef)
@ -879,6 +877,33 @@ namespace qe {
model_converter_ref mc; model_converter_ref mc;
VERIFY(mk_model(mc)); VERIFY(mk_model(mc));
in->add(mc.get()); in->add(mc.get());
model_ref mdl;
model_converter2model(m, mc.get(), mdl);
for (expr* f : fmls) {
if (is_ground(f))
std::cout << mk_pp(f, m) << " |-> " << (*mdl)(f) << "\n";
}
break;
ptr_vector<expr> todo;
todo.append(fmls.size(), fmls.c_ptr());
ast_mark visited;
while (!todo.empty()) {
expr* e = todo.back();
todo.pop_back();
if (visited.is_marked(e)) continue;
visited.mark(e, true);
if (is_ground(e)) {
std::cout << mk_pp(e, m) << " |-> " << (*mdl)(e) << "\n";
}
if (is_app(e)) {
for (expr* arg : *to_app(e)) todo.push_back(arg);
}
else if (is_quantifier(e)) {
todo.push_back(to_quantifier(e)->get_expr());
}
}
} }
break; break;
case l_undef: case l_undef: