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

Age	Commit message (Collapse)	Author
2013-11-25	Substantial Changes:	Tim King
	-ITE Simplification -- Moved the utilities in src/theory/ite_simplifier.{h,cpp} to ite_utilities. -- Separated simpWithCare from simpITE. -- Disabled ite simplification on repeat simplification by default. Currently, ite simplification cannot help unless we internally make new constant leaf ites equal to constants. -- simplifyWithCare() is now only run on QF_AUFBV by default. Speeds up nec benchmarks dramatically. -- Added a new compress ites pass that is only run on QF_LIA by default. This targets the perverse structure of ites generated during ite simplification on nec benchmarks. -- After ite simplification, if the ite simplifier was used many times and the NodeManager's node pool is large enough, this garbage collects: zombies from the NodeManager repeatedly, the ite simplification caches, and the theory rewrite caches. - TheoryEngine -- Added TheoryEngine::donePPSimpITE() which orchestrates a number of ite simplifications above. -- Switched UnconstrainedSimplifier to a pointer. - RemoveITEs -- Added a heuristic for checking whether or not a node contains term ites and if not, not bothering to invoke the rest of RemoveITE::run(). This safely changes the type of the cache used on misses of run. This cache can be cleared in the future. Currently disabled pending additional testing. - TypeChecker -- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls. - Theory Bool Rewriter -- Added additional simplifications for boolean ites. Minor Changes: - TheoryModel -- Removed vestigial copy of the ITESimplifier. - AttributeManager -- Fixed a garbage collection bug when deleting the node table caused the NodeManager to reclaimZombies() which caused memory corruption by deleting from the attributeManager. - TypeChecker -- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls. -NodeManager -- Added additional functions for reclaiming zombies. -- Exposed the size of the node pool for heuristics that worry about memory consumption. - NaryBuilder -- Added convenience classes for constructing associative and commutative n-ary operators. -- Added a pass that turns associative and commutative n-ary operators into binary operators. (Mostly for printing expressions for strict parsers.)
2013-11-21	Adding the changes needed to delete rewriter attributes. This includes ↵	Tim King
	being able to list attributes. Additionally, added debugging hooks to node manager and attribute manager.
2013-11-20	Changing the number of bits allocated per field in node values.	Tim King

2013-11-19	Bug fix for previous commit	Andrew Reynolds

2013-11-19	Add fair strategy for finite model finding multiple sorts --uf-ss-fair.	Andrew Reynolds

2013-11-14	Minor fixes for Mac OS Mavericks	Morgan Deters

2013-11-14	Allow empty record literals (fixing an oversight in previous work on empty ↵	Morgan Deters
	tuples/records)
2013-11-14	Some patches to CVC3 compatibility layer tests; Thanks to Adam Buchbinder @ ↵	Morgan Deters
	Google for the report and patch!
2013-11-14	Datatype::getCardinality() caching	Morgan Deters

2013-11-13	Add virtual destructors where missing	Morgan Deters

2013-11-13	Some patches to CVC3 compatibility layer; Thanks to Adam Buchbinder @ Google ↵	Morgan Deters
	for the report and patch!
2013-11-13	Another build fix; the dust should be settled now.	Morgan Deters

2013-11-12	Minor portfolio fixes for some platforms.	Morgan Deters

2013-11-12	Some additional explanation for a common configure error.	Morgan Deters

2013-11-12	lb change	Tianyi Liang

2013-11-12	add string progress measurements	Tianyi Liang

2013-11-12	Merge branch 'master' of github.com:tiliang/CVC4	Tianyi Liang

2013-11-12	add loop cache	Tianyi Liang

2013-11-12	add loop cache	Tianyi Liang

2013-11-12	Fix new-theory script for new, flattened build system.	Morgan Deters

2013-11-12	Minor build system cleanup	Morgan Deters

2013-11-11	length lemma is changed, var-split lemma is changed	Tianyi Liang

2013-11-11	Merge branch 'master' of https://github.com/CVC4/CVC4	Tianyi Liang

2013-11-11	Expanded usefulness of (set-info :cvc4-logic ...)	Morgan Deters

2013-11-11	Some fixes to build system with dependency-tracking is off; should fix ↵	Morgan Deters
	RPM/Debian builds.
2013-11-11	Change exit status to be more consistent with other command-line tools: 0 ↵	Morgan Deters
	success, nonzero error
2013-11-10	Fix compat-java library naming on Mac OS; thanks to Zheng Manchun for ↵	Morgan Deters
	reporting this issue
2013-11-10	Merge branch 'master' of https://github.com/CVC4/CVC4	Tianyi Liang

2013-11-10	Fix "make distclean", which should fix some of the build issues from last night	Morgan Deters

2013-11-10	Minor fixups to last commit	Morgan Deters

2013-11-10	Flatten libcvc4 build structure; remove some #include interdependences	Morgan Deters

2013-11-08	Fix "make distclean", which should fix some of the build issues from last night	Morgan Deters

2013-11-07	Minor fixups to last commit	Morgan Deters

2013-11-07	Flatten libcvc4 build structure; remove some #include interdependences	Morgan Deters

2013-11-07	Adds the header file into makefile, solving building error; adds cache for ↵	Tianyi Liang
	derivative; disables loop detection when finite model finding is enabled.
2013-11-07	Adds the header file into makefile, solving building error; adds cache for ↵	Tianyi Liang
	derivative; disables loop detection when finite model finding is enabled.
2013-11-06	bug fix	Tianyi Liang

2013-11-06	change options	Tianyi Liang

2013-11-06	Bug fixes for bounded integer quantification. Current best strategy is to ↵	Andrew Reynolds
	turn off MBQI. Disable relevant triggers by default.
2013-11-06	bug fix	Tianyi Liang

2013-11-06	Bug fixes for bounded integer quantification. Current best strategy is to ↵	Andrew Reynolds
	turn off MBQI. Disable relevant triggers by default.
2013-11-06	change options	Tianyi Liang

2013-11-06	Merge branch 'master' of github.com:tiliang/CVC4	Tianyi Liang

2013-11-06	add seperate regular expression files	Tianyi Liang

2013-11-06	add seperate regular expression files	Tianyi Liang

2013-11-05	fixed proof regression script and added a new uf test case	lianah

2013-11-04	Merge branch 'master' of https://github.com/CVC4/CVC4	lianah

2013-10-28	Turn off model-based arrays (causing crashes in portfolio)	Clark Barrett

2013-10-24	Fix for bug515	Clark Barrett

2013-10-23	add back eager approach	Tianyi Liang