From f1a4096e579b101642c5a47eb5c8e90476ccc81a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 17 Oct 2018 22:09:45 -0500 Subject: [PATCH] Sygus query generator (#2465) --- src/CMakeLists.txt | 2 + src/Makefile.am | 2 + src/options/quantifiers_options.toml | 32 ++ src/smt/smt_engine.cpp | 3 +- src/theory/quantifiers/expr_miner_manager.cpp | 40 +- src/theory/quantifiers/expr_miner_manager.h | 7 + src/theory/quantifiers/query_generator.cpp | 416 ++++++++++++++++++ src/theory/quantifiers/query_generator.h | 116 +++++ .../quantifiers/sygus/synth_conjecture.cpp | 6 +- 9 files changed, 621 insertions(+), 3 deletions(-) create mode 100644 src/theory/quantifiers/query_generator.cpp create mode 100644 src/theory/quantifiers/query_generator.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e353d53c5..676943b11 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -512,6 +512,8 @@ libcvc4_add_sources( theory/quantifiers/quantifiers_attributes.h theory/quantifiers/quantifiers_rewriter.cpp theory/quantifiers/quantifiers_rewriter.h + theory/quantifiers/query_generator.cpp + theory/quantifiers/query_generator.h theory/quantifiers/relevant_domain.cpp theory/quantifiers/relevant_domain.h theory/quantifiers/rewrite_engine.cpp diff --git a/src/Makefile.am b/src/Makefile.am index 8c1c0871d..d29dcd172 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -524,6 +524,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/quantifiers_attributes.h \ theory/quantifiers/quantifiers_rewriter.cpp \ theory/quantifiers/quantifiers_rewriter.h \ + theory/quantifiers/query_generator.cpp \ + theory/quantifiers/query_generator.h \ theory/quantifiers/relevant_domain.cpp \ theory/quantifiers/relevant_domain.h \ theory/quantifiers/rewrite_engine.cpp \ diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 07c11d73a..1c2405449 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1363,6 +1363,38 @@ header = "options/quantifiers_options.h" type = "unsigned long" help = "timeout (in milliseconds) for satisfiability checks in expression miners" +[[option]] + name = "sygusQueryGen" + category = "regular" + long = "sygus-query-gen" + type = "bool" + default = "false" + help = "use sygus to enumerate interesting satisfiability queries" + +[[option]] + name = "sygusQueryGenThresh" + category = "regular" + long = "sygus-query-gen-thresh=N" + type = "unsigned" + default = "5" + help = "number of points that we allow to be equal for enumerating satisfiable queries with sygus-query-gen" + +[[option]] + name = "sygusQueryGenCheck" + category = "regular" + long = "sygus-query-gen-check" + type = "bool" + default = "true" + help = "use interesting satisfiability queries to check soundness of CVC4" + +[[option]] + name = "sygusQueryGenDumpFiles" + category = "regular" + long = "sygus-query-gen-dump-files" + type = "bool" + default = "false" + help = "dump external files corresponding to interesting satisfiability queries with sygus-query-gen" + [[option]] name = "sygusExprMinerCheckUseExport" category = "expert" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 38c9e7ee2..196da6b9c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1876,7 +1876,8 @@ void SmtEngine::setDefaults() { options::sygusExtRew.set(false); } } - if (options::sygusRewSynth() || options::sygusRewVerify()) + if (options::sygusRewSynth() || options::sygusRewVerify() + || options::sygusQueryGen()) { // rewrite rule synthesis implies that sygus stream must be true options::sygusStream.set(true); diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp index 8c116781d..010b5a4ab 100644 --- a/src/theory/quantifiers/expr_miner_manager.cpp +++ b/src/theory/quantifiers/expr_miner_manager.cpp @@ -13,6 +13,7 @@ **/ #include "theory/quantifiers/expr_miner_manager.h" +#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { @@ -20,6 +21,7 @@ namespace quantifiers { ExpressionMinerManager::ExpressionMinerManager() : d_doRewSynth(false), + d_doQueryGen(false), d_use_sygus_type(false), d_qe(nullptr), d_tds(nullptr) @@ -32,6 +34,7 @@ void ExpressionMinerManager::initialize(const std::vector& vars, bool unique_type_ids) { d_doRewSynth = false; + d_doQueryGen = false; d_sygus_fun = Node::null(); d_use_sygus_type = false; d_qe = nullptr; @@ -46,6 +49,7 @@ void ExpressionMinerManager::initializeSygus(QuantifiersEngine* qe, bool useSygusType) { d_doRewSynth = false; + d_doQueryGen = false; d_sygus_fun = f; d_use_sygus_type = useSygusType; d_qe = qe; @@ -78,11 +82,45 @@ void ExpressionMinerManager::enableRewriteRuleSynth() d_crd.setSilent(false); } +void ExpressionMinerManager::enableQueryGeneration(unsigned deqThresh) +{ + if (d_doQueryGen) + { + // already enabled + return; + } + d_doQueryGen = true; + std::vector vars; + d_sampler.getVariables(vars); + // must also enable rewrite rule synthesis + if (!d_doRewSynth) + { + // initialize the candidate rewrite database, in silent mode + enableRewriteRuleSynth(); + d_crd.setSilent(true); + } + // initialize the query generator + d_qg.initialize(vars, &d_sampler); + d_qg.setThreshold(deqThresh); +} + bool ExpressionMinerManager::addTerm(Node sol, std::ostream& out, bool& rew_print) { - return d_crd.addTerm(sol, out, rew_print); + bool ret = d_crd.addTerm(sol, out, rew_print); + 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); + } + return ret; } bool ExpressionMinerManager::addTerm(Node sol, std::ostream& out) diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h index 668d04beb..d15b69cb5 100644 --- a/src/theory/quantifiers/expr_miner_manager.h +++ b/src/theory/quantifiers/expr_miner_manager.h @@ -20,6 +20,7 @@ #include "expr/node.h" #include "theory/quantifiers/candidate_rewrite_database.h" #include "theory/quantifiers/extended_rewrite.h" +#include "theory/quantifiers/query_generator.h" #include "theory/quantifiers/sygus_sampler.h" #include "theory/quantifiers_engine.h" @@ -67,6 +68,8 @@ class ExpressionMinerManager bool useSygusType); /** enable rewrite rule synthesis (--sygus-rr-synth) */ void enableRewriteRuleSynth(); + /** enable query generation (--sygus-query-gen) */ + void enableQueryGeneration(unsigned deqThresh); /** add term * * Expression miners may print information on the output stream out, for @@ -84,6 +87,8 @@ class ExpressionMinerManager private: /** whether we are doing rewrite synthesis */ bool d_doRewSynth; + /** whether we are doing query generation */ + bool d_doQueryGen; /** the sygus function passed to initializeSygus, if any */ Node d_sygus_fun; /** whether we are using sygus types */ @@ -94,6 +99,8 @@ class ExpressionMinerManager TermDbSygus* d_tds; /** candidate rewrite database */ CandidateRewriteDatabase d_crd; + /** query generator */ + QueryGenerator d_qg; /** sygus sampler object */ SygusSampler d_sampler; /** extended rewriter object */ diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp new file mode 100644 index 000000000..e62f3513c --- /dev/null +++ b/src/theory/quantifiers/query_generator.cpp @@ -0,0 +1,416 @@ +/********************* */ +/*! \file query_generator.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 Implementation of a class for mining interesting satisfiability + ** queries from a stream of generated expressions. + **/ + +#include "theory/quantifiers/query_generator.h" + +#include +#include "options/quantifiers_options.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "util/random.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +QueryGenerator::QueryGenerator() : d_queryCount(0) {} +void QueryGenerator::initialize(const std::vector& vars, SygusSampler* ss) +{ + Assert(ss != nullptr); + d_queryCount = 0; + ExprMiner::initialize(vars, ss); +} + +void QueryGenerator::setThreshold(unsigned deqThresh) +{ + d_deqThresh = deqThresh; +} + +bool QueryGenerator::addTerm(Node n, std::ostream& out) +{ + Node nn = n.getKind() == NOT ? n[0] : n; + if (d_terms.find(nn) != d_terms.end()) + { + return false; + } + d_terms.insert(nn); + + Trace("sygus-qgen") << "QueryGenerator::addTerm : " << n << std::endl; + unsigned npts = d_sampler->getNumSamplePoints(); + TypeNode tn = n.getType(); + // TODO : as an optimization, use a shared lazy trie? + + // the queries we generate on this round + std::vector queries; + // For each query in the above vector, this stores the indices of the points + // for which that query evaluated to true on. + std::vector> queriesPtTrue; + // the sample point indices for which the above queries are true + std::unordered_set indices; + + // collect predicate queries (if n is Boolean) + if (tn.isBoolean()) + { + std::map> ev_to_pt; + unsigned index = 0; + unsigned threshCount = 0; + while (index < npts && threshCount < 2) + { + Node v = d_sampler->evaluate(nn, index); + ev_to_pt[v].push_back(index); + if (ev_to_pt[v].size() == d_deqThresh + 1) + { + threshCount++; + } + index++; + } + if (threshCount < 2) + { + for (const std::pair>& etp : ev_to_pt) + { + if (etp.second.size() < d_deqThresh) + { + indices.insert(etp.second.begin(), etp.second.end()); + Node qy = nn; + Assert(etp.first.isConst()); + if (!etp.first.getConst()) + { + qy = qy.negate(); + } + queries.push_back(qy); + queriesPtTrue.push_back(etp.second); + } + } + } + } + + // collect equality queries + findQueries(nn, queries, queriesPtTrue); + Assert(queries.size() == queriesPtTrue.size()); + if (queries.empty()) + { + return true; + } + Trace("sygus-qgen-debug") + << "query: Check " << queries.size() << " queries..." << std::endl; + // literal queries + for (unsigned i = 0, nqueries = queries.size(); i < nqueries; i++) + { + Node qy = queries[i]; + std::vector& tIndices = queriesPtTrue[i]; + // we have an interesting query + out << "(query " << qy << ") ; " << tIndices.size() << "/" << npts + << std::endl; + AlwaysAssert(!tIndices.empty()); + checkQuery(qy, tIndices[0]); + // add information + for (unsigned& ti : tIndices) + { + d_ptToQueries[ti].push_back(qy); + d_qysToPoints[qy].push_back(ti); + indices.insert(ti); + } + } + // for each new index, we may have a new conjunctive query + NodeManager* nm = NodeManager::currentNM(); + for (const unsigned& i : indices) + { + std::vector& qsi = d_ptToQueries[i]; + if (qsi.size() > 1) + { + // take two random queries + std::shuffle(qsi.begin(), qsi.end(), Random::getRandom()); + Node qy = nm->mkNode(AND, qsi[0], qsi[1]); + checkQuery(qy, i); + } + } + Trace("sygus-qgen-check") << "...finished." << std::endl; + return true; +} + +void QueryGenerator::checkQuery(Node qy, unsigned spIndex) +{ + // external query + if (options::sygusQueryGenDumpFiles()) + { + // Print the query and the query + its model (commented) to queryN.smt2 + std::vector pt; + d_sampler->getSamplePoint(spIndex, pt); + unsigned nvars = d_vars.size(); + AlwaysAssert(pt.size() == d_vars.size()); + std::stringstream fname; + fname << "query" << d_queryCount << ".smt2"; + std::ofstream fs(fname.str(), std::ofstream::out); + fs << "(set-logic ALL)" << std::endl; + for (unsigned i = 0; i < 2; i++) + { + for (unsigned j = 0; j < nvars; j++) + { + Node x = d_vars[j]; + if (i == 0) + { + fs << "(declare-fun " << x << " () " << x.getType() << ")"; + } + else + { + fs << ";(define-fun " << x << " () " << x.getType() << " " << pt[j] + << ")"; + } + fs << std::endl; + } + } + fs << "(assert " << qy << ")" << std::endl; + fs << "(check-sat)" << std::endl; + fs.close(); + } + + if (options::sygusQueryGenCheck()) + { + Trace("sygus-qgen-check") << " query: check " << qy << "..." << std::endl; + NodeManager* nm = NodeManager::currentNM(); + // make the satisfiability query + bool needExport = false; + ExprManagerMapCollection varMap; + ExprManager em(nm->getOptions()); + std::unique_ptr queryChecker; + initializeChecker(queryChecker, em, varMap, qy, needExport); + Result r = queryChecker->checkSat(); + Trace("sygus-qgen-check") << " query: ...got : " << r << std::endl; + if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + std::stringstream ss; + ss << "--sygus-rr-query-gen detected unsoundness in CVC4 on input " << qy + << "!" << std::endl; + ss << "This query has a model : " << std::endl; + std::vector pt; + d_sampler->getSamplePoint(spIndex, pt); + Assert(pt.size() == d_vars.size()); + for (unsigned i = 0, size = pt.size(); i < size; i++) + { + ss << " " << d_vars[i] << " -> " << pt[i] << std::endl; + } + ss << "but CVC4 answered unsat!" << std::endl; + AlwaysAssert(false, ss.str().c_str()); + } + } + + d_queryCount++; +} + +void QueryGenerator::findQueries( + Node n, + std::vector& queries, + std::vector>& queriesPtTrue) +{ + // At a high level, this method traverses the LazyTrie for the type of n + // and tries to find paths to leafs that contain terms n' such that n = n' + // or n != n' is an interesting query, i.e. satisfied for a small number of + // points. + TypeNode tn = n.getType(); + LazyTrie* lt = &d_qgtTrie[tn]; + // These vectors are the set of indices of sample points for which the current + // node we are considering are { equal, disequal } from n. + std::vector eqIndex[2]; + Trace("sygus-qgen-debug") << "Compute queries for " << n << "...\n"; + + LazyTrieEvaluator* ev = d_sampler; + unsigned ntotal = d_sampler->getNumSamplePoints(); + unsigned index = 0; + bool exact = true; + bool pushEq[2] = {false, false}; + bool pre = true; + // The following parallel vectors describe the state of the locations in the + // trie we are currently visiting. + // Reference to the location in the trie + std::vector visitTr; + // The index of the sample point we are testing + std::vector currIndex; + // Whether the path to this location exactly matches the evaluation of n + std::vector currExact; + // Whether we are adding to the points that are { equal, disequal } by + // traversing to this location. + std::vector pushIndex[2]; + // Whether we are in a pre-traversal for this location. + std::vector preVisit; + visitTr.push_back(lt); + currIndex.push_back(0); + currExact.push_back(true); + pushIndex[0].push_back(false); + pushIndex[1].push_back(false); + preVisit.push_back(true); + do + { + lt = visitTr.back(); + index = currIndex.back(); + exact = currExact.back(); + for (unsigned r = 0; r < 2; r++) + { + pushEq[r] = pushIndex[r].back(); + } + pre = preVisit.back(); + if (!pre) + { + visitTr.pop_back(); + currIndex.pop_back(); + currExact.pop_back(); + preVisit.pop_back(); + // clean up the indices of points that are { equal, disequal } + for (unsigned r = 0; r < 2; r++) + { + if (pushEq[r]) + { + eqIndex[r].pop_back(); + } + pushIndex[r].pop_back(); + } + } + else + { + preVisit[preVisit.size() - 1] = false; + // add to the indices of points that are { equal, disequal } + for (unsigned r = 0; r < 2; r++) + { + if (pushEq[r]) + { + eqIndex[r].push_back(index - 1); + } + } + int eqAllow = d_deqThresh - eqIndex[0].size(); + int deqAllow = d_deqThresh - eqIndex[1].size(); + Trace("sygus-qgen-debug") + << "Find queries " << n << " " << index << "/" << ntotal + << ", deq/eq allow = " << deqAllow << "/" << eqAllow + << ", exact = " << exact << std::endl; + if (index == ntotal) + { + if (exact) + { + // add to the trie + lt->d_lazy_child = n; + } + else + { + Node nAlmostEq = lt->d_lazy_child; + // if made it here, we still should have either a equality or + // a disequality that is allowed. + Assert(deqAllow >= 0 || eqAllow >= 0); + Node query = n.eqNode(nAlmostEq); + std::vector tIndices; + if (eqAllow >= 0) + { + tIndices.insert( + tIndices.end(), eqIndex[0].begin(), eqIndex[0].end()); + } + else if (deqAllow >= 0) + { + query = query.negate(); + tIndices.insert( + tIndices.end(), eqIndex[1].begin(), eqIndex[1].end()); + } + AlwaysAssert(tIndices.size() <= d_deqThresh); + if (!tIndices.empty()) + { + queries.push_back(query); + queriesPtTrue.push_back(tIndices); + } + } + } + else + { + if (!lt->d_lazy_child.isNull()) + { + // if there is a lazy child here, push + Node e_lc = ev->evaluate(lt->d_lazy_child, index); + // store at next level + lt->d_children[e_lc].d_lazy_child = lt->d_lazy_child; + // replace + lt->d_lazy_child = Node::null(); + } + // compute + Node e_this = ev->evaluate(n, index); + + if (deqAllow >= 0) + { + // recursing on disequal points + deqAllow--; + // if there is use continuing + if (deqAllow >= 0 || eqAllow >= 0) + { + for (std::pair& ltc : lt->d_children) + { + if (ltc.first != e_this) + { + visitTr.push_back(<c.second); + currIndex.push_back(index + 1); + currExact.push_back(false); + pushIndex[0].push_back(false); + pushIndex[1].push_back(true); + preVisit.push_back(true); + } + } + } + deqAllow++; + } + bool pushEqNext = false; + if (eqAllow >= 0) + { + // below, we try recursing (if at all) on equal nodes. + eqAllow--; + pushEqNext = true; + } + // if we are on the exact path of n + if (exact) + { + if (lt->d_children.empty()) + { + // if no one has been here before, we are done + lt->d_lazy_child = n; + } + else + { + // otherwise, we recurse on the equal point + visitTr.push_back(&(lt->d_children[e_this])); + currIndex.push_back(index + 1); + currExact.push_back(true); + pushIndex[0].push_back(pushEqNext); + pushIndex[1].push_back(false); + preVisit.push_back(true); + } + } + else if (deqAllow >= 0 || eqAllow >= 0) + { + // recurse on the equal point if it exists + std::map::iterator iteq = lt->d_children.find(e_this); + if (iteq != lt->d_children.end()) + { + visitTr.push_back(&(iteq->second)); + currIndex.push_back(index + 1); + currExact.push_back(false); + pushIndex[0].push_back(pushEqNext); + pushIndex[1].push_back(false); + preVisit.push_back(true); + } + } + } + } + } while (!visitTr.empty()); +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h new file mode 100644 index 000000000..f0b3fa565 --- /dev/null +++ b/src/theory/quantifiers/query_generator.h @@ -0,0 +1,116 @@ +/********************* */ +/*! \file query_generator.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 A class for mining interesting satisfiability queries from a stream + ** of generated expressions. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H +#define __CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_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 { + +/** QueryGenerator + * + * This module is used for finding satisfiable queries that are maximally + * likely to trigger an unsound response in an SMT solver. These queries are + * mined from a stream of enumerated expressions. We judge likelihood of + * triggering unsoundness by the frequency at which the query is satisfied. + * + * In detail, given a stream of expressions t_1, ..., t_{n-1}, upon generating + * term t_n, we consider a query (not) t_n = t_i to be an interesting query + * if it is satisfied by at most D points, where D is a predefined threshold + * given by options::sygusQueryGenThresh(). If t_n has type Bool, we + * additionally consider the case where t_n is satisfied (or not satisfied) by + * fewer than D points. + * + * In addition to generating single literal queries, this module also generates + * conjunctive queries, for instance, by remembering that literals L1 and L2 + * were both satisfied by the same point, and thus L1 ^ L2 is an interesting + * query as well. + */ +class QueryGenerator : public ExprMiner +{ + public: + QueryGenerator(); + ~QueryGenerator() {} + /** 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; + /** + * Set the threshold value. This is the maximal number of sample points that + * each query we generate is allowed to be satisfied by. + */ + void setThreshold(unsigned deqThresh); + + private: + /** cache of all terms registered to this generator */ + std::unordered_set d_terms; + /** the threshold used by this module for maximum number of sat points */ + unsigned d_deqThresh; + /** + * For each type, a lazy trie storing the evaluation of all added terms on + * sample points. + */ + std::map d_qgtTrie; + /** total number of queries generated by this class */ + unsigned d_queryCount; + /** find queries + * + * This function traverses the lazy trie for the type of n, finding equality + * and disequality queries between n and other terms in the trie. The argument + * queries collects the newly generated queries, and the argument + * queriesPtTrue collects the indices of points that each query was satisfied + * by (these indices are the indices of the points in the sampler used by this + * class). + */ + void findQueries(Node n, + std::vector& queries, + std::vector>& queriesPtTrue); + /** + * Maps the index of each sample point to the list of queries that it + * satisfies, and that were generated by the above function. This map is used + * for generating conjunctive queries. + */ + std::map> d_ptToQueries; + /** + * Map from queries to the indices of the points that satisfy them. + */ + std::map> d_qysToPoints; + /** + * Check query qy, which is satisfied by (at least) sample point spIndex, + * using a separate copy of the SMT engine. Throws an exception if qy is + * reported to be unsatisfiable. + */ + void checkQuery(Node qy, unsigned spIndex); +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__QUANTIFIERS___H */ diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 7955d59a8..32342a9ba 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -981,7 +981,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out) bool is_unique_term = true; - if (status != 0 && options::sygusRewSynth()) + if (status != 0 && (options::sygusRewSynth() || options::sygusQueryGen())) { std::map::iterator its = d_exprm.find(prog); @@ -993,6 +993,10 @@ void SynthConjecture::printSynthSolution(std::ostream& out) { d_exprm[prog].enableRewriteRuleSynth(); } + if (options::sygusQueryGen()) + { + d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh()); + } its = d_exprm.find(prog); } bool rew_print = false; -- 2.30.2