diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/command.cpp | 37 | ||||
-rw-r--r-- | src/smt/command.h | 14 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 7 |
3 files changed, 48 insertions, 10 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 8012c868c..fee109923 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -383,8 +383,8 @@ CheckSynthCommand::CheckSynthCommand() throw() : d_expr() { } -CheckSynthCommand::CheckSynthCommand(const Expr& expr, bool inUnsatCore) throw() : - d_expr(expr), d_inUnsatCore(inUnsatCore) { +CheckSynthCommand::CheckSynthCommand(const Expr& expr) throw() : + d_expr(expr) { } Expr CheckSynthCommand::getExpr() const throw() { @@ -395,6 +395,33 @@ void CheckSynthCommand::invoke(SmtEngine* smtEngine) { try { d_result = smtEngine->checkSynth(d_expr); d_commandStatus = CommandSuccess::instance(); + smt::SmtScope scope(smtEngine); + d_solution.clear(); + // check whether we should print the status + if (d_result.asSatisfiabilityResult() != Result::UNSAT + || options::sygusOut() == SYGUS_SOL_OUT_STATUS_AND_DEF + || options::sygusOut() == SYGUS_SOL_OUT_STATUS) + { + if (options::sygusOut() == SYGUS_SOL_OUT_STANDARD) + { + d_solution << "(fail)" << endl; + } + else + { + d_solution << d_result << endl; + } + } + // check whether we should print the solution + if (d_result.asSatisfiabilityResult() == Result::UNSAT + && options::sygusOut() != SYGUS_SOL_OUT_STATUS) + { + // printing a synthesis solution is a non-constant + // method, since it invokes a sophisticated algorithm + // (Figure 5 of Reynolds et al. CAV 2015). + // Hence, we must call here print solution here, + // instead of during printResult. + smtEngine->printSynthSolution(d_solution); + } } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } @@ -408,18 +435,18 @@ void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const if(! ok()) { this->Command::printResult(out, verbosity); } else { - out << d_result << endl; + out << d_solution.str(); } } Command* CheckSynthCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - CheckSynthCommand* c = new CheckSynthCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); + CheckSynthCommand* c = new CheckSynthCommand(d_expr.exportTo(exprManager, variableMap)); c->d_result = d_result; return c; } Command* CheckSynthCommand::clone() const { - CheckSynthCommand* c = new CheckSynthCommand(d_expr, d_inUnsatCore); + CheckSynthCommand* c = new CheckSynthCommand(d_expr); c->d_result = d_result; return c; } diff --git a/src/smt/command.h b/src/smt/command.h index f5be9ddfe..a60c85a3c 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -529,13 +529,9 @@ public: };/* class QueryCommand */ class CVC4_PUBLIC CheckSynthCommand : public Command { -protected: - Expr d_expr; - Result d_result; - bool d_inUnsatCore; public: CheckSynthCommand() throw(); - CheckSynthCommand(const Expr& expr, bool inUnsatCore = true) throw(); + CheckSynthCommand(const Expr& expr) throw(); ~CheckSynthCommand() throw() {} Expr getExpr() const throw(); void invoke(SmtEngine* smtEngine); @@ -544,6 +540,14 @@ public: Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; std::string getCommandName() const throw(); + + protected: + /** the assertion of check-synth */ + Expr d_expr; + /** result of the check-synth call */ + Result d_result; + /** string stream that stores the output of the solution */ + std::stringstream d_solution; };/* class CheckSynthCommand */ // this is TRANSFORM in the CVC presentation language diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f93d8bd7f..2ff115606 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1294,6 +1294,13 @@ void SmtEngine::setDefaults() { options::bitvectorDivByZeroConst.set(options::inputLanguage() == language::input::LANG_SMTLIB_V2_6); } + if (options::inputLanguage() == language::input::LANG_SYGUS) + { + if (!options::ceGuidedInst.wasSetByUser()) + { + options::ceGuidedInst.set(true); + } + } if(options::forceLogicString.wasSetByUser()) { d_logic = LogicInfo(options::forceLogicString()); |