CVC3
2.4.1
|
#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"
Go to the source code of this file.
Macros | |
#define | followChaff false |
When set to true, match Chaff behavior as close as possible. More... | |
Functions | |
static bool | compareLits (const Literal &l1, const Literal &l2) |
Total order on literals for the initial sort. More... | |
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() More... | |
Author: Mark Zavislak zavis Undergraduate Stanford University lak@ stanf ord. edu
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 followChaff false |
When set to true, match Chaff behavior as close as possible.
Definition at line 39 of file search_fast.cpp.
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 | ( | 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();} | ) |
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.
Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchEngineFast::bcp(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchEngineFast::findSplitter(), CVC3::SearchEngineFast::fixConflict(), CVC3::SearchEngineFast::recordFact(), CVC3::SearchEngineFast::SearchEngineFast(), CVC3::SearchEngineFast::setInconsistent(), CVC3::SearchEngineFast::split(), and CVC3::SearchEngineFast::traceConflict().
Definition at line 1096 of file search_fast.cpp.
References DebugAssert, CVC3::Theorem::getExpr(), and CVC3::Theorem::isNull().
Referenced by CVC3::Assumptions::Assumptions().
|
static |
Auxiliary function used in analyzeUIPs()
It processes a node and populates the relevant sets used in the algorithm.
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 TRACE.
Referenced by CVC3::SearchEngineFast::analyzeUIPs().