Struct ArrayChecker 

pub struct ArrayChecker { /* private fields */ }

Array theory checker

Implementations

impl ArrayChecker

pub fn new() -> Self

Create a new array checker

pub fn without_extensionality() -> Self

Create with extensionality checking disabled

pub fn set_extensionality(&mut self, enabled: bool)

Enable/disable extensionality checking

Trait Implementations

impl Debug for ArrayChecker

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

Formats the value using the given formatter.

impl Default for ArrayChecker

fn default() -> Self

Returns the “default value” for a type.

impl TheoryChecker for ArrayChecker

fn name(&self) -> &'static str

Name of the theory

fn check_conflict(&self, clause: &[Literal]) -> CheckResult

Check a conflict clause

fn check_propagation( &self, literal: Literal, explanation: &[Literal], ) -> CheckResult

Check a propagation explanation

fn check_model(&self, assignments: &[(TermId, bool)]) -> CheckResult

Check that a model satisfies theory constraints

fn stats(&self) -> CheckerStats

Get statistics

fn reset_stats(&mut self)

Reset statistics

fn check_lemma(&self, clause: &[Literal]) -> CheckResult

Check a lemma (clause that should be T-valid)