Add support for mutual recursion between the BV and the boolean fragment

leanprover / leansat

This package provides an interface and foundation for verified SAT reasoning

Apache License 2.0

49 stars 6 forks source link

Add support for mutual recursion between the BV and the boolean fragment #68

Open hargoniX opened 4 months ago

hargoniX commented 4 months ago

If we want to support features like if statements efficiently it is necessary to process theory terms that consist e.g. of some BV logic which contains a boolean term which contains again further BV logic etc. The main connective here is BitVec.ofBool.

hargoniX commented 4 months ago

Idea: As we preprocess, for each subterm of the form BitVec.ofBool x that we encounter we add the following statements to the context:

x -> BitVec.ofBool x = 1
!x -> BitVec.ofBool x = 0 This must also be recursive within x as it might contain further BitVec logic.

The bv_unsat logic will pick up BitVec.ofBool x as an atom and thus recognize and encode these theorems properly.