use core::num::{NonZeroU32, NonZeroUsize};
use num::Num;
use crate::{
items::*,
parsers::z3::{VersionInfo, Z3LogParser},
BigRational, BoxSlice, Error as E, IString, NonMaxU32, Result, StringTable,
};
use super::{inter_line::LineKind, smt2::EventLog, terms::Terms, Z3Parser};
impl Default for Z3Parser {
fn default() -> Self {
let mut strings = StringTable::with_hasher(fxhash::FxBuildHasher::default());
Self {
version_info: VersionInfo::default(),
push_count: 0,
terms: Terms::default(),
synth_terms: Default::default(),
quantifiers: Default::default(),
insts: Default::default(),
egraph: Default::default(),
stack: Default::default(),
lits: Default::default(),
events: EventLog::new(&mut strings),
comm: Default::default(),
strings,
}
}
}
impl Z3Parser {
pub(super) fn incremental_mode(&self) -> bool {
self.push_count > 0
}
fn parse_new_full_id(&mut self, id: Option<&str>) -> Result<TermId> {
let full_id = id.ok_or(E::UnexpectedNewline)?;
TermId::parse(&mut self.strings, full_id)
}
fn parse_existing_app(&mut self, id: &str) -> Result<TermIdx> {
self.terms
.app_terms
.parse_existing_id(&mut self.strings, id)
}
fn parse_existing_proof(&mut self, id: &str) -> Result<ProofIdx> {
self.terms
.proof_terms
.parse_existing_id(&mut self.strings, id)
}
fn parse_existing_enode(&mut self, id: &str) -> Result<ENodeIdx> {
let idx = self.parse_existing_app(id)?;
self.get_existing_enode(idx)
}
fn get_existing_enode(&mut self, idx: TermIdx) -> Result<ENodeIdx> {
let res = self.egraph.get_enode(idx, &self.stack);
let can_error =
self.version_info.is_ge_version(4, 8, 9) && self.version_info.is_le_version(4, 11, 2);
if can_error && res.is_err() {
self.egraph
.new_enode(ENodeBlame::Unknown, idx, NonMaxU32::ZERO, &self.stack)?;
self.events.new_enode();
return self.egraph.get_enode(idx, &self.stack);
}
res
}
fn new_term(
&mut self,
id: TermId,
kind: TermKind,
child_ids: BoxSlice<TermIdx>,
) -> Result<TermIdx> {
let term = Term::new(id, kind, child_ids, |tidx| &self[tidx]);
self.terms.app_terms.new_term(term)
}
fn parse_z3_generation<'a>(l: &mut impl Iterator<Item = &'a str>) -> Result<Option<NonMaxU32>> {
if let Some(gen) = l.next() {
let gen = gen.parse::<NonMaxU32>().map_err(E::InvalidGeneration)?;
Ok(Some(gen))
} else {
Ok(None)
}
}
fn map<T, U>(l: impl Iterator<Item = T>, f: impl FnMut(T) -> Result<U>) -> Result<BoxSlice<U>> {
l.map(f).collect()
}
fn gobble_var_names_list<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<VarNames> {
let mut t = Self::gobble_tuples::<true>(l);
let (first, second) = t.next().ok_or(E::UnexpectedEnd)??;
if first.is_empty() {
let first = self.mk_string(second);
let tuples = t.map(|t| match t? {
("", second) => self.mk_string(second),
_ => Err(E::VarNamesListInconsistent),
});
let types = [first].into_iter().chain(tuples);
Ok(VarNames::TypeOnly(types.collect::<Result<_>>()?))
} else {
fn strip_bars(
strings: &mut StringTable,
(first, second): (&str, &str),
) -> Result<(IString, IString)> {
let first = first
.strip_prefix('|')
.ok_or(E::VarNamesNoBar)?
.strip_suffix('|')
.ok_or(E::VarNamesNoBar)?;
let second = second
.strip_prefix('|')
.ok_or(E::VarNamesNoBar)?
.strip_suffix('|')
.ok_or(E::VarNamesNoBar)?;
Ok((
IString(strings.get_or_intern(first)),
IString(strings.get_or_intern(second)),
))
}
let first = strip_bars(&mut self.strings, (first, second));
let tuples = t.map(|t| strip_bars(&mut self.strings, t?));
let names_and_types = [first].into_iter().chain(tuples);
Ok(VarNames::NameAndType(
names_and_types.collect::<Result<_>>()?,
))
}
}
fn gobble_tuples<'a, const FORMS_EQUAL: bool>(
mut l: impl Iterator<Item = &'a str>,
) -> impl Iterator<Item = Result<(&'a str, &'a str)>> {
let mut spaces = None;
let mut gobble = move || {
let Some(first) = l.next() else {
return Ok(None);
};
let (first, second) = if first.ends_with(')') {
let spaces = *spaces.get_or_insert(0);
if FORMS_EQUAL && spaces != 0 {
return Err(E::UnequalTupleForms(spaces, 0));
}
let mut l = first.split(';');
(
l.next().ok_or(E::UnexpectedNewline)?,
l.next().ok_or(E::UnexpectedNewline)?,
)
} else {
let middle = l.next().ok_or(E::UnexpectedNewline)?;
if middle != ";" {
let spaces = *spaces.get_or_insert(1);
if FORMS_EQUAL && spaces != 1 {
return Err(E::UnequalTupleForms(spaces, 1));
}
(first, middle)
} else {
let spaces = *spaces.get_or_insert(2);
if FORMS_EQUAL && spaces != 2 {
return Err(E::UnequalTupleForms(spaces, 2));
}
let second = l.next().ok_or(E::UnexpectedNewline)?;
(first, second)
}
};
let t = (
first.strip_prefix('(').ok_or(E::TupleMissingParens)?,
second.strip_suffix(')').ok_or(E::TupleMissingParens)?,
);
Ok(Some(t))
};
let inverted_gobble = move |_| gobble().map_or_else(|err| Some(Err(err)), |ok| ok.map(Ok));
std::iter::repeat(()).map_while(inverted_gobble)
}
fn append_trans_equality_tuples<'a>(
&mut self,
l: impl Iterator<Item = &'a str>,
mut f: impl FnMut((ENodeIdx, ENodeIdx)) -> Result<()>,
) -> Result<()> {
for t in Self::gobble_tuples::<true>(l) {
let (from, to) = t?;
let from = self.parse_existing_enode(from)?;
let to = self.parse_existing_enode(to)?;
f((from, to))?;
}
Ok(())
}
fn iter_until_eq<'a, 's>(
l: &'a mut impl Iterator<Item = &'s str>,
end: &'a str,
) -> impl Iterator<Item = &'s str> + 'a {
l.take_while(move |elem| *elem != end)
}
fn expect_completed<'s>(mut l: impl Iterator<Item = &'s str>) -> Result<()> {
l.next()
.map_or(Ok(()), |more| Err(E::ExpectedNewline(more.to_string())))
}
fn mk_string(&mut self, s: &str) -> Result<IString> {
Ok(IString(self.strings.try_get_or_intern(s)?))
}
fn quant_or_lamda(
&mut self,
full_id: TermId,
child_ids: BoxSlice<TermIdx>,
num_vars: NonMaxU32,
kind: QuantKind,
) -> Result<()> {
let qidx = self.quantifiers.next_key();
let tidx = self.new_term(full_id, TermKind::Quant(qidx), child_ids)?;
let q = Quantifier {
num_vars,
term: tidx,
kind,
vars: None,
blame: None,
};
self.quantifiers.raw.try_reserve(1)?;
let qidx2 = self.quantifiers.push_and_get_key(q);
debug_assert_eq!(qidx, qidx2);
Ok(())
}
fn parse_arith(meaning: &str) -> Result<BigRational> {
let (rest, num) = Self::parse_arith_inner(meaning)?;
debug_assert!(rest.is_empty());
Ok(num.into())
}
fn parse_arith_inner(meaning: &str) -> Result<(&str, num::BigRational)> {
let Some(meaning) = meaning.strip_prefix('(') else {
let end = meaning
.bytes()
.position(|b| !b.is_ascii_digit())
.unwrap_or(meaning.len());
assert_ne!(end, 0);
let value = meaning[..end]
.parse::<num::BigUint>()
.map_err(E::ParseBigUintError)?;
let value = num::BigRational::from(num::BigInt::from(value));
return Ok((&meaning[end..], value));
};
let error = || E::ParseError(meaning.to_owned());
let space = meaning.bytes().position(|b| b == b' ').ok_or_else(error)?;
let (op, mut rest) = (&meaning[..space], &meaning[space..]);
let mut arguments = Vec::new();
while let Some(r) = rest.strip_prefix(' ') {
let (r, num) = Self::parse_arith_inner(r)?;
arguments.push(num);
rest = r;
}
rest = rest.strip_prefix(')').ok_or_else(error)?;
match op {
"+" => Ok((rest, arguments.into_iter().sum())),
"-" if arguments.len() == 1 => Ok((rest, -arguments.into_iter().next().unwrap())),
"-" if arguments.len() == 2 => {
let mut args = arguments.into_iter();
Ok((rest, args.next().unwrap() - args.next().unwrap()))
}
"*" => Ok((rest, arguments.into_iter().product())),
"/" if arguments.len() == 2 => {
let mut args = arguments.into_iter();
Ok((rest, args.next().unwrap() / args.next().unwrap()))
}
_ => Err(error()),
}
}
fn parse_literal<'a>(
&mut self,
l: &mut impl Iterator<Item = &'a str>,
) -> Result<Option<(Assignment, Option<ENodeIdx>)>> {
let Some(lit) = l.next() else {
return Ok(None);
};
let (lit, value) = match lit {
"true" | "false" => return Err(E::BoolLiteral),
"(not" => {
let lit = l.next().ok_or(E::UnexpectedNewline)?;
let lit = lit.strip_suffix(')').ok_or(E::TupleMissingParens)?;
(lit, false)
}
_ => (lit, true),
};
let literal = self.parse_existing_app(lit)?;
let enode = self.get_existing_enode(literal).ok();
Ok(Some((Assignment { literal, value }, enode)))
}
fn parse_bool_literal<'a>(
version_info: &VersionInfo,
l: &mut impl Iterator<Item = &'a str>,
) -> Result<Option<(Option<NonZeroU32>, bool)>> {
let Some(lit) = l.next() else {
return Ok(None);
};
match lit {
"" => {
debug_assert_eq!(l.next().filter(|n| !n.is_empty()), None);
return Ok(None);
}
"true" => return Ok(Some((None, true))),
"false" => return Ok(Some((None, false))),
_ => (),
};
let new_mode = version_info.is_ge_version(4, 8, 10);
let (lit, value) = if new_mode {
let noneg = lit.strip_prefix('-');
(noneg.unwrap_or(lit), noneg.is_none())
} else {
let (lit, value) = if lit == "(not" {
let lit = l.next().ok_or(E::UnexpectedNewline)?;
let lit = lit.strip_suffix(')').ok_or(E::TupleMissingParens)?;
(lit, false)
} else {
(lit, true)
};
(lit.strip_prefix('p').ok_or(E::BoolLiteralNotP)?, value)
};
let bool_lit = lit.parse::<NonZeroU32>().map_err(E::InvalidBoolLiteral)?;
Ok(Some((Some(bool_lit), value)))
}
}
impl Z3LogParser for Z3Parser {
fn newline(&mut self) {
self.comm.newline();
}
fn version_info<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
let solver = l.next().ok_or(E::UnexpectedNewline)?.to_string();
let version = l.next().ok_or(E::UnexpectedNewline)?;
Self::expect_completed(l)?;
let version = semver::Version::parse(version)?;
eprintln!("{solver} {version}");
self.version_info = VersionInfo::Present { solver, version };
Ok(())
}
fn mk_quant<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
let full_id = self.parse_new_full_id(l.next())?;
let (quant_name, num_vars) = self.parse_qid(&mut l)?;
let quant_name = QuantKind::parse(&mut self.strings, &quant_name);
let child_ids = Self::map(l, |id| self.parse_existing_app(id))?;
debug_assert!(!child_ids.is_empty());
let child_id_names = || {
child_ids[..child_ids.len() - 1]
.iter()
.map(|&id| self[id].app_name().map(|name| &self[name]))
};
debug_assert!(
child_id_names().all(|name| name.is_some_and(|name| name == "pattern")),
"Expected all but last child to be \"pattern\" but found {:?}",
child_id_names().collect::<Vec<_>>()
);
self.quant_or_lamda(full_id, child_ids, num_vars, quant_name)
}
fn mk_lambda<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
let full_id = self.parse_new_full_id(l.next())?;
let lambda = l.next().ok_or(E::UnexpectedNewline)?;
self.check_lambda_name(lambda)?;
let num_vars = l.next().ok_or(E::UnexpectedNewline)?;
let num_vars = num_vars
.parse::<NonMaxU32>()
.map_err(E::InvalidQVarInteger)?;
let child_ids = Self::map(l, |id| self.parse_existing_proof(id))?;
let kind = QuantKind::Lambda(child_ids);
self.quant_or_lamda(full_id, Default::default(), num_vars, kind)
}
fn mk_var<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
let full_id = self.parse_new_full_id(l.next())?;
let kind = l.next().ok_or(E::UnexpectedNewline)?;
let kind = TermKind::parse_var(kind)?;
Self::expect_completed(l)?;
self.new_term(full_id, kind, Default::default())?;
Ok(())
}
fn mk_app<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
let id_str = l.next().ok_or(E::UnexpectedNewline)?;
let mut id = TermId::parse(&mut self.strings, id_str)?;
let (name, child) = self.parse_app_name(&mut l)?;
debug_assert!(id_str != "#1" || name == "true");
debug_assert!(id_str != "#2" || name == "false");
self.terms
.check_get_model(&mut id, &name, &mut self.strings);
let name = self.mk_string(&name)?;
let child = child.into_iter().map(Ok);
let child_ids = child.chain(l.map(|id| TermId::parse(&mut self.strings, id)));
let child_ids = Self::map(child_ids, |id| self.terms.parse_app_child_id(id?))?;
let tidx = self.new_term(id, TermKind::App(name), child_ids)?;
self.events
.new_term(tidx, &self.terms[tidx], &self.strings)?;
Ok(())
}
fn mk_proof<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
let full_id = self.parse_new_full_id(l.next())?;
let name = l.next().ok_or(E::UnexpectedNewline)?;
let kind = match name.parse() {
Ok(kind) => kind,
Err(_) => {
debug_assert!(false, "Unknown proof step kind {name:?}");
ProofStepKind::OTHER(self.mk_string(name)?)
}
};
let mut next = l.next().ok_or(E::UnexpectedNewline)?;
let mut prerequisites = Vec::new();
for n in l {
let curr = next;
next = n;
let prereq = self.parse_existing_proof(curr)?;
prerequisites.push(prereq);
}
let result = self.parse_existing_app(next)?;
let proof_step = ProofStep {
id: full_id,
kind,
result,
prerequisites: prerequisites.into(),
frame: self.stack.active_frame(),
};
let proof_idx = self.terms.proof_terms.new_term(proof_step)?;
self.terms
.new_proof(&mut self.quantifiers, proof_idx, &self.strings)?;
self.egraph
.new_proof(result, proof_idx, &self.terms, &self.stack)?;
self.events.new_proof_step(
proof_idx,
&self.terms[proof_idx],
&self.terms,
&self.strings,
)
}
fn attach_meaning<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
let id = l.next().ok_or(E::UnexpectedNewline)?;
let theory = l.next().ok_or(E::UnexpectedNewline)?;
let value = l.collect::<Vec<_>>().join(" ");
let meaning = match theory {
"arith" => {
let num = Self::parse_arith(&value)?;
Meaning::Arith(Box::new(num))
}
"bv" => {
let (value, bits) = if let Some(data) = value.strip_prefix("#x") {
let value = num::BigUint::from_str_radix(data, 16);
(value, data.len() as u32 * 4)
} else if let Some(data) = value.strip_prefix("#b") {
let value = num::BigUint::from_str_radix(data, 2);
(value, data.len() as u32)
} else {
return Err(E::ParseError(value));
};
let value = BitVec {
value: value.map_err(E::ParseBigUintError)?.into(),
bits,
};
Meaning::BitVec(Box::new(value))
}
theory => {
let theory = self.mk_string(theory)?;
let value = self.mk_string(&value)?;
Meaning::Unknown { theory, value }
}
};
let idx = self.parse_existing_app(id)?;
let idx = self.terms.new_meaning(idx, meaning)?;
let meaning = self.terms.meaning(idx).unwrap();
self.events.new_meaning(idx, meaning, &self.strings)
}
fn attach_var_names<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
let id = l.next().ok_or(E::UnexpectedNewline)?;
let var_names = self.gobble_var_names_list(l)?;
let tidx = self.parse_existing_app(id)?;
let qidx = self.terms.quant(tidx)?;
let quant = &mut self.quantifiers[qidx];
debug_assert_eq!(quant.num_vars.get() as usize, var_names.len());
debug_assert!(quant.vars.is_none());
quant.vars = Some(var_names);
Ok(())
}
fn attach_enode<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
let id = l.next().ok_or(E::UnexpectedNewline)?;
let idx = self.parse_existing_app(id);
let Ok(idx) = idx else {
if self.version_info.is_version(4, 8, 7) {
return Ok(());
} else {
return idx.map(|_| ());
}
};
let z3_gen = Self::parse_z3_generation(&mut l)?.ok_or(E::UnexpectedNewline)?;
Self::expect_completed(l)?;
debug_assert!(self[idx].app_name().is_some());
let iidx = self.active_inst(idx)?;
let blame = self.egraph.get_blame(idx, iidx, &self.terms, &self.stack);
let enode = self.egraph.new_enode(blame, idx, z3_gen, &self.stack)?;
self.events.new_enode();
if let Some(a) = self.insts.active_inst() {
a.yields.try_reserve(1)?;
a.yields.push(enode);
let idx = a.idx;
debug_assert!(self.insts.insts[idx]
.kind
.z3_generation()
.is_none_or(|g| g == z3_gen));
}
Ok(())
}
fn eq_expl<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
let from = self.parse_existing_enode(l.next().ok_or(E::UnexpectedNewline)?)?;
let kind = l.next().ok_or(E::UnexpectedNewline)?;
let eq_expl = {
let mut kind_dependent_info = Self::iter_until_eq(l.by_ref(), ";");
match kind {
"root" => EqualityExpl::Root { id: from },
"lit" => {
let eq = kind_dependent_info.next().ok_or(E::UnexpectedEnd)?;
let eq = self.parse_existing_enode(eq)?;
Self::expect_completed(kind_dependent_info)?;
let to = self.parse_existing_enode(l.next().ok_or(E::UnexpectedNewline)?)?;
let eq = self.lits.get_assign(self[eq].owner, &self.stack);
let eq = eq.ok_or(E::UnknownEqLit)?;
EqualityExpl::Literal { from, eq, to }
}
"cg" => {
let mut arg_eqs = Vec::new();
for t in Self::gobble_tuples::<true>(kind_dependent_info) {
let (from, to) = t?;
let from = self.parse_existing_enode(from)?;
let to = self.parse_existing_enode(to)?;
arg_eqs.push((from, to));
}
let to = self.parse_existing_enode(l.next().ok_or(E::UnexpectedNewline)?)?;
EqualityExpl::Congruence {
from,
arg_eqs: arg_eqs.into_boxed_slice(),
to,
uses: Vec::new(),
}
}
"th" => {
let theory = kind_dependent_info.next().ok_or(E::UnexpectedEnd)?;
let theory = TheoryKind::from_name(theory, &mut self.strings);
Self::expect_completed(kind_dependent_info)?;
let to = self.parse_existing_enode(l.next().ok_or(E::UnexpectedNewline)?)?;
EqualityExpl::Theory { from, theory, to }
}
"ax" => {
Self::expect_completed(kind_dependent_info)?;
let to = self.parse_existing_enode(l.next().ok_or(E::UnexpectedNewline)?)?;
EqualityExpl::Axiom { from, to }
}
kind => {
let args = kind_dependent_info
.map(|s| self.mk_string(s))
.collect::<Result<_>>()?;
let to = self.parse_existing_enode(l.next().ok_or(E::UnexpectedNewline)?)?;
EqualityExpl::Unknown {
kind: self.mk_string(kind)?,
from,
args,
to,
}
}
}
};
Self::expect_completed(l)?;
self.egraph.new_given_equality(from, eq_expl, &self.stack)?;
Ok(())
}
fn new_match<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
let fingerprint = l.next().ok_or(E::UnexpectedNewline)?;
let fingerprint = Fingerprint::parse(fingerprint)?;
let idx = l.next().ok_or(E::UnexpectedNewline)?;
let idx = self.parse_existing_app(idx)?;
let quant = self.terms.quant(idx)?;
let pattern = l.next().ok_or(E::UnexpectedNewline)?;
let pattern = self.parse_existing_app(pattern)?;
let pattern = self
.patterns(quant)
.ok_or(E::NewMatchOnLambda(quant))?
.position(|p| *p == pattern)
.ok_or(E::UnknownPatternIdx(pattern))?;
let bound_terms = Self::iter_until_eq(&mut l, ";");
let is_axiom = fingerprint.is_zero();
let kind = if is_axiom {
let bound_terms = bound_terms
.map(|id| self.parse_existing_app(id))
.collect::<Result<BoxSlice<_>>>()?;
debug_assert!(bound_terms
.iter()
.all(|&b| !self[b].has_var().unwrap_or(true)));
MatchKind::Axiom {
axiom: quant,
pattern,
bound_terms,
}
} else {
let bound_terms = bound_terms
.map(|id| self.parse_existing_enode(id))
.collect::<Result<BoxSlice<_>>>()?;
debug_assert!(bound_terms
.iter()
.all(|&b| !self[self[b].owner].has_var().unwrap_or(true)));
MatchKind::Quantifier {
quant,
pattern,
bound_terms,
}
};
let mut blamed = Vec::new();
let mut next = l.next();
while let Some(word) = next.take() {
let enode = self.parse_existing_enode(word)?;
let l = l.by_ref().take_while(|s| {
let cond = s.as_bytes().first().is_some_and(|f| *f == b'(')
|| s.as_bytes().last().is_some_and(|l| *l == b')');
if !cond {
next = Some(*s);
}
cond
});
let mut equalities = Vec::new();
self.append_trans_equality_tuples(l, |eq| {
equalities.try_reserve(1)?;
equalities.push(eq);
Ok(())
})?;
blamed.try_reserve(1)?;
blamed.push((blamed.len(), enode, equalities));
}
let pat = kind.quant_pat().unwrap();
let pat = self.get_pattern(pat).unwrap();
let (_correct_order, blamed) = self.make_blamed(&kind, blamed, pat)?;
let match_ = Match {
kind,
blamed,
frame: self.stack.active_frame(),
};
debug_assert_eq!(match_.pattern_matches().count(), self[pat].child_ids.len());
debug_assert!(match_
.pattern_matches()
.zip(self[pat].child_ids.iter())
.all(|(m, s)| self.check_match(&match_.kind, m, *s)));
self.insts.new_match(fingerprint, match_)?;
Ok(())
}
fn inst_discovered<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
let method = l.next().ok_or(E::UnexpectedNewline)?;
let fingerprint = Fingerprint::parse(l.next().ok_or(E::UnexpectedNewline)?)?;
let (kind, blamed) = match method {
"theory-solving" => {
debug_assert!(
fingerprint.is_zero(),
"Theory solving should have zero fingerprint"
);
let axiom_id = l.next().ok_or(E::UnexpectedNewline)?;
let axiom_id = TermId::parse(&mut self.strings, axiom_id)?;
let bound_terms = Self::iter_until_eq(&mut l, ";")
.map(|id| self.parse_existing_app(id))
.collect::<Result<_>>()?;
let mut blamed = Vec::new();
let mut rewrite_of = None;
for word in l.by_ref() {
let term = self.parse_existing_app(word)?;
if let Ok(enode) = self.get_existing_enode(term) {
if let Some(rewrite_of) = rewrite_of {
return Err(E::NonRewriteAxiomInvalidEnode(rewrite_of));
}
blamed.try_reserve(1)?;
blamed.push(Blame {
coupling: Coupling::Exact,
enode,
equalities: Default::default(),
});
} else {
if let Some(rewrite_of) = rewrite_of {
return Err(E::RewriteAxiomMultipleTerms1(rewrite_of));
}
if !blamed.is_empty() {
return Err(E::RewriteAxiomMultipleTerms2(blamed));
}
rewrite_of = Some(term);
}
}
let kind = MatchKind::TheorySolving {
axiom_id,
bound_terms,
rewrite_of,
};
(kind, blamed)
}
"MBQI" => {
let quant = self.parse_existing_app(l.next().ok_or(E::UnexpectedNewline)?)?;
let quant = self.terms.quant(quant)?;
let bound_terms = l
.map(|id| self.parse_existing_enode(id))
.collect::<Result<_>>()?;
let kind = MatchKind::MBQI { quant, bound_terms };
(kind, Vec::new())
}
_ => return Err(E::UnknownInstMethod(method.to_string())),
};
let match_ = Match {
kind,
blamed: blamed.into(),
frame: self.stack.active_frame(),
};
self.insts.new_match(fingerprint, match_)?;
Ok(())
}
fn instance<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
let fingerprint = l.next().ok_or(E::UnexpectedNewline)?;
let fingerprint = Fingerprint::parse(fingerprint)?;
let mut proof = Self::iter_until_eq(&mut l, ";");
let proof_str = proof.next();
Self::expect_completed(proof)?;
let z3_generation = Self::parse_z3_generation(&mut l)?;
let kind = if let Some(z3_generation) = z3_generation {
debug_assert!(!fingerprint.is_zero());
let proof = if let Some(proof) = proof_str {
let proof = self.parse_existing_proof(proof)?;
InstProofLink::HasProof(proof)
} else {
let last_term = self.terms.last_term_from_instance(&self.strings);
InstProofLink::ProofsDisabled(last_term)
};
InstantiationKind::NonAxiom {
fingerprint,
z3_generation,
proof,
}
} else {
debug_assert!(fingerprint.is_zero());
let proof = proof_str.expect("Axiom instantiations should have an associated term");
let body = self.parse_existing_app(proof)?;
InstantiationKind::Axiom { body }
};
let match_ = self
.insts
.get_match(fingerprint)
.ok_or(E::UnknownFingerprint(fingerprint))?;
let inst = Instantiation {
match_,
kind,
yields_terms: Default::default(),
frame: self.stack.active_frame(),
};
let body = self.instance_body(kind.proof(), match_);
let can_duplicate = self.version_info.is_ge_version(4, 12, 0);
self.insts
.new_inst(fingerprint, inst, body, &self.stack, can_duplicate)?;
self.events.new_inst();
Ok(())
}
fn end_of_instance<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()> {
self.insts.end_inst()?;
Self::expect_completed(l)
}
fn eof(&mut self) {
self.synth_terms.eof(self.terms().next_key());
self.events.new_eof();
}
fn assign<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
let created_by = self.insts.active_inst();
let iidx = created_by.as_ref().map(|a| a.idx);
let (assign, enode) = self.parse_literal(&mut l)?.ok_or(E::UnexpectedNewline)?;
let lit = self.lits.new_literal(assign, iidx, enode, &self.stack)?;
let mut justification = l.next().ok_or(E::UnexpectedNewline)?;
let decision = justification == "decision";
if decision {
let llk = self.comm.prev().last_line_kind;
if matches!(llk, LineKind::Push) && self.stack.new_decision() {
self.push_count -= 1;
self.events.undo_push();
}
self.lits.cdcl.new_decision(lit, &self.stack)?;
justification = l.next().ok_or(E::UnexpectedNewline)?;
debug_assert_eq!(justification, "axiom");
}
match justification {
"axiom" => {
Self::expect_completed(l)?;
let kind = if decision {
JustificationKind::Decision
} else {
JustificationKind::Axiom
};
self.lits.justification(lit, kind, core::iter::empty())?;
Ok(())
}
"bin" => {
let other = Self::parse_bool_literal(&self.version_info, &mut l)?
.ok_or(E::UnexpectedNewline)?;
Self::expect_completed(l)?;
let _j = self.lits.justification(
lit,
JustificationKind::Propagate,
[Ok(other)].into_iter(),
)?;
#[cfg(any())]
debug_assert_ne!(lit, j.blamed[0]);
self.lits.cdcl.new_propagate(lit, &self.stack)?;
Ok(())
}
"clause" => {
let _first = Self::parse_bool_literal(&self.version_info, &mut l)?
.ok_or(E::UnexpectedNewline)?;
let lits = core::iter::from_fn(|| {
Self::parse_bool_literal(&self.version_info, &mut l).transpose()
});
self.lits
.justification(lit, JustificationKind::Propagate, lits)?;
#[cfg(any())]
let c0 = self.lits.literal_to_term(first, false)?;
#[cfg(any())]
if lit != c0 {
eprintln!(
"Unexpected clause literal: {lit} != {c0} ({first:?}) / {:?}",
self.lits.lit_stack
);
return Err(E::UnexpectedEnd);
}
#[cfg(any())]
debug_assert_eq!(lit, c0, "{first:?}");
self.lits.cdcl.new_propagate(lit, &self.stack)?;
Ok(())
}
"justification" => {
let theory_id = l.next().ok_or(E::UnexpectedNewline)?;
let theory_id = theory_id
.strip_suffix(':')
.ok_or(E::MissingColonJustification)?;
let theory_id = theory_id.parse::<i32>().map_err(E::InvalidTheoryId)?;
let theory = TheoryKind::from_id(theory_id);
let lits = core::iter::from_fn(|| {
Self::parse_bool_literal(&self.version_info, &mut l).transpose()
});
self.lits
.justification(lit, JustificationKind::Theory(theory), lits)?;
Ok(())
}
_ => Err(E::UnknownJustification(justification.to_string())),
}
}
fn decide_and_or<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()> {
self.comm.curr().last_line_kind = LineKind::DecideAndOr;
Ok(())
}
fn conflict<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
self.comm.curr().last_line_kind = LineKind::Conflict;
let mut cut = Vec::new();
while let Some((assignment, _)) = self.parse_literal(&mut l)? {
cut.try_reserve(1)?;
cut.push(assignment);
}
let frame = self.stack.active_frame();
debug_assert!(self.lits.curr_to_root_unique());
self.lits.cdcl.new_conflict(cut.into_boxed_slice(), frame);
Ok(())
}
fn push<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
self.comm.curr().last_line_kind = LineKind::Push;
let scope = l.next().ok_or(E::UnexpectedNewline)?;
let scope = scope.parse::<usize>().map_err(E::InvalidFrameInteger)?;
Self::expect_completed(l)?;
let from_cdcl = matches!(self.comm.prev().last_line_kind, LineKind::DecideAndOr);
let from_cdcl = from_cdcl || self.stack.is_speculative();
self.stack.new_frame(scope, from_cdcl)?;
if !from_cdcl {
self.push_count += 1;
}
self.events.new_push(from_cdcl)?;
Ok(())
}
fn pop<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
let num = l.next().ok_or(E::UnexpectedNewline)?;
let num = num
.parse::<NonZeroUsize>()
.map_err(E::InvalidFrameInteger)?;
let scope = l.next().ok_or(E::UnexpectedNewline)?;
let scope = scope.parse::<usize>().map_err(E::InvalidFrameInteger)?;
Self::expect_completed(l)?;
let conflict = matches!(self.comm.prev().last_line_kind, LineKind::Conflict);
debug_assert_eq!(conflict, self.lits.cdcl.has_conflict());
let from_cdcl = self.stack.pop_frames(num, scope, conflict)?;
if conflict {
self.lits.cdcl.backtrack(&self.stack)?;
}
self.events.new_pop(num, from_cdcl)
}
fn begin_check<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Result<()> {
let scope = l.next().ok_or(E::UnexpectedNewline)?;
let scope = scope.parse::<usize>().map_err(E::InvalidFrameInteger)?;
self.stack.ensure_height(scope)?;
self.lits
.cdcl
.begin_check(self.incremental_mode(), &self.stack)?;
self.events.new_begin_check()
}
}