Revision as of 05:14, 17 November 2009

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

Comments

Whitespace/tabs

1. No tabs, please.
2. No whitespace between if, for, while, 'catch', etc., and the parentheses.
3. One space between closing paren and open curly brace (except if aligning to other nearby source lines).
4. One space around binary operators to avoid crowding, e.g.:

  x = y;
  z = y + 1;

1. In complicated arithmetic expressions, even when parentheses aren't required by operator order of evaluation, sometimes parentheses and extra spacing and alignment should be used for visual clarity, or to match more closely what is being implemented, what is described in associated source code comments, or both. For example:

  if( ( ( x1 + y1 ) - ( z  * 2 ) ) <=  4 ||
      ( ( x2 + y2 ) - ( zp * 2 ) ) >= -4 ) { ... }

1. Occasionally to emphasize a !, so it doesn't get visually lost, it's best followed or even surrounded by space. For example, this is bad:

  if(!(x + y > 4)) ...

• while this is much preferred:

  if( !( x + y > 4 ) ) { ... }

• (assuming that it's preferable not to rewrite this as x + y <= 4 for some other reason of course).

Increment/Decrement

1. Preincrement/decrement preferred over postincrement/-decrement, e.g.:

  for(int x = 0; x < 10; ++x) { ... }

Bracing

1. Braces not required around one-line blocks, but preferred in complicated cases especially with if (to avoid visually-ambiguous elses).

• • E.g. this is fine:

   if(extra_output)
     do_something();

• • But this is debatable (preferring braces on the if() but not the for():

   if(extra_output)
     for(int i = 0; i < 10; ++i)
       do_something();

• • And this is horrible:

   if(extra_output)
     do_something_simple();
   else
     while(!done)

1. Generally, if the then part of an if is complicated and braced, but the else part is simple, the else need not be braced but may be. But if the else part is complicated and braced then the then part should be (even if it's simple).
2. If in doubt, brace.
3. If anything is visually ambiguous, brace for clarity.

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.