Struct SolveResult 

pub struct SolveResult {
    pub status: SolveStatus,
    pub proof: SolveProof,
    pub stats: SolveStats,
}

Complete result from a solve operation.

Combines the solve status, proof artifact, and statistics into a single comprehensive result structure.

Construction

Use the constructor methods for common result types:

use xlog_solve::{SolveResult, SolveStats};

// Satisfiable result
let sat = SolveResult::satisfiable(vec![true, false, true]);
assert!(sat.is_sat());

// Unsatisfiable result
let unsat = SolveResult::unsatisfiable();
assert!(unsat.is_unsat());

// Unknown result (e.g., timeout)
let unknown = SolveResult::unknown(1000);
assert!(!unknown.is_sat());

// With custom statistics
let stats = SolveStats::new(100, 5000, 1024);
let result = SolveResult::satisfiable(vec![true]).with_stats(stats);

Example

use xlog_solve::SolveResult;

let result = SolveResult::satisfiable(vec![true, false]);

if result.is_sat() {
    if let Some(assignment) = result.assignment() {
        println!("Found assignment: {:?}", assignment);
    }
}

Fields

status: SolveStatus

The solve status (SAT, UNSAT, Unknown, Optimal).

proof: SolveProof

The proof artifact from solving.

stats: SolveStats

Statistics from the solve operation.

Implementations

impl SolveResult

pub fn satisfiable(assignment: Vec<bool>) -> Self

Creates a satisfiable result with the given assignment.

Automatically computes a checksum for the assignment.

Arguments

• assignment - The satisfying assignment

Example

use xlog_solve::SolveResult;

let result = SolveResult::satisfiable(vec![true, false, true]);
assert!(result.is_sat());

pub fn unsatisfiable() -> Self

Creates an unsatisfiable result.

Example

use xlog_solve::SolveResult;

let result = SolveResult::unsatisfiable();
assert!(result.is_unsat());

pub fn unknown(iterations: u32) -> Self

Creates an unknown result (e.g., timeout).

Arguments

• iterations - Number of iterations performed before giving up

Example

use xlog_solve::SolveResult;

let result = SolveResult::unknown(1000);
assert!(!result.is_sat());
assert!(!result.is_unsat());

pub fn optimal(assignment: Vec<bool>, optimal_value: u64) -> Self

Creates an optimal result (for MaxSAT).

Arguments

• assignment - The optimal assignment
• optimal_value - The optimal objective value

Example

use xlog_solve::{SolveResult, SolveStatus};

let result = SolveResult::optimal(vec![true, false], 42);
assert!(matches!(result.status, SolveStatus::Optimal(42)));

pub fn approximate( assignment: Vec<bool>, satisfied_clauses: u32, total_clauses: u32, iterations: u32, ) -> Self

Creates an approximate result from an incomplete solver.

Arguments

• assignment - The best assignment found
• satisfied_clauses - Number of satisfied clauses
• total_clauses - Total number of clauses
• iterations - Number of solver iterations

Example

use xlog_solve::SolveResult;

let result = SolveResult::approximate(vec![true, false], 8, 10, 1000);
assert!(!result.is_sat());  // Not definitively SAT

pub fn with_stats(self, stats: SolveStats) -> Self

Updates the statistics, consuming and returning self.

Arguments

• stats - The new statistics

Example

use xlog_solve::{SolveResult, SolveStats};

let stats = SolveStats::new(100, 5000, 1024);
let result = SolveResult::satisfiable(vec![true]).with_stats(stats);
assert_eq!(result.stats.iterations, 100);

pub fn is_sat(&self) -> bool

Returns true if the result is satisfiable.

Example

use xlog_solve::SolveResult;

assert!(SolveResult::satisfiable(vec![true]).is_sat());
assert!(!SolveResult::unsatisfiable().is_sat());

pub fn is_unsat(&self) -> bool

Returns true if the result is unsatisfiable.

Example

use xlog_solve::SolveResult;

assert!(SolveResult::unsatisfiable().is_unsat());
assert!(!SolveResult::satisfiable(vec![true]).is_unsat());

pub fn assignment(&self) -> Option<&[bool]>

Returns the assignment if one is available.

Example

use xlog_solve::SolveResult;

let result = SolveResult::satisfiable(vec![true, false]);
assert_eq!(result.assignment(), Some(&[true, false][..]));

pub fn optimal_value(&self) -> Option<u64>

Returns the optimal value if this is a MaxSAT result.

Example

use xlog_solve::SolveResult;

let result = SolveResult::optimal(vec![true], 42);
assert_eq!(result.optimal_value(), Some(42));

pub fn verify_proof(&self) -> Option<bool>

Verifies the integrity of the proof checksum.

Returns Some(true) if the checksum is valid, Some(false) if corrupted, or None if verification is not applicable.

Example

use xlog_solve::SolveResult;

let result = SolveResult::satisfiable(vec![true, false]);
assert_eq!(result.verify_proof(), Some(true));

Trait Implementations

impl Clone for SolveResult

fn clone(&self) -> SolveResult

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for SolveResult

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for SolveResult

fn default() -> Self

Returns the “default value” for a type.