Index: /vis_dev/zchaff/Makefile =================================================================== --- /vis_dev/zchaff/Makefile (revision 10) +++ /vis_dev/zchaff/Makefile (revision 10) @@ -0,0 +1,68 @@ +CC = g++ -Wall -m32 +CFLAGS = -O3 + +#CFLAGS = -O3 -DNDEBUG +#MFLAGS = +#LINKFLAGS = --static + +ifeq (solaris, $(OSTYPE)) + MFLAGS = -D_NEED_REDEFINE_RAND_MAX_ +endif + +RANLIB = ranlib +AR = ar + +.SUFFIXES: .o .cpp + +HEADERS = zchaff_base.h zchaff_clsgen.h zchaff_header.h zchaff_version.h zchaff_dbase.h zchaff_solver.h + +SOLVER_SRCS = sat_solver.cpp +SOLVER_OBJS = $(SOLVER_SRCS:.cpp=.o) + + +LIB_SRCS = zchaff_utils.cpp \ + zchaff_solver.cpp\ + zchaff_base.cpp \ + zchaff_dbase.cpp \ + zchaff_c_wrapper.cpp \ + zchaff_cpp_wrapper.cpp \ + +LIB_OBJS = $(LIB_SRCS:.cpp=.o) + + +zchaff: $(SOLVER_OBJS) libsat.a SAT.h + $(CC) $(LINKFLAGS) $(CFLAGS) $(MFLAGS) $(SOLVER_OBJS) libsat.a -o zchaff + +zverify_df: zverify_df.cpp + $(CC) $(LINKFLAGS) $(CFLAGS) $(MFLAGS) zverify_df.cpp -o zverify_df + +zminimal: zminimal.cpp libsat.a + $(CC) $(LINKFLAGS) $(CFLAGS) $(MFLAGS) zminimal.cpp libsat.a -o zminimal + +cnf_stats: cnf_stats.cpp + $(CC) $(LINKFLAGS) $(CFLAGS) $(MFLAGS) cnf_stats.cpp -o cnf_stats + +$(LIB_OBJS): $(HEADERS) Makefile + +$(SOLVER_OBJS): $(SOLVER_SRCS) SAT.h Makefile + +zchaff_c_wrapper.cpp: zchaff_wrapper.wrp + sed 's/EXTERN/extern \"C\"/' zchaff_wrapper.wrp > zchaff_c_wrapper.cpp + +zchaff_cpp_wrapper.cpp: zchaff_wrapper.wrp + sed 's/EXTERN//' zchaff_wrapper.wrp > zchaff_cpp_wrapper.cpp +SAT_C.h: + sed 's/gid = 0/gid/' SAT.h > SAT_C.h + +libsat.a: $(LIB_OBJS) + @rm -f libsat.a + $(AR) cr libsat.a $(LIB_OBJS) + $(RANLIB) libsat.a + +.cpp.o: + $(CC) $(CFLAGS) $(MFLAGS) -c $< + +clean: + rm -f *.o libsat.a zchaff *wrapper.cpp zminimal zverify_df cnf_stats SAT_C.h + +all: zchaff zverify_df zminimal cnf_stats Index: /vis_dev/zchaff/README =================================================================== --- /vis_dev/zchaff/README (revision 10) +++ /vis_dev/zchaff/README (revision 10) @@ -0,0 +1,125 @@ +[2008.10.12] +This is the same as 2007.3.12 but can be compiled with g++-4.3 + +[2007.3.12] +Fixed the inefficiency bug in zverify_df. Thanks to Allen Van Gelder and +Tjark Weber. + +[2004.11.15 Simplified] +This is just a simplified version of 2004.5.13. Many portions of dead +codes are removed. Some of codes are re-written and re-formatted for +easy reading. You might experience a little speedup. Please switch back +to 2004.5.13 if the functionalities you need are removed in the simplified +version. + +[2004.5.13] +Some performace update. This is the version we used for SAT04 competition. +Please consult our website for the detailed description. + +[2003.12.04] +Fixed: +1. Various bugs in add_clause_incr(). We would like to thank Alexander + Smith from University of Toronto for his suggestion and experiments on + this issue. +2. SAT_HOOK added. +3. unset_force_terminate added. + +[2003.11.04] +Fixed: +1. Compile under g++ 3.3 and above +2. Assertion error for certain instances in core extraction +3. A typo in run_till_fix. Now it takes the second argument as the max +number of iterations to run as intended. + +[2003.10.09] +Fixes in this release: +1. Bug fixed for time overflow after 2147 seconds. +2. The Perl script run_till_fix is updated such that it works for cnf +files located in other directory. +3. zverify_df.cpp now also verifies the conflict clause given in +resolve_trace with the one constructed by zverify itself using the +information given in resolve_trace. +[2003.7.22] +NOTE: If your code is in C instead of C++, please use SAT_C.h instead of +SAT.h as the header file. + +This is a new (as of June, 2003) release of zchaff, a SAT solver from +Princeton University. The main difference between this one and the +previous (2001.2.17) version are listed in the following: +1. This version of zchaff has incremental SAT solving capability + In practice, many SAT instances are related in the sense that they only + differ in a small number of clauses. Zchaff can solve a set of + such instances incrementally, leveraging the knowledge (clauses) learned + from previous runs to help current runs. This feature can only be invoked + through the functional call interface. Please read SAT.h for more + information about assigning clauses with Group IDs and how to delete + clause or add clauses by groups. + + +2. This version of zchaff is certifiable + Now zchaff can produce a verifiable trace that can be checked by a third + party checker. To invoke this, modify zchaff_solver.cpp and uncomment + #define VERIFY_ON and compile again. Now zchaff will produce a trace + called resolution_trace after each run and this can be checked by + zverify_bf or zverify_df, which are two checkers based on breadth-first + and depth-first search. + + +3. This version of zchaff can produce an unsatisfiable core from an + unsatisifable formula Unsatisfiable core extraction can be useful for + some applications. This version of zchaff implement the idea presented + in our SAT 2003 paper about extracting unsat cores. + +4. This version can compile under gcc 3.x. + +5. This version fixed a couple of serious bugs in the previous version. + (But may have introduced other bugs :(). + + +How to Install: + Use "make" to compile, or "make all" to compile zchaff with extra utilities + (e.g. core extractor, verifier). It should work without any problem + under Linux, Cygwin or Solaris. + + To compile a native Windows executable, Open Visual Studio .Net, create + a project, and add these files into the project: + zchaff_base.cpp, + zchaff_cpp_wrapper.cpp (this can be obtained by rename + zchaff_wrapper.wrp to zchaff_cpp_wrapper.cpp and delete all occurance of + "EXTERN" in the file.) + zchaff_dbase.cpp + zchaff_solver.cpp + zchaff_utils.cpp + sat_solver.cpp + + Also, modify files that contain headers "sys/*.h". Delete those troublesome + headers, replace them with "#include ", and replace the code for + function get_cpu_time() with: + + double get_cpu_time(void) { + return (double)clock()/(double)(CLOCKS_PER_SEC); + } + This function will overflow after 2147 seconds. So the reported time + may not be correct. This is a temporary solution and hopefully we will fix it in + the future. + + MSVC will report a lot of warnings. Hopefully none is serious. :(. As + you suspected, zchaff is not tested under native Windows enviroment. + But anyway, this is the hack. + +How to use: + the main executable is zchaff. The command line is + zchaff CNF_FILE [TimeLimit] + Other executables will print out a help info when executed with no + argument. + + run_till_fix can obtain a small core by iteratively run core extraction. + Do turn + VERIFY_ON in zchaff_solver.cpp when compile. + +For any questions or bug reports, please send email to +Yogesh Mahajan at yogism@Princeton.EDU + +Thanks. + +The SAT Group at Princeton University Index: /vis_dev/zchaff/SAT.h =================================================================== --- /vis_dev/zchaff/SAT.h (revision 10) +++ /vis_dev/zchaff/SAT.h (revision 10) @@ -0,0 +1,446 @@ +// /********************************************************************* +// Copyright 2000-2004, Princeton University. All rights reserved. +// By using this software the USER indicates that he or she has read, +// understood and will comply with the following: +// +// --- Princeton University hereby grants USER nonexclusive permission +// to use, copy and/or modify this software for internal, noncommercial, +// research purposes only. Any distribution, including commercial sale +// or license, of this software, copies of the software, its associated +// documentation and/or modifications of either is strictly prohibited +// without the prior consent of Princeton University. Title to copyright +// to this software and its associated documentation shall at all times +// remain with Princeton University. Appropriate copyright notice shall +// be placed on all software copies, and a complete copy of this notice +// shall be included in all copies of the associated documentation. +// No right is granted to use in advertising, publicity or otherwise +// any trademark, service mark, or the name of Princeton University. +// +// +// --- This software and any associated documentation is provided "as is" +// +// PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS +// OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A +// PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR +// ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, +// TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. +// +// Princeton University shall not be liable under any circumstances for +// any direct, indirect, special, incidental, or consequential damages +// with respect to any claim by USER or any third party on account of +// or arising from the use, or inability to use, this software or its +// associated documentation, even if Princeton University has been advised +// of the possibility of those damages. +// *********************************************************************/ + +#ifndef __SAT_HEADER__ +#define __SAT_HEADER__ + +#define SAT_Manager void * + +typedef long long long64; // this is for 32 bit unix machines +// typedef long long64; // this is for Windows or 64 bit unix machines + + +#ifndef _SAT_STATUS_ +#define _SAT_STATUS_ +enum SAT_StatusT { + UNDETERMINED, + UNSATISFIABLE, + SATISFIABLE, + TIME_OUT, + MEM_OUT, + ABORTED +}; +#endif + +#ifndef _CLS_STATUS_ +#define _CLS_STATUS_ +enum CLAUSE_STATUS { + ORIGINAL_CL, + CONFLICT_CL, + DELETED_CL, +}; +#endif + +#ifndef UNKNOWN +#define UNKNOWN 2 +#endif + +// /*============================================================ +// +// This is the header for using the sat solver. A typical flow is +// +// 1. calling SAT_InitManager to get a new manager. You can pre-set +// the number of variables upfront, or you can add it later by +// SAT_AddVariable. +// Variables are indexed from 1, NOT 0. +// +// 2. add clauses by calling SAT_AddClause. Clause is represented by +// an array of integers. Each literal is represented by +// 2 * VarIndex + Sign. The Sign is 0 for positive phased literals, +// and 1 for negative phased literals. +// For example, a clause (3 -5 11 -4 ) should be represented by +// { 6, 11, 22, 9 } +// Note: Each variable can occure no more than once in a clause. +// if a variable occures in both phase, the clause is automatically +// satisfied. If more than one occurance with same phase, they +// should be combined. IT IS YOUR RESPONSIBILITY TO KEEP EACH +// CLAUSE NON-REDUNDENT, or the solver will not function correctly. +// +// 3. zchaff support incremental SAT solving. Clauses can be added +// or deleted from the database after each run. To accomplish +// this, a clause is associated with a "Group ID". Each clause +// has one Group ID. The group of clauses with the same GID can +// be deleted from the database by calling SAT_DeleteClauseGroup +// after each run. You need to call SAT_Reset to reset the state +// of the solver before begining a new run. +// As an example, the first 10 clauses are associated with GID 1, +// We add another 2 clauses with GID 2. After solving this instance +// with 12 clauses, we may want to delete the last 2 clauses and +// add another 3 clauses. We call SAT_DeleteClauseGroup with GID +// 2 and add the three clauses (these three clauses can have any +// GID: either 1 if you don't want to delete them in the future, +// 2 if you want to distinguish them from Group 1). Then you should +// call SAT_Reset() to reset the state of the solver, and call +// SAT_Solve() again to solve the new instance (a instance with +// 13 clauses). +// You should obtain free GID using SAT_AllocClauseGroupID. When +// you call SAT_DeleteClauseGroup, the gid will be freed and can +// be re-used when you call SAT_AllocClauseGroupID() again. +// You can also merge two group of clauses into 1 by calling +// corresponding functions. +// +// 4. Optionally, you may set the time limit and memory limit for +// the solver, note: time and memory limits are not exact. +// Also, you can set other paramenters like clause deletion +// etc. +// +// 5. You can add hook function to do some extra work after +// a certain number of decisions (branchings). A hook function +// should accept input of a manager, and has no return value. +// +// 6. Calling SAT_Solve to solve the problem. it will return the +// status of the solver. +// +// 7. If the problem is satisfiable, you can call SAT_GetVarAsgnment +// to get a variable assignment which satisfy the problem. +// +// 8. You can also get some statistics from the solver, such as +// run time, mem usage, etc. +// +// 9. Release the manager by calling SAT_ReleaseManager. +// +// You need to link the library libsat.a, also, though you can compile +// your C program with c compiler when using this sat solver, you +// still need c++ linker to link the library. +// +// Have fun. +// The Chaff Team +// (contact zfu@EE.Princeton.EDU +// for any questions or suggestions) +// 2004. 3. 10 +// =============================================================*/ + + +// Following are the main functions for the flow. + +// init a manager +SAT_Manager SAT_InitManager(void); + +// get the version of the solver +char * SAT_Version(SAT_Manager mng); + +// release a manager +void SAT_ReleaseManager(SAT_Manager mng); + +// set the number of variables. +void SAT_SetNumVariables(SAT_Manager mng, + int num_vars); + +// add a variable. it will return the new var's index +int SAT_AddVariable(SAT_Manager mng); + +// the following functions will allow/disallow the variable to be branched +// user may want to branch only on certain variables (for example, primary +// inputs of a circuit, if the CNF is generated from circuit). +// By default, all variables are branchable, usually, if a variable is +// unbranchable, it's value should be determined by all the branchable variables. +// if that's not the case, then these variables may not get an assigned +// value even if the solver says that the problem is satisfiable. +// Notice, the solver determines if a problem is satisfiable by trying to assign +// all the branchable variables. If all such variables can be assigned values +// without causing conflict, then the instance is reported as satisfiable, even +// if the instance is actually unsatisfiable because of unbranchable +// variables being not dependent on branchable variables. +void SAT_EnableVarBranch(SAT_Manager mng, int vid); + +void SAT_DisableVarBranch(SAT_Manager mng, int vid); +// add a clause. a literal is a integer with value 2*V_idx + sign +// gid is the group ID. by default, gid equals 0 . Note: group 0 +// clauses can't be deleted. +void SAT_AddClause(SAT_Manager mng, + int * clause_lits, + int num_lits, + int gid = 0); + +// delete a clause group and learned clauses depending on them. +void SAT_DeleteClauseGroup(SAT_Manager mng, + int gid); + +// This will reset the solver so it will not keep the implications made before +void SAT_Reset(SAT_Manager mng); + +// merge the clause group gid1 with gid2, return a new group which +// contain both groups. +int SAT_MergeClauseGroup(SAT_Manager mng, + int gid1, + int gid2); + +// Allocate a free clause group id. will be -1 if no more available. +// current implementation allow 32 deletable group IDs ranging from +// 1-32. Group 0 is the permanent group (i.e. can't delete). +int SAT_AllocClauseGroupID(SAT_Manager mng); + +// followings are for clause gid manipulation +int SAT_IsSetClauseGroupID(SAT_Manager mng, int cl_idx, int id); +int SAT_SetClauseGroupID(SAT_Manager mng, int cl_idx, int id); +int SAT_ClearClauseGroupID(SAT_Manager mng, int cl_idx, int id); +// clauses belong to volatile group will always be deleted when +// SAT_DeleteClauseGroup is called +int SAT_GetVolatileGroupID(SAT_Manager mng); +// clauses belong to global group will never be deleted +int SAT_GetGlobalGroupID(SAT_Manager mng); + + +void SAT_SetTimeLimit(SAT_Manager mng, + float runtime); + +// note: memory estimation is very rough, so allow 30% of error +// in both SetMemLimit and EstimateMemUsage. Also, in the run +// time, the memory usage could be temporarily 50% larger than +// the limit (this occours when program reallocate memory because +// of insufficiency in the initial allocation). +void SAT_SetMemLimit(SAT_Manager mng, + int num_bytes); + + +int SAT_Solve(SAT_Manager mng); +// enum SAT_StatusT +// Get a variable's assignment. -1 means UNKNOWN or undicided +int SAT_GetVarAsgnment(SAT_Manager mng, + int v_idx); + +// this is used for randomness in decision making +void SAT_SetRandomness(SAT_Manager mng, + int n); +// if the seed < 0, solver will use the day timer to +// get a "psuedo real random" seed. +void SAT_SetRandSeed(SAT_Manager mng, + int seed); + +// add a hookfunction. This function will be called +// every "interval" of decisions. You can add more than +// one such hook functions. i.e. call SAT_AddHookFun more +// than once. +void SAT_AddHookFun(SAT_Manager mng, + void (*fun)(void *), + int interval); + +// /* ======================================================= +// This function is for users who want to customize their own +// decision making strategy. +// +// What you can do is add a hook function with interval of 1, +// that function will be called before every decision. Inside +// this hook function, use SAT_MakeDecision to make decision +// with variable "vid" and "sign". sign = 1 means value of +// the variable be 0. +// +// If there are no free variable left, problem is satisfied, +// call SAT_MakeDecision with vid = 0 && sign = 0 will cause +// solver exit with status "SATISFIABLE". +// +// Here is an example: +// +// void my_own_decision (SAT_Manager mng) +// { +// int n_var = SAT_NumVariables(mng); +// int i; +// for (i=1; i= n_var) //every var got an assignment, no free var left +// SAT_MakeDecision (mng, 0, 0); +// } +// ======================================================== */ +void SAT_MakeDecision(SAT_Manager mng, + int vid, + int sign); + +// Following are statistics collecting functions +int SAT_EstimateMemUsage(SAT_Manager mng); +// time elapsed from last call of GetElapsedCPUTime +float SAT_GetElapsedCPUTime(SAT_Manager mng); +// current cpu time +float SAT_GetCurrentCPUTime(SAT_Manager mng); +// time spent on the whole solving process +float SAT_GetCPUTime(SAT_Manager mng); + +int SAT_NumLiterals(SAT_Manager mng); + +int SAT_NumClauses(SAT_Manager mng); + +int SAT_NumVariables(SAT_Manager mng); + +int SAT_InitNumLiterals(SAT_Manager mng); + +int SAT_InitNumClauses(SAT_Manager mng); + +long64 SAT_NumAddedLiterals(SAT_Manager mng); + +int SAT_NumAddedClauses(SAT_Manager mng); + +int SAT_NumShrinkings(SAT_Manager mng); + +int SAT_NumDeletedClauses(SAT_Manager mng); + +int SAT_NumDelOrigCls(SAT_Manager mng); + +long64 SAT_NumDeletedLiterals(SAT_Manager mng); + +int SAT_NumDecisions(SAT_Manager mng); +int SAT_NumDecisionsStackConf(SAT_Manager mng); +int SAT_NumDecisionsVsids(SAT_Manager mng); +int SAT_NumDecisionsShrinking(SAT_Manager mng); + + +int SAT_Random_Seed(SAT_Manager mng); + +long64 SAT_NumImplications(SAT_Manager mng); + +int SAT_MaxDLevel(SAT_Manager mng); + +float SAT_AverageBubbleMove(SAT_Manager mng); +// Following function will allow you to traverse all the +// clauses and literals. Clause is represented by a index. +// The original clauses' indice are not changed during the +// whole process, while added clauses may get deleted, so +// a certain index may not always represent the same +// clause, also, a index may not always be valid. +int SAT_GetFirstClause(SAT_Manager mng); + +// GetClauseType will get the clause's type. it can be +// ORIGINAL_CL, CONFLICT_CL, PROBE_CL +int SAT_GetClauseType(SAT_Manager mng, int cl_idx); + +// if there are no more clauses left, return value is -1. +// the organization is like : +// index 0 ... InitNumClauses - 1 are the original clauses +// after that, they are added clauses. +int SAT_GetNextClause(SAT_Manager mng, int cl_idx); + +int SAT_GetClauseNumLits(SAT_Manager mng, int cl_idx); + +// the lits array should have been pre-allocated enough memory +// to store all the lits of a clause. Use SAT_GetClauseNumLits to find +// out before-hand how much memory is required. +void SAT_GetClauseLits(SAT_Manager mng, int cl_idx, int * lits); + +// Following functions dictate the run time behavior +// Don't mess with them unless you know what you are doing +void SAT_EnableConfClsDeletion(SAT_Manager mng); +void SAT_DisableConfClsDeletion(SAT_Manager mng); +void SAT_SetClsDeletionInterval(SAT_Manager mng, int freq); + +void SAT_SetMaxUnrelevance(SAT_Manager mng, int n); +void SAT_SetMinClsLenForDelete(SAT_Manager mng, int n); +void SAT_SetMaxConfClsLenAllowed(SAT_Manager mng, int n); + +// void SAT_AllowMultipleConflicts(SAT_Manager mng); +// void SAT_AllowMultipleConfCls(SAT_Manager mng); +// void SAT_SetLitPoolCompactRatio(SAT_Manager mng, float ratio); +// void SAT_SetLitPoolExpantionRatio(SAT_Manager mng, float ration); + +// this function cleans all learned clauses in the database. +// it can be called if you incrementally solving many instances and +// the learned clauses occupy too much memory. By calling +// this function, it essentially equal to a fresh restart, i.e. throw +// away the learned clauses obtained so far. +void SAT_CleanUpDatabase(SAT_Manager mng); + +// Followings are functions to facilitate the translation from +// Circuit to a CNF representation. It will automatically generate +// the necessary clauses to represent the gates. +// Note: The input convension are the same as in AddClause, +// e.g. 2 * Vid + Sign +// NOTE: You need to make sure that the signals (a, b, c, o etc) are +// distinctive. I.e. the two inputs to a AND2 gate are different +// signals. Otherwise, the solver may behave incorrectly. Don't +// add a gate that has signal a and a' as inputs. You should do +// these kinds of special case simplifications by yourself. + + +void SAT_GenClsAnd2(SAT_Manager mng, + int a, + int b, + int o, + int gid = 0); + +void SAT_GenClsAndN(SAT_Manager mng, + int * inputs, + int num_inputs, + int o, + int gid = 0); + +void SAT_GenClsOr2(SAT_Manager mng, + int a, + int b, + int o, + int gid = 0); + +void SAT_GenClsOrN(SAT_Manager mng, + int * inputs, + int num_inputs, + int o, + int gid = 0); + +void SAT_GenClsNand2(SAT_Manager mng, + int a, + int b, + int o, + int gid = 0); + +void SAT_GenClsNandN(SAT_Manager mng, + int * inputs, + int num_inputs, + int o, + int gid = 0); + +void SAT_GenClsNor2(SAT_Manager mng, + int a, + int b, + int o, + int gid = 0); + +void SAT_GenClsNorN(SAT_Manager mng, + int * inputs, + int num_inputs, + int o, + int gid = 0); + +void SAT_GenClsXor(SAT_Manager mng, + int a, + int b, + int o, + int gid = 0); + +void SAT_GenClsNot(SAT_Manager mng, + int a, + int o, + int gid = 0); + +#endif Index: /vis_dev/zchaff/cnf_stats.cpp =================================================================== --- /vis_dev/zchaff/cnf_stats.cpp (revision 10) +++ /vis_dev/zchaff/cnf_stats.cpp (revision 10) @@ -0,0 +1,112 @@ +#include +#include +#include +#include +#include + + +#include +#include +#include + +using namespace std; + +const int MAX_WORD_LENGTH = 64; +const int MAX_LINE_LENGTH = 256000; + +int main(int argc, char** argv) { + assert(argc == 2); + char * filename = argv[1]; + int line_num = 0; + char line_buffer[MAX_LINE_LENGTH]; + char word_buffer[MAX_WORD_LENGTH]; + set clause_vars; + set clause_lits; + int num_cls = 0; + vector variables; + int var_num; + int cl_num; + ifstream inp(filename, ios::in); + if (!inp) { + cerr << "Can't open input file" << endl; + exit(1); + } + while (inp.getline(line_buffer, MAX_LINE_LENGTH)) { + ++line_num; + if (line_buffer[0] == 'c') { + continue; + } + else if (line_buffer[0] == 'p') { + int arg = sscanf(line_buffer, "p cnf %d %d", &var_num, &cl_num); + if (arg < 2) { + cerr << "Unable to read number of variables and clauses" + << "at line " << line_num << endl; + exit(3); + } + variables.resize(var_num + 1); + for (int i = 0; i < var_num + 1; ++i) + variables[i] = false; + } else { // Clause definition or continuation + char *lp = line_buffer; + do { + char *wp = word_buffer; + while (*lp && ((*lp == ' ') || (*lp == '\t'))) { + lp++; + } + while (*lp && (*lp != ' ') && (*lp != '\t') && (*lp != '\n')) { + *(wp++) = *(lp++); + } + *wp = '\0'; // terminate string + + if (strlen(word_buffer) != 0) { // check if number is there + int var_idx = atoi(word_buffer); + int sign = 0; + + if (var_idx != 0) { + if (var_idx < 0) { + var_idx = -var_idx; + sign = 1; + } + clause_vars.insert(var_idx); + clause_lits.insert((var_idx << 1) + sign); + } else { + // add this clause + if (clause_vars.size() != 0 && + clause_vars.size() == clause_lits.size()) { + vector temp; + for (set::iterator itr = clause_lits.begin(); + itr != clause_lits.end(); ++itr) + temp.push_back(*itr); + for (unsigned i = 0; i < temp.size(); ++i) + variables[temp[i]>>1] = true; + ++num_cls; + } else { + cout << "Literals of both polarity at line " + << line_num << ", clause skipped " << endl; + } + // it contain var of both polarity, so is automatically + // satisfied, just skip it + clause_lits.clear(); + clause_vars.clear(); + } + } + } + while (*lp); + } + } + if (!inp.eof()) { + cerr << "Input line " << line_num << " too long. Unable to continue..." + << endl; + exit(2); + } + assert(clause_vars.size() == 0); + int num_vars = 0; + for (unsigned i = 0; i < variables.size(); ++i) { + if (variables[i]) + ++num_vars; + } + cout <<"Statistics of CNF file:\t\t" << filename << "\n" + <<" Claim:\t\t Cl: " << cl_num << "\t Var: " << var_num << "\n" + <<" Actual:\t Cl: " << num_cls << "\t Var: " << num_vars << endl; + return 0; +} Index: /vis_dev/zchaff/run_till_fix.pl =================================================================== --- /vis_dev/zchaff/run_till_fix.pl (revision 10) +++ /vis_dev/zchaff/run_till_fix.pl (revision 10) @@ -0,0 +1,37 @@ +#!/usr/bin/perl -w + +use strict; + +die "Usage:\nrun_till_fix CNF_Filename [Num_Max_Iterations]" if (@ARGV < 1); + +my $file = $ARGV[0]; +my $max_iteration = @ARGV > 1 ? $ARGV[1] : 1000; +my $last_cls_count = 0; +my $filename = $file."_itr_0"; +$filename =~ s/.*\///; + +system("cp $file $filename"); + +$file =~ s/.*\///; + +for (my $i = 0; $i < $max_iteration; ++$i) { + + open INPUT, "<$filename" or die "$!\n"; + + my @tokens; + + while () { + @tokens = split / /; + last if ($tokens[0] eq "p"); + } + + last if $tokens[3] == $last_cls_count; + + $last_cls_count = $tokens[3]; + + system("zchaff $filename"); + system("zverify_df $filename resolve_trace -core"); + my $j = $i + 1; + $filename = $file."_itr_".$j; + system("mv unsat_core.cnf $filename"); +} Index: /vis_dev/zchaff/sat_solver.cpp =================================================================== --- /vis_dev/zchaff/sat_solver.cpp (revision 10) +++ /vis_dev/zchaff/sat_solver.cpp (revision 10) @@ -0,0 +1,282 @@ +/* =========FOR INTERNAL USE ONLY. NO DISTRIBUTION PLEASE ========== */ + +/********************************************************************* + Copyright 2000-2004, Princeton University. All rights reserved. + By using this software the USER indicates that he or she has read, + understood and will comply with the following: + + --- Princeton University hereby grants USER nonexclusive permission + to use, copy and/or modify this software for internal, noncommercial, + research purposes only. Any distribution, including commercial sale + or license, of this software, copies of the software, its associated + documentation and/or modifications of either is strictly prohibited + without the prior consent of Princeton University. Title to copyright + to this software and its associated documentation shall at all times + remain with Princeton University. Appropriate copyright notice shall + be placed on all software copies, and a complete copy of this notice + shall be included in all copies of the associated documentation. + No right is granted to use in advertising, publicity or otherwise + any trademark, service mark, or the name of Princeton University. + + + --- This software and any associated documentation is provided "as is" + + PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS + OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A + PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR + ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, + TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. + + Princeton University shall not be liable under any circumstances for + any direct, indirect, special, incidental, or consequential damages + with respect to any claim by USER or any third party on account of + or arising from the use, or inability to use, this software or its + associated documentation, even if Princeton University has been advised + of the possibility of those damages. +*********************************************************************/ +#include +#include +#include +#include +#include + +#include +#include +#include +#include "SAT.h" + +using namespace std; + +const int MAX_LINE_LENGTH = 65536; +const int MAX_WORD_LENGTH = 64; + +//This cnf parser function is based on the GRASP code by Joao Marques Silva +void read_cnf(SAT_Manager mng, char * filename ) +{ +// cout <<"read cnf "< clause_vars; + set clause_lits; + int line_num = 0; + + if(opendir(filename)){ + cerr << "Can't open input file, it's a directory" << endl; + exit(1); + } + + ifstream inp (filename, ios::in); + if (!inp) { + cerr << "Can't open input file" << endl; + exit(1); + } + while (inp.getline(line_buffer, MAX_LINE_LENGTH)) { + ++ line_num; + if (line_buffer[0] == 'c') { + continue; + } + else if (line_buffer[0] == 'p') { + int var_num; + int cl_num; + + int arg = sscanf (line_buffer, "p cnf %d %d", &var_num, &cl_num); + if( arg < 2 ) { + cerr << "Unable to read number of variables and clauses" + << "at line " << line_num << endl; + exit(3); + } + SAT_SetNumVariables(mng, var_num); //first element not used. + } + else { // Clause definition or continuation + char *lp = line_buffer; + do { + char *wp = word_buffer; + while (*lp && ((*lp == ' ') || (*lp == '\t'))) { + lp++; + } + while (*lp && (*lp != ' ') && (*lp != '\t') && (*lp != '\n')) { + *(wp++) = *(lp++); + } + *wp = '\0'; // terminate string + + if (strlen(word_buffer) != 0) { // check if number is there + int var_idx = atoi (word_buffer); + int sign = 0; + + if( var_idx != 0) { + if( var_idx < 0) { var_idx = -var_idx; sign = 1; } + clause_vars.insert(var_idx); + clause_lits.insert( (var_idx << 1) + sign); + } + else { + //add this clause + if (clause_vars.size() != 0 && (clause_vars.size() == clause_lits.size())) { //yeah, can add this clause + vector temp; + for (set::iterator itr = clause_lits.begin(); + itr != clause_lits.end(); ++itr) + temp.push_back (*itr); + SAT_AddClause(mng, & temp.begin()[0], temp.size() ); + } + else {} //it contain var of both polarity, so is automatically satisfied, just skip it + clause_lits.clear(); + clause_vars.clear(); + } + } + } + while (*lp); + } + } + if (!inp.eof()) { + cerr << "Input line " << line_num << " too long. Unable to continue..." << endl; + exit(2); + } +// assert (clause_vars.size() == 0); //some benchmark has no 0 in the last clause + if (clause_lits.size() && clause_vars.size()==clause_lits.size() ) { + vector temp; + for (set::iterator itr = clause_lits.begin(); + itr != clause_lits.end(); ++itr) + temp.push_back (*itr); + SAT_AddClause(mng, & temp.begin()[0], temp.size() ); + } + clause_lits.clear(); + clause_vars.clear(); +// cout <<"done read cnf"<= 0; + cl_idx = SAT_GetNextClause(mng, cl_idx)) { + int len = SAT_GetClauseNumLits(mng, cl_idx); + int * lits = new int[len+1]; + SAT_GetClauseLits( mng, cl_idx, lits); + int i; + for (i=0; i< len; ++i) { + int v_idx = lits[i] >> 1; + int sign = lits[i] & 0x1; + int var_value = SAT_GetVarAsgnment( mng, v_idx); + if( (var_value == 1 && sign == 0) || + (var_value == 0 && sign == 1) ) break; + } + if (i >= len) { + cerr << "Verify Satisfiable solution failed, please file a bug report, thanks. " << endl; + exit(6); + } + delete [] lits; + ++ num_verified; + } + cout <<"c "<< num_verified << " Clauses are true, Verify Solution successful."< +#include + +using namespace std; + +#include "zchaff_base.h" + +void CLitPoolElement::dump(ostream & os) { + os << (var_sign() ? " -" : " +") << var_index(); + if (is_watched()) + os << "*"; +} + +void CClause::dump(ostream & os) { + if (status() == DELETED_CL) + os << "\t\t\t======removed====="; + for (int i = 0, sz = num_lits(); i < sz; ++i) + os << literal(i); + os << endl; +} + +bool CClause::self_check(void) { + assert(num_lits() > 0); + int watched = 0; + for (unsigned i = 0; i < num_lits(); ++i) { + assert(literal(i).is_literal()); + if (literal(i).is_watched()) + ++watched; + } + assert(num_lits() ==1 || watched == 2); // either unit, or have two watched + assert(!literal(num_lits() + 1).is_literal()); + return true; +} + +bool CVariable::self_check(void) { + for (unsigned i = 0; i < 2; ++i) { + vector& w = watched(i); + for (unsigned j = 0; j < w.size(); ++j) { + assert(w[j]->is_watched()); + assert((unsigned)w[j]->var_sign() == i); + } + } + return true; +} + +void CVariable::dump(ostream & os) { + if (is_marked()) + os << "*" ; + os << "V: " << _value << " DL: " << _dlevel << " POS: "<< _assgn_stack_pos + << " Ante: " << _antecedent << endl; + for (unsigned j = 0; j < 2; ++j) { + os << (j == 0 ? "WPos " : "WNeg ") << "(" ; + for (unsigned i = 0; i < watched(j).size(); ++i) + os << watched(j)[i]->find_clause_index() << " " ; + os << ")" << endl; + } +#ifdef KEEP_LIT_CLAUSES + for (unsigned j = 0; j < 2; ++j) { + os << (j == 0 ? "Pos " : "Neg ") << "(" ; + for (unsigned i = 0; i < lit_clause(j).size(); ++i) + os << lit_clause(j)[i] << " " ; + os << ")" << endl; + } +#endif + os << endl; +} Index: /vis_dev/zchaff/zchaff_base.h =================================================================== --- /vis_dev/zchaff/zchaff_base.h (revision 10) +++ /vis_dev/zchaff/zchaff_base.h (revision 10) @@ -0,0 +1,506 @@ +// /********************************************************************* +// Copyright 2000-2004, Princeton University. All rights reserved. +// By using this software the USER indicates that he or she has read, +// understood and will comply with the following: +// +// --- Princeton University hereby grants USER nonexclusive permission +// to use, copy and/or modify this software for internal, noncommercial, +// research purposes only. Any distribution, including commercial sale +// or license, of this software, copies of the software, its associated +// documentation and/or modifications of either is strictly prohibited +// without the prior consent of Princeton University. Title to copyright +// to this software and its associated documentation shall at all times +// remain with Princeton University. Appropriate copyright notice shall +// be placed on all software copies, and a complete copy of this notice +// shall be included in all copies of the associated documentation. +// No right is granted to use in advertising, publicity or otherwise +// any trademark, service mark, or the name of Princeton University. +// +// +// --- This software and any associated documentation is provided "as is" +// +// PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS +// OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A +// PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR +// ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, +// TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. +// +// Princeton University shall not be liable under any circumstances for +// any direct, indirect, special, incidental, or consequential damages +// with respect to any claim by USER or any third party on account of +// or arising from the use, or inability to use, this software or its +// associated documentation, even if Princeton University has been advised +// of the possibility of those damages. +// *********************************************************************/ + + +#ifndef __BASIC_CLASSES__ +#define __BASIC_CLASSES__ + +#include + +#include "zchaff_header.h" + +#define UNKNOWN 2 +#define NULL_CLAUSE -1 + +#define VOLATILE_GID -1 +#define PERMANENT_GID 0 +// #define KEEP_LIT_CLAUSES +typedef int ClauseIdx; // Used to refer a clause. Because of dynamic + // allocation of vector storage, no pointer is allowered + +#ifndef _CLS_STATUS_ +#define _CLS_STATUS_ +enum CLAUSE_STATUS { + ORIGINAL_CL, + CONFLICT_CL, + DELETED_CL, +}; +#endif + +// /**Class******************************************************************** +// +// Synopsis [Definition of a literal] +// +// Description [A literal is a variable with phase. Two things specify a +// literal: its "sign", and its variable index. +// +// Each clause that has more than 1 literal contains two special +// literals. They are being "watched". A literal is marked with +// 2 bits: 00->not watched; 11->watched, direction = 1; +// 01->watched, dir = -1; 10 is not valid. These two bits occupy +// the least significant bits of the literal. +// +// Each literal is represented by a 32 bit signed integer. The +// higher 29 bits represent the variable index. At most 2**28 +// varialbes are allowed. If the sign of this integer is +// negative, it means that it is not a valid literal. It could +// be a clause index or a deleted literal pool element. The 3rd +// least significant bit is used to mark its sign. +// 0->positive, 1->negative. +// +// The literals are collected in a storage space called literal +// pool. An element in a literal pool can be a literal or a +// special spacing element to indicate the termination of a +// clause. The spacing elements has negative value of the clause +// index.] +// +// Right Hand spacing element has the clause id, so why is it +// not less than 0? +// +// SeeAlso [CDatabase, CClause] +// +// **************************************************************************** + +class CLitPoolElement { + protected: + int32 _val; + + public: + // constructors & destructors + CLitPoolElement(void):_val(0) {} + + ~CLitPoolElement() {} + + // member access function + int & val(void) { + return _val; + } + + // stands for signed variable, i.e. 2*var_idx + sign + int s_var(void) { + return _val >> 2; + } + + unsigned var_index(void) { + return _val >> 3; + } + + unsigned var_sign(void) { + return ((_val >> 2) & 0x1); + } + + void set(int s_var) { + _val = (s_var << 2); + } + + void set(int vid, int sign) { + _val = (((vid << 1) + sign) << 2); + } + + // followings are for manipulate watched literals + int direction(void) { + return ((_val & 0x3) - 2); + } + + bool is_watched(void) { + return ((_val & 0x3) != 0); + } + + void unwatch(void) { + _val = _val & (~0x3); + } + + void set_watch(int dir) { + _val = _val + dir + 2; + } + + // following are used for spacing (e.g. indicate clause's end) + bool is_literal(void) { + return _val > 0; + } + + void set_clause_index(int cl_idx) { + _val = - cl_idx; + } + + ClauseIdx get_clause_index(void) { + assert(_val <= 0); + return -_val; + } + + // misc functions + unsigned find_clause_index(void) { + CLitPoolElement * ptr; + for (ptr = this; ptr->is_literal(); ++ptr); + return ptr->get_clause_index(); + } + + // every class should have a dump function and a self check function + void dump(ostream & os= cout); + + friend ostream & operator << (ostream & os, CLitPoolElement & l) { + l.dump(os); + return os; + } +}; + +// /**Class******************************************************************** +// +// Synopsis [Definition of a clause] +// +// Description [A clause is consisted of a certain number of literals. +// All literals are collected in a single large vector, called +// literal pool. Each clause has a pointer to the beginning +// position of it's literals in the pool. +// +// Zchaff support incremental SAT. Clauses can be added or +// deleted from the database during search. To accomodate this +// feature, some modifications are needed. +// +// Clauses can be generated during search by conflict driven +// analysis. Conflict clauses are generated by a resolution +// process. Therefore, if after one search, some clauses got +// deleted, then some of the learned conflict clause may be +// invalidated. To maintain the integrity of the clause +// database, it is necessary to keep track of the clauses that +// are involved in the resolution process for a certain conflict +// clause so that when those clauses are deleted, the conflict +// clause should also be deleted. +// +// The scheme we implement is similar to the scheme described in +// : Ofer Strichman, Pruning techniques for the SAT-based +// Bounded Model Checking Problems, in Proc. 11th Advanced +// Research Working Conference on Correct Hardware Design and +// Verification Methods (CHARME'01) +// ] +// +// SeeAlso [CDatabase] +// +// **************************************************************************** +class CClause { + protected: + CLitPoolElement * _first_lit; // pointer to the first literal + unsigned _num_lits ; + CLAUSE_STATUS _status : 3; + unsigned _id : 29; // the unique ID of a clause + unsigned _gflag; // the clause group id flag, + // maximum allow WORD_WIDTH groups + int _activity; + int _sat_lit_idx; + + public: + + // constructors & destructors + CClause(void) { + _sat_lit_idx = 0; + } + + ~CClause() {} + + // initialization & clear up + void init(CLitPoolElement * head, unsigned num_lits, unsigned gflag) { + _first_lit = head; + _num_lits = num_lits; + _gflag = gflag; + } + + // member access function + inline int & activity(void) { + return _activity; + } + + inline int & sat_lit_idx(void) { + return _sat_lit_idx; + } + + inline CLitPoolElement * literals(void) { + // literals()[i] is it's the i-th literal + return _first_lit; + } + + // return the idx-th literal + inline CLitPoolElement & literal(int idx) { + return *(_first_lit + idx); + } + + // use it only if you want to modify _first_lit + inline CLitPoolElement * & first_lit(void) { + return _first_lit; + } + + inline unsigned & num_lits(void) { + return _num_lits; + } + + inline unsigned id(void) { + return _id; + } + + inline void set_id(int id) { + _id = id; + } + + inline CLAUSE_STATUS status(void) { + return _status; + } + + inline void set_status(CLAUSE_STATUS st) { + _status = st; + } + + // manipulate the group flag + inline unsigned & gflag(void) { + return _gflag; + } + + inline bool gid(int i) { + assert(i >= 1 && i <= WORD_WIDTH); + return ((_gflag & (1 << (i - 1))) != 0); + } + + inline void set_gid(int i) { + assert(i >= 1 && i <= WORD_WIDTH); + _gflag |= (1 << (i - 1)); + } + + inline void clear_gid(int i) { + assert(i >= 1 && i <= WORD_WIDTH); + _gflag &= ~(1 << (i - 1)); + } + + // misc function + bool self_check(void); + + void dump(ostream & os = cout); + + friend ostream & operator << (ostream & os, CClause & cl) { + cl.dump(os); + return os; + } +}; + + +// /**Class******************************************************************** +// +// Synopsis [Definition of a variable] +// +// Description [CVariable contains the necessary information for a variable.] +// +// SeeAlso [CDatabase] +// +// **************************************************************************** +class CVariable { + protected: + unsigned _value : 2; // it can take 3 values, 0, 1 and UNKNOWN + bool _marked : 1; // used in conflict analysis. + unsigned _new_cl_phase : 2; // it can take 3 value + // 0: pos phase, 1: neg phase, UNKNOWN : not in new clause; + // It is used to keep track of literals appearing + // in newly added clause so that + // a. each variable can only appearing in one phase + // b. same literal won't appear more than once. + bool _enable_branch : 1; // if this variable is enabled in branch + // selection + int _implied_sign : 1; // when a var is implied, here is the + // sign (1->negative, 0->positive) + ClauseIdx _antecedent; // used in conflict analysis. + int _dlevel; // decision level this variable being assigned + int _assgn_stack_pos; // the position where it is in the assignment + // stack + int _lits_count[2]; // how many literals are there with this + // variable. (two phases) + int _2_lits_count[2]; // how many literals in 2 literal clauses are + // there with this variable. (two phases) + vector _watched[2]; // watched literals of this + // var. 0: pos phase, 1: neg phase + +#ifdef KEEP_LIT_CLAUSES + vector _lit_clauses[2]; // this will keep track of ALL the + // appearance of the variable in + // clauses + // note this will increase the database + // size by upto a factor of 2 +#endif + int _scores[2]; // the score used for decision making + int _var_score_pos; // keep track of this variable's + // position in the sorted score array + + public: + // constructors & destructors + CVariable(void) { + init(); + _lits_count[0] = _lits_count[1] = 0; + _2_lits_count[0] = _2_lits_count[1] = 0; + } + + ~CVariable() {} + + void init(void) { + _value = UNKNOWN; + _antecedent = NULL_CLAUSE; + _marked = false; + _dlevel = -1; + _assgn_stack_pos = -1; + _new_cl_phase = UNKNOWN; + _scores[0] = _scores[1] = 0; + _enable_branch = true; + } + + // member access function + inline int & score(int i) { + return _scores[i]; + } + + inline int & two_lits_count(int i) { + return _2_lits_count[i]; + } + + inline int score(void) { + // return 1; this will make a fixed order branch heuristic + int result = score(0) > score(1) ? score(0) : score(1); + if (_dlevel == 0) + result =-1; + return result; + } + + inline int & var_score_pos(void) { + return _var_score_pos; + } + + inline void set_var_score_pos(int pos) { + _var_score_pos = pos; + } + + inline unsigned value(void) { + return _value; + } + + inline void set_value(unsigned v) { + _value = v; + } + + inline int & dlevel(void) { + return _dlevel; + } + + inline int get_dlevel(void) { + return _dlevel; + } + + inline void set_dlevel(int dl) { + _dlevel = dl; + } + + inline int & assgn_stack_pos(void) { + return _assgn_stack_pos; + } + + inline int & lits_count(int i) { + return _lits_count[i]; + } + + inline bool is_marked(void) { + return _marked; + } + + inline int get_implied_sign(void) { + return _implied_sign; + } + + inline void set_implied_sign(int sign) { + _implied_sign = sign; + } + + inline unsigned new_cl_phase(void) { + return _new_cl_phase; + } + + inline void set_new_cl_phase(unsigned phase) { + _new_cl_phase = phase; + } + + inline void set_marked(void) { + _marked = true; + } + + inline void clear_marked(void) { + _marked = false; + } + + inline ClauseIdx & antecedent(void) { + return _antecedent; + } + + inline ClauseIdx get_antecedent(void) { + return _antecedent; + } + + inline void set_antecedent(ClauseIdx cl) { + _antecedent = cl; + } + + inline vector & watched(int i) { + return _watched[i]; + } + + inline void enable_branch(void) { + _enable_branch = true; + } + + inline void disable_branch(void) { + _enable_branch = false; + } + + inline bool is_branchable(void) { + return _enable_branch; + } + +#ifdef KEEP_LIT_CLAUSES + inline vector & lit_clause(int i) { + return _lit_clauses[i]; + } +#endif + + // misc function + bool self_check(void); + + void dump(ostream & os = cout); + + friend ostream & operator << (ostream & os, CVariable & v) { + v.dump(os); + return os; + } +}; +#endif Index: /vis_dev/zchaff/zchaff_clsgen.h =================================================================== --- /vis_dev/zchaff/zchaff_clsgen.h (revision 10) +++ /vis_dev/zchaff/zchaff_clsgen.h (revision 10) @@ -0,0 +1,234 @@ +// ********************************************************************* +// Copyright 2000-2004, Princeton University. All rights reserved. +// By using this software the USER indicates that he or she has read, +// understood and will comply with the following: +// +// --- Princeton University hereby grants USER nonexclusive permission +// to use, copy and/or modify this software for internal, noncommercial, +// research purposes only. Any distribution, including commercial sale +// or license, of this software, copies of the software, its associated +// documentation and/or modifications of either is strictly prohibited +// without the prior consent of Princeton University. Title to copyright +// to this software and its associated documentation shall at all times +// remain with Princeton University. Appropriate copyright notice shall +// be placed on all software copies, and a complete copy of this notice +// shall be included in all copies of the associated documentation. +// No right is granted to use in advertising, publicity or otherwise +// any trademark, service mark, or the name of Princeton University. +// +// +// --- This software and any associated documentation is provided "as is" +// +// PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS +// OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A +// PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR +// ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, +// TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. +// +// Princeton University shall not be liable under any circumstances for +// any direct, indirect, special, incidental, or consequential damages +// with respect to any claim by USER or any third party on account of +// or arising from the use, or inability to use, this software or its +// associated documentation, even if Princeton University has been advised +// of the possibility of those damages. +// ********************************************************************* + +#ifndef __CLAUSE_GENERATOR__ +#define __CLAUSE_GENERATOR__ +#include "zchaff_solver.h" + +class CClause_Gen { + private: + inline static int * ptr(vector::iterator itr) { + return &(*itr); + } + inline static int pos(int i) { + return i; + } + inline static int neg(int i) { + return i^0x1; + } + + public: + static void and2(CSolver & solver, int a, int b, int o, int gid = 0) { + // a*b=c <==> (a + o')( b + o')(a'+b'+o) + vector lits; + lits.clear(); + lits.push_back(pos(a)); + lits.push_back(neg(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + lits.clear(); + lits.push_back(pos(b)); + lits.push_back(neg(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + lits.clear(); + lits.push_back(neg(a)); + lits.push_back(neg(b)); + lits.push_back(pos(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + } + + static void and_n(CSolver & solver, int * inputs, int num_input, int o, + int gid = 0) { + vector lits; + int i; + for (i = 0; i < num_input; ++i) { + lits.clear(); + lits.push_back(pos(inputs[i])); + lits.push_back(neg(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + } + lits.clear(); + for (i = 0; i < num_input; ++i) + lits.push_back(neg(inputs[i])); + lits.push_back(pos(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + } + + static void or2(CSolver & solver, int a, int b, int o, int gid = 0) { + // a+b=c <==> (a' + c)( b' + c)(a + b + c') + vector lits; + lits.clear(); + lits.push_back(neg(a)); + lits.push_back(pos(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + lits.clear(); + lits.push_back(neg(b)); + lits.push_back(pos(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + lits.clear(); + lits.push_back(pos(a)); + lits.push_back(pos(b)); + lits.push_back(neg(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + } + + static void or_n(CSolver & solver, int * inputs, int num_input, int o, + int gid = 0) { + vector lits; + int i; + for (i = 0; i < num_input; ++i) { + lits.clear(); + lits.push_back(neg(inputs[i])); + lits.push_back(pos(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + } + lits.clear(); + for (i = 0; i < num_input; ++i) + lits.push_back(pos(inputs[i])); + lits.push_back(neg(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + } + + static void nand2(CSolver & solver, int a, int b, int o, int gid = 0) { + // a Nand b = o <==> (a + o)( b + o)(a' + b' + o') + vector lits; + lits.clear(); + lits.push_back(pos(a)); + lits.push_back(pos(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + lits.clear(); + lits.push_back(pos(b)); + lits.push_back(pos(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + lits.clear(); + lits.push_back(neg(a)); + lits.push_back(neg(b)); + lits.push_back(neg(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + } + + static void nand_n(CSolver & solver, int * inputs, int num_input, int o, + int gid = 0) { + vector lits; + int i; + for (i = 0; i < num_input; ++i) { + lits.clear(); + lits.push_back(pos(inputs[i])); + lits.push_back(pos(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + } + lits.clear(); + for (i = 0; i < num_input; ++i) + lits.push_back(neg(inputs[i])); + lits.push_back(neg(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + } + + static void nor2(CSolver & solver, int a, int b, int o, int gid = 0) { + // a Nor b = o <==> (a' + o')( b' + o')(a + b + o) + vector lits; + lits.clear(); + lits.push_back(neg(a)); + lits.push_back(neg(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + lits.clear(); + lits.push_back(neg(b)); + lits.push_back(neg(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + lits.clear(); + lits.push_back(pos(a)); + lits.push_back(pos(b)); + lits.push_back(pos(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + } + + static void nor_n(CSolver & solver, int * inputs, int num_input, int o, + int gid = 0) { + vector lits; + int i; + for (i = 0; i < num_input; ++i) { + lits.clear(); + lits.push_back(neg(inputs[i])); + lits.push_back(neg(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + } + lits.clear(); + for (i = 0; i < num_input; ++i) + lits.push_back(pos(inputs[i])); + lits.push_back(pos(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + } + + static void xor2(CSolver & solver, int a, int b, int o, int gid = 0) { + // a xor b = o <==> (a' + b' + o') + // (a + b + o' ) + // (a' + b + o) + // (a + b' + o) + vector lits; + lits.clear(); + lits.push_back(neg(a)); + lits.push_back(neg(b)); + lits.push_back(neg(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + lits.clear(); + lits.push_back(pos(a)); + lits.push_back(pos(b)); + lits.push_back(neg(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + lits.clear(); + lits.push_back(neg(a)); + lits.push_back(pos(b)); + lits.push_back(pos(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + lits.clear(); + lits.push_back(pos(a)); + lits.push_back(neg(b)); + lits.push_back(pos(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + } + + static void not1(CSolver & solver, int a, int o, int gid = 0) { + // a' = o <==> (a' + o')( a + o) + vector lits; + lits.clear(); + lits.push_back(neg(a)); + lits.push_back(neg(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + lits.clear(); + lits.push_back(pos(a)); + lits.push_back(pos(o)); + solver.add_orig_clause(ptr(lits.begin()), lits.size(), gid); + } +}; +#endif Index: /vis_dev/zchaff/zchaff_dbase.cpp =================================================================== --- /vis_dev/zchaff/zchaff_dbase.cpp (revision 10) +++ /vis_dev/zchaff/zchaff_dbase.cpp (revision 10) @@ -0,0 +1,478 @@ +// ********************************************************************* +// Copyright 2000-2004, Princeton University. All rights reserved. +// By using this software the USER indicates that he or she has read, +// understood and will comply with the following: +// +// --- Princeton University hereby grants USER nonexclusive permission +// to use, copy and/or modify this software for internal, noncommercial, +// research purposes only. Any distribution, including commercial sale +// or license, of this software, copies of the software, its associated +// documentation and/or modifications of either is strictly prohibited +// without the prior consent of Princeton University. Title to copyright +// to this software and its associated documentation shall at all times +// remain with Princeton University. Appropriate copyright notice shall +// be placed on all software copies, and a complete copy of this notice +// shall be included in all copies of the associated documentation. +// No right is granted to use in advertising, publicity or otherwise +// any trademark, service mark, or the name of Princeton University. +// +// +// --- This software and any associated documentation is provided "as is" +// +// PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS +// OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A +// PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR +// ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, +// TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. +// +// Princeton University shall not be liable under any circumstances for +// any direct, indirect, special, incidental, or consequential damages +// with respect to any claim by USER or any third party on account of +// or arising from the use, or inability to use, this software or its +// associated documentation, even if Princeton University has been advised +// of the possibility of those damages. +// ********************************************************************/ + +#include + +#include +#include +#include + +using namespace std; + +#include "zchaff_dbase.h" + +CDatabase::CDatabase(void) { + _stats.mem_used_up = false; + _stats.init_num_clauses = 0; + _stats.init_num_literals = 0; + _stats.num_added_clauses = 0; + _stats.num_added_literals = 0; + _stats.num_deleted_clauses = 0; + _stats.num_del_orig_cls = 0; + _stats.num_deleted_literals = 0; + _stats.num_enlarge = 0; + _stats.num_compact = 0; + _lit_pool_start = (CLitPoolElement *) malloc(sizeof(CLitPoolElement) * + STARTUP_LIT_POOL_SIZE); + _lit_pool_finish = _lit_pool_start; + _lit_pool_end_storage = _lit_pool_start + STARTUP_LIT_POOL_SIZE; + lit_pool_push_back(0); // set the first element as a dummy element + _params.mem_limit = 1024 * 1024 * 1024; // that's 1 G + variables()->resize(1); // var_id == 0 is never used. + _allocated_gid = 0; +} + +CDatabase::~CDatabase(void) { + free(_lit_pool_start); +} + +unsigned CDatabase::estimate_mem_usage(void) { + unsigned mem_lit_pool = sizeof(CLitPoolElement) * (lit_pool_size() + + lit_pool_free_space()); + unsigned mem_vars = sizeof(CVariable) * variables()->capacity(); + unsigned mem_cls = sizeof(CClause) * clauses()->capacity(); + unsigned mem_cls_queue = sizeof(int) * _unused_clause_idx.size(); + unsigned mem_watched = 2 * num_clauses() * sizeof(CLitPoolElement *); + unsigned mem_lit_clauses = 0; +#ifdef KEEP_LIT_CLAUSES + mem_lit_clauses = num_literals() * sizeof(ClauseIdx); +#endif + return (mem_lit_pool + mem_vars + mem_cls + + mem_cls_queue + mem_watched + mem_lit_clauses); +} + +unsigned CDatabase::mem_usage(void) { + int mem_lit_pool = (lit_pool_size() + lit_pool_free_space()) * + sizeof(CLitPoolElement); + int mem_vars = sizeof(CVariable) * variables()->capacity(); + int mem_cls = sizeof(CClause) * clauses()->capacity(); + int mem_cls_queue = sizeof(int) * _unused_clause_idx.size(); + int mem_watched = 0, mem_lit_clauses = 0; + for (unsigned i = 0, sz = variables()->size(); i < sz ; ++i) { + CVariable & v = variable(i); + mem_watched += v.watched(0).capacity() + v.watched(1).capacity(); +#ifdef KEEP_LIT_CLAUSES + mem_lit_clauses += v.lit_clause(0).capacity() + v.lit_clause(1).capacity(); +#endif + } + mem_watched *= sizeof(CLitPoolElement*); + mem_lit_clauses *= sizeof(ClauseIdx); + return (mem_lit_pool + mem_vars + mem_cls + + mem_cls_queue + mem_watched + mem_lit_clauses); +} + +int CDatabase::alloc_gid(void) { + for (unsigned i = 1; i <= WORD_WIDTH; ++i) { + if (is_gid_allocated(i) == false) { + _allocated_gid |= (1 << (i-1)); + return i; + } + } + warning(_POSITION_, "Not enough GID"); + return VOLATILE_GID; +} + +void CDatabase::free_gid(int gid) { + assert(gid > 0 && "Can't free volatile or permanent group"); + assert(gid <= WORD_WIDTH && "gid > WORD_WIDTH?"); + if (!is_gid_allocated(gid)) { + fatal(_POSITION_, "Can't free unallocated GID"); + } + _allocated_gid &= (~(1<< (gid-1))); +} + +bool CDatabase::is_gid_allocated(int gid) { + if (gid == VOLATILE_GID || gid == PERMANENT_GID) + return true; + assert(gid <= WORD_WIDTH && gid > 0); + if (_allocated_gid & (1 << (gid -1))) + return true; + return false; +} + +int CDatabase::merge_clause_group(int g2, int g1) { + assert(g1 >0 && g2> 0 && "Can't merge with permanent or volatile group"); + assert(g1 != g2); + assert(is_gid_allocated(g1) && is_gid_allocated(g2)); + for (unsigned i = 0, sz = clauses()->size(); i < sz; ++i) { + if (clause(i).status() != DELETED_CL) { + if (clause(i).gid(g1) == true) { + clause(i).clear_gid(g1); + clause(i).set_gid(g2); + } + } + } + free_gid(g1); + return g2; +} + +void CDatabase::mark_clause_deleted(CClause & cl) { + ++_stats.num_deleted_clauses; + _stats.num_deleted_literals += cl.num_lits(); + CLAUSE_STATUS status = cl.status(); + if (status == ORIGINAL_CL) + _stats.num_del_orig_cls++; + cl.set_status(DELETED_CL); + for (unsigned i = 0; i < cl.num_lits(); ++i) { + CLitPoolElement & l = cl.literal(i); + --variable(l.var_index()).lits_count(l.var_sign()); + l.val() = 0; + } + _unused_clause_idx.insert(&cl - &(*clauses()->begin())); +} + +bool CDatabase::is_conflicting(ClauseIdx cl) { + CLitPoolElement * lits = clause(cl).literals(); + for (int i = 0, sz= clause(cl).num_lits(); i < sz; ++i) { + if (literal_value(lits[i]) != 0) + return false; + } + return true; +} + +bool CDatabase::is_satisfied(ClauseIdx cl) { + CLitPoolElement * lits = clause(cl).literals(); + for (int i = 0, sz = clause(cl).num_lits(); i < sz; ++i) { + if (literal_value(lits[i]) == 1) + return true; + } + return false; +} + +bool CDatabase::is_unit(ClauseIdx cl) { + int num_unassigned = 0; + CLitPoolElement * lits = clause(cl).literals(); + for (unsigned i = 0, sz= clause(cl).num_lits(); i < sz; ++i) { + int value = literal_value(lits[i]); + if (value == 1) + return false; + else if (value != 0) + ++num_unassigned; + } + return num_unassigned == 1; +} + +int CDatabase::find_unit_literal(ClauseIdx cl) { + // will return 0 if not unit + int unit_lit = 0; + for (int i = 0, sz = clause(cl).num_lits(); i < sz; ++i) { + int value = literal_value(clause(cl).literal(i)); + if (value == 1) + return 0; + else if (value != 0) { + if (unit_lit == 0) + unit_lit = clause(cl).literals()[i].s_var(); + else + return 0; + } + } + return unit_lit; +} + +inline CLitPoolElement * CDatabase::lit_pool_begin(void) { + return _lit_pool_start; +} + +inline CLitPoolElement * CDatabase::lit_pool_end(void) { + return _lit_pool_finish; +} + +inline void CDatabase::lit_pool_incr_size(int size) { + _lit_pool_finish += size; + assert(_lit_pool_finish <= _lit_pool_end_storage); +} + +inline void CDatabase::lit_pool_push_back(int value) { + assert(_lit_pool_finish <= _lit_pool_end_storage); + _lit_pool_finish->val() = value; + ++_lit_pool_finish; +} + +inline int CDatabase::lit_pool_size(void) { + return _lit_pool_finish - _lit_pool_start; +} + +inline int CDatabase::lit_pool_free_space(void) { + return _lit_pool_end_storage - _lit_pool_finish; +} + +inline double CDatabase::lit_pool_utilization(void) { + // minus num_clauses() is because of spacing (i.e. clause indices) + return (double)num_literals() / ((double) (lit_pool_size() - num_clauses())) ; +} + +inline CLitPoolElement & CDatabase::lit_pool(int i) { + return _lit_pool_start[i]; +} + +void CDatabase::compact_lit_pool(void) { + unsigned i, sz; + int new_index = 1; + // first do the compaction for the lit pool + for (i = 1, sz = lit_pool_size(); i < sz; ++i) { + // begin with 1 because 0 position is always 0 + if (!lit_pool(i).is_literal() && !lit_pool(i-1).is_literal()) { + continue; + } else { + lit_pool(new_index) = lit_pool(i); + ++new_index; + } + } + _lit_pool_finish = lit_pool_begin() + new_index; + // update all the pointers to the literals; + // 1. clean up the watched pointers from variables + for (i = 1, sz = variables()->size(); i < sz; ++i) { + variable(i).watched(0).clear(); + variable(i).watched(1).clear(); + } + for (i = 1, sz = lit_pool_size(); i < sz; ++i) { + CLitPoolElement & lit = lit_pool(i); + // 2. reinsert the watched pointers + if (lit.is_literal()) { + if (lit.is_watched()) { + int var_idx = lit.var_index(); + int sign = lit.var_sign(); + variable(var_idx).watched(sign).push_back(& lit_pool(i)); + } + } else { // lit is not literal + // 3. update the clauses' first literal pointer + int cls_idx = lit.get_clause_index(); + clause(cls_idx).first_lit() = &lit_pool(i) - clause(cls_idx).num_lits(); + } + } + ++_stats.num_compact; +} + +bool CDatabase::enlarge_lit_pool(void) { + // will return true if successful, otherwise false. + unsigned i, sz; + // if memory efficiency < 2/3, we do a compaction + if (lit_pool_utilization() < 0.67) { + compact_lit_pool(); + return true; + } + // otherwise we have to enlarge it. + // first, check if memory is running out + int current_mem = estimate_mem_usage(); + float grow_ratio = 1; + if (current_mem < _params.mem_limit / 4) + grow_ratio = 2; + else if (current_mem < _params.mem_limit /2 ) + grow_ratio = 1.5; + else if (current_mem < _params.mem_limit * 0.8) + grow_ratio = 1.2; + if (grow_ratio < 1.2) { + if (lit_pool_utilization() < 0.9) { // still has some garbage + compact_lit_pool(); + return true; + } + else + return false; + } + // second, make room for new lit pool. + CLitPoolElement * old_start = _lit_pool_start; + CLitPoolElement * old_finish = _lit_pool_finish; + int old_size = _lit_pool_end_storage - _lit_pool_start; + int new_size = (int)(old_size * grow_ratio); + _lit_pool_start = (CLitPoolElement *) realloc(_lit_pool_start, + sizeof(CLitPoolElement) * + new_size); + _lit_pool_finish = _lit_pool_start + (old_finish - old_start); + _lit_pool_end_storage = _lit_pool_start + new_size; + + // update all the pointers + int displacement = _lit_pool_start - old_start; + for (i = 0; i < clauses()->size(); ++i) { + if (clause(i).status() != DELETED_CL) + clause(i).first_lit() += displacement; + } + for (i = 0, sz = variables()->size(); i < sz ; ++i) { + CVariable & v = variable(i); + for (int j = 0; j < 2 ; ++j) { + int k, sz1; + vector & watched = v.watched(j); + for (k = 0, sz1 = watched.size(); k < sz1 ; ++k) { + watched[k] += displacement; + } + } + } + ++_stats.num_enlarge; + return true; +} + +ClauseIdx CDatabase::get_free_clause_idx(void) { + ClauseIdx new_cl; + new_cl = _clauses.size(); + _clauses.resize(new_cl + 1); + clause(new_cl).set_id(_stats.num_added_clauses); + return new_cl; +} + +ClauseIdx CDatabase::add_clause(int * lits, int n_lits, int gflag) { + int new_cl; + // a. do we need to enlarge lits pool? + while (lit_pool_free_space() <= n_lits + 1) { + if (enlarge_lit_pool() == false) + return -1; // mem out, can't enlarge lit pool, because + // ClauseIdx can't be -1, so it shows error. + } + // b. get a free cl index; + new_cl = get_free_clause_idx(); + // c. add the clause lits to lits pool + CClause & cl = clause(new_cl); + cl.init(lit_pool_end(), n_lits, gflag); + lit_pool_incr_size(n_lits + 1); + if (n_lits == 2) { + ++variable(lits[0]>>1).two_lits_count(lits[0] & 0x1); + ++variable(lits[1]>>1).two_lits_count(lits[1] & 0x1); + } + for (int i = 0; i < n_lits; ++i) { + int var_idx = lits[i] >> 1; + assert((unsigned)var_idx < variables()->size()); + int var_sign = lits[i] & 0x1; + cl.literal(i).set(var_idx, var_sign); + ++variable(var_idx).lits_count(var_sign); +#ifdef KEEP_LIT_CLAUSES + variable(var_idx).lit_clause(var_sign).push_back(new_cl); +#endif + } + // the element after the last one is the spacing element + cl.literal(n_lits).set_clause_index(new_cl); + // d. set the watched pointers + if (cl.num_lits() > 1) { + // add the watched literal. note: watched literal must be the last free var + int max_idx = -1, max_dl = -1; + int i, sz = cl.num_lits(); + // set the first watched literal + for (i = 0; i < sz; ++i) { + int v_idx = cl.literal(i).var_index(); + int v_sign = cl.literal(i).var_sign(); + CVariable & v = variable(v_idx); + if (literal_value(cl.literal(i)) != 0) { + v.watched(v_sign).push_back(&cl.literal(i)); + cl.literal(i).set_watch(1); + break; + } else { + if (v.dlevel() > max_dl) { + max_dl = v.dlevel(); + max_idx = i; + } + } + } + if (i >= sz) { // no unassigned literal. so watch literal with max dlevel + int v_idx = cl.literal(max_idx).var_index(); + int v_sign = cl.literal(max_idx).var_sign(); + variable(v_idx).watched(v_sign).push_back(&cl.literal(max_idx)); + cl.literal(max_idx).set_watch(1); + } + + // set the second watched literal + max_idx = -1; + max_dl = -1; + for (i = sz-1; i >= 0; --i) { + if (cl.literal(i).is_watched()) + continue; // need to watch two different literals + int v_idx = cl.literal(i).var_index(); + int v_sign = cl.literal(i).var_sign(); + CVariable & v = variable(v_idx); + if (literal_value(cl.literal(i)) != 0) { + v.watched(v_sign).push_back(&cl.literal(i)); + cl.literal(i).set_watch(-1); + break; + } else { + if (v.dlevel() > max_dl) { + max_dl = v.dlevel(); + max_idx = i; + } + } + } + if (i < 0) { + int v_idx = cl.literal(max_idx).var_index(); + int v_sign = cl.literal(max_idx).var_sign(); + variable(v_idx).watched(v_sign).push_back(&cl.literal(max_idx)); + cl.literal(max_idx).set_watch(-1); + } + } + // update some statistics + ++_stats.num_added_clauses; + _stats.num_added_literals += n_lits; + return new_cl; +} + +void CDatabase::output_lit_pool_stats(void) { + cout << "Lit_Pool Used " << lit_pool_size() << " Free " + << lit_pool_free_space() + << " Total " << lit_pool_size() + lit_pool_free_space() + << " Num. Cl " << num_clauses() << " Num. Lit " << num_literals() + << " Efficiency " << lit_pool_utilization() << endl; +} + +void CDatabase::detail_dump_cl(ClauseIdx cl_idx, ostream & os) { + os << "CL : " << cl_idx; + CClause & cl = clause(cl_idx); + if (cl.status() == DELETED_CL) + os << "\t\t\t======removed====="; + char value; + for (unsigned i = 0; i < cl.num_lits(); ++i) { + if (literal_value(cl.literal(i)) == 0) + value = '0'; + else if (literal_value(cl.literal(i)) == 1) + value = '1'; + else + value = 'X'; + os << cl.literal(i) << "(" << value << "@" + << variable(cl.literal(i).var_index()).dlevel()<< ") "; + } + os << endl; +} + +void CDatabase::dump(ostream & os) { + unsigned i; + os << "Dump Database: " << endl; + for (i = 0; i < _clauses.size(); ++i) + detail_dump_cl(i); + for (i = 1; i < _variables.size(); ++i) + os << "VID " << i << ":\t" << variable(i); +} Index: /vis_dev/zchaff/zchaff_dbase.h =================================================================== --- /vis_dev/zchaff/zchaff_dbase.h (revision 10) +++ /vis_dev/zchaff/zchaff_dbase.h (revision 10) @@ -0,0 +1,298 @@ +// ********************************************************************* +// Copyright 2000-2004, Princeton University. All rights reserved. +// By using this software the USER indicates that he or she has read, +// understood and will comply with the following: +// +// --- Princeton University hereby grants USER nonexclusive permission +// to use, copy and/or modify this software for internal, noncommercial, +// research purposes only. Any distribution, including commercial sale +// or license, of this software, copies of the software, its associated +// documentation and/or modifications of either is strictly prohibited +// without the prior consent of Princeton University. Title to copyright +// to this software and its associated documentation shall at all times +// remain with Princeton University. Appropriate copyright notice shall +// be placed on all software copies, and a complete copy of this notice +// shall be included in all copies of the associated documentation. +// No right is granted to use in advertising, publicity or otherwise +// any trademark, service mark, or the name of Princeton University. +// +// +// --- This software and any associated documentation is provided "as is" +// +// PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS +// OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A +// PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR +// ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, +// TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. +// +// Princeton University shall not be liable under any circumstances for +// any direct, indirect, special, incidental, or consequential damages +// with respect to any claim by USER or any third party on account of +// or arising from the use, or inability to use, this software or its +// associated documentation, even if Princeton University has been advised +// of the possibility of those damages. +// *********************************************************************/ +#ifndef __ZCHAFF_DATABASE__ +#define __ZCHAFF_DATABASE__ + +#include "zchaff_base.h" + +#define STARTUP_LIT_POOL_SIZE 0x8000 + +// **Struct******************************************************************** +// +// Synopsis [Definition of the statistics of clause database] +// +// Description [] +// +// SeeAlso [CDatabase] +// +// **************************************************************************** + +struct CDatabaseStats { + bool mem_used_up; + unsigned init_num_clauses; + unsigned init_num_literals; + unsigned num_added_clauses; + long64 num_added_literals; + unsigned num_deleted_clauses; + unsigned num_del_orig_cls; + long64 num_deleted_literals; + unsigned num_compact; + unsigned num_enlarge; +}; + +// **Struct******************************************************************** +// +// Synopsis [Definition of the parameters of clause database] +// +// Description [] +// +// SeeAlso [CDatabase] +// +// **************************************************************************** + +struct CDatabaseParams { + int mem_limit; +}; + +// **Class********************************************************************* +// +// Synopsis [Definition of clause database ] +// +// Description [Clause Database is the place where the information of the +// SAT problem are stored. it is a parent class of CSolver ] +// +// SeeAlso [CSolver] +// +// **************************************************************************** + +class CDatabase { + protected: + CDatabaseStats _stats; + + CDatabaseParams _params; + + unsigned _allocated_gid; // the gids that have already been + // allocated + + // for efficiency, the memeory management of lit pool is done by the solver + CLitPoolElement * _lit_pool_start; // the begin of the lit vector + CLitPoolElement * _lit_pool_finish; // the tail of the used lit vector + CLitPoolElement * _lit_pool_end_storage; // the storage end of lit vector + + + vector _variables; // note: first element is not used + + vector _clauses; + + set _unused_clause_idx; + + ClauseIdx top_unsat_cls; + + protected: + // constructors & destructors + CDatabase() ; + + ~CDatabase(); + + void init_stats(void) { + _stats.mem_used_up = false; + _stats.init_num_clauses = num_clauses(); + _stats.init_num_literals = num_literals(); + _stats.num_deleted_clauses = 0; + _stats.num_del_orig_cls = 0; + _stats.num_deleted_literals = 0; + _stats.num_enlarge = 0; + _stats.num_compact = 0; + } + + // lit pool naming convention follows STL Vector + CLitPoolElement * lit_pool_begin(void); + + CLitPoolElement * lit_pool_end(void); + + void lit_pool_incr_size(int size); + + void lit_pool_push_back(int value); + + int lit_pool_size(void); + + int lit_pool_free_space(void); + + double lit_pool_utilization(void); + + CLitPoolElement & lit_pool(int i); + + // functions on lit_pool + void output_lit_pool_stats(void); + + // when allocated memeory runs out, do a reallocation + bool enlarge_lit_pool(void); + + void compact_lit_pool(void); // garbage collection + + unsigned literal_value(CLitPoolElement l) { + // note: it will return 0 or 1 or other, here "other" may not equal UNKNOWN + return (variable(l.var_index()).value() ^ l.var_sign()); + } + + unsigned svar_value(int svar) { + // note: it will return 0 or 1 or other, here "other" may not equal UNKNOWN + return (variable(svar >> 1).value() ^ (svar & 0x1)); + } + + // clause properties + void mark_clause_deleted(CClause & cl); + + int find_unit_literal(ClauseIdx cl); // if not unit clause, return 0. + + bool is_conflicting(ClauseIdx cl); // e.g. all literals assigned value 0 + + bool is_unit(ClauseIdx cl); + + bool is_satisfied(ClauseIdx cl); // e.g. at least one literal has value 1 + + // others + ClauseIdx get_free_clause_idx(void); + + ClauseIdx add_clause(int * lits, int n_lits, int gflag = 0); + + public: + + // member access function + inline vector* variables(void) { + return &_variables; + } + + inline CVariable & variable(int idx) { + return _variables[idx]; + } + + inline vector* clauses(void) { + return &_clauses; + } + + inline CClause & clause(ClauseIdx idx) { + return _clauses[idx]; + } + + inline CDatabaseStats & stats(void) { + return _stats; + } + + inline void set_mem_limit(int n) { + _params.mem_limit = n; + } + + // clause group management + int alloc_gid(void); + + void free_gid(int gid); + + inline int get_volatile_gid(void) { + return -1; + } + + inline int get_permanent_gid(void) { + return 0; + } + + bool is_gid_allocated(int gid); + + int merge_clause_group(int g1, int g2); + + // some stats + inline unsigned & init_num_clauses(void) { + return _stats.init_num_clauses; + } + + inline unsigned & init_num_literals(void) { + return _stats.init_num_literals; + } + + inline unsigned & num_added_clauses(void) { + return _stats.num_added_clauses; + } + + inline long64 & num_added_literals(void) { + return _stats.num_added_literals; + } + + inline unsigned & num_deleted_clauses(void) { + return _stats.num_deleted_clauses; + } + + inline unsigned & num_del_orig_cls(void) { + return _stats.num_del_orig_cls; + } + + inline long64 & num_deleted_literals(void) { + return _stats.num_deleted_literals; + } + + inline unsigned num_variables(void) { + return variables()->size() - 1; + } + + inline unsigned num_clauses(void) { + return _clauses.size() - _unused_clause_idx.size(); + } + + inline unsigned num_literals(void) { + return _stats.num_added_literals - _stats.num_deleted_literals; + } + + inline unsigned num_mem_compacts(void) { + return _stats.num_compact; + } + + inline unsigned num_mem_enlarges(void) { return + _stats.num_enlarge; + } + + // functions + unsigned estimate_mem_usage(void); + + unsigned mem_usage(void); + + inline void set_variable_number(int n) { + variables()->resize(n + 1); + } + + inline int add_variable(void) { + variables()->resize(variables()->size() + 1); + return variables()->size() - 1; + } + + // dump functions + void detail_dump_cl(ClauseIdx cl_idx, ostream & os = cout); + + void dump(ostream & os = cout); + + friend ostream & operator << (ostream & os, CDatabase & db) { + db.dump(os); + return os; + } +}; +#endif Index: /vis_dev/zchaff/zchaff_header.h =================================================================== --- /vis_dev/zchaff/zchaff_header.h (revision 10) +++ /vis_dev/zchaff/zchaff_header.h (revision 10) @@ -0,0 +1,75 @@ +// ********************************************************************* +// Copyright 2000-2004, Princeton University. All rights reserved. +// By using this software the USER indicates that he or she has read, +// understood and will comply with the following: +// +// --- Princeton University hereby grants USER nonexclusive permission +// to use, copy and/or modify this software for internal, noncommercial, +// research purposes only. Any distribution, including commercial sale +// or license, of this software, copies of the software, its associated +// documentation and/or modifications of either is strictly prohibited +// without the prior consent of Princeton University. Title to copyright +// to this software and its associated documentation shall at all times +// remain with Princeton University. Appropriate copyright notice shall +// be placed on all software copies, and a complete copy of this notice +// shall be included in all copies of the associated documentation. +// No right is granted to use in advertising, publicity or otherwise +// any trademark, service mark, or the name of Princeton University. +// +// +// --- This software and any associated documentation is provided "as is" +// +// PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS +// OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A +// PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR +// ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, +// TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. +// +// Princeton University shall not be liable under any circumstances for +// any direct, indirect, special, incidental, or consequential damages +// with respect to any claim by USER or any third party on account of +// or arising from the use, or inability to use, this software or its +// associated documentation, even if Princeton University has been advised +// of the possibility of those damages. +// ********************************************************************* + +#ifndef __ZCHAFF_INCLUDE__ +#define __ZCHAFF_INCLUDE__ + +#define WORD_SIZE 4 +// #define WORD_SIZE 8 + +extern int _global_debug_level; +extern int _global_check_level; + +#ifndef __FUNCTION__ +# define __FUNCTION__ ((char*)0) +#endif + +#ifndef __FILE__ +# define __FILE__ 0 +#endif + +#ifndef __LINE__ +# define __LINE__ 0 +#endif + +#define _POSITION_ __FUNCTION__, __FILE__, __LINE__ + +#if WORD_SIZE == 4 +#define WORD_WIDTH 32 +typedef unsigned uint32; +typedef int int32; +typedef long long long64; +#elif WORD_SIZE == 8 +#define WORD_WIDTH 64 +typedef unsigned int uint32; +typedef int int32; +typedef long long64; +#endif + +void fatal(const char * fun, const char * file, int lineno, const char * fmt, ...); +void warning(const char * fun, const char * file, int lineno, const char * fmt, ...); +double get_cpu_time(void); + +#endif Index: /vis_dev/zchaff/zchaff_solver.cpp =================================================================== --- /vis_dev/zchaff/zchaff_solver.cpp (revision 10) +++ /vis_dev/zchaff/zchaff_solver.cpp (revision 10) @@ -0,0 +1,1528 @@ +// ********************************************************************* +// Copyright 2000-2004, Princeton University. All rights reserved. +// By using this software the USER indicates that he or she has read, +// understood and will comply with the following: +// +// --- Princeton University hereby grants USER nonexclusive permission +// to use, copy and/or modify this software for internal, noncommercial, +// research purposes only. Any distribution, including commercial sale +// or license, of this software, copies of the software, its associated +// documentation and/or modifications of either is strictly prohibited +// without the prior consent of Princeton University. Title to copyright +// to this software and its associated documentation shall at all times +// remain with Princeton University. Appropriate copyright notice shall +// be placed on all software copies, and a complete copy of this notice +// shall be included in all copies of the associated documentation. +// No right is granted to use in advertising, publicity or otherwise +// any trademark, service mark, or the name of Princeton University. +// +// +// --- This software and any associated documentation is provided "as is" +// +// PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS +// OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A +// PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR +// ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, +// TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. +// +// Princeton University shall not be liable under any circumstances for +// any direct, indirect, special, incidental, or consequential damages +// with respect to any claim by USER or any third party on account of +// or arising from the use, or inability to use, this software or its +// associated documentation, even if Princeton University has been advised +// of the possibility of those damages. +// ******************************************************************** + +#include +#include +#include +#include +#include +#include +#include + +using namespace std; + +#include "zchaff_solver.h" + +// #define VERIFY_ON + +#ifdef VERIFY_ON +ofstream verify_out("resolve_trace"); +#endif + +void CSolver::re_init_stats(void) { + _stats.is_mem_out = false; + _stats.outcome = UNDETERMINED; + _stats.next_restart = _params.restart.first_restart; + _stats.restart_incr = _params.restart.backtrack_incr; + _stats.next_cls_deletion = _params.cls_deletion.interval; + _stats.next_var_score_decay = _params.decision.decay_period; + _stats.current_randomness = _params.decision.base_randomness; + + _stats.total_bubble_move = 0; + _stats.num_decisions = 0; + _stats.num_decisions_stack_conf = 0; + _stats.num_decisions_vsids = 0; + _stats.num_decisions_shrinking = 0; + _stats.num_backtracks = 0; + _stats.max_dlevel = 0; + _stats.num_implications = 0; + _stats.num_restarts = 0; + _stats.num_del_orig_cls = 0; + _stats.num_shrinkings = 0; + _stats.start_cpu_time = get_cpu_time(); + _stats.finish_cpu_time = 0; + _stats.random_seed = 0; +} + +void CSolver::init_stats(void) { + re_init_stats(); + + _stats.been_reset = true; + _stats.num_free_variables = 0; + _stats.num_free_branch_vars = 0; +} + +void CSolver::init_parameters(void) { + _params.verbosity = 0; + _params.time_limit = 3600 * 24; // a day + _params.shrinking.size = 95; + _params.shrinking.enable = true; + _params.shrinking.upper_bound = 800; + _params.shrinking.lower_bound = 600; + _params.shrinking.upper_delta = -5; + _params.shrinking.lower_delta = 10; + _params.shrinking.window_width = 20; + _params.shrinking.bound_update_frequency = 20; + + _params.decision.base_randomness = 0; + _params.decision.decay_period = 40; + _params.decision.bubble_init_step = 0x400; + + _params.cls_deletion.enable = true ; + _params.cls_deletion.head_activity = 500; + _params.cls_deletion.tail_activity = 10; + _params.cls_deletion.head_num_lits = 6; + _params.cls_deletion.tail_num_lits = 45; + _params.cls_deletion.tail_vs_head = 16; + _params.cls_deletion.interval = 600; + + _params.restart.enable = true; + _params.restart.interval = 700; + _params.restart.first_restart = 7000; + _params.restart.backtrack_incr = 700; +} + +CSolver::CSolver(void) { + init_parameters(); + init_stats(); + _dlevel = 0; + _force_terminate = false; + _implication_id = 0; + _num_marked = 0; + _num_in_new_cl = 0; + _outside_constraint_hook = NULL; + _sat_hook = NULL; +} + +CSolver::~CSolver(void) { + while (!_assignment_stack.empty()) { + delete _assignment_stack.back(); + _assignment_stack.pop_back(); + } +} + +void CSolver::set_time_limit(float t) { + _params.time_limit = t; +} + +float CSolver::elapsed_cpu_time(void) { + return get_cpu_time() - _stats.start_cpu_time; +} + +float CSolver::cpu_run_time(void) { + return (_stats.finish_cpu_time - _stats.start_cpu_time); +} + +void CSolver::set_variable_number(int n) { + assert(num_variables() == 0); + CDatabase::set_variable_number(n); + _stats.num_free_variables = num_variables(); + while (_assignment_stack.size() <= num_variables()) + _assignment_stack.push_back(new vector); + assert(_assignment_stack.size() == num_variables() + 1); +} + +int CSolver::add_variable(void) { + int num = CDatabase::add_variable(); + ++_stats.num_free_variables; + while (_assignment_stack.size() <= num_variables()) + _assignment_stack.push_back(new vector); + assert(_assignment_stack.size() == num_variables() + 1); + return num; +} + +void CSolver::set_mem_limit(int s) { + CDatabase::set_mem_limit(s); +} + +void CSolver::set_randomness(int n) { + _params.decision.base_randomness = n; +} + +void CSolver::set_random_seed(int seed) { + srand(seed); +} + +void CSolver::enable_cls_deletion(bool allow) { + _params.cls_deletion.enable = allow; +} + +void CSolver::add_hook(HookFunPtrT fun, int interval) { + pair a(fun, interval); + _hooks.push_back(pair > (0, a)); +} + +void CSolver::run_periodic_functions(void) { + // a. restart + if (_params.restart.enable && _stats.num_backtracks > _stats.next_restart && + _shrinking_cls.empty()) { + _stats.next_restart = _stats.num_backtracks + _stats.restart_incr; + delete_unrelevant_clauses(); + restart(); + if (_stats.num_restarts % 5 == 1) + compact_lit_pool(); + cout << "\rDecision: " << _assignment_stack[0]->size() << "/" + < _stats.next_var_score_decay) { + _stats.next_var_score_decay = _stats.num_backtracks + + _params.decision.decay_period; + decay_variable_score(); + } + + // c. run hook functions + for (unsigned i = 0; i< _hooks.size(); ++i) { + pair > & hook = _hooks[i]; + if (_stats.num_decisions >= hook.first) { + hook.first += hook.second.second; + hook.second.first((void *) this); + } + } +} + +void CSolver::init_solve(void) { + CDatabase::init_stats(); + re_init_stats(); + _stats.been_reset = false; + + assert(_conflicts.empty()); + assert(_conflict_lits.empty()); + assert(_num_marked == 0); + assert(_num_in_new_cl == 0); + assert(_dlevel == 0); + + for (unsigned i = 0, sz = variables()->size(); i < sz; ++i) { + variable(i).score(0) = variable(i).lits_count(0); + variable(i).score(1) = variable(i).lits_count(1); + } + + _ordered_vars.resize(num_variables()); + update_var_score(); + + set_random_seed(_stats.random_seed); + + top_unsat_cls = clauses()->size() - 1; + + _stats.shrinking_benefit = 0; + _shrinking_cls.clear(); + _stats.shrinking_cls_length = 0; +} + +void CSolver::set_var_value(int v, int value, ClauseIdx ante, int dl) { + assert(value == 0 || value == 1); + CVariable & var = variable(v); + assert(var.value() == UNKNOWN); + assert(dl == dlevel()); + + var.set_dlevel(dl); + var.set_value(value); + var.antecedent() = ante; + var.assgn_stack_pos() = _assignment_stack[dl]->size(); + _assignment_stack[dl]->push_back(v * 2 + !value); + set_var_value_BCP(v, value); + + ++_stats.num_implications ; + if (var.is_branchable()) + --num_free_variables(); +} + +void CSolver::set_var_value_BCP(int v, int value) { + vector & watchs = variable(v).watched(value); + for (vector ::iterator itr = watchs.begin(); + itr != watchs.end(); ++itr) { + ClauseIdx cl_idx; + CLitPoolElement * other_watched = *itr; + CLitPoolElement * watched = *itr; + int dir = watched->direction(); + CLitPoolElement * ptr = watched; + while (true) { + ptr += dir; + if (ptr->val() <= 0) { // reached one end of the clause + if (dir == 1) // reached the right end, i.e. spacing element is cl_id + cl_idx = ptr->get_clause_index(); + if (dir == watched->direction()) { // we haven't go both directions. + ptr = watched; + dir = -dir; // change direction, go the other way + continue; + } + // otherwise, we have already go through the whole clause + int the_value = literal_value(*other_watched); + if (the_value == 0) // a conflict + _conflicts.push_back(cl_idx); + else if (the_value != 1) // i.e. unknown + queue_implication(other_watched->s_var(), cl_idx); + break; + } + if (ptr->is_watched()) { // literal is the other watched lit, skip it. + other_watched = ptr; + continue; + } + if (literal_value(*ptr) == 0) // literal value is 0, keep going + continue; + // now the literal's value is either 1 or unknown, watch it instead + int v1 = ptr->var_index(); + int sign = ptr->var_sign(); + variable(v1).watched(sign).push_back(ptr); + ptr->set_watch(dir); + // remove the original watched literal from watched list + watched->unwatch(); + *itr = watchs.back(); // copy the last element in it's place + watchs.pop_back(); // remove the last element + --itr; // do this so with don't skip one during traversal + break; + } + } +} + +void CSolver::unset_var_value(int v) { + if (v == 0) + return; + CVariable & var = variable(v); + var.set_value(UNKNOWN); + var.set_antecedent(NULL_CLAUSE); + var.set_dlevel(-1); + var.assgn_stack_pos() = -1; + + if (var.is_branchable()) { + ++num_free_variables(); + if (var.var_score_pos() < _max_score_pos) + _max_score_pos = var.var_score_pos(); + } +} + +void CSolver::dump_assignment_stack(ostream & os ) { + os << "Assignment Stack: "; + for (int i = 0; i <= dlevel(); ++i) { + os << "(" <> 1) << " "; + } + os << ") " << endl; + } + os << endl; +} + +void CSolver::dump_implication_queue(ostream & os) { + _implication_queue.dump(os); +} + +void CSolver::delete_clause_group(int gid) { + assert(is_gid_allocated(gid)); + + if (_stats.been_reset == false) + reset(); // if delete some clause, then implication queue are invalidated + + for (vector::iterator itr = clauses()->begin(); + itr != clauses()->end(); ++itr) { + CClause & cl = *itr; + if (cl.status() != DELETED_CL) { + if (cl.gid(gid) == true) { + mark_clause_deleted(cl); + } + } + } + + // delete the index from variables + for (vector::iterator itr = variables()->begin(); + itr != variables()->end(); ++itr) { + for (unsigned i = 0; i < 2; ++i) { // for each phase + // delete the lit index from the vars +#ifdef KEEP_LIT_CLAUSES + vector & lit_clauses = (*itr).lit_clause(i); + for (vector::iterator itr1 = lit_clauses.begin(); + itr1 != lit_clauses.end(); ++itr1) { + if (clause(*itr1).status() == DELETED_CL) { + *itr1 = lit_clauses.back(); + lit_clauses.pop_back(); + --itr1; + } + } +#endif + // delete the watched index from the vars + vector & watched = (*itr).watched(i); + for (vector::iterator itr1 = watched.begin(); + itr1 != watched.end(); ++itr1) { + if ((*itr1)->val() <= 0) { + *itr1 = watched.back(); + watched.pop_back(); + --itr1; + } + } + } + } + free_gid(gid); +} + +void CSolver::reset(void) { + if (_stats.been_reset) + return; + if (num_variables() == 0) + return; + back_track(0); + _conflicts.clear(); + while (!_implication_queue.empty()) + _implication_queue.pop(); + + _stats.outcome = UNDETERMINED; + _stats.been_reset = true; +} + +void CSolver::delete_unrelevant_clauses(void) { + unsigned original_del_cls = num_deleted_clauses(); + int num_conf_cls = num_clauses() - init_num_clauses() + num_del_orig_cls(); + int head_count = num_conf_cls / _params.cls_deletion.tail_vs_head; + int count = 0; + for (vector::iterator itr = clauses()->begin(); + itr != clauses()->end() - 1; ++itr) { + CClause & cl = *itr; + if (cl.status() != CONFLICT_CL) { + continue; + } + bool cls_sat_at_dl_0 = false; + for (int i = 0, sz = cl.num_lits(); i < sz; ++i) { + if (literal_value(cl.literal(i)) == 1 && + variable(cl.literal(i).var_index()).dlevel() == 0) { + cls_sat_at_dl_0 = true; + break; + } + } + if (cls_sat_at_dl_0) { + int val_0_lits = 0, val_1_lits = 0, unknown_lits = 0; + for (unsigned i = 0; i < cl.num_lits(); ++i) { + int lit_value = literal_value(cl.literal(i)); + if (lit_value == 0) + ++val_0_lits; + if (lit_value == 1) + ++val_1_lits; + if (lit_value == UNKNOWN) + ++unknown_lits; + if (unknown_lits + val_1_lits > 1) { + mark_clause_deleted(cl); + break; + } + } + continue; + } + + count++; + int max_activity = _params.cls_deletion.head_activity - + (_params.cls_deletion.head_activity - + _params.cls_deletion.tail_activity) * + count/num_conf_cls; + int max_conf_cls_size; + + if (head_count > 0) { + max_conf_cls_size = _params.cls_deletion.head_num_lits; + --head_count; + } else { + max_conf_cls_size = _params.cls_deletion.tail_num_lits; + } + + if (cl.activity() > max_activity) + continue; + + int val_0_lits = 0, val_1_lits = 0, unknown_lits = 0, lit_value; + for (unsigned i = 0; i < cl.num_lits(); ++i) { + lit_value = literal_value(cl.literal(i)); + if (lit_value == 0) + ++val_0_lits; + else if (lit_value == 1) + ++val_1_lits; + else + ++unknown_lits; + if ((unknown_lits > max_conf_cls_size)) { + mark_clause_deleted(cl); + break; + } + } + } + + // if none were recently marked for deletion... + if (original_del_cls == num_deleted_clauses()) + return; + + // delete the index from variables + for (vector::iterator itr = variables()->begin(); + itr != variables()->end(); ++itr) { + for (unsigned i = 0; i < 2; ++i) { // for each phase + // delete the lit index from the vars +#ifdef KEEP_LIT_CLAUSES + vector & lit_clauses = (*itr).lit_clause(i); + for (vector::iterator itr1 = lit_clauses.begin(); + itr1 != lit_clauses.end(); ++itr1) { + if (clause(*itr1).status() == DELETED_CL) { + *itr1 = lit_clauses.back(); + lit_clauses.pop_back(); + --itr1; + } + } +#endif + // delete the watched index from the vars + vector & watched = (*itr).watched(i); + for (vector::iterator itr1 = watched.begin(); + itr1 != watched.end(); ++itr1) { + if ((*itr1)->val() <= 0) { + *itr1 = watched.back(); + watched.pop_back(); + --itr1; + } + } + } + } + + for (unsigned i = 1, sz = variables()->size(); i < sz; ++i) { + if (variable(i).dlevel() != 0) { + variable(i).score(0) = variable(i).lits_count(0); + variable(i).score(1) = variable(i).lits_count(1); + if (variable(i).lits_count(0) == 0 && variable(i).value() == UNKNOWN) { + queue_implication(i * 2 + 1, NULL_CLAUSE); + } + else if (variable(i).lits_count(1) == 0 && + variable(i).value() == UNKNOWN) { + queue_implication(i * 2, NULL_CLAUSE); + } + } else { + variable(i).score(0) = 0; + variable(i).score(1) = 0; + } + } + update_var_score(); +} + +bool CSolver::time_out(void) { + return (get_cpu_time() - _stats.start_cpu_time> _params.time_limit); +} + +void CSolver::adjust_variable_order(int * lits, int n_lits) { + // note lits are signed vars, not CLitPoolElements + for (int i = 0; i < n_lits; ++i) { + int var_idx = lits[i] >> 1; + CVariable & var = variable(var_idx); + assert(var.value() != UNKNOWN); + int orig_score = var.score(); + ++variable(var_idx).score(lits[i] & 0x1); + int new_score = var.score(); + if (orig_score == new_score) + continue; + int pos = var.var_score_pos(); + int orig_pos = pos; + assert(_ordered_vars[pos].first == & var); + assert(_ordered_vars[pos].second == orig_score); + int bubble_step = _params.decision.bubble_init_step; + for (pos = orig_pos ; pos >= 0; pos -= bubble_step) { + if (_ordered_vars[pos].second >= new_score) + break; + } + pos += bubble_step; + for (bubble_step = bubble_step >> 1; bubble_step > 0; + bubble_step = bubble_step >> 1) { + if (pos - bubble_step >= 0 && + _ordered_vars[pos - bubble_step].second < new_score) + pos -= bubble_step; + } + // now found the position, do a swap + _ordered_vars[orig_pos] = _ordered_vars[pos]; + _ordered_vars[orig_pos].first->set_var_score_pos(orig_pos); + _ordered_vars[pos].first = & var; + _ordered_vars[pos].second = new_score; + _ordered_vars[pos].first->set_var_score_pos(pos); + _stats.total_bubble_move += orig_pos - pos; + } +} + +void CSolver::decay_variable_score(void) { + unsigned i, sz; + for (i = 1, sz = variables()->size(); i < sz; ++i) { + CVariable & var = variable(i); + var.score(0) /= 2; + var.score(1) /= 2; + } + for (i = 0, sz = _ordered_vars.size(); i < sz; ++i) { + _ordered_vars[i].second = _ordered_vars[i].first->score(); + } +} + +bool CSolver::decide_next_branch(void) { + if (dlevel() > 0) + assert(_assignment_stack[dlevel()]->size() > 0); + if (!_implication_queue.empty()) { + // some hook function did a decision, so skip my own decision making. + // if the front of implication queue is 0, that means it's finished + // because var index start from 1, so 2 *vid + sign won't be 0. + // else it's a valid decision. + return (_implication_queue.front().lit != 0); + } + int s_var = 0; + if (_params.shrinking.enable) { + while (!_shrinking_cls.empty()) { + s_var = _shrinking_cls.begin()->second; + _shrinking_cls.erase(_shrinking_cls.begin()); + if (variable(s_var >> 1).value() == UNKNOWN) { + _stats.num_decisions++; + _stats.num_decisions_shrinking++; + ++dlevel(); + queue_implication(s_var ^ 0x1, NULL_CLAUSE); + return true; + } + } + } + + if (_outside_constraint_hook != NULL) + _outside_constraint_hook(this); + + if (!_implication_queue.empty()) + return (_implication_queue.front().lit != 0); + + ++_stats.num_decisions; + if (num_free_variables() == 0) // no more free vars + return false; + + bool cls_sat = true; + int i, sz, var_idx, score, max_score = -1; + + for (; clause(top_unsat_cls).status() != ORIGINAL_CL; --top_unsat_cls) { + CClause &cl=clause(top_unsat_cls); + if (cl.status() != CONFLICT_CL) + continue; + cls_sat = false; + if (cl.sat_lit_idx() < (int)cl.num_lits() && + literal_value(cl.literal(cl.sat_lit_idx())) == 1) + cls_sat = true; + if (!cls_sat) { + max_score = -1; + for (i = 0, sz = cl.num_lits(); i < sz; ++i) { + var_idx = cl.literal(i).var_index(); + if (literal_value(cl.literal(i)) == 1) { + cls_sat = true; + cl.sat_lit_idx() = i; + break; + } + else if (variable(var_idx).value() == UNKNOWN) { + score = variable(var_idx).score(); + if (score > max_score) { + max_score = score; + s_var = var_idx * 2; + } + } + } + } + if (!cls_sat) + break; + } + if (!cls_sat && max_score != -1) { + ++dlevel(); + if (dlevel() > _stats.max_dlevel) + _stats.max_dlevel = dlevel(); + CVariable& v = variable(s_var >> 1); + if (v.score(0) < v.score(1)) + s_var += 1; + else if (v.score(0) == v.score(1)) { + if (v.two_lits_count(0) > v.two_lits_count(1)) + s_var+=1; + else if (v.two_lits_count(0) == v.two_lits_count(1)) + s_var+=rand()%2; + } + assert(s_var >= 2); + queue_implication(s_var, NULL_CLAUSE); + ++_stats.num_decisions_stack_conf; + return true; + } + + for (unsigned i = _max_score_pos; i < _ordered_vars.size(); ++i) { + CVariable & var = *_ordered_vars[i].first; + if (var.value() == UNKNOWN && var.is_branchable()) { + // move th max score position pointer + _max_score_pos = i; + // make some randomness happen + if (--_stats.current_randomness < _params.decision.base_randomness) + _stats.current_randomness = _params.decision.base_randomness; + int randomness = _stats.current_randomness; + if (randomness >= num_free_variables()) + randomness = num_free_variables() - 1; + int skip = rand() % (1 + randomness); + int index = i; + while (skip > 0) { + ++index; + if (_ordered_vars[index].first->value() == UNKNOWN && + _ordered_vars[index].first->is_branchable()) + --skip; + } + CVariable * ptr = _ordered_vars[index].first; + assert(ptr->value() == UNKNOWN && ptr->is_branchable()); + int sign = 0; + if (ptr->score(0) < ptr->score(1)) + sign += 1; + else if (ptr->score(0) == ptr->score(1)) { + if (ptr->two_lits_count(0) > ptr->two_lits_count(1)) + sign += 1; + else if (ptr->two_lits_count(0) == ptr->two_lits_count(1)) + sign += rand() % 2; + } + int var_idx = ptr - &(*variables()->begin()); + s_var = var_idx + var_idx + sign; + break; + } + } + assert(s_var >= 2); // there must be a free var somewhere + ++dlevel(); + if (dlevel() > _stats.max_dlevel) + _stats.max_dlevel = dlevel(); + ++_stats.num_decisions_vsids; + _implication_id = 0; + queue_implication(s_var, NULL_CLAUSE); + return true; +} + +int CSolver::preprocess(void) { + assert(dlevel() == 0); + + // 1. detect all the unused variables + vector un_used; + for (unsigned i = 1, sz = variables()->size(); i < sz; ++i) { + CVariable & v = variable(i); + if (v.lits_count(0) == 0 && v.lits_count(1) == 0) { + un_used.push_back(i); + queue_implication(i+i, NULL_CLAUSE); + int r = deduce(); + assert(r == NO_CONFLICT); + } + } + if (_params.verbosity > 1 && un_used.size() > 0) { + cout << un_used.size() << " Variables are defined but not used " << endl; + if (_params.verbosity > 2) { + for (unsigned i = 0; i< un_used.size(); ++i) + cout << un_used[i] << " "; + cout << endl; + } + } + + // 2. detect all variables with only one phase occuring (i.e. pure literals) + vector uni_phased; + for (unsigned i = 1, sz = variables()->size(); i < sz; ++i) { + CVariable & v = variable(i); + if (v.value() != UNKNOWN) + continue; + if (v.lits_count(0) == 0) { // no positive phased lits. + queue_implication(i+i+1, NULL_CLAUSE); + uni_phased.push_back(-i); + } + else if (v.lits_count(1) == 0) { // no negative phased lits. + queue_implication(i+i, NULL_CLAUSE); + uni_phased.push_back(i); + } + } + if (_params.verbosity > 1 && uni_phased.size() > 0) { + cout << uni_phased.size() << " Variables only appear in one phase." < 2) { + for (unsigned i = 0; i< uni_phased.size(); ++i) + cout << uni_phased[i] << " "; + cout <size(); i < sz; ++i) { + if (clause(i).status() != DELETED_CL && + clause(i).num_lits() == 1 && + variable(clause(i).literal(0).var_index()).value() == UNKNOWN) + queue_implication(clause(i).literal(0).s_var(), i); + } + + if (deduce() == CONFLICT) { + cout << " CONFLICT during preprocess " <size(); ++i) { + if (variable(i).value() != UNKNOWN) { + assert(variable(i).dlevel() <= 0); + int ante = variable(i).antecedent(); + int ante_id = 0; + if (ante >= 0) { + ante_id = clause(ante).id(); + verify_out << "VAR: " << i + << " L: " << variable(i).assgn_stack_pos() + << " V: " << variable(i).value() + << " A: " << ante_id + << " Lits:"; + for (unsigned j = 0; j < clause(ante).num_lits(); ++j) + verify_out <<" " << clause(ante).literal(j).s_var(); + verify_out << endl; + } + } + } + verify_out << "CONF: " << clause(_conflicts[0]).id() << " =="; + for (unsigned i = 0; i < clause(_conflicts[0]).num_lits(); ++i) { + int svar = clause(_conflicts[0]).literal(i).s_var(); + verify_out << " " << svar; + } + verify_out << endl; +#endif + return CONFLICT; + } + if (_params.verbosity > 1) { + cout << _assignment_stack[0]->size() << " vars set during preprocess; " + << endl; + } + return NO_CONFLICT; +} + +void CSolver::mark_var_unbranchable(int vid) { + if (variable(vid).is_branchable()) { + variable(vid).disable_branch(); + if (variable(vid).value() == UNKNOWN) + --num_free_variables(); + } +} + +void CSolver::mark_var_branchable(int vid) { + CVariable & var = variable(vid); + if (!var.is_branchable()) { + var.enable_branch(); + if (var.value() == UNKNOWN) { + ++num_free_variables(); + if (var.var_score_pos() < _max_score_pos) + _max_score_pos = var.var_score_pos(); + } + } +} + +ClauseIdx CSolver::add_orig_clause(int * lits, int n_lits, int gid) { + int cid = add_clause_with_gid(lits, n_lits, gid); + if (cid >= 0) { + clause(cid).set_status(ORIGINAL_CL); + clause(cid).activity() = 0; + } + return cid; +} + +ClauseIdx CSolver::add_clause_with_gid(int * lits, int n_lits, int gid) { + unsigned gflag; + if (gid == PERMANENT_GID ) + gflag = 0; + else if (gid == VOLATILE_GID) { + gflag = (~0x0); + } else { + assert(gid <= WORD_WIDTH && gid > 0); + gflag = (1 << (gid- 1)); + } + ClauseIdx cid = add_clause(lits, n_lits, gflag); + if (cid < 0) { + _stats.is_mem_out = true; + _stats.outcome = MEM_OUT; + } + return cid; +} + +ClauseIdx CSolver::add_conflict_clause(int * lits, int n_lits, int gflag) { + ClauseIdx cid = add_clause(lits, n_lits, gflag); + if (cid >= 0) { + clause(cid).set_status(CONFLICT_CL); + clause(cid).activity() = 0; + } else { + _stats.is_mem_out = true; + _stats.outcome = MEM_OUT; + } + return cid; +} + +void CSolver::real_solve(void) { + while (_stats.outcome == UNDETERMINED) { + run_periodic_functions(); + if (decide_next_branch()) { + while (deduce() == CONFLICT) { + int blevel; + blevel = analyze_conflicts(); + if (blevel < 0) { + _stats.outcome = UNSATISFIABLE; + return; + } + } + } else { + if (_sat_hook != NULL && _sat_hook(this)) + continue; + _stats.outcome = SATISFIABLE; + return; + } + if (time_out()) { + _stats.outcome = TIME_OUT; + return; + } + if (_force_terminate) { + _stats.outcome = ABORTED; + return; + } + if (_stats.is_mem_out) { + _stats.outcome = MEM_OUT; + return; + } + } +} + +int CSolver::solve(void) { + if (_stats.outcome == UNDETERMINED) { + init_solve(); + + if (preprocess() == CONFLICT) + _stats.outcome = UNSATISFIABLE; + else // the real search + real_solve(); + cout << endl; + _stats.finish_cpu_time = get_cpu_time(); + } + return _stats.outcome; +} + +void CSolver::back_track(int blevel) { + assert(blevel <= dlevel()); + for (int i = dlevel(); i >= blevel; --i) { + vector & assignments = *_assignment_stack[i]; + for (int j = assignments.size() - 1 ; j >= 0; --j) + unset_var_value(assignments[j]>>1); + assignments.clear(); + } + dlevel() = blevel - 1; + if (dlevel() < 0 ) + dlevel() = 0; + ++_stats.num_backtracks; +} + +int CSolver::deduce(void) { + while (!_implication_queue.empty()) { + const CImplication & imp = _implication_queue.front(); + int lit = imp.lit; + int vid = lit>>1; + ClauseIdx cl = imp.antecedent; + _implication_queue.pop(); + CVariable & var = variable(vid); + if (var.value() == UNKNOWN) { // an implication + set_var_value(vid, !(lit & 0x1), cl, dlevel()); + } + else if (var.value() == (unsigned)(lit & 0x1)) { + // a conflict + // note: literal & 0x1 == 1 means the literal is in negative phase + // when a conflict occure at not current dlevel, we need to backtrack + // to resolve the problem. + // conflict analysis will only work if the conflict occure at + // the top level (current dlevel) + _conflicts.push_back(cl); + break; + } else { + // so the variable have been assigned before + // update its antecedent with a shorter one + if (var.antecedent() != NULL_CLAUSE && + clause(cl).num_lits() < clause(var.antecedent()).num_lits()) + var.antecedent() = cl; + assert(var.dlevel() <= dlevel()); + } + } + // if loop exited because of a conflict, we need to clean implication queue + while (!_implication_queue.empty()) + _implication_queue.pop(); + return (_conflicts.size() ? CONFLICT : NO_CONFLICT); +} + +void CSolver::verify_integrity(void) { + for (unsigned i = 1; i < variables()->size(); ++i) { + if (variable(i).value() != UNKNOWN) { + int pos = variable(i).assgn_stack_pos(); + int value = variable(i).value(); + int dlevel = variable(i).dlevel(); + assert((*_assignment_stack[dlevel])[pos] == (int) (i+i+1-value)); + } + } + for (unsigned i = 0; i < clauses()->size(); ++i) { + if (clause(i).status() == DELETED_CL) + continue; + CClause & cl = clause(i); + int num_0 = 0; + int num_1 = 0; + int num_unknown = 0; + int watched[2]; + int watch_index = 0; + watched[1] = watched[0] = 0; + for (unsigned j = 0; j < cl.num_lits(); ++j) { + CLitPoolElement lit = cl.literal(j); + int vid = lit.var_index(); + if (variable(vid).value() == UNKNOWN) { + ++num_unknown; + } else { + if (literal_value(lit) == 0) + ++num_0; + else + ++num_1; + } + if (lit.is_watched()) { + watched[watch_index] = lit.s_var(); + ++watch_index; + } + } + if (watch_index == 0) { + assert(cl.num_lits() == 1); + continue; + } + assert(watch_index == 2); + for (unsigned j = 0; j < cl.num_lits(); ++j) { + CLitPoolElement lit = cl.literal(j); + int vid1 = (watched[0]>>1); + if (variable(vid1).value() == (unsigned)(watched[0] & 0x1)) { + if (!lit.is_watched()) { + assert(literal_value(lit) == 0); + assert(variable(lit.var_index()).dlevel() <= + variable(vid1).dlevel()); + } + } + int vid2 = (watched[1]>>1); + if (variable(vid2).value() == (unsigned)(watched[1] & 0x1)) { + if (!lit.is_watched()) { + assert(literal_value(lit) == 0); + assert(variable(lit.var_index()).dlevel() <= + variable(vid1).dlevel()); + } + } + } + } +} + +void CSolver::mark_vars(ClauseIdx cl, int var_idx) { + assert(_resolvents.empty() || var_idx != -1); +#ifdef VERIFY_ON + _resolvents.push_back(clause(cl).id()); +#endif + for (CLitPoolElement* itr = clause(cl).literals(); (*itr).val() > 0; ++itr) { + int v = (*itr).var_index(); + if (v == var_idx) + continue; + else if (variable(v).dlevel() == dlevel()) { + if (!variable(v).is_marked()) { + variable(v).set_marked(); + ++_num_marked; + if (_mark_increase_score) { + int tmp = itr->s_var(); + adjust_variable_order(&tmp, 1); + } + } + } else { + assert(variable(v).dlevel() < dlevel()); + if (variable(v).new_cl_phase() == UNKNOWN) { // it's not in the new cl + // We can remove the variable assigned at dlevel 0 if + // we are nog going to use incremental SAT. + // if(variable(v).dlevel()){ + ++_num_in_new_cl; + variable(v).set_new_cl_phase((*itr).var_sign()); + _conflict_lits.push_back((*itr).s_var()); + // } + } else { + // if this variable is already in the new clause, it must + // have the same phase + assert(variable(v).new_cl_phase() == (*itr).var_sign()); + } + } + } +} + +int CSolver::analyze_conflicts(void) { + assert(!_conflicts.empty()); + assert(_conflict_lits.size() == 0); + assert(_implication_queue.empty()); + assert(_num_marked == 0); + if (dlevel() == 0) { // already at level 0. Conflict means unsat. +#ifdef VERIFY_ON + for (unsigned i = 1; i < variables()->size(); ++i) { + if (variable(i).value() != UNKNOWN) { + assert(variable(i).dlevel() <= 0); + int ante = variable(i).antecedent(); + int ante_id = 0; + if (ante >= 0) { + ante_id = clause(ante).id(); + assert(clause(ante).status() != DELETED_CL); + verify_out << "VAR: " << i + << " L: " << variable(i).assgn_stack_pos() + << " V: " << variable(i).value() + << " A: " << ante_id + << " Lits:"; + for (unsigned j = 0; j < clause(ante).num_lits(); ++j) + verify_out << " " << clause(ante).literal(j).s_var(); + verify_out << endl; + } + } + } + ClauseIdx shortest; + shortest = _conflicts.back(); + unsigned len = clause(_conflicts.back()).num_lits(); + while (!_conflicts.empty()) { + if (clause(_conflicts.back()).num_lits() < len) { + shortest = _conflicts.back(); + len = clause(_conflicts.back()).num_lits(); + } + _conflicts.pop_back(); + } + verify_out << "CONF: " << clause(shortest).id() << " =="; + for (unsigned i = 0; i < clause(shortest).num_lits(); ++i) { + int svar = clause(shortest).literal(i).s_var(); + verify_out << " " << svar; + } + verify_out << endl; +#endif + _conflicts.clear(); + back_track(0); + return -1; + } + return conflict_analysis_firstUIP(); +} + +// when all the literals involved are in _conflict_lits +// call this function to finish the adding clause and backtrack + +int CSolver::finish_add_conf_clause(int gflag) { + ClauseIdx added_cl = add_conflict_clause(&(*_conflict_lits.begin()), + _conflict_lits.size(), gflag); + if (added_cl < 0) { // memory out. + _stats.is_mem_out = true; + _conflicts.clear(); + assert(_implication_queue.empty()); + return 1; + } + + top_unsat_cls = clauses()->size() - 1; + +#ifdef VERIFY_ON + verify_out << "CL: " << clause(added_cl).id() << " <="; + for (unsigned i = 0; i< _resolvents.size(); ++i) + verify_out << " " << _resolvents[i]; + verify_out << endl; + _resolvents.clear(); +#endif + + adjust_variable_order(&(*_conflict_lits.begin()), _conflict_lits.size()); + + if (_params.shrinking.enable) { + _shrinking_cls.clear(); + if (_stats.shrinking_cls_length != 0) { + int benefit = _stats.shrinking_cls_length - _conflict_lits.size(); + _stats.shrinking_benefit += benefit; + _stats.shrinking_cls_length = 0; + _recent_shrinkings.push(benefit); + if (_recent_shrinkings.size() > _params.shrinking.window_width) { + _stats.shrinking_benefit -= _recent_shrinkings.front(); + _recent_shrinkings.pop(); + } + } + if (_conflict_lits.size() > _params.shrinking.size) { + _shrinking_cls.clear(); + for (unsigned i = 0, sz = _conflict_lits.size(); i < sz; ++i) { + _shrinking_cls.insert(pair + (variable(_conflict_lits[i]>>1).dlevel(), _conflict_lits[i])); + } + int prev_dl = _shrinking_cls.begin()->first; + multimap::iterator itr, itr_del; + int last_dl = _shrinking_cls.rbegin()->first; + + bool found_gap = false; + for (itr = _shrinking_cls.begin(); itr->first != last_dl;) { + if (itr->first - prev_dl > 2) { + found_gap = true; + break; + } + prev_dl = itr->first; + itr_del = itr; + ++itr; + _shrinking_cls.erase(itr_del); + } + if (found_gap && _shrinking_cls.size() > 0 && prev_dl < dlevel() - 1) { + _stats.shrinking_cls_length = _conflict_lits.size(); + ++_stats.num_shrinkings; + back_track(prev_dl + 1); + _conflicts.clear(); +#ifdef VERIFY_ON + _resolvents.clear(); +#endif + _num_in_new_cl = 0; + for (unsigned i = 0, sz = _conflict_lits.size(); i < sz; ++i) + variable(_conflict_lits[i]>>1).set_new_cl_phase(UNKNOWN); + _conflict_lits.clear(); + if (_stats.num_shrinkings % + _params.shrinking.bound_update_frequency == 0 && + _recent_shrinkings.size() == _params.shrinking.window_width) { + if (_stats.shrinking_benefit > _params.shrinking.upper_bound) + _params.shrinking.size += _params.shrinking.upper_delta; + else if (_stats.shrinking_benefit < _params.shrinking.lower_bound) + _params.shrinking.size += _params.shrinking.lower_delta; + } + return prev_dl; + } + } + } + int back_dl = 0; + int unit_lit = -1; + + for (unsigned i = 0; i < clause(added_cl).num_lits(); ++i) { + int vid = clause(added_cl).literal(i).var_index(); + int sign =clause(added_cl).literal(i).var_sign(); + assert(variable(vid).value() != UNKNOWN); + assert(literal_value(clause(added_cl).literal(i)) == 0); + int dl = variable(vid).dlevel(); + if (dl < dlevel()) { + if (dl > back_dl) + back_dl = dl; + } else { + assert(unit_lit == -1); + unit_lit = vid + vid + sign; + } + } + if (back_dl == 0) { + _stats.next_restart = _stats.num_backtracks + _stats.restart_incr; + _stats.next_cls_deletion = _stats.num_backtracks + + _params.cls_deletion.interval; + } + + back_track(back_dl + 1); + queue_implication(unit_lit, added_cl); + + // after resolve the first conflict, others must also be resolved + // for (unsigned i = 1; i < _conflicts.size(); ++i) + // assert(!is_conflicting(_conflicts[i])); + + _conflicts.clear(); + + while (!_conflict_lits.empty()) { + int svar = _conflict_lits.back(); + _conflict_lits.pop_back(); + CVariable & var = variable(svar >> 1); + assert(var.new_cl_phase() == (unsigned)(svar & 0x1)); + --_num_in_new_cl; + var.set_new_cl_phase(UNKNOWN); + } + assert(_num_in_new_cl == 0); + return back_dl; +} + +int CSolver::conflict_analysis_firstUIP(void) { + int min_conf_id = _conflicts[0]; + int min_conf_length = -1; + ClauseIdx cl; + unsigned gflag; + _mark_increase_score = false; + if (_conflicts.size() > 1) { + for (vector::iterator ci = _conflicts.begin(); + ci != _conflicts.end(); ci++) { + assert(_num_in_new_cl == 0); + assert(dlevel() > 0); + cl = *ci; + mark_vars(cl, -1); + // current dl must be the conflict cl. + vector & assignments = *_assignment_stack[dlevel()]; + // now add conflict lits, and unassign vars + for (int i = assignments.size() - 1; i >= 0; --i) { + int assigned = assignments[i]; + if (variable(assigned >> 1).is_marked()) { + // this variable is involved in the conflict clause or its antecedent + variable(assigned>>1).clear_marked(); + --_num_marked; + ClauseIdx ante_cl = variable(assigned>>1).get_antecedent(); + if ( _num_marked == 0 ) { + // the first UIP encountered, conclude add clause + assert(variable(assigned>>1).new_cl_phase() == UNKNOWN); + // add this assignment's reverse, e.g. UIP + _conflict_lits.push_back(assigned ^ 0x1); + ++_num_in_new_cl; + variable(assigned>>1).set_new_cl_phase((assigned^0x1)&0x1); + break; + } else { + assert(ante_cl != NULL_CLAUSE); + mark_vars(ante_cl, assigned >> 1); + } + } + } + if (min_conf_length == -1 || + (int)_conflict_lits.size() < min_conf_length) { + min_conf_length = _conflict_lits.size(); + min_conf_id = cl; + } + + for (vector::iterator vi = _conflict_lits.begin(); vi != + _conflict_lits.end(); ++vi) { + int s_var = *vi; + CVariable & var = variable(s_var >> 1); + assert(var.new_cl_phase() == (unsigned)(s_var & 0x1)); + var.set_new_cl_phase(UNKNOWN); + } + _num_in_new_cl = 0; + _conflict_lits.clear(); +#ifdef VERIFY_ON + _resolvents.clear(); +#endif + } + } + + assert(_num_marked == 0); + cl = min_conf_id; + clause(cl).activity() += 5; + _mark_increase_score = true; + mark_vars(cl, -1); + gflag = clause(cl).gflag(); + vector & assignments = *_assignment_stack[dlevel()]; + for (int i = assignments.size() - 1; i >= 0; --i) { + int assigned = assignments[i]; + if (variable(assigned >> 1).is_marked()) { + variable(assigned>>1).clear_marked(); + --_num_marked; + ClauseIdx ante_cl = variable(assigned>>1).get_antecedent(); + if ( _num_marked == 0 ) { + _conflict_lits.push_back(assigned ^ 0x1); + ++_num_in_new_cl; + variable(assigned >> 1).set_new_cl_phase((assigned ^ 0x1) & 0x1); + break; + } else { + gflag |= clause(ante_cl).gflag(); + mark_vars(ante_cl, assigned >> 1); + clause(ante_cl).activity() += 5; + } + } + } + return finish_add_conf_clause(gflag); +} + +void CSolver::print_cls(ostream & os) { + for (unsigned i = 0; i < clauses()->size(); ++i) { + CClause & cl = clause(i); + if (cl.status() == DELETED_CL) + continue; + if (cl.status() == ORIGINAL_CL) { + os <<"0 "; + } else { + assert(cl.status() == CONFLICT_CL); + os << "A "; + } + for (unsigned j = 1; j < 33; ++j) + os << (cl.gid(j) ? 1 : 0); + os << "\t"; + for (unsigned j = 0; j < cl.num_lits(); ++j) { + os << (cl.literal(j).var_sign() ? "-":"") + << cl.literal(j).var_index() << " "; + } + os <<"0" << endl; + } +} + +int CSolver::mem_usage(void) { + int mem_dbase = CDatabase::mem_usage(); + int mem_assignment = 0; + for (int i = 0; i < _stats.max_dlevel; ++i) + mem_assignment += _assignment_stack[i]->capacity() * sizeof(int); + mem_assignment += sizeof(vector)* _assignment_stack.size(); + return mem_dbase + mem_assignment; +} + +void CSolver::clean_up_dbase(void) { + assert(dlevel() == 0); + + int mem_before = mem_usage(); + // 1. remove all the learned clauses + for (vector::iterator itr = clauses()->begin(); + itr != clauses()->end() - 1; ++itr) { + CClause & cl = * itr; + if (cl.status() != ORIGINAL_CL) + mark_clause_deleted(cl); + } + // delete_unrelevant_clauses() is specialized using berkmin deletion strategy + + // 2. free up the mem for the vectors if possible + for (unsigned i = 0; i < variables()->size(); ++i) { + for (unsigned j = 0; j < 2; ++j) { // both phase + vector watched; + vector & old_watched = variable(i).watched(j); + watched.reserve(old_watched.size()); + for (vector::iterator itr = old_watched.begin(); + itr != old_watched.end(); ++itr) + watched.push_back(*itr); + // because watched is a temp mem allocation, it will get deleted + // out of the scope, but by swap it with the old_watched, the + // contents are reserved. + old_watched.swap(watched); +#ifdef KEEP_LIT_CLAUSES + vector lits_cls; + vector & old_lits_cls = variable(i).lit_clause(j); + lits_cls.reserve(old_lits_cls.size()); + for (vector::iterator itr1 = old_lits_cls.begin(); itr1 != + old_lits_cls.end(); ++itr1) + lits_cls.push_back(*itr1); + old_lits_cls.swap(lits_cls); +#endif + } + } + + int mem_after = mem_usage(); + if (_params.verbosity > 0) { + cout << "Database Cleaned, releasing (approximately) " + << mem_before - mem_after << " Bytes" << endl; + } +} + +void CSolver::update_var_score(void) { + for (unsigned i = 1, sz = variables()->size(); i < sz; ++i) { + _ordered_vars[i-1].first = & variable(i); + _ordered_vars[i-1].second = variable(i).score(); + } + ::stable_sort(_ordered_vars.begin(), _ordered_vars.end(), cmp_var_stat); + for (unsigned i = 0, sz = _ordered_vars.size(); i < sz; ++i) + _ordered_vars[i].first->set_var_score_pos(i); + _max_score_pos = 0; +} + +void CSolver::restart(void) { + _stats.num_restarts += 1; + if (_params.verbosity > 1 ) + cout << "Restarting ... " << endl; + if (dlevel() > 0) + back_track(1); + assert(dlevel() == 0); +} + +// this function can be called within a solving process. i.e. not after +// solve() terminate +int CSolver::add_clause_incr(int * lits, int num_lits, int gid) { + // Do not mess up with shrinking. + assert(!_params.shrinking.enable || _shrinking_cls.empty()); + unsigned gflag; + _stats.outcome = UNDETERMINED; + + if (gid == PERMANENT_GID) + gflag = 0; + else if (gid == VOLATILE_GID) { + gflag = ~0x0; + } else { + assert(gid <= WORD_WIDTH && gid > 0); + gflag = (1 << (gid - 1)); + } + + int cl = add_clause(lits, num_lits, gflag); + if (cl < 0) + return -1; + clause(cl).set_status(ORIGINAL_CL); + + if (clause(cl).num_lits() == 1) { + int var_idx = clause(cl).literal(0).var_index(); + if (literal_value(clause(cl).literal(0)) == 0 && + variable(var_idx).dlevel() == 0) { + back_track(0); + if (preprocess() == CONFLICT) + _stats.outcome = UNSATISFIABLE; + } else { + if (dlevel() > 0) + back_track(1); + queue_implication(clause(cl).literal(0).s_var(), cl); + } + return cl; + } + + for (unsigned i = 0, sz = clause(cl).num_lits(); i < sz; ++i) { + int var_idx = lits[i] >> 1; + int value = variable(var_idx).value(); + if (value == UNKNOWN) + continue; + if (variable(var_idx).dlevel() == 0 && + variable(var_idx).antecedent() == -1 && + literal_value(clause(cl).literal(i)) == 0) { + back_track(0); + if (preprocess() == CONFLICT) + _stats.outcome = UNSATISFIABLE; + return cl; + } + } + + int max_level = 0; + int max_level2 = 0; + int unit_lit = 0; + int unknown_count = 0; + int num_sat = 0; + int sat_dlevel = -1, max_lit = 0; + bool already_sat = false; + + for (unsigned i = 0, sz = clause(cl).num_lits(); + unknown_count < 2 && i < sz; ++i) { + int var_idx = lits[i] / 2; + int value = variable(var_idx).value(); + if (value == UNKNOWN) { + unit_lit = clause(cl).literal(i).s_var(); + ++unknown_count; + } else { + int dl = variable(var_idx).dlevel(); + if (dl >= max_level) { + max_level2 = max_level; + max_level = dl; + max_lit = clause(cl).literal(i).s_var(); + } + else if (dl > max_level2) + max_level2 = dl; + if (literal_value(clause(cl).literal(i)) == 1) { + already_sat = true; + ++num_sat; + sat_dlevel = dl; + } + } + } + if (unknown_count == 0) { + if (already_sat) { + assert(sat_dlevel > -1); + if (num_sat == 1 && sat_dlevel == max_level && max_level > max_level2) { + back_track(max_level2 + 1); + assert(max_lit > 1); + queue_implication(max_lit, cl); + } + } else { + assert(is_conflicting(cl)); + if (max_level > max_level2) { + back_track(max_level2 + 1); + assert(max_lit > 1); + queue_implication(max_lit, cl); + } else { + back_track(max_level); + if (max_level == 0 && preprocess() == CONFLICT) + _stats.outcome = UNSATISFIABLE; + } + } + } + else if (unknown_count == 1) { + if (!already_sat) { + if (max_level < dlevel()) + back_track(max_level + 1); + queue_implication(unit_lit, cl); + } + } + return cl; +} Index: /vis_dev/zchaff/zchaff_solver.h =================================================================== --- /vis_dev/zchaff/zchaff_solver.h (revision 10) +++ /vis_dev/zchaff/zchaff_solver.h (revision 10) @@ -0,0 +1,408 @@ +// ********************************************************************* +// Copyright 2000-2004, Princeton University. All rights reserved. +// By using this software the USER indicates that he or she has read, +// understood and will comply with the following: +// +// --- Princeton University hereby grants USER nonexclusive permission +// to use, copy and/or modify this software for internal, noncommercial, +// research purposes only. Any distribution, including commercial sale +// or license, of this software, copies of the software, its associated +// documentation and/or modifications of either is strictly prohibited +// without the prior consent of Princeton University. Title to copyright +// to this software and its associated documentation shall at all times +// remain with Princeton University. Appropriate copyright notice shall +// be placed on all software copies, and a complete copy of this notice +// shall be included in all copies of the associated documentation. +// No right is granted to use in advertising, publicity or otherwise +// any trademark, service mark, or the name of Princeton University. +// +// +// --- This software and any associated documentation is provided "as is" +// +// PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS +// OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A +// PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR +// ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, +// TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. +// +// Princeton University shall not be liable under any circumstances for +// any direct, indirect, special, incidental, or consequential damages +// with respect to any claim by USER or any third party on account of +// or arising from the use, or inability to use, this software or its +// associated documentation, even if Princeton University has been advised +// of the possibility of those damages. +// ********************************************************************* + +#ifndef __SAT_SOLVER__ +#define __SAT_SOLVER__ + +#include "zchaff_version.h" +#include "zchaff_dbase.h" + +#ifndef _SAT_STATUS_ +#define _SAT_STATUS_ + +enum SAT_StatusT { + UNDETERMINED, + UNSATISFIABLE, + SATISFIABLE, + TIME_OUT, + MEM_OUT, + ABORTED +}; +#endif + +enum SAT_DeductionT { + CONFLICT, + NO_CONFLICT +}; + +class CSolver; + +typedef void(*HookFunPtrT)(void *) ; +typedef void(*OutsideConstraintHookPtrT)(CSolver * solver); +typedef bool(*SatHookPtrT)(CSolver * solver); + +// **Struct******************************************************************** +// +// Synopsis [Sat solver parameters ] +// +// Description [] +// +// SeeAlso [] +// +// **************************************************************************** + +struct CSolverParameters { + float time_limit; + int verbosity; + + struct { + unsigned size; + int enable; + int upper_bound; + int lower_bound; + int upper_delta; + int lower_delta; + int bound_update_frequency; + unsigned window_width; + } shrinking; + + struct { + int base_randomness; + int bubble_init_step; + int decay_period; + } decision; + + struct { + bool enable; + unsigned interval; + unsigned head_activity; + unsigned tail_activity; + unsigned head_num_lits; + unsigned tail_num_lits; + int tail_vs_head; + } cls_deletion; + + struct { + bool enable; + int interval; + int first_restart; + int backtrack_incr; + } restart; +}; + +// **Struct******************************************************************** +// +// Synopsis [Sat solver statistics ] +// +// Description [] +// +// SeeAlso [] +// +// **************************************************************************** + +struct CSolverStats { + bool been_reset; // when delete clause in incremental solving, + // must reset. + SAT_StatusT outcome; + bool is_mem_out; // this flag will be set if memory out + double start_cpu_time; + double finish_cpu_time; + int current_randomness; + int next_restart; + int restart_incr; + int next_cls_deletion; + int next_var_score_decay; + int num_free_variables; + int num_free_branch_vars; + long64 total_bubble_move; + int num_decisions; + int num_decisions_stack_conf; + int num_decisions_vsids; + int num_decisions_shrinking; + int num_shrinkings; + int shrinking_benefit; + int shrinking_cls_length; + int num_backtracks; + int max_dlevel; + int random_seed; + long64 num_implications; + int num_restarts; + int num_del_orig_cls; +}; + +// **Class********************************************************************* +// +// Synopsis [Sat Solver] +// +// Description [This class contains the process and datastructrues to solve +// the Sat problem.] +// +// SeeAlso [] +// +// **************************************************************************** + +inline bool cmp_var_stat(const pair & v1, + const pair & v2) { + return v1.second >= v2.second; +} + +struct cmp_var_assgn_pos { + bool operator() (CVariable * v1, CVariable * v2) { + if (v1->dlevel() > v2->dlevel()) + return true; + else if (v1->dlevel() < v2->dlevel()) + return false; + else if (v1->assgn_stack_pos() > v2->assgn_stack_pos()) + return true; + return false; + } +}; + +struct CImplication { + int lit; + int antecedent; +}; + +struct ImplicationQueue:queue { + void dump(ostream & os) { + queue temp(*this); + os << "Implication Queue Previous: " ; + while (!temp.empty()) { + CImplication a = temp.front(); + os << "(" << ((a.lit & 0x1) ? "-" : "+") << (a.lit >> 1) + << ":" << a.antecedent << ") "; + temp.pop(); + } + } +}; + +class CSolver:public CDatabase { + protected: + int _id; // the id of the solver, in case + // we need to distinguish + bool _force_terminate; + CSolverParameters _params; // parameters for the solver + CSolverStats _stats; // statistics and states + + int _dlevel; // current decision elvel + vector*>_assignment_stack; + queue _recent_shrinkings; + bool _mark_increase_score; // used in mark_vars during + // multiple conflict analysis + long64 _implication_id; + ImplicationQueue _implication_queue; + + // hook function run after certain number of decisions + vector > > _hooks; + OutsideConstraintHookPtrT _outside_constraint_hook; + SatHookPtrT _sat_hook; // hook function run after a satisfiable + // solution found, return true to continue + // solving and false to terminate as satisfiable + + // these are for decision making + int _max_score_pos; // index the unassigned var with + // max score + vector > _ordered_vars; // pair's first pointing to + // the var, second is the score. + + // these are for conflict analysis + int _num_marked; // used when constructing learned clause + int _num_in_new_cl; // used when constructing learned clause + vector _conflicts; // the conflicting clauses + vector _conflict_lits; // used when constructing learned clause + vector _resolvents; + multimap _shrinking_cls; + + protected: + void re_init_stats(void); + void init_stats(void); + void init_parameters(void); + void init_solve(void); + void real_solve(void); + void restart(void); + int preprocess(void); + int deduce(void); + void run_periodic_functions(void); + + // for decision making + bool decide_next_branch(void); + void decay_variable_score(void) ; + void adjust_variable_order(int * lits, int n_lits); + void update_var_score(void); + + // for conflict analysis + ClauseIdx add_conflict_clause(int * lits, int n_lits, int gflag); + int analyze_conflicts(void); + ClauseIdx finish_add_conf_clause(int gflag); + int conflict_analysis_firstUIP(void); + void mark_vars(ClauseIdx cl, int var_idx); + void back_track(int level); + + // for bcp + void set_var_value(int var, int value, ClauseIdx ante, int dl); + void set_var_value_BCP(int v, int value); + void unset_var_value(int var); + + // misc functions + bool time_out(void); + void delete_unrelevant_clauses(void); + ClauseIdx add_clause_with_gid(int * lits, int n_lits, int gid = 0); + + public: + // constructors and destructors + CSolver(void); + ~CSolver(void); + + // member access function + void set_time_limit(float t); + void set_mem_limit(int s); + void enable_cls_deletion(bool allow); + void set_randomness(int n) ; + void set_random_seed(int seed); + + void set_variable_number(int n); + int add_variable(void) ; + void mark_var_branchable(int vid); + void mark_var_unbranchable(int vid); + + inline int & dlevel(void) { + return _dlevel; + } + + inline int outcome(void) { + return _stats.outcome; + } + + inline int num_decisions(void) { + return _stats.num_decisions; + } + + inline int num_decisions_stack_conf(void) { + return _stats.num_decisions_stack_conf; + } + + inline int num_decisions_vsids(void) { + return _stats.num_decisions_vsids; + } + + inline int num_decisions_shrinking(void) { + return _stats.num_decisions_shrinking; + } + + inline int num_shrinkings(void) { + return _stats.num_shrinkings; + } + + inline int & num_free_variables(void) { + return _stats.num_free_variables; + } + + inline int max_dlevel(void) { + return _stats.max_dlevel; + } + + inline int random_seed(void) { + return _stats.random_seed; + } + + inline long64 num_implications(void) { + return _stats.num_implications; + } + + inline long64 total_bubble_move(void) { + return _stats.total_bubble_move; + } + + inline const char * version(void) { + return __ZCHAFF_VERSION__; + } + + float elapsed_cpu_time(void); + float cpu_run_time(void) ; + int estimate_mem_usage(void) { + return CDatabase::estimate_mem_usage(); + } + + int mem_usage(void); + + void queue_implication(int lit, ClauseIdx ante_clause) { + CImplication i; + i.lit = lit; + i.antecedent = ante_clause; + _implication_queue.push(i); + } + + // top level function + inline int id(void) { + return _id; + } + + inline void set_id(int i) { + _id = i; + } + + inline void force_terminate(void) { + _force_terminate = true; + } + + inline void unset_force_terminate(void) { + _force_terminate = false; + } + + // for incremental SAT + int add_clause_incr(int * lits, int n_lits, int gid = 0); + + void make_decision(int lit) { + ++dlevel(); + queue_implication(lit, NULL_CLAUSE); + } + + void add_hook(HookFunPtrT fun, int interval); + + inline void add_outside_constraint_hook(OutsideConstraintHookPtrT fun) { + _outside_constraint_hook = fun; + } + + inline void add_sat_hook(SatHookPtrT fun) { + _sat_hook = fun; + } + + void verify_integrity(void); + void delete_clause_group(int gid); + void reset(void); + int solve(void); + ClauseIdx add_orig_clause(int * lits, int n_lits, int gid = 0); + void clean_up_dbase(void); + void dump_assignment_stack(ostream & os = cout); + void dump_implication_queue(ostream & os = cout); + + void print_cls(ostream & os = cout); + void dump(ostream & os = cout ) { + CDatabase::dump(os); + dump_assignment_stack(os); + } + void add_outside_clauses(void); +}; +#endif Index: /vis_dev/zchaff/zchaff_utils.cpp =================================================================== --- /vis_dev/zchaff/zchaff_utils.cpp (revision 10) +++ /vis_dev/zchaff/zchaff_utils.cpp (revision 10) @@ -0,0 +1,89 @@ +// ********************************************************************* +// Copyright 2000-2004, Princeton University. All rights reserved. +// By using this software the USER indicates that he or she has read, +// understood and will comply with the following: +// +// --- Princeton University hereby grants USER nonexclusive permission +// to use, copy and/or modify this software for internal, noncommercial, +// research purposes only. Any distribution, including commercial sale +// or license, of this software, copies of the software, its associated +// documentation and/or modifications of either is strictly prohibited +// without the prior consent of Princeton University. Title to copyright +// to this software and its associated documentation shall at all times +// remain with Princeton University. Appropriate copyright notice shall +// be placed on all software copies, and a complete copy of this notice +// shall be included in all copies of the associated documentation. +// No right is granted to use in advertising, publicity or otherwise +// any trademark, service mark, or the name of Princeton University. +// +// +// --- This software and any associated documentation is provided "as is" +// +// PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS +// OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A +// PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR +// ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, +// TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. +// +// Princeton University shall not be liable under any circumstances for +// any direct, indirect, special, incidental, or consequential damages +// with respect to any claim by USER or any third party on account of +// or arising from the use, or inability to use, this software or its +// associated documentation, even if Princeton University has been advised +// of the possibility of those damages. +// ********************************************************************* + +#include +#include +#include +#include +#include +#include + +int _global_debug_leveli = 0; + +int _global_check_level = 0; + +void fatal(const char * fun, const char * file, int lineno, const char * fmt, ...) { + va_list ap; + fprintf(stderr, "***"); + if (fun) + fprintf(stderr, " in %s", fun); + if (file) + fprintf(stderr, " at %s", file); + if (lineno) + fprintf(stderr, ":%d", lineno); + fprintf(stderr, " "); + va_start(ap, fmt); + vfprintf(stderr, fmt, ap); + va_end(ap); + fflush(stderr); + exit(1); +} + +void warning(const char * fun, const char * file, int lineno, const char * fmt, ...) { + va_list ap; + fprintf(stderr, "***"); + if (fun) + fprintf(stderr, " in %s", fun); + if (file) + fprintf(stderr, " at %s", file); + if (lineno) + fprintf(stderr, ":%d", lineno); + fprintf(stderr, " "); + + va_start(ap, fmt); + vfprintf(stderr, fmt, ap); + va_end(ap); + fflush(stderr); +} + +double get_cpu_time(void) { + double res; + struct rusage usage; + getrusage(RUSAGE_SELF, &usage); + res = usage.ru_utime.tv_usec + usage.ru_stime.tv_usec; + res *= 1e-6; + res += usage.ru_utime.tv_sec + usage.ru_stime.tv_sec; + return res; +} Index: /vis_dev/zchaff/zchaff_version.h =================================================================== --- /vis_dev/zchaff/zchaff_version.h (revision 10) +++ /vis_dev/zchaff/zchaff_version.h (revision 10) @@ -0,0 +1,38 @@ +// ********************************************************************* +// Copyright 2000-2003, Princeton University. All rights reserved. +// By using this software the USER indicates that he or she has read, +// understood and will comply with the following: +// +// --- Princeton University hereby grants USER nonexclusive permission +// to use, copy and/or modify this software for internal, noncommercial, +// research purposes only. Any distribution, including commercial sale +// or license, of this software, copies of the software, its associated +// documentation and/or modifications of either is strictly prohibited +// without the prior consent of Princeton University. Title to copyright +// to this software and its associated documentation shall at all times +// remain with Princeton University. Appropriate copyright notice shall +// be placed on all software copies, and a complete copy of this notice +// shall be included in all copies of the associated documentation. +// No right is granted to use in advertising, publicity or otherwise +// any trademark, service mark, or the name of Princeton University. +// +// +// --- This software and any associated documentation is provided "as is" +// +// PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS +// OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A +// PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR +// ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, +// TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. +// +// Princeton University shall not be liable under any circumstances for +// any direct, indirect, special, incidental, or consequential damages +// with respect to any claim by USER or any third party on account of +// or arising from the use, or inability to use, this software or its +// associated documentation, even if Princeton University has been advised +// of the possibility of those damages. +// ********************************************************************* + +#ifndef __ZCHAFF_VERSION__ +#define __ZCHAFF_VERSION__ "zChaff 2007.3.12" +#endif Index: /vis_dev/zchaff/zchaff_wrapper.wrp =================================================================== --- /vis_dev/zchaff/zchaff_wrapper.wrp (revision 10) +++ /vis_dev/zchaff/zchaff_wrapper.wrp (revision 10) @@ -0,0 +1,489 @@ +// ********************************************************************* +// Copyright 2000-2004, Princeton University. All rights reserved. +// By using this software the USER indicates that he or she has read, +// understood and will comply with the following: +// +// --- Princeton University hereby grants USER nonexclusive permission +// to use, copy and/or modify this software for internal, noncommercial, +// research purposes only. Any distribution, including commercial sale +// or license, of this software, copies of the software, its associated +// documentation and/or modifications of either is strictly prohibited +// without the prior consent of Princeton University. Title to copyright +// to this software and its associated documentation shall at all times +// remain with Princeton University. Appropriate copyright notice shall +// be placed on all software copies, and a complete copy of this notice +// shall be included in all copies of the associated documentation. +// No right is granted to use in advertising, publicity or otherwise +// any trademark, service mark, or the name of Princeton University. +// +// +// --- This software and any associated documentation is provided "as is" +// +// PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS +// OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A +// PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR +// ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, +// TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. +// +// Princeton University shall not be liable under any circumstances for +// any direct, indirect, special, incidental, or consequential damages +// with respect to any claim by USER or any third party on account of +// or arising from the use, or inability to use, this software or its +// associated documentation, even if Princeton University has been advised +// of the possibility of those damages. +// ******************************************************************** + +#include +#include +#include +#include +#include +#include +using namespace std; + +#include "zchaff_solver.h" +#include "zchaff_clsgen.h" + +#ifndef SAT_Manager +#define SAT_Manager void * +#endif + +// ===================================================================== +// Following are wrapper functions for C/C++ callers. +// +// ===================================================================== + +EXTERN SAT_Manager SAT_InitManager(void) { + CSolver * solver = new CSolver; + return (SAT_Manager)solver; +} + +EXTERN const char * SAT_Version(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + return solver->version(); +} + +EXTERN void SAT_SetNumVariables(SAT_Manager mng, int n_var) { + CSolver * solver = (CSolver*) mng; + solver->set_variable_number(n_var); +} + +EXTERN void SAT_ReleaseManager(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + delete solver; +} + +EXTERN int SAT_AddVariable(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int vid = solver->add_variable(); + return vid; +} + +EXTERN void SAT_EnableVarBranch(SAT_Manager mng, int vid) { + CSolver * solver = (CSolver*) mng; + solver->mark_var_branchable(vid); +} + +EXTERN void SAT_DisableVarBranch(SAT_Manager mng, int vid) { + CSolver * solver = (CSolver*) mng; + solver->mark_var_unbranchable(vid); +} + +EXTERN void SAT_SetTimeLimit(SAT_Manager mng, float runtime) { + CSolver * solver = (CSolver*) mng; + solver->set_time_limit(runtime); +} + +EXTERN void SAT_SetMemLimit(SAT_Manager mng, int mem_limit) { + CSolver * solver = (CSolver*) mng; + solver->set_mem_limit(mem_limit); +} + +EXTERN void SAT_AddClause(SAT_Manager mng, + int * clause_lits, + int num_lits, + int gid = 0) { + CSolver * solver = (CSolver*) mng; + solver->add_orig_clause(clause_lits, num_lits, gid); +} + +EXTERN void SAT_DeleteClauseGroup(SAT_Manager mng, + int gid) { + CSolver * solver = (CSolver*) mng; + solver->delete_clause_group(gid); +} + +EXTERN void SAT_Reset(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + solver->reset(); +} + +EXTERN int SAT_MergeClauseGroup(SAT_Manager mng, + int gid1, + int gid2) { + CSolver * solver = (CSolver*) mng; + int g = solver->merge_clause_group(gid1, gid2); + return g; +} + +EXTERN int SAT_AllocClauseGroupID(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int gid = solver->alloc_gid(); + return gid; +} + +EXTERN int SAT_GetGlobalGroupID(SAT_Manager mng) { + return 0; +} + +EXTERN int SAT_GetVolatileGroupID(SAT_Manager mng) { + return -1; +} + +EXTERN int SAT_Solve(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int result = solver->solve(); + return result; +} + +EXTERN void SAT_AddHookFun(SAT_Manager mng, + void(*fun)(void *), + int interval) { + CSolver * solver = (CSolver*) mng; + solver->add_hook(fun, interval); +} + +EXTERN void SAT_MakeDecision(SAT_Manager mng, + int vid, + int sign) { + CSolver * solver = (CSolver*) mng; + solver->make_decision(vid+vid+sign); +} + +EXTERN void SAT_SetRandomness(SAT_Manager mng, + int n) { + CSolver * solver = (CSolver*) mng; + solver->set_randomness(n); +} + +EXTERN void SAT_SetRandSeed(SAT_Manager mng, + int seed) { + CSolver * solver = (CSolver*) mng; + solver->set_random_seed(seed); +} + +EXTERN int SAT_GetVarAsgnment(SAT_Manager mng, + int v_idx) { + CSolver * solver = (CSolver*) mng; + assert(v_idx > 0 && v_idx < (int) solver->variables()->size()); + int v = solver->variable(v_idx).value(); + return v; +} + +EXTERN int SAT_EstimateMemUsage(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int usage = solver->estimate_mem_usage(); + return usage; +} + +EXTERN float SAT_GetElapsedCPUTime(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + float time = solver->elapsed_cpu_time(); + return time; +} + +EXTERN float SAT_GetCurrentCPUTime(SAT_Manager mng) { + float time = get_cpu_time() / 1000.0; + return time; +} + +EXTERN float SAT_GetCPUTime(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + float time = solver->cpu_run_time(); + return time; +} + +EXTERN int SAT_NumLiterals(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int n = solver->num_literals(); + return n; +} + +EXTERN int SAT_NumClauses(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int n = solver->num_clauses(); + return n; +} + +EXTERN int SAT_NumVariables(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int n = solver->num_variables(); + return n; +} + +EXTERN int SAT_InitNumLiterals(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int n = solver->init_num_literals(); + return n; +} + +EXTERN int SAT_InitNumClauses(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int n = solver->init_num_clauses(); + return n; +} + +EXTERN long64 SAT_NumAddedLiterals(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + long64 n = solver->num_added_literals(); + return n; +} + +EXTERN int SAT_NumAddedClauses(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int n = solver->num_added_clauses(); + return n; +} + +EXTERN int SAT_NumDeletedClauses(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int n = solver->num_deleted_clauses(); + return n; +} + +EXTERN int SAT_NumDelOrigCls(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int n = solver->num_del_orig_cls(); + return n; +} + +EXTERN long64 SAT_NumDeletedLiterals(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + long64 n = solver->num_deleted_literals(); + return n; +} + +EXTERN int SAT_NumDecisions(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int n = solver->num_decisions(); + return n; +} + +EXTERN int SAT_NumDecisionsStackConf(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int n = solver->num_decisions_stack_conf(); + return n; +} + +EXTERN int SAT_NumDecisionsVsids(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int n = solver->num_decisions_vsids(); + return n; +} + +EXTERN int SAT_NumDecisionsShrinking(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int n = solver->num_decisions_shrinking(); + return n; +} + +EXTERN int SAT_NumShrinkings(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int n = solver->num_shrinkings(); + return n; +} + +EXTERN int SAT_Random_Seed(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int n = solver->random_seed(); + return n; +} + +EXTERN long64 SAT_NumImplications(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + long64 n = solver->num_implications(); + return n; +} + +EXTERN int SAT_MaxDLevel(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + int n = solver->max_dlevel(); + return n; +} + +EXTERN float SAT_AverageBubbleMove(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + float n = ((float) solver->total_bubble_move()) / + (solver->num_added_literals() - solver->init_num_literals()); + return n; +} + +EXTERN int SAT_GetFirstClause(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + for (unsigned i = 0; i < solver->clauses()->size(); ++i) + if (solver->clause(i).status() != DELETED_CL) { + return i; + } + return -1; +} + +EXTERN int SAT_GetClauseType(SAT_Manager mng, int cl_idx) { + CSolver * solver = (CSolver*) mng; + int type = solver->clause(cl_idx).status(); + return type; +} + +EXTERN int SAT_IsSetClauseGroupID(SAT_Manager mng, int cl_idx, int id) { + CSolver * solver = (CSolver*) mng; + int r = solver->clause(cl_idx).gid(id); + return r; +} + +EXTERN void SAT_ClearClauseGroupID(SAT_Manager mng, int cl_idx, int id) { + CSolver * solver = (CSolver*) mng; + solver->clause(cl_idx).clear_gid(id); +} + +EXTERN void SAT_SetClauseGroupID(SAT_Manager mng, int cl_idx, int id) { + CSolver * solver = (CSolver*) mng; + solver->clause(cl_idx).set_gid(id); +} + +EXTERN int SAT_GetNextClause(SAT_Manager mng, int cl_idx) { + CSolver * solver = (CSolver*) mng; + for (unsigned i = cl_idx + 1; i < solver->clauses()->size(); ++i) + if (solver->clause(i).status() != DELETED_CL) { + return i; + } + return -1; +} + +EXTERN int SAT_GetClauseNumLits(SAT_Manager mng, int cl_idx) { + CSolver * solver = (CSolver*) mng; + int n = solver->clause(cl_idx).num_lits(); + return n; +} + +EXTERN void SAT_GetClauseLits(SAT_Manager mng, int cl_idx, int * lits) { + CSolver * solver = (CSolver*) mng; + for (unsigned i = 0; i < solver->clause(cl_idx).num_lits(); ++i) { + lits[i] = solver->clause(cl_idx).literal(i).s_var(); + } +} + +EXTERN void SAT_EnableConfClsDeletion(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + solver->enable_cls_deletion(true); +} + +EXTERN void SAT_DisableConfClsDeletion(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + solver->enable_cls_deletion(false); +} + +EXTERN void SAT_CleanUpDatabase(SAT_Manager mng) { + CSolver * solver = (CSolver*) mng; + solver->clean_up_dbase(); +} + +EXTERN void SAT_GenClsAnd2(SAT_Manager mng, + int a, + int b, + int o, + int gid = 0) { + CSolver * solver = (CSolver*) mng; + CClause_Gen cls_gen; + cls_gen.and2(*solver, a, b, o, gid); +} + +EXTERN void SAT_GenClsAndN(SAT_Manager mng, + int * inputs, + int num_inputs, + int o, + int gid = 0) { + CSolver * solver = (CSolver*) mng; + CClause_Gen cls_gen; + cls_gen.and_n(*solver, inputs, num_inputs, o, gid); +} + +EXTERN void SAT_GenClsOr2(SAT_Manager mng, + int a, + int b, + int o, + int gid = 0) { + CSolver * solver = (CSolver*) mng; + CClause_Gen cls_gen; + cls_gen.or2(*solver, a, b, o, gid); +} + +EXTERN void SAT_GenClsOrN(SAT_Manager mng, + int * inputs, + int num_inputs, + int o, + int gid = 0) { + CSolver * solver = (CSolver*) mng; + CClause_Gen cls_gen; + cls_gen.or_n(*solver, inputs, num_inputs, o, gid); +} + +EXTERN void SAT_GenClsNand2(SAT_Manager mng, + int a, + int b, + int o, + int gid = 0) { + CSolver * solver = (CSolver*) mng; + CClause_Gen cls_gen; + cls_gen.nand2(*solver, a, b, o, gid); +} + + +EXTERN void SAT_GenClsNandN(SAT_Manager mng, + int * inputs, + int num_inputs, + int o, + int gid = 0) { + CSolver * solver = (CSolver*) mng; + CClause_Gen cls_gen; + cls_gen.nand_n(*solver, inputs, num_inputs, o, gid); +} + + +EXTERN void SAT_GenClsNor2(SAT_Manager mng, + int a, + int b, + int o, + int gid = 0) { + CSolver * solver = (CSolver*) mng; + CClause_Gen cls_gen; + cls_gen.nor2(*solver, a, b, o, gid); +} + + +EXTERN void SAT_GenClsNorN(SAT_Manager mng, + int * inputs, + int num_inputs, + int o, + int gid = 0) { + CSolver * solver = (CSolver*) mng; + CClause_Gen cls_gen; + cls_gen.nor_n(*solver, inputs, num_inputs, o, gid); +} + +EXTERN void SAT_GenClsXor(SAT_Manager mng, + int a, + int b, + int o, + int gid = 0) { + CSolver * solver = (CSolver*) mng; + CClause_Gen cls_gen; + cls_gen.xor2(*solver, a, b, o, gid); +} + +EXTERN void SAT_GenClsNot(SAT_Manager mng, + int a, + int o, + int gid = 0) { + CSolver * solver = (CSolver*) mng; + CClause_Gen cls_gen; + cls_gen.not1(*solver, a, o, gid); +} Index: /vis_dev/zchaff/zminimal.cpp =================================================================== --- /vis_dev/zchaff/zminimal.cpp (revision 10) +++ /vis_dev/zchaff/zminimal.cpp (revision 10) @@ -0,0 +1,317 @@ +// ********************************************************************* +// Copyright 2000-2004, Princeton University. All rights reserved. +// By using this software the USER indicates that he or she has read, +// understood and will comply with the following: +// +// --- Princeton University hereby grants USER nonexclusive permission +// to use, copy and/or modify this software for internal, noncommercial, +// research purposes only. Any distribution, including commercial sale +// or license, of this software, copies of the software, its associated +// documentation and/or modifications of either is strictly prohibited +// without the prior consent of Princeton University. Title to copyright +// to this software and its associated documentation shall at all times +// remain with Princeton University. Appropriate copyright notice shall +// be placed on all software copies, and a complete copy of this notice +// shall be included in all copies of the associated documentation. +// No right is granted to use in advertising, publicity or otherwise +// any trademark, service mark, or the name of Princeton University. +// +// +// --- This software and any associated documentation is provided "as is" +// +// PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS +// OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A +// PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR +// ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, +// TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. +// +// Princeton University shall not be liable under any circumstances for +// any direct, indirect, special, incidental, or consequential damages +// with respect to any claim by USER or any third party on account of +// or arising from the use, or inability to use, this software or its +// associated documentation, even if Princeton University has been advised +// of the possibility of those damages. +// ********************************************************************* + +#include +#include +#include +#include +#include +#include +#include + +using namespace std; + +#include "SAT.h" + +const int MAX_LINE_LENGTH = 65536; +const int MAX_WORD_LENGTH = 64; + +void read_cnf_omit(SAT_Manager mng, char * filename, vector & omit) { + char line_buffer[MAX_LINE_LENGTH]; + char word_buffer[MAX_WORD_LENGTH]; + set clause_vars; + set clause_lits; + unsigned omit_idx = 0; + int line_num = 0; + ifstream inp(filename, ios::in); + if (!inp) { + cerr << "Can't open input file" << endl; + exit(1); + } + int cl_id = -1; + while (inp.getline(line_buffer, MAX_LINE_LENGTH)) { + ++line_num; + if (line_buffer[0] == 'c') { + continue; + } + else if (line_buffer[0] == 'p') { + int var_num; + int cl_num; + int arg = sscanf(line_buffer, "p cnf %d %d", &var_num, &cl_num); + if (arg < 2) { + cerr << "Unable to read number of variables and clauses" + << "at line " << line_num << endl; + exit(3); + } + SAT_SetNumVariables(mng, var_num); // first element not used. + } else { // Clause definition or continuation + char *lp = line_buffer; + do { + char *wp = word_buffer; + while (*lp && ((*lp == ' ') || (*lp == '\t'))) { + lp++; + } + while (*lp && (*lp != ' ') && (*lp != '\t') && (*lp != '\n')) { + *(wp++) = *(lp++); + } + *wp = '\0'; // terminate string + + if (strlen(word_buffer) != 0) { // check if number is there + int var_idx = atoi(word_buffer); + int sign = 0; + + if (var_idx != 0) { + if (var_idx < 0) { + var_idx = -var_idx; + sign = 1; + } + clause_vars.insert(var_idx); + clause_lits.insert((var_idx << 1) + sign); + } else { + // add this clause + ++cl_id; + if (omit_idx < omit.size()-1 && omit[omit_idx] < cl_id ) + ++omit_idx; + if (omit_idx < omit.size()) { + if (omit[omit_idx] == cl_id) { + clause_lits.clear(); + clause_vars.clear(); + } + } + if (clause_vars.size() != 0 && + clause_vars.size() == clause_lits.size()) { + vector temp; + for (set::iterator itr = clause_lits.begin(); + itr != clause_lits.end(); ++itr) { + temp.push_back(*itr); + } + SAT_AddClause(mng, & temp.begin()[0], temp.size() ); + } + clause_lits.clear(); + clause_vars.clear(); + } + } + } + while (*lp); + } + } + if (!inp.eof()) { + cerr << "Input line " << line_num << " too long. Unable to continue..." + << endl; + exit(2); + } + + if (clause_lits.size() && clause_vars.size() == clause_lits.size()) { + vector temp; + for (set::iterator itr = clause_lits.begin(); + itr != clause_lits.end(); ++itr) { + temp.push_back(*itr); + } + SAT_AddClause(mng, & temp.begin()[0], temp.size() ); + } + clause_lits.clear(); + clause_vars.clear(); +} + +int get_num_clause(char * filename) { + char line_buffer[MAX_LINE_LENGTH]; + ifstream inp(filename, ios::in); + if (!inp) { + cerr << "Can't open input file" << endl; + exit(1); + } + while (inp.getline(line_buffer, MAX_LINE_LENGTH)) { + if (inp.fail()) { + cerr << "Too large an input line. Unable to continue..." << endl; + exit(2); + } + if (line_buffer[0] == 'p') { + int var_num; + int cl_num; + int arg = sscanf(line_buffer, "p cnf %d %d", &var_num, &cl_num); + if (arg < 2) { + cerr << "Unable to read number of variables and clauses" << endl; + exit(3); + } + return cl_num; + } + } + cerr << "Can't find the header in CNF: p cnf NumVar NumCls " << endl; + exit(1); + return 0; +} + +void handle_result(SAT_Manager mng, int outcome, char * filename) { + string result = "UNKNOWN"; + switch (outcome) { + case SATISFIABLE: + cout << "Instance satisfiable" << endl; + // following lines will print out a solution if a solution exist + for (unsigned i = 1, sz = SAT_NumVariables(mng); i <= sz; ++i) { + switch (SAT_GetVarAsgnment(mng, i)) { + case -1: + cout << "(" << i<< ")"; + break; + case 0: + cout << "-" << i; + break; + case 1: + cout << i; + break; + default: + cerr << "Unknown variable value state"<< endl; + exit(4); + } + cout << " "; + } + result = "SAT"; + cout << endl; + break; + case UNSATISFIABLE: + result = "UNSAT"; + cout << "Instance unsatisfiable" << endl; + break; + case TIME_OUT: + result = "ABORT : TIME OUT"; + cout << "Time out, unable to determine the outcome of the instance"; + cout << endl; + break; + case MEM_OUT: + result = "ABORT : MEM OUT"; + cout << "Memory out, unable to determine the outcome of the instance"; + cout << endl; + break; + default: + cerr << "Unknown outcome" << endl; + exit(5); + } + cout << "Max Decision Level\t\t\t" << SAT_MaxDLevel(mng) << endl; + cout << "Num. of Decisions\t\t\t" << SAT_NumDecisions(mng) << endl; + cout << "Num. of Variables\t\t\t" << SAT_NumVariables(mng) << endl; + cout << "Original Num Clauses\t\t\t" << SAT_InitNumClauses(mng) << endl; + cout << "Original Num Literals\t\t\t" << SAT_InitNumLiterals(mng) << endl; + cout << "Added Conflict Clauses\t\t\t" << SAT_NumAddedClauses(mng) - + SAT_InitNumClauses(mng)<< endl; + cout << "Added Conflict Literals\t\t\t" << SAT_NumAddedLiterals(mng) - + SAT_InitNumLiterals(mng) << endl; + cout << "Deleted Unrelevant clause\t\t" << SAT_NumDeletedClauses(mng) <= 0; + cl_idx = SAT_GetNextClause(mng, cl_idx)) { + int len = SAT_GetClauseNumLits(mng, cl_idx); + int * lits = new int[len+1]; + SAT_GetClauseLits(mng, cl_idx, lits); + int i; + for (i = 0; i < len; ++i) { + int v_idx = lits[i] >> 1; + int sign = lits[i] & 0x1; + int var_value = SAT_GetVarAsgnment(mng, v_idx); + if ((var_value == 1 && sign == 0) || + (var_value == 0 && sign == 1)) + break; + } + if (i >= len) { + cerr << "Verify Satisfiable solution failed, please " + << "file a bug report, thanks. " << endl; + exit(6); + } + delete [] lits; + ++num_verified; + } + cout << num_verified << " Clauses are true, Verify Solution successful. "; +} + +int main(int argc, char ** argv) { + if (argc != 2) { + cerr << "ZMinimal: Find Minimal Core. " << endl; + cerr << "Copyright 2003-2004, Princeton University" << endl << endl; + cerr << "Usage: "<< argv[0] << " cnf_file " << endl; + return 2; + } + vector omit; + int num_cls = get_num_clause(argv[1]); + cout << "Total : " << num_cls << " passes"; + for (int i = 0; i < num_cls; ++i) { + if (i % 50 == 0) + cout << endl << i << ":\t"; + if (i % 10 == 0) + cout << " "; + cout.flush(); + SAT_Manager mng = SAT_InitManager(); + omit.push_back(i); + read_cnf_omit(mng, argv[1], omit); + int result = SAT_Solve(mng); + if (result != SATISFIABLE) { + cout << "*" ; + } else { + cout << "-"; + omit.pop_back(); + } + cout.flush(); + SAT_ReleaseManager(mng); + } + cout << endl; + cout << "Instance Cls: " << num_cls << " MinCore Cls: " + << num_cls - omit.size() << " Diff: " << omit.size() << endl; + cout << "Unneeded clauses are: "; + for (unsigned i = 0; i < omit.size(); ++i) { + if (i % 20 == 0) + cout << endl; + cout << omit[i] << " "; + } + cout << endl; + return 0; +} Index: /vis_dev/zchaff/zverify_df.cpp =================================================================== --- /vis_dev/zchaff/zverify_df.cpp (revision 10) +++ /vis_dev/zchaff/zverify_df.cpp (revision 10) @@ -0,0 +1,801 @@ +// ********************************************************************* +// Copyright 2000-2004, Princeton University. All rights reserved. +// By using this software the USER indicates that he or she has read, +// understood and will comply with the following: +// +// --- Princeton University hereby grants USER nonexclusive permission +// to use, copy and/or modify this software for internal, noncommercial, +// research purposes only. Any distribution, including commercial sale +// or license, of this software, copies of the software, its associated +// documentation and/or modifications of either is strictly prohibited +// without the prior consent of Princeton University. Title to copyright +// to this software and its associated documentation shall at all times +// remain with Princeton University. Appropriate copyright notice shall +// be placed on all software copies, and a complete copy of this notice +// shall be included in all copies of the associated documentation. +// No right is granted to use in advertising, publicity or otherwise +// any trademark, service mark, or the name of Princeton University. +// +// +// --- This software and any associated documentation is provided "as is" +// +// PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS +// OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A +// PARTICULAR PURPOSE, OR THAT USE OF THE SOFTWARE, MODIFICATIONS, OR +// ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, +// TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY. +// +// Princeton University shall not be liable under any circumstances for +// any direct, indirect, special, incidental, or consequential damages +// with respect to any claim by USER or any third party on account of +// or arising from the use, or inability to use, this software or its +// associated documentation, even if Princeton University has been advised +// of the possibility of those damages. +// ********************************************************************* + +#include +#include +#include +#include +#include +#include +#include +#include +#include + +using namespace std; + +const int WORD_LEN = 64000; + +const int MEM_LIMIT = 800000; + +const int UNKNOWN = 2; + +int _peak_mem; +bool _dump_core; + +double get_cpu_time(void) { + double res; + struct rusage usage; + getrusage(RUSAGE_SELF, &usage); + res = usage.ru_utime.tv_usec + usage.ru_stime.tv_usec; + res *= 1e-6; + res += usage.ru_utime.tv_sec + usage.ru_stime.tv_sec; + return res; +} + +void get_line(ifstream* fs, vector* buf) { + buf->clear(); + buf->reserve(4096); + while (!fs->eof()) { + char ch = fs->get(); + if (ch == '\n' || ch == '\377') + break; + if (ch == '\r') + continue; + buf->push_back(ch); + } + buf->push_back('\0'); + return; +} + +int get_token(char * & lp, char * token) { + char * wp = token; + while (*lp && ((*lp == ' ') || (*lp == '\t'))) { + lp++; + } + while (*lp && (*lp != ' ') && (*lp != '\t') && (*lp != '\n')) { + *(wp++) = *(lp++); + } + *wp = '\0'; // terminate string + return wp - token; +} + +int get_mem_usage(void) { + FILE * fp; + char buffer[128]; + char token[128]; + char filename[128]; + + int pid = getpid(); + snprintf(filename, sizeof(filename), "/proc/%i/status", pid); + if ((fp = fopen(filename, "r")) == NULL) { + cerr << "Can't open Proc file, are you sure you are using Linux?" << endl; + exit(1); + } + while (!feof(fp)) { + fgets(buffer, 128, fp); + char * ptr = buffer; + get_token(ptr, token); + if (strcmp(token, "VmSize:") == 0) { + get_token(ptr, token); + fclose(fp); + return atoi(token); + } + } + cerr << "Error in get memeory usage" << endl; + exit(1); + return 0; +} + +int my_a2i(char * str) { + int result = 0; + bool neg = false; + if (str[0] == '-') { + neg = true; + ++str; + } + else if (str[0] == '+') + ++str; + for (unsigned i = 0; i < strlen(str); ++i) { + int d = str[i] - '0'; + if (d < 0 || d > 9) { + cerr << "Abort: Unable to change " << str << " into a number " << endl; + exit(1); + } + result = result * 10 + d; + } + if (neg) + result = -result; + return result; +} + +class CClause { + public: + vector literals; + vector resolvents; + bool is_involved : 1; + bool is_built : 1; + bool is_needed : 1; + + CClause(void) { + is_involved = false; + is_built = false; + is_needed = false; + } + ~CClause(void) {} +}; + +class CVariable { + public: + short value; + short in_clause_phase :4; + bool is_needed :1; + int antecedent; + int num_lits[2]; + int level; + CVariable(void) { + value = UNKNOWN; + antecedent = -1; + in_clause_phase = UNKNOWN; + num_lits[0] = num_lits[1] = 0; + level = -1; + is_needed = false; + } +}; + +struct cmp_var_level { + bool operator() (CVariable * v1, CVariable * v2) { + if (v1->level > v2->level) + return true; + else if (v1->level < v2->level) + return false; + else if ( (int)v1 > (int)v2) + return true; + return false; + } +}; + +class CDatabase { + private: + int _current_num_clauses; + int _num_init_clauses; + vector _variables; + vector _clauses; + int _conf_id; + vector _conf_clause; + + public: + CDatabase(void) { + _num_init_clauses = 0; + _current_num_clauses = 0; + _conf_id = -1; + } + + int & num_init_clauses(void) { + return _num_init_clauses; + } + + vector & variables(void) { + return _variables; + } + + vector & clauses(void) { + return _clauses; + } + + void read_cnf(char * filename); + bool verify(char * filename); + bool real_verify(void); + int lit_value(int svar) { + assert(_variables[svar>>1].value != UNKNOWN); + return _variables[svar>>1].value ^ (svar & 0x1); + } + int add_orig_clause_by_lits(vector lits); + int add_learned_clause_by_resolvents(vector & resolvents); + void set_var_number(int nvar); + void set_init_cls_number(int n) { + _num_init_clauses = n; + } + void construct_learned_clauses(void); + void recursive_construct_clause(int cl_id); + void recursive_find_involved(int cl_id); + int recursive_find_level(int vid); + void dump(void); +}; + +void CDatabase::dump(void) { + cout << "p cnf " << _variables.size() - 1 << " " << _num_init_clauses << endl; + for (unsigned i = 0; i < _clauses.size(); ++i) { + for (unsigned j = 0; j < _clauses[i].literals.size(); ++j) { + int lit = _clauses[i].literals[j]; + cout << ((lit & 0x1) ? "-" : "") << (lit >> 1) << " "; + } + cout << "0" << endl; + } +} + +void CDatabase::set_var_number(int nvar) { + _variables.resize(nvar + 1); + for (unsigned i = 0; i < _variables.size(); ++i) { + _variables[i].value = UNKNOWN; + _variables[i].in_clause_phase = UNKNOWN; + } +} + +void check_mem_out(void) { + int mem = get_mem_usage(); + if (mem > MEM_LIMIT) { + cerr << "Mem out" << endl; + exit(1); + } + if (mem > _peak_mem) + _peak_mem = mem; +} + +int CDatabase::add_orig_clause_by_lits(vector lits) { + static int line_n = 0; + ++line_n; + if (lits.size() == 0) { + cerr << "Empty Clause Encountered " << endl; + exit(1); + } + int cls_id = _clauses.size(); + _clauses.resize(_clauses.size() + 1); + vector temp_cls; + for (unsigned i = 0; i < lits.size(); ++i) { + int vid = lits[i]; + int phase = 0; + if (vid < 0) { + vid = - vid; + phase = 1; + } + if (vid == 0 || vid > (int) _variables.size() - 1) { + cerr << "Variable index out of range " << endl; + exit(1); + } + if (_variables[vid].in_clause_phase == UNKNOWN) { + _variables[vid].in_clause_phase = phase; + temp_cls.push_back(vid + vid + phase); +// _clauses[cls_id].my_literals.push_back(vid + vid + phase); + ++_variables[vid].num_lits[phase]; + } + else if (_variables[vid].in_clause_phase != phase) { + cerr << "clause " << line_n << endl; + cerr << "A clause contain both literal and its negate " << endl; + exit(1); + } + } + _clauses[cls_id].literals.resize(temp_cls.size()); + for (unsigned i = 0; i< temp_cls.size(); ++i) { + _clauses[cls_id].literals[i]= temp_cls[i]; + } + _clauses[cls_id].is_built = true; +// _clauses[cls_id].my_is_built = true; + for (unsigned i = 0; i< lits.size(); ++i) { + int vid = lits[i]; + if (vid < 0) vid = -vid; + _variables[vid].in_clause_phase = UNKNOWN; + } + ++_current_num_clauses; + if (_current_num_clauses%10 == 0) + check_mem_out(); + return cls_id; +} + +int CDatabase::add_learned_clause_by_resolvents(vector & resolvents) { + int cls_id = _clauses.size(); + _clauses.resize(_clauses.size() + 1); + _clauses[cls_id].resolvents.resize(resolvents.size()); + for (unsigned i = 0; i< resolvents.size(); ++i) + _clauses[cls_id].resolvents[i] = resolvents[i]; + _clauses[cls_id].is_built = false; + return cls_id; +} + +void CDatabase::read_cnf(char * filename) { + cout << "Read in original clauses ... "; + ifstream in_file(filename); + if (!in_file) { + cerr << "Can't open input CNF file " << filename << endl; + exit(1); + } + vector buffer; + vector literals; + bool header_encountered = false; + char token[WORD_LEN]; + while (!in_file.eof()) { + get_line(&in_file, &buffer); + char * ptr = &(*buffer.begin()); + if (get_token(ptr, token)) { + if (strcmp(token, "c") == 0) + continue; + else if (strcmp(token, "p") == 0) { + get_token(ptr, token); + if (strcmp(token, "cnf") != 0) { + cerr << "Format Error, p cnf NumVar NumCls " << endl; + exit(1); + } + get_token(ptr, token); + int nvar = my_a2i(token); + set_var_number(nvar); + get_token(ptr, token); + int ncls = my_a2i(token); + set_init_cls_number(ncls); + header_encountered = true; + continue; + } else { + int lit = my_a2i(token); + if (lit != 0) { + literals.push_back(lit); + } else { + add_orig_clause_by_lits(literals); + literals.clear(); + } + } + } + while (get_token(ptr, token)) { + int lit = my_a2i(token); + if (lit != 0) { + literals.push_back(lit); + } else { + add_orig_clause_by_lits(literals); + literals.clear(); + } + } + } + if (!literals.empty()) { + cerr << "Trailing numbers without termination " << endl; + exit(1); + } + if (clauses().size() != (unsigned)num_init_clauses()) + cerr << "WARNING : Clause count inconsistant with the header " << endl; + cout << num_init_clauses() << " Clauses " << endl; +} + +void CDatabase::recursive_find_involved(int cl_id) { + if (_clauses[cl_id].is_involved == true) + return; + _clauses[cl_id].is_involved = true; + + recursive_construct_clause(cl_id); + + int num_1 = 0; + for (unsigned i = 0; i < _clauses[cl_id].literals.size(); ++i) { + int lit = _clauses[cl_id].literals[i]; + int vid = (lit>>1); + int sign = (lit & 0x1); + assert(_variables[vid].value != UNKNOWN); + if ((_variables[vid].value == 1 && sign == 0) || + (_variables[vid].value == 0 && sign == 1)) { + if (num_1 == 0) { + ++num_1; + } else { + cerr << "Clause " << cl_id << " has more than one value 1 literals " + << endl; + exit(1); + } + } else { // literal value 0, so seek its antecedent + int ante = _variables[vid].antecedent; + recursive_find_involved(ante); + } + } +} + +void CDatabase::recursive_construct_clause(int cl_id) { + CClause & cl = _clauses[cl_id]; + if (cl.is_built == true) + return; + + assert(cl.resolvents.size() > 1); + + // I have to construct them first because of recursion may + // mess up with the in_clause_signs. + for (unsigned i = 0; i < cl.resolvents.size(); ++i) { + _clauses[cl.resolvents[i]].is_needed = true; + recursive_construct_clause(cl.resolvents[i]); + } + +// cout << "Constructing clause " << cl_id << endl; + vector literals; + + // initialize + int cl1 = cl.resolvents[0]; + assert(_clauses[cl1].is_built); + for (unsigned i = 0; i < _clauses[cl1].literals.size(); ++i) { + int lit = _clauses[cl1].literals[i]; + int vid = (lit >> 0x1); + int sign = (lit & 0x1); + assert(_variables[vid].in_clause_phase == UNKNOWN); + _variables[vid].in_clause_phase = sign; + literals.push_back(lit); + } + + for (unsigned i = 1; i < cl.resolvents.size(); ++i) { + int distance = 0; + int cl1 = cl.resolvents[i]; + assert(_clauses[cl1].is_built); + for (unsigned j = 0; j < _clauses[cl1].literals.size(); ++j) { + int lit = _clauses[cl1].literals[j]; + int vid = (lit >> 0x1); + int sign = (lit & 0x1); + if (_variables[vid].in_clause_phase == UNKNOWN) { + _variables[vid].in_clause_phase = sign; + literals.push_back(lit); + } + else if (_variables[vid].in_clause_phase != sign) { + // distance 1 literal + ++distance; + _variables[vid].in_clause_phase = UNKNOWN; + } + } + if (distance != 1) { + cerr << "Resolve between two clauses with distance larger than 1" << endl; + cerr << "The resulting clause is " << cl_id << endl; + cerr << "Starting clause is " << cl.resolvents[0] << endl; + cerr << "One of the clause involved is " << cl1 << endl; + exit(1); + } + } + vector temp_cls; + for (unsigned i = 0; i < literals.size(); ++i) { + int lit = literals[i]; + int vid = (lit >> 0x1); + int sign = (lit & 0x1); + if (_variables[vid].in_clause_phase == UNKNOWN) + continue; + assert(_variables[vid].in_clause_phase == sign); + _variables[vid].in_clause_phase = UNKNOWN; + temp_cls.push_back(lit); + } + cl.literals.resize(temp_cls.size()); + for (unsigned i = 0; i < temp_cls.size(); ++i) + cl.literals[i] = temp_cls[i]; + +// ::sort(cl.literals.begin(), cl.literals.end()); +// assert(cl.literals.size()== cl.my_literals.size()); +// for (unsigned i=0; i< cl.literals.size(); ++i) +// assert(cl.literals[i] == cl.my_literals[i]); + cl.is_built = true; + ++_current_num_clauses; + if (_current_num_clauses%10 == 0) + check_mem_out(); +} + +int CDatabase::recursive_find_level(int vid) { + int ante = _variables[vid].antecedent; + assert(_variables[vid].value != UNKNOWN); + assert(_variables[vid].antecedent != -1); + assert(_clauses[ante].is_involved); + if (_variables[vid].level != -1) + return _variables[vid].level; + int level = -1; + for (unsigned i = 0; i <_clauses[ante].literals.size(); ++i) { + int v = (_clauses[ante].literals[i] >> 1); + int s = (_clauses[ante].literals[i] & 0x1); + if (v == vid) { + assert(_variables[v].value != s); + continue; + } else { + assert(_variables[v].value == s); + int l = recursive_find_level(v); + if (level < l ) + level = l; + } + } + _variables[vid].level = level + 1; + return level + 1; +} + +bool CDatabase::real_verify(void) { + // 1. If a variable is assigned value at dlevel 0, + // either it's pure or it has an antecedent + for (unsigned i = 1; i < _variables.size(); ++i) { + if (_variables[i].value != UNKNOWN && _variables[i].antecedent == -1) { + if ((_variables[i].num_lits[0] == 0 && _variables[i].value == 0) || + (_variables[i].num_lits[1] == 0 && _variables[i].value == 1)) { +// cout << "Variable " << i << " is assigned " << _variables[i].value +// << " because it is pure literal. " << endl; + } else { + cerr << "Don't know why variable " << i << " is assigned " + << _variables[i].value << " for no reasons" << endl; + exit(1); + } + } + } + // 2. Construct the final conflicting clause if needed and find all + // the clauses that are involved in making it conflicting + cout << "Begin constructing all involved clauses " << endl; + _clauses[_conf_id].is_needed = true; + recursive_find_involved(_conf_id); + int count = 0; + for (unsigned i = num_init_clauses(); i< _clauses.size(); ++i) + if (_clauses[i].is_built) + ++count; + cout << "Num. Learned Clause:\t\t\t" << _clauses.size() - num_init_clauses() + << endl + << "Num. Clause Built:\t\t\t" << count << endl + << "Constructed all involved clauses " << endl; + + // 2.5. Verify the literals in the CONF clause + // comments this out if it gives error because you give the wrong + // CONF clause literals. + assert(_clauses[_conf_id].is_built); + assert(_clauses[_conf_id].is_involved); + bool _found; + for (unsigned i = 0; i <_conf_clause.size(); ++i) { + _found = false; + for (unsigned j = 0; j <_clauses[_conf_id].literals.size(); ++j) { + if (_conf_clause[i] == _clauses[_conf_id].literals[j]) { + _found = true; + break; + } + } + if (!_found) { + cerr << "The conflict clause in trace can't be verified! " << endl; + cerr << "Literal " << _conf_clause[i] << " is not found." << endl; + } + } + cout << "Conflict clause verification finished." << endl; + + // 3. Levelize the variables that are decided at dlevel 0 + cout << "Levelize variables..."; + for (unsigned i = 1; i < _variables.size(); ++i) { + int cl_id = _variables[i].antecedent; + if (_variables[i].value != UNKNOWN && cl_id != -1) { + if (_clauses[cl_id].is_involved) { + recursive_find_level(i); +// int level = recursive_find_level(i); +// cout << "Var: " << i << " level " << level << endl; + } + } + } + cout << "finished"<< endl; + // 4. Can we construct an empty clause? + cout << "Begin Resolution..." ; + set clause_lits; + for (unsigned i = 0; i< _clauses[_conf_id].literals.size(); ++i) { + assert(lit_value(_clauses[_conf_id].literals[i]) == 0); + int vid = (_clauses[_conf_id].literals[i] >> 1); + clause_lits.insert(&_variables[vid]); + } + assert(clause_lits.size() == _clauses[_conf_id].literals.size()); + + while (!clause_lits.empty()) { +// for (set::iterator itr = clause_lits.begin(); +// itr != clause_lits.end(); ++itr) { +// int vid = (*itr) - &_variables[0]; +// cout << vid << "(" << (*itr)->level << ") "; +// } +// cout << endl; + + int vid = (*clause_lits.begin() - &_variables[0]); + int ante = _variables[vid].antecedent; + if (ante == -1) { + cerr << "Variable " << vid << " has an NULL antecedent "; + exit(1); + } + _clauses[ante].is_needed = true; + clause_lits.erase(clause_lits.begin()); + _variables[vid].in_clause_phase = 1; + CClause & cl = _clauses[ante]; + int distance = 0; + for (unsigned i = 0; i< cl.literals.size(); ++i) { + int l = cl.literals[i]; + int v = (l>>1); + assert(_variables[v].value != UNKNOWN); + if (lit_value(l) == 1) { + if (vid != v) { + cerr << "The antecedent of the variable is not really an antecedent " + << endl; + exit(1); + } + else + ++distance; + } + else + clause_lits.insert(&_variables[v]); + } + assert(distance == 1); + } + cout << " Empty clause generated." << endl; + cout << "Mem Usage :\t\t\t\t" << get_mem_usage()<< endl; + int needed_cls_count = 0; + int needed_var_count = 0; + for (int i = 0; i < num_init_clauses(); ++i) { + if (_clauses[i].is_needed == true) { + ++needed_cls_count; + for (unsigned j = 0; j < _clauses[i].literals.size(); ++j) { + int vid = (_clauses[i].literals[j] >> 1); + if (_variables[vid].is_needed == false) { + ++needed_var_count; + _variables[vid].is_needed = true; + } + } + } + } + cout << "Original Num. Clauses:\t\t\t" << num_init_clauses() << endl; + cout << "Needed Clauses to Construct Empty:\t"<< needed_cls_count << endl; + cout << "Total Variable count:\t\t\t" << _variables.size()-1 << endl; + cout << "Variables involved in Empty:\t\t" << needed_var_count << endl; + + for (unsigned i = 0; i< _clauses.size(); ++i) { + if (_clauses[i].is_built) + assert(_clauses[i].is_needed || i < (unsigned)num_init_clauses()); + } + if (_dump_core == true) { + cout << "Unsat Core dumped:\t\t\tunsat_core.cnf" << endl; + ofstream dump("unsat_core.cnf"); + dump << "c Variables Not Involved: "; + unsigned int k = 0; + for (unsigned i = 1; i < _variables.size(); ++i) { + if (_variables[i].is_needed == false) { + if (k%20 == 0) + dump << endl << "c "; + ++k; + dump << i << " "; + } + } + dump << endl; + dump << "p cnf " << _variables.size()-1 << " " << needed_cls_count << endl; + for (int i = 0; i < num_init_clauses(); ++i) { + if (_clauses[i].is_needed) { + dump << "c Original Cls ID: " << i << endl; + for (unsigned j = 0; j < _clauses[i].literals.size(); ++j) { + dump << ((_clauses[i].literals[j] & 0x1)?" -":" ") + << (_clauses[i].literals[j] >> 1); + } + dump << " 0" << endl; + } + } + } + return true; +} + +bool CDatabase::verify(char * filename) { + vector buffer; + char token[WORD_LEN]; + + ifstream in_file(filename); + if (!in_file) { + cerr << "Can't open input CNF file " << filename << endl; + exit(1); + } + + while (!in_file.eof()) { + get_line(&in_file, &buffer); + char * ptr = &(*buffer.begin()); + get_token(ptr, token); + if (strcmp(token, "CL:") == 0) { + vector resolvents; + + get_token(ptr, token); + int cl_id = my_a2i(token); + + get_token(ptr, token); + assert(strcmp(token, "<=") == 0); + + while (get_token(ptr, token)) { + int r = my_a2i(token); + resolvents.push_back(r); + } + int c = add_learned_clause_by_resolvents(resolvents); + assert(c == cl_id); + } + else if (strcmp(token, "VAR:") == 0) { + get_token(ptr, token); + int vid = my_a2i(token); + + get_token(ptr, token); + assert(strcmp(token, "L:") == 0); + get_token(ptr, token); // skip the level + + get_token(ptr, token); + assert(strcmp(token, "V:") == 0); + get_token(ptr, token); + int value = my_a2i(token); + assert(value == 1 || value == 0); + + get_token(ptr, token); + assert(strcmp(token, "A:") == 0); + get_token(ptr, token); + int ante = my_a2i(token); + + get_token(ptr, token); + assert(strcmp(token, "Lits:") == 0); + + _variables[vid].value = value; + _variables[vid].antecedent = ante; + } + else if (strcmp(token, "CONF:") == 0) { + get_token(ptr, token); + _conf_id = my_a2i(token); + + get_token(ptr, token); + assert(strcmp(token, "==") == 0); + + while (get_token(ptr, token)) { + int lit = my_a2i(token); + assert(lit > 0); + assert((lit>>1) < (int)_variables.size()); + _conf_clause.push_back(lit); + } + } + } + if (_conf_id == -1) { + cerr << "No final conflicting clause defined " << endl; + exit(1); + } + cout << "Mem Usage After Readin file:\t\t" << get_mem_usage() << endl; + return real_verify(); +} + +int main(int argc, char** argv) { + cout << "ZVerify SAT Solver Verifier" << endl; + cout << "Copyright Princeton University, 2003-2004. All Right Reseverd." + << endl; + if (argc != 3 && argc !=4) { + cerr << "Usage: " << argv[0] << " CNF_File Dump_File [-core]" << endl + << "-core: dump the unsat core " << endl; + cerr << endl; + exit(1); + } + if (argc == 3) { + _dump_core = false; + } else { + assert(argc == 4); + if (strcmp(argv[3], "-core") != 0) { + cerr << "Must use -core as the third parameter" << endl; + exit(1); + } + _dump_core = true; + } + cout << "COMMAND LINE: "; + for (int i = 0; i < argc; ++i) + cout << argv[i] << " "; + cout << endl; + + _peak_mem = get_mem_usage(); + CDatabase dbase; + double begin_time = get_cpu_time(); + dbase.read_cnf(argv[1]); + if (dbase.verify(argv[2]) == true) { + double end_time = get_cpu_time(); + cout << "CPU Time:\t\t\t\t" << end_time - begin_time << endl; + cout << "Peak Mem Usage:\t\t\t\t" << _peak_mem << endl; + cout << "Verification Successful " << endl; + } else { + cout << "Failed to verify the result " << endl; + } + return 0; +}