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

not-contains: implement not-contains > LIA reduction #168

Draft
wants to merge 24 commits into
base: devel
Choose a base branch
from
Draft

not-contains: implement not-contains > LIA reduction #168

wants to merge 24 commits into from

Commits on Aug 19, 2024

  1. not_contains: add unfinished LenDiff(lhs, rhs) implementation

    @MichalHe
    MichalHe committed Aug 19, 2024
    Configuration menu
    Copy the full SHA
    e05752a View commit details
    Browse the repository at this point in the history

Commits on Aug 20, 2024

  1. add more not_contains formulae

    @MichalHe
    MichalHe committed Aug 20, 2024
    Configuration menu
    Copy the full SHA
    9ecd797 View commit details
    Browse the repository at this point in the history

Commits on Aug 23, 2024

  1. not_contains_gen: implement length assertions and word agreements

    @MichalHe
    MichalHe committed Aug 23, 2024
    Configuration menu
    Copy the full SHA
    f26459d View commit details
    Browse the repository at this point in the history

Commits on Aug 27, 2024

  1. more work on not-contains

    @MichalHe
    MichalHe committed Aug 27, 2024
    Configuration menu
    Copy the full SHA
    0cccde9 View commit details
    Browse the repository at this point in the history

Commits on Aug 29, 2024

  1. add alternative more LIA-oriented symbol uniqueness assertion

    @MichalHe
    MichalHe committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    1094a42 View commit details
    Browse the repository at this point in the history

  2. add trace about the input diseq

    @MichalHe
    MichalHe committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    30078ef View commit details
    Browse the repository at this point in the history

  3. hook the generator into the rest of the solver

    @MichalHe
    MichalHe committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    ce43ec6 View commit details
    Browse the repository at this point in the history

  4. sat_handling: avoid adding length axiom for ca_constr

    @vhavlena
    vhavlena committed Aug 29, 2024
    Configuration menu
    Copy the full SHA
    e6b7494 View commit details
    Browse the repository at this point in the history

Commits on Aug 30, 2024

  1. quantified int variables as z3 vars; aggressive blocking for len-free… 

    … formulae
    @vhavlena
    vhavlena committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    62abf5b View commit details
    Browse the repository at this point in the history

  2. preprocess: fixing unification function for contains (overflow)

    @vhavlena
    vhavlena committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    eba6027 View commit details
    Browse the repository at this point in the history

  3. add forgotten existential quantification to not-contains

    @MichalHe
    MichalHe committed Aug 30, 2024
    Configuration menu
    Copy the full SHA
    a013bf4 View commit details
    Browse the repository at this point in the history

Commits on Sep 4, 2024

  1. formula: add export to smt2

    @MichalHe
    MichalHe committed Sep 4, 2024
    Configuration menu
    Copy the full SHA
    2d98c13 View commit details
    Browse the repository at this point in the history

  2. add forgotten assert,check-sat SMT2 commands

    @MichalHe
    MichalHe committed Sep 4, 2024
    Configuration menu
    Copy the full SHA
    f6dd504 View commit details
    Browse the repository at this point in the history

Commits on Sep 6, 2024

  1. a new internal solver for solving quantified LIA formulae

    @vhavlena
    vhavlena committed Sep 6, 2024
    Configuration menu
    Copy the full SHA
    52e7250 View commit details
    Browse the repository at this point in the history

  2. formula: do not write unary (+) nodes

    @MichalHe
    MichalHe committed Sep 6, 2024
    Configuration menu
    Copy the full SHA
    96e9110 View commit details
    Browse the repository at this point in the history

  3. nc: fix missing 2nd level parikh image

    @MichalHe
    MichalHe committed Sep 6, 2024
    Configuration menu
    Copy the full SHA
    f3ef716 View commit details
    Browse the repository at this point in the history

Commits on Sep 8, 2024

  1. reduce var assignment prior to proceeding to tag constr

    @MichalHe
    MichalHe committed Sep 8, 2024
    Configuration menu
    Copy the full SHA
    7d7134f View commit details
    Browse the repository at this point in the history

  2. debug(tag_aut): add state coloring when dumping into dot

    @MichalHe
    MichalHe committed Sep 8, 2024
    Configuration menu
    Copy the full SHA
    eb87874 View commit details
    Browse the repository at this point in the history

  3. ca_constr: avoid copying init_state offsets

    @MichalHe
    MichalHe committed Sep 8, 2024
    Configuration menu
    Copy the full SHA
    27cf5bf View commit details
    Browse the repository at this point in the history

  4. not_contains: consider only positive offsets

    @MichalHe
    MichalHe committed Sep 8, 2024
    Configuration menu
    Copy the full SHA
    a45a1c2 View commit details
    Browse the repository at this point in the history

Commits on Sep 9, 2024

  1. nc(formula): export correct formula type

    @MichalHe
    MichalHe committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    a76e1cd View commit details
    Browse the repository at this point in the history

  2. nc(formula): refactor how mismatch position is computed

    @MichalHe
    MichalHe committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    a46c719 View commit details
    Browse the repository at this point in the history

  3. ensure all straces use the same handle

    @MichalHe
    MichalHe committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    c63a7a9 View commit details
    Browse the repository at this point in the history

  4. nc: add env variable allowing to export LIA formula

    @MichalHe
    MichalHe committed Sep 9, 2024
    Configuration menu
    Copy the full SHA
    1c172ef View commit details
    Browse the repository at this point in the history