SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
OCNewBC.h
Go to the documentation of this file.
1
#pragma once
2
3
#include <
smtrat-solver/Manager.h
>
4
5
// #include "../modules/FPPModule/FPPModule.h"
6
#include <
smtrat-modules/SATModule/SATModule.h
>
7
#include <
smtrat-modules/SATModule/SATModule.tpp
>
8
9
10
namespace
smtrat
{
11
12
namespace
internal {
13
struct
OCSettings :
smtrat::mcsat::onecell::BaseSettings
{
14
constexpr
static
bool
exploit_strict_constraints
=
false
;
15
16
constexpr
static
auto
cell_heuristic
=
cadcells::representation::BIGGEST_CELL
;
17
constexpr
static
auto
covering_heuristic
=
cadcells::representation::BIGGEST_CELL_COVERING
;
18
constexpr
static
auto
op
= cadcells::operators::op::mccallum;
19
};
20
21
struct
SATSettings
:
smtrat::SATSettingsMCSAT
{
22
struct
MCSATSettings
:
mcsat::Base
{
23
using
AssignmentFinderBackend
=
mcsat::arithmetic::AssignmentFinder
;
24
using
ExplanationBackend
=
mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>
,
mcsat::nlsat::Explanation
>;
25
};
26
};
27
}
// namespace internal
28
29
class
MCSAT_OCNewBC
:
public
Manager
{
30
public
:
31
MCSAT_OCNewBC
()
32
:
Manager
() {
33
setStrategy
(
34
addBackend
<
SATModule<internal::SATSettings>
>());
35
}
36
};
37
38
}
// namespace smtrat
Manager.h
SATModule.h
SATModule.tpp
smtrat::MCSAT_OCNewBC
Definition:
OCNewBC.h:29
smtrat::MCSAT_OCNewBC::MCSAT_OCNewBC
MCSAT_OCNewBC()
Definition:
OCNewBC.h:31
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::SATModule
Implements a module performing DPLL style SAT checking.
Definition:
SATModule.h:62
smtrat::cadcells::representation::BIGGEST_CELL
@ BIGGEST_CELL
Definition:
heuristics.h:11
smtrat::cadcells::representation::BIGGEST_CELL_COVERING
@ BIGGEST_CELL_COVERING
Definition:
heuristics.h:16
smtrat
Class to create the formulas for axioms.
Definition:
handle_options.h:10
smtrat::SATSettings1::MCSATSettings
mcsat::MCSATSettingsFMVSNL MCSATSettings
Definition:
SATSettings.h:110
smtrat::SATSettingsMCSAT
Definition:
SATSettings.h:123
smtrat::cadcells::operators::Mccallum
Definition:
operator_mccallum.h:22
smtrat::internal::OCSettings::cell_heuristic
constexpr static auto cell_heuristic
Definition:
BCAll.h:20
smtrat::internal::OCSettings::exploit_strict_constraints
constexpr static bool exploit_strict_constraints
Definition:
BCAll.h:18
smtrat::internal::OCSettings::covering_heuristic
constexpr static auto covering_heuristic
Definition:
BCAll.h:21
smtrat::internal::SATSettings
Definition:
BCAll.h:25
smtrat::mcsat::Base
Definition:
MCSATSettings.h:20
smtrat::mcsat::SequentialExplanation
Definition:
SequentialExplanation.h:11
smtrat::mcsat::arithmetic::AssignmentFinder
Definition:
AssignmentFinder.h:11
smtrat::mcsat::nlsat::Explanation
Definition:
Explanation.h:12
smtrat::mcsat::onecell::BaseSettings
Definition:
Explanation.h:20
smtrat-strategies
strategies
MCSAT
OCNewBC.h
Generated by
1.9.1