mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 16:33:18 +00:00
Code Activity

Remove unused method

Browse source
This commit is contained in:
Jakob Rath 2023-12-01 15:51:53 +01:00
parent 6ce63154d2
commit 02ff7efe25
2 changed files with 0 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/math/polysat/viable_fallback.cpp
View file

@ -89,30 +89,6 @@ namespace polysat {
return us; return us;
} }
find_t viable_fallback::find_viable(pvar v, rational& out_val) {
unsigned const bit_width = s.m_size[v];
univariate_solver* us = usolver(bit_width);
auto const& cs = m_constraints[v];
for (unsigned i = cs.size(); i-- > 0; ) {
signed_constraint const c = cs[i];
LOG("Univariate constraint: " << c);
c.add_to_univariate_solver(v, s, *us, c.blit().to_uint());
}
switch (us->check()) {
case l_true:
out_val = us->model();
// we don't know whether the SMT instance has a unique solution
return find_t::multiple;
case l_false:
s.set_conflict_by_viable_fallback(v, *us);
return find_t::empty;
default:
return find_t::resource_out;
}
}
std::ostream& operator<<(std::ostream& out, find_t x) { std::ostream& operator<<(std::ostream& out, find_t x) {
switch (x) { switch (x) {
case find_t::empty: case find_t::empty:

2
src/math/polysat/viable_fallback.h
View file

@ -45,8 +45,6 @@ namespace polysat {
// or find an arbitrary violated constraint. // or find an arbitrary violated constraint.
bool check_constraints(assignment const& a, pvar v) { return !find_violated_constraint(a, v); } bool check_constraints(assignment const& a, pvar v) { return !find_violated_constraint(a, v); }
signed_constraint find_violated_constraint(assignment const& a, pvar v); signed_constraint find_violated_constraint(assignment const& a, pvar v);
find_t find_viable(pvar v, rational& out_val);
}; };
} }