diff options
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/global_negate.cpp | 116 | ||||
-rw-r--r-- | src/preprocessing/passes/global_negate.h | 52 |
2 files changed, 168 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 diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h new file mode 100644 index 000000000..0330aa10e --- /dev/null +++ b/src/preprocessing/passes/global_negate.h @@ -0,0 +1,52 @@ +/********************* */ +/*! \file global_negate.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 the global_negate preprocessing pass + * Updates a set of assertions to the negation of + * these assertions. In detail, if assertions is: + * F1, ..., Fn + * then we update this vector to: + * forall x1...xm. ~( F1 ^ ... ^ Fn ), true, ..., true + * where x1...xm are the free variables of F1...Fn. + * When this is done, d_globalNegation flag is marked, so that the solver checks + *for unsat instead of sat. +**/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H +#define __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class GlobalNegate : public PreprocessingPass +{ + public: + GlobalNegate(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + Node simplify(std::vector<Node>& assertions, NodeManager* nm); +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */ |