Skip to content

Document rare_rewrite

In the same spirit of documenting the BV rules, cvc5's Alethe output also produces RARE proof steps. The format we have converged for that is:

(step <id> <conclusion> :rule rare_rewrite :args (<rareRule> (<term>)*)

where is a string value supposed to stand for the name of the rule and may contain an operator "rare-list" whose arity is >= 0 (this operator is to model that arguments of rare rules can be lists of terms).

Somewhere there is a documentation RARE that should be linked. @Lachnitt will know more.

Edited by Hans-Jörg
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information