summaryrefslogtreecommitdiff
path: root/src/options
diff options
context:
space:
mode:
Diffstat (limited to 'src/options')
-rw-r--r--src/options/CMakeLists.txt2
-rw-r--r--src/options/bool_to_bv_mode.cpp42
-rw-r--r--src/options/bool_to_bv_mode.h57
-rw-r--r--src/options/bv_options.toml17
-rw-r--r--src/options/options_handler.cpp71
-rw-r--r--src/options/options_handler.h4
-rw-r--r--src/options/options_template.cpp2
-rw-r--r--src/options/quantifiers_modes.cpp6
-rw-r--r--src/options/quantifiers_modes.h4
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,
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback