mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-10-12 13:36:40 -07:00
parent 07deb6ee88
commit 72b1e8a714
3 changed files with 13 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/arith_solver.h
View file

@ -52,7 +52,7 @@ namespace arith {
// axioms // axioms
void mk_div_axiom(expr* p, expr* q); void mk_div_axiom(expr* p, expr* q);
void solver::mk_to_int_axiom(app* n); void mk_to_int_axiom(app* n);
void mk_is_int_axiom(app* n); void mk_is_int_axiom(app* n);
void pop_core(unsigned n) override; void pop_core(unsigned n) override;

21
src/sat/smt/q_solver.cpp
View file

@ -76,10 +76,17 @@ namespace q {
return v; return v;
} }
sat::literal solver::instantiate(quantifier* q, std::function<expr* (quantifier*, unsigned)>& mk_var) { sat::literal solver::instantiate(quantifier* _q, bool negate, std::function<expr* (quantifier*, unsigned)>& mk_var) {
sat::literal sk; sat::literal sk;
expr_ref tmp(m); expr_ref tmp(m);
quantifier_ref q(_q, m);
expr_ref_vector vars(m); expr_ref_vector vars(m);
if (negate) {
q = m.mk_quantifier(
is_forall(q) ? quantifier_kind::exists_k : quantifier_kind::forall_k,
q->get_num_decls(), q->get_decl_sorts(), q->get_decl_names(), m.mk_not(q->get_expr()),
q->get_weight(), q->get_qid(), q->get_skid());
}
quantifier* q_flat = flatten(q); quantifier* q_flat = flatten(q);
unsigned sz = q_flat->get_num_decls(); unsigned sz = q_flat->get_num_decls();
vars.resize(sz, nullptr); vars.resize(sz, nullptr);
@ -95,10 +102,7 @@ namespace q {
std::function<expr* (quantifier*, unsigned)> mk_var = [&](quantifier* q, unsigned i) { std::function<expr* (quantifier*, unsigned)> mk_var = [&](quantifier* q, unsigned i) {
return m.mk_fresh_const(q->get_decl_name(i), q->get_decl_sort(i)); return m.mk_fresh_const(q->get_decl_name(i), q->get_decl_sort(i));
}; };
sat::literal sk = instantiate(q, mk_var); return instantiate(q, is_forall(q), mk_var);
if (is_forall(q))
sk.neg();
return sk;
} }
/* /*
@ -109,10 +113,7 @@ namespace q {
std::function<expr* (quantifier*, unsigned)> mk_var = [&](quantifier* q, unsigned i) { std::function<expr* (quantifier*, unsigned)> mk_var = [&](quantifier* q, unsigned i) {
return get_unit(q->get_decl_sort(i)); return get_unit(q->get_decl_sort(i));
}; };
sat::literal sk = instantiate(q, mk_var); return instantiate(q, is_exists(q), mk_var);
if (is_exists(q))
sk.neg();
return sk;
} }
void solver::init_search() { void solver::init_search() {
@ -154,7 +155,7 @@ namespace q {
if (!m_unit_table.empty()) if (!m_unit_table.empty())
return; return;
for (euf::enode* n : ctx.get_egraph().nodes()) { for (euf::enode* n : ctx.get_egraph().nodes()) {
if (!n->interpreted()) if (!n->interpreted() && !m.is_uninterp(m.get_sort(n->get_expr())))
continue; continue;
expr* e = n->get_expr(); expr* e = n->get_expr();
sort* s = m.get_sort(e); sort* s = m.get_sort(e);

2
src/sat/smt/q_solver.h
View file

@ -45,7 +45,7 @@ namespace q {
sat::literal_vector m_universal; sat::literal_vector m_universal;
obj_map<sort, expr*> m_unit_table; obj_map<sort, expr*> m_unit_table;
sat::literal instantiate(quantifier* q, std::function<expr* (quantifier*, unsigned)>& mk_var); sat::literal instantiate(quantifier* q, bool negate, std::function<expr* (quantifier*, unsigned)>& mk_var);
sat::literal skolemize(quantifier* q); sat::literal skolemize(quantifier* q);
sat::literal specialize(quantifier* q); sat::literal specialize(quantifier* q);
void init_units(); void init_units();