This adds a new option for --sygus-query-gen=unsat to generate unsat queries (previously, only satisfiable queries were supported).
The algorithm can be seen as a variant of abduction where we conjoin predicates that both (1) refine the current model and (2) avoid repeated unsat cores.
It does some minor refactoring of ExprMinerManager to support the new module.
theory/quantifiers/quantifiers_statistics.h
theory/quantifiers/query_generator.cpp
theory/quantifiers/query_generator.h
+ theory/quantifiers/query_generator_unsat.cpp
+ theory/quantifiers/query_generator_unsat.h
theory/quantifiers/relevant_domain.cpp
theory/quantifiers/relevant_domain.h
theory/quantifiers/single_inv_partition.cpp
[[option]]
name = "sygusQueryGen"
category = "regular"
- long = "sygus-query-gen"
- type = "bool"
- default = "false"
- help = "use sygus to enumerate interesting satisfiability queries"
+ long = "sygus-query-gen=MODE"
+ type = "SygusQueryGenMode"
+ default = "NONE"
+ help = "mode for generating interesting satisfiability queries using SyGuS, for internal fuzzing"
+ help_mode = "Modes for generating interesting satisfiability queries using SyGuS."
+[[option.mode.NONE]]
+ name = "none"
+ help = "Do not generate queries with SyGuS."
+[[option.mode.SAT]]
+ name = "sat"
+ help = "Generate interesting SAT queries, for e.g. soundness testing."
+[[option.mode.UNSAT]]
+ name = "unsat"
+ help = "Generate interesting UNSAT queries, for e.g. proof testing."
[[option]]
name = "sygusQueryGenThresh"
reqBasicSygus = true;
}
if (opts.quantifiers.sygusRewSynth || opts.quantifiers.sygusRewVerify
- || opts.quantifiers.sygusQueryGen)
+ || opts.quantifiers.sygusQueryGen != options::SygusQueryGenMode::NONE)
{
// rewrite rule synthesis implies that sygus stream must be true
opts.quantifiers.sygusStream = true;
const LogicInfo& logicInfo)
{
Assert (!query.isNull());
- if (Options::current().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser)
+ if (options().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser)
{
- initializeSubsolver(
- checker, opts, logicInfo, true, options::sygusExprMinerCheckTimeout());
+ initializeSubsolver(checker,
+ opts,
+ logicInfo,
+ true,
+ options().quantifiers.sygusExprMinerCheckTimeout);
}
else
{
d_use_sygus_type(false),
d_tds(nullptr),
d_crd(env,
- options::sygusRewSynthCheck(),
- options::sygusRewSynthAccel(),
+ options().quantifiers.sygusRewSynthCheck,
+ options().quantifiers.sygusRewSynthAccel,
false),
- d_qg(env),
d_sols(env),
d_sampler(env)
{
d_sampler.initializeSygus(d_tds, f, nsamples, useSygusType);
}
+void ExpressionMinerManager::initializeMinersForOptions()
+{
+ if (options().quantifiers.sygusRewSynth)
+ {
+ enableRewriteRuleSynth();
+ }
+ if (options().quantifiers.sygusQueryGen != options::SygusQueryGenMode::NONE)
+ {
+ enableQueryGeneration(options().quantifiers.sygusQueryGenThresh);
+ }
+ if (options().quantifiers.sygusFilterSolMode
+ != options::SygusFilterSolMode::NONE)
+ {
+ if (options().quantifiers.sygusFilterSolMode
+ == options::SygusFilterSolMode::STRONG)
+ {
+ enableFilterStrongSolutions();
+ }
+ else if (options().quantifiers.sygusFilterSolMode
+ == options::SygusFilterSolMode::WEAK)
+ {
+ enableFilterWeakSolutions();
+ }
+ }
+}
+
void ExpressionMinerManager::enableRewriteRuleSynth()
{
if (d_doRewSynth)
return;
}
d_doQueryGen = true;
+ options::SygusQueryGenMode mode = options().quantifiers.sygusQueryGen;
std::vector<Node> vars;
d_sampler.getVariables(vars);
- // must also enable rewrite rule synthesis
- if (!d_doRewSynth)
+ if (mode == options::SygusQueryGenMode::SAT)
{
- // initialize the candidate rewrite database, in silent mode
- enableRewriteRuleSynth();
- d_crd.setSilent(true);
+ // must also enable rewrite rule synthesis
+ if (!d_doRewSynth)
+ {
+ // initialize the candidate rewrite database, in silent mode
+ enableRewriteRuleSynth();
+ d_crd.setSilent(true);
+ }
+ d_qg = std::make_unique<QueryGenerator>(d_env);
+ // initialize the query generator
+ d_qg->initialize(vars, &d_sampler);
+ d_qg->setThreshold(deqThresh);
+ }
+ else if (mode == options::SygusQueryGenMode::UNSAT)
+ {
+ d_qgu = std::make_unique<QueryGeneratorUnsat>(d_env);
+ // initialize the query generator
+ d_qgu->initialize(vars, &d_sampler);
}
- // initialize the query generator
- d_qg.initialize(vars, &d_sampler);
- d_qg.setThreshold(deqThresh);
}
void ExpressionMinerManager::enableFilterWeakSolutions()
bool ret = true;
if (d_doRewSynth)
{
- Node rsol = d_crd.addTerm(sol, options::sygusRewSynthRec(), out, rew_print);
+ Node rsol = d_crd.addTerm(
+ sol, options().quantifiers.sygusRewSynthRec, out, rew_print);
ret = (sol == rsol);
}
// a unique term, let's try the query generator
if (ret && d_doQueryGen)
{
- d_qg.addTerm(solb, out);
+ options::SygusQueryGenMode mode = options().quantifiers.sygusQueryGen;
+ if (mode == options::SygusQueryGenMode::SAT)
+ {
+ d_qg->addTerm(solb, out);
+ }
+ else if (mode == options::SygusQueryGenMode::UNSAT)
+ {
+ d_qgu->addTerm(solb, out);
+ }
}
// filter based on logical strength
#include "smt/env_obj.h"
#include "theory/quantifiers/candidate_rewrite_database.h"
#include "theory/quantifiers/query_generator.h"
+#include "theory/quantifiers/query_generator_unsat.h"
#include "theory/quantifiers/solution_filter.h"
#include "theory/quantifiers/sygus_sampler.h"
Node f,
unsigned nsamples,
bool useSygusType);
- /** enable rewrite rule synthesis (--sygus-rr-synth) */
- void enableRewriteRuleSynth();
- /** enable query generation (--sygus-query-gen) */
- void enableQueryGeneration(unsigned deqThresh);
- /** filter strong solutions (--sygus-filter-sol=strong) */
- void enableFilterStrongSolutions();
- /** filter weak solutions (--sygus-filter-sol=weak) */
- void enableFilterWeakSolutions();
+ /** initialize options */
+ void initializeMinersForOptions();
/** add term
*
* Expression miners may print information on the output stream out, for
bool addTerm(Node sol, std::ostream& out, bool& rew_print);
private:
+ /** enable rewrite rule synthesis (--sygus-rr-synth) */
+ void enableRewriteRuleSynth();
+ /** enable query generation (--sygus-query-gen) */
+ void enableQueryGeneration(unsigned deqThresh);
+ /** filter strong solutions (--sygus-filter-sol=strong) */
+ void enableFilterStrongSolutions();
+ /** filter weak solutions (--sygus-filter-sol=weak) */
+ void enableFilterWeakSolutions();
/** whether we are doing rewrite synthesis */
bool d_doRewSynth;
/** whether we are doing query generation */
/** candidate rewrite database */
CandidateRewriteDatabase d_crd;
/** query generator */
- QueryGenerator d_qg;
+ std::unique_ptr<QueryGenerator> d_qg;
+ /** query generator */
+ std::unique_ptr<QueryGeneratorUnsat> d_qgu;
/** solution filter based on logical strength */
SolutionFilterStrength d_sols;
/** sygus sampler object */
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * A class for mining interesting unsat queries from a stream of generated
+ * expressions.
+ */
+
+#include "theory/quantifiers/query_generator_unsat.h"
+
+#include "options/smt_options.h"
+#include "smt/env.h"
+#include "util/random.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+QueryGeneratorUnsat::QueryGeneratorUnsat(Env& env)
+ : ExprMiner(env), d_queryCount(0)
+{
+ d_true = NodeManager::currentNM()->mkConst(true);
+ d_false = NodeManager::currentNM()->mkConst(false);
+ // determine the options to use for the verification subsolvers we spawn
+ // we start with the provided options
+ d_subOptions.copyValues(d_env.getOriginalOptions());
+ d_subOptions.smt.produceProofs = true;
+ d_subOptions.smt.checkProofs = true;
+ d_subOptions.smt.produceModels = true;
+ d_subOptions.smt.checkModels = true;
+}
+
+void QueryGeneratorUnsat::initialize(const std::vector<Node>& vars,
+ SygusSampler* ss)
+{
+ Assert(ss != nullptr);
+ d_queryCount = 0;
+ ExprMiner::initialize(vars, ss);
+}
+
+bool QueryGeneratorUnsat::addTerm(Node n, std::ostream& out)
+{
+ d_terms.push_back(n);
+ Trace("sygus-qgen") << "Add term: " << n << std::endl;
+ Assert(n.getType().isBoolean());
+
+ // the loop below conjoins a random subset of predicates we have enumerated
+ // so far C1 ^ ... ^ Cn such that no subset of C1 ... Cn is an unsat core
+ // we have encountered so far, and each appended Ci is false on a model for
+ // C1 ^ ... ^ C_{i-1}.
+ std::vector<Node> currModel;
+ std::unordered_set<size_t> processed;
+ std::vector<Node> activeTerms;
+ // always start with the new term
+ processed.insert(d_terms.size() - 1);
+ activeTerms.push_back(n);
+ bool addSuccess = true;
+ size_t checkCount = 0;
+ while (checkCount < 10)
+ {
+ Assert(!activeTerms.empty());
+ // if we just successfully added a term, do a satisfiability check
+ if (addSuccess)
+ {
+ checkCount++;
+ // check the current for satisfiability
+ currModel.clear();
+ // Shuffle active terms to maximize the different possible behaviors
+ // in the subsolver. This is instead of making multiple queries with
+ // the same assertion order for a subsequence.
+ std::shuffle(activeTerms.begin(), activeTerms.end(), Random::getRandom());
+ Result r = checkCurrent(activeTerms, out, currModel);
+ if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ {
+ // exclude the last active term
+ activeTerms.pop_back();
+ }
+ }
+ if (processed.size() == d_terms.size())
+ {
+ break;
+ }
+ // activeTerms is satisfiable, add a new term
+ size_t rindex = getNextRandomIndex(processed);
+ Assert(rindex < d_terms.size());
+ processed.insert(rindex);
+ Node nextTerm = d_terms[rindex];
+ // immediately check if is satisfied by the current model using the
+ // evaluator, if so, don't conjoin the term.
+ Node newTermEval;
+ if (!currModel.empty())
+ {
+ Node nextTermSk = convertToSkolem(nextTerm);
+ newTermEval = evaluate(nextTermSk, d_skolems, currModel);
+ }
+ if (newTermEval == d_true)
+ {
+ Trace("sygus-qgen-check-debug")
+ << "...already satisfied " << convertToSkolem(nextTerm)
+ << " for model " << d_skolems << " " << currModel << std::endl;
+ addSuccess = false;
+ }
+ else
+ {
+ Trace("sygus-qgen-check-debug")
+ << "...not satisfied " << convertToSkolem(nextTerm) << " for model "
+ << d_skolems << " " << currModel << std::endl;
+ activeTerms.push_back(nextTerm);
+ addSuccess = !d_cores.hasSubset(activeTerms);
+ if (!addSuccess)
+ {
+ Trace("sygus-qgen-check-debug")
+ << "...already has unsat core " << nextTerm << std::endl;
+ activeTerms.pop_back();
+ }
+ }
+ }
+
+ return true;
+}
+
+Result QueryGeneratorUnsat::checkCurrent(const std::vector<Node>& activeTerms,
+ std::ostream& out,
+ std::vector<Node>& currModel)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Node qy = nm->mkAnd(activeTerms);
+ Trace("sygus-qgen-check") << "Check: " << qy << std::endl;
+ out << "(query " << qy << ")" << std::endl;
+ std::unique_ptr<SolverEngine> queryChecker;
+ initializeChecker(queryChecker, qy, d_subOptions, logicInfo());
+ Result r = queryChecker->checkSat();
+ Trace("sygus-qgen-check") << "..finished check got " << r << std::endl;
+ if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+ {
+ // if unsat, get the unsat core
+ std::vector<Node> unsatCore;
+ getUnsatCoreFromSubsolver(*queryChecker.get(), unsatCore);
+ Assert(!unsatCore.empty());
+ Trace("sygus-qgen-check") << "...unsat core: " << unsatCore << std::endl;
+ d_cores.add(d_false, unsatCore);
+ }
+ else if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+ {
+ getModelFromSubsolver(*queryChecker.get(), d_skolems, currModel);
+ Trace("sygus-qgen-check") << "...model: " << currModel << std::endl;
+ }
+ return r;
+}
+
+size_t QueryGeneratorUnsat::getNextRandomIndex(
+ const std::unordered_set<size_t>& processed) const
+{
+ Assert(!d_terms.empty());
+ Assert(processed.size() < d_terms.size());
+ size_t rindex = Random::getRandom().pick(0, d_terms.size() - 1);
+ while (processed.find(rindex) != processed.end())
+ {
+ rindex++;
+ if (rindex == d_terms.size())
+ {
+ rindex = 0;
+ }
+ }
+ return rindex;
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * A class for mining interesting unsat queries from a stream of generated
+ * expressions.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__QUANTIFIERS__QUERY_GENERATOR_UNSAT_H
+#define CVC5__THEORY__QUANTIFIERS__QUERY_GENERATOR_UNSAT_H
+
+#include <map>
+#include <unordered_set>
+
+#include "expr/node.h"
+#include "expr/variadic_trie.h"
+#include "options/options.h"
+#include "theory/quantifiers/expr_miner.h"
+#include "theory/quantifiers/lazy_trie.h"
+#include "theory/quantifiers/sygus_sampler.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * QueryGeneratorUnsat
+ *
+ * A module for generating interesting unsatisfiable benchmarks using SyGuS
+ * enumeration. At a high level, this is based on conjoining predicates that
+ * refine models and avoid previously encountered unsat cores.
+ */
+class QueryGeneratorUnsat : public ExprMiner
+{
+ public:
+ QueryGeneratorUnsat(Env& env);
+ ~QueryGeneratorUnsat() {}
+ /** initialize */
+ void initialize(const std::vector<Node>& vars,
+ SygusSampler* ss = nullptr) override;
+ /**
+ * Add term to this module. This may trigger the printing and/or checking of
+ * new queries.
+ */
+ bool addTerm(Node n, std::ostream& out) override;
+
+ private:
+ /**
+ * Check current query, given by conjunction activeTerms. The generated
+ * query is printed on out. If this is UNSAT, we add its unsat core to
+ * d_cores. If it is satisfiable, we add its model to currModel for
+ * its free variables (which are ExprMiner::d_skolems).
+ */
+ Result checkCurrent(const std::vector<Node>& activeTerms,
+ std::ostream& out,
+ std::vector<Node>& currModel);
+ /**
+ * Get next random index, which returns a random index [0, d_terms.size()-1]
+ * that is not already in processed.
+ */
+ size_t getNextRandomIndex(const std::unordered_set<size_t>& processed) const;
+ /** Constant nodes */
+ Node d_true;
+ Node d_false;
+ /** cache of all terms registered to this generator */
+ std::vector<Node> d_terms;
+ /** total number of queries generated by this class */
+ size_t d_queryCount;
+ /** containing the unsat cores */
+ VariadicTrie d_cores;
+ /** The options for subsolver calls */
+ Options d_subOptions;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace cvc5
+
+#endif /* CVC5__THEORY__QUANTIFIERS___H */
bool is_unique_term = true;
if (status != 0
- && (options::sygusRewSynth() || options::sygusQueryGen()
+ && (options::sygusRewSynth()
+ || options().quantifiers.sygusQueryGen
+ != options::SygusQueryGenMode::NONE
|| options::sygusFilterSolMode()
!= options::SygusFilterSolMode::NONE))
{
ExpressionMinerManager* emm = d_exprm[prog].get();
emm->initializeSygus(
d_tds, d_candidates[i], options::sygusSamples(), true);
- if (options::sygusRewSynth())
- {
- emm->enableRewriteRuleSynth();
- }
- if (options::sygusQueryGen())
- {
- emm->enableQueryGeneration(options::sygusQueryGenThresh());
- }
- if (options::sygusFilterSolMode()
- != options::SygusFilterSolMode::NONE)
- {
- if (options::sygusFilterSolMode()
- == options::SygusFilterSolMode::STRONG)
- {
- emm->enableFilterStrongSolutions();
- }
- else if (options::sygusFilterSolMode()
- == options::SygusFilterSolMode::WEAK)
- {
- emm->enableFilterWeakSolutions();
- }
- }
+ emm->initializeMinersForOptions();
its = d_exprm.find(prog);
}
bool rew_print = false;
regress2/sygus/pbe_bvurem.sy
regress2/sygus/process-10-vars-2fun.sy
regress2/sygus/process-arg-invariance.sy
+ regress2/sygus/qgu-bools.sy
regress2/sygus/real-grammar-neg.sy
regress2/sygus/sets-fun-test.sy
regress2/sygus/sumn_recur_synth.sy
--- /dev/null
+; COMMAND-LINE: --sygus-query-gen=unsat --sygus-abort-size=2
+; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun|\(query)'
+; EXIT: 1
+(set-logic ALL)
+(synth-fun P ((a Bool) (b Bool) (c Bool)) Bool
+((Start Bool))
+(
+(Start Bool (
+a
+b
+c
+(not Start)
+(= Start Start)
+(or Start Start)
+(ite Start Start Start)
+))
+))
+
+
+(check-synth)
projects / cvc5.git / commitdiff