src/theory/options_handlers.h

   1 /*********************                                                        */
   2 /*! \file options_handlers.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Custom handlers and predicates for TheoryEngine options
  13  **
  14  ** Custom handlers and predicates for TheoryEngine options.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__THEORY__OPTIONS_HANDLERS_H
  20 #define __CVC4__THEORY__OPTIONS_HANDLERS_H
  21
  22 #include "expr/metakind.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26
  27 static const std::string theoryOfModeHelp = "\
  28 TheoryOf modes currently supported by the --theoryof-mode option:\n\
  29 \n\
  30 type (default) \n\
  31 + type variables, constants and equalities by type\n\
  32 \n\
  33 term \n\
  34 + type variables as uninterpreted, equalities by the parametric theory\n\
  35 ";
  36
  37 inline TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg, SmtEngine* smt) {
  38   if(optarg == "type") {
  39     return THEORY_OF_TYPE_BASED;
  40   } else if(optarg == "term") {
  41     return THEORY_OF_TERM_BASED;
  42   } else if(optarg == "help") {
  43     puts(theoryOfModeHelp.c_str());
  44     exit(1);
  45   } else {
  46     throw OptionException(std::string("unknown option for --theoryof-mode: `") +
  47                           optarg + "'.  Try --theoryof-mode help.");
  48   }
  49 }
  50
  51 inline void useTheory(std::string option, std::string optarg, SmtEngine* smt) {
  52   if(optarg == "help") {
  53     puts(useTheoryHelp);
  54     exit(1);
  55   }
  56   if(useTheoryValidate(optarg)) {
  57     std::map<std::string, bool> m = options::theoryAlternates();
  58     m[optarg] = true;
  59     options::theoryAlternates.set(m);
  60   } else {
  61     throw OptionException(std::string("unknown option for ") + option + ": `" +
  62                           optarg + "'.  Try --use-theory help.");
  63   }
  64 }
  65
  66 }/* CVC4::theory namespace */
  67 }/* CVC4 namespace */
  68
  69 #endif /* __CVC4__THEORY__OPTIONS_HANDLERS_H */