Change option names --default-dag-thresh and --default-expr-depth (#4309)

diff --git a/contrib/cvc4_strict_smtlib b/contrib/cvc4_strict_smtlib
index 0a97bd74b3f1e05c255fd97b9afbff031558a9da..45c7cbe1a2176f311b5f83cae03e938aa5976b7b 100644 (file)
--- a/contrib/cvc4_strict_smtlib
+++ b/contrib/cvc4_strict_smtlib
@@ -5,4 +5,4 @@ cvc4="${CVC4_HOME}/cvc4"
 # This is the set of command line arguments that is required to be strictly
 # complaint with the input and output requirements of the current SMT-LIB
 # standard.
-"$cvc4" --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --abstract-values $@
+"$cvc4" --lang=smt2 --output-lang=smt2 --strict-parsing --expr-depth=-1 --print-success --incremental --abstract-values $@

diff --git a/examples/api/combination-new.cpp b/examples/api/combination-new.cpp
index 546d9ee9c08ed818f4a7c9d4eb38d004dd9b3ef2..111f718528ded8713cf1a638ff97b30d3a237230 100644 (file)
--- a/examples/api/combination-new.cpp
+++ b/examples/api/combination-new.cpp
@@ -38,7 +38,7 @@ int main()
   Solver slv;
   slv.setOption("produce-models", "true");  // Produce Models
   slv.setOption("output-language", "cvc4"); // Set the output-language to CVC's
-  slv.setOption("default-dag-thresh", "0"); // Disable dagifying the output
+  slv.setOption("dag-thresh", "0"); // Disable dagifying the output
   slv.setOption("output-language", "smt2"); // use smt-lib v2 as output language
   slv.setLogic(string("QF_UFLIRA"));
 

diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp
index 2e972a54396619558e013d7093e66c2ab97b2e2f..a3d25d7f0fced2d429327095a36cd78704c4077a 100644 (file)
--- a/examples/api/combination.cpp
+++ b/examples/api/combination.cpp
@@ -45,7 +45,7 @@ int main() {
   SmtEngine smt(&em);
   smt.setOption("produce-models", true); // Produce Models
   smt.setOption("output-language", "cvc4"); // Set the output-language to CVC's
-  smt.setOption("default-dag-thresh", 0); //Disable dagifying the output
+  smt.setOption("dag-thresh", 0); //Disable dagifying the output
   smt.setLogic(string("QF_UFLIRA"));
 
   // Sorts

diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java
index 53b1fa92db35b469e53643c24a093f207f3a50f1..1299e29286e764941ac117006c0605fec3971d0b 100644 (file)
--- a/examples/api/java/Combination.java
+++ b/examples/api/java/Combination.java
@@ -42,7 +42,7 @@ public class Combination {
     smt.setOption("tlimit", new SExpr(100));
     smt.setOption("produce-models", new SExpr(true)); // Produce Models
     smt.setOption("output-language", new SExpr("cvc4")); // output-language
-    smt.setOption("default-dag-thresh", new SExpr(0)); //Disable dagifying the output
+    smt.setOption("dag-thresh", new SExpr(0)); //Disable dagifying the output
     smt.setLogic("QF_UFLIRA");
 
     // Sorts

diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py
index 7a8055bdf2d42406607e5c23d34d69153445d654..bae2b6ef95da1deb9def7237fd0b784eecd9225f 100755 (executable)
--- a/examples/api/python/combination.py
+++ b/examples/api/python/combination.py
@@ -26,7 +26,7 @@ if __name__ == "__main__":
     slv = pycvc4.Solver()
     slv.setOption("produce-models", "true")  # Produce Models
     slv.setOption("output-language", "cvc4") # Set the output-language to CVC's
-    slv.setOption("default-dag-thresh", "0") # Disable dagifying the output
+    slv.setOption("dag-thresh", "0") # Disable dagifying the output
     slv.setOption("output-language", "smt2") # use smt-lib v2 as output language
     slv.setLogic("QF_UFLIRA")
 

diff --git a/examples/translator.cpp b/examples/translator.cpp
index 7417060705f70304241031eabdaf12c521220f61..4bdecf7efa141be0322b74ed9bd3f18ddc4eae03 100644 (file)
--- a/examples/translator.cpp
+++ b/examples/translator.cpp
@@ -47,7 +47,7 @@ const struct option longopts[] = {
   { "output-language", required_argument, NULL, OUTPUT_LANG },
   { "expand-definitions", no_argument, NULL, EXPAND_DEFINITIONS },
   { "combine-assertions", no_argument, NULL, COMBINE_ASSERTIONS },
-  { "default-dag-thresh", required_argument, NULL, DEFAULT_DAG_THRESH },
+  { "dag-thresh", required_argument, NULL, DEFAULT_DAG_THRESH },
   { "lang", required_argument, NULL, INPUT_LANG },
   { "language", required_argument, NULL, INPUT_LANG },
   { "out", required_argument, NULL, OUTPUT_FILE },
@@ -60,7 +60,7 @@ static void showHelp() {
        << "  --output-language | -O  set output language (default smt2)" << endl
        << "  --input-language | -L   set input language (default auto)" << endl
        << "  --out | -o              set output file (- for stdout)" << endl
-       << "  --default-dag-thresh=N  set DAG threshold" << endl
+       << "  --dag-thresh=N  set DAG threshold" << endl
        << "  --expand-definitions    expand define-funs" << endl
        << "  --combine-assertions    combine all assertions into one" << endl
        << "  --help | -h             this help" << endl
@@ -237,14 +237,14 @@ int main(int argc, char* argv[]) {
         break;
       case DEFAULT_DAG_THRESH: {
           if(!isdigit(*optarg)) {
-            cerr << "error: --default-dag-thresh requires non-negative argument: `"
+            cerr << "error: --dag-thresh requires non-negative argument: `"
                  << optarg << "' invalid." << endl;
             exit(1);
           }
           char* end;
           unsigned long ul = strtoul(optarg, &end, 10);
           if(errno != 0 || *end != '\0') {
-            cerr << "error: --default-dag-thresh argument malformed: `"
+            cerr << "error: --dag-thresh argument malformed: `"
                  << optarg << "'." << endl;
             exit(1);
           }

diff --git a/src/options/README b/src/options/README
index ac371e835b0120ed4dfbbe5cc3d163746ee797e0..47a7d9db7d3be5b64e657ec966b2f1065327ef89 100644 (file)
--- a/src/options/README
+++ b/src/options/README
@@ -111,7 +111,7 @@ Aliases
     [[alias]]
       category   = "regular"
       long       = "smtlib-strict"
-      links      = ["--lang=smt2", "--output-lang=smt2", "--strict-parsing", "--default-expr-depth=-1", "--print-success", "--incremental", "--abstract-values"]
+      links      = ["--lang=smt2", "--output-lang=smt2", "--strict-parsing", "--expr-depth=-1", "--print-success", "--incremental", "--abstract-values"]
       help       = "SMT-LIBv2 compliance mode (implies other options)"
 
 
@@ -123,7 +123,7 @@ Aliases
 
   is equivalent to specifying the options
 
-    --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --abstract-values
+    --lang=smt2 --output-lang=smt2 --strict-parsing --expr-depth=-1 --print-success --incremental --abstract-values
 
 
   It's also possible to pass an argument through to another option.

diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml
index b64758fd2caea589f3778397fbf355ba525e74a1..c26622fef70c52fb47e32d7abee3525879bd34c2 100644 (file)
--- a/src/options/expr_options.toml
+++ b/src/options/expr_options.toml
@@ -5,7 +5,7 @@ header = "options/expr_options.h"
 [[option]]
   name       = "defaultExprDepth"
   category   = "regular"
-  long       = "default-expr-depth=N"
+  long       = "expr-depth=N"
   type       = "int"
   default    = "0"
   predicates = ["setDefaultExprDepthPredicate"]
@@ -15,9 +15,9 @@ header = "options/expr_options.h"
 
 [[option]]
   name       = "defaultDagThresh"
-  smt_name   = "default-dag-thresh"
+  smt_name   = "dag-thresh"
   category   = "regular"
-  long       = "default-dag-thresh=N"
+  long       = "dag-thresh=N"
   type       = "int"
   default    = "1"
   predicates = ["setDefaultDagThreshPredicate"]

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 7fcc8f2ae1f7c10c754a14e0ab5bdb589ea627e3..9253ea1c82668a26a2ad9e455e9fd4ae36dec545 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -350,13 +350,13 @@ void OptionsHandler::notifyDumpMode(std::string option)
 // expr/options_handlers.h
 void OptionsHandler::setDefaultExprDepthPredicate(std::string option, int depth) {
   if(depth < -1) {
-    throw OptionException("--default-expr-depth requires a positive argument, or -1.");
+    throw OptionException("--expr-depth requires a positive argument, or -1.");
   }
 }
 
 void OptionsHandler::setDefaultDagThreshPredicate(std::string option, int dag) {
   if(dag < 0) {
-    throw OptionException("--default-dag-thresh requires a nonnegative argument.");
+    throw OptionException("--dag-thresh requires a nonnegative argument.");
   }
 }
 

diff --git a/test/java/Combination.java b/test/java/Combination.java
index 5b22945a1cd5476b4d316470adc641099aa62b73..b710bf0d95daa8b08c30b9ce6fd5931eb0f41e68 100644 (file)
--- a/test/java/Combination.java
+++ b/test/java/Combination.java
@@ -39,7 +39,7 @@ public class Combination {
     smt.setOption("tlimit", new SExpr(100));
     smt.setOption("produce-models", new SExpr(true)); // Produce Models
     smt.setOption("output-language", new SExpr("cvc4")); // output-language
-    smt.setOption("default-dag-thresh", new SExpr(0)); //Disable dagifying the output
+    smt.setOption("dag-thresh", new SExpr(0)); //Disable dagifying the output
     smt.setLogic("QF_UFLIRA");
 
     // Sorts