View source for How to write a theory in CVC4

From CVC4

You do not have permission to edit this page, for the following reason:

The action you have requested is limited to users in the group: Users.

You can view and copy the source of this page.

[[How to write a theory in CVC4 (old instructions)|The old instructions can be found here.]]

This page is under construction.

This page is intended as a reference guide.  Tutorials will be added later...

=Infrastructure=

new-theory script...

=Theory class=

''Liana, please add content here..''


=Documenting Creation of <tt>sets</tt> theory=
''For rough making rough notes on steps followed, hurdles etc -- may or may not be later used to improve this page. [[User:Kshitij|Kshitij]] 22:05, 4 September 2013 (UTC)''

0. [not related to theory creation, could skip to next step] Start afresh, create a branch 
  mkdir kbansal.CVC4.set; cd kbansal.CVC4.set
  git clone https://github.com/kbansal/CVC4 ./
  git branch sets
  git checkout sets
  # usual configure, build etc.
  ./autogen.sh
  ./contrib/get-antlr-3.4
  <run configure command as given by previous script>

1. Creating basic infrastructural files. Use the contrib/new-theory script:
  ./contrib/new-theory sets
  # Previous command calls autogen, but still need to call:
  ./configure     #with any other options, like for specifying antlr
  make
For the record, this was the output of new-theory script (which tells what all it did)

<pre>
Theory of sets
Theory directory: src/theory/sets
Theory id: THEORY_SETS
Theory class: CVC4::theory::sets::TheorySets

Creating src/theory/sets/kinds...
Creating src/theory/sets/Makefile...
Creating src/theory/sets/Makefile.am...
Creating src/theory/sets/options...
Creating src/theory/sets/options_handlers.h...
Creating src/theory/sets/README.WHATS-NEXT...
Creating src/theory/sets/theory_sets.cpp...
Creating src/theory/sets/theory_sets.h...
Creating src/theory/sets/theory_sets_rewriter.h...
Creating src/theory/sets/theory_sets_type_rules.h...

Adding sets to SUBDIRS to src/theory/Makefile.am...
Adding libsets.la to LIBADD to src/theory/Makefile.am...
Adding ../theory/sets/options.cpp to OPTIONS_FILES_SRCS
  and nodist_liboptions_la_SOURCES to src/options/Makefile.am...

Rerunning autogen.sh...
Preparing the cvc4 build system...please wait

Found GNU Autoconf version 2.68
Found GNU Automake version 1.11.3
Found GNU Libtool version 2.4.2

Automatically preparing build ... done

The cvc4 build system is now prepared.  To build here, run:
  ./configure
  make
</pre>

2. Read (as in ''red'') <code>src/theory/sets/README.WHATS-NEXT</code> ''Comment: though that is is within so many other files/lines of output that not necessarily reliable someone would read that -- I just happened to notice it while documenting :)''

Return to How to write a theory in CVC4.

Retrieved from "http://cvc4.cs.stanford.edu/wiki/How_to_write_a_theory_in_CVC4"

View source for How to write a theory in CVC4

Navigation menu

Views

Personal tools

CVC4

For CVC4 Developers

Cascade

Meta

Wiki

Search

Tools