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

Age	Commit message (Collapse)	Author
2014-11-12	BV inequality graph TNode fix.	Morgan Deters

2014-11-12	Fix BV inequality solver caching.	Morgan Deters

2014-11-07	Remove some unused variables.	Morgan Deters

2014-11-07	Fix memory issues in bitvector theory, which is now valgrind-clean (mostly ↵	Morgan Deters
	resolves bug #594).
2014-10-29	Added new, much faster, care graph computation for arrays	Clark Barrett
	Force split on true first in combineTheories Fix bugs in getModelValue in bit-vectors
2014-10-23	Fixed inefficiency in bit-vector rewrite rule.	lianah

2014-10-14	fix for memory leak in BVQuickCheck	lianah

2014-09-27	Merge branch '1.4.x'	Morgan Deters

2014-09-27	Fix infinite loop in --bitblast-aig/--bv-aig-simp options.	Morgan Deters

2014-09-26	Merge branch '1.4.x'	Morgan Deters

2014-09-26	Fix bv options doc.	Morgan Deters

2014-09-26	Fix AIG bitblaster for unsat cores.	Morgan Deters

2014-09-03	check() optimization	Kshitij Bansal
	Details of testing here: http://church.cims.nyu.edu/wiki/User:Kshitij/theorycheckoptimization
2014-08-28	fixing bug580 caused by bad bv inequality explanation	lianah

2014-08-28	fixing bug580 caused by bad bv inequality explanation	lianah

2014-08-22	Unsat core infrastruture and API (SMT-LIB compliance to come).	Morgan Deters

2014-08-18	Making getEqualityStatus more powerful for bit-vector theory.	lianah

2014-08-05	fixed bug575 for bv models	lianah

2014-08-05	fixed bug575 for bv models	lianah

2014-07-10	Merge remote-tracking branch 'origin/master' into segfaultfix	Kshitij Bansal

2014-07-04	initialize variables	Kshitij Bansal

2014-07-01	Update copyrights.	Morgan Deters

2014-06-22	Merge pull request #39 from mdeters/bv-warnings	lianah
	Fix compiler warnings in BV-related code (unused vars mostly).
2014-06-22	Merge pull request #35 from mdeters/bv-kinds	lianah
	Bit-vector kinds documentation
2014-06-21	Fix compiler warnings in BV-related code (unused vars mostly).	Morgan Deters

2014-06-21	fixed build failure	lianah

2014-06-20	Bit-vector kinds documentation	Morgan Deters

2014-06-19	added model generation to eager bit-blasting and turned abc off by default	lianah

2014-06-19	Fix compile errors with some versions of GCC.	Morgan Deters

2014-06-19	Minor fixes, spelling etc.	Morgan Deters

2014-06-15	core solver fix	lianah

2014-06-15	fixed bv bug due to applying equisatisfiable transformations in ppRewrite	lianah

2014-06-15	fixed fuzzer assertion failures for bv	lianah

2014-06-14	added rewriting to bv-pow2 pass	lianah

2014-06-14	Evil bitvector preprocessing pass for simplifying powers of two.	lianah

2014-06-14	bv static learning and rewrites for power of 2 terms	lianah

2014-06-14	more bv rewrites	lianah

2014-06-14	fix to inequality rewrite	lianah

2014-06-14	added bv inequality rewrite	lianah

2014-06-14	added bv inequality lemmas	Liana Hadarean

2014-06-12	Merge branch 'master' of https://github.com/CVC4/CVC4	lianah

2014-06-12	fixing bv inequality solver explanation bug	lianah

2014-06-12	added bvcomp case to bv to bool lifting	lianah

2014-06-11	added optionException for trying to use abc in an non-abc build	lianah

2014-06-11	switched bv equality order	lianah

2014-06-11	fixed unit tests failures	lianah

2014-06-11	fixing bv ackermanization cache bug	lianah

2014-06-10	Merging CAV14 paper bit-vector work.	lianah

2014-04-29	Mostly resolves bug #561 memory leaks, and more.	Morgan Deters

2014-04-17	simplify mkSkolem naming system: don't use $$	Kshitij Bansal
	Short summary: By default NODEID is appeneded, just continue doing what you were, just don't add the _$$ at the end. Long summary: Before this commit there were four (yes!) ways to specify the names for new skolems, which result in names as given below 1) mkSkolem("name", ..., SKOLEM_FLAG_DEFAULT) -> "name_NODEID" 2) mkSkolem("name", ..., SKOLEM_EXACT_NAME) -> "name" 3) mkSkolem("name_$$", ..., SKOLEM_FLAG_DEFAULT) -> "name_NODEID" 4) mkSkolem("na_$$_me", ..., SKOLEM_FLAG_DEFAULT) -> "na_NODEID_me" After this commit, only 1) and 2) stay. 90% usage is of 1) or 3), which results in exact same behavior (and looking at the source code it doesn't look like everyone realized that the _$$ is just redundant). Almost no one used 4), which is the only reason to even have $$. Post this commit if you really want a number in the middle, manually construct the name and use the SKOLEM_EXACT_NAME flag.