Struct Context 

pub struct Context {
    pub terms: TermManager,
    /* private fields */
}

Solver context for managing the solving process

The Context provides a high-level API for SMT solving, similar to the SMT-LIB2 standard. It manages declarations, assertions, and solver state.

Examples

Basic Usage

use oxiz_solver::Context;

let mut ctx = Context::new();
ctx.set_logic("QF_UF");

// Declare boolean constants
let p = ctx.declare_const("p", ctx.terms.sorts.bool_sort);
let q = ctx.declare_const("q", ctx.terms.sorts.bool_sort);

// Assert p AND q
let formula = ctx.terms.mk_and(vec![p, q]);
ctx.assert(formula);

// Check satisfiability
ctx.check_sat();

SMT-LIB2 Script Execution

use oxiz_solver::Context;

let mut ctx = Context::new();

let script = r#"
(set-logic QF_LIA)
(declare-const x Int)
(assert (>= x 0))
(assert (<= x 10))
(check-sat)
"#;

let _ = ctx.execute_script(script);

Fields

terms: TermManager

Term manager

Implementations

impl Context

pub fn new() -> Self

Create a new context

pub fn declare_const(&mut self, name: &str, sort: SortId) -> TermId

Declare a constant

pub fn declare_fun( &mut self, name: &str, arg_sorts: Vec<SortId>, ret_sort: SortId, )

Declare a function

Registers a function signature in the context. For nullary functions (constants), use declare_const instead.

pub fn get_fun_signature(&self, name: &str) -> Option<(Vec<SortId>, SortId)>

Get function signature if it exists

pub fn set_logic(&mut self, logic: &str)

Set the logic

pub fn logic(&self) -> Option<&str>

Get the current logic

pub fn assert(&mut self, term: TermId)

Add an assertion

pub fn check_sat(&mut self) -> SolverResult

Check satisfiability

pub fn get_model(&self) -> Option<Vec<(String, String, String)>>

Get the model (if SAT) Returns a list of (name, sort, value) tuples

pub fn format_model(&self) -> String

Format the model as SMT-LIB2

pub fn push(&mut self)

Push a context level

pub fn pop(&mut self)

Pop a context level with incremental declaration removal

pub fn reset(&mut self)

Reset the context

pub fn reset_assertions(&mut self)

Reset assertions (keep declarations and options)

pub fn get_assertions(&self) -> &[TermId]

Get all current assertions

pub fn format_assertions(&self) -> String

Format assertions as SMT-LIB2

pub fn set_option(&mut self, key: &str, value: &str)

Set an option

pub fn get_option(&self, key: &str) -> Option<&str>

Get an option

pub fn get_assignment(&self) -> String

Get assignment (for propositional variables with :named attribute) Returns an empty list as we don’t track named literals yet

pub fn get_proof(&self) -> String

Get proof (if proof generation is enabled and result is unsat)

pub fn get_statistics(&self) -> String

Get solver statistics Returns statistics about the last solving run

pub fn execute_script(&mut self, script: &str) -> Result<Vec<String>>

Execute an SMT-LIB2 script

pub fn stats(&self) -> &SolverStats

Get solver statistics

Trait Implementations

impl Debug for Context

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

Formats the value using the given formatter.

impl Default for Context

fn default() -> Self

Returns the “default value” for a type.