Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Kučera Petr RNDr. Ph.D.
PCCompile
Commits
d3b0d684
Commit
d3b0d684
authored
Aug 06, 2021
by
Kučera Petr RNDr. Ph.D.
Browse files
Fix in nnf parsing
parent
cbd1c022
Changes
2
Hide whitespace changes
Inline
Side-by-side
bin/nnfsmooth.cpp
View file @
d3b0d684
...
...
@@ -33,7 +33,9 @@ dump_config(const config_t &conf, unsigned level)
<<
"
\t
output_file: "
<<
conf
.
output_file
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
verbosity: "
<<
SUBool
::
logs
.
mVerbLevel
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
check_only: "
<<
conf
.
check_only
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
check_only: "
<<
SUBool
::
bool_to_string
(
conf
.
check_only
)
<<
std
::
endl
;
}
std
::
optional
<
config_t
>
...
...
lib/nnf.cpp
View file @
d3b0d684
...
...
@@ -71,17 +71,15 @@ namespace SUBool
};
void
nnf_header
(
std
::
istream
&
input
,
unsigned
*
max_var
,
size_t
*
edge_count
,
size_t
*
node_count
);
NnfNode
::
tPointer
nnf_parse_and
(
const
std
::
string
&
line
,
const
std
::
vector
<
NnfNode
::
tPointer
>
&
nodes
);
NnfNode
::
tPointer
nnf_parse_literal
(
const
std
::
string
&
line
,
size_t
*
node_count
);
NnfNode
::
tPointer
nnf_parse_and
(
const
std
::
string
&
line
,
const
std
::
vector
<
NnfNode
::
tPointer
>
&
nodes
);
NnfNode
::
tPointer
nnf_parse_literal
(
const
std
::
string
&
line
,
std
::
unordered_map
<
Literal
,
NnfNode
::
tPointer
>
&
literal_nodes
);
NnfNode
::
tPointer
nnf_parse_or
(
const
std
::
string
&
line
,
const
std
::
vector
<
NnfNode
::
tPointer
>
&
nodes
);
NnfNode
::
tPointer
nnf_parse_decision
(
const
std
::
string
&
line
,
const
std
::
vector
<
NnfNode
::
tPointer
>
&
nodes
);
NnfNode
::
tPointer
nnf_parse_or
(
const
std
::
string
&
line
,
const
std
::
vector
<
NnfNode
::
tPointer
>
&
nodes
);
NnfNode
::
tPointer
nnf_parse_decision
(
const
std
::
string
&
line
,
const
std
::
vector
<
NnfNode
::
tPointer
>
&
nodes
);
class
NnfCopyVisitor
:
public
NnfVisitor
{
...
...
@@ -117,9 +115,8 @@ namespace SUBool
if
(
node
->
SplitVar
()
>
0
)
{
node
->
CacheValue
(
mNodeCopy
,
NnfNode
::
MakeOr
(
node
->
SplitVar
(),
std
::
move
(
child_nodes
[
0
]),
std
::
move
(
child_nodes
[
1
])));
NnfNode
::
MakeOr
(
node
->
SplitVar
(),
std
::
move
(
child_nodes
[
0
]),
std
::
move
(
child_nodes
[
1
])));
}
else
{
...
...
@@ -130,11 +127,10 @@ namespace SUBool
virtual
void
VisitDecision
(
const
std
::
shared_ptr
<
const
NnfGateDecision
>
&
node
)
override
{
node
->
CacheValue
(
mNodeCopy
,
NnfNode
::
MakeDecision
(
node
->
DecisionVar
(),
*
node
->
TrueInput
()
->
CachedValue
(
mNodeCopy
),
*
node
->
FalseInput
()
->
CachedValue
(
mNodeCopy
)));
node
->
CacheValue
(
mNodeCopy
,
NnfNode
::
MakeDecision
(
node
->
DecisionVar
(),
*
node
->
TrueInput
()
->
CachedValue
(
mNodeCopy
),
*
node
->
FalseInput
()
->
CachedValue
(
mNodeCopy
)));
}
virtual
void
...
...
@@ -361,13 +357,18 @@ SUBool::Nnf::ReadFromStream(std::istream &input)
}
}
}
if
(
nodes
.
empty
())
{
throw
BadInputException
(
"Nnf::ReadFromStream"
,
"Stream did not contain any node"
);
}
Nnf
nnf
(
nodes
.
back
(),
max_var
,
edge_count
,
node_count
);
return
nnf
;
}
void
SUBool
::
nnf_header
(
std
::
istream
&
input
,
unsigned
*
max_var
,
size_t
*
edge_count
,
size_t
*
node_count
)
size_t
*
node_count
)
{
while
(
input
.
good
())
{
...
...
@@ -383,15 +384,16 @@ SUBool::nnf_header(std::istream &input, unsigned *max_var, size_t *edge_count,
ss
>>
*
node_count
;
ss
>>
*
edge_count
;
ss
>>
*
max_var
;
b
re
ak
;
re
turn
;
}
throw
ParseException
(
"nnf_header"
,
"Bad line "
+
line
);
}
throw
ParseException
(
"nnf_header"
,
"Header not found"
);
}
SUBool
::
NnfNode
::
tPointer
SUBool
::
nnf_parse_and
(
const
std
::
string
&
line
,
const
std
::
vector
<
NnfNode
::
tPointer
>
&
nodes
)
SUBool
::
nnf_parse_and
(
const
std
::
string
&
line
,
const
std
::
vector
<
NnfNode
::
tPointer
>
&
nodes
)
{
std
::
stringstream
ss
(
line
);
char
c
;
...
...
@@ -405,8 +407,8 @@ SUBool::nnf_parse_and(const std::string &line,
ss
>>
index
;
if
(
index
>=
nodes
.
size
())
{
throw
ParseException
(
"nnf_parse_and"
,
"Bad input index "
+
std
::
to_string
(
i
));
throw
ParseException
(
"nnf_parse_and"
,
"Bad input index "
+
std
::
to_string
(
i
));
}
inputs
.
push_back
(
nodes
[
index
]);
}
...
...
@@ -414,8 +416,7 @@ SUBool::nnf_parse_and(const std::string &line,
}
SUBool
::
NnfNode
::
tPointer
SUBool
::
nnf_parse_literal
(
const
std
::
string
&
line
,
SUBool
::
nnf_parse_literal
(
const
std
::
string
&
line
,
std
::
unordered_map
<
Literal
,
NnfNode
::
tPointer
>
&
literal_nodes
)
{
std
::
stringstream
ss
(
line
);
...
...
@@ -434,8 +435,8 @@ SUBool::nnf_parse_literal(
}
SUBool
::
NnfNode
::
tPointer
SUBool
::
nnf_parse_or
(
const
std
::
string
&
line
,
const
std
::
vector
<
NnfNode
::
tPointer
>
&
nodes
)
SUBool
::
nnf_parse_or
(
const
std
::
string
&
line
,
const
std
::
vector
<
NnfNode
::
tPointer
>
&
nodes
)
{
std
::
stringstream
ss
(
line
);
char
c
;
...
...
@@ -451,9 +452,8 @@ SUBool::nnf_parse_or(const std::string &line,
ss
>>
index
;
if
(
index
>=
nodes
.
size
())
{
throw
ParseException
(
"nnf_parse_or"
,
"Bad input index ("
+
std
::
to_string
(
i
)
+
"in "
+
line
+
")"
);
throw
ParseException
(
"nnf_parse_or"
,
"Bad input index ("
+
std
::
to_string
(
i
)
+
"in "
+
line
+
")"
);
}
inputs
.
push_back
(
nodes
[
index
]);
}
...
...
@@ -461,8 +461,7 @@ SUBool::nnf_parse_or(const std::string &line,
{
if
(
n
!=
2
||
inputs
.
size
()
!=
2
)
{
throw
ParseException
(
"nnf_parse_or"
,
throw
ParseException
(
"nnf_parse_or"
,
"Positive split variable with a wrong number of inputs ("
+
line
+
")"
);
}
...
...
@@ -472,8 +471,8 @@ SUBool::nnf_parse_or(const std::string &line,
}
SUBool
::
NnfNode
::
tPointer
SUBool
::
nnf_parse_decision
(
const
std
::
string
&
line
,
const
std
::
vector
<
NnfNode
::
tPointer
>
&
nodes
)
SUBool
::
nnf_parse_decision
(
const
std
::
string
&
line
,
const
std
::
vector
<
NnfNode
::
tPointer
>
&
nodes
)
{
std
::
stringstream
ss
(
line
);
char
c
;
...
...
@@ -484,17 +483,16 @@ SUBool::nnf_parse_decision(const std::string &line,
ss
>>
true_node
;
unsigned
false_node
;
ss
>>
false_node
;
return
NnfNode
::
MakeDecision
(
decision_var
,
nodes
[
true_node
],
nodes
[
false_node
]);
return
NnfNode
::
MakeDecision
(
decision_var
,
nodes
[
true_node
],
nodes
[
false_node
]);
}
void
SUBool
::
Nnf
::
AcceptTopological
(
NnfVisitor
&
visitor
)
const
{
std
::
stack
<
NnfNode
::
tConstPointer
>
order_stack
;
AcceptPostorderFunction
([
&
order_stack
](
const
NnfNode
::
tConstPointer
&
node
)
{
order_stack
.
push
(
node
);
});
AcceptPostorderFunction
([
&
order_stack
](
const
NnfNode
::
tConstPointer
&
node
)
{
order_stack
.
push
(
node
);
});
while
(
!
order_stack
.
empty
())
{
auto
node
=
order_stack
.
top
();
...
...
@@ -507,9 +505,8 @@ SUBool::Nnf::AcceptTopologicalMut(NnfVisitorMut &visitor)
{
InvalidateStats
();
std
::
stack
<
NnfNode
::
tPointer
>
order_stack
;
AcceptPostorderFunctionMut
([
&
order_stack
](
const
NnfNode
::
tPointer
&
node
)
{
order_stack
.
push
(
node
);
});
AcceptPostorderFunctionMut
([
&
order_stack
](
const
NnfNode
::
tPointer
&
node
)
{
order_stack
.
push
(
node
);
});
while
(
!
order_stack
.
empty
())
{
auto
node
=
order_stack
.
top
();
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment