SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
•All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
IncrementalBacktracking.h
Go to the documentation of this file.
1 #pragma once
2 
3 #include <smtrat-modules/SATModule/SATModule.h>
4 #include <smtrat-modules/NewCoveringModule/NewCoveringModule.h>
5 #include <smtrat-solver/Manager.h>
6 
7 namespace smtrat {
8 class NewCovering_IncrementalBacktracking : public Manager {
9 public:
10  NewCovering_IncrementalBacktracking()
11  : Manager() {
12  setStrategy(
13  addBackend<SATModule<SATSettings1>>(
14  addBackend<NewCoveringModule<NewCoveringSettings1>>()));
15  }
16 };
17 } // namespace smtrat
smtrat::Manager
Base class for solvers.
Definition: Manager.h:34
smtrat::Manager::setStrategy
void setStrategy(const std::initializer_list< BackendLink > &backends)
Definition: Manager.h:385
smtrat::Manager::addBackend
BackendLink addBackend(const std::initializer_list< BackendLink > &backends={})
Definition: Manager.h:396
smtrat::NewCovering_IncrementalBacktracking
Definition: IncrementalBacktracking.h:8
smtrat::NewCovering_IncrementalBacktracking::NewCovering_IncrementalBacktracking
NewCovering_IncrementalBacktracking()
Definition: IncrementalBacktracking.h:10
smtrat::SATModule
Implements a module performing DPLL style SAT checking.
Definition: SATModule.h:62
smtrat
Class to create the formulas for axioms.
Definition: handle_options.h:10