CVC3  2.4.1
theory_datatype.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file theory_datatype.h
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Wed Dec 1 22:24:32 2004
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 #ifndef _cvc3__include__theory_datatype_h_
22 #define _cvc3__include__theory_datatype_h_
23 
24 #include "theory.h"
25 #include "smartcdo.h"
26 #include "cdmap.h"
27 
28 namespace CVC3 {
29 
30 class DatatypeProofRules;
31 
32 //! Local kinds for datatypes
33  typedef enum {
39  } DatatypeKinds;
40 
41 /*****************************************************************************/
42 /*!
43  *\class TheoryDatatype
44  *\ingroup Theories
45  *\brief This theory handles datatypes.
46  *
47  * Author: Clark Barrett
48  *
49  * Created: Wed Dec 1 22:27:12 2004
50  */
51 /*****************************************************************************/
52 class TheoryDatatype :public Theory {
53 protected:
55 
56  // maps DATATYPE expressions to map containing constructors for that datatype
58  // maps constructor to its selectors
60  // maps selector to a pair containing the constructor and the position of the selctor for that constructor
62  // maps tester to constructor that it matches
65 
67 
72  const bool& d_smartSplits;
74 
75 protected:
76  virtual void instantiate(const Expr& e, const Unsigned& u);
77  virtual void initializeLabels(const Expr& e, const Type& t);
78  virtual void mergeLabels(const Theorem& thm, const Expr& e1, const Expr& e2);
79  virtual void mergeLabels(const Theorem& thm, const Expr& e,
80  unsigned position, bool positive);
81 
82 public:
84  virtual ~TheoryDatatype();
85 
86  // Trusted method that creates the proof rules class (used in constructor).
87  // Implemented in datatype_theorem_producer.cpp
89 
90  // Theory interface
91  void addSharedTerm(const Expr& e);
92  void assertFact(const Theorem& e);
93  virtual void checkSat(bool fullEffort);
94  Theorem rewrite(const Expr& e);
95  virtual void setup(const Expr& e);
96  virtual void update(const Theorem& e, const Expr& d);
97  Theorem solve(const Theorem& e);
98  void checkType(const Expr& e);
100  bool enumerate, bool computeSize);
101  void computeType(const Expr& e);
102  void computeModelTerm(const Expr& e, std::vector<Expr>& v);
103  Expr computeTCC(const Expr& e);
104  Expr parseExprOp(const Expr& e);
105  ExprStream& print(ExprStream& os, const Expr& e);
106 
107  // Returns Expr(DATATYPE_DECL datatype)
108  Expr dataType(const std::string& name,
109  const std::vector<std::string>& constructors,
110  const std::vector<std::vector<std::string> >& selectors,
111  const std::vector<std::vector<Expr> >& types);
112 
113  // Returns Expr(DATATYPE_DECL type_1, type_2, ...)
114  Expr dataType(const std::vector<std::string>& names,
115  const std::vector<std::vector<std::string> >& constructors,
116  const std::vector<std::vector<std::vector<std::string> > >& selectors,
117  const std::vector<std::vector<std::vector<Expr> > >& types);
118 
119  Expr datatypeConsExpr(const std::string& constructor,
120  const std::vector<Expr>& args);
121  Expr datatypeSelExpr(const std::string& selector, const Expr& arg);
122  Expr datatypeTestExpr(const std::string& constructor, const Expr& arg);
123 
124  const std::pair<Expr,unsigned>& getSelectorInfo(const Expr& e);
125  Expr getConsForTester(const Expr& e);
126  unsigned getConsPos(const Expr& e);
127  Expr getConstant(const Type& t);
128  const Op& getReachablePredicate(const Type& t);
129  bool canCollapse(const Expr& e);
130 
131 };
132 
133 inline bool isDatatype(const Type& t)
134  { return t.getExpr().getKind() == DATATYPE; }
135 
136 inline bool isConstructor(const Expr& e)
137  { return (e.getKind() == CONSTRUCTOR && e.getType().arity()==1) ||
138  (e.isApply() && e.getOpKind() == CONSTRUCTOR); }
139 
140 inline bool isSelector(const Expr& e)
141  { return e.isApply() && e.getOpKind() == SELECTOR; }
142 
143 inline bool isTester(const Expr& e)
144  { return e.isApply() && e.getOpKind() == TESTER; }
145 
146 inline Expr getConstructor(const Expr& e)
147  { DebugAssert(isConstructor(e), "Constructor expected");
148  return e.isApply() ? e.getOpExpr() : e; }
149 
150 }
151 
152 #endif
void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
bool isConstructor(const Expr &e)
TheoryCore * theoryCore()
Get a pointer to theoryCore.
Definition: theory.h:93
bool isDatatype(const Type &t)
CDMap< Expr, SmartCDO< Unsigned > > d_labels
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 datatypeTestExpr(const std::string &constructor, const Expr &arg)
void checkType(const Expr &e)
Check that e is a valid Type expr.
const bool & d_smartSplits
CDList< Expr > d_splitters
virtual void mergeLabels(const Theorem &thm, const Expr &e1, const Expr &e2)
virtual void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
Expr getConstructor(const Expr &e)
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
DatatypeProofRules * d_rules
MS C++ specific settings.
Definition: type.h:42
Base class for theories.
Definition: theory.h:64
Expr getConstant(const Type &t)
DatatypeKinds
Local kinds for datatypes.
bool isSelector(const Expr &e)
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
#define DebugAssert(cond, str)
Definition: debug.h:408
ExprMap< ExprMap< unsigned > > d_datatypes
virtual void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
bool canCollapse(const Expr &e)
unsigned getConsPos(const Expr &e)
Expr getConsForTester(const Expr &e)
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
Definition: expr.h:1191
void computeType(const Expr &e)
Compute and store the type of e.
const Op & getReachablePredicate(const Type &t)
const Expr & getExpr() const
Definition: type.h:52
virtual void initializeLabels(const Expr &e, const Type &t)
CDO< unsigned > d_splittersIndex
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
int arity() const
Definition: type.h:55
This theory handles datatypes.
int getOpKind() const
Get kind of operator (for APPLY Exprs only)
Definition: expr.h:1196
Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
ExprMap< Expr > d_testerMap
int getKind() const
Definition: expr.h:1168
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
const std::pair< Expr, unsigned > & getSelectorInfo(const Expr &e)
bool isApply() const
Definition: expr.h:1014
virtual void instantiate(const Expr &e, const Unsigned &u)
bool isTester(const Expr &e)
CDList< Theorem > d_facts
Expr datatypeSelExpr(const std::string &selector, const Expr &arg)
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
Generic API for Theories plus methods commonly used by theories.
CDO< bool > d_splitterAsserted
TheoryDatatype(TheoryCore *theoryCore)
Theorem solve(const Theorem &e)
An optional solver.
Expr datatypeConsExpr(const std::string &constructor, const std::vector< Expr > &args)
Cardinality
Enum for cardinality of types.
Definition: expr.h:80
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
Definition: expr.cpp:35
DatatypeProofRules * createProofRules()
Type getType() const
Get the type. Recursively compute if necessary.
Definition: expr.h:1259
ExprMap< std::pair< Expr, unsigned > > d_selectorMap
ExprMap< std::vector< Expr > > d_constructorMap
virtual void checkSat(bool fullEffort)
Check for satisfiability in the theory.
ExprMap< bool > d_getConstantStack
Expr dataType(const std::string &name, const std::vector< std::string > &constructors, const std::vector< std::vector< std::string > > &selectors, const std::vector< std::vector< Expr > > &types)
Smart context-dependent object wrapper.
ExprMap< Op > d_reach
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.