diff --git a/Lib/ArrayMap.hpp b/Lib/ArrayMap.hpp index 38e7b60154..cc1347d84c 100644 --- a/Lib/ArrayMap.hpp +++ b/Lib/ArrayMap.hpp @@ -134,6 +134,19 @@ class ArrayMap return (*this)[index]._obj; } + /** + * Return the object assigned to key @b index or @b def if there isn't any. + */ + inline + T get(size_t index, T def) + { + CALL("ArrayMap::get"); + if((*this)[index]._timestamp!=_timestamp) { + return def; + } + return (*this)[index]._obj; + } + /** * Return @b true if key @b index has an object assigned * diff --git a/Lib/Stack.hpp b/Lib/Stack.hpp index 8209e3120c..9b21a6a4a3 100644 --- a/Lib/Stack.hpp +++ b/Lib/Stack.hpp @@ -18,12 +18,17 @@ #include "Allocator.hpp" #include "Backtrackable.hpp" +namespace std +{ +template +void swap(Lib::Stack& s1, Lib::Stack& s2); +} + namespace Lib { template struct Relocator >; - /** * Class of flexible-size generic stacks. * @since 11/03/2006 Bellevue @@ -34,6 +39,9 @@ template class Stack { public: + template + friend void std::swap(Stack&,Stack&); + class Iterator; DECL_ELEMENT_TYPE(C); @@ -691,4 +699,20 @@ struct Relocator > } // namespace Lib +namespace std +{ + +template +void swap(Lib::Stack& s1, Lib::Stack& s2) +{ + CALL("std::swap(Stack&,Stack&)"); + + swap(s1._capacity, s2._capacity); + swap(s1._cursor, s2._cursor); + swap(s1._end, s2._end); + swap(s1._stack, s2._stack); +} + +} + #endif diff --git a/Makefile b/Makefile index 84b7919b3e..df2b1dd8e0 100644 --- a/Makefile +++ b/Makefile @@ -205,6 +205,7 @@ VINF_OBJ=Inferences/BackwardDemodulation.o\ VSAT_OBJ=SAT/ClauseDisposer.o\ SAT/DIMACS.o\ + SAT/ISSatSweeping.o\ SAT/MinimizingSolver.o\ SAT/Preprocess.o\ SAT/RestartStrategy.o\ diff --git a/SAT/ISSatSweeping.cpp b/SAT/ISSatSweeping.cpp new file mode 100644 index 0000000000..73e26cb2d4 --- /dev/null +++ b/SAT/ISSatSweeping.cpp @@ -0,0 +1,435 @@ +/** + * @file ISSatSweeping.cpp + * Implements class ISSatSweeping. + */ + +#include "Lib/Metaiterators.hpp" + +#include "ISSatSweeping.hpp" + +namespace SAT +{ + +/** + * @param varCnt maximal SAT variable number increased by one + * @param solver SATSolver object whose state should we sweep for literal + * equivalences. This solver should be in a satisfiable state without + * any assumptions. We will add assumptions to probe for equivalences + * and then retract them in the end. + */ +ISSatSweeping::ISSatSweeping(unsigned varCnt, SATSolver& solver) +: _varCnt(varCnt), + _candidateVarPolarities(varCnt), + _candidateGroupIndexes(varCnt), + _equivalentVars(varCnt), + _solver(solver) +{ + CALL("ISSatSweeping::ISSatSweeping"); + ASS_EQ(solver.getStatus(),SATSolver::SATISFIABLE); + ASS(!solver.hasAssumptions()); + + _interestingVars.loadFromIterator(getRangeIterator(1u,varCnt)); + + run(); +} + +/** + * Return true if v1 and v2 are in the same candidate group. If at least + * one of them is not in a candidate group, return false. + */ +bool ISSatSweeping::sameCandGroup(unsigned v1, unsigned v2) +{ + CALL("ISSatSweeping::sameCandGroup"); + + return _candidateGroupIndexes.get(v1, _varCnt+1)==_candidateGroupIndexes.get(v1, _varCnt+2); +} + +void ISSatSweeping::addTrueLit(SATLiteral lit) +{ + CALL("ISSatSweeping::addTrueLit"); + + ALWAYS(_trueVarSet.insert(lit.var())); + _trueLits.push(lit); +} + +void ISSatSweeping::createCandidates() +{ + CALL("ISSatSweeping::createCandidates"); + ASS_EQ(_solver.getStatus(),SATSolver::SATISFIABLE); + ASS(_candidateGroups.isEmpty()); + + + _candidateGroups.push(SATLiteralStack()); + SATLiteralStack& candGrp = _candidateGroups.top(); + Stack::Iterator ivit(_interestingVars); + while(ivit.hasNext()) { + unsigned i = ivit.next(); + SATSolver::VarAssignment asgn = _solver.getAssignment(i); + bool candPolarity; + switch(asgn) { + case SATSolver::TRUE: + candPolarity = true; + break; + case SATSolver::FALSE: + candPolarity = false; + break; + case SATSolver::DONT_CARE: + //don't cares cannot be equivalent to anything, so we just skip it + continue; + case SATSolver::NOT_KNOWN: //this is not to be returned with SATISFIABLE solver status + default: + ASSERTION_VIOLATION; + } + _candidateVarPolarities[i] = candPolarity; + SATLiteral candLit = SATLiteral(i, candPolarity); + if(_solver.isZeroImplied(i)) { + addTrueLit(candLit); + } + else { + candGrp.push(candLit); + } + } + + if(candGrp.size()==1) { + _candidateGroups.pop(); + ASS(_candidateGroups.isEmpty()); + return; + } + _biggestGroupIdx = 0; +} + +/** + * Split the content of orig according to the current assignment. DONT_CARE variables + * are removed from the group. + * + * Ensures that orig will never be smaller than newGrp, and if one of group would + * become of size 1, it makes it empty. + */ +void ISSatSweeping::splitByCurrAssignment(SATLiteralStack& orig, SATLiteralStack& newGrp) +{ + CALL("ISSatSweeping::splitByCurrAssignment"); + ASS_GE(orig.size(),2); + ASS_EQ(newGrp.size(),0); + ASS_EQ(_solver.getStatus(),SATSolver::SATISFIABLE); + + SATLiteralStack::DelIterator oit(orig); + while(oit.hasNext()) { + SATLiteral lit = oit.next(); + SATSolver::VarAssignment asgn; + bool asgnPol; + switch(asgn) { + case SATSolver::TRUE: + asgnPol = true; + break; + case SATSolver::FALSE: + asgnPol = false; + break; + case SATSolver::DONT_CARE: + //don't cares cannot be equivalent to anything, so we just remove it + oit.del(); + continue; + case SATSolver::NOT_KNOWN: //this is not to be returned with SATISFIABLE solver status + default: + ASSERTION_VIOLATION; + } + //true literals remain in orig and false literals go to the newGrp (later the two stacks may be swapped) + if(asgnPol!=lit.polarity()) { + oit.del(); + newGrp.push(lit); + } + } + + if(newGrp.size()>orig.size()) { + std::swap(orig,newGrp); + } + if(newGrp.size()<2) { + newGrp.reset(); + if(orig.size()<2) { + orig.reset(); + } + } +} + +/** + * Split candidate groups according to the current assignment and put + * index of the biggest group into @c _biggestGroupIdx. + */ +void ISSatSweeping::splitGroupsByCurrAssignment() +{ + CALL("ISSatSweeping::splitGroupsByCurrAssignment"); + ASS(_candidateGroups.isNonEmpty()); + + static SATLiteralStack auxNew; + ASS(auxNew.isEmpty()); + + unsigned biggestSz = 0; //smallest actual group size is 2 + unsigned gi = 0; + while(gi<_candidateGroups.size()) { + {//we put this in a special scope as later we might invalidate the currGrp reference + SATLiteralStack& currGrp = _candidateGroups[gi]; + + ASS(auxNew.isEmpty()); + splitByCurrAssignment(currGrp, auxNew); + + ASS_GE(currGrp.size(), auxNew.size()); + if(currGrp.size()>biggestSz) { + biggestSz = currGrp.size(); + _biggestGroupIdx = gi; + } + } + + if(auxNew.isNonEmpty()) { + unsigned addedGrpIdx = _candidateGroups.size(); + _candidateGroups.push(SATLiteralStack()); //this can reallocate the inside of _candidateGroups + if(gi+1!=addedGrpIdx) { + ASS_L(gi+1,addedGrpIdx); + std::swap(_candidateGroups[gi+1],_candidateGroups[addedGrpIdx]); + } + std::swap(_candidateGroups[gi+1],auxNew); + gi += 2; + } + else if(_candidateGroups[gi].isEmpty()) { + swap(_candidateGroups[gi], _candidateGroups.top()); + _candidateGroups.pop(); + } + else { + gi++; + } + } + + _candidateGroupIndexes.reset(); + unsigned groupCnt = _candidateGroups.size(); + for(gi=0; gi::Iterator ivit(_interestingVars); + while(ivit.hasNext()) { + unsigned v = ivit.next(); + if(v==probedLit.var()) { + ASS(_solver.isZeroImplied(v)); + continue; + } + if(!_solver.isZeroImplied(v)) { + continue; + } + SATSolver::VarAssignment asgn = _solver.getAssignment(v); + ASS(asgn==SATSolver::TRUE || asgn==SATSolver::FALSE); + bool asgnPos = asgn==SATSolver::TRUE; + SATLiteral candLit = SATLiteral(v, _candidateVarPolarities[v]); + bool candidateLitTrue = asgnPos==candLit.polarity(); + if(candidateLitTrue==assignedOpposite) { + //probed lit cannot be equivalent to candidate lit + //(see documentation to _candidateVarPolarities) + //We assert the below non-equality because we assume + //splitGroupsByCurrAssignment() to have been already + //called on the current assignment. + ASS(!sameCandGroup(v,probedLit.var())); + Impl imp; + if(assignedOpposite) { + //~p --> c + imp = Impl(probedLit.opposite(), candLit); + } + else { + //p --> ~c + imp = Impl(probedLit, candLit.opposite()); + } + bool foundEq = false; + addImplication(imp, foundEq); + ASS(!foundEq); + continue; + } + + Impl imp; + if(assignedOpposite) { + //~p --> ~c + imp = Impl(candLit, probedLit); + } + else { + //p --> ~c + imp = Impl(probedLit, candLit); + } + addImplication(imp, foundEquivalence); + } +} + +bool ISSatSweeping::tryProvingImplication(Impl imp, bool& foundEquivalence) +{ + CALL("ISSatSweeping::tryProvingImplication"); + ASS(!_solver.hasAssumptions()); + ASS(sameCandGroup(imp.first.var(),imp.second.var())); + + _solver.addAssumption(imp.first.opposite()); + SATSolver::Status status = _solver.getStatus(); + if(status==SATSolver::UNSATISFIABLE) { + addTrueLit(imp.first); + foundEquivalence = true; + _solver.retractAllAssumptions(); + return false; + } + + ASS_EQ(status, SATSolver::SATISFIABLE); + splitGroupsByCurrAssignment(); + lookForImplications(imp.first, true, foundEquivalence); + + if(foundEquivalence || _solver.trueInAssignment(imp.second)) { + _solver.retractAllAssumptions(); + return false; + } + if(_implications.find(imp)) { + return true; + } + + _solver.addAssumption(imp.second); + status = _solver.getStatus(); + if(status==SATSolver::UNSATISFIABLE) { + addImplication(imp, foundEquivalence); + _solver.retractAllAssumptions(); + return true; + } + + splitGroupsByCurrAssignment(); + ASS(!sameCandGroup(imp.first.var(),imp.second.var())); + _solver.retractAllAssumptions(); + return false; + +} + +/** + * Run of this function always shrinks the size of the biggest candidate group. + * Either it discovers an equivalence + */ +void ISSatSweeping::doOneProbing() +{ + CALL("ISSatSweeping::doOneProbing"); + ASS(_candidateGroups.isNonEmpty()); + + SATLiteral cand1, cand2; + { + SATLiteralStack& currGrp = _candidateGroups[_biggestGroupIdx]; + cand1 = currGrp[0]; + int candRoot = _equivalentVars.root(cand1.var()); + while(currGrp.isNonEmpty()) { + cand2 = currGrp.top(); + if(candRoot==_equivalentVars.root(cand2.var())) { + currGrp.pop(); + } + else { + break; + } + } + if(currGrp.isEmpty()) { + if(_biggestGroupIdx!=_candidateGroups.size()-1) { + std::swap(_candidateGroups[_biggestGroupIdx], _candidateGroups.top()); + } + else { + _biggestGroupIdx--; + } + ASS(_candidateGroups.top().isEmpty()); + _candidateGroups.pop(); + return; + } + } + + bool foundEquivalence = false; + if(!tryProvingImplication(Impl(cand1, cand2), foundEquivalence) || foundEquivalence) { + return; + } + + tryProvingImplication(Impl(cand2, cand1), foundEquivalence); + ASS(foundEquivalence); +} + +void ISSatSweeping::run() +{ + CALL("ISSatSweeping::run"); + + createCandidates(); + + while(_candidateGroups.isNonEmpty()) { + doOneProbing(); + } + + ASS(_equivStack.isEmpty()); + + _equivalentVars.evalComponents(); + IntUnionFind::ComponentIterator cit(_equivalentVars); + while(cit.hasNext()) { + IntUnionFind::ElementIterator eit(cit.next()); + ALWAYS(eit.hasNext()); + unsigned v1 = eit.next(); + if(v1==0) { + //this is not an actual variable, just an artifact of + //SAT variables being 1-based while IntUnionFind 0-based + ASS(!eit.hasNext()); + continue; + } + SATLiteral lit1(v1, _candidateVarPolarities[v1]); + while(eit.hasNext()) { + unsigned v2 = eit.next(); + SATLiteral lit2(v2, _candidateVarPolarities[v2]); + _equivStack.push(Equiv(lit1, lit2)); + } + } +} + +//void ISSatSweeping::doOneLitProbing(SATLiteral lit) +//{ +// CALL("ISSatSweeping::doOneLitProbing"); +// ASS(!_solver.hasAssumptions()); +// +// bool foundEquiv = false; +// _solver.addAssumption(lit.opposite()); +// SATSolver::Status status = _solver.getStatus(); +// if(status==SATSolver::UNSATISFIABLE) { +// addTrueLit(lit); +// } +// else { +// ASS_EQ(status, SATSolver::SATISFIABLE); +// splitGroupsByCurrAssignment(); +// lookForImplications(lit, true, foundEquiv); +// } +// _solver.retractAllAssumptions(); +// +// if(foundEquiv || status==SATSolver::UNSATISFIABLE) { +// return; +// } +// +// _solver.addAssumption(lit); +// status = _solver.getStatus(); +// ASS_EQ(status, SATSolver::SATISFIABLE); +// splitGroupsByCurrAssignment(); +// lookForImplications(lit, false, foundEquiv); +// _solver.retractAllAssumptions(); +// +//} + + + +} diff --git a/SAT/ISSatSweeping.hpp b/SAT/ISSatSweeping.hpp new file mode 100644 index 0000000000..08ae01c208 --- /dev/null +++ b/SAT/ISSatSweeping.hpp @@ -0,0 +1,109 @@ +/** + * @file ISSatSweeping.hpp + * Defines class ISSatSweeping. + */ + +#ifndef __ISSatSweeping__ +#define __ISSatSweeping__ + +#include "Forwards.hpp" + +#include "Lib/ArrayMap.hpp" +#include "Lib/DHSet.hpp" +#include "Lib/IntUnionFind.hpp" +#include "Lib/Stack.hpp" + +#include "SATSolver.hpp" + +namespace SAT { + +using namespace Lib; + +class ISSatSweeping +{ +public: + /** + * Represents implication "first --> second". + */ + typedef pair Impl; + typedef pair Equiv; + + ISSatSweeping(unsigned varCnt, SATSolver& solver); + + const DHSet& getImplications() const { return _implications; } + const Stack& getEquivalences() const { return _equivStack; } + const SATLiteralStack& getTrueLiterals() const { return _trueLits; } +private: + + + bool sameCandGroup(unsigned v1, unsigned v2); + + + void splitByCurrAssignment(SATLiteralStack& orig, SATLiteralStack& newGrp); + void splitGroupsByCurrAssignment(); + + void addTrueLit(SATLiteral lit); + +// void doOneLitProbing(SATLiteral lit); + + + void lookForImplications(SATLiteral probedLit, bool assignedOpposite, + bool& foundEquivalence); + void addImplication(Impl i, bool& foundEquivalence); + + bool tryProvingImplication(Impl imp, bool& foundEquivalence); + + void createCandidates(); + void doOneProbing(); + + void run(); + + unsigned _varCnt; + Stack _interestingVars; + + /** + * Polarities of candidate literals. + * Invariant: there is a satisfying assignment with candidate literals set to true + * Consequence: If there is an equivalence between two variables, it will be between + * their candidate literals (there cannot be equivalence between cand. literal and + * negation of the other cand. literal). + */ + DArray _candidateVarPolarities; + /** + * Invariant: size of each candidate group is at least two. + * Invariant: none of literals in the candidate groups is 0-implied to be false. + */ + Stack _candidateGroups; + /** + * Usually, index of the largest candidate group, assigned by splitGroupsByCurrAssignment(). + * + * In some cases it may be index of a group that is not largest, particularly when in + * @c doOneProbing() the largest group becomes collapsed. + */ + unsigned _biggestGroupIdx; + /** + * Candidate group indexes of variables. Populated by splitGroupsByCurrAssignment(). + */ + ArrayMap _candidateGroupIndexes; + + IntUnionFind _equivalentVars; + + /** + * Discovered implications (some discovered equivalences might not be included) + * + * Invariant: at least one of the literals is a candidate literal. The second may be also + * a negation of a candidate literal. + */ + DHSet _implications; + + Stack _equivStack; + + DHSet _trueVarSet; + SATLiteralStack _trueLits; + + SATSolver& _solver; +}; + +} + +#endif // __ISSatSweeping__ diff --git a/SAT/MinimizingSolver.cpp b/SAT/MinimizingSolver.cpp index c199903245..142afaa2f7 100644 --- a/SAT/MinimizingSolver.cpp +++ b/SAT/MinimizingSolver.cpp @@ -76,6 +76,14 @@ SATSolver::VarAssignment MinimizingSolver::getAssignment(unsigned var) return _asgn[var] ? SATSolver::TRUE : SATSolver::FALSE; } +bool MinimizingSolver::isZeroImplied(unsigned var) +{ + CALL("MinimizingSolver::isZeroImplied"); + bool res = _inner->isZeroImplied(var); + ASS(!res || getAssignment(var)!=DONT_CARE); //zero-implied variables cannot become a don't care + return res; +} + /** * Return a true SATLiteral that will satisfy the most unsatisfied * clauses, or SATLiteral::dummy() if there isn't any literal that diff --git a/SAT/MinimizingSolver.hpp b/SAT/MinimizingSolver.hpp index e03a4121a4..a6972b3aa2 100644 --- a/SAT/MinimizingSolver.hpp +++ b/SAT/MinimizingSolver.hpp @@ -32,6 +32,8 @@ class MinimizingSolver : public SATSolver { virtual void addClauses(SATClauseIterator cit, bool onlyPropagate=false); virtual VarAssignment getAssignment(unsigned var); + virtual bool isZeroImplied(unsigned var); + virtual void ensureVarCnt(unsigned newVarCnt); virtual void addAssumption(SATLiteral lit, bool onlyPropagate=false); diff --git a/SAT/SATSolver.hpp b/SAT/SATSolver.hpp index 591ed0d2d9..c65b47a636 100644 --- a/SAT/SATSolver.hpp +++ b/SAT/SATSolver.hpp @@ -43,6 +43,13 @@ class SATSolver { * If status is @c SATISFIABLE, return assignment of variable @c var */ virtual VarAssignment getAssignment(unsigned var) = 0; + + /** + * If status is @c SATISFIABLE, return 0 if the assignment of @c var is + * implied only by unit propagation (i.e. does not depend on any decisions) + */ + virtual bool isZeroImplied(unsigned var) = 0; + virtual void ensureVarCnt(unsigned newVarCnt) {} virtual void addAssumption(SATLiteral lit, bool onlyPropagate=false) = 0; diff --git a/SAT/TWLSolver.cpp b/SAT/TWLSolver.cpp index 323167e6c4..89f9c756ab 100644 --- a/SAT/TWLSolver.cpp +++ b/SAT/TWLSolver.cpp @@ -1113,6 +1113,13 @@ SATSolver::VarAssignment TWLSolver::getAssignment(unsigned var) } } +bool TWLSolver::isZeroImplied(unsigned var) +{ + CALL("TWLSolver::isZeroImplied"); + + return getAssignmentLevel(var)==1; +} + void TWLSolver::printAssignment() { CALL("TWLSolver::printAssignment"); diff --git a/SAT/TWLSolver.hpp b/SAT/TWLSolver.hpp index d4704bdb99..be69000034 100644 --- a/SAT/TWLSolver.hpp +++ b/SAT/TWLSolver.hpp @@ -53,6 +53,7 @@ class TWLSolver : public SATSolver { virtual Status getStatus() { return _status; }; virtual void ensureVarCnt(unsigned newVarCnt); virtual VarAssignment getAssignment(unsigned var); + virtual bool isZeroImplied(unsigned var); virtual void addAssumption(SATLiteral lit, bool onlyPropagate); void addAssumption(SATLiteral lit, unsigned conflictCountLimit); diff --git a/SAT/TransparentSolver.hpp b/SAT/TransparentSolver.hpp index 3f3bb5571b..ed0bda78f9 100644 --- a/SAT/TransparentSolver.hpp +++ b/SAT/TransparentSolver.hpp @@ -28,6 +28,7 @@ class TransparentSolver : public SATSolver virtual void ensureVarCnt(unsigned newVarCnt); virtual void addClauses(SATClauseIterator cit, bool onlyPropagate); virtual VarAssignment getAssignment(unsigned var); + virtual bool isZeroImplied(unsigned var) { return _inner->isZeroImplied(var); } //TODO: not quite sure wether this is right virtual void addAssumption(SATLiteral lit, bool onlyPropagate); virtual void retractAllAssumptions(); diff --git a/Shell/Property.cpp b/Shell/Property.cpp index ee96c8aff4..f9e15ba86a 100644 --- a/Shell/Property.cpp +++ b/Shell/Property.cpp @@ -356,6 +356,8 @@ void Property::scan(Formula* formula) scan(lit,dummy); break; } + default: + break; } } } // Property::scan(const Formula&) diff --git a/Test/CheckedSatSolver.hpp b/Test/CheckedSatSolver.hpp index 250a33df66..e6f3e6630f 100644 --- a/Test/CheckedSatSolver.hpp +++ b/Test/CheckedSatSolver.hpp @@ -29,6 +29,7 @@ class CheckedSatSolver : public SATSolver { virtual void addClauses(SATClauseIterator cit, bool onlyPropagate=false); virtual VarAssignment getAssignment(unsigned var); + virtual bool isZeroImplied(unsigned var) { return _inner->isZeroImplied(var); } virtual void ensureVarCnt(unsigned newVarCnt); virtual void addAssumption(SATLiteral lit, bool onlyPropagate=false); diff --git a/VUtils/DPTester.cpp b/VUtils/DPTester.cpp index 37a9913cf3..e7f34cd350 100644 --- a/VUtils/DPTester.cpp +++ b/VUtils/DPTester.cpp @@ -62,6 +62,9 @@ int DPTester::perform(int argc, char** argv) case DecisionProcedure::UNSATISFIABLE: cout << "UNSAT" << endl; break; + case DecisionProcedure::UNKNOWN: + cout << "UNKNOWN" << endl; + break; }