diff options
Diffstat (limited to 'examples')
-rw-r--r-- | examples/api/combination-new.cpp | 2 | ||||
-rw-r--r-- | examples/api/combination.cpp | 2 | ||||
-rw-r--r-- | examples/api/java/Combination.java | 2 | ||||
-rwxr-xr-x | examples/api/python/combination.py | 2 | ||||
-rw-r--r-- | examples/translator.cpp | 8 |
5 files changed, 8 insertions, 8 deletions
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); } |