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
797e1b86fe
makefile
2019-02-11 16:55:43 +01:00
Simon Cruanes
2b1bef9e3c
ocpindent config
2019-02-11 16:55:43 +01:00
Simon Cruanes
b92d8b39e7
remove useless dir
2019-02-11 16:55:43 +01:00
Simon Cruanes
f5b4f5d0cb
update opam files
2019-02-11 16:55:43 +01:00
Simon Cruanes
d9ceba72d4
cleanup in fields
2019-02-11 16:55:43 +01:00
Simon Cruanes
cb45782eed
travis
2019-02-11 16:55:43 +01:00
Simon Cruanes
a978ec97a3
update travis
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
f64a1556b1
details
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
8cdfe65048
Merge branch 'master' of github.com:Gbury/mSAT
2018-07-24 23:02:59 +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
Cedric Cellier
0425ce6206
Fix typo in the pigeon hole test description
2018-06-02 18:55:20 +02:00
Guillaume Bury
1722730e26
Fix typo in doc
2018-04-18 11:53:55 +02:00
Guillaume Bury
696002bcf7
[travis] Fix faulty conditional for dolmen pinning
2018-01-30 17:23:57 +01:00
Guillaume Bury
fd75f536fa
Fix typo in opam file
2018-01-30 17:15:41 +01:00
Guillaume Bury
7cd541b243
Merge branch 'master' of github.com:Gbury/mSAT
2018-01-30 17:05:19 +01:00
Guillaume Bury
16e6be0c0d
[travis] Force installation of dev version
2018-01-30 17:04:58 +01:00
Guillaume Bury
25b8c97fa0
Typo in travis.yml
2018-01-29 19:39:13 +01:00
Guillaume Bury
8821b7767f
New shiny travis script + test dep on dolmen.dev
2018-01-26 14:20:50 +01:00
Guillaume Bury
14c92bbe31
Merge branch 'master' of github.com:Gbury/mSAT
2018-01-26 13:50:05 +01:00
Guillaume Bury
c8321b4098
Added ICFP presentation in README
2018-01-26 13:49:38 +01:00
Simon Cruanes
a9d762673a
fix small linter issue in opam
2017-12-30 21:10:25 +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
