From 2606a2e1db0b7da77f784e0593a8bfe511e635ac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=81ron=20Ricardo=20Perez-Lopez?= Date: Mon, 7 Oct 2024 23:12:32 -0700 Subject: [PATCH 1/4] Support all currently existing bitwuzla options --- bitwuzla/src/bitwuzla_solver.cpp | 218 ++++++++++++++++++++++++++++++- 1 file changed, 215 insertions(+), 3 deletions(-) diff --git a/bitwuzla/src/bitwuzla_solver.cpp b/bitwuzla/src/bitwuzla_solver.cpp index 86d48ae4b..5f4f9b5c9 100644 --- a/bitwuzla/src/bitwuzla_solver.cpp +++ b/bitwuzla/src/bitwuzla_solver.cpp @@ -93,10 +93,17 @@ const std::unordered_set bvbases({ 2, 10, 16 }); void BzlaSolver::set_opt(const std::string option, const std::string value) { - // TODO support more options + // General options if (option == "incremental") { - // Do nothing, Bitwuzla is always incremental. + if (value != "true") + { + throw NotImplementedException("Bitwuzla only supports incremental mode"); + } + } + else if (option == "log-level") + { + options.set(bitwuzla::Option::LOGLEVEL, std::stoul(value)); } else if (option == "produce-models") { @@ -110,10 +117,215 @@ void BzlaSolver::set_opt(const std::string option, const std::string value) { options.set(bitwuzla::Option::PRODUCE_UNSAT_CORES, (value == "true")); } + else if (option == "seed") + { + options.set(bitwuzla::Option::SEED, std::stoull(value)); + } + else if (option == "verbosity") + { + options.set(bitwuzla::Option::VERBOSITY, std::stoull(value)); + } else if (option == "time-limit") { - options.set(bitwuzla::Option::TIME_LIMIT_PER, std::stoi(value) * 1000); + // Bitwuzla expects this in milliseconds, but smt-switch uses seconds. + options.set(bitwuzla::Option::TIME_LIMIT_PER, std::stod(value) * 1000); + } + else if (option == "memory-limit") + { + options.set(bitwuzla::Option::TIME_LIMIT_PER, std::stoull(value)); + } + + // Bitwuzla-specific options + else if (option == "bv-solver") + { + options.set(bitwuzla::Option::BV_SOLVER, value); + } + else if (option == "rewrite-level") + { + options.set(bitwuzla::Option::REWRITE_LEVEL, std::stoull(value)); + } + else if (option == "sat-solver") + { + options.set(bitwuzla::Option::SAT_SOLVER, value); + } + + // Prop engine options + else if (option == "prop-const-bits") + { + options.set(bitwuzla::Option::PROP_CONST_BITS, (value == "true")); + } + else if (option == "prop-infer-ineq-bounds") + { + options.set(bitwuzla::Option::PROP_INFER_INEQ_BOUNDS, (value == "true")); + } + else if (option == "prop-nprops") + { + options.set(bitwuzla::Option::PROP_NPROPS, std::stoull(value)); + } + else if (option == "prop-nupdates") + { + options.set(bitwuzla::Option::PROP_NUPDATES, std::stoull(value)); + } + else if (option == "prop-opt-lt-concat-sext") + { + options.set(bitwuzla::Option::PROP_OPT_LT_CONCAT_SEXT, (value == "true")); + } + else if (option == "prop-path-sel") + { + options.set(bitwuzla::Option::PROP_PATH_SEL, value); + } + else if (option == "prop-prob-random-input") + { + options.set(bitwuzla::Option::PROP_PROB_RANDOM_INPUT, std::stoull(value)); + } + else if (option == "prop-prob-use-inv-value") + { + options.set(bitwuzla::Option::PROP_PROB_USE_INV_VALUE, std::stoull(value)); + } + else if (option == "prop-sext") + { + options.set(bitwuzla::Option::PROP_SEXT, (value == "true")); + } + else if (option == "prop-normalize") + { + options.set(bitwuzla::Option::PROP_NORMALIZE, (value == "true")); + } + + // Abstraction module + else if (option == "abstraction") + { + options.set(bitwuzla::Option::ABSTRACTION, (value == "true")); + } + else if (option == "abstraction-bv-size") + { + options.set(bitwuzla::Option::ABSTRACTION_BV_SIZE, std::stoull(value)); + } + else if (option == "abstraction-eager-refine") + { + options.set(bitwuzla::Option::ABSTRACTION_EAGER_REFINE, (value == "true")); + } + else if (option == "abstraction-value-limit") + { + options.set(bitwuzla::Option::ABSTRACTION_VALUE_LIMIT, std::stoull(value)); + } + else if (option == "abstraction-value-only") + { + options.set(bitwuzla::Option::ABSTRACTION_VALUE_ONLY, (value == "true")); + } + else if (option == "abstraction-assert") + { + options.set(bitwuzla::Option::ABSTRACTION_ASSERT, (value == "true")); + } + else if (option == "abstraction-assert-refs") + { + options.set(bitwuzla::Option::ABSTRACTION_ASSERT_REFS, std::stoull(value)); } + else if (option == "abstraction-initial-lemmas") + { + options.set(bitwuzla::Option::ABSTRACTION_INITIAL_LEMMAS, + (value == "true")); + } + else if (option == "abstraction-inc-bitblast") + { + options.set(bitwuzla::Option::ABSTRACTION_INC_BITBLAST, (value == "true")); + } + else if (option == "abstraction-bv-add") + { + options.set(bitwuzla::Option::ABSTRACTION_BV_ADD, (value == "true")); + } + else if (option == "abstraction-bv-mul") + { + options.set(bitwuzla::Option::ABSTRACTION_BV_MUL, (value == "true")); + } + else if (option == "abstraction-bv-udiv") + { + options.set(bitwuzla::Option::ABSTRACTION_BV_UDIV, (value == "true")); + } + else if (option == "abstraction-bv-urem") + { + options.set(bitwuzla::Option::ABSTRACTION_BV_UREM, (value == "true")); + } + else if (option == "abstraction-equal") + { + options.set(bitwuzla::Option::ABSTRACTION_EQUAL, (value == "true")); + } + else if (option == "abstraction-ite") + { + options.set(bitwuzla::Option::ABSTRACTION_ITE, (value == "true")); + } + + // Preprocessing + else if (option == "preprocess") + { + options.set(bitwuzla::Option::PREPROCESS, (value == "true")); + } + else if (option == "pp-contradicting-ands") + { + options.set(bitwuzla::Option::PP_CONTRADICTING_ANDS, (value == "true")); + } + else if (option == "pp-elim-bv-extracts") + { + options.set(bitwuzla::Option::PP_ELIM_BV_EXTRACTS, (value == "true")); + } + else if (option == "pp-elim-bv-udiv") + { + options.set(bitwuzla::Option::PP_ELIM_BV_UDIV, (value == "true")); + } + else if (option == "pp-embedded-constr") + { + options.set(bitwuzla::Option::PP_EMBEDDED_CONSTR, (value == "true")); + } + else if (option == "pp-flatten-and") + { + options.set(bitwuzla::Option::PP_FLATTEN_AND, (value == "true")); + } + else if (option == "pp-normalize") + { + options.set(bitwuzla::Option::PP_NORMALIZE, (value == "true")); + } + else if (option == "pp-normalize-share-aware") + { + options.set(bitwuzla::Option::PP_NORMALIZE_SHARE_AWARE, (value == "true")); + } + else if (option == "pp-skeleton-preproc") + { + options.set(bitwuzla::Option::PP_SKELETON_PREPROC, (value == "true")); + } + else if (option == "pp-variable-subst") + { + options.set(bitwuzla::Option::PP_VARIABLE_SUBST, (value == "true")); + } + else if (option == "pp-variable-subst-norm-eq") + { + options.set(bitwuzla::Option::PP_VARIABLE_SUBST_NORM_EQ, (value == "true")); + } + else if (option == "pp-variable-subst-norm-diseq") + { + options.set(bitwuzla::Option::PP_VARIABLE_SUBST_NORM_DISEQ, (value == "true")); + } + else if (option == "pp-variable-subst-norm-bv-ineq") + { + options.set(bitwuzla::Option::PP_VARIABLE_SUBST_NORM_BV_INEQ, (value == "true")); + } + + // Debug options + else if (option == "dbg-rw-node-thresh") + { + options.set(bitwuzla::Option::DBG_RW_NODE_THRESH, std::stoull(value)); + } + else if (option == "dbg-pp-node-thresh") + { + options.set(bitwuzla::Option::DBG_PP_NODE_THRESH, std::stoull(value)); + } + else if (option == "dbg-check-model") + { + options.set(bitwuzla::Option::DBG_CHECK_MODEL, (value == "true")); + } + else if (option == "dbg-check-unsat-core") + { + options.set(bitwuzla::Option::DBG_CHECK_UNSAT_CORE, (value == "true")); + } + else { throw SmtException("Bitwuzla backend does not support option: " + option); From d4abf3bf25e149a2ad18ab7027f750cdfb12f44b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=81ron=20Ricardo=20Perez-Lopez?= Date: Wed, 9 Oct 2024 10:52:18 -0700 Subject: [PATCH 2/4] Remove all non-special cases --- bitwuzla/src/bitwuzla_solver.cpp | 225 +------------------------------ 1 file changed, 3 insertions(+), 222 deletions(-) diff --git a/bitwuzla/src/bitwuzla_solver.cpp b/bitwuzla/src/bitwuzla_solver.cpp index 5f4f9b5c9..0740883c0 100644 --- a/bitwuzla/src/bitwuzla_solver.cpp +++ b/bitwuzla/src/bitwuzla_solver.cpp @@ -93,7 +93,6 @@ const std::unordered_set bvbases({ 2, 10, 16 }); void BzlaSolver::set_opt(const std::string option, const std::string value) { - // General options if (option == "incremental") { if (value != "true") @@ -101,235 +100,17 @@ void BzlaSolver::set_opt(const std::string option, const std::string value) throw NotImplementedException("Bitwuzla only supports incremental mode"); } } - else if (option == "log-level") - { - options.set(bitwuzla::Option::LOGLEVEL, std::stoul(value)); - } - else if (option == "produce-models") - { - options.set(bitwuzla::Option::PRODUCE_MODELS, (value == "true")); - } - else if (option == "produce-unsat-assumptions") - { - options.set(bitwuzla::Option::PRODUCE_UNSAT_ASSUMPTIONS, (value == "true")); - } - else if (option == "produce-unsat-cores") - { - options.set(bitwuzla::Option::PRODUCE_UNSAT_CORES, (value == "true")); - } - else if (option == "seed") - { - options.set(bitwuzla::Option::SEED, std::stoull(value)); - } - else if (option == "verbosity") - { - options.set(bitwuzla::Option::VERBOSITY, std::stoull(value)); - } else if (option == "time-limit") { // Bitwuzla expects this in milliseconds, but smt-switch uses seconds. options.set(bitwuzla::Option::TIME_LIMIT_PER, std::stod(value) * 1000); } - else if (option == "memory-limit") - { - options.set(bitwuzla::Option::TIME_LIMIT_PER, std::stoull(value)); - } - - // Bitwuzla-specific options - else if (option == "bv-solver") - { - options.set(bitwuzla::Option::BV_SOLVER, value); - } - else if (option == "rewrite-level") - { - options.set(bitwuzla::Option::REWRITE_LEVEL, std::stoull(value)); - } - else if (option == "sat-solver") - { - options.set(bitwuzla::Option::SAT_SOLVER, value); - } - - // Prop engine options - else if (option == "prop-const-bits") - { - options.set(bitwuzla::Option::PROP_CONST_BITS, (value == "true")); - } - else if (option == "prop-infer-ineq-bounds") - { - options.set(bitwuzla::Option::PROP_INFER_INEQ_BOUNDS, (value == "true")); - } - else if (option == "prop-nprops") - { - options.set(bitwuzla::Option::PROP_NPROPS, std::stoull(value)); - } - else if (option == "prop-nupdates") - { - options.set(bitwuzla::Option::PROP_NUPDATES, std::stoull(value)); - } - else if (option == "prop-opt-lt-concat-sext") - { - options.set(bitwuzla::Option::PROP_OPT_LT_CONCAT_SEXT, (value == "true")); - } - else if (option == "prop-path-sel") - { - options.set(bitwuzla::Option::PROP_PATH_SEL, value); - } - else if (option == "prop-prob-random-input") - { - options.set(bitwuzla::Option::PROP_PROB_RANDOM_INPUT, std::stoull(value)); - } - else if (option == "prop-prob-use-inv-value") - { - options.set(bitwuzla::Option::PROP_PROB_USE_INV_VALUE, std::stoull(value)); - } - else if (option == "prop-sext") - { - options.set(bitwuzla::Option::PROP_SEXT, (value == "true")); - } - else if (option == "prop-normalize") - { - options.set(bitwuzla::Option::PROP_NORMALIZE, (value == "true")); - } - - // Abstraction module - else if (option == "abstraction") - { - options.set(bitwuzla::Option::ABSTRACTION, (value == "true")); - } - else if (option == "abstraction-bv-size") - { - options.set(bitwuzla::Option::ABSTRACTION_BV_SIZE, std::stoull(value)); - } - else if (option == "abstraction-eager-refine") - { - options.set(bitwuzla::Option::ABSTRACTION_EAGER_REFINE, (value == "true")); - } - else if (option == "abstraction-value-limit") - { - options.set(bitwuzla::Option::ABSTRACTION_VALUE_LIMIT, std::stoull(value)); - } - else if (option == "abstraction-value-only") - { - options.set(bitwuzla::Option::ABSTRACTION_VALUE_ONLY, (value == "true")); - } - else if (option == "abstraction-assert") - { - options.set(bitwuzla::Option::ABSTRACTION_ASSERT, (value == "true")); - } - else if (option == "abstraction-assert-refs") - { - options.set(bitwuzla::Option::ABSTRACTION_ASSERT_REFS, std::stoull(value)); - } - else if (option == "abstraction-initial-lemmas") - { - options.set(bitwuzla::Option::ABSTRACTION_INITIAL_LEMMAS, - (value == "true")); - } - else if (option == "abstraction-inc-bitblast") - { - options.set(bitwuzla::Option::ABSTRACTION_INC_BITBLAST, (value == "true")); - } - else if (option == "abstraction-bv-add") - { - options.set(bitwuzla::Option::ABSTRACTION_BV_ADD, (value == "true")); - } - else if (option == "abstraction-bv-mul") - { - options.set(bitwuzla::Option::ABSTRACTION_BV_MUL, (value == "true")); - } - else if (option == "abstraction-bv-udiv") - { - options.set(bitwuzla::Option::ABSTRACTION_BV_UDIV, (value == "true")); - } - else if (option == "abstraction-bv-urem") - { - options.set(bitwuzla::Option::ABSTRACTION_BV_UREM, (value == "true")); - } - else if (option == "abstraction-equal") - { - options.set(bitwuzla::Option::ABSTRACTION_EQUAL, (value == "true")); - } - else if (option == "abstraction-ite") - { - options.set(bitwuzla::Option::ABSTRACTION_ITE, (value == "true")); - } - - // Preprocessing - else if (option == "preprocess") - { - options.set(bitwuzla::Option::PREPROCESS, (value == "true")); - } - else if (option == "pp-contradicting-ands") - { - options.set(bitwuzla::Option::PP_CONTRADICTING_ANDS, (value == "true")); - } - else if (option == "pp-elim-bv-extracts") - { - options.set(bitwuzla::Option::PP_ELIM_BV_EXTRACTS, (value == "true")); - } - else if (option == "pp-elim-bv-udiv") - { - options.set(bitwuzla::Option::PP_ELIM_BV_UDIV, (value == "true")); - } - else if (option == "pp-embedded-constr") - { - options.set(bitwuzla::Option::PP_EMBEDDED_CONSTR, (value == "true")); - } - else if (option == "pp-flatten-and") - { - options.set(bitwuzla::Option::PP_FLATTEN_AND, (value == "true")); - } - else if (option == "pp-normalize") - { - options.set(bitwuzla::Option::PP_NORMALIZE, (value == "true")); - } - else if (option == "pp-normalize-share-aware") - { - options.set(bitwuzla::Option::PP_NORMALIZE_SHARE_AWARE, (value == "true")); - } - else if (option == "pp-skeleton-preproc") - { - options.set(bitwuzla::Option::PP_SKELETON_PREPROC, (value == "true")); - } - else if (option == "pp-variable-subst") - { - options.set(bitwuzla::Option::PP_VARIABLE_SUBST, (value == "true")); - } - else if (option == "pp-variable-subst-norm-eq") - { - options.set(bitwuzla::Option::PP_VARIABLE_SUBST_NORM_EQ, (value == "true")); - } - else if (option == "pp-variable-subst-norm-diseq") - { - options.set(bitwuzla::Option::PP_VARIABLE_SUBST_NORM_DISEQ, (value == "true")); - } - else if (option == "pp-variable-subst-norm-bv-ineq") - { - options.set(bitwuzla::Option::PP_VARIABLE_SUBST_NORM_BV_INEQ, (value == "true")); - } - - // Debug options - else if (option == "dbg-rw-node-thresh") - { - options.set(bitwuzla::Option::DBG_RW_NODE_THRESH, std::stoull(value)); - } - else if (option == "dbg-pp-node-thresh") - { - options.set(bitwuzla::Option::DBG_PP_NODE_THRESH, std::stoull(value)); - } - else if (option == "dbg-check-model") - { - options.set(bitwuzla::Option::DBG_CHECK_MODEL, (value == "true")); - } - else if (option == "dbg-check-unsat-core") - { - options.set(bitwuzla::Option::DBG_CHECK_UNSAT_CORE, (value == "true")); - } - - else + else if (!options.is_valid(option)) { throw SmtException("Bitwuzla backend does not support option: " + option); } + + options.set(option, value); } void BzlaSolver::set_logic(const std::string logic) From 413f734944fa95dd6122180ca0a825de7d78a6aa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=81ron=20Ricardo=20Perez-Lopez?= Date: Wed, 9 Oct 2024 11:06:20 -0700 Subject: [PATCH 3/4] Do not set options twice --- bitwuzla/src/bitwuzla_solver.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/bitwuzla/src/bitwuzla_solver.cpp b/bitwuzla/src/bitwuzla_solver.cpp index 0740883c0..f34a7fa17 100644 --- a/bitwuzla/src/bitwuzla_solver.cpp +++ b/bitwuzla/src/bitwuzla_solver.cpp @@ -109,8 +109,10 @@ void BzlaSolver::set_opt(const std::string option, const std::string value) { throw SmtException("Bitwuzla backend does not support option: " + option); } - - options.set(option, value); + else + { + options.set(option, value); + } } void BzlaSolver::set_logic(const std::string logic) From b98833a5d1780890551d0392adeb36ec76f89d20 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C3=81ron=20Ricardo=20Perez-Lopez?= Date: Wed, 9 Oct 2024 11:41:26 -0700 Subject: [PATCH 4/4] Handle bitwuzla exceptions --- bitwuzla/src/bitwuzla_solver.cpp | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/bitwuzla/src/bitwuzla_solver.cpp b/bitwuzla/src/bitwuzla_solver.cpp index f34a7fa17..7b02fd13d 100644 --- a/bitwuzla/src/bitwuzla_solver.cpp +++ b/bitwuzla/src/bitwuzla_solver.cpp @@ -111,7 +111,19 @@ void BzlaSolver::set_opt(const std::string option, const std::string value) } else { - options.set(option, value); + try + { + options.set(option, value); + } + catch (const bitwuzla::Exception & exception) + { + std::string detail = exception.what(); + // Remove "invalid call to 'bitwuzla::Options::set(...)'" from exception message. + detail.erase(0, detail.find(")")); + detail.erase(0, detail.find(",")); + throw IncorrectUsageException("Bitwuzla backend got bad option " + option + + detail); + } } }