TheoryCore Namespace Reference

Classes

• class CoreSatAPI

  Interface class for callbacks to SAT from Core. More...
  

Functions

• CoreProofRules * createProofRules (TheoremManager *tm)
• ~TheoryCore ()
• void assertFact (const Theorem &e)
• void checkSat (bool fullEffort)
• Theorem rewriteLitCore (const Expr &e)
• Theorem rewriteN (const Expr &e, int n)
• Theorem rewrite (const Expr &e)
• Theorem simplifyOp (const Expr &e)
• void setup (const Expr &e)
• void update (const Theorem &e, const Expr &d)
• void processUpdates ()
• Expr computeTypePred (const Type &t, const Expr &e)
• void checkType (const Expr &e)
• void computeType (const Expr &e)
• Type computeBaseType (const Type &tp)
• Expr computeTCC (const Expr &e)
• ExprStream & print (ExprStream &os, const Expr &e)
• Expr parseExpr (const Expr &e)
• Expr processCond (const Expr &e, int i)

  An auxiliary recursive function to process COND expressions into ITE.
  

• Expr parseExprOp (const Expr &e)
• void processFactQueue ()
• void setInconsistent (const Theorem &e)
• void enqueueFact (const Theorem &e)
• void addFact (const Theorem &e)
• void assertFactCore (const Theorem &e)
• void assertEqualities (const Theorem &e)
• void assertFormula (const Theorem &thm)
• void setupTerm (const Expr &t, Theory *i)
• Theorem rewriteCore (const Expr &e)
• bool checkSATCore ()
• void addToVarDB (const Expr &e)
• void refineCounterExample ()
• void computeModelBasic (const vector< Expr > &v)
• void collectBasicVars ()
• void buildModel (ExprMap< Expr > &m)
• void collectModelValues (const Expr &e, ExprMap< Expr > &m)
• void enqueueEquality (const Theorem &e)
• bool processEquality (const Theorem &thm, ExprMap< Theorem > &q)
• void processNotify (const Theorem &e, NotifyList *L)
• void setIncomplete (const string &reason)
• void setResourceLimit (unsigned limit)
• Theorem simplify (const Expr &e, bool forceRebuild)
• Theorem simplifyRec (const Expr &e)
• Theorem simplifyFullRec (const Expr &e)
• Theorem simplifyInPlaceRec (const Expr &e)
• bool incomplete (vector< string > &reasons)
• Theorem rewriteCore (const Theorem &e)
• Theorem rewriteLiteral (const Expr &e)
• Theorem solve (const Theorem &eThm)
• Theorem typePred (const Expr &e)
• Theorem subtypePredicate (const Expr &e)
• Theorem rewriteIte (const Expr &e)
• void setupSubFormulas (const Expr &s, const Expr &e)
• void registerAtom (const Expr &e)
• Theorem getImpliedLiteral (void)
• Theorem getImpliedLiteralByIndex (unsigned index)
• void assignValue (const Expr &t, const Expr &val)
• void assignValue (const Theorem &thm)
• bool getResource ()
• Theorem3 queryTCC (const Theorem &phi, const Theorem &D_phi)
• Theorem3 implIntro3 (const Theorem3 &phi, const std::vector< Expr > &assump, const std::vector< Theorem > &tccs)

---

Function Documentation

CoreProofRules* TheoryCore::createProofRules (  TheoremManager *  tm  )

Definition at line 53 of file core_theorem_producer.cpp. Referenced by d_coreSatAPI().

TheoryCore::~TheoryCore (   )

Definition at line 329 of file theory_core.cpp. References CVCL::Theory::d_em, CVCL::TheoryCore::d_exprTrans, CVCL::TheoryCore::d_printer, CVCL::TheoryCore::d_rules, CVCL::TheoryCore::d_typeComputer, and CVCL::ExprManager::unregisterPrettyPrinter().

void TheoryCore::assertFact (  const Theorem &  e  )

Definition at line 343 of file theory_core.cpp. References CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::SKOLEM_VAR, CVCL::Theorem::toString(), CVCL::UCONST, and CVCL::Expr::unnegate().

void TheoryCore::checkSat (  bool  fullEffort  )

Definition at line 350 of file theory_core.cpp. References CVCL::CDList< T >::begin(), CVCL::Debug::counter(), CVCL::Theory::d_commonRules, CVCL::TheoryCore::d_diseq, CVCL::debugger, CVCL::CDList< T >::end(), CVCL::Theory::find(), CVCL::Theorem::getRHS(), CVCL::TheoryCore::IF_DEBUG(), CVCL::Theory::iffMP(), CVCL::CommonProofRules::notToIff(), CVCL::TheoryCore::setInconsistent(), CVCL::Theory::symmetryRule(), and CVCL::Theory::transitivityRule().

Theorem TheoryCore::rewriteLitCore (  const Expr &  e  )

Definition at line 367 of file theory_core.cpp. References CVCL::Theory::d_commonRules, CVCL::EQ, CVCL::Expr::getKind(), CVCL::NOT, CVCL::Theory::reflexivityRule(), CVCL::CommonProofRules::rewriteNotFalse(), CVCL::CommonProofRules::rewriteNotNot(), CVCL::CommonProofRules::rewriteNotTrue(), CVCL::CommonProofRules::rewriteReflexivity(), and CVCL::CommonProofRules::rewriteUsingSymmetry().

Theorem TheoryCore::rewriteN (  const Expr &  e, int  n )

Definition at line 395 of file theory_core.cpp. References CVCL::Expr::arity(), CVCL::Theorem::getRHS(), CVCL::Theory::reflexivityRule(), CVCL::TheoryCore::rewrite(), CVCL::TheoryCore::rewriteN(), CVCL::Theory::substitutivityRule(), CVCL::Theory::theoryOf(), and CVCL::Theory::transitivityRule().

Theorem TheoryCore::rewrite (  const Expr &  e  )

Definition at line 419 of file theory_core.cpp. References CVCL::AND, CVCL::AND_R, CVCL::CoreProofRules::andDistributivityRule(), CVCL::Expr::andExpr(), CVCL::andExpr(), CVCL::Expr::arity(), b, CVCL::Expr::begin(), CVCL::BOUND_VAR, CVCL::CONSTDEF, CVCL::Theory::d_commonRules, CVCL::Theory::d_em, CVCL::TheoryCore::d_rules, CVCL::Expr::end(), CVCL::EQ, CVCL::EXISTS, CVCL::FALSE, CVCL::ExprManager::falseExpr(), CVCL::Theory::find(), CVCL::FORALL, CVCL::Theorem::getExpr(), CVCL::TheoryCore::getFlags(), CVCL::Expr::getKids(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Expr::getOp(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::IFF, CVCL::IFF_R, CVCL::CoreProofRules::iffAndDistrib(), CVCL::Expr::iffExpr(), CVCL::CoreProofRules::iffOrDistrib(), CVCL::IMPLIES, CVCL::int2string(), CVCL::Expr::isAnd(), CVCL::Expr::isIff(), CVCL::Expr::isNot(), CVCL::Expr::isOr(), CVCL::ITE, CVCL::ITE_R, CVCL::LETDECL, CVCL::NOT, CVCL::NULL_KIND, CVCL::OR, CVCL::CoreProofRules::orDistributivityRule(), CVCL::Expr::orExpr(), CVCL::orExpr(), CVCL::RAW_LIST, CVCL::CommonProofRules::reflexivityRule(), CVCL::Theory::reflexivityRule(), CVCL::TheoryCore::rewrite(), CVCL::Theory::rewriteAnd(), CVCL::CoreProofRules::rewriteAndSubterms(), CVCL::CoreProofRules::rewriteConstDef(), CVCL::TheoryCore::rewriteCore(), CVCL::CommonProofRules::rewriteIff(), CVCL::CoreProofRules::rewriteImplies(), CVCL::CoreProofRules::rewriteIteCond(), CVCL::CoreProofRules::rewriteIteFalse(), CVCL::CoreProofRules::rewriteIteSame(), CVCL::CoreProofRules::rewriteIteToAnd(), CVCL::CoreProofRules::rewriteIteToIff(), CVCL::CoreProofRules::rewriteIteToImp(), CVCL::CoreProofRules::rewriteIteToNot(), CVCL::CoreProofRules::rewriteIteToOr(), CVCL::CoreProofRules::rewriteIteTrue(), CVCL::CoreProofRules::rewriteLetDecl(), CVCL::TheoryCore::rewriteLitCore(), CVCL::TheoryCore::rewriteN(), CVCL::Theory::rewriteOr(), CVCL::CoreProofRules::rewriteOrSubterms(), CVCL::Expr::setRewriteNormal(), CVCL::TheoryCore::simplifyRec(), CVCL::SKOLEM_VAR, CVCL::Theory::substitutivityRule(), CVCL::Theory::symmetryRule(), CVCL::Theory::theoryOf(), CVCL::Type::toString(), CVCL::Expr::toString(), CVCL::TRACE, CVCL::Theory::transitivityRule(), CVCL::TRUE, CVCL::ExprManager::trueExpr(), and CVCL::UCONST. Referenced by CVCL::SearchImplBase::enqueueCNFrec().

Theorem TheoryCore::simplifyOp (  const Expr &  e  )

Definition at line 864 of file theory_core.cpp. References CVCL::AND, CVCL::Expr::arity(), CVCL::Debug::counter(), CVCL::TheoryCore::d_exprTrans, CVCL::TheoryCore::d_rules, CVCL::debugger, CVCL::FALSE, CVCL::Theorem::getExpr(), CVCL::TheoryCore::getFlags(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), CVCL::TheoryCore::IF_DEBUG(), CVCL::CoreProofRules::ifLiftUnaryRule(), CVCL::IMPLIES, CVCL::Expr::isFalse(), CVCL::Expr::isITE(), CVCL::Theorem::isNull(), CVCL::Expr::isTrue(), CVCL::ITE, CVCL::NOT, CVCL::OR, CVCL::ExprTransform::pushNegation1(), CVCL::Theory::reflexivityRule(), CVCL::Theory::rewriteAnd(), CVCL::CoreProofRules::rewriteImplies(), CVCL::CoreProofRules::rewriteIteSame(), CVCL::Theory::rewriteOr(), CVCL::TheoryCore::simplifyOp(), CVCL::TheoryCore::simplifyRec(), CVCL::Theory::substitutivityRule(), CVCL::Expr::toString(), CVCL::TRACE, CVCL::Theory::transitivityRule(), and CVCL::TRUE.

void TheoryCore::setup (  const Expr &  e  )

Only Boolean constants (TRUE and FALSE) and variables of uninterpreted types should appear here (they come from records and tuples). Just ignore them. Definition at line 1003 of file theory_core.cpp.

void TheoryCore::update (  const Theorem &  e, const Expr &  d )

We use the update method of theory core to track registered atomic formulas. Updates are recorded and then processed by calling processUpdates once all equalities have been processed. Definition at line 1009 of file theory_core.cpp. References CVCL::TheoryCore::d_update_data, and CVCL::TheoryCore::d_update_thms.

void TheoryCore::processUpdates (   )

Definition at line 1015 of file theory_core.cpp. References CVCL::Expr::addToNotify(), CVCL::Theory::d_commonRules, CVCL::TheoryCore::d_impliedLiterals, CVCL::TheoryCore::d_update_data, CVCL::TheoryCore::d_update_thms, CVCL::Theory::find(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::CommonProofRules::iffFalseElim(), CVCL::CommonProofRules::iffTrueElim(), CVCL::Expr::isAbsAtomicFormula(), CVCL::Type::isBool(), CVCL::Expr::isFalse(), CVCL::Expr::isImpliedLiteral(), CVCL::Theorem::isRewrite(), CVCL::Expr::isTrue(), CVCL::CDList< T >::push_back(), CVCL::Expr::setImpliedLiteral(), and CVCL::TheoryCore::simplify().

Expr TheoryCore::computeTypePred (  const Type &  t, const Expr &  e )

Definition at line 1050 of file theory_core.cpp. References CVCL::APPLY, CVCL::Theory::computeTypePred(), CVCL::CONSTDEF, CVCL::Expr::getEM(), CVCL::Type::getExpr(), CVCL::Expr::getKind(), CVCL::Theory::getTypePred(), CVCL::Expr::lookupType(), CVCL::Expr::mkOp(), CVCL::SUBTYPE, CVCL::Theory::theoryOf(), and CVCL::ExprManager::trueExpr().

void TheoryCore::checkType (  const Expr &  e  )

Definition at line 1072 of file theory_core.cpp. References CVCL::Expr::arity(), CVCL::BOOLEAN, CVCL::Theory::getEM(), CVCL::Expr::getKind(), CVCL::Expr::getType(), CVCL::Type::isFunction(), CVCL::SUBTYPE, and CVCL::Expr::toString().

void TheoryCore::computeType (  const Expr &  e  )

Definition at line 1101 of file theory_core.cpp. References CVCL::AND, CVCL::AND_R, CVCL::Expr::arity(), CVCL::Theory::boolType(), CVCL::CONSTDEF, CVCL::EQ, CVCL::Theory::getBaseType(), CVCL::Expr::getKind(), CVCL::Expr::getType(), CVCL::TheoryCore::IF_DEBUG(), CVCL::IFF, CVCL::IFF_R, CVCL::IMPLIES, CVCL::Type::isBool(), CVCL::ITE, CVCL::ITE_R, CVCL::LETDECL, CVCL::NOT, CVCL::OR, CVCL::Expr::setType(), CVCL::Expr::toString(), CVCL::Type::toString(), CVCL::TRACE, and CVCL::XOR.

Type TheoryCore::computeBaseType (  const Type &  tp  )

Definition at line 1193 of file theory_core.cpp. References CVCL::Expr::arity(), CVCL::BOOLEAN, CVCL::Theory::getBaseType(), CVCL::Type::getExpr(), CVCL::Expr::getKind(), CVCL::Expr::getType(), CVCL::Type::isFunction(), CVCL::SUBTYPE, CVCL::Type::toString(), CVCL::Expr::toString(), and CVCL::TYPEDEF.

Expr TheoryCore::computeTCC (  const Expr &  e  )

Definition at line 1221 of file theory_core.cpp. References CVCL::AND, CVCL::andExpr(), CVCL::APPLY, CVCL::Expr::begin(), CVCL::Theory::computeTCC(), CVCL::Expr::end(), CVCL::Expr::getKind(), CVCL::Theorem::getRHS(), CVCL::Theory::getTCC(), CVCL::IMPLIES, CVCL::ITE, CVCL::NOT, CVCL::OR, CVCL::orExpr(), CVCL::Theory::rewriteAnd(), CVCL::Theory::rewriteOr(), and CVCL::Theory::theoryOf().

ExprStream& TheoryCore::print (  ExprStream &  os, const Expr &  e )

Definition at line 1278 of file theory_core.cpp. References CVCL::AND, CVCL::Expr::arity(), CVCL::ARROW, CVCL::ASSERT, CVCL::ASSERTIONS, CVCL::ASSUMPTIONS, CVCL::ExprHashMap< Data >::begin(), CVCL::BOOLEAN, CVCL::BOUND_VAR, CVCL::CONST, CVCL::CONSTDEF, CVCL::COUNTEREXAMPLE, CVCL::COUNTERMODEL, std::endl(), CVCL::EQ, CVCL::FALSE, CVCL::Theory::getEM(), CVCL::Type::getExpr(), CVCL::Expr::getKind(), CVCL::Expr::getString(), CVCL::Expr::getType(), CVCL::ID, CVCL::IFF, CVCL::IMPLIES, CVCL::int2string(), CVCL::Type::isBool(), CVCL::Type::isNull(), CVCL::Expr::isString(), CVCL::ITE, CVCL::ExprStream::lang(), CVCL::LET, CVCL::LETDECL, CVCL::LISP_LANG, CVCL::nodag(), CVCL::NOT, CVCL::OR, CVCL::PF_APPLY, CVCL::PF_HOLE, CVCL::POP, CVCL::pop(), CVCL::POP_SCOPE, CVCL::popSave(), CVCL::POPTO, CVCL::POPTO_SCOPE, CVCL::PRESENTATION_LANG, CVCL::Expr::print(), CVCL::Expr::printAST(), CVCL::PUSH, CVCL::push(), CVCL::PUSH_SCOPE, CVCL::pushRestore(), CVCL::QUERY, CVCL::RAW_LIST, CVCL::SKOLEM_VAR, CVCL::SMTLIB_LANG, CVCL::space(), CVCL::STRING_EXPR, CVCL::SUBTYPE, CVCL::TRANSFORM, CVCL::TRUE, CVCL::TYPE, CVCL::TYPEDEF, CVCL::UCONST, CVCL::WHERE, and CVCL::XOR.

Expr TheoryCore::parseExpr (  const Expr &  e  )

Definition at line 1838 of file theory_core.cpp. References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::TheoryCore::d_boundVarStack, CVCL::Expr::end(), CVCL::Theory::getEM(), CVCL::ExprManager::getKind(), CVCL::Expr::getKind(), CVCL::Theory::getName(), CVCL::Expr::getString(), CVCL::Theory::hasTheory(), CVCL::ID, CVCL::Expr::isApply(), CVCL::Expr::isNull(), CVCL::LAMBDA, CVCL::Expr::mkOp(), CVCL::NULL_KIND, CVCL::TheoryCore::parseExpr(), CVCL::Theory::parseExprOp(), CVCL::RAW_LIST, CVCL::Theory::resolveID(), CVCL::Theory::theoryOf(), CVCL::Expr::toString(), and CVCL::TRACE.

Expr TheoryCore::processCond (  const Expr &  e, int  i )

An auxiliary recursive function to process COND expressions into ITE. Definition at line 1932 of file theory_core.cpp. References CVCL::Expr::arity(), CVCL::Expr::getKind(), CVCL::Expr::getString(), CVCL::ID, CVCL::int2string(), CVCL::Expr::iteExpr(), CVCL::TheoryCore::parseExpr(), CVCL::TheoryCore::processCond(), CVCL::RAW_LIST, and CVCL::Expr::toString().

Expr TheoryCore::parseExprOp (  const Expr &  e  )

Definition at line 1961 of file theory_core.cpp. References CVCL::Theory::addBoundVar(), CVCL::AND, CVCL::Expr::arity(), CVCL::ASSERT, CVCL::ASSERTIONS, CVCL::ASSUMPTIONS, CVCL::Expr::begin(), CVCL::BOOLEAN, CVCL::ExprManager::boolExpr(), CVCL::CALL, CVCL::CHECK_TYPE, CVCL::CHECKSAT, CVCL::COND, CVCL::CONST, CVCL::CONSTDEF, CVCL::CONTEXT, CVCL::CONTINUE, CVCL::COUNTEREXAMPLE, CVCL::COUNTERMODEL, CVCL::DBG, CVCL::DUMP_ASSUMPTIONS, CVCL::DUMP_CLOSURE, CVCL::DUMP_CLOSURE_PROOF, CVCL::DUMP_PROOF, CVCL::DUMP_SIG, CVCL::DUMP_TCC, CVCL::DUMP_TCC_ASSUMPTIONS, CVCL::DUMP_TCC_PROOF, CVCL::ECHO, CVCL::ELSE, CVCL::Expr::end(), CVCL::EQ, CVCL::Expr::eqExpr(), CVCL::FALSE, CVCL::ExprManager::falseExpr(), CVCL::FORGET, CVCL::GET_CHILD, CVCL::GET_TYPE, CVCL::Expr::getEM(), CVCL::Theory::getEM(), CVCL::ExprManager::getKind(), CVCL::Expr::getKind(), CVCL::Expr::getString(), CVCL::HELP, CVCL::ID, CVCL::IF, CVCL::IFF, CVCL::IMPLIES, CVCL::Expr::iteExpr(), CVCL::LET, CVCL::LETDECL, CVCL::LETDECLS, CVCL::NEQ, CVCL::ExprManager::newLeafExpr(), CVCL::NOT, CVCL::NULL_KIND, CVCL::OPTION, CVCL::OR, CVCL::TheoryCore::parseExpr(), CVCL::POP, CVCL::POP_SCOPE, CVCL::POPTO, CVCL::POPTO_SCOPE, CVCL::PRINT, CVCL::TheoryCore::processCond(), CVCL::PUSH, CVCL::PUSH_SCOPE, CVCL::QUERY, CVCL::RAW_LIST, CVCL::RESTART, CVCL::SEQ, CVCL::SUBSTITUTE, CVCL::SUBTYPE, CVCL::Expr::toString(), CVCL::TRACE, CVCL::TRANSFORM, CVCL::TRUE, CVCL::ExprManager::trueExpr(), CVCL::TYPE, CVCL::TYPEDECL, CVCL::TYPEDEF, CVCL::UNTRACE, CVCL::VARDECL, CVCL::VARDECLS, CVCL::VARLIST, CVCL::WHERE, and CVCL::XOR.

void TheoryCore::processFactQueue (   )

Definition at line 2171 of file theory_core.cpp. References CVCL::TheoryCore::CoreSatAPI::addLemma(), CVCL::TheoryCore::assertFactCore(), CVCL::Debug::counter(), CVCL::TheoryCore::d_coreSatAPI, CVCL::TheoryCore::d_inconsistent, CVCL::TheoryCore::d_queue, CVCL::TheoryCore::d_queueSE, CVCL::TheoryCore::d_theories, CVCL::debugger, CVCL::Theory::getName(), CVCL::Theory::getNumTheories(), CVCL::TheoryCore::IF_DEBUG(), and CVCL::TRACE.

void TheoryCore::setInconsistent (  const Theorem &  e  )

Definition at line 2228 of file theory_core.cpp. References CVCL::TheoryCore::d_inconsistent, CVCL::TheoryCore::d_incThm, CVCL::TheoryCore::d_queueSE, CVCL::TheoryCore::d_theories, CVCL::Theory::getName(), CVCL::Theory::getNumTheories(), and CVCL::TRACE.

void TheoryCore::enqueueFact (  const Theorem &  e  )

Definition at line 2242 of file theory_core.cpp. References CVCL::Debug::counter(), CVCL::TheoryCore::d_cm, d_dumpTrace(), d_inAddFact(), d_inCheckSATCore(), d_inRegisterAtom(), CVCL::TheoryCore::d_queue, CVCL::debugger, CVCL::Theorem::getExpr(), CVCL::TheoryCore::getResource(), CVCL::Theorem::getScope(), CVCL::TheoryCore::IF_DEBUG(), CVCL::TheoryCore::inconsistent(), CVCL::int2string(), CVCL::Expr::isFalse(), CVCL::Theorem::isRewrite(), CVCL::ContextManager::scopeLevel(), CVCL::TheoryCore::setIncomplete(), CVCL::TheoryCore::setInconsistent(), CVCL::Expr::toString(), and CVCL::TRACE.

void TheoryCore::addFact (  const Theorem &  e  )

Definition at line 2275 of file theory_core.cpp. References d_dumpTrace(), d_inAddFact(), CVCL::TheoryCore::d_inconsistent, CVCL::TheoryCore::d_queue, CVCL::TheoryCore::d_queueSE, CVCL::TheoryCore::d_update_data, CVCL::TheoryCore::d_update_thms, CVCL::TheoryCore::enqueueFact(), CVCL::Theorem::getExpr(), CVCL::TheoryCore::IF_DEBUG(), CVCL::TheoryCore::processFactQueue(), and CVCL::TRACE.

void TheoryCore::assertFactCore (  const Theorem &  e  )

Definition at line 2297 of file theory_core.cpp. References CVCL::CommonProofRules::andElim(), CVCL::Expr::arity(), CVCL::TheoryCore::assertEqualities(), CVCL::TheoryCore::assertFactCore(), CVCL::TheoryCore::assertFormula(), CVCL::Debug::counter(), CVCL::Theory::d_commonRules, CVCL::debugger, CVCL::TheoryCore::enqueueFact(), CVCL::TheoryCore::enqueueSE(), CVCL::Theorem::getExpr(), CVCL::Expr::hasFind(), CVCL::TheoryCore::IF_DEBUG(), CVCL::Theory::iffMP(), CVCL::Expr::isAbsLiteral(), CVCL::Expr::isAnd(), CVCL::Expr::isEq(), CVCL::Expr::isExists(), CVCL::Expr::isFalse(), CVCL::Expr::isNot(), CVCL::Expr::isTrue(), CVCL::TheoryCore::processUpdates(), CVCL::TheoryCore::setInconsistent(), CVCL::TheoryCore::simplify(), CVCL::CommonProofRules::skolemize(), CVCL::TheoryCore::solve(), CVCL::Expr::toString(), and CVCL::TRACE.

void TheoryCore::assertEqualities (  const Theorem &  e  )

Invariants: The input theorem e is either an equality or a conjunction of equalities; In each equality e1=e2, the RHS e2 i-leaf-simplified; At the time of calling update(), all equalities in the queue are processed by assertFormula() and the equivalence classes are merged in the union-find database. In other words, the entire equality queue is processed "in parallel". Definition at line 2368 of file theory_core.cpp. References CVCL::TheoryCore::assertFormula(), CVCL::ExprMap< Data >::begin(), CVCL::Theory::d_em, CVCL::TheoryCore::d_equalityQueue, CVCL::ExprMap< Data >::end(), CVCL::TheoryCore::enqueueEquality(), CVCL::Theory::find(), CVCL::Theorem::getExpr(), CVCL::Theorem::getLHS(), CVCL::Expr::getNotify(), CVCL::Theorem::getRHS(), CVCL::ExprManager::invalidateSimpCache(), CVCL::Theorem::isRewrite(), CVCL::Expr::isTerm(), CVCL::TheoryCore::processEquality(), CVCL::TheoryCore::processNotify(), CVCL::TheoryCore::processUpdates(), CVCL::Expr::setFind(), CVCL::Expr::toString(), and CVCL::TRACE.

void TheoryCore::assertFormula (  const Theorem &  thm  )

Definition at line 2432 of file theory_core.cpp. References CVCL::Theory::assertFact(), CVCL::CommonProofRules::contradictionRule(), CVCL::Debug::counter(), CVCL::Theory::d_commonRules, CVCL::TheoryCore::d_diseq, CVCL::Theory::d_em, CVCL::debugger, CVCL::TheoryCore::enqueueFact(), CVCL::TheoryCore::enqueueSE(), CVCL::Expr::eqExpr(), CVCL::Theory::find(), CVCL::Theory::getBaseType(), CVCL::Theorem::getExpr(), CVCL::Theory::getName(), CVCL::Expr::getNotify(), CVCL::Expr::hasFind(), CVCL::TheoryCore::IF_DEBUG(), CVCL::CommonProofRules::iffFalseElim(), CVCL::CommonProofRules::iffTrue(), CVCL::ExprManager::invalidateSimpCache(), CVCL::Expr::isAbsLiteral(), CVCL::Expr::isEq(), CVCL::Expr::isExists(), CVCL::Expr::isFalse(), CVCL::Expr::isNot(), CVCL::CommonProofRules::notToIff(), CVCL::TheoryCore::processNotify(), CVCL::CDList< T >::push_back(), CVCL::CommonProofRules::rewriteUsingSymmetry(), CVCL::Expr::setFind(), CVCL::TheoryCore::setInconsistent(), CVCL::TheoryCore::setupTerm(), CVCL::CommonProofRules::skolemize(), CVCL::Theory::symmetryRule(), CVCL::Theory::theoryOf(), CVCL::Theorem::toString(), CVCL::TRACE, and CVCL::Theory::transitivityRule().

void TheoryCore::setupTerm (  const Expr &  t, Theory *  i )

Definition at line 2557 of file theory_core.cpp. References CVCL::Theory::addSharedTerm(), CVCL::Expr::arity(), CVCL::Theory::assertTypePred(), CVCL::Debug::counter(), CVCL::Theory::d_commonRules, CVCL::TheoryCore::d_rules, CVCL::TheoryCore::d_sharedTerms, CVCL::TheoryCore::d_terms, CVCL::TheoryCore::d_typePredAsserted, CVCL::debugger, CVCL::Type::getExpr(), CVCL::Theorem::getExpr(), CVCL::Theory::getName(), CVCL::Expr::getType(), CVCL::Expr::hasFind(), CVCL::TheoryCore::IF_DEBUG(), CVCL::CDMap< Key, Data, HashFcn >::insert(), CVCL::Expr::isAbsLiteral(), CVCL::Expr::isFalse(), CVCL::Expr::isTerm(), CVCL::Expr::isTrue(), CVCL::CDList< T >::push_back(), CVCL::CommonProofRules::reflexivityRule(), CVCL::Expr::setFind(), CVCL::TheoryCore::setInconsistent(), CVCL::Theory::setup(), CVCL::TheoryCore::setupTerm(), CVCL::Theory::theoryOf(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::CoreProofRules::typePred().

Theorem TheoryCore::rewriteCore (  const Expr &  e  )

Definition at line 2633 of file theory_core.cpp. References checkRewriteType(), CVCL::Expr::clearRewriteNormal(), CVCL::Theory::find(), CVCL::Theory::getName(), CVCL::Theorem::getRHS(), CVCL::Expr::hasFind(), CVCL::TheoryCore::IF_DEBUG(), CVCL::Expr::isEq(), CVCL::Expr::isNot(), CVCL::Expr::isRewriteNormal(), CVCL::Theory::reflexivityRule(), CVCL::Theory::rewrite(), CVCL::TheoryCore::rewriteCore(), CVCL::TheoryCore::rewriteLitCore(), CVCL::Expr::setRewriteNormal(), CVCL::Theory::theoryOf(), CVCL::Expr::toString(), and CVCL::TRACE.

bool TheoryCore::checkSATCore (   )

Definition at line 2690 of file theory_core.cpp. References CVCL::Debug::counter(), d_inCheckSATCore(), CVCL::TheoryCore::d_inconsistent, CVCL::TheoryCore::d_queue, CVCL::TheoryCore::d_queueSE, CVCL::TheoryCore::d_theories, CVCL::debugger, CVCL::Theory::getName(), CVCL::Theory::getNumTheories(), CVCL::TheoryCore::IF_DEBUG(), CVCL::TheoryCore::processFactQueue(), and CVCL::TRACE.

void TheoryCore::addToVarDB (  const Expr &  e  )

Definition at line 2725 of file theory_core.cpp. References CVCL::TheoryCore::d_vars, CVCL::CDList< T >::push_back(), and CVCL::TRACE.

void TheoryCore::refineCounterExample (   )

Definition at line 2732 of file theory_core.cpp. References CVCL::Theory::d_em, CVCL::TheoryCore::d_theories, CVCL::Theorem::getLeafAssumptions(), CVCL::Theory::getName(), CVCL::Theory::getNumTheories(), CVCL::TheoryCore::inconsistent(), CVCL::TheoryCore::inconsistentThm(), CVCL::RAW_LIST, and CVCL::Expr::toString().

void TheoryCore::computeModelBasic (  const vector< Expr > &  v  )

Definition at line 2752 of file theory_core.cpp. References CVCL::TheoryCore::assignValue(), CVCL::ExprHashMap< Data >::begin(), CVCL::Theory::d_em, CVCL::Theory::find(), CVCL::Theorem::getRHS(), CVCL::Expr::isBoolConst(), CVCL::TRACE, and CVCL::ExprManager::trueExpr().

void TheoryCore::collectBasicVars (   )

Definition at line 2764 of file theory_core.cpp. References CVCL::Theory::addSharedTerm(), CVCL::CDList< T >::begin(), CVCL::ExprHashMap< Data >::clear(), CVCL::ExprHashMap< Data >::count(), CVCL::TheoryCore::d_basicModelVars, CVCL::TheoryCore::d_sharedTerms, CVCL::TheoryCore::d_simplifiedModelVars, CVCL::TheoryCore::d_varAssignments, CVCL::TheoryCore::d_varModelMap, CVCL::TheoryCore::d_vars, CVCL::CDList< T >::end(), CVCL::Theory::find(), CVCL::Theory::getBaseType(), CVCL::Theory::getEM(), CVCL::Theorem::getExpr(), CVCL::Theory::getModelTerm(), CVCL::Theorem::getRHS(), CVCL::CDMap< Key, Data, HashFcn >::insert(), CVCL::Expr::isTerm(), CVCL::RAW_LIST, CVCL::ExprHashMap< Data >::size(), CVCL::Theory::theoryOf(), CVCL::Expr::toString(), and CVCL::TRACE.

void TheoryCore::buildModel (  ExprMap< Expr > &  m  )

Definition at line 2817 of file theory_core.cpp. References CVCL::TheoryCore::assignValue(), CVCL::CDList< T >::begin(), CVCL::TheoryCore::collectModelValues(), CVCL::ExprHashMap< Data >::count(), CVCL::TheoryCore::d_basicModelVars, CVCL::Theory::d_em, CVCL::TheoryCore::d_simplifiedModelVars, CVCL::TheoryCore::d_theories, CVCL::TheoryCore::d_varAssignments, CVCL::TheoryCore::d_vars, CVCL::CDList< T >::end(), CVCL::ExprHashMap< Data >::end(), CVCL::ExprHashMap< Data >::find(), CVCL::Theory::find(), CVCL::Theory::getBaseType(), CVCL::Theorem::getLeafAssumptions(), CVCL::Theorem::getLHS(), CVCL::Theory::getName(), CVCL::Theory::getNumTheories(), CVCL::Theorem::getRHS(), CVCL::TheoryCore::inconsistent(), CVCL::TheoryCore::inconsistentThm(), CVCL::ExprHashMap< Data >::insert(), CVCL::Theorem::isNull(), CVCL::RAW_LIST, CVCL::Theory::theoryOf(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::Theory::transitivityRule().

void TheoryCore::collectModelValues (  const Expr &  e, ExprMap< Expr > &  m )

Not all theories may implement aggregation of compound values. If a compound variable is not assigned by a theory, add the more primitive variable assignments to 'm'. Some variables may simplify to something else (simplifiedVars map). INVARIANT: e is always simplified (it's not in simplifiedVars map). Also, if v simplifies to e, and e is assigned, then v must be assigned. Definition at line 2908 of file theory_core.cpp. References CVCL::TheoryCore::assignValue(), CVCL::ExprHashMap< Data >::begin(), CVCL::TheoryCore::collectModelValues(), CVCL::Theory::computeModel(), CVCL::ExprHashMap< Data >::count(), CVCL::TheoryCore::d_simplifiedModelVars, CVCL::TheoryCore::d_varAssignments, CVCL::TheoryCore::d_varModelMap, CVCL::ExprHashMap< Data >::end(), CVCL::ExprHashMap< Data >::find(), CVCL::Theory::getBaseType(), CVCL::Theory::getEM(), CVCL::Theorem::getExpr(), CVCL::TheoryCore::getModelValue(), CVCL::Theory::getName(), CVCL::Theorem::getRHS(), CVCL::TheoryCore::IF_DEBUG(), CVCL::RAW_LIST, CVCL::Theory::reflexivityRule(), CVCL::Theory::theoryOf(), CVCL::TRACE, and CVCL::Theory::transitivityRule().

void TheoryCore::enqueueEquality (  const Theorem &  e  )

Definition at line 2982 of file theory_core.cpp. References CVCL::AND, CVCL::TheoryCore::d_cm, d_dumpTrace(), CVCL::TheoryCore::d_equalityQueue, CVCL::EQ, CVCL::EXISTS, CVCL::FALSE, CVCL::Theorem::getExpr(), CVCL::Theory::getName(), CVCL::Theorem::getScope(), CVCL::TheoryCore::IF_DEBUG(), CVCL::int2string(), CVCL::ContextManager::scopeLevel(), and CVCL::TRACE.

bool TheoryCore::processEquality (  const Theorem &  thm, ExprMap< Theorem > &  q )

Fill in the copy of the equality queue with single equalities by processing the input 'eq', which can be an equality, a conjunction of equalities, or an existential quantifier of the above. Definition at line 3007 of file theory_core.cpp. References CVCL::AND, CVCL::CommonProofRules::andElim(), CVCL::Expr::arity(), CVCL::CommonProofRules::contradictionRule(), CVCL::Debug::counter(), CVCL::Theory::d_commonRules, CVCL::debugger, CVCL::EQ, CVCL::EXISTS, CVCL::FALSE, CVCL::Theory::find(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getRHS(), CVCL::TheoryCore::IF_DEBUG(), CVCL::CommonProofRules::iffFalseElim(), CVCL::Expr::isFalse(), CVCL::TheoryCore::processEquality(), CVCL::TheoryCore::setInconsistent(), CVCL::CommonProofRules::skolemize(), CVCL::Theorem::toString(), CVCL::Expr::toString(), and CVCL::TRACE.

void TheoryCore::processNotify (  const Theorem &  e, NotifyList *  L )

Definition at line 3057 of file theory_core.cpp. References CVCL::NotifyList::getExpr(), CVCL::Theory::getName(), CVCL::NotifyList::getTheory(), CVCL::NotifyList::size(), CVCL::Theorem::toString(), CVCL::TRACE, and CVCL::Theory::update().

void TheoryCore::setIncomplete (  const string &  reason  )

Definition at line 3075 of file theory_core.cpp. References CVCL::TheoryCore::d_incomplete, and CVCL::CDMap< Key, Data, HashFcn >::insert().

void TheoryCore::setResourceLimit (  unsigned  limit  )

Definition at line 3081 of file theory_core.cpp. References CVCL::TheoryCore::d_resourceLimit.

Theorem TheoryCore::simplify (  const Expr &  e, bool  forceRebuild )

Definition at line 3088 of file theory_core.cpp. References CVCL::TheoryCore::d_currentRecursiveSimplifier, CVCL::Theory::d_em, d_inSimplify(), CVCL::TheoryCore::d_simplifyInPlace, CVCL::Theorem::getRHS(), CVCL::TheoryCore::IF_DEBUG(), CVCL::ExprManager::invalidateSimpCache(), CVCL::Expr::isAbsLiteral(), CVCL::Expr::setFind(), CVCL::TheoryCore::simplifyFullRec(), CVCL::TheoryCore::simplifyInPlaceRec(), CVCL::TheoryCore::simplifyRec(), and CVCL::TRACE.

Theorem TheoryCore::simplifyRec (  const Expr &  e  )

Definition at line 3123 of file theory_core.cpp. References CVCL::TheoryCore::d_currentRecursiveSimplifier.

Theorem TheoryCore::simplifyFullRec (  const Expr &  e  )

Definition at line 3130 of file theory_core.cpp. References CVCL::Expr::arity(), CVCL::Debug::counter(), CVCL::Theory::d_commonRules, CVCL::TheoryCore::d_simplifyInPlace, CVCL::debugger, CVCL::EQ, CVCL::Theory::find(), CVCL::Expr::getFind(), CVCL::TheoryCore::getFlags(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Theory::getName(), CVCL::Theorem::getRHS(), CVCL::Expr::getSimpCache(), CVCL::Expr::hasFind(), CVCL::TheoryCore::IF_DEBUG(), CVCL::IFF, CVCL::CommonProofRules::iffTrue(), CVCL::int2string(), CVCL::Expr::isAbsLiteral(), CVCL::Expr::isFalse(), CVCL::Expr::isTerm(), CVCL::Expr::isTrue(), CVCL::Theory::reflexivityRule(), CVCL::TheoryCore::rewriteCore(), CVCL::Expr::setFind(), CVCL::Expr::setSimpCache(), CVCL::Theory::simplifyOp(), CVCL::TheoryCore::simplifyRec(), CVCL::Theory::theoryOf(), CVCL::Expr::toString(), CVCL::TRACE, CVCL::Theory::transitivityRule(), and CVCL::Expr::validSimpCache().

Theorem TheoryCore::simplifyInPlaceRec (  const Expr &  e  )

Definition at line 3233 of file theory_core.cpp. References CVCL::AND, CVCL::Expr::arity(), CVCL::Theory::find(), CVCL::Expr::getFind(), CVCL::Expr::getKids(), CVCL::Expr::getKind(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), CVCL::Expr::getSimpCache(), CVCL::Expr::hasFind(), CVCL::Expr::isAbsLiteral(), CVCL::Expr::isAtomic(), CVCL::Expr::isBoolConst(), CVCL::Expr::isFalse(), CVCL::Expr::isTerm(), CVCL::Expr::isTrue(), CVCL::ITE, CVCL::OR, CVCL::Theory::reflexivityRule(), CVCL::TheoryCore::rewriteCore(), CVCL::Expr::setFind(), CVCL::Expr::setSimpCache(), CVCL::TheoryCore::simplifyInPlaceRec(), CVCL::TheoryCore::simplifyRec(), CVCL::Theory::substitutivityRule(), CVCL::TRACE, CVCL::Theory::transitivityRule(), and CVCL::Expr::validSimpCache().

bool TheoryCore::incomplete (  vector< string > &  reasons  )

Definition at line 3326 of file theory_core.cpp. References CVCL::CDMap< Key, Data, HashFcn >::begin(), CVCL::TheoryCore::d_incomplete, CVCL::CDMap< Key, Data, HashFcn >::end(), and CVCL::CDMap< Key, Data, HashFcn >::size().

Theorem TheoryCore::rewriteCore (  const Theorem &  e  )

Definition at line 3338 of file theory_core.cpp. References CVCL::Theorem::getRHS(), CVCL::Theorem::isRewrite(), CVCL::TheoryCore::rewriteCore(), CVCL::Theorem::toString(), and CVCL::Theory::transitivityRule().

Theorem TheoryCore::rewriteLiteral (  const Expr &  e  )

Definition at line 3345 of file theory_core.cpp. References CVCL::Expr::arity(), CVCL::Theory::d_commonRules, CVCL::Theory::getBaseType(), CVCL::Theory::getName(), CVCL::CommonProofRules::iffContrapositive(), CVCL::Expr::isAbsLiteral(), CVCL::Expr::isEq(), CVCL::Expr::isNot(), CVCL::Theory::rewriteAtomic(), CVCL::Theory::theoryOf(), CVCL::Expr::toString(), and CVCL::TRACE.

Theorem TheoryCore::solve (  const Theorem &  eThm  )

Function: TheoryCore::solve Author: Clark Barrett Created: Wed Feb 26 16:17:54 2003 This is a generalization of what's in my thesis. The goal is to rewrite e into an equisatisfiable conjunction of equations such that the left-hand side of each equation is a variable which does not appear as an i-leaf of the rhs, where i is the theory of the primary solver. Any solution which satisfies this is fine. "Solvers" from other theories can do whatever they want as long as we eventually reach this form. Definition at line 3382 of file theory_core.cpp. References CVCL::TheoryCore::d_solver, CVCL::Theorem::getExpr(), CVCL::Theory::getName(), CVCL::TheoryCore::IF_DEBUG(), CVCL::Expr::isEq(), CVCL::Theory::solve(), CVCL::Theory::theoryOf(), CVCL::Expr::toString(), and CVCL::TRACE.

Theorem TheoryCore::typePred (  const Expr &  e  )

Definition at line 3428 of file theory_core.cpp. References CVCL::TheoryCore::d_rules, and CVCL::CoreProofRules::typePred().

Theorem TheoryCore::subtypePredicate (  const Expr &  e  )

Definition at line 3433 of file theory_core.cpp. References CVCL::CommonProofRules::andIntro(), CVCL::Expr::begin(), CVCL::Theory::d_commonRules, CVCL::TheoryCore::d_rules, CVCL::Expr::end(), CVCL::Theorem::getExpr(), CVCL::Theorem::isNull(), CVCL::Expr::lookupSubtypePred(), CVCL::CommonProofRules::rewriteAnd(), CVCL::Expr::setSubtypePred(), CVCL::TheoryCore::subtypePredicate(), CVCL::TRACE, and CVCL::CoreProofRules::typePred().

Theorem TheoryCore::rewriteIte (  const Expr &  e  )

Definition at line 3478 of file theory_core.cpp. References CVCL::TheoryCore::d_rules, CVCL::Theory::reflexivityRule(), CVCL::CoreProofRules::rewriteIteFalse(), CVCL::CoreProofRules::rewriteIteSame(), and CVCL::CoreProofRules::rewriteIteTrue().

void TheoryCore::setupSubFormulas (  const Expr &  s, const Expr &  e )

Definition at line 3497 of file theory_core.cpp. References CVCL::Expr::addToNotify(), CVCL::Expr::arity(), CVCL::Expr::isAbsAtomicFormula(), CVCL::Expr::isAtomic(), CVCL::TheoryCore::processFactQueue(), CVCL::TheoryCore::setupSubFormulas(), CVCL::TheoryCore::setupTerm(), and CVCL::Theory::theoryOf().

void TheoryCore::registerAtom (  const Expr &  e  )

Definition at line 3520 of file theory_core.cpp. References CVCL::Theory::d_commonRules, CVCL::TheoryCore::d_impliedLiterals, d_inRegisterAtom(), CVCL::Theorem::getRHS(), CVCL::TheoryCore::IF_DEBUG(), CVCL::CommonProofRules::iffFalseElim(), CVCL::CommonProofRules::iffTrueElim(), CVCL::Expr::isAbsAtomicFormula(), CVCL::Expr::isFalse(), CVCL::Expr::isImpliedLiteral(), CVCL::Expr::isTrue(), CVCL::CDList< T >::push_back(), CVCL::Expr::setImpliedLiteral(), CVCL::TheoryCore::setupSubFormulas(), and CVCL::TheoryCore::simplify().

Theorem TheoryCore::getImpliedLiteral (  void   )

Definition at line 3543 of file theory_core.cpp. References CVCL::TheoryCore::d_impliedLiterals, CVCL::TheoryCore::d_impliedLiteralsIdx, and CVCL::CDList< T >::size().

Theorem TheoryCore::getImpliedLiteralByIndex (  unsigned  index  )

Definition at line 3554 of file theory_core.cpp. References CVCL::TheoryCore::d_impliedLiterals, and CVCL::CDList< T >::size().

void TheoryCore::assignValue (  const Expr &  t, const Expr &  val )

Definition at line 3561 of file theory_core.cpp. References CVCL::TheoryCore::CoreSatAPI::addAssumption(), CVCL::TheoryCore::addFact(), CVCL::ExprHashMap< Data >::count(), CVCL::TheoryCore::d_coreSatAPI, CVCL::TheoryCore::d_varAssignments, CVCL::Expr::eqExpr(), CVCL::Theory::find(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::Expr::iffExpr(), CVCL::Type::isBool(), CVCL::Expr::toString(), and CVCL::Theory::transitivityRule().

void TheoryCore::assignValue (  const Theorem &  thm  )

Definition at line 3581 of file theory_core.cpp. References CVCL::TheoryCore::addFact(), CVCL::ExprHashMap< Data >::count(), CVCL::TheoryCore::d_varAssignments, CVCL::Theory::find(), CVCL::Theorem::getExpr(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), CVCL::Theorem::isRewrite(), CVCL::Theory::symmetryRule(), CVCL::Expr::toString(), CVCL::Theorem::toString(), and CVCL::Theory::transitivityRule().

bool TheoryCore::getResource (   )

Definition at line 3602 of file theory_core.cpp. References CVCL::TheoryCore::d_resourceLimit.

Theorem3 TheoryCore::queryTCC (  const Theorem &  phi, const Theorem &  D_phi )

Definition at line 3615 of file theory_core.cpp. References CVCL::TheoryCore::d_rules, and CVCL::CoreProofRules::queryTCC().

Theorem3 TheoryCore::implIntro3 (  const Theorem3 &  phi, const std::vector< Expr > &  assump, const std::vector< Theorem > &  tccs )

Definition at line 3621 of file theory_core.cpp. References CVCL::TheoryCore::d_rules, and CVCL::CoreProofRules::implIntro3().

---