Struct Question 

pub struct Question { /* private fields */ }

A question, blasted and encoded once, then decided in as many steps as its caller likes: a search that ends on its limits stops where it is, keeping what it learned, and the next solve goes on from there. Asking under 5,000 conflicts, then 15,000 more, costs what asking under 20,000 once does, and answers the same.

use bitwright::prove::{Config, Limits, Outcome, Question};
use bitwright::{Context, ParseOptions, Width};

let mut cx = Context::new();
let o = ParseOptions::width(Width::W16);
let p = cx.parse("x * x != 0x1234", &o)?;
let mut q = Question::valid(&mut cx, p, &Config::default().with_samples(0))?;
let mut out = q.solve(&mut cx, Limits::conflicts(10))?;
while let Outcome::Unknown(why) = &out {
    assert!(why.is_budget());
    out = q.solve(&mut cx, Limits::conflicts(10))?;
}
assert!(matches!(out, Outcome::Proved(_))); // 0x1234 is not a square mod 2^16
assert!(q.stats().conflicts > 0);

Implementations

impl Question

pub fn valid(cx: &mut Context, p: Expr, cfg: &Config) -> Result<Question, Error>

Whether the 1-bit p is true for every value of its symbols agreeing with their declared known bits.

pub fn equal( cx: &mut Context, a: Expr, b: Expr, cfg: &Config, ) -> Result<Question, Error>

Whether a and b (of one width) are equal for every value of their symbols agreeing with their declared known bits.

pub fn valid_under( cx: &mut Context, p: Expr, assumptions: Option<&Assumptions>, cfg: &Config, ) -> Result<Question, Error>

Whether p is true wherever the constraints of assumptions hold. Complete original facts are retained, including partial masks, signed/unsigned intervals and unsigned strides; they remain in certificates and counterexample replay. The question is simplified (see Config::simplify), optionally sampled at the word level, then blasted, sampled (see Config::samples) and encoded here; each stage may decide it.

pub fn valid_with_pairs( cx: &mut Context, p: Expr, pairs: &[CheckedPair], cfg: &Config, ) -> Result<Question, Error>

Ask the original question after applying explicitly supplied, exhaustively checked finite-domain pair facts. Verification costs are separate from this query’s budget. Models are replayed on the original predicate. Certificate requests retain the original bit-blast path and do not use these word-level facts.

pub fn valid_under_with_pairs( cx: &mut Context, p: Expr, assumptions: Option<&Assumptions>, pairs: &[CheckedPair], cfg: &Config, ) -> Result<Question, Error>

valid_with_pairs under explicit assumptions.

pub fn solve( &mut self, cx: &mut Context, limits: Limits, ) -> Result<Outcome, Error>

Searches within limits more work (counted from this call): the answer, or Unknown::Budget with the work done on the question so far, and the next call goes on from there. Once decided (here or when built), the answer is kept and returned again. cx is the context the question was built in.

pub fn outcome(&self) -> Option<&Outcome>

The answer, once decided.

pub fn stats(&self) -> Stats

The work done on the question so far.

Trait Implementations

impl Debug for Question

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

Formats the value using the given formatter.