GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/pseudo_boolean_processor.h Lines: 3 3 100.0 %
Date: 2021-03-23 Branches: 8 14 57.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file pseudo_boolean_processor.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Andres Noetzli, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "cvc4_private.h"
19
20
#ifndef CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
21
#define CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
22
23
#include <unordered_set>
24
#include <vector>
25
26
#include "context/cdhashmap.h"
27
#include "context/cdo.h"
28
#include "expr/node.h"
29
#include "preprocessing/preprocessing_pass.h"
30
#include "theory/substitutions.h"
31
#include "util/maybe.h"
32
#include "util/rational.h"
33
34
namespace CVC4 {
35
namespace preprocessing {
36
namespace passes {
37
38
17988
class PseudoBooleanProcessor : public PreprocessingPass
39
{
40
 public:
41
  PseudoBooleanProcessor(PreprocessingPassContext* preprocContext);
42
43
 protected:
44
  PreprocessingPassResult applyInternal(
45
      AssertionPipeline* assertionsToPreprocess) override;
46
47
 private:
48
  /** Assumes that the assertions have been rewritten. */
49
  void learn(const std::vector<Node>& assertions);
50
51
  /** Assumes that the assertions have been rewritten. */
52
  void applyReplacements(AssertionPipeline* assertionsToPreprocess);
53
54
  bool likelyToHelp() const;
55
56
  bool isPseudoBoolean(Node v) const;
57
58
  // Adds the fact the that integert typed variable v
59
  //   must be >= 0 to the context.
60
  // This is explained by the explanation exp.
61
  // exp cannot be null.
62
  void addGeqZero(Node v, Node exp);
63
64
  // Adds the fact the that integert typed variable v
65
  //   must be <= 1 to the context.
66
  // This is explained by the explanation exp.
67
  // exp cannot be null.
68
  void addLeqOne(Node v, Node exp);
69
70
802
  static inline bool isIntVar(Node v)
71
  {
72
802
    return v.isVar() && v.getType().isInteger();
73
  }
74
75
  void clear();
76
77
  /** Assumes that the assertion has been rewritten. */
78
  void learn(Node assertion);
79
80
  /** Rewrites a node  */
81
  Node applyReplacements(Node pre);
82
83
  void learnInternal(Node assertion, bool negated, Node orig);
84
  void learnRewrittenGeq(Node assertion, bool negated, Node orig);
85
86
  void addSub(Node from, Node to);
87
  void learnGeqSub(Node geq);
88
89
  static Node mkGeqOne(Node v);
90
91
  // x ->  <geqZero, leqOne>
92
  typedef context::CDHashMap<Node, std::pair<Node, Node>, NodeHashFunction>
93
      CDNode2PairMap;
94
  CDNode2PairMap d_pbBounds;
95
  theory::SubstitutionMap d_subCache;
96
97
  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
98
  NodeSet d_learningCache;
99
100
  context::CDO<unsigned> d_pbs;
101
102
  // decompose into \sum pos >= neg + off
103
  Maybe<Rational> d_off;
104
  std::vector<Node> d_pos;
105
  std::vector<Node> d_neg;
106
107
  /** Returns true if successful. */
108
  bool decomposeAssertion(Node assertion, bool negated);
109
};
110
111
}  // namespace passes
112
}  // namespace preprocessing
113
}  // namespace CVC4
114
115
#endif  // CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H