429 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Guillaume Bury	7dd04204ed	[travis] Only build the bin for tests	2016-11-17 00:19:40 +01:00
Guillaume Bury	c2887b2e29	[travis] Try and build on old ocaml versions	2016-11-17 00:11:26 +01:00
Guillaume Bury	66f250a57e	[travis] Changed ocaml test versions	2016-11-16 19:52:26 +01:00
Guillaume Bury	64af636341	[doc] Updated inference rules	2016-10-18 19:10:31 +02:00
Guillaume Bury	f237851e89	Added Model definitions in msat doc	2016-10-18 17:39:10 +02:00
Guillaume Bury	ee2a80bc4f	[wip] Documentation update	2016-10-14 14:12:29 +02:00
Guillaume Bury	ff6e9cb8f0	[wip] adding documentation about msat	2016-10-12 19:11:08 +02:00
Guillaume Bury	f35d3a9f23	Fixed uninterpreted predicates for mcsat solver	2016-09-23 15:57:38 +02:00
Guillaume Bury	1656995097	Added uninterpreted functions to mcsat solver	2016-09-23 15:39:23 +02:00
Guillaume Bury	4fae86c81d	Fixed typo in smt typechecker	2016-09-23 14:02:12 +02:00
Guillaume Bury	88b8c9f895	Optimisation for mcsat solver	2016-09-23 13:30:51 +02:00
Guillaume Bury	41f1ec0e82	For travis, dolmen is now pinned to github/dev version	2016-09-23 13:30:19 +02:00
Guillaume Bury	9cf13bd7a2	Mcsat now works (for pure equality problems)	2016-09-22 18:31:22 +02:00
Guillaume Bury	4f5bb640ca	[WIP] All is setup, remains to have real theories ... Architecture is now all setup, but theories for the smt and mcsat solvers are currently dummy ones that are not doing anything.	2016-09-16 15:49:33 +02:00
Guillaume Bury	2a33534312	Added (dummy) mcsat module for test binary	2016-09-14 19:55:57 +02:00
Guillaume Bury	4522aa3ddc	Removed Expr module from msat lib	2016-09-12 17:54:10 +02:00
Guillaume Bury	a0d8bd5457	Added dolmen dependency	2016-09-12 17:11:05 +02:00
Guillaume Bury	0631135bd5	Smt solver with dummy theory now builds	2016-09-12 15:43:57 +02:00
Guillaume Bury	fa8957784a	Restored simple expressions for pure SAT	2016-09-12 15:37:06 +02:00
Guillaume Bury	dfff903f8c	Removed additional libs.	2016-09-12 15:32:22 +02:00
Guillaume Bury	9d509241ad	[WIP] Some drastic cleanup of code ... Some of these changes are to be reverted, among other the structure of terms used for the instantiation of the pure SAT solver	2016-09-09 18:09:04 +02:00
Guillaume Bury	954892ac4a	[WIP] Strange compiler bug	2016-09-09 12:07:13 +02:00
Guillaume Bury	742f8c469d	Added Expr and typing module from ArchSat	2016-09-07 17:58:07 +02:00
Simon Cruanes	bb2c931d68	wip	2016-08-24 18:23:01 +02:00
Simon Cruanes	41557a1509	wip: make SMT great again	2016-08-16 17:20:48 +02:00
Guillaume Bury	7d57b3f1b5	Accept late conflict clauses, closes #4	2016-08-04 21:34:17 +02:00
Simon Cruanes	12fed8a811	do not ask for comparison on terms and formulas	2016-08-03 20:27:51 +02:00
Simon Cruanes	66707b58fc	optimize Vec.{get,set}	2016-07-29 23:43:06 +02:00
Guillaume Bury	6f54604dc9	Optim for non-mcsat solvers	2016-07-29 23:20:31 +02:00
Simon Cruanes	7016bb1825	add an inlining parameter for non-flambda versions of OCaml	2016-07-29 23:02:23 +02:00
Simon Cruanes	af55371eb4	change the caching mechanism for var's assignable subterms	2016-07-29 22:50:37 +02:00
Simon Cruanes	c70c102de9	optim in a bottleneck in Vec	2016-07-29 22:50:26 +02:00
Guillaume Bury	5fdffe1f85	Handle new clauses unsat at level >0 && <=base_lvl	2016-07-29 21:00:24 +02:00
Simon Cruanes	6eeaa8513c	fix bug	2016-07-29 20:45:30 +02:00
Simon Cruanes	85c290c0ce	small changes	2016-07-29 20:15:53 +02:00
Simon Cruanes	672b5945ce	expose true_at_level0 in Solver_intf	2016-07-29 17:51:00 +02:00
Guillaume Bury	9d6634d621	Better interface for Msat.Internal	2016-07-29 15:47:51 +02:00
Simon Cruanes	38a6d8c481	small fix	2016-07-29 15:11:53 +02:00
Guillaume Bury	bc200474eb	Simpler code for clause simplification ... Simplify_zero is a strict subset of partition_aux	2016-07-29 14:40:42 +02:00
Guillaume Bury	a32b35e994	Fix proofs with local assumptions	2016-07-29 13:35:05 +02:00
Guillaume Bury	51c76479b9	Better logging in proofs	2016-07-29 12:58:21 +02:00
Simon Cruanes	d6c6331d85	check proofs in test_api	2016-07-28 11:10:31 +02:00
Simon Cruanes	5a04fa49ed	for proofs, represent assumptions as propagations	2016-07-28 10:56:19 +02:00
Simon Cruanes	eb14a1e229	fix	2016-07-28 10:47:59 +02:00
Simon Cruanes	ac706f3e56	fix bug	2016-07-28 10:18:07 +02:00
Simon Cruanes	2e8b45edbc	many small changes	2016-07-28 00:51:36 +02:00
Simon Cruanes	09b13be78d	reflect test_api result in its errcode	2016-07-27 23:24:01 +02:00
Simon Cruanes	98d5074da6	updates to tests	2016-07-27 19:09:11 +02:00
Simon Cruanes	3e54fac7f9	add some tests for the API	2016-07-27 18:54:56 +02:00
Simon Cruanes	73c2500b05	allow propagation of lits under base_level	2016-07-27 18:16:26 +02:00