pub fn grounded_grid_problem(input: &str) -> Option<(Vec<ProofExpr>, ProofExpr)>Expand description
The GROUNDED, quantifier-free grid problem (solver_input, goal) for an Auto grid
theorem — the EXACT problem compile_theorem_for_ui solves, exposed so the trust tiers
(Untrusted CDCL / RUP / Kernel) and the benchmark all run the same input. None if the
theorem is not an Auto finite-domain grid.