Simon Cruanes
291a9d9a7f
tags
2016-07-09 00:36:37 +02:00
Guillaume Bury
eba84fba42
Aliased def of negated in Expr_intf
2016-07-08 17:34:46 +02:00
Guillaume Bury
b56e4e3355
Added if_sat to Theory_intf
2016-07-08 16:15:05 +02:00
Guillaume Bury
eb2850caa6
Moved some type def outside Plugins/Theories
2016-07-08 14:29:45 +02:00
Guillaume Bury
46b621269c
Merlin update
2016-07-08 14:29:36 +02:00
Guillaume Bury
bbbc29948d
Added src directory, moved some files around
2016-07-07 15:48:50 +02:00
Guillaume Bury
599a59dda9
Removed unused modules
2016-07-07 14:55:48 +02:00
Simon Cruanes
6e6503e793
cleanup: remove labels, use a sum type for negated formulas
2016-07-01 15:48:21 +02:00
Simon Cruanes
403347ddaf
avoid duplicating the definition of slices in Theory_intf
2016-07-01 15:25:10 +02:00
Guillaume Bury
66740e5de8
Adding documentation comments in Internal
2016-07-01 12:07:49 +02:00
Guillaume Bury
34b1cda760
Updated README
2016-07-01 09:34:34 +02:00
Guillaume Bury
553d320368
Fixed compilation. Refactored some code in external
2016-06-30 09:54:21 +02:00
Guillaume Bury
49267897e8
Fixed bad tabls in dot backend
2016-06-29 21:30:44 +02:00
Guillaume Bury
f19c6b9b77
Fixed dot printing bug
2016-06-29 21:30:44 +02:00
Guillaume Bury
1e2dc299ce
WIP: add dedukti output (not functional yet)
2016-05-20 17:03:22 +02:00
Guillaume Bury
d06de43789
Removed color flag (because ocaml < 4.03)
2016-05-20 16:26:03 +02:00
Guillaume Bury
6d706f55e5
Tags update + optimizations for ocaml 4.03
2016-05-20 16:21:06 +02:00
Guillaume Bury
fd4d52b7a6
Better syntax for functor signature in solver_types
2016-04-24 14:14:46 +02:00
Guillaume Bury
1a0fc95147
Fixed functor syntax for ocaml 4.00.1 in solver_types
2016-04-23 20:18:25 +02:00
Simon Cruanes
22ebead17a
missing change
2016-04-15 14:05:42 +02:00
Guillaume Bury
1ce3973f9e
[feature] Allow arbitrary proof types in DummyTheory
2016-04-15 14:03:13 +02:00
Guillaume Bury
2e6ff522e5
Update to Msat.Solver arguments in readme
2016-04-15 13:41:41 +02:00
Guillaume Bury
e3fc66919d
Put info about Msat.Solver higher in the readme
2016-04-15 13:39:09 +02:00
Guillaume Bury
f88a5dd514
[bugfix/minor] Ensure generativity of solver_types
...
This ensures that the same solver_types module is not reused
for two different solvers, which would be problematic.
Marked minor because of the low use of multiple instances of a solver.
2016-04-15 13:30:46 +02:00
Guillaume Bury
dcde8de10d
[bugfix/medium] Fixed printing of the new reasons
2016-04-15 13:30:20 +02:00
Guillaume Bury
63d8dc1dc2
[bugfix/major] Clauses can be added at level > 0
2016-04-15 12:49:38 +02:00
Guillaume Bury
ec7c6602e9
Merge branch 'master' of github.com:Gbury/mSAT
2016-04-15 12:11:38 +02:00
Guillaume Bury
815098dde4
Propagation reasons are now far more explicit
2016-04-15 12:09:23 +02:00
Simon Cruanes
479f4c1b79
small checks
2016-04-15 11:54:00 +02:00
Guillaume Bury
0186edbf34
[feature] Adds proofs for atoms true at level 0
2016-04-06 15:32:12 +02:00
Guillaume Bury
9a5c23d9c5
[bugfix] termination check after full slice was wrong
...
When the solver finds a SAT result, it sends the whole
model to the theory, because maybe it can do something
interesting/costly to expand the proof search. After
that there must be a check to see if the theory has effectively done
something, in which case we should resume proof search, or if nothing
has been done, in which case the solver should return that the problem
is satisfiable. That check was incorrect before (checking number of
assumptions, and if the queue is all caught up), because new learnt
clauses (i.e tautologies, which are *not* assumptions) can be added that
do not immediately causes propagation, so that the number of assumptions
and the element queue is constant, but we should still resume the
search.
2016-03-04 16:30:51 +01:00
Guillaume Bury
0883615b99
Replaced Either.destruct by explicit matching
2016-03-04 15:50:13 +01:00
Guillaume Bury
ea518c6ab3
Update for compatibility with ocaml 4.00.1
2016-02-29 13:43:46 +01:00
Guillaume Bury
6ea66dcffe
v0.2 release
...
Updated opam file to disbale log building.
2016-02-29 11:15:05 +01:00
Guillaume Bury
b6effe691c
Added dummy arguments to some functors
...
Some functors lacked a dummy argument, and thus
could introduce some problems if duplicated (because
they would share the same internal state).
2016-02-29 10:58:22 +01:00
Guillaume Bury
a6a44445c7
Small update to tool doc
2016-02-12 14:08:27 +01:00
Guillaume Bury
94ce8dbd25
Fixed push/pop base level and reset function to do what is said in doc
2016-02-05 14:32:41 +01:00
Guillaume Bury
6f02ace5e3
Fixed documentation generation
2016-02-05 14:32:31 +01:00
Guillaume Bury
e58cfe1c8f
Added function to print unsat core in dimacs format
...
Thgis is meant to be used for debugging and/or benchmarking purposes.
For instance, when using msat in an application, all unsat cores can
be output this way to different files so that the results can be checked
and easily reproduced in case of errors.
2016-02-05 14:30:47 +01:00
Guillaume Bury
a2809215ae
Update the binary for better output when checking proofs
2016-02-04 23:51:53 +01:00
Guillaume Bury
74be6cdc9f
Changed timeout message in binary
2016-01-31 14:33:51 +01:00
Guillaume Bury
ce65f10f9c
Big cleanup of interfaces. Breaks retro-compat !
2016-01-31 02:09:16 +01:00
Guillaume Bury
beff9ee7c1
Merge branch 'master' of github.com:Gbury/mSAT
2016-01-30 17:04:23 +01:00
Guillaume Bury
30842da947
Fixed refreshing of clauses with push/pop
2016-01-30 17:03:14 +01:00
Guillaume Bury
cb8092af3b
Cleaned makefile a bit + moved the testing binary
2016-01-30 17:02:24 +01:00
Simon Cruanes
60250f2611
add UndecidedLit for eval, eval_level
2016-01-29 17:00:05 +01:00
Simon Cruanes
f088ef73e1
expose tag_clause in Solver.Make
2016-01-29 14:59:48 +01:00
Simon Cruanes
f348dcd5ae
expose dummy theory in a functor
2016-01-29 14:40:43 +01:00
Simon Cruanes
e8162fdaf4
details
2016-01-29 14:34:45 +01:00
Guillaume Bury
383afcf19f
Update README after Log switch
2016-01-21 17:19:24 +01:00
