Commits on Mar 25, 2024

1. fix(BV): Properly set fully interpreted operators …

   Alt-Ergo calls "fully interpreted" symbols that are fully internalized
   in semantic values and do not need to be taken into consideration by the
   CC(X) algorithm (see function `congruents` in `ccx.ml`).
   
   (Note that `fully_interpreted` is only called for the Shostak theory
   associated with the symbol according to `is_min_symb`.)
   
   The BV theory incorrectly states that all its symbols are fully
   interpreted, including `bv2nat`, `int2bv`, etc.; however, only `concat`,
   `extract` and `bv2nat` are fully interpreted. This means that Alt-Ergo
   never performs congruence closure for these functions, leading to missed
   reasoning opportunities.

   

   bclement-ocp committed Mar 25, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for c71be56
   • Browse repository at this point

   Copy the full SHA

   c71be56 View commit details

   Browse the repository at this point in the history