search

ApproxSymate / klee

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

[WIP] Real arithmetc domain solving for solving constraints with error #70

Closed domainexpert closed 1 month ago

domainexpert commented 6 years ago

This is not ready to be merged. This implementation is to compute input values, given path condition (with error), using Z3 real number domain solver.

As a note, the next thing to do would be to implement a new Z3 interface for this. Current Z3ErrorSolver::computeOptimalValue() is for computing optimal value (bounds), whereas Z3ErrorSolve::computeInitialValue() is limited to bitvector values only (we only need real number result instead).

domainexpert commented 6 years ago

@Himeshi This PR is not ready to be merged; atm I'm using it to leave TODO items.