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

Age	Commit message (Collapse)	Author
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
2011-04-05	Minor adjustments to the Registrar commit in 1644, documentation.	Morgan Deters

2011-04-04	Merging the satliteral-before-prereg branch into trunk. Theory ↵	Tim King
	preregistration is now called during the conversion to cnf. This fixes bug 257.