diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-04-19 11:47:38 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-19 11:47:38 -0700 |
commit | 70046d35f2aff41867cbb6490e5bf6d026dc55a1 (patch) | |
tree | a6903beb73a028ea159b07bb5c773386c1e5c5f5 /src/preprocessing/passes/pseudo_boolean_processor.h | |
parent | 4af9af22f728ebb12afe48c587cfe665fc8cb123 (diff) |
Refactor pbRewrites preprocessing pass (#1767)
This commit refactors the pbRewrites preprocessing pass into the new
style. This commit is essentially just a code move and adds a regression
test for the preprocessing pass. It also makes use of the
AssertionPipeline::replace function to do proper dependency tracking.
Diffstat (limited to 'src/preprocessing/passes/pseudo_boolean_processor.h')
-rw-r--r-- | src/preprocessing/passes/pseudo_boolean_processor.h | 117 |
1 files changed, 117 insertions, 0 deletions
diff --git a/src/preprocessing/passes/pseudo_boolean_processor.h b/src/preprocessing/passes/pseudo_boolean_processor.h new file mode 100644 index 000000000..261470c74 --- /dev/null +++ b/src/preprocessing/passes/pseudo_boolean_processor.h @@ -0,0 +1,117 @@ +/********************* */ +/*! \file pseudo_boolean_processor.h + ** \verbatim + ** Top contributors (to current version): + ** Tim King, Paul Meng + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H +#define __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H + +#include <unordered_set> +#include <vector> + +#include "context/cdhashmap.h" +#include "context/cdo.h" +#include "context/context.h" +#include "expr/node.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" +#include "theory/substitutions.h" +#include "util/maybe.h" +#include "util/rational.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class PseudoBooleanProcessor : public PreprocessingPass +{ + public: + PseudoBooleanProcessor(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + /** Assumes that the assertions have been rewritten. */ + void learn(const std::vector<Node>& assertions); + + /** Assumes that the assertions have been rewritten. */ + void applyReplacements(AssertionPipeline* assertionsToPreprocess); + + bool likelyToHelp() const; + + bool isPseudoBoolean(Node v) const; + + // Adds the fact the that integert typed variable v + // must be >= 0 to the context. + // This is explained by the explanation exp. + // exp cannot be null. + void addGeqZero(Node v, Node exp); + + // Adds the fact the that integert typed variable v + // must be <= 1 to the context. + // This is explained by the explanation exp. + // exp cannot be null. + void addLeqOne(Node v, Node exp); + + static inline bool isIntVar(Node v) + { + return v.isVar() && v.getType().isInteger(); + } + + void clear(); + + /** Assumes that the assertion has been rewritten. */ + void learn(Node assertion); + + /** Rewrites a node */ + Node applyReplacements(Node pre); + + void learnInternal(Node assertion, bool negated, Node orig); + void learnRewrittenGeq(Node assertion, bool negated, Node orig); + + void addSub(Node from, Node to); + void learnGeqSub(Node geq); + + static Node mkGeqOne(Node v); + + // x -> <geqZero, leqOne> + typedef context::CDHashMap<Node, std::pair<Node, Node>, NodeHashFunction> + CDNode2PairMap; + CDNode2PairMap d_pbBounds; + theory::SubstitutionMap d_subCache; + + typedef std::unordered_set<Node, NodeHashFunction> NodeSet; + NodeSet d_learningCache; + + context::CDO<unsigned> d_pbs; + + // decompose into \sum pos >= neg + off + Maybe<Rational> d_off; + std::vector<Node> d_pos; + std::vector<Node> d_neg; + + /** Returns true if successful. */ + bool decomposeAssertion(Node assertion, bool negated); +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif // __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H |