CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
theory_simulate
simulate_proof_rules.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
*\file simulate_proof_rules.h
4
*\brief Abstract interface to the symbolic simulator proof rules
5
*
6
* Author: Sergey Berezin
7
*
8
* Created: Tue Oct 7 10:44:42 2003
9
*
10
* <hr>
11
*
12
* License to use, copy, modify, sell and/or distribute this software
13
* and its documentation for any purpose is hereby granted without
14
* royalty, subject to the terms and conditions defined in the \ref
15
* LICENSE file provided with this distribution.
16
*
17
* <hr>
18
*
19
*/
20
/*****************************************************************************/
21
22
#ifndef _cvc3__theory_simulate__simulate_proof_rules_h_
23
#define _cvc3__theory_simulate__simulate_proof_rules_h_
24
25
namespace
CVC3
{
26
27
class
Expr;
28
class
Theorem;
29
30
class
SimulateProofRules
{
31
public
:
32
//! Destructor
33
virtual
~SimulateProofRules
() { }
34
35
//! SIMULATE(f, s_0, i_1, ..., i_k, N) <=> f(...f(f(s_0, i_1), i_2), ... i_k)
36
virtual
Theorem
expandSimulate
(
const
Expr
& e) = 0;
37
38
};
// end of class SimulateProofRules
39
40
}
// end of namespace CVC3
41
42
#endif
CVC3::Expr
Data structure of expressions in CVC3.
Definition:
expr.h:133
CVC3::Theorem
Definition:
theorem.h:76
CVC3::SimulateProofRules::~SimulateProofRules
virtual ~SimulateProofRules()
Destructor.
Definition:
simulate_proof_rules.h:33
CVC3::SimulateProofRules::expandSimulate
virtual Theorem expandSimulate(const Expr &e)=0
SIMULATE(f, s_0, i_1, ..., i_k, N) <=> f(...f(f(s_0, i_1), i_2), ... i_k)
CVC3::SimulateProofRules
Definition:
simulate_proof_rules.h:30
CVC3
Definition:
expr.cpp:35
Generated on Thu Jul 2 2015 03:30:20 for CVC3 by
1.8.9.1