simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-24 18:36:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions
714 commits 53 branches 1 tag 17 MiB
Commit graph

72 commits

Author SHA1 Message Date
Simon Cruanes
2286a72437 fix: in final-check, resume if there are new decisions to do 2020-11-13 11:57:57 -05:00
Simon Cruanes
79b1585804 feat: allow the theory to ask for some literals to be decided on 
it's part of the actions provided to the theory.
close #19
 2020-11-13 11:57:57 -05:00
Simon Cruanes
d9bf16dfde feat: allow to set the default polarity of variables at creation time 2020-11-13 11:57:48 -05:00
Simon Cruanes
407a7e83f7 fix: allow conflicts below decision level in Make_cdcl_t 2020-01-14 22:56:01 -06:00
Simon Cruanes
0266a39b04 fix deprecation warnings related to pervasives 2019-11-29 14:04:33 -06:00
Simon Cruanes
9c78c6f7bb perf: some basic optimizations 2019-05-15 13:03:03 -05:00
Simon Cruanes
fb219fb415 refactor: use iter instead of sequence 2019-03-10 11:33:44 -05:00
Simon Cruanes
d3702d1e1f refactor: fix issues found by @gbury 2019-03-10 12:12:39 +01:00
Simon Cruanes
2aa9b3d4bc refactor: modifications asked by @gbury in review 2019-03-10 12:12:39 +01:00
Simon Cruanes
5bfd975ed3 refactor: move constant parameters outside of the solver 2019-03-10 12:12:39 +01:00
Simon Cruanes
efe93c3647 feat: Proof.check_empty_conclusion as a separate function 
this allows the validity checking of proofs of 0-level lits
 2019-03-10 12:12:39 +01:00
Simon Cruanes
28afd6eefe fix lazy propagation 2019-03-10 12:12:39 +01:00
Simon Cruanes
c2a6c2d47b refactor(propagate): make propagation clause lazy 2019-03-10 12:12:39 +01:00
Simon Cruanes
cdb52ee757 fix(proof): unsat conflicts now call Proof.prove_unsat 
this does the last bit of proof recording when a conflict is reached
during propagation
 2019-03-10 12:12:39 +01:00
Simon Cruanes
2e2bbfd4d0 fix(proof.check): ensure that the proof is an empty clause 2019-03-10 12:12:39 +01:00
Simon Cruanes
e30c54e11b refactor: use hyper-res steps in proofs 
- accelerates proof checking significantly
- provide a way to expand hyper-res steps into individual resolutions
  (eg for the Coq backend)
 2019-03-10 12:12:39 +01:00
Simon Cruanes
b2cec9eaa2 perf: use mutable flags on atoms to perform proof checking 2019-03-10 12:12:39 +01:00
Simon Cruanes
7f05da56cc fix: cache E_unsat in direct add_clause functions 2019-02-11 18:11:33 -06:00
Simon Cruanes
4127db2153 Revert "fix: catch E_unsat in assume, if one adds an empty clause" 
This reverts commit 5d7e34584bdbfd8326fbbf7f3314d93ac79597ce.
 2019-02-11 16:55:43 +01:00
Simon Cruanes
7673bddf82 fix: catch E_unsat in assume, if one adds an empty clause 2019-02-11 16:55:43 +01:00
Simon Cruanes
ea98f6f027 refactor: return an array from conflict analysis 2019-02-11 16:55:43 +01:00
Simon Cruanes
96c4d83781 detail: add debug message 2019-02-11 16:55:43 +01:00
Simon Cruanes
8ad78b2acd refactor: a bit of cleanup for mcsat 2019-02-11 16:55:43 +01:00
Simon Cruanes
7583e78bd2 fix(propagate): insert propagated literal itself 2019-02-11 16:55:43 +01:00
Simon Cruanes
8d012d2f49 refactor: fix problems from review 
- use `cid` instead of `name` for clauses
- has the name of the clause, not its content
- simplified some things
 2019-02-11 16:55:43 +01:00
Simon Cruanes
7891f2b69e refactor: cleaner choice of which vector to add a clause to 2019-02-11 16:55:43 +01:00
Simon Cruanes
ba4c360cbd fix: when simplifying, copy flags properly 2019-02-11 16:55:43 +01:00
Simon Cruanes
6dbaa2d335 feat: expose eval_atom 2019-02-11 16:55:43 +01:00
Simon Cruanes
c89a99e82b rename log-proof to store-proof 2019-02-11 16:55:43 +01:00
Simon Cruanes
ebd8ad7110 refactor: rename flag clause.{learnt,removable} 
more accurate representation of the semantics, esp. for theory lemmas
 2019-02-11 16:55:43 +01:00
Simon Cruanes
da24541fa0 feat: allow optional disabling of proof logging 
- goal: do not keep clauses alive after they're gc'd
- default is to indeed log proofs
 2019-02-11 16:55:43 +01:00
Simon Cruanes
f62fa88b0f api: annotate input clauses with theory proofs, too 
this replaces the old "tag" system
 2019-02-11 16:55:43 +01:00
Simon Cruanes
79bd88b999 api: remove spurious () for calls to solve 2019-02-11 16:55:43 +01:00
Simon Cruanes
1736b4a99e api: sat_state takes formulas, not atoms 2019-02-11 16:55:43 +01:00
Simon Cruanes
4fbaae7d2d refactor(log): use a S-expr-style format for log messages 2019-02-11 16:55:43 +01:00
Simon Cruanes
0a3a3b576a refactor: remove dead code, some basic simplifications 2019-02-11 16:55:43 +01:00
Simon Cruanes
fdc042aee3 fix: no need to add trivial clauses at all 2019-02-11 16:55:43 +01:00
Simon Cruanes
83c0d0e7f1 feat: add Value.t to the mcsat interface 
it can be useful to separate terms from pure values.
 2019-02-11 16:55:43 +01:00
Simon Cruanes
95bdc80ed5 feat: rename slice to acts, add some functions in it 
- add literal
- add term
- eval literal
 2019-02-11 16:55:43 +01:00
Simon Cruanes
8f1c24c1a6 refactor: change API to {final,partial}_check 2019-02-11 16:55:43 +01:00
Simon Cruanes
ced266663e refactor: change backtracking API (push/pop_levels) 2019-02-11 16:55:43 +01:00
Simon Cruanes
f26f74e119 fix: bugfix in construction of slices in SAT/theory interface 2019-02-11 16:55:43 +01:00
Simon Cruanes
5e1508ff2b refactor: use a vec for the new clauses 2019-02-11 16:55:43 +01:00
Simon Cruanes
14319f959f refactor: a bit of cleanup in analyze 2019-02-11 16:55:43 +01:00
Simon Cruanes
a5ec88f2a7 refactor: use Var.mark and a pre-allocated vec for analyze 2019-02-11 16:55:43 +01:00
Simon Cruanes
cf6147c500 details 2019-02-11 16:55:43 +01:00
Simon Cruanes
9024b0f0a9 refactor: change theory API to be simpler and more imperative 2019-02-11 16:55:43 +01:00
Simon Cruanes
74956e2e87 fix(proof): fix proof production for unsat cores 2019-02-11 16:55:43 +01:00
Simon Cruanes
8f29aa8005 refactor: small cleanup 2019-02-11 16:55:43 +01:00
Simon Cruanes
ca62db00e1 perf: garbage collect clauses (only for clauses with ≥3 lits) 2019-02-11 16:55:43 +01:00