simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-12 22:10:53 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions
694 commits 53 branches 1 tag 17 MiB
Commit graph

200 commits

Author SHA1 Message Date
Simon Cruanes
3c940ed4f6 refactor(core): use bitfield in clauses, use Vec.iter more 2019-02-11 16:55:43 +01:00
Simon Cruanes
0d7ae34880 fix(analyze-final): mistake in production of unsat cores 2019-02-11 16:55:43 +01:00
Simon Cruanes
52ae127a5d refactor: implement analyze_final to compute unsat cores 2019-02-11 16:55:43 +01:00
Simon Cruanes
4ca441fa38 fix(core): cancel-until 0 before solving 2019-02-11 16:55:43 +01:00
Simon Cruanes
1136416a7c wip: remove push/pop 2019-02-11 16:55:43 +01:00
Simon Cruanes
f3488d68db test: add regression tests and icnf parser for assumptions 2019-02-11 16:55:43 +01:00
Simon Cruanes
df9538a91e perf: exit early from propagation loop in case of conflict 2019-02-11 16:55:43 +01:00
Simon Cruanes
1655d09035 refactor: simpler, cleaner functors 2019-02-11 16:55:43 +01:00
Simon Cruanes
c815ccf648 refactor: use pp instead of print 2019-02-11 16:55:43 +01:00
Simon Cruanes
7e9fd1a363 perf: remove bitfield, implement it manually 2019-02-11 16:55:43 +01:00
Simon Cruanes
8b4458b066 refactor(api): make theory state also explicit 2019-02-11 16:55:43 +01:00
Simon Cruanes
e60aff60b6 refactor: simplify vec, remove the need to provide dummy elt 2019-02-11 16:55:43 +01:00
Simon Cruanes
b3fc070d09 style: remove old headers 2019-02-11 16:55:43 +01:00
Simon Cruanes
05e2506362 refactor: remove minismt things, make simple msat.sh 2019-02-11 16:55:43 +01:00
Simon Cruanes
2fb51d8082 chore: move to dune 2019-02-11 16:55:43 +01:00
Simon Cruanes
6eeb649cdc doc 2019-02-11 16:55:43 +01:00
Simon Cruanes
27cbb981e7 more controled API for Res 2019-02-11 16:55:43 +01:00
Simon Cruanes
83d3048648 a bit of doc 2019-02-11 16:55:43 +01:00
Simon Cruanes
f5066a2ff3 typo 2019-02-11 16:55:43 +01:00
Simon Cruanes
6762985d18 expose {push,pop} in main solver 2019-02-11 16:55:43 +01:00
Simon Cruanes
241e2fa4d7 remove useless functions 2019-02-11 16:55:43 +01:00
Simon Cruanes
87fc9aef26 reinstate better way of picking watch literals 2019-02-11 16:55:43 +01:00
Simon Cruanes
5279456419 reset some record accesses, for perf 2019-02-11 16:55:43 +01:00
Simon Cruanes
b2e646343a do not expose St in solver, but only expose a restricted API. 2019-02-11 16:55:43 +01:00
Simon Cruanes
a612a1cda2 make Solver.t more lightweight by removing some useless fields 2019-02-11 16:55:43 +01:00
Simon Cruanes
a34c191ddc add optional size argument to create functions 2019-02-11 16:55:43 +01:00
Simon Cruanes
ef7333af6d make state explicit and add type t state-wrapper in most modules 2019-02-11 16:55:43 +01:00
Simon Cruanes
eff3f8024f wip: use submodules of Solver_types to clean up code 2019-02-11 16:55:43 +01:00
Simon Cruanes
8eef2deebd faster addition of clauses' watch literals 
instead of sorting the whole clause, just select two highest level lits
 2019-02-11 16:55:43 +01:00
Simon Cruanes
9bc85160b8 restrict what Msat core lib exposes, provide shortcuts 2019-02-11 16:55:43 +01:00
Simon Cruanes
cbe3750b0d use generative functors, remove a layer of nesting for SMT libs 2019-02-11 16:55:43 +01:00
Simon Cruanes
d9ceba72d4 cleanup in fields 2019-02-11 16:55:43 +01:00
Simon Cruanes
2707215aa2 move tseitin transformation into its own lib 2019-02-11 16:55:43 +01:00
Simon Cruanes
768f59f88b big refactoring 
- move to jbuilder
- use a functorial heap (with indices embedded in lit/var)
- update Vec with optims from mc2
- change semantics of Vec.shrink
- use new Log module
 2019-02-11 16:55:43 +01:00
Simon Cruanes
48ec2d732c capitalization of files; add new Log 2019-02-11 16:55:43 +01:00
Guillaume Bury
5e57bfc827 Bugfix for user lvl push when already unsat 2018-09-11 14:19:22 +02:00
Guillaume Bury
2bba885266 Prevent semantic propagations at level 0 2018-07-24 23:42:20 +02:00
Guillaume Bury
a5eeaa0edc Propagate consequences at the lowest level possible 2018-07-24 21:57:12 +02:00
Guillaume Bury
354f2013b1 Add assertion to check theory conflict clauses 2018-07-24 21:56:58 +02:00
Guillaume Bury
1722730e26 Fix typo in doc 2018-04-18 11:53:55 +02:00
Guillaume Bury
bed469c0cf Clear unused hyps in coq proofs 2017-08-29 15:18:10 +02:00
Guillaume Bury
7749f7aaac Manual re-indent 2017-08-25 19:15:12 +02:00
Guillaume Bury
679d928b88 Auto re-indent 2017-08-25 19:11:58 +02:00
Guillaume Bury
4989026f06 Fix mcsat conflict analysis 
When analyzing an mcst conflict clause and looking at a semantic
propagation in the trail, the last resolved clause was looked at again,
which caused an invalid history to be generated (the computation of the
backtrack clause was not affected because the second resolution of the clause
was basically a no-op thanks to the 'seen' field), thus it did not
introduce any soundness bug, just a faulty clause history which was
caught during proof expansion.
 2017-08-25 18:33:42 +02:00
Guillaume Bury
607ec3f043 Added Coq backend (not tested yet) 2017-08-09 09:45:18 +02:00
Guillaume Bury
0c99e6b2e7 [breaking] Better interface for the DOT backend 2017-07-20 13:55:55 +02:00
Guillaume Bury
92835bcdda Add useful function on proof steps 
These new functions are designed to help people if (or when) the proof
API will break next time (i.e. adding a new variant case in step).
 2017-04-12 20:48:08 +02:00
Guillaume Bury
88c122c4a4 Remove incorrect tag duplication 2017-04-12 19:40:21 +02:00
Guillaume Bury
0fe8ded071 [bugfix] Fix typo following doublon elimination 
Following a bugfix for doublon elimination, doublons are now eliminated
in add_clause, and as such, in case no simplification is made, the
clause without doublons should be used (and not init). This was a typo
missed during the refactoring of doublon elimination.
 2017-04-12 19:23:46 +02:00
Guillaume Bury
7e95911dd8 [bugfix] Allow late mcsat conflicts (wrt assigns) 2017-04-07 15:13:27 +02:00