651 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Simon Cruanes	5846ae7e17	chore: finish moving to dune	2019-02-11 16:55:43 +01:00
Simon Cruanes	9d729b2136	chore: move to opam 2	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	cba9f9592d	fix: update .travis.yml	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	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