de/d55/NewGBPPModule_8h_source.html

 #pragma once


 #include "NewGBPPSettings.h"

 #include <smtrat-solver/PModule.h>


 namespace smtrat {

 template<typename Settings>

 class NewGBPPModule : public PModule {


 public:

     typedef Settings SettingsType;

     NewGBPPModule(const ModuleInput* _formula, Conditionals& _conditionals, Manager* _manager = nullptr);

     ~NewGBPPModule();

     void updateModel() const { mModel.clear(); };

     Answer checkCore();

 };

 } // namespace smtrat

NewGBPPSettings.h

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::Module::mModel
Model mModel
Stores the assignment of the current satisfiable result, if existent.
Definition: Module.h:199

smtrat::NewGBPPModule
Definition: NewGBPPModule.h:8

smtrat::NewGBPPModule::updateModel
void updateModel() const
Updates the model, if the solver has detected the consistency of the received formula,...
Definition: NewGBPPModule.h:14

smtrat::NewGBPPModule::checkCore
Answer checkCore()
Checks the received formula for consistency.

smtrat::NewGBPPModule::~NewGBPPModule
~NewGBPPModule()

smtrat::NewGBPPModule::NewGBPPModule
NewGBPPModule(const ModuleInput *_formula, Conditionals &_conditionals, Manager *_manager=nullptr)

smtrat::NewGBPPModule::SettingsType
Settings SettingsType
Definition: NewGBPPModule.h:11

smtrat::PModule
Definition: PModule.h:19

smtrat
Class to create the formulas for axioms.
Definition: handle_options.h:10

smtrat::Settings
const settings::Settings & Settings()
Definition: Settings.h:96

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