From: Andrew Reynolds Date: Mon, 25 Oct 2021 21:39:02 +0000 (-0500) Subject: Add new method for enumerating unsat queries with SyGuS (#7459) X-Git-Tag: cvc5-1.0.0~978 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cb748679157eb658ce5d1173d8f26957daf8f3df;p=cvc5.git Add new method for enumerating unsat queries with SyGuS (#7459) 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. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5bde94a5d..a2ffc1f34 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -887,6 +887,8 @@ libcvc5_add_sources( 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 diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index f3c89fd74..b15ed49a6 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1448,10 +1448,20 @@ name = "Quantifiers" [[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" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 0688810cd..17f0cd2c9 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1614,7 +1614,7 @@ void SetDefaults::setDefaultsSygus(Options& opts) const 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; diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index fad95612f..b0dd61d33 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -62,10 +62,13 @@ void ExprMiner::initializeChecker(std::unique_ptr& checker, 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 { diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp index e53fd9424..d5fa7fbdf 100644 --- a/src/theory/quantifiers/expr_miner_manager.cpp +++ b/src/theory/quantifiers/expr_miner_manager.cpp @@ -30,10 +30,9 @@ ExpressionMinerManager::ExpressionMinerManager(Env& env) 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) { @@ -69,6 +68,32 @@ void ExpressionMinerManager::initializeSygus(TermDbSygus* tds, 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) @@ -101,18 +126,29 @@ void ExpressionMinerManager::enableQueryGeneration(unsigned deqThresh) return; } d_doQueryGen = true; + options::SygusQueryGenMode mode = options().quantifiers.sygusQueryGen; std::vector 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(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(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() @@ -148,14 +184,23 @@ bool ExpressionMinerManager::addTerm(Node sol, 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 diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h index 43a615c97..9d0352408 100644 --- a/src/theory/quantifiers/expr_miner_manager.h +++ b/src/theory/quantifiers/expr_miner_manager.h @@ -22,6 +22,7 @@ #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" @@ -67,14 +68,8 @@ class ExpressionMinerManager : protected EnvObj 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 @@ -90,6 +85,14 @@ class ExpressionMinerManager : protected EnvObj 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 */ @@ -105,7 +108,9 @@ class ExpressionMinerManager : protected EnvObj /** candidate rewrite database */ CandidateRewriteDatabase d_crd; /** query generator */ - QueryGenerator d_qg; + std::unique_ptr d_qg; + /** query generator */ + std::unique_ptr d_qgu; /** solution filter based on logical strength */ SolutionFilterStrength d_sols; /** sygus sampler object */ diff --git a/src/theory/quantifiers/query_generator_unsat.cpp b/src/theory/quantifiers/query_generator_unsat.cpp new file mode 100644 index 000000000..ae7288080 --- /dev/null +++ b/src/theory/quantifiers/query_generator_unsat.cpp @@ -0,0 +1,178 @@ +/****************************************************************************** + * 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& 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 currModel; + std::unordered_set processed; + std::vector 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& activeTerms, + std::ostream& out, + std::vector& 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 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 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& 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 diff --git a/src/theory/quantifiers/query_generator_unsat.h b/src/theory/quantifiers/query_generator_unsat.h new file mode 100644 index 000000000..d03d8efb9 --- /dev/null +++ b/src/theory/quantifiers/query_generator_unsat.h @@ -0,0 +1,89 @@ +/****************************************************************************** + * 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 +#include + +#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& 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& activeTerms, + std::ostream& out, + std::vector& 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& processed) const; + /** Constant nodes */ + Node d_true; + Node d_false; + /** cache of all terms registered to this generator */ + std::vector 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 */ diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 0119f44aa..805f19b34 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -805,7 +805,9 @@ void SynthConjecture::printSynthSolutionInternal(std::ostream& out) 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)) { @@ -818,28 +820,7 @@ void SynthConjecture::printSynthSolutionInternal(std::ostream& out) 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; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 215f75e97..2cf9554e2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2638,6 +2638,7 @@ set(regress_2_tests 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 diff --git a/test/regress/regress2/sygus/qgu-bools.sy b/test/regress/regress2/sygus/qgu-bools.sy new file mode 100644 index 000000000..35445e927 --- /dev/null +++ b/test/regress/regress2/sygus/qgu-bools.sy @@ -0,0 +1,21 @@ +; 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)