smtlib-rs

smtlib-rs copied to clipboard

In cvc5, there is theory solver for finite field arithmetic. I don't see the support for it now, is there future plan to support this?

DoHoonKim8

Feature request: SyGuS input format

3

Hi! Since CVC5 has a Syntax-Guided-Synthesis (SyGuS) engine, it would be really nice if it could be used in Rust! Currently the SyGuS input format is closely modeled after the...

Sicheng-Pan

Take the following example program: ``` use miette::IntoDiagnostic; use smtlib::{backend::Z3Binary, Real, Solver, Sort}; fn main() -> miette::Result { miette::set_panic_hook(); let mut solver = Solver::new(Z3Binary::new("z3").into_diagnostic()?)?; let x = Real::from_name("x"); let y...

rbtying

Support mixing low-level and high-level SMT APIs

3

Since not all of the functions are supported in the high-level API (e.g. bvsgt for bitvectors), would it be possible to allow exposing those by having the low-level AST be...

rbtying