summaryrefslogtreecommitdiff
path: root/configure.ac
AgeCommit message (Collapse)Author
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)
2010-02-22Re-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-22undoing 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, andCesare 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-22fix bug 33 (statically link the "cvc4" binary); also main driver cleanupMorgan Deters
2010-02-22fix bug 22 (remove tracing from non-trace builds; remove all outputMorgan 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-18Adding doxygen configuration parameters and doxygen-doc Makefile targetChristopher L. Conway
2010-02-17fix bug 27: --with-cxxtest-dir=(relative-path) now worksMorgan Deters
2010-02-06force 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-05auto-generated list of AC_CONFIG_FILES so that you needn't add each ↵Morgan Deters
recursive Makefile to configure.ac
2010-02-04remove warnings from use of __gnu_cxx::hash_map<>; also spacing fixes in ↵Morgan Deters
symbol table
2010-02-04test infrastructure updated for multiple-level regressionsMorgan Deters
2010-02-04added bool and arith theory makefiles to AC_CONFIG_FILES in configure.acMorgan Deters
2010-02-03Addressed 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-26fixes to build structure, util classes, lots of fixes to Node and ↵Morgan Deters
NodeBuilder. outstanding SEGVs fixed
2010-01-05Changes to configure.ac from code reviewChristopher L. Conway
2009-12-17add system regression testing infrastructureMorgan Deters
2009-12-17support nonstandard, unconfigured builds (e.g., "./configure debug" followed ↵Morgan Deters
by "make production ASSERTIONS=1")
2009-12-16Standardizing configure arguments for ANTLR/CxxTestChristopher L. Conway
2009-12-16Fixes 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-11build fixes, configuration simplificationsMorgan Deters
2009-12-10cleanups, assert work, add a stubbed uf theory, fix driverMorgan Deters
2009-12-08check in automake/libtool/autoconf-generated files; add better file not ↵Morgan Deters
found handling
2009-12-08work on propositional layer, expression builder support for large ↵Morgan Deters
expressions, output classes, and minisat
2009-12-07big check-in of various fixes and adjustmentsMorgan Deters
2009-12-07antlr parser for the cvc4 language (boolean only)Dejan Jovanović
yet to be finalized, it should work as expected
2009-12-06Big chunk of changes:Dejan Jovanović
* Fixed bugs in option parsing * Simplified the main.cpp significantly (more c++ like) * Added the null kind, expr value, and expression, with the default constructor public * Simplified commands, we need to discuss this in the meeting (what to do with command results?) * Removed all the lex/yacc files * Symbol table is now a templated class, as we will have tables for variables, predicates and functions * The ANTLR parsing infrastructure/makefiles is all in. SMT lib Boolean benchmarks should parse + giving nice error such as Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test4.smt:3:16: Undeclared variable p Parse Error: /home/dejan/eclipse-cxx/smtlib-parser/test/test2.smt:2:11: unexpected token: sa Didn't add any unit tests as the unit testing doesn't work with the updated build system -- it doesn't know how to create directories in the corresponding build directory. TODO: * add the PL grammar and unit test when the testing becomes available * with this build setup my eclipse debugger doesn't work. Might have something to do with the visibility of symbols? * i'm getting g++ depracated warnings regarding the hash_map from the symbol table, need to figure out how to use it in a standard manner. the new <unordered_map> header is for C++0x, and the <ext/hash_map> is getting deprecation warningns... weird.
2009-12-05more build system workMorgan Deters
2009-12-04more build system workMorgan Deters
2009-12-04More changes to configure.ac to include the smt grammar directory. The ↵Dejan Jovanović
parser refuses to be built in the new separate directory structure though.
2009-12-04Forgot to commit changes to configure.acDejan Jovanović
2009-12-03additional build system fixesMorgan Deters
2009-12-03first attempt at new build systemMorgan Deters
2009-11-25additional work on parser hookup, configuration + buildMorgan Deters
2009-11-24configure option adjustments as per 11/24 meeting; various fixes and ↵Morgan Deters
improvements
2009-11-20fixes to build/test systemMorgan Deters
2009-11-20fix to expr #includes; better test-environment configurationMorgan Deters
2009-11-19testing framework, configure fixes, incorporations from meeting, continued workMorgan Deters
2009-11-18work on exprs, driver, utilMorgan Deters
2009-11-17ignored itemsMorgan Deters
2009-11-17fixes and additionsMorgan Deters
2009-11-12parser, minisat, other things..Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback