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

Age	Commit message (Collapse)	Author
2016-05-24	Merged cryptominisat from experimental branch.	Liana Hadarean

2015-12-14	Refactoring Options Handler & Library Cycle Breaking	Tim King
	What to Know As a User: A number of files have moved. Users that include files in the public API in more refined ways than using #include <cvc4.h> should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems. The Problem: The build order of CVC4 used to be [roughly] specified as: options < expr < util < libcvc4 < parsers < main Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable. The Solution: To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen: 1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file. 2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options. 3. All of the old options_handlers.h files have been refactored. 4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary. 5. I am removing the libstatistics library. The constraints that the CVC4 build system will eventually satisfy are: - The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from /kinds files and /options files. - The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases. - The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.) - One library per Makefile.am. - No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.) The build order of CVC4 can now be [roughly] specified as base < options < util < expr < smt_util < libcvc4 < parsers < main The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean. More details about the directories: base/ The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere. options/ The options/ directory is self contained. - It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h . - There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options. - Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done. - The */options_handlers.h files have been removed. - The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp. - All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h . util/ The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean. expr/ The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/. - An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h. - Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h. - The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/. - Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes. - Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources. - This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC. smt_util/ The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel. What is up next: - A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed. - The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up.
2015-10-26	This commit fixes a bug related to a public header depending on a compiler ↵	Tim King
	flag. This resulted in user code seeing a different size for the SmtEngine class than what was compiled in the library. Proofs are enabled by default again. See http://cvc4.cs.nyu.edu/bugs/show_bug.cgi?id=688 for more information.
2015-10-24	Revert "Default builds are now proof enabled."	Kshitij Bansal
	This reverts commit 4fd18dee3156a6dd1903b95662034d6e996ff88b.
2015-10-23	Changes configure.ac so that the single recurisve invocation runs with a ↵	Tim King
	relative path. This lets the @srcdir@ variable in configuration be a relative path.
2015-10-11	Default builds are now proof enabled.	Liana Hadarean

2015-10-09	Temporary reverting commit 477e72b (proofs as default build) until we fix ↵	Liana Hadarean
	nightly builds.
2015-10-07	Default builds are now proof enabled.	Liana Hadarean

2015-02-12	Changing CXXFLAGS for custom cln installation in configure.ac.	Tim King
	Making sure the CVC4 flags do not get overwritten after being set.
2015-01-19	Adding an additional search path to configure.ac for cxxtestgen to reflect ↵	Tim King
	the cxxtest git repository.
2014-08-12	To avoid confusion, permit --enable-staticbinary as an alias for ↵	Morgan Deters
	--enable-static-binary.
2014-07-13	Versioning for master.	Morgan Deters

2014-07-13	New versioning for development version.	Morgan Deters

2014-07-13	Cutting release 1.4.1.4	Morgan Deters

2014-06-26	Minor language bindings fixes.	Morgan Deters

2014-06-25	Stack-size portfolio fix. If using Boost 1.50, --thread-stack=MB is now ↵	Morgan Deters
	supported.
2014-06-21	Adjust library dependencies to be more correct (fixes lintian warnings).	Morgan Deters

2014-06-19	Fix for mac readline.	Morgan Deters

2014-06-19	Fix for pre-C++11 is_sorted().	Morgan Deters

2014-06-19	No more dependence on libstdc++ or PBDS stuff: remove build stuff that ↵	Morgan Deters
	supported it.
2014-06-19	get-glpk-cut-log script, and configure code.	Morgan Deters

2014-06-11	Some clean-up, post bv-merge.	Morgan Deters
	Add abc to build id and fix static building. Add abc to --show-config output and Configuration class API. Add ability to select abc source path. Fix arch_flags for abc.
2014-06-10	Merging CAV14 paper bit-vector work.	lianah

2014-05-30	Fix personal.mk for some make targets.	Morgan Deters

2014-01-08	Merge branch '1.3.x'	Morgan Deters
	Conflicts: COPYING NEWS config/cvc4.m4
2014-01-08	Switch license default back to BSD, and add --best and --enable-gpl options.	Morgan Deters

2013-12-23	Proof-checking code; fixups of segfaults and missing functionality in proof ↵	Morgan Deters
	generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but not --check-proofs, since LFSC code uses globals) * proofs are not yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line
2013-12-18	Merge branch '1.3.x'	Morgan Deters
	[skip ci]
2013-12-18	Fix an autoconf issue with CLN in some configurations; also clarification ↵	Morgan Deters
	re: license issues [skip ci]
2013-12-18	Merge branch '1.3.x'	Morgan Deters

2013-12-18	Fix configure handling for CLN (should fix win32 nightly builds)	Morgan Deters

2013-12-18	Reduce autoconf version for dependence (should fix 32-bit builds).	Morgan Deters

2013-12-17	Merge branch '1.3.x'	Morgan Deters

2013-12-17	configure --with-portfolio disables CLN.	Morgan Deters

2013-12-17	Merge branch '1.3.x'	Morgan Deters
	Conflicts: COPYING NEWS
2013-12-17	some config changes: new --bsd option, readline gives warning, default build ↵	Morgan Deters
	is now production.
2013-12-16	First attempt at incorporating LFSC proof checker into CVC4.	Morgan Deters

2013-12-10	GLPK build identifier, license warnings.	Morgan Deters

2013-12-09	GLPK build identifier, license warnings.	Morgan Deters

2013-12-06	Initializing master for next version.	Morgan Deters

2013-12-06	Initializing 1.3.x branch.	Morgan Deters

2013-12-06	Cutting release 1.3.1.3	Morgan Deters

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

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

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

2013-09-18	Support a personal build configuration and make rules.	Morgan Deters

2013-07-29	Fix numerous compiler warnings on various platforms	Morgan Deters

2013-07-23	fix for win32 option parsing via mingw32	Morgan Deters

2013-05-08	Prerelease versioning for master	Morgan Deters

2013-05-08	Prerelease versioning for 1.2.x	Morgan Deters