mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
commit
1a4636518c
|
@ -181,7 +181,7 @@ extern "C" {
|
|||
if (!is) {
|
||||
SET_ERROR_CODE(Z3_FILE_ACCESS_ERROR, nullptr);
|
||||
}
|
||||
else if (ext && std::string("dimacs") == ext) {
|
||||
else if (ext && (std::string("dimacs") == ext || std::string("cnf") == ext)) {
|
||||
ast_manager& m = to_solver_ref(s)->get_manager();
|
||||
std::stringstream err;
|
||||
sat::solver solver(to_solver_ref(s)->get_params(), m.limit());
|
||||
|
|
|
@ -482,6 +482,7 @@ def _to_ast_ref(a, ctx):
|
|||
else:
|
||||
return _to_expr_ref(a, ctx)
|
||||
|
||||
|
||||
#########################################
|
||||
#
|
||||
# Sorts
|
||||
|
@ -6664,17 +6665,11 @@ class Solver(Z3PPObject):
|
|||
|
||||
def from_file(self, filename):
|
||||
"""Parse assertions from a file"""
|
||||
try:
|
||||
Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
|
||||
except Z3Exception as e:
|
||||
_handle_parse_error(e, self.ctx)
|
||||
Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
|
||||
|
||||
def from_string(self, s):
|
||||
"""Parse assertions from a string"""
|
||||
try:
|
||||
Z3_solver_from_string(self.ctx.ref(), self.solver, s)
|
||||
except Z3Exception as e:
|
||||
_handle_parse_error(e, self.ctx)
|
||||
Z3_solver_from_string(self.ctx.ref(), self.solver, s)
|
||||
|
||||
def cube(self, vars = None):
|
||||
"""Get set of cubes
|
||||
|
@ -7063,17 +7058,11 @@ class Fixedpoint(Z3PPObject):
|
|||
|
||||
def parse_string(self, s):
|
||||
"""Parse rules and queries from a string"""
|
||||
try:
|
||||
return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
|
||||
except Z3Exception as e:
|
||||
_handle_parse_error(e, self.ctx)
|
||||
return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
|
||||
|
||||
def parse_file(self, f):
|
||||
"""Parse rules and queries from a file"""
|
||||
try:
|
||||
return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
|
||||
except Z3Exception as e:
|
||||
_handle_parse_error(e, self.ctx)
|
||||
return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
|
||||
|
||||
def get_rules(self):
|
||||
"""retrieve rules that have been added to fixedpoint context"""
|
||||
|
@ -7410,17 +7399,11 @@ class Optimize(Z3PPObject):
|
|||
|
||||
def from_file(self, filename):
|
||||
"""Parse assertions and objectives from a file"""
|
||||
try:
|
||||
Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
|
||||
except Z3Exception as e:
|
||||
_handle_parse_error(e, self.ctx)
|
||||
Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)
|
||||
|
||||
def from_string(self, s):
|
||||
"""Parse assertions and objectives from a string"""
|
||||
try:
|
||||
Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
|
||||
except Z3Exception as e:
|
||||
_handle_parse_error(e, self.ctx)
|
||||
Z3_optimize_from_string(self.ctx.ref(), self.optimize, s)
|
||||
|
||||
def assertions(self):
|
||||
"""Return an AST vector containing all added constraints."""
|
||||
|
|
|
@ -143,7 +143,77 @@ namespace datatype {
|
|||
}
|
||||
return r;
|
||||
}
|
||||
size* size::mk_power(size* a1, size* a2) { return alloc(power, a1, a2); }
|
||||
|
||||
size* size::mk_power(size* a1, size* a2) {
|
||||
return alloc(power, a1, a2);
|
||||
}
|
||||
|
||||
|
||||
sort_size plus::eval(obj_map<sort, sort_size> const& S) {
|
||||
rational r(0);
|
||||
ptr_vector<size> todo;
|
||||
todo.push_back(m_arg1);
|
||||
todo.push_back(m_arg2);
|
||||
while (!todo.empty()) {
|
||||
size* s = todo.back();
|
||||
todo.pop_back();
|
||||
plus* p = dynamic_cast<plus*>(s);
|
||||
if (p) {
|
||||
todo.push_back(p->m_arg1);
|
||||
todo.push_back(p->m_arg2);
|
||||
}
|
||||
else {
|
||||
sort_size sz = s->eval(S);
|
||||
if (sz.is_infinite()) return sz;
|
||||
if (sz.is_very_big()) return sz;
|
||||
r += rational(sz.size(), rational::ui64());
|
||||
}
|
||||
}
|
||||
return sort_size(r);
|
||||
}
|
||||
|
||||
size* plus::subst(obj_map<sort,size*>& S) {
|
||||
return mk_plus(m_arg1->subst(S), m_arg2->subst(S));
|
||||
}
|
||||
|
||||
sort_size times::eval(obj_map<sort, sort_size> const& S) {
|
||||
sort_size s1 = m_arg1->eval(S);
|
||||
sort_size s2 = m_arg2->eval(S);
|
||||
if (s1.is_infinite()) return s1;
|
||||
if (s2.is_infinite()) return s2;
|
||||
if (s1.is_very_big()) return s1;
|
||||
if (s2.is_very_big()) return s2;
|
||||
rational r = rational(s1.size(), rational::ui64()) * rational(s2.size(), rational::ui64());
|
||||
return sort_size(r);
|
||||
}
|
||||
|
||||
size* times::subst(obj_map<sort,size*>& S) {
|
||||
return mk_times(m_arg1->subst(S), m_arg2->subst(S));
|
||||
}
|
||||
|
||||
sort_size power::eval(obj_map<sort, sort_size> const& S) {
|
||||
sort_size s1 = m_arg1->eval(S);
|
||||
sort_size s2 = m_arg2->eval(S);
|
||||
// s1^s2
|
||||
if (s1.is_infinite()) return s1;
|
||||
if (s2.is_infinite()) return s2;
|
||||
if (s1.is_very_big()) return s1;
|
||||
if (s2.is_very_big()) return s2;
|
||||
if (s1.size() == 1) return s1;
|
||||
if (s2.size() == 1) return s1;
|
||||
if (s1.size() > (2 << 20) || s2.size() > 10) return sort_size::mk_very_big();
|
||||
rational r = ::power(rational(s1.size(), rational::ui64()), static_cast<unsigned>(s2.size()));
|
||||
return sort_size(r);
|
||||
}
|
||||
|
||||
size* power::subst(obj_map<sort,size*>& S) {
|
||||
return mk_power(m_arg1->subst(S), m_arg2->subst(S));
|
||||
}
|
||||
|
||||
size* sparam::subst(obj_map<sort, size*>& S) {
|
||||
return S[m_param];
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
namespace decl {
|
||||
|
@ -668,7 +738,7 @@ namespace datatype {
|
|||
continue;
|
||||
}
|
||||
|
||||
ptr_vector<param_size::size> s_add;
|
||||
ptr_vector<param_size::size> s_add;
|
||||
for (constructor const* c : d) {
|
||||
ptr_vector<param_size::size> s_mul;
|
||||
for (accessor const* a : *c) {
|
||||
|
|
|
@ -132,71 +132,28 @@ namespace datatype {
|
|||
size* m_arg1, *m_arg2;
|
||||
plus(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref();}
|
||||
~plus() override { m_arg1->dec_ref(); m_arg2->dec_ref(); }
|
||||
size* subst(obj_map<sort,size*>& S) override { return mk_plus(m_arg1->subst(S), m_arg2->subst(S)); }
|
||||
sort_size eval(obj_map<sort, sort_size> const& S) override {
|
||||
rational r(0);
|
||||
ptr_vector<size> todo;
|
||||
todo.push_back(m_arg1);
|
||||
todo.push_back(m_arg2);
|
||||
while (!todo.empty()) {
|
||||
size* s = todo.back();
|
||||
todo.pop_back();
|
||||
plus* p = dynamic_cast<plus*>(s);
|
||||
if (p) {
|
||||
todo.push_back(p->m_arg1);
|
||||
todo.push_back(p->m_arg2);
|
||||
}
|
||||
else {
|
||||
sort_size sz = s->eval(S);
|
||||
if (sz.is_infinite()) return sz;
|
||||
if (sz.is_very_big()) return sz;
|
||||
r += rational(sz.size(), rational::ui64());
|
||||
}
|
||||
}
|
||||
return sort_size(r);
|
||||
}
|
||||
size* subst(obj_map<sort,size*>& S) override;
|
||||
sort_size eval(obj_map<sort, sort_size> const& S) override;
|
||||
};
|
||||
struct times : public size {
|
||||
size* m_arg1, *m_arg2;
|
||||
times(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); }
|
||||
~times() override { m_arg1->dec_ref(); m_arg2->dec_ref(); }
|
||||
size* subst(obj_map<sort,size*>& S) override { return mk_times(m_arg1->subst(S), m_arg2->subst(S)); }
|
||||
sort_size eval(obj_map<sort, sort_size> const& S) override {
|
||||
sort_size s1 = m_arg1->eval(S);
|
||||
sort_size s2 = m_arg2->eval(S);
|
||||
if (s1.is_infinite()) return s1;
|
||||
if (s2.is_infinite()) return s2;
|
||||
if (s1.is_very_big()) return s1;
|
||||
if (s2.is_very_big()) return s2;
|
||||
rational r = rational(s1.size(), rational::ui64()) * rational(s2.size(), rational::ui64());
|
||||
return sort_size(r);
|
||||
}
|
||||
size* subst(obj_map<sort,size*>& S) override;
|
||||
sort_size eval(obj_map<sort, sort_size> const& S) override;
|
||||
};
|
||||
struct power : public size {
|
||||
size* m_arg1, *m_arg2;
|
||||
power(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); }
|
||||
~power() override { m_arg1->dec_ref(); m_arg2->dec_ref(); }
|
||||
size* subst(obj_map<sort,size*>& S) override { return mk_power(m_arg1->subst(S), m_arg2->subst(S)); }
|
||||
sort_size eval(obj_map<sort, sort_size> const& S) override {
|
||||
sort_size s1 = m_arg1->eval(S);
|
||||
sort_size s2 = m_arg2->eval(S);
|
||||
// s1^s2
|
||||
if (s1.is_infinite()) return s1;
|
||||
if (s2.is_infinite()) return s2;
|
||||
if (s1.is_very_big()) return s1;
|
||||
if (s2.is_very_big()) return s2;
|
||||
if (s1.size() == 1) return s1;
|
||||
if (s2.size() == 1) return s1;
|
||||
if (s1.size() > (2 << 20) || s2.size() > 10) return sort_size::mk_very_big();
|
||||
rational r = ::power(rational(s1.size(), rational::ui64()), static_cast<unsigned>(s2.size()));
|
||||
return sort_size(r);
|
||||
}
|
||||
size* subst(obj_map<sort,size*>& S) override;
|
||||
sort_size eval(obj_map<sort, sort_size> const& S) override;
|
||||
};
|
||||
struct sparam : public size {
|
||||
sort_ref m_param;
|
||||
sparam(sort_ref& p): m_param(p) {}
|
||||
~sparam() override {}
|
||||
size* subst(obj_map<sort,size*>& S) override { return S[m_param]; }
|
||||
size* subst(obj_map<sort, size*>& S) override;
|
||||
sort_size eval(obj_map<sort, sort_size> const& S) override { return S[m_param]; }
|
||||
};
|
||||
};
|
||||
|
|
|
@ -192,10 +192,14 @@ namespace sat {
|
|||
report rpt(*this);
|
||||
m_last_num_units = trail_sz;
|
||||
m_cleanup_counter = 0;
|
||||
cleanup_watches();
|
||||
cleanup_clauses(s.m_clauses);
|
||||
cleanup_clauses(s.m_learned);
|
||||
s.propagate(false);
|
||||
do {
|
||||
trail_sz = s.m_trail.size();
|
||||
cleanup_watches();
|
||||
cleanup_clauses(s.m_clauses);
|
||||
cleanup_clauses(s.m_learned);
|
||||
s.propagate(false);
|
||||
}
|
||||
while (trail_sz < s.m_trail.size());
|
||||
CASSERT("cleaner_bug", s.check_invariant());
|
||||
return true;
|
||||
}
|
||||
|
|
|
@ -23,9 +23,15 @@ Revision History:
|
|||
namespace sat {
|
||||
|
||||
elim_eqs::elim_eqs(solver & s):
|
||||
m_solver(s) {
|
||||
m_solver(s),
|
||||
m_to_delete(nullptr) {
|
||||
}
|
||||
|
||||
elim_eqs::~elim_eqs() {
|
||||
dealloc(m_to_delete);
|
||||
}
|
||||
|
||||
|
||||
inline literal norm(literal_vector const & roots, literal l) {
|
||||
if (l.sign())
|
||||
return ~roots[l.var()];
|
||||
|
@ -86,6 +92,12 @@ namespace sat {
|
|||
m_new_bin.reset();
|
||||
}
|
||||
|
||||
void elim_eqs::drat_delete_clause() {
|
||||
if (m_solver.m_config.m_drat) {
|
||||
m_solver.m_drat.del(*m_to_delete->get());
|
||||
}
|
||||
}
|
||||
|
||||
void elim_eqs::cleanup_clauses(literal_vector const & roots, clause_vector & cs) {
|
||||
clause_vector::iterator it = cs.begin();
|
||||
clause_vector::iterator it2 = it;
|
||||
|
@ -107,8 +119,16 @@ namespace sat {
|
|||
it2++;
|
||||
continue;
|
||||
}
|
||||
if (!c.frozen())
|
||||
if (!c.frozen()) {
|
||||
m_solver.detach_clause(c);
|
||||
}
|
||||
|
||||
// save clause to be deleted for drat
|
||||
if (m_solver.m_config.m_drat) {
|
||||
if (!m_to_delete) m_to_delete = alloc(tmp_clause);
|
||||
m_to_delete->set(sz, c.begin(), c.is_learned());
|
||||
}
|
||||
|
||||
// apply substitution
|
||||
for (i = 0; i < sz; i++) {
|
||||
literal lit = c[i];
|
||||
|
@ -124,60 +144,69 @@ namespace sat {
|
|||
CTRACE("sat", l != norm(roots, l), tout << l << " " << norm(roots, l) << "\n"; tout.flush(););
|
||||
SASSERT(l == norm(roots, l));
|
||||
} });
|
||||
|
||||
// remove duplicates, and check if it is a tautology
|
||||
literal l_prev = null_literal;
|
||||
unsigned j = 0;
|
||||
literal l_prev = null_literal;
|
||||
for (i = 0; i < sz; i++) {
|
||||
literal l = c[i];
|
||||
if (l == l_prev)
|
||||
continue;
|
||||
if (l == ~l_prev)
|
||||
if (l == ~l_prev) {
|
||||
break;
|
||||
}
|
||||
if (l == l_prev) {
|
||||
continue;
|
||||
}
|
||||
SASSERT(l != ~l_prev);
|
||||
l_prev = l;
|
||||
lbool val = m_solver.value(l);
|
||||
if (val == l_true)
|
||||
break; // clause was satisfied
|
||||
if (val == l_false)
|
||||
if (val == l_true) {
|
||||
break;
|
||||
}
|
||||
if (val == l_false) {
|
||||
continue; // skip
|
||||
}
|
||||
c[j] = l;
|
||||
j++;
|
||||
}
|
||||
TRACE("elim_eqs", tout << "after removing duplicates: " << c << " j: " << j << "\n";);
|
||||
|
||||
if (i < sz) {
|
||||
// clause is a tautology or was simplified to true
|
||||
m_solver.del_clause(c);
|
||||
drat_delete_clause();
|
||||
m_solver.del_clause(c, false);
|
||||
continue;
|
||||
}
|
||||
if (j == 0) {
|
||||
// empty clause
|
||||
|
||||
switch (j) {
|
||||
case 0:
|
||||
m_solver.set_conflict(justification());
|
||||
for (; it != end; ++it) {
|
||||
*it2 = *it;
|
||||
it2++;
|
||||
}
|
||||
cs.set_end(it2);
|
||||
return;
|
||||
}
|
||||
TRACE("elim_eqs", tout << "after removing duplicates: " << c << " j: " << j << "\n";);
|
||||
|
||||
SASSERT(j >= 1);
|
||||
switch (j) {
|
||||
return;
|
||||
case 1:
|
||||
m_solver.assign(c[0], justification());
|
||||
m_solver.del_clause(c);
|
||||
m_solver.del_clause(c, false);
|
||||
drat_delete_clause();
|
||||
break;
|
||||
case 2:
|
||||
m_solver.mk_bin_clause(c[0], c[1], c.is_learned());
|
||||
m_solver.del_clause(c);
|
||||
m_solver.del_clause(c, false);
|
||||
drat_delete_clause();
|
||||
break;
|
||||
default:
|
||||
SASSERT(*it == &c);
|
||||
if (j < sz) {
|
||||
if (m_solver.m_config.m_drat) m_solver.m_drat.del(c);
|
||||
c.shrink(j);
|
||||
if (m_solver.m_config.m_drat) m_solver.m_drat.add(c, true);
|
||||
}
|
||||
else
|
||||
else {
|
||||
c.update_approx();
|
||||
}
|
||||
if (m_solver.m_config.m_drat) {
|
||||
m_solver.m_drat.add(c, true);
|
||||
drat_delete_clause();
|
||||
}
|
||||
|
||||
DEBUG_CODE(for (literal l : c) VERIFY(l == norm(roots, l)););
|
||||
|
||||
|
|
|
@ -23,6 +23,7 @@ Revision History:
|
|||
|
||||
namespace sat {
|
||||
class solver;
|
||||
class tmp_clause;
|
||||
|
||||
class elim_eqs {
|
||||
struct bin {
|
||||
|
@ -32,6 +33,8 @@ namespace sat {
|
|||
};
|
||||
svector<bin> m_new_bin;
|
||||
solver & m_solver;
|
||||
tmp_clause* m_to_delete;
|
||||
void drat_delete_clause();
|
||||
void save_elim(literal_vector const & roots, bool_var_vector const & to_elim);
|
||||
void cleanup_clauses(literal_vector const & roots, clause_vector & cs);
|
||||
void cleanup_bin_watches(literal_vector const & roots);
|
||||
|
@ -39,6 +42,7 @@ namespace sat {
|
|||
bool check_clause(clause const& c, literal_vector const& roots) const;
|
||||
public:
|
||||
elim_eqs(solver & s);
|
||||
~elim_eqs();
|
||||
void operator()(literal_vector const & roots, bool_var_vector const & to_elim);
|
||||
};
|
||||
|
||||
|
|
|
@ -1272,7 +1272,8 @@ namespace sat {
|
|||
* unless C contains lit, and it is a tautology.
|
||||
*/
|
||||
bool add_ala() {
|
||||
for (; m_ala_qhead < m_covered_clause.size(); ++m_ala_qhead) {
|
||||
unsigned init_size = m_covered_clause.size();
|
||||
for (; m_ala_qhead < m_covered_clause.size() && m_ala_qhead < 5*init_size; ++m_ala_qhead) {
|
||||
literal l = m_covered_clause[m_ala_qhead];
|
||||
for (watched & w : s.get_wlist(~l)) {
|
||||
if (w.is_binary_non_learned_clause()) {
|
||||
|
@ -1282,7 +1283,6 @@ namespace sat {
|
|||
return true;
|
||||
}
|
||||
if (!s.is_marked(~lit)) {
|
||||
// if (m_covered_clause[0].var() == 10219) IF_VERBOSE(0, verbose_stream() << "ala: " << l << " " << lit << "\n");
|
||||
m_covered_clause.push_back(~lit);
|
||||
m_covered_antecedent.push_back(clause_ante(l, false));
|
||||
s.mark_visited(~lit);
|
||||
|
@ -1312,7 +1312,6 @@ namespace sat {
|
|||
if (lit1 == null_literal) {
|
||||
return true;
|
||||
}
|
||||
// if (m_covered_clause[0].var() == 10219) IF_VERBOSE(0, verbose_stream() << "ala: " << c << " " << lit1 << "\n");
|
||||
m_covered_clause.push_back(~lit1);
|
||||
m_covered_antecedent.push_back(clause_ante(c));
|
||||
s.mark_visited(~lit1);
|
||||
|
@ -1527,6 +1526,7 @@ namespace sat {
|
|||
block_covered_binary(w, l, blocked, k);
|
||||
break;
|
||||
}
|
||||
s.checkpoint();
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -1552,6 +1552,7 @@ namespace sat {
|
|||
s.set_learned(c);
|
||||
break;
|
||||
}
|
||||
s.checkpoint();
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -298,14 +298,14 @@ namespace sat {
|
|||
mk_clause(3, ls, learned);
|
||||
}
|
||||
|
||||
void solver::del_clause(clause& c) {
|
||||
void solver::del_clause(clause& c, bool enable_drat) {
|
||||
if (!c.is_learned()) {
|
||||
m_stats.m_non_learned_generation++;
|
||||
}
|
||||
if (c.frozen()) {
|
||||
--m_num_frozen;
|
||||
}
|
||||
if (m_config.m_drat && !m_drat.is_cleaned(c)) {
|
||||
if (enable_drat && m_config.m_drat && !m_drat.is_cleaned(c)) {
|
||||
m_drat.del(c);
|
||||
}
|
||||
dealloc_clause(&c);
|
||||
|
|
|
@ -232,7 +232,7 @@ namespace sat {
|
|||
void defrag_clauses();
|
||||
bool should_defrag();
|
||||
bool memory_pressure();
|
||||
void del_clause(clause & c);
|
||||
void del_clause(clause & c, bool enable_drat = true);
|
||||
clause * mk_clause_core(unsigned num_lits, literal * lits, bool learned);
|
||||
clause * mk_clause_core(literal_vector const& lits) { return mk_clause_core(lits.size(), lits.c_ptr()); }
|
||||
clause * mk_clause_core(unsigned num_lits, literal * lits) { return mk_clause_core(num_lits, lits, false); }
|
||||
|
|
|
@ -1197,8 +1197,11 @@ namespace smt {
|
|||
literal_vector& lits = get_unhelpful_literals(c, true);
|
||||
lits.push_back(c.lit());
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
DEBUG_CODE(validate_assign(c, lits, c.lit(i)););
|
||||
add_assign(c, lits, c.lit(i));
|
||||
literal lit = c.lit(i);
|
||||
if (ctx.get_assignment(lit) == l_undef) {
|
||||
DEBUG_CODE(validate_assign(c, lits, lit););
|
||||
add_assign(c, lits, c.lit(i));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
@ -51,6 +51,10 @@ bool assertions_enabled();
|
|||
#endif
|
||||
#endif
|
||||
|
||||
#ifdef __EMSCRIPTEN__
|
||||
#define NO_Z3_DEBUGGER
|
||||
#endif
|
||||
|
||||
#ifdef NO_Z3_DEBUGGER
|
||||
#define INVOKE_DEBUGGER() exit(ERR_INTERNAL_FATAL)
|
||||
#else
|
||||
|
|
Loading…
Reference in a new issue