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

Age	Commit message (Collapse)	Author
2011-09-30	interfaces fixes and cleanups...and examples of each interface!	Morgan Deters

2011-09-29	Some base infrastructure for user push/pop; a few bugfixes to user push/pop ↵	Morgan Deters
	and model gen also. I also expect this commit to fix bug #273. No performance change is expected on regressions with this commit, see http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
2011-09-24	Fix to building and linking for unit tests. (This should fix the ↵	Morgan Deters
	segfaulting units in optimized-dynamic. The problem was that the code incorrectly determined the address of one of the thread-scoped global variables, and I think it's because the same library was linked twice into the unit test in two different ways, confusing the runtime support code.)
2011-09-02	Merge from my post-smtcomp branch. Includes:	Morgan Deters
	Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated.
2011-04-25	Weekend work. The main points:	Morgan Deters
	* Type::getCardinality() returns the cardinality for for all types. Theories give a cardinality in the their kinds file. For cardinalities that depend on a type argument, a "cardinality computer" function is named in the kinds file, which takes a TypeNode and returns its cardinality. * There's a bitmap for the set of "active theories" in the TheoryEngine. Theories become "active" when a term that is owned by them, or whose type is owned by them, is pre-registered (run CVC4 with --verbose to see theory activation). Non-active theories don't get any calls for check() or propagate() or anything, and if we're running in single-theory mode, the shared term manager doesn't have to get involved. This is really important for get() performance (which can only skimp on walking the entire sub-DAG only if the theory doesn't require it AND the shared term manager doesn't require it). * TheoryEngine now does not call presolve(), registerTerm(), notifyRestart(), etc., on a Theory if that theory doesn't declare that property in its kinds file. To avoid coding errors, mktheorytraits greps the theory header and gives warnings if: + the theory appears to declare one of the functions (check, propagate, etc.) that isn't listed among its kinds file properties (but probably should be) + the theory appears NOT to declare one of the functions listed in its kinds file properties * some bounded token stream work
2010-10-31	enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some ↵	Morgan Deters
	documentation, and make it possible to "make doc" on a clean source tree (post-configure)
2010-10-27	make dist-building more pleasant (put .tar.gz in builds/ directory)	Morgan Deters

2010-09-30	fixed a number of problems with mac os x builds. build now works on mac os ↵	Morgan Deters
	x if you disable the clock_gettime check in configure.ac (resolves bug #202), but the parser is broken (new bug #208)
2010-09-13	link TAGS file into builds/ directory, when built. Resolves bug #195	Morgan Deters

2010-09-02	* add TimerStat statistic type	Morgan Deters
	* add Stats black-box unit test * new make target: "make units" now runs unit tests only * revised make target: "make regress" now runs regressions only * configure.ac: pull in librt for clock_gettime()
2010-09-01	"make check" now places binaries in the proper place before doing the ↵	Morgan Deters
	checks; this closes bug 46 finally, though the major annoyances related to this bug already had been fixed long ago
2010-04-08	A handful of build system fixes:	Morgan Deters
	* (test/unit/Makefile.am) libtool was being passed relative paths of sources in .cpp, confusing lcov if -b wasn't given. Fixed. Closes bug #102. * (configure.ac) --enable-coverage now implies --enable-static --enable-static-binary --disable-shared. * (configure.ac) Create top-level config.status for informational and re-configuration purposes. * (configure.ac) Remove -fvisibility=hidden for debug builds. Closes bug #104. * (test/unit/Makefile.am) Build unit tests with -Wall. * (various unit tests) Fixed trivially-fixable warnings in building unit tests. (Signedness in comparison, unused variables, etc.) * (Makefile.builds.in) Copy the binary correctly if it is static. (It was failing, but only with --enable-static --enable-shared --enable-static-binary.) Closes bug #103. * (src/parser/Makefile.am) libcvc4parser.so now links with libcvc4.so. * Other minor cleanups to the build system.
2010-03-08	This fixes regressions at levels >= 1 which were failing	Morgan Deters
	* implement zombification and garbage collection of NodeValues (but GC not turned on yet) * implement removal of key nodes from all attribute tables * audit NodeBuilder and fix memory leaks and improper reference-count management. This is in many places a re-write. Clearly documented invariants on NodeBuilder state. (Closes Bug 38) * created a "BackedNodeBuilder" that can be used to construct NodeBuilders with a stack-based backing store for a size that's not a compile-time constant. * NodeValues no longer depend on Node for toStream()'ing * make unit test-building "silent" with --enable-silent-rules * (Makefile.am, Makefile.builds.in) fix top-level build system so that "make regressN" works with unbuilt/out-of-date source trees in the expected way. * (various) code cleanup, documentation, formatting
2010-02-22	fix bug 33 (statically link the "cvc4" binary); also main driver cleanup	Morgan Deters

2010-02-03	Addressed many of the concerns of bug 10 (build system code review).	Morgan Deters
	Some parts split into other bugs: 19, 20, 21. Addressed concerns of bug 11 (util package code review). Slight parser source file modifications: file comments, #included headers in generated parsers/lexers Added CVC4::Result propagation back through MiniSat->PropEngine->SmtEngine->main(). Silenced MiniSat when verbosity is not requested.
2010-01-26	fixes to build structure, util classes, lots of fixes to Node and ↵	Morgan Deters
	NodeBuilder. outstanding SEGVs fixed
2009-12-17	coding standard fix on SmtEngine; fix recursive make	Morgan Deters

2009-12-08	work on propositional layer, expression builder support for large ↵	Morgan Deters
	expressions, output classes, and minisat
2009-12-05	more build system work	Morgan Deters