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

Age	Commit message (Collapse)	Author
2013-03-14	fix to build system: #include the proper file when they are in both builds ↵	Morgan Deters
	and src
2012-03-25	moving minisat implementation into their respective directories (regular and bv)	Dejan Jovanović

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