issues Search Results · repo:sarsko/CreuSAT language:Rust
Filter by
10 results
(75 ms)10 results
insarsko/CreuSAT (press backspace or delete to remove)b36aacd
$./CreuSAT --file f.cnf
c Reading file f.cnf
c Parsed formula with 1 ...
wintered
- 5
- Opened on Aug 27, 2024
- #44
Excellent project and thesis! Although I m not finished reading it :)
I think there s a minor typo for Lit struct in section 3.3. You define Lit as having a polarity bool. But this is
subsequently changed ...
mathatter997
- 1
- Opened on Jul 15, 2024
- #43
Could you add what should be cited in the readme? Here is the bibtex entry I currently use, but it might not be optimal:
@mastersthesis{creusat,
author = {Skotåm, Sarek Høverstad},
title ...
m-fleury
- 1
- Opened on Mar 6, 2023
- #40
Is it expected that the fast and slow heuristic have the same initial value in CreuSAT?
pub fn new(f: Formula) - Solver {
Solver {
num_lemmas: 0,
max_lemmas: 2000, ...
- 2
- Opened on Oct 4, 2022
- #38
Thank you! I love any progress in the Rust SAT space. varisat has an api witch I have used extensively for testing
libraries I work on. Would you be interested in adding an Rust API interface to CreuSAT? ...
enhancement
Eh2406
- 7
- Opened on Jun 18, 2022
- #30
I wonder how much time could be gained by having all formula data stored using arenas. We should investigate using
bumpalo for this.
enhancement
xldenis
- 2
- Opened on May 29, 2022
- #16
Rather self-explanatory, but taking the time to eliminate all runtime checks would be very beneficial to the proof
itself.
enhancement
- 1
- Opened on May 29, 2022
- #15
It would be a good idea to set up a simple CI script that ensures the proofs are not obsolete (without even running
them). This would avoid much risk of breakage.
- 1
- Opened on May 29, 2022
- #14
Running cargo make p crashes for me since it uses a hardcoded path for the why3 ide script. It would be nice to include
the script locally. This may also require copying prelude/ from Creusot (until we ...
- 1
- Opened on May 29, 2022
- #13
I feel like it might be a good idea to experiment with using smallvec in the definition of Clause.
Alternately, I wonder if it is possible define a custom unsized type in Rust so that we can layout the ...
enhancement
- 8
- Opened on May 29, 2022
- #12
Learn how you can use GitHub Issues to plan and track your work.
Save views for sprints, backlogs, teams, or releases. Rank, sort, and filter issues to suit the occasion. The possibilities are endless.Learn more about GitHub IssuesProTip!
Restrict your search to the title by using the in:title qualifier.Learn how you can use GitHub Issues to plan and track your work.
Save views for sprints, backlogs, teams, or releases. Rank, sort, and filter issues to suit the occasion. The possibilities are endless.Learn more about GitHub IssuesProTip!
Press the /
key to activate the search input again and adjust your query.