diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-06-17 15:55:56 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-06-17 15:57:28 -0500 |
commit | 1a2547995acc5a98c8969e628ac5e1c45b0efe94 (patch) | |
tree | 0d9abd19ba7b3b742da3e745da00c0457237f84b /src/options | |
parent | 0348b525a951a8709f9dc4b5757ce0bcb48a9472 (diff) |
Support for separation logic. Enable cbqi by default for pure BV.
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/Makefile.am | 12 | ||||
-rw-r--r-- | src/options/sep_options | 20 |
2 files changed, 29 insertions, 3 deletions
diff --git a/src/options/Makefile.am b/src/options/Makefile.am index e8a18481b..1eb84b45f 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -30,6 +30,7 @@ OPTIONS_SRC_FILES = \ proof_options \ prop_options \ quantifiers_options \ + sep_options \ sets_options \ smt_options \ strings_options \ @@ -54,6 +55,7 @@ OPTIONS_TEMPS = \ proof_options.tmp \ prop_options.tmp \ quantifiers_options.tmp \ + sep_options.tmp \ sets_options.tmp \ smt_options.tmp \ strings_options.tmp \ @@ -78,6 +80,7 @@ OPTIONS_OPTIONS_FILES = \ proof_options.options \ prop_options.options \ quantifiers_options.options \ + sep_options.options \ sets_options.options \ smt_options.options \ strings_options.options \ @@ -102,6 +105,7 @@ OPTIONS_SEDS = \ proof_options.sed \ prop_options.sed \ quantifiers_options.sed \ + sep_options.sed \ sets_options.sed \ smt_options.sed \ strings_options.sed \ @@ -126,6 +130,7 @@ OPTIONS_HEADS = \ proof_options.h \ prop_options.h \ quantifiers_options.h \ + sep_options.h \ sets_options.h \ smt_options.h \ strings_options.h \ @@ -150,6 +155,7 @@ OPTIONS_CPPS = \ proof_options.cpp \ prop_options.cpp \ quantifiers_options.cpp \ + sep_options.cpp \ sets_options.cpp \ smt_options.cpp \ strings_options.cpp \ @@ -295,14 +301,14 @@ options_holder_template.h options_template.cpp options_get_option_template.cpp o # 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:; +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 sep_options sets_options smt_options strings_options theory_options uf_options:; # 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 +.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 sep_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: +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 sep_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: diff --git a/src/options/sep_options b/src/options/sep_options new file mode 100644 index 000000000..043355bda --- /dev/null +++ b/src/options/sep_options @@ -0,0 +1,20 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module SEP "options/sep_options.h" Sep + +option sepCheckNeg --sep-check-neg bool :default true + check negated spatial assertions + +option sepExp --sep-exp bool :default false + experimental flag for sep +option sepMinimalRefine --sep-min-refine bool :default false + only add refinement lemmas for minimal (innermost) assertions +option sepPreciseBound --sep-prec-bound bool :default false + calculate precise bounds for labels +option sepDisequalC --sep-deq-c bool :default true + assume cardinality elements are distinct + +endmodule |