\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\
}
}
+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)
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(
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;
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,
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"
}
}
+Result ExprMiner::doCheck(Node query)
+{
+ Node queryr = Rewriter::rewrite(query);
+ if (queryr.isConst())
+ {
+ if (!queryr.getConst<bool>())
+ {
+ 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<SmtEngine> smte;
+ initializeChecker(smte, em, varMap, queryr, needExport);
+ return smte->checkSat();
+}
+
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
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
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)
{
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;
{
d_doRewSynth = false;
d_doQueryGen = false;
- d_doFilterImplied = false;
+ d_doFilterLogicalStrength = false;
d_sygus_fun = f;
d_use_sygus_type = useSygusType;
d_qe = qe;
d_qg.setThreshold(deqThresh);
}
-void ExpressionMinerManager::enableFilterImpliedSolutions()
+void ExpressionMinerManager::enableFilterWeakSolutions()
{
- d_doFilterImplied = true;
+ d_doFilterLogicalStrength = true;
std::vector<Node> 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<Node> vars;
+ d_sampler.getVariables(vars);
+ d_sols.initialize(vars, &d_sampler);
+ d_sols.setLogicallyStrong(false);
}
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;
}
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
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 */
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 */
namespace theory {
namespace quantifiers {
-SolutionFilter::SolutionFilter() {}
-void SolutionFilter::initialize(const std::vector<Node>& vars, SygusSampler* ss)
+SolutionFilterStrength::SolutionFilterStrength() : d_isStrong(true) {}
+void SolutionFilterStrength::initialize(const std::vector<Node>& 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())
{
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<bool>())
+ 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<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)
+ std::vector<Node> 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
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<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.
+ * 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<Node> d_curr_sols;
+ /** whether we are trying to find the logically strongest solutions */
+ bool d_isStrong;
};
} // namespace quantifiers
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<Node, ExpressionMinerManager>::iterator its =
{
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);
}
projects / cvc5.git / commitdiff