xmt_lib/
solver.rs

1// Copyright Pierre Carbonnelle, 2025.
2
3use regex::Regex;
4use std::future::Future;
5use std::time::Instant;
6
7use derive_more::Display;
8use genawaiter::{sync::Gen, sync::gen, yield_};
9use indexmap::{IndexMap, IndexSet};
10use rusqlite::{Connection, Result};
11use z3_sys::*;
12
13use crate::ast::*;
14use crate::error::{format_error, SolverError};
15use crate::grammar::parse;
16use crate::private::a_sort::{declare_datatype, declare_datatypes, declare_sort, define_sort, PolymorphicObject, SortObject};
17use crate::private::b_fun::{declare_fun, define_fun, define_funs_rec, FunctionObject};
18use crate::private::c_assert::assert_;
19use crate::private::d_interpret::{interpret_pred, interpret_fun};
20use crate::private::e_ground::{ground, Grounding};
21use crate::private::e2_ground_query::TableName;
22use crate::private::e3_ground_sql::Predefined;
23use crate::private::y_db::init_db;
24use crate::ast::L;
25
26
27#[derive(PartialEq)]
28pub(crate) enum Backend {
29    NoDriver,
30    Z3(Z3_context)
31}
32
33impl Backend {
34    /// execute a command string
35    pub(crate) fn exec(&mut self, cmd: &str) -> Result<String, SolverError> {
36        match self {
37            Backend::NoDriver => {
38                return Ok(cmd.to_string())
39            },
40            Backend::Z3(ctx) => {
41                unsafe {
42                    let c_cmd = std::ffi::CString::new(cmd).unwrap();
43                    let response = Z3_eval_smtlib2_string(*ctx, c_cmd.as_ptr());
44                    let c_str: &std::ffi::CStr = std::ffi::CStr::from_ptr(response);
45                    let str_slice: &str = c_str.to_str().unwrap();
46                    let result: String = str_slice.to_owned();
47                    return Ok(result)
48                }
49            }
50        }
51    }
52}
53
54pub(crate) type TermId = usize;
55
56// A non-parametric sort without use of aliases (defined sort)
57#[derive(Debug, Display, Clone, PartialEq, Eq, Hash)]
58pub(crate) struct CanonicalSort(pub(crate) Sort);
59
60
61/// A solver is used to solve SMT problems.
62pub struct Solver {
63    /// A connection to the sqlite database used for grounding assertions
64    /// (via the [rusqlite](https://docs.rs/rusqlite/latest/rusqlite/index.html) crate).
65    pub(crate) conn: Connection,
66    pub(crate) backend: Backend,
67    /// help ensure the backend is not changed after a command has been executed
68    pub (crate) started: bool,
69
70    /// contains only parametric data type declarations
71    pub(crate) polymorphic_sorts: IndexMap<Symbol, PolymorphicObject>,
72
73    /// contains nullary data types and the used instantiations of parametric data types
74    pub(crate) canonical_sorts: IndexMap<Sort, CanonicalSort>,
75    pub(crate) sort_objects: IndexMap<CanonicalSort, SortObject>,
76
77    /// predicate and function symbols
78    pub(crate) interpretable_functions: IndexMap<L<Identifier>, (Vec<CanonicalSort>, CanonicalSort)>,
79    pub(crate) function_objects: IndexMap<(L<Identifier>, Vec<CanonicalSort>),
80                                     IndexMap<CanonicalSort, FunctionObject>>,
81
82    /// To support differed grounding of terms.
83    /// The string is the original assertion command.
84    /// The first element is the annotated term
85    pub(crate) assertions_to_ground: Vec<L<Term>>,
86    /// a mapping from a term (top-level?) to a composable representation of its grounding
87    pub(crate) groundings: IndexMap<(L<Term>, bool), (Grounding, CanonicalSort)>,
88
89    /// to convert interpretations to definitions when given late
90    /// (i.e., make an assertion with p, x-ground, interpret p
91    /// --> need to add a definition of p to avoid losing information about p)
92    pub(crate) grounded: IndexSet<Identifier>,
93
94    /// keep track of interpretations already converted to definitions,
95    /// to avoid duplicate definitions
96    pub(crate) converted: IndexSet<L<Identifier>>,
97
98    /// to handle the fact that db names are case insensitive in sqlite
99    pub(crate) db_names: IndexSet<String>,
100}
101
102
103#[derive(Debug, strum_macros::Display, Clone, PartialEq, Eq, Hash)]
104pub(crate) enum TableType {
105    #[strum(to_string = "sort")] Sort,
106    #[strum(to_string = "selector")] Selector,
107    #[strum(to_string = "tester")] Tester,
108    #[strum(to_string = "interp" )] Interpretation,
109    #[strum(to_string = "view" )] Dynamic,
110}
111
112///////////////////////////////////////////////////////
113
114impl Solver {
115    /// Creates a solver.
116    /// Optionally gives access to a sqlite database with pre-loaded data
117    /// (via the [rusqlite](https://docs.rs/rusqlite/latest/rusqlite/index.html) crate).
118    pub fn new(conn: Option<Connection>) -> Solver {
119
120        let mut conn =
121            if let Some(conn) = conn {
122                conn
123            } else {
124                Connection::open_in_memory().unwrap()
125            };
126
127        // create Bool table
128        conn.execute(
129            "CREATE TABLE Bool (
130                    G    TEXT PRIMARY KEY
131            )",
132            (), // empty list of parameters.
133        ).unwrap();
134        conn.execute("INSERT INTO Bool (G) VALUES (\"true\")" , ()).unwrap();
135        conn.execute("INSERT INTO Bool (G) VALUES (\"false\")", ()).unwrap();
136
137        init_db(&mut conn).unwrap();
138
139        // Note: indexed sorts are created as Unknown when occurring: (_ BitVec n), (_ FloatingPoint eb sb)
140
141        // create pre-defined parametric sorts: (Array ..), (Seq ..), (Tuple..)
142        let mut polymorphic_sorts = IndexMap::new();
143        polymorphic_sorts.insert(Symbol("Array".to_string()), PolymorphicObject::Unknown);
144
145        // not in the SMT-Lib standard:
146        // polymorphic_sorts.insert(Symbol("Seq".to_string()), PolymorphicObject::Unknown);
147        // polymorphic_sorts.insert(Symbol("Tuple".to_string()), PolymorphicObject::Unknown);
148
149        // create pre-defined sorts: Bool, Int, Real
150        let mut sort_objects = IndexMap::new();
151        let sort = |s: &str|
152            Sort::new(&Symbol(s.to_string()));
153        let canonical_sort = |s: &str|
154            CanonicalSort(Sort::new(&Symbol(s.to_string())));
155
156        let bool_decl = SortObject::Normal{
157            datatype_dec: DatatypeDec::DatatypeDec(
158                vec![
159                    ConstructorDec (Symbol("true" .to_string()),vec![]),
160                    ConstructorDec (Symbol("false".to_string()),vec![]),
161                ],
162                ),
163            table: TableName("Bool".to_string()),
164            row_count: 2};
165            sort_objects.insert(CanonicalSort(sort("Bool")), bool_decl);
166        // LINK src/doc.md#_Infinite
167        sort_objects.insert(canonical_sort("Int"), SortObject::Infinite);
168        sort_objects.insert(canonical_sort("Real"), SortObject::Infinite);
169        sort_objects.insert(canonical_sort("RoundingMode"), SortObject::Infinite);  // in FloatingPoint theory
170        sort_objects.insert(canonical_sort("String"), SortObject::Infinite);  // in String theory
171        sort_objects.insert(canonical_sort("RegLan"), SortObject::Infinite);  // in String theory
172
173
174        let mut canonical_sorts = IndexMap::new();
175        canonical_sorts.insert(sort("Bool"), canonical_sort("Bool"));
176        canonical_sorts.insert(sort("Int"), canonical_sort("Int"));
177        canonical_sorts.insert(sort("Real"), canonical_sort("Real"));
178        canonical_sorts.insert(sort("RoundingMode"), canonical_sort("RoundingMode"));  // in FloatingPoint theory
179        canonical_sorts.insert(sort("String"), canonical_sort("String"));  // in String theory
180        canonical_sorts.insert(sort("RegLan"), canonical_sort("RegLan"));  // in String theory
181
182        // create function objects
183        let id = |s: &str|
184            Identifier::new(&Symbol(s.to_string()));
185
186        let mut function_objects = IndexMap::new();
187
188
189        {// boolean pre-defined functions
190            let co_domain = CanonicalSort(sort("Bool"));
191            // LINK src/doc.md#_Constructor
192            for s in ["true", "false"] {
193                let func = FunctionObject::Constructor;
194                function_objects.insert((id(s), vec![]), IndexMap::from([(co_domain.clone(), func.clone())]));
195            }
196
197            // boolean pre-defined functions
198            for (s, function) in [
199                    ("not",      Predefined::Not),
200                    ("=>",       Predefined::_Implies),
201                    ("and",      Predefined::And),
202                    ("or",       Predefined::Or),
203                    ("xor",      Predefined::_Xor),
204                    ("=",        Predefined::Eq),
205                    ("distinct", Predefined::Distinct),
206                    ("<=",       Predefined::LE),
207                    ("<",        Predefined::Less),
208                    (">=",       Predefined::GE),
209                    (">",        Predefined::Greater)
210                            ] {
211                let func = FunctionObject::Predefined{ function, boolean: Some(true) };
212                function_objects.insert((id(s), vec![]), IndexMap::from([(co_domain.clone(), func.clone())]));
213            }
214
215            // ite, lte
216            let func = FunctionObject::Predefined { function: Predefined::Ite, boolean: None };
217            function_objects.insert((id("ite"), vec![]), IndexMap::from([(co_domain.clone(), func.clone())]));
218
219            let func = FunctionObject::Predefined { function: Predefined::_Let, boolean: None };
220            function_objects.insert((id("let"), vec![]), IndexMap::from([(co_domain.clone(), func.clone())]));
221        }
222        { // non-boolean pre-defined functions
223            let co_domain = CanonicalSort(sort("Real"));
224            for (s, function) in [
225                    ("+",   Predefined::Plus),
226                    ("-",   Predefined::Minus),
227                    ("*",   Predefined::Times),
228                    ("div", Predefined::Div),
229                    ("mod", Predefined::Mod),
230                    ("abs", Predefined::Abs),
231                    ] {
232                let func = FunctionObject::Predefined{ function, boolean: Some(false) };
233                function_objects.insert((id(s), vec![]), IndexMap::from([(co_domain.clone(), func.clone())]));
234            };
235        }
236        unsafe {
237            let cfg = Z3_mk_config();
238            let ctx = Z3_mk_context(cfg);
239            let backend = Backend::Z3(ctx);
240
241            Solver {
242                backend,
243                started: false,
244                conn,
245                polymorphic_sorts,
246                sort_objects,
247                canonical_sorts,
248                interpretable_functions: IndexMap::new(),
249                function_objects,
250                assertions_to_ground: vec![],
251                groundings: IndexMap::new(),
252                grounded: IndexSet::new(),
253                db_names: IndexSet::new(),
254                converted: IndexSet::new()
255            }
256        }
257
258    }
259}
260
261
262impl Solver {
263
264    /// Execute the XMT-Lib commands in a string, and returns a generator of strings containing the results.
265    pub fn parse_and_execute<'a> (
266        &'a mut self,
267        source: &'a str
268    ) -> Gen<String, (), impl Future<Output = ()> + 'a> {
269        gen!({
270            match parse(&source) {
271                Ok(commands) => {
272                    for result in self.execute(commands) {
273                        match result {
274                            Ok(s) => yield_!(s),
275                            Err(e) => {
276                                yield_!(format_error(&source, e));
277                                break
278                            }
279                        }
280                    }
281                },
282                Err(err) => {
283                    // Pretty-print the error
284                    yield_!(format_error(&source, SolverError::ParseError(err)))
285                }
286            }
287        })
288    }
289
290    /// Execute the SMT-Lib commands and returns a generator of strings containing the results.
291    pub(crate) fn execute (
292        &mut self,
293        commands: Vec<Command>
294    ) -> Gen<Result<String, SolverError>, (), impl Future<Output = ()> + '_> {
295
296        gen!({
297            let mut start = Instant::now();
298            for command in commands {
299                for result in self.execute1(command, &mut start) {
300                    if result.is_err() {
301                        yield_!(result);
302                        break
303                    } else {
304                        yield_!(result);
305                    }
306                }
307            }
308        })
309    }
310
311    /// Execute one command and returns a generator of strings containing the results.
312    pub(crate) fn execute1<'a> (
313        &'a mut self,
314        c: Command,
315        start: &'a mut Instant
316    ) -> Gen<Result<String, SolverError>, (), impl Future<Output = ()> + 'a>
317    {
318        gen!({
319            let command = c.to_string();
320            match c {
321
322                Command::Assert(term) => {
323                    if self.backend != Backend::NoDriver {
324                        // submit to solver to detect syntax error
325                        // push and pop, to avoid polluting the SMT state
326                        yield_!(self.exec("(push)"));
327                        yield_!(self.exec(&command));
328                        yield_!(self.exec("(pop)"));
329                    }
330
331                    yield_!(assert_(&term, self))
332                }
333                Command::CheckSat => {
334                    for res in ground(false, false, false, self) {
335                        yield_!(res)
336                    }
337                    match self.exec(&command) {
338                        Ok(res) => yield_!(Ok(res)),
339                        Err(err) => {
340                            yield_!(Err(err));
341                        }
342                    };
343                }
344
345                Command::DeclareConst(symb, sort) =>
346                    yield_!(declare_fun(symb, vec![], sort, command, self)),
347
348                Command::DeclareDatatype(symb, decl) =>
349                    yield_!(declare_datatype(symb, decl, command, self)),
350
351                Command::DeclareDatatypes(sort_decls, decls) =>
352                    yield_!(declare_datatypes(sort_decls, decls, command, self)),
353
354                Command::DeclareFun(symb, domain, co_domain) =>
355                    yield_!(declare_fun(symb, domain, co_domain, command, self)),
356
357                Command::DeclareSort(symb, numeral) =>
358                    yield_!(declare_sort(symb, numeral, command, self)),
359
360                Command::DefineFun(def, rec) => yield_!(define_fun(def, rec, command, self)),
361
362                Command::DefineFunsRec(decs, terms) =>
363                    yield_!(define_funs_rec(decs, terms, command, self)),
364
365                Command::DefineSort(symb, variables, sort) =>
366                    yield_!(define_sort(symb, variables, sort, command, self)),
367
368                Command::Echo(string) => yield_!(self.exec(&command)),
369                Command::GetInfo(keyword) => yield_!(self.exec(&command)),
370                Command::XInterpretPred(identifier, tuples) =>
371                    yield_!(interpret_pred(identifier, tuples, self)),
372
373                Command::XInterpretFun(identifier, tuples, else_) =>
374                    yield_!(interpret_fun(identifier, tuples, else_, command, self)),
375
376                Command::SetOption(option) =>
377                    yield_!(self.set_option(option, command)),
378
379                Command::XDebug(typ, obj) => {
380                    match typ.to_string().as_str() {
381                        "solver" => {
382                            match obj.to_string().as_str() {
383                                "sorts" => {
384                                    yield_!(Ok("Sorts:\n".to_string()));
385                                    for (sort, canonical) in &self.canonical_sorts {
386                                        let decl = self.sort_objects.get(canonical).unwrap();
387                                        let canonical = if canonical.0 == sort.clone() { "".to_string() }
388                                            else { format!(" (= {canonical})") };
389                                        match decl {
390                                            SortObject::Normal{datatype_dec, table, row_count} =>
391                                                yield_!(Ok(format!(" - ({table}: {row_count}) {sort}{canonical}: {datatype_dec}\n"))),
392                                            SortObject::Recursive =>
393                                                yield_!(Ok(format!(" - (recursive) {sort}{canonical}\n"))),
394                                            SortObject::Infinite =>
395                                                yield_!(Ok(format!(" - (infinite) {sort}{canonical}\n"))),
396                                            SortObject::Unknown =>
397                                                yield_!(Ok(format!(" - (unknown) {sort}{canonical}\n"))),
398                                        }
399                                    }
400                                },
401                                "polymorphic_sorts" => {
402                                    yield_!(Ok("Polymorphic datatypes:\n".to_string()));
403                                    for (sort, decl) in &self.polymorphic_sorts {
404                                        match decl {
405                                            PolymorphicObject::Datatype(decl) =>
406                                                yield_!(Ok(format!(" - {sort}: {decl}\n"))),
407                                            PolymorphicObject::SortDefinition{variables, definiendum} => {
408                                                let vars = variables.iter()
409                                                    .map(|v| v.0.clone())
410                                                    .collect::<Vec<String>>().join(",");
411                                                yield_!(Ok(format!(" - {sort}: ({vars}) -> {definiendum}\n")))
412                                            },
413                                            PolymorphicObject::RecursiveDT(decl) =>
414                                                yield_!(Ok(format!(" - (recursive) {sort}: {decl}\n"))),
415                                            PolymorphicObject::Unknown =>
416                                                yield_!(Ok(format!(" - (unknown): {sort}\n"))),
417                                        }
418                                    }
419                                },
420                                "functions" => {
421                                    yield_!(Ok("Functions2:\n".to_string()));
422                                    for ((symbol, domain), map) in &self.function_objects {
423                                        let domain = domain.iter()
424                                            .map(|s| s.to_string())
425                                            .collect::<Vec<_>>().join(", ");
426                                        for (co_domain, func) in map {
427                                            yield_!(Ok(format!(" - {symbol} ({domain})->{co_domain} : {func}\n")))
428                                        }
429                                    }
430                                },
431                                "groundings" => {
432                                    yield_!(Ok("Groundings:\n".to_string()));
433                                    for ((term, top), (grounding, _)) in &self.groundings {
434                                        let top = if *top { "(top)" } else { "" };
435                                        yield_!(Ok(format!("=== {top} {term} ======================================\n{grounding}\n")))
436                                    }
437                                    yield_!(Ok("===========================================\n".to_string()))
438                                },
439                                _ => yield_!(Err(SolverError::IdentifierError("Unknown 'x-debug solver' parameter\n", obj)))
440                            }
441                        },
442                        "db" => {
443                            if obj.to_string() == "tables" {
444                                // Query to list all tables and views in the database
445                                let query = "SELECT name, type FROM sqlite_master WHERE type IN ('table', 'view')";
446                                let mut stmt = self.conn.prepare(query).unwrap();
447                                let rows = stmt.query_map([], |row| {
448                                    let name: String = row.get(0)?;
449                                    let typ: String = row.get(1)?;
450                                    Ok((name, typ))
451                                }).unwrap();
452
453                                yield_!(Ok("Tables and Views:\n".to_string()));
454                                for row in rows {
455                                    if let Ok((name, typ)) = row {
456                                        yield_!(Ok(format!(" - {name} ({typ})\n")));
457                                    }
458                                }
459                            } else if let Ok(content) = pretty_sqlite::pretty_table(&self.conn, obj.to_string().to_lowercase().as_str()) {
460                                yield_!(Ok(format!("{content}\n")))
461                            } else {
462                                yield_!(Err(SolverError::IdentifierError("Unknown table\n", typ)))
463                            }
464                        },
465                        _ => yield_!(Err(SolverError::IdentifierError("Unknown 'x-debug' parameter\n", typ)))
466                    }
467                },
468
469                Command::XDuration(string) => {
470                    let duration = start.elapsed().as_secs_f32();
471                    *start = Instant::now();
472                    yield_!(Ok(format!("{}{:.3} sec\n", string.0, duration)))
473                },
474
475                Command::XGround{no, debug, sql} => {
476                    for res in ground(no, debug, sql, self) {
477                        yield_!(res)
478                    }
479                }
480
481                Command::Verbatim(_) => yield_!(self.exec(&command)),
482            }
483        })
484    }
485
486    /// execute a command string
487    pub(crate) fn exec(&mut self, cmd: &str) -> Result<String, SolverError> {
488        if cmd.to_string().len() != 0 {
489            self.started = true;
490        }
491        self.backend.exec(cmd)
492    }
493
494    pub(crate) fn set_option(&mut self, option: Option_, cmd: String) -> Result<String, SolverError> {
495        match option {
496            Option_::Attribute(Attribute::Keyword(_)) => {
497                self.exec(&cmd)
498            },
499            Option_::Attribute(Attribute::WithValue(keyword, value)) => {
500                match (keyword.0.as_str(), value) {
501                    (":backend", AttributeValue::Symbol(Symbol(value))) => {
502                        let new =
503                            match value.as_str() {
504                                "none" => Backend::NoDriver,
505                                "Z3" => {
506                                    unsafe {
507                                        let cfg = Z3_mk_config();
508                                        let ctx = Z3_mk_context(cfg);
509                                        Backend::Z3(ctx)
510                                    }
511                                },
512                                _ => return Err(SolverError::ExprError(format!("Unknown backend: {value}")))
513                            };
514                        if self.backend != new {
515                            if self.started {
516                                return Err(SolverError::ExprError("Can't change backend anymore".to_string()))
517                            };
518                            self.backend = new;
519                        }
520                        Ok("".to_string())
521                    },
522                    _ => self.exec(&cmd)
523                }
524
525            },
526        }
527    }
528
529
530    /// Sanitize a name.  Removes non-alphanumeric characters, and adds a number if empty or ambiguous.
531    pub(crate) fn create_table_name(self: &mut Solver, name: String, type_: TableType) -> TableName {
532        let re = Regex::new(r"[\+\-/\*=\%\?\!\.\$\&\^<>@\|]").unwrap();
533        let db_name = re.replace_all(&name, "").to_string().to_lowercase();
534        let index = self.db_names.len();
535        let db_name =
536            if db_name.len() == 0 {
537                format!("_xmt_{type_}_{index}")
538            } else {
539                let temp =
540                    if db_name.starts_with("_xmt_") { strip_prefix(&db_name) }
541                    else { db_name };
542                let temp = format!("_xmt_{type_}_{temp}");
543                if self.db_names.contains(&temp) {
544                    format!("{temp}_{index}")
545                } else {
546                    temp
547                }
548            };
549        self.db_names.insert(db_name.clone());
550        TableName(db_name)
551    }
552}
553
554fn strip_prefix(s: &str) -> String {
555    // Match and remove a prefix like "_xmt_abc_"
556    let re = Regex::new(r"^_xmt_[^_]+_").unwrap();
557    re.replace(&s, "").to_string()
558}
xmt_lib/solver.rs

xmt_lib/
solver.rs
