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 "assumptions.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 bool compareLits (const Literal &l1, const Literal &l2)
Total order on literals for the initial sort.
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();}) void SearchEngineFast
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 39 of file search_fast.cpp.

Function Documentation

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

Total order on literals for the initial sort.

Used for debugging, to match Chaff's behavior as close as possible and track any discrepancies or inefficiencies. Ordering on literals, used to sort them by score

Definition at line 323 of file search_fast.cpp.

References CVC3::Literal::score().

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

IF_DEBUG ( )

Recompute the scores for all known literals. This is a relatively expensive procedure, so it should not be called too often. Currently, it is called once per 100 splitters.

Definition at line 329 of file search_fast.cpp.

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

Definition at line 1096 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 1108 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().