mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

misc

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-12-04 16:59:05 -08:00
parent b0fd25f041
commit 4d55f83654
16 changed files with 107 additions and 54 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/arith_decl_plugin.cpp
View file

@ -595,6 +595,7 @@ void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
op_names.push_back(builtin_name("abs", OP_ABS));
if (logic == symbol::null || logic == symbol("ALL")) {
op_names.push_back(builtin_name("^", OP_POWER));
op_names.push_back(builtin_name("^0", OP_POWER0));
op_names.push_back(builtin_name("sin", OP_SIN));
op_names.push_back(builtin_name("cos", OP_COS));
op_names.push_back(builtin_name("tan", OP_TAN));

1
src/ast/arith_decl_plugin.h
View file

@ -294,6 +294,7 @@ public:
bool is_to_int(expr const * n) const { return is_app_of(n, m_afid, OP_TO_INT); }
bool is_is_int(expr const * n) const { return is_app_of(n, m_afid, OP_IS_INT); }
bool is_power(expr const * n) const { return is_app_of(n, m_afid, OP_POWER); }
bool is_power0(expr const * n) const { return is_app_of(n, m_afid, OP_POWER0); }
bool is_int(sort const * s) const { return is_sort_of(s, m_afid, INT_SORT); }
bool is_int(expr const * n) const { return is_int(get_sort(n)); }

8
src/sat/smt/arith_axioms.cpp
View file

@ -49,6 +49,14 @@ namespace arith {
}
}
// t = n^0
void solver::mk_power0_axioms(app* t, app* n) {
expr_ref p0(a.mk_power0(n, t->get_arg(1)), m);
literal eq = eq_internalize(n, a.mk_numeral(rational(0), a.is_int(n)));
add_clause(~eq, eq_internalize(t, p0));
add_clause(eq, eq_internalize(t, a.mk_numeral(rational(1), a.is_int(t))));
}
// is_int(x) <=> to_real(to_int(x)) = x
void solver::mk_is_int_axiom(expr* n) {
expr* x = nullptr;

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

@ -265,7 +265,7 @@ namespace arith {
st.to_ensure_var().push_back(n1);
st.to_ensure_var().push_back(n2);
}
else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n)) {
else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n) && !a.is_power0(n)) {
found_unsupported(n);
}
else {
@ -437,12 +437,18 @@ namespace arith {
return v;
theory_var w = mk_evar(n);
internalize_term(n);
svector<lpvar> vars;
for (unsigned i = 0; i < p; ++i)
vars.push_back(register_theory_var_in_lar_solver(w));
ensure_nla();
m_solver->register_existing_terms();
m_nla->add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr());
if (p == 0) {
mk_power0_axioms(t, n);
}
else {
svector<lpvar> vars;
for (unsigned i = 0; i < p; ++i)
vars.push_back(register_theory_var_in_lar_solver(w));
ensure_nla();
m_solver->register_existing_terms();
m_nla->add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr());
}
return v;
}
@ -566,6 +572,7 @@ namespace arith {
for (expr* arg : *to_app(e))
args.push_back(e_internalize(arg));
n = ctx.mk_enode(e, args.size(), args.c_ptr());
ctx.attach_node(n);
}
return n;
}

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

@ -1127,7 +1127,7 @@ namespace arith {
set_evidence(ev.ci(), m_core, m_eqs);
DEBUG_CODE(
if (is_conflict) {
for (literal c : m_core) VERIFY(s().value(c) == l_false);
for (literal c : m_core) VERIFY(s().value(c) == l_true);
for (auto p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root());
});
for (auto const& eq : m_eqs)

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

@ -267,6 +267,7 @@ namespace arith {
void mk_rem_axiom(expr* dividend, expr* divisor);
void mk_bound_axioms(api_bound& b);
void mk_bound_axiom(api_bound& b1, api_bound& b2);
void mk_power0_axioms(app* t, app* n);
void flush_bound_axioms();
// bounds

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

@ -101,11 +101,8 @@ namespace euf {
void solver::attach_node(euf::enode* n) {
expr* e = n->get_expr();
sat::literal lit;
if (!m.is_bool(e))
drat_log_node(e);
else
lit = attach_lit(literal(si.add_bool_var(e), false), e);
if (m.is_bool(e))
attach_lit(literal(si.add_bool_var(e), false), e);
if (!m.is_bool(e) && m.get_sort(e)->get_family_id() != null_family_id) {
auto* e_ext = expr2solver(e);

33
src/sat/smt/euf_proof.cpp
View file

@ -27,9 +27,7 @@ namespace euf {
m_drat_initialized = true;
}
void solver::drat_log_node(expr* e) {
if (!use_drat())
return;
void solver::drat_log_expr1(expr* e) {
if (is_app(e)) {
app* a = to_app(e);
drat_log_decl(a->get_decl());
@ -43,12 +41,41 @@ namespace euf {
for (expr* arg : *a)
get_drat().def_add_arg(arg->get_id());
get_drat().def_end();
m_drat_asts.insert(e);
push(insert_obj_trail<solver, ast>(m_drat_asts, e));
}
else {
IF_VERBOSE(0, verbose_stream() << "logging binders is TBD\n");
}
}
void solver::drat_log_expr(expr* e) {
if (m_drat_asts.contains(e))
return;
ptr_vector<expr>::scoped_stack _sc(m_drat_todo);
m_drat_todo.push_back(e);
while (!m_drat_todo.empty()) {
e = m_drat_todo.back();
unsigned sz = m_drat_todo.size();
if (is_app(e))
for (expr* arg : *to_app(e))
if (!m_drat_asts.contains(arg))
m_drat_todo.push_back(arg);
if (m_drat_todo.size() != sz)
continue;
drat_log_expr1(e);
m_drat_todo.pop_back();
}
}
void solver::drat_bool_def(sat::bool_var v, expr* e) {
if (!use_drat())
return;
drat_log_expr(e);
get_drat().bool_def(v, e->get_id());
}
void solver::drat_log_decl(func_decl* f) {
if (f->get_family_id() != null_family_id)
return;

5
src/sat/smt/euf_solver.h
View file

@ -157,6 +157,9 @@ namespace euf {
void log_antecedents(std::ostream& out, literal l, literal_vector const& r);
void log_antecedents(literal l, literal_vector const& r);
void drat_log_decl(func_decl* f);
void drat_log_expr(expr* n);
void drat_log_expr1(expr* n);
ptr_vector<expr> m_drat_todo;
obj_hashtable<ast> m_drat_asts;
bool m_drat_initialized{ false };
void init_drat();
@ -289,6 +292,7 @@ namespace euf {
bool use_drat() { return s().get_config().m_drat && (init_drat(), true); }
sat::drat& get_drat() { return s().get_drat(); }
void drat_bool_def(sat::bool_var v, expr* n);
// decompile
bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
@ -310,7 +314,6 @@ namespace euf {
void unhandled_function(func_decl* f);
th_rewriter& get_rewriter() { return m_rewriter; }
bool is_shared(euf::enode* n) const;
void drat_log_node(expr* n);
// relevancy
bool relevancy_enabled() const { return get_config().m_relevancy_lvl > 0; }

7
src/sat/smt/sat_smt.h
View file

@ -28,13 +28,6 @@ namespace sat {
eframe(expr* e) : m_e(e), m_idx(0) {}
};
struct scoped_stack {
svector<eframe>& s;
unsigned sz;
scoped_stack(svector<eframe>& s):s(s), sz(s.size()) {}
~scoped_stack() { s.shrink(sz); }
};
class sat_internalizer {
public:
virtual ~sat_internalizer() {}

2
src/sat/smt/sat_th.cpp
View file

@ -24,7 +24,7 @@ namespace euf {
bool th_internalizer::visit_rec(ast_manager& m, expr* a, bool sign, bool root, bool redundant) {
IF_VERBOSE(110, verbose_stream() << "internalize: " << mk_pp(a, m) << "\n");
flet<bool> _is_learned(m_is_redundant, redundant);
sat::scoped_stack _sc(m_stack);
svector<sat::eframe>::scoped_stack _sc(m_stack);
unsigned sz = m_stack.size();
visit(a);
while (m_stack.size() > sz) {

40
src/sat/tactic/goal2sat.cpp
View file

@ -58,7 +58,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
};
ast_manager & m;
pb_util pb;
sat::cut_simplifier* m_aig;
svector<frame> m_frame_stack;
svector<sat::literal> m_result_stack;
obj_map<app, sat::literal> m_cache;
@ -83,7 +82,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
imp(ast_manager & _m, params_ref const & p, sat::solver_core & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
m(_m),
pb(m),
m_aig(nullptr),
m_solver(s),
m_map(map),
m_dep2asm(dep2asm),
@ -92,11 +90,15 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_default_external(default_external) {
updt_params(p);
m_true = sat::null_literal;
m_aig = s.get_cut_simplifier();
}
~imp() override {}
sat::cut_simplifier* aig() {
return m_solver.get_cut_simplifier();
}
void updt_params(params_ref const & p) {
sat_params sp(p);
m_ite_extra = p.get_bool("ite_extra", true);
@ -178,7 +180,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
if (m_expr2var_replay && m_expr2var_replay->find(n, v))
return v;
v = m_solver.add_var(is_ext);
log_node(n);
log_def(v, n);
if (top_level_relevant() && !is_bool_op(n))
ensure_euf()->track_relevancy(v);
@ -186,19 +187,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
void log_def(sat::bool_var v, expr* n) {
if (m_drat && m_solver.get_drat_ptr())
m_solver.get_drat_ptr()->bool_def(v, n->get_id());
}
void log_node(expr* n) {
if (m_drat && m_solver.get_drat_ptr()) {
if (is_app(n)) {
for (expr* arg : *to_app(n))
if (m.is_not(arg))
log_node(arg);
}
ensure_euf()->drat_log_node(n);
}
if (m_drat && m_euf)
ensure_euf()->drat_bool_def(v, n);
}
sat::literal mk_true() {
@ -413,15 +403,15 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_result_stack.push_back(~l);
lits = m_result_stack.end() - num - 1;
if (m_aig) {
if (aig()) {
aig_lits.reset();
aig_lits.append(num, lits);
}
// remark: mk_clause may perform destructive updated to lits.
// I have to execute it after the binary mk_clause above.
mk_clause(num+1, lits);
if (m_aig)
m_aig->add_or(l, num, aig_lits.c_ptr());
if (aig())
aig()->add_or(l, num, aig_lits.c_ptr());
m_solver.set_phase(~l);
m_result_stack.shrink(old_sz);
@ -468,13 +458,13 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
m_result_stack.push_back(l);
lits = m_result_stack.end() - num - 1;
if (m_aig) {
if (aig()) {
aig_lits.reset();
aig_lits.append(num, lits);
}
mk_clause(num+1, lits);
if (m_aig) {
m_aig->add_and(l, num, aig_lits.c_ptr());
if (aig()) {
aig()->add_and(l, num, aig_lits.c_ptr());
}
m_solver.set_phase(l);
if (sign)
@ -516,7 +506,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
mk_clause(~t, ~e, l);
mk_clause(t, e, ~l);
}
if (m_aig) m_aig->add_ite(l, c, t, e);
if (aig()) aig()->add_ite(l, c, t, e);
if (sign)
l.neg();
@ -581,7 +571,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
mk_clause(~l, ~l1, l2);
mk_clause(l, l1, l2);
mk_clause(l, ~l1, ~l2);
if (m_aig) m_aig->add_iff(l, l1, l2);
if (aig()) aig()->add_iff(l, l1, l2);
if (sign)
l.neg();
m_result_stack.push_back(l);

15
src/shell/drat_frontend.cpp
View file

@ -150,7 +150,7 @@ public:
check_assertion_redundant(lits);
else if (!st.is_sat() && !st.is_deleted())
check_clause(lits);
m_drat.add(lits, st);
// m_drat.add(lits, st);
}
/**
@ -201,6 +201,19 @@ public:
result = dtu.mk_is(f, args[0]);
return;
}
if (name == "Real" && sz == 4) {
arith_util au(m);
rational num = sexpr->get_child(2)->get_numeral();
rational den = sexpr->get_child(3)->get_numeral();
result = au.mk_numeral(num/den, false);
return;
}
if (name == "Int" && sz == 3) {
arith_util au(m);
rational num = sexpr->get_child(2)->get_numeral();
result = au.mk_numeral(num, true);
return;
}
for (unsigned i = 2; i < sz; ++i) {
auto* child = sexpr->get_child(i);
if (child->is_numeral() && child->get_numeral().is_unsigned())

2
src/smt/theory_lra.cpp
View file

@ -384,7 +384,7 @@ class theory_lra::imp {
vars.push_back(v);
++index;
}
else if (a.is_power(n, n1, n2) && is_app(n1) && a.is_extended_numeral(n2, r) && r.is_unsigned() && r <= 10) {
else if (a.is_power(n, n1, n2) && is_app(n1) && a.is_extended_numeral(n2, r) && r.is_unsigned() && r.is_pos() && r <= 10) {
theory_var v = internalize_power(to_app(n), to_app(n1), r.get_unsigned());
coeffs[vars.size()] = coeffs[index];
vars.push_back(v);

8
src/smt/user_propagator.cpp
View file

@ -121,8 +121,12 @@ void user_propagator::propagate() {
m_lits.append(m_id2justification[id]);
for (auto const& p : prop.m_eqs)
m_eqs.push_back(enode_pair(get_enode(p.first), get_enode(p.second)));
DEBUG_CODE(for (auto const& p : m_eqs) SASSERT(p.first->get_root() == p.second->get_root()););
DEBUG_CODE(for (auto const& p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root()););
IF_VERBOSE(5,
for (auto lit : m_lits)
verbose_stream() << lit << ":" << ctx.get_assignment(lit) << " ";
verbose_stream() << "\n";);
if (m.is_false(prop.m_conseq)) {
js = ctx.mk_justification(
ext_theory_conflict_justification(

8
src/util/vector.h
View file

@ -596,6 +596,14 @@ public:
if (s > size())
resize(s);
}
struct scoped_stack {
vector& s;
unsigned sz;
scoped_stack(vector& s):s(s), sz(s.size()) {}
~scoped_stack() { s.shrink(sz); }
};
};
template<typename T>