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
29b3d9af
Commit
29b3d9af
authored
Jul 14, 2021
by
Kučera Petr RNDr. Ph.D.
Browse files
cnfdiff using PrgOptions
parent
b51ffc69
Changes
3
Hide whitespace changes
Inline
Side-by-side
bin/cnfcanon.cpp
View file @
29b3d9af
...
@@ -71,6 +71,10 @@ parse_arguments(int argc, char *argv[])
...
@@ -71,6 +71,10 @@ parse_arguments(int argc, char *argv[])
void
void
dump_config
(
const
config_t
&
conf
,
unsigned
level
)
dump_config
(
const
config_t
&
conf
,
unsigned
level
)
{
{
if
(
!
SUBool
::
logs
.
CheckLevel
(
level
))
{
return
;
}
SUBool
::
logs
.
TLog
(
level
)
<<
"Configuration:"
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"Configuration:"
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
input_file: "
<<
conf
.
input_file
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
input_file: "
<<
conf
.
input_file
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
SUBool
::
logs
.
TLog
(
level
)
...
@@ -154,7 +158,7 @@ main(int argc, char *argv[])
...
@@ -154,7 +158,7 @@ main(int argc, char *argv[])
{
{
return
1
;
return
1
;
}
}
dump_config
(
*
conf
,
1
);
dump_config
(
*
conf
,
4
);
SUBool
::
CNF
cnf
;
SUBool
::
CNF
cnf
;
int
ret
=
input
(
*
conf
,
&
cnf
);
int
ret
=
input
(
*
conf
,
&
cnf
);
if
(
ret
!=
0
)
if
(
ret
!=
0
)
...
...
bin/cnfcomp.cpp
View file @
29b3d9af
...
@@ -61,6 +61,10 @@ struct config_t
...
@@ -61,6 +61,10 @@ struct config_t
void
void
dump_config
(
const
config_t
&
conf
,
unsigned
level
)
dump_config
(
const
config_t
&
conf
,
unsigned
level
)
{
{
if
(
!
SUBool
::
logs
.
CheckLevel
(
level
))
{
return
;
}
SUBool
::
logs
.
TLog
(
level
)
<<
"Configuration:"
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"Configuration:"
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
file_left: "
<<
conf
.
file_left
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
file_left: "
<<
conf
.
file_left
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
file_right: "
<<
conf
.
file_right
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"
\t
file_right: "
<<
conf
.
file_right
<<
std
::
endl
;
...
@@ -300,7 +304,7 @@ main(int argc, char *argv[])
...
@@ -300,7 +304,7 @@ main(int argc, char *argv[])
{
{
return
1
;
return
1
;
}
}
dump_config
(
*
conf
,
0
);
dump_config
(
*
conf
,
4
);
auto
left_cnf
=
auto
left_cnf
=
SUBool
::
input_or_die
<
SUBool
::
CNF
>
(
conf
->
file_left
,
SUBool
::
logs
);
SUBool
::
input_or_die
<
SUBool
::
CNF
>
(
conf
->
file_left
,
SUBool
::
logs
);
auto
right_cnf
=
auto
right_cnf
=
...
...
bin/cnfdiff.cpp
View file @
29b3d9af
...
@@ -6,8 +6,6 @@
...
@@ -6,8 +6,6 @@
* Program for comparing two CNFs as sets of clauses (not as representations of
* Program for comparing two CNFs as sets of clauses (not as representations of
* functions).
* functions).
*/
*/
#include <cxxopts.hpp>
#include "normalform.h"
#include "normalform.h"
#include "prgutil.h"
#include "prgutil.h"
...
@@ -20,7 +18,6 @@ struct config_t
...
@@ -20,7 +18,6 @@ struct config_t
{
{
std
::
string
file_left
{};
std
::
string
file_left
{};
std
::
string
file_right
{};
std
::
string
file_right
{};
unsigned
verbosity
{
3
};
// 0 means no output
bool
suppress_first
{
false
};
bool
suppress_first
{
false
};
bool
suppress_second
{
false
};
bool
suppress_second
{
false
};
bool
suppress_third
{
false
};
bool
suppress_third
{
false
};
...
@@ -29,68 +26,39 @@ struct config_t
...
@@ -29,68 +26,39 @@ struct config_t
void
void
dump_config
(
const
config_t
&
conf
,
unsigned
level
)
dump_config
(
const
config_t
&
conf
,
unsigned
level
)
{
{
if
(
!
SUBool
::
logs
.
CheckLevel
(
level
))
{
return
;
}
SUBool
::
logs
.
TLog
(
level
)
<<
"Configuration:"
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
level
)
<<
"Configuration:"
<<
std
::
endl
;
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"file_left"
,
conf
.
file_left
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"file_left"
,
conf
.
file_left
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"file_right"
,
conf
.
file_right
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"file_right"
,
conf
.
file_right
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"verbosity"
,
conf
.
verbosity
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"verbosity"
,
SUBool
::
logs
.
mVerbLevel
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"suppress_first"
,
conf
.
suppress_first
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"suppress_first"
,
conf
.
suppress_first
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"suppress_second"
,
conf
.
suppress_second
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"suppress_second"
,
conf
.
suppress_second
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"suppress_third"
,
conf
.
suppress_third
);
SUBool
::
logs
.
DumpValue
(
"
\t
"
,
level
,
"suppress_third"
,
conf
.
suppress_third
);
}
}
int
std
::
optional
<
config_t
>
parse_arguments
(
int
argc
,
char
*
argv
[]
,
config_t
&
conf
)
parse_arguments
(
int
argc
,
char
*
argv
[])
{
{
try
config_t
conf
;
{
SUBool
::
PrgOptions
opts
;
cxxopts
::
Options
options
(
SUBool
::
kPrgName
,
SUBool
::
kPrgDesc
);
opts
.
InputPair
(
options
.
positional_help
(
"[input-left [input-right]]"
);
{
&
conf
.
file_left
,
"input-left"
},
{
&
conf
.
file_right
,
"input-right"
});
std
::
string
check_kind
;
po
::
options_description
desc
(
"Configuration options"
);
options
.
add_options
()(
"h,help"
,
"Print help"
)(
desc
.
add_options
()(
",1"
,
po
::
bool_switch
(
&
conf
.
suppress_first
),
"v,version"
,
"Print version info"
)(
"b,verbosity"
,
"Suppress printing the clauses unique to the first CNF."
)(
",2"
,
"Verbosity level of the log which is written to standard output."
po
::
bool_switch
(
&
conf
.
suppress_second
),
" 0 means no log is written, however messages of glucose can still "
"Suppress printing the clauses unique to the second CNF."
)(
",3"
,
"appear."
,
po
::
bool_switch
(
&
conf
.
suppress_third
),
cxxopts
::
value
<
unsigned
>
(
conf
.
verbosity
)
"Suppress printing the clauses unique to the third CNF."
);
->
default_value
(
SUBool
::
LogStream
::
kMaxLogLevels
))(
"l,input-left"
,
opts
.
Add
(
desc
);
"The left hand input file"
,
if
(
!
opts
.
Parse
(
argc
,
argv
))
cxxopts
::
value
<
std
::
string
>
(
conf
.
file_left
))(
"r,input-right"
,
"The right hand input file"
,
cxxopts
::
value
<
std
::
string
>
(
conf
.
file_right
))(
"1"
,
"Suppress printing the clauses unique to the first CNF."
,
cxxopts
::
value
<
bool
>
(
conf
.
suppress_first
)
->
default_value
(
"false"
))(
"2"
,
"Suppress printing the clauses unique to the second CNF."
,
cxxopts
::
value
<
bool
>
(
conf
.
suppress_second
)
->
default_value
(
"false"
))(
"3"
,
"Suppress printing the clauses which are in both CNF formulas."
,
cxxopts
::
value
<
bool
>
(
conf
.
suppress_third
)
->
default_value
(
"false"
));
options
.
parse_positional
({
"input-left"
,
"input-right"
,
"positional"
});
auto
result
=
options
.
parse
(
argc
,
argv
);
if
(
result
.
count
(
"help"
))
{
std
::
cout
<<
options
.
help
()
<<
std
::
endl
;
return
1
;
}
if
(
result
.
count
(
"version"
))
{
SUBool
::
print_version
(
std
::
cout
);
return
1
;
}
if
(
result
.
count
(
"positional"
))
{
SUBool
::
logs
.
TLog
(
0
)
<<
"Multiple files passed as parameters, "
;
SUBool
::
logs
.
TLog
(
0
)
<<
"only two input files allowed"
<<
std
::
endl
;
SUBool
::
logs
.
TLog
(
0
)
<<
options
.
help
()
<<
std
::
endl
;
return
1
;
}
}
catch
(
const
cxxopts
::
OptionException
&
e
)
{
{
std
::
cerr
<<
"Error parsing options: "
<<
e
.
what
()
<<
std
::
endl
;
return
{};
return
1
;
}
}
return
0
;
return
conf
;
}
}
void
void
...
@@ -151,13 +119,14 @@ compare(SUBool::CNF left, SUBool::CNF right, config_t &conf)
...
@@ -151,13 +119,14 @@ compare(SUBool::CNF left, SUBool::CNF right, config_t &conf)
int
int
main
(
int
argc
,
char
*
argv
[])
main
(
int
argc
,
char
*
argv
[])
{
{
config_t
conf
;
auto
conf
=
parse_arguments
(
argc
,
argv
);
int
r
=
parse_arguments
(
argc
,
argv
,
conf
);
if
(
!
conf
)
if
(
r
!=
0
)
{
{
return
r
;
return
1
;
}
}
compare
(
SUBool
::
input_or_die
<
SUBool
::
CNF
>
(
conf
.
file_left
,
SUBool
::
logs
),
dump_config
(
*
conf
,
4
);
SUBool
::
input_or_die
<
SUBool
::
CNF
>
(
conf
.
file_right
,
SUBool
::
logs
),
conf
);
compare
(
SUBool
::
input_or_die
<
SUBool
::
CNF
>
(
conf
->
file_left
,
SUBool
::
logs
),
SUBool
::
input_or_die
<
SUBool
::
CNF
>
(
conf
->
file_right
,
SUBool
::
logs
),
*
conf
);
return
0
;
return
0
;
}
}
Write
Preview
Supports
Markdown
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