c++ linear formula simplifying library

Question

What is the best (in terms of simplicity of use and performance) C++/C++11 library which can simplify formulas like the following?

(a < 0 && b > 0) || (a < 0 && c > 0) || (a < 0 && c > 1) 

to (e.g.)

a < 0 && (b > 0 || c > 0)

I think it is very important to explain one thing (because I see this question is misunderstood).

I do not want to simplify C / C++ expressions - I know, the compiler can make it.

I'm making a graph processing tool. On the edges of the graph, there are some conditions about its vertices (lets say the vertices are a, b, c and these conditions are like a<b, b>0 etc - Please note, that these conditions are not expressed as "strings", they can be any function or library call). During processing, I'm collecting the expressions together and before further graph processing I want to simplify them.

The conditions and expressions will be created during runtime.

I want to be able to input some expressions to that library, like:

[...]
a = new Variable();
b = new Variable();
expr1 = lib.addExpr(a,0, lib.LESS);
expr2 = lib.addExpr(b,0, lib.MORE);
expr3 = lib.addExpr(expr1, expr2, lib.AND);
[...]
cout << lib.solve(exprn).getConditionsOf(a);

Of course this library will probably have a lot more beautiful API. I have written it as method calls only to show what I expect to be the underlying mechanism - to emphasize, that I do not need a source to source compiler or that this question is not related to source compilation optimization.

Answer 1

You are looking for a symbolic math library for C++ that can handle boolean logic.

Here are some to get started with:

• SymbolicC++: powerful, general purpose symbolic math library for C++, but not particularly intended for boolean mathematics.
• BoolStuff: not a general-purpose symbolic math library, very focused on boolean logic, but does probably exactly what you want.
• Logic Friday: standalone digital circuit analysis tool and boolean logic simplifier, with C API.

Answer 2

If you first generate the truth table (fairly trivial), this reduces to the circuit minimization problem, which is well-studied.