From cf2763a5e83e07d5a4955ff2bcda412d0eb851a6 Mon Sep 17 00:00:00 2001 From: YuhangQ Date: Sun, 23 Oct 2022 14:08:48 +0800 Subject: [PATCH] remove CEC code --- .gitignore | 3 +- .vscode/settings.json | 8 - acec.cpp | 399 +-- acec.log | 0 aiger.c | 2775 --------------- aiger.h | 359 -- circuit.cpp | 449 --- circuit.hpp | 16 - cms.log | 408 --- fraig.cpp | 291 -- hCaD_V2/BUILD.md | 104 - hCaD_V2/CONTRIBUTING | 4 - hCaD_V2/LICENSE | 22 - hCaD_V2/README.md | 54 - hCaD_V2/VERSION | 1 - hCaD_V2/bin/starexec_run_default | 2 - hCaD_V2/configure | 494 --- hCaD_V2/makefile | 24 - hCaD_V2/makefile.in | 84 - hCaD_V2/scripts/README.md | 42 - .../build-and-test-all-configurations.sh | 115 - hCaD_V2/scripts/check-options-occur.sh | 11 - hCaD_V2/scripts/colors.sh | 29 - hCaD_V2/scripts/extend-solution.sh | 75 - hCaD_V2/scripts/generate-cubes.sh | 37 - .../generate-embedded-options-default-list.sh | 13 - .../scripts/generate-options-range-list.sh | 18 - hCaD_V2/scripts/get-git-id.sh | 3 - hCaD_V2/scripts/make-build-header.sh | 92 - hCaD_V2/scripts/make-src-release.sh | 36 - hCaD_V2/scripts/normalize-white-space.sh | 8 - hCaD_V2/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 - hCaD_V2/scripts/update-version.sh | 12 - hCaD_V2/src/README.md | 12 - hCaD_V2/src/analyze.cpp | 830 ----- hCaD_V2/src/arena.cpp | 30 - hCaD_V2/src/arena.hpp | 103 - hCaD_V2/src/assume.cpp | 178 - hCaD_V2/src/averages.cpp | 30 - hCaD_V2/src/averages.hpp | 36 - hCaD_V2/src/backtrack.cpp | 125 - hCaD_V2/src/backward.cpp | 148 - hCaD_V2/src/bins.cpp | 22 - hCaD_V2/src/bins.hpp | 17 - hCaD_V2/src/block.cpp | 751 ---- hCaD_V2/src/block.hpp | 37 - hCaD_V2/src/cadical.cpp | 933 ----- hCaD_V2/src/cadical.hpp | 891 ----- hCaD_V2/src/ccadical.cpp | 172 - hCaD_V2/src/ccadical.h | 63 - hCaD_V2/src/checker.cpp | 555 --- hCaD_V2/src/checker.hpp | 165 - hCaD_V2/src/clause.cpp | 442 --- hCaD_V2/src/clause.hpp | 151 - hCaD_V2/src/collect.cpp | 429 --- hCaD_V2/src/compact.cpp | 416 --- hCaD_V2/src/condition.cpp | 898 ----- hCaD_V2/src/config.cpp | 97 - hCaD_V2/src/config.hpp | 20 - hCaD_V2/src/configure | 494 --- hCaD_V2/src/contract.cpp | 27 - hCaD_V2/src/contract.hpp | 112 - hCaD_V2/src/cover.cpp | 588 ---- hCaD_V2/src/cover.hpp | 33 - hCaD_V2/src/decide.cpp | 123 - hCaD_V2/src/decompose.cpp | 361 -- hCaD_V2/src/deduplicate.cpp | 139 - hCaD_V2/src/elim.cpp | 960 ----- hCaD_V2/src/elim.hpp | 37 - hCaD_V2/src/ema.cpp | 95 - hCaD_V2/src/ema.hpp | 61 - hCaD_V2/src/extend.cpp | 208 -- hCaD_V2/src/external.cpp | 541 --- hCaD_V2/src/external.hpp | 356 -- hCaD_V2/src/file.cpp | 306 -- hCaD_V2/src/file.hpp | 177 - hCaD_V2/src/flags.cpp | 119 - hCaD_V2/src/flags.hpp | 76 - hCaD_V2/src/format.cpp | 81 - hCaD_V2/src/format.hpp | 33 - hCaD_V2/src/gates.cpp | 527 --- hCaD_V2/src/heap.hpp | 198 -- hCaD_V2/src/instantiate.cpp | 241 -- hCaD_V2/src/instantiate.hpp | 47 - hCaD_V2/src/internal.cpp | 739 ---- hCaD_V2/src/internal.hpp | 1351 -------- hCaD_V2/src/ipasir.cpp | 48 - hCaD_V2/src/ipasir.h | 38 - hCaD_V2/src/level.hpp | 30 - hCaD_V2/src/limit.cpp | 122 - hCaD_V2/src/limit.hpp | 68 - hCaD_V2/src/logging.cpp | 133 - hCaD_V2/src/logging.hpp | 79 - hCaD_V2/src/lookahead.cpp | 504 --- hCaD_V2/src/lucky.cpp | 307 -- hCaD_V2/src/makefile | 1 - hCaD_V2/src/message.cpp | 206 -- hCaD_V2/src/message.hpp | 40 - hCaD_V2/src/minimize.cpp | 104 - hCaD_V2/src/mobical.cpp | 3082 ----------------- hCaD_V2/src/observer.hpp | 33 - hCaD_V2/src/occs.cpp | 38 - hCaD_V2/src/occs.hpp | 35 - hCaD_V2/src/options.cpp | 336 -- hCaD_V2/src/options.hpp | 347 -- hCaD_V2/src/parse.cpp | 368 -- hCaD_V2/src/parse.hpp | 75 - hCaD_V2/src/phases.cpp | 38 - hCaD_V2/src/phases.hpp | 19 - hCaD_V2/src/probe.cpp | 687 ---- hCaD_V2/src/profile.cpp | 108 - hCaD_V2/src/profile.hpp | 258 -- hCaD_V2/src/proof.cpp | 186 - hCaD_V2/src/proof.hpp | 64 - hCaD_V2/src/propagate.cpp | 382 -- hCaD_V2/src/queue.cpp | 86 - hCaD_V2/src/queue.hpp | 53 - hCaD_V2/src/radix.hpp | 167 - hCaD_V2/src/random.cpp | 205 -- hCaD_V2/src/random.hpp | 87 - hCaD_V2/src/range.hpp | 93 - hCaD_V2/src/reap.cpp | 130 - hCaD_V2/src/reap.hpp | 31 - hCaD_V2/src/reduce.cpp | 212 -- hCaD_V2/src/reluctant.hpp | 70 - hCaD_V2/src/rephase.cpp | 229 -- hCaD_V2/src/report.cpp | 248 -- hCaD_V2/src/resources.cpp | 145 - hCaD_V2/src/resources.hpp | 14 - hCaD_V2/src/restart.cpp | 109 - hCaD_V2/src/restore.cpp | 220 -- hCaD_V2/src/score.cpp | 49 - hCaD_V2/src/score.hpp | 16 - hCaD_V2/src/shrink.cpp | 446 --- hCaD_V2/src/signal.cpp | 132 - hCaD_V2/src/signal.hpp | 34 - hCaD_V2/src/solution.cpp | 49 - hCaD_V2/src/solver.cpp | 1273 ------- hCaD_V2/src/stats.cpp | 307 -- hCaD_V2/src/stats.hpp | 231 -- hCaD_V2/src/subsume.cpp | 612 ---- hCaD_V2/src/terminal.cpp | 34 - hCaD_V2/src/terminal.hpp | 93 - hCaD_V2/src/ternary.cpp | 365 -- hCaD_V2/src/tracer.cpp | 86 - hCaD_V2/src/tracer.hpp | 36 - hCaD_V2/src/transred.cpp | 196 -- hCaD_V2/src/util.cpp | 132 - hCaD_V2/src/util.hpp | 121 - hCaD_V2/src/var.cpp | 33 - hCaD_V2/src/var.hpp | 22 - hCaD_V2/src/version.cpp | 97 - hCaD_V2/src/version.hpp | 11 - hCaD_V2/src/vivify.cpp | 1097 ------ hCaD_V2/src/vivify.hpp | 23 - hCaD_V2/src/walk.cpp | 667 ---- hCaD_V2/src/watch.cpp | 100 - hCaD_V2/src/watch.hpp | 49 - hCaD_V2/starexec_build | 5 - hCaD_V2/starexec_description.txt | 1 - hCaD_V2/test/README.md | 55 - hCaD_V2/test/api/README.md | 8 - hCaD_V2/test/api/apitrace.cpp | 77 - hCaD_V2/test/api/cfreeze.c | 94 - hCaD_V2/test/api/cipasir.c | 114 - hCaD_V2/test/api/ctest.c | 30 - hCaD_V2/test/api/example.cpp | 64 - hCaD_V2/test/api/learn.cpp | 58 - hCaD_V2/test/api/makefile | 3 - hCaD_V2/test/api/morenmore.cpp | 20 - hCaD_V2/test/api/newdelete.cpp | 6 - hCaD_V2/test/api/run.sh | 123 - hCaD_V2/test/api/terminate.cpp | 49 - hCaD_V2/test/api/traverse.cpp | 144 - hCaD_V2/test/api/unit.cpp | 22 - hCaD_V2/test/cnf/README.md | 23 - hCaD_V2/test/cnf/drat-trim.c | 1610 --------- hCaD_V2/test/cnf/empty.sol | 2 - hCaD_V2/test/cnf/makefile | 3 - hCaD_V2/test/cnf/precochk.c | 251 -- hCaD_V2/test/cnf/prime121.sol | 20 - hCaD_V2/test/cnf/prime1369.sol | 61 - hCaD_V2/test/cnf/prime1681.sol | 61 - hCaD_V2/test/cnf/prime169.sol | 28 - hCaD_V2/test/cnf/prime1849.sol | 61 - hCaD_V2/test/cnf/prime2209.sol | 77 - hCaD_V2/test/cnf/prime25.sol | 8 - hCaD_V2/test/cnf/prime289.sol | 38 - hCaD_V2/test/cnf/prime361.sol | 38 - hCaD_V2/test/cnf/prime4.sol | 2 - hCaD_V2/test/cnf/prime49.sol | 13 - hCaD_V2/test/cnf/prime529.sol | 49 - hCaD_V2/test/cnf/prime841.sol | 49 - hCaD_V2/test/cnf/prime9.sol | 4 - hCaD_V2/test/cnf/prime961.sol | 48 - hCaD_V2/test/cnf/regr000.sol | 2 - hCaD_V2/test/cnf/run.sh | 314 -- hCaD_V2/test/cnf/sat1.sol | 2 - hCaD_V2/test/cnf/sat10.sol | 2 - hCaD_V2/test/cnf/sat11.sol | 2 - hCaD_V2/test/cnf/sat12.sol | 2 - hCaD_V2/test/cnf/sat13.sol | 2 - hCaD_V2/test/cnf/sat2.sol | 2 - hCaD_V2/test/cnf/sat3.sol | 2 - hCaD_V2/test/cnf/sat4.sol | 2 - hCaD_V2/test/cnf/sat6.sol | 2 - hCaD_V2/test/cnf/sat7.sol | 2 - hCaD_V2/test/cnf/sat8.sol | 2 - hCaD_V2/test/cnf/sat9.sol | 2 - hCaD_V2/test/cnf/sqrt10201.sol | 19 - hCaD_V2/test/cnf/sqrt1042441.sol | 42 - hCaD_V2/test/cnf/sqrt10609.sol | 20 - hCaD_V2/test/cnf/sqrt11449.sol | 20 - hCaD_V2/test/cnf/sqrt11881.sol | 20 - hCaD_V2/test/cnf/sqrt12769.sol | 19 - hCaD_V2/test/cnf/sqrt16129.sol | 20 - hCaD_V2/test/cnf/sqrt259081.sol | 33 - hCaD_V2/test/cnf/sqrt2809.sol | 14 - hCaD_V2/test/cnf/sqrt3481.sol | 14 - hCaD_V2/test/cnf/sqrt3721.sol | 14 - hCaD_V2/test/cnf/sqrt4489.sol | 19 - hCaD_V2/test/cnf/sqrt5041.sol | 19 - hCaD_V2/test/cnf/sqrt5329.sol | 19 - hCaD_V2/test/cnf/sqrt6241.sol | 20 - hCaD_V2/test/cnf/sqrt63001.sol | 26 - hCaD_V2/test/cnf/sqrt6889.sol | 20 - hCaD_V2/test/cnf/sqrt7921.sol | 19 - hCaD_V2/test/cnf/sqrt9409.sol | 19 - hCaD_V2/test/cnf/unit0.sol | 2 - hCaD_V2/test/cnf/unit1.sol | 2 - hCaD_V2/test/cnf/unit2.sol | 2 - hCaD_V2/test/cnf/unit3.sol | 2 - hCaD_V2/test/icnf/empty.icnf | 1 - hCaD_V2/test/icnf/false.icnf | 2 - hCaD_V2/test/icnf/makefile | 3 - hCaD_V2/test/icnf/run.sh | 87 - hCaD_V2/test/icnf/two1.icnf | 7 - hCaD_V2/test/icnf/two2.icnf | 7 - hCaD_V2/test/icnf/unit1.icnf | 3 - hCaD_V2/test/icnf/unit2.icnf | 3 - hCaD_V2/test/makefile | 14 - hCaD_V2/test/mbt/README.md | 7 - hCaD_V2/test/mbt/makefile | 3 - hCaD_V2/test/mbt/run.sh | 63 - hCaD_V2/test/trace/README.md | 6 - hCaD_V2/test/trace/makefile | 3 - hCaD_V2/test/trace/reg0000.trace | 18 - hCaD_V2/test/trace/reg0001.trace | 4 - hCaD_V2/test/trace/reg0002.trace | 8 - hCaD_V2/test/trace/reg0003.trace | 9 - hCaD_V2/test/trace/reg0004.trace | 12 - hCaD_V2/test/trace/reg0005.trace | 11 - hCaD_V2/test/trace/reg0006.trace | 11 - hCaD_V2/test/trace/reg0007.trace | 7 - hCaD_V2/test/trace/reg0008.trace | 39 - hCaD_V2/test/trace/reg0009.trace | 7 - hCaD_V2/test/trace/reg0010.trace | 10 - hCaD_V2/test/trace/reg0011.trace | 9 - hCaD_V2/test/trace/reg0012.trace | 11 - hCaD_V2/test/trace/reg0013.trace | 9 - hCaD_V2/test/trace/reg0014.trace | 11 - hCaD_V2/test/trace/reg0015.trace | 18 - hCaD_V2/test/trace/reg0016.trace | 15 - hCaD_V2/test/trace/reg0017.trace | 18 - hCaD_V2/test/trace/reg0018.trace | 23 - hCaD_V2/test/trace/reg0019.trace | 23 - hCaD_V2/test/trace/reg0020.trace | 16 - hCaD_V2/test/trace/reg0021.trace | 10 - hCaD_V2/test/trace/reg0022.trace | 5 - hCaD_V2/test/trace/reg0023.trace | 8 - hCaD_V2/test/trace/reg0024.trace | 19 - hCaD_V2/test/trace/reg0025.trace | 5 - hCaD_V2/test/trace/reg0026.trace | 23 - hCaD_V2/test/trace/reg0027.trace | 86 - hCaD_V2/test/trace/reg0028.trace | 11 - hCaD_V2/test/trace/reg0029.trace | 61 - hCaD_V2/test/trace/reg0030.trace | 29 - hCaD_V2/test/trace/reg0031.trace | 44 - hCaD_V2/test/trace/reg0032.trace | 12 - hCaD_V2/test/trace/reg0033.trace | 27 - hCaD_V2/test/trace/reg0034.trace | 10 - hCaD_V2/test/trace/reg0035.trace | 19 - hCaD_V2/test/trace/reg0036.trace | 9 - hCaD_V2/test/trace/reg0037.trace | 21 - hCaD_V2/test/trace/reg0038.trace | 32 - hCaD_V2/test/trace/reg0039.trace | 12 - hCaD_V2/test/trace/reg0040.trace | 28 - hCaD_V2/test/trace/reg0041.trace | 62 - hCaD_V2/test/trace/reg0042.trace | 35 - hCaD_V2/test/trace/reg0043.trace | 27 - hCaD_V2/test/trace/reg0044.trace | 10 - hCaD_V2/test/trace/reg0045.trace | 13 - hCaD_V2/test/trace/reg0046.trace | 12 - hCaD_V2/test/trace/reg0047.trace | 12 - hCaD_V2/test/trace/reg0048.trace | 69 - hCaD_V2/test/trace/reg0049.trace | 28 - hCaD_V2/test/trace/reg0050.trace | 28 - hCaD_V2/test/trace/reg0051.trace | 39 - hCaD_V2/test/trace/reg0052.trace | 67 - hCaD_V2/test/trace/reg0053.trace | 3 - hCaD_V2/test/trace/reg0054.trace | 5 - hCaD_V2/test/trace/reg0055.trace | 14 - hCaD_V2/test/trace/reg0056.trace | 393 --- hCaD_V2/test/trace/run.sh | 96 - hCaD_V2/test/usage/README.md | 8 - hCaD_V2/test/usage/makefile | 3 - hCaD_V2/test/usage/missing-clause.cnf | 2 - hCaD_V2/test/usage/relaxed-header.cnf | 5 - hCaD_V2/test/usage/run.sh | 149 - hCaD_V2/test/usage/variable-too-large.cnf | 2 - makefile | 7 +- result.smt | 428 --- result.txt | 56 - smt.result | 591 ---- sweep.cpp | 267 -- sweep.hpp | 108 - test.smt | 5 - vec.hpp | 95 - 321 files changed, 186 insertions(+), 45422 deletions(-) delete mode 100644 .vscode/settings.json delete mode 100644 acec.log delete mode 100644 aiger.c delete mode 100644 aiger.h delete mode 100644 circuit.cpp delete mode 100644 circuit.hpp delete mode 100644 cms.log delete mode 100644 fraig.cpp delete mode 100644 hCaD_V2/BUILD.md delete mode 100644 hCaD_V2/CONTRIBUTING delete mode 100644 hCaD_V2/LICENSE delete mode 100644 hCaD_V2/README.md delete mode 100644 hCaD_V2/VERSION delete mode 100644 hCaD_V2/bin/starexec_run_default delete mode 100755 hCaD_V2/configure delete mode 100644 hCaD_V2/makefile delete mode 100644 hCaD_V2/makefile.in delete mode 100644 hCaD_V2/scripts/README.md delete mode 100755 hCaD_V2/scripts/build-and-test-all-configurations.sh delete mode 100755 hCaD_V2/scripts/check-options-occur.sh delete mode 100755 hCaD_V2/scripts/colors.sh delete mode 100755 hCaD_V2/scripts/extend-solution.sh delete mode 100755 hCaD_V2/scripts/generate-cubes.sh delete mode 100755 hCaD_V2/scripts/generate-embedded-options-default-list.sh delete mode 100755 hCaD_V2/scripts/generate-options-range-list.sh delete mode 100755 hCaD_V2/scripts/get-git-id.sh delete mode 100755 hCaD_V2/scripts/make-build-header.sh delete mode 100755 hCaD_V2/scripts/make-src-release.sh delete mode 100755 hCaD_V2/scripts/normalize-white-space.sh delete mode 100755 hCaD_V2/scripts/prepare-sc2021-submission.sh delete mode 100755 hCaD_V2/scripts/run-cadical-and-check-proof.sh delete mode 100755 hCaD_V2/scripts/run-simplifier-and-extend-solution.sh delete mode 100755 hCaD_V2/scripts/update-example-in-cadical-header-file.sh delete mode 100755 hCaD_V2/scripts/update-version.sh delete mode 100644 hCaD_V2/src/README.md delete mode 100644 hCaD_V2/src/analyze.cpp delete mode 100644 hCaD_V2/src/arena.cpp delete mode 100644 hCaD_V2/src/arena.hpp delete mode 100644 hCaD_V2/src/assume.cpp delete mode 100644 hCaD_V2/src/averages.cpp delete mode 100644 hCaD_V2/src/averages.hpp delete mode 100644 hCaD_V2/src/backtrack.cpp delete mode 100644 hCaD_V2/src/backward.cpp delete mode 100644 hCaD_V2/src/bins.cpp delete mode 100644 hCaD_V2/src/bins.hpp delete mode 100644 hCaD_V2/src/block.cpp delete mode 100644 hCaD_V2/src/block.hpp delete mode 100644 hCaD_V2/src/cadical.cpp delete mode 100644 hCaD_V2/src/cadical.hpp delete mode 100644 hCaD_V2/src/ccadical.cpp delete mode 100644 hCaD_V2/src/ccadical.h delete mode 100644 hCaD_V2/src/checker.cpp delete mode 100644 hCaD_V2/src/checker.hpp delete mode 100644 hCaD_V2/src/clause.cpp delete mode 100644 hCaD_V2/src/clause.hpp delete mode 100644 hCaD_V2/src/collect.cpp delete mode 100644 hCaD_V2/src/compact.cpp delete mode 100644 hCaD_V2/src/condition.cpp delete mode 100644 hCaD_V2/src/config.cpp delete mode 100644 hCaD_V2/src/config.hpp delete mode 100644 hCaD_V2/src/configure delete mode 100644 hCaD_V2/src/contract.cpp delete mode 100644 hCaD_V2/src/contract.hpp delete mode 100644 hCaD_V2/src/cover.cpp delete mode 100644 hCaD_V2/src/cover.hpp delete mode 100644 hCaD_V2/src/decide.cpp delete mode 100644 hCaD_V2/src/decompose.cpp delete mode 100644 hCaD_V2/src/deduplicate.cpp delete mode 100644 hCaD_V2/src/elim.cpp delete mode 100644 hCaD_V2/src/elim.hpp delete mode 100644 hCaD_V2/src/ema.cpp delete mode 100644 hCaD_V2/src/ema.hpp delete mode 100644 hCaD_V2/src/extend.cpp delete mode 100644 hCaD_V2/src/external.cpp delete mode 100644 hCaD_V2/src/external.hpp delete mode 100644 hCaD_V2/src/file.cpp delete mode 100644 hCaD_V2/src/file.hpp delete mode 100644 hCaD_V2/src/flags.cpp delete mode 100644 hCaD_V2/src/flags.hpp delete mode 100644 hCaD_V2/src/format.cpp delete mode 100644 hCaD_V2/src/format.hpp delete mode 100644 hCaD_V2/src/gates.cpp delete mode 100644 hCaD_V2/src/heap.hpp delete mode 100644 hCaD_V2/src/instantiate.cpp delete mode 100644 hCaD_V2/src/instantiate.hpp delete mode 100644 hCaD_V2/src/internal.cpp delete mode 100644 hCaD_V2/src/internal.hpp delete mode 100644 hCaD_V2/src/ipasir.cpp delete mode 100644 hCaD_V2/src/ipasir.h delete mode 100644 hCaD_V2/src/level.hpp delete mode 100644 hCaD_V2/src/limit.cpp delete mode 100644 hCaD_V2/src/limit.hpp delete mode 100644 hCaD_V2/src/logging.cpp delete mode 100644 hCaD_V2/src/logging.hpp delete mode 100644 hCaD_V2/src/lookahead.cpp delete mode 100644 hCaD_V2/src/lucky.cpp delete mode 120000 hCaD_V2/src/makefile delete mode 100644 hCaD_V2/src/message.cpp delete mode 100644 hCaD_V2/src/message.hpp delete mode 100644 hCaD_V2/src/minimize.cpp delete mode 100644 hCaD_V2/src/mobical.cpp delete mode 100644 hCaD_V2/src/observer.hpp delete mode 100644 hCaD_V2/src/occs.cpp delete mode 100644 hCaD_V2/src/occs.hpp delete mode 100644 hCaD_V2/src/options.cpp delete mode 100644 hCaD_V2/src/options.hpp delete mode 100644 hCaD_V2/src/parse.cpp delete mode 100644 hCaD_V2/src/parse.hpp delete mode 100644 hCaD_V2/src/phases.cpp delete mode 100644 hCaD_V2/src/phases.hpp delete mode 100644 hCaD_V2/src/probe.cpp delete mode 100644 hCaD_V2/src/profile.cpp delete mode 100644 hCaD_V2/src/profile.hpp delete mode 100644 hCaD_V2/src/proof.cpp delete mode 100644 hCaD_V2/src/proof.hpp delete mode 100644 hCaD_V2/src/propagate.cpp delete mode 100644 hCaD_V2/src/queue.cpp delete mode 100644 hCaD_V2/src/queue.hpp delete mode 100644 hCaD_V2/src/radix.hpp delete mode 100644 hCaD_V2/src/random.cpp delete mode 100644 hCaD_V2/src/random.hpp delete mode 100644 hCaD_V2/src/range.hpp delete mode 100644 hCaD_V2/src/reap.cpp delete mode 100644 hCaD_V2/src/reap.hpp delete mode 100644 hCaD_V2/src/reduce.cpp delete mode 100644 hCaD_V2/src/reluctant.hpp delete mode 100644 hCaD_V2/src/rephase.cpp delete mode 100644 hCaD_V2/src/report.cpp delete mode 100644 hCaD_V2/src/resources.cpp delete mode 100644 hCaD_V2/src/resources.hpp delete mode 100644 hCaD_V2/src/restart.cpp delete mode 100644 hCaD_V2/src/restore.cpp delete mode 100644 hCaD_V2/src/score.cpp delete mode 100644 hCaD_V2/src/score.hpp delete mode 100644 hCaD_V2/src/shrink.cpp delete mode 100644 hCaD_V2/src/signal.cpp delete mode 100644 hCaD_V2/src/signal.hpp delete mode 100644 hCaD_V2/src/solution.cpp delete mode 100644 hCaD_V2/src/solver.cpp delete mode 100644 hCaD_V2/src/stats.cpp delete mode 100644 hCaD_V2/src/stats.hpp delete mode 100644 hCaD_V2/src/subsume.cpp delete mode 100644 hCaD_V2/src/terminal.cpp delete mode 100644 hCaD_V2/src/terminal.hpp delete mode 100644 hCaD_V2/src/ternary.cpp delete mode 100644 hCaD_V2/src/tracer.cpp delete mode 100644 hCaD_V2/src/tracer.hpp delete mode 100644 hCaD_V2/src/transred.cpp delete mode 100644 hCaD_V2/src/util.cpp delete mode 100644 hCaD_V2/src/util.hpp delete mode 100644 hCaD_V2/src/var.cpp delete mode 100644 hCaD_V2/src/var.hpp delete mode 100644 hCaD_V2/src/version.cpp delete mode 100644 hCaD_V2/src/version.hpp delete mode 100644 hCaD_V2/src/vivify.cpp delete mode 100644 hCaD_V2/src/vivify.hpp delete mode 100644 hCaD_V2/src/walk.cpp delete mode 100644 hCaD_V2/src/watch.cpp delete mode 100644 hCaD_V2/src/watch.hpp delete mode 100644 hCaD_V2/starexec_build delete mode 100644 hCaD_V2/starexec_description.txt delete mode 100644 hCaD_V2/test/README.md delete mode 100644 hCaD_V2/test/api/README.md delete mode 100644 hCaD_V2/test/api/apitrace.cpp delete mode 100644 hCaD_V2/test/api/cfreeze.c delete mode 100644 hCaD_V2/test/api/cipasir.c delete mode 100644 hCaD_V2/test/api/ctest.c delete mode 100644 hCaD_V2/test/api/example.cpp delete mode 100644 hCaD_V2/test/api/learn.cpp delete mode 100644 hCaD_V2/test/api/makefile delete mode 100644 hCaD_V2/test/api/morenmore.cpp delete mode 100644 hCaD_V2/test/api/newdelete.cpp delete mode 100644 hCaD_V2/test/api/run.sh delete mode 100644 hCaD_V2/test/api/terminate.cpp delete mode 100644 hCaD_V2/test/api/traverse.cpp delete mode 100644 hCaD_V2/test/api/unit.cpp delete mode 100644 hCaD_V2/test/cnf/README.md delete mode 100644 hCaD_V2/test/cnf/drat-trim.c delete mode 100644 hCaD_V2/test/cnf/empty.sol delete mode 100644 hCaD_V2/test/cnf/makefile delete mode 100644 hCaD_V2/test/cnf/precochk.c delete mode 100644 hCaD_V2/test/cnf/prime121.sol delete mode 100644 hCaD_V2/test/cnf/prime1369.sol delete mode 100644 hCaD_V2/test/cnf/prime1681.sol delete mode 100644 hCaD_V2/test/cnf/prime169.sol delete mode 100644 hCaD_V2/test/cnf/prime1849.sol delete mode 100644 hCaD_V2/test/cnf/prime2209.sol delete mode 100644 hCaD_V2/test/cnf/prime25.sol delete mode 100644 hCaD_V2/test/cnf/prime289.sol delete mode 100644 hCaD_V2/test/cnf/prime361.sol delete mode 100644 hCaD_V2/test/cnf/prime4.sol delete mode 100644 hCaD_V2/test/cnf/prime49.sol delete mode 100644 hCaD_V2/test/cnf/prime529.sol delete mode 100644 hCaD_V2/test/cnf/prime841.sol delete mode 100644 hCaD_V2/test/cnf/prime9.sol delete mode 100644 hCaD_V2/test/cnf/prime961.sol delete mode 100644 hCaD_V2/test/cnf/regr000.sol delete mode 100644 hCaD_V2/test/cnf/run.sh delete mode 100644 hCaD_V2/test/cnf/sat1.sol delete mode 100644 hCaD_V2/test/cnf/sat10.sol delete mode 100644 hCaD_V2/test/cnf/sat11.sol delete mode 100644 hCaD_V2/test/cnf/sat12.sol delete mode 100644 hCaD_V2/test/cnf/sat13.sol delete mode 100644 hCaD_V2/test/cnf/sat2.sol delete mode 100644 hCaD_V2/test/cnf/sat3.sol delete mode 100644 hCaD_V2/test/cnf/sat4.sol delete mode 100644 hCaD_V2/test/cnf/sat6.sol delete mode 100644 hCaD_V2/test/cnf/sat7.sol delete mode 100644 hCaD_V2/test/cnf/sat8.sol delete mode 100644 hCaD_V2/test/cnf/sat9.sol delete mode 100644 hCaD_V2/test/cnf/sqrt10201.sol delete mode 100644 hCaD_V2/test/cnf/sqrt1042441.sol delete mode 100644 hCaD_V2/test/cnf/sqrt10609.sol delete mode 100644 hCaD_V2/test/cnf/sqrt11449.sol delete mode 100644 hCaD_V2/test/cnf/sqrt11881.sol delete mode 100644 hCaD_V2/test/cnf/sqrt12769.sol delete mode 100644 hCaD_V2/test/cnf/sqrt16129.sol delete mode 100644 hCaD_V2/test/cnf/sqrt259081.sol delete mode 100644 hCaD_V2/test/cnf/sqrt2809.sol delete mode 100644 hCaD_V2/test/cnf/sqrt3481.sol delete mode 100644 hCaD_V2/test/cnf/sqrt3721.sol delete mode 100644 hCaD_V2/test/cnf/sqrt4489.sol delete mode 100644 hCaD_V2/test/cnf/sqrt5041.sol delete mode 100644 hCaD_V2/test/cnf/sqrt5329.sol delete mode 100644 hCaD_V2/test/cnf/sqrt6241.sol delete mode 100644 hCaD_V2/test/cnf/sqrt63001.sol delete mode 100644 hCaD_V2/test/cnf/sqrt6889.sol delete mode 100644 hCaD_V2/test/cnf/sqrt7921.sol delete mode 100644 hCaD_V2/test/cnf/sqrt9409.sol delete mode 100644 hCaD_V2/test/cnf/unit0.sol delete mode 100644 hCaD_V2/test/cnf/unit1.sol delete mode 100644 hCaD_V2/test/cnf/unit2.sol delete mode 100644 hCaD_V2/test/cnf/unit3.sol delete mode 100644 hCaD_V2/test/icnf/empty.icnf delete mode 100644 hCaD_V2/test/icnf/false.icnf delete mode 100644 hCaD_V2/test/icnf/makefile delete mode 100644 hCaD_V2/test/icnf/run.sh delete mode 100644 hCaD_V2/test/icnf/two1.icnf delete mode 100644 hCaD_V2/test/icnf/two2.icnf delete mode 100644 hCaD_V2/test/icnf/unit1.icnf delete mode 100644 hCaD_V2/test/icnf/unit2.icnf delete mode 100644 hCaD_V2/test/makefile delete mode 100644 hCaD_V2/test/mbt/README.md delete mode 100644 hCaD_V2/test/mbt/makefile delete mode 100644 hCaD_V2/test/mbt/run.sh delete mode 100644 hCaD_V2/test/trace/README.md delete mode 100644 hCaD_V2/test/trace/makefile delete mode 100644 hCaD_V2/test/trace/reg0000.trace delete mode 100644 hCaD_V2/test/trace/reg0001.trace delete mode 100644 hCaD_V2/test/trace/reg0002.trace delete mode 100644 hCaD_V2/test/trace/reg0003.trace delete mode 100644 hCaD_V2/test/trace/reg0004.trace delete mode 100644 hCaD_V2/test/trace/reg0005.trace delete mode 100644 hCaD_V2/test/trace/reg0006.trace delete mode 100644 hCaD_V2/test/trace/reg0007.trace delete mode 100644 hCaD_V2/test/trace/reg0008.trace delete mode 100644 hCaD_V2/test/trace/reg0009.trace delete mode 100644 hCaD_V2/test/trace/reg0010.trace delete mode 100644 hCaD_V2/test/trace/reg0011.trace delete mode 100644 hCaD_V2/test/trace/reg0012.trace delete mode 100644 hCaD_V2/test/trace/reg0013.trace delete mode 100644 hCaD_V2/test/trace/reg0014.trace delete mode 100644 hCaD_V2/test/trace/reg0015.trace delete mode 100644 hCaD_V2/test/trace/reg0016.trace delete mode 100644 hCaD_V2/test/trace/reg0017.trace delete mode 100644 hCaD_V2/test/trace/reg0018.trace delete mode 100644 hCaD_V2/test/trace/reg0019.trace delete mode 100644 hCaD_V2/test/trace/reg0020.trace delete mode 100644 hCaD_V2/test/trace/reg0021.trace delete mode 100644 hCaD_V2/test/trace/reg0022.trace delete mode 100644 hCaD_V2/test/trace/reg0023.trace delete mode 100644 hCaD_V2/test/trace/reg0024.trace delete mode 100644 hCaD_V2/test/trace/reg0025.trace delete mode 100644 hCaD_V2/test/trace/reg0026.trace delete mode 100644 hCaD_V2/test/trace/reg0027.trace delete mode 100644 hCaD_V2/test/trace/reg0028.trace delete mode 100644 hCaD_V2/test/trace/reg0029.trace delete mode 100644 hCaD_V2/test/trace/reg0030.trace delete mode 100644 hCaD_V2/test/trace/reg0031.trace delete mode 100644 hCaD_V2/test/trace/reg0032.trace delete mode 100644 hCaD_V2/test/trace/reg0033.trace delete mode 100644 hCaD_V2/test/trace/reg0034.trace delete mode 100644 hCaD_V2/test/trace/reg0035.trace delete mode 100644 hCaD_V2/test/trace/reg0036.trace delete mode 100644 hCaD_V2/test/trace/reg0037.trace delete mode 100644 hCaD_V2/test/trace/reg0038.trace delete mode 100644 hCaD_V2/test/trace/reg0039.trace delete mode 100644 hCaD_V2/test/trace/reg0040.trace delete mode 100644 hCaD_V2/test/trace/reg0041.trace delete mode 100644 hCaD_V2/test/trace/reg0042.trace delete mode 100644 hCaD_V2/test/trace/reg0043.trace delete mode 100644 hCaD_V2/test/trace/reg0044.trace delete mode 100644 hCaD_V2/test/trace/reg0045.trace delete mode 100644 hCaD_V2/test/trace/reg0046.trace delete mode 100644 hCaD_V2/test/trace/reg0047.trace delete mode 100644 hCaD_V2/test/trace/reg0048.trace delete mode 100644 hCaD_V2/test/trace/reg0049.trace delete mode 100644 hCaD_V2/test/trace/reg0050.trace delete mode 100644 hCaD_V2/test/trace/reg0051.trace delete mode 100644 hCaD_V2/test/trace/reg0052.trace delete mode 100644 hCaD_V2/test/trace/reg0053.trace delete mode 100644 hCaD_V2/test/trace/reg0054.trace delete mode 100644 hCaD_V2/test/trace/reg0055.trace delete mode 100644 hCaD_V2/test/trace/reg0056.trace delete mode 100644 hCaD_V2/test/trace/run.sh delete mode 100644 hCaD_V2/test/usage/README.md delete mode 100644 hCaD_V2/test/usage/makefile delete mode 100644 hCaD_V2/test/usage/missing-clause.cnf delete mode 100644 hCaD_V2/test/usage/relaxed-header.cnf delete mode 100644 hCaD_V2/test/usage/run.sh delete mode 100644 hCaD_V2/test/usage/variable-too-large.cnf delete mode 100644 result.smt delete mode 100644 result.txt delete mode 100644 smt.result delete mode 100644 sweep.cpp delete mode 100644 sweep.hpp delete mode 100644 test.smt delete mode 100644 vec.hpp diff --git a/.gitignore b/.gitignore index b9ee5dc..a8b4dfc 100644 --- a/.gitignore +++ b/.gitignore @@ -33,4 +33,5 @@ acec amulet2 -build \ No newline at end of file +build +.vscode \ No newline at end of file diff --git a/.vscode/settings.json b/.vscode/settings.json deleted file mode 100644 index 48cb31a..0000000 --- a/.vscode/settings.json +++ /dev/null @@ -1,8 +0,0 @@ -{ - "files.associations": { - "*.ejs": "html", - "iostream": "cpp", - "*.tcc": "cpp", - "new": "cpp" - } -} \ No newline at end of file diff --git a/acec.cpp b/acec.cpp index f1248a8..6753172 100644 --- a/acec.cpp +++ b/acec.cpp @@ -1,46 +1,8 @@ #include -#include "vec.hpp" -#include "circuit.hpp" -#include "sweep.hpp" - -//#include "libopenf4.h" -#include "src/cadical.hpp" #include "polynomial.h" -extern "C" { - #include "aiger.h" -} - -Sweep *S; - -Sweep* sweep_init(int argv, char* args[]) { - Sweep *S = new Sweep(); - S->aig = aiger_init(); - S->solver = new CaDiCaL::Solver; - S->det_v_sz = 0; - S->file = fopen(args[1], "r"); - // S->rounds = atoi(args[2]); - // if (argv > 3) { - // S->det_v = new int[argv -3]; - // for (int i = 3; i < argv; i++) - // S->det_v[S->det_v_sz++] = atoi(args[i]); - // } - return S; -} - -Var* pvar(int id) { - static std::map mp; - if(mp.count(id)) return mp[id]; - - std::string name = "A" + std::to_string(abs(id)); - if(id < 0) name = "N" + name; - - Var* var = new Var(name.c_str(), id > 0 ? S->topo_index[id] : (100000 + id) ); - - return mp[id] = var; -} bool subsitute(Polynomial* &a, Polynomial* b) { @@ -87,112 +49,112 @@ bool subsitute(Polynomial* &a, Polynomial* b) { return result->is_constant_zero_poly(); } -void getPolyOfGate(Sweep* s, int gateid, Polynomial* &resultA, Polynomial* &resultB) { - circuit *c = &(s->C[abs(gateid)]); - gateid = abs(gateid) * (c->neg ? -1 : 1); - if(c->type == And) { - add_to_vstack(pvar(gateid)); - push_mstack(new Monomial(minus_one, build_term_from_stack())); - for(int i=0; isz; i++) { - add_to_vstack(pvar(c->to[i])); - } - push_mstack(new Monomial(one, build_term_from_stack())); - resultA = build_poly(); - } else if(c->type == Xor) { - add_to_vstack(pvar(gateid)); - push_mstack(new Monomial(minus_one, build_term_from_stack())); - add_to_vstack(pvar(c->to[0])); - add_to_vstack(pvar(c->to[1])); - push_mstack(new Monomial(minus_two, build_term_from_stack())); - add_to_vstack(pvar(c->to[0])); - push_mstack(new Monomial(one, build_term_from_stack())); - add_to_vstack(pvar(c->to[1])); - push_mstack(new Monomial(one, build_term_from_stack())); - resultA = build_poly(); - } else if(c->type == HA) { - add_to_vstack(pvar(gateid)); - push_mstack(new Monomial(minus_one, build_term_from_stack())); - add_to_vstack(pvar(c->to[0])); - add_to_vstack(pvar(c->to[1])); - push_mstack(new Monomial(minus_two, build_term_from_stack())); - add_to_vstack(pvar(c->to[0])); - push_mstack(new Monomial(one, build_term_from_stack())); - add_to_vstack(pvar(c->to[1])); - push_mstack(new Monomial(one, build_term_from_stack())); - resultA = build_poly(); +// void getPolyOfGate(Sweep* s, int gateid, Polynomial* &resultA, Polynomial* &resultB) { +// circuit *c = &(s->C[abs(gateid)]); +// gateid = abs(gateid) * (c->neg ? -1 : 1); +// if(c->type == And) { +// add_to_vstack(pvar(gateid)); +// push_mstack(new Monomial(minus_one, build_term_from_stack())); +// for(int i=0; isz; i++) { +// add_to_vstack(pvar(c->to[i])); +// } +// push_mstack(new Monomial(one, build_term_from_stack())); +// resultA = build_poly(); +// } else if(c->type == Xor) { +// add_to_vstack(pvar(gateid)); +// push_mstack(new Monomial(minus_one, build_term_from_stack())); +// add_to_vstack(pvar(c->to[0])); +// add_to_vstack(pvar(c->to[1])); +// push_mstack(new Monomial(minus_two, build_term_from_stack())); +// add_to_vstack(pvar(c->to[0])); +// push_mstack(new Monomial(one, build_term_from_stack())); +// add_to_vstack(pvar(c->to[1])); +// push_mstack(new Monomial(one, build_term_from_stack())); +// resultA = build_poly(); +// } else if(c->type == HA) { +// add_to_vstack(pvar(gateid)); +// push_mstack(new Monomial(minus_one, build_term_from_stack())); +// add_to_vstack(pvar(c->to[0])); +// add_to_vstack(pvar(c->to[1])); +// push_mstack(new Monomial(minus_two, build_term_from_stack())); +// add_to_vstack(pvar(c->to[0])); +// push_mstack(new Monomial(one, build_term_from_stack())); +// add_to_vstack(pvar(c->to[1])); +// push_mstack(new Monomial(one, build_term_from_stack())); +// resultA = build_poly(); - add_to_vstack(pvar(c->carrier)); - push_mstack(new Monomial(minus_one, build_term_from_stack())); - for(int i=0; isz; i++) { - add_to_vstack(pvar(c->to[i])); - } - push_mstack(new Monomial(one, build_term_from_stack())); - resultB = build_poly(); - } else if(c->type == FA) { - add_to_vstack(pvar(gateid)); - push_mstack(new Monomial(minus_one, build_term_from_stack())); - add_to_vstack(pvar(c->to[0])); - push_mstack(new Monomial(one, build_term_from_stack())); - add_to_vstack(pvar(c->to[1])); - push_mstack(new Monomial(one, build_term_from_stack())); - add_to_vstack(pvar(c->to[2])); - push_mstack(new Monomial(one, build_term_from_stack())); +// add_to_vstack(pvar(c->carrier)); +// push_mstack(new Monomial(minus_one, build_term_from_stack())); +// for(int i=0; isz; i++) { +// add_to_vstack(pvar(c->to[i])); +// } +// push_mstack(new Monomial(one, build_term_from_stack())); +// resultB = build_poly(); +// } else if(c->type == FA) { +// add_to_vstack(pvar(gateid)); +// push_mstack(new Monomial(minus_one, build_term_from_stack())); +// add_to_vstack(pvar(c->to[0])); +// push_mstack(new Monomial(one, build_term_from_stack())); +// add_to_vstack(pvar(c->to[1])); +// push_mstack(new Monomial(one, build_term_from_stack())); +// add_to_vstack(pvar(c->to[2])); +// push_mstack(new Monomial(one, build_term_from_stack())); - add_to_vstack(pvar(c->to[0])); - add_to_vstack(pvar(c->to[1])); - push_mstack(new Monomial(minus_two, build_term_from_stack())); +// add_to_vstack(pvar(c->to[0])); +// add_to_vstack(pvar(c->to[1])); +// push_mstack(new Monomial(minus_two, build_term_from_stack())); - add_to_vstack(pvar(c->to[1])); - add_to_vstack(pvar(c->to[2])); - push_mstack(new Monomial(minus_two, build_term_from_stack())); +// add_to_vstack(pvar(c->to[1])); +// add_to_vstack(pvar(c->to[2])); +// push_mstack(new Monomial(minus_two, build_term_from_stack())); - add_to_vstack(pvar(c->to[0])); - add_to_vstack(pvar(c->to[2])); - push_mstack(new Monomial(minus_two, build_term_from_stack())); +// add_to_vstack(pvar(c->to[0])); +// add_to_vstack(pvar(c->to[2])); +// push_mstack(new Monomial(minus_two, build_term_from_stack())); - add_to_vstack(pvar(c->to[0])); - add_to_vstack(pvar(c->to[1])); - add_to_vstack(pvar(c->to[2])); - push_mstack(new Monomial(four, build_term_from_stack())); +// add_to_vstack(pvar(c->to[0])); +// add_to_vstack(pvar(c->to[1])); +// add_to_vstack(pvar(c->to[2])); +// push_mstack(new Monomial(four, build_term_from_stack())); - resultA = build_poly(); +// resultA = build_poly(); - add_to_vstack(pvar(c->carrier)); - push_mstack(new Monomial(minus_one, build_term_from_stack())); - add_to_vstack(pvar(c->to[0])); - add_to_vstack(pvar(c->to[1])); - push_mstack(new Monomial(one, build_term_from_stack())); - add_to_vstack(pvar(c->to[0])); - add_to_vstack(pvar(c->to[2])); - push_mstack(new Monomial(one, build_term_from_stack())); - add_to_vstack(pvar(c->to[1])); - add_to_vstack(pvar(c->to[2])); - push_mstack(new Monomial(one, build_term_from_stack())); - add_to_vstack(pvar(c->to[0])); - add_to_vstack(pvar(c->to[1])); - add_to_vstack(pvar(c->to[2])); - push_mstack(new Monomial(minus_two, build_term_from_stack())); +// add_to_vstack(pvar(c->carrier)); +// push_mstack(new Monomial(minus_one, build_term_from_stack())); +// add_to_vstack(pvar(c->to[0])); +// add_to_vstack(pvar(c->to[1])); +// push_mstack(new Monomial(one, build_term_from_stack())); +// add_to_vstack(pvar(c->to[0])); +// add_to_vstack(pvar(c->to[2])); +// push_mstack(new Monomial(one, build_term_from_stack())); +// add_to_vstack(pvar(c->to[1])); +// add_to_vstack(pvar(c->to[2])); +// push_mstack(new Monomial(one, build_term_from_stack())); +// add_to_vstack(pvar(c->to[0])); +// add_to_vstack(pvar(c->to[1])); +// add_to_vstack(pvar(c->to[2])); +// push_mstack(new Monomial(minus_two, build_term_from_stack())); - resultB = build_poly(); - } else if(c->type == Majority) { - add_to_vstack(pvar(gateid)); - push_mstack(new Monomial(minus_one, build_term_from_stack())); - add_to_vstack(pvar(c->to[0])); - add_to_vstack(pvar(c->to[1])); - push_mstack(new Monomial(one, build_term_from_stack())); - add_to_vstack(pvar(c->to[0])); - add_to_vstack(pvar(c->to[2])); - push_mstack(new Monomial(one, build_term_from_stack())); - add_to_vstack(pvar(c->to[1])); - add_to_vstack(pvar(c->to[2])); - push_mstack(new Monomial(one, build_term_from_stack())); - add_to_vstack(pvar(c->to[0])); - add_to_vstack(pvar(c->to[1])); - add_to_vstack(pvar(c->to[2])); - push_mstack(new Monomial(minus_two, build_term_from_stack())); - resultA = build_poly(); - } -} +// resultB = build_poly(); +// } else if(c->type == Majority) { +// add_to_vstack(pvar(gateid)); +// push_mstack(new Monomial(minus_one, build_term_from_stack())); +// add_to_vstack(pvar(c->to[0])); +// add_to_vstack(pvar(c->to[1])); +// push_mstack(new Monomial(one, build_term_from_stack())); +// add_to_vstack(pvar(c->to[0])); +// add_to_vstack(pvar(c->to[2])); +// push_mstack(new Monomial(one, build_term_from_stack())); +// add_to_vstack(pvar(c->to[1])); +// add_to_vstack(pvar(c->to[2])); +// push_mstack(new Monomial(one, build_term_from_stack())); +// add_to_vstack(pvar(c->to[0])); +// add_to_vstack(pvar(c->to[1])); +// add_to_vstack(pvar(c->to[2])); +// push_mstack(new Monomial(minus_two, build_term_from_stack())); +// resultA = build_poly(); +// } +// } bool poly_cmp(Polynomial *a, Polynomial *b) { return a->get_lt()->get_var()->get_level() > b->get_lt()->get_var()->get_level(); @@ -203,112 +165,109 @@ int main(int argv, char* args[]) { init_mpz(19260817); - S = sweep_init(argv, args); - S->solve(); + // std::map nas; + // for(int i=1; i<=S->maxvar; i++) { + // add_to_vstack(pvar(i)); + // push_mstack(new Monomial(one, build_term_from_stack())); + // add_to_vstack(pvar(-i)); + // push_mstack(new Monomial(one, build_term_from_stack())); + // push_mstack(new Monomial(minus_one, build_term_from_stack())); + // Polynomial *poly = build_poly(); + // nas[pvar(-i)->get_name()] = poly; + // nas[pvar(i)->get_name()] = poly; + // } - std::map nas; - for(int i=1; i<=S->maxvar; i++) { - add_to_vstack(pvar(i)); - push_mstack(new Monomial(one, build_term_from_stack())); - add_to_vstack(pvar(-i)); - push_mstack(new Monomial(one, build_term_from_stack())); - push_mstack(new Monomial(minus_one, build_term_from_stack())); - Polynomial *poly = build_poly(); - nas[pvar(-i)->get_name()] = poly; - nas[pvar(i)->get_name()] = poly; - } + // std::vector polys; - std::vector polys; + // std::set reserved_vars; + // std::vector subsitute_vars; + // for (int i = 1; i <= S->maxvar; i++) { + // circuit *c = &(S->C[i]); + // if (!c->sz || S->del[i] == 2) continue; + // if(c->type == Xor) { + // reserved_vars.insert(i); + // // for(int j=0; jsz; j++) + // // reserved_vars.insert(abs(c->to[j])); + // } + // } + // for (int i = 1; i <= S->maxvar; i++) { + // circuit *c = &(S->C[i]); + // if (!c->sz || S->del[i] == 2) continue; + // if(!reserved_vars.count(i)) { + // Polynomial *p, *q; + // getPolyOfGate(S, i, p, q); + // while(p->get_lt()->get_var_name()[0] == 'N') { + // Polynomial *to_div = nas[p->get_lt()->get_var_name()]; + // subsitute(p, to_div); + // } + // subsitute_vars.push_back(p); + // } + // } - std::set reserved_vars; - std::vector subsitute_vars; - for (int i = 1; i <= S->maxvar; i++) { - circuit *c = &(S->C[i]); - if (!c->sz || S->del[i] == 2) continue; - if(c->type == Xor) { - reserved_vars.insert(i); - // for(int j=0; jsz; j++) - // reserved_vars.insert(abs(c->to[j])); - } - } - for (int i = 1; i <= S->maxvar; i++) { - circuit *c = &(S->C[i]); - if (!c->sz || S->del[i] == 2) continue; - if(!reserved_vars.count(i)) { - Polynomial *p, *q; - getPolyOfGate(S, i, p, q); - while(p->get_lt()->get_var_name()[0] == 'N') { - Polynomial *to_div = nas[p->get_lt()->get_var_name()]; - subsitute(p, to_div); - } - subsitute_vars.push_back(p); - } - } + // printf("reserved: %d ; subsitute: %d\n", reserved_vars.size(), subsitute_vars.size()); - printf("reserved: %d ; subsitute: %d\n", reserved_vars.size(), subsitute_vars.size()); + // for (int i = 1; i <= S->maxvar; i++) { + // circuit *c = &(S->C[i]); + // if (!c->sz || S->del[i] == 2) continue; + // } - for (int i = 1; i <= S->maxvar; i++) { - circuit *c = &(S->C[i]); - if (!c->sz || S->del[i] == 2) continue; - } + // for (int i = 1; i <= S->maxvar; i++) { + // circuit *c = &(S->C[i]); + // if (!c->sz || S->del[i] == 2) continue; - for (int i = 1; i <= S->maxvar; i++) { - circuit *c = &(S->C[i]); - if (!c->sz || S->del[i] == 2) continue; + // if(!reserved_vars.count(i)) continue; - if(!reserved_vars.count(i)) continue; + // //if(c->sz == 2 && abs(c->to[0]) <= 14 && abs(c->to[1]) <= 14) continue; - //if(c->sz == 2 && abs(c->to[0]) <= 14 && abs(c->to[1]) <= 14) continue; + // Polynomial *resultA, *resultB = nullptr; + // getPolyOfGate(S, i, resultA, resultB); - Polynomial *resultA, *resultB = nullptr; - getPolyOfGate(S, i, resultA, resultB); + // printf(" original:\t"); resultA->print(stdout); - printf(" original:\t"); resultA->print(stdout); + // while(resultA->get_lt()->get_var_name()[0] == 'N') { + // Polynomial *to_div = nas[resultA->get_lt()->get_var_name()]; + // subsitute(resultA, to_div); + // } - while(resultA->get_lt()->get_var_name()[0] == 'N') { - Polynomial *to_div = nas[resultA->get_lt()->get_var_name()]; - subsitute(resultA, to_div); - } + // printf(" pos-var:\t"); resultA->print(stdout); - printf(" pos-var:\t"); resultA->print(stdout); + // for(auto subs : subsitute_vars) { + // //printf("delete: "); subs->print(stdout); + // subsitute(resultA, subs); + // } - for(auto subs : subsitute_vars) { - //printf("delete: "); subs->print(stdout); - subsitute(resultA, subs); - } + // printf(" xor-relative:\t"); resultA->print(stdout); - printf(" xor-relative:\t"); resultA->print(stdout); - - polys.push_back(resultA); + // polys.push_back(resultA); - if (c->type == HA || c->type == FA) { - printf("( %d %d )", i * (S->C[i].neg ? -1 : 1), c->carrier); - } - else { - printf("%d", i * (S->C[i].neg ? -1 : 1)); - } + // if (c->type == HA || c->type == FA) { + // printf("( %d %d )", i * (S->C[i].neg ? -1 : 1), c->carrier); + // } + // else { + // printf("%d", i * (S->C[i].neg ? -1 : 1)); + // } - printf(" = %s ( ", gate_type[c->type].c_str()); + // printf(" = %s ( ", gate_type[c->type].c_str()); - for (int j = 0; j < c->sz; j++) { - printf("%d ", c->to[j]); - } - puts(")"); - } + // for (int j = 0; j < c->sz; j++) { + // printf("%d ", c->to[j]); + // } + // puts(")"); + // } - add_to_vstack(pvar(32)); - push_mstack(new Monomial(one, build_term_from_stack())); + // add_to_vstack(pvar(32)); + // push_mstack(new Monomial(one, build_term_from_stack())); - Polynomial *result = build_poly(); + // Polynomial *result = build_poly(); - std::sort(polys.begin(), polys.end(), poly_cmp); + // std::sort(polys.begin(), polys.end(), poly_cmp); - for(auto p : polys) { - printf("now: "); result->print(stdout); - printf("div: "); p->print(stdout); - subsitute(result, p); - } + // for(auto p : polys) { + // printf("now: "); result->print(stdout); + // printf("div: "); p->print(stdout); + // subsitute(result, p); + // } return 0; } diff --git a/acec.log b/acec.log deleted file mode 100644 index e69de29..0000000 diff --git a/aiger.c b/aiger.c deleted file mode 100644 index e6e5bb6..0000000 --- a/aiger.c +++ /dev/null @@ -1,2775 +0,0 @@ -/*************************************************************************** -Copyright (c) 2011, Siert Wieringa, Aalto University, Finland. -Copyright (c) 2006-2019, Armin Biere, Johannes Kepler University. - -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. -***************************************************************************/ -#include "aiger.h" - -#include -#include -#include -#include -#include - - - -/*------------------------------------------------------------------------*/ - -// TODO move this to seperate file and sync it with git hash - -const char * -aiger_id (void) -{ - return "invalid id"; -} - -/*------------------------------------------------------------------------*/ - -const char * -aiger_version (void) -{ - return AIGER_VERSION; -} - -/*------------------------------------------------------------------------*/ - -#define GZIP "gzip -c > %s 2>/dev/null" -#define GUNZIP "gunzip -c %s 2>/dev/null" - -#define NEWN(p,n) \ - do { \ - size_t bytes = (n) * sizeof (*(p)); \ - (p) = private->malloc_callback (private->memory_mgr, bytes); \ - memset ((p), 0, bytes); \ - } while (0) - -#define REALLOCN(p,m,n) \ - do { \ - size_t mbytes = (m) * sizeof (*(p)); \ - size_t nbytes = (n) * sizeof (*(p)); \ - size_t minbytes = (mbytes < nbytes) ? mbytes : nbytes; \ - void * res = private->malloc_callback (private->memory_mgr, nbytes); \ - memcpy (res, (p), minbytes); \ - if (nbytes > mbytes) \ - memset (((char*)res) + mbytes, 0, nbytes - mbytes); \ - private->free_callback (private->memory_mgr, (p), mbytes); \ - (p) = res; \ - } while (0) - -#define FIT(p,m,n) \ - do { \ - size_t old_size = (m); \ - size_t new_size = (n); \ - if (old_size < new_size) \ - { \ - REALLOCN (p,old_size,new_size); \ - (m) = new_size; \ - } \ - } while (0) - -#define ENLARGE(p,s) \ - do { \ - size_t old_size = (s); \ - size_t new_size = old_size ? 2 * old_size : 1; \ - REALLOCN (p,old_size,new_size); \ - (s) = new_size; \ - } while (0) - -#define PUSH(p,t,s,l) \ - do { \ - if ((t) == (s)) \ - ENLARGE (p, s); \ - (p)[(t)++] = (l); \ - } while (0) - -#define DELETEN(p,n) \ - do { \ - size_t bytes = (n) * sizeof (*(p)); \ - private->free_callback (private->memory_mgr, (p), bytes); \ - (p) = 0; \ - } while (0) - -#define CLR(p) do { memset (&(p), 0, sizeof (p)); } while (0) - -#define NEW(p) NEWN (p,1) -#define DELETE(p) DELETEN (p,1) - -#define IMPORT_private_FROM(p) \ - aiger_private * private = (aiger_private*) (p) - -#define EXPORT_public_FROM(p) \ - aiger * public = &(p)->public - -typedef struct aiger_private aiger_private; -typedef struct aiger_buffer aiger_buffer; -typedef struct aiger_reader aiger_reader; -typedef struct aiger_type aiger_type; - -struct aiger_type -{ - unsigned input:1; - unsigned latch:1; - unsigned and:1; - - unsigned mark:1; - unsigned onstack:1; - - /* Index int to 'public->{inputs,latches,ands}'. - */ - unsigned idx; -}; - -struct aiger_private -{ - aiger public; - - aiger_type *types; /* [0..maxvar] */ - unsigned size_types; - - unsigned char * coi; - unsigned size_coi; - - unsigned size_inputs; - unsigned size_latches; - unsigned size_outputs; - unsigned size_ands; - unsigned size_bad; - unsigned size_constraints; - unsigned size_justice; - unsigned size_fairness; - - unsigned num_comments; - unsigned size_comments; - - void *memory_mgr; - aiger_malloc malloc_callback; - aiger_free free_callback; - - char *error; -}; - -struct aiger_buffer -{ - char *start; - char *cursor; - char *end; -}; - -struct aiger_reader -{ - void *state; - aiger_get get; - - int ch; - - unsigned lineno; - unsigned charno; - - unsigned lineno_at_last_token_start; - - int done_with_reading_header; - int looks_like_aag; - - aiger_mode mode; - unsigned maxvar; - unsigned inputs; - unsigned latches; - unsigned outputs; - unsigned ands; - unsigned bad; - unsigned constraints; - unsigned justice; - unsigned fairness; - - char *buffer; - unsigned top_buffer; - unsigned size_buffer; -}; - -aiger * -aiger_init_mem (void *memory_mgr, - aiger_malloc external_malloc, aiger_free external_free) -{ - aiger_private *private; - aiger *public; - - assert (external_malloc); - assert (external_free); - private = external_malloc (memory_mgr, sizeof (*private)); - CLR (*private); - private->memory_mgr = memory_mgr; - private->malloc_callback = external_malloc; - private->free_callback = external_free; - public = &private->public; - PUSH (public->comments, private->num_comments, private->size_comments, 0); - - return public; -} - -static void * -aiger_default_malloc (void *state, size_t bytes) -{ - return malloc (bytes); -} - -static void -aiger_default_free (void *state, void *ptr, size_t bytes) -{ - free (ptr); -} - -aiger * -aiger_init (void) -{ - return aiger_init_mem (0, aiger_default_malloc, aiger_default_free); -} - -static void -aiger_delete_str (aiger_private * private, char *str) -{ - if (str) - DELETEN (str, strlen (str) + 1); -} - -static char * -aiger_copy_str (aiger_private * private, const char *str) -{ - char *res; - - if (!str || !str[0]) - return 0; - - NEWN (res, strlen (str) + 1); - strcpy (res, str); - - return res; -} - -static unsigned -aiger_delete_symbols_aux (aiger_private * private, - aiger_symbol * symbols, unsigned size) -{ - unsigned i, res; - - res = 0; - for (i = 0; i < size; i++) - { - aiger_symbol *s = symbols + i; - if (!s->name) - continue; - - aiger_delete_str (private, s->name); - s->name = 0; - res++; - } - - return res; -} - -static void -aiger_delete_symbols (aiger_private * private, - aiger_symbol * symbols, unsigned size) -{ - aiger_delete_symbols_aux (private, symbols, size); - DELETEN (symbols, size); -} - -static unsigned -aiger_delete_comments (aiger * public) -{ - char **start = (char **) public->comments, ** end, ** p; - IMPORT_private_FROM (public); - - end = start + private->num_comments; - for (p = start; p < end; p++) - aiger_delete_str (private, *p); - - private->num_comments = 0; - public->comments[0] = 0; - - return private->num_comments; -} - -void -aiger_reset (aiger * public) -{ - unsigned i; - - IMPORT_private_FROM (public); - - aiger_delete_symbols (private, public->inputs, private->size_inputs); - aiger_delete_symbols (private, public->latches, private->size_latches); - aiger_delete_symbols (private, public->outputs, private->size_outputs); - aiger_delete_symbols (private, public->bad, private->size_bad); - aiger_delete_symbols (private, public->constraints, - private->size_constraints); - for (i = 0; i < public->num_justice; i++) - DELETEN (public->justice[i].lits, public->justice[i].size); - aiger_delete_symbols (private, public->justice, private->size_justice); - aiger_delete_symbols (private, public->fairness, private->size_fairness); - DELETEN (public->ands, private->size_ands); - - aiger_delete_comments (public); - DELETEN (public->comments, private->size_comments); - - DELETEN (private->coi, private->size_coi); - - DELETEN (private->types, private->size_types); - aiger_delete_str (private, private->error); - DELETE (private); -} - -static aiger_type * -aiger_import_literal (aiger_private * private, unsigned lit) -{ - unsigned var = aiger_lit2var (lit); - EXPORT_public_FROM (private); - - if (var > public->maxvar) - public->maxvar = var; - - while (var >= private->size_types) - ENLARGE (private->types, private->size_types); - - return private->types + var; -} - -void -aiger_add_input (aiger * public, unsigned lit, const char *name) -{ - IMPORT_private_FROM (public); - aiger_symbol symbol; - aiger_type *type; - - assert (!aiger_error (public)); - - assert (lit); - assert (!aiger_sign (lit)); - - type = aiger_import_literal (private, lit); - - assert (!type->input); - assert (!type->latch); - assert (!type->and); - - type->input = 1; - type->idx = public->num_inputs; - - CLR (symbol); - symbol.lit = lit; - symbol.name = aiger_copy_str (private, name); - - PUSH (public->inputs, public->num_inputs, private->size_inputs, symbol); -} - -void -aiger_add_latch (aiger * public, - unsigned lit, unsigned next, const char *name) -{ - IMPORT_private_FROM (public); - aiger_symbol symbol; - aiger_type *type; - - assert (!aiger_error (public)); - - assert (lit); - assert (!aiger_sign (lit)); - - type = aiger_import_literal (private, lit); - - assert (!type->input); - assert (!type->latch); - assert (!type->and); - - /* Warning: importing 'next' makes 'type' invalid. - */ - type->latch = 1; - type->idx = public->num_latches; - - aiger_import_literal (private, next); - - CLR (symbol); - symbol.lit = lit; - symbol.next = next; - symbol.name = aiger_copy_str (private, name); - - PUSH (public->latches, public->num_latches, private->size_latches, symbol); -} - -void -aiger_add_reset (aiger * public, unsigned lit, unsigned reset) -{ - IMPORT_private_FROM (public); - aiger_type * type; - assert (reset <= 1 || reset == lit); - assert (!aiger_error (public)); - assert (lit); - assert (!aiger_sign (lit)); - type = aiger_import_literal (private, lit); - assert (type->latch); - assert (type->idx < public->num_latches); - public->latches[type->idx].reset = reset; -} - -void -aiger_add_output (aiger * public, unsigned lit, const char *name) -{ - IMPORT_private_FROM (public); - aiger_symbol symbol; - aiger_import_literal (private, lit); - CLR (symbol); - symbol.lit = lit; - symbol.name = aiger_copy_str (private, name); - PUSH (public->outputs, public->num_outputs, private->size_outputs, symbol); -} - -void -aiger_add_bad (aiger * public, unsigned lit, const char *name) -{ - IMPORT_private_FROM (public); - aiger_symbol symbol; - aiger_import_literal (private, lit); - CLR (symbol); - symbol.lit = lit; - symbol.name = aiger_copy_str (private, name); - PUSH (public->bad, public->num_bad, private->size_bad, symbol); -} - -void -aiger_add_constraint (aiger * public, unsigned lit, const char *name) -{ - IMPORT_private_FROM (public); - aiger_symbol symbol; - aiger_import_literal (private, lit); - CLR (symbol); - symbol.lit = lit; - symbol.name = aiger_copy_str (private, name); - PUSH (public->constraints, - public->num_constraints, private->size_constraints, symbol); -} - -void -aiger_add_justice (aiger * public, - unsigned size, unsigned * lits, - const char * name) -{ - IMPORT_private_FROM (public); - aiger_symbol symbol; - unsigned i, lit; - CLR (symbol); - symbol.size = size; - NEWN (symbol.lits, size); - for (i = 0; i < size; i++) - { - lit = lits[i]; - aiger_import_literal (private, lit); - symbol.lits[i] = lit; - } - symbol.name = aiger_copy_str (private, name); - PUSH (public->justice, - public->num_justice, private->size_justice, symbol); -} - -void -aiger_add_fairness (aiger * public, unsigned lit, const char *name) -{ - IMPORT_private_FROM (public); - aiger_symbol symbol; - aiger_import_literal (private, lit); - CLR (symbol); - symbol.lit = lit; - symbol.name = aiger_copy_str (private, name); - PUSH (public->fairness, - public->num_fairness, private->size_fairness, symbol); -} - -void -aiger_add_and (aiger * public, unsigned lhs, unsigned rhs0, unsigned rhs1) -{ - IMPORT_private_FROM (public); - aiger_type *type; - aiger_and *and; - - assert (!aiger_error (public)); - - assert (lhs > 1); - assert (!aiger_sign (lhs)); - - type = aiger_import_literal (private, lhs); - - assert (!type->input); - assert (!type->latch); - assert (!type->and); - - type->and = 1; - type->idx = public->num_ands; - - aiger_import_literal (private, rhs0); - aiger_import_literal (private, rhs1); - - if (public->num_ands == private->size_ands) - ENLARGE (public->ands, private->size_ands); - - and = public->ands + public->num_ands; - - and->lhs = lhs; - and->rhs0 = rhs0; - and->rhs1 = rhs1; - - public->num_ands++; -} - -void -aiger_add_comment (aiger * public, const char *comment) -{ - IMPORT_private_FROM (public); - char **p; - - assert (!aiger_error (public)); - - assert (!strchr (comment, '\n')); - assert (private->num_comments); - p = public->comments + private->num_comments - 1; - assert (!*p); - *p = aiger_copy_str (private, comment); - PUSH (public->comments, private->num_comments, private->size_comments, 0); -} - -static const char * -aiger_error_s (aiger_private * private, const char *s, const char *a) -{ - unsigned tmp_len, error_len; - char *tmp; - assert (!private->error); - tmp_len = strlen (s) + strlen (a) + 1; - NEWN (tmp, tmp_len); - sprintf (tmp, s, a); - error_len = strlen (tmp) + 1; - NEWN (private->error, error_len); - memcpy (private->error, tmp, error_len); - DELETEN (tmp, tmp_len); - return private->error; -} - -static const char * -aiger_error_u (aiger_private * private, const char *s, unsigned u) -{ - unsigned tmp_len, error_len; - char *tmp; - assert (!private->error); - tmp_len = strlen (s) + sizeof (u) * 4 + 1; - NEWN (tmp, tmp_len); - sprintf (tmp, s, u); - error_len = strlen (tmp) + 1; - NEWN (private->error, error_len); - memcpy (private->error, tmp, error_len); - DELETEN (tmp, tmp_len); - return private->error; -} - -static const char * -aiger_error_uu (aiger_private * private, const char *s, unsigned a, - unsigned b) -{ - unsigned tmp_len, error_len; - char *tmp; - assert (!private->error); - tmp_len = strlen (s) + sizeof (a) * 4 + sizeof (b) * 4 + 1; - NEWN (tmp, tmp_len); - sprintf (tmp, s, a, b); - error_len = strlen (tmp) + 1; - NEWN (private->error, error_len); - memcpy (private->error, tmp, error_len); - DELETEN (tmp, tmp_len); - return private->error; -} - -static const char * -aiger_error_us (aiger_private * private, const char *s, unsigned a, - const char * b) -{ - unsigned tmp_len, error_len; - char *tmp; - assert (!private->error); - tmp_len = strlen (s) + sizeof (a) * 4 + strlen (b) + 1; - NEWN (tmp, tmp_len); - sprintf (tmp, s, a, b); - error_len = strlen (tmp) + 1; - NEWN (private->error, error_len); - memcpy (private->error, tmp, error_len); - DELETEN (tmp, tmp_len); - return private->error; -} - -static const char * -aiger_error_usu (aiger_private * private, - const char *s, unsigned a, const char *t, unsigned b) -{ - unsigned tmp_len, error_len; - char *tmp; - assert (!private->error); - tmp_len = strlen (s) + strlen (t) + sizeof (a) * 4 + sizeof (b) * 4 + 1; - NEWN (tmp, tmp_len); - sprintf (tmp, s, a, t, b); - error_len = strlen (tmp) + 1; - NEWN (private->error, error_len); - memcpy (private->error, tmp, error_len); - DELETEN (tmp, tmp_len); - return private->error; -} - -const char * -aiger_error (aiger * public) -{ - IMPORT_private_FROM (public); - return private->error; -} - -static int -aiger_literal_defined (aiger_private * private, unsigned lit) -{ - unsigned var = aiger_lit2var (lit); -#ifndef NDEBUG - EXPORT_public_FROM (private); -#endif - aiger_type *type; - - assert (var <= public->maxvar); - if (!var) - return 1; - - type = private->types + var; - - return type->and || type->input || type->latch; -} - -static void -aiger_check_next_defined (aiger_private * private) -{ - EXPORT_public_FROM (private); - unsigned i, next, latch; - aiger_symbol *symbol; - - if (private->error) - return; - - for (i = 0; !private->error && i < public->num_latches; i++) - { - symbol = public->latches + i; - latch = symbol->lit; - next = symbol->next; - - assert (!aiger_sign (latch)); - assert (private->types[aiger_lit2var (latch)].latch); - - if (!aiger_literal_defined (private, next)) - aiger_error_uu (private, - "next state function %u of latch %u undefined", - next, latch); - } -} - -static void -aiger_check_right_hand_side_defined (aiger_private * private, aiger_and * and, - unsigned rhs) -{ - if (private->error) - return; - - assert (and); - if (!aiger_literal_defined (private, rhs)) - aiger_error_uu (private, "literal %u in AND %u undefined", rhs, and->lhs); -} - -static void -aiger_check_right_hand_sides_defined (aiger_private * private) -{ - EXPORT_public_FROM (private); - aiger_and *and; - unsigned i; - - if (private->error) - return; - - for (i = 0; !private->error && i < public->num_ands; i++) - { - and = public->ands + i; - aiger_check_right_hand_side_defined (private, and, and->rhs0); - aiger_check_right_hand_side_defined (private, and, and->rhs1); - } -} - -static void -aiger_check_outputs_defined (aiger_private * private) -{ - EXPORT_public_FROM (private); - unsigned i, output; - - if (private->error) - return; - - for (i = 0; !private->error && i < public->num_outputs; i++) - { - output = public->outputs[i].lit; - output = aiger_strip (output); - if (output <= 1) - continue; - - if (!aiger_literal_defined (private, output)) - aiger_error_u (private, "output %u undefined", output); - } -} - -static void -aiger_check_bad_defined (aiger_private * private) -{ - EXPORT_public_FROM (private); - unsigned i, bad; - - if (private->error) - return; - - for (i = 0; !private->error && i < public->num_bad; i++) - { - bad = public->bad[i].lit; - bad = aiger_strip (bad); - if (bad <= 1) - continue; - - if (!aiger_literal_defined (private, bad)) - aiger_error_u (private, "bad %u undefined", bad); - } -} - -static void -aiger_check_constraints_defined (aiger_private * private) -{ - EXPORT_public_FROM (private); - unsigned i, constraint; - - if (private->error) - return; - - for (i = 0; !private->error && i < public->num_constraints; i++) - { - constraint = public->constraints[i].lit; - constraint = aiger_strip (constraint); - if (constraint <= 1) - continue; - - if (!aiger_literal_defined (private, constraint)) - aiger_error_u (private, "constraint %u undefined", constraint); - } -} - -static void -aiger_check_fairness_defined (aiger_private * private) -{ - EXPORT_public_FROM (private); - unsigned i, fairness; - - if (private->error) - return; - - for (i = 0; !private->error && i < public->num_fairness; i++) - { - fairness = public->fairness[i].lit; - fairness = aiger_strip (fairness); - if (fairness <= 1) - continue; - - if (!aiger_literal_defined (private, fairness)) - aiger_error_u (private, "fairness %u undefined", fairness); - } -} - -static void -aiger_check_justice_defined (aiger_private * private) -{ - EXPORT_public_FROM (private); - unsigned i, j, justice; - - if (private->error) - return; - - for (i = 0; !private->error && i < public->num_justice; i++) - { - for (j = 0; !private->error && j < public->justice[i].size; j++) - { - justice = public->justice[i].lits[j]; - justice = aiger_strip (justice); - if (justice <= 1) - continue; - - if (!aiger_literal_defined (private, justice)) - aiger_error_u (private, "justice %u undefined", justice); - } - } -} - -static void -aiger_check_for_cycles (aiger_private * private) -{ - unsigned i, j, *stack, size_stack, top_stack, tmp; - EXPORT_public_FROM (private); - aiger_type *type; - aiger_and *and; - - if (private->error) - return; - - stack = 0; - size_stack = top_stack = 0; - - for (i = 1; !private->error && i <= public->maxvar; i++) - { - type = private->types + i; - - if (!type->and || type->mark) - continue; - - PUSH (stack, top_stack, size_stack, i); - while (top_stack) - { - j = stack[top_stack - 1]; - - if (j) - { - type = private->types + j; - if (type->mark && type->onstack) - { - aiger_error_u (private, - "cyclic definition for and gate %u", j); - break; - } - - if (!type->and || type->mark) - { - top_stack--; - continue; - } - - /* Prefix code. - */ - type->mark = 1; - type->onstack = 1; - PUSH (stack, top_stack, size_stack, 0); - - assert (type->idx < public->num_ands); - and = public->ands + type->idx; - - tmp = aiger_lit2var (and->rhs0); - if (tmp) - PUSH (stack, top_stack, size_stack, tmp); - - tmp = aiger_lit2var (and->rhs1); - if (tmp) - PUSH (stack, top_stack, size_stack, tmp); - } - else - { - /* All descendends traversed. This is the postfix code. - */ - assert (top_stack >= 2); - top_stack -= 2; - j = stack[top_stack]; - assert (j); - type = private->types + j; - assert (type->mark); - assert (type->onstack); - type->onstack = 0; - } - } - } - - DELETEN (stack, size_stack); -} - -const char * -aiger_check (aiger * public) -{ - IMPORT_private_FROM (public); - - assert (!aiger_error (public)); - - aiger_check_next_defined (private); - aiger_check_outputs_defined (private); - aiger_check_bad_defined (private); - aiger_check_constraints_defined (private); - aiger_check_justice_defined (private); - aiger_check_fairness_defined (private); - aiger_check_right_hand_sides_defined (private); - aiger_check_for_cycles (private); - - return private->error; -} - -static int -aiger_default_get (FILE * file) -{ - return getc (file); -} - -static int -aiger_default_put (char ch, FILE * file) -{ - return putc ((unsigned char) ch, file); -} - -static int -aiger_string_put (char ch, aiger_buffer * buffer) -{ - if (buffer->cursor == buffer->end) - return EOF; - *buffer->cursor++ = ch; - return ch; -} - -static int -aiger_put_s (void *state, aiger_put put, const char *str) -{ - const char *p; - char ch; - - for (p = str; (ch = *p); p++) - if (put (ch, state) == EOF) - return EOF; - - return p - str; /* 'fputs' semantics, >= 0 is OK */ -} - -static int -aiger_put_u (void *state, aiger_put put, unsigned u) -{ - char buffer[sizeof (u) * 4]; - sprintf (buffer, "%u", u); - return aiger_put_s (state, put, buffer); -} - -static int -aiger_write_delta (void *state, aiger_put put, unsigned delta) -{ - unsigned char ch; - unsigned tmp = delta; - - while (tmp & ~0x7f) - { - ch = tmp & 0x7f; - ch |= 0x80; - - if (put (ch, state) == EOF) - return 0; - - tmp >>= 7; - } - - ch = tmp; - return put (ch, state) != EOF; -} - -static int -aiger_write_header (aiger * public, - const char *format_string, - int compact_inputs_and_latches, - void *state, aiger_put put) -{ - unsigned i, j; - - if (aiger_put_s (state, put, format_string) == EOF) return 0; - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->maxvar) == EOF) return 0; - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->num_inputs) == EOF) return 0; - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->num_latches) == EOF) return 0; - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->num_outputs) == EOF) return 0; - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->num_ands) == EOF) return 0; - - if (public->num_bad || - public->num_constraints || - public->num_justice || - public->num_fairness) - { - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->num_bad) == EOF) return 0; - } - - if (public->num_constraints || - public->num_justice || - public->num_fairness) - { - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->num_constraints) == EOF) return 0; - } - - if (public->num_justice || - public->num_fairness) - { - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->num_justice) == EOF) return 0; - } - - if (public->num_fairness) - { - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->num_fairness) == EOF) return 0; - } - - if (put ('\n', state) == EOF) return 0; - - if (!compact_inputs_and_latches && public->num_inputs) - { - for (i = 0; i < public->num_inputs; i++) - if (aiger_put_u (state, put, public->inputs[i].lit) == EOF || - put ('\n', state) == EOF) - return 0; - } - - if (public->num_latches) - { - for (i = 0; i < public->num_latches; i++) - { - if (!compact_inputs_and_latches) - { - if (aiger_put_u (state, put, public->latches[i].lit) == EOF) - return 0; - if (put (' ', state) == EOF) return 0; - } - - if (aiger_put_u (state, put, public->latches[i].next) == EOF) - return 0; - - if (public->latches[i].reset) - { - if (put (' ', state) == EOF) return 0; - if (aiger_put_u (state, put, public->latches[i].reset) == EOF) - return 0; - } - if (put ('\n', state) == EOF) return 0; - } - } - - if (public->num_outputs) - { - for (i = 0; i < public->num_outputs; i++) - if (aiger_put_u (state, put, public->outputs[i].lit) == EOF || - put ('\n', state) == EOF) - return 0; - } - - if (public->num_bad) - { - for (i = 0; i < public->num_bad; i++) - if (aiger_put_u (state, put, public->bad[i].lit) == EOF || - put ('\n', state) == EOF) - return 0; - } - - if (public->num_constraints) - { - for (i = 0; i < public->num_constraints; i++) - if (aiger_put_u (state, put, public->constraints[i].lit) == EOF || - put ('\n', state) == EOF) - return 0; - } - - if (public->num_justice) - { - for (i = 0; i < public->num_justice; i++) - { - if (aiger_put_u (state, put, public->justice[i].size) == EOF) - return 0; - if (put ('\n', state) == EOF) return 0; - } - - for (i = 0; i < public->num_justice; i++) - { - for (j = 0; j < public->justice[i].size; j++) - { - if (aiger_put_u (state, put, public->justice[i].lits[j]) == EOF) - return 0; - if (put ('\n', state) == EOF) return 0; - } - } - } - - if (public->num_fairness) - { - for (i = 0; i < public->num_fairness; i++) - if (aiger_put_u (state, put, public->fairness[i].lit) == EOF || - put ('\n', state) == EOF) - return 0; - } - - return 1; -} - -static int -aiger_have_at_least_one_symbol_aux (aiger * public, - aiger_symbol * symbols, unsigned size) -{ - unsigned i; - - for (i = 0; i < size; i++) - if (symbols[i].name) - return 1; - - return 0; -} - -static int -aiger_have_at_least_one_symbol (aiger * public) -{ - if (aiger_have_at_least_one_symbol_aux (public, - public->inputs, public->num_inputs)) - return 1; - - if (aiger_have_at_least_one_symbol_aux (public, - public->outputs, - public->num_outputs)) - return 1; - - if (aiger_have_at_least_one_symbol_aux (public, - public->latches, - public->num_latches)) - return 1; - - if (aiger_have_at_least_one_symbol_aux (public, - public->bad, - public->num_bad)) - return 1; - - if (aiger_have_at_least_one_symbol_aux (public, - public->constraints, - public->num_constraints)) - return 1; - - if (aiger_have_at_least_one_symbol_aux (public, - public->justice, - public->num_justice)) - return 1; - - if (aiger_have_at_least_one_symbol_aux (public, - public->fairness, - public->num_fairness)) - return 1; - - return 0; -} - -static int -aiger_write_symbols_aux (aiger * public, - void *state, aiger_put put, - const char *type, - aiger_symbol * symbols, unsigned size) -{ - unsigned i; - - for (i = 0; i < size; i++) - { - if (!symbols[i].name) - continue; - - assert (symbols[i].name[0]); - - if (aiger_put_s (state, put, type) == EOF || - aiger_put_u (state, put, i) == EOF || - put (' ', state) == EOF || - aiger_put_s (state, put, symbols[i].name) == EOF || - put ('\n', state) == EOF) - return 0; - } - - return 1; -} - -static int -aiger_write_symbols (aiger * public, void *state, aiger_put put) -{ - if (!aiger_write_symbols_aux (public, state, put, - "i", public->inputs, public->num_inputs)) - return 0; - - if (!aiger_write_symbols_aux (public, state, put, - "l", public->latches, public->num_latches)) - return 0; - - if (!aiger_write_symbols_aux (public, state, put, - "o", public->outputs, public->num_outputs)) - return 0; - - if (!aiger_write_symbols_aux (public, state, put, - "b", public->bad, public->num_bad)) - return 0; - - if (!aiger_write_symbols_aux (public, state, put, - "c", public->constraints, - public->num_constraints)) - return 0; - - if (!aiger_write_symbols_aux (public, state, put, - "j", public->justice, public->num_justice)) - return 0; - - if (!aiger_write_symbols_aux (public, state, put, - "f", public->fairness, public->num_fairness)) - return 0; - - return 1; -} - -int -aiger_write_symbols_to_file (aiger * public, FILE * file) -{ - assert (!aiger_error (public)); - return aiger_write_symbols (public, file, (aiger_put) aiger_default_put); -} - -static int -aiger_write_comments (aiger * public, void *state, aiger_put put) -{ - char **p, *str; - - for (p = public->comments; (str = *p); p++) - { - if (aiger_put_s (state, put, str) == EOF) - return 0; - - if (put ('\n', state) == EOF) - return 0; - } - - return 1; -} - -int -aiger_write_comments_to_file (aiger * public, FILE * file) -{ - assert (!aiger_error (public)); - return aiger_write_comments (public, file, (aiger_put) aiger_default_put); -} - -static int -aiger_write_ascii (aiger * public, void *state, aiger_put put) -{ - aiger_and *and; - unsigned i; - - assert (!aiger_check (public)); - - if (!aiger_write_header (public, "aag", 0, state, put)) - return 0; - - for (i = 0; i < public->num_ands; i++) - { - and = public->ands + i; - if (aiger_put_u (state, put, and->lhs) == EOF || - put (' ', state) == EOF || - aiger_put_u (state, put, and->rhs0) == EOF || - put (' ', state) == EOF || - aiger_put_u (state, put, and->rhs1) == EOF || - put ('\n', state) == EOF) - return 0; - } - - return 1; -} - -static unsigned -aiger_max_input_or_latch (aiger * public) -{ - unsigned i, tmp, res; - - res = 0; - - for (i = 0; i < public->num_inputs; i++) - { - tmp = public->inputs[i].lit; - assert (!aiger_sign (tmp)); - if (tmp > res) - res = tmp; - } - - for (i = 0; i < public->num_latches; i++) - { - tmp = public->latches[i].lit; - assert (!aiger_sign (tmp)); - if (tmp > res) - res = tmp; - } - - return res; -} - -int -aiger_is_reencoded (aiger * public) -{ - unsigned i, tmp, max, lhs; - aiger_and *and; - - max = 0; - for (i = 0; i < public->num_inputs; i++) - { - max += 2; - tmp = public->inputs[i].lit; - if (max != tmp) - return 0; - } - - for (i = 0; i < public->num_latches; i++) - { - max += 2; - tmp = public->latches[i].lit; - if (max != tmp) - return 0; - } - - lhs = aiger_max_input_or_latch (public) + 2; - for (i = 0; i < public->num_ands; i++) - { - and = public->ands + i; - - if (and->lhs <= max) - return 0; - - if (and->lhs != lhs) - return 0; - - if (and->lhs < and->rhs0) - return 0; - - if (and->rhs0 < and->rhs1) - return 0; - - lhs += 2; - } - - return 1; -} - -static void -aiger_new_code (unsigned var, unsigned *new, unsigned *code) -{ - unsigned lit = aiger_var2lit (var), res; - assert (!code[lit]); - res = *new; - code[lit] = res; - code[lit + 1] = res + 1; - *new += 2; -} - -static unsigned -aiger_reencode_lit (aiger * public, unsigned lit, - unsigned *new, unsigned *code, - unsigned **stack_ptr, unsigned * size_stack_ptr) -{ - unsigned res, old, top, child0, child1, tmp, var, size_stack, * stack; - IMPORT_private_FROM (public); - aiger_type *type; - aiger_and *and; - - if (lit < 2) - return lit; - - res = code[lit]; - if (res) - return res; - - var = aiger_lit2var (lit); - assert (var <= public->maxvar); - type = private->types + var; - - if (type->and) - { - top = 0; - stack = *stack_ptr; - size_stack = *size_stack_ptr; - PUSH (stack, top, size_stack, var); - - while (top > 0) - { - old = stack[--top]; - if (old) - { - if (code[aiger_var2lit (old)]) - continue; - - assert (old <= public->maxvar); - type = private->types + old; - if (type->onstack) - continue; - - type->onstack = 1; - - PUSH (stack, top, size_stack, old); - PUSH (stack, top, size_stack, 0); - - assert (type->and); - assert (type->idx < public->num_ands); - - and = public->ands + type->idx; - assert (and); - - child0 = aiger_lit2var (and->rhs0); - child1 = aiger_lit2var (and->rhs1); - - if (child0 < child1) - { - tmp = child0; - child0 = child1; - child1 = tmp; - } - - assert (child0 >= child1); /* smaller child first */ - - if (child0) - { - type = private->types + child0; - if (!type->input && !type->latch && !type->onstack) - PUSH (stack, top, size_stack, child0); - } - - if (child1) - { - type = private->types + child1; - if (!type->input && !type->latch && !type->onstack) - PUSH (stack, top, size_stack, child1); - } - } - else - { - assert (top > 0); - old = stack[--top]; - assert (!code[aiger_var2lit (old)]); - type = private->types + old; - assert (type->onstack); - type->onstack = 0; - aiger_new_code (old, new, code); - } - } - *size_stack_ptr = size_stack; - *stack_ptr = stack; - } - else - { - assert (type->input || type->latch); - assert (lit < *new); - - code[lit] = lit; - code[aiger_not (lit)] = aiger_not (lit); - } - - assert (code[lit]); - - return code[lit]; -} - -static int -cmp_lhs (const void *a, const void *b) -{ - const aiger_and *c = a; - const aiger_and *d = b; - return ((int) c->lhs) - (int) d->lhs; -} - -void -aiger_reencode (aiger * public) -{ - unsigned *code, i, j, size_code, old, new, lhs, rhs0, rhs1, tmp; - unsigned *stack, size_stack; - IMPORT_private_FROM (public); - - assert (!aiger_error (public)); - - aiger_symbol *symbol; - aiger_type *type; - aiger_and *and; - - if (aiger_is_reencoded (public)) - return; - - size_code = 2 * (public->maxvar + 1); - if (size_code < 2) - size_code = 2; - - NEWN (code, size_code); - - code[1] = 1; /* not used actually */ - - new = 2; - - for (i = 0; i < public->num_inputs; i++) - { - old = public->inputs[i].lit; - - code[old] = new; - code[old + 1] = new + 1; - - new += 2; - } - - for (i = 0; i < public->num_latches; i++) - { - old = public->latches[i].lit; - - code[old] = new; - code[old + 1] = new + 1; - - new += 2; - } - - stack = 0; - size_stack = 0; - - for (i = 0; i < public->num_latches; i++) - { - old = public->latches[i].next; - public->latches[i].next = - aiger_reencode_lit (public, old, &new, code, &stack, &size_stack); - - old = public->latches[i].reset; - public->latches[i].reset = - aiger_reencode_lit (public, old, &new, code, &stack, &size_stack); - } - - for (i = 0; i < public->num_outputs; i++) - { - old = public->outputs[i].lit; - public->outputs[i].lit = - aiger_reencode_lit (public, old, &new, code, &stack, &size_stack); - } - - for (i = 0; i < public->num_bad; i++) - { - old = public->bad[i].lit; - public->bad[i].lit = - aiger_reencode_lit (public, old, &new, code, &stack, &size_stack); - } - - for (i = 0; i < public->num_constraints; i++) - { - old = public->constraints[i].lit; - public->constraints[i].lit = - aiger_reencode_lit (public, old, &new, code, &stack, &size_stack); - } - - for (i = 0; i < public->num_justice; i++) - { - for (j = 0; j < public->justice[i].size; j++) - { - old = public->justice[i].lits[j]; - public->justice[i].lits[j] = - aiger_reencode_lit (public, old, &new, code, &stack, &size_stack); - } - } - - for (i = 0; i < public->num_fairness; i++) - { - old = public->fairness[i].lit; - public->fairness[i].lit = - aiger_reencode_lit (public, old, &new, code, &stack, &size_stack); - } - - DELETEN (stack, size_stack); - - j = 0; - for (i = 0; i < public->num_ands; i++) - { - and = public->ands + i; - lhs = code[and->lhs]; - if (!lhs) - continue; - - rhs0 = code[and->rhs0]; - rhs1 = code[and->rhs1]; - - and = public->ands + j++; - - if (rhs0 < rhs1) - { - tmp = rhs1; - rhs1 = rhs0; - rhs0 = tmp; - } - - assert (lhs > rhs0); - assert (rhs0 >= rhs1); - - and->lhs = lhs; - and->rhs0 = rhs0; - and->rhs1 = rhs1; - } - public->num_ands = j; - - qsort (public->ands, j, sizeof (*and), cmp_lhs); - - /* Reset types. - */ - for (i = 1; i <= public->maxvar; i++) - { - type = private->types + i; - type->input = 0; - type->latch = 0; - type->and = 0; - type->idx = 0; - } - - assert (new); - assert (public->maxvar >= aiger_lit2var (new - 1)); - public->maxvar = aiger_lit2var (new - 1); - - /* Fix types for ANDs. - */ - for (i = 0; i < public->num_ands; i++) - { - and = public->ands + i; - type = private->types + aiger_lit2var (and->lhs); - type->and = 1; - type->idx = i; - } - - /* Fix types for inputs. - */ - for (i = 0; i < public->num_inputs; i++) - { - symbol = public->inputs + i; - assert (symbol->lit < size_code); - symbol->lit = code[symbol->lit]; - type = private->types + aiger_lit2var (symbol->lit); - type->input = 1; - type->idx = i; - } - - /* Fix types for latches. - */ - for (i = 0; i < public->num_latches; i++) - { - symbol = public->latches + i; - symbol->lit = code[symbol->lit]; - type = private->types + aiger_lit2var (symbol->lit); - type->latch = 1; - type->idx = i; - } - - DELETEN (code, size_code); - -#ifndef NDEBUG - for (i = 0; i <= public->maxvar; i++) - { - type = private->types + i; - assert (!(type->input && type->latch)); - assert (!(type->input && type->and)); - assert (!(type->latch && type->and)); - } -#endif - assert (aiger_is_reencoded (public)); - assert (!aiger_check (public)); -} - -const unsigned char * -aiger_coi (aiger * public) -{ - IMPORT_private_FROM (public); - private->size_coi = public->maxvar + 1; - NEWN (private->coi, private->size_coi); - memset (private->coi, 1, private->size_coi); - return private->coi; -} - -static int -aiger_write_binary (aiger * public, void *state, aiger_put put) -{ - aiger_and *and; - unsigned lhs, i; - - assert (!aiger_check (public)); - - aiger_reencode (public); - - if (!aiger_write_header (public, "aig", 1, state, put)) - return 0; - - lhs = aiger_max_input_or_latch (public) + 2; - - for (i = 0; i < public->num_ands; i++) - { - and = public->ands + i; - - assert (lhs == and->lhs); - assert (lhs > and->rhs0); - assert (and->rhs0 >= and->rhs1); - - if (!aiger_write_delta (state, put, lhs - and->rhs0)) - return 0; - - if (!aiger_write_delta (state, put, and->rhs0 - and->rhs1)) - return 0; - - lhs += 2; - } - - return 1; -} - -unsigned -aiger_strip_symbols_and_comments (aiger * public) -{ - IMPORT_private_FROM (public); - unsigned res; - - assert (!aiger_error (public)); - - res = aiger_delete_comments (public); - - res += aiger_delete_symbols_aux (private, - public->inputs, - private->size_inputs); - res += aiger_delete_symbols_aux (private, - public->latches, - private->size_latches); - res += aiger_delete_symbols_aux (private, - public->outputs, - private->size_outputs); - res += aiger_delete_symbols_aux (private, - public->bad, - private->size_bad); - res += aiger_delete_symbols_aux (private, - public->constraints, - private->size_constraints); - res += aiger_delete_symbols_aux (private, - public->justice, - private->size_justice); - res += aiger_delete_symbols_aux (private, - public->fairness, - private->size_fairness); - return res; -} - -int -aiger_write_generic (aiger * public, - aiger_mode mode, void *state, aiger_put put) -{ - assert (!aiger_error (public)); - - if ((mode & aiger_ascii_mode)) - { - if (!aiger_write_ascii (public, state, put)) - return 0; - } - else - { - if (!aiger_write_binary (public, state, put)) - return 0; - } - - if (!(mode & aiger_stripped_mode)) - { - if (aiger_have_at_least_one_symbol (public)) - { - if (!aiger_write_symbols (public, state, put)) - return 0; - } - - if (public->comments[0]) - { - if (aiger_put_s (state, put, "c\n") == EOF) - return 0; - - if (!aiger_write_comments (public, state, put)) - return 0; - } - } - - return 1; -} - -int -aiger_write_to_file (aiger * public, aiger_mode mode, FILE * file) -{ - assert (!aiger_error (public)); - return aiger_write_generic (public, - mode, file, (aiger_put) aiger_default_put); -} - -int -aiger_write_to_string (aiger * public, aiger_mode mode, char *str, size_t len) -{ - aiger_buffer buffer; - int res; - - assert (!aiger_error (public)); - - buffer.start = str; - buffer.cursor = str; - buffer.end = str + len; - res = aiger_write_generic (public, - mode, &buffer, (aiger_put) aiger_string_put); - - if (!res) - return 0; - - if (aiger_string_put (0, &buffer) == EOF) - return 0; - - return 1; -} - -static int -aiger_has_suffix (const char *str, const char *suffix) -{ - if (strlen (str) < strlen (suffix)) - return 0; - - return !strcmp (str + strlen (str) - strlen (suffix), suffix); -} - -int -aiger_open_and_write_to_file (aiger * public, const char *file_name) -{ - IMPORT_private_FROM (public); - int res, pclose_file; - char *cmd, size_cmd; - aiger_mode mode; - FILE *file; - - assert (!aiger_error (public)); - - assert (file_name); - - if (aiger_has_suffix (file_name, ".gz")) - { - size_cmd = strlen (file_name) + strlen (GZIP); - NEWN (cmd, size_cmd); - sprintf (cmd, GZIP, file_name); - file = popen (cmd, "w"); - DELETEN (cmd, size_cmd); - pclose_file = 1; - } - else - { - file = fopen (file_name, "w"); - pclose_file = 0; - } - - if (!file) - return 0; - - if (aiger_has_suffix (file_name, ".aag") || - aiger_has_suffix (file_name, ".aag.gz")) - mode = aiger_ascii_mode; - else - mode = aiger_binary_mode; - - res = aiger_write_to_file (public, mode, file); - - if (pclose_file) - pclose (file); - else - fclose (file); - - if (!res) - unlink (file_name); - - return res; -} - -static int -aiger_next_ch (aiger_reader * reader) -{ - int res; - - res = reader->get (reader->state); - - if (isspace (reader->ch) && !isspace (res)) - reader->lineno_at_last_token_start = reader->lineno; - - reader->ch = res; - - if (reader->done_with_reading_header && reader->looks_like_aag) - { - if (!isspace (res) && !isdigit (res) && res != EOF) - reader->looks_like_aag = 0; - } - - if (res == '\n') - reader->lineno++; - - if (res != EOF) - reader->charno++; - - return res; -} - -/* Read a number assuming that the current character has already been - * checked to be a digit, e.g. the start of the number to be read. - */ -static unsigned -aiger_read_number (aiger_reader * reader) -{ - unsigned res; - - assert (isdigit (reader->ch)); - res = reader->ch - '0'; - - while (isdigit (aiger_next_ch (reader))) - res = 10 * res + (reader->ch - '0'); - - return res; -} - -/* Expect and read an unsigned number followed by at least one white space - * character. The white space should either the space character or a new - * line as specified by the 'followed_by' parameter. If a number can not be - * found or there is no white space after the number, an apropriate error - * message is returned. - */ -static const char * -aiger_read_literal (aiger_private * private, - aiger_reader * reader, - const char * context, - unsigned *res_ptr, - char expected_followed_by, - char * followed_by_ptr) -{ - unsigned res; - - assert (expected_followed_by == ' ' || - expected_followed_by == '\n' || - !expected_followed_by); - - if (!isdigit (reader->ch)) - return aiger_error_us (private, - "line %u: expected %s", - reader->lineno, context); - - res = aiger_read_number (reader); - - if (expected_followed_by == ' ') - { - if (reader->ch != ' ') - return aiger_error_usu (private, - "line %u: expected space after %s %u", - reader->lineno_at_last_token_start, context, res); -} - if (expected_followed_by == '\n') - { - if (reader->ch != '\n') - return aiger_error_usu (private, - "line %u: expected new line after %s %u", - reader->lineno_at_last_token_start, context, res); -} - if (!expected_followed_by) - { - if (reader->ch != '\n' && reader->ch != ' ') - return aiger_error_usu (private, - "line %u: expected space or new line after %s %u", - reader->lineno_at_last_token_start, context, res); - } - - if (followed_by_ptr) - *followed_by_ptr = reader->ch; - - aiger_next_ch (reader); /* skip white space */ - - *res_ptr = res; - - return 0; -} - -static const char * -aiger_already_defined (aiger * public, aiger_reader * reader, unsigned lit) -{ - IMPORT_private_FROM (public); - aiger_type *type; - unsigned var; - - assert (lit); - assert (!aiger_sign (lit)); - - var = aiger_lit2var (lit); - - if (public->maxvar < var) - return 0; - - type = private->types + var; - - if (type->input) - return aiger_error_uu (private, - "line %u: literal %u already defined as input", - reader->lineno_at_last_token_start, lit); - - if (type->latch) - return aiger_error_uu (private, - "line %u: literal %u already defined as latch", - reader->lineno_at_last_token_start, lit); - - if (type->and) - return aiger_error_uu (private, - "line %u: literal %u already defined as AND", - reader->lineno_at_last_token_start, lit); - return 0; -} - -static const char * -aiger_read_header (aiger * public, aiger_reader * reader) -{ - IMPORT_private_FROM (public); - unsigned i, j, lit, next, reset; - unsigned * sizes, * lits; - const char *error; - char ch; - - aiger_next_ch (reader); - if (reader->ch != 'a') - return aiger_error_u (private, - "line %u: expected 'a' as first character", - reader->lineno); - - if (aiger_next_ch (reader) != 'i' && reader->ch != 'a') - return aiger_error_u (private, - "line %u: expected 'i' or 'a' after 'a'", - reader->lineno); - - if (reader->ch == 'a') - reader->mode = aiger_ascii_mode; - else - reader->mode = aiger_binary_mode; - - if (aiger_next_ch (reader) != 'g') - return aiger_error_u (private, - "line %u: expected 'g' after 'a[ai]'", - reader->lineno); - - if (aiger_next_ch (reader) != ' ') - return aiger_error_u (private, - "line %u: expected ' ' after 'a[ai]g'", - reader->lineno); - - aiger_next_ch (reader); - - if (aiger_read_literal (private, reader, - "maximum variable index", &reader->maxvar, ' ', 0) || - aiger_read_literal (private, reader, - "number of inputs", &reader->inputs, ' ', 0) || - aiger_read_literal (private, reader, - "number latches", &reader->latches, ' ', 0) || - aiger_read_literal (private, reader, - "number of outputs", &reader->outputs, ' ', 0) || - aiger_read_literal (private, reader, - "number of and gates", &reader->ands, 0, &ch) || - (ch == ' ' && - aiger_read_literal (private, reader, - "number of bad state constraints", &reader->bad, 0, &ch)) || - (ch == ' ' && - aiger_read_literal (private, reader, - "number of invariant constraints", - &reader->constraints, 0, &ch)) || - (ch == ' ' && - aiger_read_literal (private, reader, - "number of justice constraints", &reader->justice, 0, &ch)) || - (ch == ' ' && - aiger_read_literal (private, reader, - "number of fairness constraints", &reader->fairness, '\n', 0))) - { - assert (private->error); - return private->error; - } - - if (reader->mode == aiger_binary_mode) - { - i = reader->inputs; - i += reader->latches; - i += reader->ands; - - if (i != reader->maxvar) - return aiger_error_u (private, - "line %u: invalid maximal variable index", - reader->lineno); - } - - public->maxvar = reader->maxvar; - - FIT (private->types, private->size_types, public->maxvar + 1); - FIT (public->inputs, private->size_inputs, reader->inputs); - FIT (public->latches, private->size_latches, reader->latches); - FIT (public->outputs, private->size_outputs, reader->outputs); - FIT (public->ands, private->size_ands, reader->ands); - FIT (public->bad, private->size_bad, reader->bad); - FIT (public->constraints, private->size_constraints, reader->constraints); - FIT (public->justice, private->size_justice, reader->justice); - FIT (public->fairness, private->size_fairness, reader->fairness); - - for (i = 0; i < reader->inputs; i++) - { - if (reader->mode == aiger_ascii_mode) - { - error = aiger_read_literal (private, reader, - "input literal", &lit, '\n', 0); - if (error) - return error; - - if (!lit || aiger_sign (lit) - || aiger_lit2var (lit) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not a valid input", - reader->lineno_at_last_token_start, lit); - - error = aiger_already_defined (public, reader, lit); - if (error) - return error; - } - else - lit = 2 * (i + 1); - - aiger_add_input (public, lit, 0); - } - - for (i = 0; i < reader->latches; i++) - { - if (reader->mode == aiger_ascii_mode) - { - error = aiger_read_literal (private, reader, - "latch literal", &lit, ' ', 0); - if (error) - return error; - - if (!lit || aiger_sign (lit) - || aiger_lit2var (lit) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not a valid latch", - reader->lineno_at_last_token_start, lit); - - error = aiger_already_defined (public, reader, lit); - if (error) - return error; - } - else - lit = 2 * (i + reader->inputs + 1); - - error = aiger_read_literal (private, reader, - "next state literal", &next, 0, &ch); - if (error) - return error; - - if (aiger_lit2var (next) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not a valid literal", - reader->lineno_at_last_token_start, next); - - aiger_add_latch (public, lit, next, 0); - - if (ch == ' ') - { - error = aiger_read_literal (private, reader, - "reset literal", &reset, '\n', 0); - if (error) - return error; - - aiger_add_reset (public, lit, reset); - } - } - - for (i = 0; i < reader->outputs; i++) - { - error = aiger_read_literal (private, reader, - "output literal", &lit, '\n', 0); - if (error) - return error; - - if (aiger_lit2var (lit) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not a valid output", - reader->lineno_at_last_token_start, lit); - - aiger_add_output (public, lit, 0); - } - - for (i = 0; i < reader->bad; i++) - { - error = aiger_read_literal (private, reader, - "bad state constraint literal", &lit, '\n', 0); - if (error) - return error; - - if (aiger_lit2var (lit) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not valid bad", - reader->lineno_at_last_token_start, lit); - - aiger_add_bad (public, lit, 0); - } - - for (i = 0; i < reader->constraints; i++) - { - error = aiger_read_literal (private, reader, - "invariant constraint literal", &lit, '\n', 0); - if (error) - return error; - - if (aiger_lit2var (lit) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not a valid constraint", - reader->lineno_at_last_token_start, lit); - - aiger_add_constraint (public, lit, 0); - } - - if (reader->justice) - { - NEWN (sizes, reader->justice); - error = 0; - for (i = 0; !error && i < reader->justice; i++) - error = aiger_read_literal (private, reader, - "justice constraint size", sizes + i, '\n', 0); - for (i = 0; !error && i < reader->justice; i++) - { - NEWN (lits, sizes[i]); - for (j = 0; !error && j < sizes[i]; j++) - error = aiger_read_literal (private, reader, - "justice constraint literal", lits + j, '\n', 0); - if (!error) - aiger_add_justice (public, sizes[i], lits, 0); - DELETEN (lits, sizes[i]); - } - DELETEN (sizes, reader->justice); - if (error) - return error; - } - - for (i = 0; i < reader->fairness; i++) - { - error = aiger_read_literal (private, reader, - "fairness constraint literal", &lit, '\n', 0); - if (error) - return error; - - if (aiger_lit2var (lit) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not valid fairness", - reader->lineno_at_last_token_start, lit); - - aiger_add_fairness (public, lit, 0); - } - - reader->done_with_reading_header = 1; - reader->looks_like_aag = 1; - - return 0; -} - -static const char * -aiger_read_ascii (aiger * public, aiger_reader * reader) -{ - IMPORT_private_FROM (public); - unsigned i, lhs, rhs0, rhs1; - const char *error; - - for (i = 0; i < reader->ands; i++) - { - error = aiger_read_literal (private, reader, - "and gate left-hand side literal", &lhs, ' ', 0); - if (error) - return error; - - if (!lhs || aiger_sign (lhs) || aiger_lit2var (lhs) > public->maxvar) - return aiger_error_uu (private, - "line %u: " - "literal %u is not a valid LHS of AND", - reader->lineno_at_last_token_start, lhs); - - error = aiger_already_defined (public, reader, lhs); - if (error) - return error; - - error = aiger_read_literal (private, reader, - "and gate first right-hand side literal", - &rhs0, ' ', 0); - if (error) - return error; - - if (aiger_lit2var (rhs0) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not a valid literal", - reader->lineno_at_last_token_start, rhs0); - - error = aiger_read_literal (private, reader, - "and gate first right-hand side literal", - &rhs1, '\n', 0); - if (error) - return error; - - if (aiger_lit2var (rhs1) > public->maxvar) - return aiger_error_uu (private, - "line %u: literal %u is not a valid literal", - reader->lineno_at_last_token_start, rhs1); - - aiger_add_and (public, lhs, rhs0, rhs1); - } - - return 0; -} - -static const char * -aiger_read_delta (aiger_private * private, aiger_reader * reader, - unsigned *res_ptr) -{ - unsigned res, i, charno; - unsigned char ch; - - if (reader->ch == EOF) - UNEXPECTED_EOF: - return aiger_error_u (private, - "character %u: unexpected end of file", - reader->charno); - i = 0; - res = 0; - ch = reader->ch; - - charno = reader->charno; - - while ((ch & 0x80)) - { - assert (sizeof (unsigned) == 4); - - if (i == 5) - INVALID_CODE: - return aiger_error_u (private, "character %u: invalid code", charno); - - res |= (ch & 0x7f) << (7 * i++); - aiger_next_ch (reader); - if (reader->ch == EOF) - goto UNEXPECTED_EOF; - - ch = reader->ch; - } - - if (i == 5 && ch >= 8) - goto INVALID_CODE; - - res |= ch << (7 * i); - *res_ptr = res; - - aiger_next_ch (reader); - - return 0; -} - -static const char * -aiger_read_binary (aiger * public, aiger_reader * reader) -{ - unsigned i, lhs, rhs0, rhs1, delta, charno; - IMPORT_private_FROM (public); - const char *error; - - delta = 0; /* avoid warning with -O3 */ - - lhs = aiger_max_input_or_latch (public); - - for (i = 0; i < reader->ands; i++) - { - lhs += 2; - charno = reader->charno; - error = aiger_read_delta (private, reader, &delta); - if (error) - return error; - - if (delta > lhs) /* can at most be the same */ - INVALID_DELTA: - return aiger_error_u (private, "character %u: invalid delta", charno); - - rhs0 = lhs - delta; - - charno = reader->charno; - error = aiger_read_delta (private, reader, &delta); - if (error) - return error; - - if (delta > rhs0) /* can well be the same ! */ - goto INVALID_DELTA; - - rhs1 = rhs0 - delta; - - aiger_add_and (public, lhs, rhs0, rhs1); - } - - return 0; -} - -static void -aiger_reader_push_ch (aiger_private * private, aiger_reader * reader, char ch) -{ - PUSH (reader->buffer, reader->top_buffer, reader->size_buffer, ch); -} - -static const char * -aiger_read_comments (aiger * public, aiger_reader * reader) -{ - IMPORT_private_FROM (public); - assert( reader->ch == '\n' ); - - aiger_next_ch (reader); - - while (reader->ch != EOF) - { - while (reader->ch != '\n') - { - aiger_reader_push_ch (private, reader, reader->ch); - aiger_next_ch (reader); - - if (reader->ch == EOF) - return aiger_error_u (private, - "line %u: new line after comment missing", - reader->lineno); - } - - aiger_next_ch (reader); - aiger_reader_push_ch (private, reader, 0); - aiger_add_comment (public, reader->buffer); - reader->top_buffer = 0; - } - - return 0; -} - -static const char * -aiger_read_symbols_and_comments (aiger * public, aiger_reader * reader) -{ - IMPORT_private_FROM (public); - const char *error, *type_name, * type_pos; - unsigned pos, num, count; - aiger_symbol *symbol; - - assert (!reader->buffer); - - for (count = 0;; count++) - { - if (reader->ch == EOF) - return 0; - - if (reader->ch != 'i' && - reader->ch != 'l' && - reader->ch != 'o' && - reader->ch != 'b' && - reader->ch != 'c' && - reader->ch != 'j' && - reader->ch != 'f') - { - if (reader->looks_like_aag) - return aiger_error_u (private, - "line %u: corrupted symbol table " - "('aig' instead of 'aag' header?)", - reader->lineno); - return aiger_error_u (private, - "line %u: expected '[cilobcjf]' or EOF", - reader->lineno); - } - - /* 'c' is a special case as it may be either the start of a comment, - or the start of a constraint symbol */ - if (reader->ch == 'c') - { - if (aiger_next_ch (reader) == '\n' ) - return aiger_read_comments(public, reader); - - type_name = "constraint"; - type_pos = "constraint"; - num = public->num_constraints; - symbol = public->constraints; - - if (!num) - return aiger_error_u (private, - "line %u: " - "unexpected invariance constraint symbol entry prefix 'c ' " - "(comment sections start with 'c' without space)", - reader->lineno_at_last_token_start); - } - else - { - if (reader->ch == 'i') - { - type_name = "input"; - type_pos = "input"; - num = public->num_inputs; - symbol = public->inputs; - } - else if (reader->ch == 'l') - { - type_name = "latch"; - type_pos = "latch"; - num = public->num_latches; - symbol = public->latches; - } - else if (reader->ch == 'o') - { - type_name = "output"; - type_pos = "output"; - num = public->num_outputs; - symbol = public->outputs; - } - else if (reader->ch == 'b') - { - type_name = "bad"; - type_pos = "bad"; - num = public->num_bad; - symbol = public->bad; - } - else if (reader->ch == 'j') - { - type_name = "justice"; - type_pos = "justice"; - num = public->num_justice; - symbol = public->justice; - } - else - { - assert (reader->ch == 'f'); - type_name = "fairness"; - type_pos = "fairness"; - num = public->num_fairness; - symbol = public->fairness; - } - - aiger_next_ch (reader); - } - - error = aiger_read_literal (private, reader, - type_pos, &pos, ' ', 0); - if (error) - return error; - - if (pos >= num) - return aiger_error_usu (private, - "line %u: " - "%s symbol table entry position %u too large", - reader->lineno_at_last_token_start, type_name, pos); - - symbol += pos; - - if (symbol->name) - return aiger_error_usu (private, - "line %u: %s literal %u has multiple symbols", - reader->lineno_at_last_token_start, type_name, - symbol->lit); - - while (reader->ch != '\n' && reader->ch != EOF) - { - aiger_reader_push_ch (private, reader, reader->ch); - aiger_next_ch (reader); - } - - if (reader->ch == EOF) - return aiger_error_u (private, - "line %u: new line missing", reader->lineno); - - assert (reader->ch == '\n'); - aiger_next_ch (reader); - - aiger_reader_push_ch (private, reader, 0); - symbol->name = aiger_copy_str (private, reader->buffer); - reader->top_buffer = 0; - } -} - -const char * -aiger_read_generic (aiger * public, void *state, aiger_get get) -{ - IMPORT_private_FROM (public); - aiger_reader reader; - const char *error; - - assert (!aiger_error (public)); - - CLR (reader); - - reader.lineno = 1; - reader.state = state; - reader.get = get; - reader.ch = ' '; - - error = aiger_read_header (public, &reader); - if (error) - return error; - - if (reader.mode == aiger_ascii_mode) - error = aiger_read_ascii (public, &reader); - else - error = aiger_read_binary (public, &reader); - - if (error) - return error; - - error = aiger_read_symbols_and_comments (public, &reader); - - DELETEN (reader.buffer, reader.size_buffer); - - if (error) - return error; - - return aiger_check (public); -} - -const char * -aiger_read_from_file (aiger * public, FILE * file) -{ - assert (!aiger_error (public)); - return aiger_read_generic (public, file, (aiger_get) aiger_default_get); -} - -const char * -aiger_open_and_read_from_file (aiger * public, const char *file_name) -{ - IMPORT_private_FROM (public); - char *cmd, size_cmd; - const char *res; - int pclose_file; - FILE *file; - - assert (!aiger_error (public)); - - if (aiger_has_suffix (file_name, ".gz")) - { - size_cmd = strlen (file_name) + strlen (GUNZIP); - NEWN (cmd, size_cmd); - sprintf (cmd, GUNZIP, file_name); - file = popen (cmd, "r"); - DELETEN (cmd, size_cmd); - pclose_file = 1; - } - else - { - file = fopen (file_name, "rb"); - pclose_file = 0; - } - - if (!file) - return aiger_error_s (private, "can not read '%s'", file_name); - - res = aiger_read_from_file (public, file); - - if (pclose_file) - pclose (file); - else - fclose (file); - - return res; -} - -const char * -aiger_get_symbol (aiger * public, unsigned lit) -{ - IMPORT_private_FROM (public); - aiger_symbol *symbol; - aiger_type *type; - unsigned var; - - assert (!aiger_error (public)); - - assert (lit); - assert (!aiger_sign (lit)); - - var = aiger_lit2var (lit); - assert (var <= public->maxvar); - type = private->types + var; - - if (type->input) - symbol = public->inputs; - else if (type->latch) - symbol = public->latches; - else - return 0; - - return symbol[type->idx].name; -} - -static aiger_type * -aiger_lit2type (aiger * public, unsigned lit) -{ - IMPORT_private_FROM (public); - aiger_type *type; - unsigned var; - - var = aiger_lit2var (lit); - assert (var <= public->maxvar); - type = private->types + var; - - return type; -} - -int -aiger_lit2tag (aiger * public, unsigned lit) -{ - aiger_type * type; - lit = aiger_strip (lit); - if (!lit) return 0; - type = aiger_lit2type (public, lit); - if (type->input) return 1; - if (type->latch) return 2; - return 3; -} - -aiger_symbol * -aiger_is_input (aiger * public, unsigned lit) -{ - aiger_type *type; - aiger_symbol *res; - - assert (!aiger_error (public)); - type = aiger_lit2type (public, lit); - if (!type->input) - return 0; - - res = public->inputs + type->idx; - - return res; -} - -aiger_symbol * -aiger_is_latch (aiger * public, unsigned lit) -{ - aiger_symbol *res; - aiger_type *type; - - assert (!aiger_error (public)); - type = aiger_lit2type (public, lit); - if (!type->latch) - return 0; - - res = public->latches + type->idx; - - return res; -} - -aiger_and * -aiger_is_and (aiger * public, unsigned lit) -{ - aiger_type *type; - aiger_and *res; - - assert (!aiger_error (public)); - type = aiger_lit2type (public, lit); - if (!type->and) - return 0; - - res = public->ands + type->idx; - - return res; -} diff --git a/aiger.h b/aiger.h deleted file mode 100644 index 84437fb..0000000 --- a/aiger.h +++ /dev/null @@ -1,359 +0,0 @@ -/*************************************************************************** -Copyright (c) 2006 - 2018, Armin Biere, Johannes Kepler University. - -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. -***************************************************************************/ - -/*------------------------------------------------------------------------*/ -/* This file contains the API of the 'AIGER' library, which is a reader and - * writer for the AIGER AIG format. The code of the library - * consists of 'aiger.c' and 'aiger.h'. It is independent of 'simpaig.c' - * and 'simpaig.h'. - * library. - */ -#ifndef aiger_h_INCLUDED -#define aiger_h_INCLUDED - -#include - -/*------------------------------------------------------------------------*/ - -#define AIGER_VERSION "1.9" - -/*------------------------------------------------------------------------*/ - -typedef struct aiger aiger; -typedef struct aiger_and aiger_and; -typedef struct aiger_symbol aiger_symbol; - -/*------------------------------------------------------------------------*/ -/* AIG references are represented as unsigned integers and are called - * literals. The least significant bit is the sign. The index of a literal - * can be obtained by dividing the literal by two. Only positive indices - * are allowed, which leaves 0 for the boolean constant FALSE. The boolean - * constant TRUE is encoded as the unsigned number 1 accordingly. - */ -#define aiger_false 0 -#define aiger_true 1 - -#define aiger_is_constant(l) \ - ((l) == aiger_false || ((l) == aiger_true)) - -#define aiger_sign(l) \ - (((unsigned)(l))&1) - -#define aiger_strip(l) \ - (((unsigned)(l))&~1) - -#define aiger_not(l) \ - (((unsigned)(l))^1) - -/*------------------------------------------------------------------------*/ -/* Each literal is associated to a variable having an unsigned index. The - * variable index is obtained by deviding the literal index by two, which is - * the same as removing the sign bit. - */ -#define aiger_var2lit(i) \ - (((unsigned)(i)) << 1) - -#define aiger_lit2var(l) \ - (((unsigned)(l)) >> 1) - -/*------------------------------------------------------------------------*/ -/* Callback functions for client memory management. The 'free' wrapper will - * get as last argument the size of the memory as it was allocated. - */ -typedef void *(*aiger_malloc) (void *mem_mgr, size_t); -typedef void (*aiger_free) (void *mem_mgr, void *ptr, size_t); - -/*------------------------------------------------------------------------*/ -/* Callback function for client character stream reading. It returns an - * ASCII character or EOF. Thus is has the same semantics as the standard - * library 'getc'. See 'aiger_read_generic' for more details. - */ -typedef int (*aiger_get) (void *client_state); - -/*------------------------------------------------------------------------*/ -/* Callback function for client character stream writing. The return value - * is EOF iff writing failed and otherwise the character 'ch' casted to an - * unsigned char. It has therefore the same semantics as 'fputc' and 'putc' - * from the standard library. - */ -typedef int (*aiger_put) (char ch, void *client_state); - -/*------------------------------------------------------------------------*/ - -enum aiger_mode -{ - aiger_binary_mode = 0, - aiger_ascii_mode = 1, - aiger_stripped_mode = 2, /* can be ORed with one of the previous */ -}; - -typedef enum aiger_mode aiger_mode; - -/*------------------------------------------------------------------------*/ - -struct aiger_and -{ - unsigned lhs; /* as literal [2..2*maxvar], even */ - unsigned rhs0; /* as literal [0..2*maxvar+1] */ - unsigned rhs1; /* as literal [0..2*maxvar+1] */ -}; - -/*------------------------------------------------------------------------*/ - -struct aiger_symbol -{ - unsigned lit; /* as literal [0..2*maxvar+1] */ - unsigned next, reset; /* used only for latches */ - unsigned size, * lits; /* used only for justice */ - char *name; -}; - -/*------------------------------------------------------------------------*/ -/* This is the externally visible state of the library. The format is - * almost the same as the ASCII file format. The first part is exactly as - * in the header 'M I L O A' and optional 'B C J F' after the format identifier - * string. - */ -struct aiger -{ - /* variable not literal index, e.g. maxlit = 2*maxvar + 1 - */ - unsigned maxvar; - - unsigned num_inputs; - unsigned num_latches; - unsigned num_outputs; - unsigned num_ands; - unsigned num_bad; - unsigned num_constraints; - unsigned num_justice; - unsigned num_fairness; - - aiger_symbol *inputs; /* [0..num_inputs[ */ - aiger_symbol *latches; /* [0..num_latches[ */ - aiger_symbol *outputs; /* [0..num_outputs[ */ - aiger_symbol *bad; /* [0..num_bad[ */ - aiger_symbol *constraints; /* [0..num_constraints[ */ - aiger_symbol *justice; /* [0..num_justice[ */ - aiger_symbol *fairness; /* [0..num_fairness[ */ - - aiger_and *ands; /* [0..num_ands[ */ - - char **comments; /* zero terminated */ -}; - -/*------------------------------------------------------------------------*/ -/* Version and CVS identifier. - */ -const char *aiger_id (void); /* not working after moving to 'git' */ -const char *aiger_version (void); - -/*------------------------------------------------------------------------*/ -/* You need to initialize the library first. This generic initialization - * function uses standard 'malloc' and 'free' from the standard library for - * memory management. - */ -aiger *aiger_init (void); - -/*------------------------------------------------------------------------*/ -/* Same as previous initialization function except that a memory manager - * from the client is used for memory allocation. See the 'aiger_malloc' - * and 'aiger_free' definitions above. - */ -aiger *aiger_init_mem (void *mem_mgr, aiger_malloc, aiger_free); - -/*------------------------------------------------------------------------*/ -/* Reset and delete the library. - */ -void aiger_reset (aiger *); - -/*------------------------------------------------------------------------*/ -/* Treat the literal 'lit' as input, output, latch, bad, constraint, - * justice of fairness respectively. The - * literal of latches and inputs can not be signed nor a constant (< 2). - * You can not register latches nor inputs multiple times. An input can not - * be a latch. The last argument is the symbolic name if non zero. - * The same literal can of course be used for multiple outputs. - */ -void aiger_add_input (aiger *, unsigned lit, const char *); -void aiger_add_latch (aiger *, unsigned lit, unsigned next, const char *); -void aiger_add_output (aiger *, unsigned lit, const char *); -void aiger_add_bad (aiger *, unsigned lit, const char *); -void aiger_add_constraint (aiger *, unsigned lit, const char *); -void aiger_add_justice (aiger *, unsigned size, unsigned *, const char *); -void aiger_add_fairness (aiger *, unsigned lit, const char *); - -/*------------------------------------------------------------------------*/ -/* Add a reset value to the latch 'lit'. The 'lit' has to be a previously - * added latch and 'reset' is either '0', '1' or equal to 'lit', the latter - * means undefined. - */ -void aiger_add_reset (aiger *, unsigned lit, unsigned reset); - -/*------------------------------------------------------------------------*/ -/* Register an unsigned AND with AIGER. The arguments are signed literals - * as discussed above, e.g. the least significant bit stores the sign and - * the remaining bit the variable index. The 'lhs' has to be unsigned - * (even). It identifies the AND and can only be registered once. After - * registration an AND can be accessed through 'ands[aiger_lit2idx (lhs)]'. - */ -void aiger_add_and (aiger *, unsigned lhs, unsigned rhs0, unsigned rhs1); - -/*------------------------------------------------------------------------*/ -/* Add a line of comments. The comment may not contain a new line character. - */ -void aiger_add_comment (aiger *, const char *comment_line); - -/*------------------------------------------------------------------------*/ -/* This checks the consistency for debugging and testing purposes. In - * particular, it is checked that all 'next' literals of latches, all - * outputs, and all right hand sides of ANDs are defined, where defined - * means that the corresponding literal is a constant 0 or 1, or defined as - * an input, a latch, or AND gate. Furthermore the definitions of ANDs are - * checked to be non cyclic. If a check fails a corresponding error message - * is returned. - */ -const char *aiger_check (aiger *); - -/*------------------------------------------------------------------------*/ -/* These are the writer functions for AIGER. They return zero on failure. - * The assumptions on 'aiger_put' are the same as with 'fputc' from the - * standard library (see the 'aiger_put' definition above). Note, that - * writing in binary mode triggers 'aig_reencode' and thus destroys the - * original literal association and may even delete AND nodes. See - * 'aiger_reencode' for more details. - */ -int aiger_write_to_file (aiger *, aiger_mode, FILE *); -int aiger_write_to_string (aiger *, aiger_mode, char *str, size_t len); -int aiger_write_generic (aiger *, aiger_mode, void *state, aiger_put); - -/*------------------------------------------------------------------------*/ -/* The following function allows to write to a file. The write mode is - * determined from the suffix in the file name. The mode used is ASCII for - * a '.aag' suffix and binary mode otherwise. In addition a '.gz' suffix can - * be added which requests the file to written by piping it through 'gzip'. - * This feature assumes that the 'gzip' program is in your path and can be - * executed through 'popen'. The return value is non zero on success. - */ -int aiger_open_and_write_to_file (aiger *, const char *file_name); - -/*------------------------------------------------------------------------*/ -/* The binary format reencodes all indices. After normalization the input - * indices come first followed by the latch and then the AND indices. In - * addition the indices will be topologically sorted to respect the - * child/parent relation, e.g. child indices will always be smaller than - * their parent indices. This function can directly be called by the - * client. As a side effect, ANDs that are not in any cone of a next state - * function nor in any cone of an output function are discarded. The new - * indices of ANDs start immediately after all input and latch indices. The - * data structures are updated accordingly including 'maxvar'. The client - * data within ANDs is reset to zero. - */ -int aiger_is_reencoded (aiger *); -void aiger_reencode (aiger *); - -/*------------------------------------------------------------------------*/ -/* This function computes the cone of influence (coi). The coi contains - * those literals that may have an influence to one of the outputs. A - * variable 'v' is in the coi if the array returned as result is non zero at - * position 'v'. All other variables can be considered redundant. The array - * returned is valid until the next call to this function and will be - * deallocated on reset. - * - * TODO: this is just a stub and actually not really implemented yet. - */ -const unsigned char * aiger_coi (aiger *); /* [1..maxvar] */ - -/*------------------------------------------------------------------------*/ -/* Read an AIG from a FILE, a string, or through a generic interface. These - * functions return a non zero error message if an error occurred and - * otherwise 0. The paramater 'aiger_get' has the same return values as - * 'getc', e.g. it returns 'EOF' when done. After an error occurred the - * library becomes invalid. Only 'aiger_reset' or 'aiger_error' can be - * used. The latter returns the previously returned error message. - */ -const char *aiger_read_from_file (aiger *, FILE *); -const char *aiger_read_from_string (aiger *, const char *str); -const char *aiger_read_generic (aiger *, void *state, aiger_get); - -/*------------------------------------------------------------------------*/ -/* Returns a previously generated error message if the library is in an - * invalid state. After this function returns a non zero error message, - * only 'aiger_reset' can be called (beside 'aiger_error'). The library can - * reach an invalid through a failed read attempt, or if 'aiger_check' - * failed. - */ -const char *aiger_error (aiger *); - -/*------------------------------------------------------------------------*/ -/* Same semantics as with 'aiger_open_and_write_to_file' for reading. - */ -const char *aiger_open_and_read_from_file (aiger *, const char *); - -/*------------------------------------------------------------------------*/ -/* Write symbol table or the comments to a file. Result is zero on failure. - */ -int aiger_write_symbols_to_file (aiger *, FILE * file); -int aiger_write_comments_to_file (aiger *, FILE * file); - -/*------------------------------------------------------------------------*/ -/* Remove symbols and comments. The result is the number of symbols - * and comments removed. - */ -unsigned aiger_strip_symbols_and_comments (aiger *); - -/*------------------------------------------------------------------------*/ -/* If 'lit' is an input or a latch with a name, the symbolic name is - * returned. Note, that literals can be used for multiple outputs. - * Therefore there is no way to associate a name with a literal itself. - * Names for outputs are stored in the 'outputs' symbols and can only be - * accesed through a linear traversal of the output symbols. - */ -const char *aiger_get_symbol (aiger *, unsigned lit); - -/*------------------------------------------------------------------------*/ -/* Return tag of the literal: - * - * 0 = constant - * 1 = input - * 2 = latch - * 3 = and - */ - -int aiger_lit2tag (aiger *, unsigned lit); - -/*------------------------------------------------------------------------*/ -/* Check whether the given unsigned, e.g. even, literal was defined as - * 'input', 'latch' or 'and'. The command returns a zero pointer if the - * literal was not defined as 'input', 'latch', or 'and' respectively. - * Otherwise a pointer to the corresponding input or latch symbol is returned. - * In the case of an 'and' the AND node is returned. The returned symbol - * if non zero is in the respective array of 'inputs', 'latches' and 'ands'. - * It thus also allows to extract the position of an input or latch literal. - * For outputs this is not possible, since the same literal may be used for - * several outputs. - */ -aiger_symbol *aiger_is_input (aiger *, unsigned lit); -aiger_symbol *aiger_is_latch (aiger *, unsigned lit); -aiger_and *aiger_is_and (aiger *, unsigned lit); - -#endif diff --git a/circuit.cpp b/circuit.cpp deleted file mode 100644 index c50d477..0000000 --- a/circuit.cpp +++ /dev/null @@ -1,449 +0,0 @@ -#include "sweep.hpp" -#include "circuit.hpp" - -bool Sweep::match_xor(int x) { // check clause x, -y, -z <==> xor - int y = C[x][0], z = C[x][1]; - if (y >= 0 || z >= 0) return false; - if (del[-y] || del[-z] || !C[-y].sz || !C[-z].sz) return false; - int u1 = C[-y][0], v1 = C[-y][1]; - int u2 = C[-z][0], v2 = C[-z][1]; - if (u1 == -u2 && v1 == -v2) goto doit; - if (u1 == -v2 && v1 == -u2) goto doit; - return false; -doit: - del[x] = 1; - if (C[-y].outs <= 1) del[-y] = 2; - if (C[-z].outs <= 1) del[-z] = 2; - C[x][0] = C[-y][0], C[x][1] = C[-y][1]; - C[x].type = Xor; - - return true; -} - -bool Sweep::match_majority(int x) { - // x = -y & z - // z = -v & -w - // y = a1 & a2 - // v = a1 & a3 - // w = a2 & a3 - int y = C[x][0], z = C[x][1]; - if (y > 0) std::swap(y, z); - if (y >= 0 || z <= 0) return false; - if (del[-y] || del[z] || !C[-y].sz || !C[z].sz) return false; - int v = C[z][0], w = C[z][1]; - if (v >= 0 || w >= 0) return false; - if (del[-v] || del[-w] || !C[-v].sz || !C[-w].sz) return false; - // -y, -w, -v - int a = C[-y][0], b = C[-y][1]; - if (C[-v][1] == a || C[-v][1] == b) std::swap(C[-v][0], C[-v][1]); - if (C[-w][1] == a || C[-w][1] == b) std::swap(C[-w][0], C[-w][1]); - if (C[-v][0] != a && C[-w][0] != a) return false; - if (C[-v][0] != b && C[-w][0] != b) return false; - if (C[-v][1] != C[-w][1]) return false; - del[x] = 1; - if (C[-y].outs <= 1) del[-y] = 2; - if (C[z].outs <= 1) del[z] = 2; - if (C[-v].outs <= 1) del[-v] = 2; - if (C[-w].outs <= 1) del[-w] = 2; - - C[x][0] = -a; C[x][1] = -b; - C[x].push(-C[-w][1]); - C[x].type = Majority; - return true; -} - -void Sweep::adjust_not() { - int *pos = new int[maxvar + 1]; - int *neg = new int[maxvar + 1]; - for (int i = 1; i <= maxvar; i++) - pos[i] = neg[i] = 0; - for (int i = 1; i <= maxvar; i++) { - if (!C[i].sz || del[i] == 2) continue; - for (int j = 0; j < C[i].sz; j++) { - int v = C[i][j]; - if (v > 0) pos[v]++; - else neg[-v]++; - } - } - for (int i = 1; i <= maxvar; i++) { - if (!C[i].sz || del[i] == 2) continue; - if (C[i].type == Xor && pos[i] == 0 && neg[i] > 0) { - for (int j = 0; j < C[i].sz; j++) - if (C[i][j] < 0 && C[-C[i][j]].neg == 0) {C[i][j] = -C[i][j]; C[i].neg = 1; break;} - } - // if (C[i].type == Xor) { - // int z = 0; - // for (int j = 0; j < C[i].sz; j++) - // if (C[i][j] < 0) {C[i][j] = -C[i][j]; z ^= 1;} - // if (z) C[i].neg = 1; - // } - } -} - -void Sweep::match_HA() { - std::map M; - int lits = maxvar << 1 | 1; - for (int i = 1; i <= maxvar; i++) { - if (!C[i].sz || del[i] == 2 || C[i].type != And) continue; - int mapid = C[i][0] * lits + C[i][1]; - M[mapid] = i; - } - for (int i = 1; i <= maxvar; i++) { - if (!C[i].sz || del[i] == 2 || C[i].type != Xor) continue; - int mapid = C[i][0] * lits + C[i][1]; - int id = M[mapid]; - if (id) { - C[i].type = HA; - C[i].carrier = id; - del[id] = 2; - continue; - } - - mapid = (-C[i][0]) * lits - C[i][1]; - id = M[mapid]; - if (id) { - C[i].type = HA; - C[i].carrier = id; - C[i][0] = -C[i][0]; - C[i][1] = -C[i][1]; - del[id] = 2; - continue; - } - - mapid = C[i][0] * lits - C[i][1]; - id = M[mapid]; - if (id) { - C[i].type = HA; - C[i].carrier = id; - C[i][1] = -C[i][1]; - C[i].neg = 1; - del[id] = 2; - continue; - } - - mapid = (-C[i][0]) * lits + C[i][1]; - id = M[mapid]; - if (id) { - C[i].type = HA; - C[i].carrier = id; - C[i][0] = -C[i][0]; - C[i].neg = 1; - del[id] = 2; - continue; - } - } -} - -bool Sweep::line_positive(int to) { - return (to < 0) == C[abs(to)].neg; -} - -void Sweep::recalculate_outs() { - for (int i = 1; i <= maxvar; i++) - C[i].outs = 0; - for (int i = 1; i <= maxvar; i++) { - circuit *c = &C[i]; - if (!c->sz || del[i] == 2) continue; - for (int j = 0; j < c->sz; j++) { - C[abs(c->to[j])].outs++; - } - } -} - -void Sweep::match_FA() { - for (int i = 1; i <= maxvar; i++) { - circuit *c = &C[i]; - if (!c->sz || del[i] == 2) continue; - if (c->type != HA) continue; - C[abs(c->carrier)].to.clear(); - C[abs(c->carrier)].to.push(i); - C[abs(c->carrier)].sz = 1; - C[abs(c->carrier)].neg = c->carrier < 0; - } - - for(int i=1; i<=maxvar; i++) { - if (!C[i].sz || del[i] == 2) continue; - - circuit *c = &C[i]; - - if(c->type != And) continue; - - if(c->sz != 2) continue; - - if(c->to[0] >= 0) continue; - if(c->to[1] >= 0) continue; - - if(C[abs(c->to[0])].sz != 1) continue; - if(C[abs(c->to[1])].sz != 1) continue; - - int ha1 = C[abs(c->to[0])][0]; - int ha2 = C[abs(c->to[1])][0]; - - ha1 = abs(ha1); - ha2 = abs(ha2); - - if(C[ha1].type != HA) continue; - if(C[ha2].type != HA) continue; - - bool check_link = true; - for(int k=0; ktype = FA; - fa->carrier = -i; - vec new_vec; - for(int k=0; kto); - fa->sz = fa->to.size(); - - C[i].to.clear(); - C[i].sz = 0; - C[i].neg = !C[i].neg; - } -} - -void Sweep::to_multi_input_gates() { - //printf("hello\n %d\n", maxvar); - std::queue q; - q.push(maxvar); - while(!q.empty()) { - int u = q.front(); - q.pop(); - - circuit *c = &C[u]; - - if(u == maxvar) { - for(int i=0; isz; i++) { - if (!C[abs(c->to[i])].sz || del[abs(c->to[i])] == 2) continue; - q.push(abs(c->to[i])); - } - continue; - } - - for(int i=0; isz; i++) { - circuit *t = &C[abs(c->to[i])]; - if(t->type != c->type) continue; - vec new_vec; - if(c->type == Xor) { - //printf("XOR: %d %d\n", u, c->to[i]); - for(int j=0; jsz; j++) { - new_vec.push(t->to[j]); - //printf("add %d\n", t->to[j]); - } - - for(int j=0; jsz; j++) { - if(i == j) { - if(!line_positive(c->to[j])) - new_vec[0] = -new_vec[0]; - } else { - new_vec.push(c->to[j]); - } - } - - if(t->outs == 1) { - del[abs(c->to[i])] = 2; - //printf("del: %d\n", c->to[i]); - } - - new_vec.copyTo(c->to); - c->sz = new_vec.size(); - - q.push(u); - break; - } - - if(c->type == And && line_positive(c->to[i])) { - if(t->to.size() == 0) continue; - - //printf("AND: %d %d\n", u, c->to[i]); - t->to.copyTo(new_vec); - //printf("new_vec %d\n", new_vec.size()); - - for(int j=0; jsz; j++) { - if(i != j) { - new_vec.push(c->to[j]); - } - } - - if(C[abs(c->to[i])].outs == 1) { - del[abs(c->to[i])] = 2; - } - - new_vec.copyTo(c->to); - c->sz = new_vec.size(); - - q.push(u); - - break; - } - } - - - - for(int i=0; isz; i++) { - if (!C[abs(c->to[i])].sz || del[abs(c->to[i])] == 2) continue; - q.push(abs(c->to[i])); - } - } -} - -void Sweep::to_dot_graph(const char* filename, int end_point) { - std::ofstream file(filename); - std::queue q; - q.push(abs(end_point)); - std::set used; - used.insert(abs(end_point)); - file << "digraph \"graph\" {\n"; - - char str[1024]; - - while(!q.empty()) { - int u = q.front(); - q.pop(); - circuit *c = &C[u]; - - if(!c->sz || del[u] == 2) continue; - - sprintf(str, "A%d[label=\"%d (%s)\"];\n", u, u, gate_type[c->type].c_str()); - file << str; - if (c->type == HA || c->type == FA) { - int a = u * (C[u].neg ? -1 : 1); - int b = c->carrier; - sprintf(str, "A%d->A%d[arrowhead=%s]\n", u, abs(b), !line_positive(b) ? "dot" : "none"); - file << str; - } - else { - int t = u * (C[u].neg ? -1 : 1); - } - for (int j = 0; j < c->sz; j++) { - /** - * 删除初始输入 - */ - if(abs(c->to[j]) <= 14) continue; - - sprintf(str, "A%d->A%d[arrowhead=%s]\n", abs(c->to[j]), u, !line_positive(c->to[j]) ? "dot" : "none"); - file << str; - } - - for(int j=0; jsz; j++) { - int x = abs(c->to[j]); - if(used.count(x)) continue; - used.insert(x); - q.push(x); - } - } - - file << "}\n"; -} - -void Sweep::identify() { - - del = new int[maxvar + 1]; - for (int i = 1; i <= maxvar; i++) del[i] = 0; - recalculate_outs(); - for (int i = 1; i <= maxvar; i++) { - if (!C[i].sz || del[i] == 2) continue; - if (match_xor(i)) continue; - } - - // recalculate_outs(); - - // for (int i = 1; i <= maxvar; i++) { - // if (!C[i].sz || del[i] == 2) continue; - // if (match_majority(i)) continue; - // } - - recalculate_outs(); - //adjust_not(); - //match_HA(); - - //to_multi_input_gates(); - //match_FA(); - - // printf("digraph \"graph\" {\n"); - // for (int i = 1; i <= maxvar; i++) { - // circuit *c = &C[i]; - // if (!c->sz || del[i] == 2) continue; - - // printf("A%d[label=\"%d (%s)\"];\n", i, i, gate_type[c->type].c_str()); - - // if (c->type == HA || c->type == FA) { - // int a = i * (C[i].neg ? -1 : 1); - // int b = c->carrier; - // printf("A%d->A%d[arrowhead=%s]\n", i, abs(b), !line_positive(b) ? "dot" : "none"); - // } - // else { - // int t = i * (C[i].neg ? -1 : 1); - // } - // for (int j = 0; j < c->sz; j++) { - // if(abs(c->to[j]) <= 14) continue; - // printf("A%d->A%d[arrowhead=%s]\n", abs(c->to[j]), i, !line_positive(c->to[j]) ? "dot" : "none"); - // } - // } - // printf("}\n"); - - recalculate_outs(); - // for (int i = 1; i <= maxvar; i++) { - // circuit *c = &C[i]; - // if (!c->sz || del[i] == 2) continue; - - // if (c->type == HA || c->type == FA) - // printf("( %d %d )", i * (C[i].neg ? -1 : 1), c->carrier); - // else - // printf("%d", i * (C[i].neg ? -1 : 1)); - - // printf(" = %s ( ", gate_type[c->type].c_str()); - - // for (int j = 0; j < c->sz; j++) { - // printf("%d ", c->to[j]); - // } - - // puts(")"); - // } - - inv_C = new vec[maxvar + 1]; - for (int i = 1; i <= maxvar; i++) { - circuit *c = &C[i]; - if (!c->sz || del[i] == 2) continue; - for (int j = 0; j < c->sz; j++) { - inv_C[abs(c->to[j])].push(i); - } - } - // to_dot_graph("graph1.dot", 291); - // to_dot_graph("graph2.dot", 175); - - // recalculate_outs(); - // for (int i = 1; i <= maxvar; i++) { - // circuit *c = &C[i]; - // if (del[i] == 2) continue; - // printf("%d : %d (outs)\n", i, c->outs); - // } - -} \ No newline at end of file diff --git a/circuit.hpp b/circuit.hpp deleted file mode 100644 index 384e563..0000000 --- a/circuit.hpp +++ /dev/null @@ -1,16 +0,0 @@ -#ifndef circuit_hpp_INCLUDED -#define circuit_hpp_INCLUDED - -enum gate_type {And, Xor, Majority, HA, FA}; -const std::string gate_type[5] = {"and", "xor", "majority", "HA", "FA"}; - -struct circuit { - vec to; - int sz, outs, type, neg, carrier; - circuit() : sz(0), outs(0), type(0), neg(0), carrier(0) {} - void push(int x) { to.push(x); sz++; } - int &operator [] (int index) { return to[index]; } - const int& operator [] (int index) const { return to[index]; } -}; - -#endif \ No newline at end of file diff --git a/cms.log b/cms.log deleted file mode 100644 index 8ae66aa..0000000 --- a/cms.log +++ /dev/null @@ -1,408 +0,0 @@ --293 -292 0 --293 176 0 -292 -176 293 0 --294 292 0 --294 -176 0 --292 176 294 0 -289 231 292 0 --173 154 176 0 --289 -288 0 --289 287 0 -288 -287 289 0 -228 197 231 0 --173 172 0 --173 -157 0 --172 157 173 0 --151 124 154 0 --288 -285 0 --288 -242 0 -285 242 288 0 --287 -286 0 --287 -249 0 -286 249 287 0 -225 208 228 0 --197 -196 0 --197 195 0 -196 -195 197 0 --172 171 0 --172 -160 0 --171 160 172 0 --150 127 157 0 --151 150 0 --151 -127 0 --150 127 151 0 -121 88 124 0 --285 -284 0 --285 283 0 -284 -283 285 0 --242 -241 0 --242 240 0 -241 -240 242 0 --286 -285 0 --286 -248 0 -285 248 286 0 --249 -248 0 --249 -242 0 -248 242 249 0 -222 216 225 0 -205 200 208 0 --196 -193 0 --196 -180 0 -193 180 196 0 --195 -194 0 --195 -187 0 -194 187 195 0 --171 170 0 --171 -163 0 --170 163 171 0 -149 130 160 0 --150 -149 0 --150 -130 0 -149 130 150 0 --119 116 127 0 --121 -120 0 --121 -115 0 -120 115 121 0 -85 78 88 0 --284 -281 0 --284 -255 0 -281 255 284 0 --283 -282 0 --283 -262 0 -282 262 283 0 --241 -238 0 --241 97 0 -238 -97 241 0 --240 -239 0 --240 -232 0 -239 232 240 0 -245 193 248 0 --219 42 222 0 -213 20 216 0 --205 -204 0 --205 203 0 -204 -203 205 0 --41 27 200 0 -190 31 193 0 --180 179 0 --180 -116 0 --179 116 180 0 --194 -193 0 --194 -186 0 -193 186 194 0 --187 -186 0 --187 -180 0 -186 180 187 0 --170 169 0 --170 -166 0 --169 166 170 0 --147 144 163 0 --149 -148 0 --149 -143 0 -148 143 149 0 -112 109 130 0 -114 91 119 0 --116 106 0 --116 105 0 --106 -105 116 0 --120 -119 0 --120 116 0 -119 -116 120 0 --115 -114 0 --115 -91 0 -114 91 115 0 --82 81 85 0 -75 48 78 0 --281 -280 0 --281 279 0 -280 -279 281 0 --255 -254 0 --255 253 0 -254 -253 255 0 --282 -281 0 --282 -261 0 -281 261 282 0 --262 -261 0 --262 -255 0 -261 255 262 0 --235 105 238 0 --97 96 0 --97 95 0 --96 -95 97 0 --239 -238 0 --239 -58 0 -238 58 239 0 --232 97 0 --232 -58 0 --97 58 232 0 -186 180 245 0 -82 21 219 0 --42 5 0 --42 4 0 --5 -4 42 0 --213 -212 0 --213 211 0 -212 -211 213 0 -17 16 20 0 --204 63 0 --204 -31 0 --63 31 204 0 --203 -202 0 --203 -201 0 -202 201 203 0 -38 37 41 0 --27 26 0 --27 25 0 --26 -25 27 0 -63 54 190 0 -26 25 31 0 --179 -178 0 --179 -177 0 -178 177 179 0 --183 62 186 0 --169 168 0 --169 167 0 --168 -167 169 0 --140 137 166 0 -142 133 147 0 --144 12 0 --144 6 0 --12 -6 144 0 --148 -147 0 --148 144 0 -147 -144 148 0 --143 -142 0 --143 -133 0 -142 133 143 0 -103 94 112 0 -106 105 109 0 --114 -113 0 --114 -104 0 -113 104 114 0 -73 70 91 0 --106 12 0 --106 2 0 --12 -2 106 0 --105 6 0 --105 5 0 --6 -5 105 0 --82 12 0 --82 9 0 --12 -9 82 0 --81 -80 0 --81 -79 0 -80 79 81 0 --75 -74 0 --75 -61 0 -74 61 75 0 -45 36 48 0 --280 -277 0 --280 -101 0 -277 101 280 0 --279 -278 0 --279 -269 0 -278 269 279 0 --254 251 0 --254 144 0 --251 -144 254 0 --253 -252 0 --253 -250 0 -252 250 253 0 -258 238 261 0 -106 55 235 0 --96 15 0 --96 8 0 --15 -8 96 0 --95 13 0 --95 3 0 --13 -3 95 0 -53 52 58 0 --21 11 0 --21 7 0 --11 -7 21 0 --212 67 0 --212 62 0 --67 -62 212 0 --211 -210 0 --211 -209 0 -210 209 211 0 --17 10 0 --17 8 0 --10 -8 17 0 --16 14 0 --16 13 0 --14 -13 16 0 --63 5 0 --63 2 0 --5 -2 63 0 --202 54 0 --202 -31 0 --54 31 202 0 --201 63 0 --201 54 0 --63 -54 201 0 --38 15 0 --38 2 0 --15 -2 38 0 --37 6 0 --37 3 0 --6 -3 37 0 --26 8 0 --26 7 0 --8 -7 26 0 --25 13 0 --25 10 0 --13 -10 25 0 --54 53 0 --54 52 0 --53 -52 54 0 --178 105 0 --178 55 0 --105 -55 178 0 --177 106 0 --177 55 0 --106 -55 177 0 -67 28 183 0 --62 15 0 --62 6 0 --15 -6 62 0 --168 12 0 --168 8 0 --12 -8 168 0 --167 13 0 --167 5 0 --13 -5 167 0 -135 134 140 0 --137 12 0 --137 11 0 --12 -11 137 0 --142 -141 0 --142 -136 0 -141 136 142 0 --101 98 133 0 --103 -102 0 --103 -97 0 -102 97 103 0 --58 55 94 0 --113 -112 0 --113 -109 0 -112 109 113 0 --104 -103 0 --104 -94 0 -103 94 104 0 -60 51 73 0 --67 66 70 0 --80 67 0 --80 -66 0 --67 66 80 0 --79 63 0 --79 62 0 --63 -62 79 0 --74 -73 0 --74 -70 0 -73 70 74 0 --61 -60 0 --61 -51 0 -60 51 61 0 --42 41 45 0 -33 24 36 0 --277 -276 0 --277 275 0 -276 -275 277 0 -96 95 101 0 --278 -277 0 --278 -268 0 -277 268 278 0 --269 -268 0 --269 -101 0 -268 101 269 0 --251 137 0 --251 135 0 --137 -135 251 0 --252 251 0 --252 98 0 --251 -98 252 0 --250 144 0 --250 98 0 --144 -98 250 0 --97 58 258 0 --55 15 0 --55 11 0 --15 -11 55 0 --53 8 0 --53 3 0 --8 -3 53 0 --52 13 0 --52 7 0 --13 -7 52 0 --67 12 0 --67 4 0 --12 -4 67 0 --210 62 0 --210 28 0 --62 -28 210 0 --209 67 0 --209 28 0 --67 -28 209 0 --28 11 0 --28 3 0 --11 -3 28 0 --135 8 0 --135 5 0 --8 -5 135 0 --134 15 0 --134 13 0 --15 -13 134 0 --141 -140 0 --141 137 0 -140 -137 141 0 --136 135 0 --136 134 0 --135 -134 136 0 --98 11 0 --98 5 0 --11 -5 98 0 --102 -101 0 --102 98 0 -101 -98 102 0 --60 -59 0 --60 -54 0 -59 54 60 0 --31 28 51 0 -63 62 66 0 --33 -32 0 --33 -27 0 -32 27 33 0 --21 20 24 0 --276 -273 0 --276 134 0 -273 -134 276 0 --275 -274 0 --275 -270 0 -274 270 275 0 --265 251 268 0 --59 -58 0 --59 55 0 -58 -55 59 0 --32 -31 0 --32 28 0 -31 -28 32 0 -137 135 273 0 --274 -273 0 --274 169 0 -273 -169 274 0 --270 169 0 --270 134 0 --169 -134 270 0 -144 98 265 0 --293 -294 0 -293 294 0 --251 252 0 -251 -252 0 --253 255 0 -253 -255 0 --254 266 0 -254 -266 0 --176 292 0 -176 -292 0 -c Solver::solve( ) diff --git a/fraig.cpp b/fraig.cpp deleted file mode 100644 index 1e8089f..0000000 --- a/fraig.cpp +++ /dev/null @@ -1,291 +0,0 @@ -#include "sweep.hpp" -#include "circuit.hpp" -#include "src/cadical.hpp" -extern "C" { - #include "aiger.h" -} - -void Sweep::propagate(int* input, int* result) { - - std::queue q; - - for(int i=0; inum_inputs; i++) { - result[aig->inputs[i].lit] = input[i]; - result[aig->inputs[i].lit+1] = !input[i]; - q.push(aiger_lit2var(aig->inputs[i].lit)); - } - - static int* topo_counter = new int[maxvar + 1]; - memset(topo_counter, 0, (maxvar + 1) * sizeof(int)); - - while(!q.empty()) { - int cur = q.front(); - q.pop(); - for(auto& edge : graph.edge[cur]) { - int v = edge.to; - topo_counter[v]++; - - if(topo_counter[v] == 2) { - q.push(v); - - //cout << "redge: " << v << " " << graph.redge[v][0].to << " " << graph.redge[v][1].to << endl; - - Graph::Edge rhs0_edge = graph.redge[v][0]; - int rhs0 = aiger_var2lit(rhs0_edge.to); - - Graph::Edge rhs1_edge = graph.redge[v][1]; - int rhs1 = aiger_var2lit(rhs1_edge.to); - - result[aiger_var2lit(v)] = result[rhs0 + rhs0_edge.neg] & result[rhs1 + rhs1_edge.neg]; - result[aiger_var2lit(v)+1] = !result[aiger_var2lit(v)]; - - //cout << "var: " << aiger_var2lit(v) << " = " << rhs0 + rhs0_edge.neg << " " << rhs1 + rhs1_edge.neg << " : " << result[aiger_var2lit(v)] << endl; - - } - } - } -} - -void Sweep::circuit_propagate(int *input, int* result) { - std::queue q; - - for(int i=1; i<=aig->num_inputs; i++) { - result[i] = input[i - 1]; - q.push(i); - // printf("%d %d\n", i, result[i]); - } - for (int i = 1; i <= maxvar; i++) seen[i] = 0; - while(!q.empty()) { - int x = q.front(); - q.pop(); - for (int i = 0; i < inv_C[x].size(); i++) { - int v = inv_C[x][i]; - seen[v]++; - if (seen[v] == C[v].sz) { - q.push(v); - if (C[v].type == And) { - result[v] = 1; - for (int j = 0; j < C[v].sz; j++) { - int x = C[v][j]; - result[v] &= x > 0 ? result[abs(x)] : !result[abs(x)]; - } - } - else if (C[v].type == Xor) { - result[v] = 0; - for (int j = 0; j < C[v].sz; j++) { - int x = C[v][j]; - result[v] ^= x > 0 ? result[abs(x)] : !result[abs(x)]; - } - } - else if (C[v].type == Majority) { - int s[2] = {0, 0}; - for (int j = 0; j < C[v].sz; j++) { - int x = C[v][j]; - s[x > 0 ? result[abs(x)] : !result[abs(x)]]++; - } - result[v] = s[1] > s[0] ? 1 : 0; - } - else if (C[v].type == HA) { - assert(C[v].sz == 2); - int s = 0; - for (int j = 0; j < C[v].sz; j++) { - int x = C[v][j]; - s += x > 0 ? result[abs(x)] : !result[abs(x)]; - } - result[v] = s % 2; - result[abs(C[v].carrier)] = s >> 1; - if (C[v].carrier < 0) result[abs(C[v].carrier)] = !result[abs(C[v].carrier)]; - q.push(abs(C[v].carrier)); - } - else if (C[v].type == FA) { - assert(C[v].sz == 3); - int s = 0; - for (int j = 0; j < C[v].sz; j++) { - int x = C[v][j]; - s += x > 0 ? result[abs(x)] : !result[abs(x)]; - } - result[v] = s % 2; - result[abs(C[v].carrier)] = s >> 1; - if (C[v].carrier < 0) result[abs(C[v].carrier)] = !result[abs(C[v].carrier)]; - q.push(abs(C[v].carrier)); - } - if (C[v].neg) result[v] = !result[v]; - // printf("%d %d\n", v, result[v]); - } - } - } - -} - -// int Sweep::seen_cut_points(aiger* aig, int x, int y) { -// std::queue q; -// int *used = - -// x = x & 1 ? -aiger_lit2var(x) : aiger_lit2var(x); -// y = y & 1 ? -aiger_lit2var(y) : aiger_lit2var(y); - -// if (!used[abs(x)]) -// q.push(abs(x)), used[abs(x)] = true; -// if(!used[abs(y)]) -// q.push(abs(y)), used[abs(y)] = true; - -// } - -bool Sweep::check_var_equal(int x, int y, int assume) { - - std::queue q; - - x = x & 1 ? -aiger_lit2var(x) : aiger_lit2var(x); - y = y & 1 ? -aiger_lit2var(y) : aiger_lit2var(y); - - if (!used[abs(x)]) - q.push(abs(x)), used[abs(x)] = true; - if(!used[abs(y)]) - q.push(abs(y)), used[abs(y)] = true; - - int can_del = 2; - - while(!q.empty()) { - int u = q.front(); - q.pop(); - - /* - (u => a & b) <=> ~u | (a & b) <=> (~u | a) & (~u | b) - (u <= a & b) <=> ~(a & b) | u <=> ~a | ~b | u - */ - if(graph.redge[u].size() == 0) continue; - - int a = graph.redge[u][0].to; - int b = graph.redge[u][1].to; - - //cout << "AND " << aiger_var2lit(u) << " " << (aiger_var2lit(a) + graph.redge[u][0].neg) << " " << (aiger_var2lit(b) + graph.redge[u][1].neg) << endl; - - if(graph.redge[u][0].neg) a = -a; - if(graph.redge[u][1].neg) b = -b; - - - solver->add(-u), solver->add( a), solver->add(0); - solver->add(-u), solver->add( b), solver->add(0); - solver->add(-a), solver->add(-b), solver->add(u), solver->add(0); - - a = abs(a), b = abs(b); - - if(!used[a]) - q.push(a), used[a] = true, can_del++; - - if(!used[b]) - q.push(b), used[b] = true, can_del++; - } - - //Assume -NV - solver->add(-assume), solver->add(-x), solver->add(-y), solver->add(0); - solver->add(-assume), solver->add(x), solver->add(y), solver->add(0); - - solver->assume (assume); - - int result = solver->solve (); - - // if (result == 20) printf("can delete %d vars\n", can_del); - return result == 20; -} - -bool Sweep::check_constant(int x, int val) { - - std::queue q; - x = x & 1 ? -aiger_lit2var(x) : aiger_lit2var(x); - - if (!used[abs(x)]) q.push(abs(x)), used[abs(x)] = true; - - while(!q.empty()) { - int u = q.front(); - q.pop(); - - if(graph.redge[u].size() == 0) continue; - - int a = graph.redge[u][0].to; - int b = graph.redge[u][1].to; - if(graph.redge[u][0].neg) a = -a; - if(graph.redge[u][1].neg) b = -b; - - solver->add(-u), solver->add( a), solver->add(0); - solver->add(-u), solver->add( b), solver->add(0); - solver->add(-a), solver->add(-b), solver->add(u), solver->add(0); - - a = abs(a), b = abs(b); - - if(!used[a]) q.push(a), used[a] = true; - if(!used[b]) q.push(b), used[b] = true; - } - - solver->assume (x * (val ? -1 : 1)); - - int result = solver->solve(); - return result == 20; -} - -void Sweep::random_simulation() { - - int* result = new int[2 * maxvar + 2]; - int* circuit_res = new int[maxvar + 1]; - int* input_vector = new int[aig->num_inputs]; - - for(int i=0; inum_inputs; i++) { - input_vector[i] = rand() % 2; - } - for (int i=0; inum_inputs) input_vector[abs(det_v[i]) - 1] = det_v[i] > 0 ? 1 : 0; - } - memset(result, -1, (2 * maxvar + 2) * sizeof(int)); - memset(circuit_res, -1, (maxvar + 1) * sizeof(int)); - - propagate(input_vector, result); - circuit_propagate(input_vector, circuit_res); - if (result[output] != !circuit_res[output >> 1]) { - printf("wrong %d %d %d\n", output, !result[output], circuit_res[output >> 1]); - for (int i = 1; i <= maxvar; i++) { - if (circuit_res[i] == -1) continue; - if (result[i * 2] != circuit_res[i]) printf("%d %d %d\n", i, result[i * 2], circuit_res[i]); - printf("%d %d\n", i, result[i << 1]); - } - return; - } - std::vector> tmp; - for(auto& clas : classes) { - std::vector v0; - std::vector v1; - for(auto &v : clas) { - if(result[v]) v1.push_back(v), sum_pos[v] += 1; - else v0.push_back(v), sum_neg[v] += 1; - } - if(v0.size() > 1) tmp.push_back(v0); - if(v1.size() > 1) tmp.push_back(v1); - } - - classes = tmp; - } - printf("c Number of equivalent classes: %d\n", classes.size()); - // printf("classes: \n"); - // for(auto& clas : classes) { - // int lit = clas[0]; - // printf("[ "); - // for(auto &v : clas) { - // printf("%d ", v); - // } - // printf("] %d %d\n", sum_pos[lit], sum_neg[lit]); - // } - -} - -void Sweep::simulation() { - //printf("c =================================== detect =================================\n"); - seen = new int[maxvar + 1]; - classes.push_back(std::vector()); - for(int i=2; i<=maxvar*2+1; i++) { - classes[0].push_back(i); - } - - random_simulation(); -} \ No newline at end of file diff --git a/hCaD_V2/BUILD.md b/hCaD_V2/BUILD.md deleted file mode 100644 index 8804f3f..0000000 --- a/hCaD_V2/BUILD.md +++ /dev/null @@ -1,104 +0,0 @@ -# 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. For instance in order to use `wine` to execute the binaries -on Linux you might want to look into the `binfmt_misc` module and -registering the appropriate interpreter for `DOSWin`. As second step -you simply tell the `configure` script to use the cross-compiler. - - CXXFLAGS=-static CXX=i686-w64-mingw32-g++ ./configure - -Note the use of '-static', which was necessary for me since by default -`wine` did not find `libstdc++` if dynamically linked. - - diff --git a/hCaD_V2/CONTRIBUTING b/hCaD_V2/CONTRIBUTING deleted file mode 100644 index fbf1cdd..0000000 --- a/hCaD_V2/CONTRIBUTING +++ /dev/null @@ -1,4 +0,0 @@ -At this point we want to keep complete ownership in one hand -to particularly avoid any additional co-authorship claims. -Thus please refrain from generating pull requests. Use the issue -tracker or send email to 'biere@jku.at' instead. diff --git a/hCaD_V2/LICENSE b/hCaD_V2/LICENSE deleted file mode 100644 index 81065ff..0000000 --- a/hCaD_V2/LICENSE +++ /dev/null @@ -1,22 +0,0 @@ -MIT License - -Copyright (c) 2016-2021 Armin Biere, Johannes Kepler University Linz, Austria -Copyright (c) 2020-2021 Mathias Fleury, Johannes Kepler University Linz, Austria - -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/hCaD_V2/README.md b/hCaD_V2/README.md deleted file mode 100644 index 756f3b8..0000000 --- a/hCaD_V2/README.md +++ /dev/null @@ -1,54 +0,0 @@ -[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT) -[![Build Status](https://travis-ci.com/arminbiere/cadical.svg?branch=master)](https://travis-ci.com/arminbiere/cadical) - - -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. - -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/hCaD_V2/VERSION b/hCaD_V2/VERSION deleted file mode 100644 index 347f583..0000000 --- a/hCaD_V2/VERSION +++ /dev/null @@ -1 +0,0 @@ -1.4.1 diff --git a/hCaD_V2/bin/starexec_run_default b/hCaD_V2/bin/starexec_run_default deleted file mode 100644 index d24f815..0000000 --- a/hCaD_V2/bin/starexec_run_default +++ /dev/null @@ -1,2 +0,0 @@ -#!/bin/sh -exec ./cadical --target=0 --walk=false $1 $2/proof.out diff --git a/hCaD_V2/configure b/hCaD_V2/configure deleted file mode 100755 index e761d26..0000000 --- a/hCaD_V2/configure +++ /dev/null @@ -1,494 +0,0 @@ -#!/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 -logging=no -check=no -competition=no -coverage=no -profile=no -contracts=yes -tracing=yes -unlocked=yes -pedantic=no -options="" -quiet=no -m32=no - -#--------------------------------------------------------------------------# - -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 -} - -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 [