diff options
| author | Tim King <taking@google.com> | 2015-12-14 18:51:40 -0800 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2015-12-14 18:51:40 -0800 |
| commit | 90e3b73fbd1b2eb262a7a7e2e72d701c8f9e3600 (patch) | |
| tree | 77af58f4233d766d31e8e032e16cc0b4833d8de2 /src/options | |
| parent | 157a2ed349418611302476dce79fced1d95a4ecc (diff) | |
Refactoring Options Handler & Library Cycle Breaking
What to Know As a User:
A number of files have moved. Users that include files in the public API in more refined ways than using #include <cvc4.h> should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems.
The Problem:
The build order of CVC4 used to be [roughly] specified as:
options < expr < util < libcvc4 < parsers < main
Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable.
The Solution:
To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen:
1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file.
2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options.
3. All of the old options_handlers.h files have been refactored.
4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary.
5. I am removing the libstatistics library.
The constraints that the CVC4 build system will eventually satisfy are:
- The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from */kinds files and */options files.
- The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases.
- The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.)
- One library per Makefile.am.
- No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.)
The build order of CVC4 can now be [roughly] specified as
base < options < util < expr < smt_util < libcvc4 < parsers < main
The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean.
More details about the directories:
base/
The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere.
options/
The options/ directory is self contained.
- It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h .
- There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options.
- Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done.
- The */options_handlers.h files have been removed.
- The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp.
- All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h .
util/
The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean.
expr/
The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/.
- An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h.
- Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h.
- The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/.
- Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes.
- Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources.
- This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC.
smt_util/
The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel.
What is up next:
- A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed.
- The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up.
Diffstat (limited to 'src/options')
63 files changed, 4870 insertions, 552 deletions
diff --git a/src/options/Makefile.am b/src/options/Makefile.am index 0d4b970d8..d871bfb0a 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -1,65 +1,177 @@ -OPTIONS_FILES_SRCS = \ - base_options.cpp \ - base_options.h \ - ../expr/options.cpp \ - ../expr/options.h \ - ../theory/booleans/options.cpp \ - ../theory/booleans/options.h \ - ../theory/options.cpp \ - ../theory/options.h \ - ../theory/bv/options.cpp \ - ../theory/bv/options.h \ - ../theory/datatypes/options.cpp \ - ../theory/datatypes/options.h \ - ../theory/builtin/options.cpp \ - ../theory/builtin/options.h \ - ../theory/arith/options.cpp \ - ../theory/arith/options.h \ - ../theory/uf/options.cpp \ - ../theory/uf/options.h \ - ../theory/arrays/options.cpp \ - ../theory/arrays/options.h \ - ../theory/quantifiers/options.cpp \ - ../theory/quantifiers/options.h \ - ../theory/strings/options.cpp \ - ../theory/strings/options.h \ - ../prop/options.cpp \ - ../prop/options.h \ - ../proof/options.cpp \ - ../proof/options.h \ - ../printer/options.cpp \ - ../printer/options.h \ - ../smt/options.cpp \ - ../smt/options.h \ - ../decision/options.cpp \ - ../decision/options.h \ - ../main/options.cpp \ - ../main/options.h \ - ../parser/options.cpp \ - ../parser/options.h \ - ../theory/idl/options.cpp \ - ../theory/idl/options.h \ - ../theory/sets/options.cpp \ - ../theory/sets/options.h \ - ../theory/fp/options.cpp \ - ../theory/fp/options.h - -OPTIONS_FILES = \ - $(patsubst %.cpp,%,$(filter %.cpp,$(OPTIONS_FILES_SRCS))) - -OPTIONS_CPPS = \ - $(filter %.cpp,$(OPTIONS_FILES_SRCS)) - -OPTIONS_HEADS = \ - $(filter %.h,$(OPTIONS_FILES_SRCS)) +# How options are built: +# Step 1: Copy the X_options source file into builddir as X_options.tmp. +# X_options.tmp is a .PHONY rule to force this step to always be done. +# Step 2: Compare X_options.tmp to X_options.options. +# If they are different, overwrite "X_options.options". +# This is the file that we use to generate options from. +# This is always up to dat with X_options. The change in name is just +# to keep Makefile stage more explicit. +# Step 3: Generate X_options.sed from X_options.options using mkoptions. +# Step 4: Generate X_options.h from X_options.sed +# Step 5: Generate X_options.cpp from X_options.sed. +# This stage also waits for X_options.h as otherwise it cannot compile. +# + +OPTIONS_SRC_FILES = \ + arith_options \ + arrays_options \ + base_options \ + booleans_options \ + builtin_options \ + bv_options \ + datatypes_options \ + decision_options \ + expr_options \ + fp_options \ + idl_options \ + main_options \ + parser_options \ + printer_options \ + proof_options \ + prop_options \ + quantifiers_options \ + sets_options \ + smt_options \ + strings_options \ + theory_options \ + uf_options + +OPTIONS_TEMPS = \ + arith_options.tmp \ + arrays_options.tmp \ + base_options.tmp \ + booleans_options.tmp \ + builtin_options.tmp \ + bv_options.tmp \ + datatypes_options.tmp \ + decision_options.tmp \ + expr_options.tmp \ + fp_options.tmp \ + idl_options.tmp \ + main_options.tmp \ + parser_options.tmp \ + printer_options.tmp \ + proof_options.tmp \ + prop_options.tmp \ + quantifiers_options.tmp \ + sets_options.tmp \ + smt_options.tmp \ + strings_options.tmp \ + theory_options.tmp \ + uf_options.tmp + +OPTIONS_OPTIONS_FILES = \ + arith_options.options \ + arrays_options.options \ + base_options.options \ + booleans_options.options \ + builtin_options.options \ + bv_options.options \ + datatypes_options.options \ + decision_options.options \ + expr_options.options \ + fp_options.options \ + idl_options.options \ + main_options.options \ + parser_options.options \ + printer_options.options \ + proof_options.options \ + prop_options.options \ + quantifiers_options.options \ + sets_options.options \ + smt_options.options \ + strings_options.options \ + theory_options.options \ + uf_options.options OPTIONS_SEDS = \ - $(patsubst %,%.sed,$(OPTIONS_FILES)) + arith_options.sed \ + arrays_options.sed \ + base_options.sed \ + booleans_options.sed \ + builtin_options.sed \ + bv_options.sed \ + datatypes_options.sed \ + decision_options.sed \ + expr_options.sed \ + fp_options.sed \ + idl_options.sed \ + main_options.sed \ + parser_options.sed \ + printer_options.sed \ + proof_options.sed \ + prop_options.sed \ + quantifiers_options.sed \ + sets_options.sed \ + smt_options.sed \ + strings_options.sed \ + theory_options.sed \ + uf_options.sed -OPTIONS_OBJ = \ - $(patsubst %.cpp,%.$(OBJEXT),$(OPTIONS_CPP)) +OPTIONS_HEADS = \ + arith_options.h \ + arrays_options.h \ + base_options.h \ + booleans_options.h \ + builtin_options.h \ + bv_options.h \ + datatypes_options.h \ + decision_options.h \ + expr_options.h \ + fp_options.h \ + idl_options.h \ + main_options.h \ + parser_options.h \ + printer_options.h \ + proof_options.h \ + prop_options.h \ + quantifiers_options.h \ + sets_options.h \ + smt_options.h \ + strings_options.h \ + theory_options.h \ + uf_options.h +OPTIONS_CPPS = \ + arith_options.cpp \ + arrays_options.cpp \ + base_options.cpp \ + booleans_options.cpp \ + builtin_options.cpp \ + bv_options.cpp \ + datatypes_options.cpp \ + decision_options.cpp \ + expr_options.cpp \ + fp_options.cpp \ + idl_options.cpp \ + main_options.cpp \ + parser_options.cpp \ + printer_options.cpp \ + proof_options.cpp \ + prop_options.cpp \ + quantifiers_options.cpp \ + sets_options.cpp \ + smt_options.cpp \ + strings_options.cpp \ + theory_options.cpp \ + uf_options.cpp + + +CPP_TEMPLATE_FILES = \ + base_options_template.h \ + base_options_template.cpp \ + options_holder_template.h \ + options_template.cpp \ + options_handler_get_option_template.cpp \ + options_handler_set_option_template.cpp +CPP_TEMPLATE_SEDS = \ + base_options_template.h.sed \ + base_options_template.cpp.sed \ + options_holder_template.h.sed \ + options_template.cpp.sed \ + options_handler_get_option_template.cpp.sed \ + options_handler_set_option_template.cpp.sed DOCUMENTATION_FILES = \ @@ -68,19 +180,17 @@ DOCUMENTATION_FILES = \ ../../doc/SmtEngine.3cvc \ ../../doc/options.3cvc -TEMPLATE_FILES = \ - base_options_template.h \ - base_options_template.cpp \ - options_holder_template.h \ - options_template.cpp \ - ../smt/smt_options_template.cpp \ +DOCUMENTATION_TEMPLATE_FILES = \ ../../doc/cvc4.1_template \ ../../doc/libcvc4.3_template \ ../../doc/SmtEngine.3cvc_template \ ../../doc/options.3cvc_template -TEMPLATE_SEDS = \ - $(patsubst %,%.sed,$(TEMPLATE_FILES)) +DOCUMENTATION_TEMPLATE_SEDS = \ + ../../doc/cvc4.1_template.sed \ + ../../doc/libcvc4.3_template.sed \ + ../../doc/SmtEngine.3cvc_template.sed \ + ../../doc/options.3cvc_template.sed AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ @@ -90,63 +200,98 @@ 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 \ + base_handlers.h \ + boolean_term_conversion_mode.cpp \ + boolean_term_conversion_mode.h \ + bv_bitblast_mode.cpp \ + bv_bitblast_mode.h \ + decision_mode.cpp \ + decision_mode.h \ + decision_weight.h \ + didyoumean.cpp \ + didyoumean.h \ + language.cpp \ + language.h \ + logic_info_forward.h \ + option_exception.h \ options.h \ - base_options_handlers.h \ - option_exception.h + options_handler_interface.cpp \ + options_handler_interface.h \ + printer_modes.cpp \ + printer_modes.h \ + quantifiers_modes.cpp \ + quantifiers_modes.h \ + simplification_mode.cpp \ + simplification_mode.h \ + theoryof_mode.cpp \ + theoryof_mode.h \ + ufss_mode.h + nodist_liboptions_la_SOURCES = \ options.cpp \ options_holder.h \ - $(OPTIONS_FILES_SRCS) + $(OPTIONS_HEADS) \ + $(OPTIONS_CPPS) \ + options_handler_get_option.cpp \ + options_handler_set_option.cpp BUILT_SOURCES = \ - exprs-builts \ - ../smt/smt_options.cpp \ + $(CPP_TEMPLATE_SEDS) \ + $(DOCUMENTATION_FILES) \ + $(DOCUMENTATION_TEMPLATE_SEDS) \ + $(OPTIONS_CPPS) \ + $(OPTIONS_HEADS) \ + $(OPTIONS_OPTIONS_FILES) \ + $(OPTIONS_SEDS) \ options.cpp \ + options_handler_get_option.cpp \ + options_handler_set_option.cpp \ options_holder.h \ - $(OPTIONS_FILES_SRCS) \ - $(OPTIONS_SEDS) \ - summary.sed \ - $(TEMPLATE_SEDS) - + summary.sed -# The documentation files are added to BUILT_SOURCES to get the files to -# be built. Alternative suggestions for building these files would be -# appreciated. +# listing {Debug,Trace}_tags too ensures that make doesn't auto-remove it +# after building (if it does, we don't get the "cached" effect with +# the .tmp files below, and we have to re-compile and re-link each +# time, even when there are no changes). BUILT_SOURCES += \ - $(DOCUMENTATION_FILES) - + Debug_tags.h \ + Debug_tags \ + Trace_tags.h \ + Trace_tags CLEANFILES = \ - $(OPTIONS_FILES_SRCS) \ $(BUILT_SOURCES) \ - $(DOCUMENTATION_FILES) + $(DOCUMENTATION_FILES) \ + $(OPTIONS_TEMPS) EXTRA_DIST = \ - mkoptions \ - base_options_template.h \ + $(DOCUMENTATION_FILES) \ + $(OPTIONS_CPPS) \ + $(OPTIONS_HEADS) \ + $(OPTIONS_SRC_FILES) \ base_options_template.cpp \ - options_template.cpp \ - options_holder_template.h \ - options.i \ - option_exception.i \ - $(OPTIONS_FILES) \ + base_options_template.h \ + language.i \ + mkoptions \ mktagheaders \ mktags \ - $(DOCUMENTATION_FILES) + option_exception.i \ + options.i \ + options_handler_get_option_template.cpp \ + options_handler_interface.i \ + options_handler_set_option_template.cpp \ + options_holder_template.h \ + options_template.cpp -# listing {Debug,Trace}_tags too ensures that make doesn't auto-remove it -# after building (if it does, we don't get the "cached" effect with -# the .tmp files below, and we have to re-compile and re-link each -# time, even when there are no changes). -BUILT_SOURCES += \ - Debug_tags.h \ - Debug_tags \ - Trace_tags.h \ - Trace_tags - %_tags.h: %_tags mktagheaders $(AM_V_at)chmod +x @srcdir@/mktagheaders $(AM_V_GEN)( @srcdir@/mktagheaders "$<" "$<" ) >"$@" @@ -175,52 +320,72 @@ MOSTLYCLEANFILES = \ Debug_tags.h \ Trace_tags.h -# mkoptions template-sed template-file (options-file)* -# mkoptions apply-sed-files-to-template sed-file template-file filename +# Make sure the implicit rules never mistake a _template.cpp or _template.h file for source file. +options_holder_template.h options_template.cpp options_handler_get_option_template.cpp options_handler_set_option_template.cpp base_options_template.h base_options_template.cpp :; + +# Make sure the implicit rules never mistake X_options for the -o file for a +# CPP file. +arith_options arrays_options base_options booleans_options builtin_options bv_options datatypes_options decision_options expr_options fp_options idl_options main_options parser_options printer_options proof_options prop_options quantifiers_options sets_options smt_options strings_options theory_options uf_options:; -$(OPTIONS_FILES):; -options_holder_template.h options_template.cpp ../smt/smt_options_template.cpp base_options_template.h base_options_template.cpp :; +# These are phony to force them to be made everytime. +.PHONY: arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp + +# Make is happier being listed explictly. Not sure why. +arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp: + echo "$@" "$(@:.tmp=)" + $(AM_V_GEN)(cp "@srcdir@/$(@:.tmp=)" "$@" || true) +#TIM: +#The (... || true) here is to make distcheck not fail. + +%_options.options: %_options.tmp + $(AM_V_GEN)\ + diff -q "$^" "$@" &>/dev/null || mv "$^" "$@" || true -$(TEMPLATE_SEDS) : %.sed : % mkoptions + +# This bit is kinda tricky. +# We use the updating of %_options.options to signal that the options file updated. +# However, we use the original file in src to generate the file. +%_options.sed: %_options.options mkoptions + $(AM_V_at)chmod +x @srcdir@/mkoptions + $(AM_V_GEN)(@srcdir@/mkoptions module-sed "@srcdir@/$(@:.sed=)" ) > "$@" + + +$(CPP_TEMPLATE_SEDS): %.sed : % mkoptions # echo "template seds" # echo "$@" # echo $(TEMPLATE_SEDS) $(AM_V_at)chmod +x @srcdir@/mkoptions $(AM_V_GEN)(@srcdir@/mkoptions template-sed "$<" ) > "$@" - -$(OPTIONS_SEDS) : %.sed : % mkoptions -# echo "sedheads" +$(DOCUMENTATION_TEMPLATE_SEDS): %.sed : % mkoptions +# echo "template seds" # echo "$@" -# echo $(OPTIONS_SEDS) +# echo $(TEMPLATE_SEDS) $(AM_V_at)chmod +x @srcdir@/mkoptions - $(AM_V_at)mkdir -p `dirname "$@"` - $(AM_V_GEN)(@srcdir@/mkoptions module-sed "$<" ) > "$@" + $(AM_V_GEN)(@srcdir@/mkoptions template-sed "$<" ) > "$@" -$(OPTIONS_HEADS) : %.h : %.sed mkoptions base_options_template.h base_options_template.h.sed +%_options.h : %_options.sed mkoptions base_options_template.h base_options_template.h.sed # echo heads # echo "$@" # echo $(OPTIONS_HEADS) $(AM_V_at)chmod +x @srcdir@/mkoptions - $(AM_V_at)mkdir -p `dirname "$@"` $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ @srcdir@/base_options_template.h \ base_options_template.h.sed \ "$<" \ ) > "$@" -summary.sed : mkoptions $(OPTIONS_FILES) +summary.sed : mkoptions $(OPTIONS_OPTIONS_FILES) $(AM_V_at)chmod +x @srcdir@/mkoptions $(AM_V_GEN)(@srcdir@/mkoptions summary-sed \ - $(foreach o,$(OPTIONS_FILES),"$(srcdir)/$(o)") \ + $(OPTIONS_OPTIONS_FILES) \ ) > summary.sed # mkoptions apply-sed-to-template sed-file template-file -options_holder.h : options_holder_template.h options_holder_template.h.sed summary.sed mkoptions -# echo "$(OPTIONS_FILES)" +options_holder.h : options_holder_template.h options_holder_template.h.sed summary.sed mkoptions $(OPTIONS_HEADS) $(AM_V_at)chmod +x @srcdir@/mkoptions $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ @srcdir@/options_holder_template.h \ @@ -228,19 +393,9 @@ options_holder.h : options_holder_template.h options_holder_template.h.sed summa summary.sed \ ) > "$@" -gen-heads-stamp : $(OPTIONS_HEADS) options_holder.h -.PHONY : gen-heads-stamp - - -# Bit of a hack here. The .h file needs to always be built before the .cpp file is compiled. -$(OPTIONS_CPPS) : %.cpp : %.sed mkoptions base_options_template.cpp base_options_template.cpp.sed gen-heads-stamp -# echo "cpps" -# echo "$@" -# echo "$<" -# echo $(OPTIONS_CPPS) -# echo $(OPTIONS_FILES_SRCS) +# Make sure not to match with "options.cpp" too. +%_options.cpp: %_options.sed %_options.h mkoptions options_holder.h base_options_template.cpp base_options_template.cpp.sed $(AM_V_at)chmod +x @srcdir@/mkoptions - $(AM_V_at)mkdir -p `dirname "$@"` $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ @srcdir@/base_options_template.cpp \ base_options_template.cpp.sed \ @@ -249,9 +404,9 @@ $(OPTIONS_CPPS) : %.cpp : %.sed mkoptions base_options_template.cpp base_options + # mkoptions apply-sed-to-template sed-file template-file -options.cpp : options_template.cpp options_template.cpp.sed mkoptions summary.sed gen-heads-stamp -# echo "$(OPTIONS_FILES)" +options.cpp : options_template.cpp options_template.cpp.sed mkoptions summary.sed $(OPTIONS_HEADS) options_holder.h $(AM_V_at)chmod +x @srcdir@/mkoptions $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ @srcdir@/options_template.cpp \ @@ -261,15 +416,21 @@ options.cpp : options_template.cpp options_template.cpp.sed mkoptions summary.se # mkoptions apply-sed-to-template sed-file template-file -../smt/smt_options.cpp : ../smt/smt_options_template.cpp ../smt/smt_options_template.cpp.sed mkoptions summary.sed gen-heads-stamp -# echo "$(OPTIONS_FILES)" +options_handler_get_option.cpp : options_handler_get_option_template.cpp options_handler_get_option_template.cpp.sed mkoptions summary.sed $(OPTIONS_HEADS) $(AM_V_at)chmod +x @srcdir@/mkoptions $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ - @srcdir@/../smt/smt_options_template.cpp \ - @builddir@/../smt/smt_options_template.cpp.sed \ + @srcdir@/options_handler_get_option_template.cpp \ + @builddir@/options_handler_get_option_template.cpp.sed \ summary.sed \ ) > "$@" +options_handler_set_option.cpp : options_handler_set_option_template.cpp options_handler_set_option_template.cpp.sed mkoptions summary.sed $(OPTIONS_HEADS) + $(AM_V_at)chmod +x @srcdir@/mkoptions + $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ + @srcdir@/options_handler_set_option_template.cpp \ + @builddir@/options_handler_set_option_template.cpp.sed \ + summary.sed \ + ) > "$@" @@ -285,7 +446,7 @@ $(DOCUMENTATION_FILES) : % : %_template %_template.sed mkoptions summary.sed -#options-stamp: options_holder_template.h options_template.cpp ../smt/smt_options_template.cpp base_options_template.h base_options_template.cpp mkoptions $(OPTIONS_FILE_SRCS) +#options-stamp: options_holder_template.h options_template.cpp smt_options_template.cpp base_options_template.h base_options_template.cpp mkoptions $(OPTIONS_FILE_SRCS) # This rule is ugly. It's needed to ensure that automake's dependence @@ -294,65 +455,3 @@ $(DOCUMENTATION_FILES) : % : %_template %_template.sed mkoptions summary.sed # fails. %.Plo:; $(MKDIR_P) "$(dir $@)" && : > "$@" -# Tim: -# This is insanely ugly and brittle! -# *Any* proposal to clean this up is welcomed! -# We are overloading automake's default distclean here. We have to overload -# distclean because otherwise it deletes the dependency directory -# "src/expr/.deps", then when running make distclean in src/expr it attempts to -# include .Plo files "defined in src/expr/.deps". -# An example from src/expr/Makefile.ina : -# @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/attribute.Plo@am__quote@ -# The include must fail because this make file deleted that directory and -# distclean cannot proceed. So we override distclean to only remove -# "-rm -rf ./$(DEPDIR)". We then do manual massaging to finish up removing the -# extra files. To reproduce this, you can comment out the distclean below, run -# a distcheck and repeat this process. -# Why was this not a problem before? I do not know. -MANUAL_RM = \ - $(CLEANFILES) \ - ../main/.dirstamp \ - ../expr/.dirstamp \ - ../options/options.lo \ - ../options/base_options.lo \ - ../options/.libs/options.o \ - ../options/.libs/base_options.o \ - ../options/.libs/liboptions.a \ - ../options/Trace_tags.tmp \ - ../options/Debug_tags.tmp \ - ../options/liboptions.la \ - ../parser/.dirstamp \ - ../expr/.deps/options.Plo \ - ../main/.deps/options.Plo \ - ../parser/.deps/options.Plo \ - ../prop/options.lo \ - ../decision/options.lo \ - ../printer/options.lo \ - ../proof/options.lo \ - ../smt/options.lo \ - ../theory/arith/options.lo \ - ../theory/arrays/options.lo \ - ../theory/booleans/options.lo \ - ../theory/builtin/options.lo \ - ../theory/bv/options.lo \ - ../theory/datatypes/options.lo \ - ../theory/fp/options.lo \ - ../theory/idl/options.lo \ - ../theory/quantifiers/options.lo \ - ../theory/sets/options.lo \ - ../theory/strings/options.lo \ - ../theory/test_newalttheory/options.lo \ - ../theory/test_newtheory/options.lo \ - ../theory/uf/options.lo \ - ../theory/options.lo - - - -distclean: - -rm -rf ./$(DEPDIR) - -rm -f Makefile - -rm -f $(MANUAL_RM) - -.PHONY: exprs-builts -exprs-builts:; $(AM_V_at)[ "$(FROM_EXPR)" != 1 ] && $(MAKE) -C ../expr builts || true - diff --git a/src/options/arith_heuristic_pivot_rule.cpp b/src/options/arith_heuristic_pivot_rule.cpp new file mode 100644 index 000000000..ff5f2102a --- /dev/null +++ b/src/options/arith_heuristic_pivot_rule.cpp @@ -0,0 +1,40 @@ +/********************* */ +/*! \file arith_heuristic_pivot_rule.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: Tim King + ** 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 "options/arith_heuristic_pivot_rule.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, ErrorSelectionRule rule) { + switch(rule) { + case MINIMUM_AMOUNT: + out << "MINIMUM_AMOUNT"; + break; + case VAR_ORDER: + out << "VAR_ORDER"; + break; + case MAXIMUM_AMOUNT: + out << "MAXIMUM_AMOUNT"; + break; + default: + out << "ArithHeuristicPivotRule!UNKNOWN"; + } + + return out; +} + +}/* CVC4 namespace */ diff --git a/src/options/arith_heuristic_pivot_rule.h b/src/options/arith_heuristic_pivot_rule.h new file mode 100644 index 000000000..e44b8105b --- /dev/null +++ b/src/options/arith_heuristic_pivot_rule.h @@ -0,0 +1,38 @@ +/********************* */ +/*! \file arith_heuristic_pivot_rule.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: Tim King + ** 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__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H +#define __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H + +#include <iostream> + +namespace CVC4 { + +enum ErrorSelectionRule { + VAR_ORDER, + MINIMUM_AMOUNT, + MAXIMUM_AMOUNT, + SUM_METRIC +}; + +std::ostream& operator<<(std::ostream& out, ErrorSelectionRule rule) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H */ diff --git a/src/options/arith_options b/src/options/arith_options new file mode 100644 index 000000000..9737d5382 --- /dev/null +++ b/src/options/arith_options @@ -0,0 +1,164 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module ARITH "options/arith_options.h" Arithmetic theory + +option arithUnateLemmaMode --unate-lemmas=MODE ArithUnateLemmaMode :handler CVC4::options::stringToArithUnateLemmaMode :default ALL_PRESOLVE_LEMMAS :handler-include "options/options_handler_interface.h" :include "options/arith_unate_lemma_mode.h" + determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help) + +option arithPropagationMode --arith-prop=MODE ArithPropagationMode :handler CVC4::options::stringToArithPropagationMode :default BOTH_PROP :handler-include "options/options_handler_interface.h" :include "options/arith_propagation_mode.h" + turns on arithmetic propagation (default is 'old', see --arith-prop=help) + +# The maximum number of difference pivots to do per invocation of simplex. +# If this is negative, the number of pivots done is the number of variables. +# If this is not set by the user, different logics are free to chose different +# defaults. +option arithHeuristicPivots --heuristic-pivots=N int16_t :default 0 :read-write + the number of times to apply the heuristic pivot rule; if N < 0, this defaults to the number of variables; if this is unset, this is tuned by the logic selection + +# The maximum number of variable order pivots to do per invocation of simplex. +# If this is negative, the number of pivots done is unlimited. +# If this is not set by the user, different logics are free to chose different +# defaults. +expert-option arithStandardCheckVarOrderPivots --standard-effort-variable-order-pivots=N int16_t :default -1 :read-write + limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule + +option arithErrorSelectionRule --error-selection-rule=RULE ErrorSelectionRule :handler CVC4::options::stringToErrorSelectionRule :default MINIMUM_AMOUNT :handler-include "options/options_handler_interface.h" :include "options/arith_heuristic_pivot_rule.h" + change the pivot rule for the basic variable (default is 'min', see --pivot-rule help) + +# The number of pivots before simplex rechecks every basic variable for a conflict +option arithSimplexCheckPeriod --simplex-check-period=N uint16_t :default 200 + the number of pivots to do in simplex before rechecking for a conflict on all variables + +# This is the pivots per basic variable that can be done using heuristic choices +# before variable order must be used. +# If this is not set by the user, different logics are free to chose different +# defaults. +option arithPivotThreshold --pivot-threshold=N uint16_t :default 2 :read-write + sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order + +option arithPropagateMaxLength --prop-row-length=N uint16_t :default 16 + sets the maximum row length to be used in propagation + +option arithDioSolver /--disable-dio-solver bool :default true + turns off Linear Diophantine Equation solver (Griggio, JSAT 2012) + +# Whether to split (= x y) into (and (<= x y) (>= x y)) in +# arithmetic preprocessing. +option arithRewriteEq --enable-arith-rewrite-equalities/--disable-arith-rewrite-equalities bool :default false :read-write + turns on the preprocessing rewrite turning equalities into a conjunction of inequalities +/turns off the preprocessing rewrite turning equalities into a conjunction of inequalities + + +option arithMLTrick miplib-trick --enable-miplib-trick/--disable-miplib-trick bool :default false + turns on the preprocessing step of attempting to infer bounds on miplib problems +/turns off the preprocessing step of attempting to infer bounds on miplib problems + +option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs=N unsigned :default 1 + do substitution for miplib 'tmp' vars if defined in <= N eliminated vars + +option doCutAllBounded --cut-all-bounded bool :default false :read-write + turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds +/turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds + +option maxCutsInContext --maxCutsInContext unsigned :default 65535 + maximum cuts in a given context before signalling a restart + +option revertArithModels --revert-arith-models-on-unsat bool :default false + revert the arithmetic model to a known safe model on unsat if one is cached + +option havePenalties --fc-penalties bool :default false :read-write + turns on degenerate pivot penalties +/turns off degenerate pivot penalties + +option useFC --use-fcsimplex bool :default false :read-write + use focusing and converging simplex (FMCAD 2013 submission) + +option useSOI --use-soi bool :default false :read-write + use sum of infeasibility simplex (FMCAD 2013 submission) + +option restrictedPivots --restrict-pivots bool :default true :read-write + have a pivot cap for simplex at effort levels below fullEffort + +option collectPivots --collect-pivot-stats bool :default false :read-write + collect the pivot history + +option useApprox --use-approx bool :default false :read-write + attempt to use an approximate solver + +option maxApproxDepth --approx-branch-depth int16_t :default 200 :read-write + maximum branch depth the approximate solver is allowed to take + +option exportDioDecompositions --dio-decomps bool :default false :read-write + let skolem variables for integer divisibility constraints leak from the dio solver + +option newProp --new-prop bool :default false :read-write + use the new row propagation system + +option arithPropAsLemmaLength --arith-prop-clauses uint16_t :default 8 :read-write + rows shorter than this are propagated as clauses + +option soiQuickExplain --soi-qe bool :default false :read-write + use quick explain to minimize the sum of infeasibility conflicts + +option rewriteDivk rewrite-divk --rewrite-divk bool :default false :read-write + rewrite division and mod when by a constant into linear terms + +option trySolveIntStandardEffort --se-solve-int bool :default false + attempt to use the approximate solve integer method on standard effort + +option replayFailureLemma --lemmas-on-replay-failure bool :default false + attempt to use external lemmas if approximate solve integer failed + +option dioSolverTurns --dio-turns int :default 10 + turns in a row dio solver cutting gets + +option rrTurns --rr-turns int :default 3 + round robin turn + +option dioRepeat --dio-repeat bool :default false + handle dio solver constraints in mass or one at a time + +option replayEarlyCloseDepths --replay-early-close-depth int :default 1 + multiples of the depths to try to close the approx log eagerly + +option replayFailurePenalty --replay-failure-penalty int :default 100 + number of solve integer attempts to skips after a numeric failure + +option replayNumericFailurePenalty --replay-num-err-penalty int :default 4194304 + number of solve integer attempts to skips after a numeric failure + +option replayRejectCutSize --replay-reject-cut unsigned :default 25500 + maximum complexity of any coefficient while replaying cuts + +option lemmaRejectCutSize --replay-lemma-reject-cut unsigned :default 25500 + maximum complexity of any coefficient while outputing replaying cut lemmas + +option soiApproxMajorFailure --replay-soi-major-threshold double :default .01 + threshold for a major tolerance failure by the approximate solver + +option soiApproxMajorFailurePen --replay-soi-major-threshold-pen int :default 50 + threshold for a major tolerance failure by the approximate solver + +option soiApproxMinorFailure --replay-soi-minor-threshold double :default .0001 + threshold for a minor tolerance failure by the approximate solver + +option soiApproxMinorFailurePen --replay-soi-minor-threshold-pen int :default 10 + threshold for a minor tolerance failure by the approximate solver + +option ppAssertMaxSubSize --pp-assert-max-sub-size unsigned :default 2 + threshold for substituting an equality in ppAssert + +option maxReplayTree --max-replay-tree int :default 512 + threshold for attempting to replay a tree + + +option pbRewrites --pb-rewrites bool :default false + apply pseudo boolean rewrites + +option pbRewriteThreshold --pb-rewrite-threshold int :default 256 + threshold of number of pseudoboolean variables to have before doing rewrites + +endmodule diff --git a/src/options/arith_propagation_mode.cpp b/src/options/arith_propagation_mode.cpp new file mode 100644 index 000000000..7f18a0356 --- /dev/null +++ b/src/options/arith_propagation_mode.cpp @@ -0,0 +1,43 @@ +/********************* */ +/*! \file arith_propagation_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 "options/arith_propagation_mode.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, ArithPropagationMode mode) { + switch(mode) { + case NO_PROP: + out << "NO_PROP"; + break; + case UNATE_PROP: + out << "UNATE_PROP"; + break; + case BOUND_INFERENCE_PROP: + out << "BOUND_INFERENCE_PROP"; + break; + case BOTH_PROP: + out << "BOTH_PROP"; + break; + default: + out << "ArithPropagationMode!UNKNOWN"; + } + + return out; +} + +}/* CVC4 namespace */ diff --git a/src/options/arith_propagation_mode.h b/src/options/arith_propagation_mode.h new file mode 100644 index 000000000..fa89496f0 --- /dev/null +++ b/src/options/arith_propagation_mode.h @@ -0,0 +1,38 @@ +/********************* */ +/*! \file arith_propagation_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__THEORY__ARITH__ARITH_PROPAGATION_MODE_H +#define __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H + +#include <iostream> + +namespace CVC4 { + +enum ArithPropagationMode { + NO_PROP, + UNATE_PROP, + BOUND_INFERENCE_PROP, + BOTH_PROP +}; + +std::ostream& operator<<(std::ostream& out, ArithPropagationMode rule) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H */ diff --git a/src/options/arith_unate_lemma_mode.cpp b/src/options/arith_unate_lemma_mode.cpp new file mode 100644 index 000000000..55fd8a01f --- /dev/null +++ b/src/options/arith_unate_lemma_mode.cpp @@ -0,0 +1,43 @@ +/********************* */ +/*! \file arith_unate_lemma_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 "options/arith_unate_lemma_mode.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, ArithUnateLemmaMode mode) { + switch(mode) { + case NO_PRESOLVE_LEMMAS: + out << "NO_PRESOLVE_LEMMAS"; + break; + case INEQUALITY_PRESOLVE_LEMMAS: + out << "INEQUALITY_PRESOLVE_LEMMAS"; + break; + case EQUALITY_PRESOLVE_LEMMAS: + out << "EQUALITY_PRESOLVE_LEMMAS"; + break; + case ALL_PRESOLVE_LEMMAS: + out << "ALL_PRESOLVE_LEMMAS"; + break; + default: + out << "ArithUnateLemmaMode!UNKNOWN"; + } + + return out; +} + +}/* CVC4 namespace */ diff --git a/src/options/arith_unate_lemma_mode.h b/src/options/arith_unate_lemma_mode.h new file mode 100644 index 000000000..5e1362bcb --- /dev/null +++ b/src/options/arith_unate_lemma_mode.h @@ -0,0 +1,38 @@ +/********************* */ +/*! \file arith_unate_lemma_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__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H +#define __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H + +#include <iostream> + +namespace CVC4 { + +typedef enum { + NO_PRESOLVE_LEMMAS, + INEQUALITY_PRESOLVE_LEMMAS, + EQUALITY_PRESOLVE_LEMMAS, + ALL_PRESOLVE_LEMMAS +} ArithUnateLemmaMode; + +std::ostream& operator<<(std::ostream& out, ArithUnateLemmaMode rule) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H */ diff --git a/src/options/arrays_options b/src/options/arrays_options new file mode 100644 index 000000000..096d773ca --- /dev/null +++ b/src/options/arrays_options @@ -0,0 +1,32 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module ARRAYS "options/arrays_options.h" Arrays theory + +option arraysOptimizeLinear --arrays-optimize-linear bool :default true :read-write + turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper) + +option arraysLazyRIntro1 --arrays-lazy-rintro1 bool :default true :read-write + turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination) + +option arraysModelBased --arrays-model-based bool :default false :read-write + turn on model-based array solver + +option arraysEagerIndexSplitting --arrays-eager-index bool :default true :read-write + turn on eager index splitting for generated array lemmas + +option arraysEagerLemmas --arrays-eager-lemmas bool :default false :read-write + turn on eager lemma generation for arrays + +option arraysConfig --arrays-config int :default 0 :read-write + set different array option configurations - for developers only + +option arraysReduceSharing --arrays-reduce-sharing bool :default false :read-write + use model information to reduce size of care graph for arrays + +option arraysPropagate --arrays-prop int :default 2 :read-write + propagation effort for arrays: 0 is none, 1 is some, 2 is full + +endmodule diff --git a/src/options/base_handlers.h b/src/options/base_handlers.h new file mode 100644 index 000000000..b37dde5c6 --- /dev/null +++ b/src/options/base_handlers.h @@ -0,0 +1,85 @@ +/********************* */ +/*! \file base_handlers.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: Kshitij Bansal + ** 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_private.h" + +#ifndef __CVC4__BASE_HANDLERS_H +#define __CVC4__BASE_HANDLERS_H + +#include <iostream> +#include <string> +#include <sstream> + +namespace CVC4 { +namespace options { + +template <template <class U> class Cmp> +class comparator { + long d_lbound; + double d_dbound; + bool d_hasLbound; + +public: + comparator(int i) throw() : d_lbound(i), d_dbound(0.0), d_hasLbound(true) {} + comparator(long l) throw() : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {} + comparator(double d) throw() : d_lbound(0), d_dbound(d), d_hasLbound(false) {} + + template <class T> + void operator()(std::string option, const T& value, OptionsHandler* handler) { + if((d_hasLbound && !(Cmp<T>()(value, T(d_lbound)))) || + (!d_hasLbound && !(Cmp<T>()(value, T(d_dbound))))) { + std::stringstream ss; + ss << option << ": " << value << " is not a legal setting"; + throw OptionException(ss.str()); + } + } +};/* class comparator */ + +struct greater : public comparator<std::greater> { + greater(int i) throw() : comparator<std::greater>(i) {} + greater(long l) throw() : comparator<std::greater>(l) {} + greater(double d) throw() : comparator<std::greater>(d) {} +};/* struct greater */ + +struct greater_equal : public comparator<std::greater_equal> { + greater_equal(int i) throw() : comparator<std::greater_equal>(i) {} + greater_equal(long l) throw() : comparator<std::greater_equal>(l) {} + greater_equal(double d) throw() : comparator<std::greater_equal>(d) {} +};/* struct greater_equal */ + +struct less : public comparator<std::less> { + less(int i) throw() : comparator<std::less>(i) {} + less(long l) throw() : comparator<std::less>(l) {} + less(double d) throw() : comparator<std::less>(d) {} +};/* struct less */ + +struct less_equal : public comparator<std::less_equal> { + less_equal(int i) throw() : comparator<std::less_equal>(i) {} + less_equal(long l) throw() : comparator<std::less_equal>(l) {} + less_equal(double d) throw() : comparator<std::less_equal>(d) {} +};/* struct less_equal */ + +struct not_equal : public comparator<std::not_equal_to> { + not_equal(int i) throw() : comparator<std::not_equal_to>(i) {} + not_equal(long l) throw() : comparator<std::not_equal_to>(l) {} + not_equal(double d) throw() : comparator<std::not_equal_to>(d) {} +};/* struct not_equal_to */ + +}/* CVC4::options namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__BASE_HANDLERS_H */ diff --git a/src/options/base_options b/src/options/base_options index ed94e68f6..588220817 100644 --- a/src/options/base_options +++ b/src/options/base_options @@ -85,9 +85,9 @@ option in std::istream* :default &std::cin :include <iostream> option out std::ostream* :default &std::cout :include <iostream> option err std::ostream* :default &std::cerr :include <iostream> -common-option inputLanguage input-language -L --lang=LANG InputLanguage :handler CVC4::options::stringToInputLanguage :include "util/language.h" :default language::input::LANG_AUTO :read-write +common-option inputLanguage input-language -L --lang=LANG InputLanguage :handler CVC4::options::stringToInputLanguage :include "options/language.h" :default language::input::LANG_AUTO :read-write force input language (default is "auto"; see --lang help) -common-option outputLanguage output-language --output-lang=LANG OutputLanguage :handler CVC4::options::stringToOutputLanguage :include "util/language.h" :default language::output::LANG_AUTO :read-write +common-option outputLanguage output-language --output-lang=LANG OutputLanguage :handler CVC4::options::stringToOutputLanguage :include "options/language.h" :default language::output::LANG_AUTO :read-write force output language (default is "auto"; see --output-lang help) option languageHelp bool @@ -96,14 +96,14 @@ option languageHelp bool undocumented-alias --language=L = --lang=L undocumented-alias --output-language=L = --output-lang=L -option verbosity verbosity int :read-write :default 0 :predicate CVC4::options::setVerbosity :predicate-include "options/base_options_handlers.h" +option verbosity verbosity int :read-write :default 0 :predicate CVC4::options::setVerbosity :predicate-include "options/base_handlers.h" the verbosity level of CVC4 common-option - -v --verbose void :handler CVC4::options::increaseVerbosity increase verbosity (may be repeated) common-option - -q --quiet void :handler CVC4::options::decreaseVerbosity decrease verbosity (may be repeated) -common-option statistics statistics --stats bool :predicate CVC4::smt::statsEnabledBuild :predicate-include "smt/options_handlers.h" +common-option statistics statistics --stats bool :predicate CVC4::options::statsEnabledBuild :predicate-include "options/options_handler_interface.h" give statistics on exit undocumented-alias --statistics = --stats undocumented-alias --no-statistics = --no-stats @@ -128,7 +128,7 @@ option - trace -t --trace=TAG argument :handler CVC4::options::addTraceTag option - debug -d --debug=TAG argument :handler CVC4::options::addDebugTag debug something (e.g. -d arith), can repeat -option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/base_options_handlers.h" +option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/options_handler_interface.h" print the "success" output required of SMT-LIBv2 alias --smtlib-strict = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --abstract-values diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h deleted file mode 100644 index ac3194f29..000000000 --- a/src/options/base_options_handlers.h +++ /dev/null @@ -1,241 +0,0 @@ -/********************* */ -/*! \file base_options_handlers.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Kshitij Bansal - ** 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_private.h" - -#ifndef __CVC4__BASE_OPTIONS_HANDLERS_H -#define __CVC4__BASE_OPTIONS_HANDLERS_H - -#include <iostream> -#include <string> -#include <sstream> - -#include "expr/command.h" -#include "util/didyoumean.h" -#include "util/language.h" - -namespace CVC4 { -namespace options { - -inline void setVerbosity(std::string option, int value, SmtEngine* smt) 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); - } - } -} - -inline void increaseVerbosity(std::string option, SmtEngine* smt) { - options::verbosity.set(options::verbosity() + 1); - setVerbosity(option, options::verbosity(), smt); -} - -inline void decreaseVerbosity(std::string option, SmtEngine* smt) { - options::verbosity.set(options::verbosity() - 1); - setVerbosity(option, options::verbosity(), smt); -} - -inline OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, SmtEngine* smt) 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(); -} - -inline InputLanguage stringToInputLanguage(std::string option, std::string optarg, SmtEngine* smt) 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(); -} - -inline std::string suggestTags(char const* const* validTags, std::string inputTag, - char const* const* additionalTags = NULL) -{ - 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); -} - -inline void addTraceTag(std::string option, std::string optarg, SmtEngine* smt) { - 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); -} - -inline void addDebugTag(std::string option, std::string optarg, SmtEngine* smt) { - 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); -} - -inline void setPrintSuccess(std::string option, bool value, SmtEngine* smt) { - 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); -} - -template <template <class U> class Cmp> -class comparator { - long d_lbound; - double d_dbound; - bool d_hasLbound; - -public: - comparator(int i) throw() : d_lbound(i), d_dbound(0.0), d_hasLbound(true) {} - comparator(long l) throw() : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {} - comparator(double d) throw() : d_lbound(0), d_dbound(d), d_hasLbound(false) {} - - template <class T> - void operator()(std::string option, const T& value, SmtEngine* smt) { - if((d_hasLbound && !(Cmp<T>()(value, T(d_lbound)))) || - (!d_hasLbound && !(Cmp<T>()(value, T(d_dbound))))) { - std::stringstream ss; - ss << option << ": " << value << " is not a legal setting"; - throw OptionException(ss.str()); - } - } -};/* class comparator */ - -struct greater : public comparator<std::greater> { - greater(int i) throw() : comparator<std::greater>(i) {} - greater(long l) throw() : comparator<std::greater>(l) {} - greater(double d) throw() : comparator<std::greater>(d) {} -};/* struct greater */ - -struct greater_equal : public comparator<std::greater_equal> { - greater_equal(int i) throw() : comparator<std::greater_equal>(i) {} - greater_equal(long l) throw() : comparator<std::greater_equal>(l) {} - greater_equal(double d) throw() : comparator<std::greater_equal>(d) {} -};/* struct greater_equal */ - -struct less : public comparator<std::less> { - less(int i) throw() : comparator<std::less>(i) {} - less(long l) throw() : comparator<std::less>(l) {} - less(double d) throw() : comparator<std::less>(d) {} -};/* struct less */ - -struct less_equal : public comparator<std::less_equal> { - less_equal(int i) throw() : comparator<std::less_equal>(i) {} - less_equal(long l) throw() : comparator<std::less_equal>(l) {} - less_equal(double d) throw() : comparator<std::less_equal>(d) {} -};/* struct less_equal */ - -struct not_equal : public comparator<std::not_equal_to> { - not_equal(int i) throw() : comparator<std::not_equal_to>(i) {} - not_equal(long l) throw() : comparator<std::not_equal_to>(l) {} - not_equal(double d) throw() : comparator<std::not_equal_to>(d) {} -};/* struct not_equal_to */ - -}/* CVC4::options namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__BASE_OPTIONS_HANDLERS_H */ - diff --git a/src/options/boolean_term_conversion_mode.cpp b/src/options/boolean_term_conversion_mode.cpp new file mode 100644 index 000000000..efeb3ab16 --- /dev/null +++ b/src/options/boolean_term_conversion_mode.cpp @@ -0,0 +1,42 @@ +/********************* */ +/*! \file boolean_term_conversion_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 "options/boolean_term_conversion_mode.h" + +#include <iostream> + + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) { + switch(mode) { + case theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS: + out << "BOOLEAN_TERM_CONVERT_TO_BITVECTORS"; + break; + case theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES: + out << "BOOLEAN_TERM_CONVERT_TO_DATATYPES"; + break; + case theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE: + out << "BOOLEAN_TERM_CONVERT_NATIVE"; + break; + default: + out << "BooleanTermConversionMode!UNKNOWN"; + } + + return out; +} + +}/* CVC4 namespace */ diff --git a/src/options/boolean_term_conversion_mode.h b/src/options/boolean_term_conversion_mode.h new file mode 100644 index 000000000..5671dea13 --- /dev/null +++ b/src/options/boolean_term_conversion_mode.h @@ -0,0 +1,53 @@ +/********************* */ +/*! \file boolean_term_conversion_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_private.h" + +#ifndef __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H +#define __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H + +#include <iostream> + +namespace CVC4 { +namespace theory { +namespace booleans { + +typedef enum { + /** + * Convert Boolean terms to bitvectors of size 1. + */ + BOOLEAN_TERM_CONVERT_TO_BITVECTORS, + /** + * Convert Boolean terms to enumerations in the Datatypes theory. + */ + BOOLEAN_TERM_CONVERT_TO_DATATYPES, + /** + * Convert Boolean terms to enumerations in the Datatypes theory IF + * used in a datatypes context, otherwise to a bitvector of size 1. + */ + BOOLEAN_TERM_CONVERT_NATIVE + +} BooleanTermConversionMode; + +}/* CVC4::theory::booleans namespace */ +}/* CVC4::theory namespace */ + +std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H */ diff --git a/src/options/booleans_options b/src/options/booleans_options new file mode 100644 index 000000000..2e2cbee1f --- /dev/null +++ b/src/options/booleans_options @@ -0,0 +1,11 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module BOOLEANS "options/booleans_options.h" Boolean theory + +option booleanTermConversionMode boolean-term-conversion-mode --boolean-term-conversion-mode=MODE CVC4::theory::booleans::BooleanTermConversionMode :default CVC4::theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS :include "options/boolean_term_conversion_mode.h" :handler CVC4::options::stringToBooleanTermConversionMode :handler-include "options/options_handler_interface.h" + policy for converting Boolean terms + +endmodule diff --git a/src/options/builtin_options b/src/options/builtin_options new file mode 100644 index 000000000..ea4229b67 --- /dev/null +++ b/src/options/builtin_options @@ -0,0 +1,8 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module BUILTIN "options/builtin_options.h" Builtin theory + +endmodule diff --git a/src/options/bv_bitblast_mode.cpp b/src/options/bv_bitblast_mode.cpp new file mode 100644 index 000000000..9576134f6 --- /dev/null +++ b/src/options/bv_bitblast_mode.cpp @@ -0,0 +1,54 @@ +/********************* */ +/*! \file bitblast_mode.cpp + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Bitblast modes for bit-vector solver. + ** + ** Bitblast modes for bit-vector solver. + **/ + +#include "options/bv_bitblast_mode.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode) { + switch(mode) { + case theory::bv::BITBLAST_MODE_LAZY: + out << "BITBLAST_MODE_LAZY"; + break; + case theory::bv::BITBLAST_MODE_EAGER: + out << "BITBLAST_MODE_EAGER"; + break; + default: + out << "BitblastMode:UNKNOWN![" << unsigned(mode) << "]"; + } + + return out; +} + +std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode) { + switch(mode) { + case theory::bv::BITVECTOR_SLICER_ON: + out << "BITVECTOR_SLICER_ON"; + break; + case theory::bv::BITVECTOR_SLICER_OFF: + out << "BITVECTOR_SLICER_OFF"; + break; + case theory::bv::BITVECTOR_SLICER_AUTO: + out << "BITVECTOR_SLICER_AUTO"; + break; + default: + out << "BvSlicerMode:UNKNOWN![" << unsigned(mode) << "]"; + } + + return out; +} + +}/* CVC4 namespace */ diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h new file mode 100644 index 000000000..89ecdc381 --- /dev/null +++ b/src/options/bv_bitblast_mode.h @@ -0,0 +1,72 @@ +/********************* */ +/*! \file bitblast_mode.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Bitblasting modes for bit-vector solver. + ** + ** Bitblasting modes for bit-vector solver. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BV__BITBLAST_MODE_H +#define __CVC4__THEORY__BV__BITBLAST_MODE_H + +#include <iostream> + +namespace CVC4 { +namespace theory { +namespace bv { + +/** Enumeration of bit-blasting modes */ +enum BitblastMode { + + /** + * Lazy bit-blasting that separates boolean reasoning + * from term reasoning. + */ + BITBLAST_MODE_LAZY, + + /** + * Bit-blast eagerly to the bit-vector SAT solver. + */ + BITBLAST_MODE_EAGER +};/* enum BitblastMode */ + +/** Enumeration of bit-vector equality slicer mode */ +enum BvSlicerMode { + + /** + * Force the slicer on. + */ + BITVECTOR_SLICER_ON, + + /** + * Slicer off. + */ + BITVECTOR_SLICER_OFF, + + /** + * Auto enable slicer if problem has only equalities. + */ + BITVECTOR_SLICER_AUTO + +};/* enum BvSlicerMode */ + + +}/* CVC4::theory::bv namespace */ +}/* CVC4::theory namespace */ + +std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__BV__BITBLAST_MODE_H */ diff --git a/src/options/bv_options b/src/options/bv_options new file mode 100644 index 000000000..73790b562 --- /dev/null +++ b/src/options/bv_options @@ -0,0 +1,69 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module BV "options/bv_options.h" Bitvector theory + +# Option to set the bit-blasting mode (lazy, eager) + +option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :handler CVC4::options::stringToBitblastMode :default CVC4::theory::bv::BITBLAST_MODE_LAZY :read-write :include "options/bv_bitblast_mode.h" :handler-include "options/options_handler_interface.h" + choose bitblasting mode, see --bitblast=help + +# Options for eager bit-blasting + +option bitvectorAig --bitblast-aig bool :default false :predicate CVC4::options::abcEnabledBuild CVC4::options::setBitblastAig :predicate-include "options/options_handler_interface.h" :read-write + bitblast by first converting to AIG (implies --bitblast=eager) +expert-option bitvectorAigSimplifications --bv-aig-simp=COMMAND std::string :default "" :predicate CVC4::options::abcEnabledBuild :read-write :link --bitblast-aig :link-smt bitblast-aig + abc command to run AIG simplifications (implies --bitblast-aig, default is "balance;drw") + +# Options for lazy bit-blasting + +option bitvectorPropagate --bv-propagate bool :default true :read-write :link --bitblast=lazy + use bit-vector propagation in the bit-blaster + +option bitvectorEqualitySolver --bv-eq-solver bool :default true :read-write :link --bitblast=lazy + use the equality engine for the bit-vector theory (only if --bitblast=lazy) + +option bitvectorEqualitySlicer --bv-eq-slicer=MODE CVC4::theory::bv::BvSlicerMode :handler CVC4::options::stringToBvSlicerMode :default CVC4::theory::bv::BITVECTOR_SLICER_OFF :read-write :include "options/bv_bitblast_mode.h" :handler-include "options/options_handler_interface.h" :read-write :link --bv-eq-solver + turn on the slicing equality solver for the bit-vector theory (only if --bitblast=lazy) + +option bitvectorInequalitySolver --bv-inequality-solver bool :default true :read-write :link --bitblast=lazy + turn on the inequality solver for the bit-vector theory (only if --bitblast=lazy) + +option bitvectorAlgebraicSolver --bv-algebraic-solver bool :default true :read-write :link --bitblast=lazy + turn on the algebraic solver for the bit-vector theory (only if --bitblast=lazy) + +expert-option bitvectorAlgebraicBudget --bv-algebraic-budget unsigned :default 1500 :read-write :link --bv-algebraic-solver + the budget allowed for the algebraic solver in number of SAT conflicts + +# General options + +option bitvectorToBool --bv-to-bool bool :default false :read-write + lift bit-vectors of size 1 to booleans when possible + +option bitvectorDivByZeroConst --bv-div-zero-const bool :default false :read-write + always return -1 on division by zero + +expert-option bvExtractArithRewrite --bv-extract-arith bool :default false :read-write + enable rewrite pushing extract [i:0] over arithmetic operations (can blow up) + +expert-option bvAbstraction --bv-abstraction bool :default false :read-write + mcm benchmark abstraction + +expert-option skolemizeArguments --bv-skolemize bool :default false :read-write + skolemize arguments for bv abstraction (only does something if --bv-abstraction is on) + +expert-option bvNumFunc --bv-num-func=NUM unsigned :default 1 + number of function symbols in conflicts that are generalized + +expert-option bvEagerExplanations --bv-eager-explanations bool :default false :read-write + compute bit-blasting propagation explanations eagerly + +expert-option bitvectorQuickXplain --bv-quick-xplain bool :default false + minimize bv conflicts using the QuickXplain algorithm + +expert-option bvIntroducePow2 --bv-intro-pow2 bool :default false + introduce bitvector powers of two as a preprocessing pass + +endmodule diff --git a/src/options/datatypes_options b/src/options/datatypes_options new file mode 100644 index 000000000..ba700a594 --- /dev/null +++ b/src/options/datatypes_options @@ -0,0 +1,23 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module DATATYPES "options/datatypes_options.h" Datatypes theory + +# How to handle selectors applied to incorrect constructors. If this option is set, +# then we do not rewrite such a selector term to an arbitrary ground term. +# For example, by default cvc4 considers cdr( nil ) = nil. If this option is set, then +# cdr( nil ) has no set value. +expert-option dtRewriteErrorSel --dt-rewrite-error-sel bool :default false :read-write + rewrite incorrectly applied selectors to arbitrary ground term +option dtForceAssignment --dt-force-assignment bool :default false :read-write + force the datatypes solver to give specific values to all datatypes terms before answering sat +option dtBinarySplit --dt-binary-split bool :default false + do binary splits for datatype constructor types +option cdtBisimilar --cdt-bisimilar bool :default true + do bisimilarity check for co-datatypes +option dtCyclic --dt-cyclic bool :default true + do cyclicity check for datatypes + +endmodule diff --git a/src/options/decision_mode.cpp b/src/options/decision_mode.cpp new file mode 100644 index 000000000..168637e64 --- /dev/null +++ b/src/options/decision_mode.cpp @@ -0,0 +1,37 @@ +/********************* */ +/*! \file decision_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 "options/decision_mode.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode) { + switch(mode) { + case decision::DECISION_STRATEGY_INTERNAL: + out << "DECISION_STRATEGY_INTERNAL"; + break; + case decision::DECISION_STRATEGY_JUSTIFICATION: + out << "DECISION_STRATEGY_JUSTIFICATION"; + break; + default: + out << "DecisionMode:UNKNOWN![" << unsigned(mode) << "]"; + } + + return out; +} + +}/* CVC4 namespace */ diff --git a/src/options/decision_mode.h b/src/options/decision_mode.h new file mode 100644 index 000000000..fb01c587b --- /dev/null +++ b/src/options/decision_mode.h @@ -0,0 +1,64 @@ +/********************* */ +/*! \file decision_mode.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: Kshitij Bansal + ** 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_private.h" + +#ifndef __CVC4__SMT__DECISION_MODE_H +#define __CVC4__SMT__DECISION_MODE_H + +#include <iostream> + +namespace CVC4 { +namespace decision { + +/** Enumeration of decision strategies */ +enum DecisionMode { + + /** + * Decision engine doesn't do anything. Use sat solver's internal + * heuristics + */ + DECISION_STRATEGY_INTERNAL, + + /** + * Use the justification heuristic + */ + DECISION_STRATEGY_JUSTIFICATION, + + /** + * Use may-relevancy. + */ + DECISION_STRATEGY_RELEVANCY + +};/* enum DecisionMode */ + + +/** Enumeration of combining functions for computing internal weights */ +enum DecisionWeightInternal { + DECISION_WEIGHT_INTERNAL_OFF, + DECISION_WEIGHT_INTERNAL_MAX, + DECISION_WEIGHT_INTERNAL_SUM, + DECISION_WEIGHT_INTERNAL_USR1 +};/* enum DecisionInternalWeight */ + +}/* CVC4::decision namespace */ + +std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__SMT__DECISION_MODE_H */ diff --git a/src/options/decision_options b/src/options/decision_options new file mode 100644 index 000000000..35a1de1e9 --- /dev/null +++ b/src/options/decision_options @@ -0,0 +1,27 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module DECISION "options/decision_options.h" Decision heuristics + +# When/whether to use any decision strategies +option decisionMode decision-mode --decision=MODE decision::DecisionMode :handler CVC4::options::stringToDecisionMode :default decision::DECISION_STRATEGY_INTERNAL :read-write :include "options/decision_mode.h" :handler-include "options/options_handler_interface.h" + choose decision mode, see --decision=help + +# only use DE to determine when to stop, not to make decisions +option decisionStopOnly bool + +expert-option decisionThreshold --decision-threshold=N decision::DecisionWeight :default 0 :include "options/decision_weight.h" + ignore all nodes greater than threshold in first attempt to pick decision + +expert-option decisionUseWeight --decision-use-weight bool :default false + use the weight nodes (locally, by looking at children) to direct recursive search + +expert-option decisionRandomWeight --decision-random-weight=N int :default 0 + assign random weights to nodes between 0 and N-1 (0: disable) + +expert-option decisionWeightInternal --decision-weight-internal=HOW decision::DecisionWeightInternal :handler CVC4::options::stringToDecisionWeightInternal :default decision::DECISION_WEIGHT_INTERNAL_OFF :handler-include "options/options_handler_interface.h" + computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving) + +endmodule diff --git a/src/options/decision_weight.h b/src/options/decision_weight.h new file mode 100644 index 000000000..42f1d5b6d --- /dev/null +++ b/src/options/decision_weight.h @@ -0,0 +1,28 @@ +/********************* */ +/*! \file decision_weight.h + ** \verbatim + ** Original author: Kshitij Bansal + ** Major contributors: Morgan Deters + ** 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 Rewriter attributes + ** + ** Rewriter attributes. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__OPTIONS__DECISION_WEIGHT_H +#define __CVC4__OPTIONS__DECISION_WEIGHT_H + +namespace CVC4 { +namespace decision { +typedef uint64_t DecisionWeight; +}/* CVC4::decision namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__OPTIONS__DECISION_WEIGHT_H */ diff --git a/src/options/didyoumean.cpp b/src/options/didyoumean.cpp new file mode 100644 index 000000000..573ee913f --- /dev/null +++ b/src/options/didyoumean.cpp @@ -0,0 +1,157 @@ +/********************* */ +/*! \file didyoumean.cpp + ** \verbatim + ** Original author: Kshitij Bansal + ** 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 did-you-mean style suggestions + ** + ** ``What do you mean? I don't understand.'' An attempt to be more + ** helpful than that. Similar to one in git. + ** + ** There are no dependencies on CVC4 (except namespace). + **/ + +#include "options/didyoumean.h" + +#include <iostream> +#include <sstream> + +using namespace std; +namespace CVC4 { + +vector<string> DidYouMean::getMatch(string input) { + /** Magic numbers */ + const int similarityThreshold = 7; + const unsigned numMatchesThreshold = 10; + + set< pair<int, string> > scores; + vector<string> ret; + for(typeof(d_words.begin()) it = d_words.begin(); it != d_words.end(); ++it) { + string s = (*it); + if( s == input ) { + // if input matches AS-IS just return that + ret.push_back(s); + return ret; + } + int score; + if(s.compare(0, input.size(), input) == 0) { + score = 0; + } else { + score = editDistance(input, s) + 1; + } + scores.insert( make_pair(score, s) ); + } + int min_score = scores.begin()->first; + for(typeof(scores.begin()) i = scores.begin(); + i != scores.end(); ++i) { + + // add if score is overall not too big, and also not much close to + // the score of the best suggestion + if(i->first < similarityThreshold && i->first <= min_score + 1) { + ret.push_back(i->second); +#ifdef DIDYOUMEAN_DEBUG + cout << i->second << ": " << i->first << std::endl; +#endif + } + } + if(ret.size() > numMatchesThreshold ) ret.resize(numMatchesThreshold);; + return ret; +} + + +int DidYouMean::editDistance(const std::string& a, const std::string& b) +{ + // input string: a + // desired string: b + + const int swapCost = 0; + const int substituteCost = 2; + const int addCost = 1; + const int deleteCost = 3; + const int switchCaseCost = 0; + + int len1 = a.size(); + int len2 = b.size(); + + int* C[3]; + int ii; + for (ii = 0; ii < 3; ++ii) { + C[ii] = new int[len2+1]; + } + // int C[3][len2+1]; // cost + + for(int j = 0; j <= len2; ++j) { + C[0][j] = j * addCost; + } + + for(int i = 1; i <= len1; ++i) { + + int cur = i%3; + int prv = (i+2)%3; + int pr2 = (i+1)%3; + + C[cur][0] = i * deleteCost; + + for(int j = 1; j <= len2; ++j) { + + C[cur][j] = 100000000; // INF + + if(a[i-1] == b[j-1]) { + // match + C[cur][j] = std::min(C[cur][j], C[prv][j-1]); + } else if(tolower(a[i-1]) == tolower(b[j-1])){ + // switch case + C[cur][j] = std::min(C[cur][j], C[prv][j-1] + switchCaseCost); + } else { + // substitute + C[cur][j] = std::min(C[cur][j], C[prv][j-1] + substituteCost); + } + + // swap + if(i >= 2 && j >= 2 && a[i-1] == b[j-2] && a[i-2] == b[j-1]) { + C[cur][j] = std::min(C[cur][j], C[pr2][j-2] + swapCost); + } + + // add + C[cur][j] = std::min(C[cur][j], C[cur][j-1] + addCost); + + // delete + C[cur][j] = std::min(C[cur][j], C[prv][j] + deleteCost); + +#ifdef DIDYOUMEAN_DEBUG1 + std::cout << "C[" << cur << "][" << 0 << "] = " << C[cur][0] << std::endl; +#endif + } + + } + int result = C[len1%3][len2]; + for (ii = 0; ii < 3; ++ii) { + delete [] C[ii]; + } + return result; +} + +string DidYouMean::getMatchAsString(string input, int prefixNewLines, int suffixNewLines) { + vector<string> matches = getMatch(input); + ostringstream oss; + if(matches.size() > 0) { + while(prefixNewLines --> 0) { oss << endl; } + if(matches.size() == 1) { + oss << "Did you mean this?"; + } else { + oss << "Did you mean any of these?"; + } + for(unsigned i = 0; i < matches.size(); ++i) { + oss << "\n " << matches[i]; + } + while(suffixNewLines --> 0) { oss << endl; } + } + return oss.str(); +} +}/* CVC4 namespace */ diff --git a/src/options/didyoumean.h b/src/options/didyoumean.h new file mode 100644 index 000000000..2615f4d0a --- /dev/null +++ b/src/options/didyoumean.h @@ -0,0 +1,53 @@ +/********************* */ +/*! \file didyoumean.h + ** \verbatim + ** Original author: Kshitij Bansal + ** 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 did-you-mean style suggestions. + ** + ** ``What do you mean? I don't understand.'' An attempt to be more + ** helpful than that. Similar to one in git. + ** + ** There are no dependencies on CVC4 (except namespace). + **/ + +#pragma once + +#include <vector> +#include <set> +#include <string> + +namespace CVC4 { + +class DidYouMean { + typedef std::set<std::string> Words; + Words d_words; + +public: + DidYouMean() {} + ~DidYouMean() {} + + DidYouMean(Words words) : d_words(words) {} + + void addWord(std::string word) { + d_words.insert(word); + } + + std::vector<std::string> getMatch(std::string input); + + /** + * This is provided to make it easier to ensure consistency of + * output. Returned string is empty if there are no matches. + */ + std::string getMatchAsString(std::string input, int prefixNewLines = 2, int suffixNewLines = 0); +private: + int editDistance(const std::string& a, const std::string& b); +}; + +}/*CVC4 namespace*/ diff --git a/src/options/didyoumean_test.cpp b/src/options/didyoumean_test.cpp new file mode 100644 index 000000000..af3daa689 --- /dev/null +++ b/src/options/didyoumean_test.cpp @@ -0,0 +1,767 @@ +/********************* */ +/*! \file didyoumean_test.cpp + ** \verbatim + ** Original author: Kshitij Bansal + ** 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 + **/ + +// This is not built as a part of CVC4 and is not built by Makefile.am. +// Compile: g++ didyoumean_test.cpp didyoumean.cpp +// For debug compile with -DDIDYOUMEAN_DEBUG or -DDIDYOUMEAN_DEBUG1 or both + +#include "didyoumean.h" +#include <iostream> +#include <boost/foreach.hpp> +using namespace std; +using namespace CVC4; + +set<string> getDebugTags(); +set<string> getOptionStrings(); + +int main() +{ + string a, b; + + cin >> a; + cout << "Matches with debug tags:" << endl; + vector<string> ret = DidYouMean(getDebugTags()).getMatch(a); + BOOST_FOREACH(string s, ret) cout << s << endl; + cout << "Matches with option strings:" << endl; + ret = DidYouMean(getOptionStrings()).getMatch(a); + BOOST_FOREACH(string s, ret) cout << s << endl; +} + +set<string> getDebugTags() +{ + set<string> a; + a.insert("CDInsertHashMap"); + a.insert("CDTrailHashMap"); + a.insert("TrailHashMap"); + a.insert("approx"); + a.insert("approx::"); + a.insert("approx::branch"); + a.insert("approx::checkCutOnPad"); + a.insert("approx::constraint"); + a.insert("approx::gmi"); + a.insert("approx::gmiCut"); + a.insert("approx::guessIsConstructable"); + a.insert("approx::lemmas"); + a.insert("approx::mir"); + a.insert("approx::mirCut"); + a.insert("approx::nodelog"); + a.insert("approx::replayAssert"); + a.insert("approx::replayLogRec"); + a.insert("approx::soi"); + a.insert("approx::solveMIP"); + a.insert("approx::sumConstraints"); + a.insert("approx::vars"); + a.insert("arith"); + a.insert("arith::addSharedTerm"); + a.insert("arith::approx::cuts"); + a.insert("arith::arithvar"); + a.insert("arith::asVectors"); + a.insert("arith::bt"); + a.insert("arith::collectModelInfo"); + a.insert("arith::conflict"); + a.insert("arith::congruenceManager"); + a.insert("arith::congruences"); + a.insert("arith::consistency"); + a.insert("arith::consistency::comitonconflict"); + a.insert("arith::consistency::final"); + a.insert("arith::consistency::initial"); + a.insert("arith::constraint"); + a.insert("arith::dio"); + a.insert("arith::dio::ex"); + a.insert("arith::dio::max"); + a.insert("arith::div"); + a.insert("arith::dual"); + a.insert("arith::ems"); + a.insert("arith::eq"); + a.insert("arith::error::mem"); + a.insert("arith::explain"); + a.insert("arith::explainNonbasics"); + a.insert("arith::findModel"); + a.insert("arith::focus"); + a.insert("arith::hasIntegerModel"); + a.insert("arith::importSolution"); + a.insert("arith::ite"); + a.insert("arith::ite::red"); + a.insert("arith::learned"); + a.insert("arith::lemma"); + a.insert("arith::nf"); + a.insert("arith::oldprop"); + a.insert("arith::pivot"); + a.insert("arith::preprocess"); + a.insert("arith::preregister"); + a.insert("arith::presolve"); + a.insert("arith::print_assertions"); + a.insert("arith::print_model"); + a.insert("arith::prop"); + a.insert("arith::resolveOutPropagated"); + a.insert("arith::restart"); + a.insert("arith::rewriter"); + a.insert("arith::selectPrimalUpdate"); + a.insert("arith::simplex:row"); + a.insert("arith::solveInteger"); + a.insert("arith::static"); + a.insert("arith::subsumption"); + a.insert("arith::tracking"); + a.insert("arith::tracking::mid"); + a.insert("arith::tracking::post"); + a.insert("arith::tracking::pre"); + a.insert("arith::unate"); + a.insert("arith::unate::conf"); + a.insert("arith::update"); + a.insert("arith::update::select"); + a.insert("arith::value"); + a.insert("array-pf"); + a.insert("array-types"); + a.insert("arrays"); + a.insert("arrays-model-based"); + a.insert("arrays::propagate"); + a.insert("arrays::sharing"); + a.insert("attrgc"); + a.insert("basicsAtBounds"); + a.insert("bitvector"); + a.insert("bitvector-bb"); + a.insert("bitvector-bitblast"); + a.insert("bitvector-expandDefinition"); + a.insert("bitvector-model"); + a.insert("bitvector-preregister"); + a.insert("bitvector-rewrite"); + a.insert("bitvector::bitblaster"); + a.insert("bitvector::core"); + a.insert("bitvector::explain"); + a.insert("bitvector::propagate"); + a.insert("bitvector::sharing"); + a.insert("bool-flatten"); + a.insert("bool-ite"); + a.insert("boolean-terms"); + a.insert("bt"); + a.insert("builder"); + a.insert("bv-bitblast"); + a.insert("bv-core"); + a.insert("bv-core-model"); + a.insert("bv-inequality"); + a.insert("bv-inequality-explain"); + a.insert("bv-inequality-internal"); + a.insert("bv-rewrite"); + a.insert("bv-slicer"); + a.insert("bv-slicer-eq"); + a.insert("bv-slicer-uf"); + a.insert("bv-subtheory-inequality"); + a.insert("bv-to-bool"); + a.insert("bva"); + a.insert("bvminisat"); + a.insert("bvminisat::explain"); + a.insert("bvminisat::search"); + a.insert("cbqi"); + a.insert("cbqi-debug"); + a.insert("cbqi-prop-as-dec"); + a.insert("cd_set_collection"); + a.insert("cdlist"); + a.insert("cdlist:cmm"); + a.insert("cdqueue"); + a.insert("check-inst"); + a.insert("check-model::rep-checking"); + a.insert("circuit-prop"); + a.insert("cnf"); + a.insert("constructInfeasiblityFunction"); + a.insert("context"); + a.insert("current"); + a.insert("datatypes"); + a.insert("datatypes-cycle-check"); + a.insert("datatypes-cycles"); + a.insert("datatypes-cycles-find"); + a.insert("datatypes-debug"); + a.insert("datatypes-explain"); + a.insert("datatypes-gt"); + a.insert("datatypes-inst"); + a.insert("datatypes-labels"); + a.insert("datatypes-output"); + a.insert("datatypes-parametric"); + a.insert("datatypes-prereg"); + a.insert("datatypes-split"); + a.insert("decision"); + a.insert("decision::jh"); + a.insert("determineArithVar"); + a.insert("diamonds"); + a.insert("dio::push"); + a.insert("dt"); + a.insert("dt-enum"); + a.insert("dt-warn"); + a.insert("dt::propagate"); + a.insert("dualLike"); + a.insert("effortlevel"); + a.insert("ensureLiteral"); + a.insert("eq"); + a.insert("equality"); + a.insert("equality::backtrack"); + a.insert("equality::disequality"); + a.insert("equality::evaluation"); + a.insert("equality::graph"); + a.insert("equality::internal"); + a.insert("equality::trigger"); + a.insert("equalsConstant"); + a.insert("error"); + a.insert("estimateWithCFE"); + a.insert("expand"); + a.insert("export"); + a.insert("flipdec"); + a.insert("fmc-entry-trie"); + a.insert("fmc-interval-model-debug"); + a.insert("fmf-card-debug"); + a.insert("fmf-eval-debug"); + a.insert("fmf-eval-debug2"); + a.insert("fmf-exit"); + a.insert("fmf-index-order"); + a.insert("fmf-model-complete"); + a.insert("fmf-model-cons"); + a.insert("fmf-model-cons-debug"); + a.insert("fmf-model-eval"); + a.insert("fmf-model-prefs"); + a.insert("fmf-model-req"); + a.insert("focusDownToJust"); + a.insert("focusDownToLastHalf"); + a.insert("foo"); + a.insert("gaussianElimConstructTableRow"); + a.insert("gc"); + a.insert("gc:leaks"); + a.insert("getBestImpliedBound"); + a.insert("getCeiling"); + a.insert("getNewDomainValue"); + a.insert("getPropagatedLiterals"); + a.insert("getType"); + a.insert("glpk::loadVB"); + a.insert("guessCoefficientsConstructTableRow"); + a.insert("guessIsConstructable"); + a.insert("handleBorders"); + a.insert("includeBoundUpdate"); + a.insert("inst"); + a.insert("inst-engine"); + a.insert("inst-engine-ctrl"); + a.insert("inst-engine-debug"); + a.insert("inst-engine-phase-req"); + a.insert("inst-engine-stuck"); + a.insert("inst-fmf-ei"); + a.insert("inst-match-gen"); + a.insert("inst-trigger"); + a.insert("integers"); + a.insert("interactive"); + a.insert("intersectConstantIte"); + a.insert("isConst"); + a.insert("ite"); + a.insert("ite::atom"); + a.insert("ite::constantIteEqualsConstant"); + a.insert("ite::print-success"); + a.insert("ite::simpite"); + a.insert("lemma-ites"); + a.insert("lemmaInputChannel"); + a.insert("literal-matching"); + a.insert("logPivot"); + a.insert("matrix"); + a.insert("minisat"); + a.insert("minisat::lemmas"); + a.insert("minisat::pop"); + a.insert("minisat::remove-clause"); + a.insert("minisat::search"); + a.insert("miplib"); + a.insert("model"); + a.insert("model-getvalue"); + a.insert("nf::tmp"); + a.insert("nm"); + a.insert("normal-form"); + a.insert("options"); + a.insert("paranoid:check_tableau"); + a.insert("parser"); + a.insert("parser-extra"); + a.insert("parser-idt"); + a.insert("parser-param"); + a.insert("partial_model"); + a.insert("pb"); + a.insert("pickle"); + a.insert("pickler"); + a.insert("pipe"); + a.insert("portfolio::outputmode"); + a.insert("prec"); + a.insert("preemptGetopt"); + a.insert("proof:sat"); + a.insert("proof:sat:detailed"); + a.insert("prop"); + a.insert("prop-explain"); + a.insert("prop-value"); + a.insert("prop::lemmas"); + a.insert("propagateAsDecision"); + a.insert("properConflict"); + a.insert("qcf-ccbe"); + a.insert("qcf-check-inst"); + a.insert("qcf-eval"); + a.insert("qcf-match"); + a.insert("qcf-match-debug"); + a.insert("qcf-nground"); + a.insert("qint-check-debug2"); + a.insert("qint-debug"); + a.insert("qint-error"); + a.insert("qint-model-debug"); + a.insert("qint-model-debug2"); + a.insert("qint-var-order-debug2"); + a.insert("quant-arith"); + a.insert("quant-arith-debug"); + a.insert("quant-arith-simplex"); + a.insert("quant-datatypes"); + a.insert("quant-datatypes-debug"); + a.insert("quant-req-phase"); + a.insert("quant-uf-strategy"); + a.insert("quantifiers"); + a.insert("quantifiers-assert"); + a.insert("quantifiers-check"); + a.insert("quantifiers-dec"); + a.insert("quantifiers-engine"); + a.insert("quantifiers-flip"); + a.insert("quantifiers-other"); + a.insert("quantifiers-prereg"); + a.insert("quantifiers-presolve"); + a.insert("quantifiers-relevance"); + a.insert("quantifiers-sat"); + a.insert("quantifiers-substitute-debug"); + a.insert("quantifiers::collectModelInfo"); + a.insert("queueConditions"); + a.insert("rationalToCfe"); + a.insert("recentlyViolated"); + a.insert("register"); + a.insert("register::internal"); + a.insert("relevant-trigger"); + a.insert("removeFixed"); + a.insert("rl"); + a.insert("sat::minisat"); + a.insert("selectFocusImproving"); + a.insert("set_collection"); + a.insert("sets"); + a.insert("sets-assert"); + a.insert("sets-checkmodel-ignore"); + a.insert("sets-eq"); + a.insert("sets-learn"); + a.insert("sets-lemma"); + a.insert("sets-model"); + a.insert("sets-model-details"); + a.insert("sets-parent"); + a.insert("sets-pending"); + a.insert("sets-prop"); + a.insert("sets-prop-details"); + a.insert("sets-scrutinize"); + a.insert("sets-terminfo"); + a.insert("shared"); + a.insert("shared-terms-database"); + a.insert("shared-terms-database::assert"); + a.insert("sharing"); + a.insert("simple-trigger"); + a.insert("simplify"); + a.insert("smart-multi-trigger"); + a.insert("smt"); + a.insert("soi::findModel"); + a.insert("soi::selectPrimalUpdate"); + a.insert("solveRealRelaxation"); + a.insert("sort"); + a.insert("speculativeUpdate"); + a.insert("strings"); + a.insert("strings-explain"); + a.insert("strings-explain-debug"); + a.insert("strings-prereg"); + a.insert("strings-propagate"); + a.insert("substitution"); + a.insert("substitution::internal"); + a.insert("tableau"); + a.insert("te"); + a.insert("term-db-cong"); + a.insert("theory"); + a.insert("theory::assertions"); + a.insert("theory::atoms"); + a.insert("theory::bv::rewrite"); + a.insert("theory::conflict"); + a.insert("theory::explain"); + a.insert("theory::idl"); + a.insert("theory::idl::model"); + a.insert("theory::internal"); + a.insert("theory::propagate"); + a.insert("trans-closure"); + a.insert("treat-unknown-error"); + a.insert("tuprec"); + a.insert("typecheck-idt"); + a.insert("typecheck-q"); + a.insert("typecheck-r"); + a.insert("uf"); + a.insert("uf-ss"); + a.insert("uf-ss-check-region"); + a.insert("uf-ss-cliques"); + a.insert("uf-ss-debug"); + a.insert("uf-ss-disequal"); + a.insert("uf-ss-na"); + a.insert("uf-ss-region"); + a.insert("uf-ss-region-debug"); + a.insert("uf-ss-register"); + a.insert("uf-ss-sat"); + a.insert("uf::propagate"); + a.insert("uf::sharing"); + a.insert("ufgc"); + a.insert("ufsymm"); + a.insert("ufsymm:clauses"); + a.insert("ufsymm:eq"); + a.insert("ufsymm:match"); + a.insert("ufsymm:norm"); + a.insert("ufsymm:p"); + a.insert("update"); + a.insert("updateAndSignal"); + a.insert("weak"); + a.insert("whytheoryenginewhy"); + return a; +} + +set<string> getOptionStrings() +{ + const char* cmdlineOptions[] = { + "lang", + "output-lang", + "language", + "output-language", + "verbose", + "quiet", + "stats", + "no-stats", + "statistics", + "no-statistics", + "stats-every-query", + "no-stats-every-query", + "statistics-every-query", + "no-statistics-every-query", + "parse-only", + "no-parse-only", + "preprocess-only", + "no-preprocess-only", + "trace", + "debug", + "print-success", + "no-print-success", + "smtlib-strict", + "default-expr-depth", + "default-dag-thresh", + "print-expr-types", + "eager-type-checking", + "lazy-type-checking", + "no-type-checking", + "biased-ites", + "no-biased-ites", + "boolean-term-conversion-mode", + "theoryof-mode", + "use-theory", + "bitblast-eager", + "no-bitblast-eager", + "bitblast-share-lemmas", + "no-bitblast-share-lemmas", + "bitblast-eager-fullcheck", + "no-bitblast-eager-fullcheck", + "bv-inequality-solver", + "no-bv-inequality-solver", + "bv-core-solver", + "no-bv-core-solver", + "bv-to-bool", + "no-bv-to-bool", + "bv-propagate", + "no-bv-propagate", + "bv-eq", + "no-bv-eq", + "dt-rewrite-error-sel", + "no-dt-rewrite-error-sel", + "dt-force-assignment", + "unate-lemmas", + "arith-prop", + "heuristic-pivots", + "standard-effort-variable-order-pivots", + "error-selection-rule", + "simplex-check-period", + "pivot-threshold", + "prop-row-length", + "disable-dio-solver", + "enable-arith-rewrite-equalities", + "disable-arith-rewrite-equalities", + "enable-miplib-trick", + "disable-miplib-trick", + "miplib-trick-subs", + "cut-all-bounded", + "no-cut-all-bounded", + "maxCutsInContext", + "revert-arith-models-on-unsat", + "no-revert-arith-models-on-unsat", + "fc-penalties", + "no-fc-penalties", + "use-fcsimplex", + "no-use-fcsimplex", + "use-soi", + "no-use-soi", + "restrict-pivots", + "no-restrict-pivots", + "collect-pivot-stats", + "no-collect-pivot-stats", + "use-approx", + "no-use-approx", + "approx-branch-depth", + "dio-decomps", + "no-dio-decomps", + "new-prop", + "no-new-prop", + "arith-prop-clauses", + "soi-qe", + "no-soi-qe", + "rewrite-divk", + "no-rewrite-divk", + "se-solve-int", + "no-se-solve-int", + "lemmas-on-replay-failure", + "no-lemmas-on-replay-failure", + "dio-turns", + "rr-turns", + "dio-repeat", + "no-dio-repeat", + "replay-early-close-depth", + "replay-failure-penalty", + "replay-num-err-penalty", + "replay-reject-cut", + "replay-lemma-reject-cut", + "replay-soi-major-threshold", + "replay-soi-major-threshold-pen", + "replay-soi-minor-threshold", + "replay-soi-minor-threshold-pen", + "symmetry-breaker", + "no-symmetry-breaker", + "condense-function-values", + "no-condense-function-values", + "disable-uf-ss-regions", + "uf-ss-eager-split", + "no-uf-ss-eager-split", + "uf-ss-totality", + "no-uf-ss-totality", + "uf-ss-totality-limited", + "uf-ss-totality-sym-break", + "no-uf-ss-totality-sym-break", + "uf-ss-abort-card", + "uf-ss-explained-cliques", + "no-uf-ss-explained-cliques", + "uf-ss-simple-cliques", + "no-uf-ss-simple-cliques", + "uf-ss-deq-prop", + "no-uf-ss-deq-prop", + "disable-uf-ss-min-model", + "uf-ss-clique-splits", + "no-uf-ss-clique-splits", + "uf-ss-sym-break", + "no-uf-ss-sym-break", + "uf-ss-fair", + "no-uf-ss-fair", + "arrays-optimize-linear", + "no-arrays-optimize-linear", + "arrays-lazy-rintro1", + "no-arrays-lazy-rintro1", + "arrays-model-based", + "no-arrays-model-based", + "arrays-eager-index", + "no-arrays-eager-index", + "arrays-eager-lemmas", + "no-arrays-eager-lemmas", + "disable-miniscope-quant", + "disable-miniscope-quant-fv", + "disable-prenex-quant", + "disable-var-elim-quant", + "disable-ite-lift-quant", + "cnf-quant", + "no-cnf-quant", + "clause-split", + "no-clause-split", + "pre-skolem-quant", + "no-pre-skolem-quant", + "ag-miniscope-quant", + "no-ag-miniscope-quant", + "macros-quant", + "no-macros-quant", + "fo-prop-quant", + "no-fo-prop-quant", + "disable-smart-triggers", + "relevant-triggers", + "no-relevant-triggers", + "relational-triggers", + "no-relational-triggers", + "register-quant-body-terms", + "no-register-quant-body-terms", + "inst-when", + "eager-inst-quant", + "no-eager-inst-quant", + "full-saturate-quant", + "no-full-saturate-quant", + "literal-matching", + "enable-cbqi", + "no-enable-cbqi", + "cbqi-recurse", + "no-cbqi-recurse", + "user-pat", + "flip-decision", + "disable-quant-internal-reps", + "finite-model-find", + "no-finite-model-find", + "mbqi", + "mbqi-one-inst-per-round", + "no-mbqi-one-inst-per-round", + "mbqi-one-quant-per-round", + "no-mbqi-one-quant-per-round", + "fmf-inst-engine", + "no-fmf-inst-engine", + "disable-fmf-inst-gen", + "fmf-inst-gen-one-quant-per-round", + "no-fmf-inst-gen-one-quant-per-round", + "fmf-fresh-dc", + "no-fmf-fresh-dc", + "disable-fmf-fmc-simple", + "fmf-bound-int", + "no-fmf-bound-int", + "axiom-inst", + "quant-cf", + "no-quant-cf", + "quant-cf-mode", + "quant-cf-when", + "rewrite-rules", + "no-rewrite-rules", + "rr-one-inst-per-round", + "no-rr-one-inst-per-round", + "strings-exp", + "no-strings-exp", + "strings-lb", + "strings-fmf", + "no-strings-fmf", + "strings-eit", + "no-strings-eit", + "strings-alphabet-card", + "show-sat-solvers", + "random-freq", + "random-seed", + "restart-int-base", + "restart-int-inc", + "refine-conflicts", + "no-refine-conflicts", + "minisat-elimination", + "no-minisat-elimination", + "minisat-dump-dimacs", + "no-minisat-dump-dimacs", + "model-format", + "dump", + "dump-to", + "force-logic", + "simplification", + "no-simplification", + "static-learning", + "no-static-learning", + "produce-models", + "no-produce-models", + "check-models", + "no-check-models", + "dump-models", + "no-dump-models", + "proof", + "no-proof", + "check-proofs", + "no-check-proofs", + "dump-proofs", + "no-dump-proofs", + "produce-unsat-cores", + "no-produce-unsat-cores", + "produce-assignments", + "no-produce-assignments", + "interactive", + "no-interactive", + "ite-simp", + "no-ite-simp", + "on-repeat-ite-simp", + "no-on-repeat-ite-simp", + "simp-with-care", + "no-simp-with-care", + "simp-ite-compress", + "no-simp-ite-compress", + "unconstrained-simp", + "no-unconstrained-simp", + "repeat-simp", + "no-repeat-simp", + "simp-ite-hunt-zombies", + "sort-inference", + "no-sort-inference", + "incremental", + "no-incremental", + "abstract-values", + "no-abstract-values", + "model-u-dt-enum", + "no-model-u-dt-enum", + "tlimit", + "tlimit-per", + "rlimit", + "rlimit-per", + "rewrite-apply-to-const", + "no-rewrite-apply-to-const", + "replay", + "replay-log", + "decision", + "decision-threshold", + "decision-use-weight", + "no-decision-use-weight", + "decision-random-weight", + "decision-weight-internal", + "version", + "license", + "help", + "show-config", + "show-debug-tags", + "show-trace-tags", + "early-exit", + "no-early-exit", + "threads", + "threadN", + "filter-lemma-length", + "fallback-sequential", + "no-fallback-sequential", + "incremental-parallel", + "no-incremental-parallel", + "no-interactive-prompt", + "continued-execution", + "immediate-exit", + "segv-spin", + "no-segv-spin", + "segv-nospin", + "wait-to-join", + "no-wait-to-join", + "strict-parsing", + "no-strict-parsing", + "mmap", + "no-mmap", + "no-checking", + "no-filesystem-access", + "no-include-file", + "enable-idl-rewrite-equalities", + "disable-idl-rewrite-equalities", + "sets-propagate", + "no-sets-propagate", + "sets-eager-lemmas", + "no-sets-eager-lemmas", + NULL, + };/* cmdlineOptions */ + int i = 0; + set<string> ret; + while(cmdlineOptions[i] != NULL) { + ret.insert(cmdlineOptions[i]); + i++; + } + return ret; +} diff --git a/src/options/expr_options b/src/options/expr_options new file mode 100644 index 000000000..fc92c75a6 --- /dev/null +++ b/src/options/expr_options @@ -0,0 +1,33 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module EXPR "options/expr_options.h" Expression package + +option defaultExprDepth --default-expr-depth=N int :default 0 :predicate CVC4::options::setDefaultExprDepth :predicate-include "options/options_handler_interface.h" + print exprs to depth N (0 == default, -1 == no limit) +undocumented-alias --expr-depth=N = --default-expr-depth=N + +option defaultDagThresh default-dag-thresh --default-dag-thresh=N int :default 1 :predicate CVC4::options::setDefaultDagThresh :predicate-include "options/options_handler_interface.h" + dagify common subexprs appearing > N times (1 == default, 0 == don't dagify) +undocumented-alias --dag-thresh=N = --default-dag-thresh=N +undocumented-alias --dag-threshold=N = --default-dag-thresh=N + +option - --print-expr-types void :handler CVC4::options::setPrintExprTypes :handler-include "options/options_handler_interface.h" + print types with variables when printing exprs + +option earlyTypeChecking --eager-type-checking/--lazy-type-checking bool :default USE_EARLY_TYPE_CHECKING_BY_DEFAULT + type check expressions immediately on creation (debug builds only) +/type check expressions only when necessary (default) + +# --no-type-checking will override any --early-type-checking or --lazy-type-checking option +# --lazy-type-checking is linked because earlyTypeChecking should be set false too +option typeChecking /--no-type-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--lazy-type-checking + never type check expressions + +option biasedITERemoval --biased-ites bool :default false + try the new remove ite pass that is biased against term ites appearing + +endmodule + diff --git a/src/options/fp_options b/src/options/fp_options new file mode 100644 index 000000000..977e868d9 --- /dev/null +++ b/src/options/fp_options @@ -0,0 +1,8 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module FP "options/fp_options.h" Fp + +endmodule diff --git a/src/options/idl_options b/src/options/idl_options new file mode 100644 index 000000000..9d4d2a442 --- /dev/null +++ b/src/options/idl_options @@ -0,0 +1,12 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module IDL "options/idl_options.h" Idl + +option idlRewriteEq --enable-idl-rewrite-equalities/--disable-idl-rewrite-equalities bool :default false :read-write + enable rewriting equalities into two inequalities in IDL solver (default is disabled) +/disable rewriting equalities into two inequalities in IDL solver (default is disabled) + +endmodule diff --git a/src/options/language.cpp b/src/options/language.cpp new file mode 100644 index 000000000..7558c6927 --- /dev/null +++ b/src/options/language.cpp @@ -0,0 +1,135 @@ +/********************* */ +/*! \file language.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds + ** 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 Definition of input and output languages + ** + ** Definition of input and output languages. + **/ + +#include "options/language.h" + +namespace CVC4 { +namespace language { + +InputLanguage toInputLanguage(OutputLanguage language) { + switch(language) { + case output::LANG_SMTLIB_V1: + case output::LANG_SMTLIB_V2_0: + case output::LANG_SMTLIB_V2_5: + case output::LANG_TPTP: + case output::LANG_CVC4: + case output::LANG_Z3STR: + case output::LANG_SYGUS: + // these entries directly correspond (by design) + return InputLanguage(int(language)); + + default: { + std::stringstream ss; + ss << "Cannot map output language `" << language + << "' to an input language."; + throw CVC4::Exception(ss.str()); + } + }/* switch(language) */ +}/* toInputLanguage() */ + +OutputLanguage toOutputLanguage(InputLanguage language) { + switch(language) { + case input::LANG_SMTLIB_V1: + case input::LANG_SMTLIB_V2_0: + case input::LANG_SMTLIB_V2_5: + case input::LANG_TPTP: + case input::LANG_CVC4: + case input::LANG_Z3STR: + case input::LANG_SYGUS: + // these entries directly correspond (by design) + return OutputLanguage(int(language)); + + default: + // Revert to the default (AST) language. + // + // We used to throw an exception here, but that's not quite right. + // We often call this while constructing exceptions, for one, and + // it's better to output SOMETHING related to the original + // exception rather than mask it with another exception. Also, + // the input language isn't always defined---e.g. during the + // initial phase of the main CVC4 driver while it determines which + // language is appropriate, and during unit tests. Also, when + // users are writing their own code against the library. + return output::LANG_AST; + }/* switch(language) */ +}/* toOutputLanguage() */ + +OutputLanguage toOutputLanguage(std::string language) { + if(language == "cvc4" || language == "pl" || + language == "presentation" || language == "native" || + language == "LANG_CVC4") { + return output::LANG_CVC4; + } else if(language == "cvc3" || language == "LANG_CVC3") { + return output::LANG_CVC3; + } else if(language == "smtlib1" || language == "smt1" || + language == "LANG_SMTLIB_V1") { + return output::LANG_SMTLIB_V1; + } else if(language == "smtlib" || language == "smt" || + language == "smtlib2" || language == "smt2" || + language == "smtlib2.0" || language == "smt2.0" || + language == "LANG_SMTLIB_V2_0" || language == "LANG_SMTLIB_V2") { + return output::LANG_SMTLIB_V2_0; + } else if(language == "smtlib2.5" || language == "smt2.5" || + language == "LANG_SMTLIB_V2_5") { + return output::LANG_SMTLIB_V2_5; + } else if(language == "tptp" || language == "LANG_TPTP") { + return output::LANG_TPTP; + } else if(language == "z3str" || language == "z3-str" || + language == "LANG_Z3STR") { + return output::LANG_Z3STR; + } else if(language == "sygus" || language == "LANG_SYGUS") { + return output::LANG_SYGUS; + } else if(language == "ast" || language == "LANG_AST") { + return output::LANG_AST; + } else if(language == "auto" || language == "LANG_AUTO") { + return output::LANG_AUTO; + } + + throw OptionException(std::string("unknown output language `" + language + "'")); +}/* toOutputLanguage() */ + +InputLanguage toInputLanguage(std::string language) { + if(language == "cvc4" || language == "pl" || + language == "presentation" || language == "native" || + language == "LANG_CVC4") { + return input::LANG_CVC4; + } else if(language == "smtlib1" || language == "smt1" || + language == "LANG_SMTLIB_V1") { + return input::LANG_SMTLIB_V1; + } else if(language == "smtlib" || language == "smt" || + language == "smtlib2" || language == "smt2" || + language == "smtlib2.0" || language == "smt2.0" || + language == "LANG_SMTLIB_V2_0" || language == "LANG_SMTLIB_V2") { + return input::LANG_SMTLIB_V2_0; + } else if(language == "smtlib2.5" || language == "smt2.5" || + language == "LANG_SMTLIB_V2_5") { + return input::LANG_SMTLIB_V2_5; + } else if(language == "tptp" || language == "LANG_TPTP") { + return input::LANG_TPTP; + } else if(language == "z3str" || language == "z3-str" || + language == "LANG_Z3STR") { + return input::LANG_Z3STR; + } else if(language == "sygus" || language == "LANG_SYGUS") { + return input::LANG_SYGUS; + } else if(language == "auto" || language == "LANG_AUTO") { + return input::LANG_AUTO; + } + + throw OptionException(std::string("unknown input language `" + language + "'")); +}/* toInputLanguage() */ + +}/* CVC4::language namespace */ +}/* CVC4 namespace */ diff --git a/src/options/language.h b/src/options/language.h new file mode 100644 index 000000000..d400b4afb --- /dev/null +++ b/src/options/language.h @@ -0,0 +1,202 @@ +/********************* */ +/*! \file language.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds + ** 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 Definition of input and output languages + ** + ** Definition of input and output languages. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__LANGUAGE_H +#define __CVC4__LANGUAGE_H + +#include <sstream> +#include <string> + +#include "base/exception.h" +#include "options/option_exception.h" + +namespace CVC4 { +namespace language { + +namespace input { + +enum CVC4_PUBLIC Language { + // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 + + /** Auto-detect the language */ + LANG_AUTO = -1, + + // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9] + // AND SHOULD CORRESPOND IN PLACEMENT WITH OUTPUTLANGUAGE + // + // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR + // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE, + // INCLUDE IT HERE + + /** The SMTLIB v1 input language */ + LANG_SMTLIB_V1 = 0, + /** The SMTLIB v2.0 input language */ + LANG_SMTLIB_V2_0, + /** The SMTLIB v2.5 input language */ + LANG_SMTLIB_V2_5, + /** Backward-compatibility for enumeration naming */ + LANG_SMTLIB_V2 = LANG_SMTLIB_V2_5, + /** The TPTP input language */ + LANG_TPTP, + /** The CVC4 input language */ + LANG_CVC4, + /** The Z3-str input language */ + LANG_Z3STR, + /** The SyGuS input language */ + LANG_SYGUS, + + // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10 + // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES + + /** LANG_MAX is > any valid InputLanguage id */ + LANG_MAX +};/* enum Language */ + +inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& out, Language lang) { + switch(lang) { + case LANG_AUTO: + out << "LANG_AUTO"; + break; + case LANG_SMTLIB_V1: + out << "LANG_SMTLIB_V1"; + break; + case LANG_SMTLIB_V2_0: + out << "LANG_SMTLIB_V2_0"; + break; + case LANG_SMTLIB_V2_5: + out << "LANG_SMTLIB_V2_5"; + break; + case LANG_TPTP: + out << "LANG_TPTP"; + break; + case LANG_CVC4: + out << "LANG_CVC4"; + break; + case LANG_Z3STR: + out << "LANG_Z3STR"; + break; + case LANG_SYGUS: + out << "LANG_SYGUS"; + break; + default: + out << "undefined_input_language"; + } + return out; +} + +}/* CVC4::language::input namespace */ + +namespace output { + +enum CVC4_PUBLIC Language { + // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 + + /** Match the output language to the input language */ + LANG_AUTO = -1, + + // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9] + // AND SHOULD CORRESPOND IN PLACEMENT WITH INPUTLANGUAGE + // + // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR + // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE, + // INCLUDE IT HERE + + /** The SMTLIB v1 output language */ + LANG_SMTLIB_V1 = input::LANG_SMTLIB_V1, + /** The SMTLIB v2.0 output language */ + LANG_SMTLIB_V2_0 = input::LANG_SMTLIB_V2_0, + /** The SMTLIB v2.5 output language */ + LANG_SMTLIB_V2_5 = input::LANG_SMTLIB_V2_5, + /** Backward-compatibility for enumeration naming */ + LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2, + /** The TPTP output language */ + LANG_TPTP = input::LANG_TPTP, + /** The CVC4 output language */ + LANG_CVC4 = input::LANG_CVC4, + /** The Z3-str output language */ + LANG_Z3STR = input::LANG_Z3STR, + /** The sygus output language */ + LANG_SYGUS = input::LANG_SYGUS, + + // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10 + // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES + + /** The AST output language */ + LANG_AST = 10, + /** The CVC3-compatibility output language */ + LANG_CVC3, + + /** LANG_MAX is > any valid OutputLanguage id */ + LANG_MAX +};/* enum Language */ + +inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& out, Language lang) { + switch(lang) { + case LANG_SMTLIB_V1: + out << "LANG_SMTLIB_V1"; + break; + case LANG_SMTLIB_V2_0: + out << "LANG_SMTLIB_V2_0"; + break; + case LANG_SMTLIB_V2_5: + out << "LANG_SMTLIB_V2_5"; + break; + case LANG_TPTP: + out << "LANG_TPTP"; + break; + case LANG_CVC4: + out << "LANG_CVC4"; + break; + case LANG_Z3STR: + out << "LANG_Z3STR"; + break; + case LANG_SYGUS: + out << "LANG_SYGUS"; + break; + case LANG_AST: + out << "LANG_AST"; + break; + case LANG_CVC3: + out << "LANG_CVC3"; + break; + default: + out << "undefined_output_language"; + } + return out; +} + +}/* CVC4::language::output namespace */ + +}/* CVC4::language namespace */ + +typedef language::input::Language InputLanguage; +typedef language::output::Language OutputLanguage; + +namespace language { + +InputLanguage toInputLanguage(OutputLanguage language) CVC4_PUBLIC; +OutputLanguage toOutputLanguage(InputLanguage language) CVC4_PUBLIC; +InputLanguage toInputLanguage(std::string language) CVC4_PUBLIC; +OutputLanguage toOutputLanguage(std::string language) CVC4_PUBLIC; + +}/* CVC4::language namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__LANGUAGE_H */ diff --git a/src/options/language.i b/src/options/language.i new file mode 100644 index 000000000..d14368ca0 --- /dev/null +++ b/src/options/language.i @@ -0,0 +1,44 @@ +%{ +#include "options/language.h" +%} + +namespace CVC4 { + namespace language { + namespace input { + %ignore operator<<(std::ostream&, Language); + }/* CVC4::language::input namespace */ + + namespace output { + %ignore operator<<(std::ostream&, Language); + }/* CVC4::language::output namespace */ + }/* CVC4::language namespace */ +}/* CVC4 namespace */ + +// These clash in the monolithic Java namespace, so we rename them. +%rename(InputLanguage) CVC4::language::input::Language; +%rename(OutputLanguage) CVC4::language::output::Language; + +%rename(INPUT_LANG_AUTO) CVC4::language::input::LANG_AUTO; +%rename(INPUT_LANG_SMTLIB_V1) CVC4::language::input::LANG_SMTLIB_V1; +%rename(INPUT_LANG_SMTLIB_V2) CVC4::language::input::LANG_SMTLIB_V2; +%rename(INPUT_LANG_SMTLIB_V2_0) CVC4::language::input::LANG_SMTLIB_V2_0; +%rename(INPUT_LANG_SMTLIB_V2_5) CVC4::language::input::LANG_SMTLIB_V2_5; +%rename(INPUT_LANG_TPTP) CVC4::language::input::LANG_TPTP; +%rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4; +%rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX; +%rename(INPUT_LANG_Z3STR) CVC4::language::input::LANG_Z3STR; +%rename(INPUT_LANG_SYGUS) CVC4::language::input::LANG_SYGUS; + +%rename(OUTPUT_LANG_AUTO) CVC4::language::output::LANG_AUTO; +%rename(OUTPUT_LANG_SMTLIB_V1) CVC4::language::output::LANG_SMTLIB_V1; +%rename(OUTPUT_LANG_SMTLIB_V2) CVC4::language::output::LANG_SMTLIB_V2; +%rename(OUTPUT_LANG_SMTLIB_V2_0) CVC4::language::output::LANG_SMTLIB_V2_0; +%rename(OUTPUT_LANG_SMTLIB_V2_5) CVC4::language::output::LANG_SMTLIB_V2_5; +%rename(OUTPUT_LANG_TPTP) CVC4::language::output::LANG_TPTP; +%rename(OUTPUT_LANG_CVC4) CVC4::language::output::LANG_CVC4; +%rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST; +%rename(OUTPUT_LANG_MAX) CVC4::language::output::LANG_MAX; +%rename(OUTPUT_LANG_Z3STR) CVC4::language::output::LANG_Z3STR; +%rename(OUTPUT_LANG_SYGUS) CVC4::language::output::LANG_SYGUS; + +%include "options/language.h" diff --git a/src/options/logic_info_forward.h b/src/options/logic_info_forward.h new file mode 100644 index 000000000..8c31a3675 --- /dev/null +++ b/src/options/logic_info_forward.h @@ -0,0 +1,9 @@ + +#ifndef __CVC4__OPTIONS_LOGIC_INFO_FORWARD_H +#define __CVC4__OPTIONS_LOGIC_INFO_FORWARD_H + +namespace CVC4 { +class LogicInfo; +}/* CVC4 namespace */ + +#endif /* __CVC4__OPTIONS_LOGIC_INFO_FORWARD_H */ diff --git a/src/options/main_options b/src/options/main_options new file mode 100644 index 000000000..b468c9284 --- /dev/null +++ b/src/options/main_options @@ -0,0 +1,63 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module DRIVER "options/main_options.h" Driver + +common-option version -V --version/ bool + identify this CVC4 binary +undocumented-alias --license = --version + +common-option help -h --help/ bool + full command line reference + +common-option - --show-config void :handler CVC4::options::showConfiguration :handler-include "options/options_handler_interface.h" + show CVC4 static configuration + +option - --show-debug-tags void :handler CVC4::options::showDebugTags :handler-include "options/options_handler_interface.h" + show all available tags for debugging +option - --show-trace-tags void :handler CVC4::options::showTraceTags :handler-include "options/options_handler_interface.h" + show all available tags for tracing + +expert-option earlyExit --early-exit bool :default true + do not run destructors at exit; default on except in debug builds + +# portfolio options +option threads --threads=N unsigned :default 2 :predicate options::greater(0) + Total number of threads for portfolio +option - --threadN=string void :handler CVC4::options::threadN :handler-include "options/options_handler_interface.h" + configures portfolio thread N (0..#threads-1) +option threadStackSize --thread-stack=N unsigned :default 0 + stack size for worker threads in MB (0 means use Boost/thread lib default) +option threadArgv std::vector<std::string> :include <vector> <string> + Thread configuration (a string to be passed to parseOptions) +option thread_id int :default -1 + Thread ID, for internal use in case of multi-threaded run +option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write + don't share (among portfolio threads) lemmas strictly longer than N +option fallbackSequential --fallback-sequential bool :default false + Switch to sequential mode (instead of printing an error) if it can't be solved in portfolio mode +option incrementalParallel --incremental-parallel bool :default false :link --incremental + Use parallel solver even in incremental mode (may print 'unknown's at times) + +option interactive : --interactive bool :read-write + force interactive/non-interactive mode +undocumented-option interactivePrompt /--no-interactive-prompt bool :default true + turn off interactive prompting while in interactive mode + +# error behaviors (--immediate-exit is default in cases we support, thus no options) +option continuedExecution --continued-execution/ bool :default false :link "--interactive --no-interactive-prompt"/ + continue executing commands, even on error + +option segvSpin --segv-spin bool :default false + spin on segfault/other crash waiting for gdb +undocumented-alias --segv-nospin = --no-segv-spin + +expert-option tearDownIncremental : --tear-down-incremental bool :default false + implement PUSH/POP/multi-query by destroying and recreating SmtEngine + +expert-option waitToJoin --wait-to-join bool :default true + wait for other threads to join before quitting + +endmodule diff --git a/src/options/mkoptions b/src/options/mkoptions index 54c731a70..05280baa8 100755 --- a/src/options/mkoptions +++ b/src/options/mkoptions @@ -12,11 +12,12 @@ # mkoptions template-sed template-file # mkoptions apply-sed-files-to-template template-file (sed-file)* # -# The primary purpose of this script is to create options.{h,cpp} +# The primary purpose of this script is to create options/*_options.{h,cpp} # from template files and a list of options. This additionally generates -# the several documentation files, smt/smt_options.{h,cpp}, and -# options_holder.{h,cpp}. This script can in broad terms be thought of -# as an interpreter for a domain specific language within bash. +# the several documentation files, option_handler_get_option.cpp, +# option_handler_set_option.cpp, and options_holder.{h,cpp}. This script can in +# broad terms be thought of as an interpreter for a domain specific language +# within bash. # # The process for generating the files is as follows. # 1) Scan all of the option files that are of interest. @@ -534,11 +535,11 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const;" if [ "$type" = bool ]; then module_specializations="${module_specializations} #line $lineno \"$kf\" -template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value, SmtEngine* smt);" +template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value, options::OptionsHandler* handler);" elif [ "$internal" != - ]; then module_specializations="${module_specializations} #line $lineno \"$kf\" -template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value, SmtEngine* smt);" +template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value, options::OptionsHandler* handler);" fi module_accessors="${module_accessors} @@ -604,7 +605,7 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r while [ $i -lt ${#smt_links[@]} ]; do run_smt_links="$run_smt_links #line $lineno \"$kf\" - smt->setOption(std::string(\"${smt_links[$i]}\"), SExpr(${smt_links[$(($i+1))]}));" + handler->setOption(std::string(\"${smt_links[$i]}\"), (${smt_links[$(($i+1))]}));" i=$((i+2)) done fi @@ -625,13 +626,13 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r for predicate in $predicates; do run_handlers="$run_handlers #line $lineno \"$kf\" - $predicate(option, b, smt);" + $predicate(option, b, handler);" done fi if [ -n "$run_handlers" ]; then all_custom_handlers="${all_custom_handlers} #line $lineno \"$kf\" -template <> void runBoolPredicates(options::${internal}__option_t, std::string option, bool b, SmtEngine* smt) { +template <> void runBoolPredicates(options::${internal}__option_t, std::string option, bool b, options::OptionsHandler* handler) { $run_handlers }" fi @@ -640,7 +641,7 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o if [ "$type" = bool ]; then all_modules_option_handlers="${all_modules_option_handlers}${cases} #line $lineno \"$kf\" - assignBool(options::$internal, option, true, NULL);$run_links + assignBool(options::$internal, option, true, handler);$run_links break; " elif [ -n "$expect_arg" -a "$internal" != - ]; then @@ -649,7 +650,7 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o for handler in $handlers; do run_handlers="$run_handlers #line $lineno \"$kf\" - $handler(option, optionarg, smt);" + $handler(option, optionarg, handler);" done else run_handlers=" @@ -660,12 +661,12 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o for predicate in $predicates; do run_handlers="$run_handlers #line $lineno \"$kf\" - $predicate(option, retval, smt);" + $predicate(option, retval, handler);" done fi all_custom_handlers="${all_custom_handlers} #line $lineno \"$kf\" -template <> options::${internal}__option_t::type runHandlerAndPredicates(options::${internal}__option_t, std::string option, std::string optionarg, SmtEngine* smt) { +template <> options::${internal}__option_t::type runHandlerAndPredicates(options::${internal}__option_t, std::string option, std::string optionarg, options::OptionsHandler* handler) { #line $lineno \"$kf\" options::${internal}__option_t::type retval = $run_handlers #line $lineno \"$kf\" @@ -673,7 +674,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options }" all_modules_option_handlers="${all_modules_option_handlers}${cases} #line $lineno \"$kf\" - assign(options::$internal, option, optionarg, NULL);$run_links + assign(options::$internal, option, optionarg, handler);$run_links break; " elif [ -n "$expect_arg" ]; then @@ -685,7 +686,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options for handler in $handlers; do run_handlers="$run_handlers #line $lineno \"$kf\" - $handler(option, optionarg, smt);" + $handler(option, optionarg, handler);" done fi all_modules_option_handlers="${all_modules_option_handlers}${cases} @@ -702,7 +703,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options for handler in $handlers; do run_handlers="$run_handlers #line $lineno \"$kf\" - $handler(option, smt);" + $handler(option, handler);" done fi all_modules_option_handlers="${all_modules_option_handlers}${cases} @@ -716,7 +717,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options if [ "$type" = bool ]; then all_modules_option_handlers="${all_modules_option_handlers}${cases_alternate} #line $lineno \"$kf\" - assignBool(options::$internal, option, false, NULL);$run_links_alternate + assignBool(options::$internal, option, false, handler);$run_links_alternate break; " else @@ -733,54 +734,33 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options bool) all_modules_get_options="${all_modules_get_options:+$all_modules_get_options #line $lineno \"$kf\" - }{ std::vector<SExpr> v; v.push_back(\"$smtname\"); v.push_back(SExpr::Keyword(d_holder->$internal ? \"true\" : \"false\")); opts.push_back(v); }" + }{ std::vector<std::string> v; v.push_back(\"$smtname\"); v.push_back(std::string(d_holder->$internal ? \"true\" : \"false\")); opts.push_back(v); }" smt_getoption_handlers="${smt_getoption_handlers} #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" - return SExprKeyword(options::$internal() ? \"true\" : \"false\"); + return std::string(options::$internal() ? \"true\" : \"false\"); }";; - int|unsigned|int*_t|uint*_t|unsigned\ long|long|CVC4::Integer) + int|unsigned|int*_t|uint*_t|unsigned\ long|long|float|double) all_modules_get_options="${all_modules_get_options:+$all_modules_get_options #line $lineno \"$kf\" - }{ std::vector<SExpr> v; v.push_back(\"$smtname\"); v.push_back(d_holder->$internal); opts.push_back(v); }" + }{ std::stringstream ss; ss << std::fixed << std::setprecision(8); ss << d_holder->$internal; std::vector<std::string> v; v.push_back(\"$smtname\"); v.push_back(ss.str()); opts.push_back(v); }" smt_getoption_handlers="${smt_getoption_handlers} #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" - return SExpr(Integer(options::$internal())); - }";; - float|double) - all_modules_get_options="${all_modules_get_options:+$all_modules_get_options -#line $lineno \"$kf\" - }{ std::vector<SExpr> v; v.push_back(\"$smtname\"); v.push_back(Rational::fromDouble(d_holder->$internal)); opts.push_back(v); }" - smt_getoption_handlers="${smt_getoption_handlers} -#line $lineno \"$kf\" - if(key == \"$smtname\") { -#line $lineno \"$kf\" - stringstream ss; ss << std::fixed << options::$internal(); - return SExpr(Rational::fromDecimal(ss.str())); - }";; - CVC4::Rational) - all_modules_get_options="${all_modules_get_options:+$all_modules_get_options -#line $lineno \"$kf\" - }{ std::vector<SExpr> v; v.push_back(\"$smtname\"); v.push_back(d_holder->$internal); opts.push_back(v); }" - smt_getoption_handlers="${smt_getoption_handlers} -#line $lineno \"$kf\" - if(key == \"$smtname\") { -#line $lineno \"$kf\" - return SExpr(options::$internal()); + std::stringstream ss; ss << std::fixed << std::setprecision(8); ss << options::$internal(); return ss.str(); }";; *) all_modules_get_options="${all_modules_get_options:+$all_modules_get_options #line $lineno \"$kf\" - }{ std::stringstream ss; ss << d_holder->$internal; std::vector<SExpr> v; v.push_back(\"$smtname\"); v.push_back(ss.str()); opts.push_back(v); }" + }{ std::stringstream ss; ss << d_holder->$internal; std::vector<std::string> v; v.push_back(\"$smtname\"); v.push_back(ss.str()); opts.push_back(v); }" smt_getoption_handlers="${smt_getoption_handlers} #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" - stringstream ss; ss << options::$internal(); - return SExpr(ss.str()); + std::stringstream ss; ss << options::$internal(); + return ss.str(); }";; esac fi @@ -790,7 +770,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" - Options::current()->assignBool(options::$internal, \"$smtname\", optionarg == \"true\", smt);$run_smt_links + Options::current()->assignBool(options::$internal, \"$smtname\", optionarg == \"true\", handler);$run_smt_links return; }" elif [ -n "$expect_arg" -a "$internal" != - ]; then @@ -799,7 +779,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options for handler in $handlers; do run_handlers="$run_handlers #line $lineno \"$kf\" - $handler(\"$smtname\", optionarg, smt); + $handler(\"$smtname\", optionarg, handler); " done fi @@ -807,7 +787,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options #line $lineno \"$kf\" if(key == \"$smtname\") { #line $lineno \"$kf\" - Options::current()->assign(options::$internal, \"$smtname\", optionarg, smt);$run_smt_links + Options::current()->assign(options::$internal, \"$smtname\", optionarg, handler);$run_smt_links return; }" elif [ -n "$expect_arg" ]; then @@ -815,7 +795,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options for handler in $handlers; do run_handlers="$run_handlers #line $lineno \"$kf\" - $handler(\"$smtname\", optionarg, smt); + $handler(\"$smtname\", optionarg, handler); " done smt_setoption_handlers="${smt_setoption_handlers} @@ -830,7 +810,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options for handler in $handlers; do run_handlers="$run_handlers #line $lineno \"$kf\" - $handler(\"$smtname\", smt); + $handler(\"$smtname\", handler); " done smt_setoption_handlers="${smt_setoption_handlers} @@ -853,23 +833,15 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options fi all_modules_get_options="${all_modules_get_options:+$all_modules_get_options #line $lineno \"$kf\" - }{ std::vector<SExpr> v; v.push_back(\"$getoption_name\"); v.push_back(SExpr::Keyword((${inv}d_holder->$internal) ? \"true\" : \"false\")); opts.push_back(v); }";; - int|unsigned|int*_t|uint*_t|unsigned\ long|long|CVC4::Integer) + }{ std::vector<std::string> v; v.push_back(\"$getoption_name\"); v.push_back(std::string((${inv}d_holder->$internal) ? \"true\" : \"false\")); opts.push_back(v); }";; + int|unsigned|int*_t|uint*_t|unsigned\ long|long|float|double) all_modules_get_options="${all_modules_get_options:+$all_modules_get_options #line $lineno \"$kf\" - }{ std::vector<SExpr> v; v.push_back(\"$long_option\"); v.push_back(d_holder->$internal); opts.push_back(v); }";; - float|double) - all_modules_get_options="${all_modules_get_options:+$all_modules_get_options -#line $lineno \"$kf\" - }{ std::vector<SExpr> v; v.push_back(\"$long_option\"); v.push_back(Rational::fromDouble(d_holder->$internal)); opts.push_back(v); }";; - CVC4::Rational) - all_modules_get_options="${all_modules_get_options:+$all_modules_get_options -#line $lineno \"$kf\" - }{ std::vector<SExpr> v; v.push_back(\"$long_option\"); v.push_back(d_holder->$internal); opts.push_back(v); }";; + }{ std::stringstream ss; ss << std::fixed << std::setprecision(8); ss << d_holder->$internal; std::vector<std::string> v; v.push_back(\"$long_option\"); v.push_back(ss.str()); opts.push_back(v); }";; *) all_modules_get_options="${all_modules_get_options:+$all_modules_get_options #line $lineno \"$kf\" - }{ std::stringstream ss; ss << d_holder->$internal; std::vector<SExpr> v; v.push_back(\"$long_option\"); v.push_back(ss.str()); opts.push_back(v); }";; + }{ std::stringstream ss; ss << std::fixed << std::setprecision(8); ss << d_holder->$internal; std::vector<std::string> v; v.push_back(\"$long_option\"); v.push_back(ss.str()); opts.push_back(v); }";; esac fi @@ -877,9 +849,9 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options # emit assignBool/assign all_custom_handlers="${all_custom_handlers} #line $lineno \"$kf\" -template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value, SmtEngine* smt) { +template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value, options::OptionsHandler* handler) { #line $lineno \"$kf\" - runBoolPredicates(options::$internal, option, value, smt); + runBoolPredicates(options::$internal, option, value, handler); #line $lineno \"$kf\" d_holder->$internal = value; #line $lineno \"$kf\" @@ -890,9 +862,9 @@ template <> void Options::assignBool(options::${internal}__option_t, std::string elif [ -n "$expect_arg" -a "$internal" != - ] && [ -n "$cases" -o -n "$cases_alternate" -o -n "$smtname" ]; then all_custom_handlers="${all_custom_handlers} #line $lineno \"$kf\" -template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value, SmtEngine* smt) { +template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value, options::OptionsHandler* handler) { #line $lineno \"$kf\" - d_holder->$internal = runHandlerAndPredicates(options::$internal, option, value, smt); + d_holder->$internal = runHandlerAndPredicates(options::$internal, option, value, handler); #line $lineno \"$kf\" d_holder->${internal}__setByUser__ = true; #line $lineno \"$kf\" diff --git a/src/options/option_exception.h b/src/options/option_exception.h index a90b96367..c57414026 100644 --- a/src/options/option_exception.h +++ b/src/options/option_exception.h @@ -19,7 +19,7 @@ #ifndef __CVC4__OPTION_EXCEPTION_H #define __CVC4__OPTION_EXCEPTION_H -#include "util/exception.h" +#include "base/exception.h" namespace CVC4 { diff --git a/src/options/options.h b/src/options/options.h index 95c0fc331..fc3bf40ac 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -24,21 +24,18 @@ #include <string> #include <vector> +#include "base/tls.h" #include "options/option_exception.h" -#include "util/language.h" -#include "util/tls.h" -#include "util/sexpr.h" namespace CVC4 { namespace options { struct OptionsHolder; + class OptionsHandler; }/* CVC4::options namespace */ +// Forward declaration for smt_options class ExprStream; -class NodeManager; -class NodeManagerScope; -class SmtEngine; class CVC4_PUBLIC Options { /** The struct that holds all option values. */ @@ -49,16 +46,27 @@ class CVC4_PUBLIC Options { /** Low-level assignment function for options */ template <class T> - void assign(T, std::string option, std::string value, SmtEngine* smt); + void assign(T, std::string option, std::string value, options::OptionsHandler* handler); /** Low-level assignment function for bool-valued options */ template <class T> - void assignBool(T, std::string option, bool value, SmtEngine* smt); + void assignBool(T, std::string option, bool value, options::OptionsHandler* handler); - friend class NodeManager; - friend class NodeManagerScope; - friend class SmtEngine; + friend class options::OptionsHandler; public: + class CVC4_PUBLIC OptionsScope { + private: + Options* d_oldOptions; + public: + OptionsScope(Options* newOptions) : + d_oldOptions(Options::s_current) + { + Options::s_current = newOptions; + } + ~OptionsScope(){ + Options::s_current = d_oldOptions; + } + }; /** Return true if current Options are null */ static inline bool isCurrentNull() { @@ -145,12 +153,12 @@ public: * The return value is what's left of the command line (that is, the * non-option arguments). */ - std::vector<std::string> parseOptions(int argc, char* argv[]) throw(OptionException); + std::vector<std::string> parseOptions(int argc, char* argv[], options::OptionsHandler* handler) throw(OptionException); /** * Get the setting for all options. */ - SExpr getOptions() const throw(); + std::vector< std::vector<std::string> > getOptions() const throw(); };/* class Options */ diff --git a/src/options/options_handler_get_option_template.cpp b/src/options/options_handler_get_option_template.cpp new file mode 100644 index 000000000..b5da8c68d --- /dev/null +++ b/src/options/options_handler_get_option_template.cpp @@ -0,0 +1,54 @@ +/********************* */ +/*! \file option_handler_get_option_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 Implementation of OptionsHandler::getOption. + ** + ** This template file is expanded into the cpp implementation of + ** OptionsHandler::setOption. The file is essentially the contents + ** of the ${smt_getoption_handlers} variable in the options/mkoptions + ** script. This variable depends on all options files. To generate this file, + ** first generate options/summary.sed. + **/ + +#include <iomanip> +#include <string> +#include <sstream> + + +#include "base/output.h" +#include "base/modal_exception.h" +#include "options/option_exception.h" +#include "options/options_handler_interface.h" + + +${include_all_option_headers} +${option_handler_includes} + +#line 31 "${template}" + +using namespace std; + +namespace CVC4 { +namespace options { + +std::string OptionsHandler::getOption(const std::string& key) const + throw(OptionException) { + Trace("options") << "SMT getOption(" << key << ")" << endl; + + ${smt_getoption_handlers} + +#line 57 "${template}" + + throw UnrecognizedOptionException(key); +} + +}/* options namespace */ +}/* CVC4 namespace */ diff --git a/src/options/options_handler_interface.cpp b/src/options/options_handler_interface.cpp new file mode 100644 index 000000000..d803fced0 --- /dev/null +++ b/src/options/options_handler_interface.cpp @@ -0,0 +1,362 @@ +/********************* */ +/*! \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 "options/options_handler_interface.h" + +#include <ostream> +#include <string> + +#include "base/cvc4_assert.h" +#include "base/exception.h" +#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/printer_modes.h" +#include "options/quantifiers_modes.h" +#include "options/simplification_mode.h" +#include "options/theoryof_mode.h" +#include "options/ufss_mode.h" + +namespace CVC4 { +namespace options { + +static const char* s_third_argument_warning = + "We no longer support passing the third argument to the setting an option as NULL."; + +// theory/arith/options_handlers.h +ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToArithUnateLemmaMode(option, optarg); +} +ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToArithPropagationMode(option, optarg); +} +ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToErrorSelectionRule(option, optarg); +} + +// theory/quantifiers/options_handlers.h +theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToInstWhenMode(option, optarg); +} +void checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->checkInstWhenMode(option, mode); +} +theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToLiteralMatchMode(option, optarg); +} +void checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->checkLiteralMatchMode(option, mode); +} +theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToMbqiMode(option, optarg); +} +void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->checkMbqiMode(option, mode); +} +theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToQcfWhenMode(option, optarg); +} +theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToQcfMode(option, optarg); +} +theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToUserPatMode(option, optarg); +} +theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToTriggerSelMode(option, optarg); +} +theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToPrenexQuantMode(option, optarg); +} +theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToCegqiFairMode(option, optarg); +} +theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler-> stringToTermDbMode(option, optarg); +} +theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToIteLiftQuantMode(option, optarg); +} +theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToSygusInvTemplMode(option, optarg); +} +theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToMacrosQuantMode(option, optarg); +} + + +// theory/bv/options_handlers.h +void abcEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->abcEnabledBuild(option, value); +} +void abcEnabledBuild(std::string option, std::string value, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->abcEnabledBuild(option, value); +} +theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToBitblastMode(option, optarg); +} +theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToBvSlicerMode(option, optarg); +} +void setBitblastAig(std::string option, bool arg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->setBitblastAig(option, arg); +} + + +// theory/booleans/options_handlers.h +theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToBooleanTermConversionMode( option, optarg); +} + +// theory/uf/options_handlers.h +theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToUfssMode(option, optarg); +} + +// theory/options_handlers.h +theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToTheoryOfMode(option, optarg); +} +void useTheory(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->useTheory(option, optarg); +} + +// printer/options_handlers.h +ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToModelFormatMode(option, optarg); +} + +InstFormatMode stringToInstFormatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToInstFormatMode(option, optarg); +} + + +// decision/options_handlers.h +decision::DecisionMode stringToDecisionMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToDecisionMode(option, optarg); +} + +decision::DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToDecisionWeightInternal(option, optarg); +} + + +/* options/base_options_handlers.h */ +void setVerbosity(std::string option, int value, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->setVerbosity(option, value); +} +void increaseVerbosity(std::string option, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->increaseVerbosity(option); +} +void decreaseVerbosity(std::string option, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->decreaseVerbosity(option); +} + +OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToOutputLanguage(option, optarg); +} + +InputLanguage stringToInputLanguage(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToInputLanguage(option, optarg); +} + +void addTraceTag(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->addTraceTag(option, optarg); +} + +void addDebugTag(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->addDebugTag(option, optarg); +} + +void setPrintSuccess(std::string option, bool value, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->setPrintSuccess(option, value); +} + + +/* main/options_handlers.h */ +void showConfiguration(std::string option, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->showConfiguration(option); +} + +void showDebugTags(std::string option, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->showDebugTags(option); +} + +void showTraceTags(std::string option, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->showTraceTags(option); +} + +void threadN(std::string option, OptionsHandler* handler){ + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->threadN(option); +} + +/* expr/options_handlers.h */ +void setDefaultExprDepth(std::string option, int depth, OptionsHandler* handler){ + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->setDefaultExprDepth(option, depth); +} + +void setDefaultDagThresh(std::string option, int dag, OptionsHandler* handler){ + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->setDefaultDagThresh(option, dag); +} + +void setPrintExprTypes(std::string option, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->setPrintExprTypes(option); +} + + +/* smt/options_handlers.h */ +void dumpMode(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->dumpMode(option, optarg); +} + +LogicInfo* stringToLogicInfo(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException){ + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToLogicInfo(option, optarg); +} + +SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException){ + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->stringToSimplificationMode(option, optarg); +} + +// ensure we haven't started search yet +void beforeSearch(std::string option, bool value, OptionsHandler* handler) throw(ModalException){ + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->beforeSearch(option, value); +} + +void setProduceAssertions(std::string option, bool value, OptionsHandler* handler) throw() { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->setProduceAssertions(option, value); +} + +// ensure we are a proof-enabled build of CVC4 +void proofEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->proofEnabledBuild(option, value); +} + +void dumpToFile(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->dumpToFile(option, optarg); +} + +void setRegularOutputChannel(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->setRegularOutputChannel(option, optarg); +} + +void setDiagnosticOutputChannel(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + handler->setDiagnosticOutputChannel(option, optarg); +} + +std::string checkReplayFilename(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->checkReplayFilename(option, optarg); +} + +std::ostream* checkReplayLogFilename(std::string option, std::string optarg, OptionsHandler* handler) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->checkReplayLogFilename(option, optarg); +} + +// ensure we are a stats-enabled build of CVC4 +void statsEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->statsEnabledBuild(option, value); +} + +unsigned long tlimitHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->tlimitHandler(option, optarg); +} + +unsigned long tlimitPerHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler-> tlimitPerHandler(option, optarg); +} + +unsigned long rlimitHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->rlimitHandler(option, optarg); +} + +unsigned long rlimitPerHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException) { + CheckArgument(handler != NULL, handler, s_third_argument_warning); + return handler->rlimitPerHandler(option, optarg); +} + + + +OptionsHandler::OptionsHandler() { } + +}/* CVC4::options namespace */ +}/* CVC4 namespace */ diff --git a/src/options/options_handler_interface.h b/src/options/options_handler_interface.h new file mode 100644 index 000000000..98575a313 --- /dev/null +++ b/src/options/options_handler_interface.h @@ -0,0 +1,275 @@ +/********************* */ +/*! \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__OPTIONS__OPTIONS_HANDLER_INTERFACE_H +#define __CVC4__OPTIONS__OPTIONS_HANDLER_INTERFACE_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/printer_modes.h" +#include "options/quantifiers_modes.h" +#include "options/simplification_mode.h" +#include "options/theoryof_mode.h" +#include "options/ufss_mode.h" + +namespace CVC4 { +class LogicInfo; +}/* CVC4 namespace */ + +namespace CVC4 { +namespace options { + +class OptionsHandler { +public: + OptionsHandler(); + virtual ~OptionsHandler() {} + + void setOption(const std::string& key, const std::string& optionarg) throw(OptionException, ModalException); + + std::string getOption(const std::string& key) const throw(OptionException); + + // DONE + // decision/options_handlers.h + // expr/options_handlers.h + // main/options_handlers.h + // options/base_options_handlers.h + // printer/options_handlers.h + // smt/options_handlers.h + // theory/options_handlers.h + // theory/booleans/options_handlers.h + // theory/uf/options_handlers.h + // theory/bv/options_handlers.h + // theory/quantifiers/options_handlers.h + // theory/arith/options_handlers.h + + + // theory/arith/options_handlers.h + virtual ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg) throw(OptionException) = 0; + + // theory/quantifiers/options_handlers.h + virtual theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual void checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode) throw(OptionException) = 0; + virtual theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual void checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException) = 0; + virtual theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode) throw(OptionException) = 0; + virtual theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException) = 0; + + // theory/bv/options_handlers.h + virtual void abcEnabledBuild(std::string option, bool value) throw(OptionException) = 0; + virtual void abcEnabledBuild(std::string option, std::string value) throw(OptionException) = 0; + virtual theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual void setBitblastAig(std::string option, bool arg) throw(OptionException) = 0; + + + // theory/booleans/options_handlers.h + virtual theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException) = 0; + + // theory/uf/options_handlers.h + virtual theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg) throw(OptionException) = 0; + + // theory/options_handlers.h + virtual theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg) = 0; + virtual void useTheory(std::string option, std::string optarg) = 0; + + + // printer/options_handlers.h + virtual ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual InstFormatMode stringToInstFormatMode(std::string option, std::string optarg) throw(OptionException) = 0; + + // decision/options_handlers.h + virtual decision::DecisionMode stringToDecisionMode(std::string option, std::string optarg) throw(OptionException) = 0; + virtual decision::DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg) throw(OptionException) = 0; + + + /* smt/options_handlers.h */ + virtual void dumpMode(std::string option, std::string optarg) = 0; + virtual LogicInfo* stringToLogicInfo(std::string option, std::string optarg) throw(OptionException) = 0; + virtual SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException) = 0; + + virtual void beforeSearch(std::string option, bool value) throw(ModalException) = 0; + virtual void setProduceAssertions(std::string option, bool value) throw() = 0; + virtual void proofEnabledBuild(std::string option, bool value) throw(OptionException) = 0; + virtual void dumpToFile(std::string option, std::string optarg) = 0; + virtual void setRegularOutputChannel(std::string option, std::string optarg) = 0; + virtual void setDiagnosticOutputChannel(std::string option, std::string optarg) = 0; + virtual std::string checkReplayFilename(std::string option, std::string optarg) = 0; + virtual std::ostream* checkReplayLogFilename(std::string option, std::string optarg) = 0; + virtual void statsEnabledBuild(std::string option, bool value) throw(OptionException) = 0; + virtual unsigned long tlimitHandler(std::string option, std::string optarg) throw(OptionException) = 0; + virtual unsigned long tlimitPerHandler(std::string option, std::string optarg) throw(OptionException) = 0; + virtual unsigned long rlimitHandler(std::string option, std::string optarg) throw(OptionException) = 0; + virtual unsigned long rlimitPerHandler(std::string option, std::string optarg) throw(OptionException) = 0; + + /* expr/options_handlers.h */ + virtual void setDefaultExprDepth(std::string option, int depth) = 0; + virtual void setDefaultDagThresh(std::string option, int dag) = 0; + virtual void setPrintExprTypes(std::string option) = 0; + + /* main/options_handlers.h */ + virtual void showConfiguration(std::string option) = 0; + virtual void showDebugTags(std::string option) = 0; + virtual void showTraceTags(std::string option) = 0; + virtual void threadN(std::string option) = 0; + + /* options/base_options_handlers.h */ + virtual void setVerbosity(std::string option, int value) throw(OptionException) = 0; + virtual void increaseVerbosity(std::string option) = 0; + virtual void decreaseVerbosity(std::string option) = 0; + virtual OutputLanguage stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException) = 0; + virtual InputLanguage stringToInputLanguage(std::string option, std::string optarg) throw(OptionException) = 0; + virtual void addTraceTag(std::string option, std::string optarg) = 0; + virtual void addDebugTag(std::string option, std::string optarg) = 0; + virtual void setPrintSuccess(std::string option, bool value) = 0; +}; /* class OptionHandler */ + +// theory/arith/options_handlers.h +ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); + +// theory/quantifiers/options_handlers.h +theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +void checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode, OptionsHandler* handler) throw(OptionException); +theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +void checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode, OptionsHandler* handler) throw(OptionException); +theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode, OptionsHandler* handler) throw(OptionException); +theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); + + +// theory/bv/options_handlers.h +void abcEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException); +void abcEnabledBuild(std::string option, std::string value, OptionsHandler* handler) throw(OptionException); +theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +void setBitblastAig(std::string option, bool arg, OptionsHandler* handler) throw(OptionException); + +// theory/booleans/options_handlers.h +theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); + +// theory/uf/options_handlers.h +theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); + + +// theory/options_handlers.h +theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg, OptionsHandler* handler); +void useTheory(std::string option, std::string optarg, OptionsHandler* handler); + +// printer/options_handlers.h +ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +InstFormatMode stringToInstFormatMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); + +// decision/options_handlers.h +decision::DecisionMode stringToDecisionMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +decision::DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); + + +/* options/base_options_handlers.h */ +void setVerbosity(std::string option, int value, OptionsHandler* handler) throw(OptionException); +void increaseVerbosity(std::string option, OptionsHandler* handler); +void decreaseVerbosity(std::string option, OptionsHandler* handler); +OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +InputLanguage stringToInputLanguage(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); +void addTraceTag(std::string option, std::string optarg, OptionsHandler* handler); +void addDebugTag(std::string option, std::string optarg, OptionsHandler* handler); +void setPrintSuccess(std::string option, bool value, OptionsHandler* handler); + +/* main/options_handlers.h */ +void showConfiguration(std::string option, OptionsHandler* handler); +void showDebugTags(std::string option, OptionsHandler* handler); +void showTraceTags(std::string option, OptionsHandler* handler); +void threadN(std::string option, OptionsHandler* handler); + +/* expr/options_handlers.h */ +void setDefaultExprDepth(std::string option, int depth, OptionsHandler* handler); +void setDefaultDagThresh(std::string option, int dag, OptionsHandler* handler); +void setPrintExprTypes(std::string option, OptionsHandler* handler); + +/* smt/options_handlers.h */ +void dumpMode(std::string option, std::string optarg, OptionsHandler* handler); + +LogicInfo* stringToLogicInfo(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); + +SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); + +// ensure we haven't started search yet +void beforeSearch(std::string option, bool value, OptionsHandler* handler) throw(ModalException); + +void setProduceAssertions(std::string option, bool value, OptionsHandler* handler) throw(); + +// ensure we are a proof-enabled build of CVC4 +void proofEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException); + +void dumpToFile(std::string option, std::string optarg, OptionsHandler* handler); + +void setRegularOutputChannel(std::string option, std::string optarg, OptionsHandler* handler); + +void setDiagnosticOutputChannel(std::string option, std::string optarg, OptionsHandler* handler); + +std::string checkReplayFilename(std::string option, std::string optarg, OptionsHandler* handler); + +std::ostream* checkReplayLogFilename(std::string option, std::string optarg, OptionsHandler* handler); + +// ensure we are a stats-enabled build of CVC4 +void statsEnabledBuild(std::string option, bool value, OptionsHandler* handler) throw(OptionException); + +unsigned long tlimitHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); + +unsigned long tlimitPerHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); + +unsigned long rlimitHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); + +unsigned long rlimitPerHandler(std::string option, std::string optarg, OptionsHandler* handler) throw(OptionException); + + +}/* CVC4::options namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__OPTIONS__OPTIONS_HANDLER_INTERFACE_H */ diff --git a/src/options/options_handler_interface.i b/src/options/options_handler_interface.i new file mode 100644 index 000000000..b7076a0b8 --- /dev/null +++ b/src/options/options_handler_interface.i @@ -0,0 +1,5 @@ +%{ +#include "options/options_handler_interface.h" +%} + +%include "options/options_handler_interface.h" diff --git a/src/options/options_handler_set_option_template.cpp b/src/options/options_handler_set_option_template.cpp new file mode 100644 index 000000000..86821bc0a --- /dev/null +++ b/src/options/options_handler_set_option_template.cpp @@ -0,0 +1,53 @@ +/********************* */ +/*! \file option_handler_set_option_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 Implementation of OptionsHandler::setOption. + ** + ** This template file is expanded into the cpp implementation of + ** OptionsHandler::setOption. The file is essentially the contents + ** of the ${smt_setoption_handlers} variable in the options/mkoptions + ** script. This variable depends on all options files. To generate this file, + ** first generate options/summary.sed. + **/ + +#include <string> +#include <sstream> + +#include "base/output.h" +#include "base/modal_exception.h" +#include "options/option_exception.h" +#include "options/options_handler_interface.h" + + +${include_all_option_headers} +${option_handler_includes} + +#line 31 "${template}" + +using namespace std; + +namespace CVC4 { +namespace options { + +void OptionsHandler::setOption(const std::string& key, const std::string& optionarg) + throw(OptionException, ModalException) { + options::OptionsHandler* const handler = this; + Trace("options") << "SMT setOption(" << key << ", " << optionarg << ")" << endl; + + ${smt_setoption_handlers} + +#line 44 "${template}" + + throw UnrecognizedOptionException(key); +} + +}/* options namespace */ +}/* CVC4 namespace */ diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index a9721ad20..ecf42ac58 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -14,6 +14,8 @@ ** Contains code for handling command-line options **/ +#warning "TODO: Remove ExprStream forward declaration from options.h." + #if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__) // force use of optreset; mingw32 croaks on argv-switching otherwise # include "cvc4autoconfig.h" @@ -34,32 +36,35 @@ extern int optreset; # undef _BSD_SOURCE #endif /* CVC4_IS_NOT_REALLY_BSD */ +#include <unistd.h> +#include <string.h> +#include <stdint.h> +#include <time.h> + #include <cstdio> #include <cstdlib> +#include <cstring> +#include <iomanip> #include <new> #include <string> #include <sstream> #include <limits> -#include <unistd.h> -#include <string.h> -#include <stdint.h> -#include <time.h> -#include "expr/expr.h" -#include "util/configuration.h" -#include "util/didyoumean.h" -#include "util/exception.h" -#include "util/language.h" -#include "util/tls.h" +#include "base/cvc4_assert.h" +#include "base/exception.h" +#include "base/output.h" +#include "base/tls.h" +#include "options/didyoumean.h" +#include "options/language.h" +#include "options/options_handler_interface.h" ${include_all_option_headers} #line 58 "${template}" -#include "util/output.h" #include "options/options_holder.h" #include "cvc4autoconfig.h" -#include "options/base_options_handlers.h" +#include "options/base_handlers.h" ${option_handler_includes} @@ -90,11 +95,29 @@ struct OptionHandler { /** Variant for integral C++ types */ template <class T> struct OptionHandler<T, true, true> { - static T handle(std::string option, std::string optionarg) { + static bool stringToInt(T& t, const std::string& str) { + std::istringstream ss(str); + ss >> t; + char tmp; + return !(ss.fail() || ss.get(tmp)); + } + + static bool containsMinus(const std::string& str) { + return str.find('-') != std::string::npos; + } + + static T handle(const std::string& option, const std::string& optionarg) { try { - Integer i(optionarg, 10); + T i; + bool success = stringToInt(i, optionarg); - if(! std::numeric_limits<T>::is_signed && i < 0) { + if(!success){ + throw OptionException(option + ": failed to parse "+ optionarg +" as an integer of the appropraite type."); + } + + // Depending in the platform unsigned numbers with '-' signs may parse. + // Reject these by looking for any minus if it is not signed. + if( (! std::numeric_limits<T>::is_signed) && containsMinus(optionarg) ) { // unsigned type but user gave negative argument throw OptionException(option + " requires a nonnegative argument"); } else if(i < std::numeric_limits<T>::min()) { @@ -109,11 +132,13 @@ struct OptionHandler<T, true, true> { throw OptionException(ss.str()); } - if(std::numeric_limits<T>::is_signed) { - return T(i.getLong()); - } else { - return T(i.getUnsignedLong()); - } + return i; + + // if(std::numeric_limits<T>::is_signed) { + // return T(i.getLong()); + // } else { + // return T(i.getUnsignedLong()); + // } } catch(std::invalid_argument&) { // user gave something other than an integer throw OptionException(option + " requires an integer argument"); @@ -183,7 +208,7 @@ std::string handleOption<std::string>(std::string option, std::string optionarg) * If a user specifies a :handler or :predicates, it overrides this. */ template <class T> -typename T::type runHandlerAndPredicates(T, std::string option, std::string optionarg, SmtEngine* smt) { +typename T::type runHandlerAndPredicates(T, std::string option, std::string optionarg, options::OptionsHandler* handler) { // By default, parse the option argument in a way appropriate for its type. // E.g., for "unsigned int" options, ensure that the provided argument is // a nonnegative integer that fits in the unsigned int type. @@ -192,7 +217,7 @@ typename T::type runHandlerAndPredicates(T, std::string option, std::string opti } template <class T> -void runBoolPredicates(T, std::string option, bool b, SmtEngine* smt) { +void runBoolPredicates(T, std::string option, bool b, options::OptionsHandler* handler) { // By default, nothing to do for bool. Users add things with // :predicate in options files to provide custom checking routines // that can throw exceptions. @@ -380,11 +405,10 @@ public: * The return value is what's left of the command line (that is, the * non-option arguments). */ -std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) { +std::vector<std::string> Options::parseOptions(int argc, char* main_argv[], options::OptionsHandler* const handler) throw(OptionException) { options::OptionsGuard guard(&s_current, this); const char *progName = main_argv[0]; - SmtEngine* const smt = NULL; Debug("options") << "main_argv == " << main_argv << std::endl; @@ -606,14 +630,14 @@ std::vector<std::string> Options::suggestSmtOptions(const std::string& optionNam return suggestions; } -SExpr Options::getOptions() const throw() { - std::vector<SExpr> opts; +std::vector< std::vector<std::string> > Options::getOptions() const throw() { + std::vector< std::vector<std::string> > opts; ${all_modules_get_options} #line 614 "${template}" - return SExpr(opts); + return opts; } #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT diff --git a/src/options/parser_options b/src/options/parser_options new file mode 100644 index 000000000..e91c735fe --- /dev/null +++ b/src/options/parser_options @@ -0,0 +1,34 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module PARSER "options/parser_options.h" Parser + +common-option strictParsing --strict-parsing bool + be less tolerant of non-conforming inputs + +option memoryMap --mmap bool + memory map file input + +option semanticChecks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--no-type-checking + disable ALL semantic checks, including type checks + +option globalDeclarations global-declarations bool :default false + force all declarations and definitions to be global + +# this is to support security in the online version, and in other similar contexts +# (--no-include-file disables filesystem access in TPTP and SMT2 parsers) +# the name --no-include-file is legacy: it also now limits any filesystem access +# (read or write) for example by using --dump-to (or the equivalent set-option) or +# set-option :regular-output-channel/:diagnostic-output-channel. However, the main +# driver is still permitted to read the input file given on the command-line if any. +# creation/use of temp files are still permitted (but the paths aren't given by the +# user). Also note this is only safe for the version invoked through the main driver, +# there are ways via the API to get the CVC4 library to open a file for reading or +# writing and thus leak information from an existing file, or overwrite an existing +# file with malicious content. +undocumented-option filesystemAccess /--no-filesystem-access bool :default true +undocumented-alias --no-include-file = --no-filesystem-access + +endmodule diff --git a/src/options/printer_modes.cpp b/src/options/printer_modes.cpp new file mode 100644 index 000000000..b698ed07d --- /dev/null +++ b/src/options/printer_modes.cpp @@ -0,0 +1,51 @@ +/********************* */ +/*! \file printer_modes.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** 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 "options/printer_modes.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) { + switch(mode) { + case MODEL_FORMAT_MODE_DEFAULT: + out << "MODEL_FORMAT_MODE_DEFAULT"; + break; + case MODEL_FORMAT_MODE_TABLE: + out << "MODEL_FORMAT_MODE_TABLE"; + break; + default: + out << "ModelFormatMode:UNKNOWN![" << unsigned(mode) << "]"; + } + + return out; +} + +std::ostream& operator<<(std::ostream& out, InstFormatMode mode) { + switch(mode) { + case INST_FORMAT_MODE_DEFAULT: + out << "INST_FORMAT_MODE_DEFAULT"; + break; + case INST_FORMAT_MODE_SZS: + out << "INST_FORMAT_MODE_SZS"; + break; + default: + out << "InstFormatMode:UNKNOWN![" << unsigned(mode) << "]"; + } + return out; +} + +}/* CVC4 namespace */ diff --git a/src/options/printer_modes.h b/src/options/printer_modes.h new file mode 100644 index 000000000..f18799aaa --- /dev/null +++ b/src/options/printer_modes.h @@ -0,0 +1,48 @@ +/********************* */ +/*! \file printer_modes.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** 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__PRINTER__MODES_H +#define __CVC4__PRINTER__MODES_H + +#include <iostream> + +namespace CVC4 { + +/** Enumeration of model_format modes (how to print models from get-model command). */ +typedef enum { + /** default mode (print expressions in the output language format) */ + MODEL_FORMAT_MODE_DEFAULT, + /** print functional values in a table format */ + MODEL_FORMAT_MODE_TABLE, +} ModelFormatMode; + +/** Enumeration of inst_format modes (how to print models from get-model command). */ +typedef enum { + /** default mode (print expressions in the output language format) */ + INST_FORMAT_MODE_DEFAULT, + /** print as SZS proof */ + INST_FORMAT_MODE_SZS, +} InstFormatMode; + +std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, InstFormatMode mode) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__PRINTER__MODEL_FORMAT_H */ diff --git a/src/options/printer_options b/src/options/printer_options new file mode 100644 index 000000000..7491570c6 --- /dev/null +++ b/src/options/printer_options @@ -0,0 +1,14 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module PRINTER "options/printer_options.h" Printing + +option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::options::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "options/printer_modes.h" :handler-include "options/options_handler_interface.h" + print format mode for models, see --model-format=help + +option instFormatMode --inst-format=MODE InstFormatMode :handler CVC4::options::stringToInstFormatMode :default INST_FORMAT_MODE_DEFAULT :read-write :include "options/printer_modes.h" :handler-include "options/options_handler_interface.h" + print format mode for instantiations, see --inst-format=help + +endmodule diff --git a/src/options/proof_options b/src/options/proof_options new file mode 100644 index 000000000..7feb00b0d --- /dev/null +++ b/src/options/proof_options @@ -0,0 +1,8 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module PROOF "options/proof_options.h" Proof + +endmodule diff --git a/src/options/prop_options b/src/options/prop_options new file mode 100644 index 000000000..3c3198147 --- /dev/null +++ b/src/options/prop_options @@ -0,0 +1,31 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module PROP "options/prop_options.h" SAT layer + +option satRandomFreq random-frequency --random-freq=P double :default 0.0 :predicate options::greater_equal(0.0) options::less_equal(1.0) + sets the frequency of random decisions in the sat solver (P=0.0 by default) +option satRandomSeed random-seed --random-seed=S uint32_t :default 0 :read-write + sets the random seed for the sat solver + +option satVarDecay double :default 0.95 :predicate options::less_equal(1.0) options::greater_equal(0.0) + variable activity decay factor for Minisat +option satClauseDecay double :default 0.999 :predicate options::less_equal(1.0) options::greater_equal(0.0) + clause activity decay factor for Minisat +option satRestartFirst --restart-int-base=N unsigned :default 25 + sets the base restart interval for the sat solver (N=25 by default) +option satRestartInc --restart-int-inc=F double :default 3.0 :predicate options::greater_equal(0.0) + sets the restart interval increase factor for the sat solver (F=3.0 by default) + +option sat_refine_conflicts --refine-conflicts bool :default false + refine theory conflict clauses (default false) + +option minisatUseElim --minisat-elimination bool :default true :read-write + use Minisat elimination + +option minisatDumpDimacs --minisat-dump-dimacs bool :default false + instead of solving minisat dumps the asserted clauses in Dimacs format + +endmodule diff --git a/src/options/quantifiers_modes.cpp b/src/options/quantifiers_modes.cpp new file mode 100644 index 000000000..e87f00d65 --- /dev/null +++ b/src/options/quantifiers_modes.cpp @@ -0,0 +1,85 @@ +/********************* */ +/*! \file quantifiers_modes.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** 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 "options/quantifiers_modes.h" + +#include <iostream> + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) { + switch(mode) { + case theory::quantifiers::INST_WHEN_PRE_FULL: + out << "INST_WHEN_PRE_FULL"; + break; + case theory::quantifiers::INST_WHEN_FULL: + out << "INST_WHEN_FULL"; + break; + case theory::quantifiers::INST_WHEN_FULL_LAST_CALL: + out << "INST_WHEN_FULL_LAST_CALL"; + break; + case theory::quantifiers::INST_WHEN_LAST_CALL: + out << "INST_WHEN_LAST_CALL"; + break; + default: + out << "InstWhenMode!UNKNOWN"; + } + + return out; +} + +std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMode mode) { + switch(mode) { + case theory::quantifiers::LITERAL_MATCH_NONE: + out << "LITERAL_MATCH_NONE"; + break; + case theory::quantifiers::LITERAL_MATCH_PREDICATE: + out << "LITERAL_MATCH_PREDICATE"; + break; + case theory::quantifiers::LITERAL_MATCH_EQUALITY: + out << "LITERAL_MATCH_EQUALITY"; + break; + default: + out << "LiteralMatchMode!UNKNOWN"; + } + + return out; +} + +std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) { + switch(mode) { + case theory::quantifiers::MBQI_GEN_EVAL: + out << "MBQI_GEN_EVAL"; + break; + case theory::quantifiers::MBQI_NONE: + out << "MBQI_NONE"; + break; + case theory::quantifiers::MBQI_FMC: + out << "MBQI_FMC"; + break; + case theory::quantifiers::MBQI_ABS: + out << "MBQI_ABS"; + break; + case theory::quantifiers::MBQI_TRUST: + out << "MBQI_TRUST"; + break; + default: + out << "MbqiMode!UNKNOWN"; + } + return out; +} + +}/* CVC4 namespace */ diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h new file mode 100644 index 000000000..540db38ec --- /dev/null +++ b/src/options/quantifiers_modes.h @@ -0,0 +1,173 @@ +/********************* */ +/*! \file quantifiers_modes.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** 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__BASE__QUANTIFIERS_MODES_H +#define __CVC4__BASE__QUANTIFIERS_MODES_H + +#include <iostream> + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +enum InstWhenMode { + /** Apply instantiation round before full effort (possibly at standard effort) */ + INST_WHEN_PRE_FULL, + /** Apply instantiation round at full effort or above */ + INST_WHEN_FULL, + /** Apply instantiation round at full effort, after all other theories finish, or above */ + INST_WHEN_FULL_DELAY, + /** Apply instantiation round at full effort half the time, and last call always */ + INST_WHEN_FULL_LAST_CALL, + /** Apply instantiation round at full effort after all other theories finish half the time, and last call always */ + INST_WHEN_FULL_DELAY_LAST_CALL, + /** Apply instantiation round at last call only */ + INST_WHEN_LAST_CALL, +}; + +enum LiteralMatchMode { + /** Do not consider polarity of patterns */ + LITERAL_MATCH_NONE, + /** Consider polarity of boolean predicates only */ + LITERAL_MATCH_PREDICATE, + /** Consider polarity of boolean predicates, as well as equalities */ + LITERAL_MATCH_EQUALITY, +}; + +enum MbqiMode { + /** mbqi from CADE 24 paper */ + MBQI_GEN_EVAL, + /** no mbqi */ + MBQI_NONE, + /** default, mbqi from Section 5.4.2 of AJR thesis */ + MBQI_FMC, + /** mbqi with integer intervals */ + MBQI_FMC_INTERVAL, + /** abstract mbqi algorithm */ + MBQI_ABS, + /** mbqi trust (produce no instantiations) */ + MBQI_TRUST, +}; + +enum QcfWhenMode { + /** default, apply at full effort */ + QCF_WHEN_MODE_DEFAULT, + /** apply at last call */ + QCF_WHEN_MODE_LAST_CALL, + /** apply at standard effort */ + QCF_WHEN_MODE_STD, + /** apply based on heuristics */ + QCF_WHEN_MODE_STD_H, +}; + +enum QcfMode { + /** default, use qcf for conflicts only */ + QCF_CONFLICT_ONLY, + /** use qcf for conflicts and propagations */ + QCF_PROP_EQ, + /** use qcf for conflicts, propagations and heuristic instantiations */ + QCF_PARTIAL, + /** use qcf for model checking */ + QCF_MC, +}; + +enum UserPatMode { + /** use but do not trust */ + USER_PAT_MODE_USE, + /** default, if patterns are supplied for a quantifier, use only those */ + USER_PAT_MODE_TRUST, + /** resort to user patterns only when necessary */ + USER_PAT_MODE_RESORT, + /** ignore user patterns */ + USER_PAT_MODE_IGNORE, + /** interleave use/resort for user patterns */ + USER_PAT_MODE_INTERLEAVE, +}; + +enum TriggerSelMode { + /** default for trigger selection */ + TRIGGER_SEL_DEFAULT, + /** only consider minimal terms for triggers */ + TRIGGER_SEL_MIN, + /** only consider maximal terms for triggers */ + TRIGGER_SEL_MAX, +}; + +enum CVC4_PUBLIC PrenexQuantMode { + /** default : prenex quantifiers without user patterns */ + PRENEX_NO_USER_PAT, + /** prenex all */ + PRENEX_ALL, + /** prenex none */ + PRENEX_NONE, +}; + +enum CegqiFairMode { + /** enforce fairness by UF corresponding to datatypes size */ + CEGQI_FAIR_UF_DT_SIZE, + /** enforce fairness by datatypes size */ + CEGQI_FAIR_DT_SIZE, + /** enforce fairness by datatypes height bound */ + CEGQI_FAIR_DT_HEIGHT_PRED, + /** do not use fair strategy for CEGQI */ + CEGQI_FAIR_NONE, +}; + +enum TermDbMode { + /** consider all terms in master equality engine */ + TERM_DB_ALL, + /** consider only relevant terms */ + TERM_DB_RELEVANT, +}; + +enum IteLiftQuantMode { + /** do not lift ITEs in quantified formulas */ + ITE_LIFT_QUANT_MODE_NONE, + /** only lift ITEs in quantified formulas if reduces the term size */ + ITE_LIFT_QUANT_MODE_SIMPLE, + /** lift ITEs */ + ITE_LIFT_QUANT_MODE_ALL, +}; + +enum SygusInvTemplMode { + /** synthesize I( x ) */ + SYGUS_INV_TEMPL_MODE_NONE, + /** synthesize ( pre( x ) V I( x ) ) */ + SYGUS_INV_TEMPL_MODE_PRE, + /** synthesize ( post( x ) ^ I( x ) ) */ + SYGUS_INV_TEMPL_MODE_POST, +}; + +enum MacrosQuantMode { + /** infer all definitions */ + MACROS_QUANT_MODE_ALL, + /** infer ground definitions */ + MACROS_QUANT_MODE_GROUND, + /** infer ground uf definitions */ + MACROS_QUANT_MODE_GROUND_UF, +}; + +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ + +std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__BASE__QUANTIFIERS_MODES_H */ diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options new file mode 100644 index 000000000..5bc20f9a8 --- /dev/null +++ b/src/options/quantifiers_options @@ -0,0 +1,297 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module QUANTIFIERS "options/quantifiers_options.h" Quantifiers + +#### rewriter options + +# Whether to mini-scope quantifiers. +# For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to +# ( forall x. P( x ) ) ^ ( forall x. Q( x ) ) +option miniscopeQuant --miniscope-quant bool :default true :read-write + miniscope quantifiers +# Whether to mini-scope quantifiers based on formulas with no free variables. +# For example, forall x. ( P( x ) V Q ) will be rewritten to +# ( forall x. P( x ) ) V Q +option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write + miniscope quantifiers for ground subformulas +option quantSplit --quant-split bool :default true + apply splitting to quantified formulas based on variable disjoint disjuncts +option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "options/quantifiers_modes.h" :read-write :handler CVC4::options::stringToPrenexQuantMode :handler-include "options/options_handler_interface.h" + prenex mode for quantified formulas +# Whether to variable-eliminate quantifiers. +# For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to +# forall y. P( c, y ) +option varElimQuant --var-elim-quant bool :default true + enable simple variable elimination for quantified formulas +option dtVarExpandQuant --dt-var-exp-quant bool :default true + expand datatype variables bound to one constructor in quantifiers +#ite lift mode for quantified formulas +option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuantMode :default CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE :include "options/quantifiers_modes.h" :read-write :handler CVC4::options::stringToIteLiftQuantMode :handler-include "options/options_handler_interface.h" + ite lifting mode for quantified formulas +option condVarSplitQuant --cond-var-split-quant bool :default true + split quantified formulas that lead to variable eliminations +option condVarSplitQuantAgg --cond-var-split-agg-quant bool :default false + aggressive split quantified formulas that lead to variable eliminations +option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false + split ites with dt testers as conditions +# Whether to CNF quantifier bodies +# option cnfQuant --cnf-quant bool :default false +# apply CNF conversion to quantified formulas +option nnfQuant --nnf-quant bool :default true + apply NNF conversion to quantified formulas +# Whether to pre-skolemize quantifier bodies. +# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to +# forall x. P( x ) => f( S( x ) ) = x +option preSkolemQuant --pre-skolem-quant bool :read-write :default false + apply skolemization eagerly to bodies of quantified formulas +option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default true + apply skolemization to nested quantified formulass +option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true + apply skolemization to quantified formulas aggressively +option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false + perform aggressive miniscoping for quantifiers +option elimTautQuant --elim-taut-quant bool :default true + eliminate tautological disjuncts of quantified formulas +option purifyQuant --purify-quant bool :default false + purify quantified formulas + +#### E-matching options + +option eMatching --e-matching bool :read-write :default true + whether to do heuristic E-matching + +option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default CVC4::theory::quantifiers::TERM_DB_ALL :read-write :include "options/quantifiers_modes.h" :handler CVC4::options::stringToTermDbMode :handler-include "options/options_handler_interface.h" + which ground terms to consider for instantiation +option registerQuantBodyTerms --register-quant-body-terms bool :default false + consider ground terms within bodies of quantified formulas for matching + +option smartTriggers --smart-triggers bool :default true + enable smart triggers +option relevantTriggers --relevant-triggers bool :default false + prefer triggers that are more relevant based on SInE style analysis +option relationalTriggers --relational-triggers bool :default false + choose relational triggers such as x = f(y), x >= f(y) +option purifyTriggers --purify-triggers bool :default false :read-write + purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1 +option purifyDtTriggers --purify-dt-triggers bool :default false :read-write + purify dt triggers, match all constructors of correct form instead of selectors +option pureThTriggers --pure-th-triggers bool :default false :read-write + use pure theory terms as single triggers +option partialTriggers --partial-triggers bool :default false :read-write + use triggers that do not contain all free variables +option multiTriggerWhenSingle --multi-trigger-when-single bool :default false + select multi triggers when single triggers exist +option multiTriggerPriority --multi-trigger-priority bool :default false + only try multi triggers if single triggers give no instantiations +option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "options/quantifiers_modes.h" :handler CVC4::options::stringToTriggerSelMode :handler-include "options/options_handler_interface.h" + selection mode for triggers +option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "options/quantifiers_modes.h" :handler CVC4::options::stringToUserPatMode :handler-include "options/options_handler_interface.h" + policy for handling user-provided patterns for quantifier instantiation +option incrementTriggers --increment-triggers bool :default true + generate additional triggers as needed during search + +option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "options/quantifiers_modes.h" :handler CVC4::options::stringToInstWhenMode :handler-include "options/options_handler_interface.h" :predicate CVC4::options::checkInstWhenMode :predicate-include "options/options_handler_interface.h" + when to apply instantiation + +option instMaxLevel --inst-max-level=N int :read-write :default -1 + maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) +option instLevelInputOnly --inst-level-input-only bool :default true + only input terms are assigned instantiation level zero +option internalReps --quant-internal-reps bool :default true + instantiate with representatives chosen by quantifiers engine + +option eagerInstQuant --eager-inst-quant bool :default false + apply quantifier instantiation eagerly + +option fullSaturateQuant --full-saturate-quant bool :default false :read-write + when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown +option fullSaturateQuantRd --full-saturate-quant-rd bool :default true + whether to use relevant domain first for full saturation instantiation strategy +option fullSaturateInst --fs-inst bool :default false + interleave full saturate instantiation with other techniques + +option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "options/quantifiers_modes.h" :handler CVC4::options::stringToLiteralMatchMode :handler-include "options/options_handler_interface.h" :predicate CVC4::options::checkLiteralMatchMode :predicate-include "options/options_handler_interface.h" + choose literal matching mode + +### finite model finding options + +option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write + use finite model finding heuristic for quantifier instantiation + +option quantFunWellDefined --quant-fun-wd bool :default false + assume that function defined by quantifiers are well defined +option fmfFunWellDefined --fmf-fun bool :default false :read-write + find models for recursively defined functions, assumes functions are admissible +option fmfFunWellDefinedRelevant --fmf-fun-rlv bool :default false + find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant +option fmfEmptySorts --fmf-empty-sorts bool :default false + allow finite model finding to assume sorts that do not occur in ground assertions are empty + +option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "options/quantifiers_modes.h" :handler CVC4::options::stringToMbqiMode :handler-include "options/options_handler_interface.h" :predicate CVC4::options::checkMbqiMode :predicate-include "options/options_handler_interface.h" + choose mode for model-based quantifier instantiation +option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default false + only add one instantiation per quantifier per round for mbqi +option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false + only add instantiations for one quantifier per round for mbqi + +option fmfInstEngine --fmf-inst-engine bool :default false + use instantiation engine in conjunction with finite model finding +option fmfInstGen --fmf-inst-gen bool :default true + enable Inst-Gen instantiation techniques for finite model finding +option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false + only perform Inst-Gen instantiation techniques on one quantifier per round +option fmfFreshDistConst --fmf-fresh-dc bool :default false + use fresh distinguished representative when applying Inst-Gen techniques +option fmfFmcSimple --fmf-fmc-simple bool :default true + simple models in full model check for finite model finding +option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write + finite model finding on bounded integer quantification +option fmfBoundIntLazy --fmf-bound-int-lazy bool :default false :read-write + enforce bounds for bounded integer quantification lazily via use of proxy variables + +### conflict-based instantiation options + +option quantConflictFind --quant-cf bool :read-write :default true + enable conflict find mechanism for quantifiers +option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default CVC4::theory::quantifiers::QCF_PROP_EQ :include "options/quantifiers_modes.h" :handler CVC4::options::stringToQcfMode :handler-include "options/options_handler_interface.h" + what effort to apply conflict find mechanism +option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "options/quantifiers_modes.h" :handler CVC4::options::stringToQcfWhenMode :handler-include "options/options_handler_interface.h" + when to invoke conflict find mechanism for quantifiers +option qcfTConstraint --qcf-tconstraint bool :read-write :default false + enable entailment checks for t-constraints in qcf algorithm +option qcfAllConflict --qcf-all-conflict bool :read-write :default false + add all available conflicting instances during conflict-based instantiation + +option instNoEntail --inst-no-entail bool :read-write :default true + do not consider instances of quantified formulas that are currently entailed + +### rewrite rules options + +option quantRewriteRules --rewrite-rules bool :default false + use rewrite rules module +option rrOneInstPerRound --rr-one-inst-per-round bool :default false + add one instance of rewrite rule per round + +### induction options + +option quantInduction --quant-ind bool :default false + use all available techniques for inductive reasoning +option dtStcInduction --dt-stc-ind bool :read-write :default false + apply strengthening for existential quantification over datatypes based on structural induction +option intWfInduction --int-wf-ind bool :read-write :default false + apply strengthening for integers based on well-founded induction +option conjectureGen --conjecture-gen bool :read-write :default false + generate candidate conjectures for inductive proofs + +option conjectureGenPerRound --conjecture-gen-per-round=N int :default 1 + number of conjectures to generate per instantiation round +option conjectureNoFilter --conjecture-no-filter bool :default false + do not filter conjectures +option conjectureFilterActiveTerms --conjecture-filter-active-terms bool :read-write :default true + filter based on active terms +option conjectureFilterCanonical --conjecture-filter-canonical bool :read-write :default true + filter based on canonicity +option conjectureFilterModel --conjecture-filter-model bool :read-write :default true + filter based on model +option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 50 + number of ground terms to generate for model filtering +option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false + more aggressive merging for universal equality engine, introduces terms + +### synthesis options + +option ceGuidedInst --cegqi bool :default false :read-write + counterexample-guided quantifier instantiation +option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "options/quantifiers_modes.h" :handler CVC4::options::stringToCegqiFairMode :handler-include "options/options_handler_interface.h" + if and how to apply fairness for cegqi +option cegqiSingleInv --cegqi-si bool :default false :read-write + process single invocation synthesis conjectures +option cegqiSingleInvPartial --cegqi-si-partial bool :default false + combined techniques for synthesis conjectures that are partially single invocation +option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true + reconstruct solutions for single invocation conjectures in original grammar +option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true + include constants when reconstruct solutions for single invocation conjectures in original grammar +option cegqiSingleInvAbort --cegqi-si-abort bool :default false + abort if synthesis conjecture is not single invocation +option cegqiSingleInvMultiInstAbort --cegqi-si-multi-inst-abort bool :default false + abort if synthesis conjecture is single invocation with no ITE in grammar and multiple instantiations are tried + +option sygusNormalForm --sygus-nf bool :default true + only search for sygus builtin terms that are in normal form +option sygusNormalFormArg --sygus-nf-arg bool :default true + account for relationship between arguments of operations in sygus normal form +option sygusNormalFormGlobal --sygus-nf-sym bool :default true + narrow sygus search space based on global state of current candidate program +option sygusNormalFormGlobalGen --sygus-nf-sym-gen bool :default true + generalize lemmas for global search space narrowing +option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true + generalize based on arguments in global search space narrowing +option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true + generalize based on content in global search space narrowing + +option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "options/quantifiers_modes.h" :handler CVC4::options::stringToSygusInvTemplMode :handler-include "options/options_handler_interface.h" + template mode for sygus invariant synthesis + +# approach applied to general quantified formulas +option cbqiSplx --cbqi-splx bool :read-write :default false + turns on old implementation of counterexample-based quantifier instantiation +option cbqi --cbqi bool :read-write :default false + turns on counterexample-based quantifier instantiation +option recurseCbqi --cbqi-recurse bool :default true + turns on recursive counterexample-based quantifier instantiation +option cbqiSat --cbqi-sat bool :read-write :default true + answer sat when quantifiers are asserted with counterexample-based quantifier instantiation +option cbqiModel --cbqi-model bool :read-write :default true + guide instantiations by model values for counterexample-based quantifier instantiation +option cbqiAll --cbqi-all bool :read-write :default false + apply counterexample-based instantiation to all quantified formulas +option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false + use integer infinity for vts in counterexample-based quantifier instantiation +option cbqiUseInfReal --cbqi-use-inf-real bool :read-write :default false + use real infinity for vts in counterexample-based quantifier instantiation +option cbqiPreRegInst --cbqi-prereg-inst bool :read-write :default false + preregister ground instantiations in counterexample-based quantifier instantiation +option cbqiMinBounds --cbqi-min-bounds bool :default false + use minimally constrained lower/upper bound for counterexample-based quantifier instantiation +option cbqiSymLia --cbqi-sym-lia bool :default false + use symbolic integer division in substitutions for counterexample-based quantifier instantiation +option cbqiRoundUpLowerLia --cbqi-round-up-lia bool :default false + round up integer lower bounds in substitutions for counterexample-based quantifier instantiation +option cbqiMidpoint --cbqi-midpoint bool :default false + choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation +option cbqiNopt --cbqi-nopt bool :default true + non-optimal bounds for counterexample-based quantifier instantiation + +### local theory extensions options + +option localTheoryExt --local-t-ext bool :default false + do instantiation based on local theory extensions +option ltePartialInst --lte-partial-inst bool :default false + partially instantiate local theory quantifiers +option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false + treat arguments of inst closure as restricted terms for instantiation + +### reduction options + +option quantAlphaEquiv --quant-alpha-equiv bool :default true + infer alpha equivalence between quantified formulas +option macrosQuant --macros-quant bool :read-write :default false + perform quantifiers macro expansion +option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF :include "options/quantifiers_modes.h" :handler CVC4::options::stringToMacrosQuantMode :handler-include "options/options_handler_interface.h" + mode for quantifiers macro expansion + +### recursive function options + +#option funDefs --fun-defs bool :default false +# enable specialized techniques for recursive function definitions + +### e-unification options + +option quantEqualityEngine --quant-ee bool :default false + maintain congrunce closure over universal equalities + +endmodule diff --git a/src/options/sets_options b/src/options/sets_options new file mode 100644 index 000000000..67bed5fe7 --- /dev/null +++ b/src/options/sets_options @@ -0,0 +1,20 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module SETS "options/sets_options.h" Sets + +option setsPropagate --sets-propagate bool :default true + determines whether to propagate learnt facts to Theory Engine / SAT solver + +option setsEagerLemmas --sets-eager-lemmas bool :default true + add lemmas even at regular effort + +expert-option setsCare1 --sets-care1 bool :default false + generate one lemma at a time for care graph + +option setsPropFull --sets-prop-full bool :default true + additional propagation at full effort + +endmodule diff --git a/src/options/simplification_mode.cpp b/src/options/simplification_mode.cpp new file mode 100644 index 000000000..08f961c15 --- /dev/null +++ b/src/options/simplification_mode.cpp @@ -0,0 +1,37 @@ +/********************* */ +/*! \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 "options/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/options/simplification_mode.h b/src/options/simplification_mode.h new file mode 100644 index 000000000..b0b78d318 --- /dev/null +++ b/src/options/simplification_mode.h @@ -0,0 +1,39 @@ +/********************* */ +/*! \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/options/smt_options b/src/options/smt_options new file mode 100644 index 000000000..f658d929a --- /dev/null +++ b/src/options/smt_options @@ -0,0 +1,164 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module SMT "options/smt_options.h" SMT layer + +common-option - dump --dump=MODE argument :handler CVC4::options::dumpMode :handler-include "options/options_handler_interface.h" + dump preprocessed assertions, etc., see --dump=help +common-option - dump-to --dump-to=FILE argument :handler CVC4::options::dumpToFile :handler-include "options/options_handler_interface.h" + all dumping goes to FILE (instead of stdout) + +expert-option forceLogic force-logic --force-logic=LOGIC LogicInfo* :include "options/logic_info_forward.h" :handler CVC4::options::stringToLogicInfo :handler-include "options/options_handler_interface.h" :default NULL + set the logic, and override all further user attempts to change it + +option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler CVC4::options::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "options/simplification_mode.h" :handler-include "options/options_handler_interface.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::options::beforeSearch :predicate-include "options/options_handler_interface.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::options::beforeSearch :predicate-include "options/options_handler_interface.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::options::proofEnabledBuild CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h" + turn on proof generation +option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.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::options::proofEnabledBuild CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.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::options::beforeSearch :predicate-include "options/options_handler_interface.h" + output unsat cores after every UNSAT/VALID response + +option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h" + support the get-assignment command + +undocumented-option interactiveMode interactive-mode bool :predicate CVC4::options::beforeSearch CVC4::options::setProduceAssertions :predicate-include "options/options_handler_interface.h" :read-write + deprecated name for produce-assertions +common-option produceAssertions produce-assertions --produce-assertions bool :predicate CVC4::options::beforeSearch CVC4::options::setProduceAssertions :predicate-include "options/options_handler_interface.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::options::setRegularOutputChannel :handler-include "options/options_handler_interface.h" + set the regular output channel of the solver +option - diagnostic-output-channel argument :handler CVC4::options::setDiagnosticOutputChannel :handler-include "options/options_handler_interface.h" + set the diagnostic output channel of the solver + +common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" :handler CVC4::options::tlimitHandler :handler-include "options/options_handler_interface.h" + enable time limiting (give milliseconds) +common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long" :handler CVC4::options::tlimitPerHandler :handler-include "options/options_handler_interface.h" + enable time limiting per query (give milliseconds) +common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" :handler CVC4::options::rlimitHandler :handler-include "options/options_handler_interface.h" + enable resource limiting (currently, roughly the number of SAT conflicts) +common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" :handler CVC4::options::rlimitPerHandler :handler-include "options/options_handler_interface.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::options::checkReplayFilename :handler-include "options/options_handler_interface.h" + replay decisions from file +undocumented-option replayLog --replay-log=FILE std::ostream* :handler CVC4::options::checkReplayLogFilename :handler-include "options/options_handler_interface.h" + log decisions and propagations to file +option replayStream ExprStream* + +# portfolio options +option lemmaInputChannel LemmaInputChannel* :default NULL :include "base/lemma_input_channel_forward.h" + The input channel to receive notfication events for new lemmas +option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "base/lemma_output_channel_forward.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/options/strings_options b/src/options/strings_options new file mode 100644 index 000000000..6247ad3a1 --- /dev/null +++ b/src/options/strings_options @@ -0,0 +1,58 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module STRINGS "options/strings_options.h" Strings theory + +option stringExp strings-exp --strings-exp bool :default false :read-write + experimental features in the theory of strings + +# :predicate-include "smt/smt_engine.h" +option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate options::less_equal(2) :predicate-include "options/base_handlers.h" + the strategy of LB rule application: 0-lazy, 1-eager, 2-no + +# :predicate-include "smt/smt_engine.h" +option stdASCII strings-std-ascii --strings-std-ascii bool :default true :predicate options::less_equal(2) :predicate-include "options/base_handlers.h" + the alphabet contains only characters from the standard ASCII or the extended one + +option stringFMF strings-fmf --strings-fmf bool :default false :read-write + the finite model finding used by the theory of strings + +option stringEager strings-eager --strings-eager bool :default false + strings eager check + +option stringEIT strings-eit --strings-eit bool :default false + the eager intersection used by the theory of strings + +option stringOpt1 strings-opt1 --strings-opt1 bool :default true + internal option1 for strings: normal form + +option stringOpt2 strings-opt2 --strings-opt2 bool :default false + internal option2 for strings: constant regexp splitting + +option stringIgnNegMembership strings-inm --strings-inm bool :default false + internal for strings: ignore negative membership constraints (fragment checking is needed, left to users for now) + +#expert-option stringCharCardinality strings-alphabet-card --strings-alphabet-card=N int16_t :default 128 :read-write +# the cardinality of the characters used by the theory of strings, default 128 (for standard ASCII) or 256 (for extended ASCII) + +option stringLazyPreproc strings-lazy-pp --strings-lazy-pp bool :default true + perform string preprocessing lazily upon assertion +option stringLazyPreproc2 strings-lazy-pp2 --strings-lazy-pp2 bool :default true + perform string preprocessing lazily upon failure to reduce + +option stringLenGeqZ strings-len-geqz --strings-len-geqz bool :default false + strings length greater than zero lemmas + +option stringLenNorm strings-len-norm --strings-len-norm bool :default true + strings length normalization lemma +option stringSplitEmp strings-sp-emp --strings-sp-emp bool :default true + strings split on empty string +option stringInferSym strings-infer-sym --strings-infer-sym bool :default true + strings split on empty string +option stringEagerLen strings-eager-len --strings-eager-len bool :default true + strings eager length lemmas + + +endmodule diff --git a/src/options/theory_options b/src/options/theory_options new file mode 100644 index 000000000..f6d6d0f84 --- /dev/null +++ b/src/options/theory_options @@ -0,0 +1,15 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module THEORY "options/theory_options.h" Theory layer + +expert-option theoryOfMode theoryof-mode --theoryof-mode=MODE CVC4::theory::TheoryOfMode :handler CVC4::options::stringToTheoryOfMode :handler-include "options/options_handler_interface.h" :default CVC4::theory::THEORY_OF_TYPE_BASED :include "options/theoryof_mode.h" :read-write + mode for Theory::theoryof() + +option - use-theory --use-theory=NAME argument :handler CVC4::options::useTheory :handler-include "options/options_handler_interface.h" + use alternate theory implementation NAME (--use-theory=help for a list) +option theoryAlternates ::std::map<std::string,bool> :include <map> :read-write + +endmodule diff --git a/src/options/theoryof_mode.cpp b/src/options/theoryof_mode.cpp new file mode 100644 index 000000000..c05f97ede --- /dev/null +++ b/src/options/theoryof_mode.cpp @@ -0,0 +1,21 @@ + +#include "options/theoryof_mode.h" + +#include <ostream> +#include "base/cvc4_assert.h" + +namespace CVC4 { +namespace theory { + +std::ostream& operator<<(std::ostream& out, TheoryOfMode m) throw() { + switch(m) { + case THEORY_OF_TYPE_BASED: return out << "THEORY_OF_TYPE_BASED"; + case THEORY_OF_TERM_BASED: return out << "THEORY_OF_TERM_BASED"; + default: return out << "TheoryOfMode!UNKNOWN"; + } + + Unreachable(); +} + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/options/theoryof_mode.h b/src/options/theoryof_mode.h new file mode 100644 index 000000000..5a8723738 --- /dev/null +++ b/src/options/theoryof_mode.h @@ -0,0 +1,38 @@ +/********************* */ +/*! \file theoryof_mode.h + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: Morgan Deters + ** 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 selection for theoryOf() operation + ** + ** Option selection for theoryOf() operation. + **/ + +#include "cvc4_public.h" + +#pragma once + +#include <ostream> + +namespace CVC4 { +namespace theory { + +/** How do we associate theories with the terms */ +enum TheoryOfMode { + /** Equality, variables and constants are associated with the types */ + THEORY_OF_TYPE_BASED, + /** Variables are uninterpreted, constants are with the type, equalities prefer parametric */ + THEORY_OF_TERM_BASED +};/* enum TheoryOfMode */ + +std::ostream& operator<<(std::ostream& out, TheoryOfMode m) throw() CVC4_PUBLIC; + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + diff --git a/src/options/uf_options b/src/options/uf_options new file mode 100644 index 000000000..baea1cb41 --- /dev/null +++ b/src/options/uf_options @@ -0,0 +1,42 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module UF "options/uf_options.h" Uninterpreted functions theory + +option ufSymmetryBreaker uf-symmetry-breaker --symmetry-breaker bool :read-write :default true + use UF symmetry breaker (Deharbe et al., CADE 2011) + +option condenseFunctionValues condense-function-values --condense-function-values bool :default true + condense models for functions rather than explicitly representing them + +option ufssRegions /--disable-uf-ss-regions bool :default true + disable region-based method for discovering cliques and splits in uf strong solver +option ufssEagerSplits --uf-ss-eager-split bool :default false + add splits eagerly for uf strong solver +option ufssTotality --uf-ss-totality bool :default false + always use totality axioms for enforcing cardinality constraints +option ufssTotalityLimited --uf-ss-totality-limited=N int :default -1 + apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default) +option ufssTotalitySymBreak --uf-ss-totality-sym-break bool :default false + apply symmetry breaking for totality axioms +option ufssAbortCardinality --uf-ss-abort-card=N int :default -1 + tells the uf strong solver a cardinality to abort at (-1 == no limit, default) +option ufssExplainedCliques --uf-ss-explained-cliques bool :default false + use explained clique lemmas for uf strong solver +option ufssSimpleCliques --uf-ss-simple-cliques bool :default true + always use simple clique lemmas for uf strong solver +option ufssDiseqPropagation --uf-ss-deq-prop bool :default false + eagerly propagate disequalities for uf strong solver +option ufssMode --uf-ss=MODE CVC4::theory::uf::UfssMode :default CVC4::theory::uf::UF_SS_FULL :include "options/options_handler_interface.h" :handler CVC4::options::stringToUfssMode :handler-include "options/options_handler_interface.h" + mode of operation for uf strong solver. +option ufssCliqueSplits --uf-ss-clique-splits bool :default false + use cliques instead of splitting on demand to shrink model + +option ufssSymBreak --uf-ss-sym-break bool :default false + finite model finding symmetry breaking techniques +option ufssFairness --uf-ss-fair bool :default true + use fair strategy for finite model finding multiple sorts + +endmodule diff --git a/src/options/ufss_mode.h b/src/options/ufss_mode.h new file mode 100644 index 000000000..25eb1d2d7 --- /dev/null +++ b/src/options/ufss_mode.h @@ -0,0 +1,40 @@ +/********************* */ +/*! \file ufss_mode.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 Custom handlers and predicates for TheoryUF options + ** + ** Custom handlers and predicates for TheoryUF options. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BASE__UFSS_MODE_H +#define __CVC4__BASE__UFSS_MODE_H + +namespace CVC4 { +namespace theory { +namespace uf { + +enum UfssMode{ + /** default, use uf strong solver to find minimal models for uninterpreted sorts */ + UF_SS_FULL, + /** use uf strong solver to shrink model sizes, but do no enforce minimality */ + UF_SS_NO_MINIMAL, + /** do not use uf strong solver */ + UF_SS_NONE, +}; + +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__BASE__UFSS_MODE_H */ + |