diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..9eeec85 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "lib/cadical"] + path = lib/cadical + url = https://github.com/arminbiere/cadical.git diff --git a/lib/cadical b/lib/cadical new file mode 160000 index 0000000..1462073 --- /dev/null +++ b/lib/cadical @@ -0,0 +1 @@ +Subproject commit 146207318796f094dcded87349a64f0c6927309e diff --git a/src/Makefile b/src/Makefile index 9d21e48..72a6b4d 100755 --- a/src/Makefile +++ b/src/Makefile @@ -2,10 +2,10 @@ # Definitions COMPILEROPTIONS = $(shell $(CC) BFAbstractionLibrary/compilerOptionGenerator.c -o /tmp/BFAbstractionCompilerOptionsProducer-$(USER);/tmp/BFAbstractionCompilerOptionsProducer-$(USER)) -DEFINES = -DUSE_CUDD -DNDEBUG +DEFINES = -DUSE_CUDD -DNDEBUG -DNBUILD CFLAGS = -pipe -O3 -g -mtune=native $(COMPILEROPTIONS) -Wall -W -fPIC $(DEFINES) CXXFLAGS = -pipe -O3 -g -std=c++11 -mtune=native $(COMPILEROPTIONS) -fPIC $(DEFINES) -INCPATH = -I. -I../lib/ -I../lib/cudd-3.0.0/ -I../lib/cudd-3.0.0/cudd -I../lib/cudd-3.0.0/mtr -I../lib/cudd-3.0.0/epd -I../lib/cudd-3.0.0/st -I../lib/cudd-3.0.0/util -I../lib/cudd-3.0.0/dddmp -IBFAbstractionLibrary +INCPATH = -I. -I../lib/ -I../lib/cudd-3.0.0/ -I../lib/cudd-3.0.0/cudd -I../lib/cudd-3.0.0/mtr -I../lib/cudd-3.0.0/epd -I../lib/cudd-3.0.0/st -I../lib/cudd-3.0.0/util -I../lib/cudd-3.0.0/dddmp -IBFAbstractionLibrary -I../lib/cadical/src LINK = $(CXX) LFLAGS = @@ -20,7 +20,88 @@ OBJECTS = main.o \ $(patsubst %.c,%.o,$(wildcard ../lib/cudd-3.0.0/epd/*.c)) \ $(filter-out ../lib/cudd-3.0.0/st/testst.o,$(patsubst %.c,%.o,$(wildcard ../lib/cudd-3.0.0/st/*.c))) \ $(filter-out ../lib/cudd-3.0.0/util/cpu_stats.o,$(patsubst %.c,%.o,$(wildcard ../lib/cudd-3.0.0/util/*.c))) \ - $(filter-out ../lib/cudd-3.0.0/dddmp/testdddmp.o,$(patsubst %.c,%.o,$(wildcard ../lib/cudd-3.0.0/dddmp/*.c))) + $(filter-out ../lib/cudd-3.0.0/dddmp/testdddmp.o,$(patsubst %.c,%.o,$(wildcard ../lib/cudd-3.0.0/dddmp/*.c))) \ + ../lib/cadical/src/analyze.o \ + ../lib/cadical/src/arena.o \ + ../lib/cadical/src/assume.o \ + ../lib/cadical/src/averages.o \ + ../lib/cadical/src/backtrack.o \ + ../lib/cadical/src/backward.o \ + ../lib/cadical/src/bins.o \ + ../lib/cadical/src/block.o \ + ../lib/cadical/src/ccadical.o \ + ../lib/cadical/src/checker.o \ + ../lib/cadical/src/clause.o \ + ../lib/cadical/src/collect.o \ + ../lib/cadical/src/compact.o \ + ../lib/cadical/src/condition.o \ + ../lib/cadical/src/config.o \ + ../lib/cadical/src/constrain.o \ + ../lib/cadical/src/contract.o \ + ../lib/cadical/src/cover.o \ + ../lib/cadical/src/decide.o \ + ../lib/cadical/src/decompose.o \ + ../lib/cadical/src/deduplicate.o \ + ../lib/cadical/src/drattracer.o \ + ../lib/cadical/src/elim.o \ + ../lib/cadical/src/ema.o \ + ../lib/cadical/src/extend.o \ + ../lib/cadical/src/external.o \ + ../lib/cadical/src/external_propagate.o \ + ../lib/cadical/src/file.o \ + ../lib/cadical/src/flags.o \ + ../lib/cadical/src/flip.o \ + ../lib/cadical/src/format.o \ + ../lib/cadical/src/frattracer.o \ + ../lib/cadical/src/gates.o \ + ../lib/cadical/src/idruptracer.o \ + ../lib/cadical/src/instantiate.o \ + ../lib/cadical/src/internal.o \ + ../lib/cadical/src/ipasir.o \ + ../lib/cadical/src/limit.o \ + ../lib/cadical/src/logging.o \ + ../lib/cadical/src/lookahead.o \ + ../lib/cadical/src/lratbuilder.o \ + ../lib/cadical/src/lratchecker.o \ + ../lib/cadical/src/lrattracer.o \ + ../lib/cadical/src/lucky.o \ + ../lib/cadical/src/message.o \ + ../lib/cadical/src/minimize.o \ + ../lib/cadical/src/occs.o \ + ../lib/cadical/src/options.o \ + ../lib/cadical/src/parse.o \ + ../lib/cadical/src/phases.o \ + ../lib/cadical/src/probe.o \ + ../lib/cadical/src/profile.o \ + ../lib/cadical/src/proof.o \ + ../lib/cadical/src/propagate.o \ + ../lib/cadical/src/queue.o \ + ../lib/cadical/src/random.o \ + ../lib/cadical/src/reap.o \ + ../lib/cadical/src/reduce.o \ + ../lib/cadical/src/rephase.o \ + ../lib/cadical/src/report.o \ + ../lib/cadical/src/resources.o \ + ../lib/cadical/src/restart.o \ + ../lib/cadical/src/restore.o \ + ../lib/cadical/src/score.o \ + ../lib/cadical/src/shrink.o \ + ../lib/cadical/src/signal.o \ + ../lib/cadical/src/solution.o \ + ../lib/cadical/src/solver.o \ + ../lib/cadical/src/stats.o \ + ../lib/cadical/src/subsume.o \ + ../lib/cadical/src/terminal.o \ + ../lib/cadical/src/ternary.o \ + ../lib/cadical/src/transred.o \ + ../lib/cadical/src/util.o \ + ../lib/cadical/src/var.o \ + ../lib/cadical/src/veripbtracer.o \ + ../lib/cadical/src/version.o \ + ../lib/cadical/src/vivify.o \ + ../lib/cadical/src/walk.o \ + ../lib/cadical/src/watch.o + # Headers HEADERS_BUT_EXTENSIONS = gr1context.hpp variableManager.hpp variableTypes.hpp \ diff --git a/src/extensionComputeInvariants.hpp b/src/extensionComputeInvariants.hpp index 5c486fa..a9abace 100644 --- a/src/extensionComputeInvariants.hpp +++ b/src/extensionComputeInvariants.hpp @@ -9,6 +9,7 @@ #include #include #include "subprocess.hpp" +#include "cadical.hpp" #ifdef CUDD #include @@ -203,57 +204,66 @@ template class XComputeInvariants : public T { // Random number generator to randomize which negative countereaxmple to pick -- leads to sufficient diversity in the examples. std::mt19937 rng(123); + // Incremental solving + std::vector startingVarsInvariantBases; + std::vector startingVarsInvariantSelectorForNegativeExample; + std::vector startingVarsActiveBasesForEachNegativeExample; + int nofVarsSoFar = 0; + + // Allocate variables for invariant bases + for (int i=0;i > clauses; - - // Allocate variables for invariant bases - std::vector startingVarsInvariantBases; - int nofVarsSoFar = 0; - for (int i=0;i > clauses; // Allocate variables for selecting for each negative example which invariant is the right one - std::vector startingVarsInvariantSelectorForNegativeExample; - for (unsigned int i=0;i0) { + for (unsigned int i=negativeExamples.size()-1;i startingVarsActiveBasesForEachNegativeExample; - for (unsigned int i=0;i clauseSelector; - for (int j=0;j clauseSelector; + for (int j=0;j(relevantCUDDVars.size());k++) { - clauses.push_back({-1*startingVarsInvariantSelectorForNegativeExample[i]-j,-1*startingVarsActiveBasesForEachNegativeExample[i]-k,startingVarsInvariantBases[j]+k}); - clauses.push_back({-1*startingVarsInvariantSelectorForNegativeExample[i]-j,startingVarsActiveBasesForEachNegativeExample[i]+k,-1*startingVarsInvariantBases[j]-k}); + // Encode base selection + for (unsigned int i=negativeExamples.size()-1;i(relevantCUDDVars.size());k++) { + solver.clause(-1*startingVarsInvariantSelectorForNegativeExample[i]-j,-1*startingVarsActiveBasesForEachNegativeExample[i]-k,startingVarsInvariantBases[j]+k); + solver.clause(-1*startingVarsInvariantSelectorForNegativeExample[i]-j,startingVarsActiveBasesForEachNegativeExample[i]+k,-1*startingVarsInvariantBases[j]-k); + } } } } @@ -262,76 +272,38 @@ template class XComputeInvariants : public T { DdNode *one = Cudd_ReadOne(toBeCovered.manager()->getMgr()); DdNode *zero = Cudd_Not(one); - for (unsigned int negativeExample=0;negativeExample,int,hashDdNodeUIntPair> nodeToVarMapper; - nodeToVarMapper[std::pair(winningPositions.getCuddNode(),0)] = ++nofVarsSoFar; - clauses.push_back({nofVarsSoFar}); - std::unordered_set,hashDdNodeUIntPair> doneList; - doneList.insert(std::pair(winningPositions.getCuddNode(),0)); - std::list> todoList; - todoList.push_back(std::pair(winningPositions.getCuddNode(),0)); - // std::cerr << "digraph {\n\"n0\";\n"; - while (todoList.size()!=0) { - std::pair thisNodeAndLevel = todoList.front(); - todoList.pop_front(); - int currentNo = nodeToVarMapper.at(thisNodeAndLevel); - - if (Cudd_IsConstant(thisNodeAndLevel.first) && (thisNodeAndLevel.second==relevantCUDDVars.size())) { - if (thisNodeAndLevel.first==one) { - clauses.push_back({-1*currentNo}); - //std::cerr << "n" << currentNo << "[label=\"n" << currentNo << ",ONE\"];\n"; - } else { - assert(thisNodeAndLevel.first==zero); - } - } else if (Cudd_IsConstant(thisNodeAndLevel.first) || - (cuddIndexToRelevantVarNumberMapper[Cudd_Regular(thisNodeAndLevel.first)->index]!=thisNodeAndLevel.second)) { - - /* Case: Skipping a variable */ - std::pair nextPair = thisNodeAndLevel; - nextPair.second++; - if (nextPair.second > relevantCUDDVarBFs.size()) { - throw "Internal error: Went too low in the hierarchy."; - } - int numNext; - if (doneList.count(nextPair)==0) { - numNext = ++nofVarsSoFar; - nodeToVarMapper[nextPair] = numNext; - doneList.insert(nextPair); - todoList.push_back(nextPair); - } else { - numNext = nodeToVarMapper[nextPair]; - } - - // Negative example the same as invariant base --> Follow only the negative example case. - // otherwise follow both cases! - clauses.push_back({-1*currentNo,numNext}); - - } else { - //std::cerr << "n" << currentNo << "[label=\"n" << currentNo << "," << thisNodeAndLevel.second << "\"];\n"; - DdNode *t; - DdNode *e; - if (reinterpret_cast(thisNodeAndLevel.first) & 1) { - t = Cudd_Not(Cudd_T(Cudd_Regular(thisNodeAndLevel.first))); - e = Cudd_Not(Cudd_E(Cudd_Regular(thisNodeAndLevel.first))); - } else { - t = Cudd_T(thisNodeAndLevel.first); - e = Cudd_E(thisNodeAndLevel.first); - } - - for (int edge=0;edge<2;edge++) { - std::pair nextPair((edge==0)?t:e,thisNodeAndLevel.second+1); - - // Sanity check - if (!Cudd_IsConstant(nextPair.first)) { - int nextIndex = Cudd_Regular(nextPair.first)->index; - if (cuddIndexToRelevantVarNumberMapper[nextIndex]index; - std::cerr << "ThisLevel: " << thisIndex << std::endl; - throw "Internal error: Skipped a level."; - } + if (negativeExamples.size()>0) { + for (unsigned int negativeExample=negativeExamples.size()-1;negativeExample,int,hashDdNodeUIntPair> nodeToVarMapper; + nodeToVarMapper[std::pair(winningPositions.getCuddNode(),0)] = ++nofVarsSoFar; + solver.clause(nofVarsSoFar); + std::unordered_set,hashDdNodeUIntPair> doneList; + doneList.insert(std::pair(winningPositions.getCuddNode(),0)); + std::list> todoList; + todoList.push_back(std::pair(winningPositions.getCuddNode(),0)); + // std::cerr << "digraph {\n\"n0\";\n"; + while (todoList.size()!=0) { + std::pair thisNodeAndLevel = todoList.front(); + todoList.pop_front(); + int currentNo = nodeToVarMapper.at(thisNodeAndLevel); + + if (Cudd_IsConstant(thisNodeAndLevel.first) && (thisNodeAndLevel.second==relevantCUDDVars.size())) { + if (thisNodeAndLevel.first==one) { + solver.clause(-1*currentNo); + //std::cerr << "n" << currentNo << "[label=\"n" << currentNo << ",ONE\"];\n"; + } else { + assert(thisNodeAndLevel.first==zero); + } + } else if (Cudd_IsConstant(thisNodeAndLevel.first) || + (cuddIndexToRelevantVarNumberMapper[Cudd_Regular(thisNodeAndLevel.first)->index]!=thisNodeAndLevel.second)) { + + /* Case: Skipping a variable */ + std::pair nextPair = thisNodeAndLevel; + nextPair.second++; + if (nextPair.second > relevantCUDDVarBFs.size()) { + throw "Internal error: Went too low in the hierarchy."; } - int numNext; if (doneList.count(nextPair)==0) { numNext = ++nofVarsSoFar; @@ -343,30 +315,70 @@ template class XComputeInvariants : public T { } // Negative example the same as invariant base --> Follow only the negative example case. - // otherwise follow both cases, also in the case of don't cares - if (((negativeExamples[negativeExample][thisNodeAndLevel.second]==1) ^ (edge==1)) || (negativeExamples[negativeExample][thisNodeAndLevel.second]==0)) { - // Take this one either way - clauses.push_back({-1*currentNo,numNext}); + // otherwise follow both cases! + solver.clause(-1*currentNo,numNext); + + } else { + //std::cerr << "n" << currentNo << "[label=\"n" << currentNo << "," << thisNodeAndLevel.second << "\"];\n"; + DdNode *t; + DdNode *e; + if (reinterpret_cast(thisNodeAndLevel.first) & 1) { + t = Cudd_Not(Cudd_T(Cudd_Regular(thisNodeAndLevel.first))); + e = Cudd_Not(Cudd_E(Cudd_Regular(thisNodeAndLevel.first))); } else { - // Take this one conditionally - int conditionLiteral = (negativeExamples[negativeExample][thisNodeAndLevel.second])*(startingVarsActiveBasesForEachNegativeExample[negativeExample]+thisNodeAndLevel.second); - clauses.push_back({conditionLiteral,-1*currentNo,numNext}); + t = Cudd_T(thisNodeAndLevel.first); + e = Cudd_E(thisNodeAndLevel.first); } - //std::cerr << "n" << currentNo << "-> n" << numNext; - //if (edge==1) std::cerr << "[style=dashed];\n"; - //else std::cerr << ";\n"; - } + for (int edge=0;edge<2;edge++) { + std::pair nextPair((edge==0)?t:e,thisNodeAndLevel.second+1); + + // Sanity check + if (!Cudd_IsConstant(nextPair.first)) { + int nextIndex = Cudd_Regular(nextPair.first)->index; + if (cuddIndexToRelevantVarNumberMapper[nextIndex]index; + std::cerr << "ThisLevel: " << thisIndex << std::endl; + throw "Internal error: Skipped a level."; + } + } + + int numNext; + if (doneList.count(nextPair)==0) { + numNext = ++nofVarsSoFar; + nodeToVarMapper[nextPair] = numNext; + doneList.insert(nextPair); + todoList.push_back(nextPair); + } else { + numNext = nodeToVarMapper[nextPair]; + } + // Negative example the same as invariant base --> Follow only the negative example case. + // otherwise follow both cases, also in the case of don't cares + if (((negativeExamples[negativeExample][thisNodeAndLevel.second]==1) ^ (edge==1)) || (negativeExamples[negativeExample][thisNodeAndLevel.second]==0)) { + // Take this one either way + solver.clause(-1*currentNo,numNext); + } else { + // Take this one conditionally + int conditionLiteral = (negativeExamples[negativeExample][thisNodeAndLevel.second])*(startingVarsActiveBasesForEachNegativeExample[negativeExample]+thisNodeAndLevel.second); + solver.clause(conditionLiteral,-1*currentNo,numNext); + } + + //std::cerr << "n" << currentNo << "-> n" << numNext; + //if (edge==1) std::cerr << "[style=dashed];\n"; + //else std::cerr << ";\n"; + } + + } } + //std::cerr << "}\n"; } - //std::cerr << "}\n"; } // Run SAT solver // Start encoding - subprocess::popen cmd(satSolver, {}); + /*subprocess::popen cmd(satSolver, {}); std::ostream &cmdos = cmd.stdin(); cmdos << "p cnf " << nofVarsSoFar << " " << clauses.size() << "\n"; for (auto &it : clauses) { @@ -380,16 +392,17 @@ template class XComputeInvariants : public T { cmd.close(); // Closes only inStream std::ostringstream stdoutBuffer; - stdoutBuffer << cmd.stdout().rdbuf(); + stdoutBuffer << cmd.stdout().rdbuf();*/ - int retVal = cmd.wait(); - if (retVal==10) { + auto retVal = solver.solve(); + if (retVal==CaDiCaL::Status::SATISFIABLE) { // Satisfiable! // Read model - std::istringstream is(stdoutBuffer.str()); - std::string currentline; + //std::istringstream is(stdoutBuffer.str()); + //std::string currentline; + std::vector model(nofVarsSoFar+1); - while (std::getline(is,currentline)) { + /*while (std::getline(is,currentline)) { //std::cerr << "Interpreting model line: " << currentline << std::endl; if (currentline.substr(0,2)=="v ") { // Read model @@ -402,6 +415,9 @@ template class XComputeInvariants : public T { } } } + }*/ + for (int i=1;i<=nofVarsSoFar;i++) { + model[i] = solver.val(i)>0; } #ifndef NDEBUG @@ -536,12 +552,12 @@ template class XComputeInvariants : public T { std::cout << "Result: Cannot find " << nofInvariants << " covering the non-winning reachable states.\n"; return; } else { - std::ostringstream stderrBuffer; - stderrBuffer << "(" << retVal << ")" << cmd.stderr().rdbuf(); - std::ostringstream error; - error << stderrBuffer.str() << ", stdout: " << stdoutBuffer.str(); - std::cerr << "BufSiz:" << error.str().length() << std::endl; - throw SlugsException(false,error.str()); + //std::ostringstream stderrBuffer; + //stderrBuffer << "(" << retVal << ")" << cmd.stderr().rdbuf(); + //std::ostringstream error; + //error << stderrBuffer.str() << ", stdout: " << stdoutBuffer.str(); + //std::cerr << "BufSiz:" << error.str().length() << std::endl; + throw SlugsException(false,"Solving Error"); }