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

Age	Commit message (Collapse)	Author
2012-04-12	Adds an operator<< to SExpr::SexprTypes. This fixes bug 317. In debug ↵	Tim King
	builds, an Unhandled(SExpr::SexprTypes) could not compile on debian.
2012-04-11	merge from arrays-clark branch	Morgan Deters

2012-04-06	* Smt2 printer for datatypes	François Bobot
	* Fix DefineFunctionCommand when a constant is defined
2012-04-06	* Fix ITEs and functions in CVC language printer.	Morgan Deters
	* Permit "BOOL = BOOL" in CVC language parser (auto-replaced with IFF internally, except in strict mode). * SExpr atoms now can be string-, integer-, or rational-valued. * SmtEngine::setInfo(":status", ...) now properly dumps a SetBenchmarkStatusCommand rather than a SetInfoCommand. * Some dumping fixes (resolves bug 313)
2012-04-06	processing assertions in bit-vectors even when in fullcheck (needed for sharing)	Dejan Jovanović

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-04-03	Fix for make dist.	Tim King

2012-04-02	- Merged in the branch cdlist-cleanup.	Tim King
	- This adds a CleanUp template argument to CDList. - CDChunkList<T> replaces the CDList specialization for ContextMemoryAllocator. - CDVector<T> has been simplified and improved. - The expected performance impact is negligible.
2012-04-02	fix for cvc4_logic dump	Kshitij Bansal

2012-03-29	Fix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is false, function ↵	Tim King
	pointers cannot be directly used with the CVC4_THREADLOCAL macro. This is why there were problems on macs.
2012-03-29	Fixes a linking problem with the new SatSolverConstructor on Mac.	Tim King

2012-03-29	bringing cryptominisat into the main branch	Dejan Jovanović

2012-03-28	enabling the --disable-arithmetic-propagation option in the arithmetic code ↵	Dejan Jovanović
	(it wasn't used)
2012-03-28	fix swig-ignored interface name; hopefully fixes Debian package nightly builds	Morgan Deters

2012-03-28	Update to the ArithRewriter to remove REWRITE_AGAIN_FULL and limit ↵	Tim King
	REWRITE_AGAIN calls.
2012-03-28	Some renaming and refactoring in SAT	Dejan Jovanović

2012-03-28	getting rid of a rewrite in uf sharing, speeds things up a bit	Dejan Jovanović

2012-03-28	fixed faulty bv rewrite rule	Liana Hadarean

2012-03-28	adding an extra cache check in the rewriter, speeds things a bit	Dejan Jovanović
	http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3828&category=&p=5&reference_id=3820
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-26	with a small fix	Dejan Jovanović

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

2012-03-25	sat_module.h,cpp -> sat_solver.h,cpp (as intended)	Dejan Jovanović

2012-03-25	sat.h,cpp -> theory_proxy.h,cpp (this is what it defines)	Dejan Jovanović

2012-03-23	Removed the variableRemovalEnabled option and d_removedRows from ↵	Tim King
	TheoryArith. This had been disabled for several months.
2012-03-22	* improving arithmetic getEqualityStatus	Dejan Jovanović
	* some sharing improvements based on model
2012-03-22	Merged updated version of the bitvector theory:	Liana Hadarean
	* added simplification rewrites
2012-03-22	some improvements to the sharing mechanism/interface	Dejan Jovanović

2012-03-21	Disable nonclausal simplification for QF_SAT benchmarks by default.	Morgan Deters
	(Can be overridden with --simplification=batch, for example.)
2012-03-09	Some work on the dump infrastructure to support portfolio work.	Morgan Deters
	Dump("foo") << FooCommand(...); now "dumps" the textual representation of the command (in the current output language) to a file, IF dumping is on at configure-time, AND the "muzzle" feature is off, AND the "foo" flag is turned on for the dump stream during this run. If it's a portfolio build, the above will also store the command in a CommandSequence, IF the "foo" flag is turned on for the dump stream during this run. This is done even if the muzzle is on. This commit also cleans up some code that used the dump feature (in arrays, particularly).
2012-03-09	fix a "lost command" bug and associated memory leak in SMT-LIBv1 parser due ↵	Morgan Deters
	to an out-of-place parenthesis
2012-03-09	Strengthen minisat assertion regarding t-propagations that was ↵	Morgan Deters
	unintentionally allowing a theory to propagate p and ~p at the same time (and the conflict was undetected, leading to an incorrect answer). Credit to Clark for finding this.
2012-03-08	fix "make dist"	Morgan Deters

2012-03-08	Fixin the bug Clark found. In final check, enqueued propagations were not ↵	Dejan Jovanović
	discharged.
2012-03-08	Removing QUICK_CHECK, and other unused ones, from the Theory::Effort.	Dejan Jovanović
	Seems to be working better <http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3749&category=&p=5&reference_id=3739>, and should fix the failing cases in the regressions. Removing one test case from the integer regress0.
2012-03-07	cdqueue : fix size(). Thank you Clark for spotting this silly mistake.	François Bobot

2012-03-07	fix some Java compatibility-layer interface problems; also fix some Mac OS X ↵	Morgan Deters
	build issues
2012-03-06	updating the equality engine to be able to give explanations for terms that ↵	Dejan Jovanović
	were not in the databas (queried by areEqual and areDisequal) and it's a bit better http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3738&category=&p=-1&reference_id=3731
2012-03-02	Remove some commented out code from sat.h	Kshitij Bansal

2012-03-02	This commit merges in the changes from branches/arithmetic/refactor0	Tim King
	- Improved the checks in AssertLower and AssertUpper so that redundant bounds cause less work. - Because of the above change, d_constantIntegerVariables now cannot have duplicate elements enqueued. This allows removing d_varsInDioSolver. - Fix to an assertion in CDQueue. - Implements a CDArithVarSet using a vector of booleans and CDList. - Refactored ArithVar out of arith_utilities.h. Miscellaneous cleanup of arithmetic.
2012-03-02	CDMap -> CDHashMap	Dejan Jovanović
	CDSet -> CDHashSet
2012-03-02	committing the TNode/Node fix that was in the kind-backend branch; there's ↵	Morgan Deters
	still something fishy here, I think I need to merge in a few more things to support incrementality properly. But this fixes "make check" for now
2012-03-02	Renamed CDQueue to CDTrailQueue and CDQueue2 to CDQueue. Small changes to ↵	Tim King
	function names and documentation.
2012-03-01	Partial merge from kind-backend branch, including Minisat and CNF work to	Morgan Deters
	support incrementality. Some clean-up work will likely follow, but the CNF/Minisat stuff should be left pretty much untouched. Expected performance change negligible; slightly better on memory: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5 Note that there are crashes, but that these are exhibited in the nightly regression run too!
2012-03-01	cdqueue2 : cdlist that can be used like queue and can delete element that ↵	François Bobot
	will never be restored