mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-10-04 17:37:12 -07:00
commit be4bc6caed
26 changed files with 309 additions and 111 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/api/api_parsers.cpp
View file

@ -23,8 +23,12 @@ Revision History:
#include "api/api_ast_vector.h"
#include "cmd_context/cmd_context.h"
#include "smt/smt_solver.h"
#include "smt/smt2_extra_cmds.h"
#include "parsers/smt2/smt2parser.h"
#include "solver/solver_na2as.h"
#include "muz/fp/dl_cmds.h"
#include "opt/opt_cmds.h"
extern "C" {
@ -42,6 +46,10 @@ extern "C" {
Z3_TRY;
ast_manager& m = mk_c(c)->m();
scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &(m));
install_dl_cmds(*ctx.get());
install_opt_cmds(*ctx.get());
install_smt2_extra_cmds(*ctx.get());
ctx->register_plist();
ctx->set_ignore_check(true);
Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), m);

6
src/api/c++/z3++.h
View file

@ -3927,7 +3927,7 @@ namespace z3 {
user_propagator_base(solver* s): s(s), c(nullptr) {
Z3_solver_propagate_init(ctx(), *s, this, push_eh, pop_eh, fresh_eh);
}
}
virtual void push() = 0;
virtual void pop(unsigned num_scopes) = 0;
@ -3948,13 +3948,13 @@ namespace z3 {
that were created using a solver.
*/
void fixed(fixed_eh_t& f) {
void register_fixed(fixed_eh_t& f) {
assert(s);
m_fixed_eh = f;
Z3_solver_propagate_fixed(ctx(), *s, fixed_eh);
}
void eq(eq_eh_t& f) {
void register_eq(eq_eh_t& f) {
assert(s);
m_eq_eh = f;
Z3_solver_propagate_eq(ctx(), *s, eq_eh);

36
src/ast/euf/euf_egraph.cpp
View file

@ -129,7 +129,7 @@ namespace euf {
return n;
}
egraph::egraph(ast_manager& m) : m(m), m_table(m), m_tmp_app(2), m_exprs(m) {
egraph::egraph(ast_manager& m) : m(m), m_table(m), m_tmp_app(2), m_exprs(m), m_eq_decls(m) {
m_tmp_eq = enode::mk_tmp(m_region, 2);
}
@ -592,7 +592,7 @@ namespace euf {
SASSERT(!n1->get_root()->m_target);
}
bool egraph::are_diseq(enode* a, enode* b) const {
bool egraph::are_diseq(enode* a, enode* b) {
enode* ra = a->get_root(), * rb = b->get_root();
if (ra == rb)
return false;
@ -600,12 +600,7 @@ namespace euf {
return true;
if (ra->get_sort() != rb->get_sort())
return true;
expr_ref eq(m.mk_eq(a->get_expr(), b->get_expr()), m);
m_tmp_eq->m_args[0] = a;
m_tmp_eq->m_args[1] = b;
m_tmp_eq->m_expr = eq;
SASSERT(m_tmp_eq->num_args() == 2);
enode* r = m_table.find(m_tmp_eq);
enode* r = tmp_eq(ra, rb);
if (r && r->get_root()->value() == l_false)
return true;
return false;
@ -617,6 +612,18 @@ namespace euf {
return find(m_tmp_app.get_app(), num_args, args);
}
enode* egraph::tmp_eq(enode* a, enode* b) {
SASSERT(a->is_root());
SASSERT(b->is_root());
if (a->num_parents() > b->num_parents())
std::swap(a, b);
for (enode* p : enode_parents(a))
if (p->is_equality() &&
(b == p->get_arg(0)->get_root() || b == p->get_arg(1)->get_root()))
return p;
return nullptr;
}
/**
\brief generate an explanation for a congruence.
Each pair of children under a congruence have the same roots
@ -714,12 +721,7 @@ namespace euf {
explain_eq(justifications, b, rb);
return sat::null_bool_var;
}
expr_ref eq(m.mk_eq(a->get_expr(), b->get_expr()), m);
m_tmp_eq->m_args[0] = a;
m_tmp_eq->m_args[1] = b;
m_tmp_eq->m_expr = eq;
SASSERT(m_tmp_eq->num_args() == 2);
enode* r = m_table.find(m_tmp_eq);
enode* r = tmp_eq(ra, rb);
SASSERT(r && r->get_root()->value() == l_false);
explain_eq(justifications, r, r->get_root());
return r->get_root()->bool_var();
@ -818,9 +820,13 @@ namespace euf {
args.push_back(old_expr2new_enode[n1->get_arg(j)->get_expr_id()]);
expr* e2 = tr(e1);
enode* n2 = mk(e2, n1->generation(), args.size(), args.data());
old_expr2new_enode.setx(e1->get_id(), n2, nullptr);
n2->set_value(n2->value());
n2->set_value(n1->value());
n2->m_bool_var = n1->m_bool_var;
n2->m_commutative = n1->m_commutative;
n2->m_merge_enabled = n1->m_merge_enabled;
n2->m_is_equality = n1->m_is_equality;
}
for (unsigned i = 0; i < src.m_nodes.size(); ++i) {
enode* n1 = src.m_nodes[i];

5
src/ast/euf/euf_egraph.h
View file

@ -165,6 +165,7 @@ namespace euf {
tmp_app m_tmp_app;
enode_vector m_nodes;
expr_ref_vector m_exprs;
func_decl_ref_vector m_eq_decls;
vector<enode_vector> m_decl2enodes;
enode_vector m_empty_enodes;
unsigned m_num_scopes = 0;
@ -263,10 +264,12 @@ namespace euf {
/**
* \brief check if two nodes are known to be disequal.
*/
bool are_diseq(enode* a, enode* b) const;
bool are_diseq(enode* a, enode* b);
enode* get_enode_eq_to(func_decl* f, unsigned num_args, enode* const* args);
enode* tmp_eq(enode* a, enode* b);
/**
\brief Maintain and update cursor into propagated consequences.
The result of get_literal() is a pair (n, is_eq)

16
src/ast/euf/euf_enode.h
View file

@ -55,17 +55,17 @@ namespace euf {
unsigned m_table_id = UINT_MAX;
unsigned m_generation = 0; // Tracks how many quantifier instantiation rounds were needed to generate this enode.
enode_vector m_parents;
enode* m_next = nullptr;
enode* m_root = nullptr;
enode* m_target = nullptr;
enode* m_cg = nullptr;
enode* m_next = nullptr;
enode* m_root = nullptr;
enode* m_target = nullptr;
enode* m_cg = nullptr;
th_var_list m_th_vars;
justification m_justification;
unsigned m_num_args = 0;
signed char m_lbl_hash = -1; // It is different from -1, if enode is used in a pattern
approx_set m_lbls;
approx_set m_plbls;
enode* m_args[0];
signed char m_lbl_hash = -1; // It is different from -1, if enode is used in a pattern
approx_set m_lbls;
approx_set m_plbls;
enode* m_args[0];
friend class enode_args;
friend class enode_parents;

15
src/ast/has_free_vars.cpp
View file

@ -18,9 +18,10 @@ Revision History:
--*/
#include "ast/ast.h"
#include "ast/expr_delta_pair.h"
#include "ast/has_free_vars.h"
#include "util/hashtable.h"
class contains_vars {
class contains_vars::imp {
typedef hashtable<expr_delta_pair, obj_hash<expr_delta_pair>, default_eq<expr_delta_pair> > cache;
cache m_cache;
svector<expr_delta_pair> m_todo;
@ -86,6 +87,18 @@ public:
}
};
contains_vars::contains_vars() {
m_imp = alloc(imp);
}
contains_vars::~contains_vars() {
dealloc(m_imp);
}
bool contains_vars::operator()(expr* e) {
return (*m_imp)(e);
}
bool has_free_vars(expr * n) {
contains_vars p;
return p(n);

9
src/ast/has_free_vars.h
View file

@ -20,6 +20,15 @@ Revision History:
class expr;
class contains_vars {
class imp;
imp* m_imp;
public:
contains_vars();
~contains_vars();
bool operator()(expr* n);
};
bool has_free_vars(expr * n);

14
src/ast/normal_forms/pull_quant.cpp
View file

@ -20,6 +20,7 @@ Notes:
#include "ast/rewriter/var_subst.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/ast_pp.h"
#include "ast/ast_util.h"
struct pull_quant::imp {
@ -50,7 +51,7 @@ struct pull_quant::imp {
quantifier * q = to_quantifier(child);
expr * body = q->get_expr();
quantifier_kind k = q->get_kind() == forall_k ? exists_k : forall_k;
result = m.update_quantifier(q, k, m.mk_not(body));
result = m.update_quantifier(q, k, mk_not(m, body));
return true;
}
else {
@ -78,9 +79,8 @@ struct pull_quant::imp {
qid = nested_q->get_qid();
}
w = std::min(w, nested_q->get_weight());
unsigned j = nested_q->get_num_decls();
while (j > 0) {
--j;
for (unsigned j = nested_q->get_num_decls(); j-- > 0; ) {
var_sorts.push_back(nested_q->get_decl_sort(j));
symbol s = nested_q->get_decl_name(j);
if (std::find(var_names.begin(), var_names.end(), s) != var_names.end())
@ -254,6 +254,10 @@ struct pull_quant::imp {
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
if (m.is_not(f) && m.is_not(args[0])) {
result = to_app(args[0])->get_arg(0);
return BR_REWRITE1;
}
if (!m.is_or(f) && !m.is_and(f) && !m.is_not(f))
return BR_FAILED;
@ -275,7 +279,7 @@ struct pull_quant::imp {
proof_ref & result_pr) {
if (is_exists(old_q)) {
result = m.mk_not(new_body);
result = mk_not(m, new_body);
result = m.mk_not(m.update_quantifier(old_q, forall_k, result));
if (m.proofs_enabled())
m.mk_rewrite(old_q, result);

19
src/ast/rewriter/bool_rewriter.cpp
View file

@ -905,6 +905,24 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
}
}
#if 0
expr* t1, *t2;
// (ite c (not (= t1 t2)) t1) ==> (not (= t1 (and c t2)))
if (m().is_not(t, t1) && m().is_eq(t1, t1, t2) && e == t1) {
expr_ref a(m());
mk_and(c, t2, a);
result = m().mk_not(m().mk_eq(t1, a));
return BR_REWRITE2;
}
if (m().is_not(t, t1) && m().is_eq(t1, t2, t1) && e == t1) {
expr_ref a(m());
mk_and(c, t2, a);
result = m().mk_eq(t1, a);
return BR_REWRITE2;
}
#endif
if (m().is_ite(t) && m_ite_extra_rules && m_elim_ite) {
// (ite c1 (ite c2 t1 t2) t1) ==> (ite (and c1 (not c2)) t2 t1)
if (e == to_app(t)->get_arg(1)) {
@ -923,6 +941,7 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
return BR_REWRITE1;
}
if (m().is_ite(e)) {
// (ite c1 (ite c2 t1 t2) (ite c3 t1 t2)) ==> (ite (or (and c1 c2) (and (not c1) c3)) t1 t2)
if (to_app(t)->get_arg(1) == to_app(e)->get_arg(1) &&

13
src/math/lp/monomial_bounds.cpp
View file

@ -24,6 +24,11 @@ namespace nla {
}
}
bool monomial_bounds::is_too_big(mpq const& q) const {
return rational(q).bitsize() > 256;
}
/**
* Accumulate product of variables in monomial starting at position 'start'
*/
@ -51,6 +56,8 @@ namespace nla {
lp::explanation ex;
dep.get_upper_dep(range, ex);
auto const& upper = dep.upper(range);
if (is_too_big(upper))
return false;
auto cmp = dep.upper_is_open(range) ? llc::LT : llc::LE;
new_lemma lemma(c(), "propagate value - upper bound of range is below value");
lemma &= ex;
@ -62,6 +69,8 @@ namespace nla {
lp::explanation ex;
dep.get_lower_dep(range, ex);
auto const& lower = dep.lower(range);
if (is_too_big(lower))
return false;
auto cmp = dep.lower_is_open(range) ? llc::GT : llc::GE;
new_lemma lemma(c(), "propagate value - lower bound of range is above value");
lemma &= ex;
@ -106,7 +115,7 @@ namespace nla {
auto le = dep.upper_is_open(range) ? llc::LT : llc::LE;
new_lemma lemma(c(), "propagate value - root case - upper bound of range is below value");
lemma &= ex;
lemma |= ineq(v, le, r);
lemma |= ineq(v, le, r);
return true;
}
if (p % 2 == 0 && val_v.is_neg()) {
@ -114,7 +123,7 @@ namespace nla {
auto ge = dep.upper_is_open(range) ? llc::GT : llc::GE;
new_lemma lemma(c(), "propagate value - root case - upper bound of range is below negative value");
lemma &= ex;
lemma |= ineq(v, ge, -r);
lemma |= ineq(v, ge, -r);
return true;
}
}

1
src/math/lp/monomial_bounds.h
View file

@ -17,6 +17,7 @@ namespace nla {
class monomial_bounds : common {
dep_intervals& dep;
void var2interval(lpvar v, scoped_dep_interval& i);
bool is_too_big(mpq const& q) const;
bool propagate_down(monic const& m, lpvar u);
bool propagate_value(dep_interval& range, lpvar v);
bool propagate_value(dep_interval& range, lpvar v, unsigned power);

8
src/math/subpaving/tactic/expr2subpaving.cpp
View file

@ -19,9 +19,10 @@ Notes:
--*/
#include "math/subpaving/tactic/expr2subpaving.h"
#include "ast/expr2var.h"
#include "ast/arith_decl_plugin.h"
#include "ast/ast_pp.h"
#include "util/ref_util.h"
#include "util/z3_exception.h"
#include "ast/arith_decl_plugin.h"
#include "util/scoped_numeral_buffer.h"
#include "util/common_msgs.h"
@ -309,6 +310,10 @@ struct expr2subpaving::imp {
case OP_MOD:
case OP_REM:
case OP_IRRATIONAL_ALGEBRAIC_NUM:
case OP_DIV0:
case OP_REM0:
case OP_MOD0:
case OP_IDIV0:
throw default_exception("you must apply arithmetic purifier before internalizing expressions into the subpaving module.");
case OP_SIN:
case OP_COS:
@ -325,6 +330,7 @@ struct expr2subpaving::imp {
// TODO
throw default_exception("transcendental and hyperbolic functions are not supported yet.");
default:
throw default_exception("unhandled arithmetic operator in subpaving");
UNREACHABLE();
}
return subpaving::null_var;

1
src/sat/smt/array_model.cpp
View file

@ -120,7 +120,6 @@ namespace array {
bool solver::must_have_different_model_values(theory_var v1, theory_var v2) {
euf::enode* else1 = nullptr, * else2 = nullptr;
euf::enode* n1 = var2enode(v1), *n2 = var2enode(v2);
euf::enode* r1 = n1->get_root(), * r2 = n2->get_root();
expr* e1 = n1->get_expr();
if (!a.is_array(e1))
return true;

20
src/sat/smt/euf_internalize.cpp
View file

@ -13,6 +13,20 @@ Author:
Nikolaj Bjorner (nbjorner) 2020-08-25
Notes:
(*) From smt_internalizer.cpp
This code is necessary because some theories may decide
not to create theory variables for a nested application.
Example:
Suppose (+ (* 2 x) y) is internalized by arithmetic
and an enode is created for the + and * applications,
but a theory variable is only created for the + application.
The (* 2 x) is internal to the arithmetic module.
Later, the core tries to internalize (f (* 2 x)).
Now, (* 2 x) is not internal to arithmetic anymore,
and a theory variable must be created for it.
--*/
#include "ast/pb_decl_plugin.h"
@ -72,6 +86,12 @@ namespace euf {
bool solver::visit(expr* e) {
euf::enode* n = m_egraph.find(e);
th_solver* s = nullptr;
if (n && !si.is_bool_op(e) && (s = expr2solver(e), s && euf::null_theory_var == n->get_th_var(s->get_id()))) {
// ensure that theory variables are attached in shared contexts. See notes (*)
s->internalize(e, false);
return true;
}
if (n)
return true;
if (si.is_bool_op(e)) {

11
src/sat/smt/euf_solver.cpp
View file

@ -316,6 +316,7 @@ namespace euf {
}
if (n->is_equality()) {
SASSERT(!m.is_iff(e));
SASSERT(m.is_eq(e));
if (sign)
m_egraph.new_diseq(n);
else
@ -487,10 +488,10 @@ namespace euf {
return sat::check_result::CR_CONTINUE;
if (m_qsolver)
apply_solver(m_qsolver);
if (num_nodes < m_egraph.num_nodes()) {
IF_VERBOSE(1, verbose_stream() << "new nodes created, but not detected\n");
if (num_nodes < m_egraph.num_nodes())
return sat::check_result::CR_CONTINUE;
if (cont)
return sat::check_result::CR_CONTINUE;
}
TRACE("after_search", s().display(tout););
if (give_up)
return sat::check_result::CR_GIVEUP;
@ -867,9 +868,9 @@ namespace euf {
for (euf::enode* n : r->m_egraph.nodes()) {
auto b = n->bool_var();
if (b != sat::null_bool_var) {
m_bool_var2expr.setx(b, n->get_expr(), nullptr);
r->m_bool_var2expr.setx(b, n->get_expr(), nullptr);
SASSERT(r->m.is_bool(n->get_sort()));
IF_VERBOSE(11, verbose_stream() << "set bool_var " << r->bpp(n) << "\n");
IF_VERBOSE(11, verbose_stream() << "set bool_var " << b << " " << r->bpp(n) << " " << mk_bounded_pp(n->get_expr(), m) << "\n");
}
}
for (auto* s_orig : m_id2solver) {

71
src/sat/smt/q_ematch.cpp
View file

@ -240,6 +240,7 @@ namespace q {
b->m_nodes[i] = _binding[i];
binding::push_to_front(c.m_bindings, b);
ctx.push(remove_binding(ctx, c, b));
++m_stats.m_num_delayed_bindings;
}
void ematch::on_binding(quantifier* q, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_gen, unsigned max_gen) {
@ -427,33 +428,11 @@ namespace q {
expr_ref body(mk_not(m, q->get_expr()), m);
q = m.update_quantifier(q, forall_k, body);
}
expr_ref_vector ors(m);
expr_ref_vector ors(m);
flatten_or(q->get_expr(), ors);
for (expr* arg : ors) {
bool sign = m.is_not(arg, arg);
expr* l, *r;
if (m.is_distinct(arg) && to_app(arg)->get_num_args() == 2) {
l = to_app(arg)->get_arg(0);
r = to_app(arg)->get_arg(1);
sign = !sign;
}
else if (!m.is_eq(arg, l, r) || is_ground(arg)) {
l = arg;
r = sign ? m.mk_false() : m.mk_true();
sign = false;
}
if (m.is_true(l) || m.is_false(l))
std::swap(l, r);
if (sign && m.is_false(r)) {
r = m.mk_true();
sign = false;
}
else if (sign && m.is_true(r)) {
r = m.mk_false();
sign = false;
}
cl->m_lits.push_back(lit(expr_ref(l, m), expr_ref(r, m), sign));
}
for (expr* arg : ors)
cl->m_lits.push_back(clausify_literal(arg));
if (q->get_num_patterns() == 0) {
expr_ref tmp(m);
m_infer_patterns(q, tmp);
@ -468,6 +447,41 @@ namespace q {
return cl;
}
lit ematch::clausify_literal(expr* arg) {
bool sign = m.is_not(arg, arg);
expr* _l, *_r;
expr_ref l(m), r(m);
// convert into equality or equivalence
if (m.is_distinct(arg) && to_app(arg)->get_num_args() == 2) {
l = to_app(arg)->get_arg(0);
r = to_app(arg)->get_arg(1);
sign = !sign;
}
else if (!is_ground(arg) && m.is_eq(arg, _l, _r)) {
l = _l;
r = _r;
}
else {
l = arg;
r = sign ? m.mk_false() : m.mk_true();
sign = false;
}
// convert Boolean disequalities into equality
if (m.is_true(l) || m.is_false(l))
std::swap(l, r);
if (sign && m.is_false(r)) {
r = m.mk_true();
sign = false;
}
else if (sign && m.is_true(r)) {
r = m.mk_false();
sign = false;
}
return lit(l, r, sign);
}
/**
* Attach ground subterms of patterns so they appear shared.
*/
@ -591,7 +605,9 @@ namespace q {
}
if (propagate(true))
return true;
return m_inst_queue.lazy_propagate();
if (m_inst_queue.lazy_propagate())
return true;
return false;
}
void ematch::collect_statistics(statistics& st) const {
@ -599,6 +615,7 @@ namespace q {
st.update("q redundant", m_stats.m_num_redundant);
st.update("q units", m_stats.m_num_propagations);
st.update("q conflicts", m_stats.m_num_conflicts);
st.update("q delayed bindings", m_stats.m_num_delayed_bindings);
}
std::ostream& ematch::display(std::ostream& out) const {

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

@ -41,6 +41,7 @@ namespace q {
unsigned m_num_propagations;
unsigned m_num_conflicts;
unsigned m_num_redundant;
unsigned m_num_delayed_bindings;
stats() { reset(); }
@ -112,6 +113,7 @@ namespace q {
void attach_ground_pattern_terms(expr* pat);
clause* clausify(quantifier* q);
lit clausify_literal(expr* arg);
fingerprint* add_fingerprint(clause& c, binding& b, unsigned max_generation);
void set_tmp_binding(fingerprint& fp);

25
src/sat/smt/q_eval.cpp
View file

@ -25,7 +25,10 @@ namespace q {
struct eval::scoped_mark_reset {
eval& e;
scoped_mark_reset(eval& e): e(e) {}
~scoped_mark_reset() { e.m_mark.reset(); }
~scoped_mark_reset() {
e.m_mark.reset();
e.m_diseq_undef = euf::enode_pair();
}
};
eval::eval(euf::solver& ctx):
@ -97,12 +100,18 @@ namespace q {
if (sn && sn == tn)
return l_true;
if (sn && sn == m_diseq_undef.first && tn == m_diseq_undef.second)
return l_undef;
if (sn && tn && ctx.get_egraph().are_diseq(sn, tn)) {
evidence.push_back(euf::enode_pair(sn, tn));
return l_false;
}
if (sn && tn)
if (sn && tn) {
m_diseq_undef = euf::enode_pair(sn, tn);
return l_undef;
}
if (!sn && !tn)
return compare_rec(n, binding, s, t, evidence);
@ -115,7 +124,11 @@ namespace q {
std::swap(t, s);
}
unsigned sz = evidence.size();
for (euf::enode* t1 : euf::enode_class(tn)) {
unsigned count = 0;
for (euf::enode* t1 : euf::enode_class(tn)) {
if (!t1->is_cgr())
continue;
++count;
expr* t2 = t1->get_expr();
if ((c = compare_rec(n, binding, s, t2, evidence), c != l_undef)) {
evidence.push_back(euf::enode_pair(t1, tn));
@ -171,10 +184,10 @@ namespace q {
}
euf::enode* eval::operator()(unsigned n, euf::enode* const* binding, expr* e, euf::enode_pair_vector& evidence) {
if (is_ground(e))
return ctx.get_egraph().find(e);
if (m_mark.is_marked(e))
return m_eval[e->get_id()];
if (is_ground(e))
return ctx.get_egraph().find(e);
ptr_buffer<expr> todo;
ptr_buffer<euf::enode> args;
todo.push_back(e);
@ -185,7 +198,7 @@ namespace q {
todo.pop_back();
continue;
}
if (is_ground(t) || (has_quantifiers(t) && !has_free_vars(t))) {
if (is_ground(t) || (has_quantifiers(t) && !m_contains_vars(t))) {
m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr);
if (!m_eval[t->get_id()])
return nullptr;

3
src/sat/smt/q_eval.h
View file

@ -16,6 +16,7 @@ Author:
--*/
#pragma once
#include "ast/has_free_vars.h"
#include "sat/smt/q_clause.h"
namespace euf {
@ -31,6 +32,8 @@ namespace q {
euf::enode_vector m_eval;
euf::enode_vector m_indirect_nodes;
bool m_freeze_swap = false;
euf::enode_pair m_diseq_undef;
contains_vars m_contains_vars;
struct scoped_mark_reset;

1
src/sat/smt/q_mam.cpp
View file

@ -2070,7 +2070,6 @@ namespace q {
enode * n = m_registers[j2->m_reg]->get_root();
if (n->num_parents() == 0)
return nullptr;
unsigned num_args = n->num_args();
enode_vector * v = mk_enode_vector();
for (enode* p : euf::enode_parents(n)) {
if (p->get_decl() == j2->m_decl &&

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

@ -30,7 +30,8 @@ namespace q {
th_euf_solver(ctx, ctx.get_manager().get_family_name(fid), fid),
m_mbqi(ctx, *this),
m_ematch(ctx, *this),
m_expanded(ctx.get_manager())
m_expanded(ctx.get_manager()),
m_der(ctx.get_manager())
{
}
@ -45,25 +46,22 @@ namespace q {
add_clause(~l, lit);
ctx.add_root(~l, lit);
}
else {
auto const& exp = expand(q);
if (exp.size() > 1) {
for (expr* e : exp) {
sat::literal lit = ctx.internalize(e, l.sign(), false, false);
add_clause(~l, lit);
ctx.add_root(~l, lit);
}
}
else if (is_ground(q->get_expr())) {
auto lit = ctx.internalize(q->get_expr(), l.sign(), false, false);
else if (expand(q)) {
for (expr* e : m_expanded) {
sat::literal lit = ctx.internalize(e, l.sign(), false, false);
add_clause(~l, lit);
ctx.add_root(~l, lit);
}
else {
ctx.push_vec(m_universal, l);
if (ctx.get_config().m_ematching)
m_ematch.add(q);
}
}
else if (is_ground(q->get_expr())) {
auto lit = ctx.internalize(q->get_expr(), l.sign(), false, false);
add_clause(~l, lit);
ctx.add_root(~l, lit);
}
else {
ctx.push_vec(m_universal, l);
if (ctx.get_config().m_ematching)
m_ematch.add(q);
}
m_stats.m_num_quantifier_asserts++;
}
@ -223,8 +221,16 @@ namespace q {
return val;
}
expr_ref_vector const& solver::expand(quantifier* q) {
bool solver::expand(quantifier* q) {
expr_ref r(m);
proof_ref pr(m);
m_der(q, r, pr);
m_expanded.reset();
if (r != q) {
ctx.get_rewriter()(r);
m_expanded.push_back(r);
return true;
}
if (is_forall(q))
flatten_and(q->get_expr(), m_expanded);
else if (is_exists(q))
@ -232,18 +238,71 @@ namespace q {
else
UNREACHABLE();
if (m_expanded.size() == 1 && is_forall(q)) {
m_expanded.reset();
flatten_or(q->get_expr(), m_expanded);
expr_ref split1(m), split2(m), e1(m), e2(m);
unsigned idx = 0;
for (unsigned i = m_expanded.size(); i-- > 0; ) {
expr* arg = m_expanded.get(i);
if (split(arg, split1, split2)) {
if (e1)
return false;
e1 = split1;
e2 = split2;
idx = i;
}
}
if (!e1)
return false;
m_expanded[idx] = e1;
e1 = mk_or(m_expanded);
m_expanded[idx] = e2;
e2 = mk_or(m_expanded);
m_expanded.reset();
m_expanded.push_back(e1);
m_expanded.push_back(e2);
}
if (m_expanded.size() > 1) {
for (unsigned i = m_expanded.size(); i-- > 0; ) {
expr_ref tmp(m.update_quantifier(q, m_expanded.get(i)), m);
ctx.get_rewriter()(tmp);
m_expanded[i] = tmp;
}
return true;
}
else {
m_expanded.reset();
m_expanded.push_back(q);
return false;
}
bool solver::split(expr* arg, expr_ref& e1, expr_ref& e2) {
expr* x, * y, * z;
if (m.is_not(arg, x) && m.is_or(x, y, z) && is_literal(y) && is_literal(z)) {
e1 = mk_not(m, y);
e2 = mk_not(m, z);
return true;
}
return m_expanded;
if (m.is_iff(arg, x, y) && is_literal(x) && is_literal(y)) {
e1 = m.mk_implies(x, y);
e2 = m.mk_implies(y, x);
return true;
}
if (m.is_and(arg, x, y) && is_literal(x) && is_literal(y)) {
e1 = x;
e2 = y;
return true;
}
if (m.is_not(arg, z) && m.is_iff(z, x, y) && is_literal(x) && is_literal(y)) {
e1 = m.mk_or(x, y);
e2 = m.mk_or(mk_not(m, x), mk_not(m, y));
return true;
}
return false;
}
bool solver::is_literal(expr* arg) {
m.is_not(arg, arg);
return !m.is_and(arg) && !m.is_or(arg) && !m.is_iff(arg) && !m.is_implies(arg);
}
void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) {

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

@ -18,6 +18,7 @@ Author:
#include "util/obj_hashtable.h"
#include "ast/ast_trail.h"
#include "ast/rewriter/der.h"
#include "sat/smt/sat_th.h"
#include "sat/smt/q_mbi.h"
#include "sat/smt/q_ematch.h"
@ -47,6 +48,7 @@ namespace q {
sat::literal_vector m_universal;
obj_map<sort, expr*> m_unit_table;
expr_ref_vector m_expanded;
der_rewriter m_der;
sat::literal instantiate(quantifier* q, bool negate, std::function<expr* (quantifier*, unsigned)>& mk_var);
sat::literal skolemize(quantifier* q);
@ -54,7 +56,9 @@ namespace q {
void init_units();
expr* get_unit(sort* s);
expr_ref_vector const& expand(quantifier* q);
bool expand(quantifier* q);
bool split(expr* arg, expr_ref& e1, expr_ref& e2);
bool is_literal(expr* arg);
friend class ematch;

6
src/smt/theory_special_relations.cpp
View file

@ -325,14 +325,12 @@ namespace smt {
);
continue;
}
expr_ref f_app(m.mk_app(f, arg1, arg2), m);
expr_ref f_app(m.mk_app(f, arg1, arg2), m);
ensure_enode(f_app);
literal f_lit = ctx.get_literal(f_app);
switch (ctx.get_assignment(f_lit)) {
case l_true:
UNREACHABLE();
// it should already be the case that v1 and reach v2 in the graph.
// whenever f(n1, n2) is asserted.
SASSERT(new_assertion);
break;
case l_false: {
//

7
src/tactic/ufbv/macro_finder_tactic.cpp
View file

@ -17,6 +17,7 @@ Notes:
--*/
#include "tactic/tactical.h"
#include "ast/recfun_decl_plugin.h"
#include "ast/macros/macro_manager.h"
#include "ast/macros/macro_finder.h"
#include "tactic/generic_model_converter.h"
@ -42,6 +43,12 @@ class macro_finder_tactic : public tactic {
tactic_report report("macro-finder", *g);
TRACE("macro-finder", g->display(tout););
recfun::util rec(m());
if (!rec.get_rec_funs().empty()) {
result.push_back(g.get());
return;
}
bool produce_proofs = g->proofs_enabled();
bool unsat_core_enabled = g->unsat_core_enabled();
macro_manager mm(m_manager);

10
src/util/vector.h
View file

@ -721,15 +721,13 @@ public:
ptr_vector(unsigned s, T * elem):vector<T *, false>(s, elem) {}
ptr_vector(unsigned s, T * const * data):vector<T *, false>(s, const_cast<T**>(data)) {}
std::ostream& display(std::ostream& out, char const* delim = " ") const {
bool first = true;
char const* d = "";
for (auto const* u : *this) {
if (!first)
out << delim;
first = false;
if (u)
out << *u;
out << d << *u;
else
out << "<NULL>";
out << d << "<NULL>";
d = delim;
}
return out;
}