theory_core.cpp File Reference

#include <locale>
#include <cctype>
#include <ctime>
#include "command_line_flags.h"
#include "expr.h"
#include "notifylist.h"
#include "pretty_printer.h"
#include "common_proof_rules.h"
#include "parser_exception.h"
#include "typecheck_exception.h"
#include "smtlib_exception.h"
#include "eval_exception.h"
#include "theory_core.h"
#include "expr_transform.h"
#include "core_proof_rules.h"
#include "theorem_manager.h"
#include "translator.h"

Include dependency graph for theory_core.cpp:

Go to the source code of this file.

Classes

• class CVC3::PrettyPrinterCore

  Implementation of PrettyPrinter class. More...
  

• class CVC3::TypeComputerCore

Namespaces

• namespace CVC3

Functions

• std::ostream & CVC3::operator<< (std::ostream &os, const NotifyList &l)

  Printing NotifyList class.
  

• static bool hasBoundVarRec (const Expr &e)
• IF_DEBUG (static bool hasBoundVar(const Expr &e){e.getEM()->clearFlags();return hasBoundVarRec(e);}) void TheoryCore

---

Detailed Description

Author: Clark Barrett, Vijay Ganesh (CNF converter)

Created: Thu Jan 30 16:57:52 2003

---

License to use, copy, modify, sell and/or distribute this software and its documentation for any purpose is hereby granted without royalty, subject to the terms and conditions defined in the LICENSE file provided with this distribution.

---

Definition in file theory_core.cpp.

---

Function Documentation

static bool hasBoundVarRec

(

const Expr &

e

)

[static]

Definition at line 3743 of file theory_core.cpp.

References CVC3::Expr::arity(), CVC3::BOUND_VAR, CVC3::Expr::getFlag(), CVC3::Expr::getKind(), CVC3::Expr::isQuantifier(), and CVC3::Expr::setFlag().

Referenced by IF_DEBUG().

IF_DEBUG

(

)

Definition at line 3755 of file theory_core.cpp.

References CVC3::ExprManager::clearFlags(), CVC3::Expr::getEM(), and hasBoundVarRec().