moved from Num to Zarith. IMpacted main.ml ad uses of Z3 in zustre_cex and seal-extract
printing nodes + more progress on seal export
Moved some code
- Refactored Error exception and messages- Bugs in partial evaluation for equalities among bool constants and a nice recursive call generating a stack overflow! Now solved- Setup a timeout for z3 in seal- Better log for seal
Commenting out unused variables
[seal] more progress on seal extract
seal: now deals with enum
seal: stateless systems
[seal] delt with Merge and when[printer] more kind2 syntax
Produce true/false statements as constants
scheduling now report unused vars and remove their definition instead of stopping processing.
Seal: solved issue with guards merging
Sorting expressions: less bugs
valid _verif node for seal-export lustre
Seal export lustre
Contract printer cocospec
Export cocospec contract
Output folder for seal-extract
Seal-export to a new file
seal-export: produce the output as well. Could be simpler
Seal-extract: first serious version. Guards are gathered as a single expression
Updated version seal-extract
Working version of seal-extract. Heavy load on z3.TODO: improvement through memoization
Better extraction in lustrev-seal
lustrev seal: ongoing work on extraction as dynamical system. Still not working yet
Minor modif on seal
Reorganizing folders