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

Age	Commit message (Collapse)	Author
2012-05-15	several bug fixes: in TheoryBV::NotifyClass missing NOT in predicate notify ↵	Liana Hadarean
	and now term notify handles boolean constants; fixed bug 328
2012-05-13	fixing build warnings	Dejan Jovanović

2012-05-09	* simplifying equality engine interface	Dejan Jovanović
	* notifications are now through the interface subclass instead of a template * notifications include constants being merged * changed contextNotifyObj::notify to contextNotifyObj::contextNotifyPop so it's more descriptive and doesn't clutter methods when subclassed * sat solver now has explicit methods to make true and false constants * 0-level literals are removed from explanations of propagations
2012-05-08	Merging in bvprop branch, with proper bit-vector propagation.	Liana Hadarean
	This should also fix bug 325.
2012-05-03	Some cleanup starting off from trying to understand the sharing code. ↵	Dejan Jovanović
	Changes include * fixed term visitor from the bvprop branch * removed all the warnings from builds -- warnings are there to be noted NOT to be used as scribbles * moved the LogicInfo into the theory constructor
2012-04-27	break dependence on zlib-dev for now	Morgan Deters

2012-04-11	merge from arrays-clark branch	Morgan Deters

2012-04-04	some settings in bvminisat	Dejan Jovanović

2012-04-04	changed BVMinisat options to use cc_min=0 in propagate only calls and ↵	Liana Hadarean
	cc_min=2 in solve
2012-04-04	changed ccmin_mode in BvMinisat	Liana Hadarean

2012-04-04	* added propagation as lemmas to TheoryBV:	Liana Hadarean
	* modified BVMinisat to work incrementally * added more bv regressions
2012-03-29	Fixes a linking problem with the new SatSolverConstructor on Mac.	Tim King

2012-03-28	Some renaming and refactoring in SAT	Dejan Jovanović

2012-03-26	Global registry of SAT solvers, where they are registered at compile time. ↵	Dejan Jovanović
	The available SAT solvers can be seen with the --show-sat-solvers option.
2012-03-26	More cleaning up.	Dejan Jovanović

2012-03-26	more datail from the build failure	Dejan Jovanović

2012-03-25	moving minisat implementation into their respective directories (regular and bv)	Dejan Jovanović

2012-03-22	Merged updated version of the bitvector theory:	Liana Hadarean
	* added simplification rewrites
2012-02-29	This should fix the debian build fails:	Liana Hadarean
	* removed bvpicosat directory as it is currently not used Cleared some of the flurry of warnings my previous merge caused in src/prop/
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