Difference between revisions of "Developer's Guide"

smooth over

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

./configure 
    --prefix=/Users/Wei/Workspace/target/cvc4/ \ 
    CPPFLAGS=-I/opt/local/include \ 
    LDFLAGS=-L/opt/local/lib \
    JAVA_CPPFLAGS=-I/System/Library/Frameworks/JavaVM.framework/Headers \ 
    SWIG=/Users/Wei/Workspace/target/swig/bin/swig \ 
    --with-antlr-dir=/Users/Wei/Workspace/target/antlr3c \ 
    ANTLR=/Users/Wei/Workspace/target/antlr/antlr3 \
    --enable-language-bindings=java \
    --enable-static-binary

 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
    make V=1

   AR     libmain.a
   GEN    cvc4
 /usr/lib/gcc/x86_64-linux-gnu/4.7/../../../x86_64-linux-gnu/libreadline.a(complete.o): In function `rl_username_completion_function':
 (.text+0x38a9): warning: Using 'getpwent' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
 /usr/lib/gcc/x86_64-linux-gnu/4.7/../../../x86_64-linux-gnu/libreadline.a(tilde.o): In function `tilde_expand_word':
 (.text+0x224): warning: Using 'getpwnam' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
 /usr/lib/gcc/x86_64-linux-gnu/4.7/../../../x86_64-linux-gnu/libreadline.a(shell.o): In function `sh_get_home_dir':
 (.text+0x15c): warning: Using 'getpwuid' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
 /usr/lib/gcc/x86_64-linux-gnu/4.7/../../../x86_64-linux-gnu/libreadline.a(complete.o): In function `rl_username_completion_function':
 (.text+0x389f): warning: Using 'setpwent' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
 /usr/lib/gcc/x86_64-linux-gnu/4.7/../../../x86_64-linux-gnu/libreadline.a(complete.o): In function `rl_username_completion_function':
 (.text+0x3939): warning: Using 'endpwent' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
 make[7]: Leaving directory `/local/king/ws/cvc4/gh/builds/x86_64-unknown-linux-gnu/production-cln-glpk-staticbinary-optimized-proof-nodebugsymbols/src/main'

 ./configure \
 --enable-gpl \
 --with-build=production \
 --without-readline \
 --enable-optimized \
 --enable-static-binary \
 --disable-debug-symbols \
 --with-cln \
 --enable-proof \
 --with-glpk \
 --with-cxxtest-dir=/home/king/software/cxxtest \
 --with-antlr-dir=/home/king/targets/antlr/antlr3.4 \
 ANTLR=/local/king/ws/antlr/antlr-3.4/bin/antlr3 \
 GLPK_HOME=/home/king/targets/glpk-cut-log/ \
 CLN_LIBS="-L/home/king/targets/cln/lib -lcln" \
 CLN_CFLAGS="-I/home/king/targets/cln/include"

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/

 LD_PRELOAD="/usr/lib/libtcmalloc.so" CPUPROFILE=profile ./builds/bin/cvc4 foo.smt

  mkdir build # you likely want this outside of the LLVM directory
  cd build
  export PREFIX=$HOME/target/llvm
  cmake -G "Unix Makefiles" -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=$PREFIX ../llvm
  make
  make install # optional

  $ ./configure \
       --disable-proof \ # We need this for now
       [usual options --with-antlr-dir=... ANTLR=...  --with-build=debug ] \
       CC=$BUILD_DIR/bin/clang CXX=$BUILD_DIR/bin/clang++ LD=$BUILD_DIR/bin/clang \
       CFLAGS="-fsanitize=address -fno-omit-frame-pointer -g" \
       LDFLAGS="-fsanitize=address" \
       CXXFLAGS="-fsanitize=address -fno-omit-frame-pointer -g" 

  ASAN_SYMBOLIZER_PATH=$BUILD_DIR/bin/llvm-symbolizer ./builds/bin/cvc4 test/regress/regress0/ite5.smt2 

  ASAN_SYMBOLIZER_PATH=$BUILD_DIR/bin/llvm-symbolizer make regress

 #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

 void myFunction() {
   ScopedDebug guard("foo", true);
   /* ... */
 }

 #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).
 **/

#!/bin/bash
# cluster-regressions-cvc4
TO_EMAIL="`whoami`@cs.nyu.edu"
CC_EMAIL=""
function RunClusterRegressions() {
  local job_name="cvc4-$1"
  local cvc4_binary="$2"
  local params="--segv-nospin $3"
  local comment="$4"
  local timeout="$5"
  if [ -z "$timeout" ]; then
    timeout=300;
  fi
  mysql -u smt_cluster --password=`cat ~/.mysql_password` smt_cluster <<EOF
    insert into Jobs values(DEFAULT, "$job_name", "custom job:$comment", "22",\
    "$timeout", "2000", "24", "$TO_EMAIL $CC_EMAIL", "2", "$cvc4_binary",\
    "$params", "1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,29", \
    DEFAULT);
EOF
}

if [ $# -ne 3 -a $# -ne 4 ]; then
  echo "usage: $0 cvc4-binary \"solver params\" \"comment\" [timeout]"
  exit 1
fi

JOB_TIME=`date +%s`
NAME="cluster-regressions-$JOB_TIME"
RunClusterRegressions "$NAME" $1 "$2" "$3" "$4"

./cluster-regressions-cvc4 /full/path/to/cvc4/static/binary '--stats' 'running my crazy idea with stats enabled'

 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

 make -j4 check CVC4_REGRESSION_ARGS="-d arith::consistency"

   n.getAttribute(InstLevelAttribute())

   struct InstLevelAttributeId {};
   typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;

  expr::Attribute< Id, value_type, CleanupStrategy, Context-Dependent>

 struct CDAttribute<class T, value_type>

 // Attribute that tell if a node have been asserted in this branch
 struct AvailableInTermDbId {};
 /** use the special for boolean flag */
 typedef expr::Attribute<AvailableInTermDbId,
                       bool,
                       expr::attr::NullCleanupStrategy,
                       true  // context dependent
                       > AvailableInTermDb;

#!/bin/bash

export CLASSPATH=$ANTLR3_JAR
exec java org.antlr.Tool "$@"

./configure --disable-antlrdebug --prefix=$LIBANTLR3C_INSTALL_DIR

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

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'

./autogen.sh

./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

 builds/x86_64-unknown-linux-gnu/default/config.log

  // 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

@@ Line 1: / Line 1: @@
-In addition to this wiki, we also have a [http://cs.nyu.edu/mailman/listinfo/cvc4-devel developer mailing list] and [http://goedel.cims.nyu.edu/bugzilla3/ Bugzilla database] for this version of CVC.  CVC3 resources have been kept separate, at this time, because of the different needs of CVC4 during active development.
+In addition to this wiki, we also have a [http://cs.nyu.edu/mailman/listinfo/cvc4-devel developer mailing list] and [https://github.com/CVC4/CVC4/issues Github issue tracker] for this version of CVC.  CVC3 resources have been kept separate, at this time, because of the different needs of CVC4 during active development.
 =Source tree layout=
@@ Line 8: / Line 8: @@
 * <code>src/context</code> - context manager, context-dependent object/collection sources
 * <code>src/expr</code> - the expression package
-* <code>src/include</code> - public includes (installed in /usr/local or whatever on a users' machines)
+* <code>src/include</code> - systemwide includes
+* <code>src/lib</code> - replacement functions needed on some platforms (which ones are needed is determined by configure)
 * <code>src/main</code> - source for the main cvc4 binary
 * <code>src/parser</code> - parsers for supported CVC4 input formats
@@ Line 16: / Line 17: @@
 * <code>src/util</code> - utility classes, debugging macros, the Exception class, etc.
 * <code>test</code> - CxxTest unit tests (invoked by <code>make check</code>)
+=Building CVC4=
+==Dependencies==
+The following tools and libraries are required to build CVC4 (versions given are minimums; more recent releases are probably OK):
+* [http://www.gnu.org/software/automake Automake] v1.11
+* [http://www.gnu.org/software/autoconf/ Autoconf] v2.61
+* [http://www.gnu.org/software/libtool Libtool] v2.2
+* [http://gmplib.org/ GMP] v4.2
+* [http://antlr3.org ANTLR3] and [http://antlr3.org/download/C libantlr3c] v3.2 or v3.4 ''([[#ANTLR3|See below]])''
+* Boost
+* [http://www.ginac.de/CLN/ CLN] v1.3 ''(optional)''
+All of the above packages are available in recent releases of Fedora and in Debian 6.0 (squeeze). All current releases of Ubuntu have out-of-date packages for ANTLR3 and libantlr3c; this should be fixed in Ubuntu 11.04 (natty). Red Hat Enterprise Linux 5 has out-of-date autotools and ANTLR packages; the autotools packages should be fixed in RHEL 6 (don't know about ANTLR3 packages yet).
+==Building==
+If all of the dependencies are installed, you should be able to build CVC4 (from a subversion checkout) by running
+    ./autogen.sh
+    ./configure --with-antlr-dir=$LIBANTLR3_INSTALL_DIR ANTLR=$ANTLR3_DIR/antlr3"
+    make
+, where <code>$LIBANTLR3_INSTALL_DIR</code> and <code>$ANTLR3_DIR/antlr3</code> have been explained in ''[[#ANTLR3|ANTLR3]]''.
+The first step is not necessary if you have a distribution tarball (such as a release or a nightly build), as the configure scripts have already been generated in that case.  In the rest of this developer's guide below, it's generally assumed you're working with a Subversion checkout rather than a distributed source tarball.  Sometimes (as when updating the ''Makefile.am'' files, or adding source directories, you'll need to run "autoreconf" instead of "autogen.sh" if you're working from a source tarball.
+===Building on Mac OS X===
+Building CVC4 on Mac OS X is exactly the same as building on any Linux machine.  However, there are some gotchas:
+* The file system typically used on Mac OS X does not distinguish between uppercase and lowercase file names; this can sometimes cause problems.
+* The CVC4 build and test scripts may not function well in directory paths with embedded spaces; if this happens, it is a bug, but as a workaround, you can put the CVC4 sources in a directory path without spaces.
+* An OS X specific frustration is that by default CVC4's build system has libtool generate a wrapper executable for ./builds/bin/cvc4 (For more information see [http://www.gnu.org/software/libtool/manual/libtool.html#Wrapper-executables]).  This can make it quite hard to debug.  To get around this, you can pass "--enable-static-binary" at configure time.
+* You may need to install several packages via the [http://www.macports.org/ MacPorts] project (''e.g.,'' gmp); these are installed under ''/opt/local,'' which means you'll have to tell CVC4's ''configure'' script how to find the #includes and libraries (see below)
+On Mac OS X, several directory paths are nonstandard.  For starters, gmp, swig and cln are installed (via MacPorts) in ''/opt/local.''  Also, the Java development files on Mac OS are installed in a strange place.  You may end up with a configure line like the following:
+ ./configure
+     --prefix=/Users/Wei/Workspace/target/cvc4/ \
+     CPPFLAGS=-I/opt/local/include \
+     LDFLAGS=-L/opt/local/lib \
+     JAVA_CPPFLAGS=-I/System/Library/Frameworks/JavaVM.framework/Headers \
+     SWIG=/Users/Wei/Workspace/target/swig/bin/swig \
+     --with-antlr-dir=/Users/Wei/Workspace/target/antlr3c \
+     ANTLR=/Users/Wei/Workspace/target/antlr/antlr3 \
+     --enable-language-bindings=java \
+     --enable-static-binary
+If you find yourself building CVC4 a lot, of course, you can set these variables in your environment; ''configure'' will get them from there, so you don't have to enter them each time.
+===Building language bindings===
+The language bindings (for Java, python, perl, ocaml, etc...) each have their own requirements, and the ''configure'' script tries to figure out if you have (and if it can find) what's necessary.  Often, the ''configure'' script needs some help finding appropriate headers.  Each language has it's own CPPFLAGS and LDFLAGS variables you can set; they are used only when building and linking that language's bindings (''e.g.,'' JAVA_CPPFLAGS, JAVA_LDFLAGS, PYTHON_CPPFLAGS, etc.).
+Swig 2.0 is required for building the language bindings, and the latest version (2.0.4 at the time of writing) is strongly preferred.
 =Using CVC4's Subversion source control repository=
@@ Line 57: / Line 114: @@
 To check out a branch, you check out the branch path instead of the trunk:
-   <nowiki>svn --username $USERNAME checkout https://subversive.cims.nyu.edu/cvc4/cvc4/branches/experimental-quantifier-instantiation cvc4.quant</nowiki>
+   <nowiki>svn --username $USERNAME checkout \
+ https://subversive.cims.nyu.edu/cvc4/cvc4/branches/experimental-quantifier-instantiation cvc4.quant</nowiki>
 To get information about where a working directory came from, use <code>svn&nbsp;info</code>
@@ Line 82: / Line 140: @@
 To create a branch, you ''copy'' the source tree to another place:
-   <nowiki>svn --username $USERNAME cp https://subversive.cims.nyu.edu/cvc4/cvc4/trunk https://subversive.cims.nyu.edu/cvc4/cvc4/branches/my-branch</nowiki>
+   <nowiki>svn --username $USERNAME cp https://subversive.cims.nyu.edu/cvc4/cvc4/trunk \
+ https://subversive.cims.nyu.edu/cvc4/cvc4/branches/my-branch</nowiki>
 ...though '''please use a more descriptive name for your branch than this!'''  Then proceed by checking out the branch:
@@ Line 354: / Line 413: @@
 to add it to the repository, and edit the appropriate <code>Makefile.am</code> to list the file under <code>*_SOURCES</code> for the correct convenience library.  All the above should still apply.
+Sometimes you need to add something to <code>EXTRA_DIST</code> rather than <code>*_SOURCES</code> (for example, if something is conditionally built, depending on the <code>configure</code> script, or a README or some such).
 If you have problems getting the Makefile.in/Makefile/dependencies rebuilt, or get a warning from the <code>missing</code> script, re-run <code>autogen.sh</code> in the top-level source directory, re-run <code>configure</code>, and then proceed.
@@ Line 387: / Line 448: @@
 * ''autogen.sh'', our auto-build-system-generation script
-* doxygen macros for autoconf (under ''contrib/'')
+* doxygen, boost, and TLS macros for autoconf (under ''config/'')
 * MiniSat (under ''src/prop/minisat'')
-* ANTLR3 (some parts under ''src/parser'')
 Naturally, we have other ''dependencies'' too, like on ''CxxTest'' and on ''libgmp'', but for these we don't need to copy source under our tree; we are simply a client of those tools.
@@ Line 408: / Line 468: @@
 <ul>
 <li> Import a pristine version into the repository under ''<nowiki>https://subversive.cims.nyu.edu/cvc4/vendor/$PACKAGE/$VERSION_NUMBER</nowiki>''. </li>
-<li> Copy to "current":<pre>svn copy https://subversive.cims.nyu.edu/cvc4/vendor/$PACKAGE/$VERSION_NUMBER https://subversive.cims.nyu.edu/cvc4/vendor/$PACKAGE/current</pre> </li>
+<li> Copy to "current":<pre>svn copy https://subversive.cims.nyu.edu/cvc4/vendor/$PACKAGE/$VERSION_NUMBER \
+https://subversive.cims.nyu.edu/cvc4/vendor/$PACKAGE/current</pre> </li>
 <li> Now copy into the cvc4 source tree.  You can "copy" into your current working directory with svn checkout, for example:<pre>svn checkout https://subversive.cims.nyu.edu/cvc4/vendor/$PACKAGE/current src/util/bar</pre> will copy your package under CVC4's src/util directory as "bar."  '''It is important that you use svn to do this, so there's a record of the link between the vendor branch and the "bar" directory.'''</li>
 </ul>
@@ Line 430: / Line 491: @@
 </li>
 </ol>
+==Checking that your Makefiles are correct==
+[http://www.gnu.org/software/hello/manual/automake/Checking-the-Distribution.html This part of the Automake manual] might be useful to people.  <code>make distcheck</code> builds CVC4 and checks it ("make check"), then does a "make install" and "make uninstall" to make sure they are working, then builds a tarball ("make dist"), then builds ''that tarball'' with configure and make, runs the test suite ("make check") on that, then does another "make dist" from the dist to make sure the distribution can itself make a distribution.  Then, it does a "make distclean" and makes sure nothing remains (distclean is supposed to clear out everything from a build, leaving you with a pristine distribution).
+==kinds files==
+After touching kinds files, test/system/ files that were originally compiled against different for different kinds files may have some trouble. To fix this, simply touch the corresponding .cpp file to get it to recompile and relink.
+==Make Verbose==
+To get the "verbose" version of make, run with the "V=1" flag:
+     make V=1
+This is useful for debugging linking problems and other compilation problems.
+==Preparing Binaries for Starexec==
+There are a few steps for configurating a binary for Starexec.
+# Make a static binary using --enable-static-binary.
+# Remove debugging symbols --disable-debug-symbols. This may be done after the fact using the command "strip cvc4".
+# Disable the readline package? See the warning below.
+    AR     libmain.a
+    GEN    cvc4
+  /usr/lib/gcc/x86_64-linux-gnu/4.7/../../../x86_64-linux-gnu/libreadline.a(complete.o): In function `rl_username_completion_function':
+  (.text+0x38a9): warning: Using 'getpwent' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
+  /usr/lib/gcc/x86_64-linux-gnu/4.7/../../../x86_64-linux-gnu/libreadline.a(tilde.o): In function `tilde_expand_word':
+  (.text+0x224): warning: Using 'getpwnam' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
+  /usr/lib/gcc/x86_64-linux-gnu/4.7/../../../x86_64-linux-gnu/libreadline.a(shell.o): In function `sh_get_home_dir':
+  (.text+0x15c): warning: Using 'getpwuid' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
+  /usr/lib/gcc/x86_64-linux-gnu/4.7/../../../x86_64-linux-gnu/libreadline.a(complete.o): In function `rl_username_completion_function':
+  (.text+0x389f): warning: Using 'setpwent' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
+  /usr/lib/gcc/x86_64-linux-gnu/4.7/../../../x86_64-linux-gnu/libreadline.a(complete.o): In function `rl_username_completion_function':
+  (.text+0x3939): warning: Using 'endpwent' in statically linked applications requires at runtime the shared libraries from the glibc version used for linking
+  make[7]: Leaving directory `/local/king/ws/cvc4/gh/builds/x86_64-unknown-linux-gnu/production-cln-glpk-staticbinary-optimized-proof-nodebugsymbols/src/main'
+An example of a starexec configuration with proofs, cln and glpk-cut-log enabled.
+  ./configure \
+  --enable-gpl \
+  --with-build=production \
+  --without-readline \
+  --enable-optimized \
+  --enable-static-binary \
+  --disable-debug-symbols \
+  --with-cln \
+  --enable-proof \
+  --with-glpk \
+  --with-cxxtest-dir=/home/king/software/cxxtest \
+  --with-antlr-dir=/home/king/targets/antlr/antlr3.4 \
+  ANTLR=/local/king/ws/antlr/antlr-3.4/bin/antlr3 \
+  GLPK_HOME=/home/king/targets/glpk-cut-log/ \
+  CLN_LIBS="-L/home/king/targets/cln/lib -lcln" \
+  CLN_CFLAGS="-I/home/king/targets/cln/include"
+=Profiling the code=
+==prof, gprof, valgrind, callgrind==
+To profile CVC4, configure with <code>--enable-profiling</code>. Unfortunately, GProf can't instrument system calls, so it will give misleading results for allocation-heavy programs like CVC4. Instead, you can use the Callgrind tool (a component of Valgrind):
+ valgrind --tool=callgrind --dump-every-bb=100000000 ''<executable> <arguments...>''
+(The <code>--dump-every-bb</code> argument causes Callgrind to produce incremental data periodically throughout the execution. A value of 100,000,000 or higher is recommended to keep the number of data files emitted manageable.) Callgrind will create a master file <code>callgrind.out.''<pid>''</code> and a number of incremental data files (<code>callgrind.out.''<pid>''.1</code>, <code>callgrind.out.''<pid>''.2</code>, etc). Open <code>callgrind.out.''<pid>''</code> using the KCachegrind GUI tool to visualize the profiling information. (You can do this before the program has terminated. Pressing F5 will cause KCachegrind to load any new incremental data.)
+==Google performance tools==
+Recently, [[User:cconway|Chris Conway]] recommended [http://goog-perftools.sourceforge.net/ Google's performance tools] for profiling, and as of revision 1454 (March 14, 2011), [[User:dejan|Dejan Jovanović]] added support for it.  Here are Dejan's revision notes:
+ 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/
+If you are having problems with cln or gmp segfaulting, try setting LD_PRELOAD to libtcmalloc. For example:
+  LD_PRELOAD="/usr/lib/libtcmalloc.so" CPUPROFILE=profile ./builds/bin/cvc4 foo.smt
+For more information, see [[Build_Problems#Profiling]].
+==Using ASAN==
+Step 1: Install Clang and LLVM from source.
+A) Install cmake.
+B) Follow the instructions for downloading clang from source [http://clang.llvm.org/get_started.html here]. You need to do steps 2 (checkout llvm), 3 (checkout clang) and 5 (checkout compiler-rt).
+C) Proceed to step 7 (building LLVM and Clang). It is recommended to use a prefix in $HOME. We'll use $PREFIX for this directory.
+   mkdir build # you likely want this outside of the LLVM directory
+   cd build
+   export PREFIX=$HOME/target/llvm
+   cmake -G "Unix Makefiles" -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=$PREFIX ../llvm
+   make
+   make install # optional
+Step 2: Configuring CVC4
+A) This is mostly all done at configure time. The main goals are to disable proofs (for now), set binary locations, and add compilation and linking flags. Let $BUILD_DIR be the directory build/ created above.
+   $ ./configure \
+        --disable-proof \ # We need this for now
+        [usual options --with-antlr-dir=... ANTLR=...  --with-build=debug ] \
+        CC=$BUILD_DIR/bin/clang CXX=$BUILD_DIR/bin/clang++ LD=$BUILD_DIR/bin/clang \
+        CFLAGS="-fsanitize=address -fno-omit-frame-pointer -g" \
+        LDFLAGS="-fsanitize=address" \
+        CXXFLAGS="-fsanitize=address -fno-omit-frame-pointer -g"
+B) Recompile with make
+Step 3: Running ASAN
+A) The documentation is [http://clang.llvm.org/docs/AddressSanitizer.html here].
+B) To run CVC4 with one example:
+   ASAN_SYMBOLIZER_PATH=$BUILD_DIR/bin/llvm-symbolizer ./builds/bin/cvc4 test/regress/regress0/ite5.smt2
+C) To run CVC4 on make regress:
+   ASAN_SYMBOLIZER_PATH=$BUILD_DIR/bin/llvm-symbolizer make regress
 =Coding guidelines=
@@ Line 529: / Line 721: @@
 * Union elements are prefixed with <code>u_</code>.
-* There is an exception to these rules for low-level ''struct'' types that have no member functions and no destructors (and only simple, initializing constructors).  For an example see the definition of ''CVC4::Options'' in <code>src/util/options.h</code>.
+* There is an exception to these rules for low-level ''struct'' types that have no member functions and no destructors (and only simple, initializing constructors).  For an example see the definition of ''CVC4::Options'' in <code>src/smt/options.h</code>.
 ==Class Organization==
@@ Line 558: / Line 750: @@
    CVC4::Debug("arith") << "foo!"; // also no line termination
 For non-debug builds, ''CVC4::Debug'' is a no-op and everything will be inlined away.
+ScopedDebug/ScopedTrace allow you to turn on a Debug/Trace flag just for a function, using the RAII C++ idiom.  So e.g.
+  void myFunction() {
+    ScopedDebug guard("foo", true);
+    /* ... */
+  }
+will ensure that the "foo" tag is on for the duration of calls to myFunction(), then returned to its original setting.
+IndentedScope is to give you the ability to indent stuff, for example if you are looping over a data structure or (especially) if you have nested loops.  You create an IndentedScope around the stream whenever you want to increase the indentation, again in RAII style. For indentation to work you should always use std::endl instead of "\n" to end lines.
 ==Assertions==
@@ Line 758: / Line 961: @@
 * 0 vs NULL
+=Adding a new Theory=
+One of the first things that new developers need to do is ''add a new theory.''  Here's the overall procedure:
+# If your theory is likely to shake things up in other parts of CVC4 for awhile, branch the repo (see [[#Branching and merging|''Branching and merging'']]).  Make sure your working copy is up to date.
+# Add a new directory for your theory (assuming you're implementing the Theory of Foo, you might use: ''mkdir src/theory/foo'')
+# Use ''addsourcedir'' ([[#Adding source directories|see the Developer's Guide section on that script]]) to set up the directory (''contrib/addsourcedir src/theory/foo'').
+# Add your directory to SUBDIRS in ''src/theory/Makefile.am''.
+# Add a ''kinds'' file specifying kinds for your theory.  The file can be empty, to start.
+# Add these files to the repository (''svn add src/theory/foo'')
+# Add ''Makefile.in'' to the ''svn:ignore'' property of your directory (''svn ps svn:ignore Makefile.in src/theory/foo'')
+# Re-run ''autogen.sh'' at the top-level.  This finds your new directory and adds it to the list of things to set up when ''configure'' runs.
+You'll now need to implement your theory!  Any source files you add will need to be listed in the appropriate ''SOURCES'' variable in your theory's ''Makefile.am''.  Any "extra things" (README files, notes, anything else that isn't really a "source" but should be included in the CVC4 tarball) should be listed in ''EXTRA_DIST''.
+There are places outside of your theory's directory you'll need to support, too.  If you want your theory to be supported by one or more input languages (instead of just through the CVC4 library API), you'll need to add support to the appropriate parser(s), under ''src/parser/LANGUAGE''.  (Right now we don't do prettyprinting, but that will eventually be in there, too.)  You'll also need to add typechecking to the ''NodeManager'' (in ''src/expr/node_manager.cpp''), and probably you'll want to add a ''type_rules'' file to your theory implementing theory-specific type rules (currently, the only modification to ''NodeManager'' is to switch on the node kind and delegate to your theory's type rules).
+For more details see [[How to write a theory in CVC4]].
+=Dealing with expressions (Nodes and TNodes)=
+There are three types in CVC4 that conceptually represent the same thing.
+# An ''Expr'' is a [[#Exporting library symbols|publicly-visible type]] that references expression data and the associated expression manager.
+# A ''Node'' is a CVC4-internal type that references expression data but '''not''' the associated expression manager (the manager is implicitly the "current" node manager)
+# A ''TNode'' is just like a ''Node'' except that it doesn't maintain a reference count.
+==Why this separation between Expr and Node?==
+In the library, we want to ensure that expressions are referenced correctly (that is, with deference to the appropriate expression manager).  We can police our own use of expressions, but we can't do the same for the users of the library.  Therefore we require external use of CVC4 expressions through the "heavier" ''Expr'' object to ensure correctness, but internally we want to use the lighter-weight ''Node'' objects.
+Similarly, ''ExprManager'' and ''NodeManager'' are split, but are conceptually the same.  ''NodeManager'' does all the real "managing" of expression data (and it has construction and reclamation-related duties) and ''ExprManager'' is the [[#Exporting library symbols|user-visible]]s, public interface to this manager.
+Under the hood, ''Expr'' objects are two simply two pointers: one to a ''Node'' and one to an ''ExprManager'', and all its implemented functionality simply delegates to one or the other.
+==Why this separation between Node and TNode?==
+Internally, then, a ''Node'' is just a "smart" pointer to a ''NodeValue'' structure, which contains expression kind information, the reference count, pointers to child expressions, etc.  Even internally to the CVC4 library, we don't allow general access to ''NodeValue''---we require all expression manipulation to go through ''Node'' objects.  Conceptually, ''Node'' objects are simple; they simply delegate to the underlying ''NodeValue''.  However, they have another purpose---to maintain the reference count on the ''NodeValue''.  When a ''Node'' object is created pointing to a ''NodeValue'', it increases the reference count on that ''NodeValue''.  When the ''Node'' is destructed (or points away), it decrements the reference count.
+This handling of the reference count can be expensive as ''Node'' objects are passed between functions, stored in data structures, updated on backtrack, etc.  Sometimes this is necessary for safety---that is, to maintain a correct reference count.  Other times, though, it's not necessary ([[#When to use TNodes|see below]]), and the use of ''TNode'' in preference to ''Node'' removes the reference-counting overhead.
+Under the hood, one template type (the ''NodeTemplate<>'') implements both ''Node'' and ''TNode''---''Node'' and ''TNode'' are typedefs to instantiations of the ''NodeTemplate<>'' template with (respectively) reference-counting turned on and off.
+==Why this separation between TNode and NodeValue?==
+One could ask, then, why does ''TNode'' exist if it conceptually provides the same services as the underlying ''NodeValue'' and it doesn't reference-count it?  Couldn't we just access the ''NodeValue'' directly?  There are two main reasons.  First, in assertions-enabled builds, ''TNode'' objects include extra assertions to make sure they're being used correctly---that is, that a ''TNode'' never references a ''NodeValue'' with a zero reference count, which is unsafe since that ''NodeValue'' is eligible for reclamation by the ''NodeManager''.  Second, the interface on ''NodeValue'' is somewhat lower-level than on ''Node'' and ''TNode'', and using the higher-level forms allows one to interchange ''Node'' and ''TNode'' without compiler troubles (one should only do so where [[#When to use TNodes|it's safe to do so]], of course).  Additionally, the use of ''TNode'' ensures that the expression data is not modified---conceptually, expressions are immutable, but of course at the lower layers of the expression package, they aren't technically immutable, so passing around a ''const NodeValue*'' would '''not''' be appropriate.
+==When to use TNodes==
+So when should one use ''TNode'' and when should one use ''Node'' when referring to expression data?
+This is a difficult question, but there are some general rules.
+First of all, it's always safe to use ''Node'', so if you're erring on the side of caution, use ''Node'' and not ''TNode''.
+''TNode'' is safe to use '''only''' when you know that a ''Node'' exists that refers to the same underlying expression data.  Since each ''NodeManager'' maintains the invariant that each expression is represented uniquely by one ''NodeValue'', that means that if a ''Node'' is guaranteed to refer to an expression, a ''TNode'' can be used to reference the same expression.  At such point as the ''Node'' no longer exists, it is no longer safe to use the ''TNode''.
+===Using TNode on the stack===
+In well-scoped situations like function calls, it's then ok to use a TNode:
+  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;
+  }
+Here, ''foo()'' calls function ''negate()'' to negate a ''Node''.  However, the function accepts the node parameter as a ''TNode''---this is ok, because a ''TNode'' can be constructed from a ''Node''.  At the function call, a copy of the underlying pointer to ''NodeValue'' is made, but no reference counting is done.  Note that when an expression is created (with ''tnode.notNode()''), however, the result is stored in a ''Node''.  It would '''not''' be safe to store this in a ''TNode'', since the negation of the parameter is not guaranteed to have an outstanding ''Node'' reference to it (and thus to have a nonzero reference count).
+'''The general rule is: functions should take TNode arguments but always return Node.'''  There are exceptions, but this one rule covers a lot.  A common mistake is reusing a variable of type ''TNode'' where it should be a ''Node'', for example:
+  Node preprocess(TNode input);
+  void query(TNode input) {
+    input = preprocess(input);// <--- BUG!!
+    // perform query...
+  }
+This is a serious error.  ''preprocess()'' will (it is presumed) take ''input'' and either create a new equivalent expression, returning that, or if no preprocessing is required, return the input.  But here, the ''Node'' return value of ''preprocess()'' is turned into a TNode in the caller's context, and the reference count on the expression data is decremented.  This means the result of preprocessing may be reclaimed by the system immediately on return of the ''preprocess()'' function!  The correct way to write ''query()'' is the following:
+  void query(TNode input) {
+    Node preprocessed = preprocess(input);
+    // now work with 'preprocessed'...
+  }
+==Using TNode in (heap-allocated) data structures==
+So far, this only handles stack-based (function call) uses for ''TNode''.  ''TNode'' objects can also be kept in data structures, but that's more complicated.  I repeat again, from the above: '''At such point as the ''Node'' no longer exists, it is no longer safe to use the ''TNode'''''.  That has an important further clarification: '''even if the ''Node'' is re-established later, it's unsafe to maintain a ''TNode'' to the expression, since the underlying ''NodeValue'' may have been reclaimed by the system and re-constructed!'''  Consider this code:
+  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
+  }
+As you trace through this code, keep in mind that if the reference count for an expression drops to zero (there are no ''Node'' references to it, only ''TNode'' references), then it is immediately eligible for reclamation by the ''NodeManager''.  So, here, ''x'' is initially a safe ''TNode'' reference to ''(p OR q)''---but then ''n'' points elsewhere, and ''x'' is no longer safe to use.  You might think that, given that the ''NodeManager'' maintains unique underlying expression structures for all expressions, that after re-constructing ''(p OR q)'', you could use ''x'' again.  But this is not true---the expression data ''may'' have been destroyed in the meantime, and thus the reconstructed ''(p OR q)'' could be a different (but still unique, since the other one has disappeared) ''NodeValue''.  This makes ''x'' unsafe to use.
+That means that you '''cannot store a ''TNode'' in a data structure unless a ''Node'' to the same expression is guaranteed to exist at least as long as the ''TNode'' does!'''  Even if you can guarantee that a ''Node'' exists every time to ''use'' the ''TNode'', this isn't enough: a "solid" ''Node'' reference must exist at all times to the underlying expression.  If you cannot guarantee this, you cannot use a ''TNode'', you must use ''Node''.
+There is no "general rule" for putting ''TNode'' in heap-allocated data structures, as there is with function calls on the stack.  Sometimes you can store ''Node'' objects in one data structure, and that permits the storage of ''TNode'' objects in another; but it depends on your data.  You just have to make sure that reference count stays above zero at all times.
+By the way, in the above program, often a re-created expression ''does'' have the same underlying ''NodeValue'', since zero-reference-count expressions are not immediately reclaimed (they are in the so-called ''zombie'' state, and they are reclaimed in bulk when there are enough zombies).  But because they are immediately ''eligible'' for reclamation, you cannot rely on this.
+==Node comparisons==
+You can compare Node and TNode using the usual comparison operator (<,>,<=,>=). The result of these operators will remain stable until the underlying NodeValue disappears. So if some of your datastructures depend on the order of Nodes you should keep them alive somewhere, since when a NodeValue is recreated it will compare differently than the disappeared NodeValue.
 =Use of autotools: automake, autoconf, autoheader, libtool=
@@ Line 765: / Line 1,098: @@
 =Commit policy=
-* Before you commit, everything should be documented and your code should conform to the coding guidelines.
+* ''Before you commit,'' everything should be documented and your code should conform to the coding guidelines.
-* An automated bot will review code commits and complain loudly to you if it doesn't like your documentation or coding style.
+* ''Before you commit,'' your source tree should pass a "make check" in both ''debug'' and ''production'' configurations.
-* Clark will review all code commits for content.
+* Ideally, your code is cross-platform, and at the very least works equally well on 32- and 64-bit Intel, but this can be difficult to determine sometimes.
-* Others in the group will review Clark's commits for content.
+* An automated bot will review code commits and complain loudly to you if it doesn't like your documentation or coding style [''wishlist---not yet implemented, except for a few [http://church.cims.nyu.edu/newswire/ newswire] items''].
-* Unit tests should be included to test any new functionality included in your commit.  These tests should pass the ''gcov'' coverage assessment for CVC4.
+* ''After you commit,'' Clark will review the commit for content.  (This is after the fact, you don't have to get a sign-off to commit.)
+* ''After Clark commits,'' others in the group will review his commits for content.  (Also after the fact.)
+* ''In practice,'' everybody reviews everyone else's commits, but on their own schedule.
+* Unit tests / system tests / regression tests should be included to test any new functionality included in your commit.
+* Any new code should be well-covered.  Please check the [http://church.cims.nyu.edu/cvc4-builds/coverage/latest/ coverage report] the next day to make sure your code is well-covered by unit tests, system tests, and regressions.  If not, add some tests to the source tree.
 =Unit tests with CxxTest=
@@ Line 779: / Line 1,116: @@
 ==Coverage testing with gcov==
-Every ''non-exceptional'' line of code should be tickled by a unit test. To generate code coverage information, configure CVC4 with <code>--enable-coverage</code> and <code>--disable-shared</code> (the coverage instrumentation is incompatible with shared binaries), recompile the project, then run <code>make check</code>.
+Every ''non-exceptional'' line of code should be tickled by a unit test. To generate code coverage information, configure CVC4 with <code>--enable-coverage</code>, recompile the project, then run <code>make check</code>.
 The code coverage information for a single file <code>SRC_PATH/foo.cpp</code> (and its <code>#include</code>'d dependencies) can be obtained by executing:
      gcov -o builds/ARCH/BUILD_ID/SRC_PATH SRC_PATH/foo.cpp
+''If you have multiple builds configured simultaneously, remember to use the correct BUILD_ID!  It will have '''coverage''' in its name, something like '''debug-coverage''' or '''production-coverage'''.''
 This will print out the percentage coverage of each processed file and create a set of <code>.gcov</code> files in the current directory. The <code>.gcov</code> files reproduce the source code with execution counts. More information about <code>gcov</code> usage is available from [http://gcc.gnu.org/onlinedocs/gcc/Gcov.html the online manual].
-You can use the [http://ltp.sourceforge.net/coverage/lcov.php <code>lcov</code>] tool to produce a more global, browseable coverage report. (<code>lcov</code> is installable via APT After running <code>make check</code> with a coverage-enabled build, execute:
+You can use the [http://ltp.sourceforge.net/coverage/lcov.php <code>lcov</code>] tool to produce a more global, browseable coverage report. (<code>lcov</code> is installable via ''APT'' and the package includes both ''lcov'' and ''genhtml'', used below). Simply run <code>make lcov</code>.
-    lcov --directory builds/ARCH/BUILD_ID/src --capture --output-file HTML_DIR/cvc4-gcov.info
+If that doesn't work for some reason, you can try running <code>lcov</code> manually. After running <code>make check</code> with a coverage-enabled build, execute:
+   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
@@ Line 863: / Line 1,204: @@
 <li> Slightly larger issues (refactoring, renaming of critical variables, methods, etc.), even when it's to bring the code in line with coding guidelines, can be directly committed but should be communicated to the developer of the code and noted on the Subversion revision log and the code review bug ticket.</li>
 <li> Larger, architectural changes to the module should be worked on WITH the developer, not solely by the code reviewer.</li>
-<li> If, during the course of review, additional changes are indicated to modules ''other'' than the one formally under review, those should be opened as an additional review/bug ticket, or mentioned to the developer of those modules for correction.</li></ol></li>
+<li> If, during the course of review, additional changes are indicated to modules ''other'' than the one formally under review, those should be opened as an additional review/bug ticket, or mentioned to the developer of those modules for correction.</li>
+<li> In general, ''please avoid having "discussions" with the developer in comments in the source code.''</ol></li>
 <li> '''Bugs, requests for documentation, etc., should be filed as ''separate'' bug tickets in bugzilla, with the module's original developer as the assignee.'''
@@ Line 876: / Line 1,218: @@
 <li> '''In the documentation at the top of all relevant file(s), mark yourself as the reviewer.'''
-<ul><li>For example:
+<ul><li>If there are other reviews listed, put yours at the end of the list (so they remain in chronological order).</li>
-<div style="white-space:pre;">
+<li>List your name, the date, and the code review ticket number.</li>
-/*********************                                                        */
+<li>For example:
-/** ecdata.cpp
+<div style="white-space:pre;font-size:larger;">
- ** Original author: taking
+ /*********************                                                        */
- ** Major contributors: mdeters
+ /** ecdata.cpp
- ** Minor contributors (to current version): none
+  ** Original author: taking
- ** This file is part of the CVC4 prototype.
+  ** Major contributors: mdeters
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+  ** Minor contributors (to current version): none
- ** Courant Institute of Mathematical Sciences
+  ** This file is part of the CVC4 prototype.
- ** New York University
+  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
- ** See the file COPYING in the top-level source directory for licensing
+  ** Courant Institute of Mathematical Sciences
- ** information.
+  ** New York University
- **
+  ** See the file COPYING in the top-level source directory for licensing
- ** Implementation of equivalence class data for UF theory.  This is a
+  ** information.
- ** context-dependent object.
+  **
- **
+  ** Implementation of equivalence class data for UF theory.  This is a
- ** <span style="background-color:red;color:white;">Reviewed by Morgan Deters, Apr 4 2010 (bug #64).</span>
+  ** context-dependent object.
- **/
+  **
+  ** <span style="color:#a00;">Reviewed by dejan, Feb 24 2010 (bug #10).</span>
+  ** <span style="color:#a00;">Reviewed by mdeters, Apr 4 2010 (bug #64).</span>
+  **/
 </div>
 </li></ul></li>
@@ Line 911: / Line 1,256: @@
 *http://ispras.linux-foundation.org/index.php/ABI_compliance_checker_Downloads
 *http://tldp.org/HOWTO/Program-Library-HOWTO/shared-libraries.html
+=Working with the cluster=
+We have a cluster of nine execution hosts at NYU, ''smt_crunch_01''...''smt_crunch_09''.  You don't interact with these nodes directly; instead, you interact with church through the web or ssh interface.
+==Submitting a job to the cluster via the web interface==
+Build a fully statically-linked binary (usually with something like ''./configure production-cln-staticbinary'') and submit it via the [http://church.cims.nyu.edu/regress-results/cvc4.php web interface].
+==Submitting a job to the cluster via the command line==
+Some of us have been passing around scripts that run various cluster jobs.  The simplest form is:
+ #!/bin/bash
+ # cluster-regressions-cvc4
+ TO_EMAIL="`whoami`@cs.nyu.edu"
+ CC_EMAIL=""
+ function RunClusterRegressions() {
+   local job_name="cvc4-$1"
+   local cvc4_binary="$2"
+   local params="--segv-nospin $3"
+   local comment="$4"
+   local timeout="$5"
+   if [ -z "$timeout" ]; then
+     timeout=300;
+   fi
+   mysql -u smt_cluster --password=`cat ~/.mysql_password` smt_cluster <<EOF
+     insert into Jobs values(DEFAULT, "$job_name", "custom job:$comment", "22",\
+     "$timeout", "2000", "24", "$TO_EMAIL $CC_EMAIL", "2", "$cvc4_binary",\
+     "$params", "1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,29", \
+     DEFAULT);
+ EOF
+ }
+ if [ $# -ne 3 -a $# -ne 4 ]; then
+   echo "usage: $0 cvc4-binary \"solver params\" \"comment\" [timeout]"
+   exit 1
+ fi
+ JOB_TIME=`date +%s`
+ NAME="cluster-regressions-$JOB_TIME"
+ RunClusterRegressions "$NAME" $1 "$2" "$3" "$4"
+If this script is called ''cluster-regressions-cvc4'', you might run it like this:
+ ./cluster-regressions-cvc4 /full/path/to/cvc4/static/binary '--stats' 'running my crazy idea with stats enabled'
+which will run it on our standard regression suite for CVC4 with stats enabled and mail you the results.  The "22" in the SQL insert is the "runner"---this is the code for an "arbitrary tool with parameters", which a general, catch-all case that you will generally want to use.  The "24" is the problem set ID, which is (here) our set of CVC4 regressions.  You can also choose all of QF_LRA in SMT-LIBv1 (problem set ID 27), the same in SMT-LIBv2 (ID 28), all of QF_UF in SMT-LIBv2 (ID 38), all of QF_AX in SMT-LIBv2 (ID 39), all of QF_BV in SMT-LIBv2 (ID 40), and others.
+'''Note that you must have''' ''~/.mysql_password'' installed in your home directory.  See someone to get the password if you don't know it.
+==Adding benchmarks to the cluster==
+# If the benchmarks are new copy them to the appropriate directory on church /usr/local/share/benchmarks. Make sure they are owned by acsys-user and are readable by all users. All cluster nodes remotely mount the benchmark files from church, so there is no need to manually sync them (like was previously done). Lets say that your benchmarks are in /usr/local/share/benchmarks/mybench
+# Make a file to that contains all the benchmarks with for example 'find /usr/local/share/benchmarks/mybench -name "*.smt" > bench.txt'
+# Use the /cluster/cvc4/scripts/add_benchmarks.sh script to add the benchmarks. The is interactive and will ask you about all the necessary information. If you are adding problems to an existing problem set you will be given the option to continue running some existing jobs on the newly added benchmarks.
 =Unit testing=
@@ Line 918: / Line 1,319: @@
    http://cxxtest.tigris.org/files/documents/6421/43281/cxxtest-3.10.1.tar.gz
-Unpack it in, say, your home directory.  Then, just point CVC4's configure to it:
+Unpack it in, say, your home directory.  '''Make sure that the ''cxxtestgen.pl'' script has eXecute permission.'''  Then, just point CVC4's configure to it:
    ./configure --with-cxxtest-dir=~/cxxtest
@@ Line 1,097: / Line 1,498: @@
    $ make -C test/regress/regress2 check
+==Running the full regression suite on the cluster==
+Experimental CVC4 binaries can be submitted to the cluster for a full run of the regression suite  [http://church.cims.nyu.edu/regress-results/cvc4.php]. The test daemon will send you an email with a link to the results when the jobs is finished running.
+You may want to refer to [[#Working with the cluster|the section on working with the cluster (above)]].
+==Adding command line arguments to the regression tests==
+Use the CVC4_REGRESSION_ARGS flag on the commandline. For example,
+  make -j4 check CVC4_REGRESSION_ARGS="-d arith::consistency"
 =System testing=
@@ Line 1,115: / Line 1,526: @@
 Next, if you don't have an equivalent short option, add the appropriate item to the <code>OptionValue</code> enumeration.  If you '''do''' have an equivalent short option, append the short option to the string passed to <code>getopt_long()</code> in <code>parseOptions()</code>.  Your option character should be followed by a single colon if an argument is required, or two colons if an argument is optional.
-Next, modify the ''switch()'' construct in <code>parseOptions()</code> to handle your short option character (or the value from the <code>OptionValue</code> enumeration).  If you need a new field in the <code>CVC4::Options</code> structure, add it in <code>src/util/options.h</code>.
+Next, modify the ''switch()'' construct in <code>parseOptions()</code> to handle your short option character (or the value from the <code>OptionValue</code> enumeration).  If you need a new field in the <code>CVC4::Options</code> structure, add it in <code>src/smt/options.h</code>.
 Finally, change the usage string in <code>src/main/usage.h</code>.
@@ Line 1,124: / Line 1,535: @@
 =Attributes=
+Attributes are roughly speaking [almost] global hash tables from Nodes (TNodes) to data.  Attributes can be thought of as additional fields used to extend NodeValues.  Attributes are mutable, and come in both sat context-dependent and non-context dependent varieties.  Attributes live only as long as the node itself does.  If a Node is garbage-collected Attribute's associated with it will automatically be garbage collected.   (Being in the domain of an Attribute does not increase a Node's reference count.)  To achieve this special relationship with Nodes, Attributes are mapped by hash tables (AttrHash<> and CDAttrHash<>) that live in the AttributeManager. The AttributeManager is owned by the NodeManager.  The following types are currently allowed:
+* bool
+* uint64_t
+* TNode
+* Node
+* std::string
+* T*
+To get the value of an Attribute InstLevelAttribute on a Node n, use
+    n.getAttribute(InstLevelAttribute())
+==Declaring Attributes==
+Attributes tend to be defined in a fixed pattern:
+    struct InstLevelAttributeId {};
+    typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
+To separate Attributes of the same type in the same table each of the structures struct InstLevelAttributeId {}; is given a different unique value at '''load time'''.  An example is the empty struct InstLevelAttributeId. These should be unique for each Attribute. Then via some template messiness when InstLevelAttribute() is passed as the argument to getAttribute(...) the load time id is instantiated. (To get the work done, the ID structs these just need to be different for each AttrHash. But if you do not use unique ones, we won't accept this into trunk!)
+More complicated T* data-structures may require a clean up strategy.  By default, NullCleanupStrategy is used where nothing happens. This allows for <code>delete</code> to be called on a pointer data-structure for example.  Formally, the full specification of an attribute is:
+   expr::Attribute< Id, value_type, CleanupStrategy, Context-Dependent>
+* Id is a compiler object to determine the load time id (normally a unique empty struct)
+* value_type is the domain type of the Attribute (bool, T*, ...)
+* CleanupStrategy specifies how value_types need to be garbage collected when removed
+* Context-Dependent is a bool that if true means the attribute is context-dependent and is false otherwise.
+As a convenience, you can also define context dependent attributes without a cleanup strategy using
+  struct CDAttribute<class T, value_type>
+Here is a declaration that makes full use of every parameter:
+  // Attribute that tell if a node have been asserted in this branch
+  struct AvailableInTermDbId {};
+  /** use the special for boolean flag */
+  typedef expr::Attribute<AvailableInTermDbId,
+                        bool,
+                        expr::attr::NullCleanupStrategy,
+                        true  // context dependent
+                        > AvailableInTermDb;
+==Attribute Internals==
+To map to more complicated data-structures T, use pointers T* as the domain type of the attribute. These are then handled as void* internally by the Attribute system. The following hash maps are defined:
+* AttrHash<bool> d_bools;
+* AttrHash<uint64_t> d_ints;
+* AttrHash<TNode> d_tnodes;
+* AttrHash<Node> d_nodes;
+* AttrHash<TypeNode> d_types;
+* AttrHash<std::string> d_strings;
+* AttrHash<void*> d_ptrs;
+* CDAttrHash<bool> d_cdbools;
+* CDAttrHash<uint64_t> d_cdints;
+* CDAttrHash<TNode> d_cdtnodes;
+* CDAttrHash<Node> d_cdnodes;
+* CDAttrHash<std::string> d_cdstrings;
+* CDAttrHash<void*> d_cdptrs;
+In principle, though user context level context dependent attributes are not currently supported, these can be added without too much difficulty.
+To dig into details, take a look at expr/{attribute.h, attribute_internals.h, attribute.cpp, node_manager.h, node_manager.cpp}
+==Common Attribute Errors==
+Like other maps, Node valued Attributes can cause circular references. These will not be detected by the garbage collector.
 What does this mean?
-<pre>
+<code>
 /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
-</pre>
+</code>
 It means that the Attribute value-type (in this case ''FooBar''), is invalid; there's no hashtable of appropriate kind to put it in.  You probably want FooBar*.
@@ Line 1,151: / Line 1,638: @@
 <ol>
-<li>Go to the ANTLR3 page and download Complete ANTLR 3.2 jar; all tools, runtime, etc... <http://antlr.org/download/antlr-3.2.jar> to <code>$ANTLR3_JAR</code>.</li>
+<li>Go to the ANTLR3 page and download Complete ANTLR 3.4 jar from http://antlr3.org/download/antlr-3.4-complete.jar.</li>
-<li>Save the following as <code>$ANTLR3_DIR/antlr3</code>, substituting the correct fully-qualified path for "<code>$ANTLR3_JAR</code>":
+<li>Make a directory <code>$ANTLR3_DIR</code>.</li>
+<li>Save the following shell script file in the <code>$ANTLR3_DIR</code> directory (make sure the file is executable), substituting the correct fully-qualified path for "<code>$ANTLR3_JAR</code>":
 <pre>
-#!/bin/sh
+#!/bin/bash
-export CLASSPATH=/usr/share/java/stringtemplate.jar:$ANTLR3_JAR
+export CLASSPATH=$ANTLR3_JAR
 exec java org.antlr.Tool "$@"
 </pre></li>
-<li>Open <code>/path/to/antlr3executable/antlr3</code> in your favorite text editor and change the 3rd line to:
+<li>Now, you are done with installing Antlr3.</li>
-<pre>
+<li>Download "libantlr3c-3.4.tar.gz" from http://antlr3.org/download/C and extract the archive. You now have an extracted src directory called "libantlr3c-3.4".</li>
-export CLASSPATH=/usr/share/java/stringtemplate.jar:/path/to/antr3jar/antlr-3.2.jar
+<li>Make a directory <code>$LIBANTLR3C_INSTALL_DIR</code>.</li>
-</pre></li>
+<li>Enter the src directory.</li>
-<li>Download "libantlr3c-3.2.tar.gz" from http://antlr.org/download/C and extract the archive to <code>LIBANTLR3C_SRC_DIR</code>.</li>
-<li>Enter <code>$LIBANTLR3C_SRC_DIR</code>.</li>
 <li>If you are on a 32-bit machine, run
 <pre>
-./configure --prefix=$LIBANTLR3C_INSTALL_DIR
+./configure --disable-antlrdebug --prefix=$LIBANTLR3C_INSTALL_DIR
 </pre>
 If you are on a 64 bit machine, run
 <pre>
-./configure --prefix=$LIBANTLR3C_INSTALL_DIR --enable-64bit
+./configure --enable-64bit --disable-antlrdebug --prefix=$LIBANTLR3C_INSTALL_DIR
 </pre>
 <code>--prefix=PREFIX</code> specifies the library installation directory. This defaults to <code>/usr/local</code>.</li>
-<li> Open up the Makefile that's generated at the top-level source directory and add <code>-fexceptions</code> to the CFLAGS setting. </li>
+<li> Open up the Makefile that is generated at the top-level source directory and add <code>-fexceptions</code> to the CFLAGS setting. </li>
+<li> If you're on Solaris, you may need to change the Makefile to add "<code>-lnsl -lsocket</code>" to the <code>libantlr3c_la_LDFLAGS</code> definition.
 <li> Run
 <pre>
@@ Line 1,198: / Line 1,685: @@
 </pre>
 </li>
-<li> <code>cd</code> to the CVC4 source tree. </li>
+<li> <code>cd</code> to the CVC4 source tree</li>
 <li>Now run
+<pre>
+./autogen.sh
+</pre>
+and
 <pre>
 ./configure --with-antlr-dir=$LIBANTLR3_INSTALL_DIR ANTLR=$ANTLR3_DIR/antlr3"
 </pre>
+, where <code>$LIBANTLR3_INSTALL_DIR</code> is the path of the library installation directory, and <code>$ANTLR3_DIR/antlr3</code> is the path of the shell script you made.
 </li>
 </ol>
+If you are still having problems trying to configure antlr3 with cvc4, take a look at
+<pre>cvc4/builds/$ARCH/$BUILD_MODE/config.log</pre>
+and double check that your architecture is is 32 versus 64bit:
+<pre>
+$ 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
+</pre>
+For systems that mix 32 bit and 64 bit libraries, you need to make sure that the ELF classes of the libraries being linked agree with each other. For example if gmp is 32 bit and libantlr3c is 64 bit, you are likely to get an ELFCLASS64 error at configure time.  To determine if this is the case, search through the appropriate config.log file, e.g.:
+  builds/x86_64-unknown-linux-gnu/default/config.log
+== Adding theory support to the parser ==
+To add support for a new theory to the SMT parser, you will need to edit <code>src/parser/smt1/Smt1.g</code>:
+<ol>
+<li> Add any new operators to the list of operator tokens near the end of file (look for <code>AND_TOK</code>, etc).
+<li> Add the new operator as an alternative in the rule <code>builtinOp</code>, mapping it to its corresponding CVC4 <code>Kind</code>.
+<li> Add the rules to match new constant tokens near the end of the file (look for <code>NUMERAL_TOK</code>, etc).
+<li>Add the new constants as alternatives in the rule <code>annotatedFormula</code>, decoding the token text and calling <code>MK_CONST</code> (which is just a macro that calls <code>ExprManager::mkConst</code>). NOTE: if you have a constant token type <code>MY_CONST_TOK</code>, you can get a <code>std::string</code> representing the matched input using the static method <code>AntlrInput::tokenText</code>, e.g.,
+<pre>  // annotatedFormula alternatives ...
+  | MY_CONST_TOK
+    { std::string myConstText = AntlrInput::tokenText($MY_CONST_TOK);
+      MyConstType c = ...;
+      expr = MK_CONST(c); }
+</pre>
+</li>
+</ol>
+== Building a 32-bit binary on a 64-bit machine ==
+(These instructions are for Debian/Ubuntu)
+First, make sure you have the 32-bit library dependencies installed
+    sudo apt-get install libc6-dev-i386 g++-multilib lib32gmpxx4 lib32gmp3 lib32gmp3-dev
+You will also need to build a 32-bit version of the ANTLR library. Just configure the library with <code>--disable-64bit</code>. [I found that I had to first configure and build with <code>--enable-64bit</code>, then reconfigure and build with <code>--disable-64bit</code> to get it to work. -Chris]
+Configure CVC4 with <code>CFLAGS=-m32 CXXFLAGS=-m32</code> and build as usual.
+=Working with Contexts=
+Contexts are a particularly complicated part of the machinery of CVC4, and much of CVC4's work hinges on them.
+The class "Context" is an abstraction for a rollback-able memory.  One can create a ''Context'':
+  Context c;
+and some objects in it (use the ''CDO<>'' wrapper to make a simple, rollback-able object, using a pointer to the ''Context'' as the constructor argument):
+  CDO<int> i(&c);
+  CDO<int> j(&c);
+  i = 4;
+  j = 3;
+One then "pushes a scope" on the ''Context'':
+  c.push();
+Further edits to ''i'' and ''j'' are then rolled back with ''pop()'':
+  i = 10000;
+  j = -5;
+  assert(i == 10000 && j == -5); // succeeds
+  c.pop();
+  assert(i == 4 && j == 3); // also succeeds
+Types wrapped by ''CDO<>'' simply employ a ''copy-on-write'' policy if the current scope is greater than that in which the object was last updated.  Rollbacks are eager (when ''pop()'' is called).  ''CDO<>'' just uses the underlying type's copy constructor.  Sometimes you want something more involved, in which case you write your own class that extends the class ''ContextObj'' and provides save and restore functionality.  Make sure to [http://church.cims.nyu.edu/cvc4-builds/documentation/latest/classCVC4_1_1context_1_1ContextObj.html#_details read the invariants in ''context.h'' carefully]!
+==Gotchas==
+Here are some important ''gotchas'' to keep in mind:
+# Your ''ContextObj'' subclass '''must''' call ''destroy()'' from its destructor.  This ensures that, if prematurely destructed (that is, before the Context goes away), your object is properly unregistered from the ''Context''.
+# Be careful if you allocate in an alternative memory manager (see [[#Using ContextObj that aren't allocated in usual heap memory|below]]).
+# FIXME add more gotchas
+==Using ContextObj that aren't allocated in usual heap memory==
+You need to be careful; even at a high scope level, all objects registered for backtracking with a Context are inserted at scope zero.  ''This means your program will crash if you delete the associated memory too soon.''  Now re-read that sentence.  If you create a ''CDO<int>'' (with '''new''') at scope level 10, and delete it upon backtracking to scope level 9, the ''CDO<int>'' destructor properly unregisters itself from the ''Context''.  However, if you allocate it in a memory manager (such as the ''ContextMemoryManager'') that doesn't guarantee that the destructor is called, your program will crash (perhaps much later), because the object is still registered at scope level 0 (and thus a bad pointer appears on a list).  You may prefer to create a ''CDO<int*>'' rather than a ''CDO<int>*'', which solves the issue (you can prematurely delete the ''int*'' without incident).  But that may leak memory, so there are additional constructors in ''ContextObj'' and ''CDO<>'' (those starting with a ''bool'' argument) that specifically "register" the object at the current scope level.  They aren't registered at scope level 0, so the problem doesn't occur.  However, you have to be careful.
+But why allocate ''ContextObj'' instances with the ''ContextMemoryManager'' if it's so complicated?  There's a big advantage: you don't have to track the lifetime of the ''ContextObj''.  The object simply ceases to exist when the ''Context'' is popped.  Thus you can create an object in context memory, and if you stow pointers to it only in context memory as well, all is cleaned up for you when the scope pops.  Here's a list of ''gotchas'':
+# For data structures intended solely to be allocated in context memory, privately declare (but don't define) an operator ''new(size_t)'' and destructor (as currently in the ''Link'' class, in ''src/theory/uf/tim/ecdata.h'').
+# For data structures that may or may not be allocated in context memory, and are designed to be that way (especially if they contain ''ContextObj'' instances), they should be heavily documented---especially the destructor, since it ''may or may not be called''.
+# There's also an issue for generic code---some class ''Foo<T>'' might be allocated in context memory, and that might normally be fine, but if ''T'' is a ''ContextObj'' this requires certain care.
+# Note that certain care is required for ''ContextObj'' inside of data structures.  If the (enclosing) data structure can be allocated in ''ContextMemoryManager'' ("CMM"), that means the (enclosed) ''ContextObj'' can be, even if it was not designed to be allocated in that way.  In many instances, it may be required that data structures enclosing ''ContextObj'' be parameterized with a similar "''bool allocatedInCMM''" argument as the special constructor in this class (and pass it on to all ''ContextObj'' instances).

Difference between revisions of "Developer's Guide"

Latest revision as of 09:10, 21 August 2017

Contents

Source tree layout

Building CVC4

Dependencies

Building

Building on Mac OS X

Building language bindings

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

kinds files

Make Verbose

Preparing Binaries for Starexec

Profiling the code

prof, gprof, valgrind, callgrind

Google performance tools

Using ASAN

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

Node comparisons

Use of autotools: automake, autoconf, autoheader, libtool

Commit policy

Unit tests with CxxTest