src/smt/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): Clark Barrett
   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 SmtEngine options
  13  **
  14  ** Custom handlers and predicates for SmtEngine options.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__SMT__OPTIONS_HANDLERS_H
  20 #define __CVC4__SMT__OPTIONS_HANDLERS_H
  21
  22 #include "cvc4autoconfig.h"
  23 #include "util/dump.h"
  24 #include "smt/modal_exception.h"
  25 #include "smt/smt_engine.h"
  26 #include "lib/strtok_r.h"
  27
  28 #include <cerrno>
  29 #include <cstring>
  30 #include <sstream>
  31
  32 namespace CVC4 {
  33 namespace smt {
  34
  35 static inline std::string __cvc4_errno_failreason() {
  36 #if HAVE_STRERROR_R
  37 #if STRERROR_R_CHAR_P
  38   if(errno != 0) {
  39     // GNU version of strerror_r: *might* use the given buffer,
  40     // or might not.  It returns a pointer to buf, or not.
  41     char buf[80];
  42     return std::string(strerror_r(errno, buf, sizeof buf));
  43   } else {
  44     return "unknown reason";
  45   }
  46 #else /* STRERROR_R_CHAR_P */
  47   if(errno != 0) {
  48     // XSI version of strerror_r: always uses the given buffer.
  49     // Returns an error code.
  50     char buf[80];
  51     if(strerror_r(errno, buf, sizeof buf) == 0) {
  52       return std::string(buf);
  53     } else {
  54       // some error occurred while getting the error string
  55       return "unknown reason";
  56     }
  57   } else {
  58     return "unknown reason";
  59   }
  60 #endif /* STRERROR_R_CHAR_P */
  61 #else /* HAVE_STRERROR_R */
  62   return "unknown reason";
  63 #endif /* HAVE_STRERROR_R */
  64 }
  65
  66 static const std::string dumpHelp = "\
  67 Dump modes currently supported by the --dump option:\n\
  68 \n\
  69 benchmark\n\
  70 + Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
  71   does not include any declarations or assertions.  Implied by all following\n\
  72   modes.\n\
  73 \n\
  74 declarations\n\
  75 + Dump user declarations.  Implied by all following modes.\n\
  76 \n\
  77 skolems\n\
  78 + Dump internally-created skolem variable declarations.  These can\n\
  79   arise from preprocessing simplifications, existential elimination,\n\
  80   and a number of other things.  Implied by all following modes.\n\
  81 \n\
  82 assertions\n\
  83 + Output the assertions after preprocessing and before clausification.\n\
  84   Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
  85   where PASS is one of the preprocessing passes: definition-expansion\n\
  86   boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\
  87   simplify static-learning ite-removal repeat-simplify\n\
  88   rewrite-apply-to-const theory-preprocessing.\n\
  89   PASS can also be the special value \"everything\", in which case the\n\
  90   assertions are printed before any preprocessing (with\n\
  91   \"assertions:pre-everything\") or after all preprocessing completes\n\
  92   (with \"assertions:post-everything\").\n\
  93 \n\
  94 clauses\n\
  95 + Do all the preprocessing outlined above, and dump the CNF-converted\n\
  96   output\n\
  97 \n\
  98 state\n\
  99 + Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\
 100   Implied by all \"stateful\" modes below and conflicts with all\n\
 101   non-stateful modes below.\n\
 102 \n\
 103 t-conflicts [non-stateful]\n\
 104 + Output correctness queries for all theory conflicts\n\
 105 \n\
 106 missed-t-conflicts [stateful]\n\
 107 + Output completeness queries for theory conflicts\n\
 108 \n\
 109 t-propagations [stateful]\n\
 110 + Output correctness queries for all theory propagations\n\
 111 \n\
 112 missed-t-propagations [stateful]\n\
 113 + Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\
 114 \n\
 115 t-lemmas [non-stateful]\n\
 116 + Output correctness queries for all theory lemmas\n\
 117 \n\
 118 t-explanations [non-stateful]\n\
 119 + Output correctness queries for all theory explanations\n\
 120 \n\
 121 bv-rewrites [non-stateful]\n\
 122 + Output correctness queries for all bitvector rewrites\n\
 123 \n\
 124 theory::fullcheck [non-stateful]\n\
 125 + Output completeness queries for all full-check effort-level theory checks\n\
 126 \n\
 127 Dump modes can be combined with multiple uses of --dump.  Generally you want\n\
 128 one from the assertions category (either assertions or clauses), and\n\
 129 perhaps one or more stateful or non-stateful modes for checking correctness\n\
 130 and completeness of decision procedure implementations.  Stateful modes dump\n\
 131 the contextual assertions made by the core solver (all decisions and\n\
 132 propagations as assertions; that affects the validity of the resulting\n\
 133 correctness and completeness queries, so of course stateful and non-stateful\n\
 134 modes cannot be mixed in the same run.\n\
 135 \n\
 136 The --output-language option controls the language used for dumping, and\n\
 137 this allows you to connect CVC4 to another solver implementation via a UNIX\n\
 138 pipe to perform on-line checking.  The --dump-to option can be used to dump\n\
 139 to a file.\n\
 140 ";
 141
 142 static const std::string simplificationHelp = "\
 143 Simplification modes currently supported by the --simplification option:\n\
 144 \n\
 145 batch (default) \n\
 146 + save up all ASSERTions; run nonclausal simplification and clausal\n\
 147   (MiniSat) propagation for all of them only after reaching a querying command\n\
 148   (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\
 149 \n\
 150 incremental\n\
 151 + run nonclausal simplification and clausal propagation at each ASSERT\n\
 152   (and at CHECKSAT/QUERY/SUBTYPE)\n\
 153 \n\
 154 none\n\
 155 + do not perform nonclausal simplification\n\
 156 ";
 157
 158 inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
 159 #ifdef CVC4_DUMPING
 160   char* optargPtr = strdup(optarg.c_str());
 161   char* tokstr = optargPtr;
 162   char* toksave;
 163   while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) {
 164     tokstr = NULL;
 165     if(!strcmp(optargPtr, "benchmark")) {
 166     } else if(!strcmp(optargPtr, "declarations")) {
 167     } else if(!strcmp(optargPtr, "assertions")) {
 168       Dump.on("assertions:post-everything");
 169     } else if(!strncmp(optargPtr, "assertions:", 11)) {
 170       const char* p = optargPtr + 11;
 171       if(!strncmp(p, "pre-", 4)) {
 172         p += 4;
 173       } else if(!strncmp(p, "post-", 5)) {
 174         p += 5;
 175       } else {
 176         throw OptionException(std::string("don't know how to dump `") +
 177                               optargPtr + "'.  Please consult --dump help.");
 178       }
 179       if(!strcmp(p, "everything")) {
 180       } else if(!strcmp(p, "definition-expansion")) {
 181       } else if(!strcmp(p, "boolean-terms")) {
 182       } else if(!strcmp(p, "constrain-subtypes")) {
 183       } else if(!strcmp(p, "substitution")) {
 184       } else if(!strcmp(p, "strings-pp")) {
 185       } else if(!strcmp(p, "skolem-quant")) {
 186       } else if(!strcmp(p, "simplify")) {
 187       } else if(!strcmp(p, "static-learning")) {
 188       } else if(!strcmp(p, "ite-removal")) {
 189       } else if(!strcmp(p, "repeat-simplify")) {
 190       } else if(!strcmp(p, "rewrite-apply-to-const")) {
 191       } else if(!strcmp(p, "theory-preprocessing")) {
 192       } else if(!strcmp(p, "nonclausal")) {
 193       } else if(!strcmp(p, "theorypp")) {
 194       } else if(!strcmp(p, "itesimp")) {
 195       } else if(!strcmp(p, "unconstrained")) {
 196       } else if(!strcmp(p, "repeatsimp")) {
 197       } else {
 198         throw OptionException(std::string("don't know how to dump `") +
 199                               optargPtr + "'.  Please consult --dump help.");
 200       }
 201       Dump.on("assertions");
 202     } else if(!strcmp(optargPtr, "skolems")) {
 203     } else if(!strcmp(optargPtr, "clauses")) {
 204     } else if(!strcmp(optargPtr, "t-conflicts") ||
 205               !strcmp(optargPtr, "t-lemmas") ||
 206               !strcmp(optargPtr, "t-explanations") ||
 207               !strcmp(optargPtr, "bv-rewrites") ||
 208               !strcmp(optargPtr, "theory::fullcheck")) {
 209       // These are "non-state-dumping" modes.  If state (SAT decisions,
 210       // propagations, etc.) is dumped, it will interfere with the validity
 211       // of these generated queries.
 212       if(Dump.isOn("state")) {
 213         throw OptionException(std::string("dump option `") + optargPtr +
 214                               "' conflicts with a previous, "
 215                               "state-dumping dump option.  You cannot "
 216                               "mix stateful and non-stateful dumping modes; "
 217                               "see --dump help.");
 218       } else {
 219         Dump.on("no-permit-state");
 220       }
 221     } else if(!strcmp(optargPtr, "state") ||
 222               !strcmp(optargPtr, "missed-t-conflicts") ||
 223               !strcmp(optargPtr, "t-propagations") ||
 224               !strcmp(optargPtr, "missed-t-propagations")) {
 225       // These are "state-dumping" modes.  If state (SAT decisions,
 226       // propagations, etc.) is not dumped, it will interfere with the
 227       // validity of these generated queries.
 228       if(Dump.isOn("no-permit-state")) {
 229         throw OptionException(std::string("dump option `") + optargPtr +
 230                               "' conflicts with a previous, "
 231                               "non-state-dumping dump option.  You cannot "
 232                               "mix stateful and non-stateful dumping modes; "
 233                               "see --dump help.");
 234       } else {
 235         Dump.on("state");
 236       }
 237     } else if(!strcmp(optargPtr, "help")) {
 238       puts(dumpHelp.c_str());
 239       exit(1);
 240     } else {
 241       throw OptionException(std::string("unknown option for --dump: `") +
 242                             optargPtr + "'.  Try --dump help.");
 243     }
 244
 245     Dump.on(optargPtr);
 246     Dump.on("benchmark");
 247     if(strcmp(optargPtr, "benchmark")) {
 248       Dump.on("declarations");
 249       if(strcmp(optargPtr, "declarations")) {
 250         Dump.on("skolems");
 251       }
 252     }
 253   }
 254   free(optargPtr);
 255 #else /* CVC4_DUMPING */
 256   throw OptionException("The dumping feature was disabled in this build of CVC4.");
 257 #endif /* CVC4_DUMPING */
 258 }
 259
 260 inline SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
 261   if(optarg == "batch") {
 262     return SIMPLIFICATION_MODE_BATCH;
 263   } else if(optarg == "incremental") {
 264     return SIMPLIFICATION_MODE_INCREMENTAL;
 265   } else if(optarg == "none") {
 266     return SIMPLIFICATION_MODE_NONE;
 267   } else if(optarg == "help") {
 268     puts(simplificationHelp.c_str());
 269     exit(1);
 270   } else {
 271     throw OptionException(std::string("unknown option for --simplification: `") +
 272                           optarg + "'.  Try --simplification help.");
 273   }
 274 }
 275
 276 // ensure we haven't started search yet
 277 inline void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(ModalException) {
 278   if(smt != NULL && smt->d_fullyInited) {
 279     std::stringstream ss;
 280     ss << "cannot change option `" << option << "' after final initialization (i.e., after logic has been set)";
 281     throw ModalException(ss.str());
 282   }
 283 }
 284
 285 // ensure we are a proof-enabled build of CVC4
 286 inline void proofEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
 287 #ifndef CVC4_PROOF
 288   if(value) {
 289     std::stringstream ss;
 290     ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support";
 291     throw OptionException(ss.str());
 292   }
 293 #endif /* CVC4_PROOF */
 294 }
 295
 296 inline void unsatCoresEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
 297   if(value) {
 298     throw UnrecognizedOptionException("CVC4 does not yet have support for unsatisfiable cores");
 299   }
 300 }
 301
 302 // This macro is used for setting :regular-output-channel and :diagnostic-output-channel
 303 // to redirect a stream.  It maintains all attributes set on the stream.
 304 #define __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(__channel_get, __channel_set) \
 305   { \
 306     int dagSetting = expr::ExprDag::getDag(__channel_get); \
 307     size_t exprDepthSetting = expr::ExprSetDepth::getDepth(__channel_get); \
 308     bool printtypesSetting = expr::ExprPrintTypes::getPrintTypes(__channel_get); \
 309     OutputLanguage languageSetting = expr::ExprSetLanguage::getLanguage(__channel_get); \
 310     __channel_set; \
 311     __channel_get << Expr::dag(dagSetting); \
 312     __channel_get << Expr::setdepth(exprDepthSetting); \
 313     __channel_get << Expr::printtypes(printtypesSetting); \
 314     __channel_get << Expr::setlanguage(languageSetting); \
 315   }
 316
 317 inline void dumpToFile(std::string option, std::string optarg, SmtEngine* smt) {
 318 #ifdef CVC4_DUMPING
 319   std::ostream* outStream = NULL;
 320   if(optarg == "") {
 321     throw OptionException(std::string("Bad file name for --dump-to"));
 322   } else if(optarg == "-") {
 323     outStream = &DumpOutC::dump_cout;
 324   } else {
 325     errno = 0;
 326     outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
 327     if(outStream == NULL || !*outStream) {
 328       std::stringstream ss;
 329       ss << "Cannot open dump-to file: `" << optarg << "': " << __cvc4_errno_failreason();
 330       throw OptionException(ss.str());
 331     }
 332   }
 333   __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Dump.getStream(), Dump.setStream(*outStream));
 334 #else /* CVC4_DUMPING */
 335   throw OptionException("The dumping feature was disabled in this build of CVC4.");
 336 #endif /* CVC4_DUMPING */
 337 }
 338
 339 inline void setRegularOutputChannel(std::string option, std::string optarg, SmtEngine* smt) {
 340   std::ostream* outStream = NULL;
 341   if(optarg == "") {
 342     throw OptionException(std::string("Bad file name setting for regular output channel"));
 343   } else if(optarg == "stdout") {
 344     outStream = &std::cout;
 345   } else if(optarg == "stderr") {
 346     outStream = &std::cerr;
 347   } else {
 348     errno = 0;
 349     outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
 350     if(outStream == NULL || !*outStream) {
 351       std::stringstream ss;
 352       ss << "Cannot open regular-output-channel file: `" << optarg << "': " << __cvc4_errno_failreason();
 353       throw OptionException(ss.str());
 354     }
 355   }
 356   __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(*options::err(), options::err.set(outStream));
 357 }
 358
 359 inline void setDiagnosticOutputChannel(std::string option, std::string optarg, SmtEngine* smt) {
 360   std::ostream* outStream = NULL;
 361   if(optarg == "") {
 362     throw OptionException(std::string("Bad file name setting for diagnostic output channel"));
 363   } else if(optarg == "stdout") {
 364     outStream = &std::cout;
 365   } else if(optarg == "stderr") {
 366     outStream = &std::cerr;
 367   } else {
 368     errno = 0;
 369     outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
 370     if(outStream == NULL || !*outStream) {
 371       std::stringstream ss;
 372       ss << "Cannot open diagnostic-output-channel file: `" << optarg << "': " << __cvc4_errno_failreason();
 373       throw OptionException(ss.str());
 374     }
 375   }
 376   __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Debug.getStream(), Debug.setStream(*outStream));
 377   __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Warning.getStream(), Warning.setStream(*outStream));
 378   __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Message.getStream(), Message.setStream(*outStream));
 379   __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Notice.getStream(), Notice.setStream(*outStream));
 380   __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Chat.getStream(), Chat.setStream(*outStream));
 381   __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Trace.getStream(), Trace.setStream(*outStream));
 382   __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(*options::err(), options::err.set(outStream));
 383 }
 384
 385 #undef __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM
 386
 387 inline std::string checkReplayFilename(std::string option, std::string optarg, SmtEngine* smt) {
 388 #ifdef CVC4_REPLAY
 389   if(optarg == "") {
 390     throw OptionException(std::string("Bad file name for --replay"));
 391   } else {
 392     return optarg;
 393   }
 394 #else /* CVC4_REPLAY */
 395   throw OptionException("The replay feature was disabled in this build of CVC4.");
 396 #endif /* CVC4_REPLAY */
 397 }
 398
 399 inline std::ostream* checkReplayLogFilename(std::string option, std::string optarg, SmtEngine* smt) {
 400 #ifdef CVC4_REPLAY
 401   if(optarg == "") {
 402     throw OptionException(std::string("Bad file name for --replay-log"));
 403   } else if(optarg == "-") {
 404     return &std::cout;
 405   } else {
 406     errno = 0;
 407     std::ostream* replayLog = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
 408     if(replayLog == NULL || !*replayLog) {
 409       std::stringstream ss;
 410       ss << "Cannot open replay-log file: `" << optarg << "': " << __cvc4_errno_failreason();
 411       throw OptionException(ss.str());
 412     }
 413     return replayLog;
 414   }
 415 #else /* CVC4_REPLAY */
 416   throw OptionException("The replay feature was disabled in this build of CVC4.");
 417 #endif /* CVC4_REPLAY */
 418 }
 419
 420 // ensure we are a stats-enabled build of CVC4
 421 inline void statsEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
 422 #ifndef CVC4_STATISTICS_ON
 423   if(value) {
 424     std::stringstream ss;
 425     ss << "option `" << option << "' requires a statistics-enabled build of CVC4; this binary was not built with statistics support";
 426     throw OptionException(ss.str());
 427   }
 428 #endif /* CVC4_STATISTICS_ON */
 429 }
 430
 431 }/* CVC4::smt namespace */
 432 }/* CVC4 namespace */
 433
 434 #endif /* __CVC4__SMT__OPTIONS_HANDLERS_H */