diff options
author | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-06-10 13:48:45 -0400 |
commit | 5f072a19d299191dbedc4b69c8e0eda694cfa957 (patch) | |
tree | 0ebfc27bd05d06b0cdb2fc0813b7d5649d36aee4 /src/theory/bv/options_handlers.h | |
parent | db51926b5ce806754fc26c81b1b7d3e739fc4fc5 (diff) |
Merging CAV14 paper bit-vector work.
Diffstat (limited to 'src/theory/bv/options_handlers.h')
-rw-r--r-- | src/theory/bv/options_handlers.h | 138 |
1 files changed, 138 insertions, 0 deletions
diff --git a/src/theory/bv/options_handlers.h b/src/theory/bv/options_handlers.h new file mode 100644 index 000000000..bc01d4dc8 --- /dev/null +++ b/src/theory/bv/options_handlers.h @@ -0,0 +1,138 @@ +/********************* */ +/*! \file options_handlers.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Custom handlers and predicates for TheoryBV options + ** + ** Custom handlers and predicates for TheoryBV options. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BV__OPTIONS_HANDLERS_H +#define __CVC4__THEORY__BV__OPTIONS_HANDLERS_H + +#include "theory/bv/bitblast_mode.h" +#include "main/options.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +static const std::string bitblastingModeHelp = "\ +Bit-blasting modes currently supported by the --bitblast option:\n\ +\n\ +lazy (default)\n\ ++ Separate boolean structure and term reasoning betwen the core\n\ + SAT solver and the bv SAT solver\n\ +\n\ +eager\n\ ++ Bitblast eagerly to bv SAT solver\n\ +\n\ +aig\n\ ++ Bitblast eagerly to bv SAT solver by converting to AIG\n\ +"; + +inline BitblastMode stringToBitblastMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "lazy") { + if (!options::bitvectorPropagate.wasSetByUser()) { + options::bitvectorPropagate.set(true); + } + if (!options::bitvectorEqualitySolver.wasSetByUser()) { + options::bitvectorEqualitySolver.set(true); + } + if (!options::bitvectorEqualitySlicer.wasSetByUser()) { + if (options::incrementalSolving()) { + options::bitvectorEqualitySlicer.set(BITVECTOR_SLICER_OFF); + } else { + options::bitvectorEqualitySlicer.set(BITVECTOR_SLICER_AUTO); + } + } + + if (!options::bitvectorInequalitySolver.wasSetByUser()) { + options::bitvectorInequalitySolver.set(true); + } + if (!options::bitvectorAlgebraicSolver.wasSetByUser()) { + options::bitvectorAlgebraicSolver.set(true); + } + return BITBLAST_MODE_LAZY; + } else if(optarg == "eager") { + if (options::produceModels()) { + throw OptionException(std::string("Eager bit-blasting does not currently support model generation. \n\ + Try --bitblast=lazy")); + } + + if (options::incrementalSolving() && + options::incrementalSolving.wasSetByUser()) { + throw OptionException(std::string("Eager bit-blasting does not currently support incremental mode. \n\ + Try --bitblast=lazy")); + } + + if (!options::bitvectorAig.wasSetByUser()) { + options::bitvectorAig.set(true); + } + if (!options::bitvectorAigSimplifications.wasSetByUser()) { + // due to a known bug in abc switching to using drw instead of rw + options::bitvectorAigSimplifications.set("balance;drw"); + } + if (!options::bitvectorToBool.wasSetByUser()) { + options::bitvectorToBool.set(true); + } + + if (!options::bvAbstraction.wasSetByUser() && + !options::skolemizeArguments.wasSetByUser()) { + options::bvAbstraction.set(true); + options::skolemizeArguments.set(true); + } + return BITBLAST_MODE_EAGER; + } else if(optarg == "help") { + puts(bitblastingModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --bitblast: `") + + optarg + "'. Try --bitblast=help."); + } +} + +static const std::string bvSlicerModeHelp = "\ +Bit-vector equality slicer modes supported by the --bv-eq-slicer option:\n\ +\n\ +auto (default)\n\ ++ Turn slicer on if input has only equalities over core symbols\n\ +\n\ +on\n\ ++ Turn slicer on\n\ +\n\ +off\n\ ++ Turn slicer off\n\ +"; + +inline BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + + if(optarg == "auto") { + return BITVECTOR_SLICER_AUTO; + } else if(optarg == "on") { + return BITVECTOR_SLICER_ON; + } else if(optarg == "off") { + return BITVECTOR_SLICER_OFF; + } else if(optarg == "help") { + puts(bitblastingModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --bv-eq-slicer: `") + + optarg + "'. Try --bv-eq-slicer=help."); + } +} + +}/* CVC4::theory::bv namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__BV__OPTIONS_HANDLERS_H */ |