{"header":{"message":"WIP","description":null,"timestamp":"2023-04-21T09:31:24.002165504Z","authors":[{}]},"hash":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC","authors":[{"login":"paradyx","key":"5AMTvjBCcPzaCthP7D55pufHFs8VkiFuYRMjh3JoBJdy"}],"deps":{"hashes":[["B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC","WIP"],["AA",null],["EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC","WIP"],["567NUQ633R5ESTE2LWXVUGM7XEZGJ65IRKPOCDZJS3JE5RAMR5KAC","Initial"],["KUEZAMEH2M3K6EDHWMYXQMHZ2QTTH4KBM5CO7A7EB64ABEWRE6WQC","WIP"]],"deps":["EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC"],"known":["567NUQ633R5ESTE2LWXVUGM7XEZGJ65IRKPOCDZJS3JE5RAMR5KAC","KUEZAMEH2M3K6EDHWMYXQMHZ2QTTH4KBM5CO7A7EB64ABEWRE6WQC"]},"hunks":[{"Replacement":{"inode":{"change":3,"pos":35},"path":"thesis.cls","line":5,"ins":{"up_context":[{"change":3,"pos":133}],"down_context":[{"change":3,"pos":184}],"flag":"BLOCK","start":0,"end":51,"inode":{"change":3,"pos":35}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":133},"to":{"change":3,"start":133,"end":184},"introduced_by":3}],"inode":{"change":3,"pos":35}},"ins_contents":[{"Add":{"text":"\\LoadClass[a4paper,11pt,twoside,openright]{memoir}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:50"}}],"del_contents":[{"Del":{"text":"\\LoadClass[a4paper,12pt,twoside,openright]{memoir}","pos":"567NUQ633R5ESTE2LWXVUGM7XEZGJ65IRKPOCDZJS3JE5RAMR5KAC:183"}}]}},{"Edit":{"inode":{"change":3,"pos":35},"path":"thesis.cls","line":38,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":960}],"down_context":[{"change":3,"pos":960}],"flag":"BLOCK","start":52,"end":78,"inode":{"change":3,"pos":35}}},"contents":[{"Add":{"text":"\\RequirePackage{stmaryrd}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:77"}}]}},{"Edit":{"inode":{"change":3,"pos":6845},"path":"main.tex","line":9,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":6973}],"down_context":[{"change":3,"pos":6973}],"flag":"BLOCK","start":79,"end":109,"inode":{"change":3,"pos":6845}}},"contents":[{"Add":{"text":"\\newtheorem{example}{Example}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:108"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":16,"ins":{"up_context":[{"change":2,"pos":108}],"down_context":[{"change":3,"pos":160}],"flag":"BLOCK","start":110,"end":237,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":108},"to":{"change":2,"start":108,"end":161},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"\\newcommand{\\C}[0]{\\mathcal{C}} % Set of polynomial constraints","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:173"}},{"Add":{"text":"\\renewcommand{\\L}{\\mathcal{L}} % Set of polynomial constraints","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:236"}}],"del_contents":[{"Del":{"text":"\\newcommand{\\C}[0]{\\mathcal{C}} % Set of Constraints","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:160"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":20,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":269}],"down_context":[{"change":3,"pos":269}],"flag":"BLOCK","start":238,"end":311,"inode":{"change":3,"pos":8115}}},"contents":[{"Add":{"text":"\\newcommand{\\Zs}[0]{\\mathfrak{Z}} % the structure of integer arithmetic.","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:310"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":27,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":482}],"down_context":[{"change":2,"pos":162}],"flag":"BLOCK","start":312,"end":435,"inode":{"change":3,"pos":8115}}},"contents":[{"Add":{"text":"\\newcommand{\\Land}[0]{\\wedge}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:341"}},{"Add":{"text":"\\newcommand{\\LAnd}[0]{\\bigwedge}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:374"}},{"Add":{"text":"\\newcommand{\\set}[2]{\\{#1\\hspace{0.5em}|\\hspace{0.5em}#2\\}}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:434"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":31,"ins":{"up_context":[{"change":2,"pos":163}],"down_context":[{"change":2,"pos":212}],"flag":"BLOCK","start":436,"end":617,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":163},"to":{"change":2,"start":163,"end":212},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"\\subsection{Constraints}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:460"}},{"Add":{"text":"%","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:462"}},{"Add":{"text":"\\newacronym{smt}{SMT}{Satisfiability Modulo Theory}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:514"}},{"Add":{"text":"\\newacronym{ppl}{PPL}{Parma Polyhedra Library}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:561"}},{"Add":{"text":"\\newacronym{koat}{KoAT2}{KoAT2} \\todo{wrong acronym}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:614"}},{"Add":{"text":"%","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:616"}}],"del_contents":[{"Del":{"text":"\\subsection{Constraints, Polyhedra, Projections}","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:211"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":39,"ins":{"up_context":[{"change":2,"pos":349}],"down_context":[{"change":2,"pos":506}],"flag":"BLOCK","start":618,"end":776,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":349},"to":{"change":2,"start":349,"end":506},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"program, one needs polynomial constraints. As an extended concept Koat2 uses","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:694"}},{"Add":{"text":"boxes and we will use polyhedra for the partial evaluation. Since those concepts","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:775"}}],"del_contents":[{"Del":{"text":"program, one needs polynomial constraints. As an extended concept Koat uses","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:424"}},{"Del":{"text":"Boxes and we will use Polyhedra for the partial evaluation. Since those concepts","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:505"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":42,"ins":{"up_context":[{"change":2,"pos":560}],"down_context":[{"change":3,"pos":482}],"flag":"BLOCK","start":777,"end":1843,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":560},"to":{"change":2,"start":560,"end":924},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:777"}},{"Add":{"text":"Let $\\Zs := (\\Z, +, \\cdot, 0, 1, <)$ be the structure of ordered standard","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:851"}},{"Add":{"text":"integer arithmetic. Let $\\PV$ be a finite set of program variables and $\\TV$ be","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:931"}},{"Add":{"text":"a finite set of temporary variables. Together they form the set of variables $\\V","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1012"}},{"Add":{"text":":= \\PV \\union \\TV$. ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1033"}},{"Add":{"text":"\\begin{definition}[Constraint]","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1064"}},{"Add":{"text":" For a given finite set of variables $\\V = {v_1, \\dots v_n}$, the set of ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1141"}},{"Add":{"text":" \\textit{linear} constraints $\\L$ over the variables $\\V$ is defined as the ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1221"}},{"Add":{"text":" set $\\set{a_0 + \\sum_{i=1}^{|\\V|} a_i v_i < 0}{a_i \\in \\Z, v_i \\in \\V}$.","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1298"}},{"Add":{"text":" The set of \\textit{polynomial} constraints $\\C$ is defined as the set $\\{e <","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1379"}},{"Add":{"text":" 0 | e \\in \\Z[\\V]\\}$. ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1405"}},{"Add":{"text":"\\end{definition}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1422"}},{"Add":{"text":"% Satisfiability ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1440"}},{"Add":{"text":"Constraints are a subset of FO formulas and thus the semantics according to the","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1520"}},{"Add":{"text":"semantics of FO-formulas. ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1547"}},{"Add":{"text":"\\begin{definition}[Satisfiability]","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1582"}},{"Add":{"text":" A constraint $c \\in \\C$ is \\textit{satisfiable} when the formula $\\varphi=","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1661"}},{"Add":{"text":" c$ is satisfiable in $\\Zs$ or $\\Zs \\models c$. We say a variable assignment","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1741"}},{"Add":{"text":" $\\beta: \\V \\mapsto \\Z$ \\textit{satisfies} the constraint $c$ when $(\\Zs,","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1818"}},{"Add":{"text":" \\beta) \\models c$. ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1842"}}],"del_contents":[{"Del":{"text":"Let $\\PV$ be a set of program variables and $\\TV$ be a set of temporary","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:631"}},{"Del":{"text":"variables. Together they form the set of variables $\\V := \\PV \\union \\TV$. ","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:707"}},{"Del":{"text":"Let $(\\N, +, \\cdot, 0, 1, <)$ be the structure of ","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:758"}},{"Del":{"text":"The set of constraints $\\C$ is defined as the minimal as $\\{c = e < 0 | e \\in","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:836"}},{"Del":{"text":"\\Z[\\V]\\}$. That is the set of all constraints over integer polynomials less than","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:917"}},{"Del":{"text":"zero.","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:923"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":63,"ins":{"up_context":[{"change":3,"pos":483}],"down_context":[{"change":2,"pos":1086}],"flag":"BLOCK","start":1844,"end":2220,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":483},"to":{"change":2,"start":925,"end":1086},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":" Analogously, satisfiability of a set of constraints is defined by the","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1917"}},{"Add":{"text":" satisfiability of its conjunction. A set of constraints $C \\subseteq \\C$ is","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:1997"}},{"Add":{"text":" \\textit{satisfiable} when $\\Zs \\models \\LAnd_{c_i \\in C} c_i$. Moreover, an","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2077"}},{"Add":{"text":" assignment $\\beta$ \\textit{satisfies} the set of constraints $C$ when $(\\Zs,","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2158"}},{"Add":{"text":" \\beta) \\models \\LAnd{c_i \\in \\C} c_i$. ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2202"}},{"Add":{"text":"\\end{definition}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2219"}}],"del_contents":[{"Del":{"text":"Note that all constraint $e_1 \\diamond e_2$ with the operators $\\diamond","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:997"}},{"Del":{"text":"\\in >, <, \\leq, \\geq$ can be transformed into an equivalent constraint $e' < 0","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:1076"}},{"Del":{"text":"\\in \\C$:","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:1085"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":70,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":1087}],"down_context":[{"change":2,"pos":1087}],"flag":"BLOCK","start":2221,"end":2781,"inode":{"change":3,"pos":8115}}},"contents":[{"Add":{"text":"We also write $\\Zs \\models C$ and $(\\Zs, \\beta)\\models C$ instead of $\\Zs","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2294"}},{"Add":{"text":"\\models \\LAnd_{c_i \\in C} c_i$ and $(\\Zs, \\beta)\\models \\LAnd {c_i \\in C} c_i$,","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2374"}},{"Add":{"text":"respectively. Furthermore, we use conjunctions and sets of constraints","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2445"}},{"Add":{"text":"interchangeably. ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2463"}},{"Add":{"text":"","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2464"}},{"Add":{"text":"Note that by definition constraints are restricted to the form $e < 0$, because","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2544"}},{"Add":{"text":"Koat2 uses this representation internally and it makes proofs more concise.","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2620"}},{"Add":{"text":"However, all constraint $e_1 \\diamond e_2$ with the operators $\\diamond \\in >,","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2699"}},{"Add":{"text":"<, \\leq, \\geq$ can be transformed into equivalent constraints $e' < 0 \\in \\C$. ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2779"}},{"Add":{"text":"","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2780"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":82,"ins":{"up_context":[{"change":2,"pos":1148}],"down_context":[{"change":2,"pos":1187}],"flag":"BLOCK","start":2782,"end":2902,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1148},"to":{"change":2,"start":1148,"end":1187},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":" e_1 \\leq e_2 &\\equiv e_1 - e_2 - 1< 0 \\\\","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2826"}},{"Add":{"text":" e_1 > e_2 &\\equiv e_2 - e_1 < 0 \\\\","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2865"}},{"Add":{"text":" e_1 < e_2 &\\equiv e_1 - e_2 < 0","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2901"}}],"del_contents":[{"Del":{"text":" e_1 \\leq e_2 &\\equiv e_1 - e_2 < 0","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:1186"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":86,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1200},"to":{"change":2,"start":1200,"end":1434},"introduced_by":2}],"inode":{"change":3,"pos":8115}}},"contents":[{"Del":{"text":"","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:1200"}},{"Del":{"text":"and so on. Koat2 internaly represents all constraints in the simplified form, ","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:1279"}},{"Del":{"text":"and one can assume that all constraints are given in the simplified form. ","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:1354"}},{"Del":{"text":"However, for better readability we will use the general form in the examples. ","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:1433"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":87,"ins":{"up_context":[{"change":2,"pos":1435}],"down_context":[{"change":2,"pos":1691}],"flag":"BLOCK","start":2903,"end":2950,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1435},"to":{"change":2,"start":1435,"end":1691},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"Equality can be simulated by two constraints. ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2949"}}],"del_contents":[{"Del":{"text":"Given a variable assignment $\\sigma: \\PV \\mapsto \\Z$ for the program variables","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:1513"}},{"Del":{"text":"we say $\\sigma$ satisfies the constraint $c \\in \\C$ when the constraint holds","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:1591"}},{"Del":{"text":"with every variable $v \\in \\V$ being replaced by it's assigned value $\\sigma(v)$","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:1672"}},{"Del":{"text":"or more formally:","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:1690"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":89,"ins":{"up_context":[{"change":2,"pos":1692}],"down_context":[{"change":2,"pos":1801}],"flag":"BLOCK","start":2951,"end":3038,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1692},"to":{"change":2,"start":1692,"end":1801},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"\\begin{equation*}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:2968"}},{"Add":{"text":" e_1 = e_2 \\equiv e_1 \\leq e_2 \\Land e_1 \\geq e_2","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3021"}},{"Add":{"text":"\\end{equation*}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3037"}}],"del_contents":[{"Del":{"text":"and we say a constraint is satisfiable if there exists a variable assignment","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:1768"}},{"Del":{"text":"that satisfies the constraint. ","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:1800"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":93,"ins":{"up_context":[{"change":2,"pos":1802}],"down_context":[{"change":3,"pos":9093}],"flag":"BLOCK","start":3039,"end":3217,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":1802},"to":{"change":2,"start":1802,"end":1969},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"Hence, we will use the all operators above, wherever it improves readability, ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3117"}},{"Add":{"text":"but assume the constraints to be into the simplified form from the definition, ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3197"}},{"Add":{"text":"in formal proofs. ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3216"}}],"del_contents":[{"Del":{"text":"For a set of constraints $C \\subset \\C$ we say that it is satisfied by the","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:1876"}},{"Del":{"text":"assignment, if and only if the assignmnet satisfies every constraint contained","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:1955"}},{"Del":{"text":"in the set. ","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:1968"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":97,"ins":{"up_context":[{"change":3,"pos":9094}],"down_context":[{"change":3,"pos":484}],"flag":"BLOCK","start":3218,"end":3464,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":9094},"to":{"change":2,"start":1970,"end":2010},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"The problem of determining, if a set of constraints is satisfiable or finding a","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3297"}},{"Add":{"text":"valid or all valid variable assignment is called \\Gls{smt} and well","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3365"}},{"Add":{"text":"studied.\\todo{Quellenangaben} We will use the SMT-solver Z3\\todo{Quellenangaben}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3446"}},{"Add":{"text":"for this thesis.","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3463"}}],"del_contents":[{"Del":{"text":"\\todo{existentially quantify variables}","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:2009"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":102,"ins":{"up_context":[{"change":3,"pos":485}],"down_context":[{"change":3,"pos":652}],"flag":"BLOCK","start":3465,"end":3681,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":485},"to":{"change":2,"start":2011,"end":2179},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"% Solutions","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3476"}},{"Add":{"text":"The we define $\\llbracket c \\rrbracket$ as the set of all satisfying assignments","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3557"}},{"Add":{"text":"of the constraint $c$ and $\\llbracket C \\rrbracket$ as the set of all satisfying","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3638"}},{"Add":{"text":"assignments for $C$. The following holds:","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3680"}}],"del_contents":[{"Del":{"text":"- struktur = universum + signatur + interpretation der signatur","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:2074"}},{"Del":{"text":"in unserem fall:","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:2091"}},{"Del":{"text":" - universum = integer","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:2115"}},{"Del":{"text":" - signatur = (+, *, 0, 1, <)","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:2146"}},{"Del":{"text":" - interpretation wie erwartet","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:2178"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":107,"ins":{"up_context":[{"change":3,"pos":653}],"down_context":[{"change":2,"pos":2313}],"flag":"BLOCK","start":3682,"end":3795,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":653},"to":{"change":2,"start":2180,"end":2313},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"\\begin{equation*}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3699"}},{"Add":{"text":" \\llbracket C \\rrbracket = \\Intersect_{c_i \\in C} \\llbracket c_i \\rrbracket","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3778"}},{"Add":{"text":"\\end{equation*}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3794"}}],"del_contents":[{"Del":{"text":"wir arbeiten auf quantoren freie ","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:2213"}},{"Del":{"text":"wir definieren constraints ","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:2241"}},{"Del":{"text":"wir erlauben ausschließlich FO(\\tau) formeln der form von constraints","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:2312"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":111,"ins":{"up_context":[{"change":2,"pos":2314}],"down_context":[{"change":2,"pos":2493}],"flag":"BLOCK","start":3796,"end":4065,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":2314},"to":{"change":2,"start":2314,"end":2493},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"% Entailment","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3808"}},{"Add":{"text":"\\begin{definition}[Entailment]","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3839"}},{"Add":{"text":" Let $A, B \\subseteq \\C$. If $A \\models B$ then, $\\llbracket A \\rrbracket \\subset","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3924"}},{"Add":{"text":" \\llbracket B \\rrbracket$ and we say that $A$ \\textit{entails} $B$.","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:3995"}},{"Add":{"text":"\\end{definition}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:4012"}},{"Add":{"text":"Example: $X < 0 \\Land Y \\leq X$ entails $Y \\leq 1$.","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:4064"}}],"del_contents":[{"Del":{"text":"- $FO(\\tau)$ formeln","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:2334"}},{"Del":{"text":"- Atom $","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:2343"}},{"Del":{"text":"- constraints als quantoren freie Formeln auffassen.","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:2396"}},{"Del":{"text":"- existentieller abschluss: existentielle quantifizierung aller Variablesn","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:2471"}},{"Del":{"text":"","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:2472"}},{"Del":{"text":"Notation: $\\models$","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:2492"}}]}},{"Replacement":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":118,"ins":{"up_context":[{"change":2,"pos":2494}],"down_context":[{"change":2,"pos":2524}],"flag":"BLOCK","start":4066,"end":4453,"inode":{"change":3,"pos":8115}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":2494},"to":{"change":2,"start":2494,"end":2524},"introduced_by":2}],"inode":{"change":3,"pos":8115}},"ins_contents":[{"Add":{"text":"\\begin{definition}[Projection]","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:4096"}},{"Add":{"text":" Let $X \\subset V$ and $C \\subset \\C$ be a set of constraints over the","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:4170"}},{"Add":{"text":" variables $V$. Then the $\\text{proj}_X(C)$ -- say the projection of $C$","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:4246"}},{"Add":{"text":" onto the variables $X$ -- is the set of constraints $C'$ such that","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:4317"}},{"Add":{"text":" $\\llbracket C' \\rrbracket = \\{\\beta|_X \\hspace{0.5em} | \\hspace{0.5em} \\beta","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:4398"}},{"Add":{"text":" \\in \\llbracket C \\rrbracket \\}$.","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:4435"}},{"Add":{"text":"\\end{definition}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:4452"}}],"del_contents":[{"Del":{"text":"Finding a variable assignment","pos":"EIPHTX56WTRFBMBNA4VYMKK4L7GWHA4Q2AQ3BCG2ZGZB3DBRENBQC:2523"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":126,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":2525}],"down_context":[{"change":2,"pos":2525}],"flag":"BLOCK","start":4454,"end":5144,"inode":{"change":3,"pos":8115}}},"contents":[{"Add":{"text":"For a finite set of variables $|V| = n $, one can think of all possible","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:4525"}},{"Add":{"text":"assignments as a set of points in an n-dimensional space. In case of linear ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:4602"}},{"Add":{"text":"constraints, the set of solutions the convex-hull around the possible solutions ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:4683"}},{"Add":{"text":"is called a polyhedron. The polyhedron doesn't need to be finite or closed in ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:4762"}},{"Add":{"text":"all dimensions, if for example, the value of the variable is unimportant to the","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:4842"}},{"Add":{"text":"satisfiability of the constraints. A set of constraints $A$ entails $B$ if the","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:4921"}},{"Add":{"text":"polyhedron is encloses by the other. Calculating polyhedra, projections","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:4993"}},{"Add":{"text":"and testing for entailment can be done with libraries like the","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:5056"}},{"Add":{"text":"\\gls{ppl}.\\todo{citation} In Koat2, Apron is used that uses \\gls{ppl} under the","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:5136"}},{"Add":{"text":"hood. ","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:5143"}}]}},{"Edit":{"inode":{"change":3,"pos":8115},"path":"ch2_preliminaries.tex","line":260,"atom":{"NewVertex":{"up_context":[{"change":3,"pos":9345}],"down_context":[{"change":3,"pos":4443}],"flag":"BLOCK","start":5145,"end":5198,"inode":{"change":3,"pos":8115}}},"contents":[{"Add":{"text":"\\newacronym{pip}{PIP}{Probabilistic Integer Program}","pos":"B5T3HFKSQF3T4T6Z2KZOA5ZDMI6TVON7BS7KKB3EAGGYAS7RJPBAC:5197"}}]}}],"owner":"paradyx","repo":"ma-tex","token":"bSkg9VLQSmqca6ucmUOV9bxzZN4Oh+dsuq7HMVhz0jI=","login":null}

…

Dependencies

Change contents

Review