40 commits

Author	SHA1	Message	Date
Simon Cruanes	79bd88b999	api: remove spurious () for calls to solve	2019-02-11 16:55:43 +01:00
Simon Cruanes	1736b4a99e	api: sat_state takes formulas, not atoms	2019-02-11 16:55:43 +01:00
Simon Cruanes	4fbaae7d2d	refactor(log): use a S-expr-style format for log messages	2019-02-11 16:55:43 +01:00
Simon Cruanes	0a3a3b576a	refactor: remove dead code, some basic simplifications	2019-02-11 16:55:43 +01:00
Simon Cruanes	fdc042aee3	fix: no need to add trivial clauses at all	2019-02-11 16:55:43 +01:00
Simon Cruanes	83c0d0e7f1	feat: add Value.t to the mcsat interface ... it can be useful to separate terms from pure values.	2019-02-11 16:55:43 +01:00
Simon Cruanes	95bdc80ed5	feat: rename slice to acts, add some functions in it ... - add literal - add term - eval literal	2019-02-11 16:55:43 +01:00
Simon Cruanes	8f1c24c1a6	refactor: change API to {final,partial}_check	2019-02-11 16:55:43 +01:00
Simon Cruanes	ced266663e	refactor: change backtracking API (push/pop_levels)	2019-02-11 16:55:43 +01:00
Simon Cruanes	f26f74e119	fix: bugfix in construction of slices in SAT/theory interface	2019-02-11 16:55:43 +01:00
Simon Cruanes	5e1508ff2b	refactor: use a vec for the new clauses	2019-02-11 16:55:43 +01:00
Simon Cruanes	14319f959f	refactor: a bit of cleanup in analyze	2019-02-11 16:55:43 +01:00
Simon Cruanes	a5ec88f2a7	refactor: use Var.mark and a pre-allocated vec for analyze	2019-02-11 16:55:43 +01:00
Simon Cruanes	cf6147c500	details	2019-02-11 16:55:43 +01:00
Simon Cruanes	9024b0f0a9	refactor: change theory API to be simpler and more imperative	2019-02-11 16:55:43 +01:00
Simon Cruanes	74956e2e87	fix(proof): fix proof production for unsat cores	2019-02-11 16:55:43 +01:00
Simon Cruanes	8f29aa8005	refactor: small cleanup	2019-02-11 16:55:43 +01:00
Simon Cruanes	ca62db00e1	perf: garbage collect clauses (only for clauses with ≥3 lits)	2019-02-11 16:55:43 +01:00
Simon Cruanes	3c940ed4f6	refactor(core): use bitfield in clauses, use Vec.iter more	2019-02-11 16:55:43 +01:00
Simon Cruanes	0d7ae34880	fix(analyze-final): mistake in production of unsat cores	2019-02-11 16:55:43 +01:00
Simon Cruanes	52ae127a5d	refactor: implement analyze_final to compute unsat cores	2019-02-11 16:55:43 +01:00
Simon Cruanes	4ca441fa38	fix(core): cancel-until 0 before solving	2019-02-11 16:55:43 +01:00
Simon Cruanes	1136416a7c	wip: remove push/pop	2019-02-11 16:55:43 +01:00
Simon Cruanes	f3488d68db	test: add regression tests and icnf parser for assumptions	2019-02-11 16:55:43 +01:00
Simon Cruanes	df9538a91e	perf: exit early from propagation loop in case of conflict	2019-02-11 16:55:43 +01:00
Simon Cruanes	1655d09035	refactor: simpler, cleaner functors	2019-02-11 16:55:43 +01:00
Simon Cruanes	8b4458b066	refactor(api): make theory state also explicit	2019-02-11 16:55:43 +01:00
Simon Cruanes	e60aff60b6	refactor: simplify vec, remove the need to provide dummy elt	2019-02-11 16:55:43 +01:00
Simon Cruanes	6762985d18	expose {push,pop} in main solver	2019-02-11 16:55:43 +01:00
Simon Cruanes	87fc9aef26	reinstate better way of picking watch literals	2019-02-11 16:55:43 +01:00
Simon Cruanes	5279456419	reset some record accesses, for perf	2019-02-11 16:55:43 +01:00
Simon Cruanes	b2e646343a	do not expose St in solver, but only expose a restricted API.	2019-02-11 16:55:43 +01:00
Simon Cruanes	a612a1cda2	make Solver.t more lightweight by removing some useless fields	2019-02-11 16:55:43 +01:00
Simon Cruanes	a34c191ddc	add optional size argument to create functions	2019-02-11 16:55:43 +01:00
Simon Cruanes	ef7333af6d	make state explicit and add type t state-wrapper in most modules	2019-02-11 16:55:43 +01:00
Simon Cruanes	eff3f8024f	wip: use submodules of Solver_types to clean up code	2019-02-11 16:55:43 +01:00
Simon Cruanes	8eef2deebd	faster addition of clauses' watch literals ... instead of sorting the whole clause, just select two highest level lits	2019-02-11 16:55:43 +01:00
Simon Cruanes	d9ceba72d4	cleanup in fields	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
Simon Cruanes	48ec2d732c	capitalization of files; add new Log	2019-02-11 16:55:43 +01:00

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