cvc5-rs 0.2.0

High-level Rust bindings for the cvc5 SMT solver
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71

//! # cvc5-rs
//!
//! Safe, high-level Rust bindings for the [cvc5](https://cvc5.github.io/) SMT solver.
//!
//! # Example
//!
//! ```no_run
//! use cvc5_rs::{TermManager, Solver, Kind};
//!
//! let tm = TermManager::new();
//! let mut solver = Solver::new(&tm);
//!
//! solver.set_logic("QF_LIA");
//! solver.set_option("produce-models", "true");
//!
//! let int_sort = tm.integer_sort();
//! let x = tm.mk_const(int_sort, "x");
//! let zero = tm.mk_integer(0);
//!
//! let gt = tm.mk_term(Kind::CVC5_KIND_GT, &[x.clone(), zero]);
//! solver.assert_formula(gt);
//!
//! let result = solver.check_sat();
//! assert!(result.is_sat());
//!
//! let x_val = solver.get_value(x);
//! println!("x = {x_val}");
//! ```

mod datatype;
mod grammar;
mod op;
#[cfg(feature = "parser")]
mod parser;
mod proof;
mod result;
mod solver;
mod sort;
mod statistics;
mod synth_result;
mod term;
mod term_manager;

pub use cvc5_sys::Cvc5Kind as Kind;
pub use cvc5_sys::Cvc5OptionInfo;
pub use cvc5_sys::Cvc5Plugin;
pub use cvc5_sys::Cvc5ProofRewriteRule as ProofRewriteRule;
pub use cvc5_sys::Cvc5ProofRule as ProofRule;
pub use cvc5_sys::Cvc5RoundingMode as RoundingMode;
pub use cvc5_sys::Cvc5SkolemId as SkolemId;
pub use cvc5_sys::Cvc5SortKind as SortKind;
pub use cvc5_sys::Cvc5UnknownExplanation as UnknownExplanation;

pub use datatype::{
    Datatype, DatatypeConstructor, DatatypeConstructorDecl, DatatypeDecl, DatatypeSelector,
};
pub use grammar::Grammar;
pub use op::Op;
pub use proof::Proof;
pub use result::Result;
pub use solver::Solver;
pub use sort::Sort;
pub use statistics::{Stat, Statistics};
pub use synth_result::SynthResult;
pub use term::Term;
pub use term_manager::TermManager;

#[cfg(feature = "parser")]
pub use cvc5_sys::Cvc5InputLanguage as InputLanguage;
#[cfg(feature = "parser")]
pub use parser::{Command, InputParser, SymbolManager};