| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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. | |||
| 2010-05-27 | Use 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-27 | fix bug 120; competition mode regression failures for intentionally-buggy input | Morgan Deters | |
| 2010-05-04 | Disabling 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, 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-08 | A 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's | Morgan 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 arguments | Morgan 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-01 | PARSER 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-01 | Adding check for --disable-shared on --enable-coverage | Christopher L. Conway | |
| 2010-03-30 | Highlights 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-26 | Added GMP backed Rational and Integer classes, and white box tests for them. ↵ | Tim King | |
| You may have to reconfigure after this update. | |||
| 2010-03-15 | This 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 away | Morgan 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-08 | Adding 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 #includes | Morgan 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.ams | Morgan 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) | |||
| 2010-02-22 | Re-committing revision 232 properly: | Morgan Deters | |
| * Add virtual destructors to CnfStream, Theory, OutputChannel, and ExplainOutputChannel. Safer and stops a compiler warning. * node attributes: fix compiler warnings on 64-bit. * Node: add asserts to make sure the current NodeManager is non-NULL when it's needed. This can happen when public-facing functions don't properly set the node manager, and it can look like a bug in another part of the library. Also some code format cleanup. * configure.ac, config/cvc4.m4: added --enable-static-binary (see discussion on bug 33), fixed bad configure lines (bug 19), added documentation for some things. * config.h.in: removed; it's auto-generated. | |||
| 2010-02-22 | undoing improperly-committed revision 232; will re-commit to get "svn blame" ↵ | Morgan Deters | |
| correct, etc.. | |||
| 2010-02-22 | * Add virtual destructors to CnfStream, Theory, OutputChannel, and | Cesare Tinelli | |
| ExplainOutputChannel. Safer and stops a compiler warning. * node attributes: fix compiler warnings on 64-bit. * Node: add asserts to make sure the current NodeManager is non-NULL when it's needed. This can happen when public-facing functions don't properly set the node manager, and it can look like a bug in another part of the library. Also some code format cleanup. * configure.ac, config/cvc4.m4: added --enable-static-binary (see discussion on bug 32), fixed bad configure lines (bug 19), added documentation for some things. * config.h.in: removed; it's auto-generated. | |||
| 2010-02-22 | fix bug 33 (statically link the "cvc4" binary); also main driver cleanup | Morgan Deters | |
| 2010-02-22 | fix bug 22 (remove tracing from non-trace builds; remove all output | Morgan Deters | |
| from muzzled builds) add public-facing CVC4::Configuration class that gives CVC4's (static) configuration (whether debugging is enabled, assertions, version information, etc...) add some whitebox tests for assertions, output classes, and new CVC4::Configuration class main driver now gets about() information from CVC4::Configuration. configure.ac now more flexible at specifying major/minor/release versions of CVC4 add --show-config option that dumps CVC4's static configuration commented option processing strings in src/main/getopt.cpp fixed some compilation problems for muzzled builds. fixed some test code for non-assertion builds (where no assertions are expected) | |||
| 2010-02-18 | Adding doxygen configuration parameters and doxygen-doc Makefile target | Christopher L. Conway | |
| 2010-02-17 | fix bug 27: --with-cxxtest-dir=(relative-path) now works | Morgan Deters | |
| 2010-02-06 | force sorting of AC_CONFIG_FILES, otherwise different computers generate the ↵ | Morgan Deters | |
| configure script differently and we get useless commits of it; fix NodeBuilder memory leak in response to Kaustubh's expr code review (bug#15) | |||
| 2010-02-05 | auto-generated list of AC_CONFIG_FILES so that you needn't add each ↵ | Morgan Deters | |
| recursive Makefile to configure.ac | |||
| 2010-02-04 | remove warnings from use of __gnu_cxx::hash_map<>; also spacing fixes in ↵ | Morgan Deters | |
| symbol table | |||
| 2010-02-04 | test infrastructure updated for multiple-level regressions | Morgan Deters | |
| 2010-02-04 | added bool and arith theory makefiles to AC_CONFIG_FILES in configure.ac | Morgan Deters | |
| 2010-02-03 | Addressed many of the concerns of bug 10 (build system code review). | Morgan Deters | |
| Some parts split into other bugs: 19, 20, 21. Addressed concerns of bug 11 (util package code review). Slight parser source file modifications: file comments, #included headers in generated parsers/lexers Added CVC4::Result propagation back through MiniSat->PropEngine->SmtEngine->main(). Silenced MiniSat when verbosity is not requested. | |||
| 2010-01-26 | fixes to build structure, util classes, lots of fixes to Node and ↵ | Morgan Deters | |
| NodeBuilder. outstanding SEGVs fixed | |||
| 2010-01-05 | Changes to configure.ac from code review | Christopher L. Conway | |
| 2009-12-17 | add system regression testing infrastructure | Morgan Deters | |
| 2009-12-17 | support nonstandard, unconfigured builds (e.g., "./configure debug" followed ↵ | Morgan Deters | |
| by "make production ASSERTIONS=1") | |||
| 2009-12-16 | Standardizing configure arguments for ANTLR/CxxTest | Christopher L. Conway | |
| 2009-12-16 | Fixes to the build system: | Morgan Deters | |
| Makefile.am files - remove obsolete INCLUDES, incorporate into AM_CPPFLAGS Makefile files in src/ - support "make" under src/ (current build profile) configure.ac - updates to fix warnings config/antlr.m4 - updates to fix warnings autogen.sh - updates to generate warnings from autotools; also support Macs src/include/cvc4_config.h - guard with #ifdef total reimplementation of NodeBuilder ExprValue => NodeValue context_mm.{h,cpp} - fixed numerous compile errors | |||
| 2009-12-11 | build fixes, configuration simplifications | Morgan Deters | |
| 2009-12-10 | cleanups, assert work, add a stubbed uf theory, fix driver | Morgan Deters | |
| 2009-12-08 | check in automake/libtool/autoconf-generated files; add better file not ↵ | Morgan Deters | |
| found handling | |||
 |
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