From d3d3d6b0c87a35deaca331d79ac607542b913d9e Mon Sep 17 00:00:00 2001 From: Krystof Hoder Date: Tue, 27 Mar 2012 23:24:44 +0000 Subject: [PATCH] --- DP/DecisionProcedure.hpp | 2 +- DP/SimpleCongruenceClosure.cpp | 81 ++++++++++++++++++++++++++++++++-- DP/SimpleCongruenceClosure.hpp | 23 ++++------ Debug/Log_TagDecls.cpp | 9 +++- Shell/AIGCompressor.cpp | 7 +++ VUtils/SimpleSMT.cpp | 2 + 6 files changed, 104 insertions(+), 20 deletions(-) diff --git a/DP/DecisionProcedure.hpp b/DP/DecisionProcedure.hpp index a023657cee..2cc6754c1f 100644 --- a/DP/DecisionProcedure.hpp +++ b/DP/DecisionProcedure.hpp @@ -36,7 +36,7 @@ class DecisionProcedure { virtual Status getStatus() = 0; virtual void getUnsatisfiableSubset(LiteralStack& res) = 0; - /** reset decision procedure object into its initial state */ + /** reset decision procedure object into state equivalent to its initial state */ virtual void reset() = 0; }; diff --git a/DP/SimpleCongruenceClosure.cpp b/DP/SimpleCongruenceClosure.cpp index ca1829fce6..481e5c4bb1 100644 --- a/DP/SimpleCongruenceClosure.cpp +++ b/DP/SimpleCongruenceClosure.cpp @@ -62,6 +62,49 @@ string SimpleCongruenceClosure::CEq::toString(SimpleCongruenceClosure& parent) c return res.str(); } +void SimpleCongruenceClosure::ConstInfo::init() { + CALL("SimpleCongruenceClosure::ConstInfo::init"); + + sigSymbol = NO_SIG_SYMBOL; + term.makeEmpty(); + lit = 0; + namedPair = CPair(0,0); + reprConst = 0; + proofPredecessor = 0; + predecessorPremise = CEq(0,0); + classList.reset(); + useList.reset(); +} + +void SimpleCongruenceClosure::ConstInfo::resetEquivalences(SimpleCongruenceClosure& parent, unsigned selfIndex) { + CALL("SimpleCongruenceClosure::ConstInfo::resetEquivalences"); + + reprConst = 0; + proofPredecessor = 0; + predecessorPremise = CEq(0,0); + classList.reset(); + + static ArraySet seen; + seen.reset(); + + Stack::DelIterator ulit(useList); + while(ulit.hasNext()) { + unsigned p = ulit.next(); + ConstInfo& pInfo = parent._cInfos[p]; + if(pInfo.namedPair.first!=p && pInfo.namedPair.second!=p) { + ulit.del(); + continue; + } + if(seen.find(p)) { + ulit.del(); + continue; + } + seen.insert(p); + } +} + + + SimpleCongruenceClosure::SimpleCongruenceClosure() { CALL("SimpleCongruenceClosure::SimpleCongruenceClosure"); @@ -81,23 +124,34 @@ void SimpleCongruenceClosure::reset() { CALL("SimpleCongruenceClosure::reset"); +#if 1 ASS_EQ(_posLitConst,1); ASS_EQ(_negLitConst,2); //this leaves us just with the true and false constants _cInfos.expand(3); - //this leaves us just with the true!=false non-equality - _negEqualities.truncate(1); - _sigConsts.reset(); _pairNames.reset(); _termNames.reset(); +#else + //do reset that keeps the data for converting terms to constants + + unsigned maxConst = getMaxConst(); + for(unsigned i=1; i<=maxConst; i++) { + _cInfos[i].resetEquivalences(*this, i); + } +#endif + + //this leaves us just with the true!=false non-equality + _negEqualities.truncate(1); + ASS_EQ(_negEqualities.top().c1,_posLitConst); + ASS_EQ(_negEqualities.top().c2,_negLitConst); + //no unsat non-equality _unsatEq = CEq(0,0); _pendingEqualities.reset(); - _negEqualities.reset(); _distinctConstraints.reset(); _negDistinctConstraints.reset(); } @@ -145,7 +199,15 @@ unsigned SimpleCongruenceClosure::getPairName(CPair p) *pRes = res; _cInfos[p.first].useList.push(res); + if(_cInfos[p.first].reprConst!=0) { + unsigned fRepr = _cInfos[p.first].reprConst; + _cInfos[fRepr].useList.push(res); + } _cInfos[p.second].useList.push(res); + if(_cInfos[p.second].reprConst!=0) { + unsigned sRepr = _cInfos[p.second].reprConst; + _cInfos[sRepr].useList.push(res); + } LOG("dp_cc_const_intr", "pairConst: "< convertor(wrk); return convertor(trm); @@ -246,6 +313,8 @@ void SimpleCongruenceClosure::readDistinct(Literal* lit) { CALL("SimpleCongruenceClosure::readDistinct"); + LOG("dp_cc_distinct","adding distinct constraint "<<(*lit)); + bool pos = lit->isPositive(); DistinctStack& tgtDStack = pos ? _distinctConstraints : _negDistinctConstraints; tgtDStack.push(DistinctEntry(lit)); @@ -255,6 +324,7 @@ void SimpleCongruenceClosure::readDistinct(Literal* lit) TermList arg = ait.next(); unsigned cNum = convertFO(arg); tgtStack.push(cNum); + LOG("dp_cc_distinct"," dist const "< classList; - /** If reprConst==0, contains list of pair names in whose pairs this - * constant appears as a representative of one of the arguments */ + /** + * If reprConst==0, contains list of pair names in whose pairs this + * constant appears as a representative of one of the arguments. + * Irregardless of the value f reprConst, also contains representatives + * of all pairs that have this very constant as one of arguments. + */ Stack useList; }; @@ -167,7 +162,7 @@ class SimpleCongruenceClosure : public DecisionProcedure /** * Map from signature symbols to the local constant numbers. - * (if the bool is true, symbol si function, otherwise a predicate). + * (if the bool is true, symbol is function, otherwise a predicate). */ DHMap,unsigned> _sigConsts; diff --git a/Debug/Log_TagDecls.cpp b/Debug/Log_TagDecls.cpp index 79a3adad9b..af59e3685f 100644 --- a/Debug/Log_TagDecls.cpp +++ b/Debug/Log_TagDecls.cpp @@ -239,6 +239,10 @@ void Logging::doTagDeclarations() DOC("unsatisfiable subset"), PARENT("dp_cc_interf",1)); + DECL("dp_cc_distinct", + DOC("distinct constraints"), + PARENT("dp_cc",3)); + DECL("dp_cc_fo_conv", DOC("conversion of first-order literals to internal represenation"), PARENT("dp_cc",1)); @@ -579,7 +583,10 @@ void Logging::doTagDeclarations() PARENT("pp_aig_compr",1)); DECL("pp_aig_compr_units", DOC("units modified by aig compression"), - PARENT("pp_aig_compr",21)); + PARENT("pp_aig_compr",2)); + DECL("pp_aig_compr_atom", + DOC("units modified by aig compression"), + PARENT("pp_aig_compr",3)); DECL("pp_aiginl", DOC("AIG based inlining"), diff --git a/Shell/AIGCompressor.cpp b/Shell/AIGCompressor.cpp index 986fe2d007..8b618287fc 100644 --- a/Shell/AIGCompressor.cpp +++ b/Shell/AIGCompressor.cpp @@ -699,6 +699,8 @@ AIGRef AIGCompressor::tryCompressAtom(AIGRef atom) CALL("AIGCompressor::tryCompressAtom"); ASS(atom.isAtom()); + LOG("pp_aig_compr_atom", "trying to compress atom "<isEquality()) { unsigned distGroup; if(*lit->nthArgument(0)==*lit->nthArgument(1)) { + LOG("pp_aig_compr_atom", "compressed trivial equality"); return isNeg ? _aig.getFalse() : _aig.getTrue(); } if(Inferences::DistinctEqualitySimplifier::mustBeDistinct(*lit->nthArgument(0), *lit->nthArgument(1), distGroup) && distGroup<=Signature::LAST_BUILT_IN_DISTINCT_GROUP) { + LOG("pp_aig_compr_atom", "compressed distinct equality"); return isNeg ? _aig.getTrue() : _aig.getFalse(); } } @@ -723,6 +727,7 @@ AIGRef AIGCompressor::tryCompressAtom(AIGRef atom) Literal* litVal; if(_ilEval->evaluate(lit, isConst, litVal, constVal)) { if(isConst) { + LOG("pp_aig_compr_atom", "compressed interptered tautology"); return (constVal^isNeg) ? _aig.getTrue() : _aig.getFalse(); } else { @@ -731,10 +736,12 @@ AIGRef AIGCompressor::tryCompressAtom(AIGRef atom) } } if(lit==lit0) { + LOG("pp_aig_compr_atom", "no compression achieved"); return atom; } else { AIGRef newPos = _aig.getLit(lit); + LOG("pp_aig_compr_atom", "compressed to atom "<<(isNeg ? newPos.neg() : newPos)); return isNeg ? newPos.neg() : newPos; } } diff --git a/VUtils/SimpleSMT.cpp b/VUtils/SimpleSMT.cpp index 68bfa0705c..ae8fdd2226 100644 --- a/VUtils/SimpleSMT.cpp +++ b/VUtils/SimpleSMT.cpp @@ -166,6 +166,8 @@ void SimpleSMT::preprocessProblem(int argc, char** argv) env.options->setInputFile(fname); env.options->set("aig_bdd_sweeping","on"); + env.options->set("inequality_splitting","0"); + env.options->set("flatten_top_level_conjunctions","on"); Problem* prb = UIHelper::getInputProblem(*env.options); TimeCounter tc2(TC_PREPROCESSING);