summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/main/command_executor.cpp6
-rw-r--r--src/options/base_options.toml3
-rw-r--r--src/smt/command.h1
-rw-r--r--src/smt/dump.cpp21
-rw-r--r--src/smt/smt_engine.cpp56
-rw-r--r--src/smt/sygus_solver.cpp6
-rw-r--r--test/regress/regress0/datatypes/datatype-dump.cvc2
-rw-r--r--test/regress/regress0/printer/let_shadowing.smt22
-rwxr-xr-xtest/regress/run_regression.py2
-rw-r--r--test/unit/api/solver_black.cpp4
10 files changed, 23 insertions, 80 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 98e93ca5a..ad0d24143 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -197,6 +197,12 @@ bool solverInvoke(api::Solver* solver,
Command* cmd,
std::ostream& out)
{
+ // print output for -o raw-benchmark
+ if (solver->isOutputOn("raw-benchmark"))
+ {
+ std::ostream& ss = solver->getOutput("raw-benchmark");
+ cmd->toStream(ss);
+ }
cmd->invoke(solver, sm, out);
// ignore the error if the command-verbosity is 0 for this command
std::string commandName =
diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index e3035e0d6..89032ba50 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -233,6 +233,9 @@ name = "Base"
[[option.mode.TRIGGER]]
name = "trigger"
help = "print selected triggers for quantified formulas"
+[[option.mode.RAW_BENCHMARK]]
+ name = "raw-benchmark"
+ help = "print the benchmark back on the output verbatim as it is processed"
# Stores then enabled output tags.
[[option]]
diff --git a/src/smt/command.h b/src/smt/command.h
index 7d2d9cfc4..b374a48c9 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -219,7 +219,6 @@ class CVC5_EXPORT Command
virtual void toStream(std::ostream& out,
int toDepth = -1,
-
size_t dag = 1,
Language language = Language::LANG_AUTO) const = 0;
diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index 630a91288..d74668433 100644
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -78,10 +78,7 @@ void DumpC::setDumpFromString(const std::string& optarg) {
while ((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL)
{
tokstr = NULL;
- if (!strcmp(optargPtr, "raw-benchmark"))
- {
- }
- else if (!strcmp(optargPtr, "benchmark"))
+ if (!strcmp(optargPtr, "benchmark"))
{
}
else if (!strcmp(optargPtr, "declarations"))
@@ -163,11 +160,6 @@ void DumpC::setDumpFromString(const std::string& optarg) {
if (strcmp(optargPtr, "benchmark"))
{
Dump.on("declarations");
- if (strcmp(optargPtr, "declarations")
- && strcmp(optargPtr, "raw-benchmark"))
- {
- Dump.on("skolems");
- }
}
}
}
@@ -190,10 +182,6 @@ benchmark\n\
declarations\n\
+ Dump user declarations. Implied by all following modes.\n\
\n\
-raw-benchmark\n\
-+ Dump all user-commands as they are received (including assertions) without\n\
- any preprocessing and without any internally-created commands.\n\
-\n\
skolems\n\
+ Dump internally-created skolem variable declarations. These can\n\
arise from preprocessing simplifications, existential elimination,\n\
@@ -228,10 +216,9 @@ theory::fullcheck\n\
+ Output completeness queries for all full-check effort-level theory checks\n\
\n\
Dump modes can be combined by concatenating the above values with \",\" in\n\
-between them. Generally you want raw-benchmark or, alternatively, one from\n\
-the assertions category (either assertions or clauses), and perhaps one or more\n\
-other modes for checking correctness and completeness of decision procedure\n\
-implementations.\n\
+between them. Generally you want one from the assertions category (either\n\
+assertions or clauses), and perhaps one or more other modes for checking\n\
+correctness and completeness of decision procedure implementations.\n\
\n\
The --output-language option controls the language used for dumping, and\n\
this allows you to connect cvc5 to another solver implementation via a UNIX\n\
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index cd8bd1d7b..279761b43 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -231,7 +231,7 @@ void SmtEngine::finishInit()
// dump out a set-logic command only when raw-benchmark is disabled to avoid
// dumping the command twice.
- if (Dump.isOn("benchmark") && !Dump.isOn("raw-benchmark"))
+ if (Dump.isOn("benchmark"))
{
LogicInfo everything;
everything.lock();
@@ -338,12 +338,6 @@ void SmtEngine::setLogic(const std::string& s)
try
{
setLogic(LogicInfo(s));
- // dump out a set-logic command
- if (Dump.isOn("raw-benchmark"))
- {
- getPrinter().toStreamCmdSetBenchmarkLogic(
- d_env->getDumpOut(), getLogicInfo().getLogicString());
- }
}
catch (IllegalArgumentException& e)
{
@@ -643,12 +637,6 @@ void SmtEngine::defineFunctionsRec(
debugCheckFunctionBody(formulas[i], formals[i], funcs[i]);
}
- if (Dump.isOn("raw-benchmark"))
- {
- getPrinter().toStreamCmdDefineFunctionRec(
- d_env->getDumpOut(), funcs, formals, formulas);
- }
-
NodeManager* nm = getNodeManager();
for (unsigned i = 0, size = funcs.size(); i < size; i++)
{
@@ -679,9 +667,9 @@ void SmtEngine::defineFunctionsRec(
Node boundVars = nm->mkNode(kind::BOUND_VAR_LIST, formals[i]);
lem = nm->mkNode(kind::FORALL, boundVars, lem, aexpr);
}
- // assert the quantified formula
- // notice we don't call assertFormula directly, since this would
- // duplicate the output on raw-benchmark.
+ // Assert the quantified formula. Notice we don't call assertFormula
+ // directly, since we should call a private member method since we have
+ // already ensuring this SmtEngine is initialized above.
// add define recursive definition to the assertions
d_asserts->addDefineFunDefinition(lem, global);
}
@@ -968,11 +956,6 @@ Result SmtEngine::assertFormula(const Node& formula)
Trace("smt") << "SmtEngine::assertFormula(" << formula << ")" << endl;
- if (Dump.isOn("raw-benchmark"))
- {
- getPrinter().toStreamCmdAssert(d_env->getDumpOut(), formula);
- }
-
// Substitute out any abstract values in ex
Node n = d_absValues->substituteAbstractValues(formula);
@@ -990,11 +973,6 @@ void SmtEngine::declareSygusVar(Node var)
{
SmtScope smts(this);
d_sygusSolver->declareSygusVar(var);
- if (Dump.isOn("raw-benchmark"))
- {
- getPrinter().toStreamCmdDeclareVar(d_env->getDumpOut(), var, var.getType());
- }
- // don't need to set that the conjecture is stale
}
void SmtEngine::declareSynthFun(Node func,
@@ -1006,16 +984,6 @@ void SmtEngine::declareSynthFun(Node func,
finishInit();
d_state->doPendingPops();
d_sygusSolver->declareSynthFun(func, sygusType, isInv, vars);
-
- // !!! TEMPORARY: We cannot construct a SynthFunCommand since we cannot
- // construct a Term-level Grammar from a Node-level sygus TypeNode. Thus we
- // must print the command using the Node-level utility method for now.
-
- if (Dump.isOn("raw-benchmark"))
- {
- getPrinter().toStreamCmdSynthFun(
- d_env->getDumpOut(), func, vars, isInv, sygusType);
- }
}
void SmtEngine::declareSynthFun(Node func,
bool isInv,
@@ -1031,10 +999,6 @@ void SmtEngine::assertSygusConstraint(Node constraint)
SmtScope smts(this);
finishInit();
d_sygusSolver->assertSygusConstraint(constraint);
- if (Dump.isOn("raw-benchmark"))
- {
- getPrinter().toStreamCmdConstraint(d_env->getDumpOut(), constraint);
- }
}
void SmtEngine::assertSygusInvConstraint(Node inv,
@@ -1045,11 +1009,6 @@ void SmtEngine::assertSygusInvConstraint(Node inv,
SmtScope smts(this);
finishInit();
d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post);
- if (Dump.isOn("raw-benchmark"))
- {
- getPrinter().toStreamCmdInvConstraint(
- d_env->getDumpOut(), inv, pre, trans, post);
- }
}
Result SmtEngine::checkSynth()
@@ -1200,12 +1159,7 @@ std::string SmtEngine::getModel(const std::vector<TypeNode>& declaredSorts,
// completely accessible by the user. This is currently not rigorously
// enforced. An alternative design would be to have this method implemented
// at the API level, but this makes exceptions in the text interface less
- // intuitive and makes it impossible to implement raw-benchmark at the
- // SmtEngine level.
- if (Dump.isOn("raw-benchmark"))
- {
- getPrinter().toStreamCmdGetModel(d_env->getDumpOut());
- }
+ // intuitive.
TheoryModel* tm = getAvailableModel("get model");
// use the smt::Model model utility for printing
const Options& opts = d_env->getOptions();
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 240f96af7..32a0ee220 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -25,8 +25,6 @@
#include "options/option_exception.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
-#include "printer/printer.h"
-#include "smt/dump.h"
#include "smt/preprocessor.h"
#include "smt/smt_solver.h"
#include "theory/datatypes/sygus_datatype_utils.h"
@@ -211,10 +209,6 @@ Result SygusSolver::checkSynth(Assertions& as)
Trace("smt") << "...constructed forall " << body << std::endl;
Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
- if (Dump.isOn("raw-benchmark"))
- {
- d_env.getPrinter().toStreamCmdCheckSynth(d_env.getDumpOut());
- }
d_sygusConjectureStale = false;
diff --git a/test/regress/regress0/datatypes/datatype-dump.cvc b/test/regress/regress0/datatypes/datatype-dump.cvc
index e28fc6305..8a193b71a 100644
--- a/test/regress/regress0/datatypes/datatype-dump.cvc
+++ b/test/regress/regress0/datatypes/datatype-dump.cvc
@@ -1,7 +1,7 @@
% This regression is the same as datatype.cvc but tests the
% dumping infrastructure.
%
-% COMMAND-LINE: --dump raw-benchmark
+% COMMAND-LINE: -o raw-benchmark
%
% EXPECT: OPTION "incremental" false;
% EXPECT: OPTION "logic" "ALL";
diff --git a/test/regress/regress0/printer/let_shadowing.smt2 b/test/regress/regress0/printer/let_shadowing.smt2
index 02eb3376a..fbea9d142 100644
--- a/test/regress/regress0/printer/let_shadowing.smt2
+++ b/test/regress/regress0/printer/let_shadowing.smt2
@@ -1,5 +1,5 @@
; REQUIRES: dumping
-; COMMAND-LINE: --dump raw-benchmark --preprocess-only
+; COMMAND-LINE: -o raw-benchmark --preprocess-only
; SCRUBBER: grep assert
; EXPECT: (assert (let ((_let_1 (* x y))) (and (= _let_1 _let_1) (= _let_1 _let_0))))
; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((_let_0 Int)) (= 0 _let_0))))))
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 0f9bcda1a..4c9ea3fcb 100755
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -141,7 +141,7 @@ def run_benchmark(dump, wrapper, scrubber, error_scrubber, cvc5_binary,
exit_status = None
if dump:
dump_args = [
- '--preprocess-only', '--dump', 'raw-benchmark',
+ '--preprocess-only', '-o', 'raw-benchmark',
'--output-lang=smt2', '-qq'
]
dump_output, _, _ = run_process(
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 75cd97060..1f6f7801e 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -1375,8 +1375,8 @@ TEST_F(TestApiBlackSolver, getOptionInfo)
auto modeInfo = std::get<OptionInfo::ModeInfo>(info.valueInfo);
EXPECT_EQ("NONE", modeInfo.defaultValue);
EXPECT_EQ("OutputTag::NONE", modeInfo.currentValue);
- std::vector<std::string> modes{"INST", "NONE", "SYGUS", "TRIGGER"};
- EXPECT_EQ(modes, modeInfo.modes);
+ EXPECT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "NONE")
+ != modeInfo.modes.end());
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback