diff options
Diffstat (limited to 'src/preprocessing/passes/synth_rew_rules.cpp')
-rw-r--r-- | src/preprocessing/passes/synth_rew_rules.cpp | 159 |
1 files changed, 159 insertions, 0 deletions
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp new file mode 100644 index 000000000..e3e3a548a --- /dev/null +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -0,0 +1,159 @@ +/********************* */ +/*! \file synth_rew_rules.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 A technique for synthesizing candidate rewrites of the form t1 = t2, + ** where t1 and t2 are subterms of the input. + **/ + +#include "preprocessing/passes/synth_rew_rules.h" + +#include "options/base_options.h" +#include "options/quantifiers_options.h" +#include "printer/printer.h" +#include "theory/quantifiers/candidate_rewrite_database.h" + +using namespace std; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +// Attribute for whether we have computed rewrite rules for a given term. +// Notice that this currently must be a global attribute, since if +// we've computed rewrites for a term, we should not compute rewrites for the +// same term in a subcall to another SmtEngine (for instance, when using +// "exact" equivalence checking). +struct SynthRrComputedAttributeId +{ +}; +typedef expr::Attribute<SynthRrComputedAttributeId, bool> + SynthRrComputedAttribute; + +SynthRewRulesPass::SynthRewRulesPass(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "synth-rr"){}; + +PreprocessingPassResult SynthRewRulesPass::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + Trace("synth-rr-pass") << "Synthesize rewrite rules from assertions..." + << std::endl; + std::vector<Node>& assertions = assertionsToPreprocess->ref(); + + // compute the variables we will be sampling + std::vector<Node> vars; + unsigned nsamples = options::sygusSamples(); + + Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); + + // attribute to mark processed terms + SynthRrComputedAttribute srrca; + + // initialize the candidate rewrite + std::unique_ptr<theory::quantifiers::CandidateRewriteDatabaseGen> crdg; + std::unordered_map<TNode, bool, TNodeHashFunction> visited; + std::unordered_map<TNode, bool, TNodeHashFunction>::iterator it; + std::vector<TNode> visit; + // two passes: the first collects the variables, the second registers the + // terms + for (unsigned r = 0; r < 2; r++) + { + visited.clear(); + visit.clear(); + TNode cur; + for (const Node& a : assertions) + { + visit.push_back(a); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + // if already processed, ignore + if (cur.getAttribute(SynthRrComputedAttribute())) + { + Trace("synth-rr-pass-debug") + << "...already processed " << cur << std::endl; + } + else if (it == visited.end()) + { + Trace("synth-rr-pass-debug") << "...preprocess " << cur << std::endl; + visited[cur] = false; + Kind k = cur.getKind(); + bool isQuant = k == kind::FORALL || k == kind::EXISTS + || k == kind::LAMBDA || k == kind::CHOICE; + // we recurse on this node if it is not a quantified formula + if (!isQuant) + { + visit.push_back(cur); + for (const Node& cc : cur) + { + visit.push_back(cc); + } + } + } + else if (!it->second) + { + Trace("synth-rr-pass-debug") << "...postprocess " << cur << std::endl; + // check if all of the children are valid + // this ensures we do not register terms that have e.g. quantified + // formulas as subterms + bool childrenValid = true; + for (const Node& cc : cur) + { + Assert(visited.find(cc) != visited.end()); + if (!visited[cc]) + { + childrenValid = false; + } + } + if (childrenValid) + { + Trace("synth-rr-pass-debug") + << "...children are valid, check rewrites..." << std::endl; + if (r == 0) + { + if (cur.isVar()) + { + vars.push_back(cur); + } + } + else + { + Trace("synth-rr-pass-debug") << "Add term " << cur << std::endl; + // mark as processed + cur.setAttribute(srrca, true); + bool ret = crdg->addTerm(cur, *nodeManagerOptions.getOut()); + Trace("synth-rr-pass-debug") << "...return " << ret << std::endl; + // if we want only rewrites of minimal size terms, we would set + // childrenValid to false if ret is false here. + } + } + visited[cur] = childrenValid; + } + } while (!visit.empty()); + } + if (r == 0) + { + Trace("synth-rr-pass-debug") + << "Initialize with " << nsamples + << " samples and variables : " << vars << std::endl; + crdg = std::unique_ptr<theory::quantifiers::CandidateRewriteDatabaseGen>( + new theory::quantifiers::CandidateRewriteDatabaseGen(vars, nsamples)); + } + } + + Trace("synth-rr-pass") << "...finished " << std::endl; + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 |