12 commits

Author	SHA1	Message	Date
Simon Cruanes	2caf53c24f	expose {push,pop} in main solver	2017-12-29 21:29:43 +01:00
Simon Cruanes	d47071c4f0	reinstate better way of picking watch literals	2017-12-29 19:00:54 +01:00
Simon Cruanes	70fcded713	reset some record accesses, for perf	2017-12-29 18:53:26 +01:00
Simon Cruanes	d415f8ed20	do not expose St in solver, but only expose a restricted API.	2017-12-29 18:29:56 +01:00
Simon Cruanes	c14f0ba020	make Solver.t more lightweight by removing some useless fields	2017-12-29 17:29:24 +01:00
Simon Cruanes	a65309d5e6	add optional size argument to create functions	2017-12-29 17:24:09 +01:00
Simon Cruanes	99078b2335	make state explicit and add type t state-wrapper in most modules	2017-12-29 16:48:26 +01:00
Simon Cruanes	148c1da3cc	wip: use submodules of Solver_types to clean up code	2017-12-29 15:29:04 +01:00
Simon Cruanes	06af58e6f3	faster addition of clauses' watch literals ... instead of sorting the whole clause, just select two highest level lits	2017-12-29 12:32:27 +01:00
Simon Cruanes	db54c8e9b2	cleanup in fields	2017-12-28 18:03:00 +01:00
Simon Cruanes	ac50e10788	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	2017-12-28 15:51:04 +01:00
Simon Cruanes	fc5a2d4e9d	capitalization of files; add new Log	2017-12-28 14:13:10 +01:00

Renamed from src/core/internal.ml (Browse further)