C++ library for solving systems of linear constraints: inequalities equality and disequality. Current version is based on Fourier-Motzkin (FM) elimination for inequalities and Gaussian elimination for equality. Quantifiers “Forall” and “Exists” are allowed. Boolean connectivities '&' -and, '|' - or '~' - not. '' '>=' '=' - arithmetical inequalities. The simplest formula for the solver might be:
Exists x (x > 0 & x < 3);The solver simplifies such formula to 'true'. The solver simplifies system of equalities using LU decomposition. For example:
x + y = 3 &
x - y = 1 ;Gives:
x = 2 & y = 1Appliances:
Such solver may be applied as arithmetic online solver for software/hardware static verification tools. Solution of the linear programming problem. But since the FM algorithm is more general solver is not such efficient as a simplex method solver.
Note. By now the code base is incomplete. It contains all Calculator's code and only small part of the Solver code. Rest of the code is coming. Stay tuned :)
If you have questions feel free to contact me vitaly.german
Copyright © 2013 Black Duck Software, Inc. and its contributors, Some Rights Reserved. Unless otherwise marked, this work is licensed under a Creative Commons Attribution 3.0 Unported License . Ohloh ® and the Ohloh logo are trademarks of Black Duck Software, Inc. in the United States and/or other jurisdictions. All other trademarks are the property of their respective holders.