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

Age	Commit message (Collapse)	Author
2018-03-21	Refactor mkoptions (#1631)	Mathias Preiner
	This commit refactors code generation for options. It uses a new configuration format for defining options (*.toml) and a new Python script mkoptions.py to generate the source code and option documentation. The option behavior did not change for most of the options, except that for bool --enable-/--disable- long options enable/disable was removed. E.g. --enable-miplib-trick and --disable-miplib-trick got changed to --miplib-trick and --no-miplib-trick. This commit fixes also an issues with set-option/get-option via the SMT2 interface. Before long options were only accessible if the name included the =ARG part.
2017-08-25	Move LFSC checker out of the CVC repository. (#222)	Aina Niemetz
	LFSC now lives outside of the CVC4 repository and is not part of the CVC4 distribution anymore. As a consequence, we + Add --with-lfsc and --with-lfsc-directory as configure options. In the case where CVC4 has not been built with integrated LFSC, all code that interacts with LFSC is disabled. + Disable proof checking if CVC4_USE_LFSC is not defined. Configuring the build with --check-proofs but without --with-lfsc results in an error. + Do not call LFSC's cleanup function (but we should in the future). LFSC checker segfaults during cleanup on regression testcase regress0/bv/core/bitvec7.smt. Disabled call to lfscc_cleanup until the problem in lfscc is fixed. + Disable building with LFSC for the distcheck travis build since it is not part of the distribution anymore. Further, make distcheck with LFSC would require to call contrib/get-lfsc-checker before calling make check on the temp build (the build of the unpacked distribution tar ball).
2017-03-28	More work on sygus. Add regress4 to Makefile.	ajreynol

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-16	First attempt at incorporating LFSC proof checker into CVC4.	Morgan Deters

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

2012-12-03	distribute the find_public_interface.sh script	Morgan Deters

2012-11-09	another DISTCLEANFILES entry, for proper "make distclean" behavior (fixes ↵	Morgan Deters
	"distclean" target error last night)
2012-11-08	fix "make distcheck"	Morgan Deters

2012-11-07	* Type ascription bug fixed (resolves bug 432), but there are others I ↵	Morgan Deters
	discovered (still outstanding). :-( * Fix a documentation-building problem when building from tarballs (fixes distcheck build failure last night) * Provide expected output for arith regression 'mod.01.smt2' * Also, fix a compiler warning in inst_gen.cpp (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-05	fix for tarball building (fixes debian and distcheck problems in nightly builds)	Morgan Deters

2012-10-23	some fixes for "make examples" and "make install-examples" when invoked from ↵	Morgan Deters
	tarballs (non-subversion-checkouts); should fix "INSTALL" failure we saw in last night's build email
2012-09-29	draft RELEASE-NOTES file, and minor release stuff	Morgan Deters

2012-09-29	fixes to "make distclean" and C compatibility bindings; should fix the ↵	Morgan Deters
	broken builds last night
2012-09-28	Public interface review items:	Morgan Deters
	* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument() * Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only * CheckArgument() throws non-AssertionException * things outside the core library (parsers, driver) use regular C-style assert, or a public exception type. * auto-generated documentation for Smt options and internal options Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
2012-09-14	Fix a few minor issues in options processing, improving usability, ↵	Morgan Deters
	consistency, error-reporting, and documentation.
2012-08-01	fixes to some *clean targets	Morgan Deters

2012-07-31	Options merge. This commit:	Morgan Deters
	1. changes the way options are declared (see http://church.cims.nyu.edu/wiki/Options) 2. moves module-specific options enumerations (SimplificationMode, DecisionMode, ArithUnateLemmaMode, etc.) to their own header files, also they are no longer inside the Options:: class namespace. 3. includes many SMT-LIBv2 compliance fixes, especially to (set-option..) and (get-option..) The biggest syntactical changes (outside of adding new options) you'll notice are in accessing and setting options: * to access an option, write (e.g.) options::unconstrainedSimp() instead of Options::current()->unconstrainedSimp. * to determine if an option value was set by the user, check (e.g.) options::unconstrainedSimp.wasSetByUser(). * ensure that you have the option available (you have to #include the right module's options.h file, e.g. #include "theory/uf/options.h" for UF options) * this point is important. If you access an option and it tells you the option doesn't exist, you aren't #including the appropriate options.h header file * Note that if you want an option to be directly set (i.e., other than via command-line parsing or SmtEngine::setOption()), you need to mark the option :read-write in its options file (otherwise it's read-only), and you then write (e.g.) options::unconstrainedSimp.set(true). Adding new options is incredibly simple for primitive types (int, unsigned, bool, string, double). For option settings that you need to turn into a member of an enumerated type, you write a custom "handler" for the option---this is no additional work than it was before, and there are many examples to copy from (a good one is stringToSimplificationMode() in src/smt/options_handlers.h). Benefits of the new options system include: 1. changes to options declarations don't require a full-source rebuild (you only have to rebuild those sources that depend on the set of options that changed). 2. lots of sanity checks (that the same option isn't declared twice, that option values are in range for their type, that all options are documented properly, etc.) 3. consistency: Boolean-valued option --foo gets a --no-foo automatically, documentation is generated consistently, the option-parsing matches the documented option name, etc. 4. setting options programmatically via SmtEngine::setOption() is enabled, and behaves the same as command-line equivalents (including checking the value is in range, etc.) 5. the notion of options being "set by the user" is now primitive; you can use (e.g.) options::unconstrainedSimp.wasSetByUser() instead of having to use (and maintain) a separate Boolean option for the purpose I've taken lots of care not to break anything. Hopefully, I've succeeded in that.
2012-07-16	now passes "make distcheck", which does important checks for the release ↵	Morgan Deters
	(e.g., "make dist" produces a distribution that passes "make dist" and "make check", "make uninstall" actually uninstalls, "make distclean" actually cleans, ...)
2012-07-09	minor fix-ups	Morgan Deters

2011-10-31	fixes to "make distclean" and "make maintainerclean"	Morgan Deters

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-18	cleaned up the mechanism for library versioning	Morgan Deters

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-03-25	This is a merge from the "theoryfixes+cdattrhash" branch. The changes	Morgan Deters
	are somewhat disparate but belonged on the same branch because they were held back from trunk all for the same reason (to keep the trunk stable for furious bitvector development). Dejan has now given me the go-ahead for a merge. ========================================= THIS COMMIT CHANGES THE THEORY INTERFACE! ========================================= Theory constructors are expected to take an additional "Valuation" parameter that each Theory should send along to the base class constructor. The base class Theory keeps the Valuation in a d_valuation field for use by it and by its derived classes. Theory::getValue() no longer takes a Valuation* (it is expected to use d_valuation instead). This allows other theory functions to take advantage of getValue() for debugging or heuristic purposes. TODO BEFORE MERGE TO TRUNK: ***implement BitIterator find() in CDAttrHash<bool>. Specifically: Added QF_BV support for SMT-LIB v2. * Two adjustments to the theory interface as requested by Tim King: 1. As described above. 2. Theories now have const access to the fact queue through base class functions facts_begin() and facts_end(); useful for debugging. * Added an "Asserted" attribute so that theories can check if something has been asserted or not (and therefore not propagate it). However, this has been disabled for now, pending more data on the overhead of it, and pending discussion at the 3/25/2011 meeting. * Do not define NDEBUG in MiniSat in assertion-enabled builds (so that MiniSat asserts are evaluated). * As a result of the new MiniSat assertions, some --incremental regressions had to be disabled; also, some bitvectors ?!! * Bug 71 is resolved by adding a specialization for CDAttrHash<> in the attribute package. * Fixes for some warnings flagged by clang. * System tests have arrived! So far mainly infrastructure for having system tests, but there is a system test aimed at improving code coverage of the printer package. * Minor other adjustments to documentation and coding to be more conformant to CVC4 policy. Tests have been performed to demonstrate that these changes have no or negligible effect on performance. In particular, changing the CDAttrHash<> doesn't have any real effect on performance or memory right now, since there is only one context-dependent boolean flag (as soon as another is added, the effect is noticeable but probably still slight).
2010-11-15	fix some things with the build system (make dist, make install, make check)	Morgan Deters

2010-10-27	"make dist" fixes; a distribution tarball can now build and pass tests. ↵	Morgan Deters
	"make distcheck" fails only because one of the "clean" targets needs work in test/unit
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-07-04	make dist && make distcheck functional, other fixes	Morgan Deters

2010-06-15	fix last commit gcc options (-wunknown-pragmas ==> -Wno-unknown-pragmas)	Morgan Deters

2010-06-15	remove warnings about unknown #pragma GCC diagnostic on older compilers	Morgan Deters

2010-04-14	* Better dependency tracking for unit test building and linking, and	Morgan Deters
	auto-generated headers (metakind.h etc.), so they don't have to be recompiled every time. This drastically improves build time when only small updates are made. * Added "memory.h" unit test header for checking out-of-memory conditions. cdlist_black uses it. * Added helpful output when you "make lcov" in a non-coverage-enabled build. * Removed strict aliasing warning when compiling metakind.h header with optimization on. * Removed const version of NodeBuilder::operator Node()---it was poorly performing, better to not permit it---and fixed the convenience builders to use the non-const version (re: code review #63) * Color-coded test output on capable terminals. * Fixed some warnings in unit tests.
2010-04-09	minor fixes to lcov build target, better contextobj testing	Morgan Deters

2010-04-09	added experimental "make lcov" target (it runs only unit tests); better ↵	Morgan Deters
	coverage for util and context classes; implemented some output functionality that was missing; reclassified some tests white -> black or black -> public; other minor fixes
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-18	Rm'ing doc from SUBDIRS	Christopher L. Conway

2010-02-18	Adding doxygen configuration parameters and doxygen-doc Makefile target	Christopher L. Conway

2010-02-05	remove the last vestiges of support for "make build-profile" without first ↵	Morgan Deters
	configuring the build-profile, simplifying the build process and closing bug 21
2010-02-04	build system for multi-level regressions	Morgan Deters

2009-12-17	coding standard fix on SmtEngine; fix recursive make	Morgan Deters

2009-12-17	support nonstandard, unconfigured builds (e.g., "./configure debug" followed ↵	Morgan Deters
	by "make production ASSERTIONS=1")
2009-12-05	more build system work	Morgan Deters

2009-11-25	additional work on parser hookup, configuration + build	Morgan Deters

2009-11-20	fixes to build/test system	Morgan Deters

2009-11-19	testing framework, configure fixes, incorporations from meeting, continued work	Morgan Deters

2009-11-17	fixes/redesign of source layout from meeting	Morgan Deters

2009-11-12	parser, minisat, other things..	Morgan Deters

2009-11-09	minor fixes, added contrib directory	Morgan Deters