Code

Rebase of Optim Alt-Ergo#553

Code

Closed

Halbaroth wants to merge 81 commits intoOCamlPro:nextOCamlPro/alt-ergo:nextfrom Halbaroth:rebase-optim-altHalbaroth/alt-ergo:rebase-optim-altCopy head branch name to clipboard

+126,722-733

Commits

Commits on May 11, 2023

• change version to models

  

  ACoquereau

  authored and

  Halbaroth

  committed
  c74ca18

• models generation: add some examples

  

  OCamlPro-mattiasdrp

  authored and

  Halbaroth

  committed
  98772b3

• check sat handled on the lowest possible level, need to work on unsat instead of valid as a result

  

  OCamlPro-mattiasdrp

  authored and

  Halbaroth

  committed
  5dacb94

• first prototype for models in Why3, lots of hard coded stuff that needs to be well understood before making it work for every case

  

  ACoquereau

  authored and

  Halbaroth

  committed
  3bca712

• Change interpretation option, use mdl-formatter to compute but not print model and interpretation

  

  ACoquereau

  authored and

  Halbaroth

  committed
  963a5b9

• Move the printing of counterexample from uf.ml to models.ml

  

  ACoquereau

  authored and

  Halbaroth

  committed
  16a9f12

• Prototype of printer for records in smt format

  

  ACoquereau

  authored and

  Halbaroth

  committed
  dceb732

• Directly use rep of bool value for counterexamples

  

  ACoquereau

  authored and

  Halbaroth

  committed
  483e561

• fix destr list rev

  

  ACoquereau

  authored and

  Halbaroth

  committed
  687b6bb

• Clean choose_adequate_model for boolean constant

  

  ACoquereau

  authored and

  Halbaroth

  committed
  5d787fd

• Add fast option that disable greedier instantiation phase

  

  ACoquereau

  authored and

  Halbaroth

  committed
  ee6f0c9

• remove greedier and get_fast in fun_sat

  

  OriginLabs-Iguernlala

  authored and

  Halbaroth

  committed
  b995c0f

• Prototype to output constraint as model if output is set to why3

  

  ACoquereau

  authored and

  Halbaroth

  committed
  d8bca6b

• Remove why3-counter-example option, use -o why3 instead

  

  ACoquereau

  authored and

  Halbaroth

  committed
  e4e1a2e

• Code cleaning and addition of functions printing with cascade of ite

  

  ACoquereau

  authored and

  Halbaroth

  committed
  e55d960

• fix compatibility for ocaml version < 4.07

  

  ACoquereau

  authored and

  Halbaroth

  committed
  a7fd0bb

• Fix printing of some type in smtlib2 output format

  

  ACoquereau

  authored and

  Halbaroth

  committed
  489a161

• Add support for record constuctor use in model

  

  ACoquereau

  authored and

  Halbaroth

  committed
  463ce8d

• Add option dummy-value for interpretation that output _ instead of dummy fresh value when no value is computed

  

  ACoquereau

  authored and

  Halbaroth

  committed
  1bd990e

• Fix pp_term and assert output prototype

  

  ACoquereau

  authored and

  Halbaroth

  committed
  a644b8d

• reeplace dummy_value with use_underscore option

  

  ACoquereau

  authored and

  Halbaroth

  committed
  55301df

• remove fast option, use --instantiation-heuristic=normal instead

  

  ACoquereau

  authored and

  Halbaroth

  committed
  d3f99ce

• Copy print expr code in models for better management of named expr

  

  ACoquereau

  authored and

  Halbaroth

  committed
  c175989

• [models] add case-split on internal bool terms

  Show description for f8aa8fa
  

  OriginLabs-Iguernlala

  authored and

  Halbaroth

  committed
  f8aa8fa

• Type Expr.view should remain "private"

  

  OriginLabs-Iguernlala

  authored and

  Halbaroth

  committed
  02b104d

• auto set option "fm_cross_limit = -1" (ie. infinity) if models-gen is set.

  

  OriginLabs-Iguernlala

  authored and

  Halbaroth

  committed
  ac9e7d2

• Fix use_underscore_interpretation option

  

  ACoquereau

  authored and

  Halbaroth

  committed
  304e0af

• Remove deadcode from models and mv models.ml in frontend

  

  ACoquereau

  authored and

  Halbaroth

  committed
  9712103

• remove unused models-generation code (all, complete and default models)

  

  OriginLabs-Iguernlala

  authored and

  Halbaroth

  committed
  81e9b01

• remove functions related to old model

  

  ACoquereau

  authored and

  Halbaroth

  committed
  6b364cf

• clean unused code

  

  OriginLabs-Iguernlala

  authored and

  Halbaroth

  committed
  c47dfec

• fix linter

  

  OriginLabs-Iguernlala

  authored and

  Halbaroth

  committed
  a987dd3

• Fix frontend output in case of timeout

  

  ACoquereau

  authored and

  Halbaroth

  committed
  ab8bb1a

• Clean models, remove old native output, and remove ref for records

  

  ACoquereau

  authored and

  Halbaroth

  committed
  5afaff6

• Move profile module from Models module to structures

  

  ACoquereau

  authored and

  Halbaroth

  committed
  5042209

• Fix printing of constraints in why3 output when constraints are functions and not just constants

  

  ACoquereau

  authored and

  Halbaroth

  committed
  1afd75f

• Fix declare-fun command in models

  

  ACoquereau

  authored and

  Halbaroth

  committed
  66af011

• Lists.ml: new function partition_map more generic than List.partition

  

  iguerNL

  authored and

  Halbaroth

  committed
  be9794d

• working examples for linear optimization feature

  

  iguerNL

  authored and

  Halbaroth

  committed
  6a7f41e

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

  Show description for 3eb3ab9
  

  iguerNL

  authored and

  Halbaroth

  committed
  3eb3ab9

• Theory: harden 'compute_concrete_model' function

  

  iguerNL

  authored and

  Halbaroth

  committed
  c5ab9ef

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

  

  iguerNL

  authored and

  Halbaroth

  committed
  70da092

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

  

  iguerNL

  authored and

  Halbaroth

  committed
  3610394

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

  

  iguerNL

  authored and

  Halbaroth

  committed
  ac7fbdd

• reintroduce debug traces in satml

  

  iguerNL

  authored and

  Halbaroth

  committed
  da2783a

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

  

  iguerNL

  authored and

  Halbaroth

  committed
  eab5339

• Frontend: new syntax for optimisation constraints, with their ordering.

  

  iguerNL

  authored and

  Halbaroth

  committed
  b839235

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

  

  iguerNL

  authored and

  Halbaroth

  committed
  8a4967b

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

  

  iguerNL

  authored and

  Halbaroth

  committed
  d5cc003

• Infrastructure in theories for CS with optimized values

  

  iguerNL

  authored and

  Halbaroth

  committed
  8dc07da

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

  

  iguerNL

  authored and

  Halbaroth

  committed
  f6c1445

• IntervalCalculus: Produce optimized splits for LIA and LRA

  

  iguerNL

  authored and

  Halbaroth

  committed
  dce2768

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

  

  iguerNL

  authored and

  Halbaroth

  committed
  211b54f

• Fun_sat: refactor the way models are handled/printed

  Show description for 5ea4ef0
  

  iguerNL

  authored and

  Halbaroth

  committed
  5ea4ef0

• satML: add missing case-split strategies

  

  iguerNL

  authored and

  Halbaroth

  committed
  1a61b24

• satML: implement models generation.

  

  iguerNL

  authored and

  Halbaroth

  committed
  3db692a

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

  Show description for 5a0e246
  

  iguerNL

  authored and

  Halbaroth

  committed
  5a0e246

• Print models of arrays (home made syntax)

  

  iguerNL

  authored and

  Halbaroth

  committed
  75c303f

• Models: re-introduce removed invariant check

  

  iguerNL

  authored and

  Halbaroth

  committed
  9d37328

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

  Show description for 7d1a860
  

  iguerNL

  authored and

  Halbaroth

  committed
  7d1a860

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

  

  ACoquereau

  authored and

  Halbaroth

  committed
  8a2e111

• Correctly handle Case-split backtrack when having Optimization constraints

  

  iguerNL

  authored and

  Halbaroth

  committed
  4f75ac2

• Handling disjunctions in optimization

  

  iguerNL

  authored and

  Halbaroth

  committed
  9d3d34e

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

  

  iguerNL

  authored and

  Halbaroth

  committed
  1766c11

• fix translate ordering in pstm2_to_alt_ergo

  

  iguerNL

  authored and

  Halbaroth

  committed
  9b61fae

• fix translate from SMT2 to AE

  

  iguerNL

  authored and

  Halbaroth

  committed
  4325df2

• re-implement all-models feature differently

  Show description for 88d0255
  

  iguerNL

  authored and

  Halbaroth

  committed
  88d0255

• pprinting models of functions: print models of args instead of args

  

  iguerNL

  authored and

  Halbaroth

  committed
  eaeaba6

• compute model of terms starting from the smallest one

  

  iguerNL

  authored and

  Halbaroth

  committed
  ed979ed

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

  

  iguerNL

  authored and

  Halbaroth

  committed
  6dd3cd4

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

  

  iguerNL

  authored and

  Halbaroth

  committed
  7030c1f

• Fix printing in models by usin Printer functions

  

  ACoquereau

  authored and

  Halbaroth

  committed
  3c963b2

• Print why3 parsable variable name when it's a fresh

  

  ACoquereau

  authored and

  Halbaroth

  committed
  10d6574

• Fix new options in output section in the manpage

  

  ACoquereau

  authored and

  Halbaroth

  committed
  b89c678

• Add timeout-as-unknown option

  

  ACoquereau

  authored and

  Halbaroth

  committed
  2322087

• Fix fresh names in ite

  

  ACoquereau

  authored and

  Halbaroth

  committed
  564ac1c

• bugfix in bitv.ml: fresh vars should be attached to syntactic terms

  

  iguerNL

  authored and

  Halbaroth

  committed
  bb55438

• Accumulate facts when calling SAT.assume

  Show description for bebfd62
  

  iguerNL

  authored and

  Halbaroth

  committed
  bebfd62

• Add ability to enable Cube-Test bounds inference (done if --no-fm is set)

  

  iguerNL

  authored and

  Halbaroth

  committed
  5e557ae

• remove useless debug messages + lint

  

  iguerNL

  authored and

  Halbaroth

  committed
  7366af6

• Fix JS worker

  Halbaroth

  committed
  09430b3