15 commits

Author	SHA1	Message	Date
Simon Cruanes	00dec7ced8	remove iarray	2022-07-15 21:06:46 -04:00
Simon Cruanes	a1bc186d2e	use ocamlformat	2022-07-14 22:09:13 -04:00
Simon Cruanes	0abe4b7020	wip: decode more proof steps to quip	2021-10-27 21:50:28 -04:00
Simon Cruanes	4a30a06f87	wip: reconstruct quip proof from binary proof-trace	2021-10-26 21:57:17 -04:00
Simon Cruanes	68250603c4	fix compat	2021-08-24 19:41:36 -04:00
Simon Cruanes	3fbb9af664	refactor(sat): hide atoms, API now talks only about literals	2021-08-19 09:35:54 -04:00
Simon Cruanes	ae6d298790	move to containers 3.0	2020-09-08 22:33:24 -04:00
Simon Cruanes	6c603d5589	refactor: remove code that checks invariants	2019-06-10 14:28:05 -05:00
Simon Cruanes	0e467e058c	fix: disable checking of invariants	2018-08-18 19:56:12 -05:00
Simon Cruanes	b8445d0ca3	refactor: introduce check_invariants in CC ... costly, but helps find bugs	2018-08-18 14:52:44 -05:00
Simon Cruanes	04f25779fa	refactor(term): much simpler term model, without builtins or typeclass ... just use a few custom functions in `Cst.t`	2018-05-25 23:45:15 -05:00
Simon Cruanes	fade033458	refactor: get SAT properly again on some problems	2018-05-20 14:30:36 -05:00
Simon Cruanes	d19b798ee9	add ability to parse and process dimacs files	2018-04-11 19:57:51 -05:00
Simon Cruanes	dac3378198	improve SAT solver messages, remove semantic reason	2018-02-23 00:43:56 -06:00
Simon Cruanes	d73684902f	wip: have a proper smtlib parser	2018-02-05 23:09:29 -06:00

Renamed from src/smt/Util.ml (Browse further)