summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2012-09-11 23:44:49 +0000
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2012-09-11 23:44:49 +0000
commit78482ce84a4652c69baa8a07d5d714408ab6cf03 (patch)
treed2dc79b21d7dc2c4d67fa1564978a403d327b963 /src/util
parentd8883776ce80199096f99d1088910d478fd0cd6e (diff)
added getCardinality to model
Diffstat (limited to 'src/util')
-rw-r--r--src/util/model.h5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/util/model.h b/src/util/model.h
index ca7565aaa..9b7db536f 100644
--- a/src/util/model.h
+++ b/src/util/model.h
@@ -23,6 +23,7 @@
#include <vector>
#include "expr/expr.h"
+#include "util/cardinality.h"
namespace CVC4 {
@@ -54,8 +55,10 @@ public:
/** get type of command */
int getCommandType( int i ) { return d_command_types[i]; }
public:
- /** get value */
+ /** get value for expression */
virtual Expr getValue( const Expr& expr ) = 0;
+ /** get cardinality for sort */
+ virtual Cardinality getCardinality( const Type& t ) = 0;
/** to stream function */
virtual void toStream(std::ostream& out) = 0;
};/* class Model */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback