From: Andrew Reynolds Date: Wed, 15 Apr 2020 13:37:46 +0000 (-0500) Subject: Change option names --default-dag-thresh and --default-expr-depth (#4309) X-Git-Tag: cvc5-1.0.0~3363 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=681fece601a4f156f2d39b4813d16535b7e2cee3;p=cvc5.git Change option names --default-dag-thresh and --default-expr-depth (#4309) --- diff --git a/contrib/cvc4_strict_smtlib b/contrib/cvc4_strict_smtlib index 0a97bd74b..45c7cbe1a 100644 --- 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 546d9ee9c..111f71852 100644 --- 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 2e972a543..a3d25d7f0 100644 --- 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 53b1fa92d..1299e2928 100644 --- 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 7a8055bdf..bae2b6ef9 100755 --- 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 741706070..4bdecf7ef 100644 --- 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 ac371e835..47a7d9db7 100644 --- 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 b64758fd2..c26622fef 100644 --- 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 7fcc8f2ae..9253ea1c8 100644 --- 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 5b22945a1..b710bf0d9 100644 --- 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