|
CVC3
|
Description: Collection of debugging macros and functions. More...
#include <string>#include <iostream>#include <sstream>#include <vector>#include "os.h"#include "exception.h"#include "cvc_util.h"Go to the source code of this file.
Description: Collection of debugging macros and functions.
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 | |||
| ) |
if(!(cond)) \ CVC3::fatalError(__FILE__, __LINE__, #cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
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 CVC3::TheoryArithOld::addPairToArithOrder(), CVC3::TheoryArray::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer3::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), MiniSat::Solver::checkClause(), MiniSat::Derivation::checkDerivation(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryBitvector::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::VCL::checkTCC(), MiniSat::Solver::checkTrail(), CVC3::TheoryDatatype::checkType(), CVC3::TheoryCore::checkType(), CVC3::TheoryBitvector::checkType(), MiniSat::Solver::checkWatched(), CVC3::ExprManager::clear(), CVC3::TheoremManager::clearAllFlags(), CVC3::TheoryBitvector::comparebv(), CVC3::TheoryBitvector::computeModel(), MiniSat::Derivation::computeRootReason(), CVC3::TheoryBitvector::computeType(), CVC3::ContextMemoryManager::ContextMemoryManager(), MiniSat::Derivation::createProof(), CVC3::ExprValue::decRefcount(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::VCCmd::evaluateCommand(), CVC3::SearchSat::findSplitterRec(), MiniSat::Derivation::finish(), CVC3::TheoryCore::finiteTypeInfo(), CVC3::TheoryBitvector::finiteTypeInfo(), CVC3::ExprManager::gc(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::TheoryDatatype::getConstant(), CVC3::CNF_TheoremProducer::getSmartClauses(), CVC3::SearchSat::getValue(), CVC3::SearchImplBase::getValue(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), CVC3::ContextMemoryManager::newChunk(), CVC3::MemoryManagerChunks::newChunk(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), MiniSat::Solver::nextClauseID(), CVC3::ExprManager::nextFlag(), CVC3::TheoryArithNew::normalize(), CVC3::BitvectorTheoremProducer::okToSplit(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::operator<=(), CVC3::TheoryArithNew::EpsRational::operator<=(), CVC3::TheoremValue::operator=(), CVC3::TheoryBitvector::parseExprOp(), MiniSat::Derivation::pop(), CVC3::pow(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryDatatype::print(), CVC3::TheoryBitvector::print(), MiniSat::Derivation::printDerivation(), CVC3::TheoryBitvector::printSmtLibShared(), CVC3::TheoryArithNew::registerAtom(), MiniSat::Derivation::registerClause(), MiniSat::Derivation::registerInference(), CVC3::ExprManager::registerSubclass(), MiniSat::Derivation::removedClause(), CVC3::VCCmd::reportResult(), MiniSat::Solver::resolveTheoryImplication(), CVC3::ContextObj::restoreData(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryBitvector::rewriteBV(), MiniSat::Solver::search(), SAT::DPLLTMiniSat::search(), CVC3::CDFlags::setNull(), CVC3::ContextManager::switchContext(), CVC3::TheoryQuant::synNewInst(), CVC3::TheoremValue::TheoremValue(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::toString(), CVC3::TheoryArithNew::EpsRational::toString(), CVC3::ExprManager::unregisterPrettyPrinter(), CVC3::Clause::~Clause(), CVC3::ClauseOwner::~ClauseOwner(), CVC3::ClauseValue::~ClauseValue(), CVC3::ContextObj::~ContextObj(), CVC3::Expr::~Expr(), CVC3::ExprManager::~ExprManager(), CVC3::RegTheoremValue::~RegTheoremValue(), CVC3::RWTheoremValue::~RWTheoremValue(), CVC3::Theorem::~Theorem(), and CVC3::TheoremValue::~TheoremValue().
| #define IF_DEBUG | ( | code | ) |
Definition at line 406 of file debug.h.
Referenced by CVC3::Assumptions::add(), CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryCore::addFact(), CVC3::SearchSat::addLemma(), CVC3::SearchEngineFast::addNonLiteralFact(), MiniSat::Solver::analyze(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::SearchSat::assertLit(), CVC3::SearchEngineFast::bcp(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::CDFlags::CDFlags(), CVC3::CDList< SmartCDO< Theorem > >::CDList(), CVC3::CDMap< Expr, Expr, HashFcn >::CDMap(), CVC3::CDMapOrdered< Key, Data >::CDMapOrdered(), CVC3::CDO< Rational >::CDO(), CVC3::CDOmap< Expr, Expr, HashFcn >::CDOmap(), CVC3::CDOmapOrdered< Key, Data >::CDOmapOrdered(), CVC3::Scope::check(), CVC3::TheoryUF::checkSat(), CVC3::TheoryArithOld::checkSat(), CVC3::TheoryCore::checkSATCore(), CVC3::SearchEngineFast::checkValidMain(), CVC3::Clause::Clause(), CVC3::ClauseValue::ClauseValue(), CVC3::ExprManager::clear(), CVC3::TheoryCore::collectModelValues(), CVC3::TheoryArithOld::computeBaseType(), CVC3::TheoryArithNew::computeBaseType(), CVC3::TheoryArith3::computeBaseType(), MiniSat::Derivation::computeRootReason(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::ContextObj::ContextObj(), CVC3::ValidityChecker::createFlags(), CVC3::DecisionEngine::DecisionEngine(), CVC3::ExprValue::decRefcount(), CVC3::Variable::deriveThmRec(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::VCCmd::evaluateCommand(), CVC3::VCCmd::evaluateNext(), CVC3::ExprManager::ExprManager(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::SearchEngineFast::findSplitter(), CVC3::DecisionEngineDFS::findSplitter(), MiniSat::Derivation::finish(), CVC3::SearchEngineFast::fixConflict(), CVC3::ExprManager::gc(), CVC3::Theory::getModelTerm(), MiniSat::Solver::insertClause(), CVC3::TheoryArithOld::kidsCanonical(), CVC3::TheoryArithNew::kidsCanonical(), CVC3::TheoryArith3::kidsCanonical(), CVC3::CNF_TheoremProducer::learnedClauses(), main(), CVC3::Clause::markDeleted(), CVC3::TheoryQuant::naiveCheckSat(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::TheoremProducer::newTheorem3(), CVC3::SearchImplBase::newUserAssumption(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::NotifyList::NotifyList(), CVC3::operator<<(), CVC3::Context::pop(), CVC3::VCL::popScope(), CVC3::VCL::poptoScope(), CVC3::TheoryArray::print(), MiniSat::Derivation::printDerivation(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArith3::projectInequalities(), MiniSat::Solver::propagate(), CVC3::Context::push(), CVC3::VCL::pushScope(), CVC3::ExprManager::rebuild(), CVC3::SearchEngineFast::recordFact(), CVC3::Expr::recursiveSubst(), CVC3::VCCmd::reportResult(), MiniSat::Solver::resolveTheoryImplication(), CVC3::TheoryUF::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryCore::rewriteCore(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteReadWrite2(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), SATDecisionHook(), CVC3::SearchEngineFast::SearchEngineFast(), CVC3::SearchImplBase::SearchImplBase(), CVC3::VariableValue::setAssumpThm(), CVC3::Expr::setEqNext(), 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::TheoryBitvector::solve(), CVC3::TheoryArithOld::solvedForm(), CVC3::TheoryArithNew::solvedForm(), CVC3::TheoryArith3::solvedForm(), CVC3::SearchEngineFast::split(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::TheoryArith3::TheoryArith3(), CVC3::TheoryArithNew::TheoryArithNew(), CVC3::TheoryArithOld::TheoryArithOld(), CVC3::TheoryQuant::TheoryQuant(), CVC3::SearchEngineFast::traceConflict(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryArith3::update(), CVC3::ContextObj::update(), CVC3::CDFlags::update(), MiniSat::Solver::updateConflict(), CVC3::VCL::VCL(), CVC3::ClauseValue::~ClauseValue(), CVC3::ContextObj::~ContextObj(), CVC3::Expr::~Expr(), CVC3::RegTheoremValue::~RegTheoremValue(), CVC3::RWTheoremValue::~RWTheoremValue(), CVC3::Theorem::~Theorem(), CVC3::TheoremValue::~TheoremValue(), and CVC3::VCL::~VCL().
| #define DebugAssert | ( | cond, | |
| str | |||
| ) |
Definition at line 408 of file debug.h.
Referenced by MiniSat::Clause::activity(), CVC3::Assumptions::add(), SAT::CNF_Manager::addAssumption(), CVC3::Theory::addBoundVar(), CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryArithOld::VarOrderGraph::addEdge(), CVC3::TheoryArith3::VarOrderGraph::addEdge(), CVC3::TheoryCore::addFact(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::SearchSat::addLemma(), SAT::CNF_Manager::addLemma(), CVC3::SearchEngineFast::addLiteralFact(), CVC3::SearchEngineFast::addNewClause(), SAT::DPLLTBasic::addNewClause(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::Theory::addSplitter(), CVC3::SearchSat::addSplitter(), CVC3::SearchImplBase::addSplitter(), CVC3::SearchEngineFast::addSplitter(), CVC3::SearchImplBase::addToCNFCache(), CVC3::Expr::addToNotify(), CVC3::TheoryArithOld::DifferenceLogicGraph::analyseConflict(), 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::TheoryBitvector::assertFact(), CVC3::TheoryArray::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::SearchSat::assertLit(), CVC3::TheoryArithNew::assertLower(), CVC3::TheoryArithNew::assertUpper(), CVC3::TheoryCore::assignValue(), CVC3::CDList< SmartCDO< Theorem > >::at(), CVC3::CDList< SmartCDO< Theorem > >::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::BitvectorTheoremProducer::buildPlusTerm(), CVC3::BVConstExpr::BVConstExpr(), CVC3::TheoryBitvector::BVSize(), CVC3::TheoryDatatype::canCollapse(), CVC3::TheoryArithOld::canon(), CVC3::TheoryArithNew::canon(), CVC3::TheoryArith3::canon(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::BitvectorTheoremProducer::canonBVMult(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducer3::canonCombineLikeTerms(), CVC3::ArithTheoremProducer::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::canonDivide(), CVC3::ArithTheoremProducer3::canonDivide(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::ArithTheoremProducerOld::canonInvert(), CVC3::ArithTheoremProducer3::canonInvert(), CVC3::ArithTheoremProducer::canonInvert(), CVC3::ArithTheoremProducerOld::canonInvertMult(), CVC3::ArithTheoremProducer3::canonInvertMult(), CVC3::ArithTheoremProducer::canonInvertMult(), CVC3::ArithTheoremProducerOld::canonInvertPow(), CVC3::ArithTheoremProducer3::canonInvertPow(), CVC3::ArithTheoremProducer::canonInvertPow(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer3::canonMult(), CVC3::ArithTheoremProducer::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstMult(), CVC3::ArithTheoremProducer3::canonMultConstMult(), CVC3::ArithTheoremProducer::canonMultConstMult(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer3::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer3::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducer3::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducer::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducerOld::canonMultPlusPlus(), CVC3::ArithTheoremProducer3::canonMultPlusPlus(), CVC3::ArithTheoremProducer::canonMultPlusPlus(), CVC3::ArithTheoremProducerOld::canonMultPowLeaf(), CVC3::ArithTheoremProducer3::canonMultPowLeaf(), CVC3::ArithTheoremProducer::canonMultPowLeaf(), CVC3::ArithTheoremProducerOld::canonMultPowPow(), CVC3::ArithTheoremProducer3::canonMultPowPow(), CVC3::ArithTheoremProducer::canonMultPowPow(), CVC3::ArithTheoremProducerOld::canonPlus(), CVC3::ArithTheoremProducer3::canonPlus(), CVC3::ArithTheoremProducer::canonPlus(), CVC3::TheoryArithOld::canonPred(), CVC3::TheoryArithNew::canonPred(), CVC3::TheoryArith3::canonPred(), CVC3::TheoryArithOld::canonPredEquiv(), CVC3::TheoryArithNew::canonPredEquiv(), CVC3::TheoryArith3::canonPredEquiv(), CVC3::TheoryArith::canonSimp(), CVC3::TheoryArithOld::canonSimplify(), CVC3::TheoryArithNew::canonSimplify(), CVC3::TheoryArith3::canonSimplify(), CVC3::TheoryArithOld::canPickEqMonomial(), CVC3::TheoryBitvector::canSolveFor(), CVC3::SearchSat::check(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::SearchSat::checkConsistent(), CVC3::TheoryCore::checkEquation(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryBitvector::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryArithOld::checkSat(), CVC3::TheoryArithNew::checkSat(), CVC3::SearchEngineFast::checkSAT(), SAT::DPLLTMiniSat::checkSat(), SAT::DPLLTBasic::checkSat(), CVC3::TheoryCore::checkSATCore(), CVC3::TheoryUF::checkType(), CVC3::TheoryRecords::checkType(), CVC3::TheoryArray::checkType(), CVC3::TheoryArithOld::checkType(), CVC3::TheoryArithNew::checkType(), CVC3::TheoryArith3::checkType(), CVC3::ExprManager::checkType(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchSimple::checkValidRec(), CVC3::BitvectorTheoremProducer::chopConcat(), CVC3::ClauseValue::ClauseValue(), CVC3::Expr::clearFlags(), CVC3::Expr::clearRewriteNormal(), CVC3::CNF_TheoremProducer::CNFConvert(), CVC3::CNF_TheoremProducer::CNFITEtranslate(), CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::TheoryCore::collectBasicVars(), CVC3::CompleteInstPreProcessor::collectIndex(), CVC3::ArithTheoremProducer3::compactNonLinearTerm(), CVC3::ArithTheoremProducer::compactNonLinearTerm(), CVC3::TheoryBitvector::comparebv(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryCore::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryArithOld::computeBaseType(), CVC3::TheoryArithNew::computeBaseType(), CVC3::TheoryArith3::computeBaseType(), 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::TheoryArith3::computeModel(), CVC3::TheoryCore::computeModelBasic(), CVC3::TheoryArray::computeModelTerm(), CVC3::TheoryBitvector::computeNegBVConst(), CVC3::TheoryArithNew::computeNormalFactor(), CVC3::TheoryUF::computeTCC(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryRecords::computeTCC(), CVC3::TheoryQuant::computeTCC(), CVC3::TheoryDatatype::computeTCC(), CVC3::TheoryBitvector::computeTCC(), CVC3::TheoryArray::computeTCC(), CVC3::TheoryArithOld::computeTCC(), CVC3::TheoryArithNew::computeTCC(), CVC3::TheoryArith3::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::TheoryArith3::computeType(), CVC3::ExprManager::computeType(), CVC3::TheoryRecords::computeTypePred(), CVC3::TheoryBitvector::computeTypePred(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::constRHSGrayShadow(), CVC3::ArithTheoremProducer3::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::ArithTheoremProducer3::create_t(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducerOld::create_t2(), CVC3::ArithTheoremProducer3::create_t2(), CVC3::ArithTheoremProducer::create_t2(), CVC3::ArithTheoremProducerOld::create_t3(), CVC3::ArithTheoremProducer3::create_t3(), CVC3::ArithTheoremProducer::create_t3(), CVC3::ArithTheoremProducer3::cycleConflict(), CVC3::ArithTheoremProducer::cycleConflict(), CVC3::Clause::deleted(), CVC3::TheoryArithNew::deriveGomoryCut(), CVC3::Variable::deriveThmRec(), CVC3::Clause::dir(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::Translator::dump(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryCore::enqueueFact(), CVC3::TheoryCore::enqueueSE(), CVC3::VCCmd::evaluateCommand(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducer3::expandGrayShadowRewrite(), CVC3::ArithTheoremProducer::expandGrayShadowRewrite(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::Expr::Expr(), CVC3::ExprApply::ExprApply(), CVC3::ExprApplyTmp::ExprApplyTmp(), CVC3::VCL::exprFromString(), CVC3::ExprValue::ExprValue(), CVC3::TheoryBitvector::extract_vars(), CVC3::TheoryArithOld::extractTermsFromInequality(), CVC3::ArithTheoremProducerOld::f(), CVC3::ArithTheoremProducer3::f(), CVC3::ArithTheoremProducer::f(), CVC3::Theory::find(), findAtom(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArith3::findBounds(), CVC3::TheoryArithNew::findCoefficient(), CVC3::SearchImplBase::findInCNFCache(), findPolarityAtomic(), CVC3::TheoryArithOld::findRationalBound(), CVC3::TheoryArithNew::findRationalBound(), CVC3::TheoryArith3::findRationalBound(), CVC3::Theory::findRef(), CVC3::SearchEngineFast::findSplitter(), CVC3::SearchSat::findSplitterRec(), CVC3::Translator::finish(), CVC3::TheoryDatatype::finiteTypeInfo(), CVC3::TypeComputerCore::finiteTypeInfo(), CVC3::ExprManager::finiteTypeInfo(), CVC3::SearchEngineFast::fixConflict(), CVC3::VCL::forallExpr(), CVC3::TheoryArithOld::freeConstIneq(), CVC3::TheoryArith3::freeConstIneq(), CVC3::VCL::funType(), CVC3::TheoryBitvector::generalBitBlast(), generateSatProof(), 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::TheoryBitvector::getBoolExtractIndex(), CVC3::ExprValue::getBoundIndex(), CVC3::Expr::getBoundIndex(), CVC3::TheoryBitvector::getBVConstSize(), CVC3::TheoryBitvector::getBVConstValue(), CVC3::TheoryBitvector::getBVIndex(), CVC3::TheoryBitvector::getBVMultParam(), CVC3::TheoryBitvector::getBVPlusParam(), MiniSat::Solver::getConflictLevel(), CVC3::TheoryDatatype::getConsForTester(), CVC3::TheoryDatatype::getConsPos(), CVC3::TheoryDatatype::getConstant(), CVC3::getConstructor(), CVC3::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), CVC3::Expr::getEM(), CVC3::Expr::getEqNext(), CVC3::ExprValue::getExistential(), CVC3::Expr::getExistential(), CVC3::SearchSat::getExplanation(), CVC3::Op::getExpr(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::TheoryArithOld::getFactors(), CVC3::TheoryArith3::getFactors(), 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::TheoryBitvector::getFixedLeftShiftParam(), CVC3::TheoryBitvector::getFixedRightShiftParam(), CVC3::Expr::getFlag(), CVC3::SearchSat::getImplication(), MiniSat::Solver::getImplicationLevel(), CVC3::TheoryCore::getImpliedLiteralByIndex(), CVC3::TheoryRecords::getIndex(), CVC3::Expr::getKids(), CVC3::ExprManager::getKindName(), SAT::SatProofNode::getLeaf(), CVC3::ArithTheoremProducerOld::getLeaves(), SAT::SatProofNode::getLeftParent(), CVC3::TheoremValue::getLHS(), SAT::SatProofNode::getLit(), CVC3::Clause::getLiteral(), CVC3::Clause::getLiterals(), CVC3::TheoryArithNew::getLowerBoundThm(), SAT::Clause::getMaxVar(), MiniSat::Heap< VarOrder_lt >::getMin(), CVC3::ExprValue::getMM(), CVC3::ExprManager::getMM(), CVC3::Expr::getMMIndex(), CVC3::Theory::getModelTerm(), CVC3::ExprValue::getName(), CVC3::Expr::getName(), CVC3::SearchSat::getNewClauses(), SAT::SatProofNode::getNodeProof(), CVC3::ExprValue::getOp(), CVC3::Expr::getOp(), CVC3::Expr::getOpExpr(), CVC3::BitvectorTheoremProducer::getPlusTerms(), SAT::DPLLTMiniSat::getProof(), CVC3::ExprValue::getRational(), CVC3::Expr::getRational(), CVC3::TheoryDatatype::getReachablePredicate(), MiniSat::Solver::getReason(), CVC3::ExprValue::getRep(), CVC3::Expr::getRep(), CVC3::TheoremValue::getRHS(), SAT::SatProofNode::getRightParent(), SAT::SatProof::getRoot(), CVC3::Theorem::GetSatAssumptionsRec(), CVC3::TheoryDatatype::getSelectorInfo(), CVC3::ExprValue::getSig(), CVC3::Expr::getSig(), CVC3::ExprValue::getString(), CVC3::Expr::getString(), CVC3::TheoryBitvector::getSXIndex(), CVC3::ExprValue::getTheorem(), CVC3::Expr::getTheorem(), CVC3::Clause::getTheorem(), CVC3::ExprValue::getTriggers(), CVC3::Expr::getTriggers(), 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(), CVC3::ExprValue::getVars(), CVC3::Expr::getVars(), CVC3::ArithTheoremProducerOld::greaterthan(), CVC3::ArithTheoremProducer3::greaterthan(), CVC3::ArithTheoremProducer::greaterthan(), CVC3::Expr::hasFind(), hasMoreBVs(), CVC3::ArithTheoremProducer3::implyDiffLogicBothBounds(), CVC3::ArithTheoremProducer::implyDiffLogicBothBounds(), CVC3::ArithTheoremProducer3::implyEqualities(), CVC3::ArithTheoremProducer::implyEqualities(), CVC3::ArithTheoremProducer3::implyNegatedInequalityDiffLogic(), CVC3::ArithTheoremProducer::implyNegatedInequalityDiffLogic(), CVC3::ArithTheoremProducer3::implyWeakerInequalityDiffLogic(), CVC3::ArithTheoremProducer::implyWeakerInequalityDiffLogic(), MiniSat::Heap< VarOrder_lt >::increase(), CVC3::Expr::indent(), MiniSat::Heap< VarOrder_lt >::inHeap(), CVC3::VCL::init(), CVC3::RWTheoremValue::init(), CVC3::TheoryDatatypeLazy::initializeLabels(), CVC3::TheoryDatatype::initializeLabels(), MiniSat::Heap< VarOrder_lt >::insert(), MiniSat::Solver::insertClause(), MiniSat::Solver::insertLemma(), CVC3::CompleteInstPreProcessor::inst(), CVC3::ExprManager::installExprValue(), CVC3::Theory::installID(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::ArithTheoremProducer3::intEqualityRationalConstant(), CVC3::ArithTheoremProducer::intEqualityRationalConstant(), CVC3::ArrayTheoremProducer::interchangeIndices(), CVC3::Expr::isApply(), CVC3::CompleteInstPreProcessor::isGood(), CVC3::ArithTheoremProducerOld::IsIntegerElim(), CVC3::ArithTheoremProducer3::IsIntegerElim(), CVC3::ArithTheoremProducer::IsIntegerElim(), CVC3::Theory::isLeafIn(), CVC3::TheoryArithOld::isNonlinearEq(), CVC3::BitvectorTheoremProducer::isolate_var(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isPowerEquality(), CVC3::TheoryArithOld::isPowersEquality(), CVC3::CompleteInstPreProcessor::isShield(), CVC3::CNF_TheoremProducer::learnedClauses(), CVC3::TheoryArith::leavesAreNumConst(), CVC3::TheoryArithOld::lessThanVar(), CVC3::TheoryArithNew::lessThanVar(), CVC3::TheoryArith3::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::ArithTheoremProducer3::modEq(), CVC3::ArithTheoremProducer::modEq(), CVC3::ArithTheoremProducerOld::monomialModM(), CVC3::ArithTheoremProducer3::monomialModM(), CVC3::ArithTheoremProducer::monomialModM(), CVC3::ArithTheoremProducerOld::monomialMulF(), CVC3::ArithTheoremProducer3::monomialMulF(), CVC3::ArithTheoremProducer::monomialMulF(), CVC3::multExpr(), 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::newBVSDivExpr(), CVC3::TheoryBitvector::newBVSLEExpr(), CVC3::TheoryBitvector::newBVSLTExpr(), CVC3::TheoryBitvector::newBVSModExpr(), CVC3::TheoryBitvector::newBVSRemExpr(), CVC3::TheoryBitvector::newBVSubExpr(), CVC3::TheoryBitvector::newBVUDivExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoryBitvector::newBVURemExpr(), 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::ExprTransform::newPPrec(), CVC3::ExprManager::newSkolemExpr(), CVC3::TheoryBitvector::newSXExpr(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::Theory::newVar(), CVC3::ArithTheoremProducer3::nonLinearIneqSignSplit(), CVC3::ArithTheoremProducer::nonLinearIneqSignSplit(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArith3::normalize(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryQuant::notifyInconsistent(), SAT::CNF_Formula_Impl::numClauses(), CVC3::TheoryBitvector::Odd_coeff(), CVC3::Op::Op(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::operator*(), CVC3::TheoryArithNew::EpsRational::operator*(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::operator+(), CVC3::TheoryArithNew::EpsRational::operator+(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::operator+=(), CVC3::TheoryArithNew::EpsRational::operator+=(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::operator-(), CVC3::TheoryArithNew::EpsRational::operator-(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::operator/(), CVC3::TheoryArithNew::EpsRational::operator/(), CVC3::Theorem::operator=(), CVC3::ContextObj::operator=(), CVC3::ClauseOwner::operator=(), CVC3::Clause::operator=(), CVC3::ExprValue::operator==(), CVC3::Expr::operator[](), CVC3::CDList< SmartCDO< Theorem > >::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::TheoryArith3::parseExprOp(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArith3::pickIntEqMonomial(), CVC3::TheoryArithOld::pickMonomial(), CVC3::TheoryArith3::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< SmartCDO< Theorem > >::pop_back(), CVC3::ExprStream::popDag(), CVC3::ExprStream::popIndent(), CVC3::pow(), CVC3::ArithTheoremProducer3::powerOfOne(), CVC3::ArithTheoremProducer::powerOfOne(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryCore::print(), CVC3::TheoryBitvector::print(), CVC3::Translator::printArrayExpr(), CVC3::Expr::printAST(), CVC3::VCCmd::printModel(), CVC3::TheoryArith::printRational(), CVC3::TheoryUF::printSmtLibShared(), CVC3::TheoryCore::printSmtLibShared(), CVC3::TheoryBitvector::printSmtLibShared(), printUsage(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryArith3::processBuffer(), CVC3::TheoryCore::processCond(), CVC3::BitvectorTheoremProducer::processExtract(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processIntEq(), CVC3::TheoryArith3::processIntEq(), processNode(), CVC3::TheoryCore::processNotify(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::SearchImplBase::processResult(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::Translator::processType(), CVC3::TheoryCore::processUpdates(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArith3::projectInequalities(), CVC3::SearchEngineFast::propagate(), MiniSat::Solver::propagate(), CVC3::Circuit::propagate(), CVC3::TheoryArithNew::propagateTheory(), CVC3::TheoryArray::pullIndex(), MiniSat::Solver::push(), CVC3::TheoryBitvector::pushNegation(), CVC3::ExprTransform::pushNegation1(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::VCL::ratExpr(), CVC3::ratRoot(), CVC3::ExprManager::rebuild(), CVC3::ExprManager::rebuildRec(), CVC3::CompleteInstPreProcessor::recInstMacros(), CVC3::TheoryQuant::recMultMatch(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryQuant::recMultMatchOldWay(), CVC3::VCL::recordExpr(), CVC3::SearchSat::recordNewRootLit(), CVC3::VCL::recordType(), CVC3::CompleteInstPreProcessor::recRewriteNot(), recursiveExprScore(), CVC3::TheoryArithOld::refineCounterExample(), CVC3::TheoryArithNew::refineCounterExample(), CVC3::TheoryArith3::refineCounterExample(), CVC3::TheoryCore::registerAtom(), SAT::CNF_Manager::registerAtom(), 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::Solver::removeWatch(), CVC3::Theory::renameExpr(), SAT::CNF_Manager::replaceITErec(), CVC3::VCCmd::reportResult(), CVC3::VCL::reprocessFlags(), 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::TheoryArith3::rewrite(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryCore::rewriteCore(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CommonTheoremProducer::rewriteIteFalse(), CVC3::CommonTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CommonTheoremProducer::rewriteIteTrue(), CVC3::ArithTheoremProducerOld::rewriteLeavesConst(), CVC3::ArithProofRules::rewriteLeavesConst(), CVC3::TheoryCore::rewriteLitCore(), CVC3::TheoryCore::rewriteLiteral(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteReadWrite2(), 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(), SATDecisionHook(), SAT::SatProofNode::SatProofNode(), MiniSat::Solver::search(), SAT::DPLLTMiniSat::search(), CVC3::TheoryArithOld::separateMonomial(), CVC3::TheoryArithNew::separateMonomial(), CVC3::TheoryArith3::separateMonomial(), CVC3::SmartCDO< Unsigned >::set(), MiniSat::Clause::setActivity(), CVC3::Variable::setAssumpThm(), MiniSat::Heap< VarOrder_lt >::setBounds(), CVC3::Expr::setComputeTransClosure(), CVC3::Expr::setContainsBoundVar(), CVC3::Expr::setEqNext(), CVC3::Expr::setFind(), CVC3::TheoryCore::setFindLiteral(), CVC3::Expr::setFinite(), CVC3::Expr::setFlag(), CVC3::Expr::setImpliedLiteral(), CVC3::TheoryCore::setInconsistent(), CVC3::Expr::setIntAssumption(), CVC3::Expr::setInUserAssumption(), CVC3::Expr::setIsAtomicFlag(), CVC3::Expr::setJustified(), CVC3::Expr::setMultiTrigger(), CVC3::Expr::setNotArrayNormalized(), MiniSat::Solver::setPushID(), 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::setTerminalsConstFlag(), CVC3::Expr::setTranslated(), CVC3::Expr::setTrigger(), CVC3::ExprValue::setTriggers(), CVC3::Expr::setTriggers(), CVC3::Expr::setType(), CVC3::TheoryArray::setup(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArithNew::setup(), CVC3::TheoryArith3::setup(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryQuant::setupTriggers(), CVC3::Expr::setUserAssumption(), CVC3::Expr::setUserRegisteredAtom(), CVC3::Expr::setUsesCC(), CVC3::Expr::setValidType(), CVC3::VariableValue::setValue(), CVC3::Variable::setValue(), CVC3::SearchSat::setValue(), CVC3::Expr::setWellFounded(), MiniSat::vec< int >::shrink(), CVC3::ArithTheoremProducer3::simpleIneqInt(), CVC3::ArithTheoremProducer::simpleIneqInt(), CVC3::ArithTheoremProducerOld::simplifiedMultExpr(), CVC3::ArithTheoremProducer3::simplifiedMultExpr(), CVC3::ArithTheoremProducer::simplifiedMultExpr(), CVC3::TheoryCore::simplify(), MiniSat::Solver::simplifyDB(), CVC3::CompleteInstPreProcessor::simplifyEq(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::ExprTransform::simplifyWithCare(), CVC3::ExprTransform::smartSimplify(), CVC3::TheoryDatatype::solve(), CVC3::TheoryCore::solve(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArray::solve(), CVC3::TheoryArithOld::solve(), CVC3::TheoryArithNew::solve(), CVC3::TheoryArith3::solve(), CVC3::TheoryArithOld::solvedForm(), CVC3::TheoryArithNew::solvedForm(), CVC3::TheoryArith3::solvedForm(), CVC3::sort2(), CVC3::SearchEngineFast::split(), CVC3::ArithTheoremProducer3::splitGrayShadowSmall(), CVC3::ArithTheoremProducer::splitGrayShadowSmall(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArith3::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::Expr::substExpr(), CVC3::Expr::substExprQuant(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CompleteInstPreProcessor::substMacro(), CVC3::ArithTheoremProducerOld::sumModM(), CVC3::ArithTheoremProducer3::sumModM(), CVC3::ArithTheoremProducer::sumModM(), CVC3::ArithTheoremProducerOld::sumMulF(), CVC3::ArithTheoremProducer3::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::Expr::typeCard(), CVC3::Expr::typeEnumerateFinite(), CVC3::Expr::typeSizeFinite(), CVC3::SearchEngineFast::unitPropagation(), CVC3::Theory::unregisterKinds(), CVC3::Theory::unregisterTheory(), CVC3::TheoryRecords::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryCore::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryArith3::update(), CVC3::ContextObj::update(), CVC3::CDFlags::update(), MiniSat::Solver::updateConflict(), CVC3::SearchEngineFast::updateLitCounts(), CVC3::SearchEngineFast::updateLitScores(), CVC3::TheoryArithOld::updateSubsumptionDB(), CVC3::TheoryArith3::updateSubsumptionDB(), CVC3::VCL::value(), CVC3::CommonTheoremProducer::varIntroSkolem(), SAT::DPLLTBasic::verify_solution(), CVC3::Clause::wp(), MiniSat::xmalloc(), and MiniSat::xrealloc().
| #define TRACE_MSG | ( | flag, | |
| msg | |||
| ) |
Definition at line 414 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::VCL::destroy(), 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::TheoryArith3::projectInequalities(), CVC3::SearchEngineFast::propagate(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), CVC3::SearchEngineFast::setInconsistent(), CVC3::TheoryArithOld::solvedForm(), CVC3::TheoryArithNew::solvedForm(), CVC3::TheoryArith3::solvedForm(), CVC3::SearchEngineFast::split(), CVC3::SearchEngineFast::traceConflict(), CVC3::SearchEngineFast::updateLitCounts(), CVC3::ClauseValue::~ClauseValue(), CVC3::ExprManager::~ExprManager(), and CVC3::VCL::~VCL().
1.7.3