diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2018-08-22 21:13:46 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-22 23:13:46 -0500 |
commit | ac7db6796f2255678d3b2e2e87940211f162223e (patch) | |
tree | c5857619f46843e8d77093e5b1f468ff2d340535 /src/preprocessing/passes/global_negate.cpp | |
parent | 83d07f5d7662557f2087136563606872b217511a (diff) |
global-negate preprocessing pass (#2317)
Diffstat (limited to 'src/preprocessing/passes/global_negate.cpp')
-rw-r--r-- | src/preprocessing/passes/global_negate.cpp | 116 |
1 files changed, 116 insertions, 0 deletions
diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp new file mode 100644 index 000000000..ddebf961f --- /dev/null +++ b/src/preprocessing/passes/global_negate.cpp @@ -0,0 +1,116 @@ +/********************* */ +/*! \file global_negate.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 global_negate + **/ + +#include "preprocessing/passes/global_negate.h" +#include <vector> +#include "expr/node.h" +#include "theory/rewriter.h" + +using namespace std; +using namespace CVC4::kind; +using namespace CVC4::theory; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +Node GlobalNegate::simplify(std::vector<Node>& assertions, NodeManager* nm) +{ + Assert(!assertions.empty()); + Trace("cbqi-gn") << "Global negate : " << std::endl; + // collect free variables in all assertions + std::vector<Node> free_vars; + std::vector<TNode> visit; + std::unordered_set<TNode, TNodeHashFunction> visited; + for (const Node& as : assertions) + { + Trace("cbqi-gn") << " " << as << std::endl; + TNode cur = as; + // compute free variables + visit.push_back(cur); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur.isVar() && cur.getKind() != BOUND_VARIABLE) + { + free_vars.push_back(cur); + } + for (const TNode& cn : cur) + { + visit.push_back(cn); + } + } + } while (!visit.empty()); + } + + Node body; + if (assertions.size() == 1) + { + body = assertions[0]; + } + else + { + body = nm->mkNode(AND, assertions); + } + + // do the negation + body = body.negate(); + + if (!free_vars.empty()) + { + std::vector<Node> bvs; + for (const Node& v : free_vars) + { + Node bv = nm->mkBoundVar(v.getType()); + bvs.push_back(bv); + } + + body = body.substitute( + free_vars.begin(), free_vars.end(), bvs.begin(), bvs.end()); + + Node bvl = nm->mkNode(BOUND_VAR_LIST, bvs); + + body = nm->mkNode(FORALL, bvl, body); + } + + Trace("cbqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl; + body = Rewriter::rewrite(body); + Trace("cbqi-gn") << "...got (post-rewrite) : " << body << std::endl; + return body; +} + +GlobalNegate::GlobalNegate(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "global-negate"){}; + +PreprocessingPassResult GlobalNegate::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + NodeManager* nm = NodeManager::currentNM(); + Node simplifiedNode = simplify(assertionsToPreprocess->ref(), nm); + Node trueNode = nm->mkConst(true); + for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) + { + assertionsToPreprocess->replace(i, trueNode); + } + assertionsToPreprocess->push_back(simplifiedNode); + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 |