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
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]]
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"
}
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);
{
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() ){
ExpressionMinerManager::ExpressionMinerManager()
: d_doRewSynth(false),
d_doQueryGen(false),
+ d_doFilterImplied(false),
d_use_sygus_type(false),
d_qe(nullptr),
d_tds(nullptr)
{
d_doRewSynth = false;
d_doQueryGen = false;
+ d_doFilterImplied = false;
d_sygus_fun = Node::null();
d_use_sygus_type = false;
d_qe = nullptr;
{
d_doRewSynth = false;
d_doQueryGen = false;
+ d_doFilterImplied = false;
d_sygus_fun = f;
d_use_sygus_type = useSygusType;
d_qe = qe;
d_qg.setThreshold(deqThresh);
}
+void ExpressionMinerManager::enableFilterImpliedSolutions()
+{
+ d_doFilterImplied = true;
+ std::vector<Node> 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;
}
#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"
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
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 */
CandidateRewriteDatabase d_crd;
/** query generator */
QueryGenerator d_qg;
+ /** solution filter */
+ SolutionFilter d_solf;
/** sygus sampler object */
SygusSampler d_sampler;
/** extended rewriter object */
--- /dev/null
+/********************* */
+/*! \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 <fstream>
+#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<Node>& 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<bool>())
+ {
+ // 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<SmtEngine> 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
--- /dev/null
+/********************* */
+/*! \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 <map>
+#include <unordered_set>
+#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<Node>& 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 */
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<Node> sols;
std::vector<int> statuses;
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<Node, ExpressionMinerManager>::iterator its =
d_exprm.find(prog);
if (its == d_exprm.end())
{
d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh());
}
+ if (options::sygusSolFilterImplied())
+ {
+ d_exprm[prog].enableFilterImpliedSolutions();
+ }
its = d_exprm.find(prog);
}
bool rew_print = false;
}
if (!is_unique_term)
{
- ++(cei->d_statistics.d_candidate_rewrites);
+ ++(cei->d_statistics.d_filtered_solutions);
}
}
if (is_unique_term)
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()
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
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 */
projects / cvc5.git / commitdiff