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

Conversation

nishantjr
Copy link
Collaborator

No description provided.

nishantjr and others added 29 commits September 27, 2018 13:53
@nishantjr
varsat/meta-aux: Stub out file
89ed827
@nishantjr
varsat/foform => meta/foform: update meta/foform; have varsat/foform …
d6f0cb5 
…load it
@nishantjr
meta/{foform,kind-ops} varsat/var-sat: Atom -> Lit
10a9a83
meta/foform: split QFFOFORM from FOFORM
94f3816
meta/foform: split QFFOFORMSET from FOFORMSET
2ec0c39
varsat/{var-sat,numbers}: switch pr FOFORM => QFFOFORM .
cd267b4
meta/foform: split QFFORM-OPERATIONS from FOFORM-OPERATIONS
90458d5
meta/foform, varsat/var-sat: restrict more modules to QFForm
159ad83
meta/foform: split QFFOFORM-SUBSTITUTION from FOFORM-SUBSTITUTION
997c88c
meta/foform: more than just renamings allowed in FOForm substitutions
48c3e41
meta/foform: lower FOFORMSUBSTITUTION-PAIR to QFFOFORMSUBSTITUTION-PAIR
7f7b63f
meta/foform, varsat/var-sat: lower FOFORM-SUBSTITUTIONSET => QFFOFORM…
6c9f704 
…-SUBSTITUTIONSET
meta/foform, varsat/var-sat: split QFFOFORM-DEFINEDOPS from FOFORM-DE…
6764d0c 
…FINEDOPS
meta/foform, varsat/var-sat: split QFFOFORMSIMPLIFY(-IMPL) from FOFOR…
c150020 
…MSIMPLIFY(-IMPL)
@nishantjr
tests/.../meta/eqform: flesh out testing harness module
19a6e3e
@nishantjr
meta/eqform: EQFORM-OPERATIONS: Port wellFormed, normalize, vars and …
398814d 
…toUnifProb
meta/eqform: add reduce and tests
c0f83b8
meta/eqform: port {QFFO => EQ}FORM-SET-OPERATIONS
49d56a0
varsat/var-sat: minimize imports
d82a48a
meta/eqform: lift _<<_ to FormSet, SubstitutionSet
f611f3a
meta/eqform: more trivial simplifications
d90ba9e
meta/eqform: mark partial functions
5006db2
varsat/var-sat: remove call to simplify which does not affect the tests
f0abd87
tests/.../varsat/var-sat: more tests
56419b6
varsat/var-sat: switch over to depending on EQFORM
29b83b4
@nishantjr
!!! var-sat query that gets stuck.
9e0a301 
Note that changing it to 'false.Bool ?= upTerm(X + X < Y + Y)
@nishantjr
tools/meta/nelson-oppen-combination: tangle and testing infrastructure
efb382a
@nishantjr
tests/nelson-oppen-combination: Begin implementation
ea0b29c
@nishantjr
tools/nelson-oppen-combination: simplify $no.tagged -> $no.basicSat
29f7aea
@nishantjr
Remove failed experiments
9387b14
@nishantjr
contrib/systems.md/hereditarily-finite-set.md: Non-trivial example of…
10e5d60 
… 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
update text
a873ae9
@nishantjr
integer-list: text; example checks validity instead of satisfiability
fb3de19
@nishantjr
test/Misc/Makefile: smtTest fails with Yices' MCSAT
b6f2be5
@nishantjr
lexical-trichotomy: Failed example (purification does not support cto…
e94a55e 
…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
tests/systems/nelson-oppen: Own Makefile.am
7a3fc86
@nishantjr
tests/systems/nelson-oppen: empty expected files
4df4dd9
@nishantjr
set print attribute on
2425753
@nishantjr
integer-list: Make note that example has become trivial
0b74719
@nishantjr
checks for other tests
0641d16
@nishantjr
empty expected files
3afc987
@nishantjr
contrib/.../hfs: print attribute
6738115
@nishantjr
Update test results (CVC4)
a8f47c7
@nishantjr
Update test results
5c81285
@nishantjr
nelson-oppen: Modify text a bit
0a536b1
@nishantjr
Update test results
1b55664
@nishantjr
systems.md/nelson-oppen: Add output to text
22eb108
@nishantjr
Update test results
7396e8a
@nishantjr
Update test results
140c9e0
@nishantjr
More text
d0e40fb
@nishantjr
More of Jose's suggestions
c9b52c2
@nishantjr
Update test results
12feecd
@nishantjr
Formatting; Jose's changes 2
d68b8fc
@nishantjr
tests are in maude files
60a7787
@nishantjr
build: add tests that need smt
9f7cb30
@nishantjr
Remove test runner
7f23dae
@nishantjr
!!! move to eq form
ed41d93
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@nishantjr