dlinear  0.0.1
Delta-complete SMT solver for linear programming
Loading...
Searching...
No Matches
Nnfizer.h
1
8#pragma once
9
10#include "dlinear/symbolic/FormulaVisitor.h"
11#include "dlinear/symbolic/symbolic.h"
12#include "dlinear/util/Config.h"
13
14namespace dlinear {
15
24class Nnfizer : public FormulaVisitor<bool, bool> {
25 public:
26 explicit Nnfizer(const Config &config);
33 [[nodiscard]] Formula Process(const Formula &f, bool push_negation_into_relationals = false) const;
34 [[nodiscard]] Formula operator()(const Formula &f, bool push_negation_into_relationals = false) const;
35
36 private:
45 [[nodiscard]] Formula VisitFalse(const Formula &f, bool polarity, bool push_negation_into_relationals) const override;
46 [[nodiscard]] Formula VisitTrue(const Formula &f, bool polarity, bool push_negation_into_relationals) const override;
47 [[nodiscard]] Formula VisitVariable(const Formula &f, bool polarity,
48 bool push_negation_into_relationals) const override;
49 [[nodiscard]] Formula VisitEqualTo(const Formula &f, bool polarity,
50 bool push_negation_into_relationals) const override;
51 [[nodiscard]] Formula VisitNotEqualTo(const Formula &f, bool polarity,
52 bool push_negation_into_relationals) const override;
53 [[nodiscard]] Formula VisitGreaterThan(const Formula &f, bool polarity,
54 bool push_negation_into_relationals) const override;
55 [[nodiscard]] Formula VisitGreaterThanOrEqualTo(const Formula &f, bool polarity,
56 bool push_negation_into_relationals) const override;
57 [[nodiscard]] Formula VisitLessThan(const Formula &f, bool polarity,
58 bool push_negation_into_relationals) const override;
59 [[nodiscard]] Formula VisitLessThanOrEqualTo(const Formula &f, bool polarity,
60 bool push_negation_into_relationals) const override;
61 [[nodiscard]] Formula VisitConjunction(const Formula &f, bool polarity,
62 bool push_negation_into_relationals) const override;
63 [[nodiscard]] Formula VisitDisjunction(const Formula &f, bool polarity,
64 bool push_negation_into_relationals) const override;
65 [[nodiscard]] Formula VisitNegation(const Formula &f, bool polarity,
66 bool push_negation_into_relationals) const override;
67 [[nodiscard]] Formula VisitForall(const Formula &f, bool polarity,
68 bool push_negation_into_relationals) const override;
69};
70} // namespace dlinear
dlinear::Config
Simple dataclass used to store the configuration of the program.
Definition Config.h:38
dlinear::FormulaVisitor
This base class provides all the methods expected to visit the underlying formula and return a modifi...
Definition FormulaVisitor.h:29
dlinear::Nnfizer
Implementation of NNF (Negation Normal Form) conversion.
Definition Nnfizer.h:24
dlinear::Nnfizer::Process
Formula Process(const Formula &f, bool push_negation_into_relationals=false) const
Convert a f into an equivalent formula f' in NNF.
Definition Nnfizer.cpp:17
dlinear::Nnfizer::VisitFalse
Formula VisitFalse(const Formula &f, bool polarity, bool push_negation_into_relationals) const override
Convert f into an equivalent formula f' in NNF.
Definition Nnfizer.cpp:27
dlinear::drake::symbolic::Formula
Represents a symbolic form of a first-order logic formula.
Definition symbolic_formula.h:100
dlinear
Global namespace for the dlinear library.