-
Notifications
You must be signed in to change notification settings - Fork 1
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.
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
Reimplement QAlpha internals and expand benchmarking #159
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
To avoid cloning terms, the previous implementation used a single shared vector of atoms (terms) which could be indexed by many parts of the algorithm, so that atoms could be represented by integer indices. However, this indirection creates an overcomplication and doesn't seem to have any effect in practice. Also, terms are still cloned many times even in the previous implementation, which means it would make little difference anyhow. Another consideration is that Ord, Eq and Hash implementations for Terms might be less efficient than for usize indices; however, this too seems to have no empirical effect. Signed-off-by: edenfrenkel <[email protected]>
This replaces the ad-hoc implementations for each case (CNF/DNF/pDNF), and is more scalable, safe and easy to test, as well as being more systematic theoretically. Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Due to the use of rayon's parallel iterators and the way they prioritize tasks, the previous implementation of parallel solvers rarely ever ran the solvers concurrently, but almost always used the first one in the vector. This change fixes that by using `thread::scope` instead. Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Also modifies parallelism and simulations infrastructure. Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: Tej Chajed <[email protected]>
Signed-off-by: Tej Chajed <[email protected]>
Signed-off-by: Tej Chajed <[email protected]>
Signed-off-by: Tej Chajed <[email protected]>
Signed-off-by: Tej Chajed <[email protected]>
Signed-off-by: Tej Chajed <[email protected]>
Signed-off-by: Tej Chajed <[email protected]>
Signed-off-by: Tej Chajed <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
Signed-off-by: edenfrenkel <[email protected]>
The upstream CVC4/CVC4 repo has been removed, which is where we were getting the 1.8 binary release.
This commit also collapses all time-limit parameters into one, and removes the unsused scalability tests. Signed-off-by: edenfrenkel <[email protected]>
If this is at a stable point, let's merge it. It's too big to review at this point so I'd rather merge it now and start splitting up future features when possible. |
I agree, you can go ahead and merge |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This pull request performs the following changes.
In
inference
:subsume.rs
->language.rs
,lemma.rs
->frame.rs
,weaken.rs
->lemmas.rs
, and move all QAlpha-related code intoinference/src/qalpha
.Not
language constructor and add dedicated constructors forAnd
,Or
, and quantification.parallel.rs
:rayon
this was often not the case). This also lead to some changes insolver/src/basics.rs
, namely replacingrayon
with standard library threading.In
bounded
:simulator.rs
, implement two bounded simulators, one based on explicit-state (usingset.rs
) and another on SAT solving (usingsat.rs
), which given a universe size can produce all initial states, as well as all successors of a given state.fly/src/rets.rs
by implementing flattening to eliminate nested function applications.In
benchmarking
: