Difference between revisions of "How to write a theory in CVC4"
(→Documenting Creation of sets theory) |
(→Documenting Creation of sets theory: trying to define kinds file) |
||
| Line 71: | Line 71: | ||
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 :)'' | 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 :)'' | ||
| + | |||
| + | 3. From README.WHATS-NEXT, trying "to specify theory constants, types, and operators in your \`kinds' file" | ||
| + | *3(a). Read <code>src/theory/built-in/kinds</code>. Observed some basic things are already filled-in in <code>src/theory/sets/kinds</code> | ||
| + | *3(b). Looked at <tt>arith</tt> kinds file. Looked at <tt>array</tt> kinds file -- seems to be closer to what we want since its sort is also parametrized. | ||
| + | *3(c). Defined <tt>SET_TYPE</tt> using the <tt>operator</tt> keyword... hope I got that right since what I want is a (parameterized) sort. In arith, REAL_TYPE is defined using the <tt>sort</tt> keyword, that would seem to be natural choice here too. | ||
Revision as of 08:37, 9 September 2013
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 sets theory
For rough making rough notes on steps followed, hurdles etc -- may or may not be later used to improve this page. 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)
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
2. Read (as in red) src/theory/sets/README.WHATS-NEXT 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 :)
3. From README.WHATS-NEXT, trying "to specify theory constants, types, and operators in your \`kinds' file"
- 3(a). Read
src/theory/built-in/kinds. Observed some basic things are already filled-in insrc/theory/sets/kinds - 3(b). Looked at arith kinds file. Looked at array kinds file -- seems to be closer to what we want since its sort is also parametrized.
- 3(c). Defined SET_TYPE using the operator keyword... hope I got that right since what I want is a (parameterized) sort. In arith, REAL_TYPE is defined using the sort keyword, that would seem to be natural choice here too.
