From 135f99f365920097ce48be87cb77fb1144d446a3 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 26 Feb 2016 13:39:06 -0600 Subject: Refactoring of inferences in strings. Add several options. --- src/options/strings_options | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src/options/strings_options') diff --git a/src/options/strings_options b/src/options/strings_options index 1b64af83f..dee379878 100644 --- a/src/options/strings_options +++ b/src/options/strings_options @@ -55,6 +55,14 @@ option stringEagerLen strings-eager-len --strings-eager-len bool :default true strings eager length lemmas option stringCheckEntailLen strings-check-entail-len --strings-check-entail-len bool :default true check entailment between length terms to reduce splitting +option stringProcessLoop strings-process-loop --strings-process-loop bool :default true + reduce looping word equations to regular expressions +option stringAbortLoop strings-abort-loop --strings-abort-loop bool :default false + abort when a looping word equation is encountered +option stringInferAsLemmas strings-infer-as-lemmas --strings-infer-as-lemmas bool :default false + always send lemmas out instead of making internal inferences +option stringRExplainLemmas strings-rexplain-lemmas --strings-rexplain-lemmas bool :default true + regression explanations for string lemmas endmodule -- cgit v1.2.3