From: Andrew Reynolds Date: Sat, 20 Oct 2018 01:59:51 +0000 (-0500) Subject: Sygus streaming non-implied predicates (#2660) X-Git-Tag: cvc5-1.0.0~4399 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ccc301aa495153b3a2bd1b3958cc49cef65b09cc;p=cvc5.git Sygus streaming non-implied predicates (#2660) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4cf8412f0..10db1dc86 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -522,6 +522,8 @@ libcvc4_add_sources( theory/quantifiers/single_inv_partition.h theory/quantifiers/skolemize.cpp theory/quantifiers/skolemize.h + theory/quantifiers/solution_filter.cpp + theory/quantifiers/solution_filter.h theory/quantifiers/sygus/ce_guided_single_inv.cpp theory/quantifiers/sygus/ce_guided_single_inv.h theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 1c2405449..0762622f0 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1094,7 +1094,6 @@ header = "options/quantifiers_options.h" default = "CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST" handler = "stringToSygusInvTemplMode" includes = ["options/quantifiers_modes.h"] - read_only = true help = "template mode for sygus invariant synthesis (weaken pre-condition, strengthen post-condition, or none)" [[option]] @@ -1395,6 +1394,14 @@ header = "options/quantifiers_options.h" default = "false" help = "dump external files corresponding to interesting satisfiability queries with sygus-query-gen" +[[option]] + name = "sygusSolFilterImplied" + category = "regular" + long = "sygus-sol-filter-implied" + type = "bool" + default = "false" + help = "use sygus to enumerate interesting satisfiability queries" + [[option]] name = "sygusExprMinerCheckUseExport" category = "expert" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e5db42a22..149d8bb35 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1927,7 +1927,9 @@ void SmtEngine::setDefaults() { } if (options::sygusStream()) { - // PBE and streaming modes are incompatible + // Streaming is incompatible with techniques that focus the search towards + // finding a single solution. This currently includes the PBE solver and + // static template inference for invariant synthesis. if (!options::sygusSymBreakPbe.wasSetByUser()) { options::sygusSymBreakPbe.set(false); @@ -1936,6 +1938,10 @@ void SmtEngine::setDefaults() { { options::sygusUnifPbe.set(false); } + if (!options::sygusInvTemplMode.wasSetByUser()) + { + options::sygusInvTemplMode.set(quantifiers::SYGUS_INV_TEMPL_MODE_NONE); + } } //do not allow partial functions if( !options::bitvectorDivByZeroConst.wasSetByUser() ){ diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp index 010b5a4ab..cc97888e3 100644 --- a/src/theory/quantifiers/expr_miner_manager.cpp +++ b/src/theory/quantifiers/expr_miner_manager.cpp @@ -22,6 +22,7 @@ namespace quantifiers { ExpressionMinerManager::ExpressionMinerManager() : d_doRewSynth(false), d_doQueryGen(false), + d_doFilterImplied(false), d_use_sygus_type(false), d_qe(nullptr), d_tds(nullptr) @@ -35,6 +36,7 @@ void ExpressionMinerManager::initialize(const std::vector& vars, { d_doRewSynth = false; d_doQueryGen = false; + d_doFilterImplied = false; d_sygus_fun = Node::null(); d_use_sygus_type = false; d_qe = nullptr; @@ -50,6 +52,7 @@ void ExpressionMinerManager::initializeSygus(QuantifiersEngine* qe, { d_doRewSynth = false; d_doQueryGen = false; + d_doFilterImplied = false; d_sygus_fun = f; d_use_sygus_type = useSygusType; d_qe = qe; @@ -104,22 +107,43 @@ void ExpressionMinerManager::enableQueryGeneration(unsigned deqThresh) d_qg.setThreshold(deqThresh); } +void ExpressionMinerManager::enableFilterImpliedSolutions() +{ + d_doFilterImplied = true; + std::vector vars; + d_sampler.getVariables(vars); + d_solf.initialize(vars, &d_sampler); +} + bool ExpressionMinerManager::addTerm(Node sol, std::ostream& out, bool& rew_print) { - bool ret = d_crd.addTerm(sol, out, rew_print); + // set the builtin version + Node solb = sol; + if (d_use_sygus_type) + { + solb = d_tds->sygusToBuiltin(sol); + } + + // add to the candidate rewrite rule database + bool ret = true; + if (d_doRewSynth) + { + ret = d_crd.addTerm(sol, out, rew_print); + } + + // a unique term, let's try the query generator if (ret && d_doQueryGen) { - // use the builtin version if d_use_sygus_type is true - Node solb = sol; - if (d_use_sygus_type) - { - solb = d_tds->sygusToBuiltin(sol); - } - // a unique term, let's try the query generator d_qg.addTerm(solb, out); } + + // filter if it's implied + if (ret && d_doFilterImplied) + { + ret = d_solf.addTerm(solb, out); + } return ret; } diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h index d15b69cb5..d8e6ae651 100644 --- a/src/theory/quantifiers/expr_miner_manager.h +++ b/src/theory/quantifiers/expr_miner_manager.h @@ -21,6 +21,7 @@ #include "theory/quantifiers/candidate_rewrite_database.h" #include "theory/quantifiers/extended_rewrite.h" #include "theory/quantifiers/query_generator.h" +#include "theory/quantifiers/solution_filter.h" #include "theory/quantifiers/sygus_sampler.h" #include "theory/quantifiers_engine.h" @@ -70,6 +71,8 @@ class ExpressionMinerManager void enableRewriteRuleSynth(); /** enable query generation (--sygus-query-gen) */ void enableQueryGeneration(unsigned deqThresh); + /** filter implied solutions (--sygus-sol-filter-implied) */ + void enableFilterImpliedSolutions(); /** add term * * Expression miners may print information on the output stream out, for @@ -89,6 +92,8 @@ class ExpressionMinerManager bool d_doRewSynth; /** whether we are doing query generation */ bool d_doQueryGen; + /** whether we are filtering implied candidates */ + bool d_doFilterImplied; /** the sygus function passed to initializeSygus, if any */ Node d_sygus_fun; /** whether we are using sygus types */ @@ -101,6 +106,8 @@ class ExpressionMinerManager CandidateRewriteDatabase d_crd; /** query generator */ QueryGenerator d_qg; + /** solution filter */ + SolutionFilter d_solf; /** 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 new file mode 100644 index 000000000..bea3356d1 --- /dev/null +++ b/src/theory/quantifiers/solution_filter.cpp @@ -0,0 +1,92 @@ +/********************* */ +/*! \file solution_filter.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 Utilities for filtering solutions. + **/ + +#include "theory/quantifiers/solution_filter.h" + +#include +#include "options/quantifiers_options.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "util/random.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +SolutionFilter::SolutionFilter() {} +void SolutionFilter::initialize(const std::vector& vars, SygusSampler* ss) +{ + ExprMiner::initialize(vars, ss); +} + +bool SolutionFilter::addTerm(Node n, std::ostream& out) +{ + if (!n.getType().isBoolean()) + { + // currently, should not register non-Boolean terms here + Assert(false); + return true; + } + 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()) + { + if (!imp.getConst()) + { + // if the implication rewrites to false, we filter + Trace("sygus-sol-implied-filter") << "Filtered (by rewriting) : " << n + << std::endl; + return false; + } + else + { + // if the implication rewrites to true, it is trivial + success = true; + } + } + if (!success) + { + 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) + { + success = true; + } + } + 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; +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/solution_filter.h b/src/theory/quantifiers/solution_filter.h new file mode 100644 index 000000000..9f098cf69 --- /dev/null +++ b/src/theory/quantifiers/solution_filter.h @@ -0,0 +1,62 @@ +/********************* */ +/*! \file solution_filter.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 Utility for filtering sygus solutions. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H +#define __CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H + +#include +#include +#include "expr/node.h" +#include "theory/quantifiers/expr_miner.h" +#include "theory/quantifiers/lazy_trie.h" +#include "theory/quantifiers/sygus_sampler.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** + * This class is used to filter solutions based on some criteria. + * + * Currently, it is used to filter predicate solutions that are collectively + * entailed by the previous predicate solutions. + */ +class SolutionFilter : public ExprMiner +{ + public: + SolutionFilter(); + ~SolutionFilter() {} + /** 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. + */ + bool addTerm(Node n, std::ostream& out) override; + + private: + /** conjunction of all (non-implied) terms registered to this class */ + Node d_conj; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H */ diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 32342a9ba..adc20008e 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -955,7 +955,7 @@ void SynthConjecture::printAndContinueStream() void SynthConjecture::printSynthSolution(std::ostream& out) { - Trace("cegqi-debug") << "Printing synth solution..." << std::endl; + Trace("cegqi-sol-debug") << "Printing synth solution..." << std::endl; Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren()); std::vector sols; std::vector statuses; @@ -981,8 +981,10 @@ void SynthConjecture::printSynthSolution(std::ostream& out) bool is_unique_term = true; - if (status != 0 && (options::sygusRewSynth() || options::sygusQueryGen())) + if (status != 0 && (options::sygusRewSynth() || options::sygusQueryGen() + || options::sygusSolFilterImplied())) { + Trace("cegqi-sol-debug") << "Run expression mining..." << std::endl; std::map::iterator its = d_exprm.find(prog); if (its == d_exprm.end()) @@ -997,6 +999,10 @@ void SynthConjecture::printSynthSolution(std::ostream& out) { d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh()); } + if (options::sygusSolFilterImplied()) + { + d_exprm[prog].enableFilterImpliedSolutions(); + } its = d_exprm.find(prog); } bool rew_print = false; @@ -1007,7 +1013,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out) } if (!is_unique_term) { - ++(cei->d_statistics.d_candidate_rewrites); + ++(cei->d_statistics.d_filtered_solutions); } } if (is_unique_term) diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index ba227bc8f..479cfa535 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -426,17 +426,16 @@ SynthEngine::Statistics::Statistics() d_cegqi_lemmas_refine("SynthEngine::cegqi_lemmas_refine", 0), d_cegqi_si_lemmas("SynthEngine::cegqi_lemmas_si", 0), d_solutions("SynthConjecture::solutions", 0), - d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print", - 0), - d_candidate_rewrites("SynthConjecture::candidate_rewrites", 0) + d_filtered_solutions("SynthConjecture::filtered_solutions", 0), + d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print", 0) { smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce); smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine); smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas); smtStatisticsRegistry()->registerStat(&d_solutions); + smtStatisticsRegistry()->registerStat(&d_filtered_solutions); smtStatisticsRegistry()->registerStat(&d_candidate_rewrites_print); - smtStatisticsRegistry()->registerStat(&d_candidate_rewrites); } SynthEngine::Statistics::~Statistics() @@ -445,8 +444,8 @@ SynthEngine::Statistics::~Statistics() smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine); smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas); smtStatisticsRegistry()->unregisterStat(&d_solutions); + smtStatisticsRegistry()->unregisterStat(&d_filtered_solutions); smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites_print); - smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites); } } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index 8f0eea58f..a7346b888 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -100,8 +100,8 @@ class SynthEngine : public QuantifiersModule IntStat d_cegqi_lemmas_refine; IntStat d_cegqi_si_lemmas; IntStat d_solutions; + IntStat d_filtered_solutions; IntStat d_candidate_rewrites_print; - IntStat d_candidate_rewrites; Statistics(); ~Statistics(); }; /* class SynthEngine::Statistics */