summaryrefslogtreecommitdiff
path: root/configure.ac
AgeCommit message (Collapse)Author
2013-05-08Cutting release 1.2.1.2Morgan Deters
2013-04-29Some fixes for GCC 4.2, and for Java on MacMorgan Deters
2013-04-29Fixes to FCSimplex for some versions of compilersMorgan Deters
2013-04-26FCSimplex branch mergeTim King
2013-04-23Theory "alternates" supportMorgan Deters
* This is a feature that Dejan and I want for the upcoming tutorial. It allows rapid prototyping of new decision procedure implementations (which we may choose to demonstrate), and a new --use-theory command-line option to select from different available implementations. It has no affect on the current set of theories, as no "alternates" are defined. * Also update the new-theory script, which was broken and incomplete.
2013-04-03Prerelease versioning for master.Morgan Deters
2013-04-03Pre-release versioningMorgan Deters
2013-04-03Cutting release 1.1.1.1Morgan Deters
2013-04-01Merging some cleanup work:Morgan Deters
* Comment cleanup * Spelling fixes * Fix warnings * Documentation updates * References in docs to cryptominisat removed * Unneeded scope resolutions removed * Old, unused regression removed
2013-03-26Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javacMorgan Deters
2013-03-19Remove PropositionalQuery class and all CUDD-related build stuff (and ↵Morgan Deters
references)
2013-01-28some fixes for win32, including ability to "make check" win32 builds via wineMorgan Deters
2013-01-24Add win32 support (merge from mdeters/win32, with some cleanup).Morgan Deters
2012-12-18Fix bug 483: readline checks must come after Boost checks in configureMorgan Deters
2012-12-03version numberingMorgan Deters
2012-12-01Cutting release 1.0.1.0Morgan Deters
2012-11-29Fix for hidden symbols in library on Mac. It's a strange issue to do withMorgan Deters
explicit template instantiation rules, -fvisibility=hidden, and the way that Apple distributes libstdc++. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-27fix for some Mac buildsMorgan Deters
2012-11-27give warning at configure-time about unsupported language bindings, and ↵Morgan Deters
don't advertise them in help listing for --enable-language-bindings
2012-11-12* Fix language bindings: various issuesMorgan Deters
** remove a number of warnings in bindings generation ** give appropriate names for operator-overloading ** make sure Java language bindings are built with -fno-strict-aliasing, to ensure the optimizer doesn't produce bad code * Also remove BitVector::equals(), which wasn't used and was inconsistently implemented (operator==() is still there). (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-05fixes for mac osMorgan Deters
2012-10-25last build system fix for now: fix some typos affecting MacACSYS
2012-10-25extra quoting for special characterMorgan Deters
2012-10-25more minor fixes to build systemACSYS
2012-10-25One of my changes to the build system yesterday broke the nightly build because:Morgan Deters
1. The source tree was configured. 2. The builds directory was removed. 3. The source tree was re-configured. Which led to a nasty dangling symlink that caused (3) to abort. Fixed.
2012-10-24Includes many fixes to build system for Solaris (thanks Tim!), and alsoMorgan Deters
just in general, and some documentation adjustments.
2012-10-06* Some documentation about building compatibility and language bindingsMorgan Deters
* Better errors/warnings when SWIG isn't installed (resolves bug 373) * Allow compatibility bindings to be built when SWIG isn't available
2012-09-29draft RELEASE-NOTES file, and minor release stuffMorgan Deters
2012-09-28Public 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-25fixMorgan Deters
2012-09-25fix some Mac issuesMorgan Deters
2012-09-21SMT-LIBv2 compliance updates:Morgan Deters
* chainability of =, <, <=, >, >= via the new CHAINABLE kind and TheoryBuiltin rewriter support (resolves bug #383) * with --smtlib2, force interactive mode off by default Also: * fix a few bugs causing crashes * better "alias" processing for options * configure-time fixes to readline detection (this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-14Fix a few minor issues in options processing, improving usability, ↵Morgan Deters
consistency, error-reporting, and documentation.
2012-09-04Accepted some patches from the Multicore Programming Group at Imperial ↵Morgan Deters
College London (via Peter Collingbourne): cvc4-0001-Look-for-cxxtestgen-as-well-as-cxxtestgen.pl-and-cxx.patch * better checking for cxxtest cvc4-0002-Do-not-read-an-additional-command-after-failure.patch * more correct failure behavior for interactive tools cvc4-0003-Only-exit-when-encountering-a-CommandFailure.patch * don't consider "unsupported" as a failure (accepted with modifications) cvc4-0004-Produce-SMT-LIB-v2-conformant-output-for-get-info.patch * better get-info responses (accepted with modifications) These patches will help the group build Boogie support for CVC4. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-08-28fix regression tests for automake 1.11 and automake 1.12---both versions ↵Morgan Deters
should work now
2012-08-28fixes for Mac and automake 1.12 detectionMorgan Deters
2012-08-06Support setting :regular-output-channel and :diagnostic-output-channel.Morgan Deters
Also some cleanup of option-related exceptions infrastructure.
2012-07-31Options 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-16reverse the order of link arguments to -lcln -lgmp, fixes linking errors for ↵Morgan Deters
static-binary CLN-enabled builds on greed
2012-07-08remove a debugging line from configure script that was left in inadvertentlyMorgan Deters
2012-07-01Some changes to configure.ac:Morgan Deters
1. Includes BOOST_CPPFLAGS during compilation of all files, not just portfolio-relevant files. This is necessary since we now have a general dependence on Boost (not just its threading stuff). This resolves bug 357. 2. Support --disable-thread-support and --enable-thread-support, in an effort to get to the bottom of bug 361. These changes shouldn't affect performance, though #1 will build the cvc4 libs with a couple of pthread definitions that conceivably could change the behavior of #included standard headers. Let's keep an eye on tonight's regressions.
2012-06-06Fixing numerous issues with tests and "make dist":Morgan Deters
* test/regress/regress0/unconstrained wasn't being distributed. This caused the debian build failure last night. (It still doesn't run on "make check", but had to be distributed properly.) * Fixing an issue where a test name was longer than 99 characters and couldn't be distributed in the "old" tar format. (Told automake to use a newer tar format.)
2012-04-28require boost library (but not the threading support---that's only necessary ↵Morgan Deters
for portfolio)
2012-04-11merge from arrays-clark branchMorgan Deters
2012-04-06fix distributed builds (and therefore the Debian nightly build) by ignoring ↵Morgan Deters
Makefile.am files under src/prop/cryptominisat.
2012-03-30some more build system fixesDejan Jovanović
2012-03-09Some work on the dump infrastructure to support portfolio work.Morgan Deters
Dump("foo") << FooCommand(...); now "dumps" the textual representation of the command (in the current output language) to a file, IF dumping is on at configure-time, AND the "muzzle" feature is off, AND the "foo" flag is turned on for the dump stream during this run. If it's a portfolio build, the above will also store the command in a CommandSequence, IF the "foo" flag is turned on for the dump stream during this run. This is done even if the muzzle is on. This commit also cleans up some code that used the dump feature (in arrays, particularly).
2012-03-03Changing the dependency checking; GMP is required (and sometimes must be ↵Morgan Deters
explicitly linked in with -l) when using CLN. Fixes a bug on recent Debian that Francois reported. Hopefully this doesn't break anything..
2012-02-23pcvc4 only built if --with-portfolio given to the configure script ↵Morgan Deters
(Clark-requested change)
2012-02-22fixes to configure and boost.m4 to make certain boost installations nonfatal ↵Morgan Deters
errors; threading support should only be required to build pcvc4, not cvc4
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback