2020-05-20 7:49:2 (GMT)
(verit-rmx only, latest veriT works)
On the following file:
(set-option :produce-proofs true)
(set-logic AUFLIA)
(assert (! (not (< 0 (ite (forall ((?v0 Int)) (or (< ?v0 0) (< 0 ?v0))) (- 1) 3))) :named a0))
(check-sat)
(get-proof)
I get the answer
$ ./veriT /tmp/veriT_sort.smt2
veriT-rmx (5fe72ca) - the SMT-solver veriT (UFRN/LORIA).
success
success
success
error : DAG_new: unable to determine sort
Expected behaviour (like normal veriT):
$ ./veriT /tmp/veriT_sort.smt2
veriT (smtcomp19-23-gb9da6ca4-changed) - the SMT-solver veriT (UFRN/LORIA).
success
success
success
unsat
success
[proof skipped]
2020-05-20 7:59:39 (GMT)
This seems be because of the constants, but I don't want to add a dummy constant per number (like replacing 0 by a and adding the assumption a = 0)
2020-05-20 12:3:29 (GMT)
This is related to the new coefficient collection code.
2020-05-20 12:6:49 (GMT)
It's because I try to create a rational DAG, but LIA has no rational numbers. I will check what I can do.
2020-05-20 12:7:23 (GMT)
Note that if you change the logic to AUFLIRA it works.
2020-05-20 13:1:10 (GMT)
Can you try again?
2020-05-20 13:4:37 (GMT)
works now (and I get a proof I cannot replay ;-))
2020-06-15 15:26:56 (GMT)
Another typing problem:
MT: Assertions:
∄u::int.
∀(x::int) y::real.
(0::int) < x ∧ (0::real) < y ⟶
- (1::int)
< x
SMT: Names:
sorts:
functions:
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 AUFLIRA)
(assert (! (not (exists ((?v0 Int)) (forall ((?v1 Int) (?v2 Real)) (=> (and (< 0 ?v1) (< 0.0 ?v2)) (< (- 1) ?v1))))) :named a0))
(check-sat)
(get-proof)
SMT: Invoking SMT solver "verit" ...
SMT: Solver:
SMT: Result:
unsat
(define-fun veriT_sk0 () Int (! (choice ((veriT_vr2 Int)) (not (forall ((veriT_vr3 Real)) (! (=> (! (and (! (< 0 veriT_vr2) :named @p_26) (! (< 0.0 veriT_vr3) :named @p_27)) :named @p_28) (! (< (- 1) veriT_vr2) :named @p_30)) :named @p_31)))) :named @p_48))
(define-fun veriT_sk1 () Real (choice ((veriT_vr3 Real)) (not (=> (and (< 0 @p_48) @p_27) (< (- 1) @p_48)))))
(assume a0 (! (not (! (exists ((?v0 Int)) (! (forall ((?v1 Int) (?v2 Real)) (! (=> (! (and (! (< 0 ?v1) :named @p_7) (! (< 0.0 ?v2) :named @p_9)) :named @p_11) (! (< (! (- 1) :named @p_6) ?v1) :named @p_14)) :named @p_16)) :named @p_2)) :named @p_1)) :named @p_3))
(step t2 (cl (= @p_1 @p_2)) :rule qnt_rm_unused)
(step t3 (cl (! (= @p_3 (! (not @p_2) :named @p_5)) :named @p_4)) :rule cong :premises (t2))
(step t4 (cl (not @p_4) @p_1 @p_5) :rule equiv_pos2)
(step t5 (cl @p_5) :rule th_resolution :premises (a0 t3 t4))
(anchor :step t6 :args ((:= ?v1 veriT_vr0) (:= ?v2 veriT_vr1)))
(step t6.t1 (cl (! (= ?v1 veriT_vr0) :named @p_13)) :rule refl)
(step t6.t2 (cl (= @p_7 (! (< 0 veriT_vr0) :named @p_8))) :rule cong :premises (t6.t1))
(step t6.t3 (cl (= ?v2 veriT_vr1)) :rule refl)
(step t6.t4 (cl (= @p_9 (! (< 0.0 veriT_vr1) :named @p_10))) :rule cong :premises (t6.t3))
(step t6.t5 (cl (= @p_11 (! (and @p_8 @p_10) :named @p_12))) :rule cong :premises (t6.t2 t6.t4))
(step t6.t6 (cl @p_13) :rule refl)
(step t6.t7 (cl (= @p_14 (! (< @p_6 veriT_vr0) :named @p_15))) :rule cong :premises (t6.t6))
(step t6.t8 (cl (= @p_16 (! (=> @p_12 @p_15) :named @p_17))) :rule cong :premises (t6.t5 t6.t7))
(step t6 (cl (= @p_2 (! (forall ((veriT_vr0 Int) (veriT_vr1 Real)) @p_17) :named @p_18))) :rule bind)
(step t7 (cl (! (= @p_5 (! (not @p_18) :named @p_20)) :named @p_19)) :rule cong :premises (t6))
(step t8 (cl (not @p_19) @p_2 @p_20) :rule equiv_pos2)
(step t9 (cl @p_20) :rule th_resolution :premises (t5 t7 t8))
(anchor :step t10 :args (veriT_vr0 veriT_vr1))
(step t10.t1 (cl (= @p_6 (- 1))) :rule minus_simplify)
(step t10.t2 (cl (= @p_15 (! (< (- 1) veriT_vr0) :named @p_21))) :rule cong :premises (t10.t1))
(step t10.t3 (cl (= @p_17 (! (=> @p_12 @p_21) :named @p_22))) :rule cong :premises (t10.t2))
(step t10 (cl (= @p_18 (! (forall ((veriT_vr0 Int) (veriT_vr1 Real)) @p_22) :named @p_23))) :rule bind)
(step t11 (cl (! (= @p_20 (! (not @p_23) :named @p_25)) :named @p_24)) :rule cong :premises (t10))
(step t12 (cl (not @p_24) @p_18 @p_25) :rule equiv_pos2)
(step t13 (cl @p_25) :rule th_resolution :premises (t9 t11 t12))
(anchor :step t14 :args ((:= veriT_vr0 veriT_vr2) (:= veriT_vr1 veriT_vr3)))
(step t14.t1 (cl (! (= veriT_vr0 veriT_vr2) :named @p_29)) :rule refl)
(step t14.t2 (cl (= @p_8 @p_26)) :rule cong :premises (t14.t1))
(step t14.t3 (cl (= veriT_vr1 veriT_vr3)) :rule refl)
(step t14.t4 (cl (= @p_10 @p_27)) :rule cong :premises (t14.t3))
(step t14.t5 (cl (= @p_12 @p_28)) :rule cong :premises (t14.t2 t14.t4))
(step t14.t6 (cl @p_29) :rule refl)
(step t14.t7 (cl (= @p_21 @p_30)) :rule cong :premises (t14.t6))
(step t14.t8 (cl (= @p_22 @p_31)) :rule cong :premises (t14.t5 t14.t7))
(step t14 (cl (= @p_23 (! (forall ((veriT_vr2 Int) (veriT_vr3 Real)) @p_31) :named @p_32))) :rule bind)
(step t15 (cl (! (= @p_25 (! (not @p_32) :named @p_34)) :named @p_33)) :rule cong :premises (t14))
(step t16 (cl (not @p_33) @p_23 @p_34) :rule equiv_pos2)
(step t17 (cl @p_34) :rule th_resolution :premises (t13 t15 t16))
(anchor :step t18 :args ((:= veriT_vr2 veriT_sk0) (:= veriT_vr3 veriT_sk1)))
(step t18.t1 (cl (! (= veriT_vr2 veriT_sk0) :named @p_38)) :rule refl)
(step t18.t2 (cl (= @p_26 (! (< 0 veriT_sk0) :named @p_35))) :rule cong :premises (t18.t1))
(step t18.t3 (cl (= veriT_vr3 veriT_sk1)) :rule refl)
(step t18.t4 (cl (= @p_27 (! (< 0.0 veriT_sk1) :named @p_36))) :rule cong :premises (t18.t3))
(step t18.t5 (cl (= @p_28 (! (and @p_35 @p_36) :named @p_37))) :rule cong :premises (t18.t2 t18.t4))
(step t18.t6 (cl @p_38) :rule refl)
(step t18.t7 (cl (= @p_30 (! (< (- 1) veriT_sk0) :named @p_39))) :rule cong :premises (t18.t6))
(step t18.t8 (cl (= @p_31 (! (=> @p_37 @p_39) :named @p_40))) :rule cong :premises (t18.t5 t18.t7))
(step t18 (cl (= @p_32 @p_40)) :rule sko_forall)
(step t19 (cl (! (= @p_34 (! (not @p_40) :named @p_42)) :named @p_41)) :rule cong :premises (t18))
(step t20 (cl (not @p_41) @p_32 @p_42) :rule equiv_pos2)
(step t21 (cl @p_42) :rule th_resolution :premises (t17 t19 t20))
(step t22 (cl (! (= @p_42 (! (and @p_37 (! (not @p_39) :named @p_45)) :named @p_44)) :named @p_43)) :rule bool_simplify)
(step t23 (cl (not @p_43) @p_40 @p_44) :rule equiv_pos2)
(step t24 (cl @p_44) :rule th_resolution :premises (t21 t22 t23))
(step t25 (cl (! (= @p_44 (! (and @p_35 @p_36 @p_45) :named @p_47)) :named @p_46)) :rule tmp_AC_simp)
(step t26 (cl (not @p_46) (not @p_44) @p_47) :rule equiv_pos2)
(step t27 (cl @p_47) :rule th_resolution :premises (t24 t25 t26))
(step t28 (cl @p_35) :rule and :premises (t27))
(step t29 (cl @p_45) :rule and :premises (t27))
(step t30 (cl @p_39 (not @p_35)) :rule la_generic :args (1.0 1.0))
(step t31 (cl) :rule resolution :premises (t30 t28 t29))
In the step (step t30 (cl @p_39 (not @p_35)) :rule la_generic :args (1.0 1.0)) (aka - (1::int) < (veriT_sk0::int) ∨ ¬ (0::int) < veriT_sk0) the coeffecient should be 1, not 1.0
2020-06-20 14:20:55 (GMT)
How should those cases by typed to work well for you? My code generates real numbers whenever they are available (and hence prints .0 in this case). I think it would be odd to change this behavior just because the denominator is 1.
2020-06-20 14:31:42 (GMT)
morally, the coefficients here should be integers because they are used as integers and not as reals in that particular equation…
2020-06-21 12:45:16 (GMT)
Basically, at the place where you currently have:
if (SORT_REAL != DAG_SORT_NULL)
I want something like:
_Bool real_sort;
/** DAG is either the negation or directly < _ _, or = _ _, or <= _ _
So extract the sort of the symbol: it is either Real -> Real -> bool or Int -> Int -> Bool
So we extract the first component of it
**/
if(DAG_symb(DAG) == CONNECTOR_NOT)
real_sort = DAG_sort_sub(DAG_symb_sort(DAG_symb(DAG_arg1(DAG))), 0) == SORT_REAL;
else
real_sort = DAG_sort_sub(DAG_symb_sort(DAG_symb(arg)),0) == SORT_REAL;
if(real_sort)
This does not work, probably because I do not understand how sorts work in veriT… it is possible that this is completely impossible, because veriT is not typed the way I expect it…
2020-06-21 14:31:22 (GMT)
Okay veriT is definitely not typed the way I expected it. I expected < to have the right sort (either Real -> Boolean or Integer -> Boolean), but it does not...
2020-06-21 18:51:18 (GMT)
Hi Mathias,
yes, sorry for that. This is a reminiscence of SMT-LIB 1.0, where we seemed to go for subsorts, and Int was kind of a subset of Real. Since SMT-LIB 2.0, and even more in SMT-LIB 3.0, things are much cleaner. This should be cleaned in the code too.
2020-06-21 19:9:46 (GMT)
Hi Pascal,
from an historical perspective, it makes sense to have it that way. And thanks for the information, I never read the SMT-LIB 1.0 syntax.
I will just fix the types in Isabelle. That should not be a problem (purely syntactic transformation on the terms). I just attempted to give Hans-Jörg more work :grinning:, but fixing all types in veriT is a lot of work.
2020-06-22 8:7:49 (GMT)
It's nice to see that work on such an integration brings some latent issues to light. Fixing the types in Isabelle seems like the easiest thing to do for now. Pascal mentions "should be cleaned", though. How hard would this be? In th old days, we had a rewrite rule at Trolltech; whenever somebody said "X should be done", we rewrote it to "I will do it" (where I is the person who said "X should be done"). ;)
2020-06-22 8:17:44 (GMT)
It depends whether it makes HO merge more complicated or not… but I have no idea
2020-06-22 8:25:51 (GMT)
HO merge is a pie-in-the-sky. From what I understant now, it's not so much merge as rewrite from scratch.
2020-06-22 8:34:41 (GMT)
This is one of many things that are not that nice in the very heart of veriT. It means going through all the code to hack/fix. There are many such things in veriT, which will all require a full pass in the code; I'd say 8 hours per pass. It requires full view of the code. And at the end, we will still not be confident that we have not broken some weird invariant somewhere.
Indeed, this will probably also be part of a difficult discussion Jasmin and I will have in July, to clearly answer who and when.
2020-06-22 12:58:7 (GMT)
yeah let's define (for now) that if reals are present the arguments are real numbers and need to be interpreted by the checker as is appropriate for the sort of the inequality. It's unfortunate, but veriT-proofs-for-smt-lib3 can fix that ^^