Create a real interface for SMT solver

[illera88]

Right now Triton uses Z3 as SMT solver but does not provides a real interface so users can plug-in any desired SMT solver (CVC4, raSAT, OpenSMT,...), send the formulas to external servers to be solved and return the solution or (why not) solve them by hand :)

To do so solverEngine.cpp should be modified to make it a real interface that could be substituted by any way of formula solving that the user may want.

Cheers

[JonathanSalwan]

I made an interface called SolverInterface, this interface takes these methods as pure virtual :

TRITON_EXPORT virtual ~SolverInterface(){};
TRITON_EXPORT virtual std::map<triton::uint32, SolverModel> getModel(const triton::ast::SharedAbstractNode& node) const = 0;
TRITON_EXPORT virtual std::list<std::map<triton::uint32, SolverModel>> getModels(const triton::ast::SharedAbstractNode& node, triton::uint32 limit) const = 0;
TRITON_EXPORT virtual std::string getName(void) const = 0;

Now, our old SolverEngine class has been renamed to Z3Solver with an inheritance of SolverInterface:

class Z3Solver : public SolverInterface {
}

As we only provide one solver (z3), we initialize this solver into our API:

void API::initEngines(void) {
    ...
    this->solver = new(std::nothrow) triton::engines::solver::Z3Solver(this->symbolic);
    ...
}