diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-27 14:12:17 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-06-27 14:12:17 -0500 |
commit | d6c7967cfc7a9f8530f0de50f12f99bfc5f93da7 (patch) | |
tree | 2741c23c2cc42c065dc2aa573e0983e8f10823c1 /src/preprocessing | |
parent | a236ade3242599d4916fd9ee676c2c68c7c004b1 (diff) |
Synthesize candidate-rewrites from standard inputs (#1918)
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/synth_rew_rules.cpp | 159 | ||||
-rw-r--r-- | src/preprocessing/passes/synth_rew_rules.h | 48 |
2 files changed, 207 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 diff --git a/src/preprocessing/passes/synth_rew_rules.h b/src/preprocessing/passes/synth_rew_rules.h new file mode 100644 index 000000000..cf0b491fb --- /dev/null +++ b/src/preprocessing/passes/synth_rew_rules.h @@ -0,0 +1,48 @@ +/********************* */ +/*! \file synth_rew_rules.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 technique for synthesizing candidate rewrites of the form t1 = t2, + ** where t1 and t2 are subterms of the input. + **/ + +#ifndef __CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H +#define __CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/** + * This class computes candidate rewrite rules of the form t1 = t2, where + * t1 and t2 are subterms of assertionsToPreprocess. It prints + * "candidate-rewrite" messages on the output stream of options. + * + * In contrast to other preprocessing passes, this pass does not modify + * the set of assertions. + */ +class SynthRewRulesPass : public PreprocessingPass +{ + public: + SynthRewRulesPass(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H */ |