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

tweaking nlqsat

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-09-05 09:55:25 +03:00
parent 5fbfc0f9f7
commit 29f0897afc
3 changed files with 27 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/nlsat/nlsat_solver.cpp
View file

@ -507,6 +507,7 @@ namespace nlsat {
m_num_bool_vars--; m_num_bool_vars--;
m_dead[b] = true; m_dead[b] = true;
m_atoms[b] = nullptr; m_atoms[b] = nullptr;
m_bvalues[b] = l_undef;
m_bid_gen.recycle(b); m_bid_gen.recycle(b);
} }
@ -3109,7 +3110,8 @@ namespace nlsat {
std::ostream& display(std::ostream & out) const { std::ostream& display(std::ostream & out) const {
display(out, m_display_var); display(out, m_display_var);
return display_assignment(out); display_assignment(out << "assignment:\n");
return out << "---\n";
} }
std::ostream& display_vars(std::ostream & out) const { std::ostream& display_vars(std::ostream & out) const {
@ -3263,15 +3265,12 @@ namespace nlsat {
as.copy(m_imp->m_assignment); as.copy(m_imp->m_assignment);
} }
void solver::get_bvalues(svector<lbool>& vs) { void solver::get_bvalues(svector<bool_var> const& bvars, svector<lbool>& vs) {
vs.reset(); vs.reset();
unsigned sz = m_imp->m_bvalues.size(); for (bool_var b : bvars) {
for (bool_var b = 0; b < sz; ++b) { vs.reserve(b + 1, l_undef);
if (m_imp->m_atoms[b] == nullptr) { if (!m_imp->m_atoms[b]) {
vs.push_back(m_imp->m_bvalues[b]); vs[b] = m_imp->m_bvalues[b];
}
else {
vs.push_back(l_undef); // don't save values from atoms.
} }
} }
TRACE("nlsat", display(tout);); TRACE("nlsat", display(tout););
@ -3279,15 +3278,24 @@ namespace nlsat {
void solver::set_bvalues(svector<lbool> const& vs) { void solver::set_bvalues(svector<lbool> const& vs) {
TRACE("nlsat", display(tout);); TRACE("nlsat", display(tout););
for (bool_var b = 0; b < vs.size(); ++b) {
if (vs[b] != l_undef) {
m_imp->m_bvalues[b] = vs[b];
SASSERT(!m_imp->m_atoms[b]);
}
}
#if 0
m_imp->m_bvalues.reset(); m_imp->m_bvalues.reset();
m_imp->m_bvalues.append(vs); m_imp->m_bvalues.append(vs);
m_imp->m_bvalues.resize(m_imp->m_atoms.size(), l_undef); m_imp->m_bvalues.resize(m_imp->m_atoms.size(), l_undef);
for (unsigned i = 0; i < m_imp->m_atoms.size(); ++i) { for (unsigned i = 0; i < m_imp->m_atoms.size(); ++i) {
atom* a = m_imp->m_atoms[i]; atom* a = m_imp->m_atoms[i];
SASSERT(!a);
if (a) { if (a) {
m_imp->m_bvalues[i] = to_lbool(m_imp->m_evaluator.eval(a, false)); m_imp->m_bvalues[i] = to_lbool(m_imp->m_evaluator.eval(a, false));
} }
} }
#endif
TRACE("nlsat", display(tout);); TRACE("nlsat", display(tout););
} }

2
src/nlsat/nlsat_solver.h
View file

@ -166,7 +166,7 @@ namespace nlsat {
void get_rvalues(assignment& as); void get_rvalues(assignment& as);
void set_rvalues(assignment const& as); void set_rvalues(assignment const& as);
void get_bvalues(svector<lbool>& vs); void get_bvalues(svector<bool_var> const& bvars, svector<lbool>& vs);
void set_bvalues(svector<lbool> const& vs); void set_bvalues(svector<lbool> const& vs);
/** /**

11
src/qe/nlqsat.cpp
View file

@ -102,7 +102,9 @@ namespace qe {
void init_expr2var(app_ref_vector const& qvars) { void init_expr2var(app_ref_vector const& qvars) {
for (app* v : qvars) { for (app* v : qvars) {
if (m.is_bool(v)) { if (m.is_bool(v)) {
m_a2b.insert(v, m_solver.mk_bool_var()); nlsat::bool_var b = m_solver.mk_bool_var();
m_solver.inc_ref(b);
m_a2b.insert(v, b);
} }
else { else {
// TODO: assert it is of type Real. // TODO: assert it is of type Real.
@ -121,8 +123,12 @@ namespace qe {
} }
void save_model(bool is_exists) { void save_model(bool is_exists) {
svector<nlsat::bool_var> bvars;
for (auto const& kv : m_bvar2level) {
bvars.push_back(kv.m_key);
}
m_solver.get_rvalues(m_rmodel); m_solver.get_rvalues(m_rmodel);
m_solver.get_bvalues(m_bmodel); m_solver.get_bvalues(bvars, m_bmodel);
m_valid_model = true; m_valid_model = true;
if (is_exists) { if (is_exists) {
m_rmodel0.copy(m_rmodel); m_rmodel0.copy(m_rmodel);
@ -311,6 +317,7 @@ namespace qe {
} }
} }
TRACE("qe", s.display(tout); TRACE("qe", s.display(tout);
tout << "assumptions\n";
for (nlsat::literal a : s.m_asms) { for (nlsat::literal a : s.m_asms) {
s.m_solver.display(tout, a) << "\n"; s.m_solver.display(tout, a) << "\n";
}); });