diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-03 15:36:38 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-03 15:36:38 -0500 |
commit | 5cafed748989602263b8ad1a27ac6b9bd159a441 (patch) | |
tree | b0e474f47251d480dce48637e73f663aba0dd179 /src | |
parent | 3f2c2c745ae2f13441c1cabd363e6539c9bdaeb9 (diff) |
Sygus clean main (#1297)
* Remove front end hack for sygus.
* Remove other hack, add sygus solution output mode.
* Clang format
* Minor
* Fix
* Minor
* Remove unused field.
Diffstat (limited to 'src')
-rw-r--r-- | src/main/driver_unified.cpp | 10 | ||||
-rw-r--r-- | src/options/Makefile.am | 1 | ||||
-rw-r--r-- | src/options/options.h | 2 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 51 | ||||
-rw-r--r-- | src/options/options_handler.h | 6 | ||||
-rw-r--r-- | src/options/options_public_functions.cpp | 7 | ||||
-rw-r--r-- | src/options/quantifiers_options | 2 | ||||
-rw-r--r-- | src/options/smt_options | 2 | ||||
-rw-r--r-- | src/options/sygus_out_mode.h | 39 | ||||
-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 |
12 files changed, 146 insertions, 32 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 8ffb47e40..ebfc7266b 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -187,16 +187,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { opts.setOutputLanguage(language::toOutputLanguage(opts.getInputLanguage())); } - // if doing sygus, turn on CEGQI by default - if(opts.getInputLanguage() == language::input::LANG_SYGUS ){ - if( !opts.wasSetByUserCeGuidedInst()) { - opts.setCeGuidedInst(true); - } - if( !opts.wasSetByUserDumpSynth()) { - opts.setDumpSynth(true); - } - } - // Determine which messages to show based on smtcomp_mode and verbosity if(Configuration::isMuzzledBuild()) { DebugChannel.setStream(&CVC4::null_os); diff --git a/src/options/Makefile.am b/src/options/Makefile.am index ff889bcb2..54027c128 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -252,6 +252,7 @@ liboptions_la_SOURCES = \ set_language.h \ simplification_mode.cpp \ simplification_mode.h \ + sygus_out_mode.h \ theoryof_mode.cpp \ theoryof_mode.h \ ufss_mode.h diff --git a/src/options/options.h b/src/options/options.h index f93663095..474ef0f96 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -242,8 +242,6 @@ public: // TODO: Document these. - void setCeGuidedInst(bool); - void setDumpSynth(bool); void setInputLanguage(InputLanguage); void setInteractive(bool); void setOut(std::ostream*); diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 351c8b608..3d74091fd 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -554,7 +554,6 @@ all \n\ \n\ "; - theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) { if(optarg == "pre-full") { return theory::quantifiers::INST_WHEN_PRE_FULL; @@ -1311,6 +1310,56 @@ SimplificationMode OptionsHandler::stringToSimplificationMode(std::string option } } +const std::string OptionsHandler::s_sygusSolutionOutModeHelp = + "\ +Modes for finite model finding bound minimization, supported by --sygus-out:\n\ +\n\ +status \n\ ++ Print only status for check-synth calls.\n\ +\n\ +status-and-def (default) \n\ ++ Print status followed by definition corresponding to solution.\n\ +\n\ +status-or-def \n\ ++ Print status if infeasible, or definition corresponding to\n\ + solution if feasible.\n\ +\n\ +sygus-standard \n\ ++ Print based on SyGuS standard.\n\ +\n\ +"; + +SygusSolutionOutMode OptionsHandler::stringToSygusSolutionOutMode( + std::string option, std::string optarg) throw(OptionException) +{ + if (optarg == "status") + { + return SYGUS_SOL_OUT_STATUS; + } + else if (optarg == "status-and-def") + { + return SYGUS_SOL_OUT_STATUS_AND_DEF; + } + else if (optarg == "status-or-def") + { + return SYGUS_SOL_OUT_STATUS_OR_DEF; + } + else if (optarg == "sygus-standard") + { + return SYGUS_SOL_OUT_STANDARD; + } + else if (optarg == "help") + { + puts(s_sygusSolutionOutModeHelp.c_str()); + exit(1); + } + else + { + throw OptionException(std::string("unknown option for --sygus-out: `") + + optarg + + "'. Try --sygus-out help."); + } +} void OptionsHandler::setProduceAssertions(std::string option, bool value) throw() { options::produceAssertions.set(value); diff --git a/src/options/options_handler.h b/src/options/options_handler.h index c525c9e0e..9d5f8cc6e 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -28,14 +28,15 @@ #include "options/arith_unate_lemma_mode.h" #include "options/base_handlers.h" #include "options/bv_bitblast_mode.h" -#include "options/decision_mode.h" #include "options/datatypes_modes.h" +#include "options/decision_mode.h" #include "options/language.h" #include "options/option_exception.h" #include "options/options.h" #include "options/printer_modes.h" #include "options/quantifiers_modes.h" #include "options/simplification_mode.h" +#include "options/sygus_out_mode.h" #include "options/theoryof_mode.h" #include "options/ufss_mode.h" @@ -143,6 +144,8 @@ public: void notifyBeforeSearch(const std::string& option) throw(ModalException); void notifyDumpMode(std::string option) throw(OptionException); SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException); + SygusSolutionOutMode stringToSygusSolutionOutMode( + std::string option, std::string optarg) throw(OptionException); void setProduceAssertions(std::string option, bool value) throw(); void proofEnabledBuild(std::string option, bool value) throw(OptionException); void LFSCEnabledBuild(std::string option, bool value); @@ -218,6 +221,7 @@ public: static const std::string s_qcfModeHelp; static const std::string s_qcfWhenModeHelp; static const std::string s_simplificationHelp; + static const std::string s_sygusSolutionOutModeHelp; static const std::string s_cbqiBvIneqModeHelp; static const std::string s_cegqiSingleInvHelp; static const std::string s_sygusInvTemplHelp; diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index 7d71c267a..b8db9d9da 100644 --- a/src/options/options_public_functions.cpp +++ b/src/options/options_public_functions.cpp @@ -241,13 +241,6 @@ std::ostream* Options::currentGetOut() { // TODO: Document these. -void Options::setCeGuidedInst(bool value) { - set(options::ceGuidedInst, value); -} - -void Options::setDumpSynth(bool value) { - set(options::dumpSynth, value); -} void Options::setInputLanguage(InputLanguage value) { set(options::inputLanguage, value); diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index ba7c8338a..c92813bf4 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -246,7 +246,7 @@ option conjectureGenMaxDepth --conjecture-gen-max-depth=N int :default 3 ### synthesis options option ceGuidedInst --cegqi bool :default false :read-write - counterexample-guided quantifier instantiation + counterexample-guided quantifier instantiation for sygus option cegqiSingleInvMode --cegqi-si=MODE CVC4::theory::quantifiers::CegqiSingleInvMode :default CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToCegqiSingleInvMode :read-write mode for processing single invocation synthesis conjectures option cegqiSingleInvPartial --cegqi-si-partial bool :default false diff --git a/src/options/smt_options b/src/options/smt_options index 00424e103..c701d5c20 100644 --- a/src/options/smt_options +++ b/src/options/smt_options @@ -39,6 +39,8 @@ option dumpProofs --dump-proofs bool :default false :link --proof :link-smt prod output proofs after every UNSAT/VALID response option dumpInstantiations --dump-instantiations bool :default false output instantiations of quantified formulas after every UNSAT/VALID response +option sygusOut --sygus-out=MODE SygusSolutionOutMode :default SYGUS_SOL_OUT_STATUS_AND_DEF :include "options/sygus_out_mode.h" :handler stringToSygusSolutionOutMode :read-write + output mode for sygus option dumpSynth --dump-synth bool :read-write :default false output solution for synthesis conjectures after every UNSAT/VALID response option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate proofEnabledBuild :notify :notify notifyBeforeSearch diff --git a/src/options/sygus_out_mode.h b/src/options/sygus_out_mode.h new file mode 100644 index 000000000..9f94be27f --- /dev/null +++ b/src/options/sygus_out_mode.h @@ -0,0 +1,39 @@ +/********************* */ +/*! \file sygus_out_mode.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Options for sygus solution output. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__SMT__SYGUS_OUT_MODE_H +#define __CVC4__SMT__SYGUS_OUT_MODE_H + +#include <iosfwd> + +namespace CVC4 { + +/** Mode for printing sygus solutions. */ +enum SygusSolutionOutMode +{ + /** print status */ + SYGUS_SOL_OUT_STATUS, + /** (default) print status and solution */ + SYGUS_SOL_OUT_STATUS_AND_DEF, + /** print status if infeasible, or solution if feasible */ + SYGUS_SOL_OUT_STATUS_OR_DEF, + /** print output specified by sygus standard */ + SYGUS_SOL_OUT_STANDARD, +}; + +} /* CVC4 namespace */ + +#endif /* __CVC4__SMT__SYGUS_OUT_MODE_H */ 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()); |