Index: /vis_dev/glu-2.1/configure =================================================================== --- /vis_dev/glu-2.1/configure (revision 8) +++ /vis_dev/glu-2.1/configure (revision 9) @@ -7629,5 +7629,5 @@ cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1 # Files that config.status was made for. -config_files="`echo $ac_config_files`" +config_files="$ac_config_files" _ACEOF Index: /vis_dev/sharpSAT/Makefile =================================================================== --- /vis_dev/sharpSAT/Makefile (revision 9) +++ /vis_dev/sharpSAT/Makefile (revision 9) @@ -0,0 +1,153 @@ + +CXX = g++ +CXXFLAGS = -pipe -w -O3 -DGMP_BIGNUM -DCOMPILE_FOR_GUI +INCPATH = -I. -Isrc/shared -I/usr/include +LINK = g++ +LFLAGS = +LIBS = $(SUBLIBS) -L/usr/lib/ -lgmpxx -lgmp +TAR = tar -cf +GZIP = gzip -9f +COPY = cp -f +COPY_FILE= $(COPY) +COPY_DIR = $(COPY) -r +INSTALL_FILE= $(COPY_FILE) +INSTALL_DIR = $(COPY_DIR) +DEL_FILE = rm -f +SYMLINK = ln -sf +DEL_DIR = rmdir +MOVE = mv -f +CHK_DIR_EXISTS= test -d +MKDIR = mkdir -p + +####### Output directory + +OBJECTS_DIR = ./ + +####### Files + +HEADERS = src/src_sharpSAT/Basics.h \ + src/shared/SomeTime.h \ + src/shared/RealNumberTypes.h \ + src/shared/Interface/AnalyzerData.h \ + src/src_sharpSAT/MainSolver/DecisionStack.h \ + src/src_sharpSAT/MainSolver/MainSolver.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h \ + src/src_sharpSAT/MainSolver/FormulaCache.h +SOURCES = src/src_sharpSAT/Basics.cpp \ + src/shared/SomeTime.cpp \ + src/shared/RealNumberTypes.cpp \ + src/shared/Interface/AnalyzerData.cpp \ + src/src_sharpSAT/MainSolver/DecisionStack.cpp \ + src/src_sharpSAT/MainSolver/MainSolver.cpp \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.cpp \ + src/src_sharpSAT/main.cpp \ + src/src_sharpSAT/MainSolver/FormulaCache.cpp +OBJECTS = Basics.o \ + SomeTime.o \ + RealNumberTypes.o \ + AnalyzerData.o \ + DecisionStack.o \ + MainSolver.o \ + InstanceGraph.o \ + AtomsAndNodes.o \ + main.o \ + FormulaCache.o +TARGET = sharpSAT + +first: all +####### Implicit rules + +.SUFFIXES: .c .o .cpp .cc .cxx .C + +.cpp.o: + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o $@ $< + +.cc.o: + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o $@ $< + +.cxx.o: + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o $@ $< + +.C.o: + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o $@ $< + +.c.o: + $(CC) -c $(CFLAGS) $(INCPATH) -o $@ $< + +####### Build rules + +all: Makefile $(TARGET) + +$(TARGET): $(OBJECTS) + $(LINK) $(LFLAGS) -o $(TARGET) $(OBJECTS) $(LIBS) +clean: + -$(DEL_FILE) $(OBJECTS) + -$(DEL_FILE) *~ core *.core + + +####### Sub-libraries + +distclean: clean + -$(DEL_FILE) $(TARGET) $(TARGET) + + +FORCE: + +####### Compile + +Basics.o: src/src_sharpSAT/Basics.cpp src/src_sharpSAT/Basics.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o Basics.o src/src_sharpSAT/Basics.cpp + +SomeTime.o: src/shared/SomeTime.cpp src/shared/SomeTime.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o SomeTime.o src/shared/SomeTime.cpp + +RealNumberTypes.o: src/shared/RealNumberTypes.cpp src/shared/RealNumberTypes.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o RealNumberTypes.o src/shared/RealNumberTypes.cpp + +AnalyzerData.o: src/shared/Interface/AnalyzerData.cpp src/shared/Interface/AnalyzerData.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o AnalyzerData.o src/shared/Interface/AnalyzerData.cpp + +DecisionStack.o: src/src_sharpSAT/MainSolver/DecisionStack.cpp src/src_sharpSAT/MainSolver/DecisionStack.h \ + src/src_sharpSAT/Basics.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o DecisionStack.o src/src_sharpSAT/MainSolver/DecisionStack.cpp + +MainSolver.o: src/src_sharpSAT/MainSolver/MainSolver.cpp src/src_sharpSAT/MainSolver/MainSolver.h \ + src/src_sharpSAT/Basics.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h \ + src/src_sharpSAT/MainSolver/FormulaCache.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h \ + src/src_sharpSAT/MainSolver/DecisionStack.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o MainSolver.o src/src_sharpSAT/MainSolver/MainSolver.cpp + +InstanceGraph.o: src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h \ + src/src_sharpSAT/Basics.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o InstanceGraph.o src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp + +AtomsAndNodes.o: src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.cpp src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/Basics.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o AtomsAndNodes.o src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.cpp + +main.o: src/src_sharpSAT/main.cpp src/src_sharpSAT/MainSolver/MainSolver.h \ + src/src_sharpSAT/Basics.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h \ + src/src_sharpSAT/MainSolver/FormulaCache.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h \ + src/src_sharpSAT/MainSolver/DecisionStack.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o main.o src/src_sharpSAT/main.cpp + +FormulaCache.o: src/src_sharpSAT/MainSolver/FormulaCache.cpp src/src_sharpSAT/MainSolver/FormulaCache.h \ + src/src_sharpSAT/Basics.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h \ + src/src_sharpSAT/MainSolver/DecisionStack.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o FormulaCache.o src/src_sharpSAT/MainSolver/FormulaCache.cpp Index: /vis_dev/sharpSAT/Makefile_ar =================================================================== --- /vis_dev/sharpSAT/Makefile_ar (revision 9) +++ /vis_dev/sharpSAT/Makefile_ar (revision 9) @@ -0,0 +1,153 @@ + +CXX = g++ +CXXFLAGS = -pipe -O3 -w -DGMP_BIGNUM -DCOMPILE_FOR_GUI +INCPATH = -I. -Isrc/shared -I/usr/include +LINK = ar r +LFLAGS = +LIBS = $(SUBLIBS) -L/usr/lib/ -lgmpxx -lgmp +TAR = tar -cf +GZIP = gzip -9f +COPY = cp -f +COPY_FILE= $(COPY) +COPY_DIR = $(COPY) -r +INSTALL_FILE= $(COPY_FILE) +INSTALL_DIR = $(COPY_DIR) +DEL_FILE = rm -f +SYMLINK = ln -sf +DEL_DIR = rmdir +MOVE = mv -f +CHK_DIR_EXISTS= test -d +MKDIR = mkdir -p + +####### Output directory + +OBJECTS_DIR = ./ + +####### Files + +HEADERS = src/src_sharpSAT/Basics.h \ + src/shared/SomeTime.h \ + src/shared/RealNumberTypes.h \ + src/shared/Interface/AnalyzerData.h \ + src/src_sharpSAT/MainSolver/DecisionStack.h \ + src/src_sharpSAT/MainSolver/MainSolver.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h \ + src/src_sharpSAT/MainSolver/FormulaCache.h +SOURCES = src/src_sharpSAT/Basics.cpp \ + src/shared/SomeTime.cpp \ + src/shared/RealNumberTypes.cpp \ + src/shared/Interface/AnalyzerData.cpp \ + src/src_sharpSAT/MainSolver/DecisionStack.cpp \ + src/src_sharpSAT/MainSolver/MainSolver.cpp \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.cpp \ + src/src_sharpSAT/main_.cpp \ + src/src_sharpSAT/MainSolver/FormulaCache.cpp +OBJECTS = Basics.o \ + SomeTime.o \ + RealNumberTypes.o \ + AnalyzerData.o \ + DecisionStack.o \ + MainSolver.o \ + InstanceGraph.o \ + AtomsAndNodes.o \ + main_.o \ + FormulaCache.o +TARGET = sharpSAT.a + +first: all +####### Implicit rules + +.SUFFIXES: .c .o .cpp .cc .cxx .C + +.cpp.o: + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o $@ $< + +.cc.o: + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o $@ $< + +.cxx.o: + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o $@ $< + +.C.o: + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o $@ $< + +.c.o: + $(CC) -c $(CFLAGS) $(INCPATH) -o $@ $< + +####### Build rules + +all: Makefile $(TARGET) + +$(TARGET): $(OBJECTS) + $(LINK) $(LFLAGS) $(TARGET) $(OBJECTS) $(LIBS) +clean: + -$(DEL_FILE) $(OBJECTS) + -$(DEL_FILE) *~ core *.core + + +####### Sub-libraries + +distclean: clean + -$(DEL_FILE) $(TARGET) $(TARGET) + + +FORCE: + +####### Compile + +Basics.o: src/src_sharpSAT/Basics.cpp src/src_sharpSAT/Basics.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o Basics.o src/src_sharpSAT/Basics.cpp + +SomeTime.o: src/shared/SomeTime.cpp src/shared/SomeTime.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o SomeTime.o src/shared/SomeTime.cpp + +RealNumberTypes.o: src/shared/RealNumberTypes.cpp src/shared/RealNumberTypes.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o RealNumberTypes.o src/shared/RealNumberTypes.cpp + +AnalyzerData.o: src/shared/Interface/AnalyzerData.cpp src/shared/Interface/AnalyzerData.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o AnalyzerData.o src/shared/Interface/AnalyzerData.cpp + +DecisionStack.o: src/src_sharpSAT/MainSolver/DecisionStack.cpp src/src_sharpSAT/MainSolver/DecisionStack.h \ + src/src_sharpSAT/Basics.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o DecisionStack.o src/src_sharpSAT/MainSolver/DecisionStack.cpp + +MainSolver.o: src/src_sharpSAT/MainSolver/MainSolver.cpp src/src_sharpSAT/MainSolver/MainSolver.h \ + src/src_sharpSAT/Basics.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h \ + src/src_sharpSAT/MainSolver/FormulaCache.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h \ + src/src_sharpSAT/MainSolver/DecisionStack.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o MainSolver.o src/src_sharpSAT/MainSolver/MainSolver.cpp + +InstanceGraph.o: src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h \ + src/src_sharpSAT/Basics.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o InstanceGraph.o src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp + +AtomsAndNodes.o: src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.cpp src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/Basics.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o AtomsAndNodes.o src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.cpp + +main_.o: src/src_sharpSAT/main.cpp src/src_sharpSAT/MainSolver/MainSolver.h \ + src/src_sharpSAT/Basics.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h \ + src/src_sharpSAT/MainSolver/FormulaCache.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h \ + src/src_sharpSAT/MainSolver/DecisionStack.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o main_.o src/src_sharpSAT/main_.cpp + +FormulaCache.o: src/src_sharpSAT/MainSolver/FormulaCache.cpp src/src_sharpSAT/MainSolver/FormulaCache.h \ + src/src_sharpSAT/Basics.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h \ + src/src_sharpSAT/MainSolver/DecisionStack.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o FormulaCache.o src/src_sharpSAT/MainSolver/FormulaCache.cpp Index: /vis_dev/sharpSAT/Makefile_nogmp =================================================================== --- /vis_dev/sharpSAT/Makefile_nogmp (revision 9) +++ /vis_dev/sharpSAT/Makefile_nogmp (revision 9) @@ -0,0 +1,153 @@ + +CXX = g++ +CXXFLAGS = -pipe -O3 -w +INCPATH = -I. -Isrc/shared -I/usr/include +LINK = g++ +LFLAGS = +LIBS = $(SUBLIBS) -L/usr/lib/ +TAR = tar -cf +GZIP = gzip -9f +COPY = cp -f +COPY_FILE= $(COPY) +COPY_DIR = $(COPY) -r +INSTALL_FILE= $(COPY_FILE) +INSTALL_DIR = $(COPY_DIR) +DEL_FILE = rm -f +SYMLINK = ln -sf +DEL_DIR = rmdir +MOVE = mv -f +CHK_DIR_EXISTS= test -d +MKDIR = mkdir -p + +####### Output directory + +OBJECTS_DIR = ./ + +####### Files + +HEADERS = src/src_sharpSAT/Basics.h \ + src/shared/SomeTime.h \ + src/shared/RealNumberTypes.h \ + src/shared/Interface/AnalyzerData.h \ + src/src_sharpSAT/MainSolver/DecisionStack.h \ + src/src_sharpSAT/MainSolver/MainSolver.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h \ + src/src_sharpSAT/MainSolver/FormulaCache.h +SOURCES = src/src_sharpSAT/Basics.cpp \ + src/shared/SomeTime.cpp \ + src/shared/RealNumberTypes.cpp \ + src/shared/Interface/AnalyzerData.cpp \ + src/src_sharpSAT/MainSolver/DecisionStack.cpp \ + src/src_sharpSAT/MainSolver/MainSolver.cpp \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.cpp \ + src/src_sharpSAT/main.cpp \ + src/src_sharpSAT/MainSolver/FormulaCache.cpp +OBJECTS = Basics.o \ + SomeTime.o \ + RealNumberTypes.o \ + AnalyzerData.o \ + DecisionStack.o \ + MainSolver.o \ + InstanceGraph.o \ + AtomsAndNodes.o \ + main.o \ + FormulaCache.o +TARGET = sharpSAT + +first: all +####### Implicit rules + +.SUFFIXES: .c .o .cpp .cc .cxx .C + +.cpp.o: + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o $@ $< + +.cc.o: + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o $@ $< + +.cxx.o: + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o $@ $< + +.C.o: + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o $@ $< + +.c.o: + $(CC) -c $(CFLAGS) $(INCPATH) -o $@ $< + +####### Build rules + +all: Makefile $(TARGET) + +$(TARGET): $(OBJECTS) + $(LINK) $(LFLAGS) -o $(TARGET) $(OBJECTS) $(LIBS) +clean: + -$(DEL_FILE) $(OBJECTS) + -$(DEL_FILE) *~ core *.core + + +####### Sub-libraries + +distclean: clean + -$(DEL_FILE) $(TARGET) $(TARGET) + + +FORCE: + +####### Compile + +Basics.o: src/src_sharpSAT/Basics.cpp src/src_sharpSAT/Basics.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o Basics.o src/src_sharpSAT/Basics.cpp + +SomeTime.o: src/shared/SomeTime.cpp src/shared/SomeTime.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o SomeTime.o src/shared/SomeTime.cpp + +RealNumberTypes.o: src/shared/RealNumberTypes.cpp src/shared/RealNumberTypes.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o RealNumberTypes.o src/shared/RealNumberTypes.cpp + +AnalyzerData.o: src/shared/Interface/AnalyzerData.cpp src/shared/Interface/AnalyzerData.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o AnalyzerData.o src/shared/Interface/AnalyzerData.cpp + +DecisionStack.o: src/src_sharpSAT/MainSolver/DecisionStack.cpp src/src_sharpSAT/MainSolver/DecisionStack.h \ + src/src_sharpSAT/Basics.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o DecisionStack.o src/src_sharpSAT/MainSolver/DecisionStack.cpp + +MainSolver.o: src/src_sharpSAT/MainSolver/MainSolver.cpp src/src_sharpSAT/MainSolver/MainSolver.h \ + src/src_sharpSAT/Basics.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h \ + src/src_sharpSAT/MainSolver/FormulaCache.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h \ + src/src_sharpSAT/MainSolver/DecisionStack.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o MainSolver.o src/src_sharpSAT/MainSolver/MainSolver.cpp + +InstanceGraph.o: src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h \ + src/src_sharpSAT/Basics.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o InstanceGraph.o src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp + +AtomsAndNodes.o: src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.cpp src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/Basics.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o AtomsAndNodes.o src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.cpp + +main.o: src/src_sharpSAT/main.cpp src/src_sharpSAT/MainSolver/MainSolver.h \ + src/src_sharpSAT/Basics.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h \ + src/src_sharpSAT/MainSolver/FormulaCache.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h \ + src/src_sharpSAT/MainSolver/DecisionStack.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o main.o src/src_sharpSAT/main.cpp + +FormulaCache.o: src/src_sharpSAT/MainSolver/FormulaCache.cpp src/src_sharpSAT/MainSolver/FormulaCache.h \ + src/src_sharpSAT/Basics.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h \ + src/src_sharpSAT/MainSolver/DecisionStack.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h \ + src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h + $(CXX) -c $(CXXFLAGS) $(INCPATH) -o FormulaCache.o src/src_sharpSAT/MainSolver/FormulaCache.cpp Index: /vis_dev/sharpSAT/README =================================================================== --- /vis_dev/sharpSAT/README (revision 9) +++ /vis_dev/sharpSAT/README (revision 9) @@ -0,0 +1,11 @@ +sharpSAT version 1.1 + +To compile this version of sharpSAT simply run + +make + +Note that this only works, if you have gmp installed. sharpSAT uses GMP to store the model counting results with infinite precision. + +If you do not want to use infinite precsision numbers in sharpSAT you simply have to use +Makefile_nogmp instead of the standard Makefile. + Index: /vis_dev/sharpSAT/res_sat =================================================================== --- /vis_dev/sharpSAT/res_sat (revision 9) +++ /vis_dev/sharpSAT/res_sat (revision 9) @@ -0,0 +1,1 @@ +100657278205558784 Index: /vis_dev/sharpSAT/semantic.cache =================================================================== --- /vis_dev/sharpSAT/semantic.cache (revision 9) +++ /vis_dev/sharpSAT/semantic.cache (revision 9) @@ -0,0 +1,15 @@ +;; Object sharpSAT/ +;; SEMANTICDB Tags save file +(semanticdb-project-database-file "sharpSAT/" + :tables (list + (semanticdb-table "Makefile" + :major-mode 'makefile-gmake-mode + :tags '(("CXX" variable (:default-value ("g++")) nil [2 18]) ("CXXFLAGS" variable (:default-value ("-pipe" "-O3" "-w" "-DGMP_BIGNUM" "-DCOMPILE_FOR_GUI")) nil [18 74]) ("INCPATH" variable (:default-value ("-I." "-Isrc/shared" "-I/usr/include")) nil [74 119]) ("LINK" variable (:default-value ("ar" "r")) nil [119 135]) ("LFLAGS" variable nil nil [135 147]) ("LIBS" variable (:default-value ("$(SUBLIBS)" "-L/usr/lib/" "-lgmpxx" "-lgmp")) nil [147 196]) ("TAR" variable (:default-value ("tar" "-cf")) nil [196 215]) ("GZIP" variable (:default-value ("gzip" "-9f")) nil [215 235]) ("COPY" variable (:default-value ("cp" "-f")) nil [235 252]) ("COPY_FILE" variable (:default-value ("$(COPY)")) nil [252 271]) ("COPY_DIR" variable (:default-value ("$(COPY)" "-r")) nil [271 293]) ("INSTALL_FILE" variable (:default-value ("$(COPY_FILE)")) nil [293 320]) ("INSTALL_DIR" variable (:default-value ("$(COPY_DIR)")) nil [320 346]) ("DEL_FILE" variable (:default-value ("rm" "-f")) nil [346 363]) ("SYMLINK" variable (:default-value ("ln" "-sf")) nil [363 381]) ("DEL_DIR" variable (:default-value ("rmdir")) nil [381 398]) ("MOVE" variable (:default-value ("mv" "-f")) nil [398 415]) ("CHK_DIR_EXISTS" variable (:default-value ("test" "-d")) nil [415 439]) ("MKDIR" variable (:default-value ("mkdir" "-p")) nil [439 459]) ("OBJECTS_DIR" variable (:default-value ("./")) nil [486 503]) ("HEADERS" variable (:default-value ("src/src_sharpSAT/Basics.h" "src/shared/SomeTime.h" "src/shared/RealNumberTypes.h" "src/shared/Interface/AnalyzerData.h" "src/src_sharpSAT/MainSolver/DecisionStack.h" "src/src_sharpSAT/MainSolver/MainSolver.h" "src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h" "src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h" "src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h" "src/src_sharpSAT/MainSolver/FormulaCache.h")) nil [519 981]) ("SOURCES" variable (:default-value ("src/src_sharpSAT/Basics.cpp" "src/shared/SomeTime.cpp" "src/shared/RealNumberTypes.cpp" "src/shared/Interface/AnalyzerData.cpp" "src/src_sharpSAT/MainSolver/DecisionStack.cpp" "src/src_sharpSAT/MainSolver/MainSolver.cpp" "src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp" "src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.cpp" "src/src_sharpSAT/main_.cpp" "src/src_sharpSAT/MainSolver/FormulaCache.cpp")) nil [981 1429]) ("OBJECTS" variable (:default-value ("Basics.o" "SomeTime.o" "RealNumberTypes.o" "AnalyzerData.o" "DecisionStack.o" "MainSolver.o" "InstanceGraph.o" "AtomsAndNodes.o" "main_.o" "FormulaCache.o")) nil [1429 1612]) ("TARGET" variable (:default-value ("sharpSAT.a")) nil [1612 1634]) ("first" function (:arguments ("all")) nil [1635 1669]) (".SUFFIXES" function (:arguments (".c" ".o" ".cpp" ".cc" ".cxx" ".C")) nil [1670 1705]) (".cpp.o" function nil nil [1705 1757]) (".cc.o" function nil nil [1757 1808]) (".cxx.o" function nil nil [1808 1860]) (".C.o" function nil nil [1860 1910]) (".c.o" function nil nil [1910 1957]) ("all" function (:arguments ("Makefile" "$(TARGET)")) nil [1978 2003]) ("$(TARGET)" function (:arguments ("$(OBJECTS)")) nil [2003 2080]) ("clean" function nil nil [2075 2137]) ("distclean" function (:arguments ("clean")) nil [2161 2213]) ("FORCE" function nil nil [2214 2222]) ("Basics.o" function (:arguments ("src/src_sharpSAT/Basics.cpp" "src/src_sharpSAT/Basics.h")) nil [2239 2378]) ("SomeTime.o" function (:arguments ("src/shared/SomeTime.cpp" "src/shared/SomeTime.h")) nil [2378 2509]) ("RealNumberTypes.o" function (:arguments ("src/shared/RealNumberTypes.cpp" "src/shared/RealNumberTypes.h")) nil [2509 2675]) ("AnalyzerData.o" function (:arguments ("src/shared/Interface/AnalyzerData.cpp" "src/shared/Interface/AnalyzerData.h")) nil [2675 2856]) ("DecisionStack.o" function (:arguments ("src/src_sharpSAT/MainSolver/DecisionStack.cpp" "src/src_sharpSAT/MainSolver/DecisionStack.h" "src/src_sharpSAT/Basics.h" "src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h" "src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h" "src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h")) nil [2856 3280]) ("MainSolver.o" function (:arguments ("src/src_sharpSAT/MainSolver/MainSolver.cpp" "src/src_sharpSAT/MainSolver/MainSolver.h" "src/src_sharpSAT/Basics.h" "src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h" "src/src_sharpSAT/MainSolver/FormulaCache.h" "src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h" "src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h" "src/src_sharpSAT/MainSolver/DecisionStack.h")) nil [3280 3784]) ("InstanceGraph.o" function (:arguments ("src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp" "src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h" "src/src_sharpSAT/Basics.h" "src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h")) nil [3784 4125]) ("AtomsAndNodes.o" function (:arguments ("src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.cpp" "src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h" "src/src_sharpSAT/Basics.h")) nil [4125 4404]) ("main_.o" function (:arguments ("src/src_sharpSAT/main.cpp" "src/src_sharpSAT/MainSolver/MainSolver.h" "src/src_sharpSAT/Basics.h" "src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h" "src/src_sharpSAT/MainSolver/FormulaCache.h" "src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h" "src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h" "src/src_sharpSAT/MainSolver/DecisionStack.h")) nil [4404 4865]) ("FormulaCache.o" function (:arguments ("src/src_sharpSAT/MainSolver/FormulaCache.cpp" "src/src_sharpSAT/MainSolver/FormulaCache.h" "src/src_sharpSAT/Basics.h" "src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h" "src/src_sharpSAT/MainSolver/DecisionStack.h" "src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h" "src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h")) nil [4865 5331])) + :file "Makefile" + :pointmax 5331 + ) + ) + :file "semantic.cache" + :semantic-tag-version "2.0beta3" + :semanticdb-version "2.0beta3" + ) Index: /vis_dev/sharpSAT/src/src_sharpSAT/Basics.cpp =================================================================== --- /vis_dev/sharpSAT/src/src_sharpSAT/Basics.cpp (revision 9) +++ /vis_dev/sharpSAT/src/src_sharpSAT/Basics.cpp (revision 9) @@ -0,0 +1,27 @@ +#include "Basics.h" + + +bool CSolverConf::analyzeConflicts = true; +bool CSolverConf::doNonChronBackTracking = true; + +bool CSolverConf::allowComponentCaching = true; +bool CSolverConf::allowImplicitBCP = true; + +bool CSolverConf::allowPreProcessing = true; + +bool CSolverConf::quietMode = false; + +unsigned int CSolverConf::secsTimeBound = 10000000; + +unsigned int CSolverConf::maxCacheSize = 0; +bool CSolverConf::count = true; + +char TriValuetoChar(TriValue v){ + switch(v){ + case W: return '1'; + case F: return '0'; + case X: return '.'; + }; + return '.'; + } + Index: /vis_dev/sharpSAT/src/src_sharpSAT/Basics.h =================================================================== --- /vis_dev/sharpSAT/src/src_sharpSAT/Basics.h (revision 9) +++ /vis_dev/sharpSAT/src/src_sharpSAT/Basics.h (revision 9) @@ -0,0 +1,74 @@ +#ifndef _BASICS_H +#define _BASICS_H + + +#include +#include +#include + +using namespace std; + + +class CSolverConf +{ +public: + static bool analyzeConflicts; + static bool doNonChronBackTracking; + + static bool quietMode; + + static bool allowComponentCaching; + static bool allowImplicitBCP; + + static bool allowPreProcessing; + + static unsigned int secsTimeBound; + + static unsigned int maxCacheSize; // maximum Cache Size in bytes + + static bool count; + + CSolverConf(); + + ~CSolverConf(); + +}; + +#ifdef COMPILE_FOR_GUI + #define toSTDOUT(X); +#else + #define toSTDOUT(X) if(!CSolverConf::quietMode) cout << X; +#endif + + +#ifdef COMPILE_FOR_GUI + #define toERROUT(X); +#else + #define toERROUT(X) if(!CSolverConf::quietMode) cout << X; +#endif + +#ifdef DEBUG + #define toDEBUGOUT(X) if(!CSolverConf::quietMode) cout << X; +#else + #define toDEBUGOUT(X); +#endif + + +enum SOLVER_StateT{ + + SUCCESS, + TIMEOUT, + ABORTED +}; + +enum TriValue{ + + F = 0, + W = 1, + X = 2 + }; + + + +extern char TriValuetoChar(TriValue v); +#endif Index: /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/DecisionStack.cpp =================================================================== --- /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/DecisionStack.cpp (revision 9) +++ /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/DecisionStack.cpp (revision 9) @@ -0,0 +1,115 @@ +#include "DecisionStack.h" + + + +void CDecisionStack::reactivateTOS() +{ + for(vector::const_iterator it = TOS_ImpliedLits_begin();it != TOS_ImpliedLits_end();it++) + { + theClPool.getVar(*it).unsetVal(); + } +} + +bool CDecisionStack::flipTOS() +{ + if(getDL() <= 0) return false; + if (top().isFlipped()) return false; // es wurde schonmal geflippt + + top().flipped = true; + + reactivateTOS(); + allImpliedLits.resize(top().iImpLitOfs); + storeTOSCachedChildren(); + top().iEndRemComps = top().iRemCompOfs; + + while(allComponentsStack.size() > top().iRemCompOfs) + { + delete allComponentsStack.back(); + allComponentsStack.pop_back(); + } + return true; +} + +bool CDecisionStack::storeTOSCachedChildren() +{ + vector::iterator it = allComponentsStack.begin() +top().iRemCompOfs; + for(;it != allComponentsStack.end(); it++) + { + if((*it)->cachedAs != 0) allComponentsStack[top().refCompId]->cachedChildren.push_back((*it)->cachedAs); + + } + return true; +} + +bool CDecisionStack::pop() +{ + if(getDL() <= 0) return false; + + reactivateTOS(); + allImpliedLits.resize(top().iImpLitOfs); + storeTOSCachedChildren(); + + while(allComponentsStack.size() > top().iRemCompOfs) + { + delete allComponentsStack.back(); + allComponentsStack.pop_back(); + } + + (end()-2)->includeSol(top().getOverallSols()); + + pop_back(); + return true; +} + + +void CDecisionStack::push() +{ + push_back(CDecision()); + + top().refCompId = (end()-2)->iEndRemComps-1; + (end()-2)->popRemComp(); + + top().iImpLitOfs = allImpliedLits.size(); + top().iRemCompOfs = allComponentsStack.size(); + top().iEndRemComps = allComponentsStack.size(); +} + + +void CDecisionStack::init(unsigned int resSize) +{ + clear(); + reserve(resSize); + allImpliedLits.clear(); + allImpliedLits.reserve(theClPool.countAllVars()); + allComponentsStack.clear(); + allComponentsStack.reserve(theClPool.countAllVars()); + allComponentsStack.push_back(new CComponentId()); + + // initialize the stack to contain at least level zero + push_back(CDecision()); + back().flipped = true; + top().iRemCompOfs = 1; + top().iEndRemComps = 1; + addToDecLev = 0; +} + +void CDecisionStack::TOS_sortRemComps() +{ + CComponentId * vBuf; + vector &keys = allComponentsStack; + + int uLower = top().iRemCompOfs; + int uUpper = top().iEndRemComps-1; + + + for(int i = uLower; i <=uUpper;i++) + for(int j = i+1; j <=uUpper;j++) + { + if(keys[i]->countVars() < keys[j]->countVars()) + { + vBuf = keys[i]; + keys[i] = keys[j]; + keys[j] = vBuf; + } + } +} Index: /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/DecisionStack.h =================================================================== --- /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/DecisionStack.h (revision 9) +++ /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/DecisionStack.h (revision 9) @@ -0,0 +1,243 @@ +#ifndef DECISIONSTACK_H +#define DECISIONSTACK_H + +#include + +#ifdef DEBUG +#include +#endif + +#include + +#include "../Basics.h" + +#include "InstanceGraph/ComponentTypes.h" +#include "InstanceGraph/AtomsAndNodes.h" +#include "InstanceGraph/InstanceGraph.h" + +using namespace std; + +/** \addtogroup Interna*/ +/*@{*/ + + +class CDecision +{ + //////////////////// + /// active Component + //////////////////// + unsigned int refCompId; + + // branch + bool flipped; + + // bcp + unsigned int iImpLitOfs; + + // Solutioncount + CRealNum rnNumSols[2]; + + //////////////////// + /// remaining Components + //////////////////// + + /** + * [iRemCompOfs,iEndRemComps) defines the interval in allComponentsStack + * where the child components of the [refCompId] component are stored + */ + unsigned int iRemCompOfs; + unsigned int iEndRemComps; + + //this function only to be used by decisionStack + unsigned int countCompsToProcess() + { + #ifdef DEBUG + assert(iEndRemComps >= iRemCompOfs); + #endif + return iEndRemComps - iRemCompOfs; + } + void popRemComp() + { + #ifdef DEBUG + assert(iEndRemComps >= iRemCompOfs); + #endif + iEndRemComps--; + } + + public: + + CDecision() + { + flipped = false; + rnNumSols[0] = 0.0; + rnNumSols[1] = 0.0; + refCompId = 0; + iImpLitOfs = (unsigned int) -1; + iRemCompOfs = (unsigned int) -1; + iEndRemComps = (unsigned int) -1; + } + + ~CDecision(){} + + bool isFlipped(){return flipped;} + bool anotherCompProcessible() + { + return getBranchSols() !=0.0 && countCompsToProcess() > 0; + } + + void includeSol(const CRealNum &rnCodedSols) + { + if(rnNumSols[flipped] == 0.0) rnNumSols[flipped] = rnCodedSols; + else + rnNumSols[flipped] *= rnCodedSols; + } + + const CRealNum &getBranchSols() const + { + return rnNumSols[flipped]; + } + + const CRealNum getOverallSols() const + { + return rnNumSols[0] + rnNumSols[1]; + } + + friend class CDecisionStack; +}; + + +class CDecisionStack : vector +{ + CInstanceGraph &theClPool; + + vector allImpliedLits; + + vector allComponentsStack; + + void reactivateTOS(); + + // store each cacheEntry where the children of top().refComp are stored + bool storeTOSCachedChildren(); + + unsigned int addToDecLev; + public: + /// + const vector & getAllCompStack() {return allComponentsStack;} + + + vector::iterator TOSRemComps_begin() {return allComponentsStack.begin() + top().iRemCompOfs;} + + CDecisionStack(CInstanceGraph &pool):theClPool(pool){addToDecLev = 0;} + + ~CDecisionStack(){} + + //begin for implicit BCP + void beginTentative() {addToDecLev = 1;} + void endTentative() {addToDecLev = 0;} + //end for implicit BCP + + bool pop(); + void push(); + + inline CDecision &top() {return back();} + + bool flipTOS(); + + unsigned int countAllImplLits() + { + return allImpliedLits.size(); + } + + void shrinkImplLitsTo(unsigned int sz) + { + if(sz >= allImpliedLits.size()) return; + allImpliedLits.resize(sz); + } + + int TOS_siblingsProcessed() + { + #ifdef DEBUG + assert(allComponentsStack.size() >= top().iEndRemComps); + #endif + return (int) allComponentsStack.size() - (int) top().iEndRemComps; + } + + unsigned int TOS_countImplLits() + { + return allImpliedLits.size() - top().iImpLitOfs; + } + + + const LiteralIdT &TOS_decLit() const + { + return allImpliedLits[back().iImpLitOfs]; + } + + void TOS_addImpliedLit(LiteralIdT aLit) + { + allImpliedLits.push_back(aLit); + } + + void TOS_popImpliedLit() + { + allImpliedLits.pop_back(); + } + + vector::const_iterator TOS_ImpliedLits_begin() + { + return allImpliedLits.begin() + top().iImpLitOfs; + } + + vector::const_iterator TOS_ImpliedLits_end() + { + return allImpliedLits.end(); + } + + + CComponentId & TOSRefComp() + { + #ifdef DEBUG + assert(top().refCompId < allComponentsStack.size()); + #endif + return *allComponentsStack[top().refCompId]; + } + + bool TOS_hasAnyRemComp() + { + return allComponentsStack.size() > top().iRemCompOfs; + } + + void TOS_popRemComp(){top().popRemComp();} + + unsigned int TOS_countRemComps() {return top().countCompsToProcess();} + + void TOS_addRemComp() + { + allComponentsStack.push_back(new CComponentId()); + top().iEndRemComps = allComponentsStack.size(); + } + + CComponentId & TOS_NextComp() + { + #ifdef DEBUG + assert(top().iEndRemComps <= allComponentsStack.size()); + assert(allComponentsStack[top().iEndRemComps -1] != NULL); + #endif + return *allComponentsStack[top().iEndRemComps - 1]; + } + + void TOS_sortRemComps(); + + CComponentId & lastComp() {return *allComponentsStack.back();} + + void printStats(); + + inline int getDL() const{return size()-1+addToDecLev;} // 0 means pre-1st-decision + + void init(unsigned int resSize = 1); +}; + +/*@}*/ + +#endif + Index: /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/FormulaCache.cpp =================================================================== --- /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/FormulaCache.cpp (revision 9) +++ /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/FormulaCache.cpp (revision 9) @@ -0,0 +1,269 @@ +#include "FormulaCache.h" + +unsigned int CFormulaCache::oldestEntryAllowed = (unsigned int) -1; + + +CFormulaCache::CFormulaCache() +{ + iBuckets = 900001;// =299999; + theData.resize(iBuckets,NULL); + theBucketBase.reserve(iBuckets); + theEntryBase.reserve(iBuckets*10); + scoresDivTime = 50000; + lastDivTime = 0; + #ifdef SUN_OS + if(CSolverConf::maxCacheSize == 0) + CSolverConf::maxCacheSize = 100*1024*1024; + #endif + #ifndef SUN_OS + if(CSolverConf::maxCacheSize == 0) + { + int pgs = getpagesize(); + long int pages = get_avphys_pages(); + CSolverConf::maxCacheSize = (pgs*pages)/2; + } + #endif +} + + + +bool CFormulaCache::include(CComponentId &rComp, const CRealNum &val) +{ + #ifdef DEBUG + // if everything is correct, a new value to be cached + // should not already be stored in the cache + assert(rComp.cachedAs == NIL_ENTRY); + #endif + + if(rComp.empty()) return false; + iCacheTries++; + + if(memUsage >= CSolverConf::maxCacheSize) return false; + + long unsigned int hV = rComp.getHashKey(); + + CCacheBucket &rBucket = at(clip(hV)); + + + CacheEntryId eId = newEntry(); + CCacheEntry & rEntry = entry(eId); + rBucket.push_back(eId); + rEntry.createFrom(rComp); + rEntry.hashKey = hV; + rEntry.theVal = val; + + rComp.cachedAs = eId; // save in the Comp, wwhere it was saved + rEntry.theDescendants = rComp.cachedChildren; // save the cache ids of its children + + rComp.cachedChildren.clear(); + + adjustDescendantsFather(eId); + + + //BEGIN satistics + + unsigned int memU = memUsage/(10*1024*1024); + + memUsage += rEntry.memSize(); + + if(memU < memUsage/(10*1024*1024)) + { + toSTDOUT("Cache: usedMem "<< memUsage<<"Bytes\n"); + } + iSumCachedCompSize += rComp.countVars(); + + iCachedComponents++; + if(iCachedComponents % 50000 == 0) + { + double d = iSumCachedCompSize; + d /= (double) iCachedComponents; + toSTDOUT("cachedComponents:"<< iCachedComponents<<" avg. size:"<getHashKey() && pComp->equals(rComp)) + { + val = pComp->theVal; + pComp->score++; + pComp->score+= (unsigned int)pComp->sizeVarVec(); + + iCacheRetrievals++; + iSumRetrieveSize += rComp.countVars(); + + if(iCacheRetrievals % 50000 == 0) + { + double d = iSumRetrieveSize; + d /= (double) iCacheRetrievals; + toSTDOUT("cache hits:"<< iCacheRetrievals<<" avg size:"<< d<::iterator it;// theDescendants; + CCacheBucket &rBuck = at(clip(entry(root).hashKey)); + unsigned int n = 0; + + + for(CCacheBucket::iterator jt= rBuck.begin(); jt != rBuck.end(); jt++) + { + if(*jt == root) + { + rBuck.erase(jt); + n++; + break; + } + } + + for(it = entry(root).theDescendants.begin(); it != entry(root).theDescendants.end(); it++) + { + n += removePollutedEntries(*it); + } + + entry(root).clear(); + + return n; +} + +bool CFormulaCache::deleteEntries(CDecisionStack & rDecStack) +{ + vector::iterator jt; + vector::iterator it,itWrite; + CCacheBucket::iterator bt; + + if(memUsage < (unsigned int) ((double) 0.85* (double)CSolverConf::maxCacheSize)) return false; + + // first : go through the EntryBase and mark the entries to be deleted as deleted (i.e. EMPTY + for(it = beginEntries(); it != endEntries(); it++) + { + if(it->score <= minScoreBound) + { + deleteFromDescendantsTree(toCacheEntryId(it)); + it->clear(); + } + } + + // then go through the BucketBase and rease all Links to empty entries + for(jt = theBucketBase.begin(); jt != theBucketBase.end(); jt++) + { + for(bt = jt->end()-1; bt != jt->begin()-1; bt--) + { + if(entry(*bt).empty()) bt = jt->erase(bt); + } + } + + // now: go through the decisionStack. and delete all Links to empty entries + revalidateCacheLinksIn(rDecStack.getAllCompStack()); + + // finally: truly erase the empty entries, but keep the descendants tree consistent + long int newSZ = 0; + long int SumNumOfVars= 0; + CacheEntryId idOld,idNew; + + itWrite = beginEntries(); + for(it = beginEntries(); it != endEntries(); it++) + { + if(!it->empty()) + { + if(it != itWrite) + { + *itWrite = *it; + idNew = toCacheEntryId(itWrite); + idOld = toCacheEntryId(it); + at(clip(itWrite->getHashKey())).substituteIds(idOld,idNew); + substituteInDescTree(idOld,idNew); + substituteCacheLinksIn(rDecStack.getAllCompStack(),idOld,idNew); + } + itWrite++; + //theEntryBase.pop_back(); + newSZ += itWrite->memSize(); + SumNumOfVars += itWrite->sizeVarVec(); + } + } + + theEntryBase.erase(itWrite,theEntryBase.end()); + + iCachedComponents = theEntryBase.size(); + iSumCachedCompSize = SumNumOfVars*sizeof(unsigned int)*8 / CCacheEntry::bitsPerVar(); + + memUsage = newSZ; + + toSTDOUT("Cache cleaned: "<>10)<< " KB remain"< (unsigned int) dbound) + { + minScoreBound <<= 1; + minScoreBound++; + scoresDivTime /= 2; + if(scoresDivTime < 50000) scoresDivTime = 50000; + } + toDEBUGOUT("setting scoresDivTime: "< &rComps) +{ + vector::const_iterator it; + vector::iterator jt; + for(it = rComps.begin(); it !=rComps.end(); it++) + { + if(!isEntry((*it)->cachedAs)) (*it)->cachedAs = 0; + + if(isEntry((*it)->cachedAs) && entry((*it)->cachedAs).empty()) (*it)->cachedAs = 0; + + for(jt = (*it)->cachedChildren.end()-1; jt != (*it)->cachedChildren.begin()-1; jt--) + { + if((!isEntry(*jt)) || entry(*jt).empty()) + { + toDEBUGOUT("_E"); + jt =(*it)->cachedChildren.erase(jt); + } + } + } +} + + +void CFormulaCache::substituteCacheLinksIn(const vector &rComps, CacheEntryId idOld, CacheEntryId idNew) +{ + vector::const_iterator it; + vector::iterator jt; + for(it = rComps.begin(); it !=rComps.end(); it++) + { + if((*it)->cachedAs == idOld) (*it)->cachedAs = idNew; + for(jt = (*it)->cachedChildren.begin(); jt != (*it)->cachedChildren.end(); jt++) + { + if(*jt == idOld){ toDEBUGOUT("_D"); *jt = idNew;} + } + } +} Index: /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/FormulaCache.h =================================================================== --- /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/FormulaCache.h (revision 9) +++ /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/FormulaCache.h (revision 9) @@ -0,0 +1,397 @@ +#ifndef FORMULACACHE_H +#define FORMULACACHE_H + + +#ifdef DEBUG +#include +#endif + +#include +#include +#include + + +#include +#include +#include + + +#include "../Basics.h" +#include "InstanceGraph/ComponentTypes.h" +#include "DecisionStack.h" +using namespace std; + +typedef unsigned int CacheEntryId; + +class CCacheEntry : public CPackedCompId +{ + long unsigned int hashKey; + friend class CFormulaCache; + + // theFather and theDescendants: + // each CCacheEntry is a Node in a tree which represents the relationship + // of the components stored + CacheEntryId theFather; + vector theDescendants; + + public: + + CRealNum theVal; + + unsigned int score; + + CCacheEntry() + { + score = 0; + theFather = 0; + } + + + void clear() + { + theVars.clear(); + theClauses.clear(); + theDescendants.clear(); + } + + + ~CCacheEntry() + { + theDescendants.clear(); + theFather = 0; + clear(); + } + + + long unsigned int getHashKey() const + { + return hashKey; + } + + void setHashKey(long unsigned int &val) + { + hashKey = val; + } + + unsigned int memSize() + { + return CPackedCompId::memSize() + theDescendants.capacity()*sizeof(CacheEntryId); + } + + void substituteDescendant(CacheEntryId iold, CacheEntryId inew) + { + vector::iterator it; + for(it = theDescendants.begin();it != theDescendants.end();it++) + { + if(*it == iold) *it = inew; + } + } + + void removeDescendant(CacheEntryId d) + { + vector::iterator it; + for(it = theDescendants.end()-1;it != theDescendants.begin()-1;it--) + { + if(*it == d) + { + it = theDescendants.erase(it); + } + } + } + + + void addDescendants(vector &dVec) + { + theDescendants.insert(theDescendants.end(),dVec.begin(),dVec.end()); + } + + CacheEntryId getFather() {return theFather;} + void substituteFather(CacheEntryId newFather){theFather = newFather;} + + +}; + + +class CCacheBucket : protected vector +{ + friend class CFormulaCache; + + + public: + + CCacheBucket() + { + } + + ~CCacheBucket() + { + clear(); + } + + bool substituteIds(CacheEntryId oldId, CacheEntryId newId) + { + for(CCacheBucket::iterator it = begin(); it != end(); it++) + { + if(*it == oldId) { *it = newId; return true;} + } + return false; + } + + using vector::size; +}; + +class CFormulaCache +{ + vector theBucketBase; + + vector theEntryBase; + + #define NIL_ENTRY 0 + + vector theData; + + vector::iterator beginEntries(){return theEntryBase.begin()+1;} + vector::iterator endEntries(){return theEntryBase.end();} + + CacheEntryId toCacheEntryId(vector::iterator &it) + { + return (CacheEntryId)(it - theEntryBase.begin()); + } + + + unsigned int iBuckets; + static unsigned int oldestEntryAllowed; + /* statistics */ + unsigned int iCacheRetrievals; + unsigned int iSumRetrieveSize; + unsigned int iCacheTries; + + unsigned int iCachedComponents; + unsigned int iSumCachedCompSize; + unsigned int iSumCachedMemSize; + unsigned int iUsedBuckets; + unsigned int scoresDivTime; + unsigned int minScoreBound; + + unsigned int lastDivTime; + + /*end statistics */ + unsigned int memUsage; + //unsigned int maxMemUsage; + + double avgCachedSize() + { + if(iCacheRetrievals == 0) return 0.0; + return (double) iSumCachedCompSize / (double) iCachedComponents; + } + + double avgCachedMemSize() + { + if(iCacheRetrievals == 0) return 0.0; + return (double) memUsage / (double) iCachedComponents; + } + + double avgHitSize() + { + if(iCacheRetrievals == 0) return 0.0; + return (double) iSumRetrieveSize / (double) iCacheRetrievals; + } + + unsigned int clip(unsigned int ofs) + { + return ofs % iBuckets; + } + + unsigned int clip(long unsigned int ofs) + { + return ofs % iBuckets; + } + + bool isEntry(CacheEntryId theId) + { + return (theId != 0) & (theId < theEntryBase.size()); + } + + CCacheEntry &entry(CacheEntryId theId) + { + #ifdef DEBUG + assert(theId < theEntryBase.size()); + #endif + return theEntryBase[theId]; + } + + CacheEntryId newEntry() + { + theEntryBase.push_back(CCacheEntry()); + return theEntryBase.size()-1; + } + + unsigned int memSizeOf(CCacheBucket &rBuck) + { + unsigned int n = 0; + for(CCacheBucket::iterator it = rBuck.begin();it!= rBuck.end();it++) + { + n += entry(*it).memSize(); + } + return n; + } + + CCacheBucket *createNewCacheBucket() + { + theBucketBase.push_back(CCacheBucket()); + iUsedBuckets++; + return &theBucketBase.back(); + } + + CCacheBucket &at(unsigned int ofs) + { + if(theData[ofs] == NULL) theData[ofs] = createNewCacheBucket(); + return *theData[ofs]; + } + + bool isBucketAt(unsigned int ofs) + { + #ifdef DEBUG + assert(theData.size() > ofs); + #endif + return theData[ofs] != NULL; + } + + public: + + unsigned int getScoresDivTime() {return scoresDivTime;} + unsigned int getLastDivTime() {return lastDivTime;} + void setLastDivTime(unsigned int d) {lastDivTime = d;} + + CFormulaCache(); + + ~CFormulaCache() + { + reset(); + } + + void init() + { + theBucketBase.clear(); + theData.clear(); + theEntryBase.clear(); + theEntryBase.push_back(CCacheEntry()); // dummy Element + theData.resize(iBuckets,NULL); + theBucketBase.reserve(iBuckets); + iUsedBuckets = 0; + memUsage = 0; + iCachedComponents = 0; + iCacheRetrievals = 0; + iSumRetrieveSize = 0; + iSumCachedCompSize = 0; + iSumCachedMemSize = 0; + iCacheTries = 0; + minScoreBound = 0; + } + + void reset() + { + theBucketBase.clear(); + theEntryBase.clear(); + theData.clear(); + } + + void printStatistics(CRunAnalyzer & rAn) + { + rAn.setValue(FCACHE_MAXMEM,CSolverConf::maxCacheSize); // Formula Cache Memory Bound + rAn.setValue(FCACHE_MEMUSE,memUsage); // Formula Cache memory usage + rAn.setValue(FCACHE_USEDBUCKETS,iUsedBuckets); // number of hashbuckets used + rAn.setValue(FCACHE_CACHEDCOMPS,iCachedComponents); + rAn.setValue(FCACHE_RETRIEVALS,iCacheRetrievals); // number of retrieved components + rAn.setValue(FCACHE_INCLUDETRIES,iCacheTries); // number of times it was tried to put a component into the cache + + } + + void divCacheScores() + { + for(vector::iterator it = theEntryBase.begin(); it != theEntryBase.end(); it++) + { + (it->score) >>= 1; + } + } + + long unsigned int computeHashVal(const CComponentId &rComp); + + bool include(CComponentId &rComp, const CRealNum &val); + + bool extract(CComponentId &rComp, CRealNum &val); + + bool deleteEntries(CDecisionStack & rDecStack); + + void revalidateCacheLinksIn(const vector &rComps); + void substituteCacheLinksIn(const vector &rComps, CacheEntryId idOld, CacheEntryId idNew); + + + int removePollutedEntries(CacheEntryId root); // remove the whole tree below root + + + bool cacheCompaction(CDecisionStack & rDecStack); + + void adjustDescendantsFather(CacheEntryId father) + { + vector::iterator it; + for(it = entry(father).theDescendants.begin(); + it != entry(father).theDescendants.end();it++) + { + entry(*it).theFather = father; + } + } + + // delete entries, keeping the descendants tree consistent + void deleteFromDescendantsTree(CacheEntryId rEnt) + { + // let ME be the entry to be deleted + CacheEntryId father = entry(rEnt).getFather(); + // first remove link from father to ME + if(father != NIL_ENTRY) + { + entry(father).removeDescendant(rEnt); + // then add all my descendants to descendants of father + entry(father).addDescendants(entry(rEnt).theDescendants); + } + // next all MY descendants have now father father + vector::iterator it; + for(it = entry(rEnt).theDescendants.begin(); + it != entry(rEnt).theDescendants.end(); + it++) + { + entry(*it).substituteFather(father); + } + } + + void substituteInDescTree(CacheEntryId rOld, CacheEntryId rNew) + { + // let ME be the entry to be deleted + CacheEntryId father = entry(rOld).getFather(); + // first subst link from father to ME + + if(father != NIL_ENTRY) + { + #ifdef DEBUG + assert(isEntry(father)); + #endif + entry(father).substituteDescendant(rOld, rNew); + } + // next all MY descendants get father rNew + vector::iterator it; + for(it = entry(rOld).theDescendants.begin(); + it != entry(rOld).theDescendants.end(); + it++) + { + #ifdef DEBUG + assert(isEntry(*it)); + #endif + entry(*it).substituteFather(rNew); + } + } + +}; + + + +#endif Index: /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.cpp =================================================================== --- /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.cpp (revision 9) +++ /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.cpp (revision 9) @@ -0,0 +1,75 @@ +#include "AtomsAndNodes.h" // class's header file + +CVariableVertex::~CVariableVertex() +{ +} + +bool CVariableVertex::substituteWatchCl(bool polarity, const ClauseIdT & oldId, const ClauseIdT &newId) +{ + for(vector::iterator jt = watchCls[polarity].end()-1;*jt != SENTINEL_CL; jt--) + { + if(*jt == oldId) *jt = newId; + } + return true; +} + + +bool CVariableVertex::substituteBinLink(bool polarity, const LiteralIdT& oldLit, const LiteralIdT& newLit) +{ + vector::iterator it; + for(it = binClLinks[polarity].begin(); it != binClLinks[polarity].end(); it++) + { + if(*it == oldLit) {*it = newLit; return true;} + } + return false; +} + + +bool CVariableVertex::eraseWatchClause(ClauseIdT idCl, bool polarity) +{ + vector& theWatchCls = watchCls[polarity]; + vector::iterator it; + + for(it = theWatchCls.begin();it != theWatchCls.end();it++) + { + if(*it == idCl) + { + theWatchCls.erase(it); + return true; + } + } + return false; +} + +bool CVariableVertex::eraseBinLinkTo(LiteralIdT idLit, bool Linkpolarity) +{ + vector &theLinks = getBinLinks(Linkpolarity); + vector::iterator it; + + for(it = theLinks.begin();it != theLinks.end();it++) + { + if(*it == idLit) + { + theLinks.erase(it); + return true; + } + } + return false; +} + + +bool CVariableVertex::hasBinLinkTo(LiteralIdT idLit,bool pol) const +{ + vector::const_iterator it; + + for(it = getBinLinks(pol).begin();*it != SENTINEL_LIT;it++) + { + if(*it == idLit) return true; + } + it++; + for(;*it != SENTINEL_LIT;it++) + { + if(*it == idLit) return true; + } + return false; +} Index: /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h =================================================================== --- /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h (revision 9) +++ /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/AtomsAndNodes.h (revision 9) @@ -0,0 +1,457 @@ +// Class automatically generated by Dev-C++ New Class wizard + +#ifndef ATOMSANDNODES_H +#define ATOMSANDNODES_H + +#include + +#include + +#include "../../Basics.h" +#include + +using namespace std; + +#define INVALID_DL -1 + +class CClauseVertex; +typedef CClauseVertex *PCLV; + +class CVariableVertex; +typedef CVariableVertex *PVARV; + +typedef unsigned int indexTypeVARS; +typedef unsigned int indexTypeCLS; + +typedef indexTypeVARS VarIdT; +typedef indexTypeCLS ClauseIdT; + +class LiteralIdT +{ + indexTypeVARS val; + public: + + LiteralIdT() + { + val = 0; + } + LiteralIdT(int iLitIdx) + { + val = (abs(iLitIdx)<<1) + (unsigned int)(iLitIdx > 0); + } + + LiteralIdT(VarIdT iVarIdx, bool polarity) + { + val = (iVarIdx<<1) + (unsigned int)polarity; + } + + VarIdT toVarIdx() const + { + return (val >> 1); + } + + unsigned int toUInt() const + { + return val; + } + + void makeFromUInt(unsigned int v) + { + val = v; + } + + bool polarity() const + { + return (bool)(val & 0x01); + } + + TriValue polarityTriVal() const + { + return (TriValue)(val & 0x01); + } + + bool operator!=(const LiteralIdT &rL2) const + { + return val != rL2.val; + } + + bool operator==(const LiteralIdT &rL2) const + { + return val == rL2.val; + } + + const LiteralIdT oppositeLit() const + { + return LiteralIdT(toVarIdx(),!polarity()); + } + + void print() const + { + toSTDOUT((polarity()?" ":"-")<< toVarIdx()<<" "); + } +}; + + +static const ClauseIdT NOT_A_CLAUSE(0); +static const LiteralIdT NOT_A_LIT(0,false); + +#define SENTINEL_CL NOT_A_CLAUSE +#define SENTINEL_LIT NOT_A_LIT + + +class CClauseVertex +{ + /// the offset of the first literal of this clause in theLitVector of + /// the main CInstanceGraph + unsigned int litPoolOfs; + + LiteralIdT litA, litB; + + unsigned int numLits; + int lastTouchTime; + + public: + + bool hasWatchLitA() { return litA != NOT_A_LIT;} + bool hasWatchLitB() { return litB != NOT_A_LIT;} + + void setLitA(const LiteralIdT & lit) { litA = lit;} + void setLitB(const LiteralIdT & lit) { litB = lit;} + + const LiteralIdT &idLitA() const {return litA;} + const LiteralIdT &idLitB() const {return litB;} + + int getLastTouchTime() const + { + return lastTouchTime; + } + + void setTouched() + { + lastTouchTime = CStepTime::getTime(); + } + + void setLength(unsigned int nlen) + { + numLits = nlen; + } + unsigned int length() const + { + return numLits; + } + + bool isDeleted() const + { + return numLits == 0; + } + + void setDeleted() + { + numLits = 0; + } + + + void setLitOfs(unsigned int ofs) {litPoolOfs = ofs;} + unsigned int getLitOfs() const {return litPoolOfs;} + + + // class constructor + CClauseVertex() + { + litA = litB = NOT_A_LIT; + numLits = 0; + litPoolOfs = 0; + lastTouchTime =0; + } + + void reset() + { + + lastTouchTime = 0; + } + + ~CClauseVertex(){} + + bool watches(const VarIdT &theVar) const + { + return (idLitA().toVarIdx() == theVar || idLitB().toVarIdx() == theVar); + } + +}; + + + + + +template +class extd_vector : public vector<_T> +{ + + + public: + void quickErase(int iOfs) + { + (*this)[iOfs] = vector<_T>::back(); + vector<_T>::pop_back(); + } + + //typename vector<_T>::iterator + void quickErase(typename vector<_T>::iterator &it) + { + *it = vector<_T>::back(); + vector<_T>::pop_back(); + } + +}; + + + +class AntecedentT +{ + unsigned int val; + + public: + AntecedentT() { val = 1;} + AntecedentT(const ClauseIdT idCl) + { + val = (idCl << 1) | 1; + } + AntecedentT(const LiteralIdT idLit) + { + val = (idLit.toUInt() << 1) ; + } + + bool isAClause() {return val & 0x01;} + + ClauseIdT toCl() + { + return val>>1; + } + LiteralIdT toLit() + { + LiteralIdT idLit; + idLit.makeFromUInt(val>>1); + return idLit; + } + bool isAnt() { return (isAClause() && !(toCl() == NOT_A_CLAUSE)) + || (!isAClause() && (toLit() != NOT_A_LIT));} + +}; + +class AntAndLit +//structure saving a Lit and the antecedent implying it +// antecedents may be clauses or literals +{ + public: + AntecedentT theAnt; + LiteralIdT theLit; + + AntAndLit(const AntecedentT ant,const LiteralIdT pL) + { + theAnt = ant; + theLit = pL; + } + + AntAndLit(const LiteralIdT idAntLit,const LiteralIdT pL) + { + theAnt = AntecedentT(idAntLit); + theLit = pL; + } + + AntAndLit(const ClauseIdT idCl = NOT_A_CLAUSE,const LiteralIdT pL = 0) + { + theAnt = AntecedentT(idCl); + theLit = pL; + } + + AntecedentT &getAnt(){return theAnt;} + LiteralIdT& getLit() {return theLit;} +}; + + +class CVariableVertex +{ + /// INVARIANT : SENTINEL clclcl ... + /// this is due to the watchCls being passed in reverse by BCP + extd_vector watchCls[2]; + + TriValue theVal; + + VarIdT itecIndex; + + AntecedentT myAntecedent; + int DecLevelOfDeactivation; + + /// INVARIANT: array content: llll SENTINEL xxxxx SENTINEL + /// x: conflict binary link + vector binClLinks[2]; // where the variable occurrs in pos/neg + + unsigned int inClsVecOfs[2]; // the offset in the theInClsVector + unsigned int iVarNum; // the number the variable had in the input file + + + public: + + void setInClsVecOfs(bool pol, unsigned int ofs) + { + inClsVecOfs[pol] = ofs; + } + + void setInClsVecOfs(unsigned int ofs) + { + unsigned int diff = inClsVecOfs[true] - inClsVecOfs[false]; + inClsVecOfs[false] = ofs; + inClsVecOfs[true] = ofs + diff; + } + + unsigned int getInClsVecOfs(bool pol) const + { + return inClsVecOfs[pol]; + } + + + int scoreDLIS[2]; + int scoreVSIDS[2]; + + void eraseAllEdges() + { + inClsVecOfs[0] = 1; + inClsVecOfs[1] = 1; + + watchCls[0].clear(); + watchCls[0].push_back(SENTINEL_CL); + watchCls[1].clear(); + watchCls[1].push_back(SENTINEL_CL); + + binClLinks[0].clear(); + binClLinks[0].push_back(SENTINEL_LIT); + binClLinks[0].push_back(SENTINEL_LIT); + binClLinks[1].clear(); + binClLinks[1].push_back(SENTINEL_LIT); + binClLinks[1].push_back(SENTINEL_LIT); + } + + + CVariableVertex(unsigned int numofVar = 0, VarIdT index = 0): itecIndex(index), iVarNum(numofVar) + { + DecLevelOfDeactivation = INVALID_DL; + theVal=X; + + scoreDLIS[0] = scoreDLIS[1] = 0; + scoreVSIDS[0] = scoreVSIDS[1] = 0; + + eraseAllEdges(); + } + + bool isolated() {return (inClsVecOfs[0] <= 1) && (inClsVecOfs[1] <= 1) + && (binClLinks[0].size()<=2) && (binClLinks[1].size()<=2);} + + LiteralIdT getLitIdT(bool polarity) {return LiteralIdT(getVarIdT(),polarity);} + + void newtecIndex(VarIdT iIdx) {itecIndex = iIdx;} + + int getDLCSScore() const {return scoreDLIS[0] + scoreDLIS[1];} + + int getVSIDSScore(){return scoreVSIDS[0] + scoreVSIDS[1];} + + inline const unsigned int getVarNum() const {return iVarNum;} + + inline const unsigned int getVarIdT() const {return itecIndex;} + + int getDLOD() const {return DecLevelOfDeactivation;} + + bool setVal(bool aVal,unsigned int atDL, AntecedentT ant = AntecedentT(NOT_A_CLAUSE)) + { + if(!isActive()) return false; + DecLevelOfDeactivation = atDL; + + myAntecedent = ant; + theVal = (TriValue) aVal; + return true; + } + + void unsetVal() + { + myAntecedent = AntecedentT(NOT_A_CLAUSE); + DecLevelOfDeactivation = INVALID_DL; + theVal = X; + } + + bool isImpliedBy(const ClauseIdT idCl) + { + if(isActive() || !myAntecedent.isAClause()) return false; + if(myAntecedent.toCl() == idCl) return true; + return false; + } + void adjustAntecedent(AntecedentT ant) {myAntecedent=ant;} + bool isActive() const {return theVal == X;} + + bool flipVal() + { + if(theVal == W) theVal =F; + else if(theVal == F) theVal =W; + + return true; + } + + AntecedentT getAntecedent() {return myAntecedent;} + + bool getboolVal() const {return theVal==W;} + + TriValue getVal() const {return theVal;} + + unsigned int countBinLinks() const {return binClLinks[0].size() + binClLinks[1].size() - 4;} + unsigned int countBinLinks(bool pol) const {return binClLinks[pol].size() - 2;} + + + extd_vector &getWatchClauses(bool polarity) + { + return watchCls[polarity]; + } + + const extd_vector &getWatchClauses(bool polarity) const + { + return watchCls[polarity]; + } + + void addWatchClause(ClauseIdT idCl,bool polarity) + { + watchCls[polarity].push_back(idCl); + } + + void addBinLink(bool polarity, LiteralIdT &lit) + { + *(binClLinks[polarity].end()-2) = lit; + binClLinks[polarity].push_back(SENTINEL_LIT); + } + + void addBinLinkCCl(bool polarity, LiteralIdT &lit) + { + *(binClLinks[polarity].end()-1) = lit; + binClLinks[polarity].push_back(SENTINEL_LIT); + } + + bool eraseBinLinkTo(LiteralIdT idLit, bool Linkpolarity); + bool hasBinLinkTo(LiteralIdT idLit,bool pol) const; + + const vector & getBinLinks(bool polarity) const + { + return binClLinks[polarity]; + } + vector & getBinLinks(bool polarity) + { + return binClLinks[polarity]; + } + + bool eraseWatchClause(ClauseIdT idCl, bool polarity); + + bool substituteWatchCl(bool polarity, const ClauseIdT & oldId, const ClauseIdT &newId); + + bool substituteBinLink(bool polarity, const LiteralIdT& oldLit, const LiteralIdT& newLit); + + // class destructor + ~CVariableVertex(); +}; + +#endif + Index: /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h =================================================================== --- /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h (revision 9) +++ /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/ComponentTypes.h (revision 9) @@ -0,0 +1,356 @@ +#ifndef COMPONENTTYPES_H +#define COMPONENTTYPES_H + +#ifdef DEBUG +#include +#endif + + +#include +#include + +#include + +#include "AtomsAndNodes.h" + +using namespace std; + +// +// the identifier of the components +// identifier for (truly) binary clauses are not stored, therefore we need +// trueClauseCount to kepp track of the number of binary clauses still active in the +// component, otherwise if theClauses is empty one might suspect that the whole component is +// empty which would not be true if there where binary clauses in the original formula +// +class CComponentId +{ + /// INVARIANT: content: vvvvv varsSENTINEL + vector theVars; + /// INVARIANT: content: cccccc clsSENTINEL + vector theClauses; + + unsigned int trueClauseCount; + + long unsigned int hashKeyVars; + long unsigned int hashKeyCls; + + public: + + /// INVARIANT: + /// cachedChildren may be nonempty only if cachedAs == NIL_ENTRY + /// if cachedAS != NIL_ENTRY then this component has been cached and + /// its descendants can be found in xFormulaCache.entry(cachedAs).theDescendants + unsigned int cachedAs; + vector cachedChildren; + + void addCachedChildren(const vector & cc) + { + cachedChildren.insert(cachedChildren.end(),cc.begin(),cc.end()); + } + + + #define varsSENTINEL 0 + #define clsSENTINEL NOT_A_CLAUSE + + void reserveSpace(unsigned int nVars, unsigned int nCls) + { + theVars.reserve(nVars + 1); + theClauses.reserve(nCls + 1); + } + + inline void addCl(const ClauseIdT & cl) + { + theClauses.push_back(cl); + + //Compute HashKey + if(cl != clsSENTINEL) hashKeyCls = hashKeyCls*7 + cl; + } + + inline void addVar(const VarIdT & var) + { + theVars.push_back(var); + + //Compute HashKey + if(var != varsSENTINEL) hashKeyVars = hashKeyVars*5 + var; + + } + + long unsigned int getHashKey() const + { + return hashKeyVars + (hashKeyCls<<9); + } + + + void clear() + { + theVars.clear(); + theClauses.clear(); + trueClauseCount = 0; + cachedAs = 0; + } + + CComponentId() + { + clear(); + trueClauseCount = 0; + cachedAs = 0; + hashKeyVars = 0; + hashKeyCls = 0; + } + + + vector::iterator varsBegin() + { + return theVars.begin(); + } + + + vector::iterator clsBegin() + { + return theClauses.begin(); + } + + inline vector::const_iterator varsBegin() const + { + return theVars.begin(); + } + + inline vector::const_iterator clsBegin() const + { + return theClauses.begin(); + } + + + unsigned int countVars() const + { + #ifdef DEBUG + assert(theVars.size() >= 1); + #endif + return theVars.size() - 1; + } + + unsigned int countCls() const + { + #ifdef DEBUG + assert(theClauses.size() >= 1); + #endif + return theClauses.size() - 1; + } + + bool empty() const + { + return theVars.empty();// || theClauses.empty(); + } + + int memSize() const + { + return theVars.capacity()*sizeof(VarIdT) + + theClauses.capacity()*sizeof(ClauseIdT); + } + + void setTrueClauseCount(unsigned int count) + { + trueClauseCount = count; + } + + unsigned int getClauseCount() + { + #ifdef DEBUG + assert(trueClauseCount >= countCls()); + #endif + return trueClauseCount; + } + + bool containsBinCls() const + { + #ifdef DEBUG + assert(trueClauseCount >= countCls()); + #endif + return (trueClauseCount > countCls()); + } + +}; + +template +class CPackedCompId +{ + static unsigned int bpeCls, bpeVars; // bitsperentry + static unsigned int maskVars,maskCls; +protected: + vector<_T> theVars; + vector<_T> theClauses; + + public: + static unsigned int bitsPerVar() { return bpeVars;} + static unsigned int bitsPerCl() { return bpeCls;} + + unsigned int sizeVarVec() {return theVars.size();} + unsigned int sizeClVec() {return theClauses.size();} + + static void adjustPackSize(unsigned int maxVarId, unsigned int maxClId); + + CPackedCompId() + { + } + + void createFrom(const CComponentId &rComp); + + + bool equals(const CPackedCompId<_T> &rComp) const + { + return theVars == rComp.theVars + && theClauses == rComp.theClauses; + } + + bool equals(const CComponentId &rComp) const; + + void clear() + { + theVars.clear(); + theClauses.clear(); + } + + bool empty() const + { + return theVars.empty() && theClauses.empty(); + } + + int memSize() const + { + return (theVars.capacity() + theClauses.capacity())*sizeof(_T); + } + +}; + +///////////////////////////////////////////////////////////////////////////// +//BEGIN Implementation CPackedCompId +///////////////////////////////////////////////////////////////////////////// + +template +unsigned int CPackedCompId<_T,_bitsPerBlock>::bpeCls = 0; +template +unsigned int CPackedCompId<_T,_bitsPerBlock>::bpeVars = 0; // bitsperentry +template +unsigned int CPackedCompId<_T,_bitsPerBlock>::maskVars = 0; +template +unsigned int CPackedCompId<_T,_bitsPerBlock>::maskCls = 0; // bitsperentry + +template +void CPackedCompId<_T,_bitsPerBlock>::adjustPackSize(unsigned int maxVarId, unsigned int maxClId) +{ + bpeVars = (unsigned int)ceil(log((double)maxVarId+1)/log(2.0)); + bpeCls = (unsigned int)ceil(log((double)maxClId+1)/log(2.0)); + + maskVars = maskCls = 0; + for(unsigned int i=0; i < bpeVars;i++) maskVars = (maskVars<<1) +1; + for(unsigned int i=0; i < bpeCls;i++) maskCls = (maskCls<<1) +1; +} + +template +void CPackedCompId<_T,_bitsPerBlock>::createFrom(const CComponentId &rComp) +{ + vector::const_iterator it; + vector::const_iterator jt; + + if(!theVars.empty()) theVars.clear(); + if(!theClauses.empty()) theClauses.clear(); + + theVars.reserve( rComp.countVars()*bpeVars/_bitsPerBlock +1); + theClauses.reserve(rComp.countCls()*bpeCls/_bitsPerBlock +1); + + unsigned int bitpos = 0; + unsigned int h = 0; + _T * pBack; + + pBack = &theVars.front(); + + for(it = rComp.varsBegin(); *it != varsSENTINEL;it++) + { + h |= ((*it)<< (bitpos)); + bitpos+= bpeVars; + + if(bitpos >= _bitsPerBlock) + { + bitpos -= _bitsPerBlock; + #ifdef DEBUG + assert(theVars.size() < theVars.capacity()); + #endif + theVars.push_back(h); + h = ((*it)>> (bpeVars - bitpos)); + } + } + if(bitpos > 0) theVars.push_back(h); + + bitpos = 0; + h = 0; + pBack = &theClauses.front(); + for(jt = rComp.clsBegin(); *jt != clsSENTINEL;jt++) + { + h |= ((*jt)<< (bitpos)); + bitpos += bpeCls; + + if(bitpos >= _bitsPerBlock) + { + bitpos -= _bitsPerBlock; + #ifdef DEBUG + assert(theClauses.size() < theClauses.capacity()); + #endif + theClauses.push_back(h); + h = ((*jt)>> (bpeCls - bitpos)); + } + } + if(bitpos > 0) theClauses.push_back(h); +} + + +template +bool CPackedCompId<_T,_bitsPerBlock>::equals(const CComponentId &rComp) const +{ + + if( (theVars.capacity() != (uint) rComp.countVars()*bpeVars/_bitsPerBlock +1) + || theClauses.capacity() != (uint) rComp.countCls()*bpeCls/_bitsPerBlock +1) return false; + + unsigned int bitpos = 0; + unsigned int h = 0; + const _T * pItA; + + pItA = &theVars.front(); + + for(vector::const_iterator it = rComp.varsBegin(); *it != varsSENTINEL;it++) + { + h = ((*pItA)>> (bitpos)); + bitpos+= bpeVars; + if(bitpos >= _bitsPerBlock) + { + bitpos -= _bitsPerBlock; + pItA++; + h |= ((*pItA)<< (bpeVars - bitpos)); + } + if(*it != (maskVars & h)) return false; + } + + bitpos = 0; + pItA = &theClauses.front(); + for(vector::const_iterator jt = rComp.clsBegin(); *jt != clsSENTINEL;jt++) + { + h = (*pItA)>> (bitpos); + bitpos += bpeCls; + + if(bitpos >= _bitsPerBlock) + { + bitpos -= _bitsPerBlock; + pItA++; + h |= ((*pItA)<< (bpeCls - bitpos)); + } + if(*jt != (maskCls & h)) return false; + } + + return true; + + +} + +///////////////////////////////////////////////////////////////////////////// +//END Implementation CPackedCompId +///////////////////////////////////////////////////////////////////////////// +#endif Index: /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp =================================================================== --- /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp (revision 9) +++ /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.cpp (revision 9) @@ -0,0 +1,916 @@ +#include "InstanceGraph.h" +#include +#include +#include + +CRunAnalyzer theRunAn; + + +// class constructor +CInstanceGraph::CInstanceGraph() +{ + +} + +// class destructor +CInstanceGraph::~CInstanceGraph() +{ + toDEBUGOUT("lv sz:"<< theLitVector.size() << endl); + toDEBUGOUT("nUcls:"<< theUnitClauses.size() << endl); +} + + +//////////////////////////////////////////////////////////////////////// +// +// BEGIN Methods for Clauses +// +/////////////////////////////////////////////////////////////////////// + +bool CInstanceGraph::substituteLitsOf(CClauseVertex &rCl,const LiteralIdT &oldLit, const LiteralIdT &newLit) +{ + vector::iterator it; + + if(oldLit == rCl.idLitA()) rCl.setLitA(newLit); + else if(oldLit == rCl.idLitB()) rCl.setLitB(newLit); + + if(oldLit.oppositeLit() == rCl.idLitA()) rCl.setLitA(newLit.oppositeLit()); + else if(oldLit.oppositeLit() == rCl.idLitB()) rCl.setLitB(newLit.oppositeLit()); + + for(it = begin(rCl); *it != ClauseEnd();it++) + { + if(*it == oldLit) + { + *it = newLit; + return true; + } + else if(*it == oldLit.oppositeLit()) + { + *it = newLit.oppositeLit(); + return true; + } + } + return false; +} + +bool CInstanceGraph::containsVar(const CClauseVertex &rCl, const VarIdT &theVar) const +{ + vector::const_iterator it; + + for(it = begin(rCl); *it != ClauseEnd();it++) + { + if(it->toVarIdx() == theVar) return true; + } + return false; +} + +bool CInstanceGraph::containsLit(const CClauseVertex &rCl, const LiteralIdT &theLit) const +{ + vector::const_iterator it; + + for(it = begin(rCl); *it != ClauseEnd();it++) + { + if(*it == theLit) return true; + } + return false; +} + + + +void CInstanceGraph::printCl(const CClauseVertex &rCl) const +{ + vector::const_iterator it; + + for(it = begin(rCl); *it != ClauseEnd();it++) + { + if(!(it)->polarity()) toSTDOUT("-"); + toSTDOUT(it->toVarIdx()+1 << " "); + } + toSTDOUT(" 0\n"); +} + +bool CInstanceGraph::createConflictClause(const vector &theCClause) +{ + ClauseIdT cclId; + vector::const_iterator it; + + #ifdef DEBUG + assert(theCClause.size() > 0); + #endif + + if(theCClause.size() == 1) + { + createUnitCl(theCClause.front()); + if(theUnitClauses.size() == 1 || theUnitClauses.size() % 5 == 0) + printCClstats(); + getVar(theCClause.front()).scoreVSIDS[theCClause.front().polarity()]++; + getVar(theCClause.front()).scoreVSIDS[theCClause.front().oppositeLit().polarity()]++; + theRunAn.addClause(); + return true; + } + + + if(theCClause.size() == 2) + { + if(!createBinCCl(theCClause[0],theCClause[1])) return false; + + getVar(theCClause[0]).scoreVSIDS[theCClause[0].polarity()]++; + getVar(theCClause[1]).scoreVSIDS[theCClause[1].polarity()]++; + getVar(theCClause[0]).scoreVSIDS[theCClause[0].oppositeLit().polarity()]++; + getVar(theCClause[1]).scoreVSIDS[theCClause[1].oppositeLit().polarity()]++; + + if(numBinCCls % 100 == 0) printCClstats(); + theRunAn.addClause(); + return true; + } + + // create the ClauseVertex + + cclId = makeConflictClause(); + + CClauseVertex *pCCl = &getClause(cclId); + + pCCl->setLitOfs(theLitVector.size()); + pCCl->setLength(theCClause.size()); + + int score = 0; + LiteralIdT aLit = NOT_A_LIT; + LiteralIdT bLit = NOT_A_LIT; + + theLitVector.reserve(theLitVector.size() + theCClause.size()); + for(it = theCClause.begin(); it != theCClause.end(); it++) + { + // add literal *it to the litvector + theLitVector.push_back(*it); + + if(getVar(*it).getDLOD() >= score) + // determine the most recently set literals to become watched + { + bLit = aLit; + aLit = *it; + score = getVar(*it).getDLOD(); + } + getVar(*it).scoreVSIDS[it->polarity()]++; + getVar(*it).scoreVSIDS[it->oppositeLit().polarity()]++; + } + score = 0; + if(bLit == NOT_A_LIT) + for(it = theCClause.begin(); it != theCClause.end(); it++) + { + if(*it != aLit && getVar(*it).getDLOD() >= score) + // determine the most recently set literals to become watched + { + bLit = *it; + score = getVar(*it).getDLOD(); + } + } + + #ifdef DEBUG + assert(aLit != NOT_A_LIT); + assert(bLit != NOT_A_LIT); + #endif + + // close the clause with a SENTINEL_LIT + theLitVector.push_back(SENTINEL_LIT); + + // set watch for litA + if(aLit != NOT_A_LIT) + { + pCCl->setLitA(aLit); + getVar(aLit).addWatchClause(cclId,aLit.polarity()); + } + // set watch for litB + if(bLit != NOT_A_LIT) + { + pCCl->setLitB(bLit); + getVar(bLit).addWatchClause(cclId,bLit.polarity()); + } + + if(countCCls() % 10000 == 0) printCClstats(); + theRunAn.addClause(); + return true; +} + +bool CInstanceGraph::setCClImplyingLit(ClauseIdT idCl, const LiteralIdT &theLit) +{ + CClauseVertex &rCV = getClause(idCl); + vector::const_iterator it; + + getVar(rCV.idLitA()).eraseWatchClause(idCl, rCV.idLitA().polarity()); + getVar(rCV.idLitB()).eraseWatchClause(idCl, rCV.idLitB().polarity()); + + int score = -1; + LiteralIdT aLit = NOT_A_LIT; + + + + #ifdef DEBUG + bool ex = false; + for(it = begin(rCV); *it != ClauseEnd(); it++) + if(*it == theLit) + { + ex = true; + break; + } + assert(ex); + #endif + + rCV.setLitA(theLit); + getVar(rCV.idLitA()).addWatchClause(idCl,rCV.idLitA().polarity()); + // set watch for litB + + aLit = NOT_A_LIT; + score = -1; + + for(it = begin(rCV); *it != ClauseEnd(); it++) + if(getVar(*it).getDLOD() > score) + { + if(*it == theLit) continue; + aLit = *it; + score = getVar(*it).getDLOD(); + } + + if(aLit != NOT_A_LIT) + { + rCV.setLitB(aLit); + getVar(aLit).addWatchClause(idCl,aLit.polarity()); + } + + return true; +} + +bool CInstanceGraph::cleanUp_deletedCCls() +{ + DepositOfClauses::iterator ct; + + /////////////////// + // clean up LitVector + /////////////////// + + vector::iterator writeLit = theLitVector.begin() + (beginOfCCls())->getLitOfs(); + ct = beginOfCCls(); + + for(vector::iterator xt = writeLit;xt != theLitVector.end();xt++) + if(*xt != NOT_A_LIT) + { + if(!ct->isDeleted()) + { + ct->setLitOfs((unsigned int)(writeLit - theLitVector.begin())); + + while(*xt != NOT_A_LIT) + { + if(writeLit != xt) *writeLit = *xt; + xt++; + writeLit++; + } + *(writeLit++) = NOT_A_LIT; + } + else { // *ct is deleted, hence, omit all its literals from consideration + while(*xt != NOT_A_LIT) xt++;//*(xt++) = NOT_A_LIT; + } + ct++; + } + + theLitVector.resize((unsigned int)(writeLit - theLitVector.begin())); + + DepositOfClauses::iterator itWrite = beginOfCCls(); + /////////////////// + // clean up clauses + /////////////////// + ClauseIdT oldId,newId; + + for(ct = beginOfCCls(); ct != endOfCCls();ct++) + if(!ct->isDeleted()) + { + if(itWrite != ct) + { + *itWrite = *ct; + //BEGIN substitute CCLs + + oldId = toClauseIdT(ct); + newId = toClauseIdT(itWrite); + + if(getVar(itWrite->idLitB()).isImpliedBy(oldId)) + getVar(itWrite->idLitB()).adjustAntecedent(AntecedentT(newId)); + if(getVar(itWrite->idLitA()).isImpliedBy(oldId)) + getVar(itWrite->idLitA()).adjustAntecedent(AntecedentT(newId)); + + getVar(itWrite->idLitA()).substituteWatchCl(itWrite->idLitA().polarity(),oldId,newId); + getVar(itWrite->idLitB()).substituteWatchCl(itWrite->idLitB().polarity(),oldId,newId); + //END substitute CCLs + + ct->setDeleted(); + } + itWrite++; + } + + theClauses.erase(itWrite,endOfCCls()); + + return true; +} + + +bool CInstanceGraph::deleteConflictCls() +{ + DepositOfClauses::iterator it; + + double vgl = 0; + + for(it = beginOfCCls(); it != endOfCCls(); it++) + { + vgl = 11000.0; + if(it->length() != 0) vgl /= pow((double)it->length(),3); + + if(CStepTime::getTime() - it->getLastTouchTime() > vgl) + { + markCClDeleted(toClauseIdT(it)); + } + } + return true; +} + +bool CInstanceGraph::markCClDeleted(ClauseIdT idCl) +{ + CClauseVertex & rCV = getClause(idCl); + if(rCV.isDeleted()) return false; + ///// + // a clause may not be deleted if it causes an implication: + /// + if(getVar(rCV.idLitB()).isImpliedBy(idCl) + ||getVar(rCV.idLitA()).isImpliedBy(idCl)) + { + return false; + } + + getVar(rCV.idLitB()).eraseWatchClause(idCl, rCV.idLitB().polarity()); + getVar(rCV.idLitA()).eraseWatchClause(idCl, rCV.idLitA().polarity()); + rCV.setDeleted(); + return true; +} + +//////////////////////////////////////////////////////////////////////// +// +// END Methods for Clauses +// +/////////////////////////////////////////////////////////////////////// + +bool CInstanceGraph::prep_substituteClauses(unsigned int oldIdx, unsigned int newIdx) +{ + CClauseVertex &rCl = getClause(newIdx); + vector::const_iterator it; + vector::iterator jt; + ClauseIdT oldId(oldIdx),newId(newIdx); + + + if(getVar(rCl.idLitB()).isImpliedBy(oldId)) + getVar(rCl.idLitB()).adjustAntecedent(AntecedentT(newId)); + + if(getVar(rCl.idLitA()).isImpliedBy(oldId)) + getVar(rCl.idLitA()).adjustAntecedent(AntecedentT(newId)); + + + getVar(rCl.idLitA()).substituteWatchCl(rCl.idLitA().polarity(),oldId,newId); + getVar(rCl.idLitB()).substituteWatchCl(rCl.idLitB().polarity(),oldId,newId); + + for(it = begin(rCl); *it != ClauseEnd(); it++) + { + // substitute ClEdges in theInClsVector + for(vector::iterator jt = var_InClsBegin(it->toVarIdx(),false);*jt != SENTINEL_CL; jt++) + { + if(*jt == oldId) *jt = newId; + } + // + } + + return true; +} + + +bool CInstanceGraph::prep_substituteVars(CVariableVertex &rV, unsigned int newIdx) +// only valid if no conflict clauses are present +{ + vector::const_iterator it; + vector::iterator kt,vt; + + vector::iterator jt; + unsigned int oldIdx = rV.getVarIdT(); + rV.newtecIndex(newIdx); + + LiteralIdT oldLit, newLit; + + oldLit = LiteralIdT(oldIdx,true); + newLit = LiteralIdT(newIdx,true); + + for(it = var_InClsBegin(rV.getVarIdT(),true); *it != SENTINEL_CL; it++) + { + substituteLitsOf(getClause(*it),oldLit,newLit); + } + + for(kt = rV.getBinLinks(true).begin(); *kt != SENTINEL_LIT; kt++) + { + getVar(*kt).substituteBinLink(kt->polarity(),oldLit,newLit); + } + + oldLit = LiteralIdT(oldIdx,false); + newLit = LiteralIdT(newIdx,false); + + for(it = var_InClsBegin(rV.getVarIdT(),true)-1; *it != SENTINEL_CL; it--) + { + substituteLitsOf(getClause(*it),oldLit,newLit); + } + + for(kt = rV.getBinLinks(false).begin(); *kt != SENTINEL_LIT; kt++) + { + getVar(*kt).substituteBinLink(kt->polarity(),oldLit,newLit); + } + return true; +} + + +bool CInstanceGraph::eraseLiteralFromCl(ClauseIdT idCl,LiteralIdT theLit) +{ + bool retV = false; + CClauseVertex & rCV = getClause(idCl); + vector::iterator it; + vector::iterator endCl = begin(rCV) + rCV.length(); + if(rCV.isDeleted()) return false; + + if(getVar(rCV.idLitA()).isImpliedBy(idCl) + || getVar(rCV.idLitB()).isImpliedBy(idCl)) return false; + + getVar(rCV.idLitA()).eraseWatchClause(idCl, rCV.idLitA().polarity()); + if(rCV.length() >= 2) + getVar(rCV.idLitB()).eraseWatchClause(idCl, rCV.idLitB().polarity()); + + for(it = begin(rCV); *it != ClauseEnd();it++) + { + if((*it) == theLit) + { + if(it != endCl-1) *it = *(endCl-1); + *(endCl-1) = NOT_A_LIT; + rCV.setLength(rCV.length()-1); + retV = true; + break; + } + } + + rCV.setLitA(NOT_A_LIT); + rCV.setLitB(NOT_A_LIT); + + if(rCV.length() >= 1) + { + rCV.setLitA(*begin(rCV)); + getVar(rCV.idLitA()).addWatchClause(idCl, rCV.idLitA().polarity()); + } + if(rCV.length() >= 2) + { + rCV.setLitB(*(begin(rCV)+1)); + getVar(rCV.idLitB()).addWatchClause(idCl, rCV.idLitB().polarity()); + } + + return retV; +} + +bool CInstanceGraph::prep_CleanUpPool() +{ + /////////////////// + // clean up clauses + /////////////////// + DepositOfClauses::iterator ct, ctWrite = theClauses.begin()+1; + + for(ct = theClauses.begin()+1; ct != theClauses.end();ct++) + if(!ct->isDeleted()) + { + if(ctWrite != ct) + { + *ctWrite = *ct; + prep_substituteClauses((unsigned int)(ct - theClauses.begin()), (unsigned int)(ctWrite - theClauses.begin())); + } + ctWrite++; + } + + theClauses.erase(ctWrite,theClauses.end()); + iOfsBeginConflictClauses = theClauses.size(); + /////////////////// + // clean up LitVector + /////////////////// + + vector::iterator writeLit = theLitVector.begin(); + + ct = theClauses.begin()+1; + + for(vector::iterator xt = writeLit;xt != theLitVector.end();xt++) + if(*xt != SENTINEL_LIT) // start of the next clause found + { + ct->setLitOfs((unsigned int) (writeLit - theLitVector.begin())); + ct++; + while(*xt != SENTINEL_LIT) + { + if(writeLit != xt) *writeLit = *xt; + xt++; writeLit++; + } + *writeLit = NOT_A_LIT; + writeLit++; + } + + theLitVector.resize((unsigned int) (writeLit - theLitVector.begin())); + + + /////////////////// + // clean up vars + /////////////////// + + DepositOfVars::iterator it, itWriteVar = theVars.begin()+1; + + for(it = theVars.begin()+1; it != theVars.end();it++) + { + if(!it->isolated() || it->isActive()) + { + if(itWriteVar != it) + { + *itWriteVar = *it; + prep_substituteVars(*itWriteVar, itWriteVar - theVars.begin()); + } + itWriteVar++; + } + } + + theVars.erase(itWriteVar,theVars.end()); + + + it = theVars.begin()+1; + /////////////////// + // clean up inCls + ////////////////// + + vector::iterator clt, cltWrite = theInClsVector.begin()+2; + for(clt = theInClsVector.begin()+2;clt != theInClsVector.end();clt++) + if(*clt != SENTINEL_CL) + { + while(theInClsVector[it->getInClsVecOfs(false)] == SENTINEL_CL + && theInClsVector[it->getInClsVecOfs(true)] == SENTINEL_CL) + { + it->setInClsVecOfs(false,0); + it->setInClsVecOfs(true,1); + it++; + } + + { + it->setInClsVecOfs((unsigned int)(cltWrite - theInClsVector.begin())); + + while(*clt != SENTINEL_CL) + { + if(cltWrite != clt) *cltWrite = *clt; + clt++; + cltWrite++; + } + *(cltWrite++) = SENTINEL_CL; + } + it++; + } + + theInClsVector.resize((unsigned int) (cltWrite - theInClsVector.begin())); + + theUnitClauses.clear(); + theUClLookUp.clear(); + theUClLookUp.resize(theVars.size(),X); + + unsigned int countBinCl= 0; + // as the number of binary clauses might have changed, + // we have to update the numBinClauses, which keeps track of the # of bin Clauses + for(it = theVars.begin(); it != theVars.end();it++) + { + countBinCl += it->countBinLinks(); + } + numBinClauses = countBinCl>>1; + + toDEBUGOUT("inCls sz:"< litVec; + vector seenV; + int clauseLen = 0; + TriValue pol; + + vector varPosMap; + + // BEGIN INIT + reset(); // clear everything + // END INIT + + ///BEGIN File input + FILE *filedesc; + filedesc = fopen(lpstrFileName,"r"); + if(filedesc == NULL){toERROUT(" Error opening file "<< lpstrFileName< '9')) i++; + while(buf[i] == '-' || buf[i] >= '0' && buf[i] <= '9') + { + token[j] = buf[i]; + i++; j++; + } + token[j] = 0x0; + lit = atoi(token); + j = 0; + if(lit == 0) // end of clause + { + if(clauseLen > 0) litVec.push_back(0); + clauseLen = 0; + } + else { + clauseLen++; + litVec.push_back(lit); + } + } + } + + + if(!inFile.eof()){ toERROUT(" CNF input: line too long");} + inFile.close(); + /// END FILE input + + + vector::iterator it, jt, itEndCl; + + int actVar; + bool istaut = true; + int imultipleLits = 0; + int ilitA, ilitB, lengthCl; + LiteralIdT LitA,LitB; + ClauseIdT idCl; + + seenV.resize(nVars+1,X); + varPosMap.resize(nVars+1,-1); + theVars.reserve(nVars+1); + theLitVector.reserve(litVec.size()); + theClauses.reserve(nCls + 10000); + theRunAn.init(nVars,nCls); + + vector > _inClLinks[2]; + + _inClLinks[0].resize(nVars+1); + _inClLinks[1].resize(nVars+1); + + it = litVec.begin(); + + + + while(it != litVec.end()) + { + jt = it; + istaut = false; + imultipleLits = 0; + ilitA = 0; ilitB = 0; // we pick two literals from each clause for watch- or bin-creation + lengthCl = 0; + while(*jt != 0) // jt passes through the clause to determine if it is valid + { + actVar = abs(*jt); + if(seenV[actVar] == X) // literal not seen + { + seenV[actVar] = (*jt > 0)?W:F; + if(ilitA == 0) ilitA = *jt; + else if(ilitB == 0) ilitB = *jt; + jt++; + } + else if(seenV[actVar] == (*jt > 0)?W:F) + { // literal occurs twice: omit it + *jt = 0; + imultipleLits++; + jt++; + } + else + { // literal in two opposing polarities -> don't include this clause (INVALID) + istaut = true; + while(*jt != 0) jt++; + //cout <<"X"; + break; + } + } + + itEndCl = jt; + lengthCl = (int)(itEndCl - it) - imultipleLits; + + if(!istaut && lengthCl > 0) // if the clause is not tautological, add it + { + #ifdef DEBUG + if(ilitA == 0){ toERROUT("ERR"); exit(3);} + #endif + + actVar = abs(ilitA); + if(varPosMap[actVar]== -1) // create new Var if not present yet + varPosMap[actVar] = makeVariable(actVar); + + LitA = LiteralIdT(varPosMap[actVar],(ilitA > 0)?W:F); + + + if(ilitB != 0)// determine LiteralIdT for ilitB + { + actVar = abs(ilitB); + if(varPosMap[actVar]== -1) // create new Var if not present yet + varPosMap[actVar] = makeVariable(actVar); + + LitB = LiteralIdT(varPosMap[actVar],(ilitB > 0)?W:F); + } + + + if(lengthCl == 1) + { + theUnitClauses.push_back(LitA); + } + else if(lengthCl == 2) + { + #ifdef DEBUG + if(ilitB == 0) { toERROUT("ERR BIN CL"); exit(3);} + #endif + + if(!getVar(LitA).hasBinLinkTo(LitB,LitA.polarity())) + { + getVar(LitA).addBinLink(LitA.polarity(),LitB); + getVar(LitB).addBinLink(LitB.polarity(),LitA); + numBinClauses++; + } + } + else + { + #ifdef DEBUG + if(ilitB == 0) { toERROUT("ERR CL"); exit(3);} + #endif + idCl = makeClause(); + getClause(idCl).setLitOfs(theLitVector.size()); + + theLitVector.push_back(LitA); + + /// new + _inClLinks[LitA.polarity()][LitA.toVarIdx()].push_back(idCl); + getVar(LitA).scoreDLIS[LitA.polarity()]++; + /// + theLitVector.push_back(LitB); + + /// new + _inClLinks[LitB.polarity()][LitB.toVarIdx()].push_back(idCl); + getVar(LitB).scoreDLIS[LitB.polarity()]++; + /// + + for(jt = it+2; jt != itEndCl;jt++) + if(*jt != 0 && *jt != ilitB) // add all nonzero literals + { + actVar = abs(*jt); + pol = (*jt > 0)?W:F; + if(varPosMap[actVar]== -1) // create new Var + varPosMap[actVar] = makeVariable(actVar); + + // add lit to litvector + theLitVector.push_back(LiteralIdT(varPosMap[actVar],pol)); + /// new + _inClLinks[pol][varPosMap[actVar]].push_back(idCl); + getVar(varPosMap[actVar]).scoreDLIS[pol]++; + /// + } + // make an end: SENTINEL_LIT + theLitVector.push_back(SENTINEL_LIT); + + getClause(idCl).setLitA(LitA); + getClause(idCl).setLitB(LitB); + getClause(idCl).setLength(lengthCl); + + getVar(LitA).addWatchClause(idCl,LitA.polarity()); + getVar(LitB).addWatchClause(idCl,LitB.polarity()); + } + + } + + // undo the entries in seenV + for(jt = it; jt != itEndCl;jt++) seenV[abs(*jt)] = X; + + it = itEndCl; + it++; + } + + + + //BEGIN initialize theInClsVector + theInClsVector.clear(); + theInClsVector.reserve(theLitVector.size() + nVars); + theInClsVector.push_back(SENTINEL_CL); + vector::iterator clt; + for(unsigned int i = 0; i <= nVars; i++) + { + getVar(i).setInClsVecOfs(false,theInClsVector.size()); + for(clt = _inClLinks[0][i].begin(); clt != _inClLinks[0][i].end(); clt++) + { + theInClsVector.push_back(*clt); + } + + getVar(i).setInClsVecOfs(true,theInClsVector.size()); + for(clt = _inClLinks[1][i].begin(); clt != _inClLinks[1][i].end(); clt++) + { + theInClsVector.push_back(*clt); + } + theInClsVector.push_back(SENTINEL_CL); + } + //END initialize theInClsVector + + #ifdef DEBUG + assert(theInClsVector.size() <= theLitVector.size() + nVars + 1); + toDEBUGOUT("inCls sz:"<::const_iterator bt; + + for(bt = rVar.getBinLinks(true).begin(); bt != rVar.getBinLinks(true).end(); bt++) + { + if(*bt != SENTINEL_LIT) n+= (unsigned int)getVar(*bt).isActive(); + } + + for(bt = rVar.getBinLinks(false).begin(); bt != rVar.getBinLinks(false).end(); bt++) + { + if(*bt != SENTINEL_LIT) n+= (unsigned int)getVar(*bt).isActive(); + } + + return n; +} + +void CInstanceGraph::print() +{ + DepositOfClauses::iterator it; + for(it = theClauses.begin()+1; it != theClauses.end();it++) + { + printCl(*it); + } +} + + +void CInstanceGraph::printActiveClause(const ClauseIdT &idCl) const +{ + vector::const_iterator it; + toSTDOUT("("); + + for(it = begin(getClause(idCl)); *it != ClauseEnd();it++) + { + if(getVar(*it).isActive()) + { + if(it->polarity()) toSTDOUT(" ") else toSTDOUT("-"); + + toSTDOUT(it->toVarIdx() << " "); + } + } + toSTDOUT(")"); +} Index: /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h =================================================================== --- /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h (revision 9) +++ /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/InstanceGraph.h (revision 9) @@ -0,0 +1,394 @@ +#ifndef INSTANCE_GRAPH_H +#define INSTANCE_GRAPH_H + + +#include +#include + +#ifdef DEBUG +#include +#endif + +using namespace std; + +#include + +#include "../../Basics.h" +#include "AtomsAndNodes.h" + + +typedef vector DepositOfClauses; +typedef vector DepositOfVars; + + +extern CRunAnalyzer theRunAn; + +class CInstanceGraph +{ + /** theLitVector: the literals of all clauses are stored here + * INVARIANT: first and last entries of theLitVector are a SENTINEL_LIT + * + */ + vector theLitVector; + + /** theInClsVector: + * the Vector containing all links from variables + * to the clauses they appear in + * INVARIANT: for each Variable x the block of clause links looks as follows: + SENTINEL_CL nnnnnnnnppppppp SENTINEL_CL + where: n ... clause where -x appears; p.. clause where x appears + */ + vector theInClsVector; + + DepositOfClauses theClauses; + unsigned int iOfsBeginConflictClauses; + + DepositOfVars theVars; + + vector theConflicted; + unsigned int numBinClauses; + unsigned int numBinCCls; + + protected: + + vector theUnitClauses; + vector theUClLookUp; + + /// THE function to clear all the data in this class + void reset() + { + theLitVector.clear(); + theLitVector.push_back(SENTINEL_LIT); + + theInClsVector.clear(); + theInClsVector.push_back(SENTINEL_CL); + + theClauses.clear(); + theClauses.push_back(CClauseVertex()); + iOfsBeginConflictClauses = 0; + + theVars.clear(); + theVars.push_back(CVariableVertex(0,0)); //initializing the Sentinel + theConflicted.clear(); + + numBinClauses = 0; + numBinCCls = 0; + + theUnitClauses.clear(); + theUClLookUp.clear(); + } + + void doVSIDSScoreDiv() + { + DepositOfVars::iterator it; + for(it = beginOfVars();it != endOfVars();it++) + { + it->scoreVSIDS[0] >>= 1; + it->scoreVSIDS[1] >>= 1; + } + } + + protected: + void printCClstats() + { + toSTDOUT("CCls (all/bin/unit):\t"); + toSTDOUT(theClauses.size() - iOfsBeginConflictClauses); + toSTDOUT("/"<< numBinCCls<< "/"<::iterator begin(CClauseVertex &rCV) + { + return theLitVector.begin() + rCV.getLitOfs(); + } + + vector::const_iterator begin(const CClauseVertex &rCV) const + { + return theLitVector.begin() + rCV.getLitOfs(); + } + + const LiteralIdT & ClauseEnd() const {return SENTINEL_LIT;} + + + bool substituteLitsOf(CClauseVertex &rCl,const LiteralIdT &oldLit, const LiteralIdT &newLit); + bool containsVar(const CClauseVertex &rCl,const VarIdT &theVar) const; + bool containsLit(const CClauseVertex &rCl,const LiteralIdT &theLit) const; + + public: + + CInstanceGraph(); + ~CInstanceGraph(); + + ///////////////////////////////////////////////////////// + // BEGIN access to variables and clauses + inline vector::const_iterator var_InClsBegin(VarIdT VarIndex) const + { + return (theInClsVector.begin() + theVars[VarIndex].getInClsVecOfs(false)); + } + + inline vector::iterator var_InClsBegin(VarIdT VarIndex,bool pol) + { + return (theInClsVector.begin() + theVars[VarIndex].getInClsVecOfs(pol)); + } + + inline vector::iterator var_InClsStart(VarIdT VarIndex,bool pol) + { + return (theInClsVector.begin() + theVars[VarIndex].getInClsVecOfs(true) - 1 + (int) pol); + } + + inline int var_InClsStep(bool pol) + { + return pol?1:-1; + } + + + inline bool var_EraseClsLink(VarIdT VarIndex, bool linkPol ,ClauseIdT idCl) + { + CVariableVertex &rV = getVar(VarIndex); + vector::iterator it; + + if(!linkPol) + { + for(it = var_InClsBegin(VarIndex, true)-1; + *it != SENTINEL_CL;it--) + if(*it == idCl) + { + while(*it != SENTINEL_CL) {*it = *(it-1); it--;} + rV.setInClsVecOfs(false,rV.getInClsVecOfs(false)+1); + return true; + } + } else + { + for(it = var_InClsBegin(VarIndex, true);*it != SENTINEL_CL;it++) + if(*it == idCl) + { + while(*it!= SENTINEL_CL) {*it = *(it+1); it++;} + return true; + } + } + return false; + } + + + + inline vector::const_iterator var_InClsBegin(CVariableVertex &vv) const + { + return (theInClsVector.begin() + vv.getInClsVecOfs(false)); + } + + + inline CVariableVertex &getVar(VarIdT VarIndex) + { + return theVars[VarIndex]; + } + inline const CVariableVertex &getVar(VarIdT VarIndex) const + { + return theVars[VarIndex]; + } + + inline bool isSatisfied(const LiteralIdT &lit) const + { + return theVars[lit.toVarIdx()].getVal() == lit.polarityTriVal(); + } + inline bool isSatisfied(const ClauseIdT &iCl) const + { + return isSatisfied(getClause(iCl).idLitA()) + || isSatisfied(getClause(iCl).idLitB()); + } + + inline CVariableVertex &getVar(const LiteralIdT &rLitId) + { + return theVars[rLitId.toVarIdx()]; + } + + inline const CVariableVertex &getVar(const LiteralIdT &rLitId) const + { + return theVars[rLitId.toVarIdx()]; + } + + inline CClauseVertex &getClause(const ClauseIdT &iClauseId) + { + return theClauses[iClauseId]; + } + + inline const CClauseVertex &getClause(const ClauseIdT &iClauseId) const + { + return theClauses[iClauseId]; + } + + // END access to variables and clauses + ///////////////////////////////////////////////////////// + + inline const ClauseIdT getLastClauseId() + { + return ClauseIdT(theClauses.size()-1); + } + + + vector &getConflicted() + { + return theConflicted; + } + + // BEGIN count something + inline unsigned int countAllClauses() const + { + return theClauses.size() - 1 + countBinClauses(); + } + + inline unsigned int countCCls() const + { + return theClauses.size() - iOfsBeginConflictClauses; + } + + inline unsigned int countOriginalClauses() const + { + return theClauses.size(); + } + + inline unsigned int getMaxOriginalClIdx() const + { + return iOfsBeginConflictClauses; + } + + inline unsigned int countAllVars() + { + return theVars.size() -1; + } + + unsigned int countActiveBinLinks(VarIdT theVar) const; + + // END count something + + bool createfromFile(const char* lpstrFileName); + + + void print(); + void printCl(const CClauseVertex &rCl) const; + void printActiveClause(const ClauseIdT &idCl) const; + + protected: + // cleans up the ClausePool + /// NOTE: this does only work correctly if no CCls are present + bool prep_CleanUpPool(); + + + // only valid if no conflict clauses are present + bool prep_substituteClauses(unsigned int oldIdx, unsigned int newIdx); + bool prep_substituteVars(CVariableVertex &rV, unsigned int newIdx); + + bool markCClDeleted(ClauseIdT idCl); + + + /// only correct if theLit is conteined in idCl + bool setCClImplyingLit(ClauseIdT idCl, const LiteralIdT &theLit); + bool eraseLiteralFromCl(ClauseIdT idCl,LiteralIdT theLit); + + bool deleteConflictCls(); + bool cleanUp_deletedCCls(); + + bool createConflictClause(const vector &theCClause); + + + unsigned int makeVariable(unsigned int VarNum) + { + theVars.push_back(CVariableVertex(VarNum,theVars.size())); + return theVars.back().getVarIdT(); + } + + ClauseIdT makeClause() + { + theClauses.push_back(CClauseVertex()); + return ClauseIdT(theClauses.size()-1); + } + + ClauseIdT makeConflictClause() + { + theClauses.push_back(CClauseVertex()); + return ClauseIdT(theClauses.size()-1); + } + + bool createUnitCl(LiteralIdT Lit) + { + theUnitClauses.push_back(Lit); + if(theUClLookUp[Lit.toVarIdx()] == Lit.oppositeLit().polarityTriVal()) return false; + theUClLookUp[Lit.toVarIdx()] = Lit.polarityTriVal(); + return true; + } + + bool createBinCl(LiteralIdT LitA,LiteralIdT LitB) + { + if(getVar(LitA).hasBinLinkTo(LitB,LitA.polarity())) + { + #ifdef DEBUG + assert(getVar(LitB).hasBinLinkTo(LitA,LitB.polarity())); + toDEBUGOUT("%"); + #endif + return false; + } + getVar(LitA).addBinLink(LitA.polarity(),LitB); + getVar(LitB).addBinLink(LitB.polarity(),LitA); + numBinClauses++; + return true; + } + + bool createBinCCl(LiteralIdT LitA,LiteralIdT LitB) + { + if(getVar(LitA).hasBinLinkTo(LitB,LitA.polarity())) + { + #ifdef DEBUG + assert(getVar(LitB).hasBinLinkTo(LitA,LitB.polarity())); + #endif + return false; + } + getVar(LitA).addBinLinkCCl(LitA.polarity(),LitB); + getVar(LitB).addBinLinkCCl(LitB.polarity(),LitA); + numBinCCls++; + return true; + } + + +}; + + + +#endif // CLAUSEPOOL_H Index: /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/semantic.cache =================================================================== --- /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/semantic.cache (revision 9) +++ /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/InstanceGraph/semantic.cache (revision 9) @@ -0,0 +1,20 @@ +;; Object InstanceGraph/ +;; SEMANTICDB Tags save file +(semanticdb-project-database-file "InstanceGraph/" + :tables (list + (semanticdb-table "InstanceGraph.h" + :major-mode 'c-mode + :tags 'nil + :file "InstanceGraph.h" + ) + (semanticdb-table "InstanceGraph.cpp" + :major-mode 'c++-mode + :tags '(("InstanceGraph.h" include nil nil [1 27]) ("math.h" include (:system-flag t) nil [28 45]) ("theRunAn" variable (:type ("CRunAnalyzer" type (:type "class") nil nil)) nil [83 105]) ("CInstanceGraph" function (:constructor-flag t :parent "CInstanceGraph" :type ("CInstanceGraph" type "class")) nil [129 166]) ("CInstanceGraph" function (:destructor-flag t :parent "CInstanceGraph" :type "void") nil [189 336]) ("substituteLitsOf" function (:parent "CInstanceGraph" :arguments (("rCl" variable (:type ("CClauseVertex" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [559 578]) ("oldLit" variable (:constant-flag t :type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [578 603]) ("newLit" variable (:constant-flag t :type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [604 629])) :type ("bool" type (:type "class") nil nil)) nil [521 1247]) ("containsVar" function (:parent "CInstanceGraph" :arguments (("rCl" variable (:constant-flag t :type ("CClauseVertex" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [1282 1307]) ("theVar" variable (:constant-flag t :type ("VarIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [1308 1329])) :type ("bool" type (:type "class") nil nil)) nil [1249 1505]) ("containsLit" function (:parent "CInstanceGraph" :arguments (("rCl" variable (:constant-flag t :type ("CClauseVertex" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [1540 1565]) ("theLit" variable (:constant-flag t :type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [1566 1591])) :type ("bool" type (:type "class") nil nil)) nil [1507 1756]) ("printCl" function (:parent "CInstanceGraph" :arguments (("rCl" variable (:constant-flag t :type ("CClauseVertex" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [1789 1814])) :type "void") nil [1760 2034]) ("createConflictClause" function (:parent "CInstanceGraph" :arguments (("theCClause" variable (:constant-flag t :type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [2078 2115])) :type ("bool" type (:type "class") nil nil)) nil [2036 4835]) ("setCClImplyingLit" function (:parent "CInstanceGraph" :arguments (("idCl" variable (:type ("ClauseIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [4876 4891]) ("theLit" variable (:constant-flag t :type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [4892 4917])) :type ("bool" type (:type "class") nil nil)) nil [4837 5868]) ("cleanUp_deletedCCls" function (:parent "CInstanceGraph" :type ("bool" type (:type "class") nil nil)) nil [5870 7880]) ("deleteConflictCls" function (:parent "CInstanceGraph" :type ("bool" type (:type "class") nil nil)) nil [7883 8281]) ("markCClDeleted" function (:parent "CInstanceGraph" :arguments (("idCl" variable (:type ("ClauseIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [8319 8334])) :type ("bool" type (:type "class") nil nil)) nil [8283 8797]) ("prep_substituteClauses" function (:parent "CInstanceGraph" :arguments (("oldIdx" variable (:type "unsigned int") (reparse-symbol arg-sub-list) [9023 9043]) ("newIdx" variable (:type "unsigned int") (reparse-symbol arg-sub-list) [9044 9064])) :type ("bool" type (:type "class") nil nil)) nil [8979 9936]) ("prep_substituteVars" function (:parent "CInstanceGraph" :arguments (("rV" variable (:type ("CVariableVertex" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [9980 10000]) ("newIdx" variable (:type "unsigned int") (reparse-symbol arg-sub-list) [10001 10021])) :type ("bool" type (:type "class") nil nil)) nil [9939 11032]) ("eraseLiteralFromCl" function (:parent "CInstanceGraph" :arguments (("idCl" variable (:type ("ClauseIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [11075 11090]) ("theLit" variable (:type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [11090 11108])) :type ("bool" type (:type "class") nil nil)) nil [11035 12205]) ("prep_CleanUpPool" function (:parent "CInstanceGraph" :type ("bool" type (:type "class") nil nil)) nil [12207 15426]) ("createfromFile" function (:parent "CInstanceGraph" :arguments (("lpstrFileName" variable (:pointer 1 :constant-flag t :type "char") (reparse-symbol arg-sub-list) [15464 15490])) :type ("bool" type (:type "class") nil nil)) nil [15428 22832]) ("countActiveBinLinks" function (:parent "CInstanceGraph" :arguments (("theVar" variable (:type ("VarIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [22884 22898])) :type "unsigned int") nil [22835 23380]) ("print" function (:parent "CInstanceGraph" :type "void") nil [23382 23535]) ("printActiveClause" function (:parent "CInstanceGraph" :arguments (("idCl" variable (:constant-flag t :type ("ClauseIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [23577 23599])) :type "void") nil [23538 23909])) + :file "InstanceGraph.cpp" + :pointmax 23910 + ) + ) + :file "semantic.cache" + :semantic-tag-version "2.0beta3" + :semanticdb-version "2.0beta3" + ) Index: /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/MainSolver.cpp =================================================================== --- /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/MainSolver.cpp (revision 9) +++ /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/MainSolver.cpp (revision 9) @@ -0,0 +1,1260 @@ +#include "MainSolver.h" // class's header file + +// class constructor +CMainSolver::CMainSolver():decStack(*this) +{ + stopWatch.setTimeBound(CSolverConf::secsTimeBound); + remPoll = 0; +} + +// class destructor +CMainSolver::~CMainSolver() +{ + toDEBUGOUT("removed. Poll: "<::const_iterator it; + + int score = -1; + int bo; + PVARV pVV = NULL; + + for(it = superComp.varsBegin(); *it != varsSENTINEL; it++) + if(getVar(*it).isActive()) + { + bo = (int) getVar(*it).getVSIDSScore() + getVar(*it).getDLCSScore() ; + + if(bo > score) + { + score = bo; + pVV = &getVar(*it); + } + } + + if(pVV == NULL) return false; + + bool pol = pVV->scoreDLIS[true] + pVV->scoreVSIDS[true] > pVV->scoreDLIS[false] + pVV->scoreVSIDS[false]; + + theLit = pVV->getLitIdT(pol); + + return true; +} + + +bool CMainSolver::decide() +{ + LiteralIdT theLit(NOT_A_LIT); + + CStepTime::stepTime(); // Solver-Zeit + + + if(CStepTime::getTime() - xFormulaCache.getLastDivTime() > xFormulaCache.getScoresDivTime()) + { + xFormulaCache.divCacheScores(); + xFormulaCache.setLastDivTime(CStepTime::getTime()); + } + + + if(!bcpImplQueue.empty()) return true; + + if(!decStack.TOS_hasAnyRemComp()) + { + recordRemainingComps(); + if(decStack.TOS_countRemComps() == 0) + { + handleSolution(); + return false; + } + } + + + if(!findVSADSDecVar(theLit, decStack.TOS_NextComp()) + || decStack.TOS_NextComp().getClauseCount() == 0) // i.e. component satisfied + { + handleSolution(); + decStack.TOS_popRemComp(); + return false; + } + + //checkCachedCompVal: + static CRealNum cacheVal; + + decStack.TOS_NextComp(); + + if(CSolverConf::allowComponentCaching + && + xFormulaCache.extract(decStack.TOS_NextComp(),cacheVal)) + { + decStack.top().includeSol(cacheVal); + theRunAn.addValue(SOLUTION,decStack.getDL()); + decStack.TOS_popRemComp(); + return false; + } + ///////////////////////////// + decStack.push(); + bcpImplQueue.clear(); + bcpImplQueue.push_back(AntAndLit(NOT_A_CLAUSE,theLit)); + + theRunAn.addValue(DECISION,decStack.getDL()); + + + if(theRunAn.getData().nDecisions % 255 == 0) + { + doVSIDSScoreDiv(); + } + + return true; +} + +void CMainSolver::removeAllCachePollutions() +{ + // check if one sibling has modelcount 0 + // if so, the other siblings may have polluted the cache --> remove pollutions + // cout << decStack.getDL()<<" "<::iterator it = decStack.TOSRemComps_begin(); + it != decStack.getAllCompStack().end(); it++) + // if component *it is cached remove it and all of its descendants + if((*it)->cachedAs != 0) + { + remPoll += xFormulaCache.removePollutedEntries((*it)->cachedAs); + (*it)->cachedAs = 0; + (*it)->cachedChildren.clear(); + } + // it might occur that *it is not yet cached, but has descedants that are cached + // thus we have to delete them + else if(!(*it)->cachedChildren.empty()) + { + for(vector::iterator ct = (*it)->cachedChildren.begin(); + ct != (*it)->cachedChildren.end(); ct++) + { + remPoll += xFormulaCache.removePollutedEntries(*ct); + } + } + xFormulaCache.revalidateCacheLinksIn(decStack.getAllCompStack()); + +} + +retStateT CMainSolver::backTrack() +{ + unsigned int refTime = theRunAn.getData().nAddedClauses; + LiteralIdT aLit; + + if(refTime - lastTimeCClDeleted > 1000 + && countCCls() > 3000) + { + deleteConflictCls(); + lastTimeCClDeleted = refTime; + } + + if(refTime - lastCClCleanUp > 35000 ) + { + cleanUp_deletedCCls(); + toSTDOUT("cleaned:"); printCClstats(); + lastCClCleanUp = refTime; + } + + //component cache delete old entries + if(CSolverConf::allowComponentCaching) + xFormulaCache.deleteEntries(decStack); + + do{ + if(decStack.top().getBranchSols() == 0.0) + removeAllCachePollutions(); + + if(decStack.top().anotherCompProcessible()) + { + return PROCESS_COMPONENT; + } + + if(!decStack.top().isFlipped()) + { + aLit = decStack.TOS_decLit(); + decStack.flipTOS(); + bcpImplQueue.push_back(AntAndLit(NOT_A_CLAUSE,aLit.oppositeLit())); + return RESOLVED; + } + + //include the component value of the current component into the Cache + if(CSolverConf::allowComponentCaching) + { + xFormulaCache.include(decStack.TOSRefComp(), decStack.top().getOverallSols()); + } + + } while(decStack.pop()); + + return EXIT; +} + + + +bool CMainSolver::bcp() +{ + bool bSucceeded; + + vector::iterator it; + + //BEGIN process unit clauses + for(it = theUnitClauses.begin(); it != theUnitClauses.end(); it++) + { + if(getVar(*it).isActive()) + bcpImplQueue.push_back(AntAndLit(NOT_A_CLAUSE, *it)); + + if(isUnitCl(it->oppositeLit())) + { + // dealing with opposing unit clauses is handed over to + // resolveConflict + return false; + } + } + //END process unit clauses + + bSucceeded = BCP(bcpImplQueue); + bcpImplQueue.clear(); + + if(CSolverConf::allowImplicitBCP + && bSucceeded ) + { + bSucceeded = implicitBCP(); + } + + theRunAn.addValue(IMPLICATION, decStack.getDL(), + decStack.TOS_countImplLits()); + + + return bSucceeded; +} + + +retStateT CMainSolver::resolveConflict() +{ + int backtrackDecLev; + + for(vector::iterator it = theUnitClauses.begin(); it != theUnitClauses.end(); it++) + { + if(isUnitCl(it->oppositeLit())) + { + toSTDOUT("\nOPPOSING UNIT CLAUSES - INSTANCE UNSAT\n"); + return EXIT; + } + } + + theRunAn.addValue(CONFLICT, decStack.getDL(), 1); + + #ifdef DEBUG + assert(!getConflicted().empty()); + #endif + + if(!CSolverConf::analyzeConflicts || getConflicted().empty()) + return backTrack(); + + caGetCauses_firstUIP(getConflicted()); + backtrackDecLev = getMaxDecLevFromAnalysis(); + + + + if(ca_1UIPClause.size() < ca_lastUIPClause.size()) + create1UIPCCl(); + //BEGIN Backtracking + + if(backtrackDecLev < decStack.getDL()) + { + if(CSolverConf::doNonChronBackTracking) + while(decStack.getDL() > backtrackDecLev) + { + /// check for polluted cache Entries + removeAllCachePollutions(); + /// + decStack.pop(); + } + return backTrack(); + + } + + // maybe the other branch had some solutions + if(decStack.top().isFlipped()) + { + return backTrack(); + } + + // now: if the other branch has to be visited: + + createAntClauseFor(decStack.TOS_decLit().oppositeLit()); + + LiteralIdT aLit = decStack.TOS_decLit(); + AntecedentT ant = getVar(aLit).getAntecedent(); + decStack.flipTOS(); + + bcpImplQueue.push_back(AntAndLit(ant,aLit.oppositeLit())); + //END Backtracking + return RESOLVED; +} + + + +///////////////////////////////////////////////////// +// BEGIN component analysis +///////////////////////////////////////////////////// + + + +bool CMainSolver::recordRemainingComps() +{ + // the refComp has to be copied!! because in case that the vector + // containing it has to realloc (which might happen here) + // copying the refcomp is not necessary anymore, as the allCompsStack is a vector + // of pointers - realloc does not invalidate these + CComponentId & refSupComp = decStack.TOSRefComp(); + + viewStateT lookUpCls[getMaxOriginalClIdx()+2]; + viewStateT lookUpVars[countAllVars()+2]; + + memset(lookUpCls,NIL,sizeof(viewStateT)*(getMaxOriginalClIdx()+2)); + memset(lookUpVars,NIL,sizeof(viewStateT)*(countAllVars()+2)); + + vector::const_iterator vt; + vector::const_iterator itCl; + + for(itCl = refSupComp.clsBegin(); *itCl != clsSENTINEL; itCl++) + { + lookUpCls[*itCl] = IN_SUP_COMP; + } + + for(vt = refSupComp.varsBegin(); *vt != varsSENTINEL; vt++) + { + if(getVar(*vt).isActive()) + { + lookUpVars[*vt] = IN_SUP_COMP; + getVar(*vt).scoreDLIS[true] = 0; + getVar(*vt).scoreDLIS[false] = 0; + } + } + + vector::const_iterator itL; + + for(vt = refSupComp.varsBegin(); *vt != varsSENTINEL; vt++) + if(lookUpVars[*vt] == IN_SUP_COMP) + { + decStack.TOS_addRemComp(); + + getComp(*vt, decStack.TOSRefComp(), lookUpCls, lookUpVars); + } + + + decStack.TOS_sortRemComps(); + return true; +} + + + + +bool CMainSolver::getComp(const VarIdT &theVar, + const CComponentId &superComp, + viewStateT lookUpCls[], + viewStateT lookUpVars[]) +{ + componentSearchStack.clear(); + + lookUpVars[theVar] = SEEN; + componentSearchStack.push_back(theVar); + vector::const_iterator vt,itVEnd; + + vector::const_iterator itL; + vector::const_iterator itCl; + + CVariableVertex * pActVar; + + unsigned int nClausesSeen = 0, nBinClsSeen = 0; + + for(vt = componentSearchStack.begin(); vt !=componentSearchStack.end();vt++) + // the for-loop is applicable here because componentSearchStack.capacity() == countAllVars() + { + pActVar = &getVar(*vt); + //BEGIN traverse binary clauses + for(itL =pActVar->getBinLinks(true).begin();*itL != SENTINEL_LIT;itL++) + if(lookUpVars[itL->toVarIdx()] == IN_SUP_COMP) + { + nBinClsSeen++; + lookUpVars[itL->toVarIdx()] = SEEN; + componentSearchStack.push_back(itL->toVarIdx()); + getVar(*itL).scoreDLIS[itL->polarity()]++; + pActVar->scoreDLIS[true]++; + } + for(itL =pActVar->getBinLinks(false).begin();*itL != SENTINEL_LIT;itL++) + if(lookUpVars[itL->toVarIdx()] == IN_SUP_COMP) + { + nBinClsSeen++; + lookUpVars[itL->toVarIdx()] = SEEN; + componentSearchStack.push_back(itL->toVarIdx()); + getVar(*itL).scoreDLIS[itL->polarity()]++; + pActVar->scoreDLIS[false]++; + } + //END traverse binary clauses + + + for(itCl = var_InClsBegin(*pActVar); *itCl != SENTINEL_CL; itCl++) + if(lookUpCls[*itCl] == IN_SUP_COMP) + { + itVEnd = componentSearchStack.end(); + for(itL = begin(getClause(*itCl)); *itL != ClauseEnd(); itL++) + if(lookUpVars[itL->toVarIdx()] == NIL) //i.e. the var is not active + { + if(!isSatisfied(*itL)) continue; + //BEGIN accidentally entered a satisfied clause: undo the search process + while(componentSearchStack.end() != itVEnd) + { + lookUpVars[componentSearchStack.back()] = IN_SUP_COMP; + componentSearchStack.pop_back(); + } + lookUpCls[*itCl] = NIL; + for(vector::iterator itX = begin(getClause(*itCl));itX != itL; itX++) + { + if(getVar(*itX).scoreDLIS[itX->polarity()] > 0) getVar(*itX).scoreDLIS[itX->polarity()]--; + } + //END accidentally entered a satisfied clause: undo the search process + break; + + }else{ + + getVar(*itL).scoreDLIS[itL->polarity()]++; + if(lookUpVars[itL->toVarIdx()] == IN_SUP_COMP) + { + lookUpVars[itL->toVarIdx()] = SEEN; + componentSearchStack.push_back(itL->toVarIdx()); + } + } + + + if(lookUpCls[*itCl] == NIL) continue; + nClausesSeen++; + lookUpCls[*itCl] = SEEN; + } + } + + ///////////////////////////////////////////////// + // BEGIN store variables in resComp + ///////////////////////////////////////////////// + + decStack.lastComp().reserveSpace(componentSearchStack.size(), nClausesSeen); + + for(vt = superComp.varsBegin(); *vt != varsSENTINEL; vt++) + if(lookUpVars[*vt] == SEEN) //we have to put a var into our component + { + decStack.lastComp().addVar(*vt); + lookUpVars[*vt] = IN_OTHER_COMP; + } + + decStack.lastComp().addVar(varsSENTINEL); + + ///////////////////////////////////////////////// + // END store variables in resComp + ///////////////////////////////////////////////// + + for(itCl = superComp.clsBegin(); *itCl != clsSENTINEL; itCl++) + if(lookUpCls[*itCl] == SEEN) + { + decStack.lastComp().addCl(*itCl); + lookUpCls[*itCl] = IN_OTHER_COMP; + } + decStack.lastComp().addCl(clsSENTINEL); + decStack.lastComp().setTrueClauseCount(nClausesSeen + nBinClsSeen); + + return true; +} + + + +///////////////////////////////////////////////////// +// END component analysis +///////////////////////////////////////////////////// + + +void CMainSolver::makeCompIdFromActGraph(CComponentId& rComp) +{ + DepositOfClauses::iterator it; + DepositOfVars::iterator jt; + + rComp.clear(); + unsigned int nBinClauses = 0; + unsigned int idx = 1; + for(it = beginOfClauses(); it != endOfClauses(); it++, idx++) + { + #ifdef DEBUG + assert(!it->isDeleted()); // deleted Cls should be cleaned by prepCleanPool + #endif + rComp.addCl(ClauseIdT(idx)); + } + rComp.addCl(clsSENTINEL); + idx = 1; + for(jt = beginOfVars(); jt != endOfVars();jt++, idx++) + { + #ifdef DEBUG + assert(jt->isActive()); // deleted Vars should be cleaned by prepCleanPool + #endif + rComp.addVar(idx); + nBinClauses += countActiveBinLinks(idx); + + } + rComp.addVar(varsSENTINEL); + + nBinClauses >>=1; + rComp.setTrueClauseCount(nBinClauses + rComp.countCls()); +} + + +void CMainSolver::printComponent(const CComponentId& rComp) +{ + vector::const_iterator it; + for(it = rComp.clsBegin(); *it != clsSENTINEL;it++) + { + printActiveClause(*it); + } +} + + + + +/////////////////////////////////////////////// + +bool CMainSolver::BCP(vector &thePairsOfImpl) +{ + extd_vector* pUnWatchCls; + extd_vector::iterator it; + bool retV; + ClauseIdT actCl; + PCLV pCl; + vector::const_iterator bt; + vector::iterator itL; + LiteralIdT satLit,unLit; + + getConflicted().clear(); + + for(unsigned int i = 0; i < thePairsOfImpl.size();i++) + if(assignVal(thePairsOfImpl[i].getLit(),thePairsOfImpl[i].getAnt())) + { + satLit = thePairsOfImpl[i].getLit(); + unLit = thePairsOfImpl[i].getLit().oppositeLit(); + decStack.TOS_addImpliedLit(satLit); + + pUnWatchCls = &getVar(unLit).getWatchClauses(unLit.polarity()); + + //BEGIN Propagate Bin Clauses + for(bt = getVar(unLit).getBinLinks(unLit.polarity()).begin(); *bt != SENTINEL_LIT;bt++) + { + if(getVar(*bt).isActive()) thePairsOfImpl.push_back(AntAndLit(unLit,*bt)); + else if(!isSatisfied(*bt)) + { + getConflicted().push_back(unLit); + getConflicted().push_back(*bt); + return false; + } + } + for(bt = bt+1; *bt != SENTINEL_LIT;bt++) + { + if(getVar(*bt).isActive()) thePairsOfImpl.push_back(AntAndLit(unLit,*bt)); + else if(!isSatisfied(*bt)) + { + getConflicted().push_back(unLit); + getConflicted().push_back(*bt); + return false; + } + } + //END Propagate Bin Clauses + + for(it = pUnWatchCls->end()-1; *it != SENTINEL_CL; it--) + { + actCl = *it; + pCl = &getClause(actCl); + // all clauses treated as conflict clauses, because no subsumption + // is being performed + if(isSatisfied(pCl->idLitA()) || isSatisfied(pCl->idLitB())) continue; + /////////////////////////////////////// + //BEGIN update watched Lits + /////////////////////////////////////// + retV = false; + for(itL = begin(*pCl); *itL != ClauseEnd(); itL++) + if(getVar(*itL).isActive() || isSatisfied(*itL)) + { + if(*itL == pCl->idLitA() || *itL == pCl->idLitB()) continue; + retV = isSatisfied(*itL); + getVar(*itL).addWatchClause(actCl,itL->polarity()); + if(pCl->idLitA() == unLit) + pCl->setLitA(*itL); + else + pCl->setLitB(*itL); + pUnWatchCls->quickErase(it); + break; + } + if(retV) continue; // i.e. clause satisfied + /////////////////////////////////////// + //END update watched Lits + /////////////////////////////////////// + + if(getVar(pCl->idLitA()).isActive()) + { + if(!getVar(pCl->idLitB()).isActive()) //IMPLIES_LITA; + { + thePairsOfImpl.push_back(AntAndLit(actCl,pCl->idLitA())); + pCl->setTouched(); + } + } + else + { + pCl->setTouched(); + if(getVar(pCl->idLitB()).isActive()) //IMPLIES_LITB; + thePairsOfImpl.push_back(AntAndLit(actCl,pCl->idLitB())); + else //provided that SATISFIED has been tested + { + getConflicted().push_back(actCl); + return false; + } + } + } + } + return true; +} + + +bool CMainSolver::createAntClauseFor(const LiteralIdT &Lit) +{ + const vector &actCCl = caGetPrevLastUIPCCl(); + + bool created = createLastUIPCCl(); + + if(!created && actCCl.size() != 2) return false; + + if(actCCl.size() == 1) + { + getVar(Lit).adjustAntecedent(NOT_A_CLAUSE); + return true; // theLit has become a unit clause: nothing to be done + } + if(actCCl.size() == 2) + { + #ifdef DEBUG + assert(actCCl.front() != Lit.oppositeLit()); + assert(actCCl.back() != Lit.oppositeLit()); + #endif + + if(actCCl.front() == Lit) + getVar(Lit).adjustAntecedent(AntecedentT(actCCl.back())); + else if(actCCl.back() == Lit) + getVar(Lit).adjustAntecedent(AntecedentT(actCCl.front())); + + return true; + } + setCClImplyingLit(getLastClauseId(),Lit); + getVar(Lit).adjustAntecedent(AntecedentT(getLastClauseId())); + return true; +} + +bool CMainSolver::implicitBCP() +{ + vector::iterator jt; + vector::const_iterator it,lt; + vector::const_iterator ct; + + static vector implPairs; + implPairs.clear(); + vector nextStep; + bool viewedLits[(countAllVars()+1)*2 +1]; + LiteralIdT newLit; + AntecedentT theAnt, nant; + LiteralIdT theLit,nlit; + implPairs.reserve(decStack.TOSRefComp().countVars()); + nextStep.reserve(decStack.TOSRefComp().countVars()); + int allFound = 0; + bool bsat; + + int impOfs = 0; + int step; + do{ + if(decStack.TOS_countImplLits() - impOfs > 0) + { + memset(viewedLits,false,sizeof(bool)*((countAllVars()+1)*2 +1)); + nextStep.clear(); + for(it = decStack.TOS_ImpliedLits_begin()+ impOfs; it != decStack.TOS_ImpliedLits_end(); it++) + { + step = var_InClsStep(!it->polarity()); + for(ct = var_InClsStart(it->toVarIdx(),!it->polarity()); *ct != SENTINEL_CL; ct+= step) + { + bsat = false; + for(lt = begin(getClause(*ct));*lt != ClauseEnd(); lt++) + { + if(isSatisfied(*lt)) { bsat = true; break; } + } + + if(bsat) continue; + for(lt = begin(getClause(*ct));*lt != ClauseEnd(); lt++) + if(getVar(*lt).isActive() && !viewedLits[lt->toUInt()]) + { + nextStep.push_back(*lt); + viewedLits[lt->toUInt()] = true; + } + } + } + } + impOfs = decStack.TOS_countImplLits(); + + for(jt = nextStep.begin(); jt != nextStep.end(); jt++) + if(getVar(*jt).isActive()) + { + implPairs.push_back(AntAndLit(NOT_A_CLAUSE,jt->oppositeLit())); + // BEGIN BCPROPAGATIONNI + unsigned int sz = decStack.countAllImplLits(); + + // we increase the decLev artificially + // s.t. after the tentative BCP call, we can learn a conflict clause + // relative to the assignment of *jt + decStack.beginTentative(); + + bool bSucceeded = BCP(implPairs); + + + decStack.shrinkImplLitsTo(sz); + theAnt = NOT_A_CLAUSE; + theLit = implPairs[0].getLit(); + + if(!bSucceeded && CSolverConf::analyzeConflicts + && !getConflicted().empty()) + { + + caGetCauses_lastUIP(getConflicted()); + + createAntClauseFor(theLit.oppositeLit()); + //createLastUIPCCl(); + + theRunAn.addValue(IBCPIMPL,decStack.getDL(),1); + theAnt = getVar(theLit).getAntecedent(); + + } + decStack.endTentative(); + + for(vector::iterator at = implPairs.begin(); at != implPairs.end(); at++) + getVar(at->theLit).unsetVal(); + implPairs.clear(); + + if(!bSucceeded) + { + implPairs.push_back(AntAndLit(theAnt,theLit.oppositeLit())); + + if(!BCP(implPairs)) + { + implPairs.clear(); + return false; + } + + implPairs.clear(); + } + // END BCPROPAGATIONNI + } + allFound += decStack.TOS_countImplLits() - impOfs; + + }while(decStack.TOS_countImplLits() - impOfs > 0); + return true; +} + +/////////////////////////////////////////////////////////////////////////////////////////////// +// BEGIN module conflictAnalyzer +/////////////////////////////////////////////////////////////////////////////////////////////// + + +void CMainSolver::caIncludeCauses(LiteralIdT theLit, bool viewedVars[]) +{ + vector::const_iterator it; + + ClauseIdT implCl; + + if(!getVar(theLit).getAntecedent().isAClause()) + { + LiteralIdT hlit; + hlit = getVar(theLit).getAntecedent().toLit(); + caIncorporateLit(hlit,viewedVars); + #ifdef DEBUG + assert(hlit != NOT_A_LIT); + #endif + return; + } + + implCl = getVar(theLit).getAntecedent().toCl(); + + if(implCl == NOT_A_CLAUSE) + // theLit has not been implied, in fact this means that + // either theLit is the decided variable, a unit clause or + // a variable that has been tentatively assigned by ImplicitBCP + // other cases may not occur ! + { + caAddtoCauses(theLit,viewedVars); + return; + } + + for(it = begin(getClause(implCl)); *it != ClauseEnd(); it ++) + { + caIncorporateLit(*it,viewedVars); + } +} +/////////////////////////////////////////////////////////////////// +// +// BEGIN public +// +/////////////////////////////////////////////////////////////////// + +void CMainSolver::caAddtoCauses(LiteralIdT theLit, bool viewedVars[]) +{ + viewedVars[theLit.toVarIdx()] = true; + + ca_lastUIPClause.push_back(theLit.oppositeLit()); + + if(getVar(theLit).getDLOD() > imaxDecLev) imaxDecLev = getVar(theLit).getDLOD(); +} + +void CMainSolver::caIncorporateLit(const LiteralIdT &Lit, bool viewedVars[]) +{ + if(Lit == NOT_A_LIT) return; + + if(!viewedVars[Lit.toVarIdx()]) + { + viewedVars[Lit.toVarIdx()] = true; + //// + getVar(Lit).scoreVSIDS[Lit.polarity()]++; + getVar(Lit).scoreVSIDS[Lit.oppositeLit().polarity()]++; + //// + if(getVar(Lit).getDLOD() == decStack.getDL()) + { + theQueue.push_back(Lit.oppositeLit()); + } + else caAddtoCauses(Lit.oppositeLit(),viewedVars); + } +} + +bool CMainSolver::caInit(vector & theConflicted, bool viewedVars[]) +{ + vector::const_iterator it; + + imaxDecLev = -1; + + ca_1UIPClause.clear(); + ca_lastUIPClause.clear(); + + theQueue.clear(); + theQueue.reserve(countAllVars()+1); + + ClauseIdT idConflCl; + LiteralIdT idConflLit; + + if(theConflicted[0].isAClause()) + { + idConflCl = theConflicted[0].toCl(); + + for(it = begin(getClause(idConflCl)); *it != ClauseEnd(); it ++) + { + caIncorporateLit(*it,viewedVars); + } + } + else + { + if(theConflicted.size() < 2) + { + toSTDOUT("error in getcauses bincl"< & theConflicted) +{ + vector::const_iterator it; + bool viewedVars[countAllVars()+1]; + + memset(viewedVars,false,sizeof(bool)*(countAllVars()+1)); + + if(!caInit(theConflicted,viewedVars)) return false; + + for(unsigned int i = 0; i < theQueue.size();i++) + { + viewedVars[theQueue[i].toVarIdx()] = true; + caIncludeCauses(theQueue[i], viewedVars); + } + + // analyzer data + theRunAn.addValue(CCL_lastUIP, decStack.getDL(),ca_lastUIPClause.size()); + return true; +} + + +bool CMainSolver::caGetCauses_firstUIP(vector & theConflicted) +{ + vector::const_iterator it; + bool viewedVars[countAllVars()+1]; + + memset(viewedVars,false,sizeof(bool)*(countAllVars()+1)); + + if(!caInit(theConflicted,viewedVars)) return false; + + bool pastfirstUIP = false; + + for(unsigned int i = 0; i < theQueue.size();i++) + { + + if(i == theQueue.size()-1 && pastfirstUIP == false) + { + pastfirstUIP = true; + + ca_1UIPClause = ca_lastUIPClause; + + ca_1UIPClause.push_back(theQueue.back().oppositeLit()); + } + viewedVars[theQueue[i].toVarIdx()] = true; + caIncludeCauses(theQueue[i], viewedVars); + } + // analyzer data + theRunAn.addValue(CCL_1stUIP, decStack.getDL(), ca_1UIPClause.size()); + theRunAn.addValue(CCL_lastUIP, decStack.getDL(),ca_lastUIPClause.size()); + + return true; +} + +/////////////////////////////////////////////////////////////////////////////////////////////// +// END module conflictAnalyzer +/////////////////////////////////////////////////////////////////////////////////////////////// + + + +//////////////////////////////////////////////////////////////////////// +// +// BEGIN Methods for Preprocessing +// +/////////////////////////////////////////////////////////////////////// + +bool CMainSolver::prep_IBCP(vector &impls) +{ + bool bSucceeded = false; + + getConflicted().clear(); + + unsigned int sz = decStack.countAllImplLits(); + + bSucceeded = BCP(impls); + decStack.shrinkImplLitsTo(sz); + + vector::iterator it; + + for(it = impls.begin(); it != impls.end(); it++) + { + getVar(it->theLit).unsetVal(); + } + + impls.clear(); + return bSucceeded; +} + +bool CMainSolver::prepFindHiddenBackBoneLits() +{ + DepositOfVars::iterator jt; + vector implPairs; + implPairs.reserve(countAllVars()); + + int foundInLoop = 0; + int allFound = 0; + + do{ + foundInLoop = 0; + + for(jt = beginOfVars(); jt != endOfVars(); jt++) + if(jt->isActive() && jt->countBinLinks() > 0) + { + if(jt->countBinLinks(false)>0) implPairs.push_back(AntAndLit(NOT_A_CLAUSE,jt->getLitIdT(true))); + if((jt->countBinLinks(false)>0) && !prep_IBCP(implPairs)) + { + foundInLoop++; + if(!prepBCP(jt->getLitIdT(false))) return false; + } + else if(jt->countBinLinks(true)>0) + { + implPairs.push_back(AntAndLit(NOT_A_CLAUSE,jt->getLitIdT(false))); + if(!prep_IBCP(implPairs)) + { + foundInLoop++; + if(!prepBCP(jt->getLitIdT(true))) return false; + } + } + } + allFound += foundInLoop; + + }while(foundInLoop != 0); + if(allFound != 0) toSTDOUT("found UCCL"< impls; + int step = 0; + LiteralIdT unLit, satLit; + + impls.reserve(countAllVars()); + + if(firstLit != NOT_A_LIT) impls.push_back(firstLit); + + // prepare UnitClauses for BCP + if(!theUnitClauses.empty()) + { + impls.insert(impls.end(),theUnitClauses.begin(),theUnitClauses.end()); + theUnitClauses.clear(); + theUClLookUp.clear(); + } + + vector::iterator it; + vector::iterator itBegin; + vector::iterator lt; + CVariableVertex *pV; + + for(unsigned int i = 0; i < impls.size();i++) + if(getVar(impls[i]).setVal(impls[i].polarity(), 0)) + { + unLit = impls[i].oppositeLit(); + satLit = impls[i]; + pV = &getVar(satLit); + + // BEGIN propagation + for(lt = pV->getBinLinks(unLit.polarity()).begin(); *lt != SENTINEL_LIT;lt++) + { + if(getVar(*lt).isActive()) impls.push_back(*lt); + else + if(getVar(*lt).getboolVal() != lt->polarity()) return false; + } + CClauseVertex *pCl; + + itBegin = var_InClsStart(unLit.toVarIdx(),unLit.polarity()); + step = var_InClsStep(unLit.polarity()); + + for(it = itBegin; *it != SENTINEL_CL; it+= step) + if(!getClause(*it).isDeleted()) + { + pCl = &getClause(*it); + eraseLiteralFromCl(*it,unLit); + switch(getClause(*it).length()) + { + case 0: return false; + case 1: impls.push_back(*begin(*pCl)); + break; + case 2: + createBinCl((*begin(*pCl)),*(begin(*pCl)+1)); + /// mark clause *it as deleted + + getVar(pCl->idLitB()).eraseWatchClause(*it, pCl->idLitB().polarity()); + getVar(pCl->idLitA()).eraseWatchClause(*it, pCl->idLitA().polarity()); + + for(vector::iterator litt = begin(*pCl); *litt != ClauseEnd();litt++) + { + if(*litt != unLit) + var_EraseClsLink(litt->toVarIdx(), litt->polarity(),*it); + *litt = NOT_A_LIT; + } + + pCl->setDeleted(); + + /// + break; + default: break; + }; + } + //END propagation + + //BEGIN subsumption + for(lt = pV->getBinLinks(satLit.polarity()).begin(); *lt != SENTINEL_LIT;lt++) + getVar(*lt).eraseBinLinkTo(satLit,lt->polarity()); + + itBegin = var_InClsStart(satLit.toVarIdx(),satLit.polarity()); + step = var_InClsStep(satLit.polarity()); + + for(it = itBegin; *it != SENTINEL_CL;it+= step) + + if(!getClause(*it).isDeleted()) + { + pCl = &getClause(*it); + /// mark clause *it as deleted + + getVar(pCl->idLitB()).eraseWatchClause(*it, pCl->idLitB().polarity()); + getVar(pCl->idLitA()).eraseWatchClause(*it, pCl->idLitA().polarity()); + + vector::iterator litt; + for(litt = begin(*pCl); *litt != ClauseEnd();litt++) + { + if(*litt != satLit) + // deleting ClauseEdges from satLit would be erroneous as it affects satPCl + var_EraseClsLink(litt->toVarIdx(), litt->polarity(),*it); + *litt = NOT_A_LIT; + } + + pCl->setDeleted(); + /// + } + // END subsumption + + for(it = var_InClsBegin(unLit.toVarIdx(),false);*it != SENTINEL_CL;it++) + { + *it = SENTINEL_CL; + } + + pV->eraseAllEdges(); + } + return true; +} + + +//////////////////////////////////////////////////////////////////////// +// +// END Methods for Preprocessing +// +/////////////////////////////////////////////////////////////////////// + + +bool CMainSolver::printUnitClauses() +{ + vector::iterator it,jt; + + toSTDOUT("UCCL:\n"); + for(it = theUnitClauses.begin(); it != theUnitClauses.end(); it++) + { + toSTDOUT((it->polarity()?" ":"-")< + +#include "../Basics.h" +#include "InstanceGraph/InstanceGraph.h" + +#include "FormulaCache.h" + + +/** \addtogroup Interna Solver Interna + * Dies sind alle Klassen, die ausschlieï¿œich vom Solver selbst verwendet werden + * sollten. + */ + + +/*@{*/ + +typedef unsigned char viewStateT; +#define NIL 0 +#define IN_SUP_COMP 1 +#define SEEN 2 +#define IN_OTHER_COMP 3 + +enum retStateT{ + + EXIT, + RESOLVED, + PROCESS_COMPONENT +}; + +enum retIBCPT +{ + NOTHING_FOUND, + FOUND, + CONTRADICTION, +}; + + +class CMainSolver : public CInstanceGraph +{ + CDecisionStack decStack; // decision stack + CStopWatch stopWatch; + + CFormulaCache xFormulaCache; + vector bcpImplQueue; + + int lastTimeCClDeleted; + int lastCClCleanUp; + + unsigned int remPoll; + + retStateT backTrack(); + + // removes all cachePollutions that might be present in decedants of comnponents from the + // present decision level + void removeAllCachePollutions(); + + + bool findVSADSDecVar(LiteralIdT &theLit, const CComponentId & superComp); + + + bool decide(); + + bool bcp(); + + void handleSolution() + { + int actCompVars = 0; + static CRealNum rnCodedSols; + + // in fact the active component should only contain active vars + if(decStack.TOS_countRemComps() != 0) + actCompVars = decStack.TOS_NextComp().countVars(); + + pow2(rnCodedSols, actCompVars); + decStack.top().includeSol(rnCodedSols); + theRunAn.addValue(SOLUTION, decStack.getDL()); + + } + + retStateT resolveConflict(); + + SOLVER_StateT countSAT(); + + bool performPreProcessing(); + + + /** + * passes a componentId to rComp that is made of all + * active variables and clauses + * !! used to initialize decStack at DL zero + **/ + void makeCompIdFromActGraph(CComponentId& rComp); + + // BEGIN component analysis + vector componentSearchStack; + bool recordRemainingComps(); + bool getComp(const VarIdT &theVar, + const CComponentId &superComp, + viewStateT lookUpCls[], + viewStateT lookUpVars[]); + // END component analysis + + void printComponent(const CComponentId& rComp); + + + inline bool assignVal(const LiteralIdT &rLitId, AntecedentT ant = AntecedentT(NOT_A_CLAUSE)) + { + return getVar(rLitId).setVal(rLitId.polarity(), decStack.getDL(), ant); + } + + bool BCP(vector &thePairsOfImpl); + + ///////////////////////////////////////////// + // BEGIN conflict analysis + ///////////////////////////////////////////// + + private: + + vector theQueue; + vector ca_1UIPClause; + vector ca_lastUIPClause; + + int imaxDecLev; + + // includes the causes of a variable assignment via + // breadth first search + void caIncludeCauses(LiteralIdT theLit, bool viewedVars[]); + void caIncorporateLit(const LiteralIdT &Lit, bool viewedVars[]); + + void caAddtoCauses(LiteralIdT theLit, bool viewedVars[]); + // initializes all data structures for the analysis + // especially the startin point of the analysis i plugged into the queue + bool caInit(vector & theConflicted, bool viewedVars[]); + + + bool caGetCauses_lastUIP(vector & theConflicted); + bool caGetCauses_firstUIP(vector & theConflicted); + + // whenever a variable that is not implied causes a conflict + // the conflict clause generated from this conflict implies a flip + // of that variable: + // creation of that clause and recording the implication is done by: + + const vector &caGetPrev1UIPCCl() + { + return ca_1UIPClause; + } + const vector &caGetPrevLastUIPCCl() + { + return ca_lastUIPClause; + } + + /// ermittelt den maximalen Entscheidungslevel von + /// Variablen die zu den Konfliktursachen gehï¿œen. + /// Ein Aufruf ist erst nach dem Auftruf von getCausesOf sinnvoll + int getMaxDecLevFromAnalysis() const {return imaxDecLev;} + + /// gibt KonfliktKlausel zurck die durch die + /// vorhergehende Analyse gewonnen wurde + bool create1UIPCCl() + { + return createConflictClause(ca_1UIPClause); + } + + bool createLastUIPCCl() + { + return createConflictClause(ca_lastUIPClause); + } + + ///////////////////////////////////////////// + // END conflict analysis + ///////////////////////////////////////////// + + ///////////////////////////////////////////// + // BEGIN implicitBCP + ///////////////////////////////////////////// + + /// this method is used for heuristically testing variable assignments + /// whether they incur a conflict. If so we can infer the opposite assignment of + /// the variable in question + /// Thus the method will then perform the assignment + /// Furthermore it manages the necessary entries to the decision stack itself + /// returned value: analogously to the bcp procedure: false iff a conflict is found + bool implicitBCP(); + + bool createAntClauseFor(const LiteralIdT &Lit); + + ///////////////////////////////////////////// + // END implicitBCP + ///////////////////////////////////////////// + + ///////////////////////////////////////////// + // BEGIN PreProcessing methods + //////////////////////////////////////////// + + ///NOTE: Preprocessing methods assume that no conflict clauses are present ! + + bool prep_IBCP(vector &impls); + /// Preprocessing + /// i.e. the "hard" version of ImplicitBCP + /// used for preprosessing ONLY + bool prepFindHiddenBackBoneLits(); + + /// Apply the BCP rule in a Preprocessing step: + /// That is: if firstLit is a valid literal, propagation is started there + /// firstLit should not be assigned already! + /// furthermore ALL unit clauses are processed + bool prepBCP(LiteralIdT firstLit = NOT_A_LIT); + + ///////////////////////////////////////////// + // END PreProcessing methods + ///////////////////////////////////////////// + + bool printUnitClauses(); + + public: + + // class constructor + CMainSolver(); + + // class destructor + ~CMainSolver(); + + void solve(const char *lpstrFileName); + + void setTimeBound(long int i) + { + stopWatch.setTimeBound(i); + } + +}; + + +/*@}*/ +#endif // SOLVER_H + + Index: /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/semantic.cache =================================================================== --- /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/semantic.cache (revision 9) +++ /vis_dev/sharpSAT/src/src_sharpSAT/MainSolver/semantic.cache (revision 9) @@ -0,0 +1,27 @@ +;; Object MainSolver/ +;; SEMANTICDB Tags save file +(semanticdb-project-database-file "MainSolver/" + :tables (list + (semanticdb-table "MainSolver.h" + :major-mode 'c-mode + :tags '(("MAINSOLVER_H" variable (:constant-flag t) nil [22 60]) ("Interface/AnalyzerData.h" include (:system-flag t) nil [59 94]) ("../Basics.h" include nil nil [96 118]) ("InstanceGraph/InstanceGraph.h" include nil nil [119 159]) ("FormulaCache.h" include nil nil [161 186]) ("viewStateT" type (:typedef ("unsigned char") :superclasses "unsigned char" :type "typedef") nil [339 372]) ("NIL" variable (:constant-flag t :default-value (nil)) nil [373 389]) ("IN_SUP_COMP" variable (:constant-flag t :default-value (nil)) nil [390 414]) ("SEEN" variable (:constant-flag t :default-value (nil)) nil [415 431]) ("IN_OTHER_COMP" variable (:constant-flag t :default-value (nil)) nil [432 458]) ("retStateT" type (:members (("EXIT" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [478 483]) ("RESOLVED" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [485 494]) ("PROCESS_COMPONENT" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [496 515])) :type "enum") nil [460 516]) ("retIBCPT" type (:members (("NOTHING_FOUND" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [536 550]) ("FOUND" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [552 558]) ("CONTRADICTION" variable (:constant-flag t :type "int") (reparse-symbol enumsubparts) [560 574])) :type "enum") nil [519 577]) ("CMainSolver" type (:superclasses ("CInstanceGraph") :members (("decStack" variable (:type ("CDecisionStack" type (:type "class") nil nil)) (reparse-symbol classsubparts) [630 654]) ("stopWatch" variable (:type ("CStopWatch" type (:type "class") nil nil)) (reparse-symbol classsubparts) [689 712]) ("xFormulaCache" variable (:type ("CFormulaCache" type (:type "class") nil nil)) (reparse-symbol classsubparts) [722 750]) ("bcpImplQueue" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol classsubparts) [756 787]) ("lastTimeCClDeleted" variable (:type "int") (reparse-symbol classsubparts) [810 833]) ("lastCClCleanUp" variable (:type "int") (reparse-symbol classsubparts) [837 856]) ("remPoll" variable (:type "unsigned int") (reparse-symbol classsubparts) [864 885]) ("backTrack" function (:prototype-flag t :type ("retStateT" type (:type "class") nil nil)) (reparse-symbol classsubparts) [893 915]) ("removeAllCachePollutions" function (:prototype-flag t :type "void") (reparse-symbol classsubparts) [1052 1084]) ("findVSADSDecVar" function (:prototype-flag t :arguments (("theLit" variable (:type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [1118 1137]) ("superComp" variable (:constant-flag t :type ("CComponentId" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [1138 1169])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [1097 1170]) ("decide" function (:prototype-flag t :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [1179 1193]) ("bcp" function (:prototype-flag t :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [1201 1212]) ("handleSolution" function (:type "void") (reparse-symbol classsubparts) [1222 1671]) ("resolveConflict" function (:prototype-flag t :type ("retStateT" type (:type "class") nil nil)) (reparse-symbol classsubparts) [1679 1707]) ("countSAT" function (:prototype-flag t :type ("SOLVER_StateT" type (:type "class") nil nil)) (reparse-symbol classsubparts) [1719 1744]) ("performPreProcessing" function (:prototype-flag t :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [1756 1784]) ("makeCompIdFromActGraph" function (:prototype-flag t :arguments (("rComp" variable (:type ("CComponentId" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [1985 2005])) :type "void") (reparse-symbol classsubparts) [1957 2006]) ("componentSearchStack" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol classsubparts) [2048 2084]) ("recordRemainingComps" function (:prototype-flag t :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [2093 2121]) ("getComp" function (:prototype-flag t :arguments (("theVar" variable (:constant-flag t :type ("VarIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [2142 2163]) ("superComp" variable (:constant-flag t :type ("CComponentId" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [2186 2216]) ("lookUpCls" variable (:dereference 1 :type ("viewStateT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [2225 2248]) ("lookUpVars" variable (:dereference 1 :type ("viewStateT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [2256 2280])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [2129 2281]) ("printComponent" function (:prototype-flag t :arguments (("rComp" variable (:constant-flag t :type ("CComponentId" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [2338 2364])) :type "void") (reparse-symbol classsubparts) [2318 2365]) ("assignVal" function (:typemodifiers ("inline") :arguments (("rLitId" variable (:constant-flag t :type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [2403 2428]) ("ant" variable (:default-value "AntecedentT(NOT_A_CLAUSE)" :type ("AntecedentT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [2429 2472])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [2381 2561]) ("BCP" function (:prototype-flag t :arguments (("thePairsOfImpl" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [2578 2612])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [2569 2613]) ("private" label nil (reparse-symbol classsubparts) [2753 2761]) ("theQueue" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol classsubparts) [2770 2798]) ("ca_1UIPClause" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol classsubparts) [2809 2842]) ("ca_lastUIPClause" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol classsubparts) [2850 2886]) ("imaxDecLev" variable (:type "int") (reparse-symbol classsubparts) [2903 2918]) ("caIncludeCauses" function (:prototype-flag t :arguments (("theLit" variable (:type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3039 3057]) ("viewedVars" variable (:dereference 1 :type ("bool" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3058 3076])) :type "void") (reparse-symbol classsubparts) [3018 3077]) ("caIncorporateLit" function (:prototype-flag t :arguments (("Lit" variable (:constant-flag t :type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3110 3132]) ("viewedVars" variable (:dereference 1 :type ("bool" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3133 3151])) :type "void") (reparse-symbol classsubparts) [3088 3152]) ("caAddtoCauses" function (:prototype-flag t :arguments (("theLit" variable (:type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3179 3197]) ("viewedVars" variable (:dereference 1 :type ("bool" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3198 3216])) :type "void") (reparse-symbol classsubparts) [3160 3217]) ("caInit" function (:prototype-flag t :arguments (("theConflicted" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3364 3400]) ("viewedVars" variable (:dereference 1 :type ("bool" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3401 3419])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [3352 3420]) ("caGetCauses_lastUIP" function (:prototype-flag t :arguments (("theConflicted" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3453 3489])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [3428 3490]) ("caGetCauses_firstUIP" function (:prototype-flag t :arguments (("theConflicted" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3520 3556])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [3494 3557]) ("caGetPrev1UIPCCl" function (:constant-flag t :type ("vector" type (:type "class") nil nil)) (reparse-symbol classsubparts) [3799 3881]) ("caGetPrevLastUIPCCl" function (:constant-flag t :type ("vector" type (:type "class") nil nil)) (reparse-symbol classsubparts) [3885 3973]) ("getMaxDecLevFromAnalysis" function (:type "int") (reparse-symbol classsubparts) [4156 4213]) ("create1UIPCCl" function (:type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [4313 4393]) ("createLastUIPCCl" function (:type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [4401 4487]) ("implicitBCP" function (:prototype-flag t :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [5175 5194]) ("createAntClauseFor" function (:prototype-flag t :arguments (("Lit" variable (:constant-flag t :type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [5229 5251])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [5205 5252]) ("prep_IBCP" function (:prototype-flag t :arguments (("impls" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [5622 5647])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [5607 5648]) ("prepFindHiddenBackBoneLits" function (:prototype-flag t :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [5754 5788]) ("prepBCP" function (:prototype-flag t :arguments (("firstLit" variable (:default-value "NOT_A_LIT)" :type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [6035 6067])) :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [6022 6068]) ("printUnitClauses" function (:prototype-flag t :type ("bool" type (:type "class") nil nil)) (reparse-symbol classsubparts) [6207 6231]) ("public" label nil (reparse-symbol classsubparts) [6238 6245]) ("CMainSolver" function (:prototype-flag t :constructor-flag t :type ("CMainSolver" type "class")) (reparse-symbol classsubparts) [6277 6291]) ("CMainSolver" function (:prototype-flag t :destructor-flag t :type "void") (reparse-symbol classsubparts) [6325 6340]) ("solve" function (:prototype-flag t :arguments (("lpstrFileName" variable (:pointer 1 :constant-flag t :type "char") (reparse-symbol arg-sub-list) [6360 6386])) :type "void") (reparse-symbol classsubparts) [6349 6387]) ("setTimeBound" function (:arguments (("i" variable (:type "long int") (reparse-symbol arg-sub-list) [6414 6425])) :type "void") (reparse-symbol classsubparts) [6396 6468])) :type "class") nil [581 6472])) + :file "MainSolver.h" + :pointmax 6503 + :unmatched-syntax 'nil + ) + (semanticdb-table "MainSolver.cpp" + :major-mode 'c++-mode + :tags '(("MainSolver.h" include nil nil [1 24]) ("CMainSolver" function (:constructor-flag t :parent "CMainSolver" :type ("CMainSolver" type "class")) nil [70 189]) ("CMainSolver" function (:destructor-flag t :parent "CMainSolver" :type "void") nil [211 292]) ("performPreProcessing" function (:parent "CMainSolver" :type ("bool" type (:type "class") nil nil)) nil [296 1080]) ("solve" function (:parent "CMainSolver" :arguments (("lpstrFileName" variable (:pointer 1 :constant-flag t :type "char") (reparse-symbol arg-sub-list) [1106 1132])) :type "void") nil [1082 2618]) ("countSAT" function (:parent "CMainSolver" :type ("SOLVER_StateT" type (:type "class") nil nil)) nil [2621 3225]) ("findVSADSDecVar" function (:parent "CMainSolver" :arguments (("theLit" variable (:type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3263 3282]) ("superComp" variable (:constant-flag t :type ("CComponentId" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [3283 3314])) :type ("bool" type (:type "class") nil nil)) nil [3229 3927]) ("decide" function (:parent "CMainSolver" :type ("bool" type (:type "class") nil nil)) nil [3930 5504]) ("removeAllCachePollutions" function (:parent "CMainSolver" :type "void") nil [5506 6634]) ("backTrack" function (:parent "CMainSolver" :type ("retStateT" type (:type "class") nil nil)) nil [6636 7973]) ("bcp" function (:parent "CMainSolver" :type ("bool" type (:type "class") nil nil)) nil [7977 8899]) ("resolveConflict" function (:parent "CMainSolver" :type ("retStateT" type (:type "class") nil nil)) nil [8902 10619]) ("recordRemainingComps" function (:parent "CMainSolver" :type ("bool" type (:type "class") nil nil)) nil [10762 12132]) ("getComp" function (:parent "CMainSolver" :arguments (("theVar" variable (:constant-flag t :type ("VarIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [12163 12184]) ("superComp" variable (:constant-flag t :type ("CComponentId" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [12207 12237]) ("lookUpCls" variable (:dereference 1 :type ("viewStateT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [12245 12268]) ("lookUpVars" variable (:dereference 1 :type ("viewStateT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [12277 12301])) :type ("bool" type (:type "class") nil nil)) nil [12137 16045]) ("makeCompIdFromActGraph" function (:parent "CMainSolver" :arguments (("rComp" variable (:type ("CComponentId" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [16226 16246])) :type "void") nil [16185 17052]) ("printComponent" function (:parent "CMainSolver" :arguments (("rComp" variable (:constant-flag t :type ("CComponentId" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [17088 17114])) :type "void") nil [17055 17250]) ("BCP" function (:parent "CMainSolver" :arguments (("thePairsOfImpl" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [17326 17360])) :type ("bool" type (:type "class") nil nil)) nil [17304 20632]) ("createAntClauseFor" function (:parent "CMainSolver" :arguments (("Lit" variable (:constant-flag t :type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [20672 20694])) :type ("bool" type (:type "class") nil nil)) nil [20635 21562]) ("implicitBCP" function (:parent "CMainSolver" :type ("bool" type (:type "class") nil nil)) nil [21564 24929]) ("caIncludeCauses" function (:parent "CMainSolver" :arguments (("theLit" variable (:type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [25192 25210]) ("viewedVars" variable (:dereference 1 :type ("bool" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [25211 25229])) :type "void") nil [25158 26026]) ("caAddtoCauses" function (:parent "CMainSolver" :arguments (("theLit" variable (:type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [26219 26237]) ("viewedVars" variable (:dereference 1 :type ("bool" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [26238 26256])) :type "void") nil [26187 26447]) ("caIncorporateLit" function (:parent "CMainSolver" :arguments (("Lit" variable (:constant-flag t :type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [26484 26506]) ("viewedVars" variable (:dereference 1 :type ("bool" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [26507 26525])) :type "void") nil [26449 26934]) ("caInit" function (:parent "CMainSolver" :arguments (("theConflicted" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [26961 26997]) ("viewedVars" variable (:dereference 1 :type ("bool" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [26998 27016])) :type ("bool" type (:type "class") nil nil)) nil [26936 27787]) ("caGetCauses_lastUIP" function (:parent "CMainSolver" :arguments (("theConflicted" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [27827 27863])) :type ("bool" type (:type "class") nil nil)) nil [27789 28337]) ("caGetCauses_firstUIP" function (:parent "CMainSolver" :arguments (("theConflicted" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [28379 28415])) :type ("bool" type (:type "class") nil nil)) nil [28340 29216]) ("prep_IBCP" function (:parent "CMainSolver" :arguments (("impls" variable (:type ("vector" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [29660 29685])) :type ("bool" type (:type "class") nil nil)) nil [29632 30046]) ("prepFindHiddenBackBoneLits" function (:parent "CMainSolver" :type ("bool" type (:type "class") nil nil)) nil [30048 31197]) ("prepBCP" function (:parent "CMainSolver" :arguments (("firstLit" variable (:type ("LiteralIdT" type (:type "class") nil nil)) (reparse-symbol arg-sub-list) [31225 31245])) :type ("bool" type (:type "class") nil nil)) nil [31199 35099]) ("printUnitClauses" function (:parent "CMainSolver" :type ("bool" type (:type "class") nil nil)) nil [35289 35605])) + :file "MainSolver.cpp" + :pointmax 35606 + ) + (semanticdb-table "FormulaCache.h" + :major-mode 'c-mode + :tags 'nil + :file "FormulaCache.h" + ) + ) + :file "semantic.cache" + :semantic-tag-version "2.0beta3" + :semanticdb-version "2.0beta3" + ) Index: /vis_dev/sharpSAT/src/src_sharpSAT/main.cpp =================================================================== --- /vis_dev/sharpSAT/src/src_sharpSAT/main.cpp (revision 9) +++ /vis_dev/sharpSAT/src/src_sharpSAT/main.cpp (revision 9) @@ -0,0 +1,173 @@ +#include + +#include // To seed random generator +#include // To seed random generator + +//include shared files +#include +#include + +#include "MainSolver/MainSolver.h" +#include "Basics.h" + + +using namespace std; + + +CMainSolver theSolver; + +// No description +void finalcSATEvaluation() +{ + const AnalyzerData &rAda = theRunAn.getData(); + + if(rAda.theExitState == TIMEOUT) + { + toSTDOUT(endl << " TIMEOUT !"< + +#include // To seed random generator +#include // To seed random generator + +//include shared files +#include +#include + +#include "MainSolver/MainSolver.h" +#include "Basics.h" + + +using namespace std; + + +CMainSolver theSolver; + +// No description +void finalcSATEvaluation() +{ + const AnalyzerData &rAda = theRunAn.getData(); + + if(rAda.theExitState == TIMEOUT) + { + toSTDOUT(endl << " TIMEOUT !"<