diff options
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 | 71 | ||||
-rw-r--r-- | src/options/options_handler.h | 4 | ||||
-rw-r--r-- | src/options/options_template.cpp | 2 | ||||
-rw-r--r-- | src/options/quantifiers_modes.cpp | 6 | ||||
-rw-r--r-- | src/options/quantifiers_modes.h | 4 |
9 files changed, 178 insertions, 27 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 bd5b00728..36144e70e 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -267,7 +267,8 @@ agg \n\ \n\ "; -const std::string OptionsHandler::s_mbqiModeHelp = "\ +const std::string OptionsHandler::s_mbqiModeHelp = + "\ Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\ \n\ default \n\ @@ -277,12 +278,8 @@ default \n\ none \n\ + Disable model-based quantifier instantiation.\n\ \n\ -gen-ev \n\ -+ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\ - model finding paper based on generalizing evaluations.\n\ -\n\ -abs \n\ -+ Use abstract MBQI algorithm (uses disjoint sets). \n\ +trust \n\ ++ Do not instantiate quantified formulas (incomplete technique).\n\ \n\ "; @@ -660,14 +657,11 @@ void OptionsHandler::checkLiteralMatchMode( theory::quantifiers::MbqiMode OptionsHandler::stringToMbqiMode( std::string option, std::string optarg) { - if(optarg == "gen-ev") { - return theory::quantifiers::MBQI_GEN_EVAL; - } else if(optarg == "none") { + if (optarg == "none") + { return theory::quantifiers::MBQI_NONE; } else if(optarg == "default" || optarg == "fmc") { return theory::quantifiers::MBQI_FMC; - } else if(optarg == "abs") { - return theory::quantifiers::MBQI_ABS; } else if(optarg == "trust") { return theory::quantifiers::MBQI_TRUST; } else if(optarg == "help") { @@ -1301,6 +1295,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) { @@ -1632,7 +1670,14 @@ void OptionsHandler::setProduceAssertions(std::string option, bool value) void OptionsHandler::proofEnabledBuild(std::string option, bool value) { -#ifndef CVC4_PROOF +#ifdef CVC4_PROOF + if (value && options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER + && options::bvSatSolver() != theory::bv::SAT_SOLVER_MINISAT) + { + throw OptionException( + "Eager BV proofs only supported when minisat is used"); + } +#else if(value) { std::stringstream ss; ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support"; 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 ; diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 85a9747fe..9650aba7a 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -112,7 +112,7 @@ struct OptionHandler<T, true, true> { if(!success){ throw OptionException(option + ": failed to parse "+ optionarg + - " as an integer of the appropraite type."); + " as an integer of the appropriate type."); } // Depending in the platform unsigned numbers with '-' signs may parse. diff --git a/src/options/quantifiers_modes.cpp b/src/options/quantifiers_modes.cpp index 1814a363d..b08f71c2e 100644 --- a/src/options/quantifiers_modes.cpp +++ b/src/options/quantifiers_modes.cpp @@ -64,18 +64,12 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMod std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) { switch(mode) { - case theory::quantifiers::MBQI_GEN_EVAL: - out << "MBQI_GEN_EVAL"; - break; case theory::quantifiers::MBQI_NONE: out << "MBQI_NONE"; break; case theory::quantifiers::MBQI_FMC: out << "MBQI_FMC"; break; - case theory::quantifiers::MBQI_ABS: - out << "MBQI_ABS"; - break; case theory::quantifiers::MBQI_TRUST: out << "MBQI_TRUST"; break; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 41378d2cd..eea043865 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -53,14 +53,10 @@ enum LiteralMatchMode { }; enum MbqiMode { - /** mbqi from CADE 24 paper */ - MBQI_GEN_EVAL, /** no mbqi */ MBQI_NONE, /** default, mbqi from Section 5.4.2 of AJR thesis */ MBQI_FMC, - /** abstract mbqi algorithm */ - MBQI_ABS, /** mbqi trust (produce no instantiations) */ MBQI_TRUST, }; |