From efdefd95abd7de85963b9dd22e98e2858864cb07 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 14 Sep 2021 10:31:07 -0500 Subject: [PATCH] Reimplement `--dump=raw-benchmark` as `-o raw-benchmark` (#7191) Printing the original benchmark is simple, as it is exactly the commands we execute. This removes the previous code from SmtEngine, which is currently broken. --- src/main/command_executor.cpp | 6 ++ src/options/base_options.toml | 3 + src/smt/command.h | 1 - src/smt/dump.cpp | 21 ++----- src/smt/smt_engine.cpp | 56 ++----------------- src/smt/sygus_solver.cpp | 6 -- .../regress0/datatypes/datatype-dump.cvc | 2 +- .../regress0/printer/let_shadowing.smt2 | 2 +- test/regress/run_regression.py | 2 +- test/unit/api/solver_black.cpp | 4 +- 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& 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(info.valueInfo); EXPECT_EQ("NONE", modeInfo.defaultValue); EXPECT_EQ("OutputTag::NONE", modeInfo.currentValue); - std::vector modes{"INST", "NONE", "SYGUS", "TRIGGER"}; - EXPECT_EQ(modes, modeInfo.modes); + EXPECT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "NONE") + != modeInfo.modes.end()); } } -- 2.30.2