Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Smt changes #70

Merged
merged 101 commits into from
Feb 26, 2024
Merged

Smt changes #70

merged 101 commits into from
Feb 26, 2024

Commits on Nov 15, 2022

  1. Replaced test/fast/smt_tests bu unit/ and bugs/

    adef committed Nov 15, 2022
    Configuration menu
    Copy the full SHA
    b230794 View commit details
    Browse the repository at this point in the history

  2. Made hyp_hint available

    adef committed Nov 15, 2022
    Configuration menu
    Copy the full SHA
    07f71e4 View commit details
    Browse the repository at this point in the history

  3. Facts may be named and marked as axioms, hyps,...

    adef committed Nov 15, 2022
    Configuration menu
    Copy the full SHA
    7724ee3 View commit details
    Browse the repository at this point in the history

  4. SMT-LIB patterns

    adef committed Nov 15, 2022
    Configuration menu
    Copy the full SHA
    e8c54bc View commit details
    Browse the repository at this point in the history

  5. Made ssnoc and app_hyps from Expr.Subst visible

    adef committed Nov 15, 2022
    Configuration menu
    Copy the full SHA
    bbf5f1f View commit details
    Browse the repository at this point in the history

  6. New expression visitors: foldmap and fold

    adef committed Nov 15, 2022
    Configuration menu
    Copy the full SHA
    557bb55 View commit details
    Browse the repository at this point in the history

  7. Option.fold

    adef committed Nov 15, 2022
    Configuration menu
    Copy the full SHA
    88a71ae View commit details
    Browse the repository at this point in the history

  8. Sets and Maps of integers

    adef committed Nov 15, 2022
    Configuration menu
    Copy the full SHA
    291ce04 View commit details
    Browse the repository at this point in the history

  9. builtin_to_string

    adef committed Nov 15, 2022
    Configuration menu
    Copy the full SHA
    f93c594 View commit details
    Browse the repository at this point in the history

  10. Expr.Collect for computing sets of free variables

    adef committed Nov 15, 2022
    Configuration menu
    Copy the full SHA
    1d7f8ee View commit details
    Browse the repository at this point in the history

  11. Fixed a bug in smt.ml that made verbosity ignored

    adef committed Nov 15, 2022
    Configuration menu
    Copy the full SHA
    289a573 View commit details
    Browse the repository at this point in the history

  12. Display obligation number in isabelle output

    adef committed Nov 15, 2022
    Configuration menu
    Copy the full SHA
    30fed8c View commit details
    Browse the repository at this point in the history

  13. Package Type: type system utilities

    adef committed Nov 15, 2022
    Configuration menu
    Copy the full SHA
    2480ac7 View commit details
    Browse the repository at this point in the history

  14. Package Encode: new SMT and TPTP encoding

    adef committed Nov 15, 2022
    Configuration menu
    Copy the full SHA
    b39335b View commit details
    Browse the repository at this point in the history

  15. New translation to SMT-LIB 

    The old version is still here, use it with the flag
    --debug oldsmt
    adef committed Nov 15, 2022
    Configuration menu
    Copy the full SHA
    8b13372 View commit details
    Browse the repository at this point in the history

  16. New translation to TPTP + Support Zipperposition 

    Usage:
- 'BY Zipper' or 'BY Zipper(T)' in TLAPS
- '--method zipper' in command-line
    adef committed Nov 15, 2022
    Configuration menu
    Copy the full SHA
    3842f53 View commit details
    Browse the repository at this point in the history

  17. FIXUP: SMT translation

    adef committed Nov 15, 2022
    Configuration menu
    Copy the full SHA
    3f08478 View commit details
    Browse the repository at this point in the history

Commits on Nov 16, 2022

  1. Improved obligation display in temp files

    adef committed Nov 16, 2022
    Configuration menu
    Copy the full SHA
    81695a3 View commit details
    Browse the repository at this point in the history

Commits on Jan 5, 2023

  1. Heuristics for set extensionality (SMT)

    adef committed Jan 5, 2023
    Configuration menu
    Copy the full SHA
    7caaa98 View commit details
    Browse the repository at this point in the history

Commits on Jan 10, 2023

  1. Mode "ext" for SMT is default

    adef committed Jan 10, 2023
    Configuration menu
    Copy the full SHA
    39a981d View commit details
    Browse the repository at this point in the history

  2. Compare all pairs of refinement sets (heuristics)

    adef committed Jan 10, 2023
    Configuration menu
    Copy the full SHA
    8450a8c View commit details
    Browse the repository at this point in the history

Commits on Jan 17, 2023

  1. Use flag --smt-logic for new SMT encoding

    adef committed Jan 17, 2023
    Configuration menu
    Copy the full SHA
    7a1f96a View commit details
    Browse the repository at this point in the history

Commits on Jan 20, 2023

  1. Use CVC4 for one regression test

    adef committed Jan 20, 2023
    Configuration menu
    Copy the full SHA
    0bdb217 View commit details
    Browse the repository at this point in the history

Commits on Mar 24, 2023

  1. Update src/util/util.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    a97d4f9 View commit details
    Browse the repository at this point in the history

  2. Update src/type/t_visit.mlt 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    c10b19d View commit details
    Browse the repository at this point in the history

  3. Update src/type/t_visit.mli 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    0e323ce View commit details
    Browse the repository at this point in the history

  4. Update src/encode/n_axioms.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    194f684 View commit details
    Browse the repository at this point in the history

  5. Update src/type/t_t.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    b887a09 View commit details
    Browse the repository at this point in the history

  6. Update src/encode/n_axioms.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    9835c02 View commit details
    Browse the repository at this point in the history

  7. Update src/encode/n_axioms.mli 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    d02264d View commit details
    Browse the repository at this point in the history

  8. Update src/encode/n_axioms.mlt 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    ddfb7a0 View commit details
    Browse the repository at this point in the history

  9. Update src/type/t_visit.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    e0f2cb5 View commit details
    Browse the repository at this point in the history

  10. Update src/type/t_t.mlt 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    c38dfea View commit details
    Browse the repository at this point in the history

  11. Update src/type/t_t.mli 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    68e0be8 View commit details
    Browse the repository at this point in the history

  12. Update src/type/t_t.mli 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    dbfee1b View commit details
    Browse the repository at this point in the history

  13. Update src/type/t_t.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    6b92292 View commit details
    Browse the repository at this point in the history

  14. Update src/type/t_t.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    162ccd6 View commit details
    Browse the repository at this point in the history

  15. Update src/type/t_synth.mlt 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    0574dca View commit details
    Browse the repository at this point in the history

  16. Update src/type/t_synth.mli 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    13ca6b7 View commit details
    Browse the repository at this point in the history

  17. Update src/type/t_synth.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    7590d73 View commit details
    Browse the repository at this point in the history

  18. Update src/backend/smtlib.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    ad5bdd8 View commit details
    Browse the repository at this point in the history

  19. Update src/backend/smtlib.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    3bdf983 View commit details
    Browse the repository at this point in the history

  20. Update src/backend/smtlib.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    99958b0 View commit details
    Browse the repository at this point in the history

  21. Update src/backend/smtlib.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    ee43771 View commit details
    Browse the repository at this point in the history

  22. Update src/backend/smtlib.mli 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    1bf5947 View commit details
    Browse the repository at this point in the history

  23. Update src/backend/smtlib.mlt 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    946976b View commit details
    Browse the repository at this point in the history

  24. Update src/type.mlt 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    9c9e87a View commit details
    Browse the repository at this point in the history

  25. Update src/backend/thf.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    25a88a3 View commit details
    Browse the repository at this point in the history

  26. Update src/backend/thf.mli 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    6def4dc View commit details
    Browse the repository at this point in the history

  27. Update src/backend/thf.mlt 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    56c9fd2 View commit details
    Browse the repository at this point in the history

  28. Update src/encode.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    f3403e9 View commit details
    Browse the repository at this point in the history

  29. Update src/encode.mli 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    cf20454 View commit details
    Browse the repository at this point in the history

  30. Update src/encode.mlt 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    76b253a View commit details
    Browse the repository at this point in the history

  31. Update src/encode/n_axiomatize.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    f791c16 View commit details
    Browse the repository at this point in the history

  32. Update src/encode/n_axiomatize.mlt 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    77ed9c2 View commit details
    Browse the repository at this point in the history

  33. Update src/type/t_hyps.mlt 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    fd4ffbd View commit details
    Browse the repository at this point in the history

  34. Update src/type/t_collect.mlt 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Mar 24, 2023
    Configuration menu
    Copy the full SHA
    14395c0 View commit details
    Browse the repository at this point in the history

  35. Really disable option ext by default

    adef committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    25b41fd View commit details
    Browse the repository at this point in the history

  36. Update (first corrections)

    adef committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    20a4949 View commit details
    Browse the repository at this point in the history

  37. Update: copyright dates

    adef committed Mar 24, 2023
    Configuration menu
    Copy the full SHA
    0c32478 View commit details
    Browse the repository at this point in the history

Commits on Apr 20, 2023

  1. Update: Two missing axioms

    adef committed Apr 20, 2023
    Configuration menu
    Copy the full SHA
    ad0dd83 View commit details
    Browse the repository at this point in the history

Commits on Apr 25, 2023

  1. Fix: typing of the remainder for SMT

    adef committed Apr 25, 2023
    Configuration menu
    Copy the full SHA
    189902d View commit details
    Browse the repository at this point in the history

Commits on May 11, 2023

  1. Some missing axioms/triggers

    adef committed May 11, 2023
    Configuration menu
    Copy the full SHA
    663ab4b View commit details
    Browse the repository at this point in the history

Commits on Aug 9, 2023

  1. Update src/encode/n_flatten.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Aug 9, 2023
    Configuration menu
    Copy the full SHA
    6fad153 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/smt-changes' into smt-changes

    adef committed Aug 9, 2023
    Configuration menu
    Copy the full SHA
    71ac023 View commit details
    Browse the repository at this point in the history

  3. Update src/encode/n_rewrite.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Aug 9, 2023
    Configuration menu
    Copy the full SHA
    bac315e View commit details
    Browse the repository at this point in the history

  4. Update src/encode/n_hints.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Aug 9, 2023
    Configuration menu
    Copy the full SHA
    1391208 View commit details
    Browse the repository at this point in the history

  5. Update src/encode/n_hints.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Aug 9, 2023
    Configuration menu
    Copy the full SHA
    2232105 View commit details
    Browse the repository at this point in the history

  6. Update src/encode/n_rewrite.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Aug 9, 2023
    Configuration menu
    Copy the full SHA
    29324d2 View commit details
    Browse the repository at this point in the history

  7. Update src/encode/n_rewrite.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @damiendoligez
    adef-inr and damiendoligez authored Aug 9, 2023
    Configuration menu
    Copy the full SHA
    0e2eb5c View commit details
    Browse the repository at this point in the history

  8. Merge remote-tracking branch 'origin/smt-changes' into smt-changes

    adef committed Aug 9, 2023
    Configuration menu
    Copy the full SHA
    b58de26 View commit details
    Browse the repository at this point in the history

  9. Some fixes

    adef committed Aug 9, 2023
    Configuration menu
    Copy the full SHA
    e9d55ab View commit details
    Browse the repository at this point in the history

Commits on Jan 24, 2024

  1. Update src/encode/n_axioms.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @rozlynd @damiendoligez
    rozlynd and damiendoligez authored Jan 24, 2024
    Configuration menu
    Copy the full SHA
    70c8eed View commit details
    Browse the repository at this point in the history

  2. Update src/encode/n_data.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @rozlynd @damiendoligez
    rozlynd and damiendoligez authored Jan 24, 2024
    Configuration menu
    Copy the full SHA
    6727f33 View commit details
    Browse the repository at this point in the history

  3. Update src/encode/n_data.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @rozlynd @damiendoligez
    rozlynd and damiendoligez authored Jan 24, 2024
    Configuration menu
    Copy the full SHA
    af76167 View commit details
    Browse the repository at this point in the history

  4. Update src/encode/n_data.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @rozlynd @damiendoligez
    rozlynd and damiendoligez authored Jan 24, 2024
    Configuration menu
    Copy the full SHA
    0a450ad View commit details
    Browse the repository at this point in the history

  5. Update src/type/t_synth.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @rozlynd @damiendoligez
    rozlynd and damiendoligez authored Jan 24, 2024
    Configuration menu
    Copy the full SHA
    4cf25fc View commit details
    Browse the repository at this point in the history

  6. Update src/type/t_synth.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @rozlynd @damiendoligez
    rozlynd and damiendoligez authored Jan 24, 2024
    Configuration menu
    Copy the full SHA
    25fdb66 View commit details
    Browse the repository at this point in the history

  7. Update src/type/t_synth.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @rozlynd @damiendoligez
    rozlynd and damiendoligez authored Jan 24, 2024
    Configuration menu
    Copy the full SHA
    3a4c947 View commit details
    Browse the repository at this point in the history

  8. Update src/type/t_synth.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @rozlynd @damiendoligez
    rozlynd and damiendoligez authored Jan 24, 2024
    Configuration menu
    Copy the full SHA
    b5b1a89 View commit details
    Browse the repository at this point in the history

  9. Update src/type/t_synth.ml 

    Co-authored-by: Damien Doligez <[email protected]>
    @rozlynd @damiendoligez
    rozlynd and damiendoligez authored Jan 24, 2024
    Configuration menu
    Copy the full SHA
    e1bcb89 View commit details
    Browse the repository at this point in the history

Commits on Jan 25, 2024

  1. fix laziness

    @damiendoligez @rozlynd
    damiendoligez authored and rozlynd committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    e0ce4e6 View commit details
    Browse the repository at this point in the history

  2. Removed unused module Encode.Hints

    @rozlynd
    rozlynd committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    7c13511 View commit details
    Browse the repository at this point in the history

  3. Fixed polarities in Encode.Rewriting

    @rozlynd
    rozlynd committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    159f728 View commit details
    Browse the repository at this point in the history

  4. Fix: And/Or lists with one member collapse 

    This raised an error with cvc5
    @rozlynd
    rozlynd committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    7b76a69 View commit details
    Browse the repository at this point in the history

  5. Clarification that tla_smb_desc is NOT injective 

    Renamed the function, previously "tla_smb_to_string"
    @rozlynd
    rozlynd committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    54915f6 View commit details
    Browse the repository at this point in the history

  6. Fix: Infinity is not a real

    @rozlynd
    rozlynd committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    2e2ee94 View commit details
    Browse the repository at this point in the history

  7. Fix duplicate case in T.Synth

    @rozlynd
    rozlynd committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    fdb9c09 View commit details
    Browse the repository at this point in the history

  8. Use subclass of Subst.map insteadof duplicate code

    @rozlynd
    rozlynd committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    93ca710 View commit details
    Browse the repository at this point in the history

  9. Factor special characters replacement in Thf/SMT

    @rozlynd
    rozlynd committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    01e2e61 View commit details
    Browse the repository at this point in the history

  10. Fixed contradictory assert in Expr.Subst

    @rozlynd
    rozlynd committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    198a64a View commit details
    Browse the repository at this point in the history

  11. Factored expansion of set extensionality fcn

    @rozlynd
    rozlynd committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    11922d8 View commit details
    Browse the repository at this point in the history

  12. Set equalities in negative contexts are unchanged

    @rozlynd
    rozlynd committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    378fd47 View commit details
    Browse the repository at this point in the history

  13. Fixed/Rephrased some comments

    @rozlynd
    rozlynd committed Jan 25, 2024
    Configuration menu
    Copy the full SHA
    ac759fa View commit details
    Browse the repository at this point in the history

Commits on Jan 26, 2024

  1. Fixed exponentation symbol for SMT 

    m^n is specified for m,n:int iff m # 0 OR n > 0

The operator has no counterpart in SMT, and no axiom is provided for
reasoning, but at least we cannot prove statements like 0^(-1) \in Int.
    @rozlynd
    rozlynd committed Jan 26, 2024
    Configuration menu
    Copy the full SHA
    035c39d View commit details
    Browse the repository at this point in the history

  2. Removed global use of debug flags in encode/ 

    Flag "nonewqut" not supported anymore

Flag "noarith" renamed to "disable_arithmetic"; always true for
Zipperposition

Flag "no_smt_set_extensionality" disables the special use of SMT
triggers for the axiom of set extensionality
    @rozlynd
    rozlynd committed Jan 26, 2024
    Configuration menu
    Copy the full SHA
    86ffa20 View commit details
    Browse the repository at this point in the history

Commits on Jan 31, 2024

  1. Merge branch 'main' into smt-changes

    @rozlynd
    rozlynd committed Jan 31, 2024
    Configuration menu
    Copy the full SHA
    f7c1d60 View commit details
    Browse the repository at this point in the history

Commits on Feb 7, 2024

  1. Change Pervasives to Stdlib to make the source compatible with OC… 

    …aml 5.

Signed-off-by: Damien Doligez <[email protected]>
    @damiendoligez
    damiendoligez committed Feb 7, 2024
    Configuration menu
    Copy the full SHA
    5f5a285 View commit details
    Browse the repository at this point in the history

Commits on Feb 13, 2024

  1. tweak proof in GFX_test.tla

    @damiendoligez
    damiendoligez committed Feb 13, 2024
    Configuration menu
    Copy the full SHA
    783df0a View commit details
    Browse the repository at this point in the history

  2. display more details in case of a failed test

    @damiendoligez
    damiendoligez committed Feb 13, 2024
    Configuration menu
    Copy the full SHA
    4f43abb View commit details
    Browse the repository at this point in the history

  3. We don't ship CVC4 in our bundled provers, and nowadays Z3 can handle… 

    … this obligation just fine.
    @damiendoligez
    damiendoligez committed Feb 13, 2024
    Configuration menu
    Copy the full SHA
    7a62b05 View commit details
    Browse the repository at this point in the history