search_fast.cpp File Reference

Go to the source code of this file.

Functions

• static void checkAssump (const Theorem &t, const Theorem &orig, const CDMap< Expr, Theorem > &assumptions)
• static void checkAssumpDebug (const Theorem &res, const CDMap< Expr, Theorem > &assumptions)

  Check that assumptions in the result of checkValid() are a subset of assertions.
  

• static bool compareLits (const Literal &l1, const Literal &l2)

  Ordering on literals, used to sort them by score.
  

• IF_DEBUG (static string lits2str(const vector< Literal > &lits){ostringstream ss;ss<< "\n[";for(vector< Literal >::const_iterator i=lits.begin(), iend=lits.end();i!=iend;++i) ss<< *i<< "\n ";ss<< "\n]";return ss.str();})
• bool TheoremEq (const Theorem &t1, const Theorem &t2)
• static void processNode (const Theorem &thm, vector< Theorem > &lits, vector< Theorem > &gamma, vector< Theorem > &fringe, int &pending)

  Auxiliary function used in analyzeUIPs().
  

---

Detailed Description

Author: Mark Zavislak <zavislak@stanford.edu> Undergraduate Stanford University

Created: Mon Jul 21 23:52:39 UTC 2003

---

Copyright (C) 2003 by the Board of Trustees of Leland Stanford Junior University and by New York University.

License to use, copy, modify, sell and/or distribute this software and its documentation for any purpose is hereby granted without royalty, subject to the terms and conditions defined in the LICENSE file provided with this distribution. In particular:

• The above copyright notice and this permission notice must appear in all copies of the software and related documentation.

• THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES, EXPRESSED OR IMPLIED. USE IT AT YOUR OWN RISK.

---

Definition in file search_fast.cpp.

---

Function Documentation

static void checkAssump (  const Theorem &  t, const Theorem &  orig, const CDMap< Expr, Theorem > &  assumptions )  [static]

Definition at line 149 of file search_fast.cpp. References CVCL::Assumptions::begin(), CVCL::CDMap< Key, Data, HashFcn >::count(), CVCL::Assumptions::end(), CVCL::Theorem::getAssumptions(), CVCL::Theorem::getExpr(), CVCL::Theorem::isAssump(), CVCL::Theorem::printDebug(), and CVCL::Theorem::toString(). Referenced by checkAssumpDebug().

static void checkAssumpDebug (  const Theorem &  res, const CDMap< Expr, Theorem > &  assumptions )  [static]

Check that assumptions in the result of checkValid() are a subset of assertions. Only defined in the debug build. Definition at line 174 of file search_fast.cpp. References checkAssump(), CVCL::Theorem::clearAllFlags(), CVCL::Theorem::getAssumptions(), CVCL::Assumptions::isNull(), and CVCL::Theorem::withAssumptions(). Referenced by CVCL::SearchEngineFast::checkValidMain().

static bool compareLits (  const Literal &  l1, const Literal &  l2 )  [inline, static]

Ordering on literals, used to sort them by score. Used for debugging, to match Chaff's behavior as close as possible and track any discrepancies or inefficiencies. Definition at line 331 of file search_fast.cpp. References CVCL::Literal::score(). Referenced by CVCL::SearchEngineFast::addSplitter(), CVCL::SearchEngineFast::updateLitCounts(), and CVCL::SearchEngineFast::updateLitScores().

IF_DEBUG (   )

Definition at line 167 of file context.cpp.

bool TheoremEq (  const Theorem &  t1, const Theorem &  t2 )  [inline]

Definition at line 1104 of file search_fast.cpp. References CVCL::Theorem::getExpr(), and CVCL::Theorem::isNull(). Referenced by CVCL::AssumptionsValue::AssumptionsValue().

static void processNode (  const Theorem &  thm, vector< Theorem > &  lits, vector< Theorem > &  gamma, vector< Theorem > &  fringe, int &  pending )  [static]

Auxiliary function used in analyzeUIPs(). It processes a node and populates the relevant sets used in the algorithm. See also: analyzeUIPs() for more detail). Definition at line 1116 of file search_fast.cpp. References CVCL::Theorem::getCachedValue(), CVCL::Theorem::getExpandFlag(), CVCL::Theorem::getExpr(), CVCL::Theorem::getLitFlag(), CVCL::Theorem::isAbsLiteral(), CVCL::Theorem::isFlagged(), CVCL::Theorem::setCachedValue(), CVCL::Theorem::setFlag(), CVCL::Theorem::toString(), and CVCL::TRACE. Referenced by CVCL::SearchEngineFast::analyzeUIPs().

---