Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
read_dimacs_cnf_file can now read DIMACS files that contain successive
authorwebertj
Tue, 01 Dec 2009 22:29:46 +0000
changeset 33937 b5ca587d0885
parent 33936 6e77ca6d3a8f
child 33944 ab87cceed53f
child 34010 ac78f5cdc430
read_dimacs_cnf_file can now read DIMACS files that contain successive white-space characters.
src/HOL/Tools/sat_solver.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/sat_solver.ML	Sun Nov 29 12:56:30 2009 +1100
+++ b/src/HOL/Tools/sat_solver.ML	Tue Dec 01 22:29:46 2009 +0000
@@ -311,7 +311,7 @@
     fun int_from_string s =
       case Int.fromString s of
         SOME i => i
-      | NONE   => error ("token " ^ quote s ^ "in DIMACS CNF file is not a number")
+      | NONE   => error ("token " ^ quote s ^ " in DIMACS CNF file is not a number")
     (* int list -> int list list *)
     fun clauses xs =
       let
@@ -350,7 +350,7 @@
     o (map (map literal_from_int))
     o clauses
     o (map int_from_string)
-    o (maps (String.fields (fn c => c mem [#" ", #"\t", #"\n"])))
+    o (maps (String.tokens (fn c => c mem [#" ", #"\t", #"\n"])))
     o filter_preamble
     o filter (fn l => l <> "")
     o split_lines
isabelle