Skip to content

Support IEEE floating point SMT theory #2229

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Chris-Hawblitzel merged 8 commits into from
Mar 16, 2026
Merged

Support IEEE floating point SMT theory #2229

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
5e1842f
Support IEEE floating point SMT theory
Chris-Hawblitzel Mar 6, 2026
5ce68c9
Add assume_ieee_float.rs
Chris-Hawblitzel Mar 6, 2026
4cf145f
vargo fmt
Chris-Hawblitzel Mar 6, 2026
fa99273
Merge branch 'main' into ieee-float
Chris-Hawblitzel Mar 6, 2026
893e340
Split assume_ieee_float off into a separate pull request
Chris-Hawblitzel Mar 7, 2026
c81de7a
Address comments
Chris-Hawblitzel Mar 9, 2026
caf6b70
Explicitly mark real->real case as unreachable
Chris-Hawblitzel Mar 9, 2026
5d0b9cf
Merge branch 'main' into ieee-float
Chris-Hawblitzel Mar 16, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 44 additions & 0 deletions source/air/src/ast.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,13 @@ pub enum TypX {
// Fun deliberately omits argument, return types to make box/unbox for generics easier
Fun,
Named(Ident),
// Bit vector; the u32 is the number of bits (e.g. (_ BitVec 64) is BitVec(64))
BitVec(u32),
// IEEE floating point type with exp_bits exponent bits and sig_bits significand bits,
// counting the implicit leading 1 bit in the significand
// (e.g. f32 is Float { exp_bits: 8, sig_bits: 24 })
// See https://smt-lib.org/theories-FloatingPoint.shtml
Float { exp_bits: u32, sig_bits: u32 },
}

#[derive(Clone, PartialEq, Eq, Hash)] // for Debug, see ast_util
Expand All @@ -35,6 +41,20 @@ pub enum Constant {
BitVec(Arc<String>, u32),
}

#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
pub enum RoundingMode {
// roundNearestTiesToEven
RNE,
// roundNearestTiesToAway
RNA,
// roundTowardPositive
RTP,
// roundTowardNegative
RTN,
// roundTowardZero
RTZ,
}

#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
pub enum UnaryOp {
Not,
Expand All @@ -43,6 +63,19 @@ pub enum UnaryOp {
BitExtract(u32, u32),
BitZeroExtend(u32),
BitSignExtend(u32),
FloatNeg,
FloatRoundToInt(RoundingMode),
FloatIsNormal,
FloatIsSubnormal,
FloatIsZero,
FloatIsInfinite,
FloatIsNaN,
FloatIsNegative,
FloatIsPositive,
FloatFromIeeeBits { exp_bits: u32, sig_bits: u32 },
FloatFrom { exp_bits: u32, sig_bits: u32, signed: bool, round: RoundingMode },
FloatToBitVec { bits: u32, signed: bool, round: RoundingMode },
FloatToReal,
ToReal,
RealToInt,
}
Expand Down Expand Up @@ -102,6 +135,15 @@ pub enum BinaryOp {
LShr,
Shl,
BitConcat,
FloatAdd(RoundingMode),
FloatSub(RoundingMode),
FloatMul(RoundingMode),
FloatDiv(RoundingMode),
FloatEq,
FloatLt,
FloatGt,
FloatLe,
FloatGe,
FieldUpdate(Ident),
}

Expand All @@ -114,6 +156,8 @@ pub enum MultiOp {
Sub,
Mul,
Distinct,
// (fp sign exp sig) constructor, taking bit vectors as arguments and returning a Float
Float,
}

pub type Binder<A> = Arc<BinderX<A>>;
Expand Down
34 changes: 33 additions & 1 deletion source/air/src/closure.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -551,6 +551,23 @@ fn simplify_expr(ctxt: &mut Context, state: &mut State, expr: &Expr) -> (Typ, Ex
TypX::BitVec(n) => Arc::new(TypX::BitVec(n + w)),
_ => panic!("internal error during processing bit extend"),
},
UnaryOp::FloatNeg => ts[0].0.clone(),
UnaryOp::FloatRoundToInt(_) => ts[0].0.clone(),
UnaryOp::FloatIsNormal => Arc::new(TypX::Bool),
UnaryOp::FloatIsSubnormal => Arc::new(TypX::Bool),
UnaryOp::FloatIsZero => Arc::new(TypX::Bool),
UnaryOp::FloatIsInfinite => Arc::new(TypX::Bool),
UnaryOp::FloatIsNaN => Arc::new(TypX::Bool),
UnaryOp::FloatIsNegative => Arc::new(TypX::Bool),
UnaryOp::FloatIsPositive => Arc::new(TypX::Bool),
UnaryOp::FloatFromIeeeBits { exp_bits, sig_bits } => {
Arc::new(TypX::Float { exp_bits: *exp_bits, sig_bits: *sig_bits })
}
UnaryOp::FloatFrom { exp_bits, sig_bits, signed: _, round: _ } => {
Arc::new(TypX::Float { exp_bits: *exp_bits, sig_bits: *sig_bits })
}
UnaryOp::FloatToBitVec { bits, .. } => Arc::new(TypX::BitVec(*bits)),
UnaryOp::FloatToReal => Arc::new(TypX::Real),
UnaryOp::ToReal => Arc::new(TypX::Real),
UnaryOp::RealToInt => Arc::new(TypX::Int),
};
Expand All @@ -570,6 +587,11 @@ fn simplify_expr(ctxt: &mut Context, state: &mut State, expr: &Expr) -> (Typ, Ex
BinaryOp::BitSGt | BinaryOp::BitSLt | BinaryOp::BitSGe | BinaryOp::BitSLe => {
Arc::new(TypX::Bool)
}
BinaryOp::FloatEq
| BinaryOp::FloatLt
| BinaryOp::FloatGt
| BinaryOp::FloatLe
| BinaryOp::FloatGe => Arc::new(TypX::Bool),
BinaryOp::BitXor
| BinaryOp::BitAnd
| BinaryOp::BitOr
Expand All @@ -582,7 +604,11 @@ fn simplify_expr(ctxt: &mut Context, state: &mut State, expr: &Expr) -> (Typ, Ex
| BinaryOp::LShr
| BinaryOp::AShr
| BinaryOp::Shl
| BinaryOp::BitURem => {
| BinaryOp::BitURem
| BinaryOp::FloatAdd(_)
| BinaryOp::FloatSub(_)
| BinaryOp::FloatMul(_)
| BinaryOp::FloatDiv(_) => {
assert!(typ_eq(&(ts[0].0), &(ts[1].0)));
ts[0].0.clone()
}
Expand All @@ -607,6 +633,12 @@ fn simplify_expr(ctxt: &mut Context, state: &mut State, expr: &Expr) -> (Typ, Ex
}
}
MultiOp::Distinct => Arc::new(TypX::Bool),
MultiOp::Float => match (&*ts[0].0, &*ts[1].0, &*ts[2].0) {
(TypX::BitVec(1), TypX::BitVec(exp_bits), TypX::BitVec(sig1_bits)) => {
Arc::new(TypX::Float { exp_bits: *exp_bits, sig_bits: *sig1_bits + 1 })
}
_ => panic!("internal error during processing float"),
},
};
let (es, t) = enclose(state, App::Multi(*op), es, ts);
(typ, Arc::new(ExprX::Multi(*op, Arc::new(es))), t)
Expand Down
120 changes: 117 additions & 3 deletions source/air/src/parser.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
use crate::ast::{
Axiom, BinaryOp, BindX, Binder, BinderX, Binders, Command, CommandX, Commands, Constant, Decl,
DeclX, Decls, Expr, ExprX, Exprs, Ident, MultiOp, Qid, Quant, QueryX, Relation, Stmt, StmtX,
Stmts, Trigger, Triggers, Typ, TypX, UnaryOp,
DeclX, Decls, Expr, ExprX, Exprs, Ident, MultiOp, Qid, Quant, QueryX, Relation, RoundingMode,
Stmt, StmtX, Stmts, Trigger, Triggers, Typ, TypX, UnaryOp,
};
use crate::def::mk_skolem_id;
use crate::messages::ArcDynMessageLabel;
Expand Down Expand Up @@ -35,6 +35,23 @@ fn is_bitvec(nodes: &Vec<Node>) -> Option<u32> {
None
}

fn is_float_type(nodes: &Vec<Node>) -> Option<Typ> {
if nodes[0] == Node::Atom("_".to_string())
&& nodes[1] == Node::Atom("FloatingPoint".to_string())
&& nodes.len() == 4
{
if let (Node::Atom(s2), Node::Atom(s3)) = (&nodes[2], &nodes[3]) {
match (s2.parse::<u32>(), s3.parse::<u32>()) {
(Ok(exp_bits), Ok(sig_bits)) => {
return Some(Arc::new(TypX::Float { exp_bits, sig_bits }));
}
_ => return None,
}
}
}
None
}

fn underscore_atom_atom_expr(s1: &str, s2: &str) -> Option<Constant> {
let value = s1.strip_prefix("bv")?;
let width = s2.parse::<u32>().ok()?;
Expand Down Expand Up @@ -116,10 +133,25 @@ impl Parser {
Node::Atom(s) if s == "Int" => Ok(Arc::new(TypX::Int)),
Node::Atom(s) if s == "Real" => Ok(Arc::new(TypX::Real)),
Node::Atom(s) if s == "Fun" => Ok(Arc::new(TypX::Fun)),
Node::Atom(s) if s == "Float16" => {
Ok(Arc::new(TypX::Float { exp_bits: 5, sig_bits: 11 }))
}
Node::Atom(s) if s == "Float32" => {
Ok(Arc::new(TypX::Float { exp_bits: 8, sig_bits: 24 }))
}
Node::Atom(s) if s == "Float64" => {
Ok(Arc::new(TypX::Float { exp_bits: 11, sig_bits: 53 }))
}
Node::Atom(s) if s == "Float128" => {
Ok(Arc::new(TypX::Float { exp_bits: 15, sig_bits: 113 }))
}
Node::Atom(s) if is_symbol(s) => Ok(Arc::new(TypX::Named(Arc::new(s.clone())))),
Node::List(nodes) if is_bitvec(nodes).is_some() => {
Ok(Arc::new(TypX::BitVec(is_bitvec(nodes).unwrap())))
}
Node::List(nodes) if is_float_type(nodes).is_some() => {
Ok(is_float_type(nodes).unwrap())
}
_ => Err(format!("expected type, found: {}", node_to_string(node))),
}
}
Expand Down Expand Up @@ -234,10 +266,82 @@ impl Parser {
}
_ => {}
}
let args = self.nodes_to_exprs(&nodes[1..])?;
let round = |args: &mut Exprs| {
Comment thread
Chris-Hawblitzel marked this conversation as resolved.
Arc::make_mut(args).remove(0);
match nodes.get(1) {
Some(Node::Atom(s)) => match s.as_str() {
"RNE" | "roundNearestTiesToEven" => Ok(RoundingMode::RNE),
"RNA" | "roundNearestTiesToAway" => Ok(RoundingMode::RNA),
"RTP" | "roundTowardPositive" => Ok(RoundingMode::RTP),
"RTN" | "roundTowardNegative" => Ok(RoundingMode::RTN),
"RTZ" | "roundTowardZero" => Ok(RoundingMode::RTZ),
_ => Err("expected rounding mode in fp operation"),
},
_ => Err("expected rounding mode in fp operation"),
}
};
let mut args = self.nodes_to_exprs(&nodes[1..])?;
let uop = match &nodes[0] {
Node::Atom(s) if s == "not" => Some(UnaryOp::Not),
Node::Atom(s) if s == "bvnot" => Some(UnaryOp::BitNot),
Node::Atom(s) if s == "bvneg" => Some(UnaryOp::BitNeg),
Node::Atom(s) if s == "fp.neg" => Some(UnaryOp::FloatNeg),
Node::Atom(s) if s == "fp.roundToIntegral" => {
Some(UnaryOp::FloatRoundToInt(round(&mut args)?))
}
Node::Atom(s) if s == "fp.isNormal" => Some(UnaryOp::FloatIsNormal),
Node::Atom(s) if s == "fp.isSubnormal" => Some(UnaryOp::FloatIsSubnormal),
Node::Atom(s) if s == "fp.isZero" => Some(UnaryOp::FloatIsZero),
Node::Atom(s) if s == "fp.isInfinite" => Some(UnaryOp::FloatIsInfinite),
Node::Atom(s) if s == "fp.isNaN" => Some(UnaryOp::FloatIsNaN),
Node::Atom(s) if s == "fp.isNegative" => Some(UnaryOp::FloatIsNegative),
Node::Atom(s) if s == "fp.isPositive" => Some(UnaryOp::FloatIsPositive),
Node::List(nodes)
if nodes.len() == 4
&& nodes[0] == Node::Atom("_".to_string())
&& (nodes[1] == Node::Atom("to_fp".to_string())
|| nodes[1] == Node::Atom("to_fp_unsigned".to_string())) =>
{
let signed = nodes[1] == Node::Atom("to_fp".to_string());
let exp_sig_bits = match (&nodes[2], &nodes[3]) {
(Node::Atom(s2), Node::Atom(s3)) => {
match (s2.parse::<u32>(), s3.parse::<u32>()) {
(Ok(exp_bits), Ok(sig_bits)) => Some((exp_bits, sig_bits)),
_ => None,
}
}
_ => None,
};
if let Some((exp_bits, sig_bits)) = exp_sig_bits {
Comment thread
Chris-Hawblitzel marked this conversation as resolved.
if args.len() <= 1 && signed {
Some(UnaryOp::FloatFromIeeeBits { exp_bits, sig_bits })
} else if args.len() > 1 {
let round = round(&mut args)?;
Some(UnaryOp::FloatFrom { exp_bits, sig_bits, signed, round })
} else {
None
}
} else {
None
}
}
Node::List(nodes)
if nodes.len() == 3
&& nodes[0] == Node::Atom("_".to_string())
&& (nodes[1] == Node::Atom("fp.to_ubv".to_string())
|| nodes[1] == Node::Atom("fp.to_sbv".to_string())) =>
{
let signed = nodes[1] == Node::Atom("fp.to_sbv".to_string());
let round = round(&mut args)?;
match &nodes[2] {
Node::Atom(s2) => match s2.parse::<u32>() {
Ok(bits) => Some(UnaryOp::FloatToBitVec { bits, signed, round }),
_ => None,
},
_ => None,
}
}
Node::Atom(s) if s == "fp.to_real" => Some(UnaryOp::FloatToReal),
Node::Atom(s) if s == "to_real" => Some(UnaryOp::ToReal),
Node::Atom(s) if s == "to_int" => Some(UnaryOp::RealToInt),
Node::List(nodes)
Expand Down Expand Up @@ -302,6 +406,15 @@ impl Parser {
Node::Atom(s) if s == "bvlshr" => Some(BinaryOp::LShr),
Node::Atom(s) if s == "bvshl" => Some(BinaryOp::Shl),
Node::Atom(s) if s == "concat" => Some(BinaryOp::BitConcat),
Node::Atom(s) if s == "fp.add" => Some(BinaryOp::FloatAdd(round(&mut args)?)),
Node::Atom(s) if s == "fp.sub" => Some(BinaryOp::FloatSub(round(&mut args)?)),
Node::Atom(s) if s == "fp.mul" => Some(BinaryOp::FloatMul(round(&mut args)?)),
Node::Atom(s) if s == "fp.div" => Some(BinaryOp::FloatDiv(round(&mut args)?)),
Node::Atom(s) if s == "fp.eq" => Some(BinaryOp::FloatEq),
Node::Atom(s) if s == "fp.lt" => Some(BinaryOp::FloatLt),
Node::Atom(s) if s == "fp.gt" => Some(BinaryOp::FloatGt),
Node::Atom(s) if s == "fp.leq" => Some(BinaryOp::FloatLe),
Node::Atom(s) if s == "fp.geq" => Some(BinaryOp::FloatGe),
Node::List(nodes)
if nodes.len() == 3
&& nodes[0] == Node::Atom("_".to_string())
Expand All @@ -326,6 +439,7 @@ impl Parser {
Node::Atom(s) if s == "-" => Some(MultiOp::Sub),
Node::Atom(s) if s == "*" => Some(MultiOp::Mul),
Node::Atom(s) if s == "distinct" => Some(MultiOp::Distinct),
Node::Atom(s) if s == "fp" => Some(MultiOp::Float),
_ => None,
};
let ite = match &nodes[0] {
Expand Down
Loading