summaryrefslogtreecommitdiff
path: root/configure.ac
AgeCommit message (Collapse)Author
2011-05-02more minor fixes related to last few commitsMorgan Deters
2011-05-01minor fixes, plus experimental readline support in InteractiveShellMorgan Deters
2011-04-10merge from replay branchMorgan Deters
2011-04-10Add -lprofiler when --with-google-perftools is offered; also fix some ↵Morgan Deters
newswire-raised documentation issues.
2011-04-02with --with-google-perftools, don't just take it on blind faith, require a ↵Morgan Deters
successful link at configure time
2011-03-25This is a merge from the "theoryfixes+cdattrhash" branch. The changesMorgan 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-15Merge from cudd branch. This mostly just adds support for linkingMorgan 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-14adding 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-17tls.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-18small changes to documentation; also, '\''make doc'\'' doesn't build dot ↵Morgan Deters
graphs (but nightly build system will produce them)
2010-10-31enable 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-29portability updates to build systemMorgan Deters
2010-10-28fix confusing CXXTEST configure message, indicating success at finding ↵Morgan Deters
cxxtest when it wasn't found.
2010-10-12Merge from cc-memout branch. Here are the main pointsMorgan 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-10additional 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-07type checking for define-fun in production builds; related to (and might ↵Morgan Deters
resolve) bug 212
2010-10-01re-add no-deprecated to C sources; update some file-level documentation; ↵Morgan Deters
first look at cdvector for code review
2010-10-01replacement implementation for clock_gettime() on mac os x, build ↵Morgan Deters
portability (resolving mac os x issues), code cleanup, fix compiler warnings
2010-09-30fixed 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-27add 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-24roll back an unintended change with r900Morgan Deters
2010-09-24Fix build system for Mac OS X builds (resolves bug #203)Morgan Deters
2010-09-02* add TimerStat statistic typeMorgan 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-24Making GMP default, CLN opt-in with --with-clnChristopher L. Conway
2010-08-17Merge 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-16add zlib checks to configure (new minisat requires it?)Morgan Deters
2010-07-07some 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-04better detection for static binary buildingMorgan Deters
2010-07-04make dist && make distcheck functional, other fixesMorgan Deters
2010-07-03better config.reconfig script auto-generatedMorgan Deters
2010-07-03With this commit come a number of changes to build system to supportMorgan 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-02Merges 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-18Merging 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.
2010-05-27Use the newer automake test driver "parallel-tests". This driver:Morgan Deters
* keeps test logs around * provides parallel testing functionality (with make -jN). I've also added new functionality in test/Makefile.am which deletes old test logs, ensures that ALL tests are tried (even if units fail), and provides a color-coded summary at the end of the test run, which shows how many units, regressions (per level), and system tests failed (or passed), and provides a link to the log file for further information. Resolves bug 117.
2010-05-27fix bug 120; competition mode regression failures for intentionally-buggy inputMorgan Deters
2010-05-04Disabling semantic checks in competition mode.Christopher L. Conway
Adding function debugTagIsOn to safely test for tracing in any compilation mode. Removing irrelevant command-line options from usage message in muzzled mode.
2010-04-14* Better dependency tracking for unit test building and linking, andMorgan 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-08A 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-04-04* Addressed issues brought up in Chris's review of Morgan'sMorgan Deters
NodeManager (bug #65). Better documentation, etc. * As part of this, removed NodeManager::mkVar() (which created a variable of unknown type). This requires changes to lots of unit tests, which were using this function. * Performed some review of parser code (my code review #73). + I changed the way exceptions were caught and rethrown in src/parser/input.cpp. + ParserExceptions weren't being properly constructed (d_line and d_column weren't intiialized and could contain junk, leading to weird error messages). Fixed. * Fix to the current working directory used by run_regression script. Makes exceptional output easier to match against (in expected error output). * (configure.ac) Ensure that CFLAGS has -fexceptions in it, in case we compile any C code and don't use the C++ compiler.
2010-04-04* Node::isAtomic() now looks at an "atomic" attribute of argumentsMorgan Deters
instead of assuming it's atomic based on kind. Atomicity is determined at node building time. Fixes bug #81. If this is determined to make node building too slow, we can allocate another attribute "AtomicHasBeenComputed" to lazily compute atomicity. * TheoryImpl<> has gone away. Theory implementations now derive from Theory directly and share a single RegisteredAttr attribute for term registration (which shouldn't overlap: every term is "owned" by exactly one Theory). Fixes bug #79. * Additional atomicity tests in ExprBlack unit test. * More appropriate whitebox testing for attribute ID assignment (AttributeWhite unit test). * Better (and more correct) assertion checking in NodeBuilderBlack. * run-regression script now checks exit status against what's provided in "% EXIT: " gesture in .cvc input files, and stderr against "% EXPECT-ERROR: ". These can be used to support intended failures. Fixes bug #84. Also add "% EXIT: " gestures to all .cvc regressions in repository. * Solved some "control reaches end of non-void function" warnings in src/parser/bounded_token_buffer.cpp by replacing "AlwaysAssert(false)" with "Unreachable()" (which is known statically to never return normally). * Regression tests now use the cvc4 binary under builds/$(CURRENT_BUILD)/src/main instead of the one in bin/ which may not be properly installed yet at that point of the build. (Partially fixes bug #46.) * -fvisibility=hidden is now included by configure.ac instead of each Makefile.am, which will make it easier to support platforms (e.g. cygwin) that do things a different way. * TheoryUF code formatting. (re: my code review bug #64) * CDMap<> is leaking memory again, pending a fix for bug #85 in the context subsystem. (To avoid serious errors, can't free context objects.) * add ContextWhite unit test for bug #85 (though it's currently "defanged," awaiting the bugfix) * Minor documentation, other cleanup.
2010-04-01PARSER STUFF:Morgan Deters
* Other minor changes to the new parser to match coding guidelines, add documentation, .... * Add CFLAGS stuff to configure.ac parser Makefile.ams. This ensures that profiling, coverage, optimization, debugging, and warning level options will apply to the new parser as well (which is in C, not C++). This fixes the deprecated warning we were seeing this evening. * Now, if you have ANTLR_HOME set in your environment, you don't need to specify --with-antlr-dir to ./configure or have libantlr3c installed in standard places. --with-antlr-dir still overrides $ANTLR_HOME, and if the installation in $ANTLR_HOME is missing or doesn't work, the standard places are still tried. * Extend "silent make" to new parser stuff. * Added src/parser/bounded_token_buffer.{h,cpp} to the list of exclusions in contrib/update-copyright.pl and mention them as excluded from CVC4 copyright in COPYING. They are antlr3-derived works, covered under a BSD license. OTHER STUFF: * expr_manager.h, expr.h, expr_manager.cpp, and expr.cpp are now auto-generated by a "mkexpr" script. This provides the correct instantiations of mkConst() for public use, e.g., by the parser. * Fix doxygen documentation in expr, expr_manager.. closes bug #35 * Node::isAtomic() implemented in a better way, based on theory kinds files. Fixes bug #40. To support this, a "nonatomic_operator" command has been added. All other "parameterized" or "operator" kinds are atomic. * Added expr_black test * Remove kind::TRUE and kind::FALSE and make a new CONST_BOOLEAN kind that takes a "bool" payload; for example, to make "true" you now do nodeManager->mkConst(true). * Make new "cvc4_public.h" and "cvc4parser_public.h" headers. Private headers should include "cvc4_private.h" (resp. "cvc4parser_private.h"), which existed previously. Public headers should include the others. **No one** should include the autoheader #include (which has been renamed "cvc4autoconfig.h") directly, and public CVC4 headers can't access its #defines. This is to avoid us having the same distribution problem as libantlr3c. * Preliminary fixes based on Tim's code review of attributes (bug #61). This includes splitting hairy template internals into attribute_internals.h, for which another code review ticket will be opened. Bug is still outstanding, but pending further refactoring/documentation. * Some *HashFcns renamed to *HashStrategy to match refactoring done elsewhere (done by Chris?) earlier this week. * Simplified creation of make rules for generated files (expr.cpp, expr.h, expr_manager.cpp, expr_manager.h, theoryof_table.h, kind.h, metakind.h). * CVC4::Configuration interface and implementation split (so private stuff doesn't leak into public headers). * Some documentation/code formatting fixes. * Add required versions of autotools to autogen.sh. * src/expr/mkmetakind: fix a nonportable thing in invocation of "expr" that was causing warnings on Red Hat. * src/context/cdmap.h: add workaround to what appears to be a g++ 4.1 parsing bug.
2010-04-01Adding check for --disable-shared on --enable-coverageChristopher L. Conway
2010-03-30Highlights of this commit are:Morgan Deters
* add NodeManagerWhite unit test * change kind::APPLY to kind::APPLY_UF * better APPLY handling: operators are no longer considered children * more efficient pool lookup; the NodeValue doesn't have to be as fully constructed for the lookup to proceed * extend DSL for kind declarations + new "theory" command declares a theory and its header. theory_def.h no longer required. + arity enforced on operators + constant mapping, hashing, equality * CONSTANT metakinds supported (via Node::getConst<T>(), for example, Node::getConst<CVC4::Rational>() gets a Rational out of a Node (assuming it is of CONST_RATIONAL kind) * added CONST_RATIONAL and CONST_INTEGER kinds * builtin operators (AND, OR, PLUS, etc..) returned by Node::getOperator() are now CONSTANT metakind and are created by NodeManager * Pretty-printing of Nodes now has a depth limit settable by a stream manipulator (e.g. "cout << Node::setdepth(5) << m << endl;" prints DAG rooted at m to a depth of 5) * getters added to Node, TNode, NodeValue, etc., for operators and metakinds * build-time generators for kind.h, metakind.h, and theoryof_table.h headers now have a simpler design and flag errors better, and the templates (kind_template.h etc.) are easier to understand. * DISTINCT is now a kind, and the SMT parser now passes through DISTINCT nodes instead of blowing them up into ANDs. Until theory rewriting is online, though, DISTINCTs are directly blown up into conjunctions in TheoryEngine::rewrite(). * add gmpxx detection and inclusion * better Asserts throughout, some documentation, cleanup
2010-03-26Added GMP backed Rational and Integer classes, and white box tests for them. ↵Tim King
You may have to reconfigure after this update.
2010-03-15This checkin resolves bug #57.Morgan Deters
* CVC4::theory::Interrupted no longer derives CVC4::Exception. * Interrupted is only thrown if "safe" parameter is TRUE ! * UF returns one conflict (instead of waiting for Interrupted to be thrown). * Minor build system work (quieter builds if V=0, better handling of build profiles in configure)
2010-03-12* src/context/cdmap.h: rename orderedIterator to iterator, do awayMorgan Deters
with old iterator (closes bug #47). * src/context/cdset.h: implemented. * src/expr/node_builder.h: fixed all the strict-aliasing warnings. * Remove Node::hash() and Expr::hash() (they had been aliases for getId()). There's now a NodeValue::internalHash(), for internal expr package purposes only, that doesn't depend on the ID. That's the only hashing of Nodes or Exprs. * Automake-quiet generation of kind.h, theoryof_table.h, and CVC and SMT parsers. * various minor code cleanups.
2010-03-08Adding quiet output of make by default. There are two additional options to ↵Dejan Jovanović
configure --enable-silent-rules less verbose build output (undo: `make V=1') --disable-silent-rules verbose build output (undo: `make V=0') If you need the verbose output, you can either reconfigure with --disable-silent-rules, or do a make V=0.
2010-03-05* public/private code untangled (smt/smt_engine.h no longer #includesMorgan Deters
expr/node.h). This removes the warnings we had during compilation, and heads off a number of potential linking errors due to improper inlining of private (library-only) stuff in client (out-of-library) code. * "configure" now takes some options as part of a "bare-option" build type (e.g., "./configure debug-coverage" or "./configure production-muzzle"). * split cdo.h, cdlist.h, cdmap.h, and cdset.h from context.h * split cdlist_black unit test from context_black * implement CDMap<>. * give ExprManagers ownership of the context (and have SmtEngine share that one) * fix main driver to properly report file-not-found * fix MemoryMappedInputBuffer class to report reasons for "errno"-returned system errors * src/expr/attribute.h: context-dependent attribute kinds now supported * test/unit/expr/node_white.h: context-dependent attribute tests * src/prop/cnf_conversion.h and associated parts of src/util/options.h and src/main/getopt.cpp: obsolete command-line option, removed. * src/util/Assert.h: assertions are now somewhat more useful (in debug builds, anyway) during stack unwinding. * test/unit/theory/theory_black.h: test context-dependent behavior of registerTerm() attribute for theories * src/expr/node_builder.h: formatting, fixes for arithmetic convenience node builders, check memory allocations * test/unit/expr/node_builder_black.h: add tessts for addition, subtraction, unary minus, and multiplication convenience node builders * src/expr/attribute.h: more comments * (various) code formatting, comment cleanup, added throws specifier to some destructors * contrib/code-checker: prototype perl script to test (some) code policy * contrib/indent-settings: command line for GNU indent to indent using CVC4 style (sort of; this is a work in progress) * COPYING: legal stuff * DESIGN_QUESTIONS: obsolete, removed
2010-02-22* configure.ac: Remove doc/ from search path for Makefile.amsMorgan Deters
* configure.ac, test/unit/Makefile.am: Resolved an issue where even when not testing, one unit test was built. * Re-ran contrib/update-copyright.pl on all source files to ensure consistent and correct header comments. * contrib/get-authors: Change definition of "minor contributor" to >= 10% of lines (rather than strictly greater than 10% of lines)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback