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

Iterative term printer #421

Draft
wants to merge 7 commits into
base: master
Choose a base branch
from
Draft

Iterative term printer #421

wants to merge 7 commits into from

Commits on Mar 31, 2022

  1. Logic: make abstract value counter member of logic

    @aehyvari
    aehyvari committed Mar 31, 2022
    Configuration menu
    Copy the full SHA
    144e659 View commit details
    Browse the repository at this point in the history

Commits on Apr 1, 2022

  1. Logic: C.45 style initialization of abstract value

    @aehyvari
    aehyvari committed Apr 1, 2022
    Configuration menu
    Copy the full SHA
    d1a5591 View commit details
    Browse the repository at this point in the history

  2. TermPrinter: Some unit tests

    @aehyvari
    aehyvari committed Apr 1, 2022
    Configuration menu
    Copy the full SHA
    ddc06eb View commit details
    Browse the repository at this point in the history

  3. Interpret: Use the new TermPrinter for printing models and interpolants

    @aehyvari
    aehyvari committed Apr 1, 2022
    Configuration menu
    Copy the full SHA
    562efb5 View commit details
    Browse the repository at this point in the history

  4. TermPrinter: the initial version of DAG printer

    @aehyvari
    aehyvari committed Apr 1, 2022
    Configuration menu
    Copy the full SHA
    6ddef12 View commit details
    Browse the repository at this point in the history

  5. TermPrinter: Guarantee unique let variable names 

    For a let term
`(let ((l1 phi1) ... (ln phin)) psi[l1/phi1 ...  ln/phin])`
it must not be the case that `li` appears in `psi[l1/phi1 ...  ln/phin]`
as a free variable.  This commit guarantees this by introducing a let
prefix in `Logic` and modifying it whenever a new variable is introduced
such that its name is a proper prefix of the current let prefix.

The current let prefix is modified by postfixing it with a character
different from the first character after the proper prefix in the new
variable.
    @aehyvari
    aehyvari committed Apr 1, 2022
    Configuration menu
    Copy the full SHA
    c3e5cef View commit details
    Browse the repository at this point in the history

  6. TermPrinter: test for correct let var naming

    @aehyvari
    aehyvari committed Apr 1, 2022
    Configuration menu
    Copy the full SHA
    394f360 View commit details
    Browse the repository at this point in the history