Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving

  • Jeroen BransenEmail author
  • L. Thomas van Binsbergen
  • Koen Claessen
  • Atze Dijkstra
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9035)


Many computations over trees can be specified using attribute grammars. Compilers for attribute grammars need to find an evaluation order (or schedule) in order to generate efficient code. For the class of linearly ordered attribute grammars such a schedule can be found statically, but this problem is known to be NP-hard.

In this paper, we show how to encode linearly ordered attribute grammar scheduling as a SAT-problem. For such grammars it is necessary to ensure that the dependency graph is cycle free, which we approach in a novel way by transforming the dependency graph to a chordal graph allowing the cycle freeness to be efficiently expressed and computed using SAT solvers.

There are two main advantages to using a SAT-solver for scheduling: (1) the scheduling algorithm runs faster than existing scheduling algorithms on real-world examples, and (2) by adding extra constraints we obtain fine-grained control over the resulting schedule, thereby enabling new scheduling optimisations.


Attribute Grammars static analysis SAT-solving 


  1. [van Binsbergen et al., 2015]
    van Binsbergen, L.T., Bransen, J., Dijkstra, A.: Linearly ordered attribute grammars: With automatic augmenting dependency selection. In: Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, PEPM 2015, pp. 49–60. ACM, New York (2015)CrossRefGoogle Scholar
  2. [Bird, 1984]
    Bird, R.S.: Using circular programs to eliminate multiple traversals of data. Acta Informatica 21, 239–250 (1984)CrossRefzbMATHGoogle Scholar
  3. [Bransen et al., 2012]
    Bransen, J., Middelkoop, A., Dijkstra, A., Swierstra, S.D.: The Kennedy-Warren algorithm revisited: Ordering attribute grammars. In: Russo, C., Zhou, N.-F. (eds.) PADL 2012. LNCS, vol. 7149, pp. 183–197. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  4. [Bryant and Velev, 2002]
    Bryant, R.E., Velev, M.N.: Boolean satisfiability with transitivity constraints. ACM Trans. Comput. Logic 3(4), 604–627 (2002)CrossRefMathSciNetGoogle Scholar
  5. [Claessen et al., 2009]
    Claessen, K., Een, N., Sheeran, M., Sörensson, N., Voronov, A., Åkesson, K.: Sat-solving in practice. Discrete Event Dynamic Systems 19(4), 495–524 (2009)CrossRefzbMATHMathSciNetGoogle Scholar
  6. [Swierstra et al., 1999]
    Codish, M., Zazon-Ivry, M.: Pairwise cardinality networks. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 154–172. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  7. [Cook, 1971]
    Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing, STOC 1971, pp. 151–158. ACM, New York (1971)CrossRefGoogle Scholar
  8. [Dijkstra et al., 2009]
    Dijkstra, A., Fokker, J., Swierstra, S.D.: The architecture of the Utrecht Haskell Compiler. In: Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell, Haskell 2009, pp. 93–104. ACM, New York (2009)Google Scholar
  9. [Dirac, 1961]
    Dirac, G.A.: On rigid circuit graphs. Abh. Math. Sem. Univ. Hamburg 25, 71–76 (1961)CrossRefzbMATHMathSciNetGoogle Scholar
  10. [Eén and Sörensson, 2004]
    Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  11. [Ekman and Hedin, 2007]
    Ekman, T., Hedin, G.: The JastAdd extensible Java compiler. In: Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems and Applications, OOPSLA 2007, pp. 1–18. ACM, New York (2007)CrossRefGoogle Scholar
  12. [Engelfriet and Filè, 1982]
    Engelfriet, J., Filè, G.: Simple multi-visit attribute grammars. Journal of Computer and System Sciences 24(3), 283–314 (1982)CrossRefzbMATHMathSciNetGoogle Scholar
  13. [Heeren et al., 2003]
    Heeren, B., Leijen, D., van IJzendoorn, A.: Helium, for learning haskell. In: Proceedings of the 2003 ACM SIGPLAN Workshop on Haskell, Haskell 2003, pp. 62–71. ACM, New York (2003)Google Scholar
  14. [Kastens, 1980]
    Kastens, U.: Ordered attributed grammars. Acta Informatica 13(3), 229–256 (1980)CrossRefzbMATHMathSciNetGoogle Scholar
  15. [Kennedy and Warren, 1976]
    Kennedy, K., Warren, S.K.: Automatic generation of efficient evaluators for attribute grammars. In: Proceedings of the 3rd ACM SIGACT-SIGPLAN Symposium on Principles on Programming Languages, POPL 1976, pp. 32–49. ACM, New York (1976)Google Scholar
  16. [Knuth, 1968]
    Knuth, D.E.: Semantics of context-free languages. Mathematical Systems Theory 2(2), 127–145 (1968)CrossRefzbMATHMathSciNetGoogle Scholar
  17. [Middelkoop et al., 2012]
    Middelkoop, A., Elyasov, A.B., Prasetya, W.: Functional instrumentation of actionscript programs with asil. In: Gill, A., Hage, J. (eds.) IFL 2011. LNCS, vol. 7257, pp. 1–16. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  18. [Saraiva, 1999]
    Saraiva, J.: Purely Functional Implementation of Attribute Grammars: Zuiver Functionele Implementatie Van Attributengrammatica’s. IPA dissertation series. IPA (1999)Google Scholar
  19. [Swierstra et al., 1999]
    Swierstra, S.D., Alcocer, P.R.A.: Designing and implementing combinator languages. In: Swierstra, S.D., Oliveira, J.N. (eds.) AFP 1998. LNCS, vol. 1608, pp. 150–206. Springer, Heidelberg (1999)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  • Jeroen Bransen
    • 1
    Email author
  • L. Thomas van Binsbergen
    • 1
    • 2
  • Koen Claessen
    • 3
  • Atze Dijkstra
    • 1
  1. 1.Utrecht UniversityUtrechtThe Netherlands
  2. 2.Royal HollowayUniversity of LondonEghamUK
  3. 3.Chalmers University of TechnologyGothenburgSweden

Personalised recommendations