1415 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Simon Cruanes	c2b1bd038d	perf(sat): use Atom.Vec for temporary atom array	2021-09-27 19:27:04 -04:00
Simon Cruanes	1f5806244e	fix docstrings	2021-09-27 19:27:04 -04:00
Simon Cruanes	697678d6d2	feat(dyn-trans): provide config record when instantiating theory	2021-09-27 19:27:04 -04:00
Simon Cruanes	5f51863cd3	feat(dyn-trans): track activity of terms to guide instantiation	2021-09-27 19:27:04 -04:00
Simon Cruanes	3840fefb0e	wip: feat(dyn-trans): provide config via env vars	2021-09-27 19:27:04 -04:00
Simon Cruanes	156eadd9df	feat(sat): refactor a bit clause pools; add stats	2021-09-27 19:27:04 -04:00
Simon Cruanes	14d2a89196	feat(cc): expose more functions for N.t->literals	2021-09-27 19:27:04 -04:00
Simon Cruanes	265442116f	feat(core): provide mk_eqn in CC	2021-09-27 19:27:04 -04:00
Simon Cruanes	156af6e803	update doc	2021-09-27 19:27:03 -04:00
Simon Cruanes	91a307d6fa	detail	2021-09-27 19:27:03 -04:00
Simon Cruanes	d7f09d5b09	basic proof emission for dyn-trans	2021-09-27 19:27:03 -04:00
Simon Cruanes	405d48ac2d	feat(dyn-trans): first implementation, quite aggressive	2021-09-27 19:27:03 -04:00
Simon Cruanes	a12e17ffda	more hooks in CC (to add clauses)	2021-09-27 19:27:03 -04:00
Simon Cruanes	18f86e8eb7	setup dyn-trans in main solver	2021-09-27 19:27:03 -04:00
Simon Cruanes	729f171985	wip: theory for dyn-trans axioms	2021-09-27 19:27:03 -04:00
Simon Cruanes	79386c2cbd	feat(smt): provide SAT solver to theories upon initialization	2021-09-27 19:27:03 -04:00
Simon Cruanes	c151f2981f	feat: clause pools in SMT	2021-09-27 19:27:03 -04:00
Simon Cruanes	74326b39c0	feat(vec): factor a bit of code for auxiliary functions in vectors	2021-09-27 19:26:04 -04:00
Simon Cruanes	acc682c5af	refactor(cc): simple renaming	2021-09-27 19:26:04 -04:00
Simon Cruanes	86512dbed0	utils	2021-09-27 19:22:48 -04:00
Simon Cruanes	c9e257d40b	cleanup	2021-09-27 12:14:04 -04:00
Simon Cruanes	5bed2d1c5f	detail	2021-09-26 23:56:40 -04:00
Simon Cruanes	a22bfe06c1	remove debug msgs	2021-08-31 23:19:06 -04:00
Simon Cruanes	debd8bcaf8	fix warning	2021-08-31 23:06:48 -04:00
Simon Cruanes	350a23d99e	feat: minimize conflicts ... similar to minisat's level 2 of minimization.	2021-08-31 23:04:32 -04:00
Simon Cruanes	5080195c5b	feat: conflict minimization à la minisat	2021-08-31 22:59:38 -04:00
Simon Cruanes	521340a23f	feat: first full implem of clause pools	2021-08-31 22:56:42 -04:00
Simon Cruanes	10dca21f59	refactor: remove history in conflict resolution; remove simpls ... no need to simplify reasons anymore, we rely on DRUP for that.	2021-08-31 22:56:11 -04:00
Simon Cruanes	f86498b386	feat: make it compile	2021-08-31 18:59:44 -04:00
Simon Cruanes	16bb65ebfa	wip: clause pools	2021-08-31 09:30:28 -04:00
Simon Cruanes	4a2367b1bd	refactor: use Atom.Vec (a VecI32) for atom vectors	2021-08-31 09:30:05 -04:00
Simon Cruanes	1877c00c02	wip: clauses pools	2021-08-30 09:32:32 -04:00
Simon Cruanes	81caf4824e	wip: feat: additional clause allocators in SAT	2021-08-30 09:03:37 -04:00
Simon Cruanes	73b39fe075	fix more warnings	2021-08-27 21:34:26 -04:00
Simon Cruanes	e7e8873295	fix more warnings	2021-08-27 09:28:59 -04:00
Simon Cruanes	b33f5fa5b1	fix tests	2021-08-26 09:19:21 -04:00
Simon Cruanes	782afa4415	feat: move Int_id into its own module	2021-08-25 23:52:08 -04:00
Simon Cruanes	68250603c4	fix compat	2021-08-24 19:41:36 -04:00
Simon Cruanes	5017d9f8bf	Merge branch 'wip-drup-check'	2021-08-24 18:09:31 -04:00
Simon Cruanes	5505ece5fb	chore: fix warning	2021-08-23 10:49:12 -04:00
Simon Cruanes	07d512badc	fix: remove dep on mtime in checker	2021-08-23 10:17:51 -04:00
Simon Cruanes	28fad1e408	chore: ci on all branches	2021-08-23 10:03:16 -04:00
Simon Cruanes	d841090e1c	feat(checker): ability to read .drup.gz files	2021-08-23 00:10:37 -04:00
Simon Cruanes	2f41a54719	feat(main): for pure SAT, emit proofs into file or locally	2021-08-23 00:10:34 -04:00
Simon Cruanes	bb682b8080	fix(sat): emit proofs where needed	2021-08-23 00:08:09 -04:00
Simon Cruanes	fa04cb7997	refactor(th-bool): remove cache and most recursion ... the preprocessing framework already takes care of both.	2021-08-22 15:50:42 -04:00
Simon Cruanes	baecce0946	feat: use Stat in SAT solver	2021-08-22 01:56:54 -04:00
Simon Cruanes	672f828c82	perf: return to default-pol=true ... previous commit fixed sign error (move from `negated` to `same_sign` so restore good behavior	2021-08-22 01:44:37 -04:00
Simon Cruanes	9aee35c6ce	fix other issue in th-bool preprocessing	2021-08-22 01:31:59 -04:00
Simon Cruanes	27796da5a8	fix preprocessing in th-bool	2021-08-22 01:29:01 -04:00