Code

Model generation support for SatML#829

Code

Merged

Halbaroth merged 28 commits intoOCamlPro:nextOCamlPro/alt-ergo:nextfrom Halbaroth:satml-modelHalbaroth/alt-ergo:satml-modelCopy head branch name to clipboardSep 27, 2023

+47,458-50,550

Commits

Commits on Sep 26, 2023

• Theory: harden 'compute_concrete_model' function

  

  iguerNL

  authored and

  Halbaroth

  committed
  914d283

  Copy full SHA for 914d283

• Push the test 'get_case_split_policy() == origin' into Theory.do_case_split

  

  iguerNL

  authored and

  Halbaroth

  committed
  982bb92

  Copy full SHA for 982bb92

• CS: functions return all the env instead of just 'gamma_finite'.

  

  iguerNL

  authored and

  Halbaroth

  committed
  de26aae

  Copy full SHA for de26aae

• Fun_sat: refactor the way models are handled/printed

  Show description for fed58a7
  

  iguerNL

  authored and

  Halbaroth

  committed
  fed58a7

  Copy full SHA for fed58a7

• satML: add missing case-split strategies

  

  iguerNL

  authored and

  Halbaroth

  committed
  7447ca3

  Copy full SHA for 7447ca3

• satML: implement models generation.

  

  iguerNL

  authored and

  Halbaroth

  committed
  0c37f66

  Copy full SHA for 0c37f66

• Make model tests negative

  Show description for 1ace3d9
  Halbaroth

  committed
  1ace3d9

  Copy full SHA for 1ace3d9

• Reindent

  Halbaroth

  committed
  3ac006b

  Copy full SHA for 3ac006b

• Update documentation about output_concrete_model

  Show description for 4b03759
  Halbaroth

  committed
  4b03759

  Copy full SHA for 4b03759

• Document the timeout_reason ADT

  Halbaroth

  committed
  0251733

  Copy full SHA for 0251733

• poetry

  Halbaroth

  committed
  9496cf6

  Copy full SHA for 9496cf6

• Restore the comment about reinit_cpt

  Halbaroth

  committed
  115a16a

  Copy full SHA for 115a16a

• Fix spelling

  Halbaroth

  committed
  986321d

  Copy full SHA for 986321d

• Remainder to the issue 834

  Halbaroth

  committed
  b39ecb8

  Copy full SHA for b39ecb8

• Simplify get-model processing

  Halbaroth

  committed
  9507d63

  Copy full SHA for 9507d63

• Remove SAT solver choices while model generating

  Show description for 1ca2286
  Halbaroth

  committed
  1ca2286

  Copy full SHA for 1ca2286

• Fix model output

  Show description for 3d75176
  Halbaroth

  committed
  3d75176

  Copy full SHA for 3d75176

• All the model tests are positive

  Halbaroth

  committed
  be505b4

  Copy full SHA for be505b4

• Remove deprecated cram tests

  Show description for afb8e44
  Halbaroth

  committed
  afb8e44

  Copy full SHA for afb8e44

• Test models with all the SAT solvers

  Halbaroth

  committed
  e0c9b34

  Copy full SHA for e0c9b34

• Restoring dump-models option

  Show description for b45ee04
  Halbaroth

  committed
  b45ee04

  Copy full SHA for b45ee04

• Use the right post-solve SAT environment for models

  Show description for a155756
  Halbaroth

  committed
  a155756

  Copy full SHA for a155756

• Print dump models on the channel models

  Show description for 709dc42
  Halbaroth

  committed
  709dc42

  Copy full SHA for 709dc42

• Prevent printing internal names in models

  Show description for cd998e7
  Halbaroth

  committed
  cd998e7

  Copy full SHA for cd998e7

• Promote tests

  Halbaroth

  committed
  819935b

  Copy full SHA for 819935b

• Revert "Simplify get-model processing"

  Show description for a6caf6a
  Halbaroth

  committed
  a6caf6a

  Copy full SHA for a6caf6a

• Review changes

  Halbaroth

  committed
  d4301df

  Copy full SHA for d4301df

Commits on Sep 27, 2023

• Test only models with FunSAT

  Show description for 3299ff7
  Halbaroth

  committed
  3299ff7

  Copy full SHA for 3299ff7