| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2011-10-28 | proof regressions | Morgan Deters | |
| 2011-10-28 | merged the proofgen3 branch into trunk: | Liana Hadarean | |
| - can now output LFSC checkable resolution proofs - added configuration option --enable-proof - added command line argument --proof To turn proofs on build with proofs enabled and run with --proof. | |||
| 2011-10-21 | add gcc version information to Configuration, and warn when building with ↵ | Morgan Deters | |
| v4.5.1 which has a buggy optimizer (resolves bug #266) | |||
| 2011-10-19 | fix configure step on Ubuntu oneiric (11.10)-- related to bug #284 | Morgan Deters | |
| 2011-10-03 | user push/pop support in minisat and simplification; also bindings work | Morgan Deters | |
| 2011-09-30 | interfaces fixes and cleanups...and examples of each interface! | Morgan Deters | |
| 2011-09-28 | better fix for #281, also fix issue with command line options not existing ↵ | Morgan Deters | |
| on older g++en, like Apple's 4.2 on Snow Leopard. | |||
| 2011-09-25 | first crack at compatibility java interface (not built by default) | Morgan Deters | |
| 2011-09-21 | Java binding now working. Some interface types still need some work (e.g. ↵ | Morgan Deters | |
| iterators aren't functional). Also, output isn't very flexible yet, as I told SWIG to ignore all the operator<<'s. | |||
| 2011-09-21 | considerable bindings interface work, some improvements to build | Morgan Deters | |
| 2011-09-18 | cleaned up the mechanism for library versioning | Morgan Deters | |
| 2011-09-16 | fix debian build without breaking anything (i hope) | Morgan Deters | |
| 2011-09-03 | this should fix the build; doxygen documentation now gets built in ↵ | Morgan Deters | |
| srcdir/doc/doxygen | |||
| 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-07-07 | cudd-building prefs with --with-cudd / --without-cudd | Morgan Deters | |
| 2011-06-18 | Some fixes inspired by Fedora 15: | Morgan Deters | |
| * compilation fixes for GCC 4.6.x + ptrdiff_t is now in std:: * fix some make rules that are ok in Make 3.81 but broke in Make 3.82 * look for cxxtestgen.py as well as cxxtestgen.pl, and look for cxxtest headers in /usr/include | |||
| 2011-05-02 | more minor fixes related to last few commits | Morgan Deters | |
| 2011-05-01 | minor fixes, plus experimental readline support in InteractiveShell | Morgan Deters | |
| 2011-04-10 | merge from replay branch | Morgan Deters | |
| 2011-04-10 | Add -lprofiler when --with-google-perftools is offered; also fix some ↵ | Morgan Deters | |
| newswire-raised documentation issues. | |||
| 2011-04-02 | with --with-google-perftools, don't just take it on blind faith, require a ↵ | Morgan Deters | |
| successful link at configure time | |||
| 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). | |||
| 2011-03-15 | Merge from cudd branch. This mostly just adds support for linking | Morgan Deters | |
| against cudd libraries, the propositional_query class (in util/), which uses cudd if it's available (and otherwise answers UNKNOWN for all queries), and the arith theory support for it (currently disabled per Tim's request, so he can clean it up). Other changes include: * contrib/debug-keys - script to print all used keys under Debug(), Trace() * test/regress/run_regression - minor fix (don't export a variable) * configure.ac - replace a comment removed by dejan's google perf commit * some minor copyright/documentation updates, and minor changes to source text to make 'clang --analyze' happy. | |||
| 2011-03-14 | adding support for google performance tools to the build sytem, it can be ↵ | Dejan Jovanović | |
| enabled at configure with --with-google-perftools to use it on ubuntu, you need to install packages google-perftools and libgoogle-perftools0 to run the profiling of the heap, you can run it for example with HEAPPROFILE=/tmp/profile ./builds/bin/cvc4 test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.smt this will create some files /tmp/profile* that you can then to get the pdf of the profile you can then run google-pprof --pdf ./builds/bin/cvc4 /tmp/profile.0001.heap > profile.pdf or for other options check http://goog-perftools.sourceforge.net/doc/ | |||
| 2010-12-17 | tls.h, rational.h, and integer.h are only re-generated if changed. this ↵ | Morgan Deters | |
| obviates the need for a full rebuild just because you re-./configured. | |||
| 2010-11-18 | small changes to documentation; also, '\''make doc'\'' doesn't build dot ↵ | Morgan Deters | |
| graphs (but nightly build system will produce them) | |||
| 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-29 | portability updates to build system | Morgan Deters | |
| 2010-10-28 | fix confusing CXXTEST configure message, indicating success at finding ↵ | Morgan Deters | |
| cxxtest when it wasn't found. | |||
| 2010-10-12 | Merge from cc-memout branch. Here are the main points | Morgan Deters | |
| * Add ContextMemoryAllocator<T> allocator type, conforming to STL allocator requirements. * Extend the CDList<> template to take an allocator (defaults to std::allocator<T>). * Add a specialized version of the CDList<> template (in src/context/cdlist_context_memory.h) that allocates a list in segments, in context memory. * Add "forward" headers -- cdlist_forward.h, cdmap_forward.h, and cdset_forward.h. Use these in public headers, and other places where you don't need the full header (just the forward-declaration). These types justify their own header (instead of just forward-declaring yourself), because they are complex templated types, with default template parameters, specializations, etc. * theory_engine.h no longer depends on individual theory headers. (Instead it forward-declares Theory implementations.) This is especially important now that theory .cpp files depend on TheoryEngine (to implement Theory::getValue()). Previously, any modification to any theory header file required *all* theories, and the engine, to be completely rebuilt. * Support memory cleanup for nontrivial CONSTANT kinds. This resolves an issue with arithmetic where memory leaked for each distinct Rational or Integer that was wrapped in a Node. | |||
| 2010-10-10 | additional model gen and SMT-LIBv2 compliance work: (get-assignment) now ↵ | Morgan Deters | |
| supported; work on Result type (biggest noticeable change is that CVC4 now outputs lowercase "sat" and "unsat"), Options class moved to src/smt, to allow for future work on runtime configuration via (set-option) command | |||
| 2010-10-07 | type checking for define-fun in production builds; related to (and might ↵ | Morgan Deters | |
| resolve) bug 212 | |||
| 2010-10-01 | re-add no-deprecated to C sources; update some file-level documentation; ↵ | Morgan Deters | |
| first look at cdvector for code review | |||
| 2010-10-01 | replacement implementation for clock_gettime() on mac os x, build ↵ | Morgan Deters | |
| portability (resolving mac os x issues), code cleanup, fix compiler warnings | |||
| 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-27 | add workaround for systems (i.e., Mac OS X) that don't support __thread; ↵ | ACSYS | |
| also configure script auto-detection of __thread support and syntax | |||
| 2010-09-24 | roll back an unintended change with r900 | Morgan Deters | |
| 2010-09-24 | Fix build system for Mac OS X builds (resolves bug #203) | 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-08-24 | Making GMP default, CLN opt-in with --with-cln | Christopher L. Conway | |
| 2010-08-17 | Merge from "cc" branch: | Morgan Deters | |
| CongruenceClosure implementation; CongruenceClosure white-box test. New UF theory implementation based on new CC module. This one supports predicates. The two UF implementations exist in parallel (they can be selected at runtime via the new command line option "--uf"). Added type infrastructure for TUPLE. Fixes to unit tests that failed in 16-August-2010 regressions. Needed to instantiate TheoryEngine with an Options structure, and explicitly call ->shutdown() on it before destruction (like the SMTEngine does). Fixed test makefiles to (1) perform all tests even in the presence of failures, (2) give proper summaries of subdirectory tests (e.g. regress0/uf and regress0/precedence) Other minor changes. | |||
| 2010-08-16 | add zlib checks to configure (new minisat requires it?) | Morgan Deters | |
| 2010-07-07 | some build system changes reverted after the CLN build system work a few ↵ | Morgan Deters | |
| days ago, these are now fixed: competition configurations build with -O9 (as they used to); they are static-binary by default and shared libs are not built; also the default autoconf compiler flags "-g -O2" is removed from builds | |||
| 2010-07-04 | better detection for static binary building | Morgan Deters | |
| 2010-07-04 | make dist && make distcheck functional, other fixes | Morgan Deters | |
| 2010-07-03 | better config.reconfig script auto-generated | Morgan Deters | |
| 2010-07-03 | With this commit come a number of changes to build system to support | Morgan Deters | |
| building with CLN or with GMP, the contrib/switch-config script (enabling "fast switching" of different configurations in the same builds/ directory), and also some minor changes. ./configure --with-gmp (or --without-cln) forces building with GMP and doesn't even look for CLN. Configure fails if GMP isn't installed. ./configure --with-cln (or --without-gmp) forces building with CLN and doesn't even look for GMP. Configure fails if CLN isn't installed. ./configure [no arguments] will detect what's installed. CLN is default, if it isn't installed, or is too old, GMP is looked for (and configure fails if neither is available). It is an error to specify --with-gmp --with-cln (or --without-* for both) at the same time. Building with CLN (whether forced or detected) adds a note to the configure output mentioning the fact that the build of CVC4 will be linked against a GPLed library and notifying the user of the --without-cln option. Building with GMP (whether forced or detected) affects the build directory, so CLN and GMP builds are kept separate. ./configure --with-cln debug builds in builds/$arch/debug ./configure --with-gmp debug builds in builds/$arch/debug-gmp The final binaries are linked explicitly against either gmp or cln, but not both. If linked against cln, cln pulls in gmp as a dependency, so the result will be linked against both. === Details that you probably don't care about === The headers src/util/{integer,rational}.h are generated from the corresponding .in versions. A user installing a CVC4-devel package will get the headers for rational and integer that match the library that s/he installs. The preprocessor #defines CVC4_GMP_IMP and CVC4_CLN_IMP are added to cvc4autoconfig.h. Only one is ever #defined. cvc4autoconfig.h doesn't need to be #included directly; you get it through #including cvc4_private.h (or the parser version). AM_CONDITIONALs are also defined so that Makefiles get the cln/gmp configuration. AC_SUBSTs are defined so that public headers (see src/util/{integer,rational}.h.in) can use the setting. *Public* headers that need to depend on the cln/gmp configuration can't use cvc4autoconfig.h, because we're keeping that in the private, internal-only space, never to be installed on users' machines. Here, something special is required, like the configure-level generation of headers that I used for src/util/{integer,rational}.h.in. Tim's Integer and Rational wrappers are the only bits of code that should care which library is used (and also src/util/configuration.h, which gives the user of the library information about how CVC4 is built), and possibly some unit tests (?). | |||
| 2010-07-02 | Merges the cln-test branch into the main branch. | Tim King | |
| The current commit allows for switching in between GMP and CLN by changing a flag manually in configure.ac. A configure time flag has not yet been added for deciding between the two. To get this to work you will need to install cln in some form (for Ubuntu users the packages are libcln6(lucid)/libcln5 on karmic and libcln-dev). You will also need to install pkg-config. You will need to rerun ./autogen.sh, and reconfigure. | |||
| 2010-06-18 | "statistics" and "staticbinary" are now tags on the build (so you get build ↵ | Morgan Deters | |
| directories like builds/x86_64-unknown-linux-gnu/debug-staticbinary-nostatistics .. etc. This is useful to distinguish static binary builds and statistics builds from each other when you configure multiple times in the same source directory | |||
| 2010-06-18 | Merging the statistics branch into the main trunk. I'll go over how to use ↵ | Tim King | |
| this Tuesday during the meeting. You'll need to run autogen and receonfigure after updating. | |||
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
path: root/configure.ac
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback