From 45e489e2d48e3edde15be2187e32893fc35d859b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 6 Apr 2020 16:44:01 -0500 Subject: [PATCH] Remove links field in all toml files (#4201) This includes: All options pertaining to SMTEngine are now handled at the top of setDefaults. smtlibStrict was deleted in favor of a script. statsEveryQuery enables stats by modifying a public option function. This is a slight hack but this code will likely get refactored as well soon. A few other changes: Fix a bug in SMTEngine: defineFunction should finalize options. Call setDefaults before initilizing the TheoryEngine and ProofManager. This is necessary so that the PROOF(...) macro works earlier during initialization. The next step will be to remove the links infrastructure for the options infrastructure. This will enable further detangling of our options dependencies. --- contrib/cvc4_strict_smtlib | 8 +++++ src/options/base_options.toml | 7 ---- src/options/bv_options.toml | 3 -- src/options/options_public_functions.cpp | 3 +- src/options/smt_options.toml | 12 ------- src/smt/set_defaults.cpp | 43 ++++++++++++++++++++++++ src/smt/smt_engine.cpp | 13 +++---- 7 files changed, 60 insertions(+), 29 deletions(-) create mode 100644 contrib/cvc4_strict_smtlib diff --git a/contrib/cvc4_strict_smtlib b/contrib/cvc4_strict_smtlib new file mode 100644 index 000000000..0a97bd74b --- /dev/null +++ b/contrib/cvc4_strict_smtlib @@ -0,0 +1,8 @@ +#!/bin/bash + +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 $@ diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 43060bc54..65eeda3ae 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -99,7 +99,6 @@ header = "options/base_options.h" long = "stats-every-query" type = "bool" default = "false" - links = ["--stats"] read_only = true help = "in incremental mode, print stats after every satisfiability or validity query" @@ -155,9 +154,3 @@ header = "options/base_options.h" notifies = ["notifyPrintSuccess"] read_only = true help = "print the \"success\" output required of SMT-LIBv2" - -[[alias]] - category = "regular" - long = "smtlib-strict" - links = ["--lang=smt2", "--output-lang=smt2", "--strict-parsing", "--default-expr-depth=-1", "--print-success", "--incremental", "--abstract-values"] - help = "SMT-LIBv2 compliance mode (implies other options)" diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 489f33ed7..05dc6b716 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -88,7 +88,6 @@ header = "options/bv_options.h" long = "bv-aig-simp=COMMAND" type = "std::string" predicates = ["abcEnabledBuild"] - links = ["--bitblast-aig"] help = "abc command to run AIG simplifications (implies --bitblast-aig, default is \"balance;drw\")" [[option]] @@ -113,7 +112,6 @@ header = "options/bv_options.h" long = "bv-eq-slicer=MODE" type = "BvSlicerMode" default = "OFF" - links = ["--bv-eq-solver"] help = "turn on the slicing equality solver for the bit-vector theory (only if --bitblast=lazy)" help_mode = "Bit-vector equality slicer modes." [[option.mode.ON]] @@ -148,7 +146,6 @@ header = "options/bv_options.h" long = "bv-algebraic-budget=N" type = "unsigned" default = "1500" - links = ["--bv-algebraic-solver"] help = "the budget allowed for the algebraic solver in number of SAT conflicts" [[option]] diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index bae60a374..a9b8b0714 100644 --- a/src/options/options_public_functions.cpp +++ b/src/options/options_public_functions.cpp @@ -135,7 +135,8 @@ bool Options::getSemanticChecks() const{ } bool Options::getStatistics() const{ - return (*this)[options::statistics]; + // statsEveryQuery enables stats + return (*this)[options::statistics] || (*this)[options::statsEveryQuery]; } bool Options::getStatsEveryQuery() const{ diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index a0e3014b0..9f9d58aad 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -72,7 +72,6 @@ header = "options/smt_options.h" type = "bool" default = "false" notifies = ["notifyBeforeSearch"] - read_only = true help = "support the get-value and get-model commands" [[option]] @@ -81,7 +80,6 @@ header = "options/smt_options.h" long = "check-models" type = "bool" notifies = ["notifyBeforeSearch"] - links = ["--produce-models", "--produce-assertions"] read_only = true help = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions" @@ -91,7 +89,6 @@ header = "options/smt_options.h" long = "dump-models" type = "bool" default = "false" - links = ["--produce-models"] read_only = true help = "output models after every SAT/INVALID/UNKNOWN response" @@ -140,7 +137,6 @@ header = "options/smt_options.h" default = "false" predicates = ["proofEnabledBuild"] notifies = ["notifyBeforeSearch"] - read_only = true help = "turn on proof generation" [[option]] @@ -150,7 +146,6 @@ header = "options/smt_options.h" type = "bool" predicates = ["LFSCEnabledBuild"] notifies = ["notifyBeforeSearch"] - links = ["--proof"] help = "after UNSAT/VALID, machine-check the generated proof" [[option]] @@ -159,7 +154,6 @@ header = "options/smt_options.h" long = "dump-proofs" type = "bool" default = "false" - links = ["--proof"] read_only = true help = "output proofs after every UNSAT/VALID response" @@ -224,7 +218,6 @@ header = "options/smt_options.h" category = "regular" long = "check-unsat-cores" type = "bool" - links = ["--produce-unsat-cores"] help = "after UNSAT/VALID, produce and check an unsat core (expensive)" [[option]] @@ -234,8 +227,6 @@ header = "options/smt_options.h" type = "bool" default = "false" notifies = ["notifyBeforeSearch"] - links = ["--produce-unsat-cores"] - read_only = true help = "output unsat cores after every UNSAT/VALID response" [[option]] @@ -245,7 +236,6 @@ header = "options/smt_options.h" type = "bool" default = "false" notifies = ["notifyBeforeSearch"] - links = ["--dump-unsat-cores"] read_only = true help = "dump the full unsat core, including unlabeled assertions" @@ -255,7 +245,6 @@ header = "options/smt_options.h" long = "produce-unsat-assumptions" type = "bool" default = "false" - links = ["--produce-unsat-cores"] predicates = ["proofEnabledBuild"] notifies = ["notifyBeforeSearch"] read_only = true @@ -277,7 +266,6 @@ header = "options/smt_options.h" type = "bool" default = "false" notifies = ["notifyBeforeSearch"] - read_only = true help = "support the get-assignment command" [[option]] diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index e0493b180..fd98064e3 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -45,6 +45,49 @@ namespace smt { void setDefaults(SmtEngine& smte, LogicInfo& logic) { + // implied options + if (options::checkModels() || options::dumpModels()) + { + Notice() << "SmtEngine: setting produceModels" << std::endl; + options::produceModels.set(true); + } + if (options::checkModels()) + { + Notice() << "SmtEngine: setting produceAssignments" << std::endl; + options::produceAssignments.set(true); + } + if (options::dumpUnsatCoresFull()) + { + Notice() << "SmtEngine: setting dumpUnsatCores" << std::endl; + options::dumpUnsatCores.set(true); + } + if (options::checkUnsatCores() || options::dumpUnsatCores() + || options::unsatAssumptions()) + { + Notice() << "SmtEngine: setting unsatCores" << std::endl; + options::unsatCores.set(true); + } + if (options::checkProofs() || options::dumpProofs()) + { + Notice() << "SmtEngine: setting proof" << std::endl; + options::proof.set(true); + } + if (options::bitvectorAigSimplifications.wasSetByUser()) + { + Notice() << "SmtEngine: setting bitvectorAig" << std::endl; + options::bitvectorAig.set(true); + } + if (options::bitvectorEqualitySlicer.wasSetByUser()) + { + Notice() << "SmtEngine: setting bitvectorEqualitySolver" << std::endl; + options::bitvectorEqualitySolver.set(true); + } + if (options::bitvectorAlgebraicBudget.wasSetByUser()) + { + Notice() << "SmtEngine: setting bitvectorAlgebraicSolver" << std::endl; + options::bitvectorAlgebraicSolver.set(true); + } + // Language-based defaults if (!options::bitvectorDivByZeroConst.wasSetByUser()) { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 03d9409be..3ac719eed 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -853,6 +853,12 @@ SmtEngine::SmtEngine(ExprManager* em) void SmtEngine::finishInit() { + // set the random seed + Random::getRandom().setSeed(options::seed()); + + // ensure that our heuristics are properly set up + setDefaults(*this, d_logic); + Trace("smt-debug") << "SmtEngine::finishInit" << std::endl; // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) @@ -870,12 +876,6 @@ void SmtEngine::finishInit() #endif } - // set the random seed - Random::getRandom().setSeed(options::seed()); - - // ensure that our heuristics are properly set up - setDefaults(*this, d_logic); - Trace("smt-debug") << "Making decision engine..." << std::endl; Trace("smt-debug") << "Making prop engine..." << std::endl; @@ -1296,6 +1296,7 @@ void SmtEngine::defineFunction(Expr func, Expr formula) { SmtScope smts(this); + finalOptionsAreSet(); doPendingPops(); Trace("smt") << "SMT defineFunction(" << func << ")" << endl; debugCheckFormals(formals, func); -- 2.30.2