diff --git a/examples/kodkod/examples/alloyinecore/TheoryOfList.java b/examples/kodkod/examples/alloyinecore/TheoryOfList.java new file mode 100644 index 00000000..18ab5340 --- /dev/null +++ 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 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 new file mode 100644 index 00000000..db74403c --- /dev/null +++ b/kodkod.iml @@ -0,0 +1,14 @@ + + + + + + + + + + + + + + \ No newline at end of file diff --git a/libglucose.so b/libglucose.so new file mode 100755 index 00000000..481ccf23 Binary files /dev/null and b/libglucose.so differ diff --git a/liblingeling.so b/liblingeling.so new file mode 100755 index 00000000..07e0881e Binary files /dev/null and b/liblingeling.so differ diff --git a/libminisat.so b/libminisat.so new file mode 100755 index 00000000..501baf07 Binary files /dev/null and b/libminisat.so differ diff --git a/libminisatprover.so b/libminisatprover.so new file mode 100755 index 00000000..cfade053 Binary files /dev/null and b/libminisatprover.so differ diff --git a/libz3.dll b/libz3.dll new file mode 100644 index 00000000..7b0760cd Binary files /dev/null and b/libz3.dll differ diff --git a/libz3.so b/libz3.so new file mode 100755 index 00000000..9b8e3c07 Binary files /dev/null and b/libz3.so differ diff --git a/libz3java.dll b/libz3java.dll new file mode 100644 index 00000000..aa00fe5a Binary files /dev/null and b/libz3java.dll differ diff --git a/libz3java.so b/libz3java.so new file mode 100755 index 00000000..ceadf2d8 Binary files /dev/null and b/libz3java.so differ diff --git a/minisat.dll b/minisat.dll new file mode 100644 index 00000000..bf9d833c Binary files /dev/null and b/minisat.dll differ diff --git a/out/production/kodkod/MANIFEST b/out/production/kodkod/MANIFEST new file mode 100644 index 00000000..21cbfa7a --- /dev/null +++ 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 \ No newline at end of file diff --git a/out/production/kodkod/kodkod/ast/operator/package.html b/out/production/kodkod/kodkod/ast/operator/package.html new file mode 100644 index 00000000..5cccc9a2 --- /dev/null +++ b/out/production/kodkod/kodkod/ast/operator/package.html @@ -0,0 +1,16 @@ + + + + + + + +Contains operators for Kodkod formulas, expressions, and integer expressions. + +

Package Specification

+ +

Contains operators for Kodkod formulas, expressions, and integer expressions.

+ + + + diff --git a/out/production/kodkod/kodkod/ast/package.html b/out/production/kodkod/kodkod/ast/package.html new file mode 100644 index 00000000..c96622b0 --- /dev/null +++ b/out/production/kodkod/kodkod/ast/package.html @@ -0,0 +1,32 @@ + + + + + + + +Contains classes for creating Kodkod formulas, expressions, +and integer expressions. + +

Package Specification

+ +

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.

+ +

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).

+ +

Related Documentation

+ +@see kodkod.ast.Relation +@see kodkod.ast.Variable +@see kodkod.ast.Expression +@see kodkod.ast.IntExpression +@see kodkod.ast.Formula +@see kodkod.ast.Node + + + diff --git a/out/production/kodkod/kodkod/ast/visitor/package.html b/out/production/kodkod/kodkod/ast/visitor/package.html new file mode 100644 index 00000000..52a29c28 --- /dev/null +++ b/out/production/kodkod/kodkod/ast/visitor/package.html @@ -0,0 +1,29 @@ + + + + + + + +Contains visitors for Kodkod formulas, expressions, and integer expressions. + +

Package Specification

+ +

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.

+ +

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.

+ +

Related Documentation

+ +@see kodkod.ast.visitor.VoidVisitor +@see kodkod.ast.visitor.ReturnVisitor + + + diff --git a/out/production/kodkod/kodkod/engine/bool/package.html b/out/production/kodkod/kodkod/engine/bool/package.html new file mode 100644 index 00000000..b97716f1 --- /dev/null +++ b/out/production/kodkod/kodkod/engine/bool/package.html @@ -0,0 +1,26 @@ + + + + + + + +Provides classes for constructing and composing boolean matrices, boolean circuits, and +boolean representations of integers. + +

Package Specification

+ +

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.

+ +

Related Documentation

+ +@see kodkod.engine.bool.BooleanFactory +@see kodkod.engine.bool.BooleanValue +@see kodkod.engine.bool.BooleanMatrix +@see kodkod.engine.bool.Int + + + diff --git a/out/production/kodkod/kodkod/engine/config/package.html b/out/production/kodkod/kodkod/engine/config/package.html new file mode 100644 index 00000000..90756013 --- /dev/null +++ b/out/production/kodkod/kodkod/engine/config/package.html @@ -0,0 +1,26 @@ + + + + + + + +Provides a mechanism for configuring the kodkod engine and for passing messages +between the engine and the client. + +

Package Specification

+ +

Provides a mechanism for configuring the kodkod engine and for passing messages +between the engine and the client. The class {@linkplain kodkod.engine.config.Options} +stores information about various user-level translation and analysis options. It can be +used to choose the SAT solver, control symmetry breaking, etc. The interface +{@linkplain kodkod.engine.config.Reporter} enables passing of messages between the kodkod engine +and the client via callback methods.

+ +

Related Documentation

+ +@see kodkod.engine.config.Options +@see kodkod.engine.config.Reporter + + + diff --git a/out/production/kodkod/kodkod/engine/fol2sat/package.html b/out/production/kodkod/kodkod/engine/fol2sat/package.html new file mode 100644 index 00000000..c726a35c --- /dev/null +++ b/out/production/kodkod/kodkod/engine/fol2sat/package.html @@ -0,0 +1,29 @@ + + + + + + + +Provides a facade for translating, evaluating, and approximating Kodkod +formulas, expressions, and int expressions with respect to a given Bounds +(or Instance) and Options. + +

Package Specification

+ +

Provides a facade for translating, evaluating, and approximating Kodkod +formulas, expressions, and int expressions with respect to given Bounds +(or Instance) and Options. The {@linkplain kodkod.engine.fol2sat.Translator} +class contains methods for translating a Kodkod formula to CNF, evaluating +a Node with respect to an instance, and over-approximating the value of an +expression based on the upper bounds in a given Bounds object.

+ +

Related Documentation

+ +@see kodkod.engine.fol2sat.Translator +@see kodkod.engine.fol2sat.Translation +@see kodkod.engine.fol2sat.TranslationLog +@see kodkod.engine.fol2sat.TranslationRecord + + + diff --git a/out/production/kodkod/kodkod/engine/package.html b/out/production/kodkod/kodkod/engine/package.html new file mode 100644 index 00000000..77e6db1b --- /dev/null +++ b/out/production/kodkod/kodkod/engine/package.html @@ -0,0 +1,38 @@ + + + + + + + +Provides classes for analyzing and evaluating Kodkod ASTs with +respect to finite bounds or instances. + +

Package Specification

+ +

Contains classes for analyzing and evaluating Kodkod ASTs with +respect to finite bounds or instances. A {@linkplain kodkod.engine.Solver Solver} +provides methods for finding finite models and minimal unsatisfiable cores of Kodkod formulas with respect +to given {@linkplain kodkod.instance.Bounds Bounds} and {@linkplain kodkod.engine.config.Options Options}. +An {@linkplain kodkod.engine.IncrementalSolver IncrementalSolver} provides a way to solve a sequence of +related formulas and bounds incrementally, with respect to the same +{@linkplain kodkod.engine.config.Options Options options}. +An {@linkplain kodkod.engine.Evaluator Evaluator} enables the evaluation of formulas, expressions, and +integer expressions with respect to a particular {@linkplain kodkod.instance.Instance Instance} and +{@linkplain kodkod.engine.config.Options Options}. + +

+ +

Related Documentation

+ +@see kodkod.instance.Bounds +@see kodkod.instance.Instance +@see kodkod.ast.Expression +@see kodkod.ast.IntExpression +@see kodkod.ast.Formula +@see kodkod.engine.Solver +@see kodkod.engine.IncrementalSolver +@see kodkod.engine.Evaluator + + + diff --git a/out/production/kodkod/kodkod/engine/satlab/package.html b/out/production/kodkod/kodkod/engine/satlab/package.html new file mode 100644 index 00000000..76506a13 --- /dev/null +++ b/out/production/kodkod/kodkod/engine/satlab/package.html @@ -0,0 +1,25 @@ + + + + + + +Provides access to various Java and C++ SAT solvers through a +common SAT Solver interface. + +

Package Specification

+ +

Provides access to various Java and C++ SAT solvers through the +{@linkplain kodkod.engine.satlab.SATSolver} and +{@linkplain kodkod.engine.satlab.SATProver} interfaces. The +{@linkplain kodkod.engine.satlab.SATFactory} class contains a selection of +static instances that can be used to generate specific SAT solvers.

+ +

Related Documentation

+ +@see kodkod.engine.satlab.SATFactory +@see kodkod.engine.satlab.SATSolver +@see kodkod.engine.satlab.SATProver + + + diff --git a/out/production/kodkod/kodkod/engine/ucore/package.html b/out/production/kodkod/kodkod/engine/ucore/package.html new file mode 100644 index 00000000..72f9903c --- /dev/null +++ b/out/production/kodkod/kodkod/engine/ucore/package.html @@ -0,0 +1,21 @@ + + + + + + +Contains strategies for minimizing unsatisfiable cores generated by SAT provers. + +

Package Specification

+ +

Contains implementations of various {@linkplain kodkod.engine.satlab.ReductionStrategy strategies} +for minimizing unsatisfiable cores generated by {@linkplain kodkod.engine.satlab.SATProver SAT provers}.

+ +

Related Documentation

+ +@see kodkod.engine.satlab.ReductionStrategy +@see kodkod.engine.satlab.SATProver + + + + diff --git a/out/production/kodkod/kodkod/instance/package.html b/out/production/kodkod/kodkod/instance/package.html new file mode 100644 index 00000000..9f889670 --- /dev/null +++ b/out/production/kodkod/kodkod/instance/package.html @@ -0,0 +1,26 @@ + + + + + + +Contains classes for creating tuples, sets of tuples, bounds, and instances +drawn from a finite universe of uninterpreted atoms. + +

Package Specification

+ +

Contains classes for creating {@linkplain kodkod.instance.Tuple tuples}, +{@linkplain kodkod.instance.TupleSet sets of tuples}, {@linkplain kodkod.instance.Bounds bounds}, and +{@linkplain kodkod.instance.Instance instances} drawn from a finite +{@linkplain kodkod.instance.Universe universe} of uninterpreted atoms.

+ +

Related Documentation

+ +@see kodkod.instance.Universe +@see kodkod.instance.TupleFactory +@see kodkod.instance.Bounds +@see kodkod.instance.Instance + + + + diff --git a/out/production/kodkod/kodkod/util/collections/package.html b/out/production/kodkod/kodkod/util/collections/package.html new file mode 100644 index 00000000..67108d4f --- /dev/null +++ b/out/production/kodkod/kodkod/util/collections/package.html @@ -0,0 +1,18 @@ + + + + + + +Contains specialized collections, such as a set that provides methods for +retrieving elements with a particular hashcode. + +

Package Specification

+ +

Contains specialized collections, such as a set that provides methods for +retrieving elements with a particular hashcode. It also provides a +utility class for working with arrays.

+ + + + diff --git a/out/production/kodkod/kodkod/util/ints/package.html b/out/production/kodkod/kodkod/util/ints/package.html new file mode 100644 index 00000000..5d7e1f66 --- /dev/null +++ b/out/production/kodkod/kodkod/util/ints/package.html @@ -0,0 +1,20 @@ + + + + + + +Provides implementations of ordered collections for storing integer primitives. + +

Package Specification

+ +

Provides several implementations of ordered collections for storing integer primitives.

+ +

Related Documentation

+ +@see kodkod.util.ints.IntSet +@see kodkod.util.ints.IntVector +@see kodkod.util.ints.SparseSequence + + + diff --git a/out/production/kodkod/kodkod/util/nodes/package.html b/out/production/kodkod/kodkod/util/nodes/package.html new file mode 100644 index 00000000..c653b9d5 --- /dev/null +++ b/out/production/kodkod/kodkod/util/nodes/package.html @@ -0,0 +1,20 @@ + + + + + + +Provides utility methods for constructing, analyzing, and pretty printing Kodkod nodes. + +

Package Specification

+ +

Provides utility methods for constructing, analyzing, and pretty printing Kodkod nodes.

+ +

Related Documentation

+ +@see kodkod.util.nodes.Nodes +@see kodkod.util.nodes.AnnotatedNode +@see kodkod.util.nodes.PrettyPrinter + + + diff --git a/plingeling b/plingeling new file mode 100755 index 00000000..b9109f8c Binary files /dev/null and b/plingeling differ diff --git a/src/kodkod/engine/Solver.java b/src/kodkod/engine/Solver.java index 6a33fb6e..06899e87 100644 --- a/src/kodkod/engine/Solver.java +++ b/src/kodkod/engine/Solver.java @@ -21,49 +21,43 @@ */ package kodkod.engine; -import java.util.ArrayList; -import java.util.Iterator; -import java.util.List; -import java.util.NoSuchElementException; - import kodkod.ast.Formula; import kodkod.ast.IntExpression; import kodkod.ast.Relation; import kodkod.engine.config.Options; -import kodkod.engine.fol2sat.HigherOrderDeclException; -import kodkod.engine.fol2sat.Translation; -import kodkod.engine.fol2sat.TranslationLog; -import kodkod.engine.fol2sat.Translator; -import kodkod.engine.fol2sat.UnboundLeafException; -import kodkod.engine.satlab.SATAbortedException; -import kodkod.engine.satlab.SATProver; -import kodkod.engine.satlab.SATSolver; +import kodkod.engine.fol2sat.*; +import kodkod.engine.satlab.*; import kodkod.instance.Bounds; import kodkod.instance.Instance; import kodkod.instance.TupleSet; +import java.util.ArrayList; +import java.util.Iterator; +import java.util.List; +import java.util.NoSuchElementException; + /** * A computational engine for solving relational satisfiability problems. - * Such a problem is described by a {@link kodkod.ast.Formula formula} in - * first order relational logic; finite {@link kodkod.instance.Bounds bounds} on - * the value of each {@link Relation relation} constrained by the formula; and - * a set of {@link kodkod.engine.config.Options options} specifying, among other global - * parameters, the length of bitvectors that describe the meaning of - * {@link IntExpression integer expressions} in the given formula. The options are + * Such a problem is described by a {@link kodkod.ast.Formula formula} in + * first order relational logic; finite {@link kodkod.instance.Bounds bounds} on + * the value of each {@link Relation relation} constrained by the formula; and + * a set of {@link kodkod.engine.config.Options options} specifying, among other global + * parameters, the length of bitvectors that describe the meaning of + * {@link IntExpression integer expressions} in the given formula. The options are * usually reused between invocations to the {@linkplain #solve(Formula, Bounds) solve} - * methods, so they are specified as a part of the {@linkplain KodkodSolver solver} state. + * methods, so they are specified as a part of the {@linkplain KodkodSolver solver} state. * *

- * A {@link Solver} takes as input a relational problem and produces a - * satisfying model or an {@link Instance instance} of it, if one exists. It can also - * produce a {@link Proof proof} of unsatisfiability for problems with no models, - * if the {@link kodkod.engine.config.Options options} specify the use of a + * A {@link Solver} takes as input a relational problem and produces a + * satisfying model or an {@link Instance instance} of it, if one exists. It can also + * produce a {@link Proof proof} of unsatisfiability for problems with no models, + * if the {@link kodkod.engine.config.Options options} specify the use of a * {@linkplain SATProver proof logging SAT solver}. - *

- * - * @specfield options: Options - * @author Emina Torlak + *

+ * + * @specfield options: Options + * @author Emina Torlak */ public final class Solver implements KodkodSolver { private final Options options; @@ -102,57 +96,78 @@ public Options options() { * @see kodkod.engine.KodkodSolver#free() */ public void free() {} - + /** - * Attempts to satisfy the given {@code formula} and {@code bounds} with respect to - * {@code this.options} or, optionally, prove the problem's unsatisfiability. If the method - * completes normally, the result is a {@linkplain Solution solution} containing either an - * {@linkplain Instance instance} of the given problem or, optionally, a {@linkplain Proof proof} of + * Attempts to satisfy the given {@code formula} and {@code bounds} with respect to + * {@code this.options} or, optionally, prove the problem's unsatisfiability. If the method + * completes normally, the result is a {@linkplain Solution solution} containing either an + * {@linkplain Instance instance} of the given problem or, optionally, a {@linkplain Proof proof} of * its unsatisfiability. An unsatisfiability - * proof will be constructed iff {@code this.options.solver} specifies a {@linkplain SATProver} and + * proof will be constructed iff {@code this.options.solver} specifies a {@linkplain SATProver} and * {@code this.options.logTranslation > 0}. - * - * @return some sol: {@link Solution} | - * some sol.instance() => - * sol.instance() in MODELS(formula, bounds, this.options) else - * UNSAT(formula, bound, this.options) - * + * + * @return some sol: {@link Solution} | + * some sol.instance() => + * sol.instance() in MODELS(formula, bounds, this.options) else + * UNSAT(formula, bound, this.options) + * * @throws NullPointerException formula = null || bounds = null * @throws UnboundLeafException the formula contains an undeclared variable or a relation not mapped by the given bounds * @throws HigherOrderDeclException the formula contains a higher order declaration that cannot * be skolemized, or it can be skolemized but {@code this.options.skolemDepth} is insufficiently large - * @throws AbortedException this solving task was aborted + * @throws AbortedException this solving task was aborted * @see Options * @see Solution * @see Instance * @see Proof */ public Solution solve(Formula formula, Bounds bounds) throws HigherOrderDeclException, UnboundLeafException, AbortedException { - + final long startTransl = System.currentTimeMillis(); - - try { - final Translation.Whole translation = Translator.translate(formula, bounds, options); - final long endTransl = System.currentTimeMillis(); - - if (translation.trivial()) - return trivial(translation, endTransl - startTransl); - final SATSolver cnf = translation.cnf(); - - options.reporter().solvingCNF(translation.numPrimaryVariables(), cnf.numberOfVariables(), cnf.numberOfClauses()); - final long startSolve = System.currentTimeMillis(); - final boolean isSat = cnf.solve(); - final long endSolve = System.currentTimeMillis(); + try { + if (options.solver().instance() instanceof Z3Solver) { + Z3Solver z3Solver = (Z3Solver) options.solver().instance(); + final long startSolve = System.currentTimeMillis(); + final boolean isSat = z3Solver.solve(formula, bounds); + final long endSolve = System.currentTimeMillis(); - final Statistics stats = new Statistics(translation, endTransl - startTransl, endSolve - startSolve); - return isSat ? sat(translation, stats) : unsat(translation, stats); - + final Statistics stats = new Statistics(0, 0, 0 + , endSolve - startSolve - z3Solver.getSolvingTimeInMilis() + , z3Solver.getSolvingTimeInMilis()); + + if (isSat) { + final Solution sol = Solution.satisfiable(stats, z3Solver.getInstance()); + return sol; + } + else { + // TODO: Get proof + final Solution sol = Solution.unsatisfiable(stats, null); + return sol; + } + } + else { + final Translation.Whole translation = Translator.translate(formula, bounds, options); + final long endTransl = System.currentTimeMillis(); + + if (translation.trivial()) + return trivial(translation, endTransl - startTransl); + + final SATSolver cnf = translation.cnf(); + + options.reporter().solvingCNF(translation.numPrimaryVariables(), cnf.numberOfVariables(), cnf.numberOfClauses()); + final long startSolve = System.currentTimeMillis(); + final boolean isSat = cnf.solve(); + final long endSolve = System.currentTimeMillis(); + + final Statistics stats = new Statistics(translation, endTransl - startTransl, endSolve - startSolve); + return isSat ? sat(translation, stats) : unsat(translation, stats); + } } catch (SATAbortedException sae) { throw new AbortedException(sae); } } - + /** * Attempts to find all solutions to the given formula with respect to the specified bounds or * to prove the formula's unsatisfiability. @@ -160,10 +175,10 @@ public Solution solve(Formula formula, Bounds bounds) throws HigherOrderDeclExce * of the first n-1 solutions is SAT or trivially SAT, and the outcome of the nth solution is UNSAT * or trivially UNSAT. Note that an unsatisfiability * proof will be constructed for the last solution iff this.options specifies the use of a core extracting SATSolver. - * Additionally, the CNF variables in the proof can be related back to the nodes in the given formula - * iff this.options has variable tracking enabled. Translation logging also requires that - * there are no subnodes in the given formula that are both syntactically shared and contain free variables. - * + * Additionally, the CNF variables in the proof can be related back to the nodes in the given formula + * iff this.options has variable tracking enabled. Translation logging also requires that + * there are no subnodes in the given formula that are both syntactically shared and contain free variables. + * * @return an iterator over all the Solutions to the formula with respect to the given bounds * @throws NullPointerException formula = null || bounds = null * @throws kodkod.engine.fol2sat.UnboundLeafException the formula contains an undeclared variable or @@ -176,27 +191,55 @@ public Solution solve(Formula formula, Bounds bounds) throws HigherOrderDeclExce * @see Options * @see Proof */ - public Iterator solveAll(final Formula formula, final Bounds bounds) + public Iterator solveAll(final Formula formula, final Bounds bounds) throws HigherOrderDeclException, UnboundLeafException, AbortedException { - + + if (options.solver().instance() instanceof Z3Solver) { + Z3Solver z3Solver = (Z3Solver) options.solver().instance(); + Iterator instanceIterator = z3Solver.solveAll(formula, bounds); + return new Iterator() { + @Override + public boolean hasNext() { + return instanceIterator.hasNext(); + } + + @Override + public Solution next() { + final long startSolve = System.currentTimeMillis(); + Instance instance = instanceIterator.next(); + final long endSolve = System.currentTimeMillis(); + + final Statistics stats = new Statistics(0, 0, 0 + , endSolve - startSolve - z3Solver.getSolvingTimeInMilis() + , z3Solver.getSolvingTimeInMilis()); + + if (instance == null) { + return Solution.unsatisfiable(stats, null); + } + else { + return Solution.satisfiable(stats, instance); + } + } + }; + } + if (!options.solver().incremental()) throw new IllegalArgumentException("cannot enumerate solutions without an incremental solver."); - + return new SolutionIterator(formula, bounds, options); - + } /** * {@inheritDoc} - * @see java.lang.Object#toString() + * @see Object#toString() */ public String toString() { return options.toString(); } - + /** * Returns the result of solving a sat formula. - * @param bounds Bounds with which solve() was called * @param translation the translation * @param stats translation / solving stats * @return the result of solving a sat formula. @@ -209,7 +252,7 @@ private static Solution sat(Translation.Whole translation, Statistics stats) { /** * Returns the result of solving an unsat formula. - * @param translation the translation + * @param translation the translation * @param stats translation / solving stats * @return the result of solving an unsat formula. */ @@ -224,10 +267,10 @@ private static Solution unsat(Translation.Whole translation, Statistics stats) { return sol; } } - + /** * Returns the result of solving a trivially (un)sat formula. - * @param translation trivial translation produced as the result of {@code translation.formula} + * @param translation trivial translation produced as the result of {@code translation.formula} * simplifying to a constant with respect to {@code translation.bounds} * @param translTime translation time * @return the result of solving a trivially (un)sat formula. @@ -243,7 +286,7 @@ private static Solution trivial(Translation.Whole translation, long translTime) translation.cnf().free(); return sol; } - + /** * Returns a proof for the trivially unsatisfiable log.formula, * provided that log is non-null. Otherwise returns null. @@ -254,7 +297,7 @@ private static Solution trivial(Translation.Whole translation, long translTime) private static Proof trivialProof(TranslationLog log) { return log==null ? null : new TrivialProof(log); } - + /** * An iterator over all solutions of a model. * @author Emina Torlak @@ -263,7 +306,7 @@ private static final class SolutionIterator implements Iterator { private Translation.Whole translation; private long translTime; private int trivial; - + /** * Constructs a solution iterator for the given formula, bounds, and options. */ @@ -273,16 +316,16 @@ private static final class SolutionIterator implements Iterator { this.translTime = System.currentTimeMillis() - translTime; this.trivial = 0; } - + /** * Returns true if there is another solution. - * @see java.util.Iterator#hasNext() + * @see Iterator#hasNext() */ public boolean hasNext() { return translation != null; } - + /** * Returns the next solution if any. - * @see java.util.Iterator#next() + * @see Iterator#next() */ public Solution next() { if (!hasNext()) throw new NoSuchElementException(); @@ -364,7 +407,7 @@ private Solution nextTrivialSolution() { final List changes = new ArrayList(); for(Relation r : bounds.relations()) { - final TupleSet lower = bounds.lowerBound(r); + final TupleSet lower = bounds.lowerBound(r); if (lower != bounds.upperBound(r)) { // r may change if (lower.isEmpty()) { diff --git a/src/kodkod/engine/satlab/SATFactory.java b/src/kodkod/engine/satlab/SATFactory.java index cd7a3508..e24f3e7a 100644 --- a/src/kodkod/engine/satlab/SATFactory.java +++ b/src/kodkod/engine/satlab/SATFactory.java @@ -21,13 +21,13 @@ */ package kodkod.engine.satlab; +import org.sat4j.minisat.SolverFactory; + import java.io.File; import java.io.IOException; import java.util.ArrayList; import java.util.List; -import org.sat4j.minisat.SolverFactory; - /** * A factory for generating SATSolver instances of a given type. * Built-in support is provided for many solvers, including @@ -69,9 +69,9 @@ public static final boolean available(SATFactory factory) { * The factory that produces instances of the default sat4j solver. * @see org.sat4j.core.ASolverFactory#defaultSolver() */ - public static final SATFactory DefaultSAT4J = new SATFactory() { - public SATSolver instance() { - return new SAT4J(SolverFactory.instance().defaultSolver()); + public static final SATFactory DefaultSAT4J = new SATFactory() { + public SATSolver instance() { + return new SAT4J(SolverFactory.instance().defaultSolver()); } public String toString() { return "DefaultSAT4J"; } }; @@ -82,8 +82,8 @@ public SATSolver instance() { * @see org.sat4j.core.ASolverFactory#lightSolver() */ public static final SATFactory LightSAT4J = new SATFactory() { - public SATSolver instance() { - return new SAT4J(SolverFactory.instance().lightSolver()); + public SATSolver instance() { + return new SAT4J(SolverFactory.instance().lightSolver()); } public String toString() { return "LightSAT4J"; } }; @@ -98,17 +98,25 @@ public SATSolver instance() { } public String toString() { return "MiniSat"; } }; + + public static final SATFactory Z3Solver = new SATFactory() { + public SATSolver instance() { + return new Z3Solver(); + } + public boolean prover() { return true; } + public String toString() { return "Z3"; } + }; /** - * The factory the produces {@link SATProver proof logging} + * The factory the produces {@link SATProver proof logging} * instances of the MiniSat solver. Note that core * extraction can incur a significant time overhead during solving, * so if you do not need this functionality, use the {@link #MiniSat} factory * instead. */ public static final SATFactory MiniSatProver = new SATFactory() { - public SATSolver instance() { - return new MiniSatProver(); + public SATSolver instance() { + return new MiniSatProver(); } @Override public boolean prover() { return true; } @@ -249,7 +257,7 @@ public SATSolver instance() { return new ExternalSolver(executable, cnf, false, options); } else { try { - return new ExternalSolver(executable, + return new ExternalSolver(executable, File.createTempFile("kodkod", String.valueOf(executable.hashCode())).getAbsolutePath(), true, options); } catch (IOException e) { diff --git a/src/kodkod/engine/satlab/Z3Solver.java b/src/kodkod/engine/satlab/Z3Solver.java new file mode 100644 index 00000000..71b57ece --- /dev/null +++ b/src/kodkod/engine/satlab/Z3Solver.java @@ -0,0 +1,717 @@ +package kodkod.engine.satlab; + +import com.microsoft.z3.*; +import kodkod.ast.*; +import kodkod.ast.operator.ExprOperator; +import kodkod.ast.operator.FormulaOperator; +import kodkod.ast.visitor.AbstractDetector; +import kodkod.instance.Bounds; +import kodkod.instance.Instance; +import kodkod.instance.Tuple; +import kodkod.instance.TupleSet; + +import java.util.*; +import java.util.stream.Collectors; + +public class Z3Solver implements SATSolver { + + private Context ctx; + + private Solver solver; + + private EnumSort UNIV; + + private Map funcDeclMap = new HashMap<>(); + private Map variableExprMap = new HashMap<>(); + + private Status status = Status.SATISFIABLE; + private Bounds bounds = null; + private Instance instance = null; + + private int quantifierID; + private int skolemID; + + + + private long solvingTime = 0; + + private Goal goal = null; + + private Set possibleExprs; + private Map> exprTupleMap; + + public Z3Solver() { + Global.setParameter("model.compact", "true"); + Global.setParameter("smt.mbqi", "true"); + Global.setParameter("smt.pull-nested-quantifiers", "true"); + Global.setParameter("smt.mbqi.trace", "true"); + + HashMap cfg = new HashMap<>(); + cfg.put("proof", "true"); + cfg.put("model", "true"); + + ctx = new Context(cfg); + goal = ctx.mkGoal(true, false, false); + } + + public Status getStatus() { + return status; + } + + public long getSolvingTimeInMilis() { + return solvingTime; + } + + public Instance getInstance() { + return instance; + } + + private void makeAssertions(Formula formula, Bounds bounds) { + System.out.println(); + System.out.println("----- z3 -----"); + System.out.println(); + + this.bounds = bounds; + + Map objectMap = new HashMap<>(); + Map objectExprMap = new HashMap<>(); + + for (int i = 0; i < bounds.universe().size(); i++) { + Object object = bounds.universe().atom(i); + objectMap.put(object.toString(), object); + } + + UNIV = ctx.mkEnumSort("Univ", objectMap.keySet().toArray(new String[objectMap.keySet().size()])); + + for (Expr expr : UNIV.getConsts()) { + Object object = objectMap.get(expr.toString()); + if (object == null) + object = objectMap.get(expr.toString().substring(1, expr.toString().length() - 1)); + objectExprMap.put(object, expr); + } + + AbstractDetector detector = new AbstractDetector(Collections.emptySet()) {}; + + FuncDecl univFuncDecl = null; + if (detector.visit((ConstantExpression) Relation.UNIV)) { + univFuncDecl = ctx.mkFuncDecl("univ", new Sort[]{UNIV}, ctx.mkBoolSort()); + funcDeclMap.put(Relation.UNIV, univFuncDecl); + } + /*FuncDecl idenFuncDecl = null; + if (detector.visit((ConstantExpression) Relation.IDEN) || formula.toString().contains("*") || formula.toString().contains("^")) { + idenFuncDecl = ctx.mkFuncDecl("iden", new Sort[]{UNIV, UNIV}, ctx.mkBoolSort()); + funcDeclMap.put(Relation.IDEN, idenFuncDecl); + }*/ + FuncDecl noneFuncDecl = null; + if (detector.visit((ConstantExpression) Relation.NONE)) { + noneFuncDecl = ctx.mkFuncDecl("None", new Sort[]{UNIV}, ctx.mkBoolSort()); + funcDeclMap.put(Relation.NONE, noneFuncDecl); + } + /*FuncDecl intsFuncDecl = null; + if (detector.visit((ConstantExpression) Relation.INTS)) { + intsFuncDecl = funcDeclMap.put(Relation.INTS, ctx.mkFuncDecl("Ints", new Sort[] {ctx.mkIntSort()}, ctx.mkBoolSort())); + funcDeclMap.put(Relation.INTS, intsFuncDecl); + }*/ + + possibleExprs = new HashSet<>(); + exprTupleMap = new HashMap<>(); + + bounds.relations().forEach(relation -> { + Sort[] sorts = new Sort[relation.arity()]; + for (int i = 0; i < sorts.length; i++) { + sorts[i] = UNIV; + } + FuncDecl funcDecl = ctx.mkFuncDecl(relation.name(), sorts, ctx.mkBoolSort()); + funcDeclMap.put(relation, funcDecl); + + bounds.lowerBounds().get(relation).forEach(tuple -> { + Expr[] exprs = new Expr[tuple.arity()]; + for (int i = 0; i < exprs.length; i++) { + exprs[i] = objectExprMap.get(tuple.atom(i)); + } + goal.add((BoolExpr) ctx.mkApp(funcDecl, exprs)); + }); + + bounds.upperBounds().get(relation).forEach(tuple -> { + Expr[] exprs = new Expr[tuple.arity()]; + for (int i = 0; i < exprs.length; i++) { + exprs[i] = objectExprMap.get(tuple.atom(i)); + } + + Expr expr = ctx.mkApp(funcDecl, exprs); + possibleExprs.add(expr); + + exprTupleMap.put(expr, new AbstractMap.SimpleEntry<>(relation, tuple)); + }); + }); + + for (Expr expr1 : objectExprMap.values()) { + if (univFuncDecl != null) + goal.add((BoolExpr) ctx.mkApp(univFuncDecl, new Expr[] {expr1})); + if (noneFuncDecl != null) + goal.add(ctx.mkNot((BoolExpr) ctx.mkApp(noneFuncDecl, new Expr[] {expr1}))); + /*if (idenFuncDecl != null) { + goal.add((BoolExpr) ctx.mkApp(idenFuncDecl, new Expr[]{expr1, expr1})); + for (Expr expr2 : objectExprMap.values()) { + if (expr1 != expr2) { + goal.add(ctx.mkNot((BoolExpr) ctx.mkApp(idenFuncDecl, new Expr[] {expr1, expr2}))); + goal.add(ctx.mkNot((BoolExpr) ctx.mkApp(idenFuncDecl, new Expr[] {expr2, expr1}))); + } + } + }*/ + } + + Map boolExprMap = separateFormula(formula).stream() + .collect(Collectors.toMap(f -> visit(f, 0, new Expr[] {}), f -> f)); + + boolExprMap.forEach((boolExpr, f) -> { + System.out.println("kodkod: " + f); + System.out.println("z3:"); + System.out.println(boolExpr); + System.out.println(); + }); + + boolExprMap.keySet().forEach(goal::add); + + System.out.println(); + System.out.println(); + } + + public Iterator solveAll(Formula formula, Bounds bounds) { + makeAssertions(formula, bounds); + + return new Iterator() { + @Override + public boolean hasNext() { + return status.equals(Status.SATISFIABLE); + } + + @Override + public Instance next() { + + System.out.println(solver); + System.out.println("---------------------------------------------------"); + + solveThis(bounds); + + if (status.equals(Status.SATISFIABLE)) { + solver.add(ctx.mkNot(ctx.mkAnd(possibleExprs.stream() + .filter(expr -> expr instanceof BoolExpr && solver.getModel().eval(expr, true).equals(ctx.mkTrue())) + .map(expr -> (BoolExpr) expr).toArray(BoolExpr[]::new)))); + } + + return instance; + } + }; + } + + public boolean solve(Formula formula, Bounds bounds) { + makeAssertions(formula, bounds); + + System.out.println("----------------After Tactics----------------------"); + //Tactics + Tactic t = ctx.andThen(ctx.mkTactic("snf"), ctx.mkTactic("qe") ); + //Tactic t = ctx.mkTactic("snf"); + solver = ctx.mkSolver(); + Params p = ctx.mkParams(); + p.add("mbqi", true); + p.add("pull-nested-quantifiers", true); + solver.setParameters(p); + ApplyResult ar = t.apply(goal); + for (BoolExpr e : ar.getSubgoals()[0].getFormulas()) + solver.add(e); + //end of tactics application + System.out.println(solver); + System.out.println("---------------------------------------------------"); + + solveThis(bounds); + + return status == Status.SATISFIABLE; + } + + private void solveThis(Bounds bounds){ + + long beginningTime = System.currentTimeMillis(); + status = solver.check(); + solvingTime = System.currentTimeMillis() - beginningTime; + + System.out.println(solvingTime + " ms"); + + switch (status) { + case SATISFIABLE: + Set reasonedExprs = possibleExprs.stream() + .filter(expr -> solver.getModel().eval(expr, true).equals(ctx.mkTrue())) + .collect(Collectors.toSet()); + + System.out.println("Sat"); + reasonedExprs.forEach(System.out::println); + System.out.println(); + possibleExprs.forEach(e -> System.out.println(e + " = " + solver.getModel().eval(e, true))); + System.out.println(); + System.out.println(solver.getModel()); + + this.instance = new Instance(bounds.universe()); + + Map> relationTuplesMap = new HashMap<>(); + + reasonedExprs.forEach(expr -> { + Map.Entry entry = exprTupleMap.get(expr); + relationTuplesMap.computeIfAbsent(entry.getKey(), r -> new HashSet<>()).add(entry.getValue()); + }); + + relationTuplesMap.forEach((relation, tuples) -> { + instance.add(relation, bounds.universe().factory().setOf(tuples)); + }); + + System.out.println(instance); + break; + case UNSATISFIABLE: + System.out.println("Unsat"); + Arrays.stream(solver.getUnsatCore()).forEach(System.out::println); + this.instance = null; + break; + case UNKNOWN: + System.out.println("Unknown"); + break; + } + } + + private Set separateFormula(Formula formula) { + if (formula instanceof BinaryFormula && ((BinaryFormula) formula).op().equals(FormulaOperator.AND)) { + Set formulaSet = new HashSet<>(); + formulaSet.addAll(separateFormula(((BinaryFormula) formula).left())); + formulaSet.addAll(separateFormula(((BinaryFormula) formula).right())); + return formulaSet; + } + if (formula instanceof NaryFormula && ((NaryFormula) formula).op().equals(FormulaOperator.AND)) { + Set formulaSet = new HashSet<>(); + ((NaryFormula) formula).iterator().forEachRemaining(f -> { + formulaSet.addAll(separateFormula(f)); + }); + return formulaSet; + } + return Collections.singleton(formula); + } + + private BoolExpr visit(Node node, int depth, Expr[] exprs) { + String quantifierPrefix = "q!"; + String skolemPrefix = "s!"; + + if (node instanceof Relation) { + return (BoolExpr) ctx.mkApp(funcDeclMap.get(node), exprs); + } + else if (node instanceof ConstantExpression) { + if (node.equals(Relation.IDEN)) { + return ctx.mkEq(exprs[0], exprs[1]); + } + return (BoolExpr) ctx.mkApp(funcDeclMap.get(node), exprs); + } + else if (node instanceof Variable) { + return ctx.mkEq(variableExprMap.get(node), exprs[0]); + } + else if (node instanceof UnaryExpression) { + UnaryExpression unaryExpression = (UnaryExpression) node; + switch (unaryExpression.op()) { + case TRANSPOSE: + return visit(unaryExpression.expression(), depth, new Expr[] {exprs[1], exprs[0]}); + case REFLEXIVE_CLOSURE: + Expression ex = unaryExpression.expression(); + while (ex instanceof BinaryExpression && ((BinaryExpression) ex).op().equals(ExprOperator.JOIN)) { + ex = ((BinaryExpression) ex).right(); + } + + int loopCount = UNIV.getConsts().length - 1; + + if (ex.equals(Relation.NONE)) { + loopCount = 0; + } + else if (ex instanceof Relation) { + loopCount = (int) (bounds.upperBound((Relation) ex).stream() + .map(t -> t.atom(t.arity() - 1)) + .distinct().count()) - 1; + } + + /*List expressions = new ArrayList<>(); + expressions.add(Relation.IDEN); + for (int i = 0; i < loopCount; i++) { + Expression expression = unaryExpression.expression(); + for (int j = 0; j < i; j++) { + expression = expression.join(unaryExpression.expression()); + } + expressions.add(expression); + }*/ + + Expression unionExpr = Relation.IDEN; + for (int i = 0; i < loopCount - 1; i++) { + unionExpr = Relation.IDEN.union(unaryExpression.expression().join(unionExpr)); + } + + //return visit(Expression.union(expressions), depth, exprs); + return visit(unionExpr, depth, exprs); + case CLOSURE: + ex = unaryExpression.expression(); + while (ex instanceof BinaryExpression && ((BinaryExpression) ex).op().equals(ExprOperator.JOIN)) { + ex = ((BinaryExpression) ex).right(); + } + + loopCount = UNIV.getConsts().length - 1; + + if (ex.equals(Relation.NONE)) { + loopCount = 0; + } + else if (ex instanceof Relation) { + loopCount = (int) (bounds.upperBound((Relation) ex).stream() + .map(t -> t.atom(t.arity() - 1)) + .distinct().count()) - 1; + } + + /*expressions = new ArrayList<>(); + for (int i = 0; i < loopCount; i++) { + Expression expression = unaryExpression.expression(); + for (int j = 0; j < i; j++) { + expression = expression.join(unaryExpression.expression()); + } + expressions.add(expression); + } + return visit(Expression.union(expressions), depth, exprs);*/ + + unionExpr = Relation.IDEN; + for (int i = 0; i < loopCount - 1; i++) { + unionExpr = Relation.IDEN.union(unaryExpression.expression().join(unionExpr)); + } + + if (unionExpr instanceof BinaryExpression && ((BinaryExpression) unionExpr).op().equals(ExprOperator.UNION)) + return visit(((BinaryExpression) unionExpr).right(), depth, exprs); + else { + return ctx.mkFalse(); + } + } + } + else if (node instanceof BinaryExpression) { + BinaryExpression binaryExpression = (BinaryExpression) node; + switch (binaryExpression.op()) { + case JOIN: + Expr expr = ctx.mkConst("x" + depth, UNIV); + + Expression leftExpression = binaryExpression.left(); + Expression rightExpression = binaryExpression.right(); + + Expr[] leftExprs = new Expr[leftExpression.arity()]; + + System.arraycopy(exprs, 0, leftExprs, 0, leftExprs.length - 1); + leftExprs[leftExprs.length - 1] = expr; + + Expr[] rightExprs = new Expr[rightExpression.arity()]; + + rightExprs[0] = expr; + System.arraycopy(exprs, exprs.length - rightExprs.length + 1, rightExprs, 1, rightExprs.length - 1); + + if (leftExpression instanceof Variable) { + rightExprs[0] = variableExprMap.get(leftExpression); + return visit(rightExpression, depth + 1, rightExprs); + } + else if (rightExpression instanceof Variable) { + rightExprs[rightExprs.length - 1] = variableExprMap.get(rightExpression); + return visit(leftExpression, depth + 1, leftExprs); + } + + return ctx.mkExists(new Expr[] {expr} + , ctx.mkAnd(visit(leftExpression, depth + 1, leftExprs) + , visit(rightExpression, depth + 1, rightExprs)) + , 0, null, null, ctx.mkSymbol(quantifierPrefix + quantifierID++), ctx.mkSymbol(skolemPrefix + skolemID++)); + case UNION: + return ctx.mkOr(visit(binaryExpression.left(), depth, exprs), visit(binaryExpression.right(), depth, exprs)); + case INTERSECTION: + return ctx.mkAnd(visit(binaryExpression.left(), depth, exprs), visit(binaryExpression.right(), depth, exprs)); + case PRODUCT: + leftExpression = binaryExpression.left(); + rightExpression = binaryExpression.right(); + + leftExprs = new Expr[leftExpression.arity()]; + System.arraycopy(exprs, 0, leftExprs, 0, leftExprs.length); + + rightExprs = new Expr[rightExpression.arity()]; + System.arraycopy(exprs, leftExpression.arity(), rightExprs, 0, rightExprs.length); + + return ctx.mkAnd(visit(leftExpression, depth, leftExprs), visit(rightExpression, depth, rightExprs)); + case DIFFERENCE: + return ctx.mkAnd(visit(binaryExpression.left(), depth, exprs), ctx.mkNot(visit(binaryExpression.right(), depth, exprs))); + case OVERRIDE: + // TODO: Implement this. + break; + } + } + else if (node instanceof NaryExpression) { + NaryExpression naryExpression = (NaryExpression) node; + + switch (naryExpression.op()) { + case UNION: + BoolExpr[] boolExprs = new BoolExpr[naryExpression.size()]; + for (int i = 0; i < boolExprs.length; i++) { + boolExprs[i] = visit(naryExpression.child(i), depth, exprs); + } + return ctx.mkOr(boolExprs); + case PRODUCT: + boolExprs = new BoolExpr[naryExpression.size()]; + for (int i = 0; i < boolExprs.length; i++) { + int start = 0; + + for (int j = 0; j < i; j++) + start += naryExpression.child(i - 1).arity(); + + Expression expression = naryExpression.child(i); + Expr[] exprs1 = new Expr[expression.arity()]; + + System.arraycopy(exprs, start, exprs1, 0, exprs1.length); + + boolExprs[i] = visit(expression, depth, exprs1); + } + return ctx.mkAnd(boolExprs); + case INTERSECTION: + boolExprs = new BoolExpr[naryExpression.size()]; + for (int i = 0; i < boolExprs.length; i++) { + boolExprs[i] = visit(naryExpression.child(i), depth, exprs); + } + return ctx.mkAnd(boolExprs); + case OVERRIDE: + // TODO: Implement this. + break; + } + } + else if (node instanceof NotFormula) { + NotFormula notFormula = (NotFormula) node; + return ctx.mkNot(visit(notFormula.formula(), depth, exprs)); + } + else if (node instanceof ComparisonFormula) { + ComparisonFormula comparisonFormula = (ComparisonFormula) node; + switch (comparisonFormula.op()) { + case EQUALS: + Expr[] exprs1; + if (comparisonFormula.left() instanceof Variable) { + if (comparisonFormula.right() instanceof Variable) { + return ctx.mkEq(variableExprMap.get(comparisonFormula.left()), variableExprMap.get(comparisonFormula.right())); + } + else { + exprs1 = new Expr[comparisonFormula.left().arity()]; + exprs1[0] = variableExprMap.get(comparisonFormula.left()); + return visit(comparisonFormula.right(), depth, exprs1); + } + } + else if (comparisonFormula.right() instanceof Variable) { + exprs1 = new Expr[comparisonFormula.right().arity()]; + exprs1[0] = variableExprMap.get(comparisonFormula.right()); + return visit(comparisonFormula.left(), depth, exprs1); + } + + exprs1 = new Expr[comparisonFormula.left().arity()]; + for (int i = 0; i < exprs1.length; i++) { + exprs1[i] = ctx.mkConst("x" + (depth + i), UNIV); + } + return ctx.mkForall(exprs1 + , ctx.mkIff(visit(comparisonFormula.left(), exprs1.length + depth, exprs1) + , visit(comparisonFormula.right(), exprs1.length + depth, exprs1)) + , 0, null, null, ctx.mkSymbol(quantifierPrefix + quantifierID++), null); + case SUBSET: + if (comparisonFormula.left() instanceof Variable) { + if (comparisonFormula.right() instanceof Variable) { + return ctx.mkEq(variableExprMap.get(comparisonFormula.left()), variableExprMap.get(comparisonFormula.right())); + } + else { + exprs1 = new Expr[comparisonFormula.left().arity()]; + exprs1[0] = variableExprMap.get(comparisonFormula.left()); + return visit(comparisonFormula.right(), depth, exprs1); + } + } + else if (comparisonFormula.right() instanceof Variable) { + exprs1 = new Expr[comparisonFormula.right().arity()]; + exprs1[0] = variableExprMap.get(comparisonFormula.right()); + return visit(comparisonFormula.left(), depth, exprs1); + } + + exprs1 = new Expr[comparisonFormula.left().arity()]; + for (int i = 0; i < exprs1.length; i++) { + exprs1[i] = ctx.mkConst("x" + (i + depth), UNIV); + } + return ctx.mkForall(exprs1 + , ctx.mkImplies(visit(comparisonFormula.left(), exprs1.length + depth, exprs1) + , visit(comparisonFormula.right(), exprs1.length + depth, exprs1)) + , 0, null, null, ctx.mkSymbol(quantifierPrefix + quantifierID++), null); + } + } + else if (node instanceof BinaryFormula) { + BinaryFormula binaryFormula = (BinaryFormula) node; + switch (binaryFormula.op()) { + case IMPLIES: + return ctx.mkImplies(visit(binaryFormula.left(), depth, exprs), visit(binaryFormula.right(), depth, exprs)); + case IFF: + return ctx.mkIff(visit(binaryFormula.left(), depth, exprs), visit(binaryFormula.right(), depth, exprs)); + case OR: + return ctx.mkOr(visit(binaryFormula.left(), depth, exprs), visit(binaryFormula.right(), depth, exprs)); + case AND: + return ctx.mkAnd(visit(binaryFormula.left(), depth, exprs), visit(binaryFormula.right(), depth, exprs)); + } + } + else if (node instanceof NaryFormula) { + NaryFormula naryFormula = (NaryFormula) node; + switch (naryFormula.op()) { + case AND: + BoolExpr[] boolExprs = new BoolExpr[naryFormula.size()]; + for (int i = 0; i < boolExprs.length; i++) { + boolExprs[i] = visit(naryFormula.child(i), depth, exprs); + } + return ctx.mkAnd(boolExprs); + case OR: + boolExprs = new BoolExpr[naryFormula.size()]; + for (int i = 0; i < boolExprs.length; i++) { + boolExprs[i] = visit(naryFormula.child(i), depth, exprs); + } + return ctx.mkOr(boolExprs); + } + } + else if (node instanceof MultiplicityFormula) { + MultiplicityFormula multiplicityFormula = (MultiplicityFormula) node; + switch (multiplicityFormula.multiplicity()) { + case SOME: + Expr[] exprs1 = new Expr[multiplicityFormula.expression().arity()]; + for (int i = 0; i < exprs1.length; i++) { + exprs1[i] = ctx.mkConst("x" + (i + depth), UNIV); + } + return ctx.mkExists(exprs1 + , visit(multiplicityFormula.expression(), exprs1.length + depth, exprs1) + , 0, null, null, ctx.mkSymbol(quantifierPrefix + quantifierID++), ctx.mkSymbol(skolemPrefix + skolemID++)); + case NO: + exprs1 = new Expr[multiplicityFormula.expression().arity()]; + for (int i = 0; i < exprs1.length; i++) { + exprs1[i] = ctx.mkConst("x" + (i + depth), UNIV); + } + return ctx.mkNot(ctx.mkExists(exprs1 + , visit(multiplicityFormula.expression(), exprs1.length + depth, exprs1) + , 0, null, null, ctx.mkSymbol(quantifierPrefix + quantifierID++), ctx.mkSymbol(skolemPrefix + skolemID++))); + case ONE: + exprs1 = new Expr[multiplicityFormula.expression().arity()]; + for (int i = 0; i < exprs1.length; i++) { + exprs1[i] = ctx.mkConst("a" + (i + depth), UNIV); + } + Expr[] exprs2 = new Expr[multiplicityFormula.expression().arity()]; + for (int i = 0; i < exprs2.length; i++) { + exprs2[i] = ctx.mkConst("b" + (i + depth), UNIV); + } + BoolExpr[] eqs = new BoolExpr[exprs1.length]; + for (int i = 0; i < eqs.length; i++) { + eqs[i] = ctx.mkEq(exprs1[i], exprs2[i]); + } + + Expr[] allExprs = new Expr[exprs1.length + exprs2.length]; + System.arraycopy(exprs1, 0, allExprs, 0, exprs1.length); + System.arraycopy(exprs2, 0, allExprs, exprs1.length, exprs2.length); + + Quantifier lone = ctx.mkForall(allExprs + , ctx.mkImplies( + ctx.mkAnd(visit(multiplicityFormula.expression(), depth, exprs1) + , visit(multiplicityFormula.expression(), depth, exprs2)) + , ctx.mkAnd(eqs)) + , 0, null, null, ctx.mkSymbol(quantifierPrefix + quantifierID++), null); + Quantifier some = ctx.mkExists(exprs1, visit(multiplicityFormula.expression(), depth, exprs1) + , 0, null, null, ctx.mkSymbol(quantifierPrefix + quantifierID++), ctx.mkSymbol(skolemPrefix + skolemID++)); + + return ctx.mkAnd(some, lone); + case LONE: + exprs1 = new Expr[multiplicityFormula.expression().arity()]; + for (int i = 0; i < exprs1.length; i++) { + exprs1[i] = ctx.mkConst("a" + (i + depth), UNIV); + } + exprs2 = new Expr[multiplicityFormula.expression().arity()]; + for (int i = 0; i < exprs1.length; i++) { + exprs2[i] = ctx.mkConst("b" + (i + depth), UNIV); + } + eqs = new BoolExpr[exprs1.length]; + for (int i = 0; i < eqs.length; i++) { + eqs[i] = ctx.mkEq(exprs1[i], exprs2[i]); + } + + allExprs = new Expr[exprs1.length + exprs2.length]; + System.arraycopy(exprs1, 0, allExprs, 0, exprs1.length); + System.arraycopy(exprs2, 0, allExprs, exprs1.length, exprs2.length); + + return ctx.mkForall(allExprs + , ctx.mkImplies( + ctx.mkAnd(visit(multiplicityFormula.expression(), depth, exprs1) + , visit(multiplicityFormula.expression(), depth, exprs2)) + , ctx.mkAnd(eqs)) + , 0, null, null, ctx.mkSymbol(quantifierPrefix + quantifierID++), null); + } + } + else if (node instanceof QuantifiedFormula) { + QuantifiedFormula quantifiedFormula = (QuantifiedFormula) node; + int exprsSize = quantifiedFormula.decls().size(); + + Expr[] exprs1 = new Expr[exprsSize]; + BoolExpr[] ands = new BoolExpr[exprsSize]; + + for (int i = 0; i < exprsSize; i++) { + Decl decl = quantifiedFormula.decls().get(i); + exprs1[i] = ctx.mkConst(decl.variable().name()/*"x" + (i + depth)*/, UNIV); + variableExprMap.put(decl.variable(), exprs1[i]); + ands[i] = visit(decl.variable().in(decl.expression()), depth + exprsSize, exprs); + } + + switch (quantifiedFormula.quantifier()) { + case ALL: + return ctx.mkForall(exprs1 + , ctx.mkImplies(ctx.mkAnd(ands) + , visit(quantifiedFormula.formula(), depth + exprs1.length, exprs1)) + , 0, null, null, ctx.mkSymbol(quantifierPrefix + quantifierID++), null); + case SOME: + return ctx.mkExists(exprs1 + , ctx.mkImplies(ctx.mkAnd(ands) + , visit(quantifiedFormula.formula(), depth + exprs1.length, exprs1)) + , 0, null, null, ctx.mkSymbol(quantifierPrefix + quantifierID++), ctx.mkSymbol(skolemPrefix + skolemID++)); + } + } + if (node instanceof ConstantFormula) { + ConstantFormula constantFormula = (ConstantFormula) node; + if (constantFormula.booleanValue()) { + return ctx.mkTrue(); + } + else { + return ctx.mkFalse(); + } + } + return ctx.mkTrue(); + } + + @Override + public int numberOfVariables() { + return 0; + } + + @Override + public int numberOfClauses() { + return 0; + } + + @Override + public void addVariables(int numVars) { + + } + + @Override + public boolean addClause(int[] lits) { + return false; + } + + @Override + public boolean solve() throws SATAbortedException { + return false; + } + + @Override + public boolean valueOf(int variable) { + return false; + } + + @Override + public void free() { + + } +} diff --git a/src/kodkod/util/nodes/PrettyPrinter.java b/src/kodkod/util/nodes/PrettyPrinter.java index 8d04341f..2250337f 100644 --- a/src/kodkod/util/nodes/PrettyPrinter.java +++ b/src/kodkod/util/nodes/PrettyPrinter.java @@ -1,769 +1,769 @@ -/* - * Kodkod -- Copyright (c) 2005-present, Emina Torlak - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in - * all copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN - * THE SOFTWARE. - */ -package kodkod.util.nodes; - -import java.util.Iterator; -import java.util.LinkedHashMap; -import java.util.Map; -import java.util.Set; - -import kodkod.ast.BinaryExpression; -import kodkod.ast.BinaryFormula; -import kodkod.ast.BinaryIntExpression; -import kodkod.ast.ComparisonFormula; -import kodkod.ast.Comprehension; -import kodkod.ast.ConstantExpression; -import kodkod.ast.ConstantFormula; -import kodkod.ast.Decl; -import kodkod.ast.Decls; -import kodkod.ast.ExprToIntCast; -import kodkod.ast.Expression; -import kodkod.ast.Formula; -import kodkod.ast.IfExpression; -import kodkod.ast.IfIntExpression; -import kodkod.ast.IntComparisonFormula; -import kodkod.ast.IntConstant; -import kodkod.ast.IntExpression; -import kodkod.ast.IntToExprCast; -import kodkod.ast.LeafExpression; -import kodkod.ast.MultiplicityFormula; -import kodkod.ast.NaryExpression; -import kodkod.ast.NaryFormula; -import kodkod.ast.NaryIntExpression; -import kodkod.ast.Node; -import kodkod.ast.NotFormula; -import kodkod.ast.ProjectExpression; -import kodkod.ast.QuantifiedFormula; -import kodkod.ast.Relation; -import kodkod.ast.RelationPredicate; -import kodkod.ast.SumExpression; -import kodkod.ast.UnaryExpression; -import kodkod.ast.UnaryIntExpression; -import kodkod.ast.Variable; -import kodkod.ast.operator.ExprOperator; -import kodkod.ast.operator.FormulaOperator; -import kodkod.ast.operator.IntOperator; -import kodkod.ast.operator.Multiplicity; -import kodkod.ast.visitor.VoidVisitor; - -/** - * Pretty-prints Kodkod nodes. - * - * @author Emina Torlak - */ -public final class PrettyPrinter { - - /** - * Returns a dot representation of the given node that can be visualized with GraphViz. - * @return a dot representation of the given node that can be visualized with GraphViz. - */ - public static String dotify(Node node) { - return Dotifier.apply(node); - } - /** - * Returns a pretty-printed string representation of the - * given node, with each line offset by at least the given - * number of whitespaces. The line parameter determines the - * length of each pretty-printed line, including the offset. - * @requires 0 <= offset < line - * @return a pretty-printed string representation of the - * given node - */ - public static String print(Node node, int offset, int line) { - final Formatter formatter = new Formatter(offset,line); - node.accept(formatter); - return formatter.tokens.toString(); - } - - /** - * Returns a pretty-printed string representation of the - * given node, with each line offset by at least the given - * number of whitespaces. - * @requires 0 <= offset < 80 - * @return a pretty-printed string representation of the - * given node - */ - public static String print(Node node, int offset) { - return print(node,offset,80); - } - - /** - * Returns a pretty-printed string representation of the - * given formulas, with each line offset by at least the given - * number of whitespaces. - * @requires 0 <= offset < 80 - * @return a pretty-printed string representation of the - * given formulas - */ - public static String print(Set formulas, int offset) { - return print(formulas,offset,80); - } - - /** - * Returns a pretty-printed string representation of the - * given formulas, with each line offset by at least the given - * number of whitespaces. The line parameter determines the - * length of each pretty-printed line, including the offset. - * @requires 0 <= offset < line - * @return a pretty-printed string representation of the - * given formulas - */ - public static String print(Set formulas, int offset, int line) { - final Formatter formatter = new Formatter(offset,line); - for(Formula f : formulas) { - f.accept(formatter); - formatter.newline(); - } - return formatter.tokens.toString(); - } - - - - /** - * Generates a buffer of tokens comprising the string representation - * of a given node. The buffer contains at least the parentheses - * needed to correctly represent the node's tree structure. - * - * @specfield tokens: seq - * @author Emina Torlak - */ - private static class Formatter implements VoidVisitor { - final StringBuilder tokens ; - //final int offset; - private final int lineLength; - private int indent, lineStart; - - /** - * Constructs a new tokenizer. - * @ensures no this.tokens - */ - Formatter(int offset, int line) { - assert offset >= 0 && offset < line; - this.tokens = new StringBuilder(); - //this.offset = offset; - this.lineLength = line; - this.lineStart = 0; - this.indent = offset; - indent(); - } - - /*--------------FORMATTERS---------------*/ - - - /** @ensures this.tokens' = concat [ this.tokens, " ", token, " " ]*/ - private void infix(Object token) { - space(); - tokens.append(token); - space(); - } - - /** @ensures this.tokens' = concat [ this.tokens, token, " " ]*/ - private void keyword(Object token) { - append(token); - space(); - } - - /** @ensures this.tokens' = concat [ this.tokens, ", " ]*/ - private void comma() { - tokens.append(","); - space(); - } - - /** @ensures this.tokens' = concat [ this.tokens, ": " ]*/ - private void colon() { - tokens.append(":"); - space(); - } - - /** @ensures adds this.indent spaces to this.tokens */ - private void indent() { for(int i = 0; i < indent; i++) { space(); } } - - /** @ensures adds newline plus this.indent spaces to this.tokens */ - private void newline() { - tokens.append("\n"); - lineStart = tokens.length(); - indent(); - } - - /** @ensures this.tokens' = concat[ this.tokens, " " ] **/ - private void space() { tokens.append(" "); } - - /** @ensures this.tokens' = concat [ this.tokens, token ]*/ - private void append(Object token) { - final String str = String.valueOf(token); - if ((tokens.length() - lineStart + str.length()) > lineLength) { - newline(); - } - tokens.append(str); - } - - /*--------------LEAVES---------------*/ - /** @ensures this.tokens' = concat[ this.tokens, node ] */ - public void visit(Relation node) { append(node); } - - /** @ensures this.tokens' = concat[ this.tokens, node ] */ - public void visit(Variable node) { append(node); } - - /** @ensures this.tokens' = concat[ this.tokens, node ] */ - public void visit(ConstantExpression node) { append(node); } - - /** @ensures this.tokens' = concat[ this.tokens, node ] */ - public void visit(IntConstant node) { append(node); } - - /** @ensures this.tokens' = concat[ this.tokens, node ] */ - public void visit(ConstantFormula node) { append(node); } - - /*--------------DECLARATIONS---------------*/ - /** - * @ensures this.tokens' = - * concat[ this.tokens, tokenize[ node.variable ], ":", tokenize[ node.expression ] - **/ - public void visit(Decl node) { - node.variable().accept(this); - colon(); - if (node.multiplicity()!=Multiplicity.ONE) { - append(node.multiplicity()); - space(); - } - node.expression().accept(this); - } - - /** - * @ensures this.tokens' = - * concat[ this.tokens, tokenize[ node.declarations[0] ], ",", - * ..., tokenize[ node.declarations[ node.size() - 1 ] ] ] - **/ - public void visit(Decls node) { - Iterator decls = node.iterator(); - decls.next().accept(this); - while(decls.hasNext()) { - comma(); - decls.next().accept(this); - } - } - - /*--------------UNARY NODES---------------*/ - - /** @ensures this.tokenize' = - * (parenthesize => concat [ this.tokens, "(", tokenize[child], ")" ] else - * concat [ this.tokens, tokenize[child] ]*/ - private void visitChild(Node child, boolean parenthesize) { - if (parenthesize) { append("("); } - child.accept(this); - if (parenthesize) { append(")"); } - } - - /** @return true if the given expression should be parenthesized when a - * child of a compound parent */ - private boolean parenthesize(Expression child) { - return child instanceof BinaryExpression || child instanceof IfExpression; - } - - /** @return true if the given expression should be parenthesized when a - * child of a compound parent */ - private boolean parenthesize(IntExpression child) { - return !(child instanceof UnaryIntExpression || - child instanceof IntConstant || - child instanceof ExprToIntCast); - } - - /** @return true if the given formula should be parenthesized when a - * child of a compound parent */ - private boolean parenthesize(Formula child) { - return !(child instanceof NotFormula || child instanceof ConstantFormula || - child instanceof RelationPredicate); - } - - /** @ensures appends the given op and child to this.tokens; the child is - * parenthesized if it's an instance of binary expression or an if expression. **/ - public void visit(UnaryExpression node) { - append(node.op()); - visitChild(node.expression(), parenthesize(node.expression())); - } - - - /** @ensures appends the given op and child to this.tokens; the child is - * parenthesized if it's not an instance of unary int expression or int constant. **/ - public void visit(UnaryIntExpression node) { - final IntExpression child = node.intExpr(); - final IntOperator op = node.op(); - final boolean parens = - (op==IntOperator.ABS) || (op==IntOperator.SGN) || - parenthesize(child); - append(node.op()); - visitChild(child, parens); - } - - /** @ensures appends the given op and child to this.tokens; the child is - * parenthesized if it's not an instance of not formula, constant formula, or - * relation predicate. **/ - public void visit(NotFormula node) { - append("!"); - final boolean pchild = parenthesize(node.formula()); - indent += pchild ? 2 : 1; - visitChild(node.formula(), parenthesize(node.formula())); - indent -= pchild ? 2 : 1; - } - - /** @ensures appends the given op and child to this.tokens; the child is - * parenthesized if it's an instance of binary expression or an if expression. **/ - public void visit(MultiplicityFormula node) { - keyword(node.multiplicity()); - visitChild(node.expression(), parenthesize(node.expression())); - } - - /*--------------BINARY NODES---------------*/ - - /** @return true if the given expression needs to be parenthesized if a - * child of a binary expression with the given operator */ - private boolean parenthesize(ExprOperator op, Expression child) { - return child instanceof IfExpression || - child instanceof NaryExpression || - (child instanceof BinaryExpression && - (op==ExprOperator.JOIN || - ((BinaryExpression)child).op()!=op)); - } - - /** @ensures appends the tokenization of the given node to this.tokens */ - public void visit(BinaryExpression node) { - final ExprOperator op = node.op(); - visitChild(node.left(), parenthesize(op, node.left())); - infix(op); - visitChild(node.right(), parenthesize(op, node.right())); - } - - - - /** @return true if the given operator is associative */ - private boolean associative(IntOperator op) { - switch(op) { - case DIVIDE : case MODULO : case SHA : case SHL : case SHR : return false; - default : return true; - } - } - - /** @return true if the given int expression needs to be parenthesized if a - * child of a binary int expression with the given operator */ - private boolean parenthesize(IntOperator op, IntExpression child) { - return child instanceof SumExpression || - child instanceof IfIntExpression || - child instanceof NaryIntExpression || - (child instanceof BinaryIntExpression && - (!associative(op) || ((BinaryIntExpression)child).op()!=op)); - } - - /** @ensures appends the tokenization of the given node to this.tokens */ - public void visit(BinaryIntExpression node) { - final IntOperator op = node.op(); - visitChild(node.left(), parenthesize(op, node.left())); - infix(op); - visitChild(node.right(), parenthesize(op, node.right())); - } - - /** @return true if the given formula needs to be parenthesized if a - * child of a binary formula with the given operator */ - private boolean parenthesize(FormulaOperator op, Formula child) { - return child instanceof QuantifiedFormula || - //child instanceof NaryFormula || - (child instanceof BinaryFormula && - (op==FormulaOperator.IMPLIES || - ((BinaryFormula)child).op()!=op)); - } - - /** @ensures appends the tokenization of the given node to this.tokens */ - public void visit(BinaryFormula node) { - final FormulaOperator op = node.op(); - final boolean pleft = parenthesize(op, node.left()); - if (pleft) indent++; - visitChild(node.left(), pleft); - if (pleft) indent--; - infix(op); - newline(); - final boolean pright = parenthesize(op, node.right()); - if (pright) indent++; - visitChild(node.right(), pright); - if (pright) indent--; - } - - /** @ensures this.tokens' = concat[ this.tokens, tokenize[node.left], node.op, tokenize[node.right] */ - public void visit(ComparisonFormula node) { - visitChild(node.left(), parenthesize(node.left())); - infix(node.op()); - visitChild(node.right(), parenthesize(node.right())); - } - - /** @ensures this.tokens' = concat[ this.tokens, tokenize[node.left], node.op, tokenize[node.right] */ - public void visit(IntComparisonFormula node) { - visitChild(node.left(), parenthesize(node.left())); - infix(node.op()); - visitChild(node.right(), parenthesize(node.right())); - } - - /*--------------TERNARY NODES---------------*/ - - /** @ensures appends the tokenization of the given node to this.tokens */ - public void visit(IfExpression node) { - visitChild(node.condition(), parenthesize(node.condition())); - infix("=>"); - indent++; - newline(); - visitChild(node.thenExpr(), parenthesize(node.thenExpr())); - infix("else"); - newline(); - visitChild(node.elseExpr(), parenthesize(node.elseExpr())); - indent--; - } - - /** @ensures appends the tokenization of the given node to this.tokens */ - public void visit(IfIntExpression node) { - visitChild(node.condition(), parenthesize(node.condition())); - infix("=>"); - indent++; - newline(); - visitChild(node.thenExpr(), parenthesize(node.thenExpr())); - infix("else"); - newline(); - visitChild(node.elseExpr(), parenthesize(node.elseExpr())); - indent--; - } - - /*--------------VARIABLE CREATOR NODES---------------*/ - /** @ensures this.tokens' = concat[ this.tokens, - * "{", tokenize[node.decls], "|", tokenize[ node.formula ], "}" ]*/ - public void visit(Comprehension node) { - append("{"); - node.decls().accept(this); - infix("|"); - node.formula().accept(this); - append("}"); - } - - /** @ensures this.tokens' = concat[ this.tokens, "sum", - * tokenize[node.decls], "|", tokenize[ node.intExpr ], ]*/ - public void visit(SumExpression node) { - keyword("sum"); - node.decls().accept(this); - infix("|"); - node.intExpr().accept(this); - } - - /** @ensures this.tokens' = concat[ this.tokens, node.quantifier, - * tokenize[node.decls], "|", tokenize[ node.formula ] ]*/ - public void visit(QuantifiedFormula node) { - keyword(node.quantifier()); - node.decls().accept(this); - infix("|"); - indent++; - newline(); - node.formula().accept(this); - indent--; - } - - /*--------------NARY NODES---------------*/ - - /** @ensures appends the tokenization of the given node to this.tokens */ - public void visit(NaryExpression node) { - final ExprOperator op = node.op(); - visitChild(node.child(0), parenthesize(op, node.child(0))); - for(int i = 1, size = node.size(); i < size; i++) { - infix(op); - visitChild(node.child(i), parenthesize(op, node.child(i))); - } - } - /** @ensures appends the tokenization of the given node to this.tokens */ - public void visit(NaryIntExpression node) { - final IntOperator op = node.op(); - visitChild(node.child(0), parenthesize(op, node.child(0))); - for(int i = 1, size = node.size(); i < size; i++) { - infix(op); - visitChild(node.child(i), parenthesize(op, node.child(i))); - } - } - /** @ensures appends the tokenization of the given node to this.tokens */ - public void visit(NaryFormula node) { - final FormulaOperator op = node.op(); - boolean parens = parenthesize(op, node.child(0)); - if (parens) indent++; - visitChild(node.child(0), parens); - if (parens) indent--; - for(int i = 1, size = node.size(); i < size; i++) { - infix(op); - newline(); - parens = parenthesize(op, node.child(i)); - if (parens) indent++; - visitChild(node.child(i), parens); - if (parens) indent--; - } - } - /*--------------OTHER NODES---------------*/ - - /** @ensures appends the tokenization of the given node to this.tokens */ - public void visit(ProjectExpression node) { - append("project"); - append("["); - node.expression().accept(this); - comma(); - append("<"); - final Iterator cols = node.columns(); - cols.next().accept(this); - while(cols.hasNext()) { - comma(); - cols.next().accept(this); - } - append(">"); - append("]"); - } - - /** @ensures this.tokens' = concat[ this.tokens, "Int","[", - * tokenize[node.intExpr], "]" ] **/ - public void visit(IntToExprCast node) { - append("Int"); - append("["); - node.intExpr().accept(this); - append("]"); - } - - /** @ensures this.tokens' = concat[ this.tokens, "int","[", - * tokenize[node.expression], "]" ] **/ - public void visit(ExprToIntCast node) { - switch(node.op()) { - case SUM: - append("int"); - append("["); - node.expression().accept(this); - append("]"); - break; - case CARDINALITY : - append("#"); - append("("); - node.expression().accept(this); - append(")"); - break; - default : throw new IllegalArgumentException("unknown operator: " + node.op()); - } - - } - - /** @ensures appends the tokenization of the given node to this.tokens */ - public void visit(RelationPredicate node) { - switch(node.name()) { - case ACYCLIC : - append("acyclic"); - append("["); - node.relation().accept(this); - append("]"); - break; - case FUNCTION : - RelationPredicate.Function func = (RelationPredicate.Function)node; - append("function"); - append("["); - func.relation().accept(this); - colon(); - func.domain().accept(this); - infix("->"); - keyword(func.targetMult()); - func.range().accept(this); - append("]"); - break; - case TOTAL_ORDERING : - RelationPredicate.TotalOrdering ord = (RelationPredicate.TotalOrdering)node; - append("ord"); - append("["); - ord.relation().accept(this); - comma(); - ord.ordered().accept(this); - comma(); - ord.first().accept(this); - comma(); - ord.last().accept(this); - append("]"); - break; - default: - throw new AssertionError("unreachable"); - } - - } - - } - - private static class Dotifier implements VoidVisitor { - private final StringBuilder graph = new StringBuilder(); - private final Map ids = new LinkedHashMap(); - - static String apply(Node node) { - final Dotifier dot = new Dotifier(); - dot.graph.append("digraph {\n"); - node.accept(dot); - dot.graph.append("}"); - return dot.graph.toString(); - } - - - private boolean visited(Node n) { - if (ids.containsKey(n)) return true; - ids.put(n, ids.size()); - return false; - } - - private String id(Node n) { return "N" + ids.get(n); } - - private void node(Node n, String label) { - graph.append(id(n)); - graph.append("[ label=\"" ); - graph.append(ids.get(n)); - graph.append("("); - graph.append(label); - graph.append(")\"];\n"); - } - - private void edge(Node n1, Node n2) { - if (n2 instanceof LeafExpression || n2 instanceof ConstantFormula || n2 instanceof IntConstant) { - - } - graph.append(id(n1)); - graph.append("->"); - graph.append(id(n2)); - graph.append(";\n"); - } - - private void visit(Node parent, Object label) { - if (visited(parent)) return; - node(parent, label.toString()); - } - - private void visit(Node parent, Object label, Node child) { - if (visited(parent)) return; - node(parent, label.toString()); - child.accept(this); - edge(parent, child); - } - - private void visit(Node parent, Object label, Node left, Node right) { - if (visited(parent)) return; - node(parent, label.toString()); - left.accept(this); - right.accept(this); - edge(parent, left); - edge(parent, right); - } - - private void visit(Node parent, Object label, Node left, Node middle, Node right) { - if (visited(parent)) return; - node(parent, label.toString()); - left.accept(this); - middle.accept(this); - right.accept(this); - edge(parent, left); - edge(parent, middle); - edge(parent, right); - } - - private void visit(Node parent, Object label, Iterator children) { - if (visited(parent)) return; - node(parent, label.toString()); - while(children.hasNext()) { - Node child = children.next(); - child.accept(this); - edge(parent, child); - } - } - - private void visit(Node parent, Object label, Node child, Iterator children) { - if (visited(parent)) return; - node(parent, label.toString()); - child.accept(this); - edge(parent, child); - while(children.hasNext()) { - Node other = children.next(); - other.accept(this); - edge(parent, other); - } - } - - public void visit(Decls decls) { visit(decls, "decls", decls.iterator()); } - - public void visit(Decl decl) { visit(decl, "decl", decl.variable(), decl.expression()); } - - public void visit(Relation relation) { visit(relation, relation.name()); } - public void visit(Variable variable) { visit(variable, variable.name()); } - public void visit(ConstantExpression constExpr) { visit(constExpr, constExpr.name()); } - - - public void visit(NaryExpression expr) { - visit(expr, expr.op(), expr.iterator()); - } - public void visit(BinaryExpression binExpr) { - visit(binExpr, binExpr.op(), binExpr.left(), binExpr.right()); - } - public void visit(UnaryExpression unaryExpr) { - visit(unaryExpr, unaryExpr.op(), unaryExpr.expression()); - } - public void visit(Comprehension comprehension) { - visit(comprehension, "setcomp", comprehension.decls(), comprehension.formula()); - } - public void visit(IfExpression ifExpr) { - visit(ifExpr, "ite", ifExpr.condition(), ifExpr.thenExpr(), ifExpr.elseExpr()); - } - public void visit(ProjectExpression project) { - visit(project, "proj", project.expression(), project.columns()); - } - - public void visit(IntToExprCast castExpr) { visit(castExpr, castExpr.op(), castExpr.intExpr()); } - public void visit(IntConstant intConst) { visit(intConst, intConst.value()); } - - public void visit(IfIntExpression intExpr) { - visit(intExpr, "ite", intExpr.condition(), intExpr.thenExpr(), intExpr.elseExpr()); - } - public void visit(ExprToIntCast intExpr) { visit(intExpr, intExpr.op(), intExpr.expression()); } - public void visit(NaryIntExpression intExpr) { visit(intExpr, intExpr.op(), intExpr.iterator());} - public void visit(BinaryIntExpression intExpr) { visit(intExpr, intExpr.op(), intExpr.left(), intExpr.right()); } - public void visit(UnaryIntExpression intExpr) { visit(intExpr, intExpr.op(), intExpr.intExpr());} - public void visit(SumExpression intExpr) { visit(intExpr, "sum", intExpr.decls(), intExpr.intExpr()); } - - public void visit(IntComparisonFormula intComp) { visit(intComp, intComp.op(), intComp.left(), intComp.right());} - public void visit(QuantifiedFormula quantFormula) { - visit(quantFormula, quantFormula.quantifier(), quantFormula.decls(), quantFormula.formula()); - } - public void visit(NaryFormula formula) { visit(formula, formula.op(), formula.iterator()); } - public void visit(BinaryFormula binFormula) { visit(binFormula, binFormula.op(), binFormula.left(), binFormula.right()); } - public void visit(NotFormula not) { visit(not, "not", not.formula()); } - public void visit(ConstantFormula constant) { visit(constant, constant.booleanValue()); } - public void visit(ComparisonFormula compFormula) { visit(compFormula, compFormula.op(), compFormula.left(), compFormula.right());} - public void visit(MultiplicityFormula multFormula) { - visit(multFormula, multFormula.multiplicity(), multFormula.expression()); - } - public void visit(RelationPredicate pred) { - if (visited(pred)) return; - - if (pred.name()==RelationPredicate.Name.FUNCTION) { - final RelationPredicate.Function fp = (RelationPredicate.Function) pred; - visit(fp, fp.name(), fp.domain(), fp.range() ); - } else if (pred.name()==RelationPredicate.Name.TOTAL_ORDERING) { - final RelationPredicate.TotalOrdering tp = (RelationPredicate.TotalOrdering) pred; - visit(tp, tp.name(), tp.ordered(), tp.first(), tp.last() ); - } else { - throw new IllegalArgumentException("Unknown predicate: " + pred); - } - } - - } -} +/* + * Kodkod -- Copyright (c) 2005-present, Emina Torlak + * + * Permission is hereby granted, free of charge, to any person obtaining a copy + * of this software and associated documentation files (the "Software"), to deal + * in the Software without restriction, including without limitation the rights + * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + * copies of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in + * all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN + * THE SOFTWARE. + */ +package kodkod.util.nodes; + +import java.util.Iterator; +import java.util.LinkedHashMap; +import java.util.Map; +import java.util.Set; + +import kodkod.ast.BinaryExpression; +import kodkod.ast.BinaryFormula; +import kodkod.ast.BinaryIntExpression; +import kodkod.ast.ComparisonFormula; +import kodkod.ast.Comprehension; +import kodkod.ast.ConstantExpression; +import kodkod.ast.ConstantFormula; +import kodkod.ast.Decl; +import kodkod.ast.Decls; +import kodkod.ast.ExprToIntCast; +import kodkod.ast.Expression; +import kodkod.ast.Formula; +import kodkod.ast.IfExpression; +import kodkod.ast.IfIntExpression; +import kodkod.ast.IntComparisonFormula; +import kodkod.ast.IntConstant; +import kodkod.ast.IntExpression; +import kodkod.ast.IntToExprCast; +import kodkod.ast.LeafExpression; +import kodkod.ast.MultiplicityFormula; +import kodkod.ast.NaryExpression; +import kodkod.ast.NaryFormula; +import kodkod.ast.NaryIntExpression; +import kodkod.ast.Node; +import kodkod.ast.NotFormula; +import kodkod.ast.ProjectExpression; +import kodkod.ast.QuantifiedFormula; +import kodkod.ast.Relation; +import kodkod.ast.RelationPredicate; +import kodkod.ast.SumExpression; +import kodkod.ast.UnaryExpression; +import kodkod.ast.UnaryIntExpression; +import kodkod.ast.Variable; +import kodkod.ast.operator.ExprOperator; +import kodkod.ast.operator.FormulaOperator; +import kodkod.ast.operator.IntOperator; +import kodkod.ast.operator.Multiplicity; +import kodkod.ast.visitor.VoidVisitor; + +/** + * Pretty-prints Kodkod nodes. + * + * @author Emina Torlak + */ +public final class PrettyPrinter { + + /** + * Returns a dot representation of the given node that can be visualized with GraphViz. + * @return a dot representation of the given node that can be visualized with GraphViz. + */ + public static String dotify(Node node) { + return Dotifier.apply(node); + } + /** + * Returns a pretty-printed string representation of the + * given node, with each line offset by at least the given + * number of whitespaces. The line parameter determines the + * length of each pretty-printed line, including the offset. + * @requires 0 <= offset < line + * @return a pretty-printed string representation of the + * given node + */ + public static String print(Node node, int offset, int line) { + final Formatter formatter = new Formatter(offset,line); + node.accept(formatter); + return formatter.tokens.toString(); + } + + /** + * Returns a pretty-printed string representation of the + * given node, with each line offset by at least the given + * number of whitespaces. + * @requires 0 <= offset < 80 + * @return a pretty-printed string representation of the + * given node + */ + public static String print(Node node, int offset) { + return print(node,offset,80); + } + + /** + * Returns a pretty-printed string representation of the + * given formulas, with each line offset by at least the given + * number of whitespaces. + * @requires 0 <= offset < 80 + * @return a pretty-printed string representation of the + * given formulas + */ + public static String print(Set formulas, int offset) { + return print(formulas,offset,80); + } + + /** + * Returns a pretty-printed string representation of the + * given formulas, with each line offset by at least the given + * number of whitespaces. The line parameter determines the + * length of each pretty-printed line, including the offset. + * @requires 0 <= offset < line + * @return a pretty-printed string representation of the + * given formulas + */ + public static String print(Set formulas, int offset, int line) { + final Formatter formatter = new Formatter(offset,line); + for(Formula f : formulas) { + f.accept(formatter); + formatter.newline(); + } + return formatter.tokens.toString(); + } + + + + /** + * Generates a buffer of tokens comprising the string representation + * of a given node. The buffer contains at least the parentheses + * needed to correctly represent the node's tree structure. + * + * @specfield tokens: seq + * @author Emina Torlak + */ + private static class Formatter implements VoidVisitor { + final StringBuilder tokens ; + //final int offset; + private final int lineLength; + private int indent, lineStart; + + /** + * Constructs a new tokenizer. + * @ensures no this.tokens + */ + Formatter(int offset, int line) { + assert offset >= 0 && offset < line; + this.tokens = new StringBuilder(); + //this.offset = offset; + this.lineLength = line; + this.lineStart = 0; + this.indent = offset; + indent(); + } + + /*--------------FORMATTERS---------------*/ + + + /** @ensures this.tokens' = concat [ this.tokens, " ", token, " " ]*/ + private void infix(Object token) { + space(); + tokens.append(token); + space(); + } + + /** @ensures this.tokens' = concat [ this.tokens, token, " " ]*/ + private void keyword(Object token) { + append(token); + space(); + } + + /** @ensures this.tokens' = concat [ this.tokens, ", " ]*/ + private void comma() { + tokens.append(","); + space(); + } + + /** @ensures this.tokens' = concat [ this.tokens, ": " ]*/ + private void colon() { + tokens.append(":"); + space(); + } + + /** @ensures adds this.indent spaces to this.tokens */ + private void indent() { for(int i = 0; i < indent; i++) { space(); } } + + /** @ensures adds newline plus this.indent spaces to this.tokens */ + private void newline() { + tokens.append("\n"); + lineStart = tokens.length(); + indent(); + } + + /** @ensures this.tokens' = concat[ this.tokens, " " ] **/ + private void space() { tokens.append(" "); } + + /** @ensures this.tokens' = concat [ this.tokens, token ]*/ + private void append(Object token) { + final String str = String.valueOf(token); + if ((tokens.length() - lineStart + str.length()) > lineLength) { + newline(); + } + tokens.append(str); + } + + /*--------------LEAVES---------------*/ + /** @ensures this.tokens' = concat[ this.tokens, node ] */ + public void visit(Relation node) { append(node); } + + /** @ensures this.tokens' = concat[ this.tokens, node ] */ + public void visit(Variable node) { append(node); } + + /** @ensures this.tokens' = concat[ this.tokens, node ] */ + public void visit(ConstantExpression node) { append(node); } + + /** @ensures this.tokens' = concat[ this.tokens, node ] */ + public void visit(IntConstant node) { append(node); } + + /** @ensures this.tokens' = concat[ this.tokens, node ] */ + public void visit(ConstantFormula node) { append(node); } + + /*--------------DECLARATIONS---------------*/ + /** + * @ensures this.tokens' = + * concat[ this.tokens, tokenize[ node.variable ], ":", tokenize[ node.expression ] + **/ + public void visit(Decl node) { + node.variable().accept(this); + colon(); + if (node.multiplicity()!=Multiplicity.ONE) { + append(node.multiplicity()); + space(); + } + node.expression().accept(this); + } + + /** + * @ensures this.tokens' = + * concat[ this.tokens, tokenize[ node.declarations[0] ], ",", + * ..., tokenize[ node.declarations[ node.size() - 1 ] ] ] + **/ + public void visit(Decls node) { + Iterator decls = node.iterator(); + decls.next().accept(this); + while(decls.hasNext()) { + comma(); + decls.next().accept(this); + } + } + + /*--------------UNARY NODES---------------*/ + + /** @ensures this.tokenize' = + * (parenthesize => concat [ this.tokens, "(", tokenize[child], ")" ] else + * concat [ this.tokens, tokenize[child] ]*/ + private void visitChild(Node child, boolean parenthesize) { + if (parenthesize) { append("("); } + child.accept(this); + if (parenthesize) { append(")"); } + } + + /** @return true if the given expression should be parenthesized when a + * child of a compound parent */ + private boolean parenthesize(Expression child) { + return child instanceof BinaryExpression || child instanceof IfExpression; + } + + /** @return true if the given expression should be parenthesized when a + * child of a compound parent */ + private boolean parenthesize(IntExpression child) { + return !(child instanceof UnaryIntExpression || + child instanceof IntConstant || + child instanceof ExprToIntCast); + } + + /** @return true if the given formula should be parenthesized when a + * child of a compound parent */ + private boolean parenthesize(Formula child) { + return !(child instanceof NotFormula || child instanceof ConstantFormula || + child instanceof RelationPredicate); + } + + /** @ensures appends the given op and child to this.tokens; the child is + * parenthesized if it's an instance of binary expression or an if expression. **/ + public void visit(UnaryExpression node) { + append(node.op()); + visitChild(node.expression(), parenthesize(node.expression())); + } + + + /** @ensures appends the given op and child to this.tokens; the child is + * parenthesized if it's not an instance of unary int expression or int constant. **/ + public void visit(UnaryIntExpression node) { + final IntExpression child = node.intExpr(); + final IntOperator op = node.op(); + final boolean parens = + (op==IntOperator.ABS) || (op==IntOperator.SGN) || + parenthesize(child); + append(node.op()); + visitChild(child, parens); + } + + /** @ensures appends the given op and child to this.tokens; the child is + * parenthesized if it's not an instance of not formula, constant formula, or + * relation predicate. **/ + public void visit(NotFormula node) { + append("!"); + final boolean pchild = parenthesize(node.formula()); + indent += pchild ? 2 : 1; + visitChild(node.formula(), parenthesize(node.formula())); + indent -= pchild ? 2 : 1; + } + + /** @ensures appends the given op and child to this.tokens; the child is + * parenthesized if it's an instance of binary expression or an if expression. **/ + public void visit(MultiplicityFormula node) { + keyword(node.multiplicity()); + visitChild(node.expression(), parenthesize(node.expression())); + } + + /*--------------BINARY NODES---------------*/ + + /** @return true if the given expression needs to be parenthesized if a + * child of a binary expression with the given operator */ + private boolean parenthesize(ExprOperator op, Expression child) { + return child instanceof IfExpression || + child instanceof NaryExpression || + (child instanceof BinaryExpression && + (op==ExprOperator.JOIN || + ((BinaryExpression)child).op()!=op)); + } + + /** @ensures appends the tokenization of the given node to this.tokens */ + public void visit(BinaryExpression node) { + final ExprOperator op = node.op(); + visitChild(node.left(), parenthesize(op, node.left())); + infix(op); + visitChild(node.right(), parenthesize(op, node.right())); + } + + + + /** @return true if the given operator is associative */ + private boolean associative(IntOperator op) { + switch(op) { + case DIVIDE : case MODULO : case SHA : case SHL : case SHR : return false; + default : return true; + } + } + + /** @return true if the given int expression needs to be parenthesized if a + * child of a binary int expression with the given operator */ + private boolean parenthesize(IntOperator op, IntExpression child) { + return child instanceof SumExpression || + child instanceof IfIntExpression || + child instanceof NaryIntExpression || + (child instanceof BinaryIntExpression && + (!associative(op) || ((BinaryIntExpression)child).op()!=op)); + } + + /** @ensures appends the tokenization of the given node to this.tokens */ + public void visit(BinaryIntExpression node) { + final IntOperator op = node.op(); + visitChild(node.left(), parenthesize(op, node.left())); + infix(op); + visitChild(node.right(), parenthesize(op, node.right())); + } + + /** @return true if the given formula needs to be parenthesized if a + * child of a binary formula with the given operator */ + private boolean parenthesize(FormulaOperator op, Formula child) { + return child instanceof QuantifiedFormula || + //child instanceof NaryFormula || + (child instanceof BinaryFormula && + (op==FormulaOperator.IMPLIES || + ((BinaryFormula)child).op()!=op)); + } + + /** @ensures appends the tokenization of the given node to this.tokens */ + public void visit(BinaryFormula node) { + final FormulaOperator op = node.op(); + final boolean pleft = parenthesize(op, node.left()); + if (pleft) indent++; + visitChild(node.left(), pleft); + if (pleft) indent--; + infix(op); + newline(); + final boolean pright = parenthesize(op, node.right()); + if (pright) indent++; + visitChild(node.right(), pright); + if (pright) indent--; + } + + /** @ensures this.tokens' = concat[ this.tokens, tokenize[node.left], node.op, tokenize[node.right] */ + public void visit(ComparisonFormula node) { + visitChild(node.left(), parenthesize(node.left())); + infix(node.op()); + visitChild(node.right(), parenthesize(node.right())); + } + + /** @ensures this.tokens' = concat[ this.tokens, tokenize[node.left], node.op, tokenize[node.right] */ + public void visit(IntComparisonFormula node) { + visitChild(node.left(), parenthesize(node.left())); + infix(node.op()); + visitChild(node.right(), parenthesize(node.right())); + } + + /*--------------TERNARY NODES---------------*/ + + /** @ensures appends the tokenization of the given node to this.tokens */ + public void visit(IfExpression node) { + visitChild(node.condition(), parenthesize(node.condition())); + infix("=>"); + indent++; + newline(); + visitChild(node.thenExpr(), parenthesize(node.thenExpr())); + infix("else"); + newline(); + visitChild(node.elseExpr(), parenthesize(node.elseExpr())); + indent--; + } + + /** @ensures appends the tokenization of the given node to this.tokens */ + public void visit(IfIntExpression node) { + visitChild(node.condition(), parenthesize(node.condition())); + infix("=>"); + indent++; + newline(); + visitChild(node.thenExpr(), parenthesize(node.thenExpr())); + infix("else"); + newline(); + visitChild(node.elseExpr(), parenthesize(node.elseExpr())); + indent--; + } + + /*--------------VARIABLE CREATOR NODES---------------*/ + /** @ensures this.tokens' = concat[ this.tokens, + * "{", tokenize[node.decls], "|", tokenize[ node.formula ], "}" ]*/ + public void visit(Comprehension node) { + append("{"); + node.decls().accept(this); + infix("|"); + node.formula().accept(this); + append("}"); + } + + /** @ensures this.tokens' = concat[ this.tokens, "sum", + * tokenize[node.decls], "|", tokenize[ node.intExpr ], ]*/ + public void visit(SumExpression node) { + keyword("sum"); + node.decls().accept(this); + infix("|"); + node.intExpr().accept(this); + } + + /** @ensures this.tokens' = concat[ this.tokens, node.quantifier, + * tokenize[node.decls], "|", tokenize[ node.formula ] ]*/ + public void visit(QuantifiedFormula node) { + keyword(node.quantifier()); + node.decls().accept(this); + infix("|"); + indent++; + newline(); + node.formula().accept(this); + indent--; + } + + /*--------------NARY NODES---------------*/ + + /** @ensures appends the tokenization of the given node to this.tokens */ + public void visit(NaryExpression node) { + final ExprOperator op = node.op(); + visitChild(node.child(0), parenthesize(op, node.child(0))); + for(int i = 1, size = node.size(); i < size; i++) { + infix(op); + visitChild(node.child(i), parenthesize(op, node.child(i))); + } + } + /** @ensures appends the tokenization of the given node to this.tokens */ + public void visit(NaryIntExpression node) { + final IntOperator op = node.op(); + visitChild(node.child(0), parenthesize(op, node.child(0))); + for(int i = 1, size = node.size(); i < size; i++) { + infix(op); + visitChild(node.child(i), parenthesize(op, node.child(i))); + } + } + /** @ensures appends the tokenization of the given node to this.tokens */ + public void visit(NaryFormula node) { + final FormulaOperator op = node.op(); + boolean parens = parenthesize(op, node.child(0)); + if (parens) indent++; + visitChild(node.child(0), parens); + if (parens) indent--; + for(int i = 1, size = node.size(); i < size; i++) { + infix(op); + newline(); + parens = parenthesize(op, node.child(i)); + if (parens) indent++; + visitChild(node.child(i), parens); + if (parens) indent--; + } + } + /*--------------OTHER NODES---------------*/ + + /** @ensures appends the tokenization of the given node to this.tokens */ + public void visit(ProjectExpression node) { + append("project"); + append("["); + node.expression().accept(this); + comma(); + append("<"); + final Iterator cols = node.columns(); + cols.next().accept(this); + while(cols.hasNext()) { + comma(); + cols.next().accept(this); + } + append(">"); + append("]"); + } + + /** @ensures this.tokens' = concat[ this.tokens, "Int","[", + * tokenize[node.intExpr], "]" ] **/ + public void visit(IntToExprCast node) { + append("Int"); + append("["); + node.intExpr().accept(this); + append("]"); + } + + /** @ensures this.tokens' = concat[ this.tokens, "int","[", + * tokenize[node.expression], "]" ] **/ + public void visit(ExprToIntCast node) { + switch(node.op()) { + case SUM: + append("int"); + append("["); + node.expression().accept(this); + append("]"); + break; + case CARDINALITY : + append("#"); + append("("); + node.expression().accept(this); + append(")"); + break; + default : throw new IllegalArgumentException("unknown operator: " + node.op()); + } + + } + + /** @ensures appends the tokenization of the given node to this.tokens */ + public void visit(RelationPredicate node) { + switch(node.name()) { + case ACYCLIC : + append("acyclic"); + append("["); + node.relation().accept(this); + append("]"); + break; + case FUNCTION : + RelationPredicate.Function func = (RelationPredicate.Function)node; + append("function"); + append("["); + func.relation().accept(this); + colon(); + func.domain().accept(this); + infix("->"); + keyword(func.targetMult()); + func.range().accept(this); + append("]"); + break; + case TOTAL_ORDERING : + RelationPredicate.TotalOrdering ord = (RelationPredicate.TotalOrdering)node; + append("ord"); + append("["); + ord.relation().accept(this); + comma(); + ord.ordered().accept(this); + comma(); + ord.first().accept(this); + comma(); + ord.last().accept(this); + append("]"); + break; + default: + throw new AssertionError("unreachable"); + } + + } + + } + + private static class Dotifier implements VoidVisitor { + private final StringBuilder graph = new StringBuilder(); + private final Map ids = new LinkedHashMap(); + + static String apply(Node node) { + final Dotifier dot = new Dotifier(); + dot.graph.append("digraph {\n"); + node.accept(dot); + dot.graph.append("}"); + return dot.graph.toString(); + } + + + private boolean visited(Node n) { + if (ids.containsKey(n)) return true; + ids.put(n, ids.size()); + return false; + } + + private String id(Node n) { return "N" + ids.get(n); } + + private void node(Node n, String label) { + graph.append(id(n)); + graph.append("[ label=\"" ); + graph.append(ids.get(n)); + graph.append("("); + graph.append(label); + graph.append(")\"];\n"); + } + + private void edge(Node n1, Node n2) { + if (n2 instanceof LeafExpression || n2 instanceof ConstantFormula || n2 instanceof IntConstant) { + + } + graph.append(id(n1)); + graph.append("->"); + graph.append(id(n2)); + graph.append(";\n"); + } + + private void visit(Node parent, Object label) { + if (visited(parent)) return; + node(parent, label.toString()); + } + + private void visit(Node parent, Object label, Node child) { + if (visited(parent)) return; + node(parent, label.toString()); + child.accept(this); + edge(parent, child); + } + + private void visit(Node parent, Object label, Node left, Node right) { + if (visited(parent)) return; + node(parent, label.toString()); + left.accept(this); + right.accept(this); + edge(parent, left); + edge(parent, right); + } + + private void visit(Node parent, Object label, Node left, Node middle, Node right) { + if (visited(parent)) return; + node(parent, label.toString()); + left.accept(this); + middle.accept(this); + right.accept(this); + edge(parent, left); + edge(parent, middle); + edge(parent, right); + } + + private void visit(Node parent, Object label, Iterator children) { + if (visited(parent)) return; + node(parent, label.toString()); + while(children.hasNext()) { + Node child = children.next(); + child.accept(this); + edge(parent, child); + } + } + + private void visit(Node parent, Object label, Node child, Iterator children) { + if (visited(parent)) return; + node(parent, label.toString()); + child.accept(this); + edge(parent, child); + while(children.hasNext()) { + Node other = children.next(); + other.accept(this); + edge(parent, other); + } + } + + public void visit(Decls decls) { visit(decls, "decls", decls.iterator()); } + + public void visit(Decl decl) { visit(decl, "decl", decl.variable(), decl.expression()); } + + public void visit(Relation relation) { visit(relation, relation.name()); } + public void visit(Variable variable) { visit(variable, variable.name()); } + public void visit(ConstantExpression constExpr) { visit(constExpr, constExpr.name()); } + + + public void visit(NaryExpression expr) { + visit(expr, expr.op(), expr.iterator()); + } + public void visit(BinaryExpression binExpr) { + visit(binExpr, binExpr.op(), binExpr.left(), binExpr.right()); + } + public void visit(UnaryExpression unaryExpr) { + visit(unaryExpr, unaryExpr.op(), unaryExpr.expression()); + } + public void visit(Comprehension comprehension) { + visit(comprehension, "setcomp", comprehension.decls(), comprehension.formula()); + } + public void visit(IfExpression ifExpr) { + visit(ifExpr, "ite", ifExpr.condition(), ifExpr.thenExpr(), ifExpr.elseExpr()); + } + public void visit(ProjectExpression project) { + visit(project, "proj", project.expression(), project.columns()); + } + + public void visit(IntToExprCast castExpr) { visit(castExpr, castExpr.op(), castExpr.intExpr()); } + public void visit(IntConstant intConst) { visit(intConst, intConst.value()); } + + public void visit(IfIntExpression intExpr) { + visit(intExpr, "ite", intExpr.condition(), intExpr.thenExpr(), intExpr.elseExpr()); + } + public void visit(ExprToIntCast intExpr) { visit(intExpr, intExpr.op(), intExpr.expression()); } + public void visit(NaryIntExpression intExpr) { visit(intExpr, intExpr.op(), intExpr.iterator());} + public void visit(BinaryIntExpression intExpr) { visit(intExpr, intExpr.op(), intExpr.left(), intExpr.right()); } + public void visit(UnaryIntExpression intExpr) { visit(intExpr, intExpr.op(), intExpr.intExpr());} + public void visit(SumExpression intExpr) { visit(intExpr, "sum", intExpr.decls(), intExpr.intExpr()); } + + public void visit(IntComparisonFormula intComp) { visit(intComp, intComp.op(), intComp.left(), intComp.right());} + public void visit(QuantifiedFormula quantFormula) { + visit(quantFormula, quantFormula.quantifier(), quantFormula.decls(), quantFormula.formula()); + } + public void visit(NaryFormula formula) { visit(formula, formula.op(), formula.iterator()); } + public void visit(BinaryFormula binFormula) { visit(binFormula, binFormula.op(), binFormula.left(), binFormula.right()); } + public void visit(NotFormula not) { visit(not, "not", not.formula()); } + public void visit(ConstantFormula constant) { visit(constant, constant.booleanValue()); } + public void visit(ComparisonFormula compFormula) { visit(compFormula, compFormula.op(), compFormula.left(), compFormula.right());} + public void visit(MultiplicityFormula multFormula) { + visit(multFormula, multFormula.multiplicity(), multFormula.expression()); + } + public void visit(RelationPredicate pred) { + if (visited(pred)) return; + + if (pred.name()==RelationPredicate.Name.FUNCTION) { + final RelationPredicate.Function fp = (RelationPredicate.Function) pred; + visit(fp, fp.name(), fp.domain(), fp.range() ); + } else if (pred.name()==RelationPredicate.Name.TOTAL_ORDERING) { + final RelationPredicate.TotalOrdering tp = (RelationPredicate.TotalOrdering) pred; + visit(tp, tp.name(), tp.ordered(), tp.first(), tp.last() ); + } else { + throw new IllegalArgumentException("Unknown predicate: " + pred); + } + } + + } +}