diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-04 17:45:56 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-04 17:45:56 +0000 |
commit | 930601b40c68d959e66abc71da6ff3296860952e (patch) | |
tree | 3172d5e8eb1177de6a4d57a8bed1dc4e0147d53b /src/util/model.h | |
parent | edc69feaf7b41e0166f172d943b0d981f392474a (diff) |
Implemented array type enumerator, more fixes for models
Diffstat (limited to 'src/util/model.h')
-rw-r--r-- | src/util/model.h | 65 |
1 files changed, 0 insertions, 65 deletions
diff --git a/src/util/model.h b/src/util/model.h deleted file mode 100644 index 97010dd45..000000000 --- a/src/util/model.h +++ /dev/null @@ -1,65 +0,0 @@ -/********************* */ -/*! \file model.h - ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Model class - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__MODEL_H -#define __CVC4__MODEL_H - -#include <iostream> -#include <vector> - -#include "expr/expr.h" -#include "util/cardinality.h" - -namespace CVC4 { - -class CVC4_PUBLIC Command; -class CVC4_PUBLIC SmtEngine; - -class CVC4_PUBLIC Model { -private: - /** The SmtEngine we're associated to */ - const SmtEngine& d_smt; -public: - /** construct the base class */ - Model(); - /** virtual destructor */ - virtual ~Model() { } - /** get number of commands to report */ - size_t getNumCommands() const; - /** get command */ - const Command* getCommand(size_t i) const; -public: - /** get value for expression */ - virtual Expr getValue(Expr expr) = 0; - /** get cardinality for sort */ - virtual Cardinality getCardinality(Type t) = 0; - /** write the model to a stream */ - virtual void toStream(std::ostream& out) = 0; -};/* class Model */ - -class ModelBuilder -{ -public: - ModelBuilder(){} - virtual ~ModelBuilder(){} - virtual void buildModel( Model* m, bool fullModel ) = 0; -};/* class ModelBuilder */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__MODEL_H */ |