Prove remaining rewrite rules for the supported theories.

ufmg-smite / lean-smt

Tactics for discharging Lean goals into SMT solvers.

Apache License 2.0

94 stars 19 forks source link

Prove remaining rewrite rules for the supported theories. #62

Closed abdoo8080 closed 1 year ago

abdoo8080 commented 1 year ago

This PR updates the rewrite rules used by cvc5 for builtin, boolean, and UF theories. Additionally, it reproves the arithmetic rewrite rules to work for both integers and rational numbers.