cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2021-03-11	Use CVC4_ASSERTIONS instead of NDEBUG. (#6099)	Mathias Preiner
	Ensures that all checks are performed in production builds with enabled assertions.
2018-09-13	Fix #include for minisat headers in bvminisat. (#2463)	Mathias Preiner

2015-10-26	This fixes a one definition rule violation for reduceDB_lt in Solver.cc in ↵	Tim King
	minisat and bvminisat. This also moves BVMinisat into CVC4. This also wrapped code in cpp files into the namespaces instead of having using namespace *.
2012-02-25	Refactored CnfStream to work with the bv theory Bitblaster:	Liana Hadarean
	* 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