theory/quantifiers/anti_skolem.h \
theory/quantifiers/bv_inverter.cpp \
theory/quantifiers/bv_inverter.h \
+ theory/quantifiers/candidate_rewrite_database.cpp \
+ theory/quantifiers/candidate_rewrite_database.h \
theory/quantifiers/cegqi/ceg_instantiator.cpp \
theory/quantifiers/cegqi/ceg_instantiator.h \
theory/quantifiers/cegqi/ceg_t_instantiator.cpp \
--- /dev/null
+/********************* */
+/*! \file candidate_rewrite_database.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 candidate_rewrite_database
+ **/
+
+#include "theory/quantifiers/candidate_rewrite_database.h"
+
+#include "options/base_options.h"
+#include "options/quantifiers_options.h"
+#include "printer/printer.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
+
+using namespace std;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+CandidateRewriteDatabase::CandidateRewriteDatabase() : d_qe(nullptr) {}
+void CandidateRewriteDatabase::initialize(QuantifiersEngine* qe,
+ Node f,
+ unsigned nsamples,
+ bool useSygusType)
+{
+ d_qe = qe;
+ d_candidate = f;
+ d_sampler.initializeSygusExt(d_qe, f, nsamples, useSygusType);
+}
+
+bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out)
+{
+ bool is_unique_term = true;
+ TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
+ Node eq_sol = d_sampler.registerTerm(sol);
+ // eq_sol is a candidate solution that is equivalent to sol
+ if (eq_sol != sol)
+ {
+ CegInstantiation* cei = d_qe->getCegInstantiation();
+ is_unique_term = false;
+ // if eq_sol is null, then we have an uninteresting candidate rewrite,
+ // e.g. one that is alpha-equivalent to another.
+ bool success = true;
+ if (!eq_sol.isNull())
+ {
+ ExtendedRewriter* er = sygusDb->getExtRewriter();
+ Node solb = sygusDb->sygusToBuiltin(sol);
+ Node solbr = er->extendedRewrite(solb);
+ Node eq_solb = sygusDb->sygusToBuiltin(eq_sol);
+ Node eq_solr = er->extendedRewrite(eq_solb);
+ bool verified = false;
+ Trace("rr-check") << "Check candidate rewrite..." << std::endl;
+ // verify it if applicable
+ if (options::sygusRewSynthCheck())
+ {
+ // Notice we don't set produce-models. rrChecker takes the same
+ // options as the SmtEngine we belong to, where we ensure that
+ // produce-models is set.
+ NodeManager* nm = NodeManager::currentNM();
+ SmtEngine rrChecker(nm->toExprManager());
+ rrChecker.setLogic(smt::currentSmtEngine()->getLogicInfo());
+ Node crr = solbr.eqNode(eq_solr).negate();
+ Trace("rr-check") << "Check candidate rewrite : " << crr << std::endl;
+ // quantify over the free variables in crr
+ std::vector<Node> fvs;
+ TermUtil::computeVarContains(crr, fvs);
+ std::map<Node, unsigned> fv_index;
+ std::vector<Node> sks;
+ if (!fvs.empty())
+ {
+ // map to skolems
+ for (unsigned i = 0, size = fvs.size(); i < size; i++)
+ {
+ Node v = fvs[i];
+ fv_index[v] = i;
+ std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v);
+ if (itf == d_fv_to_skolem.end())
+ {
+ Node sk = nm->mkSkolem("rrck", v.getType());
+ d_fv_to_skolem[v] = sk;
+ sks.push_back(sk);
+ }
+ else
+ {
+ sks.push_back(itf->second);
+ }
+ }
+ crr = crr.substitute(fvs.begin(), fvs.end(), sks.begin(), sks.end());
+ }
+ rrChecker.assertFormula(crr.toExpr());
+ Result r = rrChecker.checkSat();
+ Trace("rr-check") << "...result : " << r << std::endl;
+ if (r.asSatisfiabilityResult().isSat())
+ {
+ Trace("rr-check") << "...rewrite does not hold for: " << std::endl;
+ success = false;
+ is_unique_term = true;
+ std::vector<Node> vars;
+ d_sampler.getVariables(vars);
+ std::vector<Node> pt;
+ for (const Node& v : vars)
+ {
+ std::map<Node, unsigned>::iterator itf = fv_index.find(v);
+ Node val;
+ if (itf == fv_index.end())
+ {
+ // not in conjecture, can use arbitrary value
+ val = v.getType().mkGroundTerm();
+ }
+ else
+ {
+ // get the model value of its skolem
+ Node sk = sks[itf->second];
+ val = Node::fromExpr(rrChecker.getValue(sk.toExpr()));
+ Trace("rr-check") << " " << v << " -> " << val << std::endl;
+ }
+ pt.push_back(val);
+ }
+ d_sampler.addSamplePoint(pt);
+ // add the solution again
+ // by construction of the above point, we should be unique now
+ Node eq_sol_new = d_sampler.registerTerm(sol);
+ Assert(eq_sol_new == sol);
+ }
+ else
+ {
+ verified = !r.asSatisfiabilityResult().isUnknown();
+ }
+ }
+ else
+ {
+ // just insist that constants are not relevant pairs
+ success = !solb.isConst() || !eq_solb.isConst();
+ }
+ if (success)
+ {
+ // register this as a relevant pair (helps filtering)
+ d_sampler.registerRelevantPair(sol, eq_sol);
+ // The analog of terms sol and eq_sol are equivalent under
+ // sample points but do not rewrite to the same term. Hence,
+ // this indicates a candidate rewrite.
+ Printer* p = Printer::getPrinter(options::outputLanguage());
+ out << "(" << (verified ? "" : "candidate-") << "rewrite ";
+ p->toStreamSygus(out, sol);
+ out << " ";
+ p->toStreamSygus(out, eq_sol);
+ out << ")" << std::endl;
+ ++(cei->d_statistics.d_candidate_rewrites_print);
+ // debugging information
+ if (Trace.isOn("sygus-rr-debug"))
+ {
+ Trace("sygus-rr-debug") << "; candidate #1 ext-rewrites to: " << solbr
+ << std::endl;
+ Trace("sygus-rr-debug")
+ << "; candidate #2 ext-rewrites to: " << eq_solr << std::endl;
+ }
+ if (options::sygusRewSynthAccel())
+ {
+ // Add a symmetry breaking clause that excludes the larger
+ // of sol and eq_sol. This effectively states that we no longer
+ // wish to enumerate any term that contains sol (resp. eq_sol)
+ // as a subterm.
+ Node exc_sol = sol;
+ unsigned sz = sygusDb->getSygusTermSize(sol);
+ unsigned eqsz = sygusDb->getSygusTermSize(eq_sol);
+ if (eqsz > sz)
+ {
+ sz = eqsz;
+ exc_sol = eq_sol;
+ }
+ TypeNode ptn = d_candidate.getType();
+ Node x = sygusDb->getFreeVar(ptn, 0);
+ Node lem =
+ sygusDb->getExplain()->getExplanationForEquality(x, exc_sol);
+ lem = lem.negate();
+ Trace("sygus-rr-sb") << "Symmetry breaking lemma : " << lem
+ << std::endl;
+ sygusDb->registerSymBreakLemma(d_candidate, lem, ptn, sz);
+ }
+ }
+ }
+ // We count this as a rewrite if we did not explicitly rule it out.
+ // Notice that when --sygus-rr-synth-check is enabled,
+ // statistics on number of candidate rewrite rules is
+ // an accurate count of (#enumerated_terms-#unique_terms) only if
+ // the option sygus-rr-synth-filter-order is disabled. The reason
+ // is that the sygus sampler may reason that a candidate rewrite
+ // rule is not useful since its variables are unordered, whereby
+ // it discards it as a redundant candidate rewrite rule before
+ // checking its correctness.
+ if (success)
+ {
+ ++(cei->d_statistics.d_candidate_rewrites);
+ }
+ }
+ return is_unique_term;
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file candidate_rewrite_database.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 candidate_rewrite_database
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
+#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
+
+#include <map>
+#include "theory/quantifiers/sygus_sampler.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** CandidateRewriteDatabase
+ *
+ * This maintains the necessary data structures for generating a database
+ * of candidate rewrite rules (see Reynolds et al "Rewrites for SMT Solvers
+ * Using Syntax-Guided Enumeration" SMT 2018). The primary responsibilities
+ * of this class are to perform the "equivalence checking" and "congruence
+ * and matching filtering" in Figure 1. The equivalence checking is done
+ * through a combination of the sygus sampler object owned by this class
+ * and the calls made to copies of the SmtEngine in ::addTerm. The rewrite
+ * rule filtering (based on congruence, matching, variable ordering) is also
+ * managed by the sygus sampler object.
+ */
+class CandidateRewriteDatabase
+{
+ public:
+ CandidateRewriteDatabase();
+ ~CandidateRewriteDatabase() {}
+ /** Initialize this class
+ *
+ * qe : pointer to quantifiers engine,
+ * f : a term of some SyGuS datatype type whose values we will be
+ * testing under the free variables in the grammar of f. This is the
+ * "candidate variable" CegConjecture::d_candidates,
+ * nsamples : number of sample points this class will test,
+ * useSygusType : whether we will register terms with this sampler that have
+ * the same type as f. If this flag is false, then we will be registering
+ * terms of the analog of the type of f, that is, the builtin type that
+ * f's type encodes in the deep embedding.
+ *
+ * These arguments are used to initialize the sygus sampler class.
+ */
+ void initialize(QuantifiersEngine* qe,
+ Node f,
+ unsigned nsamples,
+ bool useSygusType);
+ /** add term
+ *
+ * Notifies this class that the solution sol was enumerated. This may
+ * cause a candidate-rewrite to be printed on the output stream out.
+ */
+ bool addTerm(Node sol, std::ostream& out);
+
+ private:
+ /** reference to quantifier engine */
+ QuantifiersEngine* d_qe;
+ /** the function-to-synthesize we are testing */
+ Node d_candidate;
+ /** sygus sampler objects for each program variable
+ *
+ * This is used for the sygusRewSynth() option to synthesize new candidate
+ * rewrite rules.
+ */
+ SygusSamplerExt d_sampler;
+ /**
+ * Cache of skolems for each free variable that appears in a synthesis check
+ * (for --sygus-rr-synth-check).
+ */
+ std::map<Node, Node> d_fv_to_skolem;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */
#include "options/quantifiers_options.h"
#include "printer/printer.h"
#include "prop/prop_engine.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "smt/smt_statistics_registry.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quantifiers_attributes.h"
if (status != 0 && options::sygusRewSynth())
{
- TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
- std::map<Node, SygusSamplerExt>::iterator its = d_sampler.find(prog);
- if (its == d_sampler.end())
+ std::map<Node, CandidateRewriteDatabase>::iterator its =
+ d_crrdb.find(prog);
+ if (its == d_crrdb.end())
{
- d_sampler[prog].initializeSygusExt(
- d_qe, prog, options::sygusSamples(), true);
- its = d_sampler.find(prog);
- }
- Node eq_sol = its->second.registerTerm(sol);
- // eq_sol is a candidate solution that is equivalent to sol
- if (eq_sol != sol)
- {
- is_unique_term = false;
- // if eq_sol is null, then we have an uninteresting candidate rewrite,
- // e.g. one that is alpha-equivalent to another.
- bool success = true;
- if (!eq_sol.isNull())
- {
- ExtendedRewriter* er = sygusDb->getExtRewriter();
- Node solb = sygusDb->sygusToBuiltin(sol);
- Node solbr = er->extendedRewrite(solb);
- Node eq_solb = sygusDb->sygusToBuiltin(eq_sol);
- Node eq_solr = er->extendedRewrite(eq_solb);
- bool verified = false;
- Trace("rr-check") << "Check candidate rewrite..." << std::endl;
- // verify it if applicable
- if (options::sygusRewSynthCheck())
- {
- // Notice we don't set produce-models. rrChecker takes the same
- // options as the SmtEngine we belong to, where we ensure that
- // produce-models is set.
- NodeManager* nm = NodeManager::currentNM();
- SmtEngine rrChecker(nm->toExprManager());
- rrChecker.setLogic(smt::currentSmtEngine()->getLogicInfo());
- Node crr = solbr.eqNode(eq_solr).negate();
- Trace("rr-check") << "Check candidate rewrite : " << crr
- << std::endl;
- // quantify over the free variables in crr
- std::vector<Node> fvs;
- TermUtil::computeVarContains(crr, fvs);
- std::map<Node, unsigned> fv_index;
- std::vector<Node> sks;
- if (!fvs.empty())
- {
- // map to skolems
- for (unsigned i = 0, size = fvs.size(); i < size; i++)
- {
- Node v = fvs[i];
- fv_index[v] = i;
- std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v);
- if (itf == d_fv_to_skolem.end())
- {
- Node sk = nm->mkSkolem("rrck", v.getType());
- d_fv_to_skolem[v] = sk;
- sks.push_back(sk);
- }
- else
- {
- sks.push_back(itf->second);
- }
- }
- crr = crr.substitute(
- fvs.begin(), fvs.end(), sks.begin(), sks.end());
- }
- rrChecker.assertFormula(crr.toExpr());
- Result r = rrChecker.checkSat();
- Trace("rr-check") << "...result : " << r << std::endl;
- if (r.asSatisfiabilityResult().isSat())
- {
- Trace("rr-check")
- << "...rewrite does not hold for: " << std::endl;
- success = false;
- is_unique_term = true;
- std::vector<Node> vars;
- d_sampler[prog].getVariables(vars);
- std::vector<Node> pt;
- for (const Node& v : vars)
- {
- std::map<Node, unsigned>::iterator itf = fv_index.find(v);
- Node val;
- if (itf == fv_index.end())
- {
- // not in conjecture, can use arbitrary value
- val = v.getType().mkGroundTerm();
- }
- else
- {
- // get the model value of its skolem
- Node sk = sks[itf->second];
- val = Node::fromExpr(rrChecker.getValue(sk.toExpr()));
- Trace("rr-check") << " " << v << " -> " << val
- << std::endl;
- }
- pt.push_back(val);
- }
- d_sampler[prog].addSamplePoint(pt);
- // add the solution again
- // by construction of the above point, we should be unique now
- Node eq_sol_new = its->second.registerTerm(sol);
- Assert(eq_sol_new == sol);
- }
- else
- {
- verified = !r.asSatisfiabilityResult().isUnknown();
- }
- }
- else
- {
- // just insist that constants are not relevant pairs
- success = !solb.isConst() || !eq_solb.isConst();
- }
- if (success)
- {
- // register this as a relevant pair (helps filtering)
- d_sampler[prog].registerRelevantPair(sol, eq_sol);
- // The analog of terms sol and eq_sol are equivalent under
- // sample points but do not rewrite to the same term. Hence,
- // this indicates a candidate rewrite.
- Printer* p = Printer::getPrinter(options::outputLanguage());
- out << "(" << (verified ? "" : "candidate-") << "rewrite ";
- p->toStreamSygus(out, sol);
- out << " ";
- p->toStreamSygus(out, eq_sol);
- out << ")" << std::endl;
- ++(cei->d_statistics.d_candidate_rewrites_print);
- // debugging information
- if (Trace.isOn("sygus-rr-debug"))
- {
- Trace("sygus-rr-debug")
- << "; candidate #1 ext-rewrites to: " << solbr << std::endl;
- Trace("sygus-rr-debug")
- << "; candidate #2 ext-rewrites to: " << eq_solr
- << std::endl;
- }
- if (options::sygusRewSynthAccel())
- {
- // Add a symmetry breaking clause that excludes the larger
- // of sol and eq_sol. This effectively states that we no longer
- // wish to enumerate any term that contains sol (resp. eq_sol)
- // as a subterm.
- Node exc_sol = sol;
- unsigned sz = sygusDb->getSygusTermSize(sol);
- unsigned eqsz = sygusDb->getSygusTermSize(eq_sol);
- if (eqsz > sz)
- {
- sz = eqsz;
- exc_sol = eq_sol;
- }
- TypeNode ptn = prog.getType();
- Node x = sygusDb->getFreeVar(ptn, 0);
- Node lem = sygusDb->getExplain()->getExplanationForEquality(
- x, exc_sol);
- lem = lem.negate();
- Trace("sygus-rr-sb")
- << "Symmetry breaking lemma : " << lem << std::endl;
- sygusDb->registerSymBreakLemma(d_candidates[i], lem, ptn, sz);
- }
- }
- }
- // We count this as a rewrite if we did not explicitly rule it out.
- // Notice that when --sygus-rr-synth-check is enabled,
- // statistics on number of candidate rewrite rules is
- // an accurate count of (#enumerated_terms-#unique_terms) only if
- // the option sygus-rr-synth-filter-order is disabled. The reason
- // is that the sygus sampler may reason that a candidate rewrite
- // rule is not useful since its variables are unordered, whereby
- // it discards it as a redundant candidate rewrite rule before
- // checking its correctness.
- if (success)
- {
- ++(cei->d_statistics.d_candidate_rewrites);
- }
+ d_crrdb[prog].initialize(
+ d_qe, d_candidates[i], options::sygusSamples(), true);
+ its = d_crrdb.find(prog);
}
+ is_unique_term = d_crrdb[prog].addTerm(sol, out);
}
if (is_unique_term)
{
#include <memory>
+#include "theory/quantifiers/candidate_rewrite_database.h"
#include "theory/quantifiers/sygus/ce_guided_single_inv.h"
#include "theory/quantifiers/sygus/cegis.h"
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
#include "theory/quantifiers/sygus/sygus_pbe.h"
#include "theory/quantifiers/sygus/sygus_process_conj.h"
-#include "theory/quantifiers/sygus_sampler.h"
#include "theory/quantifiers_engine.h"
namespace CVC4 {
/** the guard for non-syntax-guided synthesis */
Node d_nsg_guard;
//-------------------------------- end non-syntax guided (deprecated)
- /** sygus sampler objects for each program variable
+ /** candidate rewrite objects for each program variable
*
* This is used for the sygusRewSynth() option to synthesize new candidate
* rewrite rules.
*/
- std::map<Node, SygusSamplerExt> d_sampler;
- /**
- * Cache of skolems for each free variable that appears in a synthesis check
- * (for --sygus-rr-synth-check).
- */
- std::map<Node, Node> d_fv_to_skolem;
+ std::map<Node, CandidateRewriteDatabase> d_crrdb;
};
} /* namespace CVC4::theory::quantifiers */
projects / cvc5.git / commitdiff