1 files changed, 0 insertions, 160 deletions
diff --git a/src/theory/bv/options_handlers.h b/src/theory/bv/options_handlers.h
deleted file mode 100644
index a7a7101d2..000000000
--- a/src/theory/bv/options_handlers.h
+++ /dev/null
@@ -1,160 +0,0 @@
-/*********************                                                        */
-/*! \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-2014  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 {
-
-inline void abcEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
-#ifndef CVC4_USE_ABC
-  if(value) {
-    std::stringstream ss;
-    ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
-    throw OptionException(ss.str());
-  }
-#endif /* CVC4_USE_ABC */
-}
-
-inline void abcEnabledBuild(std::string option, std::string value, SmtEngine* smt) throw(OptionException) {
-#ifndef CVC4_USE_ABC
-  if(!value.empty()) {
-    std::stringstream ss;
-    ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
-    throw OptionException(ss.str());
-  }
-#endif /* CVC4_USE_ABC */
-}
-
-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\
-";
-
-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::produceModels()) {
-        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::incrementalSolving() &&
-        options::incrementalSolving.wasSetByUser()) {
-      throw OptionException(std::string("Eager bit-blasting does not currently support incremental mode. \n\
-                                         Try --bitblast=lazy"));
-    }
-    
-    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.");
-  }
-}
-
-inline void setBitblastAig(std::string option, bool arg, SmtEngine* smt) throw(OptionException) {
-  if(arg) {
-    if(options::bitblastMode.wasSetByUser()) {
-      if(options::bitblastMode() != BITBLAST_MODE_EAGER) {
-        throw OptionException("bitblast-aig must be used with eager bitblaster");
-      }
-    } else {
-      options::bitblastMode.set(stringToBitblastMode("", "eager", smt));
-    }
-    if(!options::bitvectorAigSimplifications.wasSetByUser()) {
-      options::bitvectorAigSimplifications.set("balance;drw");
-    }
-  }
-}
-
-}/* CVC4::theory::bv namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__BV__OPTIONS_HANDLERS_H */