diff options
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/CMakeLists.txt | 5 | ||||
| -rw-r--r-- | src/options/Makefile | 4 | ||||
| -rw-r--r-- | src/options/Makefile.am | 158 | ||||
| -rw-r--r-- | src/options/option_exception.cpp | 21 | ||||
| -rw-r--r-- | src/options/option_exception.h | 14 | ||||
| -rw-r--r-- | src/options/options_handler.cpp | 48 | ||||
| -rw-r--r-- | src/options/options_handler.h | 4 | ||||
| -rw-r--r-- | src/options/options_template.cpp | 15 | ||||
| -rw-r--r-- | src/options/quantifiers_options.toml | 41 | ||||
| -rw-r--r-- | src/options/smt_modes.cpp (renamed from src/options/simplification_mode.cpp) | 23 | ||||
| -rw-r--r-- | src/options/smt_modes.h (renamed from src/options/simplification_mode.h) | 41 | ||||
| -rw-r--r-- | src/options/smt_options.toml | 15 |
12 files changed, 187 insertions, 202 deletions
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 457fd23cd..c711567ab 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -21,6 +21,7 @@ libcvc4_add_sources( language.h open_ostream.cpp open_ostream.h + option_exception.cpp option_exception.h options.h options_handler.cpp @@ -32,8 +33,8 @@ libcvc4_add_sources( quantifiers_modes.h set_language.cpp set_language.h - simplification_mode.cpp - simplification_mode.h + smt_modes.cpp + smt_modes.h sygus_out_mode.h theoryof_mode.cpp theoryof_mode.h diff --git a/src/options/Makefile b/src/options/Makefile deleted file mode 100644 index 54a46191d..000000000 --- a/src/options/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../.. -srcdir = src/options - -include $(topdir)/Makefile.subdir diff --git a/src/options/Makefile.am b/src/options/Makefile.am deleted file mode 100644 index c311e04d8..000000000 --- a/src/options/Makefile.am +++ /dev/null @@ -1,158 +0,0 @@ -# if coverage is enabled: -# COVERAGE_ON = yes from configure.ac -# Using an inline conditional function to choose between absolute and -# relative paths for options files -# lcov does not support relative paths and src/options and src/expr -# in particular were breaking it -# Building with coverage will cause portability issues in some cases - -VPATH = $(if $(COVERAGE_ON), $(realpath @srcdir@), @srcdir@) - -OPTIONS_CONFIG_FILES = \ - arith_options.toml \ - arrays_options.toml \ - base_options.toml \ - booleans_options.toml \ - builtin_options.toml \ - bv_options.toml \ - datatypes_options.toml \ - decision_options.toml \ - expr_options.toml \ - fp_options.toml \ - idl_options.toml \ - main_options.toml \ - parser_options.toml \ - printer_options.toml \ - proof_options.toml \ - prop_options.toml \ - quantifiers_options.toml \ - sep_options.toml \ - sets_options.toml \ - smt_options.toml \ - strings_options.toml \ - theory_options.toml \ - uf_options.toml - -OPTIONS_GEN_H = $(OPTIONS_CONFIG_FILES:.toml=.h) - -OPTIONS_GEN_CPP = $(OPTIONS_CONFIG_FILES:.toml=.cpp) - -CPP_TEMPLATE_FILES = \ - module_template.h \ - module_template.cpp \ - options_holder_template.h \ - options_template.cpp - -DOCUMENTATION_FILES = \ - ../../doc/cvc4.1 \ - ../../doc/SmtEngine.3cvc \ - ../../doc/options.3cvc - -DOCUMENTATION_TEMPLATE_FILES = \ - ../../doc/cvc4.1_template \ - ../../doc/SmtEngine.3cvc_template \ - ../../doc/options.3cvc_template - - -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - $(if $(COVERAGE_ON), -I@abs_builddir@/.. -I@abs_srcdir@/../include -I@abs_srcdir@/.., \ - -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/..) -AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = liboptions.la - -liboptions_la_SOURCES = \ - arith_heuristic_pivot_rule.cpp \ - arith_heuristic_pivot_rule.h \ - arith_propagation_mode.cpp \ - arith_propagation_mode.h \ - arith_unate_lemma_mode.cpp \ - arith_unate_lemma_mode.h \ - argument_extender_implementation.cpp \ - argument_extender_implementation.h \ - argument_extender.h \ - base_handlers.h \ - bv_bitblast_mode.cpp \ - bv_bitblast_mode.h \ - datatypes_modes.h \ - decision_mode.cpp \ - decision_mode.h \ - decision_weight.h \ - didyoumean.cpp \ - didyoumean.h \ - language.cpp \ - language.h \ - open_ostream.cpp \ - open_ostream.h \ - option_exception.h \ - options.h \ - options_handler.cpp \ - options_handler.h \ - options_public_functions.cpp \ - printer_modes.cpp \ - printer_modes.h \ - quantifiers_modes.cpp \ - quantifiers_modes.h \ - set_language.cpp \ - set_language.h \ - simplification_mode.cpp \ - simplification_mode.h \ - sygus_out_mode.h \ - theoryof_mode.cpp \ - theoryof_mode.h \ - ufss_mode.h - - -nodist_liboptions_la_SOURCES = \ - options.cpp \ - options_holder.h \ - $(OPTIONS_GEN_H) \ - $(OPTIONS_GEN_CPP) - - -BUILT_SOURCES = \ - options.cpp - - -CLEANFILES = \ - $(BUILT_SOURCES) \ - $(OPTIONS_GEN_H) \ - $(OPTIONS_GEN_CPP) \ - $(DOCUMENTATION_FILES) \ - options_holder.h - - -EXTRA_DIST = \ - options.cpp \ - options_holder.h \ - $(OPTIONS_GEN_CPP) \ - $(OPTIONS_GEN_H) \ - $(OPTIONS_CONFIG_FILES) \ - $(CPP_TEMPLATE_FILES) \ - $(DOCUMENTATION_FILES) \ - mkoptions.py \ - language.i \ - option_exception.i \ - options.i - - - -# Make sure the implicit rules never mistake a _template.cpp or _template.h -# file for source file. -$(CPP_TEMPLATE_FILES):; - -# All source/doc files are generated in one pass with rule options.cpp. Note -# that this is done incrementally since mkoptions.py checks if a generated file -# changed before writing to the file. No global re-compilation of all generated -# files happens if only individual files were modified. -$(OPTIONS_GEN_CPP) $(OPTIONS_GEN_H) options_holder.h $(DOCUMENTATION_FILES): options.cpp - -options.cpp: mkoptions.py $(CPP_TEMPLATE_FILES) $(OPTIONS_CONFIG_FILES) $(DOCUMENTATION_TEMPLATE_FILES) - $(PYTHON) @srcdir@/mkoptions.py @abs_srcdir@ ../../doc . $(addprefix @abs_srcdir@/, $(OPTIONS_CONFIG_FILES)) - -# This rule is ugly. It's needed to ensure that automake's dependence -# includes are available during distclean, even though they come from -# directories that are cleaned first. Without this rule, "distclean" -# fails. -%.Plo:; $(MKDIR_P) "$(dir $@)" && : > "$@" diff --git a/src/options/option_exception.cpp b/src/options/option_exception.cpp new file mode 100644 index 000000000..33e2e21d1 --- /dev/null +++ b/src/options/option_exception.cpp @@ -0,0 +1,21 @@ +/********************* */ +/*! \file option_exception.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Options-related exceptions + ** + ** Options-related exceptions. + **/ + +#include "options/option_exception.h" + +namespace CVC4 { +const std::string OptionException::s_errPrefix = "Error in option parsing: "; +} // namespace CVC4 diff --git a/src/options/option_exception.h b/src/options/option_exception.h index 97a9de770..63b8aa890 100644 --- a/src/options/option_exception.h +++ b/src/options/option_exception.h @@ -31,10 +31,20 @@ namespace CVC4 { */ class CVC4_PUBLIC OptionException : public CVC4::Exception { public: - OptionException(const std::string& s) - : CVC4::Exception("Error in option parsing: " + s) + OptionException(const std::string& s) : CVC4::Exception(s_errPrefix + s) {} + + /** + * Get the error message without the prefix that is automatically added for + * OptionExceptions. + */ + std::string getRawMessage() const { + return getMessage().substr(s_errPrefix.size()); } + + private: + /** The string to be added in front of the actual error message */ + static const std::string s_errPrefix; };/* class OptionException */ /** diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 9cf5180e8..46663ce7c 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -42,8 +42,6 @@ #include "options/language.h" #include "options/option_exception.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" @@ -1472,6 +1470,51 @@ SimplificationMode OptionsHandler::stringToSimplificationMode( } } +const std::string OptionsHandler::s_modelCoresHelp = + "\ +Model cores modes currently supported by the --simplification option:\n\ +\n\ +none (default) \n\ ++ do not compute model cores\n\ +\n\ +simple\n\ ++ only include a subset of variables whose values are sufficient to show the\n\ +input formula is satisfied by the given model\n\ +\n\ +non-implied\n\ ++ only include a subset of variables whose values, in addition to the values\n\ +of variables whose values are implied, are sufficient to show the input\n\ +formula is satisfied by the given model\n\ +\n\ +"; + +ModelCoresMode OptionsHandler::stringToModelCoresMode(std::string option, + std::string optarg) +{ + if (optarg == "none") + { + return MODEL_CORES_NONE; + } + else if (optarg == "simple") + { + return MODEL_CORES_SIMPLE; + } + else if (optarg == "non-implied") + { + return MODEL_CORES_NON_IMPLIED; + } + else if (optarg == "help") + { + puts(s_modelCoresHelp.c_str()); + exit(1); + } + else + { + throw OptionException(std::string("unknown option for --model-cores: `") + + optarg + "'. Try --model-cores help."); + } +} + const std::string OptionsHandler::s_sygusSolutionOutModeHelp = "\ Modes for finite model finding bound minimization, supported by --sygus-out:\n\ @@ -1685,6 +1728,7 @@ void OptionsHandler::showConfiguration(std::string option) { print_config_cond("proof", Configuration::isProofBuild()); print_config_cond("coverage", Configuration::isCoverageBuild()); print_config_cond("profiling", Configuration::isProfilingBuild()); + print_config_cond("asan", Configuration::isAsanBuild()); print_config_cond("competition", Configuration::isCompetitionBuild()); std::cout << std::endl; diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 0205b0b73..3078db0f8 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -35,7 +35,7 @@ #include "options/options.h" #include "options/printer_modes.h" #include "options/quantifiers_modes.h" -#include "options/simplification_mode.h" +#include "options/smt_modes.h" #include "options/sygus_out_mode.h" #include "options/theoryof_mode.h" #include "options/ufss_mode.h" @@ -171,6 +171,7 @@ public: void notifyDumpMode(std::string option); SimplificationMode stringToSimplificationMode(std::string option, std::string optarg); + ModelCoresMode stringToModelCoresMode(std::string option, std::string optarg); SygusSolutionOutMode stringToSygusSolutionOutMode(std::string option, std::string optarg); void setProduceAssertions(std::string option, bool value); @@ -241,6 +242,7 @@ public: static const std::string s_qcfModeHelp; static const std::string s_qcfWhenModeHelp; static const std::string s_simplificationHelp; + static const std::string s_modelCoresHelp; static const std::string s_sygusSolutionOutModeHelp; static const std::string s_cbqiBvIneqModeHelp; static const std::string s_cegqiSingleInvHelp; diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 609713ce8..85a9747fe 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -265,7 +265,20 @@ ListenerCollection::Registration* Options::registerAndNotify( ListenerCollection::Registration* registration = collection.registerListener(listener); if(notify) { - listener->notify(); + try + { + listener->notify(); + } + catch (OptionException& e) + { + // It can happen that listener->notify() throws an OptionException. In + // that case, we have to make sure that we delete the registration of our + // listener before rethrowing the exception. Otherwise the + // ListenerCollection deconstructor will complain that not all + // registrations have been removed before invoking the deconstructor. + delete registration; + throw OptionException(e.getRawMessage()); + } } return registration; } diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 07c11d73a..0762622f0 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1094,7 +1094,6 @@ header = "options/quantifiers_options.h" default = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST" handler = "stringToSygusInvTemplMode" includes = ["options/quantifiers_modes.h"] - read_only = true help = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)" [[option]] @@ -1364,6 +1363,46 @@ header = "options/quantifiers_options.h" help = "timeout (in milliseconds) for satisfiability checks in expression miners" [[option]] + name = "sygusQueryGen" + category = "regular" + long = "sygus-query-gen" + type = "bool" + default = "false" + help = "use sygus to enumerate interesting satisfiability queries" + +[[option]] + name = "sygusQueryGenThresh" + category = "regular" + long = "sygus-query-gen-thresh=N" + type = "unsigned" + default = "5" + help = "number of points that we allow to be equal for enumerating satisfiable queries with sygus-query-gen" + +[[option]] + name = "sygusQueryGenCheck" + category = "regular" + long = "sygus-query-gen-check" + type = "bool" + default = "true" + help = "use interesting satisfiability queries to check soundness of CVC4" + +[[option]] + name = "sygusQueryGenDumpFiles" + category = "regular" + long = "sygus-query-gen-dump-files" + type = "bool" + default = "false" + help = "dump external files corresponding to interesting satisfiability queries with sygus-query-gen" + +[[option]] + name = "sygusSolFilterImplied" + category = "regular" + long = "sygus-sol-filter-implied" + type = "bool" + default = "false" + help = "use sygus to enumerate interesting satisfiability queries" + +[[option]] name = "sygusExprMinerCheckUseExport" category = "expert" long = "sygus-expr-miner-check-use-export" diff --git a/src/options/simplification_mode.cpp b/src/options/smt_modes.cpp index 6b6fc842d..4a2fd404c 100644 --- a/src/options/simplification_mode.cpp +++ b/src/options/smt_modes.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file simplification_mode.cpp +/*! \file smt_modes.cpp ** \verbatim ** Top contributors (to current version): ** Morgan Deters, Tim King @@ -15,25 +15,22 @@ ** \todo document this file **/ -#include "options/simplification_mode.h" +#include "options/smt_modes.h" #include <iostream> 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) << "]"; +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 */ +} // namespace CVC4 diff --git a/src/options/simplification_mode.h b/src/options/smt_modes.h index 52bf25fa1..761f3be01 100644 --- a/src/options/simplification_mode.h +++ b/src/options/smt_modes.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file simplification_mode.h +/*! \file smt_modes.h ** \verbatim ** Top contributors (to current version): ** Morgan Deters, Tim King @@ -17,23 +17,42 @@ #include "cvc4_public.h" -#ifndef __CVC4__SMT__SIMPLIFICATION_MODE_H -#define __CVC4__SMT__SIMPLIFICATION_MODE_H +#ifndef __CVC4__SMT__MODES_H +#define __CVC4__SMT__MODES_H #include <iosfwd> namespace CVC4 { /** Enumeration of simplification modes (when to simplify). */ -typedef enum { +enum SimplificationMode +{ /** 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 */ +}; + +std::ostream& operator<<(std::ostream& out, + SimplificationMode mode) CVC4_PUBLIC; + +/** Enumeration of model core modes. */ +enum ModelCoresMode +{ + /** Do not compute model cores */ + MODEL_CORES_NONE, + /** + * Compute "simple" model cores that exclude variables that do not + * contribute to satisfying the input. + */ + MODEL_CORES_SIMPLE, + /** + * Compute model cores that also exclude variables whose variables are implied + * by others. + */ + MODEL_CORES_NON_IMPLIED +}; + +} // namespace CVC4 + +#endif /* __CVC4__SMT__MODES_H */ diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 8af1000ba..e0041774a 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -40,7 +40,7 @@ header = "options/smt_options.h" type = "SimplificationMode" default = "SIMPLIFICATION_MODE_BATCH" handler = "stringToSimplificationMode" - includes = ["options/simplification_mode.h"] + includes = ["options/smt_modes.h"] help = "choose simplification mode, see --simplification=help" [[alias]] @@ -99,13 +99,14 @@ header = "options/smt_options.h" help = "output models after every SAT/INVALID/UNKNOWN response" [[option]] - name = "produceModelCores" + name = "modelCoresMode" category = "regular" - long = "produce-model-cores" - type = "bool" - default = "false" - read_only = true - help = "when printing models, compute a minimal core of relevant definitions" + long = "model-cores=MODE" + type = "ModelCoresMode" + default = "MODEL_CORES_NONE" + handler = "stringToModelCoresMode" + includes = ["options/smt_modes.h"] + help = "mode for producing model cores" [[option]] name = "proof" |