55 commits

Author	SHA1	Message	Date
Simon Cruanes	7f05da56cc	fix: cache E_unsat in direct add_clause functions	2019-02-11 18:11:33 -06:00
Simon Cruanes	4127db2153	Revert "fix: catch E_unsat in assume, if one adds an empty clause" ... This reverts commit 5d7e34584bdbfd8326fbbf7f3314d93ac79597ce.	2019-02-11 16:55:43 +01:00
Simon Cruanes	7673bddf82	fix: catch E_unsat in assume, if one adds an empty clause	2019-02-11 16:55:43 +01:00
Simon Cruanes	ea98f6f027	refactor: return an array from conflict analysis	2019-02-11 16:55:43 +01:00
Simon Cruanes	96c4d83781	detail: add debug message	2019-02-11 16:55:43 +01:00
Simon Cruanes	8ad78b2acd	refactor: a bit of cleanup for mcsat	2019-02-11 16:55:43 +01:00
Simon Cruanes	7583e78bd2	fix(propagate): insert propagated literal itself	2019-02-11 16:55:43 +01:00
Simon Cruanes	8d012d2f49	refactor: fix problems from review ... - use `cid` instead of `name` for clauses - has the name of the clause, not its content - simplified some things	2019-02-11 16:55:43 +01:00
Simon Cruanes	7891f2b69e	refactor: cleaner choice of which vector to add a clause to	2019-02-11 16:55:43 +01:00
Simon Cruanes	ba4c360cbd	fix: when simplifying, copy flags properly	2019-02-11 16:55:43 +01:00
Simon Cruanes	6dbaa2d335	feat: expose eval_atom	2019-02-11 16:55:43 +01:00
Simon Cruanes	c89a99e82b	rename log-proof to store-proof	2019-02-11 16:55:43 +01:00
Simon Cruanes	ebd8ad7110	refactor: rename flag clause.{learnt,removable} ... more accurate representation of the semantics, esp. for theory lemmas	2019-02-11 16:55:43 +01:00
Simon Cruanes	da24541fa0	feat: allow optional disabling of proof logging ... - goal: do not keep clauses alive after they're gc'd - default is to indeed log proofs	2019-02-11 16:55:43 +01:00
Simon Cruanes	f62fa88b0f	api: annotate input clauses with theory proofs, too ... this replaces the old "tag" system	2019-02-11 16:55:43 +01:00
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