No commit message

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;
 };
 

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<unsigned>::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: "<<res<<" ("<<p.first<<","<<p.second<<")");
   return res;
@@ -210,6 +272,11 @@ unsigned SimpleCongruenceClosure::convertFO(TermList trm)
 {
   CALL("SimpleCongruenceClosure::convertFO(TermList)");
 
+  unsigned cachedRes;
+  if(_termNames.find(trm, cachedRes)) {
+    return cachedRes;
+  }
+
   FOConversionWorker wrk(*this);
   SafeRecursion<TermList,unsigned,FOConversionWorker> 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 "<<arg<<" represented as number "<<cNum);
   }
 }
 
@@ -288,6 +358,9 @@ void SimpleCongruenceClosure::addLiterals(LiteralIterator lits)
 	_negEqualities.push(eq);
       }
     }
+    else if(isDistinctPred(l)) {
+      readDistinct(l);
+    }
     else {
       unsigned predConst = convertFONonEquality(l);
       CEq eq;

DP/SimpleCongruenceClosure.hpp

@@ -104,17 +104,8 @@ class SimpleCongruenceClosure : public DecisionProcedure
   static const unsigned NO_SIG_SYMBOL;
   struct ConstInfo
   {
-    void 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 init();
+    void resetEquivalences(SimpleCongruenceClosure& parent, unsigned selfIndex);
 
 
     /** If NO_SIG_SYMBOL, the constant doesn't represent a non-constant signature symbol */
@@ -146,8 +137,12 @@ class SimpleCongruenceClosure : public DecisionProcedure
     /** If reprConst==0, contains other constants whose representative
      * this constant is */
     Stack<unsigned> 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<unsigned> 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<pair<unsigned,bool>,unsigned> _sigConsts;
 

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"),

Shell/AIGCompressor.cpp

@@ -699,17 +699,21 @@ AIGRef AIGCompressor::tryCompressAtom(AIGRef atom)
   CALL("AIGCompressor::tryCompressAtom");
   ASS(atom.isAtom());
 
+  LOG("pp_aig_compr_atom", "trying to compress atom "<<atom);
+
   bool isNeg = !atom.polarity();
   Literal* lit0 = atom.getPositiveAtom();
   Literal* lit = lit0;
 
   if(lit->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;
   }
 }

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);