Simon Cruanes
27cbb981e7
more controled API for Res
2019-02-11 16:55:43 +01:00
Simon Cruanes
83d3048648
a bit of doc
2019-02-11 16:55:43 +01:00
Simon Cruanes
f5066a2ff3
typo
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
241e2fa4d7
remove useless functions
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
585bf6bd50
detail
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
8550102ea6
dependencies in opam files; put binary in minismt package
2019-02-11 16:55:43 +01:00
Simon Cruanes
eff8ed1c4f
split some features into minismt lib
2019-02-11 16:55:43 +01:00
Simon Cruanes
9bc85160b8
restrict what Msat core lib exposes, provide shortcuts
2019-02-11 16:55:43 +01:00
Simon Cruanes
cbe3750b0d
use generative functors, remove a layer of nesting for SMT libs
2019-02-11 16:55:43 +01:00
Simon Cruanes
b92d8b39e7
remove useless dir
2019-02-11 16:55:43 +01:00
Simon Cruanes
d9ceba72d4
cleanup in fields
2019-02-11 16:55:43 +01:00
Simon Cruanes
ec7fa9e01a
fix warnings
2019-02-11 16:55:43 +01:00
Simon Cruanes
2707215aa2
move tseitin transformation into its own lib
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
Guillaume Bury
4bb1f5b793
Update for latest version of dolmen
2018-09-11 14:19:37 +02:00
Guillaume Bury
5e57bfc827
Bugfix for user lvl push when already unsat
2018-09-11 14:19:22 +02:00
Guillaume Bury
2bba885266
Prevent semantic propagations at level 0
2018-07-24 23:42:20 +02:00
Guillaume Bury
a5eeaa0edc
Propagate consequences at the lowest level possible
2018-07-24 21:57:12 +02:00
Guillaume Bury
354f2013b1
Add assertion to check theory conflict clauses
2018-07-24 21:56:58 +02:00
Guillaume Bury
1722730e26
Fix typo in doc
2018-04-18 11:53:55 +02: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
Guillaume Bury
02aa16870c
Give all label a html context in dot backend
...
Before, atoms printed in the dot backend could either be in a html
label, or in a simple label, which caused some problems for escaping
special characters such as newlines. This commit fixes that problem by
having all labels be html labels in the dot output.
2017-07-19 00:16:37 +02:00
Simon Cruanes
b405634b1d
fix typos
2017-06-20 17:37:03 +02:00
Guillaume Bury
e9b6772e75
Added equality explanation for mcsat
2017-06-20 17:16:12 +02:00
