mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-09 23:53:25 +00:00
Code Activity

fix #2452 fix #2451

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-08-01 16:28:05 +08:00
parent b7a27ca4bd
commit 7f073a0585
4 changed files with 302 additions and 300 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/nlsat/nlsat_solver.cpp
View file

@ -1408,16 +1408,13 @@ namespace nlsat {
} }
void collect(literal_vector const& assumptions, clause_vector& clauses) { void collect(literal_vector const& assumptions, clause_vector& clauses) {
unsigned n = clauses.size();
unsigned j = 0; unsigned j = 0;
for (unsigned i = 0; i < n; i++) { for (clause * c : clauses) {
clause * c = clauses[i];
if (collect(assumptions, *c)) { if (collect(assumptions, *c)) {
del_clause(c); del_clause(c);
} }
else { else {
clauses[j] = c; clauses[j++] = c;
j++;
} }
} }
clauses.shrink(j); clauses.shrink(j);
@ -1432,11 +1429,12 @@ namespace nlsat {
} }
vector<assumption, false> deps; vector<assumption, false> deps;
m_asm.linearize(asms, deps); m_asm.linearize(asms, deps);
bool found = false; for (auto dep : deps) {
for (unsigned i = 0; !found && i < deps.size(); ++i) { if (ptr <= dep && dep < ptr + sz) {
found = ptr <= deps[i] && deps[i] < ptr + sz; return true;
}
} }
return found; return false;
} }
// ----------------------- // -----------------------
@ -1453,8 +1451,8 @@ namespace nlsat {
// Conflict resolution invariant: a marked literal is in m_lemma or on the trail stack. // Conflict resolution invariant: a marked literal is in m_lemma or on the trail stack.
bool check_marks() { bool check_marks() {
for (unsigned i = 0; i < m_marks.size(); i++) { for (unsigned m : m_marks) {
SASSERT(m_marks[i] == 0); SASSERT(m == 0);
} }
return true; return true;
} }
@ -1468,14 +1466,13 @@ namespace nlsat {
void reset_mark(bool_var b) { m_marks[b] = 0; } void reset_mark(bool_var b) { m_marks[b] = 0; }
void reset_marks() { void reset_marks() {
unsigned sz = m_lemma.size(); for (auto const& l : m_lemma) {
for (unsigned i = 0; i < sz; i++) { reset_mark(l.var());
reset_mark(m_lemma[i].var());
} }
} }
void process_antecedent(literal antecedent) { void process_antecedent(literal antecedent) {
bool_var b = antecedent.var(); bool_var b = antecedent.var();
TRACE("nlsat_resolve", tout << "resolving antecedent, l:\n"; display(tout, antecedent); tout << "\n";); TRACE("nlsat_resolve", tout << "resolving antecedent, l:\n"; display(tout, antecedent); tout << "\n";);
if (assigned_value(antecedent) == l_undef) { if (assigned_value(antecedent) == l_undef) {
// antecedent must be false in the current arith interpretation // antecedent must be false in the current arith interpretation

548
src/qe/nlqsat.cpp
View file

@ -40,8 +40,7 @@ namespace qe {
enum qsat_mode_t { enum qsat_mode_t {
qsat_t, qsat_t,
elim_t, elim_t
interp_t
}; };
class nlqsat : public tactic { class nlqsat : public tactic {
@ -55,48 +54,210 @@ namespace qe {
void reset() { memset(this, 0, sizeof(*this)); } void reset() { memset(this, 0, sizeof(*this)); }
}; };
struct solver_state {
ast_manager& m;
params_ref m_params;
nlsat::solver m_solver;
nlsat::literal m_is_true;
nlsat::assignment m_rmodel;
svector<lbool> m_bmodel;
nlsat::assignment m_rmodel0;
svector<lbool> m_bmodel0;
bool m_valid_model;
vector<nlsat::var_vector> m_bound_rvars;
vector<svector<nlsat::bool_var> > m_bound_bvars;
vector<nlsat::scoped_literal_vector> m_preds;
svector<max_level> m_rvar2level;
u_map<max_level> m_bvar2level;
expr2var m_a2b, m_t2x;
u_map<expr*> m_b2a, m_x2t;
nlsat::literal_vector m_assumptions;
nlsat::literal_vector m_asms;
nlsat::literal_vector m_cached_asms;
unsigned_vector m_cached_asms_lim;
u_map<expr*> m_asm2fml;
solver_state(ast_manager& m, params_ref const& p):
m(m),
m_params(p),
m_solver(m.limit(), p, true),
m_rmodel(m_solver.am()),
m_rmodel0(m_solver.am()),
m_valid_model(false),
m_a2b(m),
m_t2x(m)
{}
void g2s(goal const& g) {
goal2nlsat gs;
gs(g, m_params, m_solver, m_a2b, m_t2x);
}
void init_expr2var(vector<app_ref_vector> const& qvars) {
for (app_ref_vector const& qvs : qvars) {
init_expr2var(qvs);
}
}
void init_expr2var(app_ref_vector const& qvars) {
for (app* v : qvars) {
if (m.is_bool(v)) {
m_a2b.insert(v, m_solver.mk_bool_var());
}
else {
// TODO: assert it is of type Real.
m_t2x.insert(v, m_solver.mk_var(false));
}
}
}
void init_var2expr() {
for (auto const& kv : m_t2x) {
m_x2t.insert(kv.m_value, kv.m_key);
}
for (auto const& kv : m_a2b) {
m_b2a.insert(kv.m_value, kv.m_key);
}
}
void save_model(bool is_exists) {
m_solver.get_rvalues(m_rmodel);
m_solver.get_bvalues(m_bmodel);
m_valid_model = true;
if (is_exists) {
m_rmodel0.copy(m_rmodel);
m_bmodel0.reset();
m_bmodel0.append(m_bmodel);
}
}
void unsave_model() {
SASSERT(m_valid_model);
m_solver.set_rvalues(m_rmodel);
m_solver.set_bvalues(m_bmodel);
}
void clear_model() {
m_valid_model = false;
m_rmodel.reset();
m_bmodel.reset();
m_solver.set_rvalues(m_rmodel);
}
void add_assumption_literal(clause& clause, expr* fml) {
nlsat::bool_var b = m_solver.mk_bool_var();
clause.push_back(nlsat::literal(b, true));
m_assumptions.push_back(nlsat::literal(b, false));
m_solver.inc_ref(b);
m_asm2fml.insert(b, fml);
m_bvar2level.insert(b, max_level());
}
expr_ref clause2fml(nlsat::scoped_literal_vector const& clause) {
expr_ref_vector fmls(m);
expr_ref fml(m);
expr* t;
nlsat2goal n2g(m);
for (nlsat::literal l : clause) {
if (m_asm2fml.find(l.var(), t)) {
fml = t;
if (l.sign()) {
fml = push_not(fml);
}
SASSERT(l.sign());
fmls.push_back(fml);
}
else {
fmls.push_back(n2g(m_solver, m_b2a, m_x2t, l));
}
}
fml = mk_or(fmls);
return fml;
}
void add_literal(nlsat::literal_vector& lits, nlsat::literal l) {
lbool r = m_solver.value(l);
switch (r) {
case l_true:
lits.push_back(l);
break;
case l_false:
lits.push_back(~l);
break;
default:
lits.push_back(l);
break;
}
}
void display(std::ostream& out) {
out << "level " << level() << "\n";
display_preds(out);
display_assumptions(out);
m_solver.display(out << "solver:\n");
}
void display_assumptions(std::ostream& out) {
m_solver.display(out << "assumptions: ", m_asms.size(), m_asms.c_ptr());
out << "\n";
}
void display_preds(std::ostream& out) {
for (unsigned i = 0; i < m_preds.size(); ++i) {
m_solver.display(out << i << ": ", m_preds[i].size(), m_preds[i].c_ptr());
out << "\n";
}
}
unsigned level() const {
return m_cached_asms_lim.size();
}
void reset() {
m_asms.reset();
m_cached_asms.reset();
m_cached_asms_lim.reset();
m_is_true = nlsat::null_literal;
m_rmodel.reset();
m_valid_model = false;
m_bound_rvars.reset();
m_bound_bvars.reset();
m_preds.reset();
for (auto const& kv : m_bvar2level) {
m_solver.dec_ref(kv.m_key);
}
m_rvar2level.reset();
m_bvar2level.reset();
m_t2x.reset();
m_a2b.reset();
m_b2a.reset();
m_x2t.reset();
m_assumptions.reset();
m_asm2fml.reset();
}
};
ast_manager& m; ast_manager& m;
solver_state s;
qsat_mode_t m_mode; qsat_mode_t m_mode;
params_ref m_params; params_ref m_params;
nlsat::solver m_solver;
tactic_ref m_nftactic; tactic_ref m_nftactic;
nlsat::literal_vector m_asms; stats m_stats;
nlsat::literal_vector m_cached_asms; statistics m_st;
unsigned_vector m_cached_asms_lim; obj_hashtable<expr> m_free_vars;
nlsat::literal m_is_true; obj_hashtable<expr> m_aux_vars;
nlsat::assignment m_rmodel; expr_ref_vector m_answer;
svector<lbool> m_bmodel; expr_safe_replace m_answer_simplify;
nlsat::assignment m_rmodel0; expr_ref_vector m_trail;
svector<lbool> m_bmodel0;
bool m_valid_model;
vector<nlsat::var_vector> m_bound_rvars;
vector<svector<nlsat::bool_var> > m_bound_bvars;
vector<nlsat::scoped_literal_vector> m_preds;
svector<max_level> m_rvar2level;
u_map<max_level> m_bvar2level;
expr2var m_a2b, m_t2x;
u_map<expr*> m_b2a, m_x2t;
volatile bool m_cancel;
stats m_stats;
statistics m_st;
obj_hashtable<expr> m_free_vars;
obj_hashtable<expr> m_aux_vars;
expr_ref_vector m_answer;
expr_safe_replace m_answer_simplify;
nlsat::literal_vector m_assumptions;
u_map<expr*> m_asm2fml;
expr_ref_vector m_trail;
lbool check_sat() { lbool check_sat() {
while (true) { while (true) {
++m_stats.m_num_rounds; ++m_stats.m_num_rounds;
check_cancel(); check_cancel();
init_assumptions(); init_assumptions();
lbool res = m_solver.check(m_asms); lbool res = s.m_solver.check(s.m_asms);
TRACE("qe", display(tout); ); TRACE("qe", s.display(tout << res << "\n"); );
switch (res) { switch (res) {
case l_true: case l_true:
save_model(); s.save_model(is_exists(level()));
push(); push();
break; break;
case l_false: case l_false:
@ -113,70 +274,55 @@ namespace qe {
void init_assumptions() { void init_assumptions() {
unsigned lvl = level(); unsigned lvl = level();
m_asms.reset(); s.m_asms.reset();
m_asms.push_back(is_exists()?m_is_true:~m_is_true); s.m_asms.push_back(is_exists()?s.m_is_true:~s.m_is_true);
m_asms.append(m_assumptions); s.m_asms.append(s.m_assumptions);
TRACE("qe", tout << "model valid: " << m_valid_model << " level: " << lvl << " "; TRACE("qe", tout << "model valid: " << s.m_valid_model << " level: " << lvl << " ";
display_assumptions(tout); s.display_assumptions(tout);
m_solver.display(tout);); s.m_solver.display(tout););
if (!m_valid_model) { if (!s.m_valid_model) {
m_asms.append(m_cached_asms); s.m_asms.append(s.m_cached_asms);
return; return;
} }
unsave_model(); s.unsave_model();
if (lvl == 0) { if (lvl == 0) {
SASSERT(m_cached_asms.empty()); SASSERT(s.m_cached_asms.empty());
return; return;
} }
if (lvl <= m_preds.size()) { if (lvl <= s.m_preds.size()) {
for (unsigned j = 0; j < m_preds[lvl - 1].size(); ++j) { for (unsigned j = 0; j < s.m_preds[lvl - 1].size(); ++j) {
add_literal(m_cached_asms, m_preds[lvl - 1][j]); s.add_literal(s.m_cached_asms, s.m_preds[lvl - 1][j]);
} }
} }
m_asms.append(m_cached_asms); s.m_asms.append(s.m_cached_asms);
for (unsigned i = lvl + 1; i < m_preds.size(); i += 2) { for (unsigned i = lvl + 1; i < s.m_preds.size(); i += 2) {
for (unsigned j = 0; j < m_preds[i].size(); ++j) { for (unsigned j = 0; j < s.m_preds[i].size(); ++j) {
nlsat::literal l = m_preds[i][j]; nlsat::literal l = s.m_preds[i][j];
max_level lv = m_bvar2level.find(l.var()); max_level lv = s.m_bvar2level.find(l.var());
bool use = bool use =
(lv.m_fa == i && (lv.m_ex == UINT_MAX || lv.m_ex < lvl)) || (lv.m_fa == i && (lv.m_ex == UINT_MAX || lv.m_ex < lvl)) ||
(lv.m_ex == i && (lv.m_fa == UINT_MAX || lv.m_fa < lvl)); (lv.m_ex == i && (lv.m_fa == UINT_MAX || lv.m_fa < lvl));
if (use) { if (use) {
add_literal(m_asms, l); s.add_literal(s.m_asms, l);
} }
} }
} }
TRACE("qe", display(tout); TRACE("qe", s.display(tout);
for (nlsat::literal a : m_asms) { for (nlsat::literal a : s.m_asms) {
m_solver.display(tout, a) << "\n"; s.m_solver.display(tout, a) << "\n";
}); });
save_model(); s.save_model(is_exists(level()));
} }
void add_literal(nlsat::literal_vector& lits, nlsat::literal l) {
lbool r = m_solver.value(l);
switch (r) {
case l_true:
lits.push_back(l);
break;
case l_false:
lits.push_back(~l);
break;
default:
lits.push_back(l);
break;
}
}
template<class S, class T> template<class S, class T>
void insert_set(S& set, T const& vec) { void insert_set(S& set, T const& vec) {
for (unsigned i = 0; i < vec.size(); ++i) { for (auto const& v : vec) {
set.insert(vec[i]); set.insert(v);
} }
} }
void mbp(unsigned level, nlsat::scoped_literal_vector& result) { void mbp(unsigned level, nlsat::scoped_literal_vector& result) {
nlsat::var_vector vars; nlsat::var_vector vars;
@ -186,12 +332,12 @@ namespace qe {
} }
void extract_vars(unsigned level, nlsat::var_vector& vars, uint_set& fvars) { void extract_vars(unsigned level, nlsat::var_vector& vars, uint_set& fvars) {
for (unsigned i = 0; i < m_bound_rvars.size(); ++i) { for (unsigned i = 0; i < s.m_bound_rvars.size(); ++i) {
if (i < level) { if (i < level) {
insert_set(fvars, m_bound_bvars[i]); insert_set(fvars, s.m_bound_bvars[i]);
} }
else { else {
vars.append(m_bound_rvars[i]); vars.append(s.m_bound_rvars[i]);
} }
} }
} }
@ -200,27 +346,27 @@ namespace qe {
// //
// Also project auxiliary variables from clausification. // Also project auxiliary variables from clausification.
// //
unsave_model(); s.unsave_model();
nlsat::explain& ex = m_solver.get_explain(); nlsat::explain& ex = s.m_solver.get_explain();
nlsat::scoped_literal_vector new_result(m_solver); nlsat::scoped_literal_vector new_result(s.m_solver);
result.reset(); result.reset();
// project quantified Boolean variables. // project quantified Boolean variables.
for (nlsat::literal lit : m_asms) { for (nlsat::literal lit : s.m_asms) {
if (!m_b2a.contains(lit.var()) || fvars.contains(lit.var())) { if (!s.m_b2a.contains(lit.var()) || fvars.contains(lit.var())) {
result.push_back(lit); result.push_back(lit);
} }
} }
TRACE("qe", m_solver.display(tout, result.size(), result.c_ptr()); tout << "\n";); TRACE("qe", s.m_solver.display(tout, result.size(), result.c_ptr()); tout << "\n";);
// project quantified real variables. // project quantified real variables.
// They are sorted by size, so we project the largest variables first to avoid // They are sorted by size, so we project the largest variables first to avoid
// renaming variables. // renaming variables.
for (unsigned i = vars.size(); i-- > 0;) { for (unsigned i = vars.size(); i-- > 0;) {
new_result.reset(); new_result.reset();
TRACE("qe", m_solver.display(tout << "project: ", vars[i]) << "\n";); TRACE("qe", s.m_solver.display(tout << "project: ", vars[i]) << "\n";);
ex.project(vars[i], result.size(), result.c_ptr(), new_result); ex.project(vars[i], result.size(), result.c_ptr(), new_result);
result.swap(new_result); result.swap(new_result);
TRACE("qe", m_solver.display(tout, vars[i]) << ": "; TRACE("qe", s.m_solver.display(tout, vars[i]) << ": ";
m_solver.display(tout, result.size(), result.c_ptr()); tout << "\n";); s.m_solver.display(tout, result.size(), result.c_ptr()); tout << "\n";);
} }
negate_clause(result); negate_clause(result);
} }
@ -231,45 +377,21 @@ namespace qe {
} }
} }
void save_model() {
m_solver.get_rvalues(m_rmodel);
m_solver.get_bvalues(m_bmodel);
m_valid_model = true;
if (is_exists(level())) {
m_rmodel0.copy(m_rmodel);
m_bmodel0.reset();
m_bmodel0.append(m_bmodel);
}
}
void unsave_model() {
SASSERT(m_valid_model);
m_solver.set_rvalues(m_rmodel);
m_solver.set_bvalues(m_bmodel);
}
void clear_model() {
m_valid_model = false;
m_rmodel.reset();
m_bmodel.reset();
m_solver.set_rvalues(m_rmodel);
}
unsigned level() const { unsigned level() const {
return m_cached_asms_lim.size(); return s.level();
} }
void enforce_parity(clause& cl) { void enforce_parity(clause& cl) {
cl.push_back(is_exists()?~m_is_true:m_is_true); cl.push_back(is_exists()?~s.m_is_true:s.m_is_true);
} }
void add_clause(clause& cl) { void add_clause(clause& cl) {
if (cl.empty()) { if (cl.empty()) {
cl.push_back(~m_solver.mk_true()); cl.push_back(~s.m_solver.mk_true());
} }
SASSERT(!cl.empty()); SASSERT(!cl.empty());
nlsat::literal_vector lits(cl.size(), cl.c_ptr()); nlsat::literal_vector lits(cl.size(), cl.c_ptr());
m_solver.mk_clause(lits.size(), lits.c_ptr()); s.m_solver.mk_clause(lits.size(), lits.c_ptr());
} }
max_level get_level(clause const& cl) { max_level get_level(clause const& cl) {
@ -286,14 +408,14 @@ namespace qe {
max_level get_level(nlsat::literal l) { max_level get_level(nlsat::literal l) {
max_level level; max_level level;
if (m_bvar2level.find(l.var(), level)) { if (s.m_bvar2level.find(l.var(), level)) {
return level; return level;
} }
nlsat::var_vector vs; nlsat::var_vector vs;
m_solver.vars(l, vs); s.m_solver.vars(l, vs);
TRACE("qe", m_solver.display(tout << vs << " ", l) << "\n";); TRACE("qe", s.m_solver.display(tout << vs << " ", l) << "\n";);
for (unsigned v : vs) { for (unsigned v : vs) {
level.merge(m_rvar2level[v]); level.merge(s.m_rvar2level[v]);
} }
set_level(l.var(), level); set_level(l.var(), level);
return level; return level;
@ -301,19 +423,19 @@ namespace qe {
void set_level(nlsat::bool_var v, max_level const& level) { void set_level(nlsat::bool_var v, max_level const& level) {
unsigned k = level.max(); unsigned k = level.max();
while (m_preds.size() <= k) { while (s.m_preds.size() <= k) {
m_preds.push_back(nlsat::scoped_literal_vector(m_solver)); s.m_preds.push_back(nlsat::scoped_literal_vector(s.m_solver));
} }
nlsat::literal l(v, false); nlsat::literal l(v, false);
m_preds[k].push_back(l); s.m_preds[k].push_back(l);
m_solver.inc_ref(v); s.m_solver.inc_ref(v);
m_bvar2level.insert(v, level); s.m_bvar2level.insert(v, level);
TRACE("qe", m_solver.display(tout, l); tout << ": " << level << "\n";); TRACE("qe", s.m_solver.display(tout, l); tout << ": " << level << "\n";);
} }
void project() { void project() {
TRACE("qe", display_assumptions(tout);); TRACE("qe", s.display_assumptions(tout););
if (!m_valid_model) { if (!s.m_valid_model) {
pop(1); pop(1);
return; return;
} }
@ -323,7 +445,7 @@ namespace qe {
} }
SASSERT(level() >= 2); SASSERT(level() >= 2);
unsigned num_scopes; unsigned num_scopes;
clause cl(m_solver); clause cl(s.m_solver);
mbp(level()-1, cl); mbp(level()-1, cl);
max_level clevel = get_level(cl); max_level clevel = get_level(cl);
@ -347,11 +469,11 @@ namespace qe {
} }
void project_qe() { void project_qe() {
SASSERT(level() >= 1 && m_mode == elim_t && m_valid_model); SASSERT(level() >= 1 && m_mode == elim_t && s.m_valid_model);
clause cl(m_solver); clause cl(s.m_solver);
mbp(std::max(1u, level()-1), cl); mbp(std::max(1u, level()-1), cl);
expr_ref fml = clause2fml(cl); expr_ref fml = s.clause2fml(cl);
TRACE("qe", tout << level() << ": " << fml << "\n";); TRACE("qe", tout << level() << ": " << fml << "\n";);
max_level clevel = get_level(cl); max_level clevel = get_level(cl);
if (level() == 1 || clevel.max() == 0) { if (level() == 1 || clevel.max() == 0) {
@ -386,37 +508,9 @@ namespace qe {
m_answer.push_back(fml); m_answer.push_back(fml);
} }
expr_ref clause2fml(nlsat::scoped_literal_vector const& clause) {
expr_ref_vector fmls(m);
expr_ref fml(m);
expr* t;
nlsat2goal n2g(m);
for (unsigned i = 0; i < clause.size(); ++i) {
nlsat::literal l = clause[i];
if (m_asm2fml.find(l.var(), t)) {
fml = t;
if (l.sign()) {
fml = push_not(fml);
}
SASSERT(l.sign());
fmls.push_back(fml);
}
else {
fmls.push_back(n2g(m_solver, m_b2a, m_x2t, l));
}
}
fml = mk_or(fmls);
return fml;
}
void add_assumption_literal(clause& clause, expr* fml) { void add_assumption_literal(clause& clause, expr* fml) {
nlsat::bool_var b = m_solver.mk_bool_var(); s.add_assumption_literal(clause, fml);
clause.push_back(nlsat::literal(b, true));
m_assumptions.push_back(nlsat::literal(b, false));
m_solver.inc_ref(b);
m_asm2fml.insert(b, fml);
m_trail.push_back(fml); m_trail.push_back(fml);
m_bvar2level.insert(b, max_level());
} }
bool is_exists() const { return is_exists(level()); } bool is_exists() const { return is_exists(level()); }
@ -425,9 +519,6 @@ namespace qe {
bool is_forall(unsigned level) const { return is_exists(level+1); } bool is_forall(unsigned level) const { return is_exists(level+1); }
void check_cancel() { void check_cancel() {
if (m_cancel) {
throw tactic_exception(TACTIC_CANCELED_MSG);
}
} }
struct div { struct div {
@ -554,65 +645,25 @@ namespace qe {
} }
void reset() override { void reset() override {
//m_solver.reset(); s.reset();
m_asms.reset();
m_cached_asms.reset();
m_cached_asms_lim.reset();
m_is_true = nlsat::null_literal;
m_rmodel.reset();
m_valid_model = false;
m_bound_rvars.reset();
m_bound_bvars.reset();
m_preds.reset();
for (auto const& kv : m_bvar2level) {
m_solver.dec_ref(kv.m_key);
}
m_rvar2level.reset();
m_bvar2level.reset();
m_t2x.reset();
m_a2b.reset();
m_b2a.reset();
m_x2t.reset();
m_cancel = false;
m_st.reset(); m_st.reset();
m_solver.collect_statistics(m_st); s.m_solver.collect_statistics(m_st);
m_free_vars.reset(); m_free_vars.reset();
m_aux_vars.reset(); m_aux_vars.reset();
m_answer.reset(); m_answer.reset();
m_answer_simplify.reset(); m_answer_simplify.reset();
m_assumptions.reset();
m_asm2fml.reset();
m_trail.reset(); m_trail.reset();
} }
void push() { void push() {
m_cached_asms_lim.push_back(m_cached_asms.size()); s.m_cached_asms_lim.push_back(s.m_cached_asms.size());
} }
void pop(unsigned num_scopes) { void pop(unsigned num_scopes) {
clear_model(); s.clear_model();
unsigned new_level = level() - num_scopes; unsigned new_level = level() - num_scopes;
m_cached_asms.shrink(m_cached_asms_lim[new_level]); s.m_cached_asms.shrink(s.m_cached_asms_lim[new_level]);
m_cached_asms_lim.shrink(new_level); s.m_cached_asms_lim.shrink(new_level);
}
void display(std::ostream& out) {
out << "level " << level() << "\n";
display_preds(out);
display_assumptions(out);
m_solver.display(out << "solver:\n");
}
void display_assumptions(std::ostream& out) {
m_solver.display(out << "assumptions: ", m_asms.size(), m_asms.c_ptr());
out << "\n";
}
void display_preds(std::ostream& out) {
for (unsigned i = 0; i < m_preds.size(); ++i) {
m_solver.display(out << i << ": ", m_preds[i].size(), m_preds[i].c_ptr());
out << "\n";
}
} }
// expr -> nlsat::solver // expr -> nlsat::solver
@ -648,8 +699,7 @@ namespace qe {
while (!vars.empty()); while (!vars.empty());
SASSERT(qvars.size() >= 2); SASSERT(qvars.size() >= 2);
SASSERT(qvars.back().empty()); SASSERT(qvars.back().empty());
init_expr2var(qvars); s.init_expr2var(qvars);
goal2nlsat g2s;
expr_ref is_true(m), fml1(m), fml2(m); expr_ref is_true(m), fml1(m), fml2(m);
is_true = m.mk_fresh_const("is_true", m.mk_bool_sort()); is_true = m.mk_fresh_const("is_true", m.mk_bool_sort());
@ -661,38 +711,38 @@ namespace qe {
(*m_nftactic)(g, result); (*m_nftactic)(g, result);
SASSERT(result.size() == 1); SASSERT(result.size() == 1);
TRACE("qe", result[0]->display(tout);); TRACE("qe", result[0]->display(tout););
g2s(*result[0], m_params, m_solver, m_a2b, m_t2x); s.g2s(*result[0]);
// insert variables and their levels. // insert variables and their levels.
for (unsigned i = 0; i < qvars.size(); ++i) { for (unsigned i = 0; i < qvars.size(); ++i) {
m_bound_bvars.push_back(svector<nlsat::bool_var>()); s.m_bound_bvars.push_back(svector<nlsat::bool_var>());
m_bound_rvars.push_back(nlsat::var_vector()); s.m_bound_rvars.push_back(nlsat::var_vector());
max_level lvl; max_level lvl;
if (is_exists(i)) lvl.m_ex = i; else lvl.m_fa = i; if (is_exists(i)) lvl.m_ex = i; else lvl.m_fa = i;
for (app* v : qvars[i]) { for (app* v : qvars[i]) {
if (m_a2b.is_var(v)) { if (s.m_a2b.is_var(v)) {
SASSERT(m.is_bool(v)); SASSERT(m.is_bool(v));
nlsat::bool_var b = m_a2b.to_var(v); nlsat::bool_var b = s.m_a2b.to_var(v);
TRACE("qe", tout << mk_pp(v, m) << " |-> b" << b << "\n";); TRACE("qe", tout << mk_pp(v, m) << " |-> b" << b << "\n";);
m_bound_bvars.back().push_back(b); s.m_bound_bvars.back().push_back(b);
set_level(b, lvl); set_level(b, lvl);
} }
else if (m_t2x.is_var(v)) { else if (s.m_t2x.is_var(v)) {
nlsat::var w = m_t2x.to_var(v); nlsat::var w = s.m_t2x.to_var(v);
TRACE("qe", tout << mk_pp(v, m) << " |-> x" << w << "\n";); TRACE("qe", tout << mk_pp(v, m) << " |-> x" << w << "\n";);
m_bound_rvars.back().push_back(w); s.m_bound_rvars.back().push_back(w);
m_rvar2level.setx(w, lvl, max_level()); s.m_rvar2level.setx(w, lvl, max_level());
} }
else { else {
TRACE("qe", tout << mk_pp(v, m) << " not found\n";); TRACE("qe", tout << mk_pp(v, m) << " not found\n";);
} }
} }
} }
init_var2expr(); s.init_var2expr();
m_is_true = nlsat::literal(m_a2b.to_var(is_true), false); s.m_is_true = nlsat::literal(s.m_a2b.to_var(is_true), false);
// insert literals from arithmetical sub-formulas // insert literals from arithmetical sub-formulas
nlsat::atom_vector const& atoms = m_solver.get_atoms(); nlsat::atom_vector const& atoms = s.m_solver.get_atoms();
TRACE("qe", m_solver.display(tout);); TRACE("qe", s.m_solver.display(tout););
for (unsigned i = 0; i < atoms.size(); ++i) { for (unsigned i = 0; i < atoms.size(); ++i) {
if (atoms[i]) { if (atoms[i]) {
get_level(nlsat::literal(i, false)); get_level(nlsat::literal(i, false));
@ -701,32 +751,6 @@ namespace qe {
TRACE("qe", tout << fml << "\n";); TRACE("qe", tout << fml << "\n";);
} }
void init_expr2var(vector<app_ref_vector> const& qvars) {
for (app_ref_vector const& qvs : qvars) {
init_expr2var(qvs);
}
}
void init_expr2var(app_ref_vector const& qvars) {
for (app* v : qvars) {
if (m.is_bool(v)) {
m_a2b.insert(v, m_solver.mk_bool_var());
}
else {
// TODO: assert it is of type Real.
m_t2x.insert(v, m_solver.mk_var(false));
}
}
}
void init_var2expr() {
for (auto const& kv : m_t2x) {
m_x2t.insert(kv.m_value, kv.m_key);
}
for (auto const& kv : m_a2b) {
m_b2a.insert(kv.m_value, kv.m_key);
}
}
// Return false if nlsat assigned noninteger value to an integer variable. // Return false if nlsat assigned noninteger value to an integer variable.
@ -735,30 +759,30 @@ namespace qe {
bool ok = true; bool ok = true;
model_ref md = alloc(model, m); model_ref md = alloc(model, m);
arith_util util(m); arith_util util(m);
for (auto const& kv : m_t2x) { for (auto const& kv : s.m_t2x) {
nlsat::var x = kv.m_value; nlsat::var x = kv.m_value;
expr * t = kv.m_key; expr * t = kv.m_key;
if (!is_uninterp_const(t) || !m_free_vars.contains(t) || m_aux_vars.contains(t)) if (!is_uninterp_const(t) || !m_free_vars.contains(t) || m_aux_vars.contains(t))
continue; continue;
expr * v; expr * v;
try { try {
v = util.mk_numeral(m_rmodel0.value(x), util.is_int(t)); v = util.mk_numeral(s.m_rmodel0.value(x), util.is_int(t));
} }
catch (z3_error & ex) { catch (z3_error & ex) {
throw ex; throw ex;
} }
catch (z3_exception &) { catch (z3_exception &) {
v = util.mk_to_int(util.mk_numeral(m_rmodel0.value(x), false)); v = util.mk_to_int(util.mk_numeral(s.m_rmodel0.value(x), false));
ok = false; ok = false;
} }
md->register_decl(to_app(t)->get_decl(), v); md->register_decl(to_app(t)->get_decl(), v);
} }
for (auto const& kv : m_a2b) { for (auto const& kv : s.m_a2b) {
expr * a = kv.m_key; expr * a = kv.m_key;
nlsat::bool_var b = kv.m_value; nlsat::bool_var b = kv.m_value;
if (a == nullptr || !is_uninterp_const(a) || b == m_is_true.var() || !m_free_vars.contains(a) || m_aux_vars.contains(a)) if (a == nullptr || !is_uninterp_const(a) || b == s.m_is_true.var() || !m_free_vars.contains(a) || m_aux_vars.contains(a))
continue; continue;
lbool val = m_bmodel0.get(b, l_undef); lbool val = s.m_bmodel0.get(b, l_undef);
if (val == l_undef) if (val == l_undef)
continue; // don't care continue; // don't care
md->register_decl(to_app(a)->get_decl(), val == l_true ? m.mk_true() : m.mk_false()); md->register_decl(to_app(a)->get_decl(), val == l_true ? m.mk_true() : m.mk_false());
@ -770,21 +794,15 @@ namespace qe {
public: public:
nlqsat(ast_manager& m, qsat_mode_t mode, params_ref const& p): nlqsat(ast_manager& m, qsat_mode_t mode, params_ref const& p):
m(m), m(m),
s(m, p),
m_mode(mode), m_mode(mode),
m_params(p), m_params(p),
m_solver(m.limit(), p, true),
m_nftactic(nullptr), m_nftactic(nullptr),
m_rmodel(m_solver.am()),
m_rmodel0(m_solver.am()),
m_valid_model(false),
m_a2b(m),
m_t2x(m),
m_cancel(false),
m_answer(m), m_answer(m),
m_answer_simplify(m), m_answer_simplify(m),
m_trail(m) m_trail(m)
{ {
m_solver.get_explain().set_signed_project(true); s.m_solver.get_explain().set_signed_project(true);
m_nftactic = mk_tseitin_cnf_tactic(m); m_nftactic = mk_tseitin_cnf_tactic(m);
} }
@ -794,7 +812,7 @@ namespace qe {
void updt_params(params_ref const & p) override { void updt_params(params_ref const & p) override {
params_ref p2(p); params_ref p2(p);
p2.set_bool("factor", false); p2.set_bool("factor", false);
m_solver.updt_params(p2); s.m_solver.updt_params(p2);
} }
void collect_param_descrs(param_descrs & r) override { void collect_param_descrs(param_descrs & r) override {
@ -857,7 +875,7 @@ namespace qe {
void reset_statistics() override { void reset_statistics() override {
m_stats.reset(); m_stats.reset();
m_solver.reset_statistics(); s.m_solver.reset_statistics();
} }
void cleanup() override { void cleanup() override {

19
src/solver/combined_solver.cpp
View file

@ -61,25 +61,12 @@ private:
// This is relevant for big benchmarks that are meant to be solved // This is relevant for big benchmarks that are meant to be solved
// by a non-incremental solver. ); // by a non-incremental solver. );
bool m_solver2_initialized;
bool m_ignore_solver1; bool m_ignore_solver1;
inc_unknown_behavior m_inc_unknown_behavior; inc_unknown_behavior m_inc_unknown_behavior;
unsigned m_inc_timeout; unsigned m_inc_timeout;
void init_solver2_assertions() {
if (m_solver2_initialized)
return;
unsigned sz = m_solver1->get_num_assertions();
for (unsigned i = 0; i < sz; i++) {
m_solver2->assert_expr(m_solver1->get_assertion(i));
}
m_solver2_initialized = true;
}
void switch_inc_mode() { void switch_inc_mode() {
m_inc_mode = true; m_inc_mode = true;
init_solver2_assertions();
} }
struct aux_timeout_eh : public event_handler { struct aux_timeout_eh : public event_handler {
@ -131,7 +118,6 @@ public:
m_solver1 = s1; m_solver1 = s1;
m_solver2 = s2; m_solver2 = s2;
updt_local_params(p); updt_local_params(p);
m_solver2_initialized = false;
m_inc_mode = false; m_inc_mode = false;
m_check_sat_executed = false; m_check_sat_executed = false;
m_use_solver1_results = true; m_use_solver1_results = true;
@ -142,7 +128,6 @@ public:
solver* s1 = m_solver1->translate(m, p); solver* s1 = m_solver1->translate(m, p);
solver* s2 = m_solver2->translate(m, p); solver* s2 = m_solver2->translate(m, p);
combined_solver* r = alloc(combined_solver, s1, s2, p); combined_solver* r = alloc(combined_solver, s1, s2, p);
r->m_solver2_initialized = m_solver2_initialized;
r->m_inc_mode = m_inc_mode; r->m_inc_mode = m_inc_mode;
r->m_check_sat_executed = m_check_sat_executed; r->m_check_sat_executed = m_check_sat_executed;
r->m_use_solver1_results = m_use_solver1_results; r->m_use_solver1_results = m_use_solver1_results;
@ -171,15 +156,13 @@ public:
if (m_check_sat_executed) if (m_check_sat_executed)
switch_inc_mode(); switch_inc_mode();
m_solver1->assert_expr(t); m_solver1->assert_expr(t);
if (m_solver2_initialized) m_solver2->assert_expr(t);
m_solver2->assert_expr(t);
} }
void assert_expr_core2(expr * t, expr * a) override { void assert_expr_core2(expr * t, expr * a) override {
if (m_check_sat_executed) if (m_check_sat_executed)
switch_inc_mode(); switch_inc_mode();
m_solver1->assert_expr(t, a); m_solver1->assert_expr(t, a);
init_solver2_assertions();
m_solver2->assert_expr(t, a); m_solver2->assert_expr(t, a);
} }

8
src/util/params.cpp
View file

@ -20,6 +20,8 @@ Notes:
#include "util/rational.h" #include "util/rational.h"
#include "util/symbol.h" #include "util/symbol.h"
#include "util/dictionary.h" #include "util/dictionary.h"
#include <thread>
#include <atomic>
params_ref params_ref::g_empty_params_ref; params_ref params_ref::g_empty_params_ref;
@ -324,7 +326,7 @@ class params {
}; };
typedef std::pair<symbol, value> entry; typedef std::pair<symbol, value> entry;
svector<entry> m_entries; svector<entry> m_entries;
unsigned m_ref_count; std::atomic<unsigned> m_ref_count;
void del_value(entry & e); void del_value(entry & e);
void del_values(); void del_values();
@ -336,7 +338,9 @@ public:
void inc_ref() { m_ref_count++; } void inc_ref() { m_ref_count++; }
void dec_ref() { void dec_ref() {
SASSERT(m_ref_count > 0); SASSERT(m_ref_count > 0);
if (m_ref_count > 10000)
IF_VERBOSE(0, verbose_stream() << this << " " << m_ref_count << " " << std::this_thread::get_id() << "\n";);
if (--m_ref_count == 0) dealloc(this); if (--m_ref_count == 0) dealloc(this);
} }