SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
PNFerModule.h
Go to the documentation of this file.
1 #pragma once
2 
3 #include <smtrat-solver/PModule.h>
4 
5 namespace smtrat {
6 class PNFerModule : public PModule {
7 
8 public:
9  struct SettingsType {
10  static constexpr auto moduleName = "PNFerModule";
11  };
12 
13  PNFerModule(const ModuleInput*, Conditionals&, Manager* const = NULL);
14  ~PNFerModule();
15 
16  /**
17  * Checks the received formula for consistency.
18  * @return SAT, if the received formula is satisfiable;
19  * UNSAT, if the received formula is not satisfiable;
20  * Unknown, otherwise.
21  */
22  Answer checkCore();
23 };
24 
25 } // namespace smtrat
PModule.h
All preprocessing modules shall derive from this module, that is modules, which simplify their receiv...
smtrat::Manager
Base class for solvers.
Definition: Manager.h:34
smtrat::ModuleInput
The input formula a module has to consider for it's satisfiability check.
Definition: ModuleInput.h:131
smtrat::PNFerModule::PNFerModule
PNFerModule(const ModuleInput *, Conditionals &, Manager *const =NULL)
Definition: PNFerModule.cpp:6
smtrat::PNFerModule::checkCore
Answer checkCore()
Checks the received formula for consistency.
Definition: PNFerModule.cpp:12
smtrat
Class to create the formulas for axioms.
Definition: handle_options.h:10
smtrat::Answer
Answer
An enum with the possible answers a Module can give.
Definition: types.h:57
smtrat::Conditionals
std::vector< std::atomic_bool * > Conditionals
A vector of atomic bool pointers.
Definition: types.h:17
smtrat::PNFerModule::SettingsType::moduleName
static constexpr auto moduleName
Definition: PNFerModule.h:10