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

Add dependent resource inference #6

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

Add dependent resource inference #6

wants to merge 39 commits into from

Conversation

dcao
Copy link
Collaborator

@dcao dcao commented Sep 2, 2020 •
edited

✨

dcao and others added 30 commits August 9, 2020 01:38
@dcao
start work on global potl inference
c37f5d5 
as of right now, this fails because of a sort error
we're also at risk of derefencing freed z3 asts right now
@dcao
clean up after myself :^)
d1b2a6e
@dcao
fix Z3
fb10d5e 
because we were including freed AST nodes, Z3 was throwing us errors.
resource constraints still can't be solved tho - this is another
bug
@dcao
finish basic global potl inference impl
3b13b9a 
RAML-Queue and RAML-BitVec both work now :)
@dcao
fix bug with nested abstract potentials
79939c8 
previously, nested abs potls would not have potential vars
created for them; this has been fixed
@dcao
updated inference tests
77e414e 
more of them work now :))
@dcao
implement initial dependent resource inference
a59164f 
we basically throw our formulas at the internal cegis solver
and get the values of those formulas afterwards; no actual
optimizing is currently done, partially for performance
reasons
@dcao
add impl for upperBoundToConstraint
9cd6d2e
@dcao
update inference test suite
3bb6708
@dcao
add actual dependent optimization
8fbd7d1
@dcao
provide arguments for inferred potl vars
252f076 
right now we just pass in the previous function arguments
as arguments; this may be expanded later on
@dcao
add temporary changes
d0502dc
@dcao
add debug-friendly changes
7ecb6ae 
- the z3 solve and optimize fns now take lists of formulas;
  the solve fn debug prints the unsat core on failure
- actual cegis optimization machinery is disabled just for
  testing
@dcao
switch back to optimizeAssert for correctness
fbd205c
@dcao
fix formula tracked name uniqueness bug
b9f8a23
@dcao
allow specifying const/dep res inference from cmd line
aa655b3
@dcao
merge master into dependent-res-infer
a773f14 
- this adds well-formedness fixes into this branch
- also fixes test script to run with correct args
@tjknoth
pending subs
4bf8ad1
@tjknoth
actually do pending subs
49a28cd
@dcao
move List-Replicate test
1fdee3a
@dcao
add well-formedness constraint for inferred potls
fca1d34
@dcao
add fixes in prep for multiplicity inference
22cd5dd
@dcao
merge cegis fixes from master
50c84ff
@dcao
fix bug which broke cegis inference on constant examples
c463dcd 
we were only propagating our inferred potls in the inferredRVars
part of the state; we also have to do this in the resourceVars
part
@dcao
merge cgen fixes from master
22c2638
@dcao
add merge-sort-quadratic as passing test
3d191a1
@dcao
add list-merge-flatten to passing tests
6bf62fa
@dcao
fix bug with constant optimization preserving state
09036ee
@dcao
update tests
47b5208
@dcao
add dependent optimization loop
31db3b5
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.

None yet
2 participants
@dcao @tjknoth