theory_core.cpp File Reference

Go to the source code of this file.

Namespaces

• namespace CVCL

Classes

• class CVCL::PrettyPrinterCore

  Implementation of PrettyPrinter class. More...
  

• class CVCL::TypeComputerCore

Functions

• ostream & CVCL::operator<< (ostream &os, const NotifyList &l)
• IF_DEBUG (static bool isSorted(const vector< Expr > &v){Expr prev;for(vector< Expr >::const_iterator i=v.begin(), iend=v.end();i!=iend;prev=*i,++i){if(prev.isNull()) continue;if(!(prev< *i)) return false;}return true;}) static void intersect(const vector< Expr > &a

  Intersection of sorted vectors of Exprs: res := .
  

• d_cm (cm)
• d_tm (tm)
• d_flags (flags)
• d_statistics (statistics)
• d_inconsistent (cm->getCurrentContext(), false, 0)
• d_incomplete (cm->getCurrentContext())
• d_diseq (cm->getCurrentContext())
• d_incThm (cm->getCurrentContext())
• d_terms (cm->getCurrentContext())
• d_vars (cm->getCurrentContext())
• d_sharedTerms (cm->getCurrentContext())
• d_solver (NULL)
• d_simplifyInPlace (&(flags["ip"].getBool()))
• d_currentRecursiveSimplifier (NULL)
• d_cnfOption (&(flags["cnf"].getBool()))
• d_resourceLimit (0)
• d_dumpTrace (&(flags["dump-trace"].getString()))
• d_inCheckSATCore (false)
• d_inAddFact (false)
• d_inSimplify (false)
• d_inRegisterAtom (false)
• d_notifyObj (this, cm->getCurrentContext())
• d_impliedLiterals (cm->getCurrentContext())
• d_impliedLiteralsIdx (cm->getCurrentContext(), 0, 0)
• d_coreSatAPI (NULL)
• TheoryCore::~TheoryCore ()
• void TheoryCore::assertFact (const Theorem &e)
• void TheoryCore::checkSat (bool fullEffort)
• Theorem TheoryCore::rewriteLitCore (const Expr &e)
• Theorem TheoryCore::rewriteN (const Expr &e, int n)
• Theorem TheoryCore::rewrite (const Expr &e)
• Theorem TheoryCore::simplifyOp (const Expr &e)
• void TheoryCore::setup (const Expr &e)
• void TheoryCore::update (const Theorem &e, const Expr &d)
• void TheoryCore::processUpdates ()
• Expr TheoryCore::computeTypePred (const Type &t, const Expr &e)
• void TheoryCore::checkType (const Expr &e)
• void TheoryCore::computeType (const Expr &e)
• Type TheoryCore::computeBaseType (const Type &tp)
• Expr TheoryCore::computeTCC (const Expr &e)
• ExprStream & TheoryCore::print (ExprStream &os, const Expr &e)
• Expr TheoryCore::parseExpr (const Expr &e)
• Expr TheoryCore::processCond (const Expr &e, int i)

  An auxiliary recursive function to process COND expressions into ITE.
  

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

Variables

• const vector< Expr > & b

---

Detailed Description

Author: Clark Barrett, Vijay Ganesh (CNF converter)

Created: Thu Jan 30 16:57:52 2003

---

Copyright (C) 2003 by the Board of Trustees of Leland Stanford Junior University and by New York University.

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. In particular:

• The above copyright notice and this permission notice must appear in all copies of the software and related documentation.

• THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES, EXPRESSED OR IMPLIED. USE IT AT YOUR OWN RISK.

---

Definition in file theory_core.cpp.

---

Function Documentation

IF_DEBUG (   )  const

Intersection of sorted vectors of Exprs: res := . ASSUMPTION: a and b are sorted in ascending order w.r.t. operator<

d_cm (  cm   )

d_tm (  tm   )

d_flags (  flags   )

d_statistics (  statistics   )

d_inconsistent (  cm->  getCurrentContext(), false  , 0  )

d_incomplete (  cm->  getCurrentContext()  )

d_diseq (  cm->  getCurrentContext()  )

Referenced by d_coreSatAPI().

d_incThm (  cm->  getCurrentContext()  )

d_terms (  cm->  getCurrentContext()  )

d_vars (  cm->  getCurrentContext()  )

Referenced by CVCL::ExprClosure::getVars().

d_sharedTerms (  cm->  getCurrentContext()  )

d_solver (  NULL   )

d_simplifyInPlace (  &  (flags["ip"].getBool())  )

d_currentRecursiveSimplifier (  NULL   )

d_cnfOption (  &  (flags["cnf"].getBool())  )

d_resourceLimit (  0   )

d_dumpTrace (  &  (flags["dump-trace"].getString())  )

Referenced by TheoryCore::addFact(), TheoryCore::enqueueEquality(), and TheoryCore::enqueueFact().

d_inCheckSATCore (  false   )

Referenced by TheoryCore::checkSATCore(), and TheoryCore::enqueueFact().

d_inAddFact (  false   )

Referenced by TheoryCore::addFact(), and TheoryCore::enqueueFact().

d_inSimplify (  false   )

Referenced by TheoryCore::simplify().

d_inRegisterAtom (  false   )

Referenced by TheoryCore::enqueueFact(), and TheoryCore::registerAtom().

d_notifyObj (  this  , cm->  getCurrentContext() )

d_impliedLiterals (  cm->  getCurrentContext()  )

d_impliedLiteralsIdx (  cm->  getCurrentContext(), 0  , 0  )

d_coreSatAPI (  NULL   )

Definition at line 214 of file theory_core.cpp. References CVCL::AND, CVCL::AND_R, CVCL::APPLY, CVCL::ASSERT, CVCL::ASSERTIONS, CVCL::ASSUMPTIONS, CVCL::BOOLEAN, CVCL::BOUND_VAR, CVCL::CALL, CVCL::CHECK_TYPE, CVCL::COND, CVCL::CONST, CVCL::CONSTDEF, CVCL::CONTEXT, CVCL::COUNTEREXAMPLE, CVCL::COUNTERMODEL, TheoryCore::createProofRules(), d_diseq(), CVCL::DBG, CVCL::DEFUN, 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::EQ, CVCL::FALSE, CVCL::FORGET, CVCL::GET_CHILD, CVCL::GET_TYPE, CVCL::TheoremManager::getRules(), CVCL::HELP, CVCL::ID, CVCL::IF, IF_DEBUG(), CVCL::IFF, CVCL::IFF_R, CVCL::IFTHEN, CVCL::IMPLIES, CVCL::ITE, CVCL::ITE_R, CVCL::LET, CVCL::LETDECL, CVCL::LETDECLS, CVCL::NEQ, CVCL::NOT, CVCL::OPTION, CVCL::OR, CVCL::PF_APPLY, CVCL::PF_HOLE, CVCL::POP, CVCL::POP_SCOPE, CVCL::POPTO, CVCL::POPTO_SCOPE, CVCL::PRINT, CVCL::PUSH, CVCL::PUSH_SCOPE, CVCL::QUERY, CVCL::RAW_LIST, CVCL::SEQ, CVCL::SKOLEM_VAR, CVCL::STRING_EXPR, CVCL::SUBSTITUTE, CVCL::SUBTYPE, CVCL::TRACE, CVCL::TRANSFORM, CVCL::TRUE, CVCL::TYPE, CVCL::TYPEDEF, CVCL::UCONST, CVCL::UNTRACE, CVCL::VARDECL, CVCL::VARDECLS, CVCL::VARLIST, CVCL::WHERE, and CVCL::XOR.

static void checkRewriteType (  TheoryCore *  core, const Theorem &  thm )  [static]

Definition at line 2213 of file theory_core.cpp. References CVCL::Theory::getBaseType(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), CVCL::Theorem::toString(), and CVCL::Type::toString(). Referenced by TheoryCore::rewriteCore().

IF_DEBUG (  static ExprMap< bool >  simpStack  )

---

Variable Documentation

const vector<Expr>& b

Definition at line 130 of file theory_core.cpp. Referenced by CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::CoreTheoremProducer::iffAndDistrib(), CVCL::CoreTheoremProducer::iffOrDistrib(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::TheoryArith::processFiniteInterval(), CVCL::SearchEngineTheoremProducer::propIffr(), TheoryCore::rewrite(), CSolver::set_allow_multiple_conflict(), CSolver::set_allow_multiple_conflict_clause(), Xchaff::TranslateAssignmentHook(), and Xchaff::TranslateDecisionHook().

---