Developer's Guide

smooth over

   ./autogen.sh 
   ./configure
   make

 svn --username $USERNAME checkout https://subversive.cims.nyu.edu/cvc4/cvc4/trunk cvc4

 https://subversive.cims.nyu.edu/cvc4/cvc4/trunk

 svn --username $USERNAME ls https://subversive.cims.nyu.edu/cvc4/cvc4/branches

 svn --username $USERNAME checkout https://subversive.cims.nyu.edu/cvc4/cvc4/branches/experimental-quantifier-instantiation cvc4.quant

 [mdeters@adric ~]$ cd cvc4
 [mdeters@adric cvc4]$ svn info
 Path: .
 URL: https://subversive.cims.nyu.edu/cvc4/cvc4/trunk
 Repository Root: https://subversive.cims.nyu.edu/cvc4
 Repository UUID: 615e1583-3794-4256-8e52-04c157d34929
 Revision: 59
 Node Kind: directory
 Schedule: normal
 Last Changed Author: barrett
 Last Changed Rev: 59
 Last Changed Date: 2009-12-15 13:20:31 -0500 (Tue, 15 Dec 2009)

 [mdeters@adric cvc4]$

 svn --username $USERNAME cp https://subversive.cims.nyu.edu/cvc4/cvc4/trunk https://subversive.cims.nyu.edu/cvc4/cvc4/branches/my-branch

 svn --username $USERNAME checkout https://subversive.cims.nyu.edu/cvc4/cvc4/branches/my-branch cvc4.mybranch

 [mdeters@adric ~]$ cd cvc4
 [mdeters@adric cvc4]$ vi README.my-branch
 [mdeters@adric cvc4]$ cat README.my-branch
 This branch is to test the ideas of Splitting On Demand in SMT:

   ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BarNOT-LPAR-06.pdf

 -- Morgan Deters <mdeters@cs.nyu.edu>  Tue, 15 Dec 2009 17:31:01 -0500
 [mdeters@adric cvc4]$ svn add README.my-branch
 [mdeters@adric cvc4]$ svn commit

 svn --username $USERNAME cat https://subversive.cims.nyu.edu/cvc4/cvc4/branches/my-branch/README.my-branch
 This branch is to test the ideas of Splitting On Demand in SMT:

   ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/BarNOT-LPAR-06.pdf

 -- Morgan Deters <mdeters@cs.nyu.edu>  Tue, 15 Dec 2009 17:31:01 -0500

 [mdeters@adric ~]$ svn co https://subversive.cims.nyu.edu/cvc4/cvc4/trunk cvc4.clean
 [mdeters@adric ~]$ cd cvc4.clean
 [mdeters@adric cvc4.clean]$ svn merge https://subversive.cims.nyu.edu/cvc4/cvc4/branches/my-branch

 [mdeters@adric ~]$ cd cvc4.my-branch
 [mdeters@adric cvc4.my-branch]$ svn merge https://subversive.cims.nyu.edu/cvc4/cvc4/trunk

 svn --username $USERNAME cp https://subversive.cims.nyu.edu/cvc4/cvc4/trunk https://subversive.cims.nyu.edu/cvc4/cvc4/tags/cade2010

  [mdeters@adric ~]$ svn --username $USERNAME checkout https://subversive.cims.nyu.edu/cvc4/cvc4/tags/cade2010 cvc4.cade2010
  [mdeters@adric ~]$ cd cvc4.cade2010
  [mdeters@adric cvc4.cade2010]$ vi README.cade2010
  [mdeters@adric cvc4.cade2010]$ cat README.cade2010
  cade2010 version of CVC4
  ------------------------
  This version generated the results published in the CADE 2010 paper.

  -- Morgan Deters <mdeters@cs.nyu.edu>  Tue, 15 Dec 2009 17:39:05 -0500
  [mdeters@adric cvc4.cade2010]$ svn add README.cade2010
  [mdeters@adric cvc4.cade2010]$ svn commit

 svn mv foo.cpp bar.cpp

 svn mkdir newdir

 svn add newdir

 svn add new_source_file.cpp

 svn rm obsolete_test.h

 svn revert file.cpp

[mdeters@adric ~]$ svn co https://subversive.cims.nyu.edu/cvc4/cvc4/trunk cvc4.clean
[mdeters@adric ~]$ cd cvc4.clean
[mdeters@adric cvc4.clean]$ svn merge . -r 121:120

[mdeters@adric cvc4.clean]$ svn merge src/context -r 121:120

[mdeters@adric ~]$ cd cvc4
[mdeters@adric cvc4]$ EDITOR=vi svn propedit svn:ignore .

 svn propset svn:executable yes filename

svn resolved conflicting_file.cpp

 $ ./configure debug

 $ ./configure debug
 [a debug build is configured under builds/[ARCH]/debug/]
 $ make
 [builds the debug build, puts the binaries under builds/bin/]
 $ ./configure production
 [a production build is configured under builds/[ARCH]/production/]
 $ make
 [builds the production build, puts the binaries under builds/bin]
 $ make CURRENT_BUILD=[ARCH]/debug
 [builds the debug build, puts the binaries under builds/bin]
 $ make
 [builds the production build---it was the last-configured one]

 $ ./configure debug --enable-profiling --disable-assertions

 $ ./configure debug --enable-profiling --disable-assertions
 [a debug build with profiling and without assertions is configured under builds/[ARCH]/debug-profiling-noassertions/]
 $ make
 [builds the debug-noassertions-profiling build, puts the binaries under builds/bin/]
 $ ./configure debug
 [a debug build (with assertions, no profiling code) is configured under builds/[ARCH]/debug/]
 $ make
 [builds the debug build, puts the binaries under builds/bin]
 $ make CURRENT_BUILD=[ARCH]/debug-noassertions-profiling
 [builds the debug-noassertions-profiling build, puts the binaries under builds/bin]

$ builds/bin/cvc4 --show-config
This is a pre-release of CVC4.
Copyright (C) 2009, 2010
  The ACSys Group
  Courant Institute of Mathematical Sciences,
  New York University
  New York, NY  10012  USA

version   : prerelease

debug code: yes
tracing   : yes
muzzled   : no
assertions: yes
coverage  : no
profiling : no

$ ldd builds/bin/cvc4
        linux-gate.so.1 =>  (0x006b0000)
        libcvc4parser.so.0 => /home/mdeters/cvc4-cleancheckout/builds/usr/local/lib/libcvc4parser.so.0 (0x00e6d000)
        libcvc4.so.0 => /home/mdeters/cvc4-cleancheckout/builds/usr/local/lib/libcvc4.so.0 (0x00a75000)
        libgmp.so.3 => /usr/lib/libgmp.so.3 (0x00110000)
        libstdc++.so.6 => /usr/lib/libstdc++.so.6 (0x008d8000)
        libm.so.6 => /lib/tls/i686/cmov/libm.so.6 (0x00a11000)
        libgcc_s.so.1 => /lib/libgcc_s.so.1 (0x00298000)
        libc.so.6 => /lib/tls/i686/cmov/libc.so.6 (0x002b6000)
        /lib/ld-linux.so.2 (0x00d91000)

$ ldd /bin/bash-static
        not a dynamic executable

$ svn add source_file.cpp

$ svn add header_file.h

$ svn add newdir
topdir = ../..
srcdir = src/expr

include $(topdir)/Makefile.subdir

svn copy https://subversive.cims.nyu.edu/cvc4/vendor/$PACKAGE/$VERSION_NUMBER https://subversive.cims.nyu.edu/cvc4/vendor/$PACKAGE/current
svn checkout https://subversive.cims.nyu.edu/cvc4/vendor/$PACKAGE/current src/util/bar
valgrind --tool=callgrind --dump-every-bb=100000000 <executable> <arguments...>

adding support for google performance tools to the build sytem, it can be enabled at configure with
--with-google-perftools

to use it on ubuntu, you need to install packages google-perftools and libgoogle-perftools0

to run the profiling of the heap, you can run it for example with

HEAPPROFILE=/tmp/profile ./builds/bin/cvc4 test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.smt

this will create some files  /tmp/profile* that you can then

to get the pdf of the profile you can then run

google-pprof --pdf ./builds/bin/cvc4 /tmp/profile.0001.heap > profile.pdf

or for other options check http://goog-perftools.sourceforge.net/doc/

 #define DEBUG

 #ifdef DEBUG
 /* ... */
 #endif /* DEBUG */

 #define USE_MINISAT 1

 if(USE_MINISAT) {
   /* do something with minisat */
 } else {
   /* some non-minisat default behavior */
 }

   #define FOO do { S1; S2; } while(0)

  #define ADD(c, a, b) { int x = a, y = b; c = x + y; }
  int main() {
    int x = 5;
    // print out the value x + x ^ 2 (should be 30)
    int z;
    ADD(z, x, x * x);
    printf("%d\n", z); // does NOT print 30  :-(
  }

  #define ADD(c, a, b) { int __x = a, __y = b; c = x + y; }

  #define ADD(c, a, b) { int __add_x = (a), __add_y = (b); (c) = x + y; }

 class Foo {
   class Item;
   typedef Item*       iterator;
   typedef const Item* const_iterator;
 };

 class Foo {
   int d_thisIsAnInt;
 };

 class Foo {
   static int s_thisIsAStaticInt;
 };

 #include "util/output.h"
 CVC4::Debug("arith", "foo!"); // prints "foo!" if arith debugging is on
 CVC4::Warning("Equivalence classes didn't get merged."); // prints unless user gave -q or in SMT-COMP mode
 CVC4::Notice("Hi, so you don't get bored, here are some statistics: " + stats); // if user gives -v
 CVC4::Chat("I feel like doing some theory propagation.");// if user gives -vv
 CVC4::Trace("arith", "<ralph>I'm now calling a function!</ralph>");// if user gives -vvv

 CVC4::Debug::printf("arith", "foo!"); // no line termination

 CVC4::Debug("arith") << "foo!"; // also no line termination

 #include "util/assert.h"
 CVC4::Assert(condition); // asserts condition is true
 CVC4::Assert(condition, "error message on fail"); // asserts condition is true, custom error message

 #include "util/assert.h"
 CVC4::Unreachable(); // flags (supposedly) unreachable code; fails even under --disable-assertions
 CVC4::Unreachable("error message"); // custom error message

 #include "util/assert.h"
 CVC4::Unhandled(); // flags an unhandled case; fails even under --disable-assertions
 CVC4::Unhandled(the_case); // same but prints out the_case that's unhandled as well (which should be whatever is in the switch)
 CVC4::Unhandled("error message"); // custom error message
 CVC4::Unhandled(the_case, "error message"); // custom error message with the_case that is unhandled

 #include "util/assert.h"
 CVC4::AlwaysAssert(condition);
 CVC4::AlwaysAssert(condition, "error message");

 class CVC4_PUBLIC Expr {
   /* ... */
 public:
   Expr();
 };

   #ifndef __CVC4__ADJECTIVE_NOUN_H
   #define __CVC4__ADJECTIVE_NOUN_H

   ... declarations go here ...

   #endif /* __CVC4__ADJECTIVE_NOUN_H */

  x = y;
  z = y + 1;

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

  if(!(x + y > 4 && z < x)) ...

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

 Foo *a, *b;

 Bar* fooToBar(Foo* f);

 int main(int argc, char *argv[]);

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

   if(extra_output)
     do_something();

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

   if(extra_output)
     do_something_simple();
   else
     while(!done)
       for(int i = 0; i < 10; ++i)
         if(a[i] < 5)
           a[i + 10] += a[i];

  namespace CVC4 {

  namespace expr {
    class ExprValue;
  }/* CVC4::expr namespace */

  class Expr {
    /* ... */
  }/* class Expr */

  }/* CVC4 namespace */

 #if A
 #  if B
 #    warning A B case
 #  else /* ! B */
 #    warning A -B case
 #  endif /* B */
 #else /* ! B */
 #  if B
 #    warning -A B case
 #  else /* ! B */
 #    warning -A -B case
 #  endif /* B */
 #endif /* A */

 void foo() {
   NodeManager* nm = NodeManager::currentNM();
   Node a = nm->mkVar("a", nm->booleanType());
   Node b = nm->mkVar("b", nm->booleanType());
   Node n = nm->mkNode(kind::OR, a, b);
   Node not_n = negate(n);
 }

 Node negate(TNode tnode) {
   Node x = tnode.notNode();
   return x;
 }

 Node preprocess(TNode input);

 void query(TNode input) {
   input = preprocess(input);// <--- BUG!!
   // perform query...
 }

 void query(TNode input) {
   Node preprocessed = preprocess(input);
   // now work with 'preprocessed'...
 }

 void foo() {
   NodeManager* nm = NodeManager::currentNM();
   Node p = nm->mkVar("p", nm->booleanType());
   Node q = nm->mkVar("q", nm->booleanType());
   Node n = nm->mkVar(kind::OR, p, q);

   TNode x = n; // safe reference to expression (p OR q)

   Kind k = x.getKind();// <-- safe: get the kind of expression (p OR q)

   // point away from (p OR q)
   n = nm->mkVar(kind::AND, p, q);

   Kind k = x.getKind();// <-- UNSAFE: (p OR q) might not exist anymore!

   // reconstruct (p OR q)
   n = nm->mkVar(kind::OR, p, q);

   k = x.getKind();// <-- ALSO UNSAFE, (p OR q) might be in a different place in memory
   x = n;
   k = x.getKind();// <-- this is safe
 }

   gcov -o builds/ARCH/BUILD_ID/SRC_PATH SRC_PATH/foo.cpp

  mkdir -p HTML_DIR
  lcov --directory builds/ARCH/BUILD_ID/ --capture --output-file HTML_DIR/cvc4-gcov.info
  cd HTML_DIR
  genhtml cvc4-gcov.info

 namespace CVC4 {
 class Foo {
   /* pages
    * and
    * pages
    * go
    * by
    */
 };/* class Foo */
 }/* CVC4 namespace */

 #ifdef SOMETHING
 #  ifdef OTHERTHING
 #    error You can't do that.
 #  else /* !OTHERTHING */
 #    warning This is experimental code.
 #    define FOO(x) x
 #  endif /* OTHERTHING */
 #else /* SOMETHING */
 #  define FOO(x)
 #endif /* SOMETHING */

 #ifdef SOMETHING
 /* lots of
  * code here
  */
 #else /* !SOMETHING */
 /* lots of
  * code here
  */
 #  ifdef OTHERTHING /* && !SOMETHING */
 /* code... */
 #  endif
 #endif

 switch(foo) {
 case THIS_ONE:
   printf("this!\n");
   /* fall through */
 case THAT_ONE:
   printf("that!\n");
 }

/*********************                                                        */
/** ecdata.cpp
 ** Original author: taking
 ** Major contributors: mdeters
 ** Minor contributors (to current version): none
 ** This file is part of the CVC4 prototype.
 ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
 ** Courant Institute of Mathematical Sciences
 ** New York University
 ** See the file COPYING in the top-level source directory for licensing
 ** information.
 **
 ** Implementation of equivalence class data for UF theory.  This is a
 ** context-dependent object.
 **
 ** Reviewed by dejan, Feb 24 2010 (bug #10).
 ** Reviewed by mdeters, Apr 4 2010 (bug #64).
 **/

 http://cxxtest.tigris.org/files/documents/6421/43281/cxxtest-3.10.1.tar.gz

 ./configure --with-cxxtest-dir=~/cxxtest

$ make -C test/unit check

$ make -C src/expr check

TS_ASSERT( 1 + 1 > 1 );
TS_ASSERT_EQUALS( 1 + 1, 2 );

void testSomething() {
  TS_FAIL( "I don't know how to test this!" );
}

void testSomething() {
  TS_WARN( "TODO: This test still needs to be written!" );
}

 cvc4/test/unit/foo/bar.h

expr/expr_black.cpp:20: error: expected initializer before ‘suite_ExprBlack’                                                                                                                         
expr/expr_black.cpp:23: error: ‘suite_ExprBlack’ was not declared in this scope                                                                                                                      
expr/expr_black.cpp: In member function ‘virtual void TestDescription_ExprBlack_testDefaultCtor::runTest()’:                                                                                         
expr/expr_black.cpp:28: error: ‘suite_ExprBlack’ was not declared in this scope                                                                                                                      
expr/expr_black.cpp: In member function ‘virtual void TestDescription_ExprBlack_testCtors::runTest()’:                                                                                               
expr/expr_black.cpp:34: error: ‘suite_ExprBlack’ was not declared in this scope                                                                                                                      
...etc...

 $ make -C src/theory check

 $ (cd src/theory && make check)

 $ make
 [ libraries are rebuilt ]
 $ make -t check
 [the tests are marked up-to-date even though they aren't]
 $ make check
 [the tests are run]

 $ svn add test/regress/my_test.cvc

 $ make -C test/regress/regress2 check

/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/attribute.h: In member function �$-1òøvoid CVC4::expr::AttributeManager::setAttribute(const CVC4::Node&, const AttrKind&, const typename AttrKind::value_type&) [with AttrKind = TestFlag6]òù:
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/node_manager.h:128:   instantiated from �$-1òøvoid CVC4::NodeManager::setAttribute(const CVC4::Node&, const AttrKind&, const typename AttrKind::value_type&) [with AttrKind = TestFlag6]òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/node.h:291:   instantiated from �$-1òøvoid CVC4::Node::setAttribute(const AttrKind&, const typename AttrKind::value_type&) [with AttrKind = TestFlag6]òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../test/unit/expr/node_white.h:113:   instantiated from here
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/attribute.h:753: error: invalid use of undefined type �$-1òøstruct CVC4::expr::getTable<FooBar>òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/attribute.h:508: error: declaration of �$-1òøstruct CVC4::expr::getTable<FooBar>òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/attribute.h:755: error: invalid use of undefined type �$-1òøstruct CVC4::expr::getTable<FooBar>òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/attribute.h:508: error: declaration of �$-1òøstruct CVC4::expr::getTable<FooBar>òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/node_manager.h:128:   instantiated from �$-1òøvoid CVC4::NodeManager::setAttribute(const CVC4::Node&, const AttrKind&, const typename AttrKind::value_type&) [with AttrKind = TestFlag6]òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/node.h:291:   instantiated from �$-1òøvoid CVC4::Node::setAttribute(const AttrKind&, const typename AttrKind::value_type&) [with AttrKind = TestFlag6]òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../test/unit/expr/node_white.h:113:   instantiated from here
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/attribute.h:755: error: invalid use of undefined type �$-1òøstruct CVC4::expr::getTable<FooBar>òù
/home/mdeters/cvc4/builds/x86_64-unknown-linux-gnu/debug/../../../src/expr/attribute.h:508: error: declaration of �$-1òøstruct CVC4::expr::getTable<FooBar>òù
make[5]: *** [expr/node_white] Error 1

#!/bin/sh

export CLASSPATH=/usr/share/java/stringtemplate.jar:$ANTLR3_JAR
exec java org.antlr.Tool "$@"

./configure --prefix=$LIBANTLR3C_INSTALL_DIR

./configure --prefix=$LIBANTLR3C_INSTALL_DIR --enable-64bit

make
make install

sudo make install

If you ever happen to want to link against installed libraries
in a given directory, LIBDIR, you must either use libtool, and
specify the full pathname of the library, or use the `-LLIBDIR'
flag during linking and do at least one of the following:
   - add LIBDIR to the `LD_LIBRARY_PATH' environment variable
     during execution
   - add LIBDIR to the `LD_RUN_PATH' environment variable
     during linking
   - use the `-Wl,--rpath -Wl,LIBDIR' linker flag
   - have your system administrator add LIBDIR to `/etc/ld.so.conf'

./configure --with-antlr-dir=$LIBANTLR3_INSTALL_DIR ANTLR=$ANTLR3_DIR/antlr3"

cvc4/builds/$ARCH/$BUILD_MODE/config.log
$ uname -a
Linux box38.cims.nyu.edu 2.6.18-164.15.1.el5 #1 SMP Mon Mar 1 10:56:08 EST 2010 x86_64 x86_64 x86_64 GNU/Linux

  // annotatedFormula alternatives ...
  | MY_CONST_TOK 
    { std::string myConstText = AntlrInput::tokenText($MY_CONST_TOK);
      MyConstType c = ...;
      expr = MK_CONST(c); }

   sudo apt-get install libc6-dev-i386 g++-multilib lib32gmpxx4 lib32gmp3 lib32gmp3-dev

 Context c;

 CDO<int> i(&c);
 CDO<int> j(&c);
 i = 4;
 j = 3;

 c.push();

 i = 10000;
 j = -5;
 assert(i == 10000 && j == -5); // succeeds

 c.pop();

 assert(i == 4 && j == 3); // also succeeds

Developer's Guide

Contents

Source tree layout

Building CVC4

Dependencies

Building

Using CVC4's Subversion source control repository

Accessing CVC4's repository

Repository access from Eclipse

Browsing the repository

Branching and merging

Creating a branch

Merging a branch back to the trunk

Symbolically tagging a version

Branches versus tags

Working with files and directories

Reverting a file in a working directory

Reverting a commit

Ignoring files

Marking a file as executable in Subversion

Resolving conflicts in a working directory

For more information

The CVC4 build system

Build profiles

Working with multiple, concurrent build profiles

Determining the type of build from a binary

Adding source and header files

Adding source directories

Adding copyrighted sources

Checking that your Makefiles are correct

Profiling the code

prof, gprof, valgrind, callgrind

Google performance tools

Coding guidelines

File and directory names

Preprocessor macros

Binary macros

Block macros

Miscellaneous

Class names

Namespaces

Member names

Class Organization

Communicating with the user: the output classes

Assertions

Doxygen comments

Exporting library symbols

Source file layout

Class header files

Class implementation files

Imported sources

Source file headers

update-copyright.pl

Using emacs

Textual source layout

Whitespace/tabs

Increment/Decrement

Bracing

Indentation

Misc C++

Intentionally not covered

Adding a new Theory

Dealing with expressions (Nodes and TNodes)

Why this separation between Expr and Node?

Why this separation between Node and TNode?

Why this separation between TNode and NodeValue?

When to use TNodes

Using TNode on the stack

Using TNode in (heap-allocated) data structures

Use of autotools: automake, autoconf, autoheader, libtool

Commit policy

Unit tests with CxxTest

Coverage testing with gcov

Other coding guidelines (as yet uncategorized)

Vertical spacing

Code reviews

Binary compatibility: what is it and why do we care?

Unit testing

Running unit tests

Types of unit tests