Developer's Guide

Source tree layout

• config
  • this directory holds m4 macro processor files and bits of the autotools build system
• contrib
  • this directory includes maintainer scripts and other things that aren't directly part of CVC4
• doc
  • documentation
• src
  • core
    • the core of CVC4: the expression package, the core engines, ...
  • include
    • most include files (some private include files are also in parser and sat)
  • parser
    • parsers for supported CVC4 input formats
  • sat
    • propositional parts of CVC4; these include imported minisat sources

Coding guidelines

File and directory names

1. Files should be all lowercase, with CamelCase classes in header files named camel_case.h (and their implementations in camel_case.cpp);
2. File extensions .cpp and .h are generally preferred, with .ypp and .lpp for yacc and lex inputs---an exception is made for headers when autotools wants to output parser definitions as (e.g.) pl.hpp;

Source file layout

Class header files

1. A class named ThisIsAClass is guarded by a preprocessor macro __CVC4_THIS_IS_A_CLASS_H. Its definition is in src/include/this_is_a_class.h.
2. Everything should be in the CVC4 namespace.

Class implementation files

1. A class named ThisIsAClass should have its implementation under src/ in this_is_a_class.cpp.

Imported sources

1. IMPORTANT: For imported sources, make sure to add an exclusion to the contrib/update-copyright.pl script so that a CVC4 copyright isn't added.

Source file headers

1. A common comment blurb heads all source files in CVC4: non-imported headers and sources, as well as yacc and flex inputs.
2. A script is used to maintain/update this comment blurb.

update-copyright.pl

1. You can run contrib/update-copyright.pl to update all sources with a new copyright template. (Some) efforts are made to throw away old boilerplate comment blurbs and keep file-specific comments.
2. PLEASE BE CAREFUL: this updates files in place without keeping a backup. The script is probably buggy. You have been warned. It's best to do this on a copy of your source tree, or on a fresh repository checkout. (The program will warn you too.)
3. Please consult "svn diff" before committing changes made by the script.

Using emacs

1. There's an emacs-lisp snippet available that you can drop in your ~/.emacs to conform to spacing, indentation, etc., in the CVC4 source tree.
2. See contrib/editing-with-emacs.

General guidelines

Whitespace/tabs

1. No tabs, please.

Indentation

1. Indentation level is 2.
2. No indentation under switch() {} or namespace {}
3. Labels and "private/public/protected" are recessed 2.
4. template <class T> generally belongs on its own line before a function declaration or definition. An exception is inside a class file where there's a long string of simple functions that are best not separated by vertical space.
5. Attempt to keep lines under 80 columns wide. Though if this makes things excessively ugly or confusing, it's probably ok.

Use of autotools: automake, autoconf, autoheader, libtool

1. Please don't check into the repository things generated by automake, autoconf, autoheader, for example: config.h.in, Makefile.ins, Makefiles, ylwrap/libtool/aclocal.m4/missing/config.guess, configure, etc.