mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

fix #4552

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-30 19:14:49 -07:00
parent fce1252145
commit d75ce38016
3 changed files with 13 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/nlsat/nlsat_solver.cpp
View file

@ -1546,9 +1546,8 @@ namespace nlsat {
lbool r = l_undef; lbool r = l_undef;
while (true) { while (true) {
r = search(); r = search();
if (r != l_true) break; if (r != l_true) break;
vector<rational> lows; vector<std::pair<var, rational>> bounds;
vector<var> vars;
for (var x = 0; x < num_vars(); x++) { for (var x = 0; x < num_vars(); x++) {
if (m_is_int[x] && m_assignment.is_assigned(x) && !m_am.is_int(m_assignment.value(x))) { if (m_is_int[x] && m_assignment.is_assigned(x) && !m_am.is_int(m_assignment.value(x))) {
@ -1556,24 +1555,24 @@ namespace nlsat {
v = m_assignment.value(x); v = m_assignment.value(x);
rational lo; rational lo;
m_am.int_lt(v, vlo); m_am.int_lt(v, vlo);
if (!m_am.is_int(vlo)) continue; if (!m_am.is_int(vlo))
continue;
m_am.to_rational(vlo, lo); m_am.to_rational(vlo, lo);
// derive tight bounds. // derive tight bounds.
while (true) { while (true) {
lo++; lo++;
if (!m_am.gt(v, lo.to_mpq())) { lo--; break; } if (!m_am.gt(v, lo.to_mpq())) { lo--; break; }
} }
lows.push_back(lo); bounds.push_back(std::make_pair(x, lo));
vars.push_back(x);
} }
} }
if (lows.empty()) break; if (bounds.empty()) break;
init_search(); init_search();
for (unsigned i = 0; i < lows.size(); ++i) { for (auto const& b : bounds) {
rational lo = lows[i]; var x = b.first;
rational hi = lo + rational::one(); rational lo = b.second;
var x = vars[i]; rational hi = lo + 1; // rational::one();
bool is_even = false; bool is_even = false;
polynomial_ref p(m_pm); polynomial_ref p(m_pm);
rational one(1); rational one(1);

3
src/shell/dimacs_frontend.cpp
View file

@ -225,6 +225,7 @@ unsigned read_dimacs(char const * file_name) {
params_ref p = gparams::get_module("sat"); params_ref p = gparams::get_module("sat");
params_ref par = gparams::get_module("parallel"); params_ref par = gparams::get_module("parallel");
p.set_bool("produce_models", true); p.set_bool("produce_models", true);
p.set_bool("cardinality.solver", false);
sat_params sp(p); sat_params sp(p);
reslimit limit; reslimit limit;
sat::solver solver(p, limit); sat::solver solver(p, limit);
@ -248,7 +249,7 @@ unsigned read_dimacs(char const * file_name) {
params_ref p2; params_ref p2;
p2.copy(p); p2.copy(p);
p2.set_sym("drat.file", symbol::null); p2.set_sym("drat.file", symbol::null);
sat::solver solver2(p2, limit); sat::solver solver2(p2, limit);
if (p.get_bool("dimacs.core", false)) { if (p.get_bool("dimacs.core", false)) {
g_solver = &solver2; g_solver = &solver2;

1
src/smt/diff_logic.h
View file

@ -511,6 +511,7 @@ public:
// Return false if the resultant graph has a negative cycle. The negative // Return false if the resultant graph has a negative cycle. The negative
// cycle can be extracted using traverse_neg_cycle. // cycle can be extracted using traverse_neg_cycle.
// The method assumes the graph is feasible before the invocation. // The method assumes the graph is feasible before the invocation.
bool enable_edge(edge_id id) { bool enable_edge(edge_id id) {
edge& e = m_edges[id]; edge& e = m_edges[id];
SASSERT(is_feasible_dbg()); SASSERT(is_feasible_dbg());