search_fast.cpp File Reference

#include "search_fast.h"
#include "typecheck_exception.h"
#include "search_rules.h"
#include "command_line_flags.h"
#include "cdmap.h"
#include "decision_engine_dfs.h"
#include "expr_transform.h"

Include dependency graph for search_fast.cpp:

Go to the source code of this file.

Defines

• #define followChaff   false

  When set to true, match Chaff behavior as close as possible.
  

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

---

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.

---

Definition in file search_fast.cpp.

---

Define Documentation

#define followChaff   false

When set to true, match Chaff behavior as close as possible.

Definition at line 38 of file search_fast.cpp.

Referenced by CVC3::SearchEngineFast::updateLitScores().

---

Function Documentation

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

Definition at line 141 of file search_fast.cpp.

References CVC3::CDMap< Key, Data, HashFcn >::count(), DebugAssert, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::isAssump(), CVC3::Theorem::printDebug(), and CVC3::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 167 of file search_fast.cpp.

References checkAssump(), CVC3::Theorem::clearAllFlags(), and CVC3::Theorem::withAssumptions().

Referenced by CVC3::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 322 of file search_fast.cpp.

References CVC3::Literal::score().

Referenced by CVC3::SearchEngineFast::addSplitter(), CVC3::SearchEngineFast::updateLitCounts(), and CVC3::SearchEngineFast::updateLitScores().

IF_DEBUG

(

)

Definition at line 113 of file theory_core.cpp.

References CVC3::debugger, and CVC3::Debug::dumpTrace().

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

Definition at line 1095 of file search_fast.cpp.

References DebugAssert, CVC3::Theorem::getExpr(), and CVC3::Theorem::isNull().

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 1107 of file search_fast.cpp.

References DebugAssert, CVC3::Theorem::getCachedValue(), CVC3::Theorem::getExpandFlag(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLitFlag(), CVC3::Theorem::isAbsLiteral(), CVC3::Theorem::isFlagged(), CVC3::Theorem::setCachedValue(), CVC3::Theorem::setFlag(), CVC3::Theorem::toString(), and CVC3::TRACE.

Referenced by CVC3::SearchEngineFast::analyzeUIPs().

---