From: bdemsky Date: Wed, 31 Dec 2014 08:46:03 +0000 (+0900) Subject: add backend for zchaff X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satlib.git;a=commitdiff_plain;h=9bdf7d18433a3c0cde7429a013ef67fe75081ec7;ds=sidebyside add backend for zchaff --- diff --git a/zchaff64/Makefile b/zchaff64/Makefile index 44c14f0..c3d88da 100644 --- a/zchaff64/Makefile +++ b/zchaff64/Makefile @@ -33,6 +33,9 @@ LIB_OBJS = $(LIB_SRCS:.cpp=.o) zchaff: $(SOLVER_OBJS) libsat.a SAT.h $(CC) $(LINKFLAGS) $(CFLAGS) $(MFLAGS) $(SOLVER_OBJS) libsat.a -o zchaff +inc_solver: inc_solver.cpp libsat.a SAT.h + $(CC) -I../ $(LINKFLAGS) $(CFLAGS) $(MFLAGS) inc_solver.cpp libsat.a -o inc_solver + zverify_df: zverify_df.cpp $(CC) $(LINKFLAGS) $(CFLAGS) $(MFLAGS) zverify_df.cpp -o zverify_df @@ -65,4 +68,4 @@ libsat.a: $(LIB_OBJS) clean: rm -f *.o libsat.a zchaff *wrapper.cpp zminimal zverify_df cnf_stats SAT_C.h -all: zchaff zverify_df zminimal cnf_stats +all: zchaff zverify_df zminimal cnf_stats inc_solver diff --git a/zchaff64/inc_solver.cpp b/zchaff64/inc_solver.cpp new file mode 100644 index 0000000..826f054 --- /dev/null +++ b/zchaff64/inc_solver.cpp @@ -0,0 +1,200 @@ +/* =========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 "SAT.h" +#include "solver_interface.h" +#include +#include +#include + +using namespace std; + + + + +static inline double cpuTime(void) { + struct rusage ru; + getrusage(RUSAGE_SELF, &ru); + return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; +} + +int *buffer; +int length; +int offset; + +int *outbuffer; +int outoffset; + +int getInt() { + if (offset>=length) { + ssize_t ptr; + offset = 0; + do { + ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE); + if (ptr == -1) + exit(-1); + } while(ptr==0); + ssize_t bytestoread=(4-(ptr & 3)) & 3; + while(bytestoread != 0) { + ssize_t p=read(0, &((char *)buffer)[ptr], bytestoread); + if (p == -1) + exit(-1); + bytestoread -= p; + ptr += p; + } + length = ptr / 4; + offset = 0; + } + + return buffer[offset++]; +} +void flushInts() { + ssize_t bytestowrite=sizeof(int)*outoffset; + ssize_t byteswritten=0; + do { + ssize_t n=write(IS_OUT_FD, &((char *)outbuffer)[byteswritten], bytestowrite); + if (n == -1) { + fprintf(stderr, "Write failure\n"); + exit(-1); + } + bytestowrite -= n; + byteswritten += n; + } while(bytestowrite != 0); + outoffset = 0; +} + +void putInt(int value) { + if (outoffset>=IS_BUFFERSIZE) { + flushInts(); + } + outbuffer[outoffset++]=value; +} + +int numvars=0; +void readClauses(SAT_Manager solver) { + vector clause; + bool haveClause = false; + while(true) { + int lit=getInt(); + if (lit!=0) { + int var = abs(lit); + while (var > numvars) { + numvars++; + SAT_AddVariable(solver); + } + int shvar=var << 1; + clause.push_back( (lit>0) ? shvar : shvar+1); + haveClause = true; + } else { + if (haveClause) { + SAT_AddClause(solver, & clause.begin()[0], clause.size()); + haveClause = false; + clause.clear(); + } else { + //done with clauses + return; + } + } + } +} +bool first=true;; + +void processCommands(SAT_Manager solver) { + while(true) { + int command=getInt(); + switch(command) { + case IS_FREEZE: { + int var=getInt(); + break; + } + case IS_RUNSOLVER: { + if (!first) { + SAT_Reset(solver); + } + first=false; + int ret = SAT_Solve(solver); + + if (ret == SATISFIABLE) { + putInt(IS_SAT); + putInt(numvars); + for(int i=1;i<=numvars;i++) { + putInt(SAT_GetVarAsgnment(solver, i)==1); + } + } else if (ret == UNSATISFIABLE) { + putInt(IS_UNSAT); + } else { + putInt(IS_INDETER); + } + flushInts(); + return; + } + default: + fprintf(stderr, "Unreconized command\n"); + exit(-1); + } + } +} +void processSAT(SAT_Manager solver) { + buffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE); + offset=0; + length=0; + outbuffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE); + outoffset=0; + + while(true) { + double initial_time = cpuTime(); + readClauses(solver); + double parse_time = cpuTime(); + processCommands(solver); + double finish_time = cpuTime(); + printf("Parse time: %12.2f s Solve time:%12.2f s\n", parse_time-initial_time, finish_time-parse_time); + } +} + + +int main(int argc, char ** argv) { + SAT_Manager mng = SAT_InitManager(); + processSAT(mng); + return 0; +}