From 6741375aa1bfb0b9e641cc9ffabe9085277ef365 Mon Sep 17 00:00:00 2001 From: Ian Shehadeh Date: Sun, 5 Jan 2025 12:38:36 -0500 Subject: [PATCH 1/2] feat(stats) add structs + trait to export stats --- solver/Cargo.toml | 4 ++ solver/src/reasoners/cp/mod.rs | 25 +++++++++++++ solver/src/reasoners/eq/dense.rs | 52 ++++++++++++++++++++++++++ solver/src/reasoners/eq/split.rs | 27 ++++++++++++- solver/src/reasoners/sat/sat_solver.rs | 25 +++++++++++++ solver/src/reasoners/stn/theory.rs | 40 ++++++++++++++++++++ solver/src/reasoners/tautologies.rs | 18 +++++++++ solver/src/solver/solver_impl.rs | 9 +++++ solver/src/utils/mod.rs | 3 ++ solver/src/utils/statistics.rs | 10 +++++ 10 files changed, 212 insertions(+), 1 deletion(-) create mode 100644 solver/src/utils/statistics.rs diff --git a/solver/Cargo.toml b/solver/Cargo.toml index 2bf095951..9a31dc602 100644 --- a/solver/Cargo.toml +++ b/solver/Cargo.toml @@ -8,6 +8,9 @@ edition = "2021" [features] +# if enabled, solver and theory statistics may be exported and imported using serde +export_stats = [ "dep:serde" ] + # If enabled, will instruct the the solver to count cpu cycles at various point of its execution. # The implementation relies to time-stamp counter and intrinsic for the x86_64 platform. # If the target platform is not supported, activating this feature will have no effects. @@ -30,6 +33,7 @@ lru = "0.12.3" rand = { workspace = true } num-rational = { workspace = true } hashbrown = "0.15" +serde = { version = "1", optional = true } [dev-dependencies] rand = "0.8" diff --git a/solver/src/reasoners/cp/mod.rs b/solver/src/reasoners/cp/mod.rs index 4492de7c9..c7bded8a6 100644 --- a/solver/src/reasoners/cp/mod.rs +++ b/solver/src/reasoners/cp/mod.rs @@ -19,6 +19,7 @@ use crate::model::lang::mul::NFEqVarMulLit; use crate::reasoners::cp::linear::{LinearSumLeq, SumElem}; use crate::reasoners::cp::max::AtLeastOneGeq; use crate::reasoners::{Contradiction, ReasonerId, Theory}; +use crate::utils::SnapshotStatistics; use anyhow::Context; use mul::VarEqVarMulLit; use set::IterableRefSet; @@ -235,6 +236,30 @@ impl Theory for Cp { } } +#[derive(Debug, PartialEq, Eq, Clone)] +pub struct CpStatsSnapshot { + pub num_constraints: usize, + pub num_propagations: u64, +} + +impl std::fmt::Display for CpStatsSnapshot { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + writeln!(f, "# constraints: {}", self.num_constraints)?; + writeln!(f, "# propagations: {}", self.num_propagations) + } +} + +impl SnapshotStatistics for Cp { + type Stats = CpStatsSnapshot; + + fn snapshot_statistics(&self) -> Self::Stats { + Self::Stats { + num_constraints: self.constraints.len(), + num_propagations: self.stats.num_propagations, + } + } +} + impl Backtrack for Cp { fn save_state(&mut self) -> DecLvl { self.saved += 1; diff --git a/solver/src/reasoners/eq/dense.rs b/solver/src/reasoners/eq/dense.rs index 2849707cd..7f405ff94 100644 --- a/solver/src/reasoners/eq/dense.rs +++ b/solver/src/reasoners/eq/dense.rs @@ -6,6 +6,7 @@ use crate::model::{Label, Model}; use crate::reasoners::eq::domain; use crate::reasoners::{Contradiction, ReasonerId, Theory}; use crate::reif::ReifExpr; +use crate::utils::SnapshotStatistics; use itertools::Itertools; use std::collections::{HashMap, HashSet}; use std::fmt::{Debug, Formatter}; @@ -875,6 +876,57 @@ impl Theory for DenseEqTheory { } } +#[derive(Debug, Clone, PartialEq, Eq, Default)] +pub struct DenseEqTheoryStatsSnapshot { + pub num_nodes: usize, + pub num_edge_propagations: usize, + pub num_edge_propagations_pos: usize, + pub num_edge_propagations_neg: usize, + pub num_edge_propagation1_pos_pos: usize, + pub num_edge_propagation1_pos_neg: usize, + pub num_edge_propagation1_neg_pos: usize, + pub num_edge_propagation1_effective: usize, + pub num_edge_propagation2_pos_pos: usize, + pub num_edge_propagation2_pos_neg: usize, + pub num_edge_propagation2_neg_pos: usize, +} + +impl std::fmt::Display for DenseEqTheoryStatsSnapshot { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + writeln!(f, "num nodes: {}", self.num_nodes)?; + writeln!(f, "num edge props1 {}", self.num_edge_propagations)?; + writeln!(f, "num edge props+ {}", self.num_edge_propagations_pos)?; + writeln!(f, "num edge props- {}", self.num_edge_propagations_neg)?; + writeln!(f, "num edge props1 ++ {}", self.num_edge_propagation1_pos_pos)?; + writeln!(f, "num edge props1 +- {}", self.num_edge_propagation1_pos_neg)?; + writeln!(f, "num edge props1 -+ {}", self.num_edge_propagation1_neg_pos)?; + writeln!(f, "num edge props1 eff {}", self.num_edge_propagation1_effective)?; + writeln!(f, "num edge props2 ++ {}", self.num_edge_propagation2_pos_pos)?; + writeln!(f, "num edge props2 +- {}", self.num_edge_propagation2_pos_neg)?; + writeln!(f, "num edge props2 -+ {}", self.num_edge_propagation2_neg_pos) + } +} + +impl SnapshotStatistics for DenseEqTheory { + type Stats = DenseEqTheoryStatsSnapshot; + + fn snapshot_statistics(&self) -> Self::Stats { + Self::Stats { + num_nodes: self.graph.nodes_ordered.len(), + num_edge_propagations: self.stats.num_edge_propagations, + num_edge_propagations_pos: self.stats.num_edge_propagations_pos, + num_edge_propagations_neg: self.stats.num_edge_propagations_neg, + num_edge_propagation1_pos_pos: self.stats.num_edge_propagation1_pos_pos, + num_edge_propagation1_pos_neg: self.stats.num_edge_propagation1_pos_neg, + num_edge_propagation1_neg_pos: self.stats.num_edge_propagation1_neg_pos, + num_edge_propagation1_effective: self.stats.num_edge_propagation1_effective, + num_edge_propagation2_pos_pos: self.stats.num_edge_propagation2_pos_pos, + num_edge_propagation2_pos_neg: self.stats.num_edge_propagation2_pos_neg, + num_edge_propagation2_neg_pos: self.stats.num_edge_propagation2_neg_pos, + } + } +} + pub trait ReifyEq { fn domains(&self) -> &Domains; fn domain(&self, a: Node) -> (IntCst, IntCst); diff --git a/solver/src/reasoners/eq/split.rs b/solver/src/reasoners/eq/split.rs index 690d38c1f..3b936fef8 100644 --- a/solver/src/reasoners/eq/split.rs +++ b/solver/src/reasoners/eq/split.rs @@ -1,8 +1,9 @@ use crate::backtrack::{Backtrack, DecLvl, DecisionLevelTracker}; use crate::core::state::{Domains, DomainsSnapshot, Explanation, InferenceCause}; use crate::core::{IntCst, Lit, VarRef}; -use crate::reasoners::eq::{DenseEqTheory, Node, ReifyEq}; +use crate::reasoners::eq::{DenseEqTheory, DenseEqTheoryStatsSnapshot, Node, ReifyEq}; use crate::reasoners::{Contradiction, ReasonerId, Theory}; +use crate::utils::SnapshotStatistics; use itertools::Itertools; use std::collections::HashMap; @@ -17,6 +18,30 @@ pub struct SplitEqTheory { lvl: DecisionLevelTracker, } +impl SnapshotStatistics for SplitEqTheory { + type Stats = DenseEqTheoryStatsSnapshot; + + fn snapshot_statistics(&self) -> Self::Stats { + self.parts() + .map(|part| part.snapshot_statistics()) + .reduce(|sum, next| DenseEqTheoryStatsSnapshot { + num_nodes: sum.num_nodes + next.num_nodes, + num_edge_propagations: sum.num_edge_propagations + next.num_edge_propagations, + num_edge_propagations_pos: sum.num_edge_propagations_pos + next.num_edge_propagations_pos, + num_edge_propagations_neg: sum.num_edge_propagations_neg + next.num_edge_propagations_neg, + num_edge_propagation1_pos_pos: sum.num_edge_propagation1_pos_pos + next.num_edge_propagation1_pos_pos, + num_edge_propagation1_pos_neg: sum.num_edge_propagation1_pos_neg + next.num_edge_propagation1_pos_neg, + num_edge_propagation1_neg_pos: sum.num_edge_propagation1_neg_pos + next.num_edge_propagation1_neg_pos, + num_edge_propagation1_effective: sum.num_edge_propagation1_effective + + next.num_edge_propagation1_effective, + num_edge_propagation2_pos_pos: sum.num_edge_propagation2_pos_pos + next.num_edge_propagation2_pos_pos, + num_edge_propagation2_pos_neg: sum.num_edge_propagation2_pos_neg + next.num_edge_propagation2_pos_neg, + num_edge_propagation2_neg_pos: sum.num_edge_propagation2_neg_pos + next.num_edge_propagation2_neg_pos, + }) + .unwrap_or_default() + } +} + impl SplitEqTheory { pub fn add_edge(&mut self, a: VarRef, b: VarRef, model: &mut impl ReifyEq) -> Lit { debug_assert_eq!(self.lvl.num_saved(), 0, "Adding an edge but not at the root"); diff --git a/solver/src/reasoners/sat/sat_solver.rs b/solver/src/reasoners/sat/sat_solver.rs index fd7920747..84559eb65 100644 --- a/solver/src/reasoners/sat/sat_solver.rs +++ b/solver/src/reasoners/sat/sat_solver.rs @@ -6,6 +6,7 @@ use crate::core::*; use crate::model::extensions::DisjunctionExt; use crate::reasoners::sat::clauses::*; use crate::reasoners::{Contradiction, ReasonerId, Theory}; +use crate::utils::SnapshotStatistics; use itertools::Itertools; use smallvec::alloc::collections::VecDeque; @@ -721,6 +722,30 @@ impl Backtrack for SatSolver { } } +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct SatSolverStatsSnapshot { + pub num_clauses: usize, + pub propagations: u64, +} + +impl std::fmt::Display for SatSolverStatsSnapshot { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + writeln!(f, "DB size : {}", self.num_clauses)?; + writeln!(f, "Num unit propagations: {}", self.propagations) + } +} + +impl SnapshotStatistics for SatSolver { + type Stats = SatSolverStatsSnapshot; + + fn snapshot_statistics(&self) -> Self::Stats { + SatSolverStatsSnapshot { + num_clauses: self.clauses.num_clauses(), + propagations: self.stats.propagations, + } + } +} + impl Theory for SatSolver { fn identity(&self) -> ReasonerId { self.identity diff --git a/solver/src/reasoners/stn/theory.rs b/solver/src/reasoners/stn/theory.rs index 2be531d2d..95b4a88d3 100644 --- a/solver/src/reasoners/stn/theory.rs +++ b/solver/src/reasoners/stn/theory.rs @@ -10,6 +10,7 @@ use crate::core::state::*; use crate::core::*; use crate::reasoners::stn::theory::Event::EdgeActivated; use crate::reasoners::{Contradiction, ReasonerId, Theory}; +use crate::utils::SnapshotStatistics; use contraint_db::*; use distances::{Graph, StnGraph}; use edges::*; @@ -114,6 +115,29 @@ struct Stats { num_theory_deactivations: u64, } +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct StnStatSnapshot { + pub num_nodes: u32, + pub num_propagator_groups: usize, + pub num_propagations: u64, + pub bound_updates: u64, + pub num_bound_edge_deactivation: u64, + pub num_theory_propagations: u64, + pub num_theory_deactivations: u64, +} + +impl std::fmt::Display for StnStatSnapshot { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + writeln!(f, "# nodes: {}", self.num_nodes)?; + writeln!(f, "# propagators: {}", self.num_propagator_groups)?; + writeln!(f, "# propagations: {}", self.num_propagations)?; + writeln!(f, "# domain updates: {}", self.bound_updates)?; + writeln!(f, "# bounds deactivations: {}", self.num_bound_edge_deactivation)?; + writeln!(f, "# theory propagations: {}", self.num_theory_propagations)?; + writeln!(f, "# theory deactivations: {}", self.num_theory_deactivations) + } +} + #[derive(Debug, Clone, Copy)] pub(crate) struct Identity where @@ -963,6 +987,22 @@ impl Backtrack for StnTheory { } } +impl SnapshotStatistics for StnTheory { + type Stats = StnStatSnapshot; + + fn snapshot_statistics(&self) -> Self::Stats { + StnStatSnapshot { + num_nodes: self.num_nodes(), + num_propagator_groups: self.constraints.num_propagator_groups(), + num_propagations: self.stats.num_propagations, + bound_updates: self.stats.bound_updates, + num_bound_edge_deactivation: self.stats.num_bound_edge_deactivation, + num_theory_propagations: self.stats.num_theory_propagations, + num_theory_deactivations: self.stats.num_theory_deactivations, + } + } +} + #[allow(clippy::let_unit_value)] #[cfg(test)] mod tests { diff --git a/solver/src/reasoners/tautologies.rs b/solver/src/reasoners/tautologies.rs index 527c54ffd..739ee1db9 100644 --- a/solver/src/reasoners/tautologies.rs +++ b/solver/src/reasoners/tautologies.rs @@ -2,6 +2,7 @@ use crate::backtrack::{Backtrack, DecLvl}; use crate::core::state::{Cause, Domains, DomainsSnapshot, Explanation, InferenceCause}; use crate::core::Lit; use crate::reasoners::{Contradiction, ReasonerId, Theory}; +use crate::utils::SnapshotStatistics; /// A reasoner that holds a set of tautologies (single literals that are known to be true) /// and propagates them at every decision level. @@ -77,3 +78,20 @@ impl Theory for Tautologies { Box::new(self.clone()) } } + +#[derive(Debug, Clone)] +pub struct TautologiesStatSnapshot; +impl std::fmt::Display for TautologiesStatSnapshot { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + write!(f, "{}", std::any::type_name::()) + } +} + + +impl SnapshotStatistics for Tautologies { + type Stats = TautologiesStatSnapshot; + + fn snapshot_statistics(&self) -> Self::Stats { + TautologiesStatSnapshot + } +} diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index d1ddc90cd..071524354 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -13,6 +13,7 @@ use crate::solver::parallel::signals::{InputSignal, InputStream, SolverOutput, S use crate::solver::search::{default_brancher, Decision, SearchControl}; use crate::solver::stats::Stats; use crate::utils::cpu_time::StartCycleCount; +use crate::utils::SnapshotStatistics; use crossbeam_channel::Sender; use env_param::EnvParam; use itertools::Itertools; @@ -936,6 +937,14 @@ impl Solver { } } +impl SnapshotStatistics for Solver { + type Stats = Stats; + + fn snapshot_statistics(&self) -> Self::Stats { + self.stats.clone() + } +} + impl Backtrack for Solver { fn save_state(&mut self) -> DecLvl { self.brancher.pre_save_state(&self.model); diff --git a/solver/src/utils/mod.rs b/solver/src/utils/mod.rs index c9782e8cd..96e1d6f16 100644 --- a/solver/src/utils/mod.rs +++ b/solver/src/utils/mod.rs @@ -1,6 +1,9 @@ pub(crate) mod cpu_time; pub mod input; +mod statistics; +pub use statistics::*; + use std::fmt::{Display, Error, Formatter}; /// A custom type to extract the formatter and feed it to formal_impl diff --git a/solver/src/utils/statistics.rs b/solver/src/utils/statistics.rs new file mode 100644 index 000000000..61533ed15 --- /dev/null +++ b/solver/src/utils/statistics.rs @@ -0,0 +1,10 @@ + + +/// Implementors of this trait can export a snapshot of their runtime statistics. +/// The exported data must be able to _at least_ be formatted using std::fmt::Display. +/// Ideally, it should also implement serde traits when `export_stats` feature is enabled. +pub trait SnapshotStatistics { + type Stats: Sized + std::fmt::Display; + + fn snapshot_statistics(&self) -> Self::Stats; +} From 1eec9038d8ed2763856e16fbb542a7476fc3e097 Mon Sep 17 00:00:00 2001 From: Ian Shehadeh Date: Sun, 5 Jan 2025 17:43:51 -0500 Subject: [PATCH 2/2] serde definitions & export-friendly version of Solver statistics --- Cargo.lock | 2 + examples/sat/Cargo.toml | 2 +- examples/sat/main.rs | 10 ++++ solver/Cargo.toml | 2 +- solver/src/reasoners/cp/mod.rs | 1 + solver/src/reasoners/eq/dense.rs | 7 +-- solver/src/reasoners/eq/split.rs | 6 +-- solver/src/reasoners/sat/sat_solver.rs | 1 + solver/src/reasoners/stn/theory.rs | 1 + solver/src/reasoners/tautologies.rs | 3 +- solver/src/solver/parallel/parallel_solver.rs | 39 +++++++++++++++ solver/src/solver/solver_impl.rs | 50 ++++++++++++++++++- solver/src/solver/stats.rs | 44 ++++++++++++++++ solver/src/utils/statistics.rs | 4 +- 14 files changed, 158 insertions(+), 14 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 0e4ada0df..70a6118ff 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -132,6 +132,7 @@ dependencies = [ "num-integer", "num-rational", "rand", + "serde", "smallvec", "streaming-iterator", "tracing", @@ -241,6 +242,7 @@ version = "0.1.0" dependencies = [ "anyhow", "aries", + "serde_json", "structopt", "varisat-dimacs", "varisat-formula", diff --git a/examples/sat/Cargo.toml b/examples/sat/Cargo.toml index 3ef194735..4d9a08ac6 100644 --- a/examples/sat/Cargo.toml +++ b/examples/sat/Cargo.toml @@ -11,7 +11,7 @@ aries = { path = "../../solver" } varisat-dimacs = "0.2.2" varisat-formula = "0.2.2" zip = { default-features = false, features = ["deflate"], version = "2.1.3" } - +serde_json = "*" [[bin]] name = "aries-sat" diff --git a/examples/sat/main.rs b/examples/sat/main.rs index c3e046d03..14d23d4de 100644 --- a/examples/sat/main.rs +++ b/examples/sat/main.rs @@ -8,6 +8,7 @@ use aries::solver::search::combinators::{RoundRobin, WithGeomRestart}; use aries::solver::search::conflicts::{ConflictBasedBrancher, Params}; use aries::solver::search::SearchControl; use aries::solver::Solver; +use aries::utils::SnapshotStatistics; use std::collections::HashMap; use std::fs::File; use std::io::Read; @@ -30,6 +31,10 @@ struct Opt { timeout: Option, #[structopt(long, short, default_value = "")] search: String, + + /// File to write JSON-encoded solver statistics + #[structopt(long = "stats-file")] + stats_file: Option, } enum Source { @@ -168,6 +173,11 @@ fn solve_multi_threads(model: Model, opt: &Opt, deadline: Option) -> Re } } } + if let Some(stats_path) = &opt.stats_file { + let stats = par_solver.snapshot_statistics(); + let mut stats_file = std::fs::File::create(stats_path)?; + serde_json::to_writer(&mut stats_file, &stats)?; + } par_solver.print_stats(); Ok(()) diff --git a/solver/Cargo.toml b/solver/Cargo.toml index 9a31dc602..b75440297 100644 --- a/solver/Cargo.toml +++ b/solver/Cargo.toml @@ -9,7 +9,7 @@ edition = "2021" [features] # if enabled, solver and theory statistics may be exported and imported using serde -export_stats = [ "dep:serde" ] +export_stats = [ "dep:serde", "serde/serde_derive" ] # If enabled, will instruct the the solver to count cpu cycles at various point of its execution. # The implementation relies to time-stamp counter and intrinsic for the x86_64 platform. diff --git a/solver/src/reasoners/cp/mod.rs b/solver/src/reasoners/cp/mod.rs index c7bded8a6..11fdadc5e 100644 --- a/solver/src/reasoners/cp/mod.rs +++ b/solver/src/reasoners/cp/mod.rs @@ -236,6 +236,7 @@ impl Theory for Cp { } } +#[cfg_attr(feature = "export_stats", derive(serde::Serialize, serde::Deserialize))] #[derive(Debug, PartialEq, Eq, Clone)] pub struct CpStatsSnapshot { pub num_constraints: usize, diff --git a/solver/src/reasoners/eq/dense.rs b/solver/src/reasoners/eq/dense.rs index 7f405ff94..ca3e53a78 100644 --- a/solver/src/reasoners/eq/dense.rs +++ b/solver/src/reasoners/eq/dense.rs @@ -876,8 +876,9 @@ impl Theory for DenseEqTheory { } } +#[cfg_attr(feature = "export_stats", derive(serde::Serialize, serde::Deserialize))] #[derive(Debug, Clone, PartialEq, Eq, Default)] -pub struct DenseEqTheoryStatsSnapshot { +pub struct EqTheoryStatsSnapshot { pub num_nodes: usize, pub num_edge_propagations: usize, pub num_edge_propagations_pos: usize, @@ -891,7 +892,7 @@ pub struct DenseEqTheoryStatsSnapshot { pub num_edge_propagation2_neg_pos: usize, } -impl std::fmt::Display for DenseEqTheoryStatsSnapshot { +impl std::fmt::Display for EqTheoryStatsSnapshot { fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { writeln!(f, "num nodes: {}", self.num_nodes)?; writeln!(f, "num edge props1 {}", self.num_edge_propagations)?; @@ -908,7 +909,7 @@ impl std::fmt::Display for DenseEqTheoryStatsSnapshot { } impl SnapshotStatistics for DenseEqTheory { - type Stats = DenseEqTheoryStatsSnapshot; + type Stats = EqTheoryStatsSnapshot; fn snapshot_statistics(&self) -> Self::Stats { Self::Stats { diff --git a/solver/src/reasoners/eq/split.rs b/solver/src/reasoners/eq/split.rs index 3b936fef8..ffbee5b26 100644 --- a/solver/src/reasoners/eq/split.rs +++ b/solver/src/reasoners/eq/split.rs @@ -1,7 +1,7 @@ use crate::backtrack::{Backtrack, DecLvl, DecisionLevelTracker}; use crate::core::state::{Domains, DomainsSnapshot, Explanation, InferenceCause}; use crate::core::{IntCst, Lit, VarRef}; -use crate::reasoners::eq::{DenseEqTheory, DenseEqTheoryStatsSnapshot, Node, ReifyEq}; +use crate::reasoners::eq::{DenseEqTheory, EqTheoryStatsSnapshot, Node, ReifyEq}; use crate::reasoners::{Contradiction, ReasonerId, Theory}; use crate::utils::SnapshotStatistics; use itertools::Itertools; @@ -19,12 +19,12 @@ pub struct SplitEqTheory { } impl SnapshotStatistics for SplitEqTheory { - type Stats = DenseEqTheoryStatsSnapshot; + type Stats = EqTheoryStatsSnapshot; fn snapshot_statistics(&self) -> Self::Stats { self.parts() .map(|part| part.snapshot_statistics()) - .reduce(|sum, next| DenseEqTheoryStatsSnapshot { + .reduce(|sum, next| EqTheoryStatsSnapshot { num_nodes: sum.num_nodes + next.num_nodes, num_edge_propagations: sum.num_edge_propagations + next.num_edge_propagations, num_edge_propagations_pos: sum.num_edge_propagations_pos + next.num_edge_propagations_pos, diff --git a/solver/src/reasoners/sat/sat_solver.rs b/solver/src/reasoners/sat/sat_solver.rs index 84559eb65..7dcd31199 100644 --- a/solver/src/reasoners/sat/sat_solver.rs +++ b/solver/src/reasoners/sat/sat_solver.rs @@ -722,6 +722,7 @@ impl Backtrack for SatSolver { } } +#[cfg_attr(feature = "export_stats", derive(serde::Serialize, serde::Deserialize))] #[derive(Debug, Clone, PartialEq, Eq)] pub struct SatSolverStatsSnapshot { pub num_clauses: usize, diff --git a/solver/src/reasoners/stn/theory.rs b/solver/src/reasoners/stn/theory.rs index 95b4a88d3..d76d6e555 100644 --- a/solver/src/reasoners/stn/theory.rs +++ b/solver/src/reasoners/stn/theory.rs @@ -115,6 +115,7 @@ struct Stats { num_theory_deactivations: u64, } +#[cfg_attr(feature = "export_stats", derive(serde::Serialize, serde::Deserialize))] #[derive(Clone, Debug, PartialEq, Eq)] pub struct StnStatSnapshot { pub num_nodes: u32, diff --git a/solver/src/reasoners/tautologies.rs b/solver/src/reasoners/tautologies.rs index 739ee1db9..70931d3a9 100644 --- a/solver/src/reasoners/tautologies.rs +++ b/solver/src/reasoners/tautologies.rs @@ -79,15 +79,16 @@ impl Theory for Tautologies { } } +#[cfg_attr(feature = "export_stats", derive(serde::Serialize, serde::Deserialize))] #[derive(Debug, Clone)] pub struct TautologiesStatSnapshot; + impl std::fmt::Display for TautologiesStatSnapshot { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { write!(f, "{}", std::any::type_name::()) } } - impl SnapshotStatistics for Tautologies { type Stats = TautologiesStatSnapshot; diff --git a/solver/src/solver/parallel/parallel_solver.rs b/solver/src/solver/parallel/parallel_solver.rs index be5ce73a0..efbdcee6e 100644 --- a/solver/src/solver/parallel/parallel_solver.rs +++ b/solver/src/solver/parallel/parallel_solver.rs @@ -2,7 +2,9 @@ use crate::model::extensions::{AssignmentExt, SavedAssignment, Shaped}; use crate::model::lang::IAtom; use crate::model::{Label, ModelShape}; use crate::solver::parallel::signals::{InputSignal, InputStream, OutputSignal, SolverOutput, ThreadID}; +use crate::solver::stats::SolverStatsSnapshot; use crate::solver::{Exit, Solver}; +use crate::utils::SnapshotStatistics; use crossbeam_channel::{select, Receiver, Sender}; use std::sync::Arc; use std::thread; @@ -310,6 +312,43 @@ impl ParSolver { } } +#[cfg_attr(feature = "export_stats", derive(serde::Serialize, serde::Deserialize))] +#[derive(Clone, Debug)] +pub enum WorkerStatsSnapshot { + /// The worker is running on another thread, we and we can't access its stats + Running, + + /// The worker has completed + Idle(SolverStatsSnapshot), + + /// The worker is in the process of stopping + Halting, +} + +#[cfg_attr(feature = "export_stats", derive(serde::Serialize, serde::Deserialize))] +#[derive(Clone, Debug)] +pub struct ParSolverStatsSnapshot { + pub solvers: Vec, +} + +impl SnapshotStatistics for ParSolver { + type Stats = ParSolverStatsSnapshot; + + fn snapshot_statistics(&self) -> Self::Stats { + Self::Stats { + solvers: self + .solvers + .iter() + .map(|solver| match solver { + Worker::Running(_) => WorkerStatsSnapshot::Running, + Worker::Halting => WorkerStatsSnapshot::Halting, + Worker::Idle(worker) => WorkerStatsSnapshot::Idle(worker.snapshot_statistics()), + }) + .collect(), + } + } +} + impl Shaped for ParSolver { fn get_shape(&self) -> &ModelShape { &self.base_model diff --git a/solver/src/solver/solver_impl.rs b/solver/src/solver/solver_impl.rs index 071524354..7a477c19e 100644 --- a/solver/src/solver/solver_impl.rs +++ b/solver/src/solver/solver_impl.rs @@ -22,6 +22,8 @@ use std::sync::Arc; use std::time::Instant; use tracing::instrument; +use super::stats::{SolverModuleStatSnapshot, SolverModuleStats, SolverStatsSnapshot}; + /// If true, decisions will be logged to the standard output. static LOG_DECISIONS: EnvParam = EnvParam::new("ARIES_LOG_DECISIONS", "false"); @@ -938,10 +940,54 @@ impl Solver { } impl SnapshotStatistics for Solver { - type Stats = Stats; + type Stats = SolverStatsSnapshot; fn snapshot_statistics(&self) -> Self::Stats { - self.stats.clone() + let modules = SolverModuleStatSnapshot { + sat: SolverModuleStats { + propagation_cycles: self.stats[ReasonerId::Sat].propagation_time.count(), + conflicts: self.stats[ReasonerId::Sat].conflicts, + propagation_loops: self.stats[ReasonerId::Sat].propagation_loops, + internal: self.reasoners.sat.snapshot_statistics(), + }, + diff: SolverModuleStats { + propagation_cycles: self.stats[ReasonerId::Diff].propagation_time.count(), + conflicts: self.stats[ReasonerId::Diff].conflicts, + propagation_loops: self.stats[ReasonerId::Sat].propagation_loops, + internal: self.reasoners.diff.snapshot_statistics(), + }, + cp: SolverModuleStats { + propagation_cycles: self.stats[ReasonerId::Cp].propagation_time.count(), + conflicts: self.stats[ReasonerId::Cp].conflicts, + propagation_loops: self.stats[ReasonerId::Cp].propagation_loops, + internal: self.reasoners.cp.snapshot_statistics(), + }, + eq: SolverModuleStats { + propagation_cycles: self.stats[ReasonerId::Eq(0)].propagation_time.count(), + conflicts: self.stats[ReasonerId::Eq(0)].conflicts, + propagation_loops: self.stats[ReasonerId::Eq(0)].propagation_loops, + internal: self.reasoners.eq.snapshot_statistics(), + }, + tautologies: SolverModuleStats { + propagation_cycles: self.stats[ReasonerId::Tautologies].propagation_time.count(), + conflicts: self.stats[ReasonerId::Tautologies].conflicts, + propagation_loops: self.stats[ReasonerId::Tautologies].propagation_loops, + internal: self.reasoners.tautologies.snapshot_statistics(), + }, + }; + + Self::Stats { + init_time: self.stats.init_time, + init_cycles: self.stats.init_cycles.count(), + solve_time: self.stats.solve_time, + solve_cycles: self.stats.solve_cycles.count(), + num_decisions: self.stats.num_decisions, + num_conflicts: self.stats.num_conflicts, + num_restarts: self.stats.num_restarts, + num_solutions: self.stats.num_solutions, + propagation_cycles: self.stats.propagation_time.count(), + modules, + } } } diff --git a/solver/src/solver/stats.rs b/solver/src/solver/stats.rs index 7a7ebb303..c1fbe7d4a 100644 --- a/solver/src/solver/stats.rs +++ b/solver/src/solver/stats.rs @@ -1,5 +1,10 @@ use crate::backtrack::DecLvl; use crate::core::{IntCst, Lit}; +use crate::reasoners::cp::CpStatsSnapshot; +use crate::reasoners::eq::EqTheoryStatsSnapshot; +use crate::reasoners::sat::SatSolverStatsSnapshot; +use crate::reasoners::stn::theory::StnStatSnapshot; +use crate::reasoners::tautologies::TautologiesStatSnapshot; use crate::reasoners::ReasonerId; use crate::reasoners::REASONERS; use crate::utils::cpu_time::*; @@ -232,3 +237,42 @@ impl IndexMut for Stats { self.per_module_stat.get_mut(&index).unwrap() } } + +#[cfg_attr(feature = "export_stats", derive(serde::Serialize, serde::Deserialize))] +#[derive(Clone, Debug)] +pub struct SolverModuleStatSnapshot { + pub sat: SolverModuleStats, + pub diff: SolverModuleStats, + pub cp: SolverModuleStats, + pub eq: SolverModuleStats, + pub tautologies: SolverModuleStats, +} + +#[cfg_attr(feature = "export_stats", derive(serde::Serialize, serde::Deserialize))] +#[derive(Clone, Debug)] +pub struct SolverStatsSnapshot { + pub init_time: Duration, + pub init_cycles: Option, + + pub solve_time: Duration, + pub solve_cycles: Option, + + pub num_decisions: u64, + pub num_conflicts: u64, + pub num_restarts: u64, + pub num_solutions: u64, + + pub propagation_cycles: Option, + pub modules: SolverModuleStatSnapshot, +} + +#[cfg_attr(feature = "export_stats", derive(serde::Serialize, serde::Deserialize))] +#[derive(Clone, Default, Debug)] +pub struct SolverModuleStats { + pub propagation_cycles: Option, + pub conflicts: u64, + pub propagation_loops: u64, + + /// Statistics that were recorded by this module. + pub internal: InteranlStatsT, +} diff --git a/solver/src/utils/statistics.rs b/solver/src/utils/statistics.rs index 61533ed15..15d6abf13 100644 --- a/solver/src/utils/statistics.rs +++ b/solver/src/utils/statistics.rs @@ -1,10 +1,8 @@ - - /// Implementors of this trait can export a snapshot of their runtime statistics. /// The exported data must be able to _at least_ be formatted using std::fmt::Display. /// Ideally, it should also implement serde traits when `export_stats` feature is enabled. pub trait SnapshotStatistics { - type Stats: Sized + std::fmt::Display; + type Stats: Sized + std::fmt::Debug; fn snapshot_statistics(&self) -> Self::Stats; }