Code

WIP: Simplify preprocess#242

Code

Open

Stevendeo wants to merge 18 commits intoOCamlPro:nextOCamlPro/alt-ergo:nextfrom Stevendeo:simplify-preprocessStevendeo/alt-ergo:simplify-preprocessCopy head branch name to clipboard

+2,245-156

Commits

Commits on Aug 16, 2022

• Formula simplification at preprocessing

  

  Steven de Oliveira

  authored and

  Stevendeo

  committed
  40e42ba

• First version of AI preprocessing

  Stevendeo

  committed
  be706bb

• Bug fixes

  Stevendeo

  committed
  6a7be9f

• Replacing 'Intervals.scale' by Intervals arithmetic operators

  Stevendeo

  committed
  ba41bba

• Sign bugfix

  Stevendeo

  committed
  158ea20

• Not calling mk_let if a simplification has not been performed

  Stevendeo

  committed
  7ef2a6b

• Adding a reinitialization function to hconsing

  Stevendeo

  committed
  c5eb81a

• Adding a reinitialization function for the cache of Shostak.Combine.make

  Stevendeo

  committed
  69db321

• Also emptying simplifier's cache

  

  steven-de-oliveira

  authored and

  Stevendeo

  committed
  2bf23ee

• Correct indent

  Stevendeo

  committed
  f5b4d22

• Moving eq_list to util.ml

  Stevendeo

  committed
  6f09152

• Replacing vrai/faux by english equivalents

  Stevendeo

  committed
  04e53e3

• Poetry

  Stevendeo

  committed
  1c792e2

• Fixing style

  Stevendeo

  committed
  9501cb2

• Simplifying formulas in literals

  Stevendeo

  committed
  7320c61

• Rebase fix

  Stevendeo

  committed
  384795c

• Adding option for activatiing simplifier

  Stevendeo

  committed
  c3055eb

• Replacing variables values when constant

  Stevendeo

  committed
  8369dfc