Code

[WIP] OptimAE#776

Code

Closed

Halbaroth wants to merge 42 commits intoOCamlPro:nextOCamlPro/alt-ergo:nextfrom Halbaroth:cherry-pick-optimaeHalbaroth/alt-ergo:cherry-pick-optimaeCopy head branch name to clipboard

+172,642-50,790

Commits

Commits on Sep 15, 2023

• working examples for linear optimization feature

  

  iguerNL

  authored and

  Halbaroth

  committed
  b26c5dd

• New option --objectives-in-model to show optimized expressions in 'model'

  Show description for 7b97719
  

  iguerNL

  authored and

  Halbaroth

  committed
  7b97719

• Theory: harden 'compute_concrete_model' function

  

  iguerNL

  authored and

  Halbaroth

  committed
  c299944

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

  

  iguerNL

  authored and

  Halbaroth

  committed
  e69d34e

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

  

  iguerNL

  authored and

  Halbaroth

  committed
  772a682

• Refactoring to reduce "printing unbounded values" patch in uf.ml.

  

  iguerNL

  authored and

  Halbaroth

  committed
  b4348e2

• reintroduce debug traces in satml

  

  iguerNL

  authored and

  Halbaroth

  committed
  3f778b2

• Theory.query: simple test to deactivate TCP for both FunSat and CDCL

  

  iguerNL

  authored and

  Halbaroth

  committed
  9c2263b

• begin-optim-alt: Frontend: new syntax for optimisation constraints, with their ordering.

  

  iguerNL

  authored and

  Halbaroth

  committed
  2bfa13c

• Fix expr.ml: purify inside Optimize _ as well

  

  iguerNL

  authored and

  Halbaroth

  committed
  28b8447

• prepare CS to return 'Unbounded' in case of optimization requests.

  

  iguerNL

  authored and

  Halbaroth

  committed
  0429b64

• Infrastructure in theories for CS with optimized values

  

  iguerNL

  authored and

  Halbaroth

  committed
  f5d8209

• Detect optimization directives (predicates) in Theory and update env

  

  iguerNL

  authored and

  Halbaroth

  committed
  ad9d782

• IntervalCalculus: Produce optimized splits for LIA and LRA

  

  iguerNL

  authored and

  Halbaroth

  committed
  1b740fe

• update SMT2 model output with '(objectives ...)' section

  

  iguerNL

  authored and

  Halbaroth

  committed
  3a8cdad

• Fun_sat: refactor the way models are handled/printed

  Show description for 6b48f91
  

  iguerNL

  authored and

  Halbaroth

  committed
  6b48f91

• satML: add missing case-split strategies

  

  iguerNL

  authored and

  Halbaroth

  committed
  48cd803

• satML: implement models generation.

  

  iguerNL

  authored and

  Halbaroth

  committed
  73e400d

• UF: fix model_extraction: arguments of function may be interpreted

  Show description for 14b46b8
  

  iguerNL

  authored and

  Halbaroth

  committed
  14b46b8

• Print models of arrays (home made syntax)

  

  iguerNL

  authored and

  Halbaroth

  committed
  9b9e110

• Models: re-introduce removed invariant check

  

  iguerNL

  authored and

  Halbaroth

  committed
  a06e01f

• Models: don't "assert false" when seeing an AC symbols in 'assign_next'

  Show description for 296309c
  

  iguerNL

  authored and

  Halbaroth

  committed
  296309c

• Fix printing of status when in interpretation mode and add clean fmt in the print_fmt function

  

  ACoquereau

  authored and

  Halbaroth

  committed
  0325706

• Correctly handle Case-split backtrack when having Optimization constraints

  

  iguerNL

  authored and

  Halbaroth

  committed
  12714f1

• Handling disjunctions in optimization

  

  iguerNL

  authored and

  Halbaroth

  committed
  70e3514

• Translate minimize/maximize from psmt2-frontend to Alt-Ergo

  

  iguerNL

  authored and

  Halbaroth

  committed
  9e6e63c

• fix translate ordering in pstm2_to_alt_ergo

  

  iguerNL

  authored and

  Halbaroth

  committed
  230c928

• fix translate from SMT2 to AE

  

  iguerNL

  authored and

  Halbaroth

  committed
  a1698d0

• re-implement all-models feature differently

  Show description for f73a383
  

  iguerNL

  authored and

  Halbaroth

  committed
  f73a383

• compute model of terms starting from the smallest one

  

  iguerNL

  authored and

  Halbaroth

  committed
  a7ad6b9

• Models: export the map of term |-> get-value(term) computed in UF

  

  iguerNL

  authored and

  Halbaroth

  committed
  4a0d2a7

• optim:re-set timelimit when trying to find a better min in other branches

  

  iguerNL

  authored and

  Halbaroth

  committed
  3e679a2

• Fix new options in output section in the manpage

  

  ACoquereau

  authored and

  Halbaroth

  committed
  105fa4a

• Add timeout-as-unknown option

  

  ACoquereau

  authored and

  Halbaroth

  committed
  9f8ed84

• Don't run ocp-indent on mly files. See the issue

  Show description for f437e21
  Halbaroth

  committed
  f437e21

• Fix indentation in the legacy parser

  Halbaroth

  committed
  5272ea9

• Fix indentation in the legacy lexer

  Halbaroth

  committed
  61b7d1a

• Print always smtlib comments in the models

  Halbaroth

  committed
  3254796

• Negative tests

  Show description for 9f2449b
  Halbaroth

  committed
  9f2449b

• Fix the js worker

  Halbaroth

  committed
  f9e74fe

• Remove gui artefact

  Halbaroth

  committed
  9f556cf

Commits on Sep 18, 2023

• Rebase artefacts

  Halbaroth

  committed
  19fa24a