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

592 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
585bf6bd50 detail 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
8550102ea6 dependencies in opam files; put binary in minismt package 2019-02-11 16:55:43 +01:00
Simon Cruanes
eff8ed1c4f split some features into minismt lib 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
797e1b86fe makefile 2019-02-11 16:55:43 +01:00
Simon Cruanes
2b1bef9e3c ocpindent config 2019-02-11 16:55:43 +01:00
Simon Cruanes
b92d8b39e7 remove useless dir 2019-02-11 16:55:43 +01:00
Simon Cruanes
f5b4f5d0cb update opam files 2019-02-11 16:55:43 +01:00
Simon Cruanes
d9ceba72d4 cleanup in fields 2019-02-11 16:55:43 +01:00
Simon Cruanes
cb45782eed travis 2019-02-11 16:55:43 +01:00
Simon Cruanes
a978ec97a3 update travis 2019-02-11 16:55:43 +01:00
Simon Cruanes
ec7fa9e01a fix warnings 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
f64a1556b1 details 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
4bb1f5b793 Update for latest version of dolmen 2018-09-11 14:19:37 +02: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
8cdfe65048 Merge branch 'master' of github.com:Gbury/mSAT 2018-07-24 23:02:59 +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
Cedric Cellier
0425ce6206 Fix typo in the pigeon hole test description 2018-06-02 18:55:20 +02:00
Guillaume Bury
1722730e26 Fix typo in doc 2018-04-18 11:53:55 +02:00
Guillaume Bury
696002bcf7 [travis] Fix faulty conditional for dolmen pinning 2018-01-30 17:23:57 +01:00
Guillaume Bury
fd75f536fa Fix typo in opam file 2018-01-30 17:15:41 +01:00
Guillaume Bury
7cd541b243 Merge branch 'master' of github.com:Gbury/mSAT 2018-01-30 17:05:19 +01:00
Guillaume Bury
16e6be0c0d [travis] Force installation of dev version 2018-01-30 17:04:58 +01:00
Guillaume Bury
25b8c97fa0
Typo in travis.yml 2018-01-29 19:39:13 +01:00
Guillaume Bury
8821b7767f New shiny travis script + test dep on dolmen.dev 2018-01-26 14:20:50 +01:00
Guillaume Bury
14c92bbe31 Merge branch 'master' of github.com:Gbury/mSAT 2018-01-26 13:50:05 +01:00
Guillaume Bury
c8321b4098 Added ICFP presentation in README 2018-01-26 13:49:38 +01:00
Simon Cruanes
a9d762673a fix small linter issue in opam 2017-12-30 21:10:25 +01: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
631280af9a Remove use of Array.memq (absent from ocaml <4.03) 2017-08-25 19:08:52 +02:00
Guillaume Bury
2db3a5a494 Ignore some smtlib statements in test executable 2017-08-25 18:36:42 +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
8eee822ad6 Removed some unused code in coq backend 2017-08-22 14:55:21 +02:00