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

Refactored the define attribute on functions #236

Merged
merged 31 commits into from
Jun 4, 2020
Merged

Refactored the define attribute on functions #236

merged 31 commits into from
Jun 4, 2020

Commits on May 23, 2020

  1. fixup! Add support for function definitions

    @zvonimir
    Clark Barrett authored and zvonimir committed May 23, 2020
    Configuration menu
    Copy the full SHA
    ab5df04 View commit details
    Browse the repository at this point in the history

Commits on May 26, 2020

  1. Add support for function definitions

    @zvonimir
    Clark Barrett authored and zvonimir committed May 26, 2020
    Configuration menu
    Copy the full SHA
    f29eedd View commit details
    Browse the repository at this point in the history

  2. fixup! Add support for function definitions

    @zvonimir
    Clark Barrett authored and zvonimir committed May 26, 2020
    Configuration menu
    Copy the full SHA
    f321806 View commit details
    Browse the repository at this point in the history

  3. fixup! Add support for function definitions

    @zvonimir
    Clark Barrett authored and zvonimir committed May 26, 2020
    Configuration menu
    Copy the full SHA
    d746ece View commit details
    Browse the repository at this point in the history

  4. fixup! Add support for function definitions

    @zvonimir
    Clark Barrett authored and zvonimir committed May 26, 2020
    Configuration menu
    Copy the full SHA
    8b416f9 View commit details
    Browse the repository at this point in the history

  5. fixup! Add support for function definitions

    @zvonimir
    Clark Barrett authored and zvonimir committed May 26, 2020
    Configuration menu
    Copy the full SHA
    18e18ab View commit details
    Browse the repository at this point in the history

  6. fixup! Add support for function definitions

    @zvonimir
    Clark Barrett authored and zvonimir committed May 26, 2020
    Configuration menu
    Copy the full SHA
    a4aed19 View commit details
    Browse the repository at this point in the history

Commits on May 28, 2020

  1. Refactored support for function definitions 

    Instead of pushing definitions through encoded as axioms,
now there is a list of definitions that gets processed
separately from axioms.
    @zvonimir
    zvonimir committed May 28, 2020
    Configuration menu
    Copy the full SHA
    778d897 View commit details
    Browse the repository at this point in the history

  2. Minor fix, no need to pass false as immutable to forall constructor

    @zvonimir
    zvonimir committed May 28, 2020
    Configuration menu
    Copy the full SHA
    e61b35a View commit details
    Browse the repository at this point in the history

  3. Fixed indentation in parser

    @zvonimir
    zvonimir committed May 28, 2020
    Configuration menu
    Copy the full SHA
    d9be498 View commit details
    Browse the repository at this point in the history

  4. Moved data type processing into a separate function

    @zvonimir
    zvonimir committed May 28, 2020
    Configuration menu
    Copy the full SHA
    2cbc782 View commit details
    Browse the repository at this point in the history

  5. Moved processing of function definitions into a separate file 

    Also added two more regressions.
    @zvonimir
    zvonimir committed May 28, 2020
    Configuration menu
    Copy the full SHA
    32d5c3d View commit details
    Browse the repository at this point in the history

  6. Prevent function arguments from being declared in SMT queries 

    When function definition body is walked over to turn it into
SMT format, variables are being picked up and subsequently
declared. We should avoid this since they are in fact
function arguments and hence do not need declarations.
    @zvonimir
    zvonimir committed May 28, 2020
    Configuration menu
    Copy the full SHA
    5fabe6f View commit details
    Browse the repository at this point in the history

  7. Cleaned up the code and added some comments

    @zvonimir
    zvonimir committed May 28, 2020
    Configuration menu
    Copy the full SHA
    d6820fe View commit details
    Browse the repository at this point in the history

Commits on May 29, 2020

  1. Fixed a problem with missing function definition dependencies 

    Dependencies found in function definitions were printed after
the definitions themselves in the generated VCs, which led
to missing declaration errors. I am now flushing dependencies
before printing function definitions.
    @zvonimir
    zvonimir committed May 29, 2020
    Configuration menu
    Copy the full SHA
    c45d561 View commit details
    Browse the repository at this point in the history

  2. Renamed DefBody into DefinitionBody

    @zvonimir
    zvonimir committed May 29, 2020
    Configuration menu
    Copy the full SHA
    770b21b View commit details
    Browse the repository at this point in the history

  3. Function cannot have both inline and define enabled

    @zvonimir
    zvonimir committed May 29, 2020
    Configuration menu
    Copy the full SHA
    6fae2eb View commit details
    Browse the repository at this point in the history

  4. Added assertions and more comments

    @zvonimir
    zvonimir committed May 29, 2020
    Configuration menu
    Copy the full SHA
    2978973 View commit details
    Browse the repository at this point in the history

  5. Added more complex regressions that use function definitions

    @zvonimir
    zvonimir committed May 29, 2020
    Configuration menu
    Copy the full SHA
    2dbc8c3 View commit details
    Browse the repository at this point in the history

  6. Added more regressions

    @zvonimir
    zvonimir committed May 29, 2020
    Configuration menu
    Copy the full SHA
    a3f14e4 View commit details
    Browse the repository at this point in the history

  7. Minor fix since I messed up expected output for a regression

    @zvonimir
    zvonimir committed May 29, 2020
    Configuration menu
    Copy the full SHA
    11d834f View commit details
    Browse the repository at this point in the history

  8. Merge branch 'master' into define-func

    @zvonimir
    zvonimir committed May 29, 2020
    Configuration menu
    Copy the full SHA
    c3c56bf View commit details
    Browse the repository at this point in the history

  9. Fixed expected regression results based on updates to CIVL

    @zvonimir
    zvonimir committed May 29, 2020
    Configuration menu
    Copy the full SHA
    440921e View commit details
    Browse the repository at this point in the history

  10. Merge branch 'master' into define-func

    @zvonimir
    zvonimir committed May 29, 2020
    Configuration menu
    Copy the full SHA
    c3a1f48 View commit details
    Browse the repository at this point in the history

  11. Added useArrayTheory to SMACK regression that uses function definitions 

    I added the same option to the function inline version when
I updated Z3.
    @zvonimir
    zvonimir committed May 29, 2020
    Configuration menu
    Copy the full SHA
    b90bb21 View commit details
    Browse the repository at this point in the history

  12. Function definitions work only with monomorphic functions 

    As for now, I haven't managed to get it to work with polymorphic
functions. This is a TODO for future work.
    @zvonimir
    zvonimir committed May 29, 2020
    Configuration menu
    Copy the full SHA
    7795d0f View commit details
    Browse the repository at this point in the history

  13. Added checking and error reporting for polymorphic functions 

    Currently definition of polymorphic functions is not supported.
    @zvonimir
    zvonimir committed May 29, 2020
    Configuration menu
    Copy the full SHA
    719c84f View commit details
    Browse the repository at this point in the history

Commits on Jun 2, 2020

  1. Minor fix to wording of error messages

    @zvonimir
    zvonimir committed Jun 2, 2020
    Configuration menu
    Copy the full SHA
    723f921 View commit details
    Browse the repository at this point in the history

  2. Added regression that checks for recursion in function definitions

    @zvonimir
    zvonimir committed Jun 2, 2020
    Configuration menu
    Copy the full SHA
    83bbd83 View commit details
    Browse the repository at this point in the history

Commits on Jun 3, 2020

  1. Minor fix

    @zvonimir
    zvonimir committed Jun 3, 2020
    Configuration menu
    Copy the full SHA
    6728ce2 View commit details
    Browse the repository at this point in the history

  2. Check for function monomorphism before creating definition body

    @zvonimir
    zvonimir committed Jun 3, 2020
    Configuration menu
    Copy the full SHA
    5260c33 View commit details
    Browse the repository at this point in the history