Carcara confused by definitions

[BrunoDutertre]

Here's a simple problem:

(set-logic QF_UF)
(declare-sort U 0)
(declare-fun x () U)
(declare-fun y () U)
(declare-fun f (U U) U)
(define-fun aaa () Bool (not (= (f y x) (f x y))))
(assert (= x y))
(assert aaa)
(check-sat)
(exit)

On this input, cvc5 will generate a proof like this:

(assume a0 (= aaa (not (= (f y x) (f x y)))))
(assume a1 (= x y))
(assume a2 aaa)
(step t1 (cl (=> (= x y) (= (f y x) (f x y))) (= x y)) :rule implies_neg1)
(anchor :step t2)
(assume t2.a0 (= x y))
(step t2.t1 (cl (= y x)) :rule symm :premises (t2.a0))
(step t2.t2 (cl (= x y)) :rule symm :premises (t2.t1))
(step t2.t3 (cl (= (f y x) (f x y))) :rule cong :premises (t2.t1 t2.t2))
(step t2 (cl (not (= x y)) (= (f y x) (f x y))) :rule subproof :discharge (t2.a0))
(step t3 (cl (=> (= x y) (= (f y x) (f x y))) (= (f y x) (f x y))) :rule resolution :premises (t1 t2) :args ((= x y) true))
(step t4 (cl (=> (= x y) (= (f y x) (f x y))) (not (= (f y x) (f x y)))) :rule implies_neg2)
(step t5 (cl (=> (= x y) (= (f y x) (f x y))) (=> (= x y) (= (f y x) (f x y)))) :rule resolution :premises (t3 t4) :args ((= (f y x) (f x y)) true))
(step t6 (cl (=> (= x y) (= (f y x) (f x y)))) :rule contraction :premises (t5))
(step t7 (cl (not (= x y)) (= (f y x) (f x y))) :rule implies :premises (t6))
(step t8 (cl (= (f y x) (f x y)) (not (= x y))) :rule reordering :premises (t7))
(step t9 (cl (not (= aaa (not (= (f y x) (f x y))))) (not aaa) (not (= (f y x) (f x y)))) :rule equiv_pos2)
(step t10 (cl (not (= (f y x) (f x y)))) :rule resolution :premises (t9 a0 a2) :args ((= aaa (not (= (f y x) (f x y)))) false aaa false))
(step t11 (cl) :rule resolution :premises (t8 t10 a1) :args ((= (f y x) (f x y)) true (= x y) false))

The first assumption is rejected as invalid by carcara:

carcara check --skip-unknown-rules reduced0.prf reduced0.smt2
[ERROR] checking failed on step 'a0' with rule 'assume': term '(= (not (= (f y x) (f x y))) (not (= (f y x) (f x y))))' was not in original problem's assumptions
invalid

[bpandreotti]

By default, Carcará expands function definitions introduced by define-fun commands (meaning every occurence of aaa is replaced by (not (= (f y x) (f x y)))), instead of introducing a new assertion. You can override this behaviour by passing the --dont-apply-function-defs flag. Using this flag, the example you gave checks without errors.

[BrunoDutertre]

Ok thanks. Any reason not to make this default?

[bpandreotti]

While the Alethe specification does not explicitly define what is correct in this case, in retrospect it does make more sense for this to be the default behaviour. Commit e8d1e80 fixes this.