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

Tools/nelson oppen (not ready for review) #28

Open
wants to merge 84 commits into
base: master
Choose a base branch
from
Open

Tools/nelson oppen (not ready for review) #28

wants to merge 84 commits into from

Commits on Sep 27, 2018

  1. varsat/meta-aux: Stub out file

    @nishantjr
    nishantjr authored and Everett Hildenbrandt committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    89ed827 View commit details
    Browse the repository at this point in the history

  2. varsat/foform => meta/foform: update meta/foform; have varsat/foform … 

    …load it
    @nishantjr
    nishantjr authored and Everett Hildenbrandt committed Sep 27, 2018
    Configuration menu
    Copy the full SHA
    d6f0cb5 View commit details
    Browse the repository at this point in the history

Commits on Sep 28, 2018

  1. meta/{foform,kind-ops} varsat/var-sat: Atom -> Lit

    @nishantjr
    nishantjr authored and Everett Hildenbrandt committed Sep 28, 2018
    Configuration menu
    Copy the full SHA
    10a9a83 View commit details
    Browse the repository at this point in the history

  2. meta/foform: split QFFOFORM from FOFORM

    Everett Hildenbrandt committed Sep 28, 2018
    Configuration menu
    Copy the full SHA
    94f3816 View commit details
    Browse the repository at this point in the history

  3. meta/foform: split QFFOFORMSET from FOFORMSET

    Everett Hildenbrandt committed Sep 28, 2018
    Configuration menu
    Copy the full SHA
    2ec0c39 View commit details
    Browse the repository at this point in the history

  4. varsat/{var-sat,numbers}: switch pr FOFORM => QFFOFORM .

    Everett Hildenbrandt committed Sep 28, 2018
    Configuration menu
    Copy the full SHA
    cd267b4 View commit details
    Browse the repository at this point in the history

  5. meta/foform: split QFFORM-OPERATIONS from FOFORM-OPERATIONS

    Everett Hildenbrandt committed Sep 28, 2018
    Configuration menu
    Copy the full SHA
    90458d5 View commit details
    Browse the repository at this point in the history

  6. meta/foform, varsat/var-sat: restrict more modules to QFForm

    Everett Hildenbrandt committed Sep 28, 2018
    Configuration menu
    Copy the full SHA
    159ad83 View commit details
    Browse the repository at this point in the history

  7. meta/foform: split QFFOFORM-SUBSTITUTION from FOFORM-SUBSTITUTION

    Everett Hildenbrandt committed Sep 28, 2018
    Configuration menu
    Copy the full SHA
    997c88c View commit details
    Browse the repository at this point in the history

  8. meta/foform: more than just renamings allowed in FOForm substitutions

    Everett Hildenbrandt committed Sep 28, 2018
    Configuration menu
    Copy the full SHA
    48c3e41 View commit details
    Browse the repository at this point in the history

  9. meta/foform: lower FOFORMSUBSTITUTION-PAIR to QFFOFORMSUBSTITUTION-PAIR

    Everett Hildenbrandt committed Sep 28, 2018
    Configuration menu
    Copy the full SHA
    7f7b63f View commit details
    Browse the repository at this point in the history

  10. meta/foform, varsat/var-sat: lower FOFORM-SUBSTITUTIONSET => QFFOFORM… 

    …-SUBSTITUTIONSET
    Everett Hildenbrandt committed Sep 28, 2018
    Configuration menu
    Copy the full SHA
    6c9f704 View commit details
    Browse the repository at this point in the history

  11. meta/foform, varsat/var-sat: split QFFOFORM-DEFINEDOPS from FOFORM-DE… 

    …FINEDOPS
    Everett Hildenbrandt committed Sep 28, 2018
    Configuration menu
    Copy the full SHA
    6764d0c View commit details
    Browse the repository at this point in the history

  12. meta/foform, varsat/var-sat: split QFFOFORMSIMPLIFY(-IMPL) from FOFOR… 

    …MSIMPLIFY(-IMPL)
    Everett Hildenbrandt committed Sep 28, 2018
    Configuration menu
    Copy the full SHA
    c150020 View commit details
    Browse the repository at this point in the history

Commits on Sep 29, 2018

  1. tests/.../meta/eqform: flesh out testing harness module

    @nishantjr
    nishantjr authored and Everett Hildenbrandt committed Sep 29, 2018
    Configuration menu
    Copy the full SHA
    19a6e3e View commit details
    Browse the repository at this point in the history

  2. meta/eqform: EQFORM-OPERATIONS: Port wellFormed, normalize, vars and … 

    …toUnifProb
    @nishantjr
    nishantjr authored and Everett Hildenbrandt committed Sep 29, 2018
    Configuration menu
    Copy the full SHA
    398814d View commit details
    Browse the repository at this point in the history

  3. meta/eqform: add reduce and tests

    Everett Hildenbrandt committed Sep 29, 2018
    Configuration menu
    Copy the full SHA
    c0f83b8 View commit details
    Browse the repository at this point in the history

  4. meta/eqform: port {QFFO => EQ}FORM-SET-OPERATIONS

    Everett Hildenbrandt committed Sep 29, 2018
    Configuration menu
    Copy the full SHA
    49d56a0 View commit details
    Browse the repository at this point in the history

  5. varsat/var-sat: minimize imports

    Everett Hildenbrandt committed Sep 29, 2018
    Configuration menu
    Copy the full SHA
    d82a48a View commit details
    Browse the repository at this point in the history

  6. meta/eqform: lift _<<_ to FormSet, SubstitutionSet

    Everett Hildenbrandt committed Sep 29, 2018
    Configuration menu
    Copy the full SHA
    f611f3a View commit details
    Browse the repository at this point in the history

Commits on Sep 30, 2018

  1. meta/eqform: more trivial simplifications

    Everett Hildenbrandt committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    d90ba9e View commit details
    Browse the repository at this point in the history

  2. meta/eqform: mark partial functions

    Everett Hildenbrandt committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    5006db2 View commit details
    Browse the repository at this point in the history

  3. varsat/var-sat: remove call to simplify which does not affect the tests

    Everett Hildenbrandt committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    f0abd87 View commit details
    Browse the repository at this point in the history

  4. tests/.../varsat/var-sat: more tests

    Everett Hildenbrandt committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    56419b6 View commit details
    Browse the repository at this point in the history

  5. varsat/var-sat: switch over to depending on EQFORM

    Everett Hildenbrandt committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    29b83b4 View commit details
    Browse the repository at this point in the history

  6. !!! var-sat query that gets stuck. 

    Note that changing it to 'false.Bool ?= upTerm(X + X < Y + Y)
    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    9e0a301 View commit details
    Browse the repository at this point in the history

  7. tools/meta/nelson-oppen-combination: tangle and testing infrastructure

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    efb382a View commit details
    Browse the repository at this point in the history

  8. tests/nelson-oppen-combination: Begin implementation

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    ea0b29c View commit details
    Browse the repository at this point in the history

  9. tools/nelson-oppen-combination: simplify $no.tagged -> $no.basicSat

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    29f7aea View commit details
    Browse the repository at this point in the history

  10. tools/nelson-oppen-combination: $nosat.simplified => $nosat.dnf

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    398a959 View commit details
    Browse the repository at this point in the history

  11. tools/nelson-oppen-combination: Write some documentation 

    We also mark the code blocks we want in the thesis document with a class so we can filter on them.
    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    c60601e View commit details
    Browse the repository at this point in the history

  12. tools/nelson-oppen-combination: and-then is more readable than `if_… 

    …then_else`
    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    65497ec View commit details
    Browse the repository at this point in the history

  13. tools/nelson-oppen-combination: TaggedFormulaSet uses semicolon for u… 

    …nion to reduce ambiguities
    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    15a5d99 View commit details
    Browse the repository at this point in the history

  14. tools/nelson-oppen-combination: More if_then_else => and-then

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    8e248f1 View commit details
    Browse the repository at this point in the history

  15. tools/nelson-oppen-combination: Only split for theories tagged 'conve… 

    …x > 'false

If there is no `'convex` tag, we add one marking it non-convex.
    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    500e365 View commit details
    Browse the repository at this point in the history

  16. tools/nelson-oppen-combination: Rename make-equalities => candidate-e… 

    …qualities
    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    86b9f96 View commit details
    Browse the repository at this point in the history

  17. tools/nelson-oppen-combination: Rename var DISJ? => CANDEQ to ref… 

    …ect text in thesis
    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    35aeec0 View commit details
    Browse the repository at this point in the history

  18. tools/nelson-oppen-combination: Document inteference rules

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    2b91365 View commit details
    Browse the repository at this point in the history

  19. tests/nelson-oppen-combination: Split the integer-list combination te… 

    …sts to own file
    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    7887139 View commit details
    Browse the repository at this point in the history

  20. nelson-oppen-uninterpreted-funcs: Demonstration of NO with uninterpre… 

    …ted functions
    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    fd4017c View commit details
    Browse the repository at this point in the history

  21. nelson-oppen-matrix example

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    f06dd44 View commit details
    Browse the repository at this point in the history

  22. ! src/Mixfix/yices2_Bindings.cc: Change yices config to allow nonline… 

    …ar real arithmetic

This uses the MCSAT solver which requires the `one-shot` mode.
    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    68a0daf View commit details
    Browse the repository at this point in the history

  23. systems/nelson-oppen: example showing "all real invertible matrices h… 

    …ave det != 0"
    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    4e906e4 View commit details
    Browse the repository at this point in the history

  24. TTT meta/cterms: purify: Handle breaking of disequalities

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    f625e66 View commit details
    Browse the repository at this point in the history

  25. tools/nelson-oppen-combination: foform-to-smt: Convert tt to 'true

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    799005e View commit details
    Browse the repository at this point in the history

  26. meta/nelson-oppen: Print attribute for all inference steps 

    Also allow easy enabling of smt/var-sat checks (these are commented to reduce output)
    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    c5a5530 View commit details
    Browse the repository at this point in the history

  27. meta/nelson-oppen-combination: When vars are identified, substitute o… 

    …ne of the variables with the other

This reduces the number of candidate equalities we need to try.
    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    232e0fa View commit details
    Browse the repository at this point in the history

  28. meta/nelson-oppen-combination: addConvexTag: Be more discriminating a… 

    …bout typos in the convex tag value
    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    8cdd027 View commit details
    Browse the repository at this point in the history

  29. meta/nelson-oppen-combination: Add nelson-oppen-valid

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    f0044bd View commit details
    Browse the repository at this point in the history

  30. old matrix

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    c24790a View commit details
    Browse the repository at this point in the history

  31. uninterpreted-funcs -> uninterpreted-bijections

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    16fee1e View commit details
    Browse the repository at this point in the history

  32. nelson-oppen: foform-to-smt: 'tt.Bool* is not part of FOForm

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    cab3ec3 View commit details
    Browse the repository at this point in the history

  33. TTT meta/cterms: break-eqatoms: Generate additional extra variables t… 

    …o capture implicit equalities
    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    45b0007 View commit details
    Browse the repository at this point in the history

  34. TTT meta/purification: Handle some TruthAtoms

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    282dc5a View commit details
    Browse the repository at this point in the history

  35. GAUSIAN-INT, text

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    bfbc17f View commit details
    Browse the repository at this point in the history

  36. Remove failed experiments

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    9387b14 View commit details
    Browse the repository at this point in the history

  37. contrib/systems.md/hereditarily-finite-set.md: Non-trivial example of… 

    … integrating nelson-oppen-sat and var-sat

!!! hereditarily-finite-set: Add equation needed for variant generation

I'm not sure why this is needed (it is implied by `M,M=M` and `comm`)
but it is mentioned in the paper too.

hereditarily-finite-set: Documentation for thesis

hereditarily-finite-set: Remove unused Elt sort

Rename  HEREDITARILY-FINITE-SET-COUNTABLE-X => REAL-HEREDITARILY-FINITE-SET

!!! HFS: Change test to use { } instead of empty  (Why?)

HFS: Formatting

HFS: More docs for thesis

!!! Rename 'REAL-HEREDITARILY-FINITE-SET  => 'HFS-REAL

Weird issue where purify would fail if module name has "REAL" as prefix

HFS: Fix sanity checks
    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    10e5d60 View commit details
    Browse the repository at this point in the history

  38. update text

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    a873ae9 View commit details
    Browse the repository at this point in the history

  39. integer-list: text; example checks validity instead of satisfiability

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    fb3de19 View commit details
    Browse the repository at this point in the history

  40. test/Misc/Makefile: smtTest fails with Yices' MCSAT

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    b6f2be5 View commit details
    Browse the repository at this point in the history

  41. lexical-trichotomy: Failed example (purification does not support cto… 

    …rs shared accross theories)

In particular  'X:Real < 'Y:Real ?= 'true  doesn't get split in a way that is shared between the theories
    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    e94a55e View commit details
    Browse the repository at this point in the history

  42. tests/systems/nelson-oppen: Own Makefile.am

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    7a3fc86 View commit details
    Browse the repository at this point in the history

  43. tests/systems/nelson-oppen: empty expected files

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    4df4dd9 View commit details
    Browse the repository at this point in the history

  44. set print attribute on

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    2425753 View commit details
    Browse the repository at this point in the history

  45. integer-list: Make note that example has become trivial

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    0b74719 View commit details
    Browse the repository at this point in the history

  46. checks for other tests

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    0641d16 View commit details
    Browse the repository at this point in the history

  47. empty expected files

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    3afc987 View commit details
    Browse the repository at this point in the history

  48. contrib/.../hfs: print attribute

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    6738115 View commit details
    Browse the repository at this point in the history

  49. Update test results (CVC4)

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    a8f47c7 View commit details
    Browse the repository at this point in the history

  50. Update test results

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    5c81285 View commit details
    Browse the repository at this point in the history

  51. nelson-oppen: Modify text a bit

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    0a536b1 View commit details
    Browse the repository at this point in the history

  52. Update test results

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    1b55664 View commit details
    Browse the repository at this point in the history

  53. systems.md/nelson-oppen: Add output to text

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    22eb108 View commit details
    Browse the repository at this point in the history

  54. Update test results

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    7396e8a View commit details
    Browse the repository at this point in the history

  55. Update test results

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    140c9e0 View commit details
    Browse the repository at this point in the history

  56. More text

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    d0e40fb View commit details
    Browse the repository at this point in the history

  57. More of Jose's suggestions

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    c9b52c2 View commit details
    Browse the repository at this point in the history

  58. Update test results

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    12feecd View commit details
    Browse the repository at this point in the history

  59. Formatting; Jose's changes 2

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    d68b8fc View commit details
    Browse the repository at this point in the history

  60. tests are in maude files

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    60a7787 View commit details
    Browse the repository at this point in the history

  61. build: add tests that need smt

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    9f7cb30 View commit details
    Browse the repository at this point in the history

  62. Remove test runner

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    7f23dae View commit details
    Browse the repository at this point in the history

  63. !!! move to eq form

    @nishantjr
    nishantjr committed Sep 30, 2018
    Configuration menu
    Copy the full SHA
    ed41d93 View commit details
    Browse the repository at this point in the history

Commits on Sep 20, 2019

  1. build: Make sure we build with mcsat for non-linear arithmetic support

    @nishantjr
    nishantjr committed Sep 20, 2019
    Configuration menu
    Copy the full SHA
    ea077fa View commit details
    Browse the repository at this point in the history