#include <string>
#include <iostream>
#include <sstream>
#include <vector>
#include "os.h"
#include "exception.h"
#include "compat_hash_map.h"
#include "compat_hash_set.h"
#include "cvc_util.h"
Include dependency graph for debug.h:
This graph shows which files directly or indirectly include this file:
Go to the source code of this file.
Author: Sergey Berezin
Created: Thu Dec 5 13:12:59 2002
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 debug.h.
| #define FatalAssert | ( | cond, | |||
| msg | ) |
Value:
if(!(cond)) \ CVC3::fatalError(__FILE__, __LINE__, #cond, msg)
This macro stays even in the non-debug build, so the end users can send us meaningful bug reports.
Definition at line 37 of file debug.h.
Referenced by SAT::CNF_Manager::addAssumption(), SAT::CNF_Manager::addLemma(), CVC3::TheoryArithNew::assertFact(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), MiniSat::Solver::checkClause(), CVC3::VCL::checkTCC(), MiniSat::Solver::checkTrail(), CVC3::TheoryBitvector::checkType(), MiniSat::Solver::checkWatched(), CVC3::ExprManager::clear(), CVC3::TheoremManager::clearAllFlags(), CVC3::TheoryBitvector::comparebv(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryBitvector::computeType(), CVC3::ContextMemoryManager::ContextMemoryManager(), SAT::CNF_Manager::convertLemma(), CVC3::ExprValue::decRefcount(), CVC3::VCCmd::evaluateCommand(), CVC3::SearchSat::findSplitterRec(), CVC3::TheoryDatatype::getConstant(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), CVC3::ContextMemoryManager::newChunk(), CVC3::MemoryManagerChunks::newChunk(), CVC3::TheoryQuant::newTopMatch(), MiniSat::Solver::nextClauseID(), CVC3::ExprManager::nextFlag(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryBitvector::normalizeConcat(), CVC3::TheoryArithNew::EpsRational::operator<=(), CVC3::TheoremValue::operator=(), CVC3::TheoryBitvector::parseExprOp(), CVC3::pow(), CVC3::Translator::preprocessRec(), CVC3::TheoryDatatype::print(), CVC3::TheoryBitvector::print(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::TheoryQuant::recSynMatch(), CVC3::TheoryArithNew::registerAtom(), CVC3::ExprManager::registerSubclass(), CVC3::VCCmd::reportResult(), CVC3::ContextObj::restoreData(), CVC3::TheoryArithNew::rewrite(), MiniSat::Solver::search(), SAT::DPLLTMiniSat::search(), SAT::Clause::setId(), CVC3::CDFlags::setNull(), CVC3::TheoryBitvector::setup(), CVC3::TheoryBitvector::setupExpr(), CVC3::ContextManager::switchContext(), CVC3::TheoryQuant::synNewInst(), CVC3::TheoremValue::TheoremValue(), CVC3::TheoryArithNew::EpsRational::toString(), SAT::CNF_Manager::translateExpr(), CVC3::ExprManager::unregisterPrettyPrinter(), CVC3::Clause::~Clause(), CVC3::ClauseOwner::~ClauseOwner(), CVC3::ClauseValue::~ClauseValue(), CVC3::ContextObj::~ContextObj(), CVC3::ExprManager::~ExprManager(), CVC3::RegTheoremValue::~RegTheoremValue(), CVC3::RWTheoremValue::~RWTheoremValue(), CVC3::Theorem::~Theorem(), and CVC3::TheoremValue::~TheoremValue().
| #define IF_DEBUG | ( | code | ) | code |
Any debugging code must be within IF_DEBUG(...).
Definition at line 54 of file debug.h.
Referenced by CVC3::Assumptions::add(), CVC3::TheoryCore::addFact(), CVC3::SearchSat::addLemma(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::TheoryBitvector::addSharedTerm(), MiniSat::Solver::analyze(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::SearchSat::assertLit(), CVC3::SearchEngineFast::bcp(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::CDFlags::CDFlags(), CVC3::CDList< CVC3::Literal >::CDList(), CVC3::CDMap< CVC3::Expr, CVC3::Expr, HashFcn >::CDMap(), CVC3::CDMapOrdered< Key, Data >::CDMapOrdered(), CVC3::CDO< CVC3::QueryResult >::CDO(), CVC3::CDOmap< CVC3::Expr, CVC3::Expr, HashFcn >::CDOmap(), CVC3::CDOmapOrdered< Key, Data >::CDOmapOrdered(), CVC3::Scope::check(), CVC3::TheoryUF::checkSat(), CVC3::TheoryCore::checkSATCore(), CVC3::SearchEngineFast::checkValidMain(), CVC3::ExprManager::clear(), CVC3::TheoryCore::collectModelValues(), CVC3::TheoryArithOld::computeBaseType(), CVC3::TheoryArithNew::computeBaseType(), MiniSat::Derivation::computeRootReason(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::ContextObj::ContextObj(), SAT::CNF_Manager::convertLemma(), CVC3::ValidityChecker::createFlags(), CVC3::DecisionEngine::DecisionEngine(), CVC3::Variable::deriveThmRec(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::VCCmd::evaluateCommand(), CVC3::VCCmd::evaluateNext(), CVC3::ExprManager::ExprManager(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::SearchEngineFast::findSplitter(), CVC3::DecisionEngineMBTF::findSplitter(), CVC3::DecisionEngineDFS::findSplitter(), CVC3::DecisionEngineCaching::findSplitter(), CVC3::SearchEngineFast::fixConflict(), CVC3::Theory::getModelTerm(), MiniSat::Solver::insertClause(), CVC3::TheoryArithOld::kidsCanonical(), CVC3::TheoryArithNew::kidsCanonical(), CVC3::CNF_TheoremProducer::learnedClause(), main(), CVC3::TheoryQuant::naiveCheckSat(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::TheoremProducer::newTheorem3(), CVC3::SearchImplBase::newUserAssumption(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::NotifyList::NotifyList(), CVC3::operator<<(), CVC3::Context::pop(), CVC3::VCL::popScope(), CVC3::VCL::poptoScope(), CVC3::TheoryCore::processEquality(), CVC3::TheoryArithOld::projectInequalities(), MiniSat::Solver::propagate(), CVC3::Context::push(), CVC3::VCL::pushScope(), CVC3::ExprManager::rebuild(), CVC3::SearchEngineFast::recordFact(), CVC3::Expr::recursiveSubst(), CVC3::TheoryCore::registerAtom(), MiniSat::Derivation::registerClause(), CVC3::VCCmd::reportResult(), MiniSat::Solver::resolveTheoryImplication(), CVC3::TheoryUF::rewrite(), CVC3::TheoryBitvector::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryCore::rewriteCore(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::SearchEngineFast::SearchEngineFast(), CVC3::SearchImplBase::SearchImplBase(), CVC3::VariableValue::setAssumpThm(), CVC3::Expr::setFind(), CVC3::TheoryCore::setFindLiteral(), CVC3::Theory::setInconsistent(), CVC3::SearchEngineFast::setInconsistent(), CVC3::Expr::setRep(), CVC3::Expr::setSig(), CVC3::TheoryCore::setupTerm(), CVC3::VariableValue::setValue(), sighandler(), CVC3::TheoryCore::simplify(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryCore::solve(), CVC3::TheoryArithOld::solvedForm(), CVC3::TheoryArithNew::solvedForm(), CVC3::SearchEngineFast::split(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::TheoryArithNew::TheoryArithNew(), CVC3::TheoryArithOld::TheoryArithOld(), CVC3::TheoryQuant::TheoryQuant(), CVC3::SearchEngineFast::traceConflict(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), CVC3::ContextObj::update(), CVC3::CDFlags::update(), MiniSat::Solver::updateConflict(), CVC3::ContextObj::~ContextObj(), CVC3::RegTheoremValue::~RegTheoremValue(), CVC3::RWTheoremValue::~RWTheoremValue(), CVC3::Theorem::~Theorem(), and CVC3::TheoremValue::~TheoremValue().
| #define DBG_PRINT | ( | cond, | |||
| pre, | |||||
| v, | |||||
| post | ) |
Value:
if(cond) CVC3::debugger.getOS() \ << (pre) << (v) << (post) << std::endl
If 'cond' is true, print 'pre', then 'v', then 'post'. The type of v must have overloaded operator<<. It expects a ';' after it.
| #define DBG_PRINT_MSG | ( | cond, | |||
| msg | ) | if(cond) CVC3::debugger.getOS() << (msg) << std::endl |
| #define TRACE | ( | flag, | |||
| pre, | |||||
| v, | |||||
| post | ) | DBG_PRINT(CVC3::debugger.trace(flag), pre, v, post) |
Same as DBG_PRINT, only takes a flag name instead of a general condition.
Definition at line 68 of file debug.h.
Referenced by SATAssignmentHook().
| #define TRACE_MSG | ( | flag, | |||
| msg | ) | DBG_PRINT_MSG(CVC3::debugger.trace(flag), msg) |
Same as TRACE, but for a simple message.
Definition at line 72 of file debug.h.
Referenced by CVC3::SearchImplBase::addCNFFact(), CVC3::SearchImplBase::addFact(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchImplBase::applyCNFRules(), CVC3::VCL::assertFormula(), CVC3::SearchEngineFast::bcp(), CVC3::TheoryCore::buildModel(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchSimple::checkValidRec(), CVC3::ExprManager::clear(), CVC3::SearchEngineFast::clearFacts(), CVC3::SearchEngineFast::clearLiterals(), CVC3::TheoryCore::collectBasicVars(), CVC3::SearchImplBase::enqueueCNF(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchEngineFast::enqueueFact(), CVC3::VCCmd::evaluateCommand(), CVC3::VCCmd::evaluateNext(), CVC3::SearchImplBase::findInCNFCache(), CVC3::SearchEngineFast::findSplitter(), CVC3::SearchEngineFast::fixConflict(), main(), CVC3::Clause::markDeleted(), CVC3::TheoryArithOld::projectInequalities(), CVC3::SearchEngineFast::propagate(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), CVC3::SearchEngineFast::setInconsistent(), CVC3::TheoryArithOld::solvedForm(), CVC3::TheoryArithNew::solvedForm(), CVC3::SearchEngineFast::split(), CVC3::SearchEngineFast::traceConflict(), CVC3::SearchEngineFast::updateLitCounts(), CVC3::ClauseValue::~ClauseValue(), CVC3::ExprManager::~ExprManager(), and CVC3::VCL::~VCL().
| #define DebugAssert | ( | cond, | |||
| str | ) |
Value:
if(!(cond)) \ CVC3::debugError(__FILE__, __LINE__, #cond, str)
Definition at line 76 of file debug.h.
Referenced by MiniSat::Clause::activity(), CVC3::Assumptions::add(), CVC3::Assumptions::add1(), CVC3::Theory::addBoundVar(), CVC3::TheoryArithOld::VarOrderGraph::addEdge(), CVC3::TheoryCore::addFact(), CVC3::SearchSat::addLemma(), CVC3::SearchEngineFast::addLiteralFact(), CVC3::SearchEngineFast::addNewClause(), SAT::DPLLTBasic::addNewClause(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::Theory::addSplitter(), CVC3::SearchImplBase::addSplitter(), CVC3::SearchEngineFast::addSplitter(), CVC3::SearchImplBase::addToCNFCache(), CVC3::Expr::addToNotify(), MiniSat::Solver::analyze(), MiniSat::Solver::analyze_removable(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::andExpr(), CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryUF::assertFact(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryQuant::assertFact(), CVC3::TheoryCore::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::SearchSat::assertLit(), CVC3::TheoryArithNew::assertLower(), CVC3::TheoryArithNew::assertUpper(), Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::assignTable(), CVC3::TheoryCore::assignValue(), CVC3::CDList< CVC3::Literal >::at(), CVC3::CDList< CVC3::Literal >::back(), MiniSat::Solver::backtrack(), CVC3::SearchEngineFast::bcp(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractConcatenation(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::TheoryCore::buildModel(), CVC3::BVConstExpr::BVConstExpr(), CVC3::TheoryBitvector::BVSize(), CVC3::TheoryDatatype::canCollapse(), CVC3::TheoryArithOld::canon(), CVC3::TheoryArithNew::canon(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducer::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::canonDivide(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::ArithTheoremProducerOld::canonInvert(), CVC3::ArithTheoremProducer::canonInvert(), CVC3::ArithTheoremProducerOld::canonInvertMult(), CVC3::ArithTheoremProducer::canonInvertMult(), CVC3::ArithTheoremProducerOld::canonInvertPow(), CVC3::ArithTheoremProducer::canonInvertPow(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstMult(), CVC3::ArithTheoremProducer::canonMultConstMult(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducer::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducerOld::canonMultPlusPlus(), CVC3::ArithTheoremProducer::canonMultPlusPlus(), CVC3::ArithTheoremProducerOld::canonMultPowLeaf(), CVC3::ArithTheoremProducer::canonMultPowLeaf(), CVC3::ArithTheoremProducerOld::canonMultPowPow(), CVC3::ArithTheoremProducer::canonMultPowPow(), CVC3::ArithTheoremProducerOld::canonPlus(), CVC3::ArithTheoremProducer::canonPlus(), CVC3::TheoryArithOld::canonPred(), CVC3::TheoryArithNew::canonPred(), CVC3::TheoryArithOld::canonPredEquiv(), CVC3::TheoryArithNew::canonPredEquiv(), CVC3::TheoryArith::canonSimp(), CVC3::TheoryArithOld::canonSimplify(), CVC3::TheoryArithNew::canonSimplify(), CVC3::SearchSat::check(), CVC3::TheoryArithOld::checkAssertEqInvariant(), checkAssump(), CVC3::SearchSat::checkConsistent(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryBitvector::checkSat(), CVC3::TheoryArithNew::checkSat(), CVC3::SearchEngineFast::checkSAT(), SAT::DPLLTMiniSat::checkSat(), SAT::DPLLTBasic::checkSat(), CVC3::TheoryCore::checkSATCore(), CVC3::TheoryUF::checkType(), CVC3::TheoryRecords::checkType(), CVC3::TheoryDatatype::checkType(), CVC3::TheoryCore::checkType(), CVC3::TheoryArray::checkType(), CVC3::TheoryArithOld::checkType(), CVC3::TheoryArithNew::checkType(), CVC3::ExprManager::checkType(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchSimple::checkValidRec(), MiniSat::Clause_new(), CVC3::ClauseValue::ClauseValue(), CVC3::Theorem::clearAllFlags(), CVC3::Expr::clearFlags(), CVC3::Expr::clearRewriteNormal(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryCore::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryArithOld::computeBaseType(), CVC3::TheoryArithNew::computeBaseType(), CVC3::computeBVConst(), CVC3::TheoryBitvector::computeBVConst(), CVC3::BitvectorTheoremProducer::computeCarry(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::TheoryUF::computeModel(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryArithOld::computeModel(), CVC3::TheoryArithNew::computeModel(), CVC3::TheoryCore::computeModelBasic(), CVC3::TheoryArray::computeModelTerm(), CVC3::TheoryBitvector::computeNegBVConst(), CVC3::TheoryArithNew::computeNormalFactor(), MiniSat::Derivation::computeRootReason(), CVC3::TheoryUF::computeTCC(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryRecords::computeTCC(), CVC3::TheoryQuant::computeTCC(), CVC3::TheoryDatatype::computeTCC(), CVC3::TheoryArray::computeTCC(), CVC3::TheoryArithOld::computeTCC(), CVC3::TheoryArithNew::computeTCC(), CVC3::TheoryUF::computeType(), CVC3::TheorySimulate::computeType(), CVC3::TheoryRecords::computeType(), CVC3::TheoryQuant::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryCore::computeType(), CVC3::TypeComputerCore::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::ExprManager::computeType(), CVC3::TheoryRecords::computeTypePred(), CVC3::TheoryBitvector::computeTypePred(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::constRHSGrayShadow(), CVC3::ArithTheoremProducer::constRHSGrayShadow(), CVC3::ContextObj::ContextObj(), SAT::DPLLTMiniSat::continueCheck(), SAT::DPLLTBasic::continueCheck(), SAT::CNF_Manager::convertLemma(), CVC3::SearchEngineTheoremProducer::convertToCNF(), CVC3::ExprValue::copy(), CVC3::Clause::countOwner(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducerOld::create_t2(), CVC3::ArithTheoremProducer::create_t2(), CVC3::ArithTheoremProducerOld::create_t3(), CVC3::ArithTheoremProducer::create_t3(), CVC3::Clause::deleted(), SAT::CNF_Formula_Impl::deleteLast(), CVC3::TheoryArithNew::deriveGomoryCut(), CVC3::Variable::deriveThmRec(), CVC3::TheoryCore::difference(), CVC3::Clause::dir(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::Translator::dump(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryCore::enqueueFact(), CVC3::TheoryCore::enqueueSE(), CVC3::VCCmd::evaluateCommand(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::Expr::Expr(), CVC3::ExprApply::ExprApply(), CVC3::ExprApplyTmp::ExprApplyTmp(), CVC3::ExprValue::ExprValue(), CVC3::ArithTheoremProducerOld::f(), CVC3::ArithTheoremProducer::f(), CVC3::Theory::find(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArithNew::findCoefficient(), CVC3::SearchImplBase::findInCNFCache(), findPolarity(), CVC3::TheoryArithOld::findRationalBound(), CVC3::TheoryArithNew::findRationalBound(), CVC3::Theory::findRef(), CVC3::SearchEngineFast::findSplitter(), CVC3::DecisionEngineMBTF::findSplitter(), CVC3::DecisionEngineCaching::findSplitter(), CVC3::SearchSat::findSplitterRec(), CVC3::Translator::finish(), MiniSat::Derivation::finish(), CVC3::SearchEngineFast::fixConflict(), CVC3::TheoryBitvector::flattenBVPlus(), CVC3::VCL::forallExpr(), CVC3::TheoryArithOld::freeConstIneq(), CVC3::SearchEngineFast::fullCheck(), CVC3::VCL::funType(), genInstSetThm(), genPartInstSetThm(), CVC3::SmartCDO< unsigned >::get(), SAT::DPLLTMiniSat::getActiveSolver(), CVC3::VCL::getAssumptionsRec(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theory::getBaseType(), CVC3::TheoryBitvector::getBitvectorTypeParam(), CVC3::ExprValue::getBody(), CVC3::Expr::getBody(), CVC3::CLFlag::getBool(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::ExprValue::getBoundIndex(), CVC3::Expr::getBoundIndex(), Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::getBucketByIndex(), CVC3::TheoryBitvector::getBVConstSize(), CVC3::TheoryBitvector::getBVConstValue(), CVC3::TheoryBitvector::getBVIndex(), CVC3::TheoryBitvector::getBVMultParam(), CVC3::TheoryBitvector::getBVPlusParam(), CVC3::Theorem::getCachedValue(), MiniSat::Solver::getConflictLevel(), CVC3::TheoryDatatype::getConsForTester(), CVC3::TheoryDatatype::getConsPos(), CVC3::TheoryDatatype::getConstant(), CVC3::getConstructor(), CVC3::Expr::getEM(), CVC3::ExprValue::getExistential(), CVC3::Expr::getExistential(), CVC3::Theorem::getExpandFlag(), CVC3::SearchSat::getExplanation(), CVC3::Theorem::getExpr(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), SAT::CNF_Manager::getFanin(), SAT::CNF_Manager::getFanout(), CVC3::TheoryRecords::getField(), CVC3::ExprValue::getField(), CVC3::TheoryRecords::getFieldIndex(), CVC3::TheoryRecords::getFields(), CVC3::ExprValue::getFields(), CVC3::Expr::getFind(), CVC3::Expr::getFindLevel(), CVC3::Assumptions::getFirst(), CVC3::TheoryBitvector::getFixedLeftShiftParam(), CVC3::TheoryBitvector::getFixedRightShiftParam(), CVC3::Expr::getFlag(), CVC3::CLFlags::getFlag(), CVC3::CLFlags::getFlag0(), CVC3::SearchSat::getImplication(), MiniSat::Solver::getImplicationLevel(), CVC3::TheoryCore::getImpliedLiteralByIndex(), CVC3::TheoryRecords::getIndex(), CVC3::CLFlag::getInt(), CVC3::Expr::getKids(), CVC3::ExprManager::getKindName(), CVC3::TheoremValue::getLHS(), CVC3::Theorem::getLHS(), CVC3::Clause::getLiteral(), CVC3::Clause::getLiterals(), CVC3::Theorem::getLitFlag(), CVC3::TheoryArithNew::getLowerBoundThm(), SAT::Clause::getMaxVar(), MiniSat::Heap< MiniSat::VarOrder_lt >::getMin(), CVC3::ExprValue::getMM(), CVC3::ExprManager::getMM(), CVC3::Expr::getMMIndex(), CVC3::Theory::getModelTerm(), CVC3::ExprValue::getName(), CVC3::Expr::getName(), CVC3::ExprValue::getOp(), CVC3::Expr::getOp(), CVC3::Expr::getOpExpr(), CVC3::Theorem::getProof(), CVC3::Theorem::getQuantLevel(), CVC3::ExprValue::getRational(), CVC3::Expr::getRational(), CVC3::TheoryDatatype::getReachablePredicate(), MiniSat::Solver::getReason(), CVC3::ExprValue::getRep(), CVC3::Expr::getRep(), CVC3::TheoremValue::getRHS(), CVC3::Theorem::getRHS(), CVC3::Theorem::getScope(), CVC3::TheoryDatatype::getSelectorInfo(), CVC3::ExprValue::getSig(), CVC3::Expr::getSig(), CVC3::ExprValue::getString(), CVC3::Expr::getString(), CVC3::CLFlag::getString(), CVC3::CLFlag::getStrVec(), CVC3::TheoryBitvector::getSXIndex(), CVC3::ExprValue::getTheorem(), CVC3::Expr::getTheorem(), CVC3::Clause::getTheorem(), CVC3::TheoryCore::getTheoremForTerm(), CVC3::ExprValue::getTupleIndex(), CVC3::TheoryBitvector::getTypePredExpr(), CVC3::TheoryBitvector::getTypePredType(), CVC3::ExprValue::getUid(), CVC3::Expr::getUid(), CVC3::TheoryArithNew::getUpperBoundThm(), CVC3::SearchSat::getValue(), SAT::DPLLTMiniSat::getValue(), CVC3::BVConstExpr::getValue(), CVC3::ExprValue::getVar(), SAT::Lit::getVar(), CVC3::ExprValue::getVars(), CVC3::Expr::getVars(), CVC3::TheoryQuant::goodSynMatch(), CVC3::ArithTheoremProducerOld::greaterthan(), CVC3::ArithTheoremProducer::greaterthan(), CVC3::Expr::hasFind(), CVC3::ExprManager::hash(), hasMoreBVs(), MiniSat::Heap< MiniSat::VarOrder_lt >::increase(), CVC3::Expr::indent(), MiniSat::Heap< MiniSat::VarOrder_lt >::inHeap(), CVC3::RWTheoremValue::init(), CVC3::TheoryDatatypeLazy::initializeLabels(), CVC3::TheoryDatatype::initializeLabels(), MiniSat::Heap< MiniSat::VarOrder_lt >::insert(), MiniSat::Solver::insertClause(), MiniSat::Solver::insertLemma(), CVC3::ExprManager::installExprValue(), CVC3::Theory::installID(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::ArrayTheoremProducer::interchangeIndices(), CVC3::Expr::isApply(), CVC3::Theorem::isAssump(), CVC3::Theorem::isFlagged(), CVC3::Theory::isLeafIn(), CVC3::TheoryArithOld::isolateVariable(), CVC3::Theorem::isRewrite(), CVC3::CNF_TheoremProducer::learnedClause(), MiniSat::Lemma_new(), CVC3::TheoryArithOld::lessThanVar(), CVC3::TheoryArithNew::lessThanVar(), CVC3::TheoryQuant::loc_gterm(), CVC3::SearchSat::makeDecision(), CVC3::Clause::markDeleted(), CVC3::Clause::markSat(), CVC3::TheoryDatatypeLazy::mergeLabels(), CVC3::TheoryDatatype::mergeLabels(), CVC3::Expr::mkOp(), CVC3::ArithTheoremProducerOld::modEq(), CVC3::ArithTheoremProducer::modEq(), CVC3::ArithTheoremProducerOld::monomialModM(), CVC3::ArithTheoremProducer::monomialModM(), CVC3::ArithTheoremProducerOld::monomialMulF(), CVC3::ArithTheoremProducer::monomialMulF(), CVC3::multExpr(), CVC3::ContextObjChain::name(), CVC3::TheoryBitvector::newBitvectorTypeExpr(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::ExprManager::newBoundVarExpr(), CVC3::TheoryBitvector::newBVAndExpr(), CVC3::TheoryBitvector::newBVCompExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVIndexExpr(), CVC3::TheoryBitvector::newBVLEExpr(), CVC3::TheoryBitvector::newBVLTExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVNandExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVNorExpr(), CVC3::TheoryBitvector::newBVOneString(), CVC3::TheoryBitvector::newBVOrExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVSLEExpr(), CVC3::TheoryBitvector::newBVSLTExpr(), CVC3::TheoryBitvector::newBVSubExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoryBitvector::newBVXnorExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::ContextMemoryManager::newChunk(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::ContextMemoryManager::newData(), CVC3::MemoryManagerChunks::newData(), CVC3::ExprManager::newExprValue(), CVC3::TheoryBitvector::newFixedConstWidthLeftShiftExpr(), CVC3::TheoryBitvector::newFixedLeftShiftExpr(), CVC3::TheoryBitvector::newFixedRightShiftExpr(), CVC3::Theory::newFunction(), CVC3::SearchImplBase::newIntAssumption(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::ExprManager::newKind(), CVC3::ExprManager::newLeafExpr(), CVC3::TheoremProducer::newPf(), CVC3::ExprManager::newSkolemExpr(), CVC3::TheoryBitvector::newSXExpr(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::Theory::newVar(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryBitvector::normalizeBVArith(), CVC3::TheoryBitvector::normalizeConcat(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::Op::Op(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::TheoryArithNew::EpsRational::operator *(), CVC3::TheoryArithNew::EpsRational::operator+(), Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::const_iterator::operator++(), Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::iterator::operator++(), CVC3::TheoryArithNew::EpsRational::operator+=(), CVC3::TheoryArithNew::EpsRational::operator-(), CVC3::TheoryArithNew::EpsRational::operator/(), CVC3::Theorem::operator=(), CVC3::ContextObj::operator=(), CVC3::CLFlag::operator=(), CVC3::ClauseOwner::operator=(), CVC3::Clause::operator=(), Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::const_iterator::operator==(), Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::iterator::operator==(), CVC3::ExprValue::operator==(), CVC3::Expr::operator[](), CVC3::CDList< CVC3::Literal >::operator[](), CVC3::orExpr(), CVC3::TheoryBitvector::pad(), CVC3::BitvectorTheoremProducer::pad(), parse_args(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryUF::parseExprOp(), CVC3::TheorySimulate::parseExprOp(), CVC3::TheoryRecords::parseExprOp(), CVC3::TheoryQuant::parseExprOp(), CVC3::TheoryDatatype::parseExprOp(), CVC3::TheoryCore::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArray::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArithOld::pickMonomial(), CVC3::TheoryArithNew::pivot(), CVC3::TheoryArithNew::pivotAndUpdate(), CVC3::TheoryArithNew::pivotRule(), CVC3::plusExpr(), MiniSat::Solver::pop(), SAT::DPLLTMiniSat::pop(), SAT::DPLLTBasic::pop(), CVC3::Context::pop(), CVC3::CDList< CVC3::Literal >::pop_back(), CVC3::ExprStream::popDag(), CVC3::ExprStream::popIndent(), CVC3::pow(), CVC3::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryCore::print(), CVC3::TheoryBitvector::print(), CVC3::Expr::print(), CVC3::Translator::printArrayExpr(), CVC3::Expr::printAST(), MiniSat::Derivation::printProof(), CVC3::TheoryArith::printRational(), printUsage(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryCore::processCond(), CVC3::TheoryCore::processEquality(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processIntEq(), processNode(), CVC3::TheoryCore::processNotify(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::SearchImplBase::processResult(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryCore::processUpdates(), CVC3::TheoryArithOld::projectInequalities(), CVC3::SearchEngineFast::propagate(), MiniSat::Solver::propagate(), CVC3::Circuit::propagate(), CVC3::TheoryArithNew::propagateTheory(), MiniSat::Solver::push(), CVC3::ExprTransform::pushNegation1(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::ExprTransform::pushNegationRec(), CVC3::VCL::ratExpr(), CVC3::ExprManager::rebuild(), CVC3::ExprManager::rebuildRec(), CVC3::VCL::recordExpr(), CVC3::SearchSat::recordNewRootLit(), CVC3::VCL::recordType(), CVC3::TheoryQuant::recSynMatch(), recursiveExprScore(), CVC3::TheoryArithOld::refineCounterExample(), CVC3::TheoryArithNew::refineCounterExample(), CVC3::TheoryCore::registerAtom(), SAT::CNF_Manager::registerAtom(), MiniSat::Derivation::registerClause(), MiniSat::Derivation::registerInference(), CVC3::Theory::registerKinds(), CVC3::ExprManager::registerPrettyPrinter(), CVC3::Theory::registerTheory(), SAT::CD_CNF_Formula::registerUnit(), SAT::CNF_Formula_Impl::registerUnit(), MiniSat::Solver::registerVar(), CVC3::RegTheoremValue::RegTheoremValue(), MiniSat::Derivation::removedClause(), MiniSat::Solver::removeWatch(), CVC3::TheoryArray::renameExpr(), SAT::CNF_Manager::replaceITErec(), CVC3::VCCmd::reportResult(), MiniSat::Solver::requestPop(), MiniSat::Solver::resolveTheoryImplication(), CVC3::SearchEngineFast::restartInternal(), CVC3::ContextObjChain::restore(), CVC3::SearchSat::restorePre(), CVC3::TheoryRecords::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryCore::rewriteCore(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteFalse(), CVC3::CoreTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CoreTheoremProducer::rewriteIteTrue(), CVC3::TheoryCore::rewriteLitCore(), CVC3::TheoryCore::rewriteLiteral(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite2(), CVC3::CommonTheoremProducer::rewriteReflexivity(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::TheoryArith::rewriteToDiff(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::BitvectorTheoremProducer::rightShiftToConcat(), CVC3::Clause::sat(), MiniSat::Solver::search(), SAT::DPLLTMiniSat::search(), CVC3::TheoryArithOld::separateMonomial(), CVC3::TheoryArithNew::separateMonomial(), CVC3::SmartCDO< unsigned >::set(), CVC3::Variable::setAssumpThm(), MiniSat::Heap< MiniSat::VarOrder_lt >::setBounds(), CVC3::Theorem::setCachedValue(), CVC3::Expr::setComputeTransClosure(), CVC3::Expr::setContainsBoundVar(), CVC3::Theorem::setExpandFlag(), CVC3::Expr::setFind(), CVC3::TheoryCore::setFindLiteral(), CVC3::Expr::setFinite(), CVC3::Theorem::setFlag(), CVC3::Expr::setFlag(), CVC3::CLFlags::setFlag(), CVC3::Expr::setImpliedLiteral(), CVC3::Expr::setIntAssumption(), CVC3::Expr::setInUserAssumption(), CVC3::Expr::setIsAtomicFlag(), CVC3::Expr::setJustified(), CVC3::Theorem::setLitFlag(), MiniSat::Solver::setPushID(), CVC3::Theorem::setQuantLevel(), CVC3::Expr::setRegisteredAtom(), CVC3::ExprValue::setRep(), CVC3::Expr::setRep(), CVC3::Expr::setRewriteNormal(), CVC3::Expr::setSelected(), CVC3::ExprValue::setSig(), CVC3::Expr::setSig(), CVC3::Expr::setSimpCache(), CVC3::Expr::setStoredPredicate(), CVC3::Expr::setTranslated(), CVC3::Expr::setType(), CVC3::TheoryArray::setup(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArithNew::setup(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryQuant::setupTriggers(), CVC3::Expr::setUserAssumption(), CVC3::Expr::setUserRegisteredAtom(), CVC3::Expr::setValidType(), CVC3::VariableValue::setValue(), CVC3::Variable::setValue(), CVC3::SearchSat::setValue(), CVC3::Expr::setWellFounded(), MiniSat::vec< int >::shrink(), CVC3::TheoryBitvector::signExtendBVLT(), CVC3::ArithTheoremProducerOld::simplifiedMultExpr(), CVC3::ArithTheoremProducer::simplifiedMultExpr(), CVC3::TheoryCore::simplify(), MiniSat::Solver::simplifyDB(), CVC3::TheoryCore::simplifyOp(), CVC3::ExprTransform::smartSimplify(), CVC3::TheoryDatatype::solve(), CVC3::TheoryCore::solve(), CVC3::TheoryArray::solve(), CVC3::TheoryArithOld::solve(), CVC3::TheoryArithNew::solve(), CVC3::TheoryArithOld::solvedForm(), CVC3::TheoryArithNew::solvedForm(), CVC3::SearchEngineFast::split(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::Expr::substExpr(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::ArithTheoremProducerOld::sumModM(), CVC3::ArithTheoremProducer::sumModM(), CVC3::ArithTheoremProducerOld::sumMulF(), CVC3::ArithTheoremProducer::sumMulF(), CVC3::ContextManager::switchContext(), CVC3::Theorem::Theorem(), CVC3::Theorem::TheoremEq(), TheoremEq(), CVC3::TheoremManager::TheoremManager(), CVC3::Theory::theoryOf(), CVC3::SearchEngineFast::traceConflict(), CVC3::CommonTheoremProducer::transitivityRule(), SAT::CNF_Manager::translateExprRec(), CVC3::VCL::tupleExpr(), CVC3::SearchEngineFast::unitPropagation(), CVC3::TheoryRecords::update(), CVC3::TheoryCore::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), CVC3::ContextObj::update(), CVC3::CDFlags::update(), MiniSat::Solver::updateConflict(), CVC3::SearchEngineFast::updateLitCounts(), CVC3::SearchEngineFast::updateLitScores(), CVC3::TheoryArithOld::updateSubsumptionDB(), CVC3::CommonTheoremProducer::varIntroSkolem(), SAT::DPLLTBasic::verify_solution(), CVC3::Clause::wp(), MiniSat::xmalloc(), and MiniSat::xrealloc().
1.5.1