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

$ 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

 $ 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

@@ Line 756: / Line 756: @@
 [http://cxxtest.sourceforge.net/guide.html The users' guide is here for your reference.]
-==Debugging Unit Tests==
+==Debugging unit tests==
 In order to run, CxxTest takes a header file, generates from that a new cpp file, and then then compiles the cpp file into a binary.

Difference between revisions of "Developer's Guide"

Revision as of 14:23, 4 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

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

Regression testing

Multi-level regression testing

System testing

Command-line options

NodeBuilders

Attributes

Navigation menu

Search