/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | selftest.sml | 509 fun clauseToFormula cl = 510 Formula.listMkDisj (LiteralSet.transform Literal.toFormula cl); 538 fun checkModelClause M cl = 544 val {T = T', F = F'} = Model.checkClause {maxChecks = SOME 1} M cl 552 val {T,F} = Model.checkClause {maxChecks = NONE} M cl 555 [Formula.toString (LiteralSet.disjoin cl), 582 fun perturbClause (fv,cl) = 586 if Model.interpretClause M V cl then () 587 else Model.perturbClause M V cl 590 val cls = List.map (fn cl 649 val cl = LS[`$x = $x`]; value 651 val cl = LS[`~($x = $y)`,`$y = $x`]; value 653 val cl = LS[`~($x = $y)`,`~($y = $z)`,`$x = $z`]; value 658 val cl = LS[`project1 $x1 = $x1`]; value 660 val cl = LS[`project1 $x1 $x2 = $x1`]; value 662 val cl = LS[`project2 $x1 $x2 = $x2`]; value 664 val cl = LS[`project1 $x1 $x2 $x3 = $x1`]; value 666 val cl = LS[`project2 $x1 $x2 $x3 = $x2`]; value 668 val cl = LS[`project3 $x1 $x2 $x3 = $x3`]; value 670 val cl = LS[`project1 $x1 $x2 $x3 $x4 = $x1`]; value 672 val cl = LS[`project2 $x1 $x2 $x3 $x4 = $x2`]; value 674 val cl = LS[`project3 $x1 $x2 $x3 $x4 = $x3`]; value 676 val cl = LS[`project4 $x1 $x2 $x3 $x4 = $x4`]; value 678 val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 = $x1`]; value 680 val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 = $x2`]; value 682 val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 = $x3`]; value 684 val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 = $x4`]; value 686 val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 = $x5`]; value 688 val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 $x6 = $x1`]; value 690 val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 $x6 = $x2`]; value 692 val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 $x6 = $x3`]; value 694 val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 $x6 = $x4`]; value 696 val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 $x6 = $x5`]; value 698 val cl = LS[`project6 $x1 $x2 $x3 $x4 $x5 $x6 = $x6`]; value 700 val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x1`]; value 702 val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x2`]; value 704 val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x3`]; value 706 val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x4`]; value 708 val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x5`]; value 710 val cl = LS[`project6 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x6`]; value 712 val cl = LS[`project7 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x7`]; value 714 val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x1`]; value 716 val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x2`]; value 718 val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x3`]; value 720 val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x4`]; value 722 val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x5`]; value 724 val cl = LS[`project6 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x6`]; value 726 val cl = LS[`project7 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x7`]; value 728 val cl = LS[`project8 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x8`]; value 730 val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x1`]; value 732 val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x2`]; value 734 val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x3`]; value 736 val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x4`]; value 738 val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x5`]; value 740 val cl = LS[`project6 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x6`]; value 742 val cl = LS[`project7 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x7`]; value 744 val cl = LS[`project8 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x8`]; value 746 val cl = LS[`project9 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x9`]; value 752 val cl = LS[`~isZero $x`,`$x = 0`]; value 754 val cl = LS[`isZero $x`,`~($x = 0)`]; value 758 val cl = LS[`0 + 1 = 1`]; value 760 val cl = LS[`1 + 1 = 2`]; value 762 val cl = LS[`2 + 1 = 3`]; value 764 val cl = LS[`3 + 1 = 4`]; value 766 val cl = LS[`4 + 1 = 5`]; value 768 val cl = LS[`5 + 1 = 6`]; value 770 val cl = LS[`6 + 1 = 7`]; value 772 val cl = LS[`7 + 1 = 8`]; value 774 val cl = LS[`8 + 1 = 9`]; value 776 val cl = LS[`9 + 1 = 10`]; value 780 val cl = LS[`~1 = negative1`]; value 782 val cl = LS[`~2 = negative2`]; value 784 val cl = LS[`~3 = negative3`]; value 786 val cl = LS[`~4 = negative4`]; value 788 val cl = LS[`~5 = negative5`]; value 790 val cl = LS[`~6 = negative6`]; value 792 val cl = LS[`~7 = negative7`]; value 794 val cl = LS[`~8 = negative8`]; value 796 val cl = LS[`~9 = negative9`]; value 798 val cl = LS[`~10 = negative10`]; value 802 val cl = LS[`0 + $x = $x`]; value 804 val cl = LS[`$x + $y = $y + $x`]; value 806 val cl = LS[`$x + ($y + $z) = ($x + $y) + $z`]; value 810 val cl = LS[`~$x + $x = 0`]; value 812 val cl = LS[`~~$x = $x`]; value 816 val cl = LS[`$x - $y = $x + ~$y`]; value 820 val cl = LS[`suc $x = $x + 1`]; value 824 val cl = LS[`pre $x = $x - 1`]; value 828 val cl = LS[`$x <= $x`]; value 830 val cl = LS[`~($x <= $y)`,`~($y <= $z)`,`$x <= $z`]; value 832 val cl = LS[`~($x <= $y)`,`~($y <= $x)`,`$x = $y`]; value 834 val cl = LS[`0 <= $x`]; value 836 val cl = LS[`~($x >= $y)`,`$y <= $x`]; value 838 val cl = LS[`$x >= $y`,`~($y <= $x)`]; value 840 val cl = LS[`$x > $y`,`$x <= $y`]; value 842 val cl = LS[`~($x > $y)`,`~($x <= $y)`]; value 844 val cl = LS[`$x < $y`,`$y <= $x`]; value 846 val cl = LS[`~($x < $y)`,`~($y <= $x)`]; value 848 val cl = LS[`$x = 0`,`~($x <= $y)`,`~$y <= ~$x`]; value 852 val cl = LS[`1 * $x = $x`]; value 854 val cl = LS[`0 * $x = 0`]; value 856 val cl = LS[`$x * $y = $y * $x`]; value 858 val cl = LS[`$x * ($y * $z) = ($x * $y) * $z`]; value 860 val cl = LS[`$x * ($y + $z) = ($x * $y) + ($x * $z)`]; value 862 val cl = LS[`$x * ~$y = ~($x * $y)`]; value 866 val cl = LS[`$y = 0`,`$x mod $y < $y`]; value 868 val cl = LS[`$y * ($x div $y) + $x mod $y = $x`]; value 872 val cl = LS[`exp $x 0 = 1`]; value 874 val cl = LS[`$y = 0`,`exp $x $y = $x * exp $x (pre $y)`]; value 878 val cl = LS[`divides $x $x`]; value 880 val cl = LS[`~(divides $x $y)`,`~(divides $y $z)`,`divides $x $z`]; value 882 val cl = LS[`~(divides $x $y)`,`~(divides $y $x)`,`$x = $y`]; value 884 val cl = LS[`divides 1 $x`]; value 886 val cl = LS[`divides $x 0`]; value 890 val cl = LS[`even 0`]; value 892 val cl = LS[`$x = 0`,`~(even (pre $x))`,`odd $x`]; value 894 val cl = LS[`$x = 0`,`~(odd (pre $x))`,`even $x`]; value 900 val cl = LS[`~member $x empty`]; value 904 val cl = LS[`member $x universe`]; value 908 val cl = LS[`member $x $y`,`member $x (complement $y)`]; value 910 val cl = LS[`~(member $x $y)`,`~member $x (complement $y)`]; value 912 val cl = LS[`complement (complement $x) = $x`]; value 914 val cl = LS[`complement empty = universe`]; value 916 val cl = LS[`complement universe = empty`]; value 920 val cl = LS[`subset $x $x`]; value 922 val cl = LS[`~subset $x $y`,`~subset $y $z`,`subset $x $z`]; value 924 val cl = LS[`~subset $x $y`,`~subset $y $x`,`$x = $y`]; value 926 val cl = LS[`subset empty $x`]; value 928 val cl = LS[`subset $x universe`]; value 930 val cl = LS[`~subset $x $y`,`subset (complement $y) (complement $x)`]; value 932 val cl = LS[`~member $x $y`,`~subset $y $z`,`member $x $z`]; value 936 val cl = LS[`union $x $y = union $y $x`]; value 938 val cl = LS[`union $x (union $y $z) = union (union $x $y) $z`]; value 940 val cl = LS[`union empty $x = $x`]; value 942 val cl = LS[`union universe $x = universe`]; value 944 val cl = LS[`subset $x (union $x $y)`]; value 946 val cl = LS[`~member $x (union $y $z)`,`member $x $y`,`member $x $z`]; value 950 val cl = LS[`intersect $x $y = value 953 val cl = LS[`subset (intersect $x $y) $x`]; value 957 val cl = LS[`difference $x $y = intersect $x (complement $y)`]; value 961 val cl = LS[`symmetricDifference $x $y = value 966 val cl = LS[`member $x (insert $x $y)`]; value 970 val cl = LS[`singleton $x = (insert $x empty)`]; value 974 val cl = LS[`card empty = 0`]; value 976 val cl = LS[`member $x $y`,`card (insert $x $y) = suc (card $y)`]; value 982 val cl = LS[`null nil`]; value 984 val cl = LS[`~null $x`, `$x = nil`]; value 988 val cl = LS[`~(nil = $x :: $y)`]; value 992 val cl = LS[`$x @ ($y @ $z) = ($x @ $y) @ $z`]; value 994 val cl = LS[`nil @ $x = $x`]; value 996 val cl = LS[`$x @ nil = $x`]; value 1000 val cl = LS[`length nil = 0`]; value 1002 val cl = LS[`length ($x :: $y) >= length $y`]; value 1004 val cl = LS[`length ($x @ $y) >= length $x`]; value 1006 val cl = LS[`length ($x @ $y) >= length $y`]; value 1010 val cl = LS[`null $x`,`suc (length (tail $x)) = length $x`]; value 1017 val cl = pvCl (CL[`P $x`,`P $y`]); value 1020 val cl = pvCl (CL[`P $x`,`~P (f $x)`]); value 1022 val cl = pvCl (CL[`$x = $y`,`f $y = f $x`]); value 1024 val cl = pvCl (CL[`$x = f $y`,`f $x = $y`]); value 1026 val cl = pvCl (CL[`s = a`,`s = b`,`h b c`]); value 1028 val cl = pvCl (CL[`a = a`,`a = b`,`h b c`]); value 1063 val cl = pvCl (LcpCL[`~($y <= (2 + (2 * $x + pow $x 2)) / 2)`, `~(0 <= $x)`, value [all...] |
H A D | Active.sml | 19 fun add (cl,rw) = 21 val {id, thm = th, ...} = Clause.dest cl 33 fun allClause cl = 34 List.all red (cl :: Clause.factor cl) orelse 37 "Active.isSaturated.allFactors: cl" cl 47 fun allClause2 cl_lit cl = 50 case total (Clause.resolve cl_lit) (cl,lit) of 52 | SOME cl 388 val cl = if r then Clause.reduce units cl else cl value 901 val cl = Clause.freshVars cl value [all...] |
H A D | Subsume.sml | 33 fun sortClause cl = 35 val lits = LiteralSet.toList cl 101 fun insert (Subsume {empty,unit,nonunit}) (cl',a) = 102 case sortClause cl' of 105 val empty = (cl',Subst.empty,a) :: empty 111 val unit = LiteralNet.insert unit (lit,(lit,cl',a)) 118 val id_length = (nextId, LiteralSet.size cl') 126 val clauses = IntMap.insert clauses (nextId,(lits',cl',a)) 174 fun genClauseSubsumes pred cl' lits' cl 262 val cl = clauseSym (LiteralSet.toList cl) value [all...] |
H A D | Problem.sml | 23 fun lits (cl,n) = n + LiteralSet.size cl 25 fun syms (cl,n) = n + LiteralSet.symbols cl 27 fun typedSyms (cl,n) = n + LiteralSet.typedSymbols cl 43 fun clauseToFormula cl = 44 Formula.listMkDisj (LiteralSet.transform Literal.toFormula cl); 99 fun f (cl,set) = NameAritySet.union set (LiteralSet.relations cl) [all...] |
H A D | Thm.sml | 34 fun clause (Thm (cl,_)) = cl; 58 fun destUnit (Thm (cl,_)) = 59 if LiteralSet.size cl = 1 then LiteralSet.pick cl 72 fun member lit (Thm (cl,_)) = LiteralSet.member lit cl; 74 fun negateMember lit (Thm (cl,_)) = LiteralSet.negateMember lit cl; 88 fun freeIn v (Thm (cl, 209 val cl = LiteralSet.fromList [eqLit, Literal.negate lit, lit'] value [all...] |
H A D | Proof.sml | 84 Axiom cl => ppAxiom cl 92 fun ppAxiom cl = 97 (Print.ppBracket "{" "}" (Print.ppOpList "," Literal.pp)) cl); 110 val cl = Thm.clause th value 112 fun pred (_,(th',_)) = LiteralSet.equal (Thm.clause th') cl 159 fun inferenceToThm (Axiom cl) = Thm.axiom cl 167 fun reconstructSubst cl cl' 312 val cl = Thm.clause th value 359 val cl = Thm.clause th value 376 val cl = Thm.clause th value [all...] |
H A D | Waiting.sml | 66 List.map (fn (w,(_,cl)) => (w, Clause.id cl, cl)) (Heap.toList clauses)) 76 fun mkModelClause cl = 78 val lits = Clause.literals cl 92 fun perturbClause (fv,cl) = 96 if Model.interpretClause M V cl then () 97 else Model.perturbClause M V cl 115 fun checkModels parms models (fv,cl) = 121 val {T,F} = Model.check Model.interpretClause n model fv cl [all...] |
H A D | Clause.sml | 64 fun toString cl = Print.toString pp cl; 83 fun equalThms cl cl' = Thm.equal (thm cl) (thm cl'); 88 fun literals cl = Thm.clause (thm cl); 156 val largestLiterals = fn cl => 159 val () = Print.trace pp "Clause.largestLiterals: cl" c 310 val cl = Clause {parameters = parameters, id = newId (), thm = th} value [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | selftest.sml | 509 fun clauseToFormula cl = 510 Formula.listMkDisj (LiteralSet.transform Literal.toFormula cl); 538 fun checkModelClause M cl = 544 val {T = T', F = F'} = Model.checkClause {maxChecks = SOME 1} M cl 552 val {T,F} = Model.checkClause {maxChecks = NONE} M cl 555 [Formula.toString (LiteralSet.disjoin cl), 582 fun perturbClause (fv,cl) = 586 if Model.interpretClause M V cl then () 587 else Model.perturbClause M V cl 590 val cls = List.map (fn cl 649 val cl = LS[`$x = $x`]; value 651 val cl = LS[`~($x = $y)`,`$y = $x`]; value 653 val cl = LS[`~($x = $y)`,`~($y = $z)`,`$x = $z`]; value 658 val cl = LS[`project1 $x1 = $x1`]; value 660 val cl = LS[`project1 $x1 $x2 = $x1`]; value 662 val cl = LS[`project2 $x1 $x2 = $x2`]; value 664 val cl = LS[`project1 $x1 $x2 $x3 = $x1`]; value 666 val cl = LS[`project2 $x1 $x2 $x3 = $x2`]; value 668 val cl = LS[`project3 $x1 $x2 $x3 = $x3`]; value 670 val cl = LS[`project1 $x1 $x2 $x3 $x4 = $x1`]; value 672 val cl = LS[`project2 $x1 $x2 $x3 $x4 = $x2`]; value 674 val cl = LS[`project3 $x1 $x2 $x3 $x4 = $x3`]; value 676 val cl = LS[`project4 $x1 $x2 $x3 $x4 = $x4`]; value 678 val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 = $x1`]; value 680 val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 = $x2`]; value 682 val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 = $x3`]; value 684 val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 = $x4`]; value 686 val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 = $x5`]; value 688 val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 $x6 = $x1`]; value 690 val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 $x6 = $x2`]; value 692 val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 $x6 = $x3`]; value 694 val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 $x6 = $x4`]; value 696 val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 $x6 = $x5`]; value 698 val cl = LS[`project6 $x1 $x2 $x3 $x4 $x5 $x6 = $x6`]; value 700 val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x1`]; value 702 val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x2`]; value 704 val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x3`]; value 706 val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x4`]; value 708 val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x5`]; value 710 val cl = LS[`project6 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x6`]; value 712 val cl = LS[`project7 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x7`]; value 714 val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x1`]; value 716 val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x2`]; value 718 val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x3`]; value 720 val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x4`]; value 722 val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x5`]; value 724 val cl = LS[`project6 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x6`]; value 726 val cl = LS[`project7 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x7`]; value 728 val cl = LS[`project8 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x8`]; value 730 val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x1`]; value 732 val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x2`]; value 734 val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x3`]; value 736 val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x4`]; value 738 val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x5`]; value 740 val cl = LS[`project6 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x6`]; value 742 val cl = LS[`project7 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x7`]; value 744 val cl = LS[`project8 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x8`]; value 746 val cl = LS[`project9 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x9`]; value 752 val cl = LS[`~isZero $x`,`$x = 0`]; value 754 val cl = LS[`isZero $x`,`~($x = 0)`]; value 758 val cl = LS[`0 + 1 = 1`]; value 760 val cl = LS[`1 + 1 = 2`]; value 762 val cl = LS[`2 + 1 = 3`]; value 764 val cl = LS[`3 + 1 = 4`]; value 766 val cl = LS[`4 + 1 = 5`]; value 768 val cl = LS[`5 + 1 = 6`]; value 770 val cl = LS[`6 + 1 = 7`]; value 772 val cl = LS[`7 + 1 = 8`]; value 774 val cl = LS[`8 + 1 = 9`]; value 776 val cl = LS[`9 + 1 = 10`]; value 780 val cl = LS[`~1 = negative1`]; value 782 val cl = LS[`~2 = negative2`]; value 784 val cl = LS[`~3 = negative3`]; value 786 val cl = LS[`~4 = negative4`]; value 788 val cl = LS[`~5 = negative5`]; value 790 val cl = LS[`~6 = negative6`]; value 792 val cl = LS[`~7 = negative7`]; value 794 val cl = LS[`~8 = negative8`]; value 796 val cl = LS[`~9 = negative9`]; value 798 val cl = LS[`~10 = negative10`]; value 802 val cl = LS[`0 + $x = $x`]; value 804 val cl = LS[`$x + $y = $y + $x`]; value 806 val cl = LS[`$x + ($y + $z) = ($x + $y) + $z`]; value 810 val cl = LS[`~$x + $x = 0`]; value 812 val cl = LS[`~~$x = $x`]; value 816 val cl = LS[`$x - $y = $x + ~$y`]; value 820 val cl = LS[`suc $x = $x + 1`]; value 824 val cl = LS[`pre $x = $x - 1`]; value 828 val cl = LS[`$x <= $x`]; value 830 val cl = LS[`~($x <= $y)`,`~($y <= $z)`,`$x <= $z`]; value 832 val cl = LS[`~($x <= $y)`,`~($y <= $x)`,`$x = $y`]; value 834 val cl = LS[`0 <= $x`]; value 836 val cl = LS[`~($x >= $y)`,`$y <= $x`]; value 838 val cl = LS[`$x >= $y`,`~($y <= $x)`]; value 840 val cl = LS[`$x > $y`,`$x <= $y`]; value 842 val cl = LS[`~($x > $y)`,`~($x <= $y)`]; value 844 val cl = LS[`$x < $y`,`$y <= $x`]; value 846 val cl = LS[`~($x < $y)`,`~($y <= $x)`]; value 848 val cl = LS[`$x = 0`,`~($x <= $y)`,`~$y <= ~$x`]; value 852 val cl = LS[`1 * $x = $x`]; value 854 val cl = LS[`0 * $x = 0`]; value 856 val cl = LS[`$x * $y = $y * $x`]; value 858 val cl = LS[`$x * ($y * $z) = ($x * $y) * $z`]; value 860 val cl = LS[`$x * ($y + $z) = ($x * $y) + ($x * $z)`]; value 862 val cl = LS[`$x * ~$y = ~($x * $y)`]; value 866 val cl = LS[`$y = 0`,`$x mod $y < $y`]; value 868 val cl = LS[`$y * ($x div $y) + $x mod $y = $x`]; value 872 val cl = LS[`exp $x 0 = 1`]; value 874 val cl = LS[`$y = 0`,`exp $x $y = $x * exp $x (pre $y)`]; value 878 val cl = LS[`divides $x $x`]; value 880 val cl = LS[`~(divides $x $y)`,`~(divides $y $z)`,`divides $x $z`]; value 882 val cl = LS[`~(divides $x $y)`,`~(divides $y $x)`,`$x = $y`]; value 884 val cl = LS[`divides 1 $x`]; value 886 val cl = LS[`divides $x 0`]; value 890 val cl = LS[`even 0`]; value 892 val cl = LS[`$x = 0`,`~(even (pre $x))`,`odd $x`]; value 894 val cl = LS[`$x = 0`,`~(odd (pre $x))`,`even $x`]; value 900 val cl = LS[`~member $x empty`]; value 904 val cl = LS[`member $x universe`]; value 908 val cl = LS[`member $x $y`,`member $x (complement $y)`]; value 910 val cl = LS[`~(member $x $y)`,`~member $x (complement $y)`]; value 912 val cl = LS[`complement (complement $x) = $x`]; value 914 val cl = LS[`complement empty = universe`]; value 916 val cl = LS[`complement universe = empty`]; value 920 val cl = LS[`subset $x $x`]; value 922 val cl = LS[`~subset $x $y`,`~subset $y $z`,`subset $x $z`]; value 924 val cl = LS[`~subset $x $y`,`~subset $y $x`,`$x = $y`]; value 926 val cl = LS[`subset empty $x`]; value 928 val cl = LS[`subset $x universe`]; value 930 val cl = LS[`~subset $x $y`,`subset (complement $y) (complement $x)`]; value 932 val cl = LS[`~member $x $y`,`~subset $y $z`,`member $x $z`]; value 936 val cl = LS[`union $x $y = union $y $x`]; value 938 val cl = LS[`union $x (union $y $z) = union (union $x $y) $z`]; value 940 val cl = LS[`union empty $x = $x`]; value 942 val cl = LS[`union universe $x = universe`]; value 944 val cl = LS[`subset $x (union $x $y)`]; value 946 val cl = LS[`~member $x (union $y $z)`,`member $x $y`,`member $x $z`]; value 950 val cl = LS[`intersect $x $y = value 953 val cl = LS[`subset (intersect $x $y) $x`]; value 957 val cl = LS[`difference $x $y = intersect $x (complement $y)`]; value 961 val cl = LS[`symmetricDifference $x $y = value 966 val cl = LS[`member $x (insert $x $y)`]; value 970 val cl = LS[`singleton $x = (insert $x empty)`]; value 974 val cl = LS[`card empty = 0`]; value 976 val cl = LS[`member $x $y`,`card (insert $x $y) = suc (card $y)`]; value 982 val cl = LS[`null nil`]; value 984 val cl = LS[`~null $x`, `$x = nil`]; value 988 val cl = LS[`~(nil = $x :: $y)`]; value 992 val cl = LS[`$x @ ($y @ $z) = ($x @ $y) @ $z`]; value 994 val cl = LS[`nil @ $x = $x`]; value 996 val cl = LS[`$x @ nil = $x`]; value 1000 val cl = LS[`length nil = 0`]; value 1002 val cl = LS[`length ($x :: $y) >= length $y`]; value 1004 val cl = LS[`length ($x @ $y) >= length $x`]; value 1006 val cl = LS[`length ($x @ $y) >= length $y`]; value 1010 val cl = LS[`null $x`,`suc (length (tail $x)) = length $x`]; value 1017 val cl = pvCl (CL[`P $x`,`P $y`]); value 1020 val cl = pvCl (CL[`P $x`,`~P (f $x)`]); value 1022 val cl = pvCl (CL[`$x = $y`,`f $y = f $x`]); value 1024 val cl = pvCl (CL[`$x = f $y`,`f $x = $y`]); value 1026 val cl = pvCl (CL[`s = a`,`s = b`,`h b c`]); value 1028 val cl = pvCl (CL[`a = a`,`a = b`,`h b c`]); value 1063 val cl = pvCl (LcpCL[`~($y <= (2 + (2 * $x + pow $x 2)) / 2)`, `~(0 <= $x)`, value [all...] |
H A D | Active.sml | 19 fun add (cl,rw) = 21 val {id, thm = th, ...} = Clause.dest cl 33 fun allClause cl = 34 List.all red (cl :: Clause.factor cl) orelse 37 "Active.isSaturated.allFactors: cl" cl 47 fun allClause2 cl_lit cl = 50 case total (Clause.resolve cl_lit) (cl,lit) of 52 | SOME cl 388 val cl = if r then Clause.reduce units cl else cl value 901 val cl = Clause.freshVars cl value [all...] |
H A D | Subsume.sml | 33 fun sortClause cl = 35 val lits = LiteralSet.toList cl 101 fun insert (Subsume {empty,unit,nonunit}) (cl',a) = 102 case sortClause cl' of 105 val empty = (cl',Subst.empty,a) :: empty 111 val unit = LiteralNet.insert unit (lit,(lit,cl',a)) 118 val id_length = (nextId, LiteralSet.size cl') 126 val clauses = IntMap.insert clauses (nextId,(lits',cl',a)) 174 fun genClauseSubsumes pred cl' lits' cl 262 val cl = clauseSym (LiteralSet.toList cl) value [all...] |
H A D | Problem.sml | 23 fun lits (cl,n) = n + LiteralSet.size cl 25 fun syms (cl,n) = n + LiteralSet.symbols cl 27 fun typedSyms (cl,n) = n + LiteralSet.typedSymbols cl 43 fun clauseToFormula cl = 44 Formula.listMkDisj (LiteralSet.transform Literal.toFormula cl); 99 fun f (cl,set) = NameAritySet.union set (LiteralSet.relations cl) [all...] |
H A D | Thm.sml | 34 fun clause (Thm (cl,_)) = cl; 58 fun destUnit (Thm (cl,_)) = 59 if LiteralSet.size cl = 1 then LiteralSet.pick cl 72 fun member lit (Thm (cl,_)) = LiteralSet.member lit cl; 74 fun negateMember lit (Thm (cl,_)) = LiteralSet.negateMember lit cl; 88 fun freeIn v (Thm (cl, 209 val cl = LiteralSet.fromList [eqLit, Literal.negate lit, lit'] value [all...] |
H A D | Proof.sml | 84 Axiom cl => ppAxiom cl 92 fun ppAxiom cl = 97 (Print.ppBracket "{" "}" (Print.ppOpList "," Literal.pp)) cl); 110 val cl = Thm.clause th value 112 fun pred (_,(th',_)) = LiteralSet.equal (Thm.clause th') cl 159 fun inferenceToThm (Axiom cl) = Thm.axiom cl 167 fun reconstructSubst cl cl' 312 val cl = Thm.clause th value 359 val cl = Thm.clause th value 376 val cl = Thm.clause th value [all...] |
H A D | Waiting.sml | 66 List.map (fn (w,(_,cl)) => (w, Clause.id cl, cl)) (Heap.toList clauses)) 76 fun mkModelClause cl = 78 val lits = Clause.literals cl 92 fun perturbClause (fv,cl) = 96 if Model.interpretClause M V cl then () 97 else Model.perturbClause M V cl 115 fun checkModels parms models (fv,cl) = 121 val {T,F} = Model.check Model.interpretClause n model fv cl [all...] |
H A D | Clause.sml | 64 fun toString cl = Print.toString pp cl; 83 fun equalThms cl cl' = Thm.equal (thm cl) (thm cl'); 88 fun literals cl = Thm.clause (thm cl); 156 val largestLiterals = fn cl => 159 val () = Print.trace pp "Clause.largestLiterals: cl" c 310 val cl = Clause {parameters = parameters, id = newId (), thm = th} value [all...] |
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibKernel.sml | 34 fun AXIOM cl = 35 if List.all is_literal cl then mlibThm (cl, (Axiom, [])) 44 fun INST env (th as mlibThm (cl, pr)) = 46 val cl' = map (formula_subst env) cl 48 if cl' = cl then th else 50 => if cl' = clause th' then th' else mlibThm (cl', (Ins 55 let val cl = rev (setify (clause th)) value 65 val cl = cl1' @ cl2' value [all...] |
H A D | mlibClauseset.sml | 96 fun add_unit cl units = 97 let val {thm, ...} = dest_clause cl in U.add thm units end; 99 fun add_subsum cl = S.add (literals cl |-> cl); 228 fun beef_up (SET {units, ...}) cl = 230 val () = taut cl 231 val cl = NEQ_VARS cl value 232 val () = taut cl 233 val cl = DEMODULATE units cl value 319 val cl = mlibClause.drop_order cl value 335 val (cl,set) = add_rewr cl set value 542 val (cl,set) = add_rewr cl set value [all...] |
H A D | mlibClause.sml | 224 fun free_vars cl = 225 FVL (constraint_vars (#order (dest_clause cl))) (literals cl); 229 fun dest_rewr cl = 231 val {parm, thm, id, ...} = dest_clause cl 260 fun pp_clause cl = f (!show_id) (!show_constraint) cl; 351 fun drop_order (cl as CL (p,i,th,c,d)) = 352 if T.null c then cl else CL (p, i, th, no_constraints p, d); 358 fun subsumes (cl a [all...] |
H A D | mlibResolution.sml | 79 fun clause_to_string cl = 80 PP.pp_to_string (!LINE_LENGTH) mlibClause.pp_clause cl; 152 and check set sos n (d,cl) = 153 case ofilt (not o mlibClauseset.subsumed set) (beef_up set cl) of 155 | SOME cl => (n, SOME ((d,cl),sos)); 164 | SOME ((d,cl),sos) => 167 val {order_stickiness, ...} = #parm (mlibClause.dest_clause cl) 168 val cl = if order_stickiness <= 2 then mlibClause.drop_order cl els value 182 val cl = mlibClause.FRESH_VARS cl value [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/ |
H A D | raw_api.c | 218 ffi_raw_closure *cl = (ffi_raw_closure*)user_data; local 221 (*cl->fun) (cif, rvalue, raw, cl->user_data); 225 ffi_prep_raw_closure_loc (ffi_raw_closure* cl, argument 233 status = ffi_prep_closure_loc ((ffi_closure*) cl, 240 cl->fun = fun; 241 cl->user_data = user_data; 257 ffi_prep_raw_closure (ffi_raw_closure* cl, argument 262 return ffi_prep_raw_closure_loc (cl, cif, fun, user_data, cl); [all...] |
H A D | java_raw_api.c | 329 ffi_raw_closure *cl = (ffi_raw_closure*)user_data; local 332 (*cl->fun) (cif, rvalue, (ffi_raw*)raw, cl->user_data); 337 ffi_prep_java_raw_closure_loc (ffi_java_raw_closure* cl, argument 345 status = ffi_prep_closure_loc ((ffi_closure*) cl, 352 cl->fun = fun; 353 cl->user_data = user_data; 364 ffi_prep_java_raw_closure (ffi_java_raw_closure* cl, argument 369 return ffi_prep_java_raw_closure_loc (cl, cif, fun, user_data, cl); [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
H A D | msvcc.sh | 41 # GCC-compatible wrapper for cl.exe and ml.exe. Arguments are given in GCC 42 # format and translated into something sensible for cl or ml. 49 cl="cl" 71 -clang-cl) 72 cl="clang-cl" 235 echo "$cl -nologo -EP $includes $defines $src > $ppsrc" 236 "$cl" -nologo -EP $includes $defines $src > $ppsrc || exit $? 248 echo "$cl [all...] |
/seL4-l4v-10.1.1/isabelle/Admin/Release/ |
H A D | mirror-website | 11 *.cl.cam.ac.uk)
|
/seL4-l4v-10.1.1/l4v/isabelle/Admin/Release/ |
H A D | mirror-website | 11 *.cl.cam.ac.uk)
|