use clap::Parser;
use demystify::{
named_strategy,
problem::{
self,
planner::{MusMethod, PlannerConfig, PuzzlePlanner},
solver::{MusConfig, PuzzleSolver, SolverConfig},
util::exec::{RunMethod, set_run_method},
},
stats::{print_mus_stats, print_sat_stats},
web::{base_css, base_javascript},
};
use std::{fs::File, path::PathBuf, sync::Arc};
use tracing_subscriber::fmt::format::FmtSpan;
use tracing_subscriber::prelude::*;
#[derive(clap::Parser, Debug)]
#[command(
about = "Explain a constraint puzzle step by step.",
long_about = "Reads an Essence Prime model + parameter file, computes minimal \
explanations (MUSes) for each deduction, and emits HTML, JSON, or a \
debug-formatted trace.\n\n\
Flag categories (see `--help` for full descriptions):\n \
Required: --model, --param (or --load-parsed instead)\n \
Output: --html, --json\n \
MUS tuning: --merge, --skip, --no-expand, --all-muses,\n \
--mus-method, --max-steps\n \
Performance: --searches, --conflict-limit, --conjure\n \
Persistence: --save-parsed, --load-parsed, --pin-assignment\n \
Logging: --trace, --log, --quiet, --verbose\n \
Database: --strategy-db\n\n\
Environment:\n \
DEMYSTIFY_PARSE_CACHE Parsed puzzles are cached (keyed by model+param\n \
content and tool/library versions) to skip Conjure/Savile\n \
Row on repeat runs. Default: a SQLite DB under the OS temp\n \
dir. Set to a directory to relocate it, or to `off` to\n \
disable."
)]
struct Opt {
#[arg(
long,
help = "Path to the Essence Prime model (`.eprime` / `.essence`)"
)]
model: String,
#[arg(long, help = "Path to the parameter file (`.param`)")]
param: String,
#[arg(
long,
default_value_t = 1,
help = "Merge MUSes of this size or smaller together in a single step (set to -1 to disable)"
)]
merge: i64,
#[arg(
long,
default_value_t = 0,
help = "Skip MUSes of this size or smaller (set to -1 to disable)"
)]
skip: i64,
#[arg(
long,
help = "Greedy mode: find the largest MUS (the puzzle's difficulty) as fast \
as possible. Like --merge but with a threshold that auto-discovers the \
difficulty — each step applies every deduction whose MUS is at or below \
the largest size seen so far, paying the full smallest-MUS search only \
when forced to raise that maximum. Output stays readable (every shown \
MUS is minimised)."
)]
greedy: bool,
#[arg(
long,
help = "Write a full trace log to `demystify.trace` (all targets, all levels)"
)]
trace: bool,
#[arg(long, help = "Emit a single self-contained HTML page on stdout")]
html: bool,
#[arg(
long,
help = "Only target positive value-assignment lits; never individual `!=` lits"
)]
only_assign: bool,
#[arg(
long,
help = "Cap parallel MUS searches per round (advanced; usually leave unset)"
)]
searches: Option<i64>,
#[arg(long, help = "Stop after this many solve steps")]
max_steps: Option<usize>,
#[arg(
long,
help = "Find all MUSes (disables find_one optimization that stops after the first MUS per batch)"
)]
all_muses: bool,
#[arg(long, help = "Suppress progress and statistics output on stderr")]
quiet: bool,
#[arg(long, help = "Disable expanding a MUS to all literals it can deduce")]
no_expand: bool,
#[arg(
long,
help = "Emit each solve step as a JSON object (instead of the default debug format)"
)]
json: bool,
#[arg(
long,
help = "After solving, print a final line to stdout reporting solvability: \
`SOLVABILITY unsolved=N` where N is the number of solution literals not \
pinned to a single value (0 = uniquely solvable), or `SOLVABILITY inconsistent`."
)]
report_solvability: bool,
#[arg(
long,
value_enum,
help = "Specify the method to run the solver (Native, Docker, Podman)"
)]
conjure: Option<RunMethod>,
#[arg(
long,
help = "Save the parsed puzzle to a JSON file (for use with Lua interface or to skip parsing later)"
)]
save_parsed: Option<PathBuf>,
#[arg(
long,
help = "Load a pre-parsed puzzle from JSON instead of parsing .eprime/.param files"
)]
load_parsed: Option<PathBuf>,
#[arg(
long,
help = "Pin an externally-generated puzzle assignment (JSON) onto the model as known givens. \
Accepts either a bare assignment object {\"puz_grid\": {...}, ...} or a full mystify \
output JSON (the assignment is read from its top-level `puzzle` key). Use this with \
models — such as mystify's — whose clue cells are `find` variables that a .param file \
cannot assign."
)]
pin_assignment: Option<PathBuf>,
#[arg(
long,
default_value_t = 1000,
help = "Per-SAT-call conflict limit (0 = no limit). Default 1000."
)]
conflict_limit: i64,
#[arg(
long,
value_enum,
default_value_t = MusMethod::default(),
help = "MUS generation algorithm: core (raw cores only), mus (standard MUS search), core+mus (hybrid: size-1 pass, cores, then full MUS if needed)"
)]
mus_method: MusMethod,
#[arg(
long,
value_delimiter = ',',
help = "Enable logging targets on stderr (comma-separated). Available: progress, cores, solver, planner, solve, parser"
)]
log: Vec<String>,
#[arg(
long,
help = "Path to the named-strategy database directory. Each <KIND>.toml file inside defines named techniques for that puzzle kind. Defaults to <crate>/named-strategies."
)]
strategy_db: Option<PathBuf>,
#[arg(
long,
help = "Attach diagnostic sections (e.g. current $#VAR domains) to every rendered step. Visible in --html output as a collapsible 'Verbose diagnostics' block."
)]
verbose: bool,
}
fn main() -> anyhow::Result<()> {
let opt = Opt::parse();
if !opt.quiet {
eprintln!(
"[demystify] running with defaults; use --help for output, MUS-tuning, \
logging, and database flags."
);
}
let mut _trace_guard = None;
if let Some(method) = opt.conjure {
set_run_method(method);
}
demystify::satcore::set_global_conflict_limit(opt.conflict_limit);
{
let trace_layer = if opt.trace {
let (non_block, guard) =
tracing_appender::non_blocking(File::create("demystify.trace")?);
_trace_guard = Some(guard);
Some(
tracing_subscriber::fmt::layer()
.with_span_events(FmtSpan::ACTIVE)
.with_ansi(false)
.without_time()
.with_writer(non_block)
.with_filter(tracing_subscriber::filter::LevelFilter::TRACE),
)
} else {
None
};
let mut log_targets = opt.log.clone();
if !opt.quiet && !log_targets.contains(&"progress".to_string()) {
log_targets.push("progress".to_string());
}
let log_layer = if !log_targets.is_empty() {
let filter_str = log_targets
.iter()
.map(|t| format!("{}=info", t.trim()))
.collect::<Vec<_>>()
.join(",");
Some(
tracing_subscriber::fmt::layer()
.with_writer(std::io::stderr)
.with_target(false)
.with_level(false)
.without_time()
.with_filter(tracing_subscriber::filter::EnvFilter::new(filter_str)),
)
} else {
None
};
tracing_subscriber::registry()
.with(trace_layer)
.with(log_layer)
.init();
}
let puzzle = if let Some(ref load_path) = opt.load_parsed {
eprintln!("Loading pre-parsed puzzle from {:?}", load_path);
problem::parse::PuzzleParse::load_from_json(load_path)?
} else {
problem::parse::parse_essence(&PathBuf::from(&opt.model), &PathBuf::from(&opt.param))?
};
if let Some(ref save_path) = opt.save_parsed {
eprintln!("Saving parsed puzzle to {:?}", save_path);
puzzle.save_to_json(save_path)?;
eprintln!("Saved successfully.");
}
let puzzle = Arc::new(puzzle);
let mut solver = PuzzleSolver::new_with_config(
puzzle,
SolverConfig {
only_assignments: opt.only_assign,
},
)?;
if let Some(ref pin_path) = opt.pin_assignment {
eprintln!("Pinning puzzle assignment from {:?}", pin_path);
let json: serde_json::Value =
serde_json::from_reader(std::io::BufReader::new(File::open(pin_path)?))
.map_err(|e| anyhow::anyhow!("reading {pin_path:?}: {e}"))?;
let assignment = if json.get("puzzle").is_some() {
problem::parse::mystify_puzzle_assignment(&json)?
} else {
&json
};
solver.pin_assignment(assignment)?;
if !solver.is_currently_solvable() {
anyhow::bail!(
"the pinned puzzle assignment makes the model unsatisfiable — \
either the assignment is inconsistent or it does not match this model"
);
}
}
let mus_config: MusConfig = {
let mut cfg = if let Some(searches) = opt.searches {
MusConfig::new_with_repeats(searches)
} else {
MusConfig::default()
};
if opt.all_muses {
cfg.find_one = false;
}
cfg
};
let planner_config = PlannerConfig {
mus_config,
merge_small_threshold: opt.merge,
skip_small_threshold: opt.skip,
expand_to_all_deductions: !opt.no_expand,
max_steps: opt.max_steps,
mus_method: opt.mus_method,
verbose: opt.verbose,
};
let strategy_db = named_strategy::load_or_discover(opt.strategy_db.as_deref())?;
let mut planner =
PuzzlePlanner::new_with_config(solver, planner_config).with_database(strategy_db);
let t_solve = demystify::time::Instant::now();
if opt.html {
let html = if opt.greedy {
planner.quick_solve_greedy_html()
} else {
planner.quick_solve_html()
};
println!(
"<html> <head> <style> {} </style> <script> {} </script> </head>",
base_css(),
base_javascript()
);
println!("<body> {html}");
println!("<script> doJavascript(); </script>");
println!("</body> </html>");
} else {
let steps = if opt.greedy {
planner.quick_solve_greedy()
} else {
planner.quick_solve()
};
if opt.json {
for step in steps {
let json_step: Vec<serde_json::Value> = step
.iter()
.map(|um| {
serde_json::json!({
"lits": um.lits,
"constraints": um.constraints,
"fingerprint": um.fingerprint,
"name": um.name,
})
})
.collect();
println!("{}", serde_json::to_string(&json_step).unwrap());
}
} else {
for p in steps {
println!("{p:?}");
}
}
}
let solve_secs = t_solve.elapsed().as_secs_f64();
tracing::info!(target: "progress", "solve completed in {solve_secs:.2}s");
if opt.report_solvability {
match planner.check_solvability() {
Some(unsolved) => println!("SOLVABILITY unsolved={unsolved}"),
None => println!("SOLVABILITY inconsistent"),
}
}
if !opt.quiet {
print_mus_stats();
print_sat_stats();
demystify::satcore::print_phase_breakdown();
}
Ok(())
}