Revision as of 07:20, 11 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 now 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 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)

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 in src/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.
• 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:

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 SETMINUS 2 "set subtraction"
operator SUBSET 2 "subset"
operator IN 2 "set membership"

endtheory

4. Jumping to parsing step in README (will get to type rules, re-writer later). As a first step, I only support smtlib2. This required changes in src/parser/smt2/Smt2.g. Again, I just looked for what all was going on for bitvectors and also for arrays; and was able to figure out the rest.

• (a) Defined tokens for new operators for the theory (union, subset etc). Patch:

--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1567,6 +1578,12 @@ BVSLE_TOK : 'bvsle';
 BVSGT_TOK : 'bvsgt';
 BVSGE_TOK : 'bvsge';
 
+SETUNION_TOK: 'union';
+SETINT_TOK: 'intersection';
+SETMINUS_TOK: 'setminus';
+SETSUB_TOK: 'subset';
+SETIN_TOK: 'in';
+
 /**
  * A sequence of printable ASCII characters (except backslash) that starts
  * and ends with | and does not otherwise contain |.

• (b) Translated these tokens into corresponding kinds I created in step 3.

--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1210,6 +1210,12 @@ builtinOp[CVC4::Kind& kind]
   | BVSGT_TOK     { $kind = CVC4::kind::BITVECTOR_SGT; }
   | BVSGE_TOK     { $kind = CVC4::kind::BITVECTOR_SGE; }
 
+  | SETUNION_TOK  { $kind = CVC4::kind::UNION; }
+  | SETINT_TOK    { $kind = CVC4::kind::INTERSECTION; }
+  | SETMINUS_TOK  { $kind = CVC4::kind::SETMINUS; }
+  | SETSUB_TOK    { $kind = CVC4::kind::SUBSET; }
+  | SETIN_TOK     { $kind = CVC4::kind::IN; }
+
   // NOTE: Theory operators go here
   ;
 

• (c) In addition, I added a sort symbol Set 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)

--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1318,6 +1324,11 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
           PARSER_STATE->parseError("Illegal array type.");
         }
         t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
+      } else if(name == "Set") {
+        if(args.size() != 1) {
+          PARSER_STATE->parseError("Illegal set type.");
+        }
+        t = EXPR_MANAGER->mkSetType( args[0] );
       } else if(check == CHECK_DECLARED ||
                 PARSER_STATE->isDeclared(name, SYM_SORT)) {
         t = PARSER_STATE->getSort(name, args);

• (d) As you see in the substep (c), we call EXPR_MANAGER->mkSetType 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):

SetType ExprManager::mkSetType(Type elementType) const
TypeNode NodeManager::mkSetType(TypeNode elementType)
bool Type::isSet() const
class CVC4_PUBLIC SetType : public Type {
  SetType(const Type& type = Type())
  Type getElementType() const;
}
bool TypeNode::isSet() const
TypeNode TypeNode::getSetElementType() const

5. Printer was simpler. Also, even without these changes it would print the internal representation in any case -- so not such an urgent step in initial stages. Here is the patch:

--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -316,6 +316,14 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     stillNeedToPrintParams = false;
     break;
 
+    // sets
+  case kind::UNION:
+  case kind::INTERSECTION:
+  case kind::SETMINUS:
+  case kind::IN:
+  case kind::SET_TYPE: out << smtKindString(k) << " "; break;
+
     // datatypes
   case kind::APPLY_TYPE_ASCRIPTION: {
       out << "as ";
@@ -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";
   case kind::BITVECTOR_ROTATE_RIGHT: return "rotate_right";
+
+  case kind::UNION: return "union";
+  case kind::INTERSECTION: return "intersection";
+  case kind::SETMINUS: return "setminus";
+  case kind::SUBSET: return "subset";
+  case kind::IN: return "in";
+  case kind::SET_TYPE: return "Set";
   default:
     ; /* fall through */
   }

6. At this stage, there seemed to be enough infrastructure to start testing more directly to figure out next steps.

• (a) I used the following example (actually, to be precise, I used this example to iron out various issues in step 4 and 5 too.)

(set-logic ALL_SUPPORTED)
(declare-fun a () (Set Int))
(declare-fun b () (Set Int))
(declare-fun c () (Set Int))
(assert (= c (union a b) ))
(check-sat)

• (b) What happened trying to run this?

kshitij@church~/cvc/kbansal.CVC4.set (sets)$ builds/bin/cvc4 -v -v -v sets-sample.smt2 
Invoking: (set-logic ALL_SUPPORTED)
Invoking: (declare-fun a () (Set Int))
Invoking: (declare-fun b () (Set Int))
Invoking: (declare-fun c () (Set Int))
Invoking: (assert (= c (union a b)))
CVC4 threw an "unexpected" exception.
terminate called after throwing an instance of 'CVC4::UnhandledCaseException'
  what():  Unhandled case encountered
static CVC4::TypeNode CVC4::expr::TypeChecker::computeType(CVC4::NodeManager*, CVC4::TNode, bool)
/home/kshitij/cvc/kbansal.CVC4.set/builds/x86_64-unknown-linux-gnu/default/../../../src/expr/type_checker_template.cpp:52
The case was: UNION
Aborted (core dumped)
kshitij@church~/cvc/kbansal.CVC4.set (sets)$ 

Excellent! So we go to a step we skipped in the README: add typing rules to theory_sets_type_rules.h for your operators and constants. Note that I used a debug build (specified at configure time).

7. To wrap up: type rules, avoiding going down rewriter and dummy implementation of check-sat to do a syntactic-level check of basic infrastructure.

• (a) Here is what the patch for the typerule for union looked like (others to be similarly done)

--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -27,4 +27,6 @@ operator SETMINUS 2 "set subtraction"
 operator SUBSET 2 "subset"
 operator IN 2 "set membership"
 
+typerule UNION ::CVC4::theory::sets::SetUnionTypeRule
+
 endtheory
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -28,6 +28,26 @@ public:
 
 };/* class SetsTypeRule */
 
+struct SetUnionTypeRule {
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+    throw (TypeCheckingExceptionPrivate, AssertionException) {
+    Assert(n.getKind() == kind::UNION);
+    TypeNode setType = n[0].getType(check);
+    if( check ) {
+      if(!setType.isSet()) {
+        throw TypeCheckingExceptionPrivate(n, "set union operating on non-set");
+      }
+      TypeNode secondSetType = n[1].getType(check);
+      if(secondSetType != setType) {
+        throw TypeCheckingExceptionPrivate(n, "set union operating on sets of different types");
+      }
+    }
+    return setType;
+  }
+};/* struct SetUnionTypeRule */
+
+
+
 struct SetsProperties {
   inline static Cardinality computeCardinality(TypeNode type) {
     Assert(type.getKind() == kind::SET_TYPE);

• (b) Without the rewriter, running cvc4 with default options gave an assertion failure. To get around this, I used the --no-simplification command line option which makes sure the rewriter code doesn't get called. (For the record, the failed assertion was at src/smt/smt_engine.cpp:1783 : Rewriter::rewrite(d_topLevelSubstitutions.apply(learnedLiteral)).isConst())
• (c) A dummy implementation of the theory, which always says Satisfiable.

--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -17,6 +17,7 @@ TheorySets::TheorySets(context::Context* c,
 }/* TheorySets::TheorySets() */
 
 void TheorySets::check(Effort level) {
+  return;
 
   while(!done()) {
     // Get all the assertions

• (d) End result of everything in this document -- a "complete" (though slightly unsound) new theory!

kshitij@church~/cvc/kbansal.CVC4.set (sets)$ builds/bin/cvc4 -v -v -v sets-sample.smt2  --no-simplification
Invoking: (set-logic ALL_SUPPORTED)
Invoking: (declare-fun a () (Set Int))
Invoking: (declare-fun b () (Set Int))
Invoking: (declare-fun c () (Set Int))
Invoking: (assert (= c (union a b)))
Invoking: (push 1)
(assert true)
(check-sat)
(pop 1)
[...snipped...]
sat
kshitij@church~/cvc/kbansal.CVC4.set (sets)$