https://gitlab.lrde.epita.fr/akheireddine/bmctool

sort by:
Revision Author Date Message Commit Date
3707304 get minimum attempts script for edacc csv : scripts/addUnknownLines_EDACCcsv.py 30 August 2021, 12:42:36 UTC
eb7d451 other scripts *scripts/addUnknownLines_EDACCcsv.py 17 August 2021, 09:27:53 UTC
1c9a3ad update scripts for CP21 * compile_exp_mode.sh, compile_log_mode.sh:Here 09 August 2021, 09:01:39 UTC
aa099a9 update painless submodule * painless 11 July 2021, 12:45:32 UTC
0c4a0f2 New script to simplify the compilation * compile_exp_mode.sh, compile_log_mode.sh:Here. 27 May 2021, 21:00:50 UTC
b331563 Clean ouput * bmctool.cc, painless:Here. 27 May 2021, 15:21:42 UTC
89ed528 Merge branch 'ak/octo_version' 26 May 2021, 13:55:44 UTC
55123c8 Update painless sub-module * painless 04 May 2021, 12:53:34 UTC
f93cef6 update script * scripts/plot_shared_clauses.py 02 May 2021, 21:33:11 UTC
93b6f06 update script * scripts/plot_shared_clauses.py 28 April 2021, 11:15:13 UTC
1a8674d CLEAN CODE and input parameters * bmctool.cc, painless, src/utils/EnvBMC.hh:Here. 17 April 2021, 15:10:21 UTC
078b7ee remove srand * bmctool.cc 09 April 2021, 16:29:11 UTC
2b62d0c Script for generate smv instances + plots information : * scripts/negate_property_smv.py, scripts/organize_csv_edacc_exepriments.py, scripts/plot_category_used_clauses.py, scripts/plot_shared_clauses.py:Here. 06 April 2021, 11:56:30 UTC
9444554 New SMV instnaces : * examples/data-beem/elevator_planning.1.smv, examples/data-beem/elevator_planning.2.smv, examples/data-beem/lann.1.smv, examples/data-beem/lann.2.smv, examples/data-beem/schedule_world.1.smv, examples/data-beem/schedule_world.2.smv, examples/data-beem/schedule_world.3.smv:Here. 04 April 2021, 18:37:10 UTC
a62229c Update code * bmctool.cc, painless:Here. 04 April 2021, 18:35:08 UTC
0c8b689 New filter strategy and sharing strategy * bmctool.cc, painless:Here. 29 March 2021, 15:03:06 UTC
ec9d840 Use max-memory to limit sharing clauses * bmctool.cc, painless:Here. 26 March 2021, 15:13:49 UTC
f9da892 New sharing strategy for Maple *bmctool.cc, painless:Here. 19 March 2021, 13:27:03 UTC
f345284 Remove some unused parameters/log * bmctool.cc, painless:Here. 19 March 2021, 10:13:56 UTC
c633207 New parameter dyn * bmctool.cc 13 March 2021, 09:47:24 UTC
82ac419 Move src/decomposition repository to painless/painless-src * painless, src/decomposition/algorithms/ANISSADecomposition.hh, src/decomposition/algorithms/ANISSADecomposition.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/mc/NuSMV.hh, src/solver/Preprocessor.cc, src/solver/Preprocessor.hh:Here. 13 March 2021, 09:32:26 UTC
e6a0431 New filters and new input parameter to enable import clauses from DeSAT solver * bmctool.cc, painless:Here 05 March 2021, 12:14:04 UTC
dfe4fca New input parameter : probability of sharing ITP/CONFL clauses from DeSAT solver * bmctool.cc, painless:Here. 26 February 2021, 12:46:59 UTC
48780ef ADD/UPDATE input parameter * bmctool.cc, painless, src/utils/EnvBMC.hh:Here. 25 February 2021, 17:34:22 UTC
1dfbf77 Remove ratio parameter : * bmctool.cc, painless, src/solver/Preprocessor.cc, src/utils/EnvBMC.hh:Here. 23 February 2021, 12:11:52 UTC
ee0bbd8 Separate filter for ITP and Conflict Clauses : * bmctool.cc, painless:Here. 23 February 2021, 11:07:53 UTC
5b8ba61 Add EnvBMC to Maple Solver : * bmctool.cc, painless:Here. 18 February 2021, 14:32:57 UTC
c1a02d8 Update script for computing information about ITP * scripts/identification_impact_of_formula.py:Here. 17 February 2021, 13:22:39 UTC
292fda2 Update input options * bmctool.cc, painless:Here. 17 February 2021, 13:21:58 UTC
a886ad9 Fix shroot option on painless repository * painless:Here. 11 February 2021, 09:53:56 UTC
21f271c Start to integrate new option -shroot used in painless: * bmctool.cc, painless:Here. 10 February 2021, 11:33:01 UTC
c9d236a Add new input parameters used in painless : * bmctool.cc, painless, src/utils/EnvBMC.hh:Here. 09 February 2021, 12:43:03 UTC
e0d54b3 Fix problem with random decomposition of the problem : * bmctool.cc:Here. 08 February 2021, 15:54:15 UTC
0240c4e Pull up variables of initial step to root : * src/decomposition/algorithms/OPTIDecomposition.cc, src/utils/EnvBMC.hh:Here. 08 February 2021, 14:52:27 UTC
3bd3bc5 Ignore .smv extension * bmctool.cc src/decomposition/splitFormula.cc src/mc/ModelChecker.hh src/mc/NuSMV.cc src/prop/Property.hh src/utils/Utils.hh 05 February 2021, 19:47:18 UTC
e24a7ca Update scripts : * scripts/boxplotgenerator.py, scripts/compare_itp_conversion.py, scripts/identification_impact_of_formula.py:Here. 05 February 2021, 11:08:33 UTC
7628e2b FIX parse value k * src/utils/Utils.hh:Here. 04 February 2021, 11:42:56 UTC
d6a62e2 Save BMC information such as Property's variables * painless, src/decomposition/splitFormula.cc, src/utils/EnvBMC.hh:Here. 02 February 2021, 11:58:20 UTC
4049620 New argument for createDeSATSolver * src/solver/Preprocessor.cc:Here. 01 February 2021, 19:50:07 UTC
f60c2fb FIXED : at random decomposition option * src/solver/Preprocessor.cc:Here 28 January 2021, 14:19:35 UTC
4aad9d9 Submit fomula's clauses to clauses base : * src/decomposition/algorithms/OPTIDecomposition.cc:Here. 26 January 2021, 13:10:30 UTC
6b1fac9 Remove empty partitions and indent code * src/decomposition/splitFormula.cc, src/decomposition/splitFormula.hh, src/solver/Preprocessor.cc: Here. 25 January 2021, 15:39:47 UTC
91b0bc7 Update BMC-D decomposition * src/decomposition/algorithms/OPTIDecomposition.cc:Here. 25 January 2021, 15:36:28 UTC
89ef465 Update RND decomposition : * src/decomposition/splitFormula.cc:Here. 22 January 2021, 15:21:15 UTC
4739760 No need for k parameter when using standard CDCL solver : * bmctool.cc:Here. 19 January 2021, 14:22:49 UTC
76e49cf script for variable analysis : * scripts/caracterize_learnt_clauses_itp.py:Here. 05 January 2021, 16:39:25 UTC
0ca2d4d Print variable information : * src/utils/EnvBMC.hh:Here. 05 January 2021, 16:24:09 UTC
3c97183 Joining steps decomposition : * src/decomposition/splitFormula.cc 29 December 2020, 14:53:09 UTC
4f5fd44 Add clause formula to root G : * src/decomposition/algorithms/OPTIDecomposition.cc:Here. 29 December 2020, 11:36:36 UTC
4a61cf3 New decomposition method : inequal repartition of steps *src/decomposition/splitFormula.cc, src/decomposition/splitFormula.hh:Here. 29 December 2020, 11:35:51 UTC
a181099 Activate NuSMV verbose for debugging + create .csv unique output filename * bmctool.cc, src/mc/NuSMV.cc, src/utils/EnvBMC.hh:Here. 29 December 2020, 11:33:12 UTC
65c1ef9 Caracterize variables of the problem : * src/decomposition/algorithms/OPTIDecomposition.cc, src/decomposition/splitFormula.cc, src/utils/EnvBMC.hh:Here. 17 December 2020, 19:16:24 UTC
f6eb990 Generate unique log depending on t parameter : * bmctool.cc, painless, src/solver/Preprocessor.cc:Here. 17 December 2020, 15:06:37 UTC
24f5872 NEW method based on different percentage of step coverage for decomposition * bmctool.cc, painless, src/decomposition/splitFormula.cc, src/decomposition/splitFormula.hh:Here 17 December 2020, 11:09:49 UTC
f45e0f6 Restore BMC decomposition algorithm * bmctool.cc, painless, src/decomposition/algorithms/OPTIDecomposition.cc, src/decomposition/algorithms/OPTIDecomposition.hh, src/decomposition/splitFormula.cc:Here. 16 December 2020, 11:08:02 UTC
bb5d07c Merge branch 'ak/bmctool' of https://gitlab.lrde.epita.fr/akheireddine/bmctool into ak/bmctool 08 December 2020, 16:20:33 UTC
f82a350 Update bmctool with painless : * Makefile, bmctool.cc, painless:Here. 08 December 2020, 16:02:35 UTC
32cdcb7 Merge branch 'ak/bmctool' of https://gitlab.lrde.epita.fr/akheireddine/bmctool into ak/bmctool 07 December 2020, 12:57:05 UTC
6f9ed04 Read input file one time for all standard solvers : * bmctool.cc, painless:Here. 05 December 2020, 14:29:26 UTC
09893ce Mergeach 'akbmctool' of https://gitlab.lrde.epita.fr/akheireddine/bmctool into ak/bmctool 04 December 2020, 12:22:17 UTC
6825df8 Decomposition strategy : fix issue when number of variable blocs is higher than nleafs input parameter: * bmctool.cc, painless, src/decomposition/splitFormula.cc, src/decomposition/splitFormula.hh, 04 December 2020, 11:39:01 UTC
44218af cleanup code and remove warnings during compilation : * nusmv_wrapper.hh, src/mc/ModelChecker.hh, src/mc/NuSMV.cc, src/prop/NuSMVProperty.cc, src/prop/NuSMVProperty.hh, src/prop/Property.hh, src/solver/Preprocessor.cc, src/utils/Utils.hh:Here 04 December 2020, 11:36:14 UTC
f69a97d Update scripts * scripts/extract_information_from_outpufile_info.py:Here. 03 December 2020, 10:15:51 UTC
93e6598 Update makefile and painless submodule : * Makefile, painless/ : Here. 02 December 2020, 16:19:29 UTC
0da1395 Updata main function : * bmctool.cc 02 December 2020, 16:17:46 UTC
f0a8b6e cleanup files : * src/solver/SATSolver.hh, src/utils/Utils.hh:Here. 02 December 2020, 16:16:59 UTC
732947e 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 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 NuSMV: splitter parameter optionnal * src/mc/NuSMV.cc, src/mc/NuSMV.hh:Here. 02 December 2020, 14:46:04 UTC
89b75c4 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 script: update scripts * scripts/extract_information_from_outpufile_info.py:Here. 20 November 2020, 12:45:50 UTC
61f14e0 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 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 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 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 update output files * bmctool.cc, painless 05 November 2020, 13:26:09 UTC
17dc0b2 scripts : update script * scripts/extract_information_from_outpufile_info.py : here. 05 November 2020, 11:05:17 UTC
c9a68ce examples/data-beem: new SMV files with no property yet 03 November 2020, 17:09:19 UTC
9218528 scripts : new script reset * scripts/total_time_in_reset_periplo.py : Here. 29 October 2020, 09:25:46 UTC
4295214 Merge branch 'ak/bmctool' of https://gitlab.lrde.epita.fr/akheireddine/bmctool into ak/bmctool 27 October 2020, 17:05:47 UTC
4c11afa 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 Makefile : add push Doker image * Makefile: Here. 26 October 2020, 16:55:50 UTC
f4626d1 giltab-ci: update * .gitlab-ci.yml: Here. 26 October 2020, 11:52:22 UTC
768edca Merge branch 'ak/bmctool' of https://gitlab.lrde.epita.fr/akheireddine/bmctool into ak/bmctool 26 October 2020, 11:15:11 UTC
33400c7 scripts : update * scripts/extract_information_from_outpufile_info.py:Here. 26 October 2020, 11:10:25 UTC
314e218 add check option * .gitlab-ci.yml, Makefile, test.sh: Here. 26 October 2020, 10:49:40 UTC
bd84fd5 Makefile: update Docker image names * Makefile: Here. 26 October 2020, 10:20:12 UTC
f41f98a gitlab: make can push Docker images * Makefile: Here. 26 October 2020, 09:39:01 UTC
74e9401 gitlab-ci: first setup * .gitlab-ci.yml, Dockerfile, Makefile: Here. 26 October 2020, 09:35:20 UTC
354b8f1 examples: New benchs * examples/rers-2016-ad32499615589e33a34ca4edf340995663657329-models-nusmv/models/nusmv:Here. 24 October 2020, 19:25:57 UTC
dbaa116 Merge branch 'ak/bmctool' of https://gitlab.lrde.epita.fr/akheireddine/bmctool into ak/bmctool 22 October 2020, 12:01:42 UTC
823bee2 bmctool: fix logs * bmctool.cc, painless, src/decomposition/splitFormula.cc, src/utils/StatsBMC.hh: Here. 22 October 2020, 11:55:51 UTC
f7d858f bmctool: fix logs * painless, src/decomposition/splitFormula.cc, src/utils/StatsBMC.hh: Here. 22 October 2020, 11:05:48 UTC
4caed09 Makefile: add -O3 option during compilation * Makefile, painless: Here. 22 October 2020, 10:29:10 UTC
0bb3c1a bmctool: move k extraction method * bmctool.cc: Here. 22 October 2020, 05:46:24 UTC
69d77f3 Merge branch 'ak/bmctool' of https://gitlab.lrde.epita.fr/akheireddine/bmctool into ak/bmctool 21 October 2020, 20:01:24 UTC
0eafdcd splitFormula: simplify random decomposition of clause * src/decomposition/splitFormula.cc: Here. 21 October 2020, 20:00:08 UTC
399a8bc 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 scripts: rm Tools repository and move files to scripts/ * Tools, scripts: Here 21 October 2020, 09:19:55 UTC
fb41379 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
back to top