From 6db84f6e373f9651af48df7b654e3992f68472ac Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Wed, 3 Mar 2021 04:28:45 -0600 Subject: [PATCH] Remove uses of SExpr class. (#6035) This PR is a step towards removing SExpr class. It replaces SExpr with std::string for set-info and set-option commands. --- src/printer/ast/ast_printer.cpp | 8 +- src/printer/ast/ast_printer.h | 4 +- src/printer/cvc/cvc_printer.cpp | 14 +-- src/printer/cvc/cvc_printer.h | 4 +- src/printer/printer.cpp | 4 +- src/printer/printer.h | 4 +- src/printer/smt2/smt2_printer.cpp | 24 +--- src/printer/smt2/smt2_printer.h | 4 +- src/smt/command.cpp | 30 ++--- src/smt/command.h | 16 +-- src/smt/smt_engine.cpp | 104 ++++++++---------- src/smt/smt_engine.h | 5 +- src/theory/quantifiers/expr_miner.cpp | 2 +- .../quantifiers/sygus/sygus_repair_const.cpp | 6 +- test/unit/theory/theory_arith_white.cpp | 2 +- test/unit/theory/theory_bv_white.cpp | 6 +- .../theory_quantifiers_bv_inverter_white.cpp | 4 +- 17 files changed, 102 insertions(+), 139 deletions(-) diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index ab792f6fe..66dcdbfb2 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -346,9 +346,9 @@ void AstPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out, void AstPrinter::toStreamCmdSetInfo(std::ostream& out, const std::string& flag, - SExpr sexpr) const + const std::string& value) const { - out << "SetInfo(" << flag << ", " << sexpr << ')' << std::endl; + out << "SetInfo(" << flag << ", " << value << ')' << std::endl; } void AstPrinter::toStreamCmdGetInfo(std::ostream& out, @@ -359,9 +359,9 @@ void AstPrinter::toStreamCmdGetInfo(std::ostream& out, void AstPrinter::toStreamCmdSetOption(std::ostream& out, const std::string& flag, - SExpr sexpr) const + const std::string& value) const { - out << "SetOption(" << flag << ", " << sexpr << ')' << std::endl; + out << "SetOption(" << flag << ", " << value << ')' << std::endl; } void AstPrinter::toStreamCmdGetOption(std::ostream& out, diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index 732933bb4..be1529b04 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -124,7 +124,7 @@ class AstPrinter : public CVC4::Printer /** Print set-info command */ void toStreamCmdSetInfo(std::ostream& out, const std::string& flag, - SExpr sexpr) const override; + const std::string& value) const override; /** Print get-info command */ void toStreamCmdGetInfo(std::ostream& out, @@ -133,7 +133,7 @@ class AstPrinter : public CVC4::Printer /** Print set-option command */ void toStreamCmdSetOption(std::ostream& out, const std::string& flag, - SExpr sexpr) const override; + const std::string& value) const override; /** Print get-option command */ void toStreamCmdGetOption(std::ostream& out, diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 82798d074..7ac2da40b 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -1420,13 +1420,9 @@ void CvcPrinter::toStreamCmdSetBenchmarkLogic(std::ostream& out, void CvcPrinter::toStreamCmdSetInfo(std::ostream& out, const std::string& flag, - SExpr sexpr) const + const std::string& value) const { - out << "% (set-info " << flag << ' '; - OutputLanguage language = - d_cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4; - SExpr::toStream(out, sexpr, language); - out << ')' << std::endl; + out << "% (set-info " << flag << ' ' << value << ')' << std::endl; } void CvcPrinter::toStreamCmdGetInfo(std::ostream& out, @@ -1437,11 +1433,9 @@ void CvcPrinter::toStreamCmdGetInfo(std::ostream& out, void CvcPrinter::toStreamCmdSetOption(std::ostream& out, const std::string& flag, - SExpr sexpr) const + const std::string& value) const { - out << "OPTION \"" << flag << "\" "; - SExpr::toStream(out, sexpr, language::output::LANG_CVC4); - out << ';' << std::endl; + out << "OPTION \"" << flag << "\" " << value << ';' << std::endl; } void CvcPrinter::toStreamCmdGetOption(std::ostream& out, diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index 58e47dbac..ab18d62de 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -125,7 +125,7 @@ class CvcPrinter : public CVC4::Printer /** Print set-info command */ void toStreamCmdSetInfo(std::ostream& out, const std::string& flag, - SExpr sexpr) const override; + const std::string& value) const override; /** Print get-info command */ void toStreamCmdGetInfo(std::ostream& out, @@ -134,7 +134,7 @@ class CvcPrinter : public CVC4::Printer /** Print set-option command */ void toStreamCmdSetOption(std::ostream& out, const std::string& flag, - SExpr sexpr) const override; + const std::string& value) const override; /** Print get-option command */ void toStreamCmdGetOption(std::ostream& out, diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 4e464f829..2d5ae58cd 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -388,7 +388,7 @@ void Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out, void Printer::toStreamCmdSetInfo(std::ostream& out, const std::string& flag, - SExpr sexpr) const + const std::string& value) const { printUnknownCommand(out, "set-info"); } @@ -401,7 +401,7 @@ void Printer::toStreamCmdGetInfo(std::ostream& out, void Printer::toStreamCmdSetOption(std::ostream& out, const std::string& flag, - SExpr sexpr) const + const std::string& value) const { printUnknownCommand(out, "set-option"); } diff --git a/src/printer/printer.h b/src/printer/printer.h index f17029618..0a5ed1eac 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -217,7 +217,7 @@ class Printer /** Print set-info command */ virtual void toStreamCmdSetInfo(std::ostream& out, const std::string& flag, - SExpr sexpr) const; + const std::string& value) const; /** Print get-info command */ virtual void toStreamCmdGetInfo(std::ostream& out, @@ -226,7 +226,7 @@ class Printer /** Print set-option command */ virtual void toStreamCmdSetOption(std::ostream& out, const std::string& flag, - SExpr sexpr) const; + const std::string& value) const; /** Print get-option command */ virtual void toStreamCmdGetOption(std::ostream& out, diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 8c122f26d..c3ac36b5e 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -50,8 +50,6 @@ namespace CVC4 { namespace printer { namespace smt2 { -static OutputLanguage variantToLanguage(Variant v); - /** returns whether the variant is smt-lib 2.6 or greater */ bool isVariant_2_6(Variant v) { return v == smt2_6_variant; } @@ -1808,11 +1806,9 @@ void Smt2Printer::toStreamCmdSetBenchmarkLogic(std::ostream& out, void Smt2Printer::toStreamCmdSetInfo(std::ostream& out, const std::string& flag, - SExpr sexpr) const + const std::string& value) const { - out << "(set-info :" << flag << ' '; - SExpr::toStream(out, sexpr, variantToLanguage(d_variant)); - out << ')' << std::endl; + out << "(set-info :" << flag << ' ' << value << ')' << std::endl; } void Smt2Printer::toStreamCmdGetInfo(std::ostream& out, @@ -1823,11 +1819,9 @@ void Smt2Printer::toStreamCmdGetInfo(std::ostream& out, void Smt2Printer::toStreamCmdSetOption(std::ostream& out, const std::string& flag, - SExpr sexpr) const + const std::string& value) const { - out << "(set-option :" << flag << ' '; - SExpr::toStream(out, sexpr, language::output::LANG_SMTLIB_V2_5); - out << ')' << std::endl; + out << "(set-option :" << flag << ' ' << value << ')' << std::endl; } void Smt2Printer::toStreamCmdGetOption(std::ostream& out, @@ -2233,16 +2227,6 @@ static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) return false; } -static OutputLanguage variantToLanguage(Variant variant) -{ - switch(variant) { - case smt2_0_variant: - return language::output::LANG_SMTLIB_V2_0; - case no_variant: - default: return language::output::LANG_SMTLIB_V2_6; - } -} - }/* CVC4::printer::smt2 namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 8934967b9..4ba0d6cad 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -178,7 +178,7 @@ class Smt2Printer : public CVC4::Printer /** Print set-info command */ void toStreamCmdSetInfo(std::ostream& out, const std::string& flag, - SExpr sexpr) const override; + const std::string& value) const override; /** Print get-info command */ void toStreamCmdGetInfo(std::ostream& out, @@ -187,7 +187,7 @@ class Smt2Printer : public CVC4::Printer /** Print set-option command */ void toStreamCmdSetOption(std::ostream& out, const std::string& flag, - SExpr sexpr) const override; + const std::string& value) const override; /** Print get-option command */ void toStreamCmdGetOption(std::ostream& out, diff --git a/src/smt/command.cpp b/src/smt/command.cpp index f10191c75..9227c3703 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2572,18 +2572,19 @@ void SetBenchmarkLogicCommand::toStream(std::ostream& out, /* class SetInfoCommand */ /* -------------------------------------------------------------------------- */ -SetInfoCommand::SetInfoCommand(std::string flag, const std::string& sexpr) - : d_flag(flag), d_sexpr(sexpr) +SetInfoCommand::SetInfoCommand(const std::string& flag, + const std::string& value) + : d_flag(flag), d_value(value) { } -std::string SetInfoCommand::getFlag() const { return d_flag; } -const std::string& SetInfoCommand::getSExpr() const { return d_sexpr; } +const std::string& SetInfoCommand::getFlag() const { return d_flag; } +const std::string& SetInfoCommand::getValue() const { return d_value; } void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - solver->setInfo(d_flag, d_sexpr); + solver->setInfo(d_flag, d_value); d_commandStatus = CommandSuccess::instance(); } catch (api::CVC4ApiRecoverableException&) @@ -2599,7 +2600,7 @@ void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm) Command* SetInfoCommand::clone() const { - return new SetInfoCommand(d_flag, d_sexpr); + return new SetInfoCommand(d_flag, d_value); } std::string SetInfoCommand::getCommandName() const { return "set-info"; } @@ -2609,7 +2610,7 @@ void SetInfoCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { - Printer::getPrinter(language)->toStreamCmdSetInfo(out, d_flag, d_sexpr); + Printer::getPrinter(language)->toStreamCmdSetInfo(out, d_flag, d_value); } /* -------------------------------------------------------------------------- */ @@ -2672,18 +2673,19 @@ void GetInfoCommand::toStream(std::ostream& out, /* class SetOptionCommand */ /* -------------------------------------------------------------------------- */ -SetOptionCommand::SetOptionCommand(std::string flag, const std::string& sexpr) - : d_flag(flag), d_sexpr(sexpr) +SetOptionCommand::SetOptionCommand(const std::string& flag, + const std::string& value) + : d_flag(flag), d_value(value) { } -std::string SetOptionCommand::getFlag() const { return d_flag; } -const std::string& SetOptionCommand::getSExpr() const { return d_sexpr; } +const std::string& SetOptionCommand::getFlag() const { return d_flag; } +const std::string& SetOptionCommand::getValue() const { return d_value; } void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - solver->setOption(d_flag, d_sexpr); + solver->setOption(d_flag, d_value); d_commandStatus = CommandSuccess::instance(); } catch (api::CVC4ApiRecoverableException&) @@ -2698,7 +2700,7 @@ void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm) Command* SetOptionCommand::clone() const { - return new SetOptionCommand(d_flag, d_sexpr); + return new SetOptionCommand(d_flag, d_value); } std::string SetOptionCommand::getCommandName() const { return "set-option"; } @@ -2708,7 +2710,7 @@ void SetOptionCommand::toStream(std::ostream& out, size_t dag, OutputLanguage language) const { - Printer::getPrinter(language)->toStreamCmdSetOption(out, d_flag, d_sexpr); + Printer::getPrinter(language)->toStreamCmdSetOption(out, d_flag, d_value); } /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index a88b7e022..c11012944 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1298,13 +1298,13 @@ class CVC4_PUBLIC SetInfoCommand : public Command { protected: std::string d_flag; - std::string d_sexpr; + std::string d_value; public: - SetInfoCommand(std::string flag, const std::string& sexpr); + SetInfoCommand(const std::string& flag, const std::string& value); - std::string getFlag() const; - const std::string& getSExpr() const; + const std::string& getFlag() const; + const std::string& getValue() const; void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; @@ -1343,13 +1343,13 @@ class CVC4_PUBLIC SetOptionCommand : public Command { protected: std::string d_flag; - std::string d_sexpr; + std::string d_value; public: - SetOptionCommand(std::string flag, const std::string& sexpr); + SetOptionCommand(const std::string& flag, const std::string& value); - std::string getFlag() const; - const std::string& getSExpr() const; + const std::string& getFlag() const; + const std::string& getValue() const; void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ed5e73d5d..80d7b96fa 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -435,53 +435,51 @@ void SmtEngine::setLogicInternal() d_userLogic.lock(); } -void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) +void SmtEngine::setInfo(const std::string& key, const std::string& value) { SmtScope smts(this); Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; - if(Dump.isOn("benchmark")) { - if(key == "status") { - string s = value.getValue(); + if (Dump.isOn("benchmark")) + { + if (key == "status") + { Result::Sat status = - (s == "sat") ? Result::SAT - : ((s == "unsat") ? Result::UNSAT : Result::SAT_UNKNOWN); + (value == "sat") + ? Result::SAT + : ((value == "unsat") ? Result::UNSAT : Result::SAT_UNKNOWN); getOutputManager().getPrinter().toStreamCmdSetBenchmarkStatus( getOutputManager().getDumpOut(), status); - } else { + } + else + { getOutputManager().getPrinter().toStreamCmdSetInfo( getOutputManager().getDumpOut(), key, value); } } - // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...) - if (key == "source" || key == "category" || key == "difficulty" - || key == "notes" || key == "name" || key == "license") + if (key == "filename") { - // ignore these - return; - } - else if (key == "filename") - { - d_state->setFilename(value.getValue()); - return; + d_state->setFilename(value); } else if (key == "smt-lib-version" && !options::inputLanguage.wasSetByUser()) { language::input::Language ilang = language::input::LANG_AUTO; - if( (value.isInteger() && value.getIntegerValue() == Integer(2)) || - (value.isRational() && value.getRationalValue() == Rational(2)) || - value.getValue() == "2" || - value.getValue() == "2.0" ) { + + if (value == "2" || value == "2.0") + { ilang = language::input::LANG_SMTLIB_V2_0; - } else if( (value.isRational() && value.getRationalValue() == Rational(5, 2)) || - value.getValue() == "2.5" ) { + } + else if (value == "2.5") + { ilang = language::input::LANG_SMTLIB_V2_5; - } else if( (value.isRational() && value.getRationalValue() == Rational(13, 5)) || - value.getValue() == "2.6" ) { + } + else if (value == "2.6") + { ilang = language::input::LANG_SMTLIB_V2_6; } + options::inputLanguage.set(ilang); // also update the output language if (!options::outputLanguage.wasSetByUser()) @@ -493,18 +491,10 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) *options::out() << language::SetLanguage(olang); } } - return; - } else if(key == "status") { - string s; - if(value.isAtom()) { - s = value.getValue(); - } - if(s != "sat" && s != "unsat" && s != "unknown") { - throw OptionException("argument to (set-info :status ..) must be " - "`sat' or `unsat' or `unknown'"); - } - d_state->notifyExpectedStatus(s); - return; + } + else if (key == "status") + { + d_state->notifyExpectedStatus(value); } } @@ -1913,16 +1903,9 @@ void SmtEngine::setUserAttribute(const std::string& attr, te->setUserAttribute(attr, expr, expr_values, str_value); } -void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) +void SmtEngine::setOption(const std::string& key, const std::string& value) { - // Always check whether the SmtEngine has been initialized (which is done - // upon entering Assert mode the first time). No option can be set after - // initialized. - if (d_state->isFullyInited()) - { - throw ModalException("SmtEngine::setOption called after initialization."); - } - NodeManagerScope nms(d_nodeManager); + NodeManagerScope nms(d_nodeManager); Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; if(Dump.isOn("benchmark")) { @@ -1931,28 +1914,29 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) } if(key == "command-verbosity") { - if(!value.isAtom()) { - const vector& cs = value.getChildren(); - if(cs.size() == 2 && - (cs[0].isKeyword() || cs[0].isString()) && - cs[1].isInteger()) { - string c = cs[0].getValue(); - const Integer& v = cs[1].getIntegerValue(); - if(v < 0 || v > 2) { - throw OptionException("command-verbosity must be 0, 1, or 2"); - } - d_commandVerbosity[c] = v; - return; + size_t fstIndex = value.find(" "); + size_t sndIndex = value.find(" ", fstIndex + 1); + if (sndIndex == std::string::npos) + { + string c = value.substr(1, fstIndex - 1); + int v = + std::stoi(value.substr(fstIndex + 1, value.length() - fstIndex - 1)); + if (v < 0 || v > 2) + { + throw OptionException("command-verbosity must be 0, 1, or 2"); } + d_commandVerbosity[c] = v; + return; } throw OptionException("command-verbosity value must be a tuple (command-name, integer)"); } - if(!value.isAtom()) { + if (value.find(" ") != std::string::npos) + { throw OptionException("bad value for :" + key); } - string optionarg = value.getValue(); + std::string optionarg = value; d_options.setOption(key, optionarg); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 53a5b7f2f..8974e5e60 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -218,9 +218,8 @@ class CVC4_PUBLIC SmtEngine /** * Set information about the script executing. - * @throw OptionException, ModalException */ - void setInfo(const std::string& key, const CVC4::SExpr& value); + void setInfo(const std::string& key, const std::string& value); /** Return true if given keyword is a valid SMT-LIB v2 get-info flag. */ bool isValidGetInfoFlag(const std::string& key) const; @@ -232,7 +231,7 @@ class CVC4_PUBLIC SmtEngine * Set an aspect of the current SMT execution environment. * @throw OptionException, ModalException */ - void setOption(const std::string& key, const CVC4::SExpr& value); + void setOption(const std::string& key, const std::string& value); /** Set is internal subsolver. * diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 6ce561b2d..96a26059d 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -76,7 +76,7 @@ void ExprMiner::initializeChecker(std::unique_ptr& checker, Assert (!query.isNull()); initializeSubsolver(checker); // also set the options - checker->setOption("sygus-rr-synth-input", false); + checker->setOption("sygus-rr-synth-input", "false"); checker->setOption("input-language", "smt2"); // Convert bound variables to skolems. This ensures the satisfiability // check is ground. diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 8b741b6d7..9b4a03473 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -237,9 +237,9 @@ bool SygusRepairConst::repairSolution(Node sygusBody, options::sygusRepairConstTimeout.wasSetByUser(), options::sygusRepairConstTimeout()); // renable options disabled by sygus - repcChecker->setOption("miniscope-quant", true); - repcChecker->setOption("miniscope-quant-fv", true); - repcChecker->setOption("quant-split", true); + repcChecker->setOption("miniscope-quant", "true"); + repcChecker->setOption("miniscope-quant-fv", "true"); + repcChecker->setOption("quant-split", "true"); repcChecker->assertFormula(fo_body); // check satisfiability Result r = repcChecker->checkSat(); diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp index 5e5b52d3e..4c8834c8d 100644 --- a/test/unit/theory/theory_arith_white.cpp +++ b/test/unit/theory/theory_arith_white.cpp @@ -41,7 +41,7 @@ class TestTheoryWhiteArith : public TestSmtNoFinishInit void SetUp() override { TestSmtNoFinishInit::SetUp(); - d_smtEngine->setOption("incremental", CVC4::SExpr(false)); + d_smtEngine->setOption("incremental", "false"); d_smtEngine->finishInit(); d_context = d_smtEngine->getContext(); d_user_context = d_smtEngine->getUserContext(); diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp index c07f2c402..976724c8e 100644 --- a/test/unit/theory/theory_bv_white.cpp +++ b/test/unit/theory/theory_bv_white.cpp @@ -43,8 +43,8 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core) { d_smtEngine->setLogic("QF_BV"); - d_smtEngine->setOption("bitblast", SExpr("eager")); - d_smtEngine->setOption("incremental", SExpr("false")); + d_smtEngine->setOption("bitblast", "eager"); + d_smtEngine->setOption("incremental", "false"); // Notice that this unit test uses the theory engine of a created SMT // engine d_smtEngine. We must ensure that d_smtEngine is properly initialized // via the following call, which constructs its underlying theory engine. @@ -72,7 +72,7 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core) TEST_F(TestTheoryWhiteBv, mkUmulo) { - d_smtEngine->setOption("incremental", SExpr("true")); + d_smtEngine->setOption("incremental", "true"); for (uint32_t w = 1; w < 16; ++w) { d_smtEngine->push(); diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp index 5c222d2c1..b5996a684 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp @@ -35,8 +35,8 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit void SetUp() override { TestSmtNoFinishInit::SetUp(); - d_smtEngine->setOption("cegqi-full", CVC4::SExpr(true)); - d_smtEngine->setOption("produce-models", CVC4::SExpr(true)); + d_smtEngine->setOption("cegqi-full", "true"); + d_smtEngine->setOption("produce-models", "true"); d_smtEngine->finishInit(); d_s = d_nodeManager->mkVar("s", d_nodeManager->mkBitVectorType(4)); -- 2.30.2