simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions
560 commits 53 branches 1 tag 17 MiB
Commit graph

560 commits

This branch
This branch
All branches
Author SHA1 Message Date
Guillaume Bury
3e30a77569 Some more comments 2016-07-22 17:28:12 +02:00
Simon Cruanes
c4beb7054b spurious assertion 2016-07-22 16:51:45 +02:00
Simon Cruanes
895cb9cbfb some additional comments and cleanup 2016-07-22 16:40:22 +02:00
Simon Cruanes
891f764ee8 some more cleanup 2016-07-22 16:31:00 +02:00
Simon Cruanes
c3cfe67696 cleanup boolean propagation 2016-07-22 16:00:02 +02:00
Simon Cruanes
c1915ba2d3 wip: cleanup and documentation of internal.ml 2016-07-22 15:42:17 +02:00
Simon Cruanes
8b1d657695 remove Either 2016-07-22 13:19:16 +02:00
Simon Cruanes
51f10d7ad5 update some files 2016-07-22 11:31:17 +02:00
Simon Cruanes
e251799f8e add some array utils for pre-4.03 compat 2016-07-22 11:25:00 +02:00
Guillaume Bury
216ca82fe7 Ensure pushed clauses are added after if_sat slice 2016-07-20 11:45:13 +02:00
Guillaume Bury
d1ebc59856 Avoid unnecessary atoms array to list conversions 2016-07-18 18:49:28 +02:00
Guillaume Bury
38b4fde5c1 Clause atoms are now in an array instead of a vec 2016-07-18 18:42:15 +02:00
Guillaume Bury
933943c4e3 Merge branch '0.3.1' 2016-07-18 18:13:48 +02:00
Guillaume Bury
9dadb67fc9 [bugfix] Sort false atoms by levels in new clauses 
When a new clauses is added and it is a conflict (i.e all atoms
are false), one must take care of which literals to watch.
In order to work, the watched literals must be those with the higher
decision levels, or else the watched literals might not react when
needed. This is fixed by sorting the literals in decreasing order of
decision level when adding a new clause which happens to be false in the
current trail.
 2016-07-16 15:55:26 +02:00
Guillaume Bury
1acecc0815 Small printing upgrades 2016-07-13 18:14:23 +02:00
Guillaume Bury
2ff1279f26 Better perfs for unsat_core 2016-07-13 18:14:18 +02:00
Guillaume Bury
ef49d5eaaa Slightly better formatting for clause printing 2016-07-13 17:07:03 +02:00
Guillaume Bury
c159a60d9b Better premises for clauses 2016-07-13 16:48:14 +02:00
Guillaume Bury
245941efdb Remember more added clauses 2016-07-13 16:23:34 +02:00
Guillaume Bury
9be4c66911 [bugfix] Clause level now computed at creation 
Apart from new assumptions, clause level can always
be computed from the histoy of the clause, so it is
better to do it in Solver_types when creating clauses.
Aditionally, it seems there was an error in the manual
computing of clause level somewhere, this fixes the bug.
 2016-07-09 03:20:38 +02:00
Guillaume Bury
dcc410c8a0 Added stack to delay adding of pushed clauses 2016-07-09 03:20:38 +02:00
Guillaume Bury
510a8aaa34 [bugfix] Clause level now computed at creation 
Apart from new assumptions, clause level can always
be computed from the histoy of the clause, so it is
better to do it in Solver_types when creating clauses.
Aditionally, it seems there was an error in the manual
computing of clause level somewhere, this fixes the bug.
 2016-07-09 03:06:21 +02:00
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