mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-05 23:05:46 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-05-16 13:50:41 -07:00
parent eaca24ac01
commit 973a32a015
2 changed files with 74 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

41
src/math/polysat/linear_solver.cpp
View file

@ -13,6 +13,7 @@ Author:
--*/
#include "math/polysat/linear_solver.h"
#include "math/polysat/fixplex_def.h"
#include "math/polysat/solver.h"
namespace polysat {
@ -33,6 +34,13 @@ namespace polysat {
m_rows.pop_back();
break;
}
case trail_i::add_mono_i: {
auto m = m_monomials.back();
m_mono2var.erase(m);
m_alloc.deallocate(m.num_vars*sizeof(unsigned), m.vars);
m_monomials.pop_back();
break;
}
case trail_i::set_bound_i: {
auto [v, sz] = m_rows.back();
sz2fixplex(sz).restore_bound();
@ -105,11 +113,12 @@ namespace polysat {
auto& fp = sz2fixplex(sz);
m_trail.push_back(trail_i::set_bound_i);
m_rows.push_back(std::make_pair(v, sz));
rational z(0), o(1);
if (c.is_positive())
fp.set_bounds(v, rational::zero(), rational::zero());
fp.set_bounds(v, z, z);
else
fp.set_bounds(v, rational::one(), rational::power_of_two(sz) - 1);
}
fp.set_bounds(v, o, z);
}
void linear_solver::new_le(ule_constraint& c) {
var_t v = internalize_pdd(c.lhs());
@ -186,8 +195,17 @@ namespace polysat {
}
var_t linear_solver::mono2var(unsigned sz, unsigned_vector const& var) {
NOT_IMPLEMENTED_YET();
return 0;
mono_info m(sz, var.size(), var.data()), m1;
if (m_mono2var.find(m, m1))
return m1.var;
m.vars = static_cast<unsigned*>(m_alloc.allocate(var.size()*sizeof(unsigned)));
for (unsigned i = 0; i < var.size(); var.data())
m.vars[i] = var[i];
m.var = fresh_var(sz);
m_mono2var.insert(m);
m_monomials.push_back(m);
m_trail.push_back(trail_i::add_mono_i);
return m.var;
}
var_t linear_solver::pvar2var(unsigned sz, pvar v) {
@ -222,9 +240,20 @@ namespace polysat {
}
// check integer modular feasibility under current bounds.
// and inequalities
lbool linear_solver::check() {
lbool res = l_true;
// loop over fp solvers that have been touched and use make_feasible.
for (auto* f : m_fix) {
if (!f)
continue;
lbool r = f->make_feasible();
if (r == l_false) {
// m_unsat_f = f;
return r;
}
if (r == l_undef)
res = l_undef;
}
return res;
}