5 commits

Author	SHA1	Message	Date
Simon Cruanes	cbe3750b0d	use generative functors, remove a layer of nesting for SMT libs	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
Guillaume Bury	e7b22b9c3e	Merge branch 'wip-basic-smt'	2016-11-17 15:22:28 +01:00
Guillaume Bury	9cf13bd7a2	Mcsat now works (for pure equality problems)	2016-09-22 18:31:22 +02:00
Guillaume Bury	2a33534312	Added (dummy) mcsat module for test binary	2016-09-14 19:55:57 +02:00