SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Main Page
Related Pages
Namespaces
Namespace List
Namespace Members
All
_
a
b
c
d
e
f
g
h
i
j
l
m
n
o
p
q
r
s
t
u
v
w
x
Functions
_
a
b
c
d
e
f
g
h
i
l
m
n
o
p
q
r
s
t
u
v
w
x
Variables
Typedefs
a
b
c
d
e
f
g
i
j
l
m
o
p
q
r
s
t
u
v
Enumerations
a
b
c
d
f
i
l
m
n
o
p
q
r
s
t
u
v
Enumerator
a
b
c
d
e
f
g
i
l
m
n
o
p
r
s
t
u
x
Data Structures
Data Structures
Data Structure Index
Class Hierarchy
Data Fields
All
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
~
Functions
_
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
z
~
Variables
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
q
r
s
t
u
v
w
x
y
z
Typedefs
a
b
c
d
e
f
g
h
i
j
k
l
m
n
o
p
r
s
t
u
v
w
Enumerations
Enumerator
a
b
c
e
i
l
m
n
o
p
r
s
t
u
w
z
Related Functions
c
d
e
i
m
o
p
s
t
v
Files
File List
Globals
All
_
a
b
c
e
h
i
l
m
o
p
s
u
v
Functions
Variables
Typedefs
Macros
_
a
b
c
e
h
l
m
o
p
s
u
v
•
All
Data Structures
Namespaces
Files
Functions
Variables
Typedefs
Enumerations
Enumerator
Friends
Macros
Pages
PPOCNew.h
Go to the documentation of this file.
1
#pragma once
2
3
#include <
smtrat-modules/FPPModule/FPPModule.h
>
4
#include <
smtrat-modules/SATModule/SATModule.tpp
>
5
#include <
smtrat-solver/Manager.h
>
6
7
namespace
smtrat
{
8
9
namespace
internal {
10
struct
SATSettings :
smtrat::SATSettingsMCSAT
{
11
struct
MCSATSettings
: mcsat::Base {
12
using
AssignmentFinderBackend
=
mcsat::arithmetic::AssignmentFinder
;
13
using
ExplanationBackend
=
mcsat::SequentialExplanation<mcsat::onecell::Explanation<smtrat::mcsat::onecell::DefaultSettings>
,
mcsat::nlsat::Explanation
>;
14
};
15
};
16
}
// namespace internal
17
18
class
MCSAT_PPOCNew
:
public
Manager
{
19
public
:
20
MCSAT_PPOCNew
() :
Manager
() {
21
setStrategy
(
22
addBackend
<
FPPModule<FPPSettings1>
>({
23
addBackend<SATModule<internal::SATSettings>>()
24
})
25
);
26
}
27
};
28
29
}
// namespace smtrat
FPPModule.h
Manager.h
SATModule.tpp
smtrat::FPPModule
Definition:
FPPModule.h:18
smtrat::MCSAT_PPOCNew
Definition:
PPOCNew.h:18
smtrat::MCSAT_PPOCNew::MCSAT_PPOCNew
MCSAT_PPOCNew()
Definition:
PPOCNew.h:20
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
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::mcsat::SequentialExplanation
Definition:
SequentialExplanation.h:11
smtrat::mcsat::arithmetic::AssignmentFinder
Definition:
AssignmentFinder.h:11
smtrat::mcsat::nlsat::Explanation
Definition:
Explanation.h:12
smtrat-strategies
strategies
MCSAT
PPOCNew.h
Generated by
1.9.1