search_theorem_producer.cpp File Reference

Implementation of the proof rules for the simple search engine. More...

#include "search.h"
#include "theory_core.h"
#include "theorem_manager.h"
#include "common_proof_rules.h"
#include "search_theorem_producer.h"

Include dependency graph for search_theorem_producer.cpp:

Go to the source code of this file.

Classes

• class LFSCPrinter

Defines

• #define _CVC3_TRUSTED_

Functions

• bool is_leaf (const Expr &e)
• void collectVars (const Expr &e, ExprMap< bool > &varCache, ExprMap< bool > &visited)

---

Detailed Description

Implementation of the proof rules for the simple search engine.

Author: Sergey Berezin

Created: Mon Feb 24 14:51:51 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 search_theorem_producer.cpp.

---

Define Documentation

#define _CVC3_TRUSTED_

Definition at line 28 of file search_theorem_producer.cpp.

---

Function Documentation

bool is_leaf

(

const Expr &

e

)

Definition at line 1415 of file search_theorem_producer.cpp.

References CVC3::Expr::arity(), and CVC3::Expr::isNot().

Referenced by LFSCPrinter::collect_assumps().

void collectVars	(	const Expr &	e,
		ExprMap< bool > &	varCache,
		ExprMap< bool > &	visited
	)

Definition at line 1541 of file search_theorem_producer.cpp.

References CVC3::Expr::begin(), CVC3::ExprMap< Data >::count(), CVC3::Expr::end(), CVC3::Expr::getKind(), and CVC3::UCONST.

Referenced by CVC3::SearchEngineTheoremProducer::satProof().

---