cvc5-rs 0.3.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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152

//! # 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::Cvc5BlockModelsMode as BlockModelsMode;
pub use cvc5_sys::Cvc5FindSynthTarget as FindSynthTarget;
pub use cvc5_sys::Cvc5Kind as Kind;
pub use cvc5_sys::Cvc5LearnedLitType as LearnedLitType;
pub use cvc5_sys::Cvc5OptionInfo;
pub use cvc5_sys::Cvc5Plugin;
pub use cvc5_sys::Cvc5ProofComponent as ProofComponent;
pub use cvc5_sys::Cvc5ProofFormat as ProofFormat;
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};

/// Get a string representation of an [`InputLanguage`].
#[cfg(feature = "parser")]
pub fn input_language_to_string(lang: InputLanguage) -> String {
    unsafe {
        std::ffi::CStr::from_ptr(cvc5_sys::cvc5_modes_input_language_to_string(lang))
            .to_string_lossy()
            .into_owned()
    }
}

// ---------------------------------------------------------------------------
// String conversion helpers for re-exported enums
// ---------------------------------------------------------------------------

macro_rules! enum_to_string_fn {
    ($(#[$meta:meta])* $fn_name:ident, $ty:ty, $c_fn:path) => {
        $(#[$meta])*
        pub fn $fn_name(val: $ty) -> String {
            unsafe {
                std::ffi::CStr::from_ptr($c_fn(val))
                    .to_string_lossy()
                    .into_owned()
            }
        }
    };
}

enum_to_string_fn!(
    /// Get a string representation of a [`Kind`].
    kind_to_string, Kind, cvc5_sys::cvc5_kind_to_string
);
enum_to_string_fn!(
    /// Get a string representation of a [`SortKind`].
    sort_kind_to_string, SortKind, cvc5_sys::cvc5_sort_kind_to_string
);
enum_to_string_fn!(
    /// Get a string representation of a [`ProofRule`].
    proof_rule_to_string, ProofRule, cvc5_sys::cvc5_proof_rule_to_string
);
enum_to_string_fn!(
    /// Get a string representation of a [`ProofRewriteRule`].
    proof_rewrite_rule_to_string, ProofRewriteRule, cvc5_sys::cvc5_proof_rewrite_rule_to_string
);
enum_to_string_fn!(
    /// Get a string representation of a [`RoundingMode`].
    rounding_mode_to_string, RoundingMode, cvc5_sys::cvc5_rm_to_string
);
enum_to_string_fn!(
    /// Get a string representation of a [`SkolemId`].
    skolem_id_to_string, SkolemId, cvc5_sys::cvc5_skolem_id_to_string
);
enum_to_string_fn!(
    /// Get a string representation of an [`UnknownExplanation`].
    unknown_explanation_to_string, UnknownExplanation, cvc5_sys::cvc5_unknown_explanation_to_string
);
enum_to_string_fn!(
    /// Get a string representation of a [`BlockModelsMode`].
    block_models_mode_to_string, BlockModelsMode, cvc5_sys::cvc5_modes_block_models_mode_to_string
);
enum_to_string_fn!(
    /// Get a string representation of a [`LearnedLitType`].
    learned_lit_type_to_string, LearnedLitType, cvc5_sys::cvc5_modes_learned_lit_type_to_string
);
enum_to_string_fn!(
    /// Get a string representation of a [`ProofComponent`].
    proof_component_to_string, ProofComponent, cvc5_sys::cvc5_modes_proof_component_to_string
);
enum_to_string_fn!(
    /// Get a string representation of a [`ProofFormat`].
    proof_format_to_string, ProofFormat, cvc5_sys::cvc5_modes_proof_format_to_string
);
enum_to_string_fn!(
    /// Get a string representation of a [`FindSynthTarget`].
    find_synth_target_to_string, FindSynthTarget, cvc5_sys::cvc5_modes_find_synth_target_to_string
);