Skip to content

Commit e4f3b57

Browse files
committed
solving regressions/smt2/b1.smt2
1 parent 71c4339 commit e4f3b57

File tree

3 files changed

+91
-74
lines changed

3 files changed

+91
-74
lines changed

src/math/lp/dioph_eq.cpp

+86-69
Original file line numberDiff line numberDiff line change
@@ -238,7 +238,7 @@ namespace lp {
238238
unsigned m_max_number_of_iterations = 1000;
239239
unsigned m_number_of_iterations;
240240
struct branch {
241-
unsigned m_j;
241+
unsigned m_j = UINT_MAX;
242242
mpq m_rs;
243243
// if m_left is true, then the branch is interpreted
244244
// as x[j] <= m_rs
@@ -275,8 +275,6 @@ namespace lp {
275275

276276
std_vector<variable_branch_stats> m_branch_stats;
277277
std_vector<branch> m_branch_stack;
278-
std_vector<unsigned> m_added_fixed;
279-
std_vector<unsigned> m_added_fixed_sizes;
280278
std_vector<constraint_index> m_explanation_of_branches;
281279

282280
public:
@@ -712,7 +710,7 @@ namespace lp {
712710
}
713711
}
714712

715-
// returns true if there is a change in the bounds
713+
// returns true only on a conflict.
716714
// m_indexed_work_vector contains the coefficients of the term
717715
// m_c contains the constant term
718716
// m_tmp_l is the linear combination of the equations that removs the
@@ -737,6 +735,7 @@ namespace lp {
737735
return false;
738736
}
739737

738+
// returns true only on a conflict
740739
bool tighten_bound_kind(const mpq& g, unsigned j, const mpq& ub, bool upper,
741740
u_dependency* prev_dep) {
742741
// ub = (upper_bound(j) - m_c)/g.
@@ -768,12 +767,12 @@ namespace lp {
768767
print_lar_term_L(lra.get_term(j), tout) << "\ndep:";
769768
print_dep(tout, dep) << std::endl;);
770769
lra.update_column_type_and_bound(j, kind, bound, dep);
771-
int st = (int)lra.find_feasible_solution();
772-
if (st >= (int)lp::lp_status::FEASIBLE) {
773-
lra.get_infeasibility_explanation(m_infeas_explanation);
774-
return true;
770+
lp_status st = lra.find_feasible_solution();
771+
if ((int)st >= (int)lp::lp_status::FEASIBLE) {
772+
return false;
775773
}
776-
return false;
774+
lra.get_infeasibility_explanation(m_infeas_explanation);
775+
return true;
777776
}
778777

779778
u_dependency* explain_fixed_in_meta_term(const lar_term& t) {
@@ -844,31 +843,22 @@ namespace lp {
844843
m_explanation_of_branches.push_back(p.ci());
845844
}
846845
}
847-
848-
void undo_fixed(unsigned j) {
849-
NOT_IMPLEMENTED_YET();
850-
}
851-
852-
void undo_last_branch() {
846+
847+
// returns true if the left and the right branches were explored
848+
bool undo_last_branch() {
853849
unsigned h = m_branch_stack.size() - 1;
854-
unsigned n_of_fixed_before = m_added_fixed_sizes[h];
855-
while (m_added_fixed.size() > n_of_fixed_before) {
856-
unsigned j = m_added_fixed.back();
857-
m_added_fixed.pop_back();
858-
undo_fixed(j);
859-
}
860850
if (m_branch_stack.back().m_fully_explored) {
861-
TRACE("dio_br", tout << "pop fully explored" << std::endl;);
851+
TRACE("dio_br", tout << "pop fully explored, m_branch_stack.size():" << m_branch_stack.size() << std::endl;);
862852
m_branch_stack.pop_back();
863-
m_added_fixed_sizes.pop_back();
864-
NOT_IMPLEMENTED_YET();
865-
} else { // exploring the other side of the branch
866-
TRACE("dio_br", tout << "flipped branch" << std::endl;);
867-
m_branch_stack.back().flip();
868-
}
853+
return true;
854+
}
855+
// exploring the other side of the branch
856+
TRACE("dio_br", tout << "flipped branch" << std::endl;);
857+
m_branch_stack.back().flip();
858+
return false;
869859
}
870860

871-
lia_move check_fixing(unsigned j) {
861+
lia_move check_fixing(unsigned j) const {
872862
// do not change entry here
873863
unsigned ei = m_k2s[j]; // entry index
874864
mpq g = mpq(0); // gcd
@@ -889,35 +879,42 @@ namespace lp {
889879
if (g.is_one()) return lia_move::undef;
890880
}
891881
if (!(c/g).is_int()) {
892-
m_conflict_index = ei;
893882
return lia_move::conflict;
894883
}
895884
return lia_move::undef;
896885
}
897886
// here j is a local variable
898887
lia_move fix_var(unsigned j) {
899888
SASSERT(is_fixed(local_to_lar_solver(j)));
900-
m_added_fixed.push_back(j);
901889
/*
902-
The only conflict we can get it is when j is substituted, and the entry m_k2s[j], the entry defining the substitution
903-
becomes infeaseable, that is the gcd of the monomial coeffitients does not dived the free coefficients.
890+
We only can get a conflict when j is substituted, and the entry m_k2s[j], the entry defining the substitution becomes infeaseable, that is the gcd of the monomial coeffitients does not dive the free coefficient. In other cases the gcd of the monomials will remain to be 1.
904891
*/
905892
if (can_substitute(j)) {
906893
TRACE("dio_br",
907894
tout << "fixed j:" << j <<", was substited by "; print_entry(m_k2s[j], tout););
908-
if (check_fixing(j) == lia_move::conflict)
895+
if (check_fixing(j) == lia_move::conflict) {
896+
m_conflict_index = m_k2s[j];
909897
return lia_move::conflict;
898+
}
910899
}
911-
NOT_IMPLEMENTED_YET();
900+
return lia_move::undef;
912901
}
913902

914903
void undo_branching() {
915-
NOT_IMPLEMENTED_YET();
904+
while (m_lra_level --) {
905+
lra.pop();
906+
}
907+
lra.find_feasible_solution();
908+
SASSERT(lra.is_feasible());
916909
}
917-
918-
void push_branch() {
919-
m_branch_stack.push_back(create_branch());
920-
m_added_fixed_sizes.push_back(m_added_fixed.size());
910+
// Returns true if a branch is created, and false if not.
911+
// The latter case can happen if we have a sat.
912+
bool push_branch() {
913+
branch br = create_branch();
914+
if (br.m_j == UINT_MAX)
915+
return false;
916+
m_branch_stack.push_back(br);
917+
return true;
921918
}
922919

923920
lia_move add_var_bound_for_branch(const branch* b) {
@@ -933,31 +930,46 @@ namespace lp {
933930
return lia_move::undef;
934931
}
935932

936-
unsigned n_deb_lra_level = 0;
933+
unsigned m_lra_level = 0;
937934
void lra_push() {
938-
n_deb_lra_level++;
935+
m_lra_level++;
939936
lra.push();
940-
SASSERT(n_deb_lra_level == m_branch_stack.size());
937+
SASSERT(m_lra_level == m_branch_stack.size());
941938
}
942939
void lra_pop() {
943-
n_deb_lra_level--;
940+
m_lra_level--;
944941
lra.pop();
942+
lra.find_feasible_solution();
943+
SASSERT(lra.is_feasible());
945944
}
946945

947946
lia_move process_undef() {
948947
m_explanation_of_branches.clear();
949948
branch* b;
950949
bool need_create_branch = true;
951-
while (true) {
950+
m_number_of_iterations = 0;
951+
while (++m_number_of_iterations < m_max_number_of_iterations) {
952952
if (need_create_branch) {
953-
push_branch();
953+
if (!push_branch()) {
954+
undo_branching();
955+
return lia_move::sat;
956+
}
954957
need_create_branch = false;
955958
b = &m_branch_stack.back();
956959
}
957960
lra_push(); // exploring a new branch
958961

959-
if (add_var_bound_for_branch(b) == lia_move::conflict)
960-
return lia_move::conflict;
962+
if (add_var_bound_for_branch(b) == lia_move::conflict) {
963+
collect_evidence();
964+
if (m_branch_stack.size() == 0)
965+
return lia_move::conflict;
966+
TRACE("dio_br", tout << lp_status_to_string(lra.get_status()) << std::endl;
967+
tout << "explanation:\n"; lra.print_expl(tout, m_infeas_explanation););
968+
if (undo_last_branch())
969+
need_create_branch = true;
970+
lra_pop();
971+
continue;
972+
}
961973
int st = static_cast<int>(lra.find_feasible_solution());
962974
if (st >= static_cast<int>(lp_status::FEASIBLE)) {
963975
// have a feasible solution
@@ -976,10 +988,12 @@ namespace lp {
976988
return lia_move::conflict;
977989
TRACE("dio_br", tout << lp_status_to_string(lra.get_status()) << std::endl;
978990
tout << "explanation:\n"; lra.print_expl(tout, m_infeas_explanation););
979-
undo_last_branch();
991+
if (undo_last_branch())
992+
need_create_branch = true;
980993
lra_pop();
981994
}
982995
}
996+
undo_branching();
983997
return lia_move::undef;
984998
}
985999

@@ -1011,7 +1025,7 @@ namespace lp {
10111025
}
10121026

10131027
branch create_branch() {
1014-
unsigned bj;
1028+
unsigned bj = UINT_MAX;
10151029
double score = std::numeric_limits<double>::infinity();
10161030
// looking for the minimal score
10171031
unsigned n = 0;
@@ -1026,6 +1040,19 @@ namespace lp {
10261040
}
10271041
}
10281042
branch br;
1043+
if (bj == UINT_MAX) { // it a the case when we cannot create a branch
1044+
SASSERT(lra.is_feasible() &&
1045+
[&]() {
1046+
for (unsigned j = 0; j < lra.column_count(); ++j) {
1047+
if (lia.column_is_int_inf(j)) {
1048+
return false;
1049+
}
1050+
}
1051+
return true;
1052+
}());
1053+
return br; // to signal that we have no ii variables
1054+
}
1055+
10291056
br.m_j = bj;
10301057
br.m_left = (lra.settings().random_next() % 2 == 0);
10311058
br.m_rs = floor(lra.get_column_value(bj).x);
@@ -1037,26 +1064,16 @@ namespace lp {
10371064

10381065
public:
10391066
lia_move check() {
1067+
lra.settings().stats().m_dio_calls++;
10401068
init();
1041-
lia_move ret;
1042-
while (m_number_of_iterations++ < m_max_number_of_iterations) {
1043-
ret = iterate();
1044-
// decide on ret
1045-
if (ret == lia_move::branch) {
1046-
process_branch();
1047-
} else if (ret == lia_move::conflict) {
1048-
process_conflict();
1049-
if (decide_on_conflict())
1050-
return lia_move::conflict;
1051-
} else {
1052-
SASSERT(ret == lia_move::undef);
1053-
ret = process_undef();
1054-
if (ret == lia_move::sat)
1055-
return ret;
1056-
if (ret == lia_move::conflict)
1057-
return ret;
1058-
}
1059-
}
1069+
lia_move ret = iterate();
1070+
if (ret == lia_move::branch || ret == lia_move::conflict)
1071+
return ret;
1072+
SASSERT(ret == lia_move::undef);
1073+
ret = process_undef();
1074+
if (ret == lia_move::sat || ret == lia_move::conflict)
1075+
return ret;
1076+
SASSERT(ret == lia_move::undef);
10601077
return lia_move::undef;
10611078
}
10621079

src/math/lp/int_solver.cpp

+2-4
Original file line numberDiff line numberDiff line change
@@ -179,10 +179,8 @@ namespace lp {
179179
} else if (r == lia_move::branch) {
180180
m_dioph_eq_period = settings().m_dioph_eq_period;
181181
return lia_move::branch;
182-
}
183-
184-
// m_dioph_eq_period *= 2;
185-
return lia_move::undef;
182+
}
183+
return r;
186184
}
187185

188186
lp_settings& settings() { return lra.settings(); }

src/math/lp/lp_settings.h

+3-1
Original file line numberDiff line numberDiff line change
@@ -129,6 +129,7 @@ struct statistics {
129129
unsigned m_offset_eqs = 0;
130130
unsigned m_fixed_eqs = 0;
131131
unsigned m_dio_conflicts = 0;
132+
unsigned m_dio_calls = 0;
132133
::statistics m_st = {};
133134

134135
void reset() {
@@ -161,7 +162,8 @@ struct statistics {
161162
st.update("arith-nla-lemmas", m_nla_lemmas);
162163
st.update("arith-nra-calls", m_nra_calls);
163164
st.update("arith-bounds-improvements", m_nla_bounds_improvements);
164-
st.update("arith-lp-dio-conflicts", m_dio_conflicts);
165+
st.update("arith-dio-calls", m_dio_calls);
166+
st.update("arith-dio-conflicts", m_dio_conflicts);
165167
st.copy(m_st);
166168
}
167169
};

0 commit comments

Comments
 (0)