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.

diff --git a/contrib/cvc4_strict_smtlib b/contrib/cvc4_strict_smtlib
new file mode 100644 (file)
index 0000000..0a97bd7
--- /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 43060bc5493213702f9bea4bdafbdabaeba1ea67..65eeda3aeda008ae1760f77979c918d713c7bcbf 100644 (file)
--- 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 489f33ed73bdbe0d15cd69d8e8a36a990a2ac785..05dc6b716f559827c41a0709ce86232d152d095e 100644 (file)
--- 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 bae60a3741f13a604264496795751c92136eb559..a9b8b0714eb9ac482d1cf235329955f5f786ecc2 100644 (file)
--- 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 a0e3014b0e13d7e34b2f44351cfe9f4f56f9db5f..9f9d58aad8c570f308ffee6567b1896e380369d3 100644 (file)
--- 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 e0493b1808f3a11a4005139d354ee76dea5d2fde..fd98064e307984a29ddc9c7fe2786b5fb43fd9d5 100644 (file)
--- 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 03d9409bee86b0f1521886c130fa39c9a4a7cf66..3ac719eed0f010fe6ceab60fda007f7d07be0104 100644 (file)
--- 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);