diff options
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/boolean_terms.cpp | 21 | ||||
| -rw-r--r-- | src/smt/command_list.cpp | 3 | ||||
| -rw-r--r-- | src/smt/logic_exception.h | 2 | ||||
| -rw-r--r-- | src/smt/modal_exception.h | 47 | ||||
| -rw-r--r-- | src/smt/modal_exception.i | 7 | ||||
| -rw-r--r-- | src/smt/options | 164 | ||||
| -rw-r--r-- | src/smt/options_handlers.h | 517 | ||||
| -rw-r--r-- | src/smt/simplification_mode.cpp | 37 | ||||
| -rw-r--r-- | src/smt/simplification_mode.h | 39 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 267 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 34 | ||||
| -rw-r--r-- | src/smt/smt_engine.i | 1 | ||||
| -rw-r--r-- | src/smt/smt_engine_check_proof.cpp | 12 | ||||
| -rw-r--r-- | src/smt/smt_engine_scope.h | 9 | ||||
| -rw-r--r-- | src/smt/smt_options_handler.cpp | 1729 | ||||
| -rw-r--r-- | src/smt/smt_options_handler.h | 198 | ||||
| -rw-r--r-- | src/smt/smt_options_template.cpp | 138 |
17 files changed, 2165 insertions, 1060 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 69dc06e47..f7dfdb410 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -14,21 +14,22 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ - #include "smt/boolean_terms.h" + +#include <algorithm> +#include <map> +#include <set> +#include <stack> +#include <string> + +#include "expr/kind.h" +#include "expr/node_manager_attributes.h" +#include "options/boolean_term_conversion_mode.h" +#include "options/booleans_options.h" #include "smt/smt_engine.h" #include "theory/theory_engine.h" #include "theory/theory_model.h" -#include "theory/booleans/boolean_term_conversion_mode.h" -#include "theory/booleans/options.h" -#include "expr/kind.h" -#include "expr/node_manager_attributes.h" #include "util/ntuple.h" -#include <string> -#include <algorithm> -#include <set> -#include <map> -#include <stack> using namespace std; using namespace CVC4::theory; diff --git a/src/smt/command_list.cpp b/src/smt/command_list.cpp index 18a09e7ed..3e912d338 100644 --- a/src/smt/command_list.cpp +++ b/src/smt/command_list.cpp @@ -17,8 +17,7 @@ // we include both of these to make sure they agree on the typedef #include "smt/command_list.h" #include "smt/smt_engine.h" - -#include "expr/command.h" +#include "smt_util/command.h" namespace CVC4 { namespace smt { diff --git a/src/smt/logic_exception.h b/src/smt/logic_exception.h index 8fda9b9e2..a641f8d21 100644 --- a/src/smt/logic_exception.h +++ b/src/smt/logic_exception.h @@ -22,7 +22,7 @@ #ifndef __CVC4__SMT__LOGIC_EXCEPTION_H #define __CVC4__SMT__LOGIC_EXCEPTION_H -#include "util/exception.h" +#include "base/exception.h" namespace CVC4 { diff --git a/src/smt/modal_exception.h b/src/smt/modal_exception.h deleted file mode 100644 index 11e78ab19..000000000 --- a/src/smt/modal_exception.h +++ /dev/null @@ -1,47 +0,0 @@ -/********************* */ -/*! \file modal_exception.h - ** \verbatim - ** Original author: Morgan Deters - ** 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 An exception that is thrown when an interactive-only - ** feature while CVC4 is being used in a non-interactive setting - ** - ** An exception that is thrown when an interactive-only feature while - ** CVC4 is being used in a non-interactive setting (for example, the - ** "(get-assertions)" command in an SMT-LIBv2 script). - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__SMT__MODAL_EXCEPTION_H -#define __CVC4__SMT__MODAL_EXCEPTION_H - -#include "util/exception.h" - -namespace CVC4 { - -class CVC4_PUBLIC ModalException : public CVC4::Exception { -public: - ModalException() : - Exception("Feature used while operating in " - "incorrect state") { - } - - ModalException(const std::string& msg) : - Exception(msg) { - } - - ModalException(const char* msg) : - Exception(msg) { - } -};/* class ModalException */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__SMT__MODAL_EXCEPTION_H */ diff --git a/src/smt/modal_exception.i b/src/smt/modal_exception.i deleted file mode 100644 index 15b8150cf..000000000 --- a/src/smt/modal_exception.i +++ /dev/null @@ -1,7 +0,0 @@ -%{ -#include "smt/modal_exception.h" -%} - -%ignore CVC4::ModalException::ModalException(const char*); - -%include "smt/modal_exception.h" diff --git a/src/smt/options b/src/smt/options deleted file mode 100644 index 7c725e508..000000000 --- a/src/smt/options +++ /dev/null @@ -1,164 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module SMT "smt/options.h" SMT layer - -common-option - dump --dump=MODE argument :handler CVC4::smt::dumpMode :handler-include "smt/options_handlers.h" - dump preprocessed assertions, etc., see --dump=help -common-option - dump-to --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h" - all dumping goes to FILE (instead of stdout) - -expert-option forceLogic force-logic --force-logic=LOGIC LogicInfo :include "theory/logic_info.h" :handler CVC4::smt::stringToLogicInfo :handler-include "smt/options_handlers.h" :default '""' - set the logic, and override all further user attempts to change it - -option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler CVC4::smt::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "smt/simplification_mode.h" :handler-include "smt/options_handlers.h" - choose simplification mode, see --simplification=help -alias --no-simplification = --simplification=none - turn off all simplification (same as --simplification=none) - -option doStaticLearning static-learning --static-learning bool :default true - use static learning (on by default) - -option expandDefinitions expand-definitions bool :default false - always expand symbol definitions in output -common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h" - support the get-value and get-model commands -option checkModels check-models --check-models bool :link --produce-models --produce-assertions :link-smt produce-models :link-smt produce-assertions :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" - after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions -option dumpModels --dump-models bool :default false :link --produce-models - output models after every SAT/INVALID/UNKNOWN response -option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" - turn on proof generation -option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" :read-write - after UNSAT/VALID, machine-check the generated proof -option dumpProofs --dump-proofs bool :default false :link --proof - output proofs after every UNSAT/VALID response -option dumpInstantiations --dump-instantiations bool :default false - output instantiations of quantified formulas after every UNSAT/VALID response -option dumpSynth --dump-synth bool :read-write :default false - output solution for synthesis conjectures after every UNSAT/VALID response -option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" - turn on unsat core generation -option checkUnsatCores check-unsat-cores --check-unsat-cores bool :link --produce-unsat-cores :link-smt produce-unsat-cores :read-write - after UNSAT/VALID, produce and check an unsat core (expensive) -option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" - output unsat cores after every UNSAT/VALID response - -option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" - support the get-assignment command - -undocumented-option interactiveMode interactive-mode bool :predicate CVC4::smt::beforeSearch CVC4::smt::setProduceAssertions :predicate-include "smt/options_handlers.h" :read-write - deprecated name for produce-assertions -common-option produceAssertions produce-assertions --produce-assertions bool :predicate CVC4::smt::beforeSearch CVC4::smt::setProduceAssertions :predicate-include "smt/options_handlers.h" :read-write - keep an assertions list (enables get-assertions command) - -option doITESimp --ite-simp bool :read-write - turn on ite simplification (Kim (and Somenzi) et al., SAT 2009) - -option doITESimpOnRepeat --on-repeat-ite-simp bool :read-write :default false - do the ite simplification pass again if repeating simplification - -option simplifyWithCareEnabled --simp-with-care bool :default false :read-write - enables simplifyWithCare in ite simplificiation - -option compressItes --simp-ite-compress bool :default false :read-write - enables compressing ites after ite simplification - -option unconstrainedSimp --unconstrained-simp bool :default false :read-write - turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis) - -option repeatSimp --repeat-simp bool :read-write - make multiple passes with nonclausal simplifier - -option zombieHuntThreshold --simp-ite-hunt-zombies uint32_t :default 524288 - post ite compression enables zombie removal while the number of nodes is above this threshold - -option sortInference --sort-inference bool :read-write :default false - calculate sort inference of input problem, convert the input based on monotonic sorts - -common-option incrementalSolving incremental -i --incremental bool :default true - enable incremental solving - -option abstractValues abstract-values --abstract-values bool :default false - in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard -option modelUninterpDtEnum --model-u-dt-enum bool :default false - in models, output uninterpreted sorts as datatype enumerations - -option - regular-output-channel argument :handler CVC4::smt::setRegularOutputChannel :handler-include "smt/options_handlers.h" - set the regular output channel of the solver -option - diagnostic-output-channel argument :handler CVC4::smt::setDiagnosticOutputChannel :handler-include "smt/options_handlers.h" - set the diagnostic output channel of the solver - -common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" :handler CVC4::smt::tlimitHandler :handler-include "smt/options_handlers.h" - enable time limiting (give milliseconds) -common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long" :handler CVC4::smt::tlimitPerHandler :handler-include "smt/options_handlers.h" - enable time limiting per query (give milliseconds) -common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" :handler CVC4::smt::rlimitHandler :handler-include "smt/options_handlers.h" - enable resource limiting (currently, roughly the number of SAT conflicts) -common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" :handler CVC4::smt::rlimitPerHandler :handler-include "smt/options_handlers.h" - enable resource limiting per query -common-option hardLimit hard-limit --hard-limit bool :default false - the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out) -common-option cpuTime cpu-time --cpu-time bool :default false - measures CPU time if set to true and wall time if false (default false) - -# Resource spending options for SPARK -expert-option rewriteStep rewrite-step --rewrite-step unsigned :default 1 - ammount of resources spent for each rewrite step - -expert-option theoryCheckStep theory-check-step --theory-check-step unsigned :default 1 - ammount of resources spent for each theory check call - -expert-option decisionStep decision-step --decision-step unsigned :default 1 - ammount of getNext decision calls in the decision engine - -expert-option bitblastStep bitblast-step --bitblast-step unsigned :default 1 - ammount of resources spent for each bitblast step - -expert-option parseStep parse-step --parse-step unsigned :default 1 - ammount of resources spent for each command/expression parsing - -expert-option lemmaStep lemma-step --lemma-step unsigned :default 1 - ammount of resources spent when adding lemmas - -expert-option restartStep restart-step --restart-step unsigned :default 1 - ammount of resources spent for each theory restart - -expert-option cnfStep cnf-step --cnf-step unsigned :default 1 - ammount of resources spent for each call to cnf conversion - -expert-option preprocessStep preprocess-step --preprocess-step unsigned :default 1 - ammount of resources spent for each preprocessing step in SmtEngine - -expert-option quantifierStep quantifier-step --quantifier-step unsigned :default 1 - ammount of resources spent for quantifier instantiations - -expert-option satConflictStep sat-conflict-step --sat-conflict-step unsigned :default 1 - ammount of resources spent for each sat conflict (main sat solver) - -expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step unsigned :default 1 - ammount of resources spent for each sat conflict (bitvectors) - - -expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false - eliminate function applications, rewriting e.g. f(5) to a new symbol f_5 - -# --replay is currently broken; don't document it for 1.0 -undocumented-option replayFilename --replay=FILE std::string :handler CVC4::smt::checkReplayFilename :handler-include "smt/options_handlers.h" - replay decisions from file -undocumented-option replayLog --replay-log=FILE std::ostream* :handler CVC4::smt::checkReplayLogFilename :handler-include "smt/options_handlers.h" - log decisions and propagations to file -option replayStream ExprStream* - -# portfolio options -option lemmaInputChannel LemmaInputChannel* :default NULL :include "util/lemma_input_channel.h" - The input channel to receive notfication events for new lemmas -option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "util/lemma_output_channel.h" - The output channel to receive notfication events for new lemmas - -option forceNoLimitCpuWhileDump --force-no-limit-cpu-while-dump bool :default false - Force no CPU limit when dumping models and proofs - -endmodule diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h deleted file mode 100644 index eeefd7af0..000000000 --- a/src/smt/options_handlers.h +++ /dev/null @@ -1,517 +0,0 @@ -/********************* */ -/*! \file options_handlers.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Clark Barrett, Liana Hadarean - ** 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 SmtEngine options - ** - ** Custom handlers and predicates for SmtEngine options. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__SMT__OPTIONS_HANDLERS_H -#define __CVC4__SMT__OPTIONS_HANDLERS_H - -#include "cvc4autoconfig.h" -#include "util/configuration_private.h" -#include "util/dump.h" -#include "util/resource_manager.h" -#include "smt/modal_exception.h" -#include "smt/smt_engine.h" -#include "lib/strtok_r.h" - -#include <cerrno> -#include <cstring> -#include <sstream> - -namespace CVC4 { -namespace smt { - -static inline std::string __cvc4_errno_failreason() { -#if HAVE_STRERROR_R -#if STRERROR_R_CHAR_P - if(errno != 0) { - // GNU version of strerror_r: *might* use the given buffer, - // or might not. It returns a pointer to buf, or not. - char buf[80]; - return std::string(strerror_r(errno, buf, sizeof buf)); - } else { - return "unknown reason"; - } -#else /* STRERROR_R_CHAR_P */ - if(errno != 0) { - // XSI version of strerror_r: always uses the given buffer. - // Returns an error code. - char buf[80]; - if(strerror_r(errno, buf, sizeof buf) == 0) { - return std::string(buf); - } else { - // some error occurred while getting the error string - return "unknown reason"; - } - } else { - return "unknown reason"; - } -#endif /* STRERROR_R_CHAR_P */ -#else /* HAVE_STRERROR_R */ - return "unknown reason"; -#endif /* HAVE_STRERROR_R */ -} - -static const std::string dumpHelp = "\ -Dump modes currently supported by the --dump option:\n\ -\n\ -benchmark\n\ -+ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\ - does not include any declarations or assertions. Implied by all following\n\ - modes.\n\ -\n\ -declarations\n\ -+ Dump user declarations. Implied by all following modes.\n\ -\n\ -skolems\n\ -+ Dump internally-created skolem variable declarations. These can\n\ - arise from preprocessing simplifications, existential elimination,\n\ - and a number of other things. Implied by all following modes.\n\ -\n\ -assertions\n\ -+ Output the assertions after preprocessing and before clausification.\n\ - Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\ - where PASS is one of the preprocessing passes: definition-expansion\n\ - boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\ - simplify static-learning ite-removal repeat-simplify\n\ - rewrite-apply-to-const theory-preprocessing.\n\ - PASS can also be the special value \"everything\", in which case the\n\ - assertions are printed before any preprocessing (with\n\ - \"assertions:pre-everything\") or after all preprocessing completes\n\ - (with \"assertions:post-everything\").\n\ -\n\ -clauses\n\ -+ Do all the preprocessing outlined above, and dump the CNF-converted\n\ - output\n\ -\n\ -state\n\ -+ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\ - Implied by all \"stateful\" modes below and conflicts with all\n\ - non-stateful modes below.\n\ -\n\ -t-conflicts [non-stateful]\n\ -+ Output correctness queries for all theory conflicts\n\ -\n\ -missed-t-conflicts [stateful]\n\ -+ Output completeness queries for theory conflicts\n\ -\n\ -t-propagations [stateful]\n\ -+ Output correctness queries for all theory propagations\n\ -\n\ -missed-t-propagations [stateful]\n\ -+ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\ -\n\ -t-lemmas [non-stateful]\n\ -+ Output correctness queries for all theory lemmas\n\ -\n\ -t-explanations [non-stateful]\n\ -+ Output correctness queries for all theory explanations\n\ -\n\ -bv-rewrites [non-stateful]\n\ -+ Output correctness queries for all bitvector rewrites\n\ -\n\ -bv-abstraction [non-stateful]\n\ -+ Output correctness queries for all bv abstraction \n\ -\n\ -bv-algebraic [non-stateful]\n\ -+ Output correctness queries for bv algebraic solver. \n\ -\n\ -theory::fullcheck [non-stateful]\n \ -+ Output completeness queries for all full-check effort-level theory checks\n\ -\n\ -Dump modes can be combined with multiple uses of --dump. Generally you want\n\ -one from the assertions category (either assertions or clauses), and\n\ -perhaps one or more stateful or non-stateful modes for checking correctness\n\ -and completeness of decision procedure implementations. Stateful modes dump\n\ -the contextual assertions made by the core solver (all decisions and\n\ -propagations as assertions; that affects the validity of the resulting\n\ -correctness and completeness queries, so of course stateful and non-stateful\n\ -modes cannot be mixed in the same run.\n\ -\n\ -The --output-language option controls the language used for dumping, and\n\ -this allows you to connect CVC4 to another solver implementation via a UNIX\n\ -pipe to perform on-line checking. The --dump-to option can be used to dump\n\ -to a file.\n\ -"; - -static const std::string simplificationHelp = "\ -Simplification modes currently supported by the --simplification option:\n\ -\n\ -batch (default) \n\ -+ save up all ASSERTions; run nonclausal simplification and clausal\n\ - (MiniSat) propagation for all of them only after reaching a querying command\n\ - (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\ -\n\ -none\n\ -+ do not perform nonclausal simplification\n\ -"; - -inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) { -#ifdef CVC4_DUMPING - char* optargPtr = strdup(optarg.c_str()); - char* tokstr = optargPtr; - char* toksave; - while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) { - tokstr = NULL; - if(!strcmp(optargPtr, "benchmark")) { - } else if(!strcmp(optargPtr, "declarations")) { - } else if(!strcmp(optargPtr, "assertions")) { - Dump.on("assertions:post-everything"); - } else if(!strncmp(optargPtr, "assertions:", 11)) { - const char* p = optargPtr + 11; - if(!strncmp(p, "pre-", 4)) { - p += 4; - } else if(!strncmp(p, "post-", 5)) { - p += 5; - } else { - throw OptionException(std::string("don't know how to dump `") + - optargPtr + "'. Please consult --dump help."); - } - if(!strcmp(p, "everything")) { - } else if(!strcmp(p, "definition-expansion")) { - } else if(!strcmp(p, "boolean-terms")) { - } else if(!strcmp(p, "constrain-subtypes")) { - } else if(!strcmp(p, "substitution")) { - } else if(!strcmp(p, "strings-pp")) { - } else if(!strcmp(p, "skolem-quant")) { - } else if(!strcmp(p, "simplify")) { - } else if(!strcmp(p, "static-learning")) { - } else if(!strcmp(p, "ite-removal")) { - } else if(!strcmp(p, "repeat-simplify")) { - } else if(!strcmp(p, "rewrite-apply-to-const")) { - } else if(!strcmp(p, "theory-preprocessing")) { - } else if(!strcmp(p, "nonclausal")) { - } else if(!strcmp(p, "theorypp")) { - } else if(!strcmp(p, "itesimp")) { - } else if(!strcmp(p, "unconstrained")) { - } else if(!strcmp(p, "repeatsimp")) { - } else { - throw OptionException(std::string("don't know how to dump `") + - optargPtr + "'. Please consult --dump help."); - } - Dump.on("assertions"); - } else if(!strcmp(optargPtr, "skolems")) { - } else if(!strcmp(optargPtr, "clauses")) { - } else if(!strcmp(optargPtr, "t-conflicts") || - !strcmp(optargPtr, "t-lemmas") || - !strcmp(optargPtr, "t-explanations") || - !strcmp(optargPtr, "bv-rewrites") || - !strcmp(optargPtr, "theory::fullcheck")) { - // These are "non-state-dumping" modes. If state (SAT decisions, - // propagations, etc.) is dumped, it will interfere with the validity - // of these generated queries. - if(Dump.isOn("state")) { - throw OptionException(std::string("dump option `") + optargPtr + - "' conflicts with a previous, " - "state-dumping dump option. You cannot " - "mix stateful and non-stateful dumping modes; " - "see --dump help."); - } else { - Dump.on("no-permit-state"); - } - } else if(!strcmp(optargPtr, "state") || - !strcmp(optargPtr, "missed-t-conflicts") || - !strcmp(optargPtr, "t-propagations") || - !strcmp(optargPtr, "missed-t-propagations")) { - // These are "state-dumping" modes. If state (SAT decisions, - // propagations, etc.) is not dumped, it will interfere with the - // validity of these generated queries. - if(Dump.isOn("no-permit-state")) { - throw OptionException(std::string("dump option `") + optargPtr + - "' conflicts with a previous, " - "non-state-dumping dump option. You cannot " - "mix stateful and non-stateful dumping modes; " - "see --dump help."); - } else { - Dump.on("state"); - } - } else if(!strcmp(optargPtr, "help")) { - puts(dumpHelp.c_str()); - exit(1); - } else if(!strcmp(optargPtr, "bv-abstraction")) { - Dump.on("bv-abstraction"); - } else if(!strcmp(optargPtr, "bv-algebraic")) { - Dump.on("bv-algebraic"); - } else { - throw OptionException(std::string("unknown option for --dump: `") + - optargPtr + "'. Try --dump help."); - } - - Dump.on(optargPtr); - Dump.on("benchmark"); - if(strcmp(optargPtr, "benchmark")) { - Dump.on("declarations"); - if(strcmp(optargPtr, "declarations")) { - Dump.on("skolems"); - } - } - } - free(optargPtr); -#else /* CVC4_DUMPING */ - throw OptionException("The dumping feature was disabled in this build of CVC4."); -#endif /* CVC4_DUMPING */ -} - -inline LogicInfo stringToLogicInfo(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - try { - LogicInfo logic(optarg); - if(smt != NULL) { - smt->setLogic(logic); - } - return logic; - } catch(IllegalArgumentException& e) { - throw OptionException(std::string("invalid logic specification for --force-logic: `") + - optarg + "':\n" + e.what()); - } -} - -inline SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "batch") { - return SIMPLIFICATION_MODE_BATCH; - } else if(optarg == "none") { - return SIMPLIFICATION_MODE_NONE; - } else if(optarg == "help") { - puts(simplificationHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --simplification: `") + - optarg + "'. Try --simplification help."); - } -} - -// ensure we haven't started search yet -inline void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(ModalException) { - if(smt != NULL && smt->d_fullyInited) { - std::stringstream ss; - ss << "cannot change option `" << option << "' after final initialization (i.e., after logic has been set)"; - throw ModalException(ss.str()); - } -} - -inline void setProduceAssertions(std::string option, bool value, SmtEngine* smt) throw() { - options::produceAssertions.set(value); - options::interactiveMode.set(value); -} - -// ensure we are a proof-enabled build of CVC4 -inline void proofEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) { -#if !(IS_PROOFS_BUILD) - if(value) { - std::stringstream ss; - ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support"; - throw OptionException(ss.str()); - } -#endif /* IS_PROOFS_BUILD */ -} - -// This macro is used for setting :regular-output-channel and :diagnostic-output-channel -// to redirect a stream. It maintains all attributes set on the stream. -#define __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(__channel_get, __channel_set) \ - { \ - int dagSetting = expr::ExprDag::getDag(__channel_get); \ - size_t exprDepthSetting = expr::ExprSetDepth::getDepth(__channel_get); \ - bool printtypesSetting = expr::ExprPrintTypes::getPrintTypes(__channel_get); \ - OutputLanguage languageSetting = expr::ExprSetLanguage::getLanguage(__channel_get); \ - __channel_set; \ - __channel_get << Expr::dag(dagSetting); \ - __channel_get << Expr::setdepth(exprDepthSetting); \ - __channel_get << Expr::printtypes(printtypesSetting); \ - __channel_get << Expr::setlanguage(languageSetting); \ - } - -inline void dumpToFile(std::string option, std::string optarg, SmtEngine* smt) { -#ifdef CVC4_DUMPING - std::ostream* outStream = NULL; - if(optarg == "") { - throw OptionException(std::string("Bad file name for --dump-to")); - } else if(optarg == "-") { - outStream = &DumpOutC::dump_cout; - } else if(!options::filesystemAccess()) { - throw OptionException(std::string("Filesystem access not permitted")); - } else { - errno = 0; - outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc); - if(outStream == NULL || !*outStream) { - std::stringstream ss; - ss << "Cannot open dump-to file: `" << optarg << "': " << __cvc4_errno_failreason(); - throw OptionException(ss.str()); - } - } - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Dump.getStream(), Dump.setStream(*outStream)); -#else /* CVC4_DUMPING */ - throw OptionException("The dumping feature was disabled in this build of CVC4."); -#endif /* CVC4_DUMPING */ -} - -inline void setRegularOutputChannel(std::string option, std::string optarg, SmtEngine* smt) { - std::ostream* outStream = NULL; - if(optarg == "") { - throw OptionException(std::string("Bad file name setting for regular output channel")); - } else if(optarg == "stdout") { - outStream = &std::cout; - } else if(optarg == "stderr") { - outStream = &std::cerr; - } else if(!options::filesystemAccess()) { - throw OptionException(std::string("Filesystem access not permitted")); - } else { - errno = 0; - outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc); - if(outStream == NULL || !*outStream) { - std::stringstream ss; - ss << "Cannot open regular-output-channel file: `" << optarg << "': " << __cvc4_errno_failreason(); - throw OptionException(ss.str()); - } - } - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(*options::err(), options::err.set(outStream)); -} - -inline void setDiagnosticOutputChannel(std::string option, std::string optarg, SmtEngine* smt) { - std::ostream* outStream = NULL; - if(optarg == "") { - throw OptionException(std::string("Bad file name setting for diagnostic output channel")); - } else if(optarg == "stdout") { - outStream = &std::cout; - } else if(optarg == "stderr") { - outStream = &std::cerr; - } else if(!options::filesystemAccess()) { - throw OptionException(std::string("Filesystem access not permitted")); - } else { - errno = 0; - outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc); - if(outStream == NULL || !*outStream) { - std::stringstream ss; - ss << "Cannot open diagnostic-output-channel file: `" << optarg << "': " << __cvc4_errno_failreason(); - throw OptionException(ss.str()); - } - } - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Debug.getStream(), Debug.setStream(*outStream)); - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Warning.getStream(), Warning.setStream(*outStream)); - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Message.getStream(), Message.setStream(*outStream)); - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Notice.getStream(), Notice.setStream(*outStream)); - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Chat.getStream(), Chat.setStream(*outStream)); - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Trace.getStream(), Trace.setStream(*outStream)); - __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(*options::err(), options::err.set(outStream)); -} - -#undef __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM - -inline std::string checkReplayFilename(std::string option, std::string optarg, SmtEngine* smt) { -#ifdef CVC4_REPLAY - if(optarg == "") { - throw OptionException(std::string("Bad file name for --replay")); - } else { - return optarg; - } -#else /* CVC4_REPLAY */ - throw OptionException("The replay feature was disabled in this build of CVC4."); -#endif /* CVC4_REPLAY */ -} - -inline std::ostream* checkReplayLogFilename(std::string option, std::string optarg, SmtEngine* smt) { -#ifdef CVC4_REPLAY - if(optarg == "") { - throw OptionException(std::string("Bad file name for --replay-log")); - } else if(optarg == "-") { - return &std::cout; - } else if(!options::filesystemAccess()) { - throw OptionException(std::string("Filesystem access not permitted")); - } else { - errno = 0; - std::ostream* replayLog = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc); - if(replayLog == NULL || !*replayLog) { - std::stringstream ss; - ss << "Cannot open replay-log file: `" << optarg << "': " << __cvc4_errno_failreason(); - throw OptionException(ss.str()); - } - return replayLog; - } -#else /* CVC4_REPLAY */ - throw OptionException("The replay feature was disabled in this build of CVC4."); -#endif /* CVC4_REPLAY */ -} - -// ensure we are a stats-enabled build of CVC4 -inline void statsEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) { -#ifndef CVC4_STATISTICS_ON - if(value) { - std::stringstream ss; - ss << "option `" << option << "' requires a statistics-enabled build of CVC4; this binary was not built with statistics support"; - throw OptionException(ss.str()); - } -#endif /* CVC4_STATISTICS_ON */ -} - -inline unsigned long tlimitHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - unsigned long ms; - std::istringstream convert(optarg); - if (!(convert >> ms)) - throw OptionException("option `"+option+"` requires a number as an argument"); - - // make sure the resource is set if the option is updated - // if the smt engine is null the resource will be set in the - if (smt != NULL) { - ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager(); - rm->setTimeLimit(ms, true); - } - return ms; -} - -inline unsigned long tlimitPerHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - unsigned long ms; - - std::istringstream convert(optarg); - if (!(convert >> ms)) - throw OptionException("option `"+option+"` requires a number as an argument"); - - if (smt != NULL) { - ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager(); - rm->setTimeLimit(ms, false); - } - return ms; -} - -inline unsigned long rlimitHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - unsigned long ms; - - std::istringstream convert(optarg); - if (!(convert >> ms)) - throw OptionException("option `"+option+"` requires a number as an argument"); - - if (smt != NULL) { - ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager(); - rm->setResourceLimit(ms, true); - } - return ms; -} - -inline unsigned long rlimitPerHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - unsigned long ms; - - std::istringstream convert(optarg); - if (!(convert >> ms)) - throw OptionException("option `"+option+"` requires a number as an argument"); - - if (smt != NULL) { - ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager(); - rm->setResourceLimit(ms, false); - } - return ms; -} - -}/* CVC4::smt namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__SMT__OPTIONS_HANDLERS_H */ diff --git a/src/smt/simplification_mode.cpp b/src/smt/simplification_mode.cpp deleted file mode 100644 index be46badfc..000000000 --- a/src/smt/simplification_mode.cpp +++ /dev/null @@ -1,37 +0,0 @@ -/********************* */ -/*! \file simplification_mode.cpp - ** \verbatim - ** Original author: Morgan Deters - ** 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "smt/simplification_mode.h" - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, SimplificationMode mode) { - switch(mode) { - case SIMPLIFICATION_MODE_BATCH: - out << "SIMPLIFICATION_MODE_BATCH"; - break; - case SIMPLIFICATION_MODE_NONE: - out << "SIMPLIFICATION_MODE_NONE"; - break; - default: - out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]"; - } - - return out; -} - -}/* CVC4 namespace */ diff --git a/src/smt/simplification_mode.h b/src/smt/simplification_mode.h deleted file mode 100644 index b0b78d318..000000000 --- a/src/smt/simplification_mode.h +++ /dev/null @@ -1,39 +0,0 @@ -/********************* */ -/*! \file simplification_mode.h - ** \verbatim - ** Original author: Morgan Deters - ** 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__SMT__SIMPLIFICATION_MODE_H -#define __CVC4__SMT__SIMPLIFICATION_MODE_H - -#include <iostream> - -namespace CVC4 { - -/** Enumeration of simplification modes (when to simplify). */ -typedef enum { - /** Simplify the assertions all together once a check is requested */ - SIMPLIFICATION_MODE_BATCH, - /** Don't do simplification */ - SIMPLIFICATION_MODE_NONE -} SimplificationMode; - -std::ostream& operator<<(std::ostream& out, SimplificationMode mode) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* __CVC4__SMT__SIMPLIFICATION_MODE_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4136c3163..21d190d0e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -14,86 +14,89 @@ ** The main entry point into the CVC4 library's SMT interface. **/ -#include <vector> -#include <string> +#include "smt/smt_engine.h" + +#include <algorithm> +#include <cctype> +#include <ext/hash_map> #include <iterator> -#include <utility> #include <sstream> #include <stack> -#include <cctype> -#include <algorithm> -#include <ext/hash_map> +#include <string> +#include <utility> +#include <vector> -#include "context/cdlist.h" +#include "options/boolean_term_conversion_mode.h" +#include "options/decision_mode.h" +#include "base/exception.h" +#include "base/modal_exception.h" +#include "options/option_exception.h" +#include "base/output.h" #include "context/cdhashset.h" +#include "context/cdlist.h" #include "context/context.h" #include "decision/decision_engine.h" -#include "decision/decision_mode.h" -#include "decision/options.h" -#include "expr/command.h" +#include "expr/attribute.h" #include "expr/expr.h" #include "expr/kind.h" #include "expr/metakind.h" -#include "expr/node_builder.h" #include "expr/node.h" +#include "expr/node_builder.h" #include "expr/node_self_iterator.h" -#include "expr/attribute.h" -#include "prop/prop_engine.h" -#include "proof/theory_proof.h" -#include "smt/modal_exception.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "smt/model_postprocessor.h" -#include "smt/logic_request.h" -#include "theory/theory_engine.h" -#include "theory/bv/theory_bv_rewriter.h" -#include "proof/proof_manager.h" -#include "main/options.h" -#include "util/unsat_core.h" -#include "util/proof.h" -#include "util/resource_manager.h" +#include "expr/resource_manager.h" +#include "options/arith_options.h" +#include "options/arrays_options.h" +#include "options/booleans_options.h" +#include "options/booleans_options.h" +#include "options/bv_options.h" +#include "options/datatypes_options.h" +#include "options/decision_options.h" +#include "options/main_options.h" +#include "options/options_handler_interface.h" +#include "options/printer_options.h" +#include "options/prop_options.h" +#include "options/quantifiers_options.h" +#include "options/smt_options.h" +#include "options/strings_options.h" +#include "options/theory_options.h" +#include "options/uf_options.h" +#include "printer/printer.h" #include "proof/proof.h" #include "proof/proof_manager.h" -#include "util/boolean_simplification.h" -#include "util/node_visitor.h" -#include "util/configuration.h" -#include "util/configuration_private.h" -#include "util/exception.h" -#include "util/nary_builder.h" -#include "smt/command_list.h" +#include "proof/proof_manager.h" +#include "proof/unsat_core.h" +#include "proof/theory_proof.h" +#include "prop/prop_engine.h" #include "smt/boolean_terms.h" -#include "smt/options.h" -#include "options/option_exception.h" -#include "util/output.h" -#include "util/hash.h" -#include "theory/substitutions.h" -#include "theory/uf/options.h" -#include "theory/arith/options.h" -#include "theory/strings/options.h" -#include "theory/bv/options.h" -#include "theory/theory_traits.h" -#include "theory/logic_info.h" -#include "theory/options.h" +#include "smt/command_list.h" +#include "smt/logic_request.h" +#include "smt/model_postprocessor.h" +#include "smt/smt_engine_scope.h" +#include "smt/smt_options_handler.h" +#include "smt_util/command.h" +#include "smt_util/boolean_simplification.h" +#include "smt_util/ite_removal.h" +#include "smt_util/nary_builder.h" +#include "smt_util/node_visitor.h" +#include "theory/arith/pseudoboolean_proc.h" #include "theory/booleans/circuit_propagator.h" -#include "theory/booleans/boolean_term_conversion_mode.h" -#include "theory/booleans/options.h" -#include "util/ite_removal.h" -#include "theory/theory_model.h" -#include "printer/printer.h" -#include "prop/options.h" -#include "theory/arrays/options.h" -#include "util/sort_inference.h" -#include "theory/quantifiers/macros.h" +#include "theory/bv/bvintropow2.h" +#include "theory/bv/theory_bv_rewriter.h" +#include "theory/logic_info.h" +#include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/fun_def_process.h" +#include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" -#include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/quantifiers/options.h" -#include "theory/datatypes/options.h" +#include "theory/sort_inference.h" #include "theory/strings/theory_strings.h" -#include "printer/options.h" - -#include "theory/arith/pseudoboolean_proc.h" -#include "theory/bv/bvintropow2.h" +#include "theory/substitutions.h" +#include "theory/theory_engine.h" +#include "theory/theory_model.h" +#include "theory/theory_traits.h" +#include "util/configuration.h" +#include "util/configuration_private.h" +#include "util/hash.h" +#include "util/proof.h" using namespace std; using namespace CVC4; @@ -712,6 +715,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_needPostsolve(false), d_earlyTheoryPP(true), d_status(), + d_optionsHandler(new SmtOptionsHandler(this)), d_private(NULL), d_smtAttributes(NULL), d_statisticsRegistry(NULL), @@ -884,6 +888,9 @@ SmtEngine::~SmtEngine() throw() { delete d_statisticsRegistry; d_statisticsRegistry = NULL; + delete d_optionsHandler; + d_optionsHandler = NULL; + delete d_private; d_private = NULL; @@ -934,7 +941,7 @@ void SmtEngine::setLogicInternal() throw() { void SmtEngine::setDefaults() { if(options::forceLogic.wasSetByUser()) { - d_logic = options::forceLogic(); + d_logic = *(options::forceLogic()); } // set strings-exp @@ -1596,6 +1603,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) SmtScope smts(this); Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; + if(Dump.isOn("benchmark")) { if(key == "status") { string s = value.getValue(); @@ -1700,29 +1708,29 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const v.push_back((*i).second); stats.push_back(v); } - return stats; + return SExpr(stats); } else if(key == "error-behavior") { // immediate-exit | continued-execution if( options::continuedExecution() || options::interactive() ) { - return SExpr::Keyword("continued-execution"); + return SExpr(SExpr::Keyword("continued-execution")); } else { - return SExpr::Keyword("immediate-exit"); + return SExpr(SExpr::Keyword("immediate-exit")); } } else if(key == "name") { - return Configuration::getName(); + return SExpr(Configuration::getName()); } else if(key == "version") { - return Configuration::getVersionString(); + return SExpr(Configuration::getVersionString()); } else if(key == "authors") { - return Configuration::about(); + return SExpr(Configuration::about()); } else if(key == "status") { // sat | unsat | unknown switch(d_status.asSatisfiabilityResult().isSat()) { case Result::SAT: - return SExpr::Keyword("sat"); + return SExpr(SExpr::Keyword("sat")); case Result::UNSAT: - return SExpr::Keyword("unsat"); + return SExpr(SExpr::Keyword("unsat")); default: - return SExpr::Keyword("unknown"); + return SExpr(SExpr::Keyword("unknown")); } } else if(key == "reason-unknown") { if(!d_status.isNull() && d_status.isUnknown()) { @@ -1730,7 +1738,7 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const ss << d_status.whyUnknown(); string s = ss.str(); transform(s.begin(), s.end(), s.begin(), ::tolower); - return SExpr::Keyword(s); + return SExpr(SExpr::Keyword(s)); } else { throw ModalException("Can't get-info :reason-unknown when the " "last result wasn't unknown!"); @@ -1739,7 +1747,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const return SExpr(d_userLevels.size()); } else if(key == "all-options") { // get the options, like all-statistics - return Options::current()->getOptions(); + std::vector< std::vector<std::string> > current_options = Options::current()->getOptions(); + return SExpr::parseListOfListOfAtoms(current_options); } else { throw UnrecognizedOptionException(); } @@ -4068,13 +4077,13 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, UnsafeInterruptExce vector<SExpr> v; if((*i).getKind() == kind::APPLY) { Assert((*i).getNumChildren() == 0); - v.push_back(SExpr::Keyword((*i).getOperator().toString())); + v.push_back(SExpr(SExpr::Keyword((*i).getOperator().toString()))); } else { Assert((*i).isVar()); - v.push_back(SExpr::Keyword((*i).toString())); + v.push_back(SExpr(SExpr::Keyword((*i).toString()))); } - v.push_back(SExpr::Keyword(resultNode.toString())); - sexprs.push_back(v); + v.push_back(SExpr(SExpr::Keyword(resultNode.toString()))); + sexprs.push_back(SExpr(v)); } return SExpr(sexprs); } @@ -4669,4 +4678,108 @@ void SmtEngine::setPrintFuncInModel(Expr f, bool p) { } } + + +void SmtEngine::beforeSearch(SmtEngine* smt, const std::string& option) throw(ModalException) { + if(smt != NULL && smt->d_fullyInited) { + std::stringstream ss; + ss << "cannot change option `" << option << "' after final initialization (i.e., after logic has been set)"; + throw ModalException(ss.str()); + } +} + + +void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) + throw(OptionException, ModalException) { + + NodeManagerScope nms(d_nodeManager); + Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; + + if(Dump.isOn("benchmark")) { + Dump("benchmark") << SetOptionCommand(key, value); + } + + if(key == "command-verbosity") { + if(!value.isAtom()) { + const vector<SExpr>& cs = value.getChildren(); + if(cs.size() == 2 && + (cs[0].isKeyword() || cs[0].isString()) && + cs[1].isInteger()) { + string c = cs[0].getValue(); + const Integer& v = cs[1].getIntegerValue(); + if(v < 0 || v > 2) { + throw OptionException("command-verbosity must be 0, 1, or 2"); + } + d_commandVerbosity[c] = v; + return; + } + } + throw OptionException("command-verbosity value must be a tuple (command-name, integer)"); + } + + if(!value.isAtom()) { + throw OptionException("bad value for :" + key); + } + + string optionarg = value.getValue(); + + d_optionsHandler->setOption(key, optionarg); +} + +CVC4::SExpr SmtEngine::getOption(const std::string& key) const + throw(OptionException) { + + NodeManagerScope nms(d_nodeManager); + + Trace("smt") << "SMT getOption(" << key << ")" << endl; + + if(key.length() >= 18 && + key.compare(0, 18, "command-verbosity:") == 0) { + map<string, Integer>::const_iterator i = d_commandVerbosity.find(key.c_str() + 18); + if(i != d_commandVerbosity.end()) { + return SExpr((*i).second); + } + i = d_commandVerbosity.find("*"); + if(i != d_commandVerbosity.end()) { + return SExpr((*i).second); + } + return SExpr(Integer(2)); + } + + if(Dump.isOn("benchmark")) { + Dump("benchmark") << GetOptionCommand(key); + } + + if(key == "command-verbosity") { + vector<SExpr> result; + SExpr defaultVerbosity; + for(map<string, Integer>::const_iterator i = d_commandVerbosity.begin(); + i != d_commandVerbosity.end(); + ++i) { + vector<SExpr> v; + v.push_back(SExpr((*i).first)); + v.push_back(SExpr((*i).second)); + if((*i).first == "*") { + // put the default at the end of the SExpr + defaultVerbosity = SExpr(v); + } else { + result.push_back(SExpr(v)); + } + } + // put the default at the end of the SExpr + if(!defaultVerbosity.isAtom()) { + result.push_back(defaultVerbosity); + } else { + // ensure the default is always listed + vector<SExpr> v; + v.push_back(SExpr("*")); + v.push_back(SExpr(Integer(2))); + result.push_back(SExpr(v)); + } + return SExpr(result); + } + + return SExpr::parseAtom(d_optionsHandler->getOption(key)); +} + }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index be31d768b..c94646c40 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -22,22 +22,22 @@ #include <string> #include <vector> -#include "context/cdlist_forward.h" +#include "base/modal_exception.h" #include "context/cdhashmap_forward.h" #include "context/cdhashset_forward.h" +#include "context/cdlist_forward.h" #include "expr/expr.h" #include "expr/expr_manager.h" -#include "util/proof.h" -#include "util/unsat_core.h" -#include "smt/modal_exception.h" -#include "smt/logic_exception.h" +#include "expr/result.h" +#include "expr/sexpr.h" +#include "expr/statistics.h" #include "options/options.h" -#include "util/result.h" -#include "util/sexpr.h" +#include "proof/unsat_core.h" +#include "smt/logic_exception.h" +#include "theory/logic_info.h" #include "util/hash.h" +#include "util/proof.h" #include "util/unsafe_interrupt_exception.h" -#include "util/statistics.h" -#include "theory/logic_info.h" // In terms of abstraction, this is below (and provides services to) // ValidityChecker and above (and requires the services of) @@ -72,6 +72,10 @@ namespace prop { class PropEngine; }/* CVC4::prop namespace */ +namespace options { + class OptionsHandler; +}/* CVC4::prop namespace */ + namespace expr { namespace attr { class AttributeManager; @@ -93,7 +97,6 @@ namespace smt { class SmtScope; class BooleanTermConverter; - void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException); ProofManager* currentProofManager(); struct CommandCleanup; @@ -264,6 +267,11 @@ class CVC4_PUBLIC SmtEngine { std::map<std::string, Integer> d_commandVerbosity; /** + * This responds to requests to set options. + */ + options::OptionsHandler* d_optionsHandler; + + /** * A private utility class to SmtEngine. */ smt::SmtEnginePrivate* d_private; @@ -354,7 +362,6 @@ class CVC4_PUBLIC SmtEngine { friend class ::CVC4::smt::SmtScope; friend class ::CVC4::smt::BooleanTermConverter; friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*); - friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException); friend ProofManager* ::CVC4::smt::currentProofManager(); friend class ::CVC4::LogicRequest; // to access d_modelCommands @@ -717,6 +724,11 @@ public: */ void setPrintFuncInModel(Expr f, bool p); + + /** + * Throws a ModalException if smt is non-null and the SmtEngine has not been fully initialized. + */ + static void beforeSearch(SmtEngine* smt, const std::string& option) throw(ModalException); };/* class SmtEngine */ }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i index 9cf4467a8..443e4cc58 100644 --- a/src/smt/smt_engine.i +++ b/src/smt/smt_engine.i @@ -46,7 +46,6 @@ SWIGEXPORT void JNICALL Java_edu_nyu_acsys_CVC4_SmtEngine_dlRef(JNIEnv* jenv, jc %ignore CVC4::SmtEngine::setLogic(const char*); %ignore CVC4::stats::getStatisticsRegistry(SmtEngine*); -%ignore CVC4::smt::beforeSearch(std::string, bool, SmtEngine*); %ignore CVC4::smt::currentProofManager(); %include "smt/smt_engine.h" diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index d04daef92..2add88afb 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -15,16 +15,18 @@ ** \todo document this file **/ -#include "smt/smt_engine.h" -#include "util/configuration_private.h" -#include "util/statistics_registry.h" -#include "check.h" +#include <unistd.h> #include <cstdlib> #include <cstring> #include <fstream> #include <string> -#include <unistd.h> + +#include "base/output.h" +#include "check.h" +#include "expr/statistics_registry.h" +#include "smt/smt_engine.h" +#include "util/configuration_private.h" using namespace CVC4; using namespace std; diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index bc978b728..1dd69abc9 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -19,13 +19,14 @@ #pragma once +#include "base/cvc4_assert.h" +#include "base/output.h" +#include "base/tls.h" #include "expr/node_manager.h" +#include "options/smt_options.h" #include "smt/smt_engine.h" -#include "smt/options.h" #include "util/configuration_private.h" -#include "util/cvc4_assert.h" -#include "util/output.h" -#include "util/tls.h" + namespace CVC4 { diff --git a/src/smt/smt_options_handler.cpp b/src/smt/smt_options_handler.cpp new file mode 100644 index 000000000..3dc5720ab --- /dev/null +++ b/src/smt/smt_options_handler.cpp @@ -0,0 +1,1729 @@ +/********************* */ +/*! \file options_handler_interface.cpp + ** \verbatim + ** Original author: Tim King + ** 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 Interface for custom handlers and predicates options. + ** + ** Interface for custom handlers and predicates options. + **/ + +#include "smt/smt_options_handler.h" + +#include <cerrno> +#include <cstring> +#include <ostream> +#include <sstream> +#include <string> + +#include "base/modal_exception.h" +#include "base/output.h" +#include "cvc4autoconfig.h" +#include "expr/metakind.h" +#include "expr/node_manager.h" +#include "expr/resource_manager.h" +#include "lib/strtok_r.h" +#include "options/arith_heuristic_pivot_rule.h" +#include "options/arith_propagation_mode.h" +#include "options/arith_unate_lemma_mode.h" +#include "options/boolean_term_conversion_mode.h" +#include "options/bv_bitblast_mode.h" +#include "options/bv_options.h" +#include "options/decision_mode.h" +#include "options/decision_options.h" +#include "options/didyoumean.h" +#include "options/language.h" +#include "options/main_options.h" +#include "options/option_exception.h" +#include "options/options_handler_interface.h" +#include "options/parser_options.h" +#include "options/printer_modes.h" +#include "options/quantifiers_modes.h" +#include "options/simplification_mode.h" +#include "options/smt_options.h" +#include "options/theory_options.h" +#include "options/theoryof_mode.h" +#include "options/ufss_mode.h" +#include "smt/smt_engine.h" +#include "smt_util/command.h" +#include "smt_util/dump.h" +#include "theory/logic_info.h" +#include "util/configuration.h" +#include "util/configuration_private.h" + + +#warning "TODO: Make SmtOptionsHandler non-public and refactor driver unified." + +namespace CVC4 { +namespace smt { + +SmtOptionsHandler::SmtOptionsHandler(SmtEngine* smt) + : d_smtEngine(smt) +{} + +SmtOptionsHandler::~SmtOptionsHandler(){} + +// theory/arith/options_handlers.h +const std::string SmtOptionsHandler::s_arithUnateLemmasHelp = "\ +Unate lemmas are generated before SAT search begins using the relationship\n\ +of constant terms and polynomials.\n\ +Modes currently supported by the --unate-lemmas option:\n\ ++ none \n\ ++ ineqs \n\ + Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n\ ++ eqs \n\ + Outputs lemmas of the general forms\n\ + (= p c) implies (<= p d) for c < d, or\n\ + (= p c) implies (not (= p d)) for c != d.\n\ ++ all \n\ + A combination of inequalities and equalities.\n\ +"; + +const std::string SmtOptionsHandler::s_arithPropagationModeHelp = "\ +This decides on kind of propagation arithmetic attempts to do during the search.\n\ ++ none\n\ ++ unate\n\ + use constraints to do unate propagation\n\ ++ bi (Bounds Inference)\n\ + infers bounds on basic variables using the upper and lower bounds of the\n\ + non-basic variables in the tableau.\n\ ++both\n\ +"; + +const std::string SmtOptionsHandler::s_errorSelectionRulesHelp = "\ +This decides on the rule used by simplex during heuristic rounds\n\ +for deciding the next basic variable to select.\n\ +Heuristic pivot rules available:\n\ ++min\n\ + The minimum abs() value of the variable's violation of its bound. (default)\n\ ++max\n\ + The maximum violation the bound\n\ ++varord\n\ + The variable order\n\ +"; + +ArithUnateLemmaMode SmtOptionsHandler::stringToArithUnateLemmaMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "all") { + return ALL_PRESOLVE_LEMMAS; + } else if(optarg == "none") { + return NO_PRESOLVE_LEMMAS; + } else if(optarg == "ineqs") { + return INEQUALITY_PRESOLVE_LEMMAS; + } else if(optarg == "eqs") { + return EQUALITY_PRESOLVE_LEMMAS; + } else if(optarg == "help") { + puts(s_arithUnateLemmasHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --unate-lemmas: `") + + optarg + "'. Try --unate-lemmas help."); + } +} + +ArithPropagationMode SmtOptionsHandler::stringToArithPropagationMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "none") { + return NO_PROP; + } else if(optarg == "unate") { + return UNATE_PROP; + } else if(optarg == "bi") { + return BOUND_INFERENCE_PROP; + } else if(optarg == "both") { + return BOTH_PROP; + } else if(optarg == "help") { + puts(s_arithPropagationModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --arith-prop: `") + + optarg + "'. Try --arith-prop help."); + } +} + +ErrorSelectionRule SmtOptionsHandler::stringToErrorSelectionRule(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "min") { + return MINIMUM_AMOUNT; + } else if(optarg == "varord") { + return VAR_ORDER; + } else if(optarg == "max") { + return MAXIMUM_AMOUNT; + } else if(optarg == "help") { + puts(s_errorSelectionRulesHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --heuristic-pivot-rule: `") + + optarg + "'. Try --heuristic-pivot-rule help."); + } +} + +// theory/quantifiers/options_handlers.h + +const std::string SmtOptionsHandler::s_instWhenHelp = "\ +Modes currently supported by the --inst-when option:\n\ +\n\ +full-last-call (default)\n\ ++ Alternate running instantiation rounds at full effort and last\n\ + call. In other words, interleave instantiation and theory combination.\n\ +\n\ +full\n\ ++ Run instantiation round at full effort, before theory combination.\n\ +\n\ +full-delay \n\ ++ Run instantiation round at full effort, before theory combination, after\n\ + all other theories have finished.\n\ +\n\ +full-delay-last-call \n\ ++ Alternate running instantiation rounds at full effort after all other\n\ + theories have finished, and last call. \n\ +\n\ +last-call\n\ ++ Run instantiation at last call effort, after theory combination and\n\ + and theories report sat.\n\ +\n\ +"; + +const std::string SmtOptionsHandler::s_literalMatchHelp = "\ +Literal match modes currently supported by the --literal-match option:\n\ +\n\ +none (default)\n\ ++ Do not use literal matching.\n\ +\n\ +predicate\n\ ++ Consider the phase requirements of predicate literals when applying heuristic\n\ + quantifier instantiation. For example, the trigger P( x ) in the quantified \n\ + formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\ + terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\ + Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\ +\n\ +"; + +const std::string SmtOptionsHandler::s_mbqiModeHelp = "\ +Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\ +\n\ +default \n\ ++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\ + Modulo Theories.\n\ +\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\ +fmc-interval \n\ ++ Same as default, but with intervals for models of integer functions.\n\ +\n\ +abs \n\ ++ Use abstract MBQI algorithm (uses disjoint sets). \n\ +\n\ +"; + +const std::string SmtOptionsHandler::s_qcfWhenModeHelp = "\ +Quantifier conflict find modes currently supported by the --quant-cf-when option:\n\ +\n\ +default \n\ ++ Default, apply conflict finding at full effort.\n\ +\n\ +last-call \n\ ++ Apply conflict finding at last call, after theory combination and \n\ + and all theories report sat. \n\ +\n\ +std \n\ ++ Apply conflict finding at standard effort.\n\ +\n\ +std-h \n\ ++ Apply conflict finding at standard effort when heuristic says to. \n\ +\n\ +"; + +const std::string SmtOptionsHandler::s_qcfModeHelp = "\ +Quantifier conflict find modes currently supported by the --quant-cf option:\n\ +\n\ +prop-eq \n\ ++ Default, apply QCF algorithm to propagate equalities as well as conflicts. \n\ +\n\ +conflict \n\ ++ Apply QCF algorithm to find conflicts only.\n\ +\n\ +partial \n\ ++ Apply QCF algorithm to instantiate heuristically as well. \n\ +\n\ +mc \n\ ++ Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\ +\n\ +"; + +const std::string SmtOptionsHandler::s_userPatModeHelp = "\ +User pattern modes currently supported by the --user-pat option:\n\ +\n\ +trust \n\ ++ When provided, use only user-provided patterns for a quantified formula.\n\ +\n\ +use \n\ ++ Use both user-provided and auto-generated patterns when patterns\n\ + are provided for a quantified formula.\n\ +\n\ +resort \n\ ++ Use user-provided patterns only after auto-generated patterns saturate.\n\ +\n\ +ignore \n\ ++ Ignore user-provided patterns. \n\ +\n\ +interleave \n\ ++ Alternate between use/resort. \n\ +\n\ +"; + +const std::string SmtOptionsHandler::s_triggerSelModeHelp = "\ +Trigger selection modes currently supported by the --trigger-sel option:\n\ +\n\ +default \n\ ++ Default, consider all subterms of quantified formulas for trigger selection.\n\ +\n\ +min \n\ ++ Consider only minimal subterms that meet criteria for triggers.\n\ +\n\ +max \n\ ++ Consider only maximal subterms that meet criteria for triggers. \n\ +\n\ +"; +const std::string SmtOptionsHandler::s_prenexQuantModeHelp = "\ +Prenex quantifiers modes currently supported by the --prenex-quant option:\n\ +\n\ +default \n\ ++ Default, prenex all nested quantifiers except those with user patterns.\n\ +\n\ +all \n\ ++ Prenex all nested quantifiers.\n\ +\n\ +none \n\ ++ Do no prenex nested quantifiers. \n\ +\n\ +"; + +const std::string SmtOptionsHandler::s_cegqiFairModeHelp = "\ +Modes for enforcing fairness for counterexample guided quantifier instantion, supported by --cegqi-fair:\n\ +\n\ +uf-dt-size \n\ ++ Enforce fairness using an uninterpreted function for datatypes size.\n\ +\n\ +default | dt-size \n\ ++ Default, enforce fairness using size theory operator.\n\ +\n\ +dt-height-bound \n\ ++ Enforce fairness by height bound predicate.\n\ +\n\ +none \n\ ++ Do not enforce fairness. \n\ +\n\ +"; + +const std::string SmtOptionsHandler::s_termDbModeHelp = "\ +Modes for term database, supported by --term-db-mode:\n\ +\n\ +all \n\ ++ Quantifiers module considers all ground terms.\n\ +\n\ +relevant \n\ ++ Quantifiers module considers only ground terms connected to current assertions. \n\ +\n\ +"; + +const std::string SmtOptionsHandler::s_iteLiftQuantHelp = "\ +Modes for term database, supported by --ite-lift-quant:\n\ +\n\ +none \n\ ++ Do not lift if-then-else in quantified formulas.\n\ +\n\ +simple \n\ ++ Lift if-then-else in quantified formulas if results in smaller term size.\n\ +\n\ +all \n\ ++ Lift if-then-else in quantified formulas. \n\ +\n\ +"; + +const std::string SmtOptionsHandler::s_sygusInvTemplHelp = "\ +Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\ +\n\ +none \n\ ++ Synthesize invariant directly.\n\ +\n\ +pre \n\ ++ Synthesize invariant based on weakening of precondition .\n\ +\n\ +post \n\ ++ Synthesize invariant based on strengthening of postcondition. \n\ +\n\ +"; + +const std::string SmtOptionsHandler::s_macrosQuantHelp = "\ +Template modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\ +\n\ +all \n\ ++ Infer definitions for functions, including those containing quantified formulas.\n\ +\n\ +ground (default) \n\ ++ Only infer ground definitions for functions.\n\ +\n\ +ground-uf \n\ ++ Only infer ground definitions for functions that result in triggers for all free variables.\n\ +\n\ +"; + +theory::quantifiers::InstWhenMode SmtOptionsHandler::stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "pre-full") { + return theory::quantifiers::INST_WHEN_PRE_FULL; + } else if(optarg == "full") { + return theory::quantifiers::INST_WHEN_FULL; + } else if(optarg == "full-delay") { + return theory::quantifiers::INST_WHEN_FULL_DELAY; + } else if(optarg == "full-last-call") { + return theory::quantifiers::INST_WHEN_FULL_LAST_CALL; + } else if(optarg == "full-delay-last-call") { + return theory::quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL; + } else if(optarg == "last-call") { + return theory::quantifiers::INST_WHEN_LAST_CALL; + } else if(optarg == "help") { + puts(s_instWhenHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --inst-when: `") + + optarg + "'. Try --inst-when help."); + } +} + +void SmtOptionsHandler::checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode) throw(OptionException) { + if(mode == theory::quantifiers::INST_WHEN_PRE_FULL) { + throw OptionException(std::string("Mode pre-full for ") + option + " is not supported in this release."); + } +} + +theory::quantifiers::LiteralMatchMode SmtOptionsHandler::stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "none") { + return theory::quantifiers::LITERAL_MATCH_NONE; + } else if(optarg == "predicate") { + return theory::quantifiers::LITERAL_MATCH_PREDICATE; + } else if(optarg == "equality") { + return theory::quantifiers::LITERAL_MATCH_EQUALITY; + } else if(optarg == "help") { + puts(s_literalMatchHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --literal-matching: `") + + optarg + "'. Try --literal-matching help."); + } +} + +void SmtOptionsHandler::checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException) { + if(mode == theory::quantifiers::LITERAL_MATCH_EQUALITY) { + throw OptionException(std::string("Mode equality for ") + option + " is not supported in this release."); + } +} + +theory::quantifiers::MbqiMode SmtOptionsHandler::stringToMbqiMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "gen-ev") { + return theory::quantifiers::MBQI_GEN_EVAL; + } else if(optarg == "none") { + return theory::quantifiers::MBQI_NONE; + } else if(optarg == "default" || optarg == "fmc") { + return theory::quantifiers::MBQI_FMC; + } else if(optarg == "fmc-interval") { + return theory::quantifiers::MBQI_FMC_INTERVAL; + } else if(optarg == "abs") { + return theory::quantifiers::MBQI_ABS; + } else if(optarg == "trust") { + return theory::quantifiers::MBQI_TRUST; + } else if(optarg == "help") { + puts(s_mbqiModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --mbqi: `") + + optarg + "'. Try --mbqi help."); + } +} + + +void SmtOptionsHandler::checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode) throw(OptionException) {} + + +theory::quantifiers::QcfWhenMode SmtOptionsHandler::stringToQcfWhenMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "default") { + return theory::quantifiers::QCF_WHEN_MODE_DEFAULT; + } else if(optarg == "last-call") { + return theory::quantifiers::QCF_WHEN_MODE_LAST_CALL; + } else if(optarg == "std") { + return theory::quantifiers::QCF_WHEN_MODE_STD; + } else if(optarg == "std-h") { + return theory::quantifiers::QCF_WHEN_MODE_STD_H; + } else if(optarg == "help") { + puts(s_qcfWhenModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --quant-cf-when: `") + + optarg + "'. Try --quant-cf-when help."); + } +} + +theory::quantifiers::QcfMode SmtOptionsHandler::stringToQcfMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "conflict") { + return theory::quantifiers::QCF_CONFLICT_ONLY; + } else if(optarg == "default" || optarg == "prop-eq") { + return theory::quantifiers::QCF_PROP_EQ; + } else if(optarg == "partial") { + return theory::quantifiers::QCF_PARTIAL; + } else if(optarg == "mc" ) { + return theory::quantifiers::QCF_MC; + } else if(optarg == "help") { + puts(s_qcfModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --quant-cf-mode: `") + + optarg + "'. Try --quant-cf-mode help."); + } +} + +theory::quantifiers::UserPatMode SmtOptionsHandler::stringToUserPatMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "use") { + return theory::quantifiers::USER_PAT_MODE_USE; + } else if(optarg == "default" || optarg == "trust") { + return theory::quantifiers::USER_PAT_MODE_TRUST; + } else if(optarg == "resort") { + return theory::quantifiers::USER_PAT_MODE_RESORT; + } else if(optarg == "ignore") { + return theory::quantifiers::USER_PAT_MODE_IGNORE; + } else if(optarg == "interleave") { + return theory::quantifiers::USER_PAT_MODE_INTERLEAVE; + } else if(optarg == "help") { + puts(s_userPatModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --user-pat: `") + + optarg + "'. Try --user-pat help."); + } +} + +theory::quantifiers::TriggerSelMode SmtOptionsHandler::stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "default" || optarg == "all" ) { + return theory::quantifiers::TRIGGER_SEL_DEFAULT; + } else if(optarg == "min") { + return theory::quantifiers::TRIGGER_SEL_MIN; + } else if(optarg == "max") { + return theory::quantifiers::TRIGGER_SEL_MAX; + } else if(optarg == "help") { + puts(s_triggerSelModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --trigger-sel: `") + + optarg + "'. Try --trigger-sel help."); + } +} + + +theory::quantifiers::PrenexQuantMode SmtOptionsHandler::stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "default" ) { + return theory::quantifiers::PRENEX_NO_USER_PAT; + } else if(optarg == "all") { + return theory::quantifiers::PRENEX_ALL; + } else if(optarg == "none") { + return theory::quantifiers::PRENEX_NONE; + } else if(optarg == "help") { + puts(s_prenexQuantModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --prenex-quant: `") + + optarg + "'. Try --prenex-quant help."); + } +} + +theory::quantifiers::CegqiFairMode SmtOptionsHandler::stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "uf-dt-size" ) { + return theory::quantifiers::CEGQI_FAIR_UF_DT_SIZE; + } else if(optarg == "default" || optarg == "dt-size") { + return theory::quantifiers::CEGQI_FAIR_DT_SIZE; + } else if(optarg == "dt-height-bound" ){ + return theory::quantifiers::CEGQI_FAIR_DT_HEIGHT_PRED; + } else if(optarg == "none") { + return theory::quantifiers::CEGQI_FAIR_NONE; + } else if(optarg == "help") { + puts(s_cegqiFairModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --cegqi-fair: `") + + optarg + "'. Try --cegqi-fair help."); + } +} + +theory::quantifiers::TermDbMode SmtOptionsHandler::stringToTermDbMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "all" ) { + return theory::quantifiers::TERM_DB_ALL; + } else if(optarg == "relevant") { + return theory::quantifiers::TERM_DB_RELEVANT; + } else if(optarg == "help") { + puts(s_termDbModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --term-db-mode: `") + + optarg + "'. Try --term-db-mode help."); + } +} + +theory::quantifiers::IteLiftQuantMode SmtOptionsHandler::stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "all" ) { + return theory::quantifiers::ITE_LIFT_QUANT_MODE_ALL; + } else if(optarg == "simple") { + return theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE; + } else if(optarg == "none") { + return theory::quantifiers::ITE_LIFT_QUANT_MODE_NONE; + } else if(optarg == "help") { + puts(s_iteLiftQuantHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --ite-lift-quant: `") + + optarg + "'. Try --ite-lift-quant help."); + } +} + +theory::quantifiers::SygusInvTemplMode SmtOptionsHandler::stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "none" ) { + return theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE; + } else if(optarg == "pre") { + return theory::quantifiers::SYGUS_INV_TEMPL_MODE_PRE; + } else if(optarg == "post") { + return theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST; + } else if(optarg == "help") { + puts(s_sygusInvTemplHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --sygus-inv-templ: `") + + optarg + "'. Try --sygus-inv-templ help."); + } +} + +theory::quantifiers::MacrosQuantMode SmtOptionsHandler::stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "all" ) { + return theory::quantifiers::MACROS_QUANT_MODE_ALL; + } else if(optarg == "ground") { + return theory::quantifiers::MACROS_QUANT_MODE_GROUND; + } else if(optarg == "ground-uf") { + return theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF; + } else if(optarg == "help") { + puts(s_macrosQuantHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --macros-quant-mode: `") + + optarg + "'. Try --macros-quant-mode help."); + } +} + + + +// theory/bv/options_handlers.h +void SmtOptionsHandler::abcEnabledBuild(std::string option, bool value) 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 */ +} + +void SmtOptionsHandler::abcEnabledBuild(std::string option, std::string value) 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 */ +} + +const std::string SmtOptionsHandler::s_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\ +"; + +theory::bv::BitblastMode SmtOptionsHandler::stringToBitblastMode(std::string option, std::string optarg) 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(theory::bv::BITVECTOR_SLICER_OFF); + } else { + options::bitvectorEqualitySlicer.set(theory::bv::BITVECTOR_SLICER_AUTO); + } + } + + if (!options::bitvectorInequalitySolver.wasSetByUser()) { + options::bitvectorInequalitySolver.set(true); + } + if (!options::bitvectorAlgebraicSolver.wasSetByUser()) { + options::bitvectorAlgebraicSolver.set(true); + } + return theory::bv::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 theory::bv::BITBLAST_MODE_EAGER; + } else if(optarg == "help") { + puts(s_bitblastingModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --bitblast: `") + + optarg + "'. Try --bitblast=help."); + } +} + +const std::string SmtOptionsHandler::s_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\ +"; + +theory::bv::BvSlicerMode SmtOptionsHandler::stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "auto") { + return theory::bv::BITVECTOR_SLICER_AUTO; + } else if(optarg == "on") { + return theory::bv::BITVECTOR_SLICER_ON; + } else if(optarg == "off") { + return theory::bv::BITVECTOR_SLICER_OFF; + } else if(optarg == "help") { + puts(s_bitblastingModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --bv-eq-slicer: `") + + optarg + "'. Try --bv-eq-slicer=help."); + } +} + +void SmtOptionsHandler::setBitblastAig(std::string option, bool arg) throw(OptionException) { + if(arg) { + if(options::bitblastMode.wasSetByUser()) { + if(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER) { + throw OptionException("bitblast-aig must be used with eager bitblaster"); + } + } else { + theory::bv::BitblastMode mode = stringToBitblastMode("", "eager"); + options::bitblastMode.set(mode); + } + if(!options::bitvectorAigSimplifications.wasSetByUser()) { + options::bitvectorAigSimplifications.set("balance;drw"); + } + } +} + + +// theory/booleans/options_handlers.h +const std::string SmtOptionsHandler::s_booleanTermConversionModeHelp = "\ +Boolean term conversion modes currently supported by the\n\ +--boolean-term-conversion-mode option:\n\ +\n\ +bitvectors [default]\n\ ++ Boolean terms are converted to bitvectors of size 1.\n\ +\n\ +datatypes\n\ ++ Boolean terms are converted to enumerations in the Datatype theory.\n\ +\n\ +native\n\ ++ Boolean terms are converted in a \"natural\" way depending on where they\n\ + are used. If in a datatype context, they are converted to an enumeration.\n\ + Elsewhere, they are converted to a bitvector of size 1.\n\ +"; + +theory::booleans::BooleanTermConversionMode SmtOptionsHandler::stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException){ + if(optarg == "bitvectors") { + return theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS; + } else if(optarg == "datatypes") { + return theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES; + } else if(optarg == "native") { + return theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE; + } else if(optarg == "help") { + puts(s_booleanTermConversionModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --boolean-term-conversion-mode: `") + + optarg + "'. Try --boolean-term-conversion-mode help."); + } +} + +// theory/uf/options_handlers.h +const std::string SmtOptionsHandler::s_ufssModeHelp = "\ +UF strong solver options currently supported by the --uf-ss option:\n\ +\n\ +full \n\ ++ Default, use uf strong solver to find minimal models for uninterpreted sorts.\n\ +\n\ +no-minimal \n\ ++ Use uf strong solver to shrink model sizes, but do no enforce minimality.\n\ +\n\ +none \n\ ++ Do not use uf strong solver to shrink model sizes. \n\ +\n\ +"; + +theory::uf::UfssMode SmtOptionsHandler::stringToUfssMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "default" || optarg == "full" ) { + return theory::uf::UF_SS_FULL; + } else if(optarg == "no-minimal") { + return theory::uf::UF_SS_NO_MINIMAL; + } else if(optarg == "none") { + return theory::uf::UF_SS_NONE; + } else if(optarg == "help") { + puts(s_ufssModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --uf-ss: `") + + optarg + "'. Try --uf-ss help."); + } +} + + + +// theory/options_handlers.h +const std::string SmtOptionsHandler::s_theoryOfModeHelp = "\ +TheoryOf modes currently supported by the --theoryof-mode option:\n\ +\n\ +type (default) \n\ ++ type variables, constants and equalities by type\n\ +\n\ +term \n\ ++ type variables as uninterpreted, equalities by the parametric theory\n\ +"; + +theory::TheoryOfMode SmtOptionsHandler::stringToTheoryOfMode(std::string option, std::string optarg) { + if(optarg == "type") { + return theory::THEORY_OF_TYPE_BASED; + } else if(optarg == "term") { + return theory::THEORY_OF_TERM_BASED; + } else if(optarg == "help") { + puts(s_theoryOfModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --theoryof-mode: `") + + optarg + "'. Try --theoryof-mode help."); + } +} + +void SmtOptionsHandler::useTheory(std::string option, std::string optarg) { + if(optarg == "help") { + puts(theory::useTheoryHelp); + exit(1); + } + if(theory::useTheoryValidate(optarg)) { + std::map<std::string, bool> m = options::theoryAlternates(); + m[optarg] = true; + options::theoryAlternates.set(m); + } else { + throw OptionException(std::string("unknown option for ") + option + ": `" + + optarg + "'. Try --use-theory help."); + } +} + + + +// printer/options_handlers.h +const std::string SmtOptionsHandler::s_modelFormatHelp = "\ +Model format modes currently supported by the --model-format option:\n\ +\n\ +default \n\ ++ Print model as expressions in the output language format.\n\ +\n\ +table\n\ ++ Print functional expressions over finite domains in a table format.\n\ +"; + +const std::string SmtOptionsHandler::s_instFormatHelp = "\ +Inst format modes currently supported by the --model-format option:\n\ +\n\ +default \n\ ++ Print instantiations as a list in the output language format.\n\ +\n\ +szs\n\ ++ Print instantiations as SZS compliant proof.\n\ +"; + +ModelFormatMode SmtOptionsHandler::stringToModelFormatMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "default") { + return MODEL_FORMAT_MODE_DEFAULT; + } else if(optarg == "table") { + return MODEL_FORMAT_MODE_TABLE; + } else if(optarg == "help") { + puts(s_modelFormatHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --model-format: `") + + optarg + "'. Try --model-format help."); + } +} + +InstFormatMode SmtOptionsHandler::stringToInstFormatMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "default") { + return INST_FORMAT_MODE_DEFAULT; + } else if(optarg == "szs") { + return INST_FORMAT_MODE_SZS; + } else if(optarg == "help") { + puts(s_instFormatHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --inst-format: `") + + optarg + "'. Try --inst-format help."); + } +} + + + +// decision/options_handlers.h +const std::string SmtOptionsHandler::s_decisionModeHelp = "\ +Decision modes currently supported by the --decision option:\n\ +\n\ +internal (default)\n\ ++ Use the internal decision heuristics of the SAT solver\n\ +\n\ +justification\n\ ++ An ATGP-inspired justification heuristic\n\ +\n\ +justification-stoponly\n\ ++ Use the justification heuristic only to stop early, not for decisions\n\ +"; + +decision::DecisionMode SmtOptionsHandler::stringToDecisionMode(std::string option, std::string optarg) throw(OptionException) { + options::decisionStopOnly.set(false); + + if(optarg == "internal") { + return decision::DECISION_STRATEGY_INTERNAL; + } else if(optarg == "justification") { + return decision::DECISION_STRATEGY_JUSTIFICATION; + } else if(optarg == "justification-stoponly") { + options::decisionStopOnly.set(true); + return decision::DECISION_STRATEGY_JUSTIFICATION; + } else if(optarg == "help") { + puts(s_decisionModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --decision: `") + + optarg + "'. Try --decision help."); + } +} + +decision::DecisionWeightInternal SmtOptionsHandler::stringToDecisionWeightInternal(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "off") + return decision::DECISION_WEIGHT_INTERNAL_OFF; + else if(optarg == "max") + return decision::DECISION_WEIGHT_INTERNAL_MAX; + else if(optarg == "sum") + return decision::DECISION_WEIGHT_INTERNAL_SUM; + else if(optarg == "usr1") + return decision::DECISION_WEIGHT_INTERNAL_USR1; + else + throw OptionException(std::string("--decision-weight-internal must be off, max or sum.")); +} + + + +// smt/options_handlers.h +const std::string SmtOptionsHandler::SmtOptionsHandler::s_dumpHelp = "\ +Dump modes currently supported by the --dump option:\n\ +\n\ +benchmark\n\ ++ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\ + does not include any declarations or assertions. Implied by all following\n\ + modes.\n\ +\n\ +declarations\n\ ++ Dump user declarations. Implied by all following modes.\n\ +\n\ +skolems\n\ ++ Dump internally-created skolem variable declarations. These can\n\ + arise from preprocessing simplifications, existential elimination,\n\ + and a number of other things. Implied by all following modes.\n\ +\n\ +assertions\n\ ++ Output the assertions after preprocessing and before clausification.\n\ + Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\ + where PASS is one of the preprocessing passes: definition-expansion\n\ + boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\ + simplify static-learning ite-removal repeat-simplify\n\ + rewrite-apply-to-const theory-preprocessing.\n\ + PASS can also be the special value \"everything\", in which case the\n\ + assertions are printed before any preprocessing (with\n\ + \"assertions:pre-everything\") or after all preprocessing completes\n\ + (with \"assertions:post-everything\").\n\ +\n\ +clauses\n\ ++ Do all the preprocessing outlined above, and dump the CNF-converted\n\ + output\n\ +\n\ +state\n\ ++ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\ + Implied by all \"stateful\" modes below and conflicts with all\n\ + non-stateful modes below.\n\ +\n\ +t-conflicts [non-stateful]\n\ ++ Output correctness queries for all theory conflicts\n\ +\n\ +missed-t-conflicts [stateful]\n\ ++ Output completeness queries for theory conflicts\n\ +\n\ +t-propagations [stateful]\n\ ++ Output correctness queries for all theory propagations\n\ +\n\ +missed-t-propagations [stateful]\n\ ++ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\ +\n\ +t-lemmas [non-stateful]\n\ ++ Output correctness queries for all theory lemmas\n\ +\n\ +t-explanations [non-stateful]\n\ ++ Output correctness queries for all theory explanations\n\ +\n\ +bv-rewrites [non-stateful]\n\ ++ Output correctness queries for all bitvector rewrites\n\ +\n\ +bv-abstraction [non-stateful]\n\ ++ Output correctness queries for all bv abstraction \n\ +\n\ +bv-algebraic [non-stateful]\n\ ++ Output correctness queries for bv algebraic solver. \n\ +\n\ +theory::fullcheck [non-stateful]\n \ ++ Output completeness queries for all full-check effort-level theory checks\n\ +\n\ +Dump modes can be combined with multiple uses of --dump. Generally you want\n\ +one from the assertions category (either assertions or clauses), and\n\ +perhaps one or more stateful or non-stateful modes for checking correctness\n\ +and completeness of decision procedure implementations. Stateful modes dump\n\ +the contextual assertions made by the core solver (all decisions and\n\ +propagations as assertions; that affects the validity of the resulting\n\ +correctness and completeness queries, so of course stateful and non-stateful\n\ +modes cannot be mixed in the same run.\n\ +\n\ +The --output-language option controls the language used for dumping, and\n\ +this allows you to connect CVC4 to another solver implementation via a UNIX\n\ +pipe to perform on-line checking. The --dump-to option can be used to dump\n\ +to a file.\n\ +"; + +const std::string SmtOptionsHandler::s_simplificationHelp = "\ +Simplification modes currently supported by the --simplification option:\n\ +\n\ +batch (default) \n\ ++ save up all ASSERTions; run nonclausal simplification and clausal\n\ + (MiniSat) propagation for all of them only after reaching a querying command\n\ + (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\ +\n\ +none\n\ ++ do not perform nonclausal simplification\n\ +"; + +void SmtOptionsHandler::dumpMode(std::string option, std::string optarg) { +#ifdef CVC4_DUMPING + char* optargPtr = strdup(optarg.c_str()); + char* tokstr = optargPtr; + char* toksave; + while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) { + tokstr = NULL; + if(!strcmp(optargPtr, "benchmark")) { + } else if(!strcmp(optargPtr, "declarations")) { + } else if(!strcmp(optargPtr, "assertions")) { + Dump.on("assertions:post-everything"); + } else if(!strncmp(optargPtr, "assertions:", 11)) { + const char* p = optargPtr + 11; + if(!strncmp(p, "pre-", 4)) { + p += 4; + } else if(!strncmp(p, "post-", 5)) { + p += 5; + } else { + throw OptionException(std::string("don't know how to dump `") + + optargPtr + "'. Please consult --dump help."); + } + if(!strcmp(p, "everything")) { + } else if(!strcmp(p, "definition-expansion")) { + } else if(!strcmp(p, "boolean-terms")) { + } else if(!strcmp(p, "constrain-subtypes")) { + } else if(!strcmp(p, "substitution")) { + } else if(!strcmp(p, "strings-pp")) { + } else if(!strcmp(p, "skolem-quant")) { + } else if(!strcmp(p, "simplify")) { + } else if(!strcmp(p, "static-learning")) { + } else if(!strcmp(p, "ite-removal")) { + } else if(!strcmp(p, "repeat-simplify")) { + } else if(!strcmp(p, "rewrite-apply-to-const")) { + } else if(!strcmp(p, "theory-preprocessing")) { + } else if(!strcmp(p, "nonclausal")) { + } else if(!strcmp(p, "theorypp")) { + } else if(!strcmp(p, "itesimp")) { + } else if(!strcmp(p, "unconstrained")) { + } else if(!strcmp(p, "repeatsimp")) { + } else { + throw OptionException(std::string("don't know how to dump `") + + optargPtr + "'. Please consult --dump help."); + } + Dump.on("assertions"); + } else if(!strcmp(optargPtr, "skolems")) { + } else if(!strcmp(optargPtr, "clauses")) { + } else if(!strcmp(optargPtr, "t-conflicts") || + !strcmp(optargPtr, "t-lemmas") || + !strcmp(optargPtr, "t-explanations") || + !strcmp(optargPtr, "bv-rewrites") || + !strcmp(optargPtr, "theory::fullcheck")) { + // These are "non-state-dumping" modes. If state (SAT decisions, + // propagations, etc.) is dumped, it will interfere with the validity + // of these generated queries. + if(Dump.isOn("state")) { + throw OptionException(std::string("dump option `") + optargPtr + + "' conflicts with a previous, " + "state-dumping dump option. You cannot " + "mix stateful and non-stateful dumping modes; " + "see --dump help."); + } else { + Dump.on("no-permit-state"); + } + } else if(!strcmp(optargPtr, "state") || + !strcmp(optargPtr, "missed-t-conflicts") || + !strcmp(optargPtr, "t-propagations") || + !strcmp(optargPtr, "missed-t-propagations")) { + // These are "state-dumping" modes. If state (SAT decisions, + // propagations, etc.) is not dumped, it will interfere with the + // validity of these generated queries. + if(Dump.isOn("no-permit-state")) { + throw OptionException(std::string("dump option `") + optargPtr + + "' conflicts with a previous, " + "non-state-dumping dump option. You cannot " + "mix stateful and non-stateful dumping modes; " + "see --dump help."); + } else { + Dump.on("state"); + } + } else if(!strcmp(optargPtr, "help")) { + puts(s_dumpHelp.c_str()); + exit(1); + } else if(!strcmp(optargPtr, "bv-abstraction")) { + Dump.on("bv-abstraction"); + } else if(!strcmp(optargPtr, "bv-algebraic")) { + Dump.on("bv-algebraic"); + } else { + throw OptionException(std::string("unknown option for --dump: `") + + optargPtr + "'. Try --dump help."); + } + + Dump.on(optargPtr); + Dump.on("benchmark"); + if(strcmp(optargPtr, "benchmark")) { + Dump.on("declarations"); + if(strcmp(optargPtr, "declarations")) { + Dump.on("skolems"); + } + } + } + free(optargPtr); +#else /* CVC4_DUMPING */ + throw OptionException("The dumping feature was disabled in this build of CVC4."); +#endif /* CVC4_DUMPING */ +} + +LogicInfo* SmtOptionsHandler::stringToLogicInfo(std::string option, std::string optarg) throw(OptionException) { + try { +#warning "TODO: Fix the blatant memory leak here." + LogicInfo* logic = new LogicInfo(optarg); + if(d_smtEngine != NULL) { + d_smtEngine->setLogic(*logic); + } + return logic; + } catch(IllegalArgumentException& e) { + throw OptionException(std::string("invalid logic specification for --force-logic: `") + + optarg + "':\n" + e.what()); + } +} + +SimplificationMode SmtOptionsHandler::stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "batch") { + return SIMPLIFICATION_MODE_BATCH; + } else if(optarg == "none") { + return SIMPLIFICATION_MODE_NONE; + } else if(optarg == "help") { + puts(s_simplificationHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --simplification: `") + + optarg + "'. Try --simplification help."); + } +} + + +void SmtOptionsHandler::beforeSearch(std::string option, bool value) throw(ModalException) { + SmtEngine::beforeSearch(d_smtEngine, option); +} + +void SmtOptionsHandler::setProduceAssertions(std::string option, bool value) throw() { + options::produceAssertions.set(value); + options::interactiveMode.set(value); +} + + +void SmtOptionsHandler::proofEnabledBuild(std::string option, bool value) throw(OptionException) { +#if !(IS_PROOFS_BUILD) + if(value) { + std::stringstream ss; + ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support"; + throw OptionException(ss.str()); + } +#endif /* IS_PROOFS_BUILD */ +} + + +// This macro is used for setting :regular-output-channel and :diagnostic-output-channel +// to redirect a stream. It maintains all attributes set on the stream. +#define __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(__channel_get, __channel_set) \ + { \ + int dagSetting = expr::ExprDag::getDag(__channel_get); \ + size_t exprDepthSetting = expr::ExprSetDepth::getDepth(__channel_get); \ + bool printtypesSetting = expr::ExprPrintTypes::getPrintTypes(__channel_get); \ + OutputLanguage languageSetting = expr::ExprSetLanguage::getLanguage(__channel_get); \ + __channel_set; \ + __channel_get << Expr::dag(dagSetting); \ + __channel_get << Expr::setdepth(exprDepthSetting); \ + __channel_get << Expr::printtypes(printtypesSetting); \ + __channel_get << Expr::setlanguage(languageSetting); \ + } + +void SmtOptionsHandler::dumpToFile(std::string option, std::string optarg) { +#ifdef CVC4_DUMPING + std::ostream* outStream = NULL; + if(optarg == "") { + throw OptionException(std::string("Bad file name for --dump-to")); + } else if(optarg == "-") { + outStream = &DumpOutC::dump_cout; + } else if(!options::filesystemAccess()) { + throw OptionException(std::string("Filesystem access not permitted")); + } else { + errno = 0; + outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc); + if(outStream == NULL || !*outStream) { + std::stringstream ss; + ss << "Cannot open dump-to file: `" << optarg << "': " << __cvc4_errno_failreason(); + throw OptionException(ss.str()); + } + } + __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Dump.getStream(), Dump.setStream(*outStream)); +#else /* CVC4_DUMPING */ + throw OptionException("The dumping feature was disabled in this build of CVC4."); +#endif /* CVC4_DUMPING */ +} + +void SmtOptionsHandler::setRegularOutputChannel(std::string option, std::string optarg) { + std::ostream* outStream = NULL; + if(optarg == "") { + throw OptionException(std::string("Bad file name setting for regular output channel")); + } else if(optarg == "stdout") { + outStream = &std::cout; + } else if(optarg == "stderr") { + outStream = &std::cerr; + } else if(!options::filesystemAccess()) { + throw OptionException(std::string("Filesystem access not permitted")); + } else { + errno = 0; + outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc); + if(outStream == NULL || !*outStream) { + std::stringstream ss; + ss << "Cannot open regular-output-channel file: `" << optarg << "': " << __cvc4_errno_failreason(); + throw OptionException(ss.str()); + } + } + __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(*options::err(), options::err.set(outStream)); +} + +void SmtOptionsHandler::setDiagnosticOutputChannel(std::string option, std::string optarg) { + std::ostream* outStream = NULL; + if(optarg == "") { + throw OptionException(std::string("Bad file name setting for diagnostic output channel")); + } else if(optarg == "stdout") { + outStream = &std::cout; + } else if(optarg == "stderr") { + outStream = &std::cerr; + } else if(!options::filesystemAccess()) { + throw OptionException(std::string("Filesystem access not permitted")); + } else { + errno = 0; + outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc); + if(outStream == NULL || !*outStream) { + std::stringstream ss; + ss << "Cannot open diagnostic-output-channel file: `" << optarg << "': " << __cvc4_errno_failreason(); + throw OptionException(ss.str()); + } + } + __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Debug.getStream(), Debug.setStream(*outStream)); + __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Warning.getStream(), Warning.setStream(*outStream)); + __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Message.getStream(), Message.setStream(*outStream)); + __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Notice.getStream(), Notice.setStream(*outStream)); + __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Chat.getStream(), Chat.setStream(*outStream)); + __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Trace.getStream(), Trace.setStream(*outStream)); + __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(*options::err(), options::err.set(outStream)); +} + +#undef __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM + + + +std::string SmtOptionsHandler::checkReplayFilename(std::string option, std::string optarg) { +#ifdef CVC4_REPLAY + if(optarg == "") { + throw OptionException(std::string("Bad file name for --replay")); + } else { + return optarg; + } +#else /* CVC4_REPLAY */ + throw OptionException("The replay feature was disabled in this build of CVC4."); +#endif /* CVC4_REPLAY */ +} + +std::ostream* SmtOptionsHandler::checkReplayLogFilename(std::string option, std::string optarg) { +#ifdef CVC4_REPLAY + if(optarg == "") { + throw OptionException(std::string("Bad file name for --replay-log")); + } else if(optarg == "-") { + return &std::cout; + } else if(!options::filesystemAccess()) { + throw OptionException(std::string("Filesystem access not permitted")); + } else { + errno = 0; + std::ostream* replayLog = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc); + if(replayLog == NULL || !*replayLog) { + std::stringstream ss; + ss << "Cannot open replay-log file: `" << optarg << "': " << __cvc4_errno_failreason(); + throw OptionException(ss.str()); + } + return replayLog; + } +#else /* CVC4_REPLAY */ + throw OptionException("The replay feature was disabled in this build of CVC4."); +#endif /* CVC4_REPLAY */ +} + +void SmtOptionsHandler::statsEnabledBuild(std::string option, bool value) throw(OptionException) { +#ifndef CVC4_STATISTICS_ON + if(value) { + std::stringstream ss; + ss << "option `" << option << "' requires a statistics-enabled build of CVC4; this binary was not built with statistics support"; + throw OptionException(ss.str()); + } +#endif /* CVC4_STATISTICS_ON */ +} + +unsigned long SmtOptionsHandler::tlimitHandler(std::string option, std::string optarg) throw(OptionException) { + unsigned long ms; + std::istringstream convert(optarg); + if (!(convert >> ms)) { + throw OptionException("option `"+option+"` requires a number as an argument"); + } + + // make sure the resource is set if the option is updated + // if the smt engine is null the resource will be set in the + if (d_smtEngine != NULL) { + ResourceManager* rm = NodeManager::fromExprManager(d_smtEngine->getExprManager())->getResourceManager(); + rm->setTimeLimit(ms, true); + } + return ms; +} + +unsigned long SmtOptionsHandler::tlimitPerHandler(std::string option, std::string optarg) throw(OptionException) { + unsigned long ms; + + std::istringstream convert(optarg); + if (!(convert >> ms)) { + throw OptionException("option `"+option+"` requires a number as an argument"); + } + + if (d_smtEngine != NULL) { + ResourceManager* rm = NodeManager::fromExprManager(d_smtEngine->getExprManager())->getResourceManager(); + rm->setTimeLimit(ms, false); + } + return ms; +} + +unsigned long SmtOptionsHandler::rlimitHandler(std::string option, std::string optarg) throw(OptionException) { + unsigned long ms; + + std::istringstream convert(optarg); + if (!(convert >> ms)) { + throw OptionException("option `"+option+"` requires a number as an argument"); + } + + if (d_smtEngine != NULL) { + ResourceManager* rm = NodeManager::fromExprManager(d_smtEngine->getExprManager())->getResourceManager(); + rm->setResourceLimit(ms, true); + } + return ms; +} + +unsigned long SmtOptionsHandler::rlimitPerHandler(std::string option, std::string optarg) throw(OptionException) { + unsigned long ms; + + std::istringstream convert(optarg); + if (!(convert >> ms)) { + throw OptionException("option `"+option+"` requires a number as an argument"); + } + + // TODO: Remove check? + if (d_smtEngine != NULL) { + ResourceManager* rm = NodeManager::fromExprManager(d_smtEngine->getExprManager())->getResourceManager(); + rm->setResourceLimit(ms, false); + } + return ms; +} + + + +// expr/options_handlers.h +void SmtOptionsHandler::setDefaultExprDepth(std::string option, int depth) { + if(depth < -1) { + throw OptionException("--default-expr-depth requires a positive argument, or -1."); + } + + Debug.getStream() << Expr::setdepth(depth); + Trace.getStream() << Expr::setdepth(depth); + Notice.getStream() << Expr::setdepth(depth); + Chat.getStream() << Expr::setdepth(depth); + Message.getStream() << Expr::setdepth(depth); + Warning.getStream() << Expr::setdepth(depth); + // intentionally exclude Dump stream from this list +} + +void SmtOptionsHandler::setDefaultDagThresh(std::string option, int dag) { + if(dag < 0) { + throw OptionException("--default-dag-thresh requires a nonnegative argument."); + } + + Debug.getStream() << Expr::dag(dag); + Trace.getStream() << Expr::dag(dag); + Notice.getStream() << Expr::dag(dag); + Chat.getStream() << Expr::dag(dag); + Message.getStream() << Expr::dag(dag); + Warning.getStream() << Expr::dag(dag); + Dump.getStream() << Expr::dag(dag); +} + +void SmtOptionsHandler::setPrintExprTypes(std::string option) { + Debug.getStream() << Expr::printtypes(true); + Trace.getStream() << Expr::printtypes(true); + Notice.getStream() << Expr::printtypes(true); + Chat.getStream() << Expr::printtypes(true); + Message.getStream() << Expr::printtypes(true); + Warning.getStream() << Expr::printtypes(true); + // intentionally exclude Dump stream from this list +} + + +// main/options_handlers.h +void SmtOptionsHandler::showConfiguration(std::string option) { + fputs(Configuration::about().c_str(), stdout); + printf("\n"); + printf("version : %s\n", Configuration::getVersionString().c_str()); + if(Configuration::isGitBuild()) { + const char* branchName = Configuration::getGitBranchName(); + if(*branchName == '\0') { + branchName = "-"; + } + printf("scm : git [%s %s%s]\n", + branchName, + std::string(Configuration::getGitCommit()).substr(0, 8).c_str(), + Configuration::hasGitModifications() ? + " (with modifications)" : ""); + } else if(Configuration::isSubversionBuild()) { + printf("scm : svn [%s r%u%s]\n", + Configuration::getSubversionBranchName(), + Configuration::getSubversionRevision(), + Configuration::hasSubversionModifications() ? + " (with modifications)" : ""); + } else { + printf("scm : no\n"); + } + printf("\n"); + printf("library : %u.%u.%u\n", + Configuration::getVersionMajor(), + Configuration::getVersionMinor(), + Configuration::getVersionRelease()); + printf("\n"); + printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no"); + printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no"); + printf("replay : %s\n", Configuration::isReplayBuild() ? "yes" : "no"); + printf("tracing : %s\n", Configuration::isTracingBuild() ? "yes" : "no"); + printf("dumping : %s\n", Configuration::isDumpingBuild() ? "yes" : "no"); + printf("muzzled : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no"); + printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no"); + printf("proof : %s\n", Configuration::isProofBuild() ? "yes" : "no"); + printf("coverage : %s\n", Configuration::isCoverageBuild() ? "yes" : "no"); + printf("profiling : %s\n", Configuration::isProfilingBuild() ? "yes" : "no"); + printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no"); + printf("\n"); + printf("cudd : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no"); + printf("cln : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no"); + printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no"); + printf("glpk : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no"); + printf("abc : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no"); + printf("readline : %s\n", Configuration::isBuiltWithReadline() ? "yes" : "no"); + printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); + exit(0); +} + +void SmtOptionsHandler::showDebugTags(std::string option) { + if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) { + printf("available tags:"); + unsigned ntags = Configuration::getNumDebugTags(); + char const* const* tags = Configuration::getDebugTags(); + for(unsigned i = 0; i < ntags; ++ i) { + printf(" %s", tags[i]); + } + printf("\n"); + } else if(! Configuration::isDebugBuild()) { + throw OptionException("debug tags not available in non-debug builds"); + } else { + throw OptionException("debug tags not available in non-tracing builds"); + } + exit(0); +} + +void SmtOptionsHandler::showTraceTags(std::string option) { + if(Configuration::isTracingBuild()) { + printf("available tags:"); + unsigned ntags = Configuration::getNumTraceTags(); + char const* const* tags = Configuration::getTraceTags(); + for (unsigned i = 0; i < ntags; ++ i) { + printf(" %s", tags[i]); + } + printf("\n"); + } else { + throw OptionException("trace tags not available in non-tracing build"); + } + exit(0); +} + +void SmtOptionsHandler::threadN(std::string option) { + throw OptionException(option + " is not a real option by itself. Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\""); +} + + + +/* options/base_options_handlers.h */ +void SmtOptionsHandler::setVerbosity(std::string option, int value) throw(OptionException) { + if(Configuration::isMuzzledBuild()) { + DebugChannel.setStream(CVC4::null_os); + TraceChannel.setStream(CVC4::null_os); + NoticeChannel.setStream(CVC4::null_os); + ChatChannel.setStream(CVC4::null_os); + MessageChannel.setStream(CVC4::null_os); + WarningChannel.setStream(CVC4::null_os); + } else { + if(value < 2) { + ChatChannel.setStream(CVC4::null_os); + } else { + ChatChannel.setStream(std::cout); + } + if(value < 1) { + NoticeChannel.setStream(CVC4::null_os); + } else { + NoticeChannel.setStream(std::cout); + } + if(value < 0) { + MessageChannel.setStream(CVC4::null_os); + WarningChannel.setStream(CVC4::null_os); + } else { + MessageChannel.setStream(std::cout); + WarningChannel.setStream(std::cerr); + } + } +} + +void SmtOptionsHandler::increaseVerbosity(std::string option) { + options::verbosity.set(options::verbosity() + 1); + setVerbosity(option, options::verbosity()); +} + +void SmtOptionsHandler::decreaseVerbosity(std::string option) { + options::verbosity.set(options::verbosity() - 1); + setVerbosity(option, options::verbosity()); +} + +OutputLanguage SmtOptionsHandler::stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "help") { + options::languageHelp.set(true); + return language::output::LANG_AUTO; + } + + try { + return language::toOutputLanguage(optarg); + } catch(OptionException& oe) { + throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --output-language help"); + } + + Unreachable(); +} + +InputLanguage SmtOptionsHandler::stringToInputLanguage(std::string option, std::string optarg) throw(OptionException) { + if(optarg == "help") { + options::languageHelp.set(true); + return language::input::LANG_AUTO; + } + + try { + return language::toInputLanguage(optarg); + } catch(OptionException& oe) { + throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --language help"); + } + + Unreachable(); +} + +void SmtOptionsHandler::addTraceTag(std::string option, std::string optarg) { + if(Configuration::isTracingBuild()) { + if(!Configuration::isTraceTag(optarg.c_str())) { + + if(optarg == "help") { + printf("available tags:"); + unsigned ntags = Configuration::getNumTraceTags(); + char const* const* tags = Configuration::getTraceTags(); + for(unsigned i = 0; i < ntags; ++ i) { + printf(" %s", tags[i]); + } + printf("\n"); + exit(0); + } + + throw OptionException(std::string("trace tag ") + optarg + + std::string(" not available.") + + suggestTags(Configuration::getTraceTags(), optarg) ); + } + } else { + throw OptionException("trace tags not available in non-tracing builds"); + } + Trace.on(optarg); +} + +void SmtOptionsHandler::addDebugTag(std::string option, std::string optarg) { + if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) { + if(!Configuration::isDebugTag(optarg.c_str()) && + !Configuration::isTraceTag(optarg.c_str())) { + + if(optarg == "help") { + printf("available tags:"); + unsigned ntags = Configuration::getNumDebugTags(); + char const* const* tags = Configuration::getDebugTags(); + for(unsigned i = 0; i < ntags; ++ i) { + printf(" %s", tags[i]); + } + printf("\n"); + exit(0); + } + + throw OptionException(std::string("debug tag ") + optarg + + std::string(" not available.") + + suggestTags(Configuration::getDebugTags(), optarg, Configuration::getTraceTags()) ); + } + } else if(! Configuration::isDebugBuild()) { + throw OptionException("debug tags not available in non-debug builds"); + } else { + throw OptionException("debug tags not available in non-tracing builds"); + } + Debug.on(optarg); + Trace.on(optarg); +} + +void SmtOptionsHandler::setPrintSuccess(std::string option, bool value) { + Debug.getStream() << Command::printsuccess(value); + Trace.getStream() << Command::printsuccess(value); + Notice.getStream() << Command::printsuccess(value); + Chat.getStream() << Command::printsuccess(value); + Message.getStream() << Command::printsuccess(value); + Warning.getStream() << Command::printsuccess(value); + *options::out() << Command::printsuccess(value); +} + + +std::string SmtOptionsHandler::suggestTags(char const* const* validTags, std::string inputTag, + char const* const* additionalTags) +{ + DidYouMean didYouMean; + + const char* opt; + for(size_t i = 0; (opt = validTags[i]) != NULL; ++i) { + didYouMean.addWord(validTags[i]); + } + if(additionalTags != NULL) { + for(size_t i = 0; (opt = additionalTags[i]) != NULL; ++i) { + didYouMean.addWord(additionalTags[i]); + } + } + + return didYouMean.getMatchAsString(inputTag); +} + +std::string SmtOptionsHandler::__cvc4_errno_failreason() { +#if HAVE_STRERROR_R +#if STRERROR_R_CHAR_P + if(errno != 0) { + // GNU version of strerror_r: *might* use the given buffer, + // or might not. It returns a pointer to buf, or not. + char buf[80]; + return std::string(strerror_r(errno, buf, sizeof buf)); + } else { + return "unknown reason"; + } +#else /* STRERROR_R_CHAR_P */ + if(errno != 0) { + // XSI version of strerror_r: always uses the given buffer. + // Returns an error code. + char buf[80]; + if(strerror_r(errno, buf, sizeof buf) == 0) { + return std::string(buf); + } else { + // some error occurred while getting the error string + return "unknown reason"; + } + } else { + return "unknown reason"; + } +#endif /* STRERROR_R_CHAR_P */ +#else /* HAVE_STRERROR_R */ + return "unknown reason"; +#endif /* HAVE_STRERROR_R */ +} + +}/* CVC4::smt namespace */ +}/* CVC4 namespace */ diff --git a/src/smt/smt_options_handler.h b/src/smt/smt_options_handler.h new file mode 100644 index 000000000..c4d27a722 --- /dev/null +++ b/src/smt/smt_options_handler.h @@ -0,0 +1,198 @@ +/********************* */ +/*! \file options_handler_interface.h + ** \verbatim + ** Original author: Tim King + ** 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 Interface for custom handlers and predicates options. + ** + ** Interface for custom handlers and predicates options. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__SMT__SMT_OPTIONS_HANDLER_H +#define __CVC4__SMT__SMT_OPTIONS_HANDLER_H + +#include <ostream> +#include <string> + +#include "base/modal_exception.h" +#include "options/arith_heuristic_pivot_rule.h" +#include "options/arith_propagation_mode.h" +#include "options/arith_unate_lemma_mode.h" +#include "options/boolean_term_conversion_mode.h" +#include "options/bv_bitblast_mode.h" +#include "options/decision_mode.h" +#include "options/language.h" +#include "options/option_exception.h" +#include "options/options_handler_interface.h" +#include "options/printer_modes.h" +#include "options/quantifiers_modes.h" +#include "options/simplification_mode.h" +#include "options/theoryof_mode.h" +#include "options/ufss_mode.h" +#include "smt/smt_engine.h" +#include "theory/logic_info.h" + +namespace CVC4 { +namespace smt { + +class CVC4_PUBLIC SmtOptionsHandler : public options::OptionsHandler { +public: + SmtOptionsHandler(SmtEngine* smt); + ~SmtOptionsHandler(); + + // TODO + // theory/arith/options_handlers.h + // theory/quantifiers/options_handlers.h + // theory/bv/options_handlers.h + // theory/booleans/options_handlers.h + // theory/uf/options_handlers.h + // theory/options_handlers.h + // printer/options_handlers.h + // decision/options_handlers.h + // smt/options_handlers.h + // expr/options_handlers.h + // main/options_handlers.h + // options/base_options_handlers.h + + // theory/arith/options_handlers.h + virtual ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg) throw(OptionException); + virtual ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg) throw(OptionException); + virtual ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg) throw(OptionException); + + // theory/quantifiers/options_handlers.h + virtual theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException); + virtual void checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode) throw(OptionException); + virtual theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException); + virtual void checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException); + virtual theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, std::string optarg) throw(OptionException); + virtual void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode) throw(OptionException); + virtual theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg) throw(OptionException); + virtual theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg) throw(OptionException); + virtual theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg) throw(OptionException); + virtual theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException); + virtual theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException); + virtual theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException); + virtual theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException); + virtual theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException); + virtual theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException); + virtual theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException); + + // theory/bv/options_handlers.h + virtual void abcEnabledBuild(std::string option, bool value) throw(OptionException); + virtual void abcEnabledBuild(std::string option, std::string value) throw(OptionException); + virtual theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg) throw(OptionException); + virtual theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException); + virtual void setBitblastAig(std::string option, bool arg) throw(OptionException); + + + // theory/booleans/options_handlers.h + virtual theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException); + + // theory/uf/options_handlers.h + virtual theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg) throw(OptionException); + + // theory/options_handlers.h + virtual theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg); + virtual void useTheory(std::string option, std::string optarg); + + + // printer/options_handlers.h + virtual ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg) throw(OptionException); + virtual InstFormatMode stringToInstFormatMode(std::string option, std::string optarg) throw(OptionException); + + // decision/options_handlers.h + virtual decision::DecisionMode stringToDecisionMode(std::string option, std::string optarg) throw(OptionException); + virtual decision::DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg) throw(OptionException); + + + // smt/options_handlers.h + virtual void dumpMode(std::string option, std::string optarg); + virtual LogicInfo* stringToLogicInfo(std::string option, std::string optarg) throw(OptionException); + virtual SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException); + virtual void beforeSearch(std::string option, bool value) throw(ModalException); + virtual void setProduceAssertions(std::string option, bool value) throw(); + virtual void proofEnabledBuild(std::string option, bool value) throw(OptionException); + virtual void dumpToFile(std::string option, std::string optarg); + virtual void setRegularOutputChannel(std::string option, std::string optarg); + virtual void setDiagnosticOutputChannel(std::string option, std::string optarg); + virtual std::string checkReplayFilename(std::string option, std::string optarg); + virtual std::ostream* checkReplayLogFilename(std::string option, std::string optarg); + virtual void statsEnabledBuild(std::string option, bool value) throw(OptionException); + virtual unsigned long tlimitHandler(std::string option, std::string optarg) throw(OptionException); + virtual unsigned long tlimitPerHandler(std::string option, std::string optarg) throw(OptionException); + virtual unsigned long rlimitHandler(std::string option, std::string optarg) throw(OptionException); + virtual unsigned long rlimitPerHandler(std::string option, std::string optarg) throw(OptionException); + + /* expr/options_handlers.h */ + virtual void setDefaultExprDepth(std::string option, int depth); + virtual void setDefaultDagThresh(std::string option, int dag); + virtual void setPrintExprTypes(std::string option); + + /* main/options_handlers.h */ + virtual void showConfiguration(std::string option); + virtual void showDebugTags(std::string option); + virtual void showTraceTags(std::string option); + virtual void threadN(std::string option); + + /* options/base_options_handlers.h */ + virtual void setVerbosity(std::string option, int value) throw(OptionException); + virtual void increaseVerbosity(std::string option); + virtual void decreaseVerbosity(std::string option); + virtual OutputLanguage stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException); + virtual InputLanguage stringToInputLanguage(std::string option, std::string optarg) throw(OptionException) ; + virtual void addTraceTag(std::string option, std::string optarg); + virtual void addDebugTag(std::string option, std::string optarg); + virtual void setPrintSuccess(std::string option, bool value); + +private: + SmtEngine* d_smtEngine; + + /* Helper utilities */ + static std::string suggestTags(char const* const* validTags, std::string inputTag, + char const* const* additionalTags = NULL); + static std::string __cvc4_errno_failreason(); + + /* Help strings */ + static const std::string s_bitblastingModeHelp; + static const std::string s_booleanTermConversionModeHelp; + static const std::string s_bvSlicerModeHelp; + static const std::string s_cegqiFairModeHelp; + static const std::string s_decisionModeHelp; + static const std::string s_dumpHelp; + static const std::string s_instFormatHelp ; + static const std::string s_instWhenHelp; + static const std::string s_iteLiftQuantHelp; + static const std::string s_literalMatchHelp; + static const std::string s_macrosQuantHelp; + static const std::string s_mbqiModeHelp; + static const std::string s_modelFormatHelp; + static const std::string s_prenexQuantModeHelp; + static const std::string s_qcfModeHelp; + static const std::string s_qcfWhenModeHelp; + static const std::string s_simplificationHelp; + static const std::string s_sygusInvTemplHelp; + static const std::string s_termDbModeHelp; + static const std::string s_theoryOfModeHelp; + static const std::string s_triggerSelModeHelp; + static const std::string s_ufssModeHelp; + static const std::string s_userPatModeHelp; + static const std::string s_errorSelectionRulesHelp; + static const std::string s_arithPropagationModeHelp; + static const std::string s_arithUnateLemmasHelp; + + +}; /* class SmtOptionsHandler */ + + +}/* CVC4::smt namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__SMT__SMT_OPTIONS_HANDLER_H */ diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp deleted file mode 100644 index 376584636..000000000 --- a/src/smt/smt_options_template.cpp +++ /dev/null @@ -1,138 +0,0 @@ -/********************* */ -/*! \file smt_options_template.cpp - ** \verbatim - ** Original author: Morgan Deters - ** 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 Option handling for SmtEngine - ** - ** Option handling for SmtEngine. - **/ - -#include "smt/smt_engine.h" -#include "smt/modal_exception.h" -#include "util/sexpr.h" -#include "util/dump.h" -#include "expr/command.h" -#include "expr/node_manager.h" - -#include <string> -#include <sstream> - -${include_all_option_headers} -${option_handler_includes} - -#line 31 "${template}" - -using namespace std; - -namespace CVC4 { - -void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) - throw(OptionException, ModalException) { - - NodeManagerScope nms(d_nodeManager); - SmtEngine* const smt = this; - - Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; - if(Dump.isOn("benchmark")) { - Dump("benchmark") << SetOptionCommand(key, value); - } - - if(key == "command-verbosity") { - if(!value.isAtom()) { - const vector<SExpr>& cs = value.getChildren(); - if(cs.size() == 2 && - (cs[0].isKeyword() || cs[0].isString()) && - cs[1].isInteger()) { - string c = cs[0].getValue(); - const Integer& v = cs[1].getIntegerValue(); - if(v < 0 || v > 2) { - throw OptionException("command-verbosity must be 0, 1, or 2"); - } - d_commandVerbosity[c] = v; - return; - } - } - throw OptionException("command-verbosity value must be a tuple (command-name, integer)"); - } - - if(!value.isAtom()) { - throw OptionException("bad value for :" + key); - } - - string optionarg = value.getValue(); - - ${smt_setoption_handlers} - -#line 74 "${template}" - - throw UnrecognizedOptionException(key); -} - -CVC4::SExpr SmtEngine::getOption(const std::string& key) const - throw(OptionException) { - - NodeManagerScope nms(d_nodeManager); - - Trace("smt") << "SMT getOption(" << key << ")" << endl; - - if(key.length() >= 18 && - key.compare(0, 18, "command-verbosity:") == 0) { - map<string, Integer>::const_iterator i = d_commandVerbosity.find(key.c_str() + 18); - if(i != d_commandVerbosity.end()) { - return (*i).second; - } - i = d_commandVerbosity.find("*"); - if(i != d_commandVerbosity.end()) { - return (*i).second; - } - return Integer(2); - } - - if(Dump.isOn("benchmark")) { - Dump("benchmark") << GetOptionCommand(key); - } - - if(key == "command-verbosity") { - vector<SExpr> result; - SExpr defaultVerbosity; - for(map<string, Integer>::const_iterator i = d_commandVerbosity.begin(); - i != d_commandVerbosity.end(); - ++i) { - vector<SExpr> v; - v.push_back((*i).first); - v.push_back((*i).second); - if((*i).first == "*") { - // put the default at the end of the SExpr - defaultVerbosity = v; - } else { - result.push_back(v); - } - } - // put the default at the end of the SExpr - if(!defaultVerbosity.isAtom()) { - result.push_back(defaultVerbosity); - } else { - // ensure the default is always listed - vector<SExpr> v; - v.push_back("*"); - v.push_back(Integer(2)); - result.push_back(v); - } - return result; - } - - ${smt_getoption_handlers} - -#line 134 "${template}" - - throw UnrecognizedOptionException(key); -} - -}/* CVC4 namespace */ |