initial code

emina · May 29, 2018 · 2619109 · 2619109
1 parent 6e80244
commit 2619109
Show file tree

Hide file tree

Showing 30 changed files with 2,241 additions and 861 deletions.
diff --git a/examples/kodkod/examples/alloyinecore/TheoryOfList.java b/examples/kodkod/examples/alloyinecore/TheoryOfList.java
@@ -0,0 +1,265 @@
+package kodkod.examples.alloyinecore;
+
+import kodkod.ast.Formula;
+import kodkod.ast.Relation;
+import kodkod.ast.Variable;
+import kodkod.engine.Solution;
+import kodkod.engine.Solver;
+import kodkod.engine.satlab.SATFactory;
+import kodkod.instance.Bounds;
+import kodkod.instance.TupleFactory;
+import kodkod.instance.Universe;
+
+import java.util.ArrayList;
+import java.util.List;
+
+final class TheoryOfList {
+
+    public static void main(String[] args) {
+        TheoryOfList theoryOfList = new TheoryOfList();
+        System.out.println(theoryOfList);
+    }
+
+    private List<Formula> formulaList;
+    private Bounds bounds;
+    private Solution solution;
+
+    private TheoryOfList() {
+        formulaList = new ArrayList<>();
+
+        solveExample();
+    }
+
+    private Relation Object;
+    private Relation List;
+    private Relation Nil;
+
+    private Relation car;
+    private Relation cdr;
+    private Relation eq;
+
+    private void solveExample() {
+        defineTypes();
+        defineFormulas();
+        createInstance();
+
+        Solver solver = new Solver();
+
+        solver.options().setSolver(SATFactory.Z3Solver);
+
+        solution = solver.solve(Formula.and(formulaList), bounds);
+    }
+
+    private void defineTypes() {
+        // sig Object
+        Object = Relation.unary("Object");
+        // sig List
+        List = Relation.unary("List");
+        // one 'sig Nil' extends List
+        Nil = Relation.unary("Nil");
+
+        // sig 'Nil extends List'
+        Formula nilExtendsList = Nil.in(List);
+
+        // no Object & List
+        Formula objectListDisjoint = Object.intersection(List).no();
+
+        // 'one' sig Nil extends List
+        Formula oneNil = Nil.one();
+
+        car = Relation.binary("car");
+        cdr = Relation.binary("cdr");
+        eq = Relation.binary("eq");
+
+        // car: lone 'Vehicle'
+        Formula carDefinition = car.in(List.product(Object));
+
+        // cdr: lone 'List'
+        Formula cdrDefinition = cdr.in(List.product(List));
+
+        // eq: set 'List'
+        Formula eqDefinition = eq.in(List.product(List));
+
+        // ******************************************************
+
+        formulaList.add(nilExtendsList);
+        formulaList.add(objectListDisjoint);
+        formulaList.add(oneNil);
+        formulaList.add(carDefinition);
+        formulaList.add(cdrDefinition);
+        formulaList.add(eqDefinition);
+    }
+
+    private void defineFormulas() {
+        // car: 'lone' Object
+        Variable l = Variable.unary("l");
+        Formula carLone = l.join(car).lone().forAll(l.oneOf(List));
+
+        // cdr: 'lone' List
+        l = Variable.unary("l");
+        Formula cdrLone = l.join(cdr).lone().forAll(l.oneOf(List));
+
+        // car: 'set' List -- By default, no need for a formula.
+
+        // no Nil.car
+        Formula noNilCar = Nil.join(car).no();
+
+        // no Nil.cdr
+        Formula noNilCdr = Nil.join(cdr).no();
+
+        // all l: List - Nil | some l.cdr and some l.car
+        l = Variable.unary("l");
+        Formula someCarAndCdr = l.join(cdr).some().and(l.join(car).some()).forAll(l.oneOf(List.difference(Nil)));
+
+        // all l: List: Nil in l.*cdr
+        l = Variable.unary("l");
+        Formula cdrToNil = Nil.in(l.join(cdr.reflexiveClosure())).forAll(l.oneOf(List));
+
+        // fact listEquality { all a, b: List | a in b.eq iff (a.car = b.car and a.cdr in b.cdr.eq) }
+        Variable a = Variable.unary("a");
+        Variable b = Variable.unary("b");
+        Formula listEquality = a.in(b.join(eq)).iff(a.join(car).eq(b.join(car)).and(a.join(cdr).in(b.join(cdr).join(eq)))).forAll(a.oneOf(List).and(b.oneOf(List)));
+
+        // ******************************************************
+
+        formulaList.add(carLone);
+        formulaList.add(cdrLone);
+        formulaList.add(noNilCar);
+        formulaList.add(noNilCdr);
+        formulaList.add(someCarAndCdr);
+        formulaList.add(cdrToNil);
+        formulaList.add(listEquality);
+    }
+
+    private void createInstance() {
+        String VehicleList0 = "VehicleList0";
+        String VehicleList1 = "VehicleList1";
+        String VehicleList2 = "VehicleList2";
+        String VehicleList3 = "VehicleList3";
+        String VehicleList4 = "VehicleList4";
+        String VehicleList5 = "VehicleList5";
+        String Vehicle0 = "Vehicle0";
+        String Vehicle1 = "Vehicle1";
+
+        Universe universe = new Universe(VehicleList0, VehicleList1, VehicleList2, VehicleList3, VehicleList4, VehicleList5, Vehicle0, Vehicle1);
+
+        TupleFactory tupleFactory = universe.factory();
+
+        bounds = new Bounds(universe);
+
+        // Bound types
+        bounds.boundExactly(Object, tupleFactory.setOf(Vehicle0, Vehicle1));
+        bounds.boundExactly(List, tupleFactory.setOf(VehicleList0, VehicleList1, VehicleList2, VehicleList3, VehicleList4, VehicleList5));
+        bounds.bound(Nil, tupleFactory.setOf(VehicleList0, VehicleList1, VehicleList2, VehicleList3, VehicleList4, VehicleList5));
+
+        // Bound relations
+        bounds.bound(cdr, tupleFactory.setOf(
+                    tupleFactory.tuple(VehicleList1, VehicleList2)
+                    , tupleFactory.tuple(VehicleList2, VehicleList0)
+                    , tupleFactory.tuple(VehicleList4, VehicleList3)
+                    , tupleFactory.tuple(VehicleList3, VehicleList0))
+                , tupleFactory.setOf(
+                        tupleFactory.tuple(VehicleList0, VehicleList0)
+                        , tupleFactory.tuple(VehicleList0, VehicleList1)
+                        , tupleFactory.tuple(VehicleList0, VehicleList2)
+                        , tupleFactory.tuple(VehicleList0, VehicleList3)
+                        , tupleFactory.tuple(VehicleList0, VehicleList4)
+                        , tupleFactory.tuple(VehicleList0, VehicleList5)
+                        , tupleFactory.tuple(VehicleList1, VehicleList0)
+                        , tupleFactory.tuple(VehicleList1, VehicleList1)
+                        , tupleFactory.tuple(VehicleList1, VehicleList2)
+                        , tupleFactory.tuple(VehicleList1, VehicleList3)
+                        , tupleFactory.tuple(VehicleList1, VehicleList4)
+                        , tupleFactory.tuple(VehicleList1, VehicleList5)
+                        , tupleFactory.tuple(VehicleList2, VehicleList0)
+                        , tupleFactory.tuple(VehicleList2, VehicleList1)
+                        , tupleFactory.tuple(VehicleList2, VehicleList2)
+                        , tupleFactory.tuple(VehicleList2, VehicleList3)
+                        , tupleFactory.tuple(VehicleList2, VehicleList4)
+                        , tupleFactory.tuple(VehicleList2, VehicleList5)
+                        , tupleFactory.tuple(VehicleList3, VehicleList0)
+                        , tupleFactory.tuple(VehicleList3, VehicleList1)
+                        , tupleFactory.tuple(VehicleList3, VehicleList2)
+                        , tupleFactory.tuple(VehicleList3, VehicleList3)
+                        , tupleFactory.tuple(VehicleList3, VehicleList4)
+                        , tupleFactory.tuple(VehicleList3, VehicleList5)
+                        , tupleFactory.tuple(VehicleList4, VehicleList0)
+                        , tupleFactory.tuple(VehicleList4, VehicleList1)
+                        , tupleFactory.tuple(VehicleList4, VehicleList2)
+                        , tupleFactory.tuple(VehicleList4, VehicleList3)
+                        , tupleFactory.tuple(VehicleList4, VehicleList4)
+                        , tupleFactory.tuple(VehicleList4, VehicleList5)
+                        , tupleFactory.tuple(VehicleList5, VehicleList0)
+                        , tupleFactory.tuple(VehicleList5, VehicleList1)
+                        , tupleFactory.tuple(VehicleList5, VehicleList2)
+                        , tupleFactory.tuple(VehicleList5, VehicleList3)
+                        , tupleFactory.tuple(VehicleList5, VehicleList4)
+                        , tupleFactory.tuple(VehicleList5, VehicleList5)
+                ));
+
+        bounds.bound(car, tupleFactory.setOf(
+                    tupleFactory.tuple(VehicleList1, Vehicle1)
+                    , tupleFactory.tuple(VehicleList2, Vehicle0)
+                    , tupleFactory.tuple(VehicleList4, Vehicle1)
+                    , tupleFactory.tuple(VehicleList0, Vehicle1)
+                    , tupleFactory.tuple(VehicleList3, Vehicle0))
+                , tupleFactory.setOf(
+                        tupleFactory.tuple(VehicleList0, Vehicle0)
+                        , tupleFactory.tuple(VehicleList0, Vehicle1)
+                        , tupleFactory.tuple(VehicleList1, Vehicle0)
+                        , tupleFactory.tuple(VehicleList1, Vehicle1)
+                        , tupleFactory.tuple(VehicleList2, Vehicle0)
+                        , tupleFactory.tuple(VehicleList2, Vehicle1)
+                        , tupleFactory.tuple(VehicleList3, Vehicle0)
+                        , tupleFactory.tuple(VehicleList3, Vehicle1)
+                        , tupleFactory.tuple(VehicleList4, Vehicle0)
+                        , tupleFactory.tuple(VehicleList4, Vehicle1)
+                        , tupleFactory.tuple(VehicleList5, Vehicle0)
+                        , tupleFactory.tuple(VehicleList5, Vehicle1)
+                ));
+
+        bounds.bound(eq, tupleFactory.setOf(
+                tupleFactory.tuple(VehicleList0, VehicleList0)
+                , tupleFactory.tuple(VehicleList0, VehicleList1)
+                , tupleFactory.tuple(VehicleList0, VehicleList2)
+                , tupleFactory.tuple(VehicleList0, VehicleList3)
+                , tupleFactory.tuple(VehicleList0, VehicleList4)
+                , tupleFactory.tuple(VehicleList0, VehicleList5)
+                , tupleFactory.tuple(VehicleList1, VehicleList0)
+                , tupleFactory.tuple(VehicleList1, VehicleList1)
+                , tupleFactory.tuple(VehicleList1, VehicleList2)
+                , tupleFactory.tuple(VehicleList1, VehicleList3)
+                , tupleFactory.tuple(VehicleList1, VehicleList4)
+                , tupleFactory.tuple(VehicleList1, VehicleList5)
+                , tupleFactory.tuple(VehicleList2, VehicleList0)
+                , tupleFactory.tuple(VehicleList2, VehicleList1)
+                , tupleFactory.tuple(VehicleList2, VehicleList2)
+                , tupleFactory.tuple(VehicleList2, VehicleList3)
+                , tupleFactory.tuple(VehicleList2, VehicleList4)
+                , tupleFactory.tuple(VehicleList2, VehicleList5)
+                , tupleFactory.tuple(VehicleList3, VehicleList0)
+                , tupleFactory.tuple(VehicleList3, VehicleList1)
+                , tupleFactory.tuple(VehicleList3, VehicleList2)
+                , tupleFactory.tuple(VehicleList3, VehicleList3)
+                , tupleFactory.tuple(VehicleList3, VehicleList4)
+                , tupleFactory.tuple(VehicleList3, VehicleList5)
+                , tupleFactory.tuple(VehicleList4, VehicleList0)
+                , tupleFactory.tuple(VehicleList4, VehicleList1)
+                , tupleFactory.tuple(VehicleList4, VehicleList2)
+                , tupleFactory.tuple(VehicleList4, VehicleList3)
+                , tupleFactory.tuple(VehicleList4, VehicleList4)
+                , tupleFactory.tuple(VehicleList4, VehicleList5)
+                , tupleFactory.tuple(VehicleList5, VehicleList0)
+                , tupleFactory.tuple(VehicleList5, VehicleList1)
+                , tupleFactory.tuple(VehicleList5, VehicleList2)
+                , tupleFactory.tuple(VehicleList5, VehicleList3)
+                , tupleFactory.tuple(VehicleList5, VehicleList4)
+                , tupleFactory.tuple(VehicleList5, VehicleList5)
+        ));
+    }
+
+    @Override
+    public String toString() {
+        return solution.toString();
+    }
+}
diff --git a/kodkod.iml b/kodkod.iml
@@ -0,0 +1,14 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<module type="JAVA_MODULE" version="4">
+  <component name="NewModuleRootManager" inherit-compiler-output="true">
+    <exclude-output />
+    <content url="file://$MODULE_DIR$">
+      <sourceFolder url="file://$MODULE_DIR$/src" isTestSource="false" />
+      <sourceFolder url="file://$MODULE_DIR$/examples" isTestSource="false" />
+    </content>
+    <orderEntry type="inheritedJdk" />
+    <orderEntry type="sourceFolder" forTests="false" />
+    <orderEntry type="library" name="com.microsoft.z3" level="project" />
+    <orderEntry type="library" name="org.sat4j.core-2.3.1" level="project" />
+  </component>
+</module>
diff --git a/libglucose.so b/libglucose.so
diff --git a/liblingeling.so b/liblingeling.so
diff --git a/libminisat.so b/libminisat.so
diff --git a/libminisatprover.so b/libminisatprover.so
diff --git a/libz3.dll b/libz3.dll
diff --git a/libz3.so b/libz3.so
diff --git a/libz3java.dll b/libz3java.dll
diff --git a/libz3java.so b/libz3java.so
diff --git a/minisat.dll b/minisat.dll
diff --git a/out/production/kodkod/MANIFEST b/out/production/kodkod/MANIFEST
@@ -0,0 +1,7 @@
+Name: kodkod
+Specification-Title: Kodkod API
+Specification-Version: 2.1
+Specification-Vendor: Emina Torlak
+Implementation-Title: Kodkod API
+Implementation-Version: 2.1
+Implementation-Vendor: Emina Torlak
diff --git a/out/production/kodkod/kodkod/ast/operator/package.html b/out/production/kodkod/kodkod/ast/operator/package.html
@@ -0,0 +1,16 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
+<html>
+<head>
+</head>
+<body bgcolor="white">
+
+
+Contains operators for Kodkod formulas, expressions, and integer expressions.
+
+<h2>Package Specification</h2>
+
+<p>Contains operators for Kodkod formulas, expressions, and integer expressions. </p>
+
+
+</body>
+</html>
diff --git a/out/production/kodkod/kodkod/ast/package.html b/out/production/kodkod/kodkod/ast/package.html
@@ -0,0 +1,32 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
+<html>
+<head>
+</head>
+<body bgcolor="white">
+
+
+Contains classes for creating Kodkod formulas, expressions, 
+and integer expressions.
+
+<h2>Package Specification</h2>
+
+<p>Contains the classes for creating a Kodkod abstract syntax 
+tree (AST). An object such as a quantified formula or a union expression is called a node. 
+The {@linkplain kodkod.ast.Node} class is the root of the Kodkod syntax hierarchy.</p> 
+
+<p>All classes in this package are immutable.  Their instances
+are created by calling factory methods of the classes {@linkplain kodkod.ast.Relation}, {@linkplain kodkod.ast.Variable}, 
+{@linkplain kodkod.ast.Expression}, {@linkplain kodkod.ast.IntExpression}, and {@linkplain kodkod.ast.Formula}.  Nodes can be freely shared between
+multiple parents (so a Kodkod AST is actually a directed acyclic graph).</p>
+
+<h2>Related Documentation</h2>
+
+@see kodkod.ast.Relation
+@see kodkod.ast.Variable
+@see kodkod.ast.Expression
+@see kodkod.ast.IntExpression
+@see kodkod.ast.Formula
+@see kodkod.ast.Node
+
+</body>
+</html>
diff --git a/out/production/kodkod/kodkod/ast/visitor/package.html b/out/production/kodkod/kodkod/ast/visitor/package.html
@@ -0,0 +1,29 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
+<html>
+<head>
+</head>
+<body bgcolor="white">
+
+
+Contains visitors for Kodkod formulas, expressions, and integer expressions.
+
+<h2>Package Specification</h2>
+
+<p>Provides two interfaces for traversing the Kodkod AST using
+the visitor pattern.  A {@linkplain kodkod.ast.visitor.VoidVisitor} visits the nodes but returns no values.  A
+{@linkplain kodkod.ast.visitor.ReturnVisitor} can be parametrized to return values of specific types for
+{@linkplain kodkod.ast.Decls}, {@linkplain kodkod.ast.Expression}, {@linkplain kodkod.ast.IntExpression}, 
+and {@linkplain kodkod.ast.Formula} nodes.  </p>
+
+<p>Several skeletal implementations of the VoidVisitor and ReturnVisitor interfaces
+are also provided.  These traverse the AST in a depth-first manner and optionally cache
+the results of visiting specified nodes.  The caching functionality makes it convenient
+to implement visitors that visit shared nodes only once.  </p>
+
+<h2>Related Documentation</h2>
+
+@see kodkod.ast.visitor.VoidVisitor
+@see kodkod.ast.visitor.ReturnVisitor
+
+</body>
+</html>
diff --git a/out/production/kodkod/kodkod/engine/bool/package.html b/out/production/kodkod/kodkod/engine/bool/package.html
@@ -0,0 +1,26 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2 Final//EN">
+<html>
+<head>
+</head>
+<body bgcolor="white">
+
+
+Provides classes for constructing and composing boolean matrices, boolean circuits, and
+boolean representations of integers.
+
+<h2>Package Specification</h2>
+
+<p>Contains classes that represent {@linkplain kodkod.engine.bool.BooleanMatrix boolean matrices}, 
+{@linkplain kodkod.engine.bool.BooleanValue boolean circuits}, and {@linkplain kodkod.engine.bool.Int boolean
+representation of integers}.  Matrices, circuits, and integers are constructed via factory methods of the  
+ {@linkplain kodkod.engine.bool.BooleanFactory} class. </p> 
+
+<h2>Related Documentation</h2>
+
+@see kodkod.engine.bool.BooleanFactory
+@see kodkod.engine.bool.BooleanValue
+@see kodkod.engine.bool.BooleanMatrix
+@see kodkod.engine.bool.Int
+
+</body>
+</html>