From 7f255b9d0618f9baf8c3edff516f623f1ec82890 Mon Sep 17 00:00:00 2001 From: idan0610 Date: Mon, 8 Apr 2024 16:23:28 +0300 Subject: [PATCH 001/430] Adding CaDiCaL, integrating CaDiCaL building into CMakeLists.txt, and adding CaDiCaL objects as field members into Engine --- CMakeLists.txt | 20 + src/engine/Engine.h | 4 + tools/build_cadical.sh | 12 + tools/cadical/.clang-format | 4 + tools/cadical/.dockerignore | 1 + tools/cadical/BUILD.md | 115 + tools/cadical/CONTRIBUTING.md | 48 + tools/cadical/Dockerfile | 34 + tools/cadical/LICENSE | 27 + tools/cadical/NEWS.md | 241 + tools/cadical/README.md | 55 + tools/cadical/VERSION | 1 + tools/cadical/configure | 557 ++ .../contrib/craigtracer.LICENSE.APACHE | 15 + tools/cadical/contrib/craigtracer.LICENSE.MIT | 9 + tools/cadical/contrib/craigtracer.cpp | 986 +++ tools/cadical/contrib/craigtracer.hpp | 200 + tools/cadical/contrib/craigtracer.md | 177 + tools/cadical/makefile | 26 + tools/cadical/makefile.in | 106 + tools/cadical/scripts/README.md | 42 + .../build-and-test-all-configurations.sh | 115 + tools/cadical/scripts/check-options-occur.sh | 11 + tools/cadical/scripts/colors.sh | 29 + tools/cadical/scripts/extend-solution.sh | 75 + tools/cadical/scripts/generate-cubes.sh | 37 + .../generate-embedded-options-default-list.sh | 13 + .../scripts/generate-options-range-list.sh | 21 + tools/cadical/scripts/get-git-id.sh | 3 + tools/cadical/scripts/make-build-header.sh | 95 + tools/cadical/scripts/make-src-release.sh | 36 + .../cadical/scripts/normalize-white-space.sh | 8 + .../scripts/prepare-sc2021-submission.sh | 52 + .../scripts/run-cadical-and-check-proof.sh | 58 + .../run-simplifier-and-extend-solution.sh | 84 + .../update-example-in-cadical-header-file.sh | 28 + tools/cadical/scripts/update-version.sh | 12 + tools/cadical/src/README.md | 12 + tools/cadical/src/analyze.cpp | 1174 +++ tools/cadical/src/arena.cpp | 30 + tools/cadical/src/arena.hpp | 104 + tools/cadical/src/assume.cpp | 614 ++ tools/cadical/src/averages.cpp | 32 + tools/cadical/src/averages.hpp | 35 + tools/cadical/src/backtrack.cpp | 164 + tools/cadical/src/backward.cpp | 230 + tools/cadical/src/bins.cpp | 22 + tools/cadical/src/bins.hpp | 22 + tools/cadical/src/block.cpp | 824 ++ tools/cadical/src/block.hpp | 37 + tools/cadical/src/cadical.cpp | 1004 +++ tools/cadical/src/cadical.hpp | 1223 +++ tools/cadical/src/ccadical.cpp | 188 + tools/cadical/src/ccadical.h | 69 + tools/cadical/src/checker.cpp | 605 ++ tools/cadical/src/checker.hpp | 171 + tools/cadical/src/clause.cpp | 566 ++ tools/cadical/src/clause.hpp | 181 + tools/cadical/src/collect.cpp | 544 ++ tools/cadical/src/compact.cpp | 537 ++ tools/cadical/src/condition.cpp | 939 +++ tools/cadical/src/config.cpp | 101 + tools/cadical/src/config.hpp | 20 + tools/cadical/src/configure | 1 + tools/cadical/src/constrain.cpp | 64 + tools/cadical/src/contract.cpp | 27 + tools/cadical/src/contract.hpp | 125 + tools/cadical/src/cover.cpp | 704 ++ tools/cadical/src/cover.hpp | 34 + tools/cadical/src/decide.cpp | 243 + tools/cadical/src/decompose.cpp | 749 ++ tools/cadical/src/decompose.hpp | 23 + tools/cadical/src/deduplicate.cpp | 170 + tools/cadical/src/drattracer.cpp | 153 + tools/cadical/src/drattracer.hpp | 53 + tools/cadical/src/elim.cpp | 1123 +++ tools/cadical/src/elim.hpp | 37 + tools/cadical/src/ema.cpp | 95 + tools/cadical/src/ema.hpp | 68 + tools/cadical/src/extend.cpp | 284 + tools/cadical/src/external.cpp | 860 +++ tools/cadical/src/external.hpp | 422 + tools/cadical/src/external_propagate.cpp | 910 +++ tools/cadical/src/file.cpp | 458 ++ tools/cadical/src/file.hpp | 208 + tools/cadical/src/flags.cpp | 127 + tools/cadical/src/flags.hpp | 83 + tools/cadical/src/flip.cpp | 247 + tools/cadical/src/format.cpp | 89 + tools/cadical/src/format.hpp | 36 + tools/cadical/src/frattracer.cpp | 274 + tools/cadical/src/frattracer.hpp | 62 + tools/cadical/src/gates.cpp | 760 ++ tools/cadical/src/heap.hpp | 212 + tools/cadical/src/idruptracer.cpp | 538 ++ tools/cadical/src/idruptracer.hpp | 108 + tools/cadical/src/instantiate.cpp | 367 + tools/cadical/src/instantiate.hpp | 45 + tools/cadical/src/internal.cpp | 990 +++ tools/cadical/src/internal.hpp | 1567 ++++ tools/cadical/src/inttypes.hpp | 28 + tools/cadical/src/ipasir.cpp | 43 + tools/cadical/src/ipasir.h | 37 + tools/cadical/src/level.hpp | 33 + tools/cadical/src/lidruptracer.cpp | 630 ++ tools/cadical/src/lidruptracer.hpp | 115 + tools/cadical/src/limit.cpp | 129 + tools/cadical/src/limit.hpp | 80 + tools/cadical/src/logging.cpp | 155 + tools/cadical/src/logging.hpp | 84 + tools/cadical/src/lookahead.cpp | 520 ++ tools/cadical/src/lratbuilder.cpp | 937 +++ tools/cadical/src/lratbuilder.hpp | 195 + tools/cadical/src/lratchecker.cpp | 742 ++ tools/cadical/src/lratchecker.hpp | 166 + tools/cadical/src/lrattracer.cpp | 206 + tools/cadical/src/lrattracer.hpp | 57 + tools/cadical/src/lucky.cpp | 384 + tools/cadical/src/makefile | 1 + tools/cadical/src/message.cpp | 212 + tools/cadical/src/message.hpp | 65 + tools/cadical/src/minimize.cpp | 215 + tools/cadical/src/mobical.cpp | 4479 +++++++++++ tools/cadical/src/occs.cpp | 38 + tools/cadical/src/occs.hpp | 36 + tools/cadical/src/options.cpp | 359 + tools/cadical/src/options.hpp | 362 + tools/cadical/src/parse.cpp | 435 ++ tools/cadical/src/parse.hpp | 72 + tools/cadical/src/phases.cpp | 44 + tools/cadical/src/phases.hpp | 18 + tools/cadical/src/probe.cpp | 925 +++ tools/cadical/src/profile.cpp | 107 + tools/cadical/src/profile.hpp | 243 + tools/cadical/src/proof.cpp | 634 ++ tools/cadical/src/proof.hpp | 117 + tools/cadical/src/propagate.cpp | 568 ++ tools/cadical/src/queue.cpp | 88 + tools/cadical/src/queue.hpp | 64 + tools/cadical/src/radix.hpp | 179 + tools/cadical/src/random.cpp | 206 + tools/cadical/src/random.hpp | 98 + tools/cadical/src/range.hpp | 99 + tools/cadical/src/reap.cpp | 127 + tools/cadical/src/reap.hpp | 28 + tools/cadical/src/reduce.cpp | 243 + tools/cadical/src/reluctant.hpp | 82 + tools/cadical/src/rephase.cpp | 336 + tools/cadical/src/report.cpp | 285 + tools/cadical/src/resources.cpp | 160 + tools/cadical/src/resources.hpp | 16 + tools/cadical/src/restart.cpp | 137 + tools/cadical/src/restore.cpp | 267 + tools/cadical/src/score.cpp | 51 + tools/cadical/src/score.hpp | 16 + tools/cadical/src/shrink.cpp | 494 ++ tools/cadical/src/signal.cpp | 136 + tools/cadical/src/signal.hpp | 33 + tools/cadical/src/solution.cpp | 50 + tools/cadical/src/solver.cpp | 1634 ++++ tools/cadical/src/stats.cpp | 619 ++ tools/cadical/src/stats.hpp | 271 + tools/cadical/src/subsume.cpp | 690 ++ tools/cadical/src/terminal.cpp | 38 + tools/cadical/src/terminal.hpp | 98 + tools/cadical/src/ternary.cpp | 445 ++ tools/cadical/src/tracer.hpp | 167 + tools/cadical/src/transred.cpp | 252 + tools/cadical/src/util.cpp | 129 + tools/cadical/src/util.hpp | 128 + tools/cadical/src/var.cpp | 39 + tools/cadical/src/var.hpp | 22 + tools/cadical/src/veripbtracer.cpp | 391 + tools/cadical/src/veripbtracer.hpp | 102 + tools/cadical/src/version.cpp | 103 + tools/cadical/src/version.hpp | 11 + tools/cadical/src/vivify.cpp | 1363 ++++ tools/cadical/src/vivify.hpp | 24 + tools/cadical/src/walk.cpp | 695 ++ tools/cadical/src/watch.cpp | 106 + tools/cadical/src/watch.hpp | 72 + tools/cadical/test/README.md | 55 + tools/cadical/test/api/README.md | 8 + tools/cadical/test/api/apitrace.cpp | 76 + tools/cadical/test/api/cfreeze.c | 94 + tools/cadical/test/api/cipasir.c | 113 + tools/cadical/test/api/ctest.c | 30 + tools/cadical/test/api/example.cpp | 64 + tools/cadical/test/api/example_constraint.cpp | 76 + tools/cadical/test/api/example_tracer.cpp | 92 + tools/cadical/test/api/incproof.cpp | 67 + tools/cadical/test/api/learn.cpp | 66 + tools/cadical/test/api/makefile | 3 + tools/cadical/test/api/morenmore.cpp | 21 + tools/cadical/test/api/newdelete.cpp | 6 + tools/cadical/test/api/run.sh | 129 + tools/cadical/test/api/terminate.cpp | 47 + tools/cadical/test/api/traverse.cpp | 160 + tools/cadical/test/api/unit.cpp | 22 + tools/cadical/test/cnf/README.md | 23 + tools/cadical/test/cnf/add128.cnf | 6850 +++++++++++++++++ tools/cadical/test/cnf/add16.cnf | 928 +++ tools/cadical/test/cnf/add32.cnf | 1959 +++++ tools/cadical/test/cnf/add4.cnf | 166 + tools/cadical/test/cnf/add64.cnf | 4030 ++++++++++ tools/cadical/test/cnf/add8.cnf | 417 + tools/cadical/test/cnf/block0.cnf | 6 + tools/cadical/test/cnf/drat-trim.c | 2250 ++++++ tools/cadical/test/cnf/elimclash.cnf | 11 + tools/cadical/test/cnf/elimredundant.cnf | 11 + tools/cadical/test/cnf/empty.cnf | 1 + tools/cadical/test/cnf/empty.sol | 2 + tools/cadical/test/cnf/factor2708413neg.cnf | 3112 ++++++++ tools/cadical/test/cnf/factor2708413pos.cnf | 3112 ++++++++ tools/cadical/test/cnf/false.cnf | 2 + tools/cadical/test/cnf/full1.cnf | 3 + tools/cadical/test/cnf/full2.cnf | 5 + tools/cadical/test/cnf/full3.cnf | 9 + tools/cadical/test/cnf/full4.cnf | 17 + tools/cadical/test/cnf/full5.cnf | 33 + tools/cadical/test/cnf/full6.cnf | 65 + tools/cadical/test/cnf/full7.cnf | 129 + tools/cadical/test/cnf/lrat-trim.c | 2572 +++++++ tools/cadical/test/cnf/makefile | 3 + tools/cadical/test/cnf/ph2.cnf | 10 + tools/cadical/test/cnf/ph3.cnf | 23 + tools/cadical/test/cnf/ph4.cnf | 46 + tools/cadical/test/cnf/ph5.cnf | 82 + tools/cadical/test/cnf/ph6.cnf | 134 + tools/cadical/test/cnf/precochk.c | 254 + tools/cadical/test/cnf/prime121.cnf | 965 +++ tools/cadical/test/cnf/prime121.sol | 20 + tools/cadical/test/cnf/prime1369.cnf | 2929 +++++++ tools/cadical/test/cnf/prime1369.sol | 61 + tools/cadical/test/cnf/prime1681.cnf | 2929 +++++++ tools/cadical/test/cnf/prime1681.sol | 61 + tools/cadical/test/cnf/prime169.cnf | 1357 ++++ tools/cadical/test/cnf/prime169.sol | 28 + tools/cadical/test/cnf/prime1849.cnf | 2929 +++++++ tools/cadical/test/cnf/prime1849.sol | 61 + tools/cadical/test/cnf/prime2209.cnf | 3585 +++++++++ tools/cadical/test/cnf/prime2209.sol | 77 + tools/cadical/test/cnf/prime25.cnf | 379 + tools/cadical/test/cnf/prime25.sol | 8 + tools/cadical/test/cnf/prime289.cnf | 1815 +++++ tools/cadical/test/cnf/prime289.sol | 38 + tools/cadical/test/cnf/prime361.cnf | 1815 +++++ tools/cadical/test/cnf/prime361.sol | 38 + tools/cadical/test/cnf/prime4.cnf | 54 + tools/cadical/test/cnf/prime4.sol | 2 + tools/cadical/test/cnf/prime4294967297.cnf | 6341 +++++++++++++++ tools/cadical/test/cnf/prime49.cnf | 639 ++ tools/cadical/test/cnf/prime49.sol | 13 + tools/cadical/test/cnf/prime529.cnf | 2339 ++++++ tools/cadical/test/cnf/prime529.sol | 49 + tools/cadical/test/cnf/prime65537.cnf | 6221 +++++++++++++++ tools/cadical/test/cnf/prime841.cnf | 2339 ++++++ tools/cadical/test/cnf/prime841.sol | 49 + tools/cadical/test/cnf/prime9.cnf | 185 + tools/cadical/test/cnf/prime9.sol | 4 + tools/cadical/test/cnf/prime961.cnf | 2339 ++++++ tools/cadical/test/cnf/prime961.sol | 48 + tools/cadical/test/cnf/regr000.cnf | 2 + tools/cadical/test/cnf/regr000.sol | 2 + tools/cadical/test/cnf/run.sh | 333 + tools/cadical/test/cnf/sat0.cnf | 5 + tools/cadical/test/cnf/sat1.cnf | 5 + tools/cadical/test/cnf/sat1.sol | 2 + tools/cadical/test/cnf/sat10.cnf | 9 + tools/cadical/test/cnf/sat10.sol | 2 + tools/cadical/test/cnf/sat11.cnf | 9 + tools/cadical/test/cnf/sat11.sol | 2 + tools/cadical/test/cnf/sat12.cnf | 9 + tools/cadical/test/cnf/sat12.sol | 2 + tools/cadical/test/cnf/sat13.cnf | 9 + tools/cadical/test/cnf/sat13.sol | 2 + tools/cadical/test/cnf/sat2.cnf | 5 + tools/cadical/test/cnf/sat2.sol | 2 + tools/cadical/test/cnf/sat3.cnf | 5 + tools/cadical/test/cnf/sat3.sol | 2 + tools/cadical/test/cnf/sat4.cnf | 5 + tools/cadical/test/cnf/sat4.sol | 2 + tools/cadical/test/cnf/sat5.cnf | 9 + tools/cadical/test/cnf/sat6.cnf | 9 + tools/cadical/test/cnf/sat6.sol | 2 + tools/cadical/test/cnf/sat7.cnf | 9 + tools/cadical/test/cnf/sat7.sol | 2 + tools/cadical/test/cnf/sat8.cnf | 9 + tools/cadical/test/cnf/sat8.sol | 2 + tools/cadical/test/cnf/sat9.cnf | 9 + tools/cadical/test/cnf/sat9.sol | 2 + tools/cadical/test/cnf/sqrt10201.cnf | 842 ++ tools/cadical/test/cnf/sqrt10201.sol | 19 + tools/cadical/test/cnf/sqrt1042441.cnf | 1878 +++++ tools/cadical/test/cnf/sqrt1042441.sol | 42 + tools/cadical/test/cnf/sqrt10609.cnf | 842 ++ tools/cadical/test/cnf/sqrt10609.sol | 20 + tools/cadical/test/cnf/sqrt11449.cnf | 842 ++ tools/cadical/test/cnf/sqrt11449.sol | 20 + tools/cadical/test/cnf/sqrt11881.cnf | 842 ++ tools/cadical/test/cnf/sqrt11881.sol | 20 + tools/cadical/test/cnf/sqrt12769.cnf | 840 ++ tools/cadical/test/cnf/sqrt12769.sol | 19 + tools/cadical/test/cnf/sqrt16129.cnf | 840 ++ tools/cadical/test/cnf/sqrt16129.sol | 20 + tools/cadical/test/cnf/sqrt259081.cnf | 1487 ++++ tools/cadical/test/cnf/sqrt259081.sol | 33 + tools/cadical/test/cnf/sqrt2809.cnf | 586 ++ tools/cadical/test/cnf/sqrt2809.sol | 14 + tools/cadical/test/cnf/sqrt3481.cnf | 584 ++ tools/cadical/test/cnf/sqrt3481.sol | 14 + tools/cadical/test/cnf/sqrt3721.cnf | 584 ++ tools/cadical/test/cnf/sqrt3721.sol | 14 + tools/cadical/test/cnf/sqrt4489.cnf | 840 ++ tools/cadical/test/cnf/sqrt4489.sol | 19 + tools/cadical/test/cnf/sqrt5041.cnf | 840 ++ tools/cadical/test/cnf/sqrt5041.sol | 19 + tools/cadical/test/cnf/sqrt5329.cnf | 840 ++ tools/cadical/test/cnf/sqrt5329.sol | 19 + tools/cadical/test/cnf/sqrt6241.cnf | 840 ++ tools/cadical/test/cnf/sqrt6241.sol | 20 + tools/cadical/test/cnf/sqrt63001.cnf | 1141 +++ tools/cadical/test/cnf/sqrt63001.sol | 26 + tools/cadical/test/cnf/sqrt6889.cnf | 840 ++ tools/cadical/test/cnf/sqrt6889.sol | 20 + tools/cadical/test/cnf/sqrt7921.cnf | 840 ++ tools/cadical/test/cnf/sqrt7921.sol | 19 + tools/cadical/test/cnf/sqrt9409.cnf | 842 ++ tools/cadical/test/cnf/sqrt9409.sol | 19 + tools/cadical/test/cnf/sub0.cnf | 3 + tools/cadical/test/cnf/unit0.cnf | 2 + tools/cadical/test/cnf/unit0.sol | 2 + tools/cadical/test/cnf/unit1.cnf | 2 + tools/cadical/test/cnf/unit1.sol | 2 + tools/cadical/test/cnf/unit2.cnf | 3 + tools/cadical/test/cnf/unit2.sol | 2 + tools/cadical/test/cnf/unit3.cnf | 3 + tools/cadical/test/cnf/unit3.sol | 2 + tools/cadical/test/cnf/unit4.cnf | 4 + tools/cadical/test/cnf/unit5.cnf | 8 + tools/cadical/test/cnf/unit6.cnf | 5 + tools/cadical/test/cnf/unit7.cnf | 6 + tools/cadical/test/contrib/README.md | 8 + tools/cadical/test/contrib/craigtracer.cpp | 39 + .../test/contrib/craigtracer_incremental.cpp | 73 + tools/cadical/test/contrib/makefile | 3 + tools/cadical/test/contrib/run.sh | 118 + tools/cadical/test/icnf/empty.icnf | 1 + tools/cadical/test/icnf/false.icnf | 2 + tools/cadical/test/icnf/makefile | 3 + tools/cadical/test/icnf/prime49.icnf | 632 ++ tools/cadical/test/icnf/run.sh | 87 + tools/cadical/test/icnf/two1.icnf | 7 + tools/cadical/test/icnf/two2.icnf | 7 + tools/cadical/test/icnf/unit1.icnf | 3 + tools/cadical/test/icnf/unit2.icnf | 3 + tools/cadical/test/makefile | 16 + tools/cadical/test/mbt/README.md | 7 + tools/cadical/test/mbt/makefile | 3 + tools/cadical/test/mbt/run.sh | 63 + tools/cadical/test/trace/README.md | 6 + tools/cadical/test/trace/makefile | 3 + tools/cadical/test/trace/reg0000.trace | 18 + tools/cadical/test/trace/reg0001.trace | 4 + tools/cadical/test/trace/reg0002.trace | 8 + tools/cadical/test/trace/reg0003.trace | 9 + tools/cadical/test/trace/reg0004.trace | 12 + tools/cadical/test/trace/reg0005.trace | 11 + tools/cadical/test/trace/reg0006.trace | 11 + tools/cadical/test/trace/reg0007.trace | 7 + tools/cadical/test/trace/reg0008.trace | 39 + tools/cadical/test/trace/reg0009.trace | 7 + tools/cadical/test/trace/reg0010.trace | 10 + tools/cadical/test/trace/reg0011.trace | 9 + tools/cadical/test/trace/reg0012.trace | 11 + tools/cadical/test/trace/reg0013.trace | 9 + tools/cadical/test/trace/reg0014.trace | 11 + tools/cadical/test/trace/reg0015.trace | 18 + tools/cadical/test/trace/reg0016.trace | 15 + tools/cadical/test/trace/reg0017.trace | 18 + tools/cadical/test/trace/reg0018.trace | 23 + tools/cadical/test/trace/reg0019.trace | 23 + tools/cadical/test/trace/reg0020.trace | 16 + tools/cadical/test/trace/reg0021.trace | 10 + tools/cadical/test/trace/reg0022.trace | 5 + tools/cadical/test/trace/reg0023.trace | 8 + tools/cadical/test/trace/reg0024.trace | 19 + tools/cadical/test/trace/reg0025.trace | 5 + tools/cadical/test/trace/reg0026.trace | 23 + tools/cadical/test/trace/reg0027.trace | 86 + tools/cadical/test/trace/reg0028.trace | 11 + tools/cadical/test/trace/reg0029.trace | 61 + tools/cadical/test/trace/reg0030.trace | 29 + tools/cadical/test/trace/reg0031.trace | 44 + tools/cadical/test/trace/reg0032.trace | 12 + tools/cadical/test/trace/reg0033.trace | 27 + tools/cadical/test/trace/reg0034.trace | 10 + tools/cadical/test/trace/reg0035.trace | 19 + tools/cadical/test/trace/reg0036.trace | 9 + tools/cadical/test/trace/reg0037.trace | 21 + tools/cadical/test/trace/reg0038.trace | 32 + tools/cadical/test/trace/reg0039.trace | 12 + tools/cadical/test/trace/reg0040.trace | 28 + tools/cadical/test/trace/reg0041.trace | 62 + tools/cadical/test/trace/reg0042.trace | 35 + tools/cadical/test/trace/reg0043.trace | 27 + tools/cadical/test/trace/reg0044.trace | 10 + tools/cadical/test/trace/reg0045.trace | 13 + tools/cadical/test/trace/reg0046.trace | 12 + tools/cadical/test/trace/reg0047.trace | 12 + tools/cadical/test/trace/reg0048.trace | 69 + tools/cadical/test/trace/reg0049.trace | 28 + tools/cadical/test/trace/reg0050.trace | 28 + tools/cadical/test/trace/reg0051.trace | 39 + tools/cadical/test/trace/reg0052.trace | 67 + tools/cadical/test/trace/reg0053.trace | 3 + tools/cadical/test/trace/reg0054.trace | 5 + tools/cadical/test/trace/reg0055.trace | 14 + tools/cadical/test/trace/reg0056.trace | 390 + tools/cadical/test/trace/reg0057.trace | 54 + tools/cadical/test/trace/reg0058.trace | 54 + tools/cadical/test/trace/reg0059.trace | 10 + tools/cadical/test/trace/reg0060.trace | 44 + tools/cadical/test/trace/reg0061.trace | 12 + tools/cadical/test/trace/reg0062.trace | 18 + tools/cadical/test/trace/reg0063.trace | 26 + tools/cadical/test/trace/reg0064.trace | 17 + tools/cadical/test/trace/reg0065.trace | 17 + tools/cadical/test/trace/reg0066.trace | 45 + tools/cadical/test/trace/reg0067.trace | 10 + tools/cadical/test/trace/reg0068.trace | 18 + tools/cadical/test/trace/reg0069.trace | 12 + tools/cadical/test/trace/reg0070.trace | 70 + tools/cadical/test/trace/reg0071.trace | 55 + tools/cadical/test/trace/reg0072.trace | 155 + tools/cadical/test/trace/reg0073.trace | 69 + tools/cadical/test/trace/reg0074.trace | 35 + tools/cadical/test/trace/reg0075.trace | 16 + tools/cadical/test/trace/reg0076.trace | 7 + tools/cadical/test/trace/reg0077.trace | 9 + tools/cadical/test/trace/reg0078.trace | 8 + tools/cadical/test/trace/run.sh | 96 + tools/cadical/test/usage/README.md | 8 + tools/cadical/test/usage/makefile | 3 + tools/cadical/test/usage/missing-clause.cnf | 2 + tools/cadical/test/usage/relaxed-header.cnf | 5 + tools/cadical/test/usage/run.sh | 149 + .../cadical/test/usage/variable-too-large.cnf | 2 + 448 files changed, 138078 insertions(+) create mode 100755 tools/build_cadical.sh create mode 100644 tools/cadical/.clang-format create mode 100644 tools/cadical/.dockerignore create mode 100644 tools/cadical/BUILD.md create mode 100644 tools/cadical/CONTRIBUTING.md create mode 100644 tools/cadical/Dockerfile create mode 100644 tools/cadical/LICENSE create mode 100644 tools/cadical/NEWS.md create mode 100644 tools/cadical/README.md create mode 100644 tools/cadical/VERSION create mode 100755 tools/cadical/configure create mode 100644 tools/cadical/contrib/craigtracer.LICENSE.APACHE create mode 100644 tools/cadical/contrib/craigtracer.LICENSE.MIT create mode 100644 tools/cadical/contrib/craigtracer.cpp create mode 100644 tools/cadical/contrib/craigtracer.hpp create mode 100644 tools/cadical/contrib/craigtracer.md create mode 100644 tools/cadical/makefile create mode 100644 tools/cadical/makefile.in create mode 100644 tools/cadical/scripts/README.md create mode 100755 tools/cadical/scripts/build-and-test-all-configurations.sh create mode 100755 tools/cadical/scripts/check-options-occur.sh create mode 100644 tools/cadical/scripts/colors.sh create mode 100755 tools/cadical/scripts/extend-solution.sh create mode 100755 tools/cadical/scripts/generate-cubes.sh create mode 100755 tools/cadical/scripts/generate-embedded-options-default-list.sh create mode 100755 tools/cadical/scripts/generate-options-range-list.sh create mode 100755 tools/cadical/scripts/get-git-id.sh create mode 100755 tools/cadical/scripts/make-build-header.sh create mode 100755 tools/cadical/scripts/make-src-release.sh create mode 100755 tools/cadical/scripts/normalize-white-space.sh create mode 100755 tools/cadical/scripts/prepare-sc2021-submission.sh create mode 100755 tools/cadical/scripts/run-cadical-and-check-proof.sh create mode 100755 tools/cadical/scripts/run-simplifier-and-extend-solution.sh create mode 100755 tools/cadical/scripts/update-example-in-cadical-header-file.sh create mode 100755 tools/cadical/scripts/update-version.sh create mode 100644 tools/cadical/src/README.md create mode 100644 tools/cadical/src/analyze.cpp create mode 100644 tools/cadical/src/arena.cpp create mode 100644 tools/cadical/src/arena.hpp create mode 100644 tools/cadical/src/assume.cpp create mode 100644 tools/cadical/src/averages.cpp create mode 100644 tools/cadical/src/averages.hpp create mode 100644 tools/cadical/src/backtrack.cpp create mode 100644 tools/cadical/src/backward.cpp create mode 100644 tools/cadical/src/bins.cpp create mode 100644 tools/cadical/src/bins.hpp create mode 100644 tools/cadical/src/block.cpp create mode 100644 tools/cadical/src/block.hpp create mode 100644 tools/cadical/src/cadical.cpp create mode 100644 tools/cadical/src/cadical.hpp create mode 100644 tools/cadical/src/ccadical.cpp create mode 100644 tools/cadical/src/ccadical.h create mode 100644 tools/cadical/src/checker.cpp create mode 100644 tools/cadical/src/checker.hpp create mode 100644 tools/cadical/src/clause.cpp create mode 100644 tools/cadical/src/clause.hpp create mode 100644 tools/cadical/src/collect.cpp create mode 100644 tools/cadical/src/compact.cpp create mode 100644 tools/cadical/src/condition.cpp create mode 100644 tools/cadical/src/config.cpp create mode 100644 tools/cadical/src/config.hpp create mode 120000 tools/cadical/src/configure create mode 100644 tools/cadical/src/constrain.cpp create mode 100644 tools/cadical/src/contract.cpp create mode 100644 tools/cadical/src/contract.hpp create mode 100644 tools/cadical/src/cover.cpp create mode 100644 tools/cadical/src/cover.hpp create mode 100644 tools/cadical/src/decide.cpp create mode 100644 tools/cadical/src/decompose.cpp create mode 100644 tools/cadical/src/decompose.hpp create mode 100644 tools/cadical/src/deduplicate.cpp create mode 100644 tools/cadical/src/drattracer.cpp create mode 100644 tools/cadical/src/drattracer.hpp create mode 100644 tools/cadical/src/elim.cpp create mode 100644 tools/cadical/src/elim.hpp create mode 100644 tools/cadical/src/ema.cpp create mode 100644 tools/cadical/src/ema.hpp create mode 100644 tools/cadical/src/extend.cpp create mode 100644 tools/cadical/src/external.cpp create mode 100644 tools/cadical/src/external.hpp create mode 100644 tools/cadical/src/external_propagate.cpp create mode 100644 tools/cadical/src/file.cpp create mode 100644 tools/cadical/src/file.hpp create mode 100644 tools/cadical/src/flags.cpp create mode 100644 tools/cadical/src/flags.hpp create mode 100644 tools/cadical/src/flip.cpp create mode 100644 tools/cadical/src/format.cpp create mode 100644 tools/cadical/src/format.hpp create mode 100644 tools/cadical/src/frattracer.cpp create mode 100644 tools/cadical/src/frattracer.hpp create mode 100644 tools/cadical/src/gates.cpp create mode 100644 tools/cadical/src/heap.hpp create mode 100644 tools/cadical/src/idruptracer.cpp create mode 100644 tools/cadical/src/idruptracer.hpp create mode 100644 tools/cadical/src/instantiate.cpp create mode 100644 tools/cadical/src/instantiate.hpp create mode 100644 tools/cadical/src/internal.cpp create mode 100644 tools/cadical/src/internal.hpp create mode 100644 tools/cadical/src/inttypes.hpp create mode 100644 tools/cadical/src/ipasir.cpp create mode 100644 tools/cadical/src/ipasir.h create mode 100644 tools/cadical/src/level.hpp create mode 100644 tools/cadical/src/lidruptracer.cpp create mode 100644 tools/cadical/src/lidruptracer.hpp create mode 100644 tools/cadical/src/limit.cpp create mode 100644 tools/cadical/src/limit.hpp create mode 100644 tools/cadical/src/logging.cpp create mode 100644 tools/cadical/src/logging.hpp create mode 100644 tools/cadical/src/lookahead.cpp create mode 100644 tools/cadical/src/lratbuilder.cpp create mode 100644 tools/cadical/src/lratbuilder.hpp create mode 100644 tools/cadical/src/lratchecker.cpp create mode 100644 tools/cadical/src/lratchecker.hpp create mode 100644 tools/cadical/src/lrattracer.cpp create mode 100644 tools/cadical/src/lrattracer.hpp create mode 100644 tools/cadical/src/lucky.cpp create mode 120000 tools/cadical/src/makefile create mode 100644 tools/cadical/src/message.cpp create mode 100644 tools/cadical/src/message.hpp create mode 100644 tools/cadical/src/minimize.cpp create mode 100644 tools/cadical/src/mobical.cpp create mode 100644 tools/cadical/src/occs.cpp create mode 100644 tools/cadical/src/occs.hpp create mode 100644 tools/cadical/src/options.cpp create mode 100644 tools/cadical/src/options.hpp create mode 100644 tools/cadical/src/parse.cpp create mode 100644 tools/cadical/src/parse.hpp create mode 100644 tools/cadical/src/phases.cpp create mode 100644 tools/cadical/src/phases.hpp create mode 100644 tools/cadical/src/probe.cpp create mode 100644 tools/cadical/src/profile.cpp create mode 100644 tools/cadical/src/profile.hpp create mode 100644 tools/cadical/src/proof.cpp create mode 100644 tools/cadical/src/proof.hpp create mode 100644 tools/cadical/src/propagate.cpp create mode 100644 tools/cadical/src/queue.cpp create mode 100644 tools/cadical/src/queue.hpp create mode 100644 tools/cadical/src/radix.hpp create mode 100644 tools/cadical/src/random.cpp create mode 100644 tools/cadical/src/random.hpp create mode 100644 tools/cadical/src/range.hpp create mode 100644 tools/cadical/src/reap.cpp create mode 100644 tools/cadical/src/reap.hpp create mode 100644 tools/cadical/src/reduce.cpp create mode 100644 tools/cadical/src/reluctant.hpp create mode 100644 tools/cadical/src/rephase.cpp create mode 100644 tools/cadical/src/report.cpp create mode 100644 tools/cadical/src/resources.cpp create mode 100644 tools/cadical/src/resources.hpp create mode 100644 tools/cadical/src/restart.cpp create mode 100644 tools/cadical/src/restore.cpp create mode 100644 tools/cadical/src/score.cpp create mode 100644 tools/cadical/src/score.hpp create mode 100644 tools/cadical/src/shrink.cpp create mode 100644 tools/cadical/src/signal.cpp create mode 100644 tools/cadical/src/signal.hpp create mode 100644 tools/cadical/src/solution.cpp create mode 100644 tools/cadical/src/solver.cpp create mode 100644 tools/cadical/src/stats.cpp create mode 100644 tools/cadical/src/stats.hpp create mode 100644 tools/cadical/src/subsume.cpp create mode 100644 tools/cadical/src/terminal.cpp create mode 100644 tools/cadical/src/terminal.hpp create mode 100644 tools/cadical/src/ternary.cpp create mode 100644 tools/cadical/src/tracer.hpp create mode 100644 tools/cadical/src/transred.cpp create mode 100644 tools/cadical/src/util.cpp create mode 100644 tools/cadical/src/util.hpp create mode 100644 tools/cadical/src/var.cpp create mode 100644 tools/cadical/src/var.hpp create mode 100644 tools/cadical/src/veripbtracer.cpp create mode 100644 tools/cadical/src/veripbtracer.hpp create mode 100644 tools/cadical/src/version.cpp create mode 100644 tools/cadical/src/version.hpp create mode 100644 tools/cadical/src/vivify.cpp create mode 100644 tools/cadical/src/vivify.hpp create mode 100644 tools/cadical/src/walk.cpp create mode 100644 tools/cadical/src/watch.cpp create mode 100644 tools/cadical/src/watch.hpp create mode 100644 tools/cadical/test/README.md create mode 100644 tools/cadical/test/api/README.md create mode 100644 tools/cadical/test/api/apitrace.cpp create mode 100644 tools/cadical/test/api/cfreeze.c create mode 100644 tools/cadical/test/api/cipasir.c create mode 100644 tools/cadical/test/api/ctest.c create mode 100644 tools/cadical/test/api/example.cpp create mode 100644 tools/cadical/test/api/example_constraint.cpp create mode 100644 tools/cadical/test/api/example_tracer.cpp create mode 100644 tools/cadical/test/api/incproof.cpp create mode 100644 tools/cadical/test/api/learn.cpp create mode 100644 tools/cadical/test/api/makefile create mode 100644 tools/cadical/test/api/morenmore.cpp create mode 100644 tools/cadical/test/api/newdelete.cpp create mode 100755 tools/cadical/test/api/run.sh create mode 100644 tools/cadical/test/api/terminate.cpp create mode 100644 tools/cadical/test/api/traverse.cpp create mode 100644 tools/cadical/test/api/unit.cpp create mode 100644 tools/cadical/test/cnf/README.md create mode 100644 tools/cadical/test/cnf/add128.cnf create mode 100644 tools/cadical/test/cnf/add16.cnf create mode 100644 tools/cadical/test/cnf/add32.cnf create mode 100644 tools/cadical/test/cnf/add4.cnf create mode 100644 tools/cadical/test/cnf/add64.cnf create mode 100644 tools/cadical/test/cnf/add8.cnf create mode 100644 tools/cadical/test/cnf/block0.cnf create mode 100644 tools/cadical/test/cnf/drat-trim.c create mode 100644 tools/cadical/test/cnf/elimclash.cnf create mode 100644 tools/cadical/test/cnf/elimredundant.cnf create mode 100644 tools/cadical/test/cnf/empty.cnf create mode 100644 tools/cadical/test/cnf/empty.sol create mode 100644 tools/cadical/test/cnf/factor2708413neg.cnf create mode 100644 tools/cadical/test/cnf/factor2708413pos.cnf create mode 100644 tools/cadical/test/cnf/false.cnf create mode 100644 tools/cadical/test/cnf/full1.cnf create mode 100644 tools/cadical/test/cnf/full2.cnf create mode 100644 tools/cadical/test/cnf/full3.cnf create mode 100644 tools/cadical/test/cnf/full4.cnf create mode 100644 tools/cadical/test/cnf/full5.cnf create mode 100644 tools/cadical/test/cnf/full6.cnf create mode 100644 tools/cadical/test/cnf/full7.cnf create mode 100644 tools/cadical/test/cnf/lrat-trim.c create mode 100644 tools/cadical/test/cnf/makefile create mode 100644 tools/cadical/test/cnf/ph2.cnf create mode 100644 tools/cadical/test/cnf/ph3.cnf create mode 100644 tools/cadical/test/cnf/ph4.cnf create mode 100644 tools/cadical/test/cnf/ph5.cnf create mode 100644 tools/cadical/test/cnf/ph6.cnf create mode 100644 tools/cadical/test/cnf/precochk.c create mode 100644 tools/cadical/test/cnf/prime121.cnf create mode 100644 tools/cadical/test/cnf/prime121.sol create mode 100644 tools/cadical/test/cnf/prime1369.cnf create mode 100644 tools/cadical/test/cnf/prime1369.sol create mode 100644 tools/cadical/test/cnf/prime1681.cnf create mode 100644 tools/cadical/test/cnf/prime1681.sol create mode 100644 tools/cadical/test/cnf/prime169.cnf create mode 100644 tools/cadical/test/cnf/prime169.sol create mode 100644 tools/cadical/test/cnf/prime1849.cnf create mode 100644 tools/cadical/test/cnf/prime1849.sol create mode 100644 tools/cadical/test/cnf/prime2209.cnf create mode 100644 tools/cadical/test/cnf/prime2209.sol create mode 100644 tools/cadical/test/cnf/prime25.cnf create mode 100644 tools/cadical/test/cnf/prime25.sol create mode 100644 tools/cadical/test/cnf/prime289.cnf create mode 100644 tools/cadical/test/cnf/prime289.sol create mode 100644 tools/cadical/test/cnf/prime361.cnf create mode 100644 tools/cadical/test/cnf/prime361.sol create mode 100644 tools/cadical/test/cnf/prime4.cnf create mode 100644 tools/cadical/test/cnf/prime4.sol create mode 100644 tools/cadical/test/cnf/prime4294967297.cnf create mode 100644 tools/cadical/test/cnf/prime49.cnf create mode 100644 tools/cadical/test/cnf/prime49.sol create mode 100644 tools/cadical/test/cnf/prime529.cnf create mode 100644 tools/cadical/test/cnf/prime529.sol create mode 100644 tools/cadical/test/cnf/prime65537.cnf create mode 100644 tools/cadical/test/cnf/prime841.cnf create mode 100644 tools/cadical/test/cnf/prime841.sol create mode 100644 tools/cadical/test/cnf/prime9.cnf create mode 100644 tools/cadical/test/cnf/prime9.sol create mode 100644 tools/cadical/test/cnf/prime961.cnf create mode 100644 tools/cadical/test/cnf/prime961.sol create mode 100644 tools/cadical/test/cnf/regr000.cnf create mode 100644 tools/cadical/test/cnf/regr000.sol create mode 100755 tools/cadical/test/cnf/run.sh create mode 100644 tools/cadical/test/cnf/sat0.cnf create mode 100644 tools/cadical/test/cnf/sat1.cnf create mode 100644 tools/cadical/test/cnf/sat1.sol create mode 100644 tools/cadical/test/cnf/sat10.cnf create mode 100644 tools/cadical/test/cnf/sat10.sol create mode 100644 tools/cadical/test/cnf/sat11.cnf create mode 100644 tools/cadical/test/cnf/sat11.sol create mode 100644 tools/cadical/test/cnf/sat12.cnf create mode 100644 tools/cadical/test/cnf/sat12.sol create mode 100644 tools/cadical/test/cnf/sat13.cnf create mode 100644 tools/cadical/test/cnf/sat13.sol create mode 100644 tools/cadical/test/cnf/sat2.cnf create mode 100644 tools/cadical/test/cnf/sat2.sol create mode 100644 tools/cadical/test/cnf/sat3.cnf create mode 100644 tools/cadical/test/cnf/sat3.sol create mode 100644 tools/cadical/test/cnf/sat4.cnf create mode 100644 tools/cadical/test/cnf/sat4.sol create mode 100644 tools/cadical/test/cnf/sat5.cnf create mode 100644 tools/cadical/test/cnf/sat6.cnf create mode 100644 tools/cadical/test/cnf/sat6.sol create mode 100644 tools/cadical/test/cnf/sat7.cnf create mode 100644 tools/cadical/test/cnf/sat7.sol create mode 100644 tools/cadical/test/cnf/sat8.cnf create mode 100644 tools/cadical/test/cnf/sat8.sol create mode 100644 tools/cadical/test/cnf/sat9.cnf create mode 100644 tools/cadical/test/cnf/sat9.sol create mode 100644 tools/cadical/test/cnf/sqrt10201.cnf create mode 100644 tools/cadical/test/cnf/sqrt10201.sol create mode 100644 tools/cadical/test/cnf/sqrt1042441.cnf create mode 100644 tools/cadical/test/cnf/sqrt1042441.sol create mode 100644 tools/cadical/test/cnf/sqrt10609.cnf create mode 100644 tools/cadical/test/cnf/sqrt10609.sol create mode 100644 tools/cadical/test/cnf/sqrt11449.cnf create mode 100644 tools/cadical/test/cnf/sqrt11449.sol create mode 100644 tools/cadical/test/cnf/sqrt11881.cnf create mode 100644 tools/cadical/test/cnf/sqrt11881.sol create mode 100644 tools/cadical/test/cnf/sqrt12769.cnf create mode 100644 tools/cadical/test/cnf/sqrt12769.sol create mode 100644 tools/cadical/test/cnf/sqrt16129.cnf create mode 100644 tools/cadical/test/cnf/sqrt16129.sol create mode 100644 tools/cadical/test/cnf/sqrt259081.cnf create mode 100644 tools/cadical/test/cnf/sqrt259081.sol create mode 100644 tools/cadical/test/cnf/sqrt2809.cnf create mode 100644 tools/cadical/test/cnf/sqrt2809.sol create mode 100644 tools/cadical/test/cnf/sqrt3481.cnf create mode 100644 tools/cadical/test/cnf/sqrt3481.sol create mode 100644 tools/cadical/test/cnf/sqrt3721.cnf create mode 100644 tools/cadical/test/cnf/sqrt3721.sol create mode 100644 tools/cadical/test/cnf/sqrt4489.cnf create mode 100644 tools/cadical/test/cnf/sqrt4489.sol create mode 100644 tools/cadical/test/cnf/sqrt5041.cnf create mode 100644 tools/cadical/test/cnf/sqrt5041.sol create mode 100644 tools/cadical/test/cnf/sqrt5329.cnf create mode 100644 tools/cadical/test/cnf/sqrt5329.sol create mode 100644 tools/cadical/test/cnf/sqrt6241.cnf create mode 100644 tools/cadical/test/cnf/sqrt6241.sol create mode 100644 tools/cadical/test/cnf/sqrt63001.cnf create mode 100644 tools/cadical/test/cnf/sqrt63001.sol create mode 100644 tools/cadical/test/cnf/sqrt6889.cnf create mode 100644 tools/cadical/test/cnf/sqrt6889.sol create mode 100644 tools/cadical/test/cnf/sqrt7921.cnf create mode 100644 tools/cadical/test/cnf/sqrt7921.sol create mode 100644 tools/cadical/test/cnf/sqrt9409.cnf create mode 100644 tools/cadical/test/cnf/sqrt9409.sol create mode 100644 tools/cadical/test/cnf/sub0.cnf create mode 100644 tools/cadical/test/cnf/unit0.cnf create mode 100644 tools/cadical/test/cnf/unit0.sol create mode 100644 tools/cadical/test/cnf/unit1.cnf create mode 100644 tools/cadical/test/cnf/unit1.sol create mode 100644 tools/cadical/test/cnf/unit2.cnf create mode 100644 tools/cadical/test/cnf/unit2.sol create mode 100644 tools/cadical/test/cnf/unit3.cnf create mode 100644 tools/cadical/test/cnf/unit3.sol create mode 100644 tools/cadical/test/cnf/unit4.cnf create mode 100644 tools/cadical/test/cnf/unit5.cnf create mode 100644 tools/cadical/test/cnf/unit6.cnf create mode 100644 tools/cadical/test/cnf/unit7.cnf create mode 100644 tools/cadical/test/contrib/README.md create mode 100644 tools/cadical/test/contrib/craigtracer.cpp create mode 100644 tools/cadical/test/contrib/craigtracer_incremental.cpp create mode 100644 tools/cadical/test/contrib/makefile create mode 100755 tools/cadical/test/contrib/run.sh create mode 100644 tools/cadical/test/icnf/empty.icnf create mode 100644 tools/cadical/test/icnf/false.icnf create mode 100644 tools/cadical/test/icnf/makefile create mode 100644 tools/cadical/test/icnf/prime49.icnf create mode 100755 tools/cadical/test/icnf/run.sh create mode 100644 tools/cadical/test/icnf/two1.icnf create mode 100644 tools/cadical/test/icnf/two2.icnf create mode 100644 tools/cadical/test/icnf/unit1.icnf create mode 100644 tools/cadical/test/icnf/unit2.icnf create mode 100644 tools/cadical/test/makefile create mode 100644 tools/cadical/test/mbt/README.md create mode 100644 tools/cadical/test/mbt/makefile create mode 100755 tools/cadical/test/mbt/run.sh create mode 100644 tools/cadical/test/trace/README.md create mode 100644 tools/cadical/test/trace/makefile create mode 100644 tools/cadical/test/trace/reg0000.trace create mode 100644 tools/cadical/test/trace/reg0001.trace create mode 100644 tools/cadical/test/trace/reg0002.trace create mode 100644 tools/cadical/test/trace/reg0003.trace create mode 100644 tools/cadical/test/trace/reg0004.trace create mode 100644 tools/cadical/test/trace/reg0005.trace create mode 100644 tools/cadical/test/trace/reg0006.trace create mode 100644 tools/cadical/test/trace/reg0007.trace create mode 100644 tools/cadical/test/trace/reg0008.trace create mode 100644 tools/cadical/test/trace/reg0009.trace create mode 100644 tools/cadical/test/trace/reg0010.trace create mode 100644 tools/cadical/test/trace/reg0011.trace create mode 100644 tools/cadical/test/trace/reg0012.trace create mode 100644 tools/cadical/test/trace/reg0013.trace create mode 100644 tools/cadical/test/trace/reg0014.trace create mode 100644 tools/cadical/test/trace/reg0015.trace create mode 100644 tools/cadical/test/trace/reg0016.trace create mode 100644 tools/cadical/test/trace/reg0017.trace create mode 100644 tools/cadical/test/trace/reg0018.trace create mode 100644 tools/cadical/test/trace/reg0019.trace create mode 100644 tools/cadical/test/trace/reg0020.trace create mode 100644 tools/cadical/test/trace/reg0021.trace create mode 100644 tools/cadical/test/trace/reg0022.trace create mode 100644 tools/cadical/test/trace/reg0023.trace create mode 100644 tools/cadical/test/trace/reg0024.trace create mode 100644 tools/cadical/test/trace/reg0025.trace create mode 100644 tools/cadical/test/trace/reg0026.trace create mode 100644 tools/cadical/test/trace/reg0027.trace create mode 100644 tools/cadical/test/trace/reg0028.trace create mode 100644 tools/cadical/test/trace/reg0029.trace create mode 100644 tools/cadical/test/trace/reg0030.trace create mode 100644 tools/cadical/test/trace/reg0031.trace create mode 100644 tools/cadical/test/trace/reg0032.trace create mode 100644 tools/cadical/test/trace/reg0033.trace create mode 100644 tools/cadical/test/trace/reg0034.trace create mode 100644 tools/cadical/test/trace/reg0035.trace create mode 100644 tools/cadical/test/trace/reg0036.trace create mode 100644 tools/cadical/test/trace/reg0037.trace create mode 100644 tools/cadical/test/trace/reg0038.trace create mode 100644 tools/cadical/test/trace/reg0039.trace create mode 100644 tools/cadical/test/trace/reg0040.trace create mode 100644 tools/cadical/test/trace/reg0041.trace create mode 100644 tools/cadical/test/trace/reg0042.trace create mode 100644 tools/cadical/test/trace/reg0043.trace create mode 100644 tools/cadical/test/trace/reg0044.trace create mode 100644 tools/cadical/test/trace/reg0045.trace create mode 100644 tools/cadical/test/trace/reg0046.trace create mode 100644 tools/cadical/test/trace/reg0047.trace create mode 100644 tools/cadical/test/trace/reg0048.trace create mode 100644 tools/cadical/test/trace/reg0049.trace create mode 100644 tools/cadical/test/trace/reg0050.trace create mode 100644 tools/cadical/test/trace/reg0051.trace create mode 100644 tools/cadical/test/trace/reg0052.trace create mode 100644 tools/cadical/test/trace/reg0053.trace create mode 100644 tools/cadical/test/trace/reg0054.trace create mode 100644 tools/cadical/test/trace/reg0055.trace create mode 100644 tools/cadical/test/trace/reg0056.trace create mode 100644 tools/cadical/test/trace/reg0057.trace create mode 100644 tools/cadical/test/trace/reg0058.trace create mode 100644 tools/cadical/test/trace/reg0059.trace create mode 100644 tools/cadical/test/trace/reg0060.trace create mode 100644 tools/cadical/test/trace/reg0061.trace create mode 100644 tools/cadical/test/trace/reg0062.trace create mode 100644 tools/cadical/test/trace/reg0063.trace create mode 100644 tools/cadical/test/trace/reg0064.trace create mode 100644 tools/cadical/test/trace/reg0065.trace create mode 100644 tools/cadical/test/trace/reg0066.trace create mode 100644 tools/cadical/test/trace/reg0067.trace create mode 100644 tools/cadical/test/trace/reg0068.trace create mode 100644 tools/cadical/test/trace/reg0069.trace create mode 100644 tools/cadical/test/trace/reg0070.trace create mode 100644 tools/cadical/test/trace/reg0071.trace create mode 100644 tools/cadical/test/trace/reg0072.trace create mode 100644 tools/cadical/test/trace/reg0073.trace create mode 100644 tools/cadical/test/trace/reg0074.trace create mode 100644 tools/cadical/test/trace/reg0075.trace create mode 100644 tools/cadical/test/trace/reg0076.trace create mode 100644 tools/cadical/test/trace/reg0077.trace create mode 100644 tools/cadical/test/trace/reg0078.trace create mode 100755 tools/cadical/test/trace/run.sh create mode 100644 tools/cadical/test/usage/README.md create mode 100644 tools/cadical/test/usage/makefile create mode 100644 tools/cadical/test/usage/missing-clause.cnf create mode 100644 tools/cadical/test/usage/relaxed-header.cnf create mode 100755 tools/cadical/test/usage/run.sh create mode 100644 tools/cadical/test/usage/variable-too-large.cnf diff --git a/CMakeLists.txt b/CMakeLists.txt index f144148c0c..02b362432d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -209,6 +209,26 @@ if (NOT MSVC AND ${ENABLE_OPENBLAS}) target_include_directories(${OPENBLAS_LIB} INTERFACE ${OPENBLAS_DIR}/installed/include) endif() +########## +## CaDiCaL ## +########## + +if (NOT CADICAL_DIR) + set(CADICAL_DIR "${TOOLS_DIR}/cadical") +endif() + +if(NOT EXISTS "${CADICAL_DIR}/build") + message("building CaDiCaL SAT Solver") + execute_process(COMMAND ${TOOLS_DIR}/build_cadical.sh) +endif() + +set(CADICAL_LIB cadical) +add_library(${CADICAL_LIB} SHARED IMPORTED) +set_property(TARGET ${CADICAL_LIB} PROPERTY POSITION_INDEPENDENT_CODE ON) +set_target_properties(${CADICAL_LIB} PROPERTIES IMPORTED_LOCATION ${CADICAL_DIR}/build/libcadical.a) +target_include_directories(${CADICAL_LIB} INTERFACE ${CADICAL_DIR}/src) +list(APPEND LIBS ${CADICAL_LIB}) + ########### ## Build ## ########### diff --git a/src/engine/Engine.h b/src/engine/Engine.h index feb9ac1279..9fba1046de 100644 --- a/src/engine/Engine.h +++ b/src/engine/Engine.h @@ -50,6 +50,7 @@ #include #include +#include #ifdef _WIN32 @@ -895,6 +896,9 @@ class Engine Writes the details of a contradiction to the UNSAT certificate node */ void writeContradictionToCertificate( unsigned infeasibleVar ) const; + + std::unique_ptr d_solver; + std::unique_ptr d_terminator; }; #endif // __Engine_h__ diff --git a/tools/build_cadical.sh b/tools/build_cadical.sh new file mode 100755 index 0000000000..24f2a0e2f1 --- /dev/null +++ b/tools/build_cadical.sh @@ -0,0 +1,12 @@ +#!/bin/bash +curdir=$pwd +mydir="${0%/*}" + +echo $mydir +cd $mydir +cd cadical +echo "building cadical" +./configure +make + +cd $curdir diff --git a/tools/cadical/.clang-format b/tools/cadical/.clang-format new file mode 100644 index 0000000000..300836e634 --- /dev/null +++ b/tools/cadical/.clang-format @@ -0,0 +1,4 @@ +AlignEscapedNewlines: DontAlign +ColumnLimit: 76 +SpaceBeforeParens: Always +SpaceAfterCStyleCast: true diff --git a/tools/cadical/.dockerignore b/tools/cadical/.dockerignore new file mode 100644 index 0000000000..94143827ed --- /dev/null +++ b/tools/cadical/.dockerignore @@ -0,0 +1 @@ +Dockerfile diff --git a/tools/cadical/BUILD.md b/tools/cadical/BUILD.md new file mode 100644 index 0000000000..5c7af7ec90 --- /dev/null +++ b/tools/cadical/BUILD.md @@ -0,0 +1,115 @@ +# CaDiCaL Build + +Use `./configure && make` to configure and build `cadical` in the default +`build` sub-directory. + +This will also build the library `libcadical.a` as well as the model based +tester `mobical`: + + build/cadical + build/mobical + build/libcadical.a + +The header file of the library is in + + src/cadical.hpp + +The build process requires GNU make. Using the generated `makefile` with +GNU make compiles separate object files, which can be cached (for instance +with `ccache`). In order to force parallel build you can use the '-j' +option either for 'configure' or with 'make'. If the environment variable +'MAKEFLAGS' is set, e.g., 'MAKEFLAGS=-j ./configure', the same effect +is achieved and the generated makefile will use those flags. + +Options +------- + +You might want to check out options of `./configure -h`, such as + + ./configure -c # include assertion checking code + + ./configure -l # include code to really see what the solver is doing + + ./configure -a # both above and in addition `-g` for debugging. + +You can easily use multiple build directories, e.g., + + mkdir debug; cd debug; ../configure -g; make + +which compiles and builds a debugging version in the sub-directory `debug`, +since `-g` was specified as parameter to `configure`. The object files, +the library and the binaries are all independent of those in the default +build directory `build`. + +All source files reside in the `src` directory. The library `libcadical.a` +is compiled from all the `.cpp` files except `cadical.cpp` and +`mobical.cpp`, which provide the applications, i.e., the stand alone solver +`cadical` and the model based tester `mobical`. + +Manual Build +------------ + +If you can not or do not want to rely on our `configure` script nor on our +build system based on GNU `make`, then this is easily doable as follows. + + mkdir build + cd build + for f in ../src/*.cpp; do g++ -O3 -DNDEBUG -DNBUILD -c $f; done + ar rc libcadical.a `ls *.o | grep -v ical.o` + g++ -o cadical cadical.o -L. -lcadical + g++ -o mobical mobical.o -L. -lcadical + +Note that application object files are excluded from the library. +Of course you can use different compilation options as well. + +Since `build.hpp` is not generated in this flow the `-DNBUILD` flag is +necessary though, which avoids dependency of `version.cpp` on `build.hpp`. +Consequently you will only get very basic version information compiled into +the library and binaries (guaranteed is in essence just the version number +of the library). + +And if you really do not care about compilation time nor caching and just +want to build the solver once manually then the following also works. + + g++ -O3 -DNDEBUG -DNBUILD -o cadical `ls *.cpp | grep -v mobical` + +Further note that the `configure` script provides some feature checks and +might generate additional compiler flags necessary for compilation. You +might need to set those yourself or just use a modern C++11 compiler. + +This manual build process using object files is fast enough in combination +with caching solutions such as `ccache`. But it lacks the ability of our +GNU make solution to run compilation in parallel without additional parallel +process scheduling solutions. + +Cross-Compilation +----------------- + +We have preliminary support for cross-compilation using MinGW32 (only +tested for a Linux compilation host and Windows-64 target host at this +point). + +There are two steps necessary to make this work. First make +sure to be able to execute binaries compiled with the cross-compiler +directly. Otherwise 'configure' does not work automatically and you +have to build manually (as described above). + +For instance in order to use `wine` to execute the binaries first install +`wine` which for instance on Ubuntu just requires + + sudo apt install wine + +Then on Linux you might want to look into the `binfmt_misc` module and +as root register the appropriate interpreter for `DOSWin`. + + cd /proc/sys/fs/binfmt_misc + echo ':DOSWin:M::MZ::/usr/bin/wine:' > register + +Finally simply tell the `configure` script to use the cross-compiler. + + CXX=i686-w64-mingw32-g++ ./configure -static -lpsapi && make cadical + +Note the use of '-static', which was necessary for me since by default +`wine` did not find `libstdc++` if dynamically linked. There is also +a dependency on the 'psapi' library. Also `mobical` does not compile with +MinGW32 due to too many Unix dependencies and thus only make 'cadical'. diff --git a/tools/cadical/CONTRIBUTING.md b/tools/cadical/CONTRIBUTING.md new file mode 100644 index 0000000000..fc31b78bc9 --- /dev/null +++ b/tools/cadical/CONTRIBUTING.md @@ -0,0 +1,48 @@ +# Contributing + +CaDiCaL is distributed under the MIT license (see [LICENSE](LICENSE) file). +By submitting a contribution you automatically accept the conditions +described in [LICENSE](LICENSE). Additionally, we ask you to certify that +you have the right to submit such contributions. To manage this +process we use a mechanism known as Developer Certificate of Origin, +which can be acknowledged by signing-off your commits with `git +commit -s`. + +**We require all pull requests to be squashed into a single commit +and signed-off.** + +``` +Developer Certificate of Origin +Version 1.1 + +Copyright (C) 2004, 2006 The Linux Foundation and its contributors. + +Everyone is permitted to copy and distribute verbatim copies of this +license document, but changing it is not allowed. + +Developer's Certificate of Origin 1.1 + +By making a contribution to this project, I certify that: + +(a) The contribution was created in whole or in part by me and I + have the right to submit it under the open source license + indicated in the file; or + +(b) The contribution is based upon previous work that, to the best + of my knowledge, is covered under an appropriate open source + license and I have the right under that license to submit that + work with modifications, whether created in whole or in part + by me, under the same open source license (unless I am + permitted to submit under a different license), as indicated + in the file; or + +(c) The contribution was provided directly to me by some other + person who certified (a), (b) or (c) and I have not modified + it. + +(d) I understand and agree that this project and the contribution + are public and that a record of the contribution (including all + personal information I submit with it, including my sign-off) is + maintained indefinitely and may be redistributed consistent with + this project or the open source license(s) involved. +``` diff --git a/tools/cadical/Dockerfile b/tools/cadical/Dockerfile new file mode 100644 index 0000000000..2d270e3fb4 --- /dev/null +++ b/tools/cadical/Dockerfile @@ -0,0 +1,34 @@ +# ----------------------------------------------------------------------------- +# Builder container +# ----------------------------------------------------------------------------- +FROM ubuntu:22.04 as builder + +ENV DEBIAN_FRONTEND "noninteractive" +ENV TZ "Europe/Berlin" + +# Install compiler, build tools and required libraries +RUN apt-get update \ + && apt-get install -y --no-install-recommends build-essential g++ \ + && apt-get clean + +COPY . /work + +WORKDIR /work +RUN ./configure \ + && make + +# ----------------------------------------------------------------------------- +# Runtime container +# ----------------------------------------------------------------------------- + +FROM ubuntu:22.04 as runner + +ENV DEBIAN_FRONTEND "noninteractive" +ENV TZ "Europe/Berlin" + +COPY --from=builder /work/build/cadical /cadical/cadical +COPY --from=builder /work/build/mobical /cadical/mobical + +WORKDIR /cadical +ENTRYPOINT ["/cadical/cadical"] +CMD ["--help"] diff --git a/tools/cadical/LICENSE b/tools/cadical/LICENSE new file mode 100644 index 0000000000..a951f69535 --- /dev/null +++ b/tools/cadical/LICENSE @@ -0,0 +1,27 @@ +MIT License + +Copyright (c) 2016-2021 Armin Biere, Johannes Kepler University Linz, Austria +Copyright (c) 2020-2021 Mathias Fleury, Johannes Kepler University Linz, Austria +Copyright (c) 2020-2021 Nils Froleyks, Johannes Kepler University Linz, Austria +Copyright (c) 2022-2024 Katalin Fazekas, Vienna University of Technology, Austria +Copyright (c) 2021-2024 Armin Biere, University of Freiburg, Germany +Copyright (c) 2021-2024 Mathias Fleury, University of Freiburg, Germany +Copyright (c) 2023-2024 Florian Pollitt, University of Freiburg, Germany + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/tools/cadical/NEWS.md b/tools/cadical/NEWS.md new file mode 100644 index 0000000000..462c190464 --- /dev/null +++ b/tools/cadical/NEWS.md @@ -0,0 +1,241 @@ +Version 2.0.0 +------------- + +- We have now a `contrib` directory and for starters there our + `CadiCraig` interpolator, which goes through the `Tracer` API. + +- We moved back to use the C99 flexible array member feature in + `Clause` which however is not supported by all C++ compiler + configurations, particularly if compiling in pedantic mode. + Therefore the `configure` script checks for support of flexible + array members and also has a new `--no-flexible` option. + +- Added `Dockerfile` to support docker containers. + +- Added `--no-status` to skip printing "s SATISFIABLE" or "s + UNSATISFIABLE". This is useful for online proof checking. + +Version 1.9.5 +------------- + +- Removed an unexpected performance regression on the anniversary track + due to marking forward strengthened redundant clauses as used. + +Version 1.9.4 +------------- + +- Simplified code by removing reimply again (but keeping ILB). + +Version 1.9.3 +------------- + +- Fixed bogus notification if a user propagator is connected + with ILB and after local search preprocessing and a second incremental + call lead to an inconsistent trail to assumption mapping, which might + have lead to an infinite loop (in very rare cases). + +Version 1.9.2 +------------- + +- Important fixes for ILB, trail-reuse and external propagation with + assumptions. + +- Restored effectiveness of Mobical and improved external mock + propagator. + +- Forced garbage collection of binary clauses before restore. + +- Merge internal status and state encodings and made them consistent. + +- Disabled non-verbose message if empty clause found in input. + +- Improved support for IDRUP. + +Version 1.9.1 +------------- + +- Fixed position of `idrup` option. + +Version 1.9.0 +------------- + +- Clause IDs in binary LRAT proofs are now always signed. + +- Internal CNF regression suite also checks LRAT proofs now. + +- Improving the OTFS heuristic (properly bumping literals and + considering that the conflict clause is updated). + +- Making progress to formal 1.9 release with minor fixes for + different platforms and compilers. + +Version 1.8.0 +------------- + +- Explicit `Solver::clause` functions to simplify clause addition. + +- More fine-grained handling of printing proof size information by + adding `bool print = false` flags to the `flush_proof_trace` and + the `close_proof_trace` API calls. The former prints the number + of addition and deletion steps, while the latter prints the size + of the proof size (and the actual number of bytes if compressed). + The main effect is that by default printing of proof size disabled + for API usage but enabled for the stand-alone solver. + +Version 1.7.5 +------------- + +- Decreased verbosity level for printing proof size. + +Version 1.7.4 +------------- + +- As `fork` and `wait` do not exist on Windows writing compressed files + through `pipe/fork/exec/wait` has to be disabled for Windows cross + compilation to go through. Alternatively one could go back to `popen` + for writing compressed files on Windows which however is not safe and + therefore we simply decided to disable that feature for windows. + Compressed file reading still (and as far we are aware safely) uses + `popen` and thus also compiles for Windows. + +Version 1.7.3 +------------- + +- Replaced the unsafe `popen` approach for compressed file writing + with an explicit `pipe/fork/exec/waitpid` flow and accordingly + removed the `--safe` configuration option again. + +- Incremental lazy backtracking (ILB) enabled by `--ilb` allows + to add new clauses incrementally while keeping the assignments + on the trail. Also works for assumptions (`--ilbassumptions`). + +- Reimplication (`--reimply`) fixes assignment levels of literals by + "elevating" them (assigning a lower decision level and propating them + out-of-order on this lower decision level). Out-of-order assignments + are introduced by chronological backtracking, adding external clauses + during solving (e.g., by a user propagation) or simply by ILB. + Reimplication improves quality of learned clauses and potentially + shortens search in such cases. + +- A new proof tracer interface allows to add a proof `Tracer` through the + API (via `connect_proof_tracer`). This feature allows to use custom + proof tracers to process clausal proofs on-the-fly while solving. Both + proofs steps with proof antecedents (needed for instance for + interpolation) as well as without (working direclty on DRAT level) are + supported. + +- Reworked options for proof tracing to be less confusing. Support for + DRAT, LRAT, FRAT and VeriPB (with or without antecedents). + +Version 1.7.2 +------------- + +- Configuration option `--safe` disables writing to a file + through `popen` which makes library usage safer. + +Version 1.7.1 +------------- + +- Added support for VeriPB proofs (--lrat --lratveripb). + +- Various fixes: LRAT proofs for constrain (which previously were + not traced correctly); internal-external mapping issues for LRAT + (worked for user propagator but now also in combination with LRAT); + further minor bug fixes. + +- Added support for LRAT + external propagator in combination. + +Version 1.7.0 +------------- + +- Added native LRAT support. + +Version 1.6.0 +------------- + +- Added IPASIR-UP functions to the API to support external propagation, + external decisions, and clause addition during search. + For more details see the following paper at SAT 2023: + + Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, + Stefan Szeider and Armin Biere. IPASIR-UP: User Propagators for CDCL. + +- During decisions the phase set by `void phase (int lit)` has now + higher precedence than the initial phase set by options `phase` and + `forcephase`. + +Version 1.5.6 +------------- + +- Clang formatted all source code (and fixed one failing regression + test by disabling `otfs` for it). + +- Implementing OTFS during conflict analysis (`--otfs`). + +- The last literal set by vivification is instantiated (`--vivifyinst`). + +- More accurate tracking of binary clauses in watch lists by updating + the size in watch lists. + +Version 1.5.4 +------------- + +- Picking highest score literal in assumed clause (`constrain`) + and caching of satisfied literal by moving them to the front. + +- Added `bool flippable (int lit)` to API. + +- Fixed `val` to return `lit` or `-lit` and not just `-1` and `1`. + +- Allowing `fixed` between `constrain` in `mobical`. + +- Fixed LZMA magic header. + +- Added `bool flip (int lit)` to API. + +- Fixed different garbage collection times with and without + clause IDs (with `./configure -l` or just `./configure`). + This solves issue #44 by John Reeves. At the same time + made sure to trigger garbage collection independent on the + number of clause header bytes by relying on the number of + garbage literals instead. + +- Fixed `mmap` usage for FreeBSD (#48 issue of `yurivict`). + +- Removed several compiler warnings when using newer compilers, + including gcc-11, gcc-12, clang-14, and clang-15. + +- Replaced `sprintf` by `snprintf` to avoid warning on MacOS + (thanks to Marijn for bringing this up). + +- Assigning a C `FILE` pointer to `stdout` during initialization + fails on MacOS and thus separated declaration and initialization. + +- Fixed random seed initialization from MAC address issue #47 + as used by `mobical` which produces segmentation faults + (thanks to Sam Bayless for pointing this out). + +Version 1.5.2 +------------- + +- Updates to documentation and copyright. + +Version 1.5.2 +------------- + +- More copyright updates in banner. + +- Fixed MinGW cross-compilation (see `BUILD.md`). + +Version 1.5.1 +------------- + +- Fixed copyright and added two regression traces. + +Version 1.5.0 +------------- + +- Added `constrain` API call described in our FMCAD'21 paper. + +- Replaced `while () push_back ()` with `if () resize ()` idiom + (thanks go to Alexander Smal for pointing this out). diff --git a/tools/cadical/README.md b/tools/cadical/README.md new file mode 100644 index 0000000000..2fc45bb021 --- /dev/null +++ b/tools/cadical/README.md @@ -0,0 +1,55 @@ +[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT) + + +CaDiCaL Simplified Satisfiability Solver +=============================================================================== + +The goal of the development of CaDiCaL was to obtain a CDCL solver, +which is easy to understand and change, while at the same time not being +much slower than other state-of-the-art CDCL solvers. + +Originally we wanted to also radically simplify the design and internal data +structures, but that goal was only achieved partially, at least for instance +compared to Lingeling. + +However, the code is much better documented and CaDiCaL actually became in +general faster than Lingeling even though it is missing some preprocessors +(mostly parity and cardinality constraint reasoning), which would be crucial +to solve certain instances. + +Use `./configure && make` to configure and build `cadical` and the library +`libcadical.a` in the default `build` sub-directory. The header file of +the library is [`src/cadical.hpp`](src/cadical.hpp) and includes an example +for API usage. + +See [`BUILD.md`](BUILD.md) for options and more details related to the build +process and [`test/README.md`](test/README.md) for testing the library and +the solver. Since release 1.5.1 we have a [`NEWS.md`](NEWS.md) file. +You might also want to check out [`CONTRIBUTING.md`](CONTRIBUTING.md) on +if you want to contribute. + +The solver has the following usage `cadical [ dimacs [ proof ] ]`. +See `cadical -h` for more options. + +If you want to cite CaDiCaL please use the solver description in the +latest SAT competition proceedings: + +
+  @inproceedings{BiereFazekasFleuryHeisinger-SAT-Competition-2020-solvers,
+    author    = {Armin Biere and Katalin Fazekas and Mathias Fleury and Maximillian Heisinger},
+    title     = {{CaDiCaL}, {Kissat}, {Paracooba}, {Plingeling} and {Treengeling}
+		 Entering the {SAT Competition 2020}},
+    pages     = {51--53},
+    editor    = {Tomas Balyo and Nils Froleyks and Marijn Heule and 
+		 Markus Iser and Matti J{\"a}rvisalo and Martin Suda},
+    booktitle = {Proc.~of {SAT Competition} 2020 -- Solver and Benchmark Descriptions},
+    volume    = {B-2020-1},
+    series    = {Department of Computer Science Report Series B},
+    publisher = {University of Helsinki},
+    year      = 2020,
+  }
+
+ +You might also find more information on CaDiCaL at . + +Armin Biere diff --git a/tools/cadical/VERSION b/tools/cadical/VERSION new file mode 100644 index 0000000000..227cea2156 --- /dev/null +++ b/tools/cadical/VERSION @@ -0,0 +1 @@ +2.0.0 diff --git a/tools/cadical/configure b/tools/cadical/configure new file mode 100755 index 0000000000..87ca8cd28f --- /dev/null +++ b/tools/cadical/configure @@ -0,0 +1,557 @@ +#!/bin/sh + +#--------------------------------------------------------------------------# + +# Run './configure' to produce a 'makefile' in the 'build' sub-directory or +# in any immediate sub-directory different from the 'src', 'scripts' and +# 'test' directories. + +#--------------------------------------------------------------------------# + +rm -f configure.log + +#--------------------------------------------------------------------------# + +# Common default options. + +all=no +debug=no +libs="" +logging=no +check=no +competition=no +coverage=no +flexible=yes +profile=no +contracts=yes +tracing=yes +unlocked=yes +pedantic=no +options="" +quiet=no +m32=no +contrib=yes + +#--------------------------------------------------------------------------# + +if [ -f ./scripts/colors.sh ] +then + . ./scripts/colors.sh +elif [ -f ../scripts/colors.sh ] +then + . ../scripts/colors.sh +else + BAD="" + HILITE="" + BOLD="" + NORMAL="" +fi + +die () { + if [ -f configure.log ] + then + checklog=" (check also 'configure.log')" + else + checklog="" + fi + cecho "${BOLD}configure:${NORMAL} ${BAD}error:${NORMAL} $*${checklog}" + exit 1 +} + +rm -f configure.log + +msg () { + cecho "${BOLD}configure:${NORMAL} $*" +} + +# if we can find the 'color.sh' script source it and overwrite color codes + +for dir in . .. +do + [ -f $dir/scripts/colors.sh ] || continue + . $dir/scripts/colors.sh || exit 1 + break +done + +#--------------------------------------------------------------------------# + +# Parse and handle command line options. + +usage () { +cat << EOF +usage: configure [