summaryrefslogtreecommitdiff
path: root/src/util/sexpr.h
AgeCommit message (Collapse)Author
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-05parser and core support for SMT-LIBv2 commands get-info, set-option, ↵Morgan Deters
get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...
2010-10-04remove/shuffle some #include dependencies; fix some documentation; apply ↵Morgan Deters
coding standards
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-02re-generated comment headers of source filesMorgan Deters
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-06-04** Don't fear the files-changed list, almost all changes are in the **Morgan Deters
** file-level documentation at the top of the sources. ** This is the "make bugzilla stop bugging me" bugfix commit. * Remove BackedNodeBuilder<> and collapse NodeBuilder<> hierarchy. Updated documentation in the file. Resolves bug #99. * Convenience NodeBuilders (PlusNodeBuilder, OrNodeBuilder, etc.) moved into a separate file. Partially resolves bug #100. * Moved isAssociative(Kind) into kind.h (and into the CVC4::kind namespace) instead of metakind.h (where it was in CVC4::metakind). This clears up a warning (private #inclusion) from the SMT and SMT2 parsers, and maybe makes more sense anyways, since this is based on the kind (and not the metakind) of an operator. * Documentation improvement; doxygen top-level \file gestures, \brief gestures for files, etc. Changed contrib/update-copyright.pl for this change, and post-processed to add \brief. Resolves bug #98. * Removed ExprManager::mkExpr(Kind) and NodeManager::mkNode(Kind). They no longer made sense. Resolves bug #91.
2010-05-04Adding general support for SMT2 set-info commandChristopher L. Conway
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback