projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 2c78f3b)
Disable re-elim by default (#4508)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 21 May 2020 23:33:14 +0000 (18:33 -0500)
committerGitHub <noreply@github.com>
Thu, 21 May 2020 23:33:14 +0000 (18:33 -0500)
Disabling re-elim performs better overall in many recent experiments.

src/options/strings_options.toml patch | blob | history
test/regress/regress1/strings/complement-test.smt2 patch | blob | history

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 44ca2c390a40a83142a54af1c8ed090728dddd45..3cf8f585214ea40db7b14fd0f934fa716f6d2e6a 100644 (file)
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -174,7 +174,7 @@ header = "options/strings_options.h"
   category   = "regular"
   long       = "re-elim"
   type       = "bool"
-  default    = "true"
+  default    = "false"
   help       = "elimination techniques for regular expressions"
 
 [[option]]
diff --git a/test/regress/regress1/strings/complement-test.smt2 b/test/regress/regress1/strings/complement-test.smt2
index 5d3c8310f9d29b68815114a46086f7a2c88c932e..0bb74a2395ccc9bf71fbf684e81a8f3a034c5608 100644 (file)
--- a/test/regress/regress1/strings/complement-test.smt2
+++ b/test/regress/regress1/strings/complement-test.smt2
@@ -1,4 +1,5 @@
 (set-logic SLIA)
+(set-option :strings-exp true)
 (set-info :status sat)
 (declare-fun x () String)
 (declare-fun y () String)