remove_unused:dependency not strong enough with definition given in drivers
The transformation remove_unused
does not remove the axioms that are marked with the meta remove_unused:dependency
when a symbol in this axiom is defined in a driver.
I have a small repro-case to make it clearer.
(* a.mlw *)
module A
predicate p (x : int)
axiom p_def: forall x. x <> 0 -> p x
meta "remove_unused:dependency" axiom p_def, predicate p
predicate q (x : int)
axiom q_def: forall x. p x -> q x
meta "remove_unused:dependency" axiom q_def, predicate q
end
(* b.mlw *)
module B
use a.A
predicate c (x : int)
lemma l: forall x. c x
end
and I use a driver to override the symbol q
:
(* drv.drv *)
theory a.A
syntax predicate q "(= %1 0)"
end
together with the config:
[prover_modifiers]
driver = "drv.drv"
name = "CVC4"
When I run the IDE, with why3 ide -L . --extra-config=c.conf
, and I look at the cvc4 smt2 file generated for the task l
, I get
;; produced by cvc4_17.drv ;;
(set-logic ALL_SUPPORTED)
(set-info :smt-lib-version 2.6)
;; p
(declare-fun p (Int) Bool)
;; p_def
(assert (forall ((x Int)) (=> (not (= x 0)) (p x))))
;; q_def
(assert (forall ((x Int)) (=> (p x) (= x 0))))
;; c
(declare-fun c (Int) Bool)
(assert
(not (forall ((x Int)) (c x))))
(check-sat)
(get-info :reason-unknown)
As you can see, the axiom p_def
and q_def
have not been removed despite the meta remove_unused
. If I do not define q
in a driver, both axioms are removed. It seems that this case always happen in the standard library and unfortunately we keep a lot of axioms in the context that should be removed by the transformation remove_unused
because the axiom is not used in the task.