| 93e6598 | akheireddine | 02 December 2020, 16:19:29 UTC | Update makefile and painless submodule : * Makefile, painless/ : Here. | 02 December 2020, 16:19:29 UTC |
| 0da1395 | akheireddine | 02 December 2020, 16:17:46 UTC | Updata main function : * bmctool.cc | 02 December 2020, 16:17:46 UTC |
| f0a8b6e | akheireddine | 02 December 2020, 16:16:59 UTC | cleanup files : * src/solver/SATSolver.hh, src/utils/Utils.hh:Here. | 02 December 2020, 16:16:59 UTC |
| 732947e | akheireddine | 02 December 2020, 16:14:01 UTC | Update code source change Painless class to Preprocessor name * src/solver/Preprocessor.cc src/solver/Preprocessor.hh:Here. | 02 December 2020, 16:14:01 UTC |
| d28c60d | akheireddine | 02 December 2020, 14:49:12 UTC | Use enum to identify decomposition option : * src/utils/EnvBMC.hh, src/decomposition/splitFormula.cc, src/decomposition/splitFormula.hh:Here. | 02 December 2020, 14:49:12 UTC |
| 4781856 | akheireddine | 02 December 2020, 14:46:04 UTC | NuSMV: splitter parameter optionnal * src/mc/NuSMV.cc, src/mc/NuSMV.hh:Here. | 02 December 2020, 14:46:04 UTC |
| 89b75c4 | akheireddine | 02 December 2020, 14:41:38 UTC | Move BMC Working strategy in Painless : * src/solver/SWBMC.cc, src/solver/SWBMC.hh, src/solver/SWBMCItp.cc, src/solver/SWBMCItp.hh, src/solver/SWBMCItpPool.cc, src/solver/SWBMCItpPool.hh, src/solver/SWInterpolator.cc, src/solver/SWInterpolator.hh, src/solver/SWInterpolatorNoSTOP.cc, src/solver/SWInterpolatorNoSTOP.hh, src/solver/SWInterpolatorPool.cc, src/solver/SWInterpolatorPool.hh, src/solver/SWInterpolatorPoolNoSTOP.cc, src/solver/SWInterpolatorPoolNoSTOP.hh, src/solver/SequentialWorkerBMC.cc, src/solver/SequentialWorkerBMC.hh:Here. | 02 December 2020, 14:41:38 UTC |
| 6436b69 | akheireddine | 20 November 2020, 12:45:50 UTC | script: update scripts * scripts/extract_information_from_outpufile_info.py:Here. | 20 November 2020, 12:45:50 UTC |
| 61f14e0 | akheireddine | 16 November 2020, 13:04:00 UTC | decomposition : Change floor to ceil when computing the number of unified steps in one partition : * src/decomposition/splitFormula.cc:Here. | 16 November 2020, 13:04:00 UTC |
| 2f8ec59 | akheireddine | 16 November 2020, 13:02:44 UTC | parser dimacs : throw exception when files is not recognized by parser_nusmv_dimacs function * src/utils/Dimacs.hh:Here. | 16 November 2020, 13:02:44 UTC |
| 7bc10a0 | akheireddine | 16 November 2020, 12:57:39 UTC | examples: update data-beem instances * examples/data-beem/adding.1.smv, examples/data-beem/adding.2.smv, examples/data-beem/adding.3.smv, examples/data-beem/adding.4.smv, examples/data-beem/adding.5.smv, examples/data-beem/adding.6.smv, examples/data-beem/bopdp.1.1.smv, examples/data-beem/bopdp.1.smv, examples/data-beem/bopdp.2.1.smv, examples/data-beem/bopdp.2.smv, examples/data-beem/bridge.1.smv, examples/data-beem/bridge.2.smv, examples/data-beem/bridge.3.smv, examples/data-beem/brp.1.smv, examples/data-beem/elevator_planning.1.smv, examples/data-beem/krebs.1.smv, examples/data-beem/krebs.2.smv, examples/data-beem/krebs.3.smv, examples/data-beem/krebs.4.smv:Here. | 16 November 2020, 12:57:39 UTC |
| e39b55f | akheireddine | 05 November 2020, 14:14:35 UTC | fix log timer for decomposition : * sc/solver/Painless.cc scripts/extract_information_from_outputfile_info.py : Here | 05 November 2020, 19:14:39 UTC |
| ae0a04c | akheireddine | 05 November 2020, 13:26:09 UTC | update output files * bmctool.cc, painless | 05 November 2020, 13:26:09 UTC |
| 17dc0b2 | akheireddine | 05 November 2020, 11:05:17 UTC | scripts : update script * scripts/extract_information_from_outpufile_info.py : here. | 05 November 2020, 11:05:17 UTC |
| c9a68ce | akheireddine | 03 November 2020, 17:09:19 UTC | examples/data-beem: new SMV files with no property yet | 03 November 2020, 17:09:19 UTC |
| 9218528 | akheireddine | 29 October 2020, 09:25:46 UTC | scripts : new script reset * scripts/total_time_in_reset_periplo.py : Here. | 29 October 2020, 09:25:46 UTC |
| 4c11afa | akheireddine | 26 October 2020, 16:58:57 UTC | tests: new tests repository for check * tests/Makefile, tests/SAT, tests/SAT.cc, tests/chnl10_11.cnf, tests/s3-3-3-1.cnf, tests/test.sh: Here. | 26 October 2020, 16:58:57 UTC |
| ae4655c | akheireddine | 26 October 2020, 16:55:50 UTC | Makefile : add push Doker image * Makefile: Here. | 26 October 2020, 16:55:50 UTC |
| f4626d1 | akheireddine | 26 October 2020, 11:52:22 UTC | giltab-ci: update * .gitlab-ci.yml: Here. | 26 October 2020, 11:52:22 UTC |
| 768edca | akheireddine | 26 October 2020, 11:13:50 UTC | Merge branch 'ak/bmctool' of https://gitlab.lrde.epita.fr/akheireddine/bmctool into ak/bmctool | 26 October 2020, 11:15:11 UTC |
| 33400c7 | akheireddine | 26 October 2020, 11:10:25 UTC | scripts : update * scripts/extract_information_from_outpufile_info.py:Here. | 26 October 2020, 11:10:25 UTC |
| 314e218 | Etienne Renault | 26 October 2020, 10:45:21 UTC | add check option * .gitlab-ci.yml, Makefile, test.sh: Here. | 26 October 2020, 10:49:40 UTC |
| bd84fd5 | Etienne Renault | 26 October 2020, 10:20:12 UTC | Makefile: update Docker image names * Makefile: Here. | 26 October 2020, 10:20:12 UTC |
| f41f98a | Etienne Renault | 26 October 2020, 09:39:01 UTC | gitlab: make can push Docker images * Makefile: Here. | 26 October 2020, 09:39:01 UTC |
| 74e9401 | Etienne Renault | 26 October 2020, 09:35:20 UTC | gitlab-ci: first setup * .gitlab-ci.yml, Dockerfile, Makefile: Here. | 26 October 2020, 09:35:20 UTC |
| 354b8f1 | akheireddine | 24 October 2020, 19:25:57 UTC | examples: New benchs * examples/rers-2016-ad32499615589e33a34ca4edf340995663657329-models-nusmv/models/nusmv:Here. | 24 October 2020, 19:25:57 UTC |
| 823bee2 | akheireddine | 22 October 2020, 10:52:16 UTC | bmctool: fix logs * bmctool.cc, painless, src/decomposition/splitFormula.cc, src/utils/StatsBMC.hh: Here. | 22 October 2020, 11:55:51 UTC |
| 4caed09 | akheireddine | 22 October 2020, 10:08:31 UTC | Makefile: add -O3 option during compilation * Makefile, painless: Here. | 22 October 2020, 10:29:10 UTC |
| 0bb3c1a | akheireddine | 22 October 2020, 05:46:24 UTC | bmctool: move k extraction method * bmctool.cc: Here. | 22 October 2020, 05:46:24 UTC |
| 69d77f3 | akheireddine | 21 October 2020, 20:01:24 UTC | Merge branch 'ak/bmctool' of https://gitlab.lrde.epita.fr/akheireddine/bmctool into ak/bmctool | 21 October 2020, 20:01:24 UTC |
| 0eafdcd | akheireddine | 21 October 2020, 20:00:08 UTC | splitFormula: simplify random decomposition of clause * src/decomposition/splitFormula.cc: Here. | 21 October 2020, 20:00:08 UTC |
| 399a8bc | Anissa Kheireddine | 21 October 2020, 17:32:03 UTC | scripts: update scripts * scripts/extract_information_from_outpufile_info.py, scripts/ranking.py, scripts/scatter-plotly.py: Here. | 21 October 2020, 17:32:03 UTC |
| f4f3ae2 | akheireddine | 21 October 2020, 09:19:55 UTC | scripts: rm Tools repository and move files to scripts/ * Tools, scripts: Here | 21 October 2020, 09:19:55 UTC |
| fb41379 | akheireddine | 21 October 2020, 09:09:44 UTC | Merge remote-tracking branch 'origin/er/osx' into ak/bmctool * Makefile, NuSMV-2.6.0/NuSMV/code/nusmv/core/bmc/bmcTableauLTLformula.c, NuSMV-2.6.0/NuSMV/code/nusmv/core/bmc/bmcTableauPLTLformula.c, NuSMV-2.6.0/NuSMV/code/nusmv/core/bmc/sbmc/sbmcTableauInc.c, NuSMV-2.6.0/NuSMV/code/nusmv/core/bmc/sbmc/sbmcTableauIncLTLformula.c, NuSMV-2.6.0/NuSMV/code/nusmv/core/compile/compileFlatten.c, NuSMV-2.6.0/NuSMV/code/nusmv/core/compile/symb_table/NFunction.c, NuSMV-2.6.0/NuSMV/code/nusmv/core/dd/dd.c, NuSMV-2.6.0/NuSMV/code/nusmv/core/hrc/dumpers/HrcDumperDebug.c, NuSMV-2.6.0/NuSMV/code/nusmv/core/prop/PropDb.c, NuSMV-2.6.0/NuSMV/code/nusmv/core/simulate/simulate.c, NuSMV-2.6.0/NuSMV/code/nusmv/core/trace/TraceMgr.c, NuSMV-2.6.0/NuSMV/code/nusmv/core/utils/WordNumber.c, NuSMV-2.6.0/NuSMV/code/nusmv/core/utils/defs.h, NuSMV-2.6.0/NuSMV/code/nusmv/shell/cmd/cmd.c, NuSMV-2.6.0/NuSMV/libnusmv.sh, NuSMV-2.6.0/NuSMV/libnusmvshell.sh, painless, src/mc/NuSMV.cc: Here. | 21 October 2020, 09:16:30 UTC |
| 2bb7dc4 | akheireddine | 21 October 2020, 08:27:14 UTC | scripts: updated * scripts/extract_information_from_outpufile_info.py | 21 October 2020, 08:27:14 UTC |
| 281b26a | akheireddine | 20 October 2020, 14:40:56 UTC | bmctool: when nbleaf parameters is getting -1, change it to value k/3 * bmctool.cc: Here. | 20 October 2020, 14:40:56 UTC |
| e2b0388 | akheireddine | 20 October 2020, 14:21:24 UTC | scripts: update scripts * scripts/extract_information_from_outpufile_info.py: Here. | 20 October 2020, 14:21:24 UTC |
| ab73c85 | Etienne Renault | 20 October 2020, 10:07:22 UTC | update painless commit number * painless: Here. | 20 October 2020, 10:07:22 UTC |
| fae975d | Etienne Renault | 20 October 2020, 10:00:17 UTC | fix remaining compilation errors in MacOS / Debian * Makefile, * src/mc/NuSMV.cc: Here. | 20 October 2020, 10:00:17 UTC |
| 63229a4 | akheireddine | 20 October 2020, 09:41:25 UTC | bmctool: FIXED : should return UNSAT when nusmv dimacs file has empty variable decision * bmctool.cc: Here. | 20 October 2020, 09:41:25 UTC |
| 93ab0eb | Etienne Renault | 20 October 2020, 08:13:49 UTC | painless: commit version * painless: Here. | 20 October 2020, 08:13:49 UTC |
| f279780 | akheireddine | 19 October 2020, 17:11:56 UTC | Tools: scripts ! * Tools: Here. | 19 October 2020, 17:11:56 UTC |
| d919021 | akheireddine | 19 October 2020, 17:11:05 UTC | utils: fix reading bound k in filename when its not given as input parameter * src/utils/Utils.hh: Here. | 19 October 2020, 17:11:05 UTC |
| 19dfa3e | akheireddine | 19 October 2020, 12:41:55 UTC | script: New script for .info file output * scripts/extract_information_from_outpufile_info.py: Here. | 19 October 2020, 17:04:26 UTC |
| 80e2b0b | Etienne Renault | 19 October 2020, 12:58:24 UTC | nusmv: kill some warnings * NuSMV-2.6.0/NuSMV/code/nusmv/core/compile/compileFlatten.c, * NuSMV-2.6.0/NuSMV/code/nusmv/core/compile/symb_table/NFunction.c, * NuSMV-2.6.0/NuSMV/code/nusmv/core/dd/dd.c, * NuSMV-2.6.0/NuSMV/code/nusmv/core/hrc/dumpers/HrcDumperDebug.c, * NuSMV-2.6.0/NuSMV/code/nusmv/core/prop/PropDb.c, * NuSMV-2.6.0/NuSMV/code/nusmv/core/simulate/simulate.c, * NuSMV-2.6.0/NuSMV/code/nusmv/core/trace/TraceMgr.c, * NuSMV-2.6.0/NuSMV/code/nusmv/core/utils/WordNumber.c, * NuSMV-2.6.0/NuSMV/code/nusmv/shell/cmd/cmd.c: Here. | 19 October 2020, 12:58:24 UTC |
| 06210cf | Etienne Renault | 19 October 2020, 12:23:23 UTC | fix MacOS compilation for nusmv and bmctool * Makefile, * NuSMV-2.6.0/NuSMV/code/nusmv/core/bmc/bmcTableauLTLformula.c, * NuSMV-2.6.0/NuSMV/code/nusmv/core/bmc/bmcTableauPLTLformula.c, * NuSMV-2.6.0/NuSMV/code/nusmv/core/bmc/sbmc/sbmcTableauInc.c, * NuSMV-2.6.0/NuSMV/code/nusmv/core/bmc/sbmc/sbmcTableauIncLTLformula.c, * NuSMV-2.6.0/NuSMV/code/nusmv/core/utils/defs.h, * NuSMV-2.6.0/NuSMV/libnusmvshell.sh, * NuSMV-2.6.0/NuSMV/libnusmv.sh: Here. | 19 October 2020, 12:32:28 UTC |
| cd84fca | akheireddine | 16 October 2020, 12:13:32 UTC | bmctool: update file output for stats * bmctool.cc, painless, src/decomposition/algorithms/OPTIDecomposition.cc, src/decomposition/algorithms/OPTIDecomposition.hh, src/decomposition/splitFormula.cc, src/solver/Painless.cc, src/utils/StatsBMC.hh: Here. | 16 October 2020, 12:13:32 UTC |
| 9d29cfb | akheireddine | 15 October 2020, 13:59:07 UTC | decomposition: fix OPTIDecomposition algorithm * src/decomposition/algorithms/OPTIDecomposition.cc: Here. | 15 October 2020, 13:59:07 UTC |
| be47b05 | akheireddine | 14 October 2020, 12:15:03 UTC | bmctool: fix initialization of bound k when not given in input parameters * bmctool.cc: Here. | 14 October 2020, 12:15:03 UTC |
| 2a45654 | akheireddine | 12 October 2020, 14:58:47 UTC | bmctool: change set to unordered_set * src/decomposition/algorithms/OPTIDecomposition.cc src/solver/SWBMC.cc src/solver/SWBMCItp.cc src/solver/SWBMCItpPool.cc src/solver/SWInterpolator.cc src/solver/SWInterpolatorNoSTOP.cc src/solver/SequentialWorkerBMC.cc src/solver/SequentialWorkerBMC.hh src/utils/EnvBMC.hh src/utils/StatsBMC.hh: Here. | 12 October 2020, 14:58:47 UTC |
| 8b9c6f8 | akheireddine | 12 October 2020, 14:55:06 UTC | NuSMV: rename directive define max * NuSMV-2.6.0/NuSMV/code/nusmv/core/bmc/bmcTableauPLTLformula.c NuSMV-2.6.0/NuSMV/code/nusmv/core/bmc/sbmc/sbmcBmcInc.c NuSMV-2.6.0/NuSMV/code/nusmv/core/bmc/sbmc/sbmcTableauInc.c NuSMV-2.6.0/NuSMV/code/nusmv/core/bmc/sbmc/sbmcTableauIncLTLformula.c NuSMV-2.6.0/NuSMV/code/nusmv/core/compile/compile.c NuSMV-2.6.0/NuSMV/code/nusmv/core/enc/bool/BoolEnc.c NuSMV-2.6.0/NuSMV/code/nusmv/core/utils/defs.h NuSMV-2.6.0/NuSMV/code/nusmv/core/wff/exprWff.c: Here. | 12 October 2020, 14:55:06 UTC |
| 57ecf0b | akheireddine | 12 October 2020, 14:54:21 UTC | README: update dependecies * README.md: Here. | 12 October 2020, 14:54:21 UTC |
| 4616ff4 | akheireddine | 12 October 2020, 14:16:29 UTC | bmctool: use unordered_set rather than set * bmctool.cc src/decomposition/algorithms/ANISSADecopmosition.cc src/decomposition/algorithms/BMCDecomposition.cc src/decomposition/algorithms/BMCDecomposition.hh src/decomposition/algorithms/OPTIDecomposition.cc src/decomposition/algorithms/OPTIDecomposition.hh src/decomposition/algorithms/lazyDecomposition.cc src/decomposition/algorithms/lazyDecomposition.hh src/decomposition/splitFormula.cc src/decomposition/splitFormula.hh src/solver/Painless.cc src/utils/Dimacs.hh src/utils/EnvBMC.hh: Here. | 12 October 2020, 14:16:29 UTC |
| b9fd284 | akheireddine | 12 October 2020, 09:16:36 UTC | decomposition: New optimized decomposition * src/decomposition/algorithms/OPTIDecomposition.cc src/decomposition/algorithms/OPTIDecomposition.hh src/decomposition/splitFormula.cc src/decomposition/splitFormula.hh: Here. | 12 October 2020, 10:19:37 UTC |
| 9c6a882 | akheireddine | 12 October 2020, 09:15:34 UTC | bmctool : clean code and rename important variables * bmctool.cc painless src/mc/NuSMV.cc src/mc/NuSMV.hh src/solver/Painless.cc src/solver/SWInterpolatorPool.cc src/solver/SWInterpolatorPoolNoSTOP.cc src/utils/Dimacs.hh src/utils/EnvBMC.hh src/utils/Utils.hh: Here. | 12 October 2020, 09:15:34 UTC |
| 07e6400 | Etienne Renault | 08 October 2020, 14:39:28 UTC | [WIP] decomposition: rework strategy 7 in 8 * bmctool.cc, src/decomposition/splitFormula.cc: Here. | 08 October 2020, 14:39:28 UTC |
| 8f05d22 | akheireddine | 07 October 2020, 16:00:42 UTC | bmctool: optimize decomposition tools * bmctool.cc src/algorithms/ANISSADecomposition.hh -> src/decomposition/algorithms/ANISSADecomposition.hh src/algorithms/ANISSADecopmosition.cc -> src/decomposition/algorithms/ANISSADecopmosition.cc src/algorithms/BMCDecomposition.cc -> src/decomposition/algorithms/BMCDecomposition.cc src/algorithms/BMCDecomposition.hh -> src/decomposition/algorithms/BMCDecomposition.hh src/algorithms/lazyDecomposition.cc -> src/decomposition/algorithms/lazyDecomposition.cc src/algorithms/lazyDecomposition.hh -> src/decomposition/algorithms/lazyDecomposition.hh src/bmc/spliter/splitFormula.cc -> src/decomposition/splitFormula.cc src/bmc/spliter/splitFormula.hh -> src/decomposition/splitFormula.hh src/mc/NuSMV.cc src/solver/Painless.cc src/solver/Painless.hh src/solver/SWBMCItp.cc src/solver/SWBMCItpPool.cc src/solver/SWInterpolator.cc src/solver/SWInterpolatorNoSTOP.cc src/solver/SWInterpolatorPool.cc src/solver/SWInterpolatorPoolNoSTOP.cc src/solver/SequentialWorkerBMC.cc src/utils/Utils.hh: Here. | 07 October 2020, 16:00:42 UTC |
| 512c4ee | akheireddine | 07 October 2020, 11:35:14 UTC | bmctool: update README * README.md: Here. | 07 October 2020, 11:35:14 UTC |
| 03ff661 | akheireddine | 07 October 2020, 10:57:39 UTC | bmctool: compile with ccache * Makefile, painless: Here. | 07 October 2020, 11:01:23 UTC |
| 0b40360 | Etienne Renault | 06 October 2020, 14:41:40 UTC | bmctool: fix memory leaks * bmctool.cc, painless, src/solver/Painless.cc, src/utils/EnvBMC.hh: Here. | 07 October 2020, 10:55:52 UTC |
| dc6ef4b | akheireddine | 05 October 2020, 16:58:03 UTC | Cleanning code : * bmctool.cc * src/algorithms/ANISSADecomposition.hh * src/algorithms/ANISSADecopmosition.cc * src/algorithms/BMCDecomposition.cc * src/algorithms/BMCDecomposition.hh * src/algorithms/lazyDecomposition.cc * src/algorithms/lazyDecomposition.hh * src/bmc/spliter/splitFormula.cc * src/bmc/spliter/splitFormula.hh * src/mc/ModelChecker.hh * src/mc/NuSMV.cc * src/mc/NuSMV.hh * src/solver/Painless.cc * src/solver/Painless.hh * src/solver/SWInterpolatorPool.cc * src/solver/SWInterpolatorPoolNoSTOP.cc * src/utils/EnvBMC.hh * src/utils/Utils.hh | 05 October 2020, 16:58:03 UTC |
| bb822a7 | akheireddine | 05 October 2020, 09:35:12 UTC | New decomposition algorithm and start to adapt methods for common operation : * bmctool.cc * scripts/evolution_itp_hammadi_algo.py * src/algorithms/ANISSADecomposition.hh * src/algorithms/ANISSADecopmosition.cc * src/algorithms/BMCDecomposition.cc * src/algorithms/BMCDecomposition.hh * src/algorithms/lazyDecomposition.cc * src/algorithms/lazyDecomposition.hh * src/bmc/spliter/splitFormula.cc * src/bmc/spliter/splitFormula.hh * src/utils/Utils.hh | 05 October 2020, 09:35:12 UTC |
| dc72011 | akheireddine | 30 September 2020, 13:37:17 UTC | Generate file _k-1 with no meaning for now : * src/bmc/spliter/splitFormula.cc * src/utils/StatsBMC.hh * src/utils/Utils.hh | 30 September 2020, 13:37:17 UTC |
| a3e718a | akheireddine | 30 September 2020, 09:44:09 UTC | Fix dimacs nusmv parser : * bmctool.cc * src/utils/Utils.hh | 30 September 2020, 09:44:09 UTC |
| f30f632 | akheireddine | 28 September 2020, 15:06:53 UTC | Update script + save original problem directly for -output file : * scripts/splitProblem.py * src/bmc/spliter/splitFormula.cc * src/utils/Utils.hh | 28 September 2020, 15:06:53 UTC |
| e30aebe | akheireddine | 27 September 2020, 12:56:20 UTC | Fix read_file parser (for smv dimacs file) * bmctool.cc * src/bmc/spliter/splitFormula.cc * src/utils/Utils.hh | 27 September 2020, 13:25:55 UTC |
| 0f013b8 | akheireddine | 24 September 2020, 16:11:14 UTC | clean examples/ directory | 24 September 2020, 16:11:14 UTC |
| 1ae27ac | akheireddine | 24 September 2020, 13:50:14 UTC | New SMV benchs : examples/rers-2016-ad32499615589e33a34ca4edf340995663657329-models-nusmv/ | 24 September 2020, 13:50:14 UTC |
| b8f9f5c | akheireddine | 19 September 2020, 12:29:01 UTC | Improve BMC splitting approach : * src/algorithms/BMCDecomposition.cc * src/algorithms/BMCDecomposition.hh * src/bmc/spliter/splitFormula.cc * src/bmc/spliter/splitFormula.hh * src/mc/NuSMV.cc * src/utils/EnvBMC.hh | 19 September 2020, 13:17:39 UTC |
| e0952f3 | akheireddine | 18 September 2020, 17:39:00 UTC | New simple STEP decomposition (àlaHAMMADI) : * bmctool.cc * src/algorithms/BMCDecomposition.cc * src/algorithms/BMCDecomposition.hh * src/algorithms/lazyDecomposition.cc * src/bmc/spliter/splitFormula.cc * src/bmc/spliter/splitFormula.hh | 18 September 2020, 17:39:00 UTC |
| 7d46685 | akheireddine | 18 September 2020, 13:49:44 UTC | Test if max_vars is null -> unsat problem * bmctool.cc | 18 September 2020, 13:49:44 UTC |
| aa56316 | akheireddine | 17 September 2020, 12:16:35 UTC | fix2 split=4 strategy=4 stats=2 * bmctool.cc | 17 September 2020, 12:16:35 UTC |
| 0d3ba97 | akheireddine | 17 September 2020, 11:08:32 UTC | fix decomposition BMC algorithm using tool=p mode: * bmctool.cc * src/utils/Utils.hh | 17 September 2020, 11:08:32 UTC |
| 3c45599 | akheireddine | 11 September 2020, 15:57:16 UTC | add printout : * bmctool.cc | 11 September 2020, 15:57:16 UTC |
| 09320b3 | akheireddine | 11 September 2020, 15:49:53 UTC | Remove unused parameter from called painless method : * bmctool.cc : Here. | 11 September 2020, 15:49:53 UTC |
| 8957246 | akheireddine | 10 September 2020, 16:43:04 UTC | First benchs * examples/TACAS21-BENCH_SHERIDAN/* | 10 September 2020, 16:43:04 UTC |
| 1e3af33 | akheireddine | 10 September 2020, 16:42:13 UTC | Do not ignore .dimacs files * .gitignore | 10 September 2020, 16:42:13 UTC |
| b5b2f67 | akheireddine | 10 September 2020, 11:20:36 UTC | Update EnvBMC and insert output stream to the class : * bmctool.cc * bmctool.hh * painless * painless_wrapper.hh * src/bmc/spliter/splitFormula.cc * src/bmc/spliter/splitFormula.hh * src/mc/NuSMV.cc * src/solver/Painless.cc * src/solver/Painless.hh * src/solver/SWBMCItpPool.cc * src/solver/SWInterpolatorPool.cc * src/solver/SWInterpolatorPool.hh * src/solver/SWInterpolatorPoolNoSTOP.cc * src/solver/SWInterpolatorPoolNoSTOP.hh * src/solver/SequentialWorkerBMC.cc * src/solver/SequentialWorkerBMC.hh * src/utils/EnvBMC.hh * src/utils/Utils.hh | 10 September 2020, 11:20:36 UTC |
| 25fde14 | akheireddine | 07 September 2020, 14:55:14 UTC | use remover of extension filename, update some classes : * bmctool.cc, * src/mc/NuSMV.cc, * src/mc/NuSMV.hh : Here | 07 September 2020, 14:55:14 UTC |
| 52893c3 | akheireddine | 07 September 2020, 10:47:50 UTC | Disable debug mode : * Makefile, * painless/ : Here. | 07 September 2020, 10:47:50 UTC |
| a6dccfc | Anissa Kheireddin | 07 September 2020, 09:06:31 UTC | Add new option cs for clause size filter : * bmctool.cc | 07 September 2020, 09:24:17 UTC |
| e77323f | Anissa Kheireddin | 07 September 2020, 08:48:37 UTC | New script to generate dimacs files * scripts/generate_dimacs_from_smv.sh : Here. | 07 September 2020, 08:48:37 UTC |
| f79ea4b | Anissa Kheireddin | 07 September 2020, 08:47:16 UTC | Add configurable stdout(ofstream) : * bmctool.cc * bmctool.hh * painless * painless_wrapper.hh * src/bmc/spliter/splitFormula.cc * src/bmc/spliter/splitFormula.hh * src/solver/Painless.cc * src/solver/SequentialWorkerBMC.cc * src/solver/SequentialWorkerBMC.hh | 07 September 2020, 08:47:16 UTC |
| a91118d | Anissa Kheireddin | 04 September 2020, 14:58:56 UTC | Update main and input options : * bmctool.cc * src/solver/Painless.cc * src/solver/Painless.hh | 04 September 2020, 14:58:56 UTC |
| fc3a655 | Anissa Kheireddin | 04 September 2020, 14:56:37 UTC | Move global variables of painless to painless_wrapper header : * painless_wrapper.hh * src/solver/SWBMC.cc * src/solver/SWBMCItp.cc * src/solver/SWBMCItpPool.cc * src/solver/SWInterpolator.cc * src/solver/SWInterpolatorNoSTOP.cc * src/solver/SWInterpolatorPool.cc * src/solver/SWInterpolatorPoolNoSTOP.cc * src/utils/EnvBMC.hh | 04 September 2020, 14:56:37 UTC |
| 7889b93 | Anissa Kheireddin | 27 August 2020, 13:37:35 UTC | Merge branch 'master' of https://gitlab.lrde.epita.fr/akheireddine/bmctool | 27 August 2020, 13:37:35 UTC |
| d791871 | Anissa Kheireddin | 26 August 2020, 11:51:42 UTC | Stop resolution before create working strategy : * src/solver/Painless.cc, * src/solver/SWInterpolatorPool.cc, * src/bmc/spliter/splitFormula.cc : Here. | 27 August 2020, 13:36:49 UTC |
| 4f0eb53 | Anissa Kheireddin | 26 August 2020, 11:51:42 UTC | Stop resolution before create working strategy : * src/solver/Painless.cc * src/solver/SWInterpolatorPool.cc | 26 August 2020, 11:51:42 UTC |
| 79ea79c | Anissa Kheireddin | 25 August 2020, 11:11:47 UTC | clean some files : * bmctool.cc, * src/bmc/spliter/splitFormula.cc, * src/bmc/spliter/splitFormula.hh : Here. | 25 August 2020, 11:11:47 UTC |
| 563d298 | Anissa Kheireddin | 16 August 2020, 18:28:16 UTC | fix model filter : * src/solver/SequentialWokerBMC.cc : Here. | 16 August 2020, 18:28:16 UTC |
| 47a2dbe | Anissa Kheireddin | 13 August 2020, 12:06:40 UTC | fix option strategy 2 : src/solver/Painless.cc : Here. | 13 August 2020, 12:06:40 UTC |
| 4c61d6c | Anissa Kheireddin | 21 July 2020, 08:55:09 UTC | Fix variable_bloc and will contains pure variables of each step : * src/bmc/spliter/splitFormula.cc, * src/bmc/spliter/splitFormula.hh, * src/utils/StatsBMC.hh : Here. | 21 July 2020, 08:55:09 UTC |
| be6ee9a | Anissa Kheireddin | 20 July 2020, 15:46:42 UTC | Create an environement class EnvBMC : * bmctool.cc, * bmctool.hh, * src/bmc/spliter/splitFormula.cc, * src/bmc/spliter/splitFormula.hh, * src/mc/NuSMV.cc, * src/mc/NuSMV.hh, * src/solver/Painless.cc, * src/solver/Painless.hh, * src/solver/SWBMC.cc, * src/solver/SWBMCItp.cc, * src/solver/SWBMCItpPool.cc, * src/solver/SWInterpolator.cc, * src/solver/SWInterpolatorNoSTOP.cc, * src/solver/SWInterpolatorPool.cc, * src/solver/SWInterpolatorPoolNoSTOP.cc, * src/solver/SequentialWorkerBMC.cc, * src/solver/SequentialWorkerBMC.hh, * src/utils/EnvBMC.hh, * src/utils/Thread_Pool.hh : Here. | 20 July 2020, 15:46:42 UTC |
| 0362b86 | Anissa Kheireddin | 20 July 2020, 07:19:21 UTC | clean code and updated version of dotGraphiz python file * bmctool.cc * scripts/dotGraphiz.py * src/bmc/spliter/splitFormula.cc | 20 July 2020, 07:19:21 UTC |
| c8b9467 | Anissa Kheireddin | 20 July 2020, 07:16:55 UTC | New class for BMC statistics : * src/solver/Painless.cc * src/solver/Painless.hh * src/solver/SWInterpolatorPool.cc * src/solver/SWInterpolatorPool.hh * src/solver/SequentialWorkerBMC.cc * src/solver/SequentialWorkerBMC.hh * src/utils/StatsBMC.hh * src/utils/Utils.hh * painless : Here. | 20 July 2020, 07:18:45 UTC |
| c00a4b2 | Anissa Kheireddin | 17 July 2020, 15:14:50 UTC | Fix wroking strategy (strategy=1) to stop all neighbour's children if interpolant concerns parent above : * src/solver/SWInterpolatorPool.cc : Here. | 17 July 2020, 15:14:50 UTC |
| 5b6498c | Anissa Kheireddin | 17 July 2020, 15:13:20 UTC | Fix nary-to-binary-tree-decomposition (split=5) * src/bmc/spliter/splitFormula.cc : Here. | 17 July 2020, 15:14:36 UTC |
| f017f82 | Anissa Kheireddin | 16 July 2020, 12:59:15 UTC | Update input parameters * bmctool.cc, * src/bmc/spliter/splitFormula.cc, * src/bmc/spliter/splitFormula.hh, * src/mc/NuSMV.cc, * src/solver/Painless.cc, * src/solver/SWInterpolatorPool.cc : Here. | 16 July 2020, 12:59:15 UTC |
| 5f099eb | Anissa Kheireddin | 13 July 2020, 08:18:28 UTC | join when subproblem is completeley UNSAT (no interpolant returned) : * src/solver/SWInterpolatorPool.cc : Here. | 13 July 2020, 08:18:28 UTC |
| 8ab7a0c | Anissa Kheireddin | 13 July 2020, 08:17:40 UTC | New version of BMCtree decomposition : * src/bmc/spliter/splitFormula.cc, * src/bmc/spliter/splitFormula.hh : Here. | 13 July 2020, 08:17:40 UTC |
