Commits on Dec 11, 2023

1. Wrong destructor for mutually recursive ADT …

   The new Dolmen frontend didn't create the correct destructor in presence
   of mutually recursive ADT. For instance the input:
   ```smt2
   (set-logic ALL)
   (declare-datatypes ((Data1 0) (Data2 0))
     (
       ((cons1 (d1 Int) (d2 Data2)))
       (
         (cons2 (d3 Data1))
         (cons3)
       )
     )
   )
   (declare-const a Data1)
   (declare-const b Data2)
   (declare-const x Int)
   (assert ((_ is cons1) a))
   (assert ((_ is cons3) b))
   (assert (= (d1 a) x))
   (check-sat)
   ```
   raised an assertion in the record theory.
   The presence of a flaw in a test of `d_cnf` to discriminate between records
   and ADT produced `Sy.Access` destructors intead of `Sy.Destructor`
   destructors on some terms whose the type is a mutually recursive ADT.
   For instance `d1 a` was translated into `mk_term Sy.Access [a] ...`.
   
   The fix consists in using the cache of AE types in `d_cnf` to discriminate
   between records and ADT.
   
   Notice that the legacy frontend parses the previous file correctly.

   

   Halbaroth committed Dec 11, 2023
   Configuration menu

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

   Copy the full SHA

   565c105 View commit details

   Browse the repository at this point in the history