summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/main/driver_unified.cpp2
-rw-r--r--src/options/main_options.toml7
-rw-r--r--src/smt/env.cpp4
-rw-r--r--src/smt/env.h14
-rw-r--r--src/smt/proof_manager.cpp5
-rw-r--r--src/smt/smt_engine.cpp34
-rw-r--r--src/smt/smt_engine.h16
-rw-r--r--src/smt/smt_engine_state.cpp3
-rw-r--r--src/smt/smt_solver.cpp3
-rw-r--r--src/util/statistics_public.cpp1
10 files changed, 26 insertions, 63 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 005de6a34..2c6413503 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -205,7 +205,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
int returnValue = 0;
{
// notify SmtEngine that we are starting to parse
- pExecutor->getSmtEngine()->notifyStartParsing(filenameStr);
+ pExecutor->getSmtEngine()->setInfo("filename", filenameStr);
// Parse and execute commands until we are done
std::unique_ptr<Command> cmd;
diff --git a/src/options/main_options.toml b/src/options/main_options.toml
index 55f74f50c..41d6766e8 100644
--- a/src/options/main_options.toml
+++ b/src/options/main_options.toml
@@ -73,6 +73,13 @@ public = true
help = "force interactive shell/non-interactive mode"
[[option]]
+ name = "filename"
+ category = "undocumented"
+ long = "filename=FILENAME"
+ type = "std::string"
+ help = "filename of the input"
+
+[[option]]
name = "segvSpin"
category = "regular"
long = "segv-spin"
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 7efefabcd..9f647f7c9 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -65,8 +65,6 @@ void Env::setProofNodeManager(ProofNodeManager* pnm)
d_topLevelSubs->setProofNodeManager(pnm);
}
-void Env::setFilename(const std::string& filename) { d_filename = filename; }
-
void Env::shutdown()
{
d_rewriter.reset(nullptr);
@@ -83,8 +81,6 @@ NodeManager* Env::getNodeManager() const { return d_nodeManager; }
ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; }
-const std::string& Env::getFilename() const { return d_filename; }
-
bool Env::isSatProofProducing() const
{
return d_proofNodeManager != nullptr
diff --git a/src/smt/env.h b/src/smt/env.h
index 7c12c86b9..786cdcab2 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -82,9 +82,6 @@ class Env
*/
ProofNodeManager* getProofNodeManager();
- /** Return the input name, or the empty string if not set */
- const std::string& getFilename() const;
-
/**
* Check whether the SAT solver should produce proofs. Other than whether
* the proof node manager is set, SAT proofs are only generated when the
@@ -143,11 +140,6 @@ class Env
/** Set proof node manager if it exists */
void setProofNodeManager(ProofNodeManager* pnm);
- /**
- * Set that the file name of the current instance is the given string. This
- * is used for various purposes (e.g. get-info, SZS status).
- */
- void setFilename(const std::string& filename);
/* Private shutdown ------------------------------------------------------- */
/**
@@ -214,12 +206,6 @@ class Env
const Options* d_originalOptions;
/** Manager for limiting time and abstract resource usage. */
std::unique_ptr<ResourceManager> d_resourceManager;
-
- /**
- * The input file name or the name set through (set-info :filename ...), if
- * any.
- */
- std::string d_filename;
}; /* class Env */
} // namespace cvc5
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 58ae025b8..829d6f2f5 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -16,6 +16,7 @@
#include "smt/proof_manager.h"
#include "options/base_options.h"
+#include "options/main_options.h"
#include "options/proof_options.h"
#include "options/smt_options.h"
#include "proof/dot/dot_printer.h"
@@ -161,10 +162,10 @@ void PfManager::printProof(std::ostream& out,
}
else if (options::proofFormatMode() == options::ProofFormatMode::TPTP)
{
- out << "% SZS output start Proof for " << d_env.getFilename() << std::endl;
+ out << "% SZS output start Proof for " << d_env.getOptions().driver.filename << std::endl;
// TODO (proj #37) print in TPTP compliant format
out << *fp << std::endl;
- out << "% SZS output end Proof for " << d_env.getFilename() << std::endl;
+ out << "% SZS output end Proof for " << d_env.getOptions().driver.filename << std::endl;
}
else
{
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0ca4d5b15..8ecf171bd 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -375,25 +375,6 @@ LogicInfo SmtEngine::getUserLogicInfo() const
return res;
}
-void SmtEngine::notifyStartParsing(const std::string& filename)
-{
- d_env->setFilename(filename);
- d_env->getStatisticsRegistry().registerValue<std::string>("driver::filename",
- filename);
- // Copy the original options. This is called prior to beginning parsing.
- // Hence reset should revert to these options, which note is after reading
- // the command line.
-}
-
-const std::string& SmtEngine::getFilename() const
-{
- return d_env->getFilename();
-}
-
-void SmtEngine::setResultStatistic(const std::string& result) {
- d_env->getStatisticsRegistry().registerValue<std::string>("driver::sat/unsat",
- result);
-}
void SmtEngine::setTotalTimeStatistic(double seconds) {
d_env->getStatisticsRegistry().registerValue<double>("driver::totalTime",
seconds);
@@ -432,7 +413,10 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value)
if (key == "filename")
{
- d_env->setFilename(value);
+ d_env->d_options.driver.filename = value;
+ d_env->d_originalOptions->driver.filename = value;
+ d_env->getStatisticsRegistry().registerValue<std::string>(
+ "driver::filename", value);
}
else if (key == "smt-lib-version" && !getOptions().base.inputLanguageWasSetByUser)
{
@@ -487,6 +471,10 @@ std::string SmtEngine::getInfo(const std::string& key) const
{
return "immediate-exit";
}
+ if (key == "filename")
+ {
+ return d_env->getOptions().driver.filename;
+ }
if (key == "name")
{
return toSExpr(Configuration::getName());
@@ -724,7 +712,7 @@ void SmtEngine::defineFunctionRec(Node func,
Result SmtEngine::quickCheck() {
Assert(d_state->isFullyInited());
Trace("smt") << "SMT quickCheck()" << endl;
- const std::string& filename = d_env->getFilename();
+ const std::string& filename = d_env->getOptions().driver.filename;
return Result(
Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename);
}
@@ -940,7 +928,7 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
{
printStatisticsDiff();
}
- return Result(Result::SAT_UNKNOWN, why, d_env->getFilename());
+ return Result(Result::SAT_UNKNOWN, why, d_env->getOptions().driver.filename);
}
}
@@ -1242,7 +1230,7 @@ Model* SmtEngine::getModel() {
}
// set the information on the SMT-level model
Assert(m != nullptr);
- m->d_inputName = d_env->getFilename();
+ m->d_inputName = d_env->getOptions().driver.filename;
m->d_isKnownSat = (d_state->getMode() == SmtMode::SAT);
return m;
}
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index a250e2a7f..353d96da8 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -227,22 +227,6 @@ class CVC5_EXPORT SmtEngine
bool isInternalSubsolver() const;
/**
- * Notify that we are now parsing the input with the given filename.
- * This call sets the filename maintained by this SmtEngine for bookkeeping
- * and also makes a copy of the current options of this SmtEngine. This
- * is required so that the SMT-LIB command (reset) returns the SmtEngine
- * to a state where its options were prior to parsing but after e.g.
- * reading command line options.
- */
- void notifyStartParsing(const std::string& filename) CVC5_EXPORT;
- /** return the input name (if any) */
- const std::string& getFilename() const;
-
- /**
- * Helper method for the API to put the last check result into the statistics.
- */
- void setResultStatistic(const std::string& result) CVC5_EXPORT;
- /**
* Helper method for the API to put the total runtime into the statistics.
*/
void setTotalTimeStatistic(double seconds) CVC5_EXPORT;
diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp
index a61c18384..2206b29cd 100644
--- a/src/smt/smt_engine_state.cpp
+++ b/src/smt/smt_engine_state.cpp
@@ -17,6 +17,7 @@
#include "base/modal_exception.h"
#include "options/base_options.h"
+#include "options/main_options.h"
#include "options/option_exception.h"
#include "options/smt_options.h"
#include "smt/env.h"
@@ -43,7 +44,7 @@ void SmtEngineState::notifyExpectedStatus(const std::string& status)
Assert(status == "sat" || status == "unsat" || status == "unknown")
<< "SmtEngineState::notifyExpectedStatus: unexpected status string "
<< status;
- d_expectedStatus = Result(status, d_env.getFilename());
+ d_expectedStatus = Result(status, d_env.getOptions().driver.filename);
}
void SmtEngineState::notifyResetAssertions()
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 214193b00..e509eafcf 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -15,6 +15,7 @@
#include "smt/smt_solver.h"
+#include "options/main_options.h"
#include "options/smt_options.h"
#include "prop/prop_engine.h"
#include "smt/assertions.h"
@@ -133,7 +134,7 @@ Result SmtSolver::checkSatisfiability(Assertions& as,
Trace("smt") << "SmtSolver::check()" << endl;
- const std::string& filename = d_env.getFilename();
+ const std::string& filename = d_env.getOptions().driver.filename;
ResourceManager* rm = d_env.getResourceManager();
if (rm->out())
{
diff --git a/src/util/statistics_public.cpp b/src/util/statistics_public.cpp
index f88996278..5d17ae792 100644
--- a/src/util/statistics_public.cpp
+++ b/src/util/statistics_public.cpp
@@ -30,7 +30,6 @@ void registerPublicStatistics(StatisticsRegistry& reg)
reg.registerHistogram<api::Kind>("api::TERM", false);
reg.registerValue<std::string>("driver::filename", false);
- reg.registerValue<std::string>("driver::sat/unsat", false);
reg.registerValue<double>("driver::totalTime", false);
for (theory::TheoryId id = theory::THEORY_FIRST; id != theory::THEORY_LAST;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback