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 "theory_arith.h"

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 containsRec (const Expr &def, ExprHashMap< bool > &defs, ExprHashMap< bool > &visited)
• static bool contains (const Expr &def, ExprHashMap< bool > &defs)
• static bool hasBoundVarRec (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

static bool containsRec	(	const Expr &	def,
		ExprHashMap< bool > &	defs,
		ExprHashMap< bool > &	visited
	)		[static]

Definition at line 2014 of file theory_core.cpp.

References CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::ExprHashMap< Data >::end(), CVC3::ExprHashMap< Data >::find(), CVC3::Expr::getBody(), and CVC3::Expr::isClosure().

Referenced by contains().

static bool contains	(	const Expr &	def,
		ExprHashMap< bool > &	defs
	)		[static]

Definition at line 2031 of file theory_core.cpp.

References containsRec().

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

static bool hasBoundVarRec

(

const Expr &

e

)

[static]

Definition at line 4152 of file theory_core.cpp.

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