Struct SolverService 

pub struct SolverService { /* private fields */ }

Incremental SAT/MaxSAT service facade.

Implementations

impl SolverService

pub fn new(instance: SolveInstance) -> Self

Create a service for an instance.

pub fn assume(&mut self, literal: Literal) -> usize

Add an assumption and return its token.

pub fn retract_assumption(&mut self, token: usize) -> bool

Retract an assumption by token.

pub fn solve(&self) -> SolverServiceResult

Solve with exhaustive search.

pub fn solve_with_budget( &self, budget: SolverServiceBudget, ) -> SolverServiceResult

Solve with a bounded search budget.

pub fn transfer_learned_clauses_to( &self, target: &mut SolverService, ) -> LearnedClauseTransfer

Transfer learned clauses to another service.

pub fn trace(&self) -> SolverServiceTrace

Return current service trace.

pub fn gpu_portfolio_status(&self) -> SolverPortfolioStatus

Report that the semantic-oracle facade is not the GPU portfolio path.