Age | Commit message (Collapse) | Author |
|
|
|
|
|
This commit replaces all uses of assert with Assert from base/check.h to ensure that all assertions get checked in production builds with enabled assertions.
|
|
This avoids conflicts when CVC4 is linked to an application that
also uses plain Minisat.
|
|
* separated SatSolverInput interface class into two classes:
- TheoryProxy for the sat solver to communicate with the theories
- SatSolverInterface abstract class to communicate with the sat solver
* instead of using #ifdef typedef for SatClauses and SatLiterals, now there are CVC4 SatLiteral/SatClause types and mappings between them and the internal sat solver clause/literal representation
* added abstract classes for DPLLSatSolver and BVSatSolver different interfaces
Replaced TheoryBV with bitblasting implementation:
* all operators bitblasted
* only operator elimination rewrite rules so far
|
|
|
|
|
|
|
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback