General CVC Support with Basic String Equality

[GroundPound]

I've added CVC as an alternative solver to Z3 and included a basic symbolic string. The default is still Z3, but CVC can be used with the --cvc flag.

Running with CVC passes all but 6 test cases. Unlike the Z3 implementation, the CVC implementation doesn't encode all numbers as bit vectors and so CVC fails to generate a model for formulas that have nonlinear relationships on an infinite domain. I still wanted to encode some basic bit vector operations so CVCInteger converts back and forth between bit vectors just for bitwise operations. Since the built-in CVC bit vector conversion only generates positive numbers, I limited the domain of bit vectors causing a couple of test cases to fail, sacrificing more completeness in order to prevent the generation of inputs that do not behave as expected. The GCD test case finishes correctly but can take up to 15 minutes and uses a lot of memory. I suspect it has to do with the repeated conversion between bit vectors and integers. I hope this isn't too much of a problem "in the real world" as I believe bitwise operations in Python are rare in general.

I also added a symbolic string. For now the only supported operation is equality, but I plan to add more in the near future. In order to support more than one variable type in a formula (previously it was either integers or bit vectors) I had to re-architecture Expression such that the expression generation code was outside of the expression class hierarchy. As far as I can tell this was necessary as I needed the AST traversal to case out on the subclasses of expression and a superclass cannot reference its own subclasses (circular reference).

Current issues:

• The CVC expression code doesn't mirror the Z3 expression code due to the Expression re-architecture. I'm happy to refactor the Z3 code to this end if you'd like.
• There is currently no Z3 representation for strings. I'm interested in adding support but not sure what the most time-efficient approach is to doing so.
• There is quite a bit of duplicate code between z3_wrap.py, cvc_wrap.py, exprbuilder.py, and the expression.py classes. I think the AST traversal code can be shared as the main difference is the concrete classes that are instantiated. I'm happy to do this if you'd like.
• Expression currently serves as a strange hybrid between a base-class and a CVCBoolean. That functionality should probably be separated out.

[thomasjball]

This is great! Please feel free to refactor the code.

[thomasjball]

Peter, can you please refactor the code so that CVC4 is not required. I get the following message:

from .cvc_wrap import CVCWrapper

import CVC4 ImportError: No module named 'CVC4' Since Z3 is the default, CVC4 should not be required. Best, -- Tom

[GroundPound]

Of course! I apologize for that oversight. I'll make the import conditional. I'll try to get a pull request in later today.