From e194e29c76f30ab9f0b42d20af699f132ef82fe4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 28 Nov 2018 11:06:32 -0600 Subject: [PATCH] Generalize sygus stream solution filtering to logical strength (#2697) --- src/options/options_handler.cpp | 44 +++++++++ src/options/options_handler.h | 3 + src/options/quantifiers_modes.h | 10 +++ src/options/quantifiers_options.toml | 16 +++- src/theory/quantifiers/expr_miner.cpp | 23 +++++ src/theory/quantifiers/expr_miner.h | 8 ++ src/theory/quantifiers/expr_miner_manager.cpp | 28 ++++-- src/theory/quantifiers/expr_miner_manager.h | 14 +-- src/theory/quantifiers/solution_filter.cpp | 89 +++++++++++-------- src/theory/quantifiers/solution_filter.h | 35 +++++--- .../quantifiers/sygus/synth_conjecture.cpp | 16 +++- 11 files changed, 215 insertions(+), 71 deletions(-) diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 565f28334..bd5b00728 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -508,6 +508,21 @@ trust \n\ \n\ "; +const std::string OptionsHandler::s_sygusFilterSolHelp = + "\ +Modes for filtering sygus solutions supported by --sygus-filter-sol:\n\ +\n\ +none (default) \n\ ++ Do not filter sygus solutions.\n\ +\n\ +strong \n\ ++ Filter solutions that are logically stronger than others.\n\ +\n\ +weak \n\ ++ Filter solutions that are logically weaker than others.\n\ +\n\ +"; + const std::string OptionsHandler::s_sygusInvTemplHelp = "\ Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\ \n\ @@ -951,6 +966,35 @@ theory::quantifiers::CegisSampleMode OptionsHandler::stringToCegisSampleMode( } } +theory::quantifiers::SygusFilterSolMode +OptionsHandler::stringToSygusFilterSolMode(std::string option, + std::string optarg) +{ + if (optarg == "none") + { + return theory::quantifiers::SYGUS_FILTER_SOL_NONE; + } + else if (optarg == "strong") + { + return theory::quantifiers::SYGUS_FILTER_SOL_STRONG; + } + else if (optarg == "weak") + { + return theory::quantifiers::SYGUS_FILTER_SOL_WEAK; + } + else if (optarg == "help") + { + puts(s_cegisSampleHelp.c_str()); + exit(1); + } + else + { + throw OptionException( + std::string("unknown option for --sygus-filter-sol: `") + optarg + + "'. Try --sygus-filter-sol help."); + } +} + theory::quantifiers::SygusInvTemplMode OptionsHandler::stringToSygusInvTemplMode(std::string option, std::string optarg) diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 3078db0f8..53e317895 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -112,6 +112,8 @@ public: std::string option, std::string optarg); theory::quantifiers::CegisSampleMode stringToCegisSampleMode( std::string option, std::string optarg); + theory::quantifiers::SygusFilterSolMode stringToSygusFilterSolMode( + std::string option, std::string optarg); theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode( std::string option, std::string optarg); theory::quantifiers::SygusActiveGenMode stringToSygusActiveGenMode( @@ -248,6 +250,7 @@ public: static const std::string s_cegqiSingleInvHelp; static const std::string s_cegqiSingleInvRconsHelp; static const std::string s_cegisSampleHelp; + static const std::string s_sygusFilterSolHelp; static const std::string s_sygusInvTemplHelp; static const std::string s_sygusActiveGenHelp; static const std::string s_termDbModeHelp; diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index 05388cdf6..41378d2cd 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -276,6 +276,16 @@ enum SygusActiveGenMode SYGUS_ACTIVE_GEN_AUTO, }; +enum SygusFilterSolMode +{ + /** do not filter solutions */ + SYGUS_FILTER_SOL_NONE, + /** filter logically stronger solutions */ + SYGUS_FILTER_SOL_STRONG, + /** filter logically weaker solutions */ + SYGUS_FILTER_SOL_WEAK, +}; + enum MacrosQuantMode { /** infer all definitions */ MACROS_QUANT_MODE_ALL, diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index c555c37bf..d9d3e0d38 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1403,12 +1403,22 @@ header = "options/quantifiers_options.h" help = "dump external files corresponding to interesting satisfiability queries with sygus-query-gen" [[option]] - name = "sygusSolFilterImplied" + name = "sygusFilterSolMode" category = "regular" - long = "sygus-sol-filter-implied" + long = "sygus-filter-sol=MODE" + type = "CVC4::theory::quantifiers::SygusFilterSolMode" + default = "CVC4::theory::quantifiers::SYGUS_FILTER_SOL_NONE" + handler = "stringToSygusFilterSolMode" + includes = ["options/quantifiers_modes.h"] + help = "mode for filtering sygus solutions" + +[[option]] + name = "sygusFilterSolRevSubsume" + category = "expert" + long = "sygus-filter-sol-rev" type = "bool" default = "false" - help = "use sygus to enumerate interesting satisfiability queries" + help = "compute backwards filtering to compute whether previous solutions are filtered based on later ones" [[option]] name = "sygusExprMinerCheckUseExport" diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 16e59c119..b65d1c522 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -113,6 +113,29 @@ void ExprMiner::initializeChecker(std::unique_ptr& checker, } } +Result ExprMiner::doCheck(Node query) +{ + Node queryr = Rewriter::rewrite(query); + if (queryr.isConst()) + { + if (!queryr.getConst()) + { + return Result(Result::UNSAT); + } + else + { + return Result(Result::SAT); + } + } + NodeManager* nm = NodeManager::currentNM(); + bool needExport = false; + ExprManagerMapCollection varMap; + ExprManager em(nm->getOptions()); + std::unique_ptr smte; + initializeChecker(smte, em, varMap, queryr, needExport); + return smte->checkSat(); +} + } // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index c09f40d0e..59d9989c5 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -92,6 +92,14 @@ class ExprMiner ExprManagerMapCollection& varMap, Node query, bool& needExport); + /** + * Run the satisfiability check on query and return the result + * (sat/unsat/unknown). + * + * In contrast to the above method, this call should be used for cases where + * the model for the query is not important. + */ + Result doCheck(Node query); }; } // namespace quantifiers diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp index cc97888e3..a808d386c 100644 --- a/src/theory/quantifiers/expr_miner_manager.cpp +++ b/src/theory/quantifiers/expr_miner_manager.cpp @@ -22,7 +22,7 @@ namespace quantifiers { ExpressionMinerManager::ExpressionMinerManager() : d_doRewSynth(false), d_doQueryGen(false), - d_doFilterImplied(false), + d_doFilterLogicalStrength(false), d_use_sygus_type(false), d_qe(nullptr), d_tds(nullptr) @@ -36,7 +36,7 @@ void ExpressionMinerManager::initialize(const std::vector& vars, { d_doRewSynth = false; d_doQueryGen = false; - d_doFilterImplied = false; + d_doFilterLogicalStrength = false; d_sygus_fun = Node::null(); d_use_sygus_type = false; d_qe = nullptr; @@ -52,7 +52,7 @@ void ExpressionMinerManager::initializeSygus(QuantifiersEngine* qe, { d_doRewSynth = false; d_doQueryGen = false; - d_doFilterImplied = false; + d_doFilterLogicalStrength = false; d_sygus_fun = f; d_use_sygus_type = useSygusType; d_qe = qe; @@ -107,12 +107,22 @@ void ExpressionMinerManager::enableQueryGeneration(unsigned deqThresh) d_qg.setThreshold(deqThresh); } -void ExpressionMinerManager::enableFilterImpliedSolutions() +void ExpressionMinerManager::enableFilterWeakSolutions() { - d_doFilterImplied = true; + d_doFilterLogicalStrength = true; std::vector vars; d_sampler.getVariables(vars); - d_solf.initialize(vars, &d_sampler); + d_sols.initialize(vars, &d_sampler); + d_sols.setLogicallyStrong(true); +} + +void ExpressionMinerManager::enableFilterStrongSolutions() +{ + d_doFilterLogicalStrength = true; + std::vector vars; + d_sampler.getVariables(vars); + d_sols.initialize(vars, &d_sampler); + d_sols.setLogicallyStrong(false); } bool ExpressionMinerManager::addTerm(Node sol, @@ -139,10 +149,10 @@ bool ExpressionMinerManager::addTerm(Node sol, d_qg.addTerm(solb, out); } - // filter if it's implied - if (ret && d_doFilterImplied) + // filter based on logical strength + if (ret && d_doFilterLogicalStrength) { - ret = d_solf.addTerm(solb, out); + ret = d_sols.addTerm(solb, out); } return ret; } diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h index d8e6ae651..d817d3775 100644 --- a/src/theory/quantifiers/expr_miner_manager.h +++ b/src/theory/quantifiers/expr_miner_manager.h @@ -71,8 +71,10 @@ class ExpressionMinerManager void enableRewriteRuleSynth(); /** enable query generation (--sygus-query-gen) */ void enableQueryGeneration(unsigned deqThresh); - /** filter implied solutions (--sygus-sol-filter-implied) */ - void enableFilterImpliedSolutions(); + /** filter strong solutions (--sygus-filter-sol=strong) */ + void enableFilterStrongSolutions(); + /** filter weak solutions (--sygus-filter-sol=weak) */ + void enableFilterWeakSolutions(); /** add term * * Expression miners may print information on the output stream out, for @@ -92,8 +94,8 @@ class ExpressionMinerManager bool d_doRewSynth; /** whether we are doing query generation */ bool d_doQueryGen; - /** whether we are filtering implied candidates */ - bool d_doFilterImplied; + /** whether we are filtering solutions based on logical strength */ + bool d_doFilterLogicalStrength; /** the sygus function passed to initializeSygus, if any */ Node d_sygus_fun; /** whether we are using sygus types */ @@ -106,8 +108,8 @@ class ExpressionMinerManager CandidateRewriteDatabase d_crd; /** query generator */ QueryGenerator d_qg; - /** solution filter */ - SolutionFilter d_solf; + /** solution filter based on logical strength */ + SolutionFilterStrength d_sols; /** sygus sampler object */ SygusSampler d_sampler; /** extended rewriter object */ diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp index bea3356d1..19d39e997 100644 --- a/src/theory/quantifiers/solution_filter.cpp +++ b/src/theory/quantifiers/solution_filter.cpp @@ -26,13 +26,19 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SolutionFilter::SolutionFilter() {} -void SolutionFilter::initialize(const std::vector& vars, SygusSampler* ss) +SolutionFilterStrength::SolutionFilterStrength() : d_isStrong(true) {} +void SolutionFilterStrength::initialize(const std::vector& vars, + SygusSampler* ss) { ExprMiner::initialize(vars, ss); } -bool SolutionFilter::addTerm(Node n, std::ostream& out) +void SolutionFilterStrength::setLogicallyStrong(bool isStrong) +{ + d_isStrong = isStrong; +} + +bool SolutionFilterStrength::addTerm(Node n, std::ostream& out) { if (!n.getType().isBoolean()) { @@ -40,51 +46,58 @@ bool SolutionFilter::addTerm(Node n, std::ostream& out) Assert(false); return true; } + Node basen = d_isStrong ? n : n.negate(); NodeManager* nm = NodeManager::currentNM(); - Node imp = d_conj.isNull() ? n.negate() : nm->mkNode(AND, d_conj, n.negate()); - imp = Rewriter::rewrite(imp); - bool success = false; - if (imp.isConst()) + // Do i subsume the disjunction of all previous solutions? If so, we discard + // this immediately + Node curr; + if (!d_curr_sols.empty()) { - if (!imp.getConst()) + curr = d_curr_sols.size() == 1 + ? d_curr_sols[0] + : nm->mkNode(d_isStrong ? AND : OR, d_curr_sols); + Node imp = nm->mkNode(AND, basen.negate(), curr); + Trace("sygus-sol-implied") + << " implies: check subsumed " << imp << "..." << std::endl; + // check the satisfiability query + Result r = doCheck(imp); + Trace("sygus-sol-implied") << " implies: ...got : " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) { - // if the implication rewrites to false, we filter - Trace("sygus-sol-implied-filter") << "Filtered (by rewriting) : " << n - << std::endl; + // it is subsumed by the current, discard this return false; } - else - { - // if the implication rewrites to true, it is trivial - success = true; - } } - if (!success) + // check which solutions would have been filtered if the current had come + // first + if (options::sygusFilterSolRevSubsume()) { - Trace("sygus-sol-implied") << " implies: check " << imp << "..." - << std::endl; - // make the satisfiability query - bool needExport = false; - ExprManagerMapCollection varMap; - ExprManager em(nm->getOptions()); - std::unique_ptr queryChecker; - initializeChecker(queryChecker, em, varMap, imp, needExport); - Result r = queryChecker->checkSat(); - Trace("sygus-sol-implied") << " implies: ...got : " << r << std::endl; - if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) + std::vector nsubsume; + for (const Node& s : d_curr_sols) { - success = true; + Node imp = nm->mkNode(AND, s.negate(), basen); + Trace("sygus-sol-implied") + << " implies: check subsuming " << imp << "..." << std::endl; + // check the satisfiability query + Result r = doCheck(imp); + Trace("sygus-sol-implied") << " implies: ...got : " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) + { + nsubsume.push_back(s); + } + else + { + Options& nodeManagerOptions = nm->getOptions(); + std::ostream* out = nodeManagerOptions.getOut(); + (*out) << "; (filtered " << (d_isStrong ? s : s.negate()) << ")" + << std::endl; + } } + d_curr_sols.clear(); + d_curr_sols.insert(d_curr_sols.end(), nsubsume.begin(), nsubsume.end()); } - if (success) - { - d_conj = d_conj.isNull() ? n : nm->mkNode(AND, d_conj, n); - d_conj = Rewriter::rewrite(d_conj); - // note if d_conj is false, we could terminate here - return true; - } - Trace("sygus-sol-implied-filter") << "Filtered : " << n << std::endl; - return false; + d_curr_sols.push_back(basen); + return true; } } // namespace quantifiers diff --git a/src/theory/quantifiers/solution_filter.h b/src/theory/quantifiers/solution_filter.h index 9f098cf69..d162f41f0 100644 --- a/src/theory/quantifiers/solution_filter.h +++ b/src/theory/quantifiers/solution_filter.h @@ -29,30 +29,43 @@ namespace theory { namespace quantifiers { /** - * This class is used to filter solutions based on some criteria. + * This class is used to filter solutions based on logical strength. * * Currently, it is used to filter predicate solutions that are collectively - * entailed by the previous predicate solutions. + * entailed by the previous predicate solutions (if we are looking for logically + * stronger solutions), or to filter predicate solutions that entail any + * previous predicate (if we are looking for logically weaker solutions). */ -class SolutionFilter : public ExprMiner +class SolutionFilterStrength : public ExprMiner { public: - SolutionFilter(); - ~SolutionFilter() {} + SolutionFilterStrength(); + ~SolutionFilterStrength() {} /** initialize */ void initialize(const std::vector& vars, SygusSampler* ss = nullptr) override; /** - * Add term to this module. It is expected that n has Boolean type. - * If this method returns false, then the entailment n_1 ^ ... ^ n_m |= n - * holds, where n_1, ..., n_m are the terms previously registered to this - * class. + * Add term to this miner. It is expected that n has Boolean type. + * + * If d_isStrong is true, then if this method returns false, then the + * entailment n_1 ^ ... ^ n_m |= n holds, where n_1, ..., n_m are the terms + * previously registered to this class. + * + * Dually, if d_isStrong is false, then if this method returns false, then + * the entailment n |= n_1 V ... V n_m holds. */ bool addTerm(Node n, std::ostream& out) override; + /** set logically strong */ + void setLogicallyStrong(bool isStrong); private: - /** conjunction of all (non-implied) terms registered to this class */ - Node d_conj; + /** + * Set of all (non-filtered) terms registered to this class. We store the + * negation of these terms if d_isStrong is false. + */ + std::vector d_curr_sols; + /** whether we are trying to find the logically strongest solutions */ + bool d_isStrong; }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 3f0ac70f5..ff7bb6378 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -1039,8 +1039,9 @@ void SynthConjecture::printSynthSolution(std::ostream& out) bool is_unique_term = true; - if (status != 0 && (options::sygusRewSynth() || options::sygusQueryGen() - || options::sygusSolFilterImplied())) + if (status != 0 + && (options::sygusRewSynth() || options::sygusQueryGen() + || options::sygusFilterSolMode() != SYGUS_FILTER_SOL_NONE)) { Trace("cegqi-sol-debug") << "Run expression mining..." << std::endl; std::map::iterator its = @@ -1057,9 +1058,16 @@ void SynthConjecture::printSynthSolution(std::ostream& out) { d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh()); } - if (options::sygusSolFilterImplied()) + if (options::sygusFilterSolMode() != SYGUS_FILTER_SOL_NONE) { - d_exprm[prog].enableFilterImpliedSolutions(); + if (options::sygusFilterSolMode() == SYGUS_FILTER_SOL_STRONG) + { + d_exprm[prog].enableFilterStrongSolutions(); + } + else if (options::sygusFilterSolMode() == SYGUS_FILTER_SOL_WEAK) + { + d_exprm[prog].enableFilterWeakSolutions(); + } } its = d_exprm.find(prog); } -- 2.30.2