theory_core.cpp File Reference

#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.

Namespaces

• namespace CVC3

Classes

• class CVC3::PrettyPrinterCore

  Implementation of PrettyPrinter class. More...
  

• class CVC3::TypeComputerCore

Functions

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

  Printing NotifyList class.
  

• IF_DEBUG (bool TheoryCore::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;}) void TheoryCore
• static bool hasBoundVarRec (const Expr &e)
• static bool hasBoundVar (const Expr &e)

---

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

IF_DEBUG

(

)

Definition at line 113 of file theory_core.cpp.

static bool hasBoundVarRec

(

const Expr &

e

)

[static]

Definition at line 3265 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 hasBoundVar().

static bool hasBoundVar

(

const Expr &

e

)

[static]

Definition at line 3277 of file theory_core.cpp.

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

Referenced by CVC3::TheoryCore::enqueueFact().

---