search

ApproxSymate / klee

KLEE Symbolic Virtual Machine for Numerical Precision Analysis
Other
0 stars 0 forks source link

Implement better expression to represent errors #8

Closed domainexpert closed 7 years ago

domainexpert commented 7 years ago

@Himeshi We need an expression system of real numbers to represent the error amount. The problem with KLEE's standard Expr system is that it is confusing to read. Making it nicer to read is the same amount of work as implementing a new real number-based expression system altogether.

domainexpert commented 7 years ago

We need a Z3ErrorBuilder to convert KLEE Expr representing error expression to Z3 real number constraints. Such constraints are not only to be solved, but presumably also easier to read than KLEE Expr.

domainexpert commented 7 years ago

Resolved via #20 .