d326677 | Anthony Blomme | 20 September 2021, 14:04:37 UTC | Delete Anthony2.java | 20 September 2021, 14:04:37 UTC |
ced102e | Anthony Blomme | 20 September 2021, 14:03:46 UTC | Delete Anthony.java | 20 September 2021, 14:03:46 UTC |
6ce7661 | Blomme Anthony | 20 September 2021, 12:46:02 UTC | handling other file formats | 20 September 2021, 12:46:02 UTC |
c19d473 | Blomme Anthony | 20 September 2021, 12:03:57 UTC | rectification saturation | 20 September 2021, 12:03:57 UTC |
09bb8a7 | Blomme Anthony | 20 September 2021, 09:29:48 UTC | veriPB : try to use saturation in the proof only when necessary | 20 September 2021, 09:29:48 UTC |
504d5ca | Blomme Anthony | 17 September 2021, 14:58:43 UTC | Notify the listener when a clause is inferred after a saturation | 17 September 2021, 14:58:43 UTC |
7e7177d | Blomme Anthony | 17 September 2021, 14:24:17 UTC | push | 17 September 2021, 14:24:17 UTC |
82b5967 | Blomme Anthony | 17 September 2021, 14:21:05 UTC | Detect division to clause | 17 September 2021, 14:21:05 UTC |
d265bf7 | Blomme Anthony | 16 September 2021, 11:14:29 UTC | Add multiplication/division iff coeff > 1 | 16 September 2021, 11:14:29 UTC |
6b85bf8 | Blomme Anthony | 16 September 2021, 11:11:32 UTC | Add multiplication and division iff coeff > 1 | 16 September 2021, 11:11:32 UTC |
81030b6 | Daniel Le Berre | 15 September 2021, 07:24:35 UTC | Phase selection strategy is also random | 15 September 2021, 07:24:35 UTC |
24b0639 | Daniel Le Berre | 11 September 2021, 13:12:49 UTC | Greedy OPB solver | 11 September 2021, 13:12:49 UTC |
9c04ce7 | Daniel Le Berre | 07 September 2021, 15:04:34 UTC | Better message (0 >= 1 instead of null). | 07 September 2021, 15:04:34 UTC |
09815de | Daniel Le Berre | 07 September 2021, 14:48:29 UTC | Merge branch 'VERIPB2' of https://gitlab.ow2.org/sat4j/sat4j into VERIPB | 07 September 2021, 14:48:29 UTC |
93082e1 | Daniel Le Berre | 07 September 2021, 14:47:12 UTC | Taking into account the case of null parameter. | 07 September 2021, 14:47:12 UTC |
08d180f | Blomme Anthony | 02 September 2021, 09:44:00 UTC | Fix weakening bug | 02 September 2021, 09:44:00 UTC |
e8f5db2 | Blomme Anthony | 02 September 2021, 09:36:08 UTC | Fix weakening bug | 02 September 2021, 09:36:08 UTC |
644cead | Daniel Le Berre | 31 August 2021, 14:10:50 UTC | Fix compilation problems. | 31 August 2021, 14:10:50 UTC |
498622d | Daniel Le Berre | 15 July 2021, 11:56:04 UTC | Using dedicated message for VERIPB. | 31 August 2021, 13:37:11 UTC |
c632d76 | Daniel Le Berre | 15 July 2021, 11:47:26 UTC | Textual representation of listeners. | 31 August 2021, 13:37:11 UTC |
808cb14 | Daniel Le Berre | 13 July 2021, 17:01:31 UTC | Using dump() instead of toString() to get the expected textual representation. | 31 August 2021, 13:37:11 UTC |
6f236c9 | Blomme Anthony | 13 July 2021, 15:56:36 UTC | Fix for last clause derivation | 31 August 2021, 13:37:11 UTC |
49947d1 | Blomme Anthony | 05 June 2021, 09:18:15 UTC | Adding the option e | 31 August 2021, 13:37:10 UTC |
83265ac | Daniel Le Berre | 17 May 2021, 14:51:32 UTC | added constraints for = in the same order as expected by VeriPB | 31 August 2021, 13:37:10 UTC |
ea618d8 | Daniel Le Berre | 17 May 2021, 14:44:14 UTC | Do the loop on each enclosed constraint. | 31 August 2021, 13:37:10 UTC |
ac1ce77 | Daniel Le Berre | 17 May 2021, 14:38:23 UTC | fixes id for = constraints | 31 August 2021, 13:37:10 UTC |
c4ebee2 | Blomme Anthony | 26 April 2021, 13:54:15 UTC | MAJ VERIPB | 31 August 2021, 13:37:10 UTC |
27a76ef | Daniel Le Berre | 22 February 2021, 10:19:58 UTC | Make sure that plain SearchListener objects can be used with CP based solvers which now expect a PBSearchListener. | 31 August 2021, 13:37:10 UTC |
62a414b | Daniel Le Berre | 21 February 2021, 08:29:48 UTC | Uses a default void PBSearchListener when MapPb are not used for conflict analysis (e.g. constraints normalization). | 31 August 2021, 13:37:10 UTC |
feffd5d | Daniel Le Berre | 20 February 2021, 17:43:47 UTC | Move IConflict.setListener() to make sure it is called in all CP solvers. | 31 August 2021, 13:37:10 UTC |
454cc5f | Daniel Le Berre | 20 February 2021, 17:27:39 UTC | Not applicable here. | 31 August 2021, 13:37:10 UTC |
29c133a | Blomme Anthony | 22 February 2021, 09:08:40 UTC | First implementation of proof logging | 31 August 2021, 13:37:10 UTC |
db3d1a8 | Daniel Le Berre | 19 February 2021, 13:35:21 UTC | Move PBSearchListener setter in createReader. | 31 August 2021, 13:37:10 UTC |
97043f8 | Daniel Le Berre | 18 February 2021, 13:05:16 UTC | Moved set/get id to IConstr | 31 August 2021, 13:37:10 UTC |
b80e750 | Daniel Le Berre | 15 February 2021, 17:04:11 UTC | Added optional setId() to Constr. | 31 August 2021, 13:37:10 UTC |
dbf63dc | Daniel Le Berre | 15 February 2021, 16:51:04 UTC | Fix for ClassCastException. | 31 August 2021, 13:37:10 UTC |
e944820 | Daniel Le Berre | 15 February 2021, 16:38:08 UTC | Got all possible solution for nofail. | 31 August 2021, 13:37:10 UTC |
e7a44ad | Blomme Anthony | 15 February 2021, 15:38:00 UTC | Complete nofail solver | 31 August 2021, 13:37:10 UTC |
30d564e | Daniel Le Berre | 10 February 2021, 13:49:37 UTC | Refactored code to be easier to check. | 31 August 2021, 13:37:10 UTC |
f6902cb | Daniel Le Berre | 10 February 2021, 13:43:40 UTC | First version of the discerning solver (1 single solution). | 31 August 2021, 13:37:10 UTC |
e7ff6a8 | Daniel Le Berre | 25 January 2021, 18:01:36 UTC | Calcul de BB pour Anthony | 31 August 2021, 13:37:10 UTC |
0730580 | Daniel Le Berre | 25 January 2021, 17:40:30 UTC | Overridden getId() in PBConstr. | 31 August 2021, 13:37:10 UTC |
14cd271 | Daniel Le Berre | 14 January 2021, 15:53:25 UTC | Linking ConflictMap and PBSearchListener. | 31 August 2021, 13:37:10 UTC |
b0f351a | Daniel Le Berre | 13 January 2021, 14:08:06 UTC | Added an id to PB constrs | 31 August 2021, 13:34:14 UTC |
0f590ec | Romain WALLON | 18 November 2020, 19:42:15 UTC | Fixes a wrong use of a method | 31 August 2021, 13:32:17 UTC |
d10e3c9 | Romain WALLON | 18 November 2020, 19:26:13 UTC | First attempt to integrate PB proof logging in conflict analysis | 31 August 2021, 13:32:17 UTC |
6c9eacb | Romain WALLON | 18 November 2020, 17:56:04 UTC | Allows to log partial weakening | 31 August 2021, 13:32:17 UTC |
db0fdbf | Daniel Le Berre | 11 November 2020, 18:33:31 UTC | Java 1.8+ to get default methods support | 31 August 2021, 13:32:17 UTC |
ad7f983 | Daniel Le Berre | 11 November 2020, 17:30:34 UTC | Default SearchListener in PBSolverCP is now a PBSearchListener | 31 August 2021, 13:29:47 UTC |
c3562b2 | Daniel Le Berre | 11 November 2020, 17:05:19 UTC | Interface for PB conflict analysis | 31 August 2021, 13:29:47 UTC |
0e8589a | Daniel Le Berre | 31 August 2021, 13:27:02 UTC | Detect when no decision are taken after the first conflict. | 31 August 2021, 13:27:02 UTC |
ca754f5 | Daniel Le Berre | 08 May 2021, 08:39:28 UTC | Merge branch 'master' of https://gitlab.ow2.org/sat4j/sat4j | 08 May 2021, 08:39:28 UTC |
f0d9a86 | Romain WALLON | 10 February 2021, 15:17:47 UTC | Double bump conflicting and better effectiveness. (cherry picked from commit b872caa503b14baacafc4c573408c56aa9b20b57) | 08 May 2021, 08:37:59 UTC |
4a3e7d8 | Daniel Le Berre | 12 April 2021, 07:03:38 UTC | Removing ow2 staging repository | 12 April 2021, 07:03:38 UTC |
2e54e44 | Daniel Le Berre | 11 April 2021, 08:04:05 UTC | log properly exception messages. | 11 April 2021, 08:04:05 UTC |
7d51fde | Daniel Le Berre | 10 April 2021, 14:49:05 UTC | Refactored propagatePI: it is void a void method. | 10 April 2021, 14:49:05 UTC |
c84cb5b | Daniel Le Berre | 10 April 2021, 13:09:36 UTC | Make Explainer serializable. | 10 April 2021, 13:09:36 UTC |
9f0bb8e | Daniel Le Berre | 10 April 2021, 12:57:18 UTC | Fix serialization violation (sonarqube). | 10 April 2021, 12:57:18 UTC |
2600793 | Daniel Le Berre | 10 April 2021, 12:53:19 UTC | Fix deprecated code and use more adapted assertEquals. | 10 April 2021, 12:53:19 UTC |
1824d4f | Daniel Le Berre | 10 April 2021, 12:31:31 UTC | Remove empty tests cases. | 10 April 2021, 12:31:31 UTC |
b96720d | Daniel Le Berre | 10 April 2021, 12:30:37 UTC | Add missing assertion. | 10 April 2021, 12:30:37 UTC |
66ef175 | Daniel Le Berre | 10 April 2021, 11:10:11 UTC | Fix test case. | 10 April 2021, 11:10:11 UTC |
49895cd | Daniel Le Berre | 10 April 2021, 11:07:22 UTC | Removed deprecated class. | 10 April 2021, 11:07:22 UTC |
ce1061d | Daniel Le Berre | 10 April 2021, 10:25:49 UTC | Add missing assertions. | 10 April 2021, 10:25:49 UTC |
a2117f8 | Daniel Le Berre | 10 April 2021, 10:18:17 UTC | Add missing assertion. | 10 April 2021, 10:18:17 UTC |
3b2122a | Daniel Le Berre | 10 April 2021, 10:02:42 UTC | Add missing assertions. | 10 April 2021, 10:02:42 UTC |
5e65dab | Daniel Le Berre | 10 April 2021, 09:50:17 UTC | Add assertions in bug report test | 10 April 2021, 09:50:17 UTC |
5e1d42a | Daniel Le Berre | 10 April 2021, 09:45:43 UTC | Remove empty test cases. | 10 April 2021, 09:45:43 UTC |
8d4679f | Daniel Le Berre | 10 April 2021, 09:43:41 UTC | Add missing assertions in bug report test. | 10 April 2021, 09:43:41 UTC |
c12a031 | Daniel Le Berre | 10 April 2021, 09:33:00 UTC | Introduce assertions in bug report tests | 10 April 2021, 09:33:00 UTC |
824bfaf | Daniel Le Berre | 10 April 2021, 09:24:51 UTC | Add assertion in test case. | 10 April 2021, 09:24:51 UTC |
28aded5 | Daniel Le Berre | 10 April 2021, 08:55:40 UTC | Moved prefixes in an enum. No more constants in ILauncherMode. | 10 April 2021, 08:55:40 UTC |
845d056 | Daniel Le Berre | 10 April 2021, 08:13:56 UTC | Add details regarding the name of the solver having unit clauses problem. | 10 April 2021, 08:13:56 UTC |
77c2776 | Daniel Le Berre | 10 April 2021, 07:44:51 UTC | update dependencies for java 16 | 10 April 2021, 07:44:51 UTC |
fd6cb9d | Daniel Le Berre | 10 April 2021, 07:36:57 UTC | bump mockito version to 3.8.25 | 10 April 2021, 07:36:57 UTC |
548fddc | Daniel Le Berre | 09 April 2021, 10:54:38 UTC | testing ow2 staging 1.5.1 parent pom | 09 April 2021, 10:54:38 UTC |
00d5623 | Daniel Le Berre | 09 April 2021, 08:58:48 UTC | Update maven 3.6.3 -> 3.8.1 | 09 April 2021, 08:58:48 UTC |
04589bb | Daniel Le Berre | 09 April 2021, 08:55:35 UTC | Using ow2 parent pom 1.5.1-snapshot for maven 3.8.1 | 09 April 2021, 08:55:35 UTC |
facdc8b | Daniel Le Berre | 02 March 2021, 13:05:51 UTC | WIP: fix for #165. Need to check how much it affects the solver performance. | 03 March 2021, 06:50:11 UTC |
83133f7 | Daniel Le Berre | 25 February 2021, 10:50:32 UTC | Fix for #164 | 25 February 2021, 10:50:32 UTC |
4a45855 | Daniel Le Berre | 24 February 2021, 06:41:00 UTC | Rename the field lbdTimer into glucoseTimer to make clear it is using the Glucose scheme. | 24 February 2021, 06:41:00 UTC |
250cdf8 | Daniel Le Berre | 24 February 2021, 06:38:07 UTC | Renamed LBDConflictTimer as GlucoseConflictTimer. This scheme is not related to LBD, but to the way Glucose is performing it's clauses cleaning checks. | 24 February 2021, 06:38:07 UTC |
502d199 | Daniel Le Berre | 22 February 2021, 20:09:42 UTC | Remove spurious debug message | 22 February 2021, 20:09:42 UTC |
8c4f55e | Daniel Le Berre | 22 February 2021, 17:58:31 UTC | Test case for #162 | 22 February 2021, 17:58:31 UTC |
4897e44 | Daniel Le Berre | 22 February 2021, 17:57:41 UTC | First steps to fix #162 | 22 February 2021, 17:57:41 UTC |
dbb8901 | Daniel Le Berre | 13 January 2021, 13:18:37 UTC | Updated CI for Sat4j 3.0: Java 11+ | 13 January 2021, 13:18:37 UTC |
eba76d9 | Daniel Le Berre | 13 January 2021, 13:18:05 UTC | Heading to Sat4j 3.0 | 13 January 2021, 13:18:05 UTC |
bf44d05 | Daniel Le Berre | 14 December 2020, 17:12:27 UTC | release 2.3.6 | 14 December 2020, 17:12:27 UTC |
2bcdcb3 | Daniel Le Berre | 08 December 2020, 06:40:25 UTC | ACLIB files for Sat4j | 08 December 2020, 06:40:25 UTC |
4d2dea0 | Daniel Le Berre | 31 October 2020, 09:12:06 UTC | Allow DetectCards to enumerate solutions. | 31 October 2020, 09:12:06 UTC |
b39dab5 | Daniel Le Berre | 31 October 2020, 09:11:05 UTC | Feature annotation. | 31 October 2020, 09:11:05 UTC |
ee9c972 | Daniel Le Berre | 31 October 2020, 09:10:16 UTC | Allow nondeterministic behavior of the solver. | 31 October 2020, 09:10:16 UTC |
4d8c557 | Daniel Le Berre | 04 October 2020, 20:13:55 UTC | Merge branch 'master' of https://gitlab.ow2.org/sat4j/sat4j | 04 October 2020, 20:13:55 UTC |
c2ab17e | Daniel Le Berre | 04 October 2020, 20:12:39 UTC | settings to Java 7 instead of 6 | 04 October 2020, 20:12:39 UTC |
a5ae1b2 | Daniel Le Berre | 04 October 2020, 20:11:38 UTC | Rebuilt random solver. | 04 October 2020, 20:11:38 UTC |
aea5894 | Daniel Le Berre | 04 October 2020, 20:10:38 UTC | Improved debug display | 04 October 2020, 20:10:38 UTC |
b0e95ae | Daniel Le Berre | 04 October 2020, 20:09:15 UTC | Allow non deterministic behavior. | 04 October 2020, 20:09:15 UTC |
0e6a814 | Daniel Le Berre | 04 October 2020, 20:06:13 UTC | Allow setting timeout on core java launcher. | 04 October 2020, 20:06:13 UTC |
4e856a4 | Daniel Le Berre | 04 October 2020, 10:02:19 UTC | Merge branch 'cdcl-strategies' into 'master' Cdcl strategies See merge request sat4j/sat4j!6 | 04 October 2020, 10:02:19 UTC |
c3d638a | Romain WALLON | 18 September 2020, 11:18:21 UTC | Improves the backjump level by looking to falsified literals only | 18 September 2020, 11:18:21 UTC |