From 354daa843a6fde8e046292d00eec266aad3ed58a Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Mon, 29 Jan 2024 14:42:18 +0000 Subject: [PATCH] Remove unused files in `k-distribution` (#3928) We identified that these files are all unused in the K frontend deep dive meeting; this PR just clears them all out. Co-authored-by: rv-jenkins --- k-distribution/include/kframework/coq/maps.v | 272 ----- k-distribution/include/kframework/coq/proof.v | 59 - k-distribution/include/kframework/coq/sets.v | 74 -- .../include/kframework/documentation.k | 4 - .../include/kframework/html/k-definition.css | 160 --- .../kframework/html/k-documentation.css | 148 --- k-distribution/include/kframework/latex/k.sty | 1011 ----------------- .../include/kframework/z3/basic.smt2 | 35 - .../include/kframework/z3/floating_point.smt2 | 25 - .../include/kframework/z3/list.smt2 | 40 - .../include/kframework/z3/search_tree.smt2 | 50 - .../include/kframework/z3/sorted_list.smt2 | 71 -- .../include/kframework/z3/string.smt2 | 80 -- 13 files changed, 2029 deletions(-) delete mode 100644 k-distribution/include/kframework/coq/maps.v delete mode 100644 k-distribution/include/kframework/coq/proof.v delete mode 100644 k-distribution/include/kframework/coq/sets.v delete mode 100644 k-distribution/include/kframework/documentation.k delete mode 100644 k-distribution/include/kframework/html/k-definition.css delete mode 100644 k-distribution/include/kframework/html/k-documentation.css delete mode 100644 k-distribution/include/kframework/latex/k.sty delete mode 100644 k-distribution/include/kframework/z3/basic.smt2 delete mode 100644 k-distribution/include/kframework/z3/floating_point.smt2 delete mode 100644 k-distribution/include/kframework/z3/list.smt2 delete mode 100644 k-distribution/include/kframework/z3/search_tree.smt2 delete mode 100644 k-distribution/include/kframework/z3/sorted_list.smt2 delete mode 100644 k-distribution/include/kframework/z3/string.smt2 diff --git a/k-distribution/include/kframework/coq/maps.v b/k-distribution/include/kframework/coq/maps.v deleted file mode 100644 index 7f07b521c89..00000000000 --- a/k-distribution/include/kframework/coq/maps.v +++ /dev/null @@ -1,272 +0,0 @@ -Require Import BinPos. -Require Import ZArith. -Require Import FMapPositive. -Require Import String. - -Require Import Setoid. - -Set Implicit Arguments. - -(** * Maps - - Define maps, by making constructors for - empty and singleton maps and map union, - and defining a suitable equivalence relation *) - -(* TODO: - define a well-formedness predicate saying keys are not repeated, - augment language definition with a proof that all evaluation - steps preserve it - *) - -Inductive Map (Key Elt : Type) : Type := -| mapEmpty -| mapItem (k : Key) (v : Elt) -| mapJoin (m1 m2 : Map Key Elt) -. -Arguments mapEmpty [Key Elt]. - -(** ** Map notations - *) -Delimit Scope Map with Map. -Bind Scope Map with Map. - -Open Scope Map. - -Infix "|->" := mapItem (at level 50, no associativity) : Map. -Infix ":*" := mapJoin (at level 60, right associativity) : Map. - -(** ** Map equivalence - - Map equivalence is axiomatized by - identitiy, associativity, commutativity, and congruence of union, - closed under reflexivity, symmetry, and transitivity. - *) -Inductive MapEquiv {K E : Type} : Map K E -> Map K E -> Prop := -| equivUnit : forall m, MapEquiv (m :* mapEmpty) m -| equivComm : forall m1 m2, MapEquiv (m1 :* m2) (m2 :* m1) -| equivAssoc : forall m1 m2 m3, MapEquiv ((m1 :* m2) :* m3) (m1 :* (m2 :* m3)) - -| equivJoin : forall l1 r1 l2 r2, MapEquiv l1 l2 -> MapEquiv r1 r2 -> MapEquiv (l1 :* r1) (l2 :* r2) -| equivTrans : forall m1 m2 m3, MapEquiv m1 m2 -> MapEquiv m2 m3 -> MapEquiv m1 m3 -| equivSym : forall m1 m2, MapEquiv m1 m2 -> MapEquiv m2 m1 -| equivRefl : forall m, MapEquiv m m -. - -Infix "~=" := MapEquiv (at level 70, no associativity) : Map. - -(** Registering map equivalence as an equivalence relation *) - -Add Parametric Relation (K E : Type) : (Map K E) MapEquiv - reflexivity proved by equivRefl - symmetry proved by equivSym - transitivity proved by equivTrans - as map_equiv_rel. - -Add Parametric Morphism K E : (@mapJoin K E) with - signature MapEquiv ==> MapEquiv ==> MapEquiv as map_join_mor. -Proof. auto using equivJoin. Qed. - -(** Some derived equivalences *) - -(** A unit law with the unit on the left *) -Lemma equivUnitL : forall {K V} (m : Map K V), MapEquiv (mapEmpty :* m) m. -intros. rewrite equivComm. apply equivUnit. -Qed. - -(** Switching the first two maps in a right-associated sequence *) -Lemma equivComAssoc : forall {K V} (m1 m2 m3 : Map K V), m1 :* m2 :* m3 ~= m2 :* m1 :* m3. -intros. rewrite <- equivAssoc, (equivComm m1 m2), equivAssoc. reflexivity. Qed. - -(** ** Map Equality Tactic - - The map equality tactic [equate_maps] tries to solve map equations involving - at most one map-typed evar. - - The general approach is to put both maps into a standard form, - as a sequence of singleton items and residual map-typed variables, - then cancel entries between the sides, until everything that's - left can be absorbed into the evar (or we're stuck with - a residual equation). - *) - -(** *** Finding items in a map - These are the tactics for commuting target items to the - head of a map *) - -(** Specializing congruence for the find tactic *) -Definition equivJoinL {K V} (r : Map K V) l1 l2 pfl : l1 :* r ~= l2 :* r := - equivJoin pfl (equivRefl r). -Definition equivJoinR {K V} (l : Map K V) r1 r2 pfr : l :* r1 ~= l :* r2 := - equivJoin (equivRefl l) pfr. - -(** Find an entry with key [x] in map [map]. - If found, it calls the continuation tactic [k] on - an equality of the form [map ~= x |-> _ :* _], - otherwise it simply fails. - *) -Ltac find x map k := - match map with - | (x |-> _) => let pf := constr:(equivSym (equivUnit map)) in k pf - | (x |-> _ :* _) => let pf := constr:(equivRefl map) in k pf - | (?mapl :* (x |-> ?v)) => let pf := constr:(equivComm mapl (x |-> v)) in k pf - | ?mapl :* ?mapr => - find x mapl ltac:(fun pfl => let pf := constr:(equivTrans (equivJoinL mapr pfl) - (equivAssoc (x |-> _) _ mapr)) - in k pf) - || find x mapr ltac:(fun pfr => let pf := constr:(equivTrans (equivJoinR mapl pfr) - (equivComAssoc mapl (x |-> _) _)) - in k pf) - end. - -(** Find an entire map [submap] appearing exactly all or part of a map [map]. - It's expeted that [submap] be a variable, this tactic makes no attempt - to search search up to map equality if [submap] is a more complicated - map expression. - If found, calls the continuation tactic [k] on an equality of the form - [map ~= submap :* _] - *) -Ltac find_submap map submap k := - match map with - | submap => let pf := constr:(equivSym (equivUnit map)) in k pf - | (submap :* _) => let pf := constr:(equivRefl map) in k pf - | (?mapl :* submap) => let pf := constr:(equivComm mapl submap) in k pf - | ?mapl :* ?mapr => - find_submap mapl submap - - ltac:(fun pfl => let pf := constr:(equivTrans (equivJoinL mapr pfl) - (equivAssoc submap _ mapr)) - in k pf) - || find_submap mapr submap - ltac:(fun pfr => let pf := constr:(equivTrans (equivJoinR mapl pfr) - (equivComAssoc mapl submap _)) - in k pf) - end. - -(** *** Map well-formedness predicates - - [check_maps] checks that each map is right associated, - has items before map-typed ordinary variables before - evars, and that there is at most one evar, on the right side. - - [is_map_exp] is also used elsewhere, and succeeds only if the given - map is neither an evar nor any of the map constructors. - *) - -Ltac is_map_exp m := - match m with - | (_ |-> _) => fail 1 - | (_ :* _) => fail 1 - | mapEmpty => fail 1 - | _ => try (is_evar m;fail 2) - end. -Ltac check_left_var_map m := - match m with - | (?l :* ?m') => is_map_exp l;check_left_var_map m' - | _ => is_map_exp m - end. -Ltac check_left_map m := - match m with - | mapEmpty => idtac - | _ |-> _ => idtac - | (_ |-> _ :* ?m') => check_left_map m' - | _ => check_left_var_map m - end. -Ltac check_right_var_map m := - match m with - | (?l :* ?m') => is_map_exp l;check_right_var_map m' - | _ => first [is_evar m | is_map_exp m] - end. -Ltac check_right_map m := - match m with - | mapEmpty => idtac - | _ |-> _ => idtac - | (_ |-> _ :* ?m') => check_right_map m' - | _ => check_right_var_map m - end. -Ltac check_maps := - match goal with - | [|- ?l ~= ?r] => check_left_map l;check_right_map r - end. - -(** *** Preparing maps. - - An equation is prepared by using any map equation hypotheses to - expand variables in the maps involed, - then using map equalities to remove empties, right-associate - unions, and move singleton items to the front. - - This tactic isn't entirely careful about locating evars, - but they are checked afterwards. - *) -Ltac expand_map m := - match m with - | ?l :* ?r => expand_map l; expand_map r - | ?v => is_var v; - match goal with - | [H : v ~= ?m |- _] => rewrite !H;clear H;expand_map m - | [H : ?m ~= v |- _] => rewrite <- !H;clear H;expand_map m - end - | _ => idtac - end. - - -(* maybe do by reflection? *) -Ltac prepare_maps := - match goal with - | [|- ?l ~= ?r] => expand_map l;expand_map r - end; - repeat - match goal with - | [|- context [mapEmpty :* ?m]] => rewrite (equivUnitL m) - | [|- context [?m :* mapEmpty]] => rewrite (equivUnit m) - | [|- context [(?m1 :* ?m2) :* ?m3]] => rewrite (equivAssoc m1 m2 m3) - end; - (* switch if left side has a map evar *) - match goal with - | [|- ?l ~= ?r] => - match l with - | context [?v] => is_evar v; - match type of v with Map _ _ => symmetry end - end - | _ => idtac - end; - (* Now commute items to the front things *) - repeat match goal with - | [|- context [?m1 :* ?m2 :* ?m3]] => - match m2 with _ |-> _ => is_map_exp m1; rewrite (equivComAssoc m1 m2 m3) - end - | [|- context [?m1 :* ?m2]] => - match m2 with _ |-> _ => is_map_exp m1; rewrite (equivComm m1 m2) - end - end - . - -(* *** Solving the map equation - - After preparing the maps, the left side has no evars, so the non-evar - part of the RHS must appear as a submap of the left side. - - This tactic proceeds item by item, finding and cancelling identical - items between sides. - If this ends with an equation between a map and an evar it is - instantiated. - - If the equation isn't completely solved, the tactic still succeeds, - leaving the reduced equation. - *) -Ltac equate_maps := - prepare_maps; - first[check_maps| fail 1]; - (* Find item or submap when rhs has a join *) - repeat match goal with - | [|- MapEquiv ?map (?x |-> _ :* _)] => find x map - ltac:(fun pf => apply (equivTrans pf);apply equivJoinR) - | [|- MapEquiv ?map (?submap :* _)] => find_submap map submap - ltac:(fun pf => apply (equivTrans pf);apply equivJoinR) - end; - (* If we're not failing, the rhs is down to a join-free map. - Because the lhs is still in prepared form, reflexivity - can handle all the remaining solvable possibilities. - *) - try reflexivity. \ No newline at end of file diff --git a/k-distribution/include/kframework/coq/proof.v b/k-distribution/include/kframework/coq/proof.v deleted file mode 100644 index 39642bb44f2..00000000000 --- a/k-distribution/include/kframework/coq/proof.v +++ /dev/null @@ -1,59 +0,0 @@ -Set Implicit Arguments. - -Section relations. -Variables (cfg : Set) (cstep : cfg -> cfg -> Prop). - -Definition Spec : Type := cfg -> (cfg -> Prop) -> Prop. - -(* Soundness *) -CoInductive reaches (k : cfg) (P : cfg -> Prop) : Prop := - | rdone : P k -> reaches k P - | rstep : forall k', cstep k k' -> reaches k' P -> reaches k P. - -Definition sound (Rules : Spec) : Prop := - forall x P, Rules x P -> reaches x P. - -Inductive step (X : Spec) (k : cfg) (P : cfg -> Prop) : Prop := - | sdone : P k -> step X k P - | sstep : forall k', cstep k k' -> X k' P -> step X k P - . - -CoFixpoint stable_sound (Rules : Spec) - (Hstable : forall x P, Rules x P -> step Rules x P) - : sound Rules := - fun x P H => - match Hstable _ _ H with - | sdone pf => rdone _ _ pf - | sstep k' Hstep H' => - rstep Hstep (stable_sound Hstable _ _ H') - end. - -Inductive trans (X : Spec) (k : cfg) (P : cfg -> Prop) : Prop := - | ddone : P k -> trans X k P - | dtrans : forall Q, X k Q -> (forall k', Q k' -> trans X k' P) -> trans X k P - | dstep : forall k', cstep k k' -> trans X k' P -> trans X k P - . - -Lemma trans_trans (X : Spec) : - forall x P Q, - trans X x P -> (forall y, P y -> trans X y Q) -> trans X x Q. -induction 1;eauto using trans. -Qed. - -Lemma trans_stable (Rules : Spec) : - (forall x P, Rules x P -> step (trans Rules) x P) - -> forall x P, trans Rules x P -> step (trans Rules) x P. -induction 2;try econstructor(eassumption). -destruct (H _ _ H0);eauto using step,trans_trans. -Qed. - -Lemma proved_sound (Rules : Spec) : - (forall x P, Rules x P -> step (trans Rules) x P) - -> sound Rules. -unfold sound. -intros. -apply stable_sound with (trans Rules); -eauto using trans, trans_stable. -Qed. - -End relations. diff --git a/k-distribution/include/kframework/coq/sets.v b/k-distribution/include/kframework/coq/sets.v deleted file mode 100644 index e971ecc881a..00000000000 --- a/k-distribution/include/kframework/coq/sets.v +++ /dev/null @@ -1,74 +0,0 @@ -Require Import BinPos. -Require Import ZArith. -Require Import FMapPositive. -Require Import String. - -Require Import Setoid. - -Require Import maps. - -Set Implicit Arguments. - -(* Sets, similarly to Map *) - -Inductive MultiSet (Elt : Type) := -| setEmpty -| setItem (e : Elt) -| setJoin (s1 s2 : MultiSet Elt) -. -Arguments setEmpty [Elt]. - -Inductive SetEquiv {E : Type} : MultiSet E -> MultiSet E -> Prop := -| equivUnit : forall s, SetEquiv (setJoin s setEmpty) s -| equivComm : forall s1 s2, SetEquiv (setJoin s1 s2) (setJoin s2 s1) -| equivAssoc : forall s1 s2 s3, SetEquiv (setJoin (setJoin s1 s2) s3) (setJoin s1 (setJoin s2 s3)) - -| equivJoin : forall l1 r1 l2 r2, SetEquiv l1 l2 -> SetEquiv r1 r2 - -> SetEquiv (setJoin l1 r1) (setJoin l2 r2) -| equivTrans : forall s1 s2 s3, SetEquiv s1 s2 -> SetEquiv s2 s3 -> SetEquiv s1 s3 -| equivSym : forall s1 s2, SetEquiv s1 s2 -> SetEquiv s2 s1 -| equivRefl : forall s, SetEquiv s s -. - -Lemma equivCommAssoc : forall {E} (s1 s2 s3 : MultiSet E), - SetEquiv (setJoin s1 (setJoin s2 s3)) - (setJoin s2 (setJoin s1 s3)). -intros. -eapply equivTrans. -apply equivSym. apply equivAssoc. -eapply equivTrans. -eapply equivJoin. -eapply equivComm. -eapply equivRefl. -eapply equivAssoc. -Qed. - -Add Parametric Relation (E : Type) : (MultiSet E) SetEquiv - reflexivity proved by equivRefl - symmetry proved by equivSym - transitivity proved by equivTrans - as map_equiv_rel. - -Add Parametric Morphism (E : Type) : (@setJoin E) with - signature SetEquiv ==> SetEquiv ==> SetEquiv as set_join_mor. -Proof. auto using equivJoin. Qed. -Add Parametric Morphism E : (@SetEquiv E) with - signature SetEquiv ==> SetEquiv ==> iff as set_equiv_mor. -Proof. split;eauto using equivTrans,equivSym. Qed. - -Fixpoint keys {Key Elt} (m : Map Key Elt) : MultiSet Key := -match m with -| mapEmpty => @setEmpty Key -| mapItem k _ => setItem k -| mapJoin l r => setJoin (keys l) (keys r) -end. - -Add Parametric Morphism K E : (@keys K E) with - signature MapEquiv ==> SetEquiv as keys_mor. -induction 1; try solve[econstructor(eassumption)]. -Qed. - -Lemma equivs {Key Elt} (m1 m2 : Map Key Elt) : - m1 ~= m2 -> SetEquiv (keys m1) (keys m2). -induction 1;solve[econstructor(eassumption)]. -Qed. \ No newline at end of file diff --git a/k-distribution/include/kframework/documentation.k b/k-distribution/include/kframework/documentation.k deleted file mode 100644 index 3e81f87b33c..00000000000 --- a/k-distribution/include/kframework/documentation.k +++ /dev/null @@ -1,4 +0,0 @@ -// Copyright (c) Runtime Verification, Inc. All Rights Reserved. -module DOCUMENTATION - configuration $PGM:K -endmodule diff --git a/k-distribution/include/kframework/html/k-definition.css b/k-distribution/include/kframework/html/k-definition.css deleted file mode 100644 index a3a7c45e7fe..00000000000 --- a/k-distribution/include/kframework/html/k-definition.css +++ /dev/null @@ -1,160 +0,0 @@ -/* Copyright (c) Runtime Verification, Inc. All Rights Reserved. */ -.bold -{ -font-weight: bold; -} -.italic -{ -font-style: italic; -} -em -{ -font-style: italic; -} -.large -{ -font-size: large; -} -.xlarge -{ -font-size: x-large; -} -.courier -{ -font-family: courier; -} -.attribute -{ -color: blue; -} -.center -{ -text-align: center; -} -.textCentered -{ -text-align: center; -display: inline-block; -vertical-align: top; -min-width: 2em; -} -.rewrite -{ -padding: 0; -padding-left: 2px; -padding-right: 2px; -margin: 0; -border-collapse: collapse; -text-align: center; -display: inline-block; -vertical-align: top; -min-width: 2em; -} -.rewriteLeft -{ -border-bottom-style:solid; -border-bottom-color:black; -border-bottom-width:1.5px; -} - -.cell -{ -font-style:normal; -font-weight:normal; -display: inline-block; -vertical-align: top; -text-align:left; -} -hr.rewriteLine -{ -color: black; -background-color: black; -height: 1.5px; -padding: 0px; -} -/* -hr.reduce:after -{ -width: 0; -height: 0; -border-left : 6px solid transparent; -border-right : 6px solid transparent; -border-top : 6px solid black; -position: absolute; -content: ""; -} -*/ -.tab -{ -display: inline-block; -padding : 2px; -margin-left : 0; -border-top : 3px solid; -border-left : 3px solid; -border-right : 3px solid; -text-align: left; -} -.tab.curvedEdge -{ -position: relative; -left: 30px; -top : 3px; -} -.tab.straightEdge -{ -position: relative; -left: 8px; -top : 3px; -} -.block -{ -color : black; -border-width: 3px; -display: inline-block; -padding: 10px; -padding-left: 20px; -padding-right: 20px; -border-radius: 30px; -border-style: solid; -min-width: 60px; -text-align: left; -} -.commentBlock -{ -color : black; -border-width: 1px; -display: inline-block; -padding: 10px; -padding-left: 20px; -padding-right: 20px; -border-radius: 30px; -border-style: solid; -text-align: left; -} -.block.right -{ -border-top-right-radius: 0px; -border-bottom-right-radius: 0px; -border-right-style: dotted; -} -.block.left -{ -border-top-left-radius: 0px; -border-bottom-left-radius: 0px; -border-left-style: dotted; -} -.defaultColor -{ -border-color: #000000; -background-color: #FFFFFF; -} -.definitionComment -{ -border-color: #000000; -background-color: #f2f2f2; -} -.moduleComment -{ -border-color: #000000; -background-color: #e5e5e5; -} diff --git a/k-distribution/include/kframework/html/k-documentation.css b/k-distribution/include/kframework/html/k-documentation.css deleted file mode 100644 index 7da89be1758..00000000000 --- a/k-distribution/include/kframework/html/k-documentation.css +++ /dev/null @@ -1,148 +0,0 @@ -/* Copyright (c) Runtime Verification, Inc. All Rights Reserved. */ -.bold -{ -font-weight: bold; -} -.italic -{ -font-style: italic; -} -em -{ -font-style: italic; -} -.large -{ -font-size: large; -} -.xlarge -{ -font-size: x-large; -} -.courier -{ -font-family: courier; -} -.attribute -{ -color: blue; -} -.center -{ -text-align: center; -} -.textCentered -{ -text-align: center; -display: inline-block; -vertical-align: top; -min-width: 20px; -} -.cell -{ -display: inline-block; -vertical-align: top; -text-align:left; -} -hr.reduce -{ -color: black; -background-color: black; -height: 3px; -} -hr.reduce:after -{ -width: 0; -height: 0; -border-left : 6px solid transparent; -border-right : 6px solid transparent; -border-top : 6px solid black; -position: absolute; -content: ""; -} -.tab -{ -display: inline-block; -padding : 2px; -margin-left : 0; -border-top : 3px solid; -border-left : 3px solid; -border-right : 3px solid; -text-align: left; -} -.tab.curvedEdge -{ -position: relative; -left: 30px; -top : 3px; -} -.tab.straightEdge -{ -position: relative; -left: 8px; -top : 3px; -} -.block -{ -color : black; -border-width: 3px; -display: inline-block; -padding: 10px; -padding-left: 20px; -padding-right: 20px; -border-radius: 30px; -border-style: solid; -min-width: 60px; -text-align: left; -} -.commentBlock -{ -/*color : black; -border-width: 1px; -display: inline-block; -padding: 10px; -padding-left: 20px; -padding-right: 20px; -border-radius: 30px; -border-style: solid; -*/ -text-align: left; -} -.block.right -{ -border-top-right-radius: 0px; -border-bottom-right-radius: 0px; -border-right-style: dotted; -} -.block.left -{ -border-top-left-radius: 0px; -border-bottom-left-radius: 0px; -border-left-style: dotted; -} -.defaultColor -{ -border-color: #000000; -background-color: #FFFFFF; -} -.definitionComment -{ -/*border-color: #000000; -background-color: #f2f2f2; -*/ -} -.moduleComment -{ - /* -border-color: #000000; -background-color: #e5e5e5; -*/ -} -.alert -{ - color: red; -} -.bluetext -{ - color: blue; -} diff --git a/k-distribution/include/kframework/latex/k.sty b/k-distribution/include/kframework/latex/k.sty deleted file mode 100644 index 880480a2436..00000000000 --- a/k-distribution/include/kframework/latex/k.sty +++ /dev/null @@ -1,1011 +0,0 @@ -% Copyright (c) Runtime Verification, Inc. All Rights Reserved. -\NeedsTeXFormat{LaTeX2e} -\ProvidesPackage{k}[2012/02/14 Package for typesetting K Framework definitions http://k-framework.org] - -\RequirePackage{bookmark} -\RequirePackage{kvoptions} -\RequirePackage{ifthen} -% \RequirePackage{etoolbox} -% \RequirePackage{etextools} % for xifstrequal -% \RequirePackage{stringstrings} % for \stringlength - -\SetupKeyvalOptions{family=k,prefix=k@} - - -\DeclareStringOption[bubble]{style} % the default style for cells & stuff -\DeclareBoolOption{tight} % whether (bubble) cells should be tight or not -\DeclareBoolOption{beamer} % whether (bubble) cells should be tight or not -\DeclareBoolOption{poster} % to generate a poster from the definition -\ProcessKeyvalOptions* - -% Usage Examples %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% Next command uses the default style (bubble) with tight edges for cells. -% \usepackage[tight]{k} -% -% Next command changes the default style to mathematic cells. -% \usepackage[style=math]{k} -% -% Next command enables poster mode with mathematic cells -% \usepackage[style=math,poster]{k} -% -% Next command can be used to include k definitions in beamer presentations -% \usepackage[beamer]{k} -% To do that, though, some of the options required by k need to be passed -% to beamer, e.g. like: -% \documentclass[pdftex,usenames,dvipsnames,svgnames,x11names]{beamer} -% -% Use next command to temporary change the default style inside a definition -% \begin{k}[math] -% . . . -% \end{k} -% If the default was set to math, use bubble instead of math above. - -% Some exported commands (useful for manually writing K): -% \kall, \kprefix, \ksuffix, and \kmiddle are used to specify cells which are -% either complete, open to the right, open to the left, and open both ways, -% respectively . - -\ifthenelse{\equal{\k@style}{bubble}}{ -\newcommand{\kall}[3][white]{\ball{#1}{#2}{#3}} -\newcommand{\kallLarge}[3][white]{\ballLarge{#1}{#2}{#3}} -\newcommand{\kprefix}[3][white]{\bprefix{#1}{#2}{#3}} -\newcommand{\ksuffix}[3][white]{\bsuffix{#1}{#2}{#3}} -\newcommand{\kmiddle}[3][white]{\bmiddle{#1}{#2}{#3}} -\newcommand{\kdot}{\bdot} -\newcommand{\AnyVar}[1][]{\bAnyVar{#1}} -}{% else, assume default style is math -\newcommand{\kall}[3][white]{\mall{#1}{#2}{#3}} -\newcommand{\kallLarge}[3][white]{\mallLarge{#1}{#2}{#3}} -\newcommand{\kprefix}[3][white]{\mprefix{#1}{#2}{#3}} -\newcommand{\ksuffix}[3][white]{\msuffix{#1}{#2}{#3}} -\newcommand{\kmiddle}[3][white]{\mmiddle{#1}{#2}{#3}} -\newcommand{\kdot}{\mdot} -\newcommand{\AnyVar}[1][]{\mAnyVar{#1}} -} - - - -\RequirePackage[T1]{fontenc} -\RequirePackage{textcomp} - - -\ifk@beamer -\else -\RequirePackage{hyperref} -\RequirePackage{xcolor} -\fi - -\ifk@poster -%%% PDF functionality. -\RequirePackage{pdfcomment} -%%% Layout and design. - -% microtype is nice, but seems to create strange problems -% \RequirePackage{microtype} - -\RequirePackage{times} -\RequirePackage[scaled]{berasans} -\RequirePackage[scaled]{beramono} - -\RequirePackage[small,compact]{titlesec} -%\titleformat{command}[shape]{format}{label}{sep}{before}[after] -% shape ::= hang | block | display | runin | leftmargin | rightmargin -% | drop | wrap | frame -% sep is mandatory to be a length. -% more on http://www.ctex.org/documents/packages/layout/titlesec.pdf -\titleformat{\subsubsection}[runin]{\bfseries}{}{0pt}{}[.\hspace*{1ex}] - -% PDF link colors -% The color values and names come from the Tango Icon Scheme -\definecolor{SkyBlue2}{rgb}{.204, .396, .643} -\definecolor{ScarletRed3}{rgb}{.643, 0, 0} -\definecolor{Chocolate3}{rgb}{.561, .349, .008} - -\hypersetup{% - % Color the text of links instead of framing them. - colorlinks=true, - linkcolor=SkyBlue2, - urlcolor=ScarletRed3, - filecolor=Chocolate3 -} -\else -\newcommand{\organization}{\date} -\fi - -%%% Additional symbols and notation. - -\RequirePackage{amsmath} -\RequirePackage{amssymb} -\RequirePackage{stmaryrd} - -%%% Graphics. - -\RequirePackage{tikz} -\usetikzlibrary{shapes.misc} -\usetikzlibrary{calc} - -%%% Auxiliary packages. - -\RequirePackage{calc} -\RequirePackage{ifthen} -\RequirePackage{ifdraft} -\RequirePackage{ucs} -\RequirePackage{xspace} - -\makeatletter - -% Page Setup %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -% To output all definitions, rules, and comments onto a single, long page, we -% take the following steps: -% -% - Wrap the whole document in a 'kdefinition' environment and tell the -% 'preview' package to typeset it onto a single page. This gives us a single -% page of output. Setting a suitable border and the 'tightpage' option -% adjusts the page height to match the content. -% -% - Finding the correct page width requires two runs of TeX[1]. In the first -% run, we mark the width of every typeset block (rules, comments, etc.). -% This information is is written into an auxiliary file of name -% '\jobname.mrk'. At the beginning of the second run, we read this file -% (if it exists), determine the maximum width, and use the maximum as -% the text width. If no width information is available, we default to -% a text width of 16 inches. -% -% --- -% [1] (At least) two runs are necessary anyway: cross-referencing and indexing -% require them, and so do PDF annotations. -\ifk@poster -\pagestyle{empty} - -%%% PDF default view - -% Most PDF viewers seem to default to the "fit whole page" view mode. A single, -% long page badly fits this behavior, so we request "fit page width" instead. -\hypersetup{pdfstartview=FitH} - -%%% Use the 'preview' package to typeset everything onto a single page. - -\usepackage[active,tightpage,pdftex]{preview} -\setlength\PreviewBorder{5pt} -\fi - -% Everything within an environment that is marked as \PreviewEnvironment -% is put onto its own page. Thus, by defining a global environment that -% wraps the whole document, we get all output on a single page. -% -% The 'kompile.pl' script takes care of the wrapping. -\newenvironment{kdefinition}{}{} - -\ifk@poster -\PreviewEnvironment{kdefinition} - -%%% Determine the text width from markers put at the lower right end of -% each content block. - -% The system layer of the 'PGF' package hides the gory details. -% (See "Position Tracking Commands" in Part XIII of the PGF manual.) -\usepackage{pgfsys} - -% Try to load the marker positions from the previous run. -\newcounter{k@prevMarkerCount}% -\InputIfFileExists{\jobname.mrk}{}{}% - -% Set the text width to the maximum of the X coordinates. -\newlength{\k@maxX}% -\newlength{\k@currentMarkerX}% - -\whiledo{\value{k@prevMarkerCount} > 0}{% - \addtocounter{k@prevMarkerCount}{-1}% - \pgfsys@getposition{k@marker@\the\c@k@prevMarkerCount}{\k@currentMarker}% - \pgfextractx{\k@currentMarkerX}{\k@currentMarker}% - \ifthenelse{\lengthtest{\k@currentMarkerX > \k@maxX}}{% - \setlength{\k@maxX}{\k@currentMarkerX}% - }{}% -}% -\ifthenelse{\lengthtest{\k@maxX > 0pt}}{% - \setlength{\textwidth}{\k@maxX}% -}{% - \setlength{\textwidth}{16in}% -}% - - -% To mark the position, we use the PGF system layer macro \pgfsys@markposition. -% However, this macro usually writes to the main auxiliary file '\jobname.aux'. -% This will not work in our setting because the marker positions would then -% only be available just before the document starts, which is too late to set -% the text width. Thus we use our own auxiliary file. - -% Open the marker file for writing. -\newwrite\k@markerOut -\immediate\openout\k@markerOut=\jobname.mrk - -\newcounter{k@marker} -% The marker macro generates the marker names and briefly swaps the output -% stream that \pgfsys@markposition uses before calling it. -\newcommand{\k@markPosition}{% - \let\k@tmpAuxOut=\pgfutil@auxout% - \let\pgfutil@auxout=\k@markerOut% - \pgfsys@markposition{k@marker@\the\c@k@marker}% - \let\pgfutil@auxout=\k@tmpAuxOut% - \addtocounter{k@marker}{1}% -} - -% Also store the number of set markers for the next run (for easier looping). -\AtEndDocument{% - \immediate\write\k@markerOut{% - \string\setcounter{k@prevMarkerCount}{\the\c@k@marker}% - }{}% -} - -% Title %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\renewcommand{\@maketitle}{ - \null - \vspace*{3ex} - {\Huge \@title} - \par\vspace*{2ex} - {\Large \@author} - \par\vspace*{1ex} - {\large \@organization} - \par\vspace*{3ex} -} - -% Also add respective PDF meta information -\hypersetup{ - pdftitle={\@title}, - pdfauthor={\@author} -} - -\let\k@oldTitle=\title -\renewcommand{\title}[1]{% - \k@oldTitle{#1}% - \hypersetup{pdftitle={#1}}% -} -\let\k@oldAuthor=\author -\renewcommand{\author}[1]{% - \k@oldAuthor{#1}% - \hypersetup{pdfauthor={#1}}% -} -\let\@organization=\@empty -\newcommand{\organization}[1]{% - \def\@organization{#1}% -} - -% Source Comments %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -% Turn off section numbering: all headings will look like they were starred. -% However, they will still appear in the table of contents (and the bookmarks -% that hyperref generates for the PDF). -% -% Note that hyperref seems to rely on the "secnumdepth" counter for bookmark -% generation. Thus, the "traditional" approach \setcounter{secnumdepth}{0} -% leads to (rather) arbitrary bookmark nestings. -% -% Simply remove the labeling number from all titles. -\titlelabel{} -% Create TOC entries down to subsections. -\setcounter{tocdepth}{4} -% Show the TOC by default. -\hypersetup{% - bookmarksopen=true, - bookmarksopenlevel=2 -} -\else -\newcommand{\k@markPosition}{} -\fi - -\usepackage{fancyvrb} -\usepackage{fancybox} - -\tikzset{basic comment/.style={ - rectangle, - rounded corners, - draw, - inner sep=.75em - } -} - - - -\tikzset{comment/.style={basic comment, fill=black!5 } } - - -% Macros for use in the comments. -\newcommand{\K}{\mbox{$\mathbb{K}$}\xspace} -\newcommand{\KLabel}{\textit{KLabel}\xspace} -\newcommand{\KResult}{\textit{KResult}\xspace} - - -% Special Glyphs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\newcommand{\lp}{(} -\newcommand{\rp}{)} -\newcommand{\myquote}[1]{ - \k@withTooltip{\text{\rmfamily ``\ttfamily #1\rmfamily ''}}{Constant Sort: String}% -} -\newcommand{\mysinglequote}[1]{\text{\rmfamily "}} -\newcommand{\mybracket}[1]{(#1)} -\newcommand{\sqbracket}[1]{[#1]} -\newcommand{\crlbracket}[1]{\{#1\}} - -\newcommand{\nothing}{} -\newcommand{\somespace}{\mathbin{}} -\newcommand{\subscript}[1]{\ensuremath{\nothing_{#1}}} - -\newcommand{\kBR}{\\} - -% Builtins %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\newcommand{\builtinEqBool}[2]{{#1}==_{\scriptstyle\it Bool}{#2}} -\newcommand{\builtinNeqBool}[2]{{#1}!=_{\scriptstyle\it Bool}{#2}} - -\newcommand{\builtinAnd}[2]{{#1}\wedge_{\scriptstyle\it Bool}{#2}} -\newcommand{\builtinOr}[2]{{#1}\vee_{\scriptstyle\it Bool}{#2}} -\newcommand{\builtinXor}[2]{{#1}\oplus_{\scriptstyle\it Bool}{#2}} -\newcommand{\builtinNot}[1]{\neg_{\scriptstyle\it Bool}{#1}} -\newcommand{\builtinImplies}[2]{{#1}\Rightarrow_{\scriptstyle\it Bool}{#2}} - -\newcommand{\builtinIntPlus}[2]{{#1}\mathrel{+_{\scriptstyle\it Int}}{#2}} -\newcommand{\builtinIntMinus}[2]{{#1}\mathrel{-_{\scriptstyle\it Int}}{#2}} -\newcommand{\builtinIntTimes}[2]{{#1}\mathrel{\ast_{\scriptstyle\it Int}}{#2}} -\newcommand{\builtinIntDiv}[2]{{#1}\mathrel{\div_{\scriptstyle\it Int}}{#2}} -\newcommand{\builtinIntMod}[2]{{#1}\mathrel{\%_{\scriptstyle\it Int}}{#2}} - - -% K Blocks %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\newlength{\commentIndent} -\setlength{\commentIndent}{1em} - -\newlength{\kblock@indent} -\newenvironment{kblock}[1][\k@style]{% -\ifk@tight% -\small% -\fi% -\newcommand{\kblock@arg}{#1}% -\setlength{\kblock@indent}{\parindent}% -\ifthenelse{\equal{#1}{bubble}}{% -\renewcommand{\kall}{\ball}% -\renewcommand{\kallLarge}{\ballLarge}% -\renewcommand{\kprefix}{\bprefix}% -\renewcommand{\ksuffix}{\bsuffix}% -\renewcommand{\kmiddle}{\bmiddle}% -\renewcommand{\kdot}{\bdot}% -\renewcommand{\AnyVar}{\bAnyVar}% -}{\ifthenelse{\equal{#1}{math}}{% -\renewcommand{\kall}{\mall}% -\renewcommand{\kallLarge}{\mallLarge}% -\renewcommand{\kprefix}{\mprefix}% -\renewcommand{\ksuffix}{\msuffix}% -\renewcommand{\kmiddle}{\mmiddle}% -\renewcommand{\kdot}{\mdot}% -\renewcommand{\AnyVar}{\mAnyVar}% -}% -{\ifthenelse{\equal{#1}{text}}{% -\ifk@poster% - \setlength{\parindent}{\commentIndent}% - \indent% - \begin{Sbox}% - \begin{minipage}{50em}% - \addtolength{\parskip}{.5\baselineskip}% -\else% -\fi% -}{% -}}}% -}{% -\ifthenelse{\equal{\kblock@arg}{text}}{% -\ifk@poster% - \ \end{minipage}% - \end{Sbox}% - \begin{tikzpicture} - \node[comment]{\TheSbox}; - \end{tikzpicture}% - \k@markPosition% -\fi% -}{% -}% -\setlength{\parindent}{\kblock@indent}% -\par\ \par% -} - -% Modules %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\newenvironment{module}[1]{% - \tikzset{comment/.style={basic comment,fill=black!10}}% - \par\noindent% - \text{\scshape module #1}% - \setlength{\parindent}{1em}% - \par\ \par% -}{% - \par\noindent\text{\scshape end module}% - \par\ \par% -} - -\newenvironment{commentModule}{% - \setlength{\parindent}{1em}% - \par\ \par% -}{% - \par\ \par% -} - -\newcommand{\moduleName}[1]{#1} -\newcommand{\including}[1]{\par\text{\scshape imports}\ #1\par\ \par} -\newcommand{\modulePlus}{$+$} - - -% Syntax %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -% Sorts and kinds. -\newcommand{\sorts}[1]{} -\newcommand{\sort}[1]{\text{\itshape #1}} -\newcommand{\kind}[1]{\text{\itshape #1}} - -\newcommand{\syntaxKeyword}{\mbox{\scshape syntax}\hspace{1em}} - -% Syntax rules. -\newlength{\syntaxlength} % The amount of indention for continued rules. - -\newcommand{\syntax}[3][\defSort]{\rulebox{% -\syntaxKeyword$#1\mathrel{::=}{#2}$ \ifthenelse{\equal{#3}{}}{}{[#3]}% -}\k@markPosition% -} -\newcommand{\syntaxCont}[3][\defSort]{\par\indent\rulebox{% - $\setlength{\syntaxlength}{\widthof{$\mathrel{::=}$}}% - \setlength{\syntaxlength}{.5\syntaxlength}% - \addtolength{\syntaxlength}{\widthof{\syntaxKeyword$#1$}}% - \hspace{\syntaxlength}% - \;\;\!\mid\;{#2}$ \ifthenelse{\equal{#3}{}}{}{[#3]}% - }\k@markPosition% -} -\newcommand{\syntaxContL}[3]{{\small%\par\indent% -$\mid\;{#2}$ \ifthenelse{\equal{#3}{}}{}{[#3]\;}% -}} - - -\newenvironment{syntaxBlock}[1]{\newcommand{\defSort}{#1}\par\indent\ }{\par\ \par} - - -% Non-terminals. -\newcommand{\nonTerminal}[1]{\text{\itshape #1}\/} - -% Terminals. -\newcommand{\terminal}[1]{\ensuremath\mathrel{\text{\ttfamily #1}}} -\newcommand{\terminalNoSpace}[1]{\ensuremath\mathord{\text{\ttfamily #1}}} - -% Tags. -\newcommand{\kassoc}{assoc} -\newcommand{\kcomm}{comm} -\newcommand{\khybrid}{{\color{blue}hybrid}} -%\newcommand{\klabel}[1]{} -% \newcommand{\ignoreThisLabel}{} % this is used to figure out whether we should ignore an attribute (like the name) -%\newcommand{\kattribute}[1]{\xifstrequal{#1}{\ignoreThisLabel}{}{{\color{blue}#1}}} -\newcommand{\kattribute}[1]{{\color{blue}#1}} -\newcommand{\kid}[1]{id: {#1}} -\newcommand{\kditto}{ditto} -\newcommand{\karity}[1]{{\color{blue}arity(#1)}} -\newcommand{\kstrict}[2]{{% - \color{blue}strict% - \ifx&% - \else% - (#1)% - \fi% - \ifx&% - \else% - in (#2)% - \fi% -}} -\newcommand{\kseqstrict}[2]{{% - \color{blue}seqstrict% - \ifx&% - \else% - (#1)% - \fi% - \ifx&% - \else% - in (#2)% - \fi% -}} - - -% Configuration %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\newcommand{\kconfig}[1]{\par% - {\sc configuration:}\par% - \ensuremath{#1}\k@markPosition% - \par\ \par% -} - -\newcommand{\kconfigb}[1]{\begin{kblock}\kconfig{#1}\end{kblock}} - -% Cells %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\ifk@poster -%%% Tooltips. - -% Following a how-to guide for Adobe InDesign, we create tooltips for items by -% overlaying them with a transparent button. -% -% For documentation on the JavaScript objects, see the JavaScript for Acrobat -% API Reference at http://www.adobe.com/devnet/acrobat/javascript.html -% -% For documentation on the PDF code, see the PDF reference manual at -% http://www.adobe.com/devnet/pdf/pdf_reference.html - -% These definitions will hold the payload. They have to be global because -% hyperref definitions vanish when the document starts(?). -\def\k@tooltipText{}% -\edef\k@tooltipString{}% - -% The "user name" of fields is the user visible name of this entity. For -% (non-readonly) buttons, it shows up as tooltip when the mouse hovers over it. -% Unfortunately, the hyperref package does not allow specifying the user name; -% thus, by means of a small hack, we push in some raw PDF code when hyperref -% creates a PushButton object. The raw PDF code is appended to the "flags" -% field \Fld@flags. See the button creation macro "\PDFForm@Push" in the -% hpdftex.def driver. -% -% For the definition of the user name property of fields, see section 12.7.3.1 -% in the PDF specification. -\let\k@hyPushButtonFlags=\HyField@FlagsPushButton -\gdef\HyField@FlagsPushButton{% - % Execute the original macro - \k@hyPushButtonFlags% - % Save the current flags and add the user visible name via /TU ("text user"?). - \let\k@currentFlags=\Fld@flags% - \pdfstringdef\k@tooltipString{\k@tooltipText}% - \edef\Fld@flags{/TU (\k@tooltipString)\k@currentFlags}% - \edef\Fld@bordercolor{\space}% -} - -\newcounter{k@tooltipCounter} - -\newcommand{\k@withTooltip}[2]{% - % #1 is the target / box, #2 is the tooltip - \def\k@tooltipText{#2} - \hbox{\PushButton[name=tooltip\the\c@k@tooltipCounter, - borderwidth=0, - % The focus handler executes before the click happens, so the - % button is set to "not interact" just before it would change - % its visual appearance. - onfocus={ var t = this.getField("tooltip\the\c@k@tooltipCounter"); - t.highlight = highlight.n; } - ]{#1}}% - \addtocounter{k@tooltipCounter}{1}% -} - -% Buttons are form elements and require a surrounding Form environment. -% \AtBeginDocument{\begin{Form}} -% \AtEndDocument{\end{Form}} -\else -\newcommand{\k@withTooltip}[2]{#1} -\fi - -%%% Cell contents. - -\newcommand{\reduceTop}[2]{{#1}\Rightarrow{#2}} -\newcommand{\reduceTopS}[2]{{#1}\rightharpoonup{#2}} -\newcommand{\reduce}[2]{\hbox{% - \begin{tikzpicture}[baseline=(top.base), - inner xsep=0pt, - inner ysep=.3333ex, - minimum width=2em] - \path node (top) {$#1$\strut} - (top.south) - node (bottom) [anchor=north, inner ysep=.5ex] {$#2$\strut}; - %%% Draw the horizontal line: - % Line with chevron. - %\path[draw,thin,solid] let \p1 = (current bounding box.west), - % \p2 = (current bounding box.east), - % \p3 = (top.south) - % in (top.south) ++(0,-1.5pt) -- ++(-2pt,1.5pt) -- (\x1,\y3) - % (top.south) ++(0,-1.5pt) -- ++(2pt,1.5pt) -- (\x2,\y3); - %%% Other options: - % Solid line. - \path[draw,thin,solid] let \p1 = (current bounding box.west), - \p2 = (current bounding box.east), - \p3 = (top.south) - in (\x1,\y3) -- (\x2,\y3); - % Solid arrow (augmenting the solid line). - \path[fill] (top.south) ++(2pt,0) -- ++(-4pt,0) -- ++(2pt,-1.5pt) -- cycle; - \end{tikzpicture}% -}} -\newcommand{\reduceS}[2]{\hbox{% - \begin{tikzpicture}[baseline=(top.base), - inner xsep=0pt, - inner ysep=.3333ex, - minimum width=2em] - \path node (top) {$#1$\strut} - (top.south) - node (bottom) [anchor=north] {$#2$\strut}; - \path[draw,thin,densely dashed] let \p1 = (current bounding box.west), - \p2 = (current bounding box.east), - \p3 = (top.south) - in (\x1,\y3) -- (\x2,\y3); - \end{tikzpicture}% -}} -\newcommand{\kra}{\curvearrowright} -\newcommand{\kcomma}{\mathpunct{\textbf{,}}} -\newcommand{\kvalue}[1]{{\color{red}#1}} -\newcommand{\constant}[2][none]{% - \k@withTooltip{\text{\sffamily #2}}{syntax #1 ::= "#2"}% -} - -\newcommand{\typedTo}[1]{{\it :}#1} - -\newcommand{\variable}[3][none]{% -\k@withTooltip{\text{\ensuremath{\it #2\ifthenelse{\equal{#3}{user}}{\typedTo{#1}}{}}}\/}{Variable #2:#1}% -} - -\newcommand{\displayGreek}[1]{% - \text{\Large\ensuremath{\displaystyle #1}}% -} - -\newcommand{\prefixOp}{\terminalNoSpace} -\newcommand{\dotCt}[1]{% -\ensuremath{{\raise.3ex\hbox{\ensuremath{\kdot}}}_{\color{black!60}\scriptstyle\it \!#1}} -% \k@withTooltip{\raise.3ex\hbox{\ensuremath{\kdot}}}{Constant Sort: #1}% -} - -%%% Mathematical notation. - -\newcommand{\mcell}[3]{{\ifthenelse{\equal{#1}{}}{\color{white!50!black}}{\color{#1!50!black}}\left\langle{#3}\ifthenelse{\equal{#1}{}}{\color{white!50!black}}{\color{#1!50!black}}\right\rangle_{\sf #2}}} -\newcommand{\ellipses}{\mathrel{\cdot\!\!\cdot\!\!\cdot}} -\newcommand{\mallLarge}{\mall} -\newcommand{\mall}[3]{\mcell{#1}{#2}{{#3}}} -\newcommand{\mprefix}[3]{\mcell{#1}{#2}{{#3}\ {\color{#1!50!black}\ellipses}}} -\newcommand{\msuffix}[3]{\mcell{#1}{#2}{{\color{#1!50!black}\ellipses}\ {#3}}} -\newcommand{\mmiddle}[3]{\mcell{#1}{#2}{{\color{#1!50!black}\ellipses}\ {#3}\ {\color{#1!50!black}\ellipses}}} -\newcommand{\mdot}{\cdot} -\newcommand{\mAnyVar}[2]{\_\ifthenelse{\equal{#2}{user}}{\typedTo{#1}}{}} - -%%% Bubble notation. - -\newcommand{\ball}[3]{\kcell{#1}{#2}{#3}{convex}{convex}} -\newcommand{\ballLarge}[3]{% - \kcell{#1}% - {#2}% - {% - #3% - }% - {convex}% - {convex}% -} -\newcommand{\bprefix}[3]{\kcell{#1}{#2}{#3}{convex}{none}} -\newcommand{\bsuffix}[3]{\kcell{#1}{#2}{#3}{none}{convex}} -\newcommand{\bmiddle}[3]{\kcell{#1}{#2}{#3}{none}{none}} -\newcommand{\bdot}{{\scriptscriptstyle\bullet}} -\newcommand{\bAnyVar}[2]{% - \k@withTooltip{\mbox{---}\ifthenelse{\equal{#2}{user}}{\typedTo{#1}}{}}{Variable \_:#1}% -} - -\tikzset{ - cell/.style={ - line width=1pt, - draw=#1!50!black, - shade, - shading=axis, - top color=#1!20, - bottom color=#1!20!white!90!black, - }, - body/.style={ - rounded rectangle, - rounded rectangle arc length=180, - minimum width=\ifk@tight 1em \else 3em \fi, - minimum height=4ex, - inner ysep=.3333em, - inner xsep=.3333em - }, - label/.style={ - rectangle, - inner xsep=.5ex, - inner ysep=.5ex, - text depth=.15em, -% font=\sffamily\footnotesize - }, -} - - -%%% The main bubble drawing method \kcell. - -\pgfdeclarelayer{background} -\pgfsetlayers{background,main} - -\newlength{\k@cellContentWidth} -\newlength{\k@cellContentHeight} -\newlength{\k@labelXShift} -\newlength{\k@ruptureStepSize} - -% Cell drawing happens roughly as follows: -% 1) The cell content is placed in the image. -% 2) TikZ fits a 'rounded rectangle' node around the content. This node, which -% we call 'body' here, remains invisible; its anchors serve as reference points. -% 3) The label is placed on the top left of the cell body. -% 4) The cell outline is drawn and filled on the background layer, that is, -% behind the already placed cell content. -% 5) Some vertical space is added around the whole drawing. -\newcommand{\kcell}[5]{\hbox{% - \begingroup - \def\cellColor{#1}% - \def\cellLabel{\textsf{\footnotesize\strut #2}}% The strut ensures even label height. - \def\cellContent{$#3$}% - % Parameters #4 and #5 determine whether the west and east arc are curved - % or straight ("whole" or "ruptured"). - - \begin{tikzpicture}[baseline=(cell label.base)] - \begin{scope}[inner sep=0pt,outer sep=0pt,anchor=base west] - % Beside the cell content, also draw an empty node a bit wider than - % the cell label. That way, the cell body will always be wide enough - % for the label. - \path node (cell content) {\cellContent} - node {\phantom{\cellLabel}\hbox to \ifk@tight 1pt \else 2em \fi {}}; - \end{scope} - % Determine the size of the cell content. - \def\k@cellContentBBox{\pgfpointdiff{\pgfpointanchor{current bounding box}{south west}} - {\pgfpointanchor{current bounding box}{north east}}} - \pgfextractx{\k@cellContentWidth}{\k@cellContentBBox}% - \pgfextracty{\k@cellContentHeight}{\k@cellContentBBox}% - - \begin{pgfonlayer}{background} - \ifdraft{% - \path (cell content.center) - node (cell body) [body, - rectangle, - anchor=center, - text width=\k@cellContentWidth, - text height=\k@cellContentHeight] {}; - }{% - % Let TikZ find the best rounded rectangle around the content. - \path (cell content.center) - node (cell body) [body, - anchor=center, - text width=\k@cellContentWidth, - text height=\k@cellContentHeight, -rectangle,rectangle -% rounded rectangle west arc=#4, -% rounded rectangle east arc=#5 -] {}; - } - \end{pgfonlayer} - - % Place the cell label relative to the rounded rectangle. If the left side - % is straight, shift the label a little to the right to avoid an ugly - % long vertical left side. - \ifthenelse{\equal{#4}{convex}}{% - \setlength{\k@labelXShift}{0pt}% - }{ - \setlength{\k@labelXShift}{1ex} - }% - - \path (cell body.north west) - ++(\k@labelXShift,.6ex) - node (cell label) [label,anchor=base west] {\cellLabel}; - - % Finally, draw the background of the cell behind the content. - \begin{pgfonlayer}{background} - % Decide how to draw the cell's west and east side. - \ifthenelse{\equal{#4}{convex}}{% - \def\cellWestArc{ arc (90:270:\n4 and \n3) -- (cell body.south west) }% - }{% - \ifdraft{% - \def\cellWestArc{ |- (cell body.south west) } - }{% - % This yields a rounded zig zag pattern (starting outward). - \def\cellWestArc{ { [rounded corners=.25ex] - \foreach \signPrefix in {-,0,-,0,-,0,-,0} {% - -- ++(\signPrefix{}.75\k@ruptureStepSize,-\k@ruptureStepSize)} - } - }% - }% - }% - \ifthenelse{\equal{#5}{convex}}{% - \def\cellEastArc{ arc (-90:90:\n4 and \n3) }% - }{% - \ifdraft{% - \def\cellEastArc{ -- (cell body.north east) } - }{% - \def\cellEastArc{ { [rounded corners=.25ex] - \foreach \signPrefix in {0,-,0,-,0,-,0,-} {% - -- ++(\signPrefix{}.75\k@ruptureStepSize,\k@ruptureStepSize)} - } - }% - }% - }% - - % Draw the cell outline - \path[cell=\cellColor] - % Compute half of the body's height. The value is the - % radius for the arced sides; it also determines the size - % of the zig zag pattern of ruptured sides. - let \p1 = (cell body.north east), - \p2 = (cell body.center), - \n3 = {\y1 - \y2}, - \n4 = {\ifk@tight 1ex + \n3 / 5 \else \n3 \fi} - in - \pgfextra{% - \setlength{\k@ruptureStepSize}{\n3}% - \setlength{\k@ruptureStepSize}{.25\k@ruptureStepSize}% - }% - - % Draw counter-clock-wise, starting from the - % lower right corner. - (cell body.south east) - - % Right - \cellEastArc - - % Top - { [rounded corners=.2em] - -| (cell label.north east) - -- (cell label.north west) - |- (cell body.north west) - } - % A little offset to the left for a more pleasant look - -- ++(-.2em,0pt) - - % Left - \cellWestArc - - % Bottom (just close the path) - -- cycle; - \end{pgfonlayer} - - % Add extra space above and below the cell. - \path[use as bounding box] (current bounding box.south west) ++(0,-.3333em) - rectangle (current bounding box.north east) ++(0,.3333em); - \end{tikzpicture}% - \endgroup -}} - - -% Rules and Equations %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - -\newcommand{\when}[1]{% - \hspace{2em} when \ensuremath{#1}% - \k@markPosition% -} -\newcommand{\whenEns}[1]{% - \hspace{2em} ensures \ensuremath{#1}% - \k@markPosition% -} -\newcommand{\whenReq}[1]{% - \hspace{2em} requires \ensuremath{#1}% - \k@markPosition% -} - -%%% Context - -% Context. -\newcommand{\kcontext}[5][]{ -\ksentence{context}{#1}{#2}{#3}{#4}{#5} -} - -\newcommand{\kcontextb}[4]{\begin{kblock}\kcontext{#1}{#2}{#3}{#4}\end{kblock}} - - -\newcommand{\khole}{\Box} - -%%% Equations and structural rules. - -\newcommand{\k@ruleLabel}[2]{% - \ifthenelse{\equal{#1}{}}{\mbox{\scshape #2}}{\k@withTooltip{\mbox{\scshape #2}}{Rule Label: #1}}% -} - -\newcommand{\rulebox}[1]{\hbox{#1}} - -\newcommand{\mequation}[3]{% - \wrapRules{% - \rulebox{% - \k@ruleLabel{#1}{macro}\hspace{1em}$#2 = #3$% - }% - \k@markPosition% - }% -} -\newcommand{\cmequation}[4]{% - \wrapRules{% - \rulebox{% - \k@ruleLabel{#1}{macro}\hspace{1em}$#2 = #3$% - \when{#4}% - }% - \k@markPosition% - }% -} - -\newcommand{\wrapRules}[1]{\par\indent#1\par\ \par} -%%% Rules. -\newcommand{\ruleAttributes}[1]{\hfill[#1]} - -\newcommand{\ksentence}[7][]{% - \par\indent - \k@ruleLabel{#3}{#2}\hspace{1em}$% - \ifthenelse{\equal{#1}{}}{}{% - \left(% - }% - #4% - \ifthenelse{\equal{#1}{}}{}{% - \right)% - }% - $% - \ifthenelse{\equal{#5}{}}{}{% - \whenReq{#5}% - }% - \ifthenelse{\equal{#6}{}}{}{% - \whenEns{#6}% - }% - \k@markPosition% - \ifthenelse{\equal{#7}{}}{}{% - \ruleAttributes{#7}% - }% - \par\ \par -} - -\newcommand{\krule}[6][]{% -\ksentence[#6]{rule}{#1}{#2}{#3}{#4}{#5} -} - -\newcommand{\kruleb}[4]{\begin{kblock}\krule[#1]{#2}{#3}{#4}\end{kblock}} - - -\ifk@poster -\newcommand{\myskip}{\bigskip} -\else -\renewcommand{\when}[1]{\par{}\hspace{2em} when \ensuremath{#1}} -\renewcommand{\ruleAttributes}[1]{\par{}\hspace{2em} [#1]} -\renewcommand{\rulebox}[1]{\parbox[b]{\columnwidth}{#1}} -\renewcommand{\wrapRules}[1]{\par{\parbox[b]{\columnwidth}{#1}}\par\ \par} -\renewcommand{\k@ruleLabel}[2]{% - \ifthenelse{\equal{#1}{\textbackslash !}}{\mbox{\scshape #2}}{\k@withTooltip{\mbox{\scshape #2 \kattribute{#1}}}{Rule Label: #1}}\\% -% \global\def\ignoreThisLabel{#1}% -} -\newcommand{\myskip}{\smallskip} -\fi - - -\makeatother - -\usepackage{listings} - - -\lstnewenvironment{asciik}{ - \lstset{ - language=k, - basicstyle=\small, - tabsize=2, - %frame=tb, - columns=flexible, - mathescape=false, - upquote=true, -% literate= -% {"}{\textquotedbl}1 - } -}{} -\lstdefinelanguage{k}{ - upquote=true, - morekeywords={kompile, kast, krun, require, HOLE, configuration, module, end, imports, rule, macro, op, ops, syntax, sort, sorts, subsort, subsorts, context, HOLE, hybrid, strict, seqstrict, binder, color, latex, kvar, transition, superheat, supercool, search, rewrite, prec, gather, stream, multiplicity, when}, - emph={[3]Map, Set, Bag, List, K, KLabel, KResult, KProper, CellLabel, SetItem, BagItem, ListItem, MapItem, Int, Bool, String, Id}, - emphstyle={[3]\textit}, - literate= - {LT}{$<$}3 - {LEQ}{$<=$}4 -% {.K}{$\kdot{\it K}$}2 -% {.List}{$\kdot{\it List}$}4 - {PROMPT}{\$}1 - {...<}{${\ellipses}\langle$}2 - {>}{$\rangle$}1 - {>...}{$\rangle{\ellipses}$}2 - {+Int}{$+{\rm\scriptstyle Int}$}4 - {*Int}{$*{\rm\scriptstyle Int}$}4 - {/Int}{$/{\rm\scriptstyle Int}$}4 - {LeqInt}{${<}{=}{\rm\scriptstyle Int}$}9 - {!=Int}{${!}{=}{\rm\scriptstyle Int}$}5 - {==Bool}{${=}{=}{\rm\scriptstyle Bool}$}7 - {=/=Bool}{${=}{/}{=}{\rm\scriptstyle Bool}$}9 - {notBool}{${\tt not}{\rm\scriptstyle Bool}$}5 - {<}{$\langle$}1 - {_}{$\_$}1 {~}{$\_$}1 - {=>}{$\;=\!>$}5 - {->}{{$->$}}3 - {~>}{{$\sim\!\!>$}}3 - {|->}{$\;|-\!\!>$}5 -} -\newcommand{\ka}[1]{\mbox{\lstinline[language=k]{#1}}} diff --git a/k-distribution/include/kframework/z3/basic.smt2 b/k-distribution/include/kframework/z3/basic.smt2 deleted file mode 100644 index 0bcd9fae7f0..00000000000 --- a/k-distribution/include/kframework/z3/basic.smt2 +++ /dev/null @@ -1,35 +0,0 @@ -(set-option :auto-config false) -(set-option :smt.mbqi false) - -; int extra -(define-fun int_max ((x Int) (y Int)) Int (ite (< x y) y x)) -(define-fun int_min ((x Int) (y Int)) Int (ite (< x y) x y)) -(define-fun int_abs ((x Int)) Int (ite (< x 0) (- 0 x) x)) - -; bool to int -(define-fun smt_bool2int ((b Bool)) Int (ite b 1 0)) - -; set axioms -(declare-sort IntSet) - -(declare-fun smt_set_cup (IntSet IntSet) IntSet) -(declare-fun smt_set_ele (Int) IntSet) -(declare-fun smt_set_emp () IntSet) -(declare-fun smt_set_mem (Int IntSet) Bool) - -(declare-fun smt_set_lt ((IntSet) (IntSet)) Bool) -(declare-fun smt_set_le ((IntSet) (IntSet)) Bool) - -; sequence axioms -(declare-sort IntSeq) - -(declare-fun smt_seq_concat (IntSeq IntSeq) IntSeq) -(declare-fun smt_seq_elem (Int) IntSeq) -(declare-fun smt_seq_nil () IntSeq) -(declare-fun smt_seq_len (IntSeq) Int) - -(declare-fun smt_seq_sum (IntSeq) Int) -(declare-fun smt_seq2set (IntSeq) IntSet) -(declare-fun smt_seq_sorted (IntSeq) Bool) - -(declare-fun smt_seq_filter (Int IntSeq) IntSeq) diff --git a/k-distribution/include/kframework/z3/floating_point.smt2 b/k-distribution/include/kframework/z3/floating_point.smt2 deleted file mode 100644 index c23d8af6969..00000000000 --- a/k-distribution/include/kframework/z3/floating_point.smt2 +++ /dev/null @@ -1,25 +0,0 @@ -(set-logic QF_FPA) - -; TODO: remove sort/fun declarations that are not actually used -; set axioms -(declare-sort IntSet) - -(declare-fun smt_set_cup (IntSet IntSet) IntSet) -(declare-fun smt_set_ele (Int) IntSet) -(declare-fun smt_set_emp () IntSet) -(declare-fun smt_set_mem (Int IntSet) Bool) - -(declare-fun smt_set_lt ((IntSet) (IntSet)) Bool) -(declare-fun smt_set_le ((IntSet) (IntSet)) Bool) - -; sequence axioms -(declare-sort IntSeq) - -(declare-fun smt_seq_concat (IntSeq IntSeq) IntSeq) -(declare-fun smt_seq_elem (Int) IntSeq) -(declare-fun smt_seq_nil () IntSeq) -(declare-fun smt_seq_len (IntSeq) Int) - -(declare-fun smt_seq_sum (IntSeq) Int) -(declare-fun smt_seq2set (IntSeq) IntSet) -(declare-fun smt_seq_sorted (IntSeq) Bool) diff --git a/k-distribution/include/kframework/z3/list.smt2 b/k-distribution/include/kframework/z3/list.smt2 deleted file mode 100644 index 42a442dee5f..00000000000 --- a/k-distribution/include/kframework/z3/list.smt2 +++ /dev/null @@ -1,40 +0,0 @@ -(set-option :auto-config false) -(set-option :smt.mbqi false) - -; int extra -(define-fun int_max ((x Int) (y Int)) Int (ite (< x y) y x)) -(define-fun int_min ((x Int) (y Int)) Int (ite (< x y) x y)) -(define-fun int_abs ((x Int)) Int (ite (< x 0) (- 0 x) x)) - -; bool to int -(define-fun smt_bool2int ((b Bool)) Int (ite b 1 0)) - -; set axioms -(declare-sort IntSet) - -(declare-fun smt_set_cup (IntSet IntSet) IntSet) -(declare-fun smt_set_ele (Int) IntSet) -(declare-fun smt_set_emp () IntSet) -(declare-fun smt_set_mem (Int IntSet) Bool) - -(declare-fun smt_set_lt ((IntSet) (IntSet)) Bool) -(declare-fun smt_set_le ((IntSet) (IntSet)) Bool) - -; sequence axioms -(declare-sort IntSeq) - -(declare-fun smt_seq_concat (IntSeq IntSeq) IntSeq) -(declare-fun smt_seq_elem (Int) IntSeq) -(declare-fun smt_seq_nil () IntSeq) -(declare-fun smt_seq_len (IntSeq) Int) - -(declare-fun smt_seq_sum (IntSeq) Int) -(declare-fun smt_seq2set (IntSeq) IntSet) -(declare-fun smt_seq_sorted (IntSeq) Bool) - -(assert (forall ((s1 IntSeq) (s2 IntSeq) (s3 IntSeq)) (= (smt_seq_concat s1 (smt_seq_concat s2 s3)) (smt_seq_concat (smt_seq_concat s1 s2) s3)))) - -(assert (forall ((e1 Int) (e2 Int) (s1 IntSeq) (s2 IntSeq)) (= (= (smt_seq_concat (smt_seq_elem e1) s1) (smt_seq_concat (smt_seq_elem e2) s2)) (and (= e1 e2) (= s1 s2))))) - -(declare-fun smt_seq_filter (Int IntSeq) IntSeq) -;(assert (forall ((v Int) (e Int)) (= (smt_seq_filter v (smt_seq_elem e)) (ite (= v e) smt_seq_nil (smt_seq_elem e))))) diff --git a/k-distribution/include/kframework/z3/search_tree.smt2 b/k-distribution/include/kframework/z3/search_tree.smt2 deleted file mode 100644 index 27c7c86a1d7..00000000000 --- a/k-distribution/include/kframework/z3/search_tree.smt2 +++ /dev/null @@ -1,50 +0,0 @@ -(set-option :smt.mbqi.max_iterations 15) - -; int extra -(define-fun int_max ((x Int) (y Int)) Int (ite (< x y) y x)) -(define-fun int_min ((x Int) (y Int)) Int (ite (< x y) x y)) -(define-fun int_abs ((x Int)) Int (ite (< x 0) (- 0 x) x)) - -; bool to int -(define-fun smt_bool2int ((b Bool)) Int (ite b 1 0)) - -; sets as arrays -(define-sort IntSet () (Array Int Bool)) -(define-fun smt_set_mem ((x Int) (s IntSet)) Bool (select s x)) -(define-fun smt_set_add ((s IntSet) (x Int)) IntSet (store s x true)) -(define-fun smt_set_emp () IntSet ((as const IntSet) false)) -(define-fun smt_set_cup ((s1 IntSet) (s2 IntSet)) IntSet ((_ map or) s1 s2)) -(define-fun smt_set_cap ((s1 IntSet) (s2 IntSet)) IntSet ((_ map and) s1 s2)) -(define-fun smt_set_com ((s IntSet)) IntSet ((_ map not) s)) -(define-fun smt_set_ele ((x Int)) IntSet (smt_set_add smt_set_emp x)) -(define-fun smt_set_dif ((s1 IntSet) (s2 IntSet)) IntSet (smt_set_cap s1 (smt_set_com s2))) -(define-fun smt_set_sub ((s1 IntSet) (s2 IntSet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) -(define-fun smt_set_lt ((s1 IntSet) (s2 IntSet)) Bool (forall ((__mbqi__i Int) (__mbqi__j Int)) (implies (>= __mbqi__i __mbqi__j) (not (and (select s1 __mbqi__i) (select s2 __mbqi__j)))))) -(define-fun smt_set_le ((s1 IntSet) (s2 IntSet)) Bool (forall ((__mbqi__i Int) (__mbqi__j Int)) (implies (> __mbqi__i __mbqi__j) (not (and (select s1 __mbqi__i) (select s2 __mbqi__j)))))) - -; hardcoded 32bit unsigned mi sets as arrays -(define-sort MInt () (_ BitVec 32)) -(define-sort MIntSet () (Array MInt Bool)) -(define-fun smt_miset_mem ((x MInt) (s MIntSet)) Bool (select s x)) -(define-fun smt_miset_add ((s MIntSet) (x MInt)) MIntSet (store s x true)) -(define-fun smt_miset_emp () MIntSet ((as const MIntSet) false)) -(define-fun smt_miset_cup ((s1 MIntSet) (s2 MIntSet)) MIntSet ((_ map or) s1 s2)) -(define-fun smt_miset_cap ((s1 MIntSet) (s2 MIntSet)) MIntSet ((_ map and) s1 s2)) -(define-fun smt_miset_com ((s MIntSet)) MIntSet ((_ map not) s)) -(define-fun smt_miset_ele ((x MInt)) MIntSet (smt_miset_add smt_miset_emp x)) -(define-fun smt_miset_dif ((s1 MIntSet) (s2 MIntSet)) MIntSet (smt_miset_cap s1 (smt_miset_com s2))) -(define-fun smt_miset_sub ((s1 MIntSet) (s2 MIntSet)) Bool (= smt_miset_emp (smt_miset_dif s1 s2))) -(define-fun smt_miset_lt ((s1 MIntSet) (s2 MIntSet)) Bool (forall ((__mbqi__i MInt) (__mbqi__j MInt)) (implies (bvuge __mbqi__i __mbqi__j) (not (and (select s1 __mbqi__i) (select s2 __mbqi__j)))))) -(define-fun smt_miset_le ((s1 MIntSet) (s2 MIntSet)) Bool (forall ((__mbqi__i MInt) (__mbqi__j MInt)) (implies (bvugt __mbqi__i __mbqi__j) (not (and (select s1 __mbqi__i) (select s2 __mbqi__j)))))) - -; sequence axioms -(declare-sort IntSeq) - -(declare-fun smt_seq_concat (IntSeq IntSeq) IntSeq) -(declare-fun smt_seq_elem (Int) IntSeq) -(declare-fun smt_seq_nil () IntSeq) -(declare-fun smt_seq_len (IntSeq) Int) - -(declare-fun smt_seq_sum (IntSeq) Int) -(declare-fun smt_seq2set (IntSeq) IntSet) -(declare-fun smt_seq_sorted (IntSeq) Bool) diff --git a/k-distribution/include/kframework/z3/sorted_list.smt2 b/k-distribution/include/kframework/z3/sorted_list.smt2 deleted file mode 100644 index 08128bc5373..00000000000 --- a/k-distribution/include/kframework/z3/sorted_list.smt2 +++ /dev/null @@ -1,71 +0,0 @@ -(set-option :auto-config false) -(set-option :smt.mbqi false) - -; int extra -(define-fun int_max ((x Int) (y Int)) Int (ite (< x y) y x)) -(define-fun int_min ((x Int) (y Int)) Int (ite (< x y) x y)) -(define-fun int_abs ((x Int)) Int (ite (< x 0) (- 0 x) x)) - -; bool to int -(define-fun smt_bool2int ((b Bool)) Int (ite b 1 0)) - -; set axioms -(declare-sort IntSet) - -(declare-fun smt_set_cup (IntSet IntSet) IntSet) -(declare-fun smt_set_ele (Int) IntSet) -(declare-fun smt_set_emp () IntSet) -(declare-fun smt_set_mem (Int IntSet) Bool) - -(assert (forall ((s1 IntSet) (s2 IntSet) (s3 IntSet)) (= (smt_set_cup (smt_set_cup s1 s2) s3) (smt_set_cup s1 (smt_set_cup s2 s3))))) -(assert (forall ((s1 IntSet) (s2 IntSet)) (= (smt_set_cup s1 s2) (smt_set_cup s2 s1)))) -(assert (forall ((e Int)) (not (= (smt_set_ele e) smt_set_emp)))) - -(assert (forall ((s IntSet)) (= (smt_set_cup s s) s))) - -(declare-fun smt_set_lt ((IntSet) (IntSet)) Bool) -(declare-fun smt_set_le ((IntSet) (IntSet)) Bool) - -(assert (forall ((s1 IntSet) (s2 IntSet) (s3 IntSet)) (= (smt_set_lt (smt_set_cup s1 s2) s3) (and (smt_set_lt s1 s3) (smt_set_lt s2 s3))))) -(assert (forall ((s1 IntSet) (s2 IntSet) (s3 IntSet)) (= (smt_set_lt s1 (smt_set_cup s2 s3)) (and (smt_set_lt s1 s2) (smt_set_lt s1 s3))))) -(assert (forall ((e1 Int) (e2 Int)) (= (smt_set_lt (smt_set_ele e1) (smt_set_ele e2)) (< e1 e2)))) -(assert (forall ((s IntSet)) (smt_set_lt s smt_set_emp))) -(assert (forall ((s IntSet)) (smt_set_lt smt_set_emp s))) - -(assert (forall ((s1 IntSet) (s2 IntSet) (s3 IntSet)) (= (smt_set_le (smt_set_cup s1 s2) s3) (and (smt_set_le s1 s3) (smt_set_le s2 s3))))) -(assert (forall ((s1 IntSet) (s2 IntSet) (s3 IntSet)) (= (smt_set_le s1 (smt_set_cup s2 s3)) (and (smt_set_le s1 s2) (smt_set_le s1 s3))))) -(assert (forall ((e1 Int) (e2 Int)) (= (smt_set_le (smt_set_ele e1) (smt_set_ele e2)) (<= e1 e2)))) -(assert (forall ((s IntSet)) (smt_set_le s smt_set_emp))) -(assert (forall ((s IntSet)) (smt_set_le smt_set_emp s))) - -(assert (forall ((e Int) (s1 IntSet) (s2 IntSet)) (! (implies (and (smt_set_le s1 (smt_set_ele e)) (smt_set_le (smt_set_ele e) s2)) (smt_set_le s1 s2)) - :pattern ((smt_set_le s1 (smt_set_ele e)) (smt_set_le (smt_set_ele e) s2)) - :pattern ((smt_set_ele e) (smt_set_le s1 s2)) -))) -(assert (forall ((e Int) (s1 IntSet) (s2 IntSet)) (implies (and (smt_set_lt s1 (smt_set_ele e)) (smt_set_le (smt_set_ele e) s2)) (smt_set_lt s1 s2)))) -(assert (forall ((e Int) (s1 IntSet) (s2 IntSet)) (implies (and (smt_set_le s1 (smt_set_ele e)) (smt_set_lt (smt_set_ele e) s2)) (smt_set_lt s1 s2)))) -(assert (forall ((s1 IntSet) (s2 IntSet)) (implies (smt_set_lt s1 s2) (smt_set_le s1 s2)))) - -; sequence axioms -(declare-sort IntSeq) - -(declare-fun smt_seq_concat (IntSeq IntSeq) IntSeq) -(declare-fun smt_seq_elem (Int) IntSeq) -(declare-fun smt_seq_nil () IntSeq) -(declare-fun smt_seq_len (IntSeq) Int) - -(declare-fun smt_seq_sum (IntSeq) Int) -(declare-fun smt_seq2set (IntSeq) IntSet) -(declare-fun smt_seq_sorted (IntSeq) Bool) - -(assert (forall ((s1 IntSeq) (s2 IntSeq)) (! (= (smt_seq_sorted (smt_seq_concat s1 s2)) (and (smt_set_le (smt_seq2set s1) (smt_seq2set s2)) (smt_seq_sorted s1) (smt_seq_sorted s2))) - :pattern ((smt_seq_sorted (smt_seq_concat s1 s2))) - :pattern ((smt_seq_sorted s1) (smt_seq_sorted s2)) -))) - -(assert (forall ((e Int)) (= (smt_seq_sorted (smt_seq_elem e)) true))) -(assert (= (smt_seq_sorted smt_seq_nil) true)) - -(assert (forall ((s IntSeq)) (>= (smt_seq_len s) 0))) - -(assert (forall ((e Int) (s IntSet)) (not (= (smt_set_cup (smt_set_ele e) s) smt_set_emp)))) diff --git a/k-distribution/include/kframework/z3/string.smt2 b/k-distribution/include/kframework/z3/string.smt2 deleted file mode 100644 index 3fdf80884a2..00000000000 --- a/k-distribution/include/kframework/z3/string.smt2 +++ /dev/null @@ -1,80 +0,0 @@ -; floats as uninterpreted with a partial order relation -(declare-sort Float) -(declare-fun float_nan () Float) -(declare-fun float_zero () Float) - -(declare-fun float_lt (Float Float) Bool) -; transitivity -(assert (forall ((x1 Float) (x2 Float) (x3 Float)) (implies (and (float_lt x1 x2) (float_lt x2 x3)) (float_lt x1 x3)))) -; irreflexivity -(assert (forall ((x1 Float) (x2 Float)) (not (and (float_lt x1 x2) (float_lt x2 x1))))) -; total order without nan -(assert (forall ((x1 Float) (x2 Float)) (implies (and (not (= x1 float_nan)) (not (= x2 float_nan))) (or (float_lt x1 x2) (= x1 x2) (float_lt x2 x1))))) -; nan -(assert (forall ((x Float)) (and (not (float_lt x float_nan)) (not (float_lt float_nan x))))) - -(define-fun float_le ((x1 Float) (x2 Float)) Bool (or (float_lt x1 x2) (= x1 x2))) -(define-fun float_gt ((x1 Float) (x2 Float)) Bool (float_lt x2 x1)) -(define-fun float_ge ((x1 Float) (x2 Float)) Bool (float_le x2 x1)) - -(define-fun float_max ((x Float) (y Float)) Float (ite (float_lt x y) y x)) -(define-fun float_min ((x Float) (y Float)) Float (ite (float_lt x y) x y)) - -; float sets as arrays -(define-sort FloatSet () (Array Float Bool)) -(define-fun float_set_mem ((x Float) (s FloatSet)) Bool (select s x)) -(define-fun float_set_add ((s FloatSet) (x Float)) FloatSet (store s x true)) -(define-fun float_set_emp () FloatSet ((as const FloatSet) false)) -(define-fun float_set_cup ((s1 FloatSet) (s2 FloatSet)) FloatSet ((_ map or) s1 s2)) -(define-fun float_set_cap ((s1 FloatSet) (s2 FloatSet)) FloatSet ((_ map and) s1 s2)) -(define-fun float_set_com ((s FloatSet)) FloatSet ((_ map not) s)) -(define-fun float_set_ele ((x Float)) FloatSet (float_set_add float_set_emp x)) -(define-fun float_set_dif ((s1 FloatSet) (s2 FloatSet)) FloatSet (float_set_cap s1 (float_set_com s2))) -(define-fun float_set_sub ((s1 FloatSet) (s2 FloatSet)) Bool (= float_set_emp (float_set_dif s1 s2))) -(define-fun float_set_lt ((s1 FloatSet) (s2 FloatSet)) Bool (forall ((i Float) (j Float)) (implies (and (select s1 i) (select s2 j)) (float_lt i j)))) -(define-fun float_set_le ((s1 FloatSet) (s2 FloatSet)) Bool (forall ((i Float) (j Float)) (implies (and (select s1 i) (select s2 j)) (float_le i j)))) - - -; strings as uninterpreted with a total order relation -(declare-sort String) - -(declare-fun string_lt (String String) Bool) -; transitivity -(assert (forall ((x1 String) (x2 String) (x3 String)) (implies (and (string_lt x1 x2) (string_lt x2 x3)) (string_lt x1 x3)))) -; irreflexivity -(assert (forall ((x1 String) (x2 String)) (not (and (string_lt x1 x2) (string_lt x2 x1))))) -; total order -(assert (forall ((x1 String) (x2 String)) (or (string_lt x1 x2) (= x1 x2) (string_lt x2 x1)))) - -(define-fun string_le ((x1 String) (x2 String)) Bool (or (string_lt x1 x2) (= x1 x2))) -(define-fun string_gt ((x1 String) (x2 String)) Bool (string_lt x2 x1)) -(define-fun string_ge ((x1 String) (x2 String)) Bool (string_le x2 x1)) - -; string sets as arrays -(define-sort StringSet () (Array String Bool)) -(define-fun string_set_mem ((x String) (s StringSet)) Bool (select s x)) -(define-fun string_set_add ((s StringSet) (x String)) StringSet (store s x true)) -(define-fun string_set_emp () StringSet ((as const StringSet) false)) -(define-fun string_set_cup ((s1 StringSet) (s2 StringSet)) StringSet ((_ map or) s1 s2)) -(define-fun string_set_cap ((s1 StringSet) (s2 StringSet)) StringSet ((_ map and) s1 s2)) -(define-fun string_set_com ((s StringSet)) StringSet ((_ map not) s)) -(define-fun string_set_ele ((x String)) StringSet (string_set_add string_set_emp x)) -(define-fun string_set_dif ((s1 StringSet) (s2 StringSet)) StringSet (string_set_cap s1 (string_set_com s2))) -(define-fun string_set_sub ((s1 StringSet) (s2 StringSet)) Bool (= string_set_emp (string_set_dif s1 s2))) -(define-fun string_set_lt ((s1 StringSet) (s2 StringSet)) Bool (forall ((i String) (j String)) (implies (and (select s1 i) (select s2 j)) (string_lt i j)))) -(define-fun string_set_le ((s1 StringSet) (s2 StringSet)) Bool (forall ((i String) (j String)) (implies (and (select s1 i) (select s2 j)) (string_le i j)))) - -; sequence axioms -(declare-sort IntSeq) -(declare-fun smt_seq_concat (IntSeq IntSeq) IntSeq) -(declare-fun smt_seq_elem (Int) IntSeq) -(declare-fun smt_seq_nil () IntSeq) - -; int extra -(define-fun int_max ((x Int) (y Int)) Int (ite (< x y) y x)) -(define-fun int_min ((x Int) (y Int)) Int (ite (< x y) x y)) -(define-fun int_abs ((x Int)) Int (ite (< x 0) (- 0 x) x)) - -; bool to int -(define-fun smt_bool2int ((b Bool)) Int (ite b 1 0)) -