Refactored inclusion of files and added namespaces

[Tomaqa]

Tests and the parallel component are not included yet. I also reformatted some files that I considered meaningful. I struggled a bit with the parser. It compiles but I am pretty sure that a better solution exists... It still uses a deprecated option of Bison and I could not figure out how to get rid of it.

[Tomaqa]

I included also the parallel module ..

[Tomaqa]

The thing is that minisat is still somewhat a third-party library. However, its datatypes are so heavily used across the whole project that it might seem that it is a bit painful and repetitive to use the additional namespace. But how is it different from std:: or e.g. boost::, if we used other libraries? It is a question whether we treat minisat like an adopted, inherent code, or not. Currently, minisat is tightly integrated into OpenSMT (way too much IMHO), making it very difficult to replace it by other SAT solver, which may be necessary in the future. I guess that in most cases, these datatypes are used because they were believed to be more efficient than std containers (which may or may not be true nowadays), not because explicitly minisat datatypes were needed.

If the main purpose is using efficient containers, then we should use type aliases that can be easily replaced, such as using Map = minisat::Map<...> or using Map = std::unordered_map<...>.

For me personally, as a person still not that familiar with the codebase, the fact that some datatypes or especially functions are related to minisat was quite useful, because in some places their usage is counter-intuitive.

What do you think?

[blishko]

The thing is that minisat is still somewhat a third-party library. However, its datatypes are so heavily used across the whole project that it might seem that it is a bit painful and repetitive to use the additional namespace. But how is it different from std:: or e.g. boost::, if we used other libraries? It is a question whether we treat minisat like an adopted, inherent code, or not. Currently, minisat is tightly integrated into OpenSMT (way too much IMHO), making it very difficult to replace it by other SAT solver, which may be necessary in the future. I guess that in most cases, these datatypes are used because they were believed to be more efficient than std containers (which may or may not be true nowadays), not because explicitly minisat datatypes were needed.

If the main purpose is using efficient containers, then we should use type aliases that can be easily replaced, such as using Map = minisat::Map<...> or using Map = std::unordered_map<...>.

For me personally, as a person still not that familiar with the codebase, the fact that some datatypes or especially functions are related to minisat was quite useful, because in some places their usage is counter-intuitive.

What do you think?

In case of OpenSMT, minisat is no longer a third-party library, but it was the base on which OpenSMT has been built. As such, its containers were used instead of std:: equivalents. The problem with drop-in replacements is that Map does not have the same interface as std::(unordered_)map. We could in principle try to replace them with std equivalents.

My main concern is that it makes our code more noisy then I would like and the API's feels more clunky where user's have to manipulate opensmt::minisat::vec instead of opensmt::vec (or equivalently without opensmt prefix).

Overall, I have long since considered these data structures as OpenSMT's data structures, rather than minisat's that we just happen to use.

[Tomaqa]

OK, so what about using a type alias? Because it is a bit counter-intuitive that <minisat/mtl/..> is being used most of times, even at places that does not have to do anything with sat-solving. What about using sth. similar to <common/Number.h>, for example <common/Containers.h>?

[blishko]

OK, so what about using a type alias? Because it is a bit counter-intuitive that <minisat/mtl/..> is being used most of times, even at places that does not have to do anything with sat-solving. What about using sth. similar to <common/Number.h>, for example <common/Containers.h>?

That sounds reasonable to me. As I said, mtl was basically used in OpenSMT as a replacement of stl. We can try to phase it out gradually.

[Tomaqa]

We decided to gradually integrate the minisat modules right into OpenSMT (and possibly also to get rid of some of the structures) -> #743.