Difference between revisions of "Developer's Guide"

smooth over

 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

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

 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");
 }

 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

 $ 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

For the ANTLR3 neophytes amongst us, here are the steps Chris led me through
to get CVC4 to compile with this new ANTLR3 stuff:

1. 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 /path/to/antr3jar/
2. Download the attachment to Chris's email "antlr3" to /path/to/antlr3executable/
3. Open /path/to/antlr3executable/antlr3 in your favorite text editor and change the 3rd line to
   "export CLASSPATH=/usr/share/java/stringtemplate.jar:/path/to/antr3jar/antlr-3.2.jar"
4. Download "libantlr3c-3.2.tar.gz" from http://antlr.org/download/C and extract the archive to /path/to/libantr/src/
5. Enter /path/to/libantr/src/
6. If you are on a 32-bit machine, run "./configure --prefix=/path/to/libantlr3c/installation".
    If you are on a 64 bit machine, run "./configure --prefix=/path/to/libantlr3c/installation --enable-64bit".
    --prefix=PREFIX specifies the library installation directory. This defaults to "/usr/local"
7. make
8. [sudo] make install
9. cd /path/to/cvc4
10. Now run "./configure --with-antlr-dir=/path/to/libantlr3c/installation
ANTLR3=/path/to/antlr3executable/antlr3"

--Tim

Difference between revisions of "Developer's Guide"

Revision as of 20:57, 30 March 2010

Contents

Source tree layout

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

Coding guidelines

File and directory names

Preprocessor macros

Binary macros

Block macros

Miscellaneous

Class names

Namespaces

Member names

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

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

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

Unit testing

Running unit tests

Types of unit tests

Adding unit tests

Test implementations

Debugging unit tests

Test rebuilding

Partial testing

Marking the test tree up-to-date (not preferred)

Regression testing

Multi-level regression testing

System testing

Command-line options

NodeBuilders

Attributes

ANTLR3

Navigation menu

Search