1use std::{borrow::Cow, collections::hash_map::Entry};
2
3#[cfg(feature = "mem_dbg")]
4use mem_dbg::{MemDbg, MemSize};
5
6use crate::{
7 items::{
8 Blame, BoundVars, ENodeIdx, EqTransIdx, InstIdx, MatchIdx, MatchKind, ProofIdx,
9 ProofStepKind, TermId, TermIdx, TermKind,
10 },
11 Error as E, FxHashMap, FxHashSet, IString, NonMaxU32, Result, StringTable,
12};
13
14use super::{
15 blame::{BasicEq, BlameFinder, BlamedEqsParse, ComplexEq, CustomEq, ForceEq},
16 terms::Terms,
17 Z3Parser,
18};
19
20impl Z3Parser {
24 fn is_z3_6081_fixed(&self) -> bool {
25 self.version_info.is_ge_version(4, 9, 0)
26 }
27
28 pub(super) fn check_lambda_name(&self, lambda: &str) -> Result<()> {
29 let correct = if self.is_z3_6081_fixed() {
30 lambda == "<null>"
31 } else {
32 lambda == "null"
33 };
34 correct
35 .then_some(())
36 .ok_or_else(|| E::NonNullLambdaName(lambda.to_string()))
37 }
38
39 pub(super) fn parse_qid<'a>(
40 &self,
41 l: &mut impl Iterator<Item = &'a str>,
42 ) -> Result<(Cow<'a, str>, NonMaxU32)> {
43 let mut qid = Cow::Borrowed(l.next().ok_or(E::UnexpectedNewline)?);
44 let mut num_vars = l.next().ok_or(E::UnexpectedNewline)?;
45 if self.is_z3_6081_fixed() {
46 if qid.starts_with('|') && !qid.ends_with('|') {
47 qid += " ";
48 qid += num_vars;
49 while !num_vars.ends_with('|') {
50 num_vars = l.next().ok_or(E::UnexpectedNewline)?;
51 qid += " ";
52 qid += num_vars;
53 }
54 num_vars = l.next().ok_or(E::UnexpectedNewline)?;
55 }
56 let nvs = num_vars.parse::<NonMaxU32>().map_err(E::InvalidVarNum)?;
57 return Ok((qid, nvs));
58 }
59
60 let mut nvs = num_vars.parse::<NonMaxU32>();
61 if nvs.is_err() {
62 qid = Cow::Owned(format!("|{qid}"));
63 }
64 while nvs.is_err() {
65 qid += " ";
66 qid += num_vars;
67 num_vars = l.next().ok_or(E::UnexpectedNewline)?;
68 nvs = num_vars.parse::<NonMaxU32>();
69 }
70 if matches!(qid, Cow::Owned(_)) {
71 qid += "|";
72 }
73 Ok((qid, nvs.unwrap()))
74 }
75}
76
77impl Z3Parser {
80 pub(super) fn parse_app_name<'a>(
81 &mut self,
82 l: &mut impl Iterator<Item = &'a str>,
83 ) -> Result<(Cow<'a, str>, Option<TermId>)> {
84 let mut name = Cow::Borrowed(l.next().ok_or(E::UnexpectedNewline)?);
85 let mut l = l.map(|id| (id, TermId::parse(&mut self.strings, id)));
86 let mut idp = l.next();
87
88 let post = |name: Cow<'a, str>| match name {
89 Cow::Borrowed(n) => Cow::Borrowed(n),
90 Cow::Owned(mut n) => {
91 n += "|";
92 Cow::Owned(n)
93 }
94 };
95 while let Some((ids, id)) = idp {
96 if let Ok(id) = id {
97 return Ok((post(name), Some(id)));
98 }
99 if let Cow::Borrowed(n) = name {
100 name = Cow::Owned(format!("|{n}"));
101 }
102 name += " ";
103 name += ids;
104 idp = l.next();
105 }
106 Ok((post(name), None))
107 }
108}
109
110impl Z3Parser {
111 pub fn check_eq(&self, from: ENodeIdx, to: ENodeIdx) -> bool {
114 self.egraph.check_eq(from, to, &self.stack)
115 || self.check_eq_if(from, to)
116 || self.check_eq_if(to, from)
117 }
118
119 fn check_eq_if(&self, from: ENodeIdx, to: ENodeIdx) -> bool {
120 let term = &self[self[from].owner];
121 if term.app_name().is_none_or(|n| &self[n] != "if") || term.child_ids.len() != 3 {
122 return false;
123 }
124 let Some(lit) = self.lits.get_assign(term.child_ids[0], &self.stack) else {
125 return false;
126 };
127 let from = if self[lit].term.value {
128 term.child_ids[1]
129 } else {
130 term.child_ids[2]
131 };
132 let Some(from) = self.egraph.get_enode_imm(from, &self.stack) else {
133 debug_assert!(false, "if child not in egraph");
134 return false;
135 };
136 self.check_eq(from, to)
137 }
138}
139
140#[derive(Debug, Clone, Copy)]
143pub struct TransEqAllowed {
144 pub can_mismatch_initial: bool,
145 pub can_mismatch_congr: bool,
146}
147
148impl Z3Parser {
149 pub(super) fn make_blamed(
150 &mut self,
151 match_: &MatchKind,
152 blamed: Vec<(usize, ENodeIdx, BlamedEqsParse)>,
153 pat: TermIdx,
154 ) -> Result<(bool, Box<[Blame]>)> {
155 let pattern = &self[pat];
156 if blamed.len() < pattern.child_ids.len() {
157 return Err(E::SubpatTooFewBlame(pattern.child_ids.len() - blamed.len()));
158 }
159
160 let mut finder = BlameFinder::new(self, match_, blamed, pat)?;
161 if let Some((correct_order, result)) = finder.find_blamed::<BasicEq>()? {
162 return Ok((correct_order, result));
163 }
164 if let Some((correct_order, result)) = finder.find_blamed::<ComplexEq>()? {
165 return Ok((correct_order, result));
166 }
167 if let Some((correct_order, result)) = finder.find_blamed::<CustomEq>()? {
168 return Ok((correct_order, result));
169 }
170 if let Some((correct_order, result)) = finder.find_blamed::<ForceEq>()? {
171 return Ok((correct_order, result));
172 }
173
174 let not_found = finder.not_found();
175 Err(E::SubpatNoBlame(not_found))
176 }
177}
178
179#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
182#[derive(Debug, Default)]
183pub(super) struct TermsBug {
184 get_model: Option<IString>,
186 get_model_idx: u32,
187}
188
189impl Terms {
190 pub fn parse_app_child_id(&self, mut term_id: TermId) -> Result<TermIdx> {
193 if let Some(namespace) = self.bug.get_model {
194 debug_assert!(term_id.namespace.is_none());
195 term_id.namespace = Some(namespace);
196 }
197 self.get_app_term_bug(term_id)
198 }
199
200 pub fn check_get_model(&mut self, id: &mut TermId, name: &str, strings: &mut StringTable) {
201 let bug = &mut self.bug;
202 let get_model = bug.get_model.take();
203 if id.namespace.is_some() {
204 return;
205 }
206 let Some(get_model) = get_model else {
208 if name == "string" {
210 let namespace = format!("get-model-{}", bug.get_model_idx);
211 bug.get_model_idx += 1;
212 bug.get_model = Some(IString(strings.get_or_intern(namespace)));
213 id.namespace = bug.get_model;
214 }
215 return;
216 };
217 match name {
218 "string" | "cr" | "compose" | "indent" | "choice" => {
219 bug.get_model = Some(get_model);
220 id.namespace = Some(get_model);
221 }
222 _ => (),
223 }
224 }
225}
226
227#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
231#[derive(Debug, Default)]
232pub(super) struct InstanceBody {
233 pub req_eqs: FxHashMap<TermIdx, FxHashSet<(ENodeIdx, ENodeIdx)>>,
234}
235
236impl Z3Parser {
237 pub(super) fn instance_body(
238 &self,
239 proof: Option<ProofIdx>,
240 midx: MatchIdx,
241 ) -> Option<InstanceBody> {
242 let proof = &self[proof?];
243 let match_ = &self[midx];
245 let Some((qidx, bound)) = match_.kind.quant_and_enodes() else {
246 debug_assert!(false, "unexpected kind {match_:?}");
247 return None;
248 };
249 let body = match proof.kind {
250 ProofStepKind::PR_QUANT_INST => {
251 let result = &self[proof.result];
253 debug_assert_eq!(result.child_ids.len(), 2);
254 debug_assert!(result.app_name().is_some_and(|n| &self[n] == "or"));
255 debug_assert!({
256 let not = &self[result.child_ids[0]];
257 not.child_ids.len() == 1
258 && not.app_name().is_some_and(|n| &self[n] == "not")
259 && self[not.child_ids[0]]
260 .quant_idx()
261 .is_some_and(|q| q == qidx)
262 });
263 result.child_ids[1]
264 }
265 ProofStepKind::PR_TRANS => {
266 let result = &self[proof.result];
268 debug_assert_eq!(result.child_ids.len(), 2);
269 debug_assert!(result.app_name().is_some_and(|n| &self[n] == "="));
270 debug_assert!({
271 let true_ = &self[result.child_ids[1]];
272 true_.child_ids.is_empty()
273 && true_.app_name().is_some_and(|n| &self[n] == "true")
274 });
275 result.child_ids[0]
276 }
277 _ => {
278 debug_assert!(
279 false,
280 "unexpected kind {proof:?} / {:?}",
281 self[proof.result].id
282 );
283 return None;
284 }
285 };
286 let Some(qbody) = self.quantifier_body(qidx) else {
287 debug_assert!(false, "quantifier {:?} has no body", self[qidx]);
288 return None;
289 };
290 let mut ib = InstanceBody::default();
291 self.mk_instance_body(bound, 0, qbody, body, &mut ib);
292 Some(ib)
293 }
294
295 fn mk_instance_body(
296 &self,
297 bound: BoundVars<ENodeIdx>,
298 mut inner_binds: u32,
301 qbody: TermIdx,
302 body: TermIdx,
303 ib: &mut InstanceBody,
304 ) -> bool {
305 let Entry::Vacant(v) = ib.req_eqs.entry(body) else {
306 return false;
307 };
308
309 let qb = &self[qbody];
310 if qb.has_var().is_some_and(|v| !v) {
311 debug_assert_eq!(qbody, body, "unexpected unequal no var body");
312 return qbody != body;
313 }
314
315 let b = match qb.kind() {
316 TermKind::Var(qvar) => {
317 if let Some(qvar) = qvar.get().checked_sub(inner_binds) {
318 let Some(qb) = bound.get(NonMaxU32::new(qvar).unwrap()) else {
319 debug_assert!(false, "error: {qvar:?} / {bound:?} ({inner_binds})");
320 return true;
321 };
322 let qbody = self[qb].owner;
323 if qbody != body {
324 let Some(b) = self.egraph.get_enode_imm(body, &self.stack) else {
325 debug_assert!(false, "body not in egraph");
326 return true;
327 };
328 if !self.egraph.check_eq(qb, b, &self.stack) {
329 return true;
331 }
332 v.insert(Default::default()).insert((qb, b));
333 }
334 return false;
335 } else {
336 let b = &self[body];
337 let TermKind::Var(var) = b.kind() else {
338 debug_assert!(false, "unexpected kind {b:?}");
339 return true;
340 };
341 debug_assert_eq!(qvar, var, "unexpected var {qvar} / {var} / {bound:?}");
342 return qvar != var;
343 }
344 }
345 TermKind::Quant(qinner) => {
346 let b = &self[body];
347 let TermKind::Quant(inner) = b.kind() else {
348 debug_assert!(false, "unexpected kind {b:?}");
349 return true;
350 };
351 let qinner = &self[qinner];
352 let inner = &self[inner];
353 if qinner.num_vars != inner.num_vars
354 || qinner.kind != inner.kind
355 || qb.child_ids.len() != b.child_ids.len()
356 {
357 debug_assert!(
358 false,
359 "unexpected quant {qinner:?} / {inner:?} / {qb:?} / {b:?}"
360 );
361 return true;
362 }
363 let vars = qinner.num_vars.get();
364 inner_binds += vars;
365 b
366 }
367 TermKind::App(qname) => {
368 let b = &self[body];
369 debug_assert!(inner_binds > 0 || !b.has_var().is_some_and(|v| v));
370 let TermKind::App(name) = b.kind() else {
371 debug_assert!(false, "unexpected kind {b:?}");
372 return true;
373 };
374 if qname != name || qb.child_ids.len() != b.child_ids.len() {
375 debug_assert!(false, "unexpected app body {qb:?} / {b:?}");
376 return true;
377 }
378 b
379 }
380 };
381 let mut error = false;
382 for (q, b) in qb.child_ids.iter().zip(b.child_ids.iter()) {
383 error |= self.mk_instance_body(bound, inner_binds, *q, *b, ib);
384 }
385 let eqs = b.child_ids.iter();
386 let eqs: FxHashSet<_> = eqs
387 .flat_map(|b| {
388 let eqs = ib.req_eqs.get(b);
389 eqs.into_iter().flat_map(|e| e.iter().copied())
390 })
391 .collect();
392 let old = ib.req_eqs.insert(body, eqs);
393 debug_assert!(old.is_none(), "unexpected old eqs {old:?}");
394 error || old.is_some()
395 }
396
397 pub(super) fn active_inst(
398 &mut self,
399 idx: TermIdx,
400 ) -> Result<Option<(InstIdx, FxHashSet<EqTransIdx>)>> {
401 let created_by = self.insts.active_inst();
402 created_by
403 .as_ref()
404 .map(|a| {
405 let req_eqs = a.req_eqs(idx);
406 let mismatch = TransEqAllowed {
407 can_mismatch_initial: false,
408 can_mismatch_congr: false,
409 };
410 let req_eqs = req_eqs
411 .map(|(from, to)| {
412 self.egraph
413 .new_trans_equality(from, to, &self.stack, mismatch)
414 .map(|r| r.unwrap())
415 })
416 .collect::<Result<_>>()?;
417 Ok((a.idx, req_eqs))
418 })
419 .transpose()
420 }
421}