Download The Omega Library - Computer Science
Transcript
Contents 1 Introduction 1.1 About this release . . . . . . . . . . . . . . . 1.1.1 Changes since the last release . . . . . 1.2 What is the Omega Library? . . . . . . . . . 1.3 What are tuple relations and sets? . . . . . . 1.4 What are Presburger formulas? . . . . . . . . 1.5 What are uninterpreted function symbols ? . 1.6 What is the UNKNOWN constraint? . . . . . 1.7 Manipulating integer tuple relations and sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 Compiling And Running Programs With The Omega Library 2.1 2.2 2.3 2.4 2.5 2.6 Introduction . . . . . . . . Avoiding Name Collisions Compiling Templates . . . G++ 2.7.2 . . . . . . . . . Debugging information . . Enabling one-pass linking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 3 3 4 4 4 5 5 5 6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 . 10 . 10 . 11 Creating relations . . . . . . Building formulas . . . . . . Referring to variables . . . . Building atomic constraints Finalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Relations during and after queries Printing . . . . . . . . . . . . . . . Simplication and satisability . . Querying variables . . . . . . . . . Iterating through a DNF . . . . . . Inexact relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Collections and Iterators . Sequences . . . . . . . . . Lists and Tuples . . . . . Generators . . . . . . . . 5 Querying Existing Relations 5.1 5.2 5.3 5.4 5.5 5.6 . . . . . . . . . . . . . . 4 Building New Relations 4.1 4.2 4.3 4.4 4.5 . . . . . . . . . . . . . . 3 Primitive Data Structures 3.1 3.2 3.3 3.4 . . . . . . . . 1 6 6 7 7 8 8 9 12 12 13 15 16 20 21 21 21 22 22 24 25