Simon Cruanes
ac396e8cf5
rename to cdcl
2018-01-22 22:09:47 -06:00
Simon Cruanes
8c8209c08c
large refactoring to keep only a simpler, easier CDCL(T) interface
...
- only one functor to instantiate
- explicit state that is carried around
- remove minismt stuff
2018-01-22 21:52:06 -06:00
Simon Cruanes
7324647fb1
doc
2018-01-03 22:08:55 +01:00
Simon Cruanes
53cc8b35a0
more controled API for Res
2018-01-03 22:07:40 +01:00
Simon Cruanes
3f4f7ec7e4
a bit of doc
2018-01-03 22:01:12 +01:00
Simon Cruanes
c7015450a1
typo
2017-12-29 22:10:01 +01:00
Simon Cruanes
2caf53c24f
expose {push,pop} in main solver
2017-12-29 21:29:43 +01:00
Simon Cruanes
be929d056a
remove useless functions
2017-12-29 19:12:17 +01:00
Simon Cruanes
d47071c4f0
reinstate better way of picking watch literals
2017-12-29 19:00:54 +01:00
Simon Cruanes
70fcded713
reset some record accesses, for perf
2017-12-29 18:53:26 +01:00
Simon Cruanes
38b670ebc0
detail
2017-12-29 18:35:27 +01:00
Simon Cruanes
d415f8ed20
do not expose St in solver, but only expose a restricted API.
2017-12-29 18:29:56 +01:00
Simon Cruanes
c14f0ba020
make Solver.t more lightweight by removing some useless fields
2017-12-29 17:29:24 +01:00
Simon Cruanes
a65309d5e6
add optional size argument to create functions
2017-12-29 17:24:09 +01:00
Simon Cruanes
99078b2335
make state explicit and add type t state-wrapper in most modules
2017-12-29 16:48:26 +01:00
Simon Cruanes
148c1da3cc
wip: use submodules of Solver_types to clean up code
2017-12-29 15:29:04 +01:00
Simon Cruanes
06af58e6f3
faster addition of clauses' watch literals
...
instead of sorting the whole clause, just select two highest level lits
2017-12-29 12:32:27 +01:00
Simon Cruanes
1592196c72
dependencies in opam files; put binary in minismt package
2017-12-28 19:48:59 +01:00
Simon Cruanes
1cd70b048c
split some features into minismt lib
2017-12-28 19:43:54 +01:00
Simon Cruanes
d6c84b93bf
restrict what Msat core lib exposes, provide shortcuts
2017-12-28 19:31:55 +01:00
Simon Cruanes
1037c06636
use generative functors, remove a layer of nesting for SMT libs
2017-12-28 19:12:41 +01:00
Simon Cruanes
d4646ffd63
makefile
2017-12-28 19:12:32 +01:00
Simon Cruanes
b3e9b640f0
ocpindent config
2017-12-28 18:55:01 +01:00
Simon Cruanes
4aed7762a7
remove useless dir
2017-12-28 18:48:21 +01:00
Simon Cruanes
875efa33c6
update opam files
2017-12-28 18:33:52 +01:00
Simon Cruanes
db54c8e9b2
cleanup in fields
2017-12-28 18:03:00 +01:00
Simon Cruanes
d884c9fe41
travis
2017-12-28 17:33:03 +01:00
Simon Cruanes
2a3afe7ec1
update travis
2017-12-28 16:08:49 +01:00
Simon Cruanes
5e12b26fc0
fix warnings
2017-12-28 16:02:47 +01:00
Simon Cruanes
7722319b0a
move tseitin transformation into its own lib
2017-12-28 16:01:36 +01:00
Simon Cruanes
64d7314aab
details
2017-12-28 15:55:00 +01:00
Simon Cruanes
ac50e10788
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
2017-12-28 15:51:04 +01:00
Simon Cruanes
fc5a2d4e9d
capitalization of files; add new Log
2017-12-28 14:13:10 +01:00
Guillaume Bury
bed469c0cf
Clear unused hyps in coq proofs
2017-08-29 15:18:10 +02:00
Guillaume Bury
7749f7aaac
Manual re-indent
2017-08-25 19:15:12 +02:00
Guillaume Bury
679d928b88
Auto re-indent
2017-08-25 19:11:58 +02:00
Guillaume Bury
631280af9a
Remove use of Array.memq (absent from ocaml <4.03)
2017-08-25 19:08:52 +02:00
Guillaume Bury
2db3a5a494
Ignore some smtlib statements in test executable
2017-08-25 18:36:42 +02:00
Guillaume Bury
4989026f06
Fix mcsat conflict analysis
...
When analyzing an mcst conflict clause and looking at a semantic
propagation in the trail, the last resolved clause was looked at again,
which caused an invalid history to be generated (the computation of the
backtrack clause was not affected because the second resolution of the clause
was basically a no-op thanks to the 'seen' field), thus it did not
introduce any soundness bug, just a faulty clause history which was
caught during proof expansion.
2017-08-25 18:33:42 +02:00
Guillaume Bury
8eee822ad6
Removed some unused code in coq backend
2017-08-22 14:55:21 +02:00
Guillaume Bury
887de5d0af
Change coq backend requirements
...
Remove the automatic clausification encoding of the coq backend, which
was slow because of the 'tauto' tactic. It was particularly a problem
for long problems, since the tauto tactic would take longer each time
because of the new hypotheses. The buren is now on the hands of the
functor argument, which hopefully should be able to do it better.
2017-08-16 11:49:51 +02:00
Guillaume Bury
bd5fa2426b
Use pose proof instead of assert in coq backend
2017-08-12 10:37:06 +02:00
Guillaume Bury
fa7da17cde
Fix Coq backend
...
Uses a more complete tactic to go from or-separated clause to the
negation-implication encoding of clauses used by the coq backend.
Also uses a better suffix for temporary clauses than "_or".
2017-08-09 21:53:06 +02:00
Guillaume Bury
87f080ea47
Fix Coq backend
...
Fix the end of the coq proof, so as to not introduce the empty clause as
a subgoal, and instead directly prove False
2017-08-09 21:09:44 +02:00
Guillaume Bury
04eb1ec1c5
Fixes to the Coq backend
...
Formerly, clauses introduced by the theory were left as is, but it
should instead be 'clausified' i.e transformed into what msat expects
(which is an encoding of clauses).
2017-08-09 21:05:49 +02:00
Guillaume Bury
0119d04899
Update after Dolmen change
...
Dolmen Introduced a new 'Clause' statement, which has to be taken into
account in the test executable of msat.
2017-08-09 20:54:53 +02:00
Guillaume Bury
607ec3f043
Added Coq backend (not tested yet)
2017-08-09 09:45:18 +02:00
Guillaume Bury
daa30a2b4f
Correctly print edges in dot backend
...
The bug was introduced when reversing the direction of edge arrow,
unfortunatley the "node <- node" syntax overlaps with the html label
syntax.
2017-07-24 17:04:12 +02:00
Guillaume Bury
0c99e6b2e7
[breaking] Better interface for the DOT backend
2017-07-20 13:55:55 +02:00
Guillaume Bury
5d4b87673d
reverse arrow direction in DOT backend
2017-07-20 13:55:44 +02:00
