dReal4
nnfizer.h
1 #pragma once
2 #include "dreal/symbolic/symbolic.h"
3 
4 namespace dreal {
5 
6 /// A class implementing NNF (Negation Normal Form) conversion. See
7 /// https://en.wikipedia.org/wiki/Negation_normal_form for more
8 /// information on NNF. When `push_negation_into_relationals` is true, it pushed
9 /// negations into relational formulas by flipping relational
10 /// operators. For example, `¬(x >= 10)` is transformed into `(x <
11 /// 10)`.
12 class Nnfizer {
13  public:
14  /// Converts @p f into an equivalent formula @c f' in NNF.
15  Formula Convert(const Formula& f,
16  bool push_negation_into_relationals = false) const;
17 
18  private:
19  // Converts @p f into an equivalent formula @c f' in NNF. The parameter @p
20  // polarity is to indicate whether it processes @c f (if @p polarity is
21  // true) or @c ¬f (if @p polarity is false).
22  Formula Visit(const Formula& f, bool polarity,
23  bool push_negation_into_relationals) const;
24 
25  Formula VisitFalse(const Formula& f, bool polarity,
26  bool push_negation_into_relationals) const;
27  Formula VisitTrue(const Formula& f, bool polarity,
28  bool push_negation_into_relationals) const;
29  Formula VisitVariable(const Formula& f, bool polarity,
30  bool push_negation_into_relationals) const;
31  Formula VisitEqualTo(const Formula& f, bool polarity,
32  bool push_negation_into_relationals) const;
33  Formula VisitNotEqualTo(const Formula& f, bool polarity,
34  bool push_negation_into_relationals) const;
35  Formula VisitGreaterThan(const Formula& f, bool polarity,
36  bool push_negation_into_relationals) const;
37  Formula VisitGreaterThanOrEqualTo(const Formula& f, bool polarity,
38  bool push_negation_into_relationals) const;
39  Formula VisitLessThan(const Formula& f, bool polarity,
40  bool push_negation_into_relationals) const;
41  Formula VisitLessThanOrEqualTo(const Formula& f, bool polarity,
42  bool push_negation_into_relationals) const;
43  Formula VisitConjunction(const Formula& f, bool polarity,
44  bool push_negation_into_relationals) const;
45  Formula VisitDisjunction(const Formula& f, bool polarity,
46  bool push_negation_into_relationals) const;
47  Formula VisitNegation(const Formula& f, bool polarity,
48  bool push_negation_into_relationals) const;
49  Formula VisitForall(const Formula& f, bool polarity,
50  bool push_negation_into_relationals) const;
51 
52  // Makes VisitFormula a friend of this class so that it can use private
53  // methods.
54  friend Formula drake::symbolic::VisitFormula<Formula>(const Nnfizer*,
55  const Formula&,
56  const bool&,
57  const bool&);
58 };
59 } // namespace dreal
dreal::Nnfizer::Convert
Formula Convert(const Formula &f, bool push_negation_into_relationals=false) const
Converts f into an equivalent formula f&#39; in NNF.
Definition: nnfizer.cc:9
dreal
Sum type of symbolic::Expression and symbolic::Formula.
Definition: api.cc:9
dreal::Nnfizer
A class implementing NNF (Negation Normal Form) conversion.
Definition: nnfizer.h:12
symbolic.h
This is the header file that we consolidate Drake&#39;s symbolic classes and expose them inside of dreal ...
dreal::drake::symbolic::Formula
Represents a symbolic form of a first-order logic formula.
Definition: symbolic_formula.h:101