1 /********************* */
2 /*! \file pseudo_boolean_processor.h
4 ** Top contributors (to current version):
5 ** Tim King, Andres Noetzli
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "cvc4_private.h"
20 #ifndef CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
21 #define CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
23 #include <unordered_set>
26 #include "context/cdhashmap.h"
27 #include "context/cdo.h"
28 #include "context/context.h"
29 #include "expr/node.h"
30 #include "preprocessing/preprocessing_pass.h"
31 #include "preprocessing/preprocessing_pass_context.h"
32 #include "theory/substitutions.h"
33 #include "util/maybe.h"
34 #include "util/rational.h"
37 namespace preprocessing
{
40 class PseudoBooleanProcessor
: public PreprocessingPass
43 PseudoBooleanProcessor(PreprocessingPassContext
* preprocContext
);
46 PreprocessingPassResult
applyInternal(
47 AssertionPipeline
* assertionsToPreprocess
) override
;
50 /** Assumes that the assertions have been rewritten. */
51 void learn(const std::vector
<Node
>& assertions
);
53 /** Assumes that the assertions have been rewritten. */
54 void applyReplacements(AssertionPipeline
* assertionsToPreprocess
);
56 bool likelyToHelp() const;
58 bool isPseudoBoolean(Node v
) const;
60 // Adds the fact the that integert typed variable v
61 // must be >= 0 to the context.
62 // This is explained by the explanation exp.
63 // exp cannot be null.
64 void addGeqZero(Node v
, Node exp
);
66 // Adds the fact the that integert typed variable v
67 // must be <= 1 to the context.
68 // This is explained by the explanation exp.
69 // exp cannot be null.
70 void addLeqOne(Node v
, Node exp
);
72 static inline bool isIntVar(Node v
)
74 return v
.isVar() && v
.getType().isInteger();
79 /** Assumes that the assertion has been rewritten. */
80 void learn(Node assertion
);
82 /** Rewrites a node */
83 Node
applyReplacements(Node pre
);
85 void learnInternal(Node assertion
, bool negated
, Node orig
);
86 void learnRewrittenGeq(Node assertion
, bool negated
, Node orig
);
88 void addSub(Node from
, Node to
);
89 void learnGeqSub(Node geq
);
91 static Node
mkGeqOne(Node v
);
93 // x -> <geqZero, leqOne>
94 typedef context::CDHashMap
<Node
, std::pair
<Node
, Node
>, NodeHashFunction
>
96 CDNode2PairMap d_pbBounds
;
97 theory::SubstitutionMap d_subCache
;
99 typedef std::unordered_set
<Node
, NodeHashFunction
> NodeSet
;
100 NodeSet d_learningCache
;
102 context::CDO
<unsigned> d_pbs
;
104 // decompose into \sum pos >= neg + off
105 Maybe
<Rational
> d_off
;
106 std::vector
<Node
> d_pos
;
107 std::vector
<Node
> d_neg
;
109 /** Returns true if successful. */
110 bool decomposeAssertion(Node assertion
, bool negated
);
113 } // namespace passes
114 } // namespace preprocessing
117 #endif // CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H