Searched refs:cl (Results 1 - 25 of 119) sorted by relevance

12345

/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A Dselftest.sml509 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 DActive.sml19 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 DSubsume.sml33 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 DProblem.sml23 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 DThm.sml34 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 DProof.sml84 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 DWaiting.sml66 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 DClause.sml64 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 Dselftest.sml509 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 DActive.sml19 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 DSubsume.sml33 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 DProblem.sml23 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 DThm.sml34 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 DProof.sml84 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 DWaiting.sml66 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 DClause.sml64 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 DmlibKernel.sml34 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 DmlibClauseset.sml96 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 DmlibClause.sml224 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 DmlibResolution.sml79 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 Draw_api.c218 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 Djava_raw_api.c329 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 Dmsvcc.sh41 # 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 Dmirror-website11 *.cl.cam.ac.uk)
/seL4-l4v-10.1.1/l4v/isabelle/Admin/Release/
H A Dmirror-website11 *.cl.cam.ac.uk)

Completed in 175 milliseconds

12345