[new release] alt-ergo (4 packages) (2.6.0)

[bclement-ocp]

The Alt-Ergo SMT prover

• Project page: https://alt-ergo.ocamlpro.com/
• Documentation: https://ocamlpro.github.io/alt-ergo

CHANGES:

Command-line interface

• Enable FPA theory by default (Active fpa as default OCamlPro/alt-ergo#1177)
• Remove deprecated output channels (Simplify output channels OCamlPro/alt-ergo#782)
• Deprecate the --use-underscore since it produces models that are not SMT-LIB
  compliant (Deprecate the option --use-underscore OCamlPro/alt-ergo#805)
• Add --dump-models-on to dump models on a specific output channel (Adding an option to dump models on a specific output channel OCamlPro/alt-ergo#838)
• Use consistent return codes (Fix error handling of dolmen OCamlPro/alt-ergo#842)
• Add --continue-on-error flag to set the SMT-LIB error behavior (Handling error strategy OCamlPro/alt-ergo#853)
• Make dolmen the default value for the --frontend option (Make Dolmen the default frontend OCamlPro/alt-ergo#857)
• Restore functionality to broken --profiling option (fix: Make --profiling not crash OCamlPro/alt-ergo#947)
• Add bare-bones support for interactive input in SMT-LIB format (feat: Allow interactive SMT-LIB input OCamlPro/alt-ergo#949)
• Less confusing behavior on timeout (Fix timeout OCamlPro/alt-ergo#982, Fix timelimit per goal OCamlPro/alt-ergo#984)
• Add --strict option for SMT-LIB compliant mode (feat: Option --optimize OCamlPro/alt-ergo#916, fix(CLI): Remove --optimize option in favor of --strict OCamlPro/alt-ergo#1133)
• Deprecate sum, typing and warnings debug flags (Deprecate debug flags OCamlPro/alt-ergo#1204)

SMT-LIB support

• Add support for the many new SMT-LIB commands (Support of get-info SMT2 command OCamlPro/alt-ergo#837, feat: get-assignment statement OCamlPro/alt-ergo#848, Adding (reset) and (exit) statements OCamlPro/alt-ergo#852, feat: support (get-info :all-statistics) and refactoring Profiling module OCamlPro/alt-ergo#863, feat: Echo command OCamlPro/alt-ergo#911,
  Make get_value sound by not stating a formula is false when it is absent from the environment OCamlPro/alt-ergo#942, feat: Steps on :all-statistics command OCamlPro/alt-ergo#945, Fixed get-value OCamlPro/alt-ergo#961, Print unknown reason in SMT-LIB syntax OCamlPro/alt-ergo#975, fix(smt-lib): Respect reproducible-resource-limit specification OCamlPro/alt-ergo#1069)
• Expose the FPA rounding builtin in the SMT-LIB format (feat: exporting alt-ergo FPA built-in primitives OCamlPro/alt-ergo#876, feat(FPA): Add ae.float{16,32,64,128} SMT-LIB builtins OCamlPro/alt-ergo#1135)
• Allow changing the SAT solver using (set-option) (Allow dynamic selection of the SAT solver with set-option OCamlPro/alt-ergo#880)
• Add support for the :named attribute (Dolmen named formulae OCamlPro/alt-ergo#957)
• Add support for quoted identifiers (Quoted identifiers OCamlPro/alt-ergo#909, Using dolmen printer to display quoted identifiers OCamlPro/alt-ergo#972)
• Add support for naming lemmas in SMT-LIB syntax (Named lemmas in SMT-LIB format OCamlPro/alt-ergo#1141, Use a custom attribute to name lemma OCamlPro/alt-ergo#1143)

Model generation

• Use post-solve SAT environment in model generation, fixing issues where
  incorrect models were generated (Use post-solve SAT environment for model generation OCamlPro/alt-ergo#789)
• Restore support for records in models (Restore record printing functionality OCamlPro/alt-ergo#793)
• Use abstract values instead of dummy values in models where the
  actual value does not matter (Replace dummy values in Model by abstract values OCamlPro/alt-ergo#804, Use a separated counter for abstract value OCamlPro/alt-ergo#835)
• Use fresh names for all abstract values to prevent accidental captures (Use fresh names for all the abstract values OCamlPro/alt-ergo#811)
• Add support for model generation with the default CDCL solver (Model generation support for SatML OCamlPro/alt-ergo#829)
• Support model generation for the BV theory ([bitv] Add support for model generation OCamlPro/alt-ergo#841, fix(BV): Fix unsoundness in BV model generation OCamlPro/alt-ergo#968)
• Add support for optimization (MaxSMT / OptiSMT) with
  lexicographic Int and Real objectives (feat: OptimAE OCamlPro/alt-ergo#861, Clean up OptimAE OCamlPro/alt-ergo#921)
• Add a SMT-LIB printer for expressions (Add a SMT-LIB compliant printer for Expr OCamlPro/alt-ergo#952, Simplify numerical expressions in SMT-LIB printers OCamlPro/alt-ergo#981, feat(BV): Display BV constants using hexadecimal OCamlPro/alt-ergo#1082, Fix issue 926 OCamlPro/alt-ergo#931, Bubble printing model OCamlPro/alt-ergo#932)
• Ensure models have a value for all constants in the problem (Complete model OCamlPro/alt-ergo#1019)
• Fix a rare soundness issue with integer constraints when model generation is
  enabled (fix(arith): Do not overly tighten bounds over infinite domains OCamlPro/alt-ergo#1025)
• Support model generation for the ADT theory (feat(ADT): model generation OCamlPro/alt-ergo#1093, Use Dolmen attribute to store well founded order OCamlPro/alt-ergo#1153)

Theory reasoning

• Add word-level propagators for the BV theory (feat(BV): Word-level propagation for BV logic OCamlPro/alt-ergo#944, refactor(BV): Track domains for uninterpreted leaves only OCamlPro/alt-ergo#1004, fix(BV): Treat bvand, bvor, bvxor as interpreted OCamlPro/alt-ergo#1007, refactor(BV): Merge Congruence and Constraints OCamlPro/alt-ergo#1010,
  fix(BV): Actually propagate freshness change OCamlPro/alt-ergo#1011, feat: Count steps for constraint propagation OCamlPro/alt-ergo#1012, cleanup(CP): Simplify constraint handling OCamlPro/alt-ergo#1040, CP: Support for domains on non-leaves OCamlPro/alt-ergo#1044, feat(BV,CP): Use a FIFO queue for constraint propagation OCamlPro/alt-ergo#1054, feat(BV,CP): Ephemeral API for domain updates OCamlPro/alt-ergo#1055, feat(BV,CP): Explicit constraint simplification OCamlPro/alt-ergo#1056, feat(BV): Generic constraint representation OCamlPro/alt-ergo#1057, fix(CP): Do not add unnecessary explanations to domains OCamlPro/alt-ergo#1065, fix(BV): Properly set fully interpreted operators OCamlPro/alt-ergo#1073, feat(BV): Do not store width in Bitlist OCamlPro/alt-ergo#1144,
  feat(BV): Only store domains on variable parts OCamlPro/alt-ergo#1152)
• Add interval domains and arithmetic propagators for the BV theory ( feat(BV): Interval domains for bit-vectors  OCamlPro/alt-ergo#1058,
  feat(BV, CP): Propagators for addition and multiplication  OCamlPro/alt-ergo#1083, feat(BV, CP): Add propagators for bvudiv and bvurem OCamlPro/alt-ergo#1084, feat(BV, CP): Add propagators for bvshl and bvlshr OCamlPro/alt-ergo#1085)
• Native support for bv2nat of bit-vector normal forms (feat(BV): Add support for bv2nat/int2bv normal forms  OCamlPro/alt-ergo#1154)
• Fix incompleteness issues in the BV solver (fix(BV): Apply C-substitutions recursively OCamlPro/alt-ergo#978, fix(BV): Allow substituting constants OCamlPro/alt-ergo#979)
• Abstract more arguments of AC symbols to avoid infinite loops when
  they contain other AC symbols (fix(AC): Abstract AC arguments that contain other AC symbols OCamlPro/alt-ergo#990)
• Do not make irrelevant decisions in CDCL solver, improving
  performance slightly (feat(CDCL-Tableaux): Do not make irrelevant decisions OCamlPro/alt-ergo#1041)
• Rewrite the ADT theory to use domains and integrate the enum theory into the
  ADT theory (Refactoring Enum_rel using domains on class representatives only OCamlPro/alt-ergo#1078, ADT destructors are delayed functions OCamlPro/alt-ergo#1086, Refactoring Adt_rel using domains on class representatives only OCamlPro/alt-ergo#1087, Fix soudness bug in Enum OCamlPro/alt-ergo#1091, Merge Enum theory into ADT theory OCamlPro/alt-ergo#1094, Case splits on enum domains OCamlPro/alt-ergo#1138)
• Rewrite the Intervals module entirely (feat: Rewrite the Intervals module entirely OCamlPro/alt-ergo#1108)
• Add maximize/minimize terms for matching (Add maximize/minimize terms for matching OCamlPro/alt-ergo#1166)
• Internalize sign_extend and repeat (fix(BV): Internalize sign_extend and repeat OCamlPro/alt-ergo#1192)
• Run cross-propagators to completion (fix(BV, CP): Run cross-propagators to completion OCamlPro/alt-ergo#1221)
• Support binary distinct on arbitrary bit-widths (feat(BV): Support binary distinct on arbitrary bit-widths OCamlPro/alt-ergo#1222)
• Only perform optimization when building a model (fix(opt): Only perform optimization when building a model OCamlPro/alt-ergo#1224)
• Make sure domains do not overflow the default domain (fix(CP): Make sure domains do not overflow the default domain OCamlPro/alt-ergo#1225)
• Do not build unnormalized values in zero_extend (fix(BV): Do not build unnormalized values in zero_extend OCamlPro/alt-ergo#1226)

Internal/library changes

• Rewrite the Vec module (New vec module OCamlPro/alt-ergo#607)
• Move printer definitions closer to type definitions (Define Shostak printing immediately after type definition OCamlPro/alt-ergo#808)
• Mark proxy names as reserved (Reserve proxy names of SatML OCamlPro/alt-ergo#836)
• Use a Zarith-based representation for numbers and bit-vectors (Use ZArith-based representations for numbers and bitvectors OCamlPro/alt-ergo#850, refactor(BV): Use Z.t in BV solver OCamlPro/alt-ergo#943)
• Add native support for (bvnot) in the BV solver ([bitv] Add support for (bvnot) in the solver OCamlPro/alt-ergo#856)
• Add constant propagators for partially interpreted functions (Support delayed computation of partially interpreted functions OCamlPro/alt-ergo#869)
• Remove Util.failwith in favor of Fmt.failwith (Remove Util.failwith OCamlPro/alt-ergo#872)
• Add more Expr smart constructors (Use ZArith convention for ~$ and ~$$ OCamlPro/alt-ergo#877, Add Expr constructors for the Reals SMT-LIB theory OCamlPro/alt-ergo#878)
• Do not use existential variables for integer division (Do not use existential variables for integer division OCamlPro/alt-ergo#881)
• Preserve Subst literals to prevent accidental incompleteness (Preserve Subst literals OCamlPro/alt-ergo#886)
• Properly start timers (Starting missing timer OCamlPro/alt-ergo#924)
• Compute a concrete representation of a model instead of performing (Refactoring models representation OCamlPro/alt-ergo#925)
• Allow direct access to the SAT API in the Alt-Ergo library computations
  during printing (SAT API avaiable without process_decl in Frontend OCamlPro/alt-ergo#927)
• Better handling for step limit (Cleaner handling of step limit OCamlPro/alt-ergo#936)
• Add a generic option manager to deal with the dolmen state (Adding a generic option manager for the dolmen state OCamlPro/alt-ergo#951)
• Expose an imperative SAT API in the Alt-Ergo library (Imperative API  OCamlPro/alt-ergo#962)
• Keep track of the SMT-LIB mode (Smtlib mode mechanism OCamlPro/alt-ergo#971)
• Add ability to decide on semantic literals (feat(CDCL): Add ability to decide on semantic literals OCamlPro/alt-ergo#1027, fix(CDCL): Semantic splits are always relevant OCamlPro/alt-ergo#1118)
• Preserve trigger order when parsing quantifiers with multiple trigger
  (fix(dolmen): Preserve trigger order OCamlPro/alt-ergo#1046).
• Store domains inside the union-find module (feat(UF): Store domains inside the union-find OCamlPro/alt-ergo#1119)
• Remove some polymorphic hashtables (Remove some polymorphic hashtables OCamlPro/alt-ergo#1219)

Build and integration

• Drop support for OCaml <4.08.1 (Test AE on 4.08.1 and 4.14.1 OCamlPro/alt-ergo#803)
• Use dune-site for the inequalities plugins. External pluginsm ust now be
  registered through the dune-site plugin mechanism in the
  (alt-ergo plugins) site to be picked up by Alt-Ergo (feat(plugins): Use dune-site for inequalities plugins OCamlPro/alt-ergo#1049).
• Add a release workflow (Release workflow OCamlPro/alt-ergo#827)
• Add a Windows workflow (Restore Windows CI on Cygwin OCamlPro/alt-ergo#1203)
• Mark the dune.inc file as linguist-generated to avoid huge diffs (The file dune.inc is linguist-generated OCamlPro/alt-ergo#830)
• Use GitHub Actions badges in the README (Replace Travis badges with GitHub Actions badges in README OCamlPro/alt-ergo#882)
• Use dune build @check to build the project (Using dune build @check to build the project OCamlPro/alt-ergo#887)
• Enable warnings as errors on the CI (Warnings as errors on the CI OCamlPro/alt-ergo#888)
• Uniformization of internal identifiers generation (Uniformization of internal identifiers generation OCamlPro/alt-ergo#905, Changing the internal variables prefix OCamlPro/alt-ergo#918)
• Use an efficient String.starts_with implementation (Use efficient String.starts_with implementation OCamlPro/alt-ergo#912)
• Fix the Makefile (Fix the target all of the Makefile OCamlPro/alt-ergo#914)
• Add Logs dependency (Minimal Logs integration OCamlPro/alt-ergo#1206)
• Use dynamic_include to include the generated file dune.inc (Use dynamic_include to include the generated file dune.inc OCamlPro/alt-ergo#1199)
• Support Windows (Use Unix eof for shell scripts OCamlPro/alt-ergo#1184,Rewrite gen_link_flags in OCaml OCamlPro/alt-ergo#1189,Do not use lock file for all OCaml versions OCamlPro/alt-ergo#1195,Use dynamic_include to include the generated file dune.inc OCamlPro/alt-ergo#1199,Ignore :reproducible-resource-limit on non-Unix plateform OCamlPro/alt-ergo#1200)
• Wrap the library Alt_ergo_prelude (Wrap the library Alt_ergo_prelude OCamlPro/alt-ergo#1223)

Testing

• Use --enable-assertions in tests (Use --enable-assertions in tests OCamlPro/alt-ergo#809)
• Add a test for push/pop (Adding a test for push/pop OCamlPro/alt-ergo#843)
• Use the CDCL solver when testing model generation (Use default solver for testing models OCamlPro/alt-ergo#938)
• Do not test .smt2 files with the legacy frontend (Do not test .smt2 files with the legacy frontend OCamlPro/alt-ergo#939)
• Restore automatic creation of .expected files ([gentest] Restore automatic creation of expected files OCamlPro/alt-ergo#941)

Documentation

• Add a new example for model generation (Add a new example for model generation OCamlPro/alt-ergo#826)
• Add a Pygments lexer for the Alt-Ergo native language (Add a Pygments lexer for the Alt-Ergo language OCamlPro/alt-ergo#862)
• Update the current authors (Update the current authors OCamlPro/alt-ergo#865)
• Documentation of the Enum theory (Documentation of the Enum theory OCamlPro/alt-ergo#871)
• Document Th_util.lit_origin (Document Th_util.lit_origin OCamlPro/alt-ergo#915)
• Document the CDCL-Tableaux solver (doc(CDCL): Document the CDCL-Tableaux solver OCamlPro/alt-ergo#995)
• Document Windows support (Add documentation for Windows support OCamlPro/alt-ergo#1216)
• Remove instructions to install Alt-Ergo on Debian (Remove instructions to install AE on Debian OCamlPro/alt-ergo#1217)
• Document optimization feature (Update sphinx doc 2.6.0 OCamlPro/alt-ergo#1231)

[bclement-ocp]

Dependencies should be fixed now.

The Frama-C reverse-dependency failures seem unrelated. One mentions:

# Error: The files /home/opam/.opam/4.14/lib/lablgtk3/gWindow.cmi
#        and /home/opam/.opam/4.14/lib/ocamlgraph_gtk/graph_gtk__DGraphContainer.cmi
#        make inconsistent assumptions over interface Pango

and the other:

# /usr/bin/ld: CMakeFiles/framaCIRGen.dir/FramaCIRGen.cpp.o: undefined reference to symbol '_ZN4llvm15SmallVectorBaseIjE13mallocForGrowEmmRm@@LLVM_14'
# /usr/bin/ld: /usr/lib/llvm-14/lib/libLLVM-14.so.1: error adding symbols: DSO missing from command line
# collect2: error: ld returned 1 exit status

[mseri]

Thanks, the remain issues are unrelated. It's not the first time I see those failures, I think they are related to some concurrency bug while installing certain libraries with deopots