From 45029f8fe26c828952c460ab4862ab28d6181484 Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Sat, 6 Jun 2020 16:29:27 +0200 Subject: [PATCH 1/2] SAT Competition 2020 Submission --- LICENSE | 3 +- VERSION | 2 +- configure | 26 +- makefile.in | 6 +- scripts/build-and-test-all-configurations.sh | 17 +- scripts/generate-cubes.sh | 37 + scripts/make-build-header.sh | 2 +- ...ission.sh => prepare-sc2020-submission.sh} | 7 +- src/README.md | 2 +- src/analyze.cpp | 91 +- src/block.cpp | 30 +- src/cadical.cpp | 871 +++++++++++++----- src/cadical.hpp | 195 +++- src/ccadical.cpp | 76 +- src/ccadical.h | 3 + src/checker.cpp | 31 +- src/checker.hpp | 23 +- src/clause.cpp | 16 +- src/clause.hpp | 24 +- src/collect.cpp | 104 ++- src/compact.cpp | 44 +- src/condition.cpp | 31 +- src/config.cpp | 58 +- src/config.hpp | 15 +- src/contract.cpp | 27 + src/contract.hpp | 58 +- src/cover.cpp | 19 +- src/decide.cpp | 7 +- src/decompose.cpp | 17 +- src/deduplicate.cpp | 6 +- src/elim.cpp | 176 ++-- src/extend.cpp | 2 +- src/external.cpp | 159 +++- src/external.hpp | 168 ++-- src/flags.hpp | 19 +- src/gates.cpp | 3 +- src/instantiate.cpp | 4 +- src/internal.cpp | 284 +++--- src/internal.hpp | 270 ++++-- src/ipasir.cpp | 7 + src/ipasir.h | 4 + src/limit.cpp | 50 +- src/limit.hpp | 13 +- src/lookahead.cpp | 430 +++++++++ src/lucky.cpp | 121 ++- src/message.cpp | 6 +- src/message.hpp | 17 +- src/mobical.cpp | 469 ++++++---- src/occs.cpp | 2 +- src/options.cpp | 134 +-- src/options.hpp | 387 ++++---- src/parse.cpp | 223 +++-- src/parse.hpp | 36 +- src/phases.cpp | 25 +- src/phases.hpp | 7 +- src/probe.cpp | 72 +- src/profile.hpp | 5 +- src/propagate.cpp | 11 +- src/random.hpp | 24 +- src/range.hpp | 93 ++ src/reduce.cpp | 31 +- src/rephase.cpp | 10 +- src/report.cpp | 4 +- src/resources.cpp | 139 ++- src/resources.hpp | 7 +- src/restore.cpp | 4 +- src/score.cpp | 8 +- src/solution.cpp | 8 +- src/solver.cpp | 200 +++- src/stats.cpp | 21 +- src/stats.hpp | 1 + src/subsume.cpp | 61 +- src/terminal.hpp | 1 + src/ternary.cpp | 12 +- src/tracer.hpp | 7 +- src/transred.cpp | 14 +- src/util.cpp | 77 +- src/util.hpp | 32 +- src/var.cpp | 8 +- src/var.hpp | 8 +- src/version.cpp | 14 +- src/vivify.cpp | 24 +- src/walk.cpp | 6 +- src/watch.cpp | 46 +- test/api/cipasir.c | 95 ++ test/api/learn.cpp | 58 ++ test/api/run.sh | 5 +- test/icnf/empty.icnf | 1 + test/icnf/false.icnf | 2 + test/icnf/run.sh | 87 ++ test/icnf/two1.icnf | 7 + test/icnf/two2.icnf | 7 + test/icnf/unit1.icnf | 3 + test/icnf/unit2.icnf | 3 + test/makefile | 6 +- test/trace/reg0053.trace | 3 + test/trace/reg0054.trace | 5 + test/trace/reg0055.trace | 14 + test/usage/relaxed-header.cnf | 5 + test/usage/run.sh | 6 + 100 files changed, 4464 insertions(+), 1655 deletions(-) create mode 100755 scripts/generate-cubes.sh rename scripts/{prepare-sr2019-submission.sh => prepare-sc2020-submission.sh} (86%) create mode 100644 src/contract.cpp create mode 100644 src/lookahead.cpp create mode 100644 src/range.hpp create mode 100644 test/api/cipasir.c create mode 100644 test/api/learn.cpp create mode 100644 test/icnf/empty.icnf create mode 100644 test/icnf/false.icnf create mode 100755 test/icnf/run.sh create mode 100644 test/icnf/two1.icnf create mode 100644 test/icnf/two2.icnf create mode 100644 test/icnf/unit1.icnf create mode 100644 test/icnf/unit2.icnf create mode 100644 test/trace/reg0053.trace create mode 100644 test/trace/reg0054.trace create mode 100644 test/trace/reg0055.trace create mode 100644 test/usage/relaxed-header.cnf diff --git a/LICENSE b/LICENSE index 23d808a1..52e39d02 100644 --- a/LICENSE +++ b/LICENSE @@ -1,6 +1,7 @@ MIT License -Copyright (c) 2016-2019 Armin Biere, Johannes Kepler University Linz, Austria +Copyright (c) 2016-2020 Armin Biere, Johannes Kepler University Linz, Austria +Copyright (c) 2020 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 diff --git a/VERSION b/VERSION index 6085e946..6582e891 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -1.2.1 +sc2020 diff --git a/configure b/configure index f1ffa1f3..c45a7b87 100755 --- a/configure +++ b/configure @@ -18,8 +18,11 @@ all=no debug=no logging=no check=no +competition=no coverage=no profile=no +contracts=yes +tracing=yes unlocked=yes pedantic=no options="" @@ -79,7 +82,7 @@ where '