src/decision/justification_heuristic.h

   1 /*********************                                                        */
   2 /*! \file justification_heuristic.h
   3  ** \verbatim
   4  ** Original author: kshitij
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2012  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Justification heuristic for decision making
  15  **
  16  ** A ATGP-inspired justification-based decision heuristic. See
  17  ** [insert reference] for more details. This code is, or not, based
  18  ** on the CVC3 implementation of the same heuristic.
  19  **
  20  ** It needs access to the simplified but non-clausal formula.
  21  **/
  22
  23 #ifndef __CVC4__DECISION__JUSTIFICATION_HEURISTIC
  24 #define __CVC4__DECISION__JUSTIFICATION_HEURISTIC
  25
  26 #include "decision_engine.h"
  27 #include "decision_strategy.h"
  28
  29 #include "context/cdhashset.h"
  30 #include "expr/node.h"
  31 #include "prop/sat_solver_types.h"
  32
  33 namespace CVC4 {
  34
  35 namespace decision {
  36
  37 class GiveUpException : public Exception {
  38 public:
  39   GiveUpException() :
  40     Exception("justification heuristic: giving up") {
  41   }
  42 };/* class GiveUpException */
  43
  44 class JustificationHeuristic : public ITEDecisionStrategy {
  45   typedef std::vector<pair<TNode,TNode> > IteList;
  46   typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache;
  47   typedef hash_map<TNode,TNode,TNodeHashFunction> SkolemMap;
  48
  49   // being 'justified' is monotonic with respect to decisions
  50   typedef context::CDHashSet<TNode,TNodeHashFunction> JustifiedSet;
  51   JustifiedSet d_justified;
  52   context::CDO<unsigned>  d_prvsIndex;
  53
  54   IntStat d_helfulness;
  55   IntStat d_giveup;
  56   TimerStat d_timestat;
  57
  58   /**
  59    * A copy of the assertions that need to be justified
  60    * directly. Doesn't have ones introduced during during ITE-removal.
  61    */
  62   std::vector<TNode> d_assertions;
  63   //TNode is fine since decisionEngine has them too
  64
  65   /** map from ite-rewrite skolem to a boolean-ite assertion */
  66   SkolemMap d_iteAssertions;
  67   // 'key' being TNode is fine since if a skolem didn't exist anywhere,
  68   // we won't look it up. as for 'value', same reason as d_assertions
  69
  70   /** Cache for ITE skolems present in a atomic formula */
  71   IteCache d_iteCache;
  72
  73   /**
  74    * This is used to prevent infinite loop when trying to find a
  75    * splitter. Can happen when exploring assertion corresponding to a
  76    * term-ITE.
  77    */
  78   hash_set<TNode,TNodeHashFunction> d_visited;
  79 public:
  80   JustificationHeuristic(CVC4::DecisionEngine* de, context::Context *c):
  81     ITEDecisionStrategy(de, c),
  82     d_justified(c),
  83     d_prvsIndex(c, 0),
  84     d_helfulness("decision::jh::helpfulness", 0),
  85     d_giveup("decision::jh::giveup", 0),
  86     d_timestat("decision::jh::time") {
  87     StatisticsRegistry::registerStat(&d_helfulness);
  88     StatisticsRegistry::registerStat(&d_giveup);
  89     StatisticsRegistry::registerStat(&d_timestat);
  90     Trace("decision") << "Justification heuristic enabled" << std::endl;
  91   }
  92   ~JustificationHeuristic() {
  93     StatisticsRegistry::unregisterStat(&d_helfulness);
  94     StatisticsRegistry::unregisterStat(&d_timestat);
  95   }
  96   prop::SatLiteral getNext(bool &stopSearch) {
  97     Trace("decision") << "JustificationHeuristic::getNext()" << std::endl;
  98     TimerStat::CodeTimer codeTimer(d_timestat);
  99
 100     d_visited.clear();
 101
 102     if(Trace.isOn("justified")) {
 103       for(JustifiedSet::iterator i = d_justified.begin();
 104           i != d_justified.end(); ++i) {
 105         TNode n = *i;
 106         SatLiteral l = d_decisionEngine->hasSatLiteral(n) ?
 107           d_decisionEngine->getSatLiteral(n) : -1;
 108         SatValue v = tryGetSatValue(n);
 109         Trace("justified") <<"{ "<<l<<"}" << n <<": "<<v << std::endl;
 110       }
 111     }
 112
 113     for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) {
 114       Debug("decision") << "---" << std::endl << d_assertions[i] << std::endl;
 115
 116       // Sanity check: if it was false, aren't we inconsistent?
 117       Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE);
 118
 119       SatValue desiredVal = SAT_VALUE_TRUE;
 120       SatLiteral litDecision;
 121       try {
 122         litDecision = findSplitter(d_assertions[i], desiredVal);
 123       }catch(GiveUpException &e) {
 124         return prop::undefSatLiteral;
 125       }
 126
 127       if(litDecision != undefSatLiteral)
 128         return litDecision;
 129     }
 130
 131     Trace("decision") << "jh: Nothing to split on " << std::endl;
 132
 133 #if defined CVC4_ASSERTIONS || defined CVC4_DEBUG
 134     bool alljustified = true;
 135     for(unsigned i = 0 ; i < d_assertions.size() && alljustified ; ++i) {
 136       TNode curass = d_assertions[i];
 137       while(curass.getKind() == kind::NOT)
 138         curass = curass[0];
 139       alljustified &= checkJustified(curass);
 140
 141       if(Debug.isOn("decision")) {
 142         if(!checkJustified(curass))
 143           Debug("decision") << "****** Not justified [i="<<i<<"]: "
 144                             << d_assertions[i] << std::endl;
 145       }
 146     }
 147     Assert(alljustified);
 148 #endif
 149
 150     // SAT solver can stop...
 151     stopSearch = true;
 152     d_decisionEngine->setResult(SAT_VALUE_TRUE);
 153     return prop::undefSatLiteral;
 154   }
 155
 156   void addAssertions(const std::vector<Node> &assertions,
 157                      unsigned assertionsEnd,
 158                      IteSkolemMap iteSkolemMap) {
 159     Trace("decision")
 160       << "JustificationHeuristic::addAssertions()"
 161       << " size = " << assertions.size()
 162       << " assertionsEnd = " << assertionsEnd
 163       << std::endl;
 164
 165     // Save the 'real' assertions locally
 166     for(unsigned i = 0; i < assertionsEnd; ++i)
 167       d_assertions.push_back(assertions[i]);
 168
 169     // Save mapping between ite skolems and ite assertions
 170     for(IteSkolemMap::iterator i = iteSkolemMap.begin();
 171         i != iteSkolemMap.end(); ++i) {
 172       Trace("jh-ite") << " jh-ite: " << (i->first) << " maps to "
 173                       << assertions[(i->second)] << std::endl;
 174       Assert(i->second >= assertionsEnd && i->second < assertions.size());
 175       d_iteAssertions[i->first] = assertions[i->second];
 176     }
 177   }
 178
 179   /* Compute justified */
 180   /*bool computeJustified() {
 181
 182   }*/
 183 private:
 184   SatLiteral findSplitter(TNode node, SatValue desiredVal)
 185   {
 186     bool ret;
 187     SatLiteral litDecision;
 188     ret = findSplitterRec(node, desiredVal, &litDecision);
 189     if(ret == true) {
 190       Debug("decision") << "Yippee!!" << std::endl;
 191       //d_prvsIndex = i;
 192       ++d_helfulness;
 193       return litDecision;
 194     } else {
 195       return undefSatLiteral;
 196     }
 197   }
 198
 199   /**
 200    * Do all the hard work.
 201    * @param findFirst returns
 202    */
 203   bool findSplitterRec(TNode node, SatValue value, SatLiteral* litDecision);
 204
 205   /* Helper functions */
 206   void setJustified(TNode);
 207   bool checkJustified(TNode);
 208
 209   /* If literal exists corresponding to the node return
 210      that. Otherwise an UNKNOWN */
 211   SatValue tryGetSatValue(Node n);
 212
 213   /* Get list of all term-ITEs for the atomic formula v */
 214   const JustificationHeuristic::IteList& getITEs(TNode n);
 215
 216   /* Compute all term-ITEs in a node recursively */
 217   void computeITEs(TNode n, IteList &l);
 218 };/* class JustificationHeuristic */
 219
 220 }/* namespace decision */
 221
 222 }/* namespace CVC4 */
 223
 224 #endif /* __CVC4__DECISION__JUSTIFICATION_HEURISTIC */