144 lines
4.9 KiB
Diff
144 lines
4.9 KiB
Diff
--- ./Makefile.orig 2014-11-26 07:04:53.000000000 -0700
|
|
+++ ./Makefile 2014-12-10 20:00:00.000000000 -0700
|
|
@@ -23,7 +23,7 @@ SETUP_PY_EXTRA_ARG = --root=$(DESTDIR)
|
|
SETUP_PY_INSTALL_EXTRA_ARG = $(SETUP_PY_EXTRA_ARG)
|
|
endif
|
|
|
|
-all: picosat/libpicosat.a checkpuma $(PUMALIB) FORCE
|
|
+all: checkpuma $(PUMALIB) FORCE
|
|
$(MAKE) all_progs
|
|
|
|
all_progs: $(OTHER_PROGS) checkpuma undertaker_progs
|
|
@@ -114,7 +114,7 @@ distclean: clean
|
|
test ! -f picosat/makefile || $(MAKE) -C picosat clean
|
|
test ! -f $(LOCALPUMA)/Makefile || $(MAKE) clean-Puma
|
|
|
|
-models: picosat/libpicosat.a
|
|
+models:
|
|
$(MAKE) -C undertaker/kconfig-dumps/
|
|
|
|
###################################################################################################
|
|
@@ -183,8 +183,6 @@ install: all $(MANPAGES)
|
|
@install -v undertaker/rsf2cnf $(DESTDIR)$(BINDIR)
|
|
@install -v undertaker/satyr $(DESTDIR)$(BINDIR)
|
|
|
|
- @install -v picosat/picomus $(DESTDIR)$(BINDIR)
|
|
-
|
|
@install -v ziz/zizler $(DESTDIR)$(BINDIR)
|
|
|
|
@install -v scripts/Makefile.list $(DESTDIR)$(LIBDIR)
|
|
--- ./undertaker/Makefile.orig 2014-11-26 07:04:53.000000000 -0700
|
|
+++ ./undertaker/Makefile 2014-12-10 20:00:00.000000000 -0700
|
|
@@ -5,15 +5,15 @@ SUFFIXES += .d
|
|
NODEPS:=clean clean-check clean-parsers clean-regenerate
|
|
|
|
CFLAGS = -Wall -Wextra -O2
|
|
-CPPFLAGS = -I../scripts/kconfig -I../picosat
|
|
+CPPFLAGS = -I../scripts/kconfig
|
|
CXXFLAGS = $(CFLAGS) -std=gnu++11
|
|
|
|
# use g++ for linking, will automaticly use "-lstdc++ -lm" libraries
|
|
CC = g++
|
|
|
|
-LDFLAGS =
|
|
+LDFLAGS = -Wl,--as-needed
|
|
BOOST_LIBS = -lboost_system -lboost_regex -lboost_filesystem -lboost_thread
|
|
-LDLIBS = $(BOOST_LIBS) -lpthread
|
|
+LDLIBS = $(BOOST_LIBS) -lpthread -lpicosat
|
|
|
|
# LDCOV = -coverage
|
|
ifdef LDCOV
|
|
@@ -72,10 +72,10 @@ PARSERDIR = BoolExpLP
|
|
|
|
all: $(PROGS)
|
|
|
|
-undertaker: libparser.a ../picosat/libpicosat.a $(PUMALIB)
|
|
-rsf2cnf: libparser.a ../picosat/libpicosat.a
|
|
+undertaker: libparser.a $(PUMALIB)
|
|
+rsf2cnf: libparser.a
|
|
predator: predator.o PredatorVisitor.o $(PUMALIB)
|
|
-satyr: libsatyr.a zconf.tab.o ../picosat/libpicosat.a
|
|
+satyr: libsatyr.a zconf.tab.o
|
|
|
|
ifneq ($(LOCALPUMA),)
|
|
$(PUMALIB):
|
|
@@ -126,7 +126,7 @@ endif
|
|
%.d: %.cpp
|
|
@$(CXX) $(CPPFLAGS) $(CXXFLAGS) -MM -MG $< > $@
|
|
|
|
-test-%: test-%.cpp libparser.a ../picosat/libpicosat.a $(PUMALIB)
|
|
+test-%: test-%.cpp libparser.a $(PUMALIB)
|
|
$(CXX) $(CPPFLAGS) $(CXXFLAGS) -g -O0 -o $@ $^ -lcheck -lrt $(LDFLAGS) $(LDLIBS)
|
|
|
|
clean: clean-check
|
|
--- ./undertaker/PicosatCNF.cpp.orig 2014-11-26 07:04:53.000000000 -0700
|
|
+++ ./undertaker/PicosatCNF.cpp 2014-12-10 20:00:00.000000000 -0700
|
|
@@ -30,7 +30,7 @@
|
|
namespace Picosat {
|
|
// include picosat header as C
|
|
extern "C" {
|
|
- #include "picosat.h"
|
|
+ #include <picosat.h>
|
|
}
|
|
} // namespace Picosat
|
|
|
|
@@ -39,6 +39,7 @@ using namespace kconfig;
|
|
|
|
static bool picosatIsInitalized = false;
|
|
static PicosatCNF *currentContext = nullptr;
|
|
+static Picosat::PicoSAT *picosat_inst;
|
|
|
|
PicosatCNF::PicosatCNF(Picosat::SATMode defaultPhase) : defaultPhase(defaultPhase) {}
|
|
|
|
@@ -309,26 +310,26 @@ bool PicosatCNF::checkSatisfiable() {
|
|
if (this != currentContext){
|
|
// if not, reset the context....
|
|
if (picosatIsInitalized)
|
|
- Picosat::picosat_reset();
|
|
- Picosat::picosat_init();
|
|
+ Picosat::picosat_reset(picosat_inst);
|
|
+ picosat_inst = Picosat::picosat_init();
|
|
picosatIsInitalized = true;
|
|
// and load the current context
|
|
currentContext = this;
|
|
- Picosat::picosat_set_global_default_phase(defaultPhase);
|
|
+ Picosat::picosat_set_global_default_phase(picosat_inst, defaultPhase);
|
|
}
|
|
if (pushed_clauses_index < clauses.size()) {
|
|
// tell picosat how many different variables it will receive
|
|
- Picosat::picosat_adjust(varcount);
|
|
+ Picosat::picosat_adjust(picosat_inst, varcount);
|
|
|
|
for (unsigned int i = pushed_clauses_index, e = clauses.size(); i < e; ++i)
|
|
- Picosat::picosat_add(clauses[i]);
|
|
+ Picosat::picosat_add(picosat_inst, clauses[i]);
|
|
pushed_clauses_index = clauses.size();
|
|
}
|
|
for (const int &assumption : assumptions)
|
|
- Picosat::picosat_assume(assumption);
|
|
+ Picosat::picosat_assume(picosat_inst, assumption);
|
|
|
|
assumptions.clear();
|
|
- return Picosat::picosat_sat(-1) == PICOSAT_SATISFIABLE;
|
|
+ return Picosat::picosat_sat(picosat_inst, -1) == PICOSAT_SATISFIABLE;
|
|
}
|
|
|
|
void PicosatCNF::pushAssumptions(std::map<std::string, bool> &a) {
|
|
@@ -340,7 +341,7 @@ void PicosatCNF::pushAssumptions(std::ma
|
|
}
|
|
|
|
bool PicosatCNF::deref(int s) const {
|
|
- return Picosat::picosat_deref(s) == 1;
|
|
+ return Picosat::picosat_deref(picosat_inst, s) == 1;
|
|
}
|
|
|
|
bool PicosatCNF::deref(const std::string &s) const {
|
|
@@ -359,7 +360,7 @@ const std::string *PicosatCNF::getAssoci
|
|
}
|
|
|
|
const int *PicosatCNF::failedAssumptions() const {
|
|
- return Picosat::picosat_failed_assumptions();
|
|
+ return Picosat::picosat_failed_assumptions(picosat_inst);
|
|
}
|
|
|
|
void PicosatCNF::addMetaValue(const std::string &key, const std::string &value) {
|