Diff Coverage

    value: &Literal,
) -> Option<Literal> {
    if matches!(reference_domain, Some(GroundDomain::Bool)) {
        return match value {
            Literal::Bool(x) => Some(Literal::Bool(*x)),
            Literal::Int(1) => Some(Literal::Bool(true)),
            Literal::Int(0) => Some(Literal::Bool(false)),
            _ => None,
        };
    }

    Some(value.clone())

    }

    Some(value.clone())
}

fn substitute_from_solution(
    expr: &Expression,
    previous_solution: &BTreeMap<Name, Literal>,
) -> Option<Expression> {

    solver_input_file: &Option<PathBuf>,
) -> Result<Vec<BTreeMap<Name, Literal>>, anyhow::Error> {
    let dominance_expression = model.dominance.as_ref().map(|expr| match expr {
        Expression::DominanceRelation(_, inner) => inner.as_ref().clone(),
        _ => expr.clone(),
    });

    let adaptor_name = solver.get_name();

    rule_sets: &Vec<&'a RuleSet<'a>>,
    configured_rewriter: Rewriter,
) -> Result<Model, RewriteError> {
    match configured_rewriter {
        Rewriter::Morph => Ok(rewrite_morph(model, rule_sets, false)),
        Rewriter::Naive => rewrite_naive(&model, rule_sets, false),
    }
}

            if reprs.is_empty() {
                return None;
            }
            if reprs.len() > 1 || reprs[0].len() != 1 {
                return None;
            }
            Some((name, reprs[0][0].clone()))
        })
        .collect_vec();

        .into_iter()
        .collect::<BTreeMap<Name, Literal>>();
    for (name, representation) in representations {
        let Ok(value) = representation.value_up(&solution_btree) else {
            continue;
        };
        solution.insert(name.clone(), value.clone());
        solution_btree.insert(name, value);
    }

            return Ok(());
        };

        let Some(model_template) = dominance_model_template else {
            return Ok(());
        };

        use uniplate::Uniplate;

        let rewritten_dominance =
            dominance_expression.rewrite(&|e| sub_in_solution_into_dominance_expr(&e, solution));

        let mut dominance_model = model_template.clone();
        dominance_model.replace_constraints(vec![]);
        dominance_model.replace_clauses(vec![]);
        dominance_model.dominance = None;

            rewrite_model_with_configured_rewriter(dominance_model, &rule_sets, current_rewriter())
                .map_err(|e| {
                    SolverError::Runtime(format!(
                        "Failed to rewrite dominance constraint into CNF clauses: {e}"
                    ))
                })?;

        for clause in rewritten.clauses() {
            let mut missing_refs: Vec<Name> = Vec::new();
            let mut largest_new_var: Option<satVar> = None;
            for literal in clause.iter() {
                let maybe_name = match literal {
                    Expression::Atomic(_, Atom::Reference(reference)) => {
                        Some(reference.name().clone())
                    }
                    Expression::Not(_, inner) => {
                        if let Expression::Atomic(_, Atom::Reference(reference)) = inner.as_ref() {
                            Some(reference.name().clone())

                if let Some(name) = maybe_name
                    && !var_map.contains_key(&name)
                {
                    missing_refs.push(name);
                }
            }

            if !missing_refs.is_empty() {
                missing_refs.sort_by_key(|name| name.to_string());

                for name in &missing_refs {
                    if var_map.contains_key(name) {
                        continue;
                    }
                    let next_idx = var_map
                        .values()
                        .map(|lit| lit.var().idx32())
                        .max()
                        .map(|idx| idx + 1)
                        .unwrap_or(0);
                    let new_var = satVar::new(next_idx);
                    let new_lit = new_var.pos_lit();
                    var_map.insert(name.clone(), new_lit);
                    largest_new_var = Some(new_var);

                    let new_lit = new_var.pos_lit();
                    var_map.insert(name.clone(), new_lit);
                    largest_new_var = Some(new_var);
                }
            }

            if let Some(max_var) = largest_new_var {
                solver.reserve(max_var).map_err(|e| {
                    SolverError::Runtime(format!(
                        "Failed reserving SAT variable capacity up to {max_var} for dominance clauses: {e}"
                    ))
                })?;
            }

            if let Some(sat_clause) = cnf_clause_to_sat_clause(clause, var_map).map_err(|e| {

            }

            if let Some(sat_clause) = cnf_clause_to_sat_clause(clause, var_map).map_err(|e| {
                SolverError::Runtime(format!(
                    "Failed converting dominance CNF clause to SAT clause. clause={clause:?}; error={e}"
                ))
            })? {
                solver.add_clause(sat_clause).map_err(|e| {
                    SolverError::Runtime(format!(
                        "Failed adding dominance clause to SAT solver: {e}"
                    ))
                })?;
            }
        }

        Ok(())

        let dominance_expression = self.dominance_expression.clone();
        let dominance_model_template = self.dominance_model_template.clone();
        let mut solver = &mut self.solver_inst;
        let mut var_map = self.var_map.clone().ok_or_else(|| {
            SolverError::Runtime("Variable map is missing when retrieving solution".to_string())
        })?;

        let cnf: (Cnf, BasicVarManager) = self
            .model_inst
            .clone()

            .ok_or_else(|| SolverError::Runtime("Model instance is missing".to_string()))?
            .into_cnf();

        solver.add_cnf(cnf.0).map_err(|e| {
            SolverError::Runtime(format!("Failed adding CNF to SAT solver before solve: {e}"))
        })?;

        let mut has_sol = false;
        loop {
            let res = match solver.solve() {

                    dominance_model_template.as_ref(),
                    solver,
                    &dominance_solution,
                    &mut var_map,
                )?;
            }

            let blocking_vec: Vec<_> = sol.clone().iter().map(|lit| !lit).collect();
            let mut blocking_cl = Clause::new();

            for lit_i in blocking_vec {
                blocking_cl.add(lit_i);
            }
            solver.add_clause(blocking_cl).map_err(|e| {
                SolverError::Runtime(format!("Failed adding blocking clause to SAT solver: {e}"))
            })?;
        }
    }

    fn solve_mut(

    fn load_model(&mut self, model: ConjureModel, _: private::Internal) -> Result<(), SolverError> {
        self.dominance_expression = model.dominance.as_ref().map(|expr| match expr {
            Expression::DominanceRelation(_, inner) => inner.as_ref().clone(),
            _ => expr.clone(),
        });
        self.dominance_model_template = self.dominance_expression.as_ref().map(|_| model.clone());

        let sym_tab = model.symbols().deref().clone();

    names.sort();
    let total = names.len();
    let preview = names.into_iter().take(25).collect::<Vec<_>>().join(", ");
    format!("known_vars_total={total}; known_vars_preview=[{preview}]")
}

pub fn handle_lit(
    l1: &Expression,
    vars_added: &mut HashMap<Name, Lit>,

pub fn cnf_literal_to_sat_lit(
    literal: &Expression,
    var_map: &HashMap<Name, Lit>,
) -> Result<Option<Lit>, SolverError> {
    match literal {
        Expression::Atomic(_, Atom::Reference(reference)) => {
            let name = reference.name();
            let lit = var_map.get(&name).ok_or_else(|| {
                SolverError::Runtime(format!(
                    "CNF clause references unknown variable '{name}'. literal={literal:?}. {}",
                    var_map_debug_summary(var_map)
                ))
            })?;
            Ok(Some(*lit))
        }
        Expression::Not(_, inner) => {
            let Expression::Atomic(_, Atom::Reference(reference)) = inner.as_ref() else {
                return Err(SolverError::Runtime(
                    "CNF clause contains unsupported negated literal".to_string(),
                ));
            };
            let name = reference.name();
            let lit = var_map.get(&name).ok_or_else(|| {
                SolverError::Runtime(format!(
                    "CNF clause references unknown variable '{name}'. literal={literal:?}. {}",
                    var_map_debug_summary(var_map)
                ))
            })?;
            Ok(Some(!*lit))
        }
        Expression::Atomic(_, Atom::Literal(Literal::Bool(true))) => Ok(None),
        Expression::Atomic(_, Atom::Literal(Literal::Bool(false))) => Ok(None),
        _ => Err(SolverError::Runtime(format!(
            "CNF clause contains non-literal expression: {literal:?}"
        ))),
    }
}

pub fn cnf_clause_to_sat_clause(

    }

    if sat_clause.iter().next().is_none() && !has_false_only {
        // Empty after simplification and no explicit false literal => tautology.
        return Ok(None);
    }

    Ok(Some(sat_clause))
}

                let value = solution.get(&var_name)?;
                let value = if let Some(domain) = reference.resolved_domain() {
                    if domain.as_ref() == &GroundDomain::Bool {
                        match value {
                            Literal::Bool(x) => Literal::Bool(*x),
                            Literal::Int(1) => Literal::Bool(true),
                            Literal::Int(0) => Literal::Bool(false),
                            _ => return None,
                        }
                    } else {
                        value.clone()
                    }
                } else {
                    value.clone()
                };

                return Some(Expression::Atomic(Metadata::new(), Atom::Literal(value)));
            }
            Some(expr.clone())
        }
        _ => Some(expr.clone()),
    }

                        Literal::Int(0) => Literal::Bool(false),
                        _ => return None,
                    }
                } else {
                    value.clone()
                }
            } else {
                value.clone()
            };

            Metadata::new(),
            atom_expr.as_ref().clone(),
        )),
        _ => Some(expr.clone()),
    }
}

fn add_represented_decision_values(solution: &mut HashMap<Name, Literal>, model: &Model) {
    let symbols = model.symbols().clone();
    let names = symbols.clone().into_iter().map(|x| x.0).collect_vec();
    let representations = names
        .into_iter()
        .filter_map(|name| {
            symbols
                .representations_for(&name)
                .map(|reprs| (name, reprs))
        })
        .filter_map(|(name, reprs)| {

        .filter_map(|(name, reprs)| {
            if reprs.is_empty() {
                return None;
            }
            if reprs.len() > 1 || reprs[0].len() != 1 {
                return None;
            }
            Some((name, reprs[0][0].clone()))
        })
        .collect_vec();

    if representations.is_empty() {
        return;
    }

    let mut solution_btree = solution
        .clone()
        .into_iter()
        .collect::<BTreeMap<Name, Literal>>();
    for (name, representation) in representations {
        let Ok(value) = representation.value_up(&solution_btree) else {
            continue;
        };
        solution.insert(name.clone(), value.clone());
        solution_btree.insert(name, value);
    }
}

fn extract_z3_version(full_version: &str) -> Result<&str, SolverError> {
    match full_version.strip_prefix("Z3 ") {
        Some(v) => v.split_whitespace().next().ok_or_else(|| {

            return Ok(());
        };

        let Some(model_template) = dominance_model_template else {
            return Ok(());
        };

        // Block future solutions dominated by the current solution:
        // assert NOT dominance(current_solution, future_solution).

        let rule_sets = dominance_model.context.read().unwrap().rule_sets.clone();
        let rewritten =
            rewrite_model_with_configured_rewriter(dominance_model, &rule_sets, current_rewriter())
                .map_err(|e| {
                    SolverError::Runtime(format!(
                        "Failed to rewrite dominance constraint for SMT solving: {e}"
                    ))
                })?;

        load_model_impl(
            store,
            solver,

                    true,
                    |solver, store, instance| {
                        let mut dominance_solution = match instance.as_literals_map() {
                            Ok(solution) => solution,
                            Err(err) => {
                                hook_error = Some(err);
                                return false;
                            }
                        };
                        if let Some(model_template) = dominance_model_template.as_ref() {
                            add_represented_decision_values(
                                &mut dominance_solution,
                                model_template,
                            );
                        }

                        match Smt::add_dominance_constraints_for_solution(
                            dominance_expression.as_ref(),

                            theory_config,
                            &dominance_solution,
                        ) {
                            Ok(()) => true,
                            Err(err) => {
                                hook_error = Some(err);
                                false
                            }
                        }
                    },
                );

                    .count();

                drop(solutions);
                if let Some(err) = hook_error {
                    return Err(err);
                }

                let search_complete = if found_solution {
                    SearchComplete::HasSolutions

        // Fail fast if an older system or precompiled Z3 was linked in.
        ensure_supported_z3_runtime()?;
        self.dominance_expression = model.dominance.as_ref().map(|expr| match expr {
            Expression::DominanceRelation(_, inner) => inner.as_ref().clone(),
            _ => expr.clone(),
        });
        self.dominance_model_template = self.dominance_expression.as_ref().map(|_| model.clone());
        load_model_impl(
            &mut self.store,

    type Item = (T::ModelInstance, Statistics);

    fn next(&mut self) -> Option<Self::Item> {
        if self.done {
            return None;
        }

        match self.solver.check() {
            SatResult::Sat => {

                let instance = self.ast.read_from_model(&model, self.model_completion)?;
                let counterexample = self.ast.generate_constraint(&instance);

                if !(self.on_solution)(&mut self.solver, &mut self.ast, &instance) {
                    self.done = true;
                    return None;
                }

                self.solver.assert(counterexample);
                Some((instance, stats))

            tracing::subscriber::with_default(subscriber, || {
                rewrite_naive(&model, &rule_sets, false)
            })?
        }
        Rewriter::Naive => rewrite_naive(&model, &rule_sets, false)?,
        Rewriter::Morph => {
            let submodel = &mut model;
            let rules_grouped = get_rules_grouped(&rule_sets)

        // Always overwrite these ones. Unlike the rest, we don't need to selectively do these
        // based on the test results, so they don't get done later.
        copy_generated_to_expected(path, case_name, "solutions", "json", solver_fam)?;
        if should_validate_rule_trace {
            copy_human_trace_generated_to_expected(path, case_name, solver_fam)?;
        }
    }

    // Check Stage 3a (solutions)
    let expected_solutions_json = read_solutions_json(path, case_name, "expected", solver_fam)?;