CVC3  2.4.1
theory_simulate.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file theory_simulate.h
4  *\brief Implementation of a symbolic simulator
5  *
6  * Author: Sergey Berezin
7  *
8  * Created: Tue Oct 7 10:13:15 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__include__theory_simulate_h_
23 #define _cvc3__include__theory_simulate_h_
24 
25 #include "theory.h"
26 
27 namespace CVC3 {
28 
29 class SimulateProofRules;
30 
31 /*****************************************************************************/
32 /*!
33  * \class TheorySimulate
34  * \ingroup Theories
35  * \brief "Theory" of symbolic simulation.
36  *
37  * Author: Sergey Berezin
38  *
39  * Created: Tue Oct 7 10:13:15 2003
40  *
41  * This theory owns the SIMULATE operator. It's job is to replace the above
42  * expressions by their definitions using rewrite rules.
43  */
44 /*****************************************************************************/
45 
46 class TheorySimulate: public Theory {
47 private:
48  //! Our local proof rules
50  //! Create proof rules for this theory
52 public:
53  //! Constructor
55  //! Destructor
57  // The required Theory API functions
58  void assertFact(const Theorem& e) { }
59  void checkSat(bool fullEffort) { }
60  Theorem rewrite(const Expr& e);
61  void computeType(const Expr& e);
62  Expr computeTCC(const Expr& e);
63  Expr parseExprOp(const Expr& e);
64  ExprStream& print(ExprStream& os, const Expr& e);
65 }; // end of class TheorySimulate
66 
67 } // end of namespace CVC3
68 
69 #endif
~TheorySimulate()
Destructor.
Data structure of expressions in CVC3.
Definition: expr.h:133
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
Base class for theories.
Definition: theory.h:64
"Theory" of symbolic simulation.
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
SimulateProofRules * d_rules
Our local proof rules.
void computeType(const Expr &e)
Compute and store the type of e.
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
TheorySimulate(TheoryCore *core)
Constructor.
Generic API for Theories plus methods commonly used by theories.
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
SimulateProofRules * createProofRules()
Create proof rules for this theory.