Shaobo

[WIP] Add Floating-Point Support

2

This is a working-in-process PR that adds floating-point support to pysmt (#285 ) Questions: 1. The syntax of creating a floating-point constant node. I propose something like FP(BV(...), eb, sb),...

Add real to int conversions

8

Specifically, three operations are added, RealToInt -- The SMT `to_int` function Ceiling -- Equivalent to the Racket `ceiling` function Truncate -- Equivalent to the Racket `truncate` function

Premature optimizations on real division

5

Division by 0 will lead to exception via this block: https://github.com/pysmt/pysmt/blob/3b8169a785e5e6e39059630bbbcd049851743ca5/pysmt/formula.py#L264-L267 It also blocks reasonable optimization like this: https://github.com/pysmt/pysmt/blob/3b8169a785e5e6e39059630bbbcd049851743ca5/pysmt/simplifier.py#L978-L982 This is because division with a constant real divisor is rewritten...

Rust edition 2021 is stable after version 1.56.0. It seems a lot of projects are migrating to this version. We need to catch up with them as well. Version 1.56.0...

Generalize `clang-options` into `compiler-options`

1

We should be able to feed rustc options via this flag.

Added a pass that warns about loops

2

It also prints a loop bound if it can be determined via LLVM's ScalarEvolution class. Specifically, it's equal to the `ConstantMaxBackedgeTakenCount`. Partially addressed #760

It seems this pass could produce much simpler LLVM IRs.

Some Rust `Box` operation is internally supported by rustc

1

Consider this program, ```Rust // An example from `The Little MLer` chapter 3 #[macro_use] extern crate smack; use smack::*; //#[derive(Debug)] enum Pizza { Crust, Cheese(Box), Onion(Box), Anchovy(Box), Sausage(Box), } fn...

## Motivation Currently, we only have one bookkeeping variable `$Alloc` for the entire program. We can split it into multiple bookkeep variables such that one variable roughly corresponds to one...