use crate::Btor;
use giputils::{bitvec::BitVec, hash::GHashMap};
use logicrs::fol::{
Sort, Term,
op::{self, DynOp},
};
use num_bigint::{BigInt, Sign};
use num_traits::Num;
#[derive(Default)]
pub struct Parser {
sorts: GHashMap<usize, Sort>,
nodes: GHashMap<usize, Term>,
input: Vec<Term>,
latch: Vec<Term>,
init: GHashMap<Term, Term>,
next: GHashMap<Term, Term>,
output: Vec<Term>,
bad: Vec<Term>,
constraint: Vec<Term>,
symbols: GHashMap<Term, String>,
}
impl Parser {
#[inline]
fn get_node(&self, nid: isize) -> Term {
let abs: usize = nid.unsigned_abs();
let mut res = self.nodes.get(&abs).unwrap().clone();
if nid < 0 {
res = !res;
}
res
}
fn parse_sort<'a>(&self, mut split: impl Iterator<Item = &'a str>) -> Sort {
match split.next().unwrap() {
"bitvec" => {
let w = split.next().unwrap().parse::<usize>().unwrap();
Sort::Bv(w)
}
"array" => {
let index = parse_id(&mut split);
let element = parse_id(&mut split);
let index = self.sorts.get(&index).unwrap();
let element = self.sorts.get(&element).unwrap();
if element.is_array() {
panic!("currently arrays of arrays are not supported");
}
Sort::Array(index.bv(), element.bv())
}
_ => panic!(),
}
}
fn parse_symbol<'a>(&mut self, t: &Term, mut split: impl Iterator<Item = &'a str>) {
if let Some(symbol) = split.next() {
self.symbols.insert(t.clone(), symbol.to_string());
}
}
pub fn parse(mut self, s: &str) -> Btor {
for line in s.lines() {
if line.starts_with(';') {
continue;
}
let mut split = line.split_whitespace();
let Some(id) = split.next() else {
continue;
};
let id = id.parse().unwrap();
let second = split.next().unwrap();
match second {
"sort" => {
let sort = self.parse_sort(split);
assert!(self.sorts.insert(id, sort).is_none());
}
"input" => {
let sort = *self.sorts.get(&parse_id(&mut split)).unwrap();
let v = Term::new_var(sort);
self.input.push(v.clone());
self.parse_symbol(&v, split);
assert!(self.nodes.insert(id, v).is_none());
}
"state" => {
let sort = *self.sorts.get(&parse_id(&mut split)).unwrap();
let v = Term::new_var(sort);
self.latch.push(v.clone());
self.parse_symbol(&v, split);
assert!(self.nodes.insert(id, v).is_none());
}
"init" => {
let _sort = self.sorts.get(&parse_id(&mut split)).unwrap();
let state = self.get_node(parse_signed_id(&mut split));
let value = self.get_node(parse_signed_id(&mut split));
self.init.insert(state, value);
}
"next" => {
let sort = self.sorts.get(&parse_id(&mut split)).unwrap();
let state = self.get_node(parse_signed_id(&mut split));
let value = self.get_node(parse_signed_id(&mut split));
assert!(state.sort().eq(sort));
assert!(value.sort().eq(sort));
self.next.insert(state, value);
}
"output" => {
let o = self.get_node(parse_signed_id(&mut split));
self.parse_symbol(&o, split);
self.output.push(o);
}
"bad" => {
let b = self.get_node(parse_signed_id(&mut split));
self.parse_symbol(&b, split);
self.bad.push(b);
}
"constraint" => {
let c = self.get_node(parse_signed_id(&mut split));
self.parse_symbol(&c, split);
self.constraint.push(c);
}
"const" | "constd" | "consth" => {
let ty = ConstType::try_from(second).unwrap();
let sort = *self.sorts.get(&parse_id(&mut split)).unwrap();
let Sort::Bv(w) = sort else { todo!() };
let c = split.next().unwrap();
let radix = match ty {
ConstType::Const => 2,
ConstType::Constd => 10,
ConstType::Consth => 16,
};
let c = BigInt::from_str_radix(c, radix).unwrap();
let (s, c) = c.to_radix_le(2);
let mut c: Vec<bool> = c.into_iter().map(|x| x == 1).collect();
assert!(c.len() <= w);
while c.len() < w {
c.push(false);
}
if let Sign::Minus = s {
c = c.into_iter().map(|x| !x).collect();
let mut carry = true;
for i in c.iter_mut() {
if !carry {
break;
}
let ni = *i ^ carry;
carry = *i && carry;
*i = ni;
}
}
assert!(
self.nodes
.insert(id, Term::bv_const(BitVec::from(&c)))
.is_none()
);
}
"zero" => {
let sort = *self.sorts.get(&parse_id(&mut split)).unwrap();
assert!(
self.nodes
.insert(id, Term::bv_const(BitVec::zero(sort.bv())))
.is_none()
);
}
"one" => {
let sort = *self.sorts.get(&parse_id(&mut split)).unwrap();
assert!(
self.nodes
.insert(id, Term::bv_const(BitVec::one(sort.bv())))
.is_none()
);
}
"ones" => {
let sort = *self.sorts.get(&parse_id(&mut split)).unwrap();
assert!(
self.nodes
.insert(id, Term::bv_const(BitVec::ones(sort.bv())))
.is_none()
);
}
_ => {
let term = self.parse_op(second, split);
assert!(self.nodes.insert(id, term).is_none());
}
}
}
Btor {
input: self.input,
latch: self.latch,
init: self.init,
next: self.next,
bad: self.bad,
constraint: self.constraint,
symbols: self.symbols,
}
}
fn parse_op<'a>(&mut self, second: &str, mut split: impl Iterator<Item = &'a str>) -> Term {
let op = DynOp::from(second);
let sort = self.sorts.get(&parse_id(&mut split)).unwrap();
let mut operand = Vec::new();
if op == op::Uext || op == op::Sext {
let opa = self.get_node(parse_signed_id(&mut split));
let ext_len: usize = split.next().unwrap().parse().unwrap();
if ext_len == 0 {
return opa;
} else {
let ext_len = Term::bv_const(BitVec::zero(ext_len));
operand.push(opa);
operand.push(ext_len);
}
} else if op == op::Slice {
let opa = self.get_node(parse_signed_id(&mut split));
let high: usize = split.next().unwrap().parse().unwrap();
let low: usize = split.next().unwrap().parse().unwrap();
operand.push(opa);
operand.push(Term::bv_const(BitVec::zero(high)));
operand.push(Term::bv_const(BitVec::zero(low)));
} else {
for _ in 0..op.num_operand() {
operand.push(self.get_node(parse_signed_id(&mut split)));
}
}
let res = Term::new_op(op, &operand);
assert!(res.sort().eq(sort));
res
}
}
#[derive(Debug, Clone, strum::EnumString, strum::Display)]
#[strum(serialize_all = "lowercase")]
pub enum ConstType {
Const = 2,
Constd = 10,
Consth = 16,
}
#[inline]
fn parse_id<'a>(split: &mut impl Iterator<Item = &'a str>) -> usize {
split.next().unwrap().parse().unwrap()
}
#[inline]
fn parse_signed_id<'a>(split: &mut impl Iterator<Item = &'a str>) -> isize {
split.next().unwrap().parse().unwrap()
}