Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add log-file option to write debug/tracing information into a file #74

Merged
merged 1 commit into from
Aug 13, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 25 additions & 11 deletions crates/fzn-huub/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ mod trace;

use std::{
collections::HashMap,
convert::Infallible,
fmt::{self, Debug, Display},
fs::File,
io::BufReader,
Expand Down Expand Up @@ -37,28 +38,32 @@ FLAGS
-a, --all-solutions Find all possible solutions for the given (satisfaction) instance.
-i, --intermediate-solutions Display all intermediate solutions found during the search.
-f, --free-search Allow the solver to adjust any search options as it judges best.
This flag overrides all other search-related flags.
This flag overrides all other search-related flags.
-s, --statistics Print statistics about the solving process.
-t, --time-limit <value> Set a time limit for the solver. The value can be a number of
milliseconds or a human-readable duration string.
milliseconds or a human-readable duration string.
-v, --verbose Display addtional information about actions taken by the solver.
Can be used multiple times to increase verbosity.
Can be used multiple times to increase verbosity.
(0: INFO, 1: DEBUG, 2: TRACE)

=== INITIALIZATION OPTIONS ===
--int-eager-limit Set the maximum cardinality for which all order literals to
represent an integer variable are created eagerly.
(default: 255)

=== SOLVING OPTIONS ===
--vsids-after <value> Switch to the VSIDS search heuristic after a certain number of
conflicts. (overwritten by --toggle-vsids and --vsids-only)
--toggle-vsids Switch between the activity-based search heuristic and the user-
specific search heuristic after every restart.
(overwritten by --vsids-only)
(default: 255)

=== SOLVING OPTIONS ===
--vsids-after <value> Switch to the VSIDS search heuristic after a certain number of
conflicts. (overwritten by --toggle-vsids and --vsids-only)
--toggle-vsids Switch between the activity-based search heuristic and the user-
specific search heuristic after every restart.
(overwritten by --vsids-only)
--vsids-only Only use the activity-based search heuristic provided by the SAT
solver. Ignore the user-specific search heuristic.


=== BEHAVIOUR OPTIONS ===
--log-file <FILE> Output log messages from the solver to a file, instead of stderr.

DESCRIPTION
Create a Huub Solver instance tailored to a given FlatZinc JSON input file and solve the problem.

Expand Down Expand Up @@ -105,6 +110,8 @@ struct Cli {
time_limit: Option<Duration>,
/// Level of verbosity
verbose: u8,
/// Log file
log_file: Option<PathBuf>,

// --- Initialization configuration ---
/// Cardinatility cutoff for eager order literals
Expand Down Expand Up @@ -170,6 +177,7 @@ impl Cli {
let int_reverse_map: Arc<Mutex<Vec<Ustr>>> = Arc::default();
let subscriber = trace::create_subscriber(
self.verbose,
self.log_file.clone(),
Arc::clone(&lit_reverse_map),
Arc::clone(&int_reverse_map),
);
Expand Down Expand Up @@ -479,6 +487,12 @@ impl TryFrom<Arguments> for Cli {
.opt_value_from_str("--vsids-after")
.map_err(|e| e.to_string())?,

log_file: args
.opt_value_from_os_str("--log-file", |s| -> Result<PathBuf, Infallible> {
Ok(s.into())
})
.map_err(|e| e.to_string())?,

verbose,
path: args
.free_from_os_str(|s| -> Result<PathBuf, &'static str> { Ok(s.into()) })
Expand Down
33 changes: 29 additions & 4 deletions crates/fzn-huub/src/trace.rs
Original file line number Diff line number Diff line change
@@ -1,8 +1,9 @@
use std::{
collections::HashMap,
fmt::{self, Display},
io,
fs, io,
num::NonZeroI32,
path::PathBuf,
sync::{Arc, Mutex},
};

Expand Down Expand Up @@ -62,18 +63,42 @@ struct RegisterLazyLits {

pub(crate) fn create_subscriber(
verbose: u8,
log_file: Option<PathBuf>,
lit_reverse_map: Arc<Mutex<HashMap<LitInt, LitName>>>,
int_reverse_map: Arc<Mutex<Vec<Ustr>>>,
) -> impl Subscriber {
tracing_subscriber::fmt()
let logged_to_file = log_file.is_some();
// Function that will create the writer for the log output
let make_writer = move || -> Box<dyn io::Write> {
if let Some(path) = log_file.clone() {
Box::new(
fs::OpenOptions::new()
.create(true)
.append(true)
.open(path)
.expect("Failed to open log file"),
)
} else {
Box::new(io::stderr())
}
};

// Builder for the formatting subscriber
let builder = tracing_subscriber::fmt()
.with_max_level(match verbose {
0 => Level::INFO,
1 => Level::DEBUG,
_ => Level::TRACE, // 2 or more
})
.with_writer(io::stderr)
.with_writer(make_writer)
.with_ansi(!logged_to_file)
.with_timer(uptime())
.map_fmt_fields(|fmt| FmtLitFields::new(fmt, Arc::clone(&lit_reverse_map), int_reverse_map))
.map_fmt_fields(|fmt| {
FmtLitFields::new(fmt, Arc::clone(&lit_reverse_map), int_reverse_map)
});

// Create final subscriber and add the layer that will register new lazily created literals
builder
.finish()
.with(RegisterLazyLits::new(lit_reverse_map))
}
Expand Down