How to write a theory in CVC4 - Revision history

Kshitij: /* Documenting Creation of sets theory */

2013-09-11T15:23:58Z

‎Documenting Creation of sets theory

Kshitij: /* Documenting Creation of sets theory */ typo

2013-09-11T15:20:20Z

‎Documenting Creation of sets theory: typo

Kshitij: /* Documenting Creation of sets theory */ wrap-up

2013-09-11T01:53:23Z

‎Documenting Creation of sets theory: wrap-up

Kshitij: /* Documenting Creation of sets theory */ prvs change msg should had been "printer". this one is "create an example to test"

2013-09-10T23:13:43Z

‎Documenting Creation of sets theory: prvs change msg should had been "printer". this one is "create an example to test"

Kshitij: /* Documenting Creation of sets theory */

2013-09-10T22:57:59Z

‎Documenting Creation of sets theory

Kshitij: /* Documenting Creation of sets theory */ Creating the parser

2013-09-10T22:43:13Z

‎Documenting Creation of sets theory: Creating the parser

Kshitij: /* Documenting Creation of sets theory */ trying to define kinds file

2013-09-09T16:56:22Z

‎Documenting Creation of sets theory: trying to define kinds file

Kshitij: /* Documenting Creation of sets theory */ trying to define kinds file

2013-09-09T16:37:45Z

‎Documenting Creation of sets theory: trying to define kinds file

Kshitij: /* Documenting Creation of sets theory */

2013-09-04T22:10:20Z

‎Documenting Creation of sets theory

Kshitij: sets, steps 1 and 2

2013-09-04T22:05:21Z

sets, steps 1 and 2

@@ Line 70: / Line 70: @@
 </pre>
-. 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 :)''
+. Read (as in ''red'') <code>src/theory/sets/README.WHATS-NEXT</code> ''Comment: The readme lies in the obvious place and has a name shouting to be read next, but could also be highlighted (e.g. at end of script).''
 . From README.WHATS-NEXT, trying "to specify theory constants, types, and operators in your \`kinds' file"

@@ Line 140: / Line 140: @@
 </pre>
-*(c) In addition, I added a sort symbol <code>Array</code> which eventually got translated to SET_TYPE "operator" defined in kinds file. (this would look different for non-parametrized sorts, both here and step 3)
+*(c) In addition, I added a sort symbol <code>Set</code> which eventually got translated to SET_TYPE "operator" defined in kinds file. (this would look different for non-parametrized sorts, both here and step 3)
 <pre>
 --- a/src/parser/smt2/Smt2.g

@@ Line 15: / Line 15: @@
 =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)''
+''For now 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)''
 . [not related to theory creation, could skip to next step] Start afresh, create a branch
@@ Line 30: / Line 30: @@
    ./contrib/new-theory sets
    # Previous command calls autogen, but still need to call:
-   ./configure     #with any other options, like for specifying antlr
+   ./configure   #with any other options, like using a 'debug' configuration and specifying antlr.
    make
 For the record, this was the output of new-theory script (which tells what all it did)
@@ Line 230: / Line 230: @@
 </pre>
 Excellent! So we go to a step we skipped in the README: <code>add typing rules to theory_sets_type_rules.h for your operators and constants</code>. Note that I used a <tt>debug</tt> build (specified at configure time).

@@ Line 173: / Line 173: @@
 --- a/src/printer/smt2/smt2_printer.cpp
 +++ b/src/printer/smt2/smt2_printer.cpp
-@@ -316,6 +316,13 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
+@@ -316,6 +316,14 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       stillNeedToPrintParams = false;
       break;
@@ Line 181: / Line 181: @@
 +  case kind::INTERSECTION:
 +  case kind::SETMINUS:
-+  case kind::SUBSET:
++  case kind::IN:
-+  case kind::IN: out << smtKindString(k) << " "; break;
++  case kind::SET_TYPE: out << smtKindString(k) << " "; break;
++
       // datatypes
     case kind::APPLY_TYPE_ASCRIPTION: {
         out << "as ";
-@@ -499,6 +506,13 @@ static string smtKindString(Kind k) throw() {
+@@ -499,6 +507,13 @@ static string smtKindString(Kind k) throw() {
     case kind::BITVECTOR_SIGN_EXTEND: return "sign_extend";
     case kind::BITVECTOR_ROTATE_LEFT: return "rotate_left";
@@ Line 202: / Line 202: @@
+    }
 </pre>

@@ Line 157: / Line 157: @@
           t = PARSER_STATE->getSort(name, args);
 </pre>
-*(d) As you see in the previous step, we call <code>EXPR_MANAGER->mkSetType</code> which eventually leads to a node of kind SET_TYPE with appropriate parameter. This needed us to create a bunch of functions, instead of the full patch I just list the functions added (though it was mostly straight forward, it took some time as it is spread across files and needed some grep/compile error cycles):
+*(d) As you see in the substep (c), we call <code>EXPR_MANAGER->mkSetType</code> which eventually leads to a node of kind SET_TYPE with appropriate parameter. This needed us to create a bunch of functions, instead of the full patch I just list the functions added (though it was mostly straight forward, it took some time as it is spread across files and needed some grep/compile error cycles):
 <pre>
 SetType ExprManager::mkSetType(Type elementType) const
@@ Line 168: / Line 168: @@
 bool TypeNode::isSet() const
 TypeNode TypeNode::getSetElementType() const
 </pre>

@@ Line 97: / Line 97: @@
 operator UNION 2 "set union"
 operator INTERSECTION 2 "set intersection"
-operator SET_MINUS 2 "set subtraction"
+operator SETMINUS 2 "set subtraction"
 operator SUBSET 2 "subset"
 operator IN 2 "set membership"
 endtheory
 </pre>

← Older revision		Revision as of 16:56, 9 September 2013
Line 76:		Line 76:
	*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(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.		*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.
		+	*3(d). Defined bunch of operators. Things seem to compile fine for the moment, no type-checking going on at the moment -- moving ahead with README for now and will come back to kinds file later. For now, the kinds file looks like this:
		+	<pre>
		+	theory THEORY_SETS ::CVC4::theory::sets::TheorySets "theory/sets/theory_sets.h"
		+	typechecker "theory/sets/theory_sets_type_rules.h"
		+	rewriter ::CVC4::theory::sets::TheorySetsRewriter "theory/sets/theory_sets_rewriter.h"
		+
		+	properties check
		+
		+	# Theory content goes here.
		+
		+	# constants...
		+
		+	# types...
		+	operator SET_TYPE 1 "set type" # the type
		+	cardinality SET_TYPE \
		+	"::CVC4::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
		+	"theory/sets/theory_sets_type_rules.h"
		+
		+	# operators...
		+	operator UNION 2 "set union"
		+	operator INTERSECTION 2 "set intersection"
		+	operator SET_MINUS 2 "set subtraction"
		+	operator SUBSET 2 "subset"
		+	operator IN 2 "set membership"
		+
		+	endtheory
		+	</pre>

← Older revision		Revision as of 16:37, 9 September 2013
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.

← Older revision		Revision as of 22:10, 4 September 2013
Line 69:		Line 69:
	make		make
	</pre>		</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 :)''

← Older revision		Revision as of 22:05, 4 September 2013
Line 12:		Line 12:

	''Liana, please add content here..''		''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>