OCamlPro
Better handling of Unsat and Unknown in solver.ml
In particular, reaching Unsat is possible if someones does owi_assume(false) and then calls owi_assert(false). We should try to display something better.
Whereas failing on `Unknown is still OK for now, as it never happened as of today.
In particular, reaching Unsat is possible if someones does owi_assume(false) and then calls owi_assert(false). We should try to display something better.
I don't understand this, if I do owi_assume(false) in a certain branch I would expect it to not follow that path any more and continue exploring another one, never even reaching the owi_assert(false).
Is there a particular example you have with this?
Yes, I wrote owi_assume(false) to simplify. But here the idea was that @S41d was doing some solver-aided programming and added something that was actually unsat. I maybe was not unsat directly with a single owi_assume but rather was after a combination of many.
We could check the satisfiability on each owi_assume but it may slow down things?
@S41d can probably give you the full example he had.
Yes, I wrote owi_assume(false) to simplify. But here the idea was that @S41d was doing some solver-aided programming and added something that was actually unsat. I maybe was not unsat directly with a single owi_assume but rather was after a combination of many.
Ahhh, I understand it now! This was exactly why we used to call the solver for assume in WASP. Sometimes people would add unsatisfiable assumptions so we wanted to terminate early.
We could check the satisfiability on each owi_assume but it may slow down things?
It depends, it might slow some benchmarks down but it might help speed things in this case. I wouldn't oppose to doing it like this as it would be more precise. It might also help to have an outcome for an assumption that isn't concrete and doesn't hold?
For reference, here's the file that I was trying to run:
#include "owi.h"
#include <stdbool.h>
#define VERTICES 9
#define VERTEX_EDGES 4
#define ADJ_NEIGHBORS 1
#define NADJ_NEIGHBORS 2
int common_neighbor_count(bool m[VERTICES][VERTICES], int x, int y) {
bool *xs = m[x];
bool *ys = m[y];
int count = 0;
for (int i = 0; i < VERTICES; i++) {
for (int j = 0; j < VERTICES; j++) {
if (xs[i] == ys[j])
count++;
}
}
return count;
}
int main() {
bool m[VERTICES][VERTICES] = {0};
for (int i = 0; i < VERTICES / 2; i++) {
m[i][i] = 0;
for (int j = i + 1; j < VERTICES; j++) {
// mettre un boolean 0 ou 1
bool c = owi_i8();
m[i][j] = c;
m[j][i] = c;
}
}
for (int i = 0; i < VERTICES; i++) {
int neighbor_count = 0;
for (int j = 0; j < VERTICES; j++) {
if (i == j)
continue;
neighbor_count += m[i][j];
}
owi_assume(neighbor_count == VERTEX_EDGES);
}
for (int i = 0; i < VERTICES; i++) {
for (int j = 0; j < VERTICES; j++) {
if (m[i][j]) { // adj
owi_assume(common_neighbor_count(m, i, j) == ADJ_NEIGHBORS);
} else {
owi_assume(common_neighbor_count(m, i, j) == NADJ_NEIGHBORS);
}
}
}
owi_assert(false);
return 0;
}