mirror of
https://github.com/Z3Prover/z3
synced 2025-08-14 06:45:25 +00:00
Merge branch 'master' into polysat
This commit is contained in:
Jakob Rath
commit
59c3234fb8
196 changed files with 4705 additions and 4168 deletions
|
|
@ -94,7 +94,7 @@ namespace sat {
|
|||
// from clause x, y, z
|
||||
// then ~x, ~y -> z
|
||||
// look for ~y, z -> ~x - contains ternary(y, ~z, ~x)
|
||||
// look for ~x, y -> u - u is used in a ternary claues (~y, x)
|
||||
// look for ~x, y -> u - u is used in a ternary clause (~y, x)
|
||||
// look for y, u -> ~x - contains ternary(~u, ~x, ~y)
|
||||
// then ~x = if ~y then z else u
|
||||
|
||||
|
|
|
|||
|
|
@ -47,7 +47,7 @@ Marijn's version:
|
|||
if inconsistent():
|
||||
learn C (subsumes C or p)
|
||||
else:
|
||||
candidates' := C union ~(consequencs of propagate(~C))
|
||||
candidates' := C union ~(consequences of propagate(~C))
|
||||
candidates := candidates' intersect candidates
|
||||
pop(1)
|
||||
for q in candidates:
|
||||
|
|
@ -77,7 +77,7 @@ Marijn's version:
|
|||
if inconsistent():
|
||||
learn C (subsumes C or p)
|
||||
else:
|
||||
candidates := candicates union C union ~(consequencs of propagate(~C))
|
||||
candidates := candidates union C union ~(consequences of propagate(~C))
|
||||
pop(1)
|
||||
for q in candidates:
|
||||
push(1)
|
||||
|
|
|
|||
|
|
@ -28,7 +28,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
// for nary clauses
|
||||
static bool contains_watched(watch_list const & wlist, clause const & c, clause_offset cls_off) {
|
||||
bool integrity_checker::contains_watched(watch_list const & wlist, clause const & c, clause_offset cls_off) const {
|
||||
for (watched const& w : wlist) {
|
||||
if (w.is_clause()) {
|
||||
if (w.get_clause_offset() == cls_off) {
|
||||
|
|
@ -38,6 +38,8 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
}
|
||||
TRACE("sat", tout << "clause " << c << " not found in watch-list\n");
|
||||
TRACE("sat", s.display_watches(tout));
|
||||
UNREACHABLE();
|
||||
return false;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -25,6 +25,7 @@ Revision History:
|
|||
namespace sat {
|
||||
class integrity_checker {
|
||||
solver const & s;
|
||||
bool contains_watched(watch_list const & wlist, clause const & c, clause_offset cls_off) const;
|
||||
public:
|
||||
integrity_checker(solver const & s);
|
||||
|
||||
|
|
|
|||
|
|
@ -7,15 +7,13 @@
|
|||
|
||||
Abstract:
|
||||
|
||||
proof replay and trim
|
||||
The proof is trimmed by re-running the proof steps and collecting justified literals
|
||||
at level 0. The proof is obtained by back-tracing the justificiations attached to literals.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner 2023-10-04
|
||||
|
||||
Notes:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#include "sat/sat_proof_trim.h"
|
||||
|
|
@ -29,53 +27,50 @@ namespace sat {
|
|||
Output: reduced trail - result
|
||||
*/
|
||||
|
||||
unsigned_vector proof_trim::trim() {
|
||||
unsigned_vector result;
|
||||
m_core_literals.reset();
|
||||
m_core_literals.insert(literal_vector());
|
||||
vector<std::pair<unsigned, unsigned_vector>> proof_trim::trim() {
|
||||
m_result.reset();
|
||||
m_propagated.resize(num_vars(), false);
|
||||
for (unsigned i = m_trail.size(); i-- > 0; ) {
|
||||
|
||||
|
||||
IF_VERBOSE(10, s.display(verbose_stream() << "trim\n"));
|
||||
|
||||
auto const& [id, cl, clp, is_add, is_initial] = m_trail.back();
|
||||
SASSERT(cl.empty());
|
||||
m_result.push_back({id, unsigned_vector()});
|
||||
conflict_analysis_core(m_conflict, m_conflict_clause);
|
||||
m_trail.pop_back();
|
||||
|
||||
|
||||
for (unsigned i = m_trail.size(); i-- > 0; ) {
|
||||
auto const& [id, cl, clp, is_add, is_initial] = m_trail[i];
|
||||
if (!is_add) {
|
||||
revive(cl, clp);
|
||||
continue;
|
||||
}
|
||||
}
|
||||
IF_VERBOSE(10, s.display(verbose_stream()));
|
||||
prune_trail(cl, clp);
|
||||
IF_VERBOSE(10, verbose_stream() << cl << " " << in_core(cl, clp) << ": "; for (auto const& c : m_core_literals) verbose_stream() << "{" << c << "} ");
|
||||
IF_VERBOSE(10, s.display(verbose_stream() << "\n"));
|
||||
del(cl, clp);
|
||||
if (!in_core(cl, clp))
|
||||
if (!in_core(cl))
|
||||
continue;
|
||||
result.push_back(id);
|
||||
IF_VERBOSE(4, verbose_stream() << cl << " in-core " << in_core(cl) << ": "; for (auto const& [k,v] : m_clauses) verbose_stream() << "{" << v.m_clauses << "} "; verbose_stream() << "\n");
|
||||
|
||||
m_result.push_back({id, unsigned_vector()});
|
||||
if (is_initial)
|
||||
continue;
|
||||
conflict_analysis_core(cl, clp);
|
||||
}
|
||||
result.reverse();
|
||||
return result;
|
||||
m_result.reverse();
|
||||
return m_result;
|
||||
}
|
||||
|
||||
void proof_trim::del(literal_vector const& cl, clause* cp) {
|
||||
CTRACE("sat", cp, tout << "del " << *cp << "\n");
|
||||
if (cp)
|
||||
s.detach_clause(*cp);
|
||||
else
|
||||
del(cl);
|
||||
}
|
||||
|
||||
bool proof_trim::match_clause(literal_vector const& cl, literal l1, literal l2) const {
|
||||
return cl.size() == 2 && ((l1 == cl[0] && l2 == cl[1]) || (l1 == cl[1] && l2 == cl[0]));
|
||||
}
|
||||
|
||||
bool proof_trim::match_clause(literal_vector const& cl, literal l1, literal l2, literal l3) const {
|
||||
return cl.size() == 3 &&
|
||||
((l1 == cl[0] && l2 == cl[1] && l3 == cl[2]) ||
|
||||
(l1 == cl[0] && l2 == cl[2] && l3 == cl[1]) ||
|
||||
(l1 == cl[1] && l2 == cl[0] && l3 == cl[2]) ||
|
||||
(l1 == cl[1] && l2 == cl[2] && l3 == cl[0]) ||
|
||||
(l1 == cl[2] && l2 == cl[1] && l3 == cl[0]) ||
|
||||
(l1 == cl[2] && l2 == cl[0] && l3 == cl[1]));
|
||||
}
|
||||
|
||||
/**
|
||||
* cl is on the trail if there is some literal l that is implied by cl
|
||||
|
|
@ -90,6 +85,8 @@ namespace sat {
|
|||
void proof_trim::prune_trail(literal_vector const& cl, clause* cp) {
|
||||
m_in_clause.reset();
|
||||
m_in_coi.reset();
|
||||
|
||||
// verbose_stream() << "prune trail " << cl << "\n";
|
||||
|
||||
if (cl.empty())
|
||||
return;
|
||||
|
|
@ -121,12 +118,21 @@ namespace sat {
|
|||
auto js = s.get_justification(l);
|
||||
bool in_coi = false;
|
||||
if (js.is_clause())
|
||||
for (literal lit : s.get_clause(j))
|
||||
for (literal lit : s.get_clause(js))
|
||||
in_coi |= m_in_coi.contains(lit.index());
|
||||
else if (js.is_binary_clause())
|
||||
in_coi = m_in_coi.contains(js.get_literal().index());
|
||||
else
|
||||
else if (js.is_none()) {
|
||||
verbose_stream() << "none " << js << "\n";
|
||||
}
|
||||
else if (js.is_ext_justification()) {
|
||||
verbose_stream() << js << "\n";
|
||||
UNREACHABLE(); // approach does not work for external justifications
|
||||
}
|
||||
else {
|
||||
verbose_stream() << js << "\n";
|
||||
UNREACHABLE(); // approach does not work for external justifications
|
||||
}
|
||||
|
||||
if (in_coi)
|
||||
unassign_literal(l);
|
||||
|
|
@ -134,6 +140,7 @@ namespace sat {
|
|||
s.m_trail[j++] = s.m_trail[i];
|
||||
}
|
||||
s.m_trail.shrink(j);
|
||||
// verbose_stream() << "trail after " << s.m_trail << "\n";
|
||||
s.m_inconsistent = false;
|
||||
s.m_qhead = s.m_trail.size();
|
||||
s.propagate(false);
|
||||
|
|
@ -188,11 +195,14 @@ namespace sat {
|
|||
m_propagated[s.m_trail[i].var()] = true;
|
||||
}
|
||||
SASSERT(s.inconsistent());
|
||||
IF_VERBOSE(3, verbose_stream() << s.m_not_l << " " << s.m_conflict << "\n");
|
||||
IF_VERBOSE(3, s.display_justification(verbose_stream() << "conflict " << s.m_not_l << " ", s.m_conflict) << "\n");
|
||||
IF_VERBOSE(3, s.display(verbose_stream()));
|
||||
sat::literal l = sat::null_literal;
|
||||
if (s.m_not_l != null_literal) {
|
||||
add_core(~s.m_not_l, s.m_conflict);
|
||||
add_dependency(s.m_not_l);
|
||||
l = ~s.m_not_l;
|
||||
}
|
||||
add_core(l, s.m_conflict);
|
||||
add_dependency(s.m_conflict);
|
||||
|
||||
for (unsigned i = s.m_trail.size(); i-- > trail_size0; ) {
|
||||
|
|
@ -201,7 +211,7 @@ namespace sat {
|
|||
if (!s.is_marked(v))
|
||||
continue;
|
||||
add_core(v);
|
||||
s.reset_mark(v);
|
||||
s.reset_mark(v);
|
||||
add_dependency(s.get_justification(v));
|
||||
}
|
||||
if (!cl.empty())
|
||||
|
|
@ -210,8 +220,10 @@ namespace sat {
|
|||
|
||||
void proof_trim::add_dependency(literal lit) {
|
||||
bool_var v = lit.var();
|
||||
if (m_propagated[v]) // literal was propagated after assuming ~C
|
||||
s.mark(v);
|
||||
if (m_propagated[v]) { // literal was propagated after assuming ~C
|
||||
if (!s.is_marked(v))
|
||||
s.mark(v);
|
||||
}
|
||||
else if (s.lvl(v) == 0) // literal depends on level 0, it is not assumed by ~C
|
||||
// inefficient for repeated insertions ?
|
||||
add_core(v);
|
||||
|
|
@ -253,28 +265,28 @@ namespace sat {
|
|||
m_clause.push_back(j.get_literal());
|
||||
break;
|
||||
case justification::CLAUSE:
|
||||
s.get_clause(j).mark_used();
|
||||
IF_VERBOSE(3, verbose_stream() << "add core " << s.get_clause(j) << "\n");
|
||||
return;
|
||||
for (auto lit : s.get_clause(j))
|
||||
m_clause.push_back(lit);
|
||||
break;
|
||||
default:
|
||||
verbose_stream() << j << "\n";
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
std::sort(m_clause.begin(), m_clause.end());
|
||||
IF_VERBOSE(3, verbose_stream() << "add core " << m_clause << "\n");
|
||||
m_core_literals.insert(m_clause);
|
||||
if (s.lvl(l) == 0) {
|
||||
auto& [clauses, id, in_core] = m_clauses.find(m_clause);
|
||||
in_core = true;
|
||||
m_result.back().second.push_back(id);
|
||||
if (l != null_literal && s.lvl(l) == 0) {
|
||||
m_clause.reset();
|
||||
m_clause.push_back(l);
|
||||
m_core_literals.insert(m_clause);
|
||||
m_clauses.insert_if_not_there(m_clause, {{}, 0, true }).m_in_core = true;
|
||||
}
|
||||
}
|
||||
|
||||
bool proof_trim::in_core(literal_vector const& cl, clause* cp) const {
|
||||
if (cp)
|
||||
return cp->was_used();
|
||||
else
|
||||
return m_core_literals.contains(cl);
|
||||
bool proof_trim::in_core(literal_vector const& cl) const {
|
||||
return m_clauses.find(cl).m_in_core;
|
||||
}
|
||||
|
||||
void proof_trim::revive(literal_vector const& cl, clause* cp) {
|
||||
|
|
@ -286,7 +298,7 @@ namespace sat {
|
|||
|
||||
clause* proof_trim::del(literal_vector const& cl) {
|
||||
clause* cp = nullptr;
|
||||
IF_VERBOSE(3, verbose_stream() << "del: " << cl << "\n");
|
||||
TRACE("sat", tout << "del: " << cl << "\n");
|
||||
if (cl.size() == 2) {
|
||||
s.detach_bin_clause(cl[0], cl[1], true);
|
||||
return cp;
|
||||
|
|
@ -294,23 +306,15 @@ namespace sat {
|
|||
auto* e = m_clauses.find_core(cl);
|
||||
if (!e)
|
||||
return cp;
|
||||
auto& v = e->get_data().m_value;
|
||||
if (!v.empty()) {
|
||||
cp = v.back();
|
||||
IF_VERBOSE(3, verbose_stream() << "del: " << *cp << "\n");
|
||||
auto& [clauses, id, in_core] = e->get_data().m_value;
|
||||
if (!clauses.empty()) {
|
||||
cp = clauses.back();
|
||||
TRACE("sat", tout << "del: " << *cp << "\n");
|
||||
s.detach_clause(*cp);
|
||||
v.pop_back();
|
||||
clauses.pop_back();
|
||||
}
|
||||
return cp;
|
||||
}
|
||||
|
||||
void proof_trim::save(literal_vector const& lits, clause* cl) {
|
||||
if (!cl)
|
||||
return;
|
||||
IF_VERBOSE(3, verbose_stream() << "add: " << *cl << "\n");
|
||||
auto& v = m_clauses.insert_if_not_there(lits, clause_vector());
|
||||
v.push_back(cl);
|
||||
}
|
||||
}
|
||||
|
||||
proof_trim::proof_trim(params_ref const& p, reslimit& lim):
|
||||
s(p, lim) {
|
||||
|
|
@ -318,14 +322,53 @@ namespace sat {
|
|||
}
|
||||
|
||||
void proof_trim::assume(unsigned id, bool is_initial) {
|
||||
std::sort(m_clause.begin(), m_clause.end());
|
||||
std::sort(m_clause.begin(), m_clause.end());
|
||||
if (unit_or_binary_occurs())
|
||||
return;
|
||||
return;
|
||||
if (!m_conflict.empty() && m_clause.empty()) {
|
||||
m_clauses.insert(m_clause, { {}, id, m_clause.empty() });
|
||||
m_trail.push_back({ id , m_clause, nullptr, true, is_initial });
|
||||
}
|
||||
if (!m_conflict.empty())
|
||||
return;
|
||||
|
||||
IF_VERBOSE(3, verbose_stream() << (is_initial?"assume ":"rup ") << m_clause << "\n");
|
||||
auto* cl = s.mk_clause(m_clause, status::redundant());
|
||||
auto& [clauses, id2, in_core] = m_clauses.insert_if_not_there(m_clause, { {}, id, m_clause.empty() });
|
||||
if (cl)
|
||||
clauses.push_back(cl);
|
||||
m_trail.push_back({ id, m_clause, cl, true, is_initial });
|
||||
|
||||
auto is_unit2 = [&]() {
|
||||
if (s.value(m_clause[0]) == l_false)
|
||||
std::swap(m_clause[0], m_clause[1]);
|
||||
return s.value(m_clause[1]) == l_false;
|
||||
};
|
||||
|
||||
auto is_unit = [&]() {
|
||||
unsigned undef_idx = m_clause.size();
|
||||
for (unsigned i = 0; i < m_clause.size(); ++i) {
|
||||
sat::literal lit = (*cl)[i];
|
||||
if (s.value(lit) != l_undef)
|
||||
continue;
|
||||
if (undef_idx < m_clause.size())
|
||||
return false;
|
||||
undef_idx = i;
|
||||
}
|
||||
if (undef_idx < m_clause.size()) {
|
||||
std::swap((*cl)[undef_idx], (*cl)[0]);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
};
|
||||
|
||||
if (m_clause.size() == 2 && is_unit2())
|
||||
s.propagate_bin_clause(m_clause[0], m_clause[1]);
|
||||
else if (m_clause.size() > 2 && is_unit())
|
||||
s.propagate_clause(*cl, true, 0, s.cls_allocator().get_offset(cl));
|
||||
s.propagate(false);
|
||||
save(m_clause, cl);
|
||||
if (s.inconsistent() || all_of(m_clause, [&](sat::literal lit) { return s.value(lit) == l_false; }))
|
||||
set_conflict(m_clause, cl);
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -352,6 +395,4 @@ namespace sat {
|
|||
void proof_trim::infer(unsigned id) {
|
||||
assume(id, false);
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -30,11 +30,12 @@ namespace sat {
|
|||
|
||||
class proof_trim {
|
||||
solver s;
|
||||
literal_vector m_clause;
|
||||
literal_vector m_clause, m_conflict;
|
||||
uint_set m_in_clause;
|
||||
uint_set m_in_coi;
|
||||
clause* m_conflict_clause = nullptr;
|
||||
vector<std::tuple<unsigned, literal_vector, clause*, bool, bool>> m_trail;
|
||||
|
||||
vector<std::pair<unsigned, unsigned_vector>> m_result;
|
||||
|
||||
struct hash {
|
||||
unsigned operator()(literal_vector const& v) const {
|
||||
|
|
@ -46,16 +47,20 @@ namespace sat {
|
|||
return a == b;
|
||||
}
|
||||
};
|
||||
map<literal_vector, clause_vector, hash, eq> m_clauses;
|
||||
|
||||
hashtable<literal_vector, hash, eq> m_core_literals;
|
||||
|
||||
struct clause_info {
|
||||
clause_vector m_clauses;
|
||||
unsigned m_id = 0;
|
||||
bool m_in_core = false;
|
||||
};
|
||||
|
||||
|
||||
map<literal_vector, clause_info, hash, eq> m_clauses;
|
||||
bool_vector m_propagated;
|
||||
|
||||
void del(literal_vector const& cl, clause* cp);
|
||||
|
||||
bool match_clause(literal_vector const& cl, literal l1, literal l2) const;
|
||||
bool match_clause(literal_vector const& cl, literal l1, literal l2, literal l3) const;
|
||||
|
||||
void prune_trail(literal_vector const& cl, clause* cp);
|
||||
void conflict_analysis_core(literal_vector const& cl, clause* cp);
|
||||
|
||||
|
|
@ -63,13 +68,13 @@ namespace sat {
|
|||
void add_dependency(justification j);
|
||||
void add_core(bool_var v);
|
||||
void add_core(literal l, justification j);
|
||||
bool in_core(literal_vector const& cl, clause* cp) const;
|
||||
bool in_core(literal_vector const& cl) const;
|
||||
void revive(literal_vector const& cl, clause* cp);
|
||||
clause* del(literal_vector const& cl);
|
||||
void save(literal_vector const& lits, clause* cl);
|
||||
|
||||
uint_set m_units;
|
||||
bool unit_or_binary_occurs();
|
||||
void set_conflict(literal_vector const& c, clause* cp) { m_conflict.reset(); m_conflict.append(c); m_conflict_clause = cp;}
|
||||
|
||||
public:
|
||||
|
||||
|
|
@ -85,7 +90,7 @@ namespace sat {
|
|||
void infer(unsigned id);
|
||||
void updt_params(params_ref const& p) { s.updt_params(p); }
|
||||
|
||||
unsigned_vector trim();
|
||||
vector<std::pair<unsigned, unsigned_vector>> trim();
|
||||
|
||||
};
|
||||
}
|
||||
|
|
|
|||
|
|
@ -90,7 +90,7 @@ namespace sat {
|
|||
|
||||
solver::~solver() {
|
||||
m_ext = nullptr;
|
||||
SASSERT(m_config.m_num_threads > 1 || check_invariant());
|
||||
SASSERT(m_config.m_num_threads > 1 || m_trim || check_invariant());
|
||||
CTRACE("sat", !m_clauses.empty(), tout << "Delete clauses\n";);
|
||||
del_clauses(m_clauses);
|
||||
CTRACE("sat", !m_learned.empty(), tout << "Delete learned\n";);
|
||||
|
|
@ -879,6 +879,7 @@ namespace sat {
|
|||
m_conflict = c;
|
||||
m_not_l = not_l;
|
||||
TRACE("sat", display(display_justification(tout << "conflict " << not_l << " ", c) << "\n"));
|
||||
TRACE("sat", display_watches(tout));
|
||||
}
|
||||
|
||||
void solver::assign_core(literal l, justification j) {
|
||||
|
|
@ -3462,7 +3463,7 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
// can't eliminat FUIP
|
||||
// can't eliminate FUIP
|
||||
SASSERT(is_marked_lit(m_lemma[0]));
|
||||
|
||||
unsigned j = 0;
|
||||
|
|
|
|||
|
|
@ -47,7 +47,7 @@ class sat_smt_solver : public solver {
|
|||
ast_manager& m;
|
||||
trail_stack& m_trail;
|
||||
expr_ref_vector m_refs;
|
||||
obj_map<expr, expr*> m_dep2orig; // map original dependency to uninterpeted literal
|
||||
obj_map<expr, expr*> m_dep2orig; // map original dependency to uninterpreted literal
|
||||
|
||||
u_map<expr*> m_lit2dep; // map from literal assumption to original expression
|
||||
obj_map<expr, sat::literal> m_dep2lit; // map uninterpreted literal to sat literal
|
||||
|
|
|
|||
|
|
@ -136,9 +136,22 @@ namespace arith {
|
|||
arith_proof_hint const* solver::explain_conflict(sat::literal_vector const& core, euf::enode_pair_vector const& eqs) {
|
||||
arith_proof_hint* hint = nullptr;
|
||||
if (ctx.use_drat()) {
|
||||
m_coeffs.reset();
|
||||
for (auto const& e : m_explanation) {
|
||||
if (inequality_source == m_constraint_sources[e.ci()])
|
||||
m_coeffs.push_back(e.coeff());
|
||||
}
|
||||
|
||||
m_arith_hint.set_type(ctx, hint_type::farkas_h);
|
||||
for (auto lit : core)
|
||||
m_arith_hint.add_lit(rational::one(), lit);
|
||||
if (m_coeffs.size() == core.size()) {
|
||||
unsigned i = 0;
|
||||
for (auto lit : core)
|
||||
m_arith_hint.add_lit(m_coeffs[i], lit), ++i;
|
||||
}
|
||||
else {
|
||||
for (auto lit : core)
|
||||
m_arith_hint.add_lit(rational::one(), lit);
|
||||
}
|
||||
for (auto const& [a,b] : eqs)
|
||||
m_arith_hint.add_eq(a, b);
|
||||
hint = m_arith_hint.mk(ctx);
|
||||
|
|
|
|||
|
|
@ -160,7 +160,6 @@ namespace arith {
|
|||
expr_ref_vector& terms = st.terms();
|
||||
svector<theory_var>& vars = st.vars();
|
||||
vector<rational>& coeffs = st.coeffs();
|
||||
rational& offset = st.offset();
|
||||
rational r;
|
||||
expr* n1, * n2;
|
||||
unsigned index = 0;
|
||||
|
|
@ -204,7 +203,9 @@ namespace arith {
|
|||
++index;
|
||||
}
|
||||
else if (a.is_numeral(n, r)) {
|
||||
offset += coeffs[index] * r;
|
||||
theory_var v = internalize_numeral(to_app(n), r);
|
||||
coeffs[vars.size()] = coeffs[index];
|
||||
vars.push_back(v);
|
||||
++index;
|
||||
}
|
||||
else if (a.is_uminus(n, n1)) {
|
||||
|
|
@ -457,6 +458,19 @@ namespace arith {
|
|||
return v;
|
||||
}
|
||||
|
||||
theory_var solver::internalize_numeral(app* n, rational const& val) {
|
||||
theory_var v = mk_evar(n);
|
||||
lpvar vi = get_lpvar(v);
|
||||
if (vi == UINT_MAX) {
|
||||
vi = lp().add_var(v, a.is_int(n));
|
||||
add_def_constraint_and_equality(vi, lp::GE, val);
|
||||
add_def_constraint_and_equality(vi, lp::LE, val);
|
||||
register_fixed_var(v, val);
|
||||
}
|
||||
return v;
|
||||
}
|
||||
|
||||
|
||||
theory_var solver::internalize_mul(app* t) {
|
||||
SASSERT(a.is_mul(t));
|
||||
internalize_args(t, true);
|
||||
|
|
@ -484,57 +498,32 @@ namespace arith {
|
|||
theory_var v = mk_evar(term);
|
||||
TRACE("arith", tout << mk_bounded_pp(term, m) << " v" << v << "\n";);
|
||||
|
||||
if (is_unit_var(st) && v == st.vars()[0]) {
|
||||
if (is_unit_var(st) && v == st.vars()[0])
|
||||
return st.vars()[0];
|
||||
}
|
||||
else if (is_one(st) && a.is_numeral(term)) {
|
||||
return lp().local_to_external(get_one(a.is_int(term)));
|
||||
}
|
||||
else if (is_zero(st) && a.is_numeral(term)) {
|
||||
return lp().local_to_external(get_zero(a.is_int(term)));
|
||||
}
|
||||
else {
|
||||
init_left_side(st);
|
||||
lpvar vi = get_lpvar(v);
|
||||
if (vi == UINT_MAX) {
|
||||
if (m_left_side.empty()) {
|
||||
vi = lp().add_var(v, a.is_int(term));
|
||||
add_def_constraint_and_equality(vi, lp::GE, st.offset());
|
||||
add_def_constraint_and_equality(vi, lp::LE, st.offset());
|
||||
register_fixed_var(v, st.offset());
|
||||
return v;
|
||||
}
|
||||
if (!st.offset().is_zero()) {
|
||||
m_left_side.push_back(std::make_pair(st.offset(), get_one(a.is_int(term))));
|
||||
}
|
||||
if (m_left_side.empty()) {
|
||||
vi = lp().add_var(v, a.is_int(term));
|
||||
add_def_constraint_and_equality(vi, lp::GE, rational(0));
|
||||
add_def_constraint_and_equality(vi, lp::LE, rational(0));
|
||||
}
|
||||
else {
|
||||
vi = lp().add_term(m_left_side, v);
|
||||
SASSERT(lp::tv::is_term(vi));
|
||||
TRACE("arith_verbose",
|
||||
tout << "v" << v << " := " << mk_pp(term, m)
|
||||
<< " slack: " << vi << " scopes: " << m_scopes.size() << "\n";
|
||||
lp().print_term(lp().get_term(lp::tv::raw(vi)), tout) << "\n";);
|
||||
}
|
||||
|
||||
init_left_side(st);
|
||||
lpvar vi = get_lpvar(v);
|
||||
|
||||
if (vi == UINT_MAX) {
|
||||
if (m_left_side.empty()) {
|
||||
vi = lp().add_var(v, a.is_int(term));
|
||||
add_def_constraint_and_equality(vi, lp::GE, rational(0));
|
||||
add_def_constraint_and_equality(vi, lp::LE, rational(0));
|
||||
}
|
||||
else {
|
||||
vi = lp().add_term(m_left_side, v);
|
||||
SASSERT(lp::tv::is_term(vi));
|
||||
TRACE("arith_verbose",
|
||||
tout << "v" << v << " := " << mk_pp(term, m)
|
||||
<< " slack: " << vi << " scopes: " << m_scopes.size() << "\n";
|
||||
lp().print_term(lp().get_term(lp::tv::raw(vi)), tout) << "\n";);
|
||||
}
|
||||
return v;
|
||||
}
|
||||
return v;
|
||||
}
|
||||
|
||||
bool solver::is_unit_var(scoped_internalize_state& st) {
|
||||
return st.offset().is_zero() && st.vars().size() == 1 && st.coeffs()[0].is_one();
|
||||
}
|
||||
|
||||
bool solver::is_one(scoped_internalize_state& st) {
|
||||
return st.offset().is_one() && st.vars().empty();
|
||||
}
|
||||
|
||||
bool solver::is_zero(scoped_internalize_state& st) {
|
||||
return st.offset().is_zero() && st.vars().empty();
|
||||
return st.vars().size() == 1 && st.coeffs()[0].is_one();
|
||||
}
|
||||
|
||||
void solver::init_left_side(scoped_internalize_state& st) {
|
||||
|
|
|
|||
|
|
@ -145,13 +145,11 @@ namespace arith {
|
|||
expr_ref_vector m_terms;
|
||||
vector<rational> m_coeffs;
|
||||
svector<theory_var> m_vars;
|
||||
rational m_offset;
|
||||
ptr_vector<expr> m_to_ensure_enode, m_to_ensure_var;
|
||||
internalize_state(ast_manager& m) : m_terms(m) {}
|
||||
void reset() {
|
||||
m_terms.reset();
|
||||
m_coeffs.reset();
|
||||
m_offset.reset();
|
||||
m_vars.reset();
|
||||
m_to_ensure_enode.reset();
|
||||
m_to_ensure_var.reset();
|
||||
|
|
@ -178,7 +176,6 @@ namespace arith {
|
|||
expr_ref_vector& terms() { return m_st.m_terms; }
|
||||
vector<rational>& coeffs() { return m_st.m_coeffs; }
|
||||
svector<theory_var>& vars() { return m_st.m_vars; }
|
||||
rational& offset() { return m_st.m_offset; }
|
||||
ptr_vector<expr>& to_ensure_enode() { return m_st.m_to_ensure_enode; }
|
||||
ptr_vector<expr>& to_ensure_var() { return m_st.m_to_ensure_var; }
|
||||
void push(expr* e, rational c) { m_st.m_terms.push_back(e); m_st.m_coeffs.push_back(c); }
|
||||
|
|
@ -254,6 +251,7 @@ namespace arith {
|
|||
lp::explanation m_explanation;
|
||||
vector<nla::lemma> m_nla_lemma_vector;
|
||||
literal_vector m_core, m_core2;
|
||||
vector<rational> m_coeffs;
|
||||
svector<enode_pair> m_eqs;
|
||||
vector<parameter> m_params;
|
||||
nla::lemma m_lemma;
|
||||
|
|
@ -290,6 +288,7 @@ namespace arith {
|
|||
void ensure_arg_vars(app* t);
|
||||
theory_var internalize_power(app* t, app* n, unsigned p);
|
||||
theory_var internalize_mul(app* t);
|
||||
theory_var internalize_numeral(app* t, rational const& v);
|
||||
theory_var internalize_def(expr* term);
|
||||
theory_var internalize_def(expr* term, scoped_internalize_state& st);
|
||||
theory_var internalize_linearized_def(expr* term, scoped_internalize_state& st);
|
||||
|
|
|
|||
|
|
@ -43,15 +43,19 @@ namespace user_solver {
|
|||
m_prop.push_back(prop_info(explain, v, r));
|
||||
}
|
||||
|
||||
void solver::propagate_cb(
|
||||
unsigned num_fixed, expr* const* fixed_ids,
|
||||
unsigned num_eqs, expr* const* eq_lhs, expr* const* eq_rhs,
|
||||
expr* conseq) {
|
||||
bool solver::propagate_cb(
|
||||
unsigned num_fixed, expr* const* fixed_ids,
|
||||
unsigned num_eqs, expr* const* eq_lhs, expr* const* eq_rhs,
|
||||
expr* conseq) {
|
||||
auto* n = ctx.get_enode(conseq);
|
||||
if (n && s().value(ctx.enode2literal(n)) == l_true)
|
||||
return false;
|
||||
m_fixed_ids.reset();
|
||||
for (unsigned i = 0; i < num_fixed; ++i)
|
||||
m_fixed_ids.push_back(get_th_var(fixed_ids[i]));
|
||||
m_prop.push_back(prop_info(num_fixed, m_fixed_ids.data(), num_eqs, eq_lhs, eq_rhs, expr_ref(conseq, m)));
|
||||
DEBUG_CODE(validate_propagation(););
|
||||
return true;
|
||||
}
|
||||
|
||||
void solver::register_cb(expr* e) {
|
||||
|
|
@ -76,7 +80,7 @@ namespace user_solver {
|
|||
|
||||
sat::check_result solver::check() {
|
||||
if (!(bool)m_final_eh)
|
||||
return sat::check_result::CR_DONE;
|
||||
return sat::check_result::CR_DONE;
|
||||
unsigned sz = m_prop.size();
|
||||
m_final_eh(m_user_context, this);
|
||||
return sz == m_prop.size() ? sat::check_result::CR_DONE : sat::check_result::CR_CONTINUE;
|
||||
|
|
|
|||
|
|
@ -135,7 +135,7 @@ namespace user_solver {
|
|||
|
||||
bool has_fixed() const { return (bool)m_fixed_eh; }
|
||||
|
||||
void propagate_cb(unsigned num_fixed, expr* const* fixed_ids, unsigned num_eqs, expr* const* lhs, expr* const* rhs, expr* conseq) override;
|
||||
bool propagate_cb(unsigned num_fixed, expr* const* fixed_ids, unsigned num_eqs, expr* const* lhs, expr* const* rhs, expr* conseq) override;
|
||||
void register_cb(expr* e) override;
|
||||
bool next_split_cb(expr* e, unsigned idx, lbool phase) override;
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue