Added annotations to examples

emina · Jul 13, 2018 · d875826 · d875826
1 parent 2cef25f
commit d875826
Show file tree

Hide file tree

Showing 11 changed files with 497 additions and 547 deletions.
diff --git a/.idea/workspace.xml b/.idea/workspace.xml
diff --git a/examples/kodkod/examples/tptp/ALG195.java b/examples/kodkod/examples/tptp/ALG195.java
@@ -10,6 +10,7 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.Tuple;
 import kodkod.instance.TupleFactory;
@@ -19,6 +20,25 @@
  * A KK encoding of ALG195+1.p from http://www.cs.miami.edu/~tptp/
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "ALG195",
+		Note = "",
+		IsCheck = true,
+		PartialModel = true,
+		BinaryRelations = 7,
+		TernaryRelations = 2,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 49,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 17,
+		OrderedRelations = 0,
+		Constraints = 38
+)
 public final class ALG195 extends Quasigroups7 {
 
 	/**

diff --git a/examples/kodkod/examples/tptp/ALG195_1.java b/examples/kodkod/examples/tptp/ALG195_1.java
@@ -14,6 +14,7 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.Instance;
 import kodkod.instance.Tuple;
@@ -25,6 +26,25 @@
  * @author emina
  *
  */
+@ExampleMetadata(
+		Name = "ALG195_1",
+		Note = "",
+		IsCheck = true,
+		PartialModel = true,
+		BinaryRelations = 7,
+		TernaryRelations = 2,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 80,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 20,
+		OrderedRelations = 0,
+		Constraints = 25
+)
 public final class ALG195_1 {
 	final Relation[] e1, e2, h;
 	final Relation op1, op2, s1, s2;

diff --git a/examples/kodkod/examples/tptp/ALG212.java b/examples/kodkod/examples/tptp/ALG212.java
@@ -14,13 +14,33 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.Universe;
 
 /**
  * A KK encoding of ALG212+1.p from http://www.cs.miami.edu/~tptp/
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "ALG212",
+		Note = "",
+		IsCheck = true,
+		PartialModel = false,
+		BinaryRelations = 0,
+		TernaryRelations = 0,
+		NaryRelations = 1,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 16,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 5,
+		OrderedRelations = 0,
+		Constraints = 6
+)
 public final class ALG212 {
 	private final Relation f;
 

diff --git a/examples/kodkod/examples/tptp/COM008.java b/examples/kodkod/examples/tptp/COM008.java
@@ -15,6 +15,7 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleFactory;
 import kodkod.instance.TupleSet;
@@ -24,6 +25,25 @@
  * 
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "COM008",
+		Note = "",
+		IsCheck = true,
+		PartialModel = false,
+		BinaryRelations = 3,
+		TernaryRelations = 0,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 0,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 1,
+		OrderedRelations = 0,
+		Constraints = 14
+)
 public final class COM008 {
 	private final Relation equalish, rewrite, trr;
 	private final Relation a, b, c, goal;

diff --git a/examples/kodkod/examples/tptp/GEO091.java b/examples/kodkod/examples/tptp/GEO091.java
@@ -5,13 +5,33 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 
 /**
  * The  GEO091+1 problem from http://www.cs.miami.edu/~tptp/
  * 
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "GEO091",
+		Note = "",
+		IsCheck = true,
+		PartialModel = false,
+		BinaryRelations = 4,
+		TernaryRelations = 2,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 4,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 9,
+		OrderedRelations = 0,
+		Constraints = 39
+)
 public class GEO091 extends GEO158 {
 
 	/**

diff --git a/examples/kodkod/examples/tptp/GEO092.java b/examples/kodkod/examples/tptp/GEO092.java
@@ -9,13 +9,33 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 
 /**
  * The  GEO092+1 problem from http://www.cs.miami.edu/~tptp/
  * 
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "GEO092",
+		Note = "",
+		IsCheck = true,
+		PartialModel = false,
+		BinaryRelations = 4,
+		TernaryRelations = 2,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 4,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 8,
+		OrderedRelations = 0,
+		Constraints = 39
+)
 public class GEO092 extends GEO158 {
 
 	/**

diff --git a/examples/kodkod/examples/tptp/GEO158.java b/examples/kodkod/examples/tptp/GEO158.java
@@ -10,6 +10,7 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleFactory;
 import kodkod.instance.TupleSet;
@@ -20,14 +21,33 @@
  * 
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "GEO158",
+		Note = "",
+		IsCheck = true,
+		PartialModel = false,
+		BinaryRelations = 4,
+		TernaryRelations = 2,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 4,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 8,
+		OrderedRelations = 0,
+		Constraints = 37
+)
 public class GEO158 {
 	final Relation partOf, incident, sum, endPoint, innerPoint, meet, closed, open;
 	final Relation curve, point;
 	/*
 	 * part_of		:	C -> C
 	 * incident_c	: 	P -> C
 	 * sum			:	C -> C -> one C     	 
-	 * end_point		:	P -> C
+	 * end_point	:	P -> C
 	 * inner_point	:	P -> C
 	 * meet			: 	P -> C -> C
 	 * closed		:	C

diff --git a/examples/kodkod/examples/tptp/GEO159.java b/examples/kodkod/examples/tptp/GEO159.java
@@ -10,13 +10,33 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleSet;
 
 /**
  * The  GEO159+1 problem from http://www.cs.miami.edu/~tptp/
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "GEO159",
+		Note = "",
+		IsCheck = true,
+		PartialModel = false,
+		BinaryRelations = 4,
+		TernaryRelations = 2,
+		NaryRelations = 1,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 4,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 9,
+		OrderedRelations = 0,
+		Constraints = 39
+)
 public class GEO159 extends GEO158 {
 	final Relation between;
 	/*

diff --git a/examples/kodkod/examples/tptp/GRA013_026.java b/examples/kodkod/examples/tptp/GRA013_026.java
@@ -17,6 +17,7 @@
 import kodkod.engine.fol2sat.HigherOrderDeclException;
 import kodkod.engine.fol2sat.UnboundLeafException;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleFactory;
 import kodkod.instance.TupleSet;
@@ -27,6 +28,25 @@
  * A KK encoding of GRA019+1.p through GRA026+1.p from http://www.cs.miami.edu/~tptp/
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "GRA013_026",
+		Note = "",
+		IsCheck = true,
+		PartialModel = true,
+		BinaryRelations = 3,
+		TernaryRelations = 0,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 0,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 0,
+		OrderedRelations = 0,
+		Constraints = 5
+)
 public final class GRA013_026 {
 	private final Relation red, green, lessThan,goal,node;
 	private final int graphSize, cliqueSize;

diff --git a/examples/kodkod/examples/tptp/LAT258.java b/examples/kodkod/examples/tptp/LAT258.java
@@ -17,6 +17,7 @@
 import kodkod.engine.fol2sat.HigherOrderDeclException;
 import kodkod.engine.fol2sat.UnboundLeafException;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleFactory;
 import kodkod.instance.TupleSet;
@@ -26,6 +27,25 @@
  * A KK encoding of LAT258+1.p from http://www.cs.miami.edu/~tptp/
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "LAT258",
+		Note = "",
+		IsCheck = true,
+		PartialModel = false,
+		BinaryRelations = 1,
+		TernaryRelations = 2,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 10,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 0,
+		OrderedRelations = 0,
+		Constraints = 21
+)
 public final class LAT258 {
 	private final Relation goal, p, t, u, v, w, x, y, z;
 	private final Relation lessThan, meet, join;