新文件: .test.cnf.swp

	删除:         bin/Debug/zmaxsat
	重命名:       utils/ParseUtils.h -> core/Input.h
	修改:         core/Solver.cc
	修改:         core/Solver.h
	修改:         core/SolverTypes.h
	新文件:       core/debug.cc
	新文件:       core/debug.h
	修改:         core/main.cc
	删除:         main.cpp
	新文件:       maxsatz2013.c
	修改:         mtl/Vec.h
	新文件:       obj/Debug/core/Solver.o
	新文件:       obj/Debug/core/debug.o
	修改:         obj/Debug/core/main.o
	新文件:       obj/Debug/utils/System.o
	新文件:       test.cnf
	删除:         utils/Options.cc
	删除:         utils/Options.h
	修改:         utils/System.cc
	修改:         utils/System.h
	新文件:       zmaxsat-NSConflict-MrPigeon.layout
	修改:         zmaxsat.cbp
	修改:         zmaxsat.depend
	修改:         zmaxsat.layout
	新文件:       zmaxsat_mini.c
	新文件:       "\350\257\264\346\230\216.txt"

Author: frankc

.test.cnf.swp

@@ -1,39 +1,13 @@
-/************************************************************************************[ParseUtils.h]
-Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
-Copyright (c) 2007-2010, Niklas Sorensson
 
-Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
-associated documentation files (the "Software"), to deal in the Software without restriction,
-including without limitation the rights to use, copy, modify, merge, publish, distribute,
-sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all copies or
-substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
-NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
-DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
-OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-**************************************************************************************************/
-
-#ifndef zmaxsat_ParseUtils_h
-#define zmaxsat_ParseUtils_h
-
-#include <stdlib.h>
 #include <stdio.h>
-
 #include <zlib.h>
+//#include "SolverTypes.h"
+#include "Solver.h"
 
 namespace zmaxsat {
-
-//-------------------------------------------------------------------------------------------------
-// A simple buffered character stream class:
-
+//==============================================================================================================
+//data structure for input function --parseutils.h
 static const int buffer_size = 1048576;
-
-
 class StreamBuffer {
     gzFile        in;
     unsigned char buf[buffer_size];
@@ -44,7 +18,7 @@ class StreamBuffer {
         if (pos >= size) {
             pos  = 0;
             size = gzread(in, buf, sizeof(buf)); } }
-
+//circulate reading
 public:
     explicit StreamBuffer(gzFile i) : in(i), pos(0), size(0) { assureLookahead(); }
 
@@ -53,32 +27,24 @@ class StreamBuffer {
     int  position    () const { return pos; }
 };
 
-
 //-------------------------------------------------------------------------------------------------
 // End-of-file detection functions for StreamBuffer and char*:
-
-
 static inline bool isEof(StreamBuffer& in) { return *in == EOF;  }
 static inline bool isEof(const char*   in) { return *in == '\0'; }
-
 //-------------------------------------------------------------------------------------------------
 // Generic parse functions parametrized over the input-stream type.
-
-
 template<class B>
 static void skipWhitespace(B& in) {
     while ((*in >= 9 && *in <= 13) || *in == 32)
         ++in; }
 
-
 template<class B>
 static void skipLine(B& in) {
     for (;;){
         if (isEof(in)) return;
         if (*in == '\n') { ++in; return; }
         ++in; } }
-
-
+ //函数功能是把字符串转换成数字
 template<class B>
 static int parseInt(B& in) {
     int     val = 0;
@@ -91,8 +57,6 @@ static int parseInt(B& in) {
         val = val*10 + (*in - '0'),
         ++in;
     return neg ? -val : val; }
-
-
 // String matching: in case of a match the input iterator will be advanced the corresponding
 // number of characters.
 template<class B>
@@ -101,10 +65,8 @@ static bool match(B& in, const char* str) {
     for (i = 0; str[i] != '\0'; i++)
         if (in[i] != str[i])
             return false;
-
     in += i;
-
-    return true;
+	return true;
 }
 
 // String matching: consumes characters eagerly, but does not require random access iterator.
@@ -115,8 +77,71 @@ static bool eagerMatch(B& in, const char* str) {
             return false;
     return true; }
 
+//=================================================================================================
+// input fuctions for instance:
+
+template<class B, class Solver>
+static void readClause(B& in, Solver& S, vec<Lit>& lits) {
+    int parsed_lit, var;
+    lits.clear();
+    for (;;){
+        parsed_lit = parseInt(in);
+        if (parsed_lit == 0) break;
+        var = abs(parsed_lit)-1;
+        while (var>= S.nVars()) S.newVar();
+        lits.push( (parsed_lit > 0) ? mkLit(var) : ~ mkLit(var) );
+    }
+}
+
+template<class B, class Solver>
+static void parse_DIMACS_main(B& in, Solver& S) {
+    vec<Lit> lits;
+    int cnt= 0;
+    for (;;){
+        skipWhitespace(in); //略过空格
+        if (*in == EOF) break; //读文件结束
+        else if (*in == 'p'){
+           if (eagerMatch(in, "p cnf")){
+                S.setnVars(parseInt(in)); //获取变元个数
+                S.setnClauses(parseInt(in)); //获取子句个数
+                S.setisWeight(0);
+           }
+	       else if(eagerMatch(in, "p wcnf")){
+                S.setnVars(parseInt(in)); //获取变元个数
+                S.setnClauses(parseInt(in)); //获取子句个数
+                S.setisWeight(1);
+           	    if(*in!='\n'){
+		          skipWhitespace(in);
+		          int hardweight=0;
+		          while (*in >= '0' && *in <= '9'){
+                    hardweight= hardweight*10 + (*in - '0'),
+                    ++in;
+                  }
+		         S.setHardWeight(hardweight);
+           	    }
+                if(S.getHardWeight()>0)
+		          S.setPartial(1);
+	       }
+        }
+        else if(*in == 'c' || *in!= 'p')
+            skipLine(in);// 略去文件开始部分的说明性信息
+        else{   //开始读入每个子句
+            cnt++;
+            readClause(in, S, lits);
+	        S.addClause(lits);
+        }
+ }//end for
+ if (cnt!=S.getnClauses())
+        fprintf(stderr, "WARNING! DIMACS header mismatch: wrong number of clauses.\n");
+}
+
+// Inserts problem into solver.
+//
+template<class Solver>
+static void buildInstance(gzFile input_stream, Solver& S) {
+    StreamBuffer in(input_stream); //为文件分配一个读入的字符流缓存
+    parse_DIMACS_main(in, S); }//读入算例的子句等信息
 
 //=================================================================================================
 }
 
-#endif