2020-06-22 13:23:41 (GMT)
The lia_generic rule is issued when the solver is in integer solving mode. In this case it also does branch and bound. I haven't thought this through, but I guess the inequalities + coefficients is probably not enough in this case. One might need the bounds too?
2020-06-22 13:30:18 (GMT)
if you have the coefficients, I would reconstruct it directly, so it would be cool to have it.
2020-06-22 13:30:34 (GMT)
But why would coefficients not be enough? Because of the rounding?
2020-06-22 13:41:0 (GMT)
well we know that coefficients are complete because of the Farkas' lemma, but that only holds for reals. I tried to search for equivalents for integers, but there are not really usable ones. I think normal coefficients + rounding is not enough: if one has an inequality with more than one variable one does not know which one to round.
2020-06-22 13:41:28 (GMT)
that said: I think I can print the coefficients, that might help. I could also print the bounds.
2020-06-22 14:52:49 (GMT)
the question is more: are coefficients enough for what veriT does internally and can they be easily computed?
2020-06-22 14:55:29 (GMT)
can you give me an example problem that results in such a step? I want to check how the result looks like/see what the code does.
2020-06-22 15:8:43 (GMT)
SMT: Problem:
; --proof-with-sharing --index-fresh-sorts --proof-define-skolems --proof-prune --proof-merge --disable-print-success --disable-banner --max-time=20
(set-option :produce-proofs true)
(set-logic AUFLIA)
(declare-sort Nat$ 0)
(declare-fun x$ () Nat$)
(declare-fun of_nat$ (Nat$) Int)
(assert (! (not (not (= (* 2 (of_nat$ x$)) 1))) :named a0))
(assert (! (<= 0 (of_nat$ x$)) :named a1))
(check-sat)
(get-proof)
2020-06-22 17:34:17 (GMT)
which actually proves that coefficients are not enough:
(step t2 (cl (not (= 1 (* 2 (of_nat$ x$))))) :rule lia_generic)
2020-06-22 19:29:36 (GMT)
yeah -.- the code that does the reasoning is actually relative straightforward. let me try to write some pseudocode.
2020-06-22 19:47:10 (GMT)
integer_reason(unsigned level) {
if level == max_level:
return UNKNOWN
if simplex_solve() == UNSAT:
return UNSAT
if an integer variable has a non integer value assigned:
pick one such variable x_i according to some score
y_i = current value assigned to x_i
add backtrack point u_level
assert x_i < ⌊y_i⌋ and update simplex
r = integer_reason(level + 1)
backtrack to u_level
if r != UNSAT:
return r
add backtrack point u_level
assert x_i > ⌈y_i⌉ and update simplex
r = integer_reason(level + 1)
backtrack to u_level
return r
}
2020-06-22 20:0:3 (GMT)
this might be wrong regarding y_i though, this part is odd