diff options
author | makaimann <makaim@stanford.edu> | 2018-12-10 08:37:11 -0800 |
---|---|---|
committer | Mathias Preiner <mathias.preiner@gmail.com> | 2018-12-10 08:37:11 -0800 |
commit | e1dc39321cd4ab29b436025badfb05714f5649b3 (patch) | |
tree | c2f02cd7370157fbea51ec6602ad174b149cd850 /src/options | |
parent | 7270b2a800c45fa87ef4cdcad8fc353ccb8cd471 (diff) |
BoolToBV modes (off, ite, all) (#2530)
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/options/bool_to_bv_mode.cpp | 42 | ||||
-rw-r--r-- | src/options/bool_to_bv_mode.h | 57 | ||||
-rw-r--r-- | src/options/bv_options.toml | 17 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 44 | ||||
-rw-r--r-- | src/options/options_handler.h | 4 |
6 files changed, 163 insertions, 3 deletions
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index c711567ab..b86db8d00 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -9,6 +9,8 @@ libcvc4_add_sources( arith_unate_lemma_mode.cpp arith_unate_lemma_mode.h base_handlers.h + bool_to_bv_mode.cpp + bool_to_bv_mode.h bv_bitblast_mode.cpp bv_bitblast_mode.h datatypes_modes.h diff --git a/src/options/bool_to_bv_mode.cpp b/src/options/bool_to_bv_mode.cpp new file mode 100644 index 000000000..670e15419 --- /dev/null +++ b/src/options/bool_to_bv_mode.cpp @@ -0,0 +1,42 @@ +/********************* */ +/*! \file bool_to_bv_mode.cpp +** \verbatim +** Top contributors (to current version): +** Makai Mann +** This file is part of the CVC4 project. +** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS +** in the top-level source directory) and their institutional affiliations. +** All rights reserved. See the file COPYING in the top-level source +** directory for licensing information.\endverbatim +** +** \brief Modes for bool-to-bv preprocessing pass +** +** Modes for bool-to-bv preprocessing pass which tries to lower booleans +** to bit-vectors of width 1 at various levels of aggressiveness. +**/ + +#include "options/bool_to_bv_mode.h" + +#include <iostream> + + +namespace CVC4 +{ + std::ostream& operator<<(std::ostream& out, preprocessing::passes::BoolToBVMode mode) { + switch(mode) { + case preprocessing::passes::BOOL_TO_BV_OFF: + out << "BOOL_TO_BV_OFF"; + break; + case preprocessing::passes::BOOL_TO_BV_ITE: + out << "BOOL_TO_BV_ITE"; + break; + case preprocessing::passes::BOOL_TO_BV_ALL: + out << "BOOL_TO_BV_ALL"; + break; + default: + out << "BoolToBVMode:UNKNOWN![" << unsigned(mode) << "]"; + } + + return out; + } +} // namespace CVC4 diff --git a/src/options/bool_to_bv_mode.h b/src/options/bool_to_bv_mode.h new file mode 100644 index 000000000..f2911c339 --- /dev/null +++ b/src/options/bool_to_bv_mode.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file bool_to_bv_mode.h +** \verbatim +** Top contributors (to current version): +** Makai Mann +** This file is part of the CVC4 project. +** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS +** in the top-level source directory) and their institutional affiliations. +** All rights reserved. See the file COPYING in the top-level source +** directory for licensing information.\endverbatim +** +** \brief Modes for bool-to-bv preprocessing pass +** +** Modes for bool-to-bv preprocessing pass which tries to lower booleans +** to bit-vectors of width 1 at various levels of aggressiveness. +**/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H +#define __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H + +#include <iosfwd> + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/** Enumeration of bool-to-bv modes */ +enum BoolToBVMode +{ + /** + * No bool-to-bv pass + */ + BOOL_TO_BV_OFF, + + /** + * Only lower bools in condition of ITEs + * Tries to give more info to bit-vector solver + * by using bit-vector-ITEs when possible + */ + BOOL_TO_BV_ITE, + + /** + * Lower every bool beneath the top layer to be a + * bit-vector + */ + BOOL_TO_BV_ALL +}; +} +} + +std::ostream& operator<<(std::ostream& out, preprocessing::passes::BoolToBVMode mode); + +} + +#endif /* __CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_MODE_H */ diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 15a9047c7..00290da7d 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -105,11 +105,22 @@ header = "options/bv_options.h" [[option]] name = "boolToBitvector" + smt_name = "bool-to-bv" category = "regular" - long = "bool-to-bv" + long = "bool-to-bv=MODE" + type = "CVC4::preprocessing::passes::BoolToBVMode" + default = "CVC4::preprocessing::passes::BOOL_TO_BV_OFF" + handler = "stringToBoolToBVMode" + includes = ["options/bool_to_bv_mode.h"] + help = "convert booleans to bit-vectors of size 1 at various levels of aggressiveness, see --bool-to-bv=help" + +[[option]] + name = "bitwiseEq" + category = "regular" + long = "bitwise-eq" type = "bool" - default = "false" - help = "convert booleans to bit-vectors of size 1 when possible" + default = "true" + help = "lift equivalence with one-bit bit-vectors to be boolean operations" [[option]] name = "bitvectorDivByZeroConst" diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index a808ecd3c..420396452 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1301,6 +1301,50 @@ theory::bv::BvSlicerMode OptionsHandler::stringToBvSlicerMode( } } +const std::string OptionsHandler::s_boolToBVModeHelp = + "\ +BoolToBV pass modes supported by the --bool-to-bv option:\n\ +\n\ +off (default)\n\ ++ Don't push any booleans to width one bit-vectors\n\ +\n\ +ite\n\ ++ Try to turn ITEs into BITVECTOR_ITE when possible. It can fail per-formula \n\ + if not all sub-formulas can be turned to bit-vectors\n\ +\n\ +all\n\ ++ Force all booleans to be bit-vectors of width one except at the top level.\n\ + Most aggressive mode\n\ +"; + +preprocessing::passes::BoolToBVMode OptionsHandler::stringToBoolToBVMode( + std::string option, std::string optarg) +{ + if (optarg == "off") + { + return preprocessing::passes::BOOL_TO_BV_OFF; + } + else if (optarg == "ite") + { + return preprocessing::passes::BOOL_TO_BV_ITE; + } + else if (optarg == "all") + { + return preprocessing::passes::BOOL_TO_BV_ALL; + } + else if (optarg == "help") + { + puts(s_boolToBVModeHelp.c_str()); + exit(1); + } + else + { + throw OptionException(std::string("unknown option for --bool-to-bv: `") + + optarg + + "'. Try --bool-to-bv=help"); + } +} + void OptionsHandler::setBitblastAig(std::string option, bool arg) { if(arg) { diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 53e317895..f96632696 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -27,6 +27,7 @@ #include "options/arith_propagation_mode.h" #include "options/arith_unate_lemma_mode.h" #include "options/base_handlers.h" +#include "options/bool_to_bv_mode.h" #include "options/bv_bitblast_mode.h" #include "options/datatypes_modes.h" #include "options/decision_mode.h" @@ -137,6 +138,8 @@ public: std::string optarg); theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg); + preprocessing::passes::BoolToBVMode stringToBoolToBVMode(std::string option, + std::string optarg); void setBitblastAig(std::string option, bool arg); theory::bv::SatSolverMode stringToSatSolver(std::string option, @@ -229,6 +232,7 @@ public: static const std::string s_bvSatSolverHelp; static const std::string s_booleanTermConversionModeHelp; static const std::string s_bvSlicerModeHelp; + static const std::string s_boolToBVModeHelp; static const std::string s_cegqiFairModeHelp; static const std::string s_decisionModeHelp; static const std::string s_instFormatHelp ; |