diff options
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 */ + |