summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/datatype.cpp12
-rw-r--r--src/util/dump.h11
-rw-r--r--src/util/ite_removal.cpp4
-rw-r--r--src/util/model.cpp31
-rw-r--r--src/util/model.h43
5 files changed, 50 insertions, 51 deletions
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index bdb3f6cf6..522bcd935 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -414,7 +414,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
string typeName = (*i).d_name.substr((*i).d_name.find('\0') + 1);
(*i).d_name.resize((*i).d_name.find('\0'));
if(typeName == "") {
- (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, selfTypeNode)).toExpr();
+ (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, selfTypeNode), "is a selector").toExpr();
} else {
map<string, DatatypeType>::const_iterator j = resolutions.find(typeName);
if(j == resolutions.end()) {
@@ -424,7 +424,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
<< "of constructor \"" << d_name << "\"";
throw DatatypeResolutionException(msg.str());
} else {
- (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType((*j).second))).toExpr();
+ (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType((*j).second)), "is a selector").toExpr();
}
}
} else {
@@ -437,7 +437,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
if(!paramTypes.empty() ) {
range = doParametricSubstitution( range, paramTypes, paramReplacements );
}
- (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range))).toExpr();
+ (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range)), "is a selector").toExpr();
}
Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++);
(*i).d_resolved = true;
@@ -450,8 +450,8 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
// fails above, we want Constuctor::isResolved() to remain "false".
// Further, mkConstructorType() iterates over the selectors, so
// should get the results of any resolutions we did above.
- d_tester = nm->mkSkolem(getTesterName(), nm->mkTesterType(selfTypeNode)).toExpr();
- d_constructor = nm->mkSkolem(getName(), nm->mkConstructorType(*this, selfTypeNode)).toExpr();
+ d_tester = nm->mkSkolem(getTesterName(), nm->mkTesterType(selfTypeNode), "is a tester").toExpr();
+ d_constructor = nm->mkSkolem(getName(), nm->mkConstructorType(*this, selfTypeNode), "is a constructor").toExpr();
// associate constructor with all selectors
for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
(*i).d_constructor = d_constructor;
@@ -521,7 +521,7 @@ void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
// we're using some internals, so we have to set up this library context
ExprManagerScope ems(selectorType);
- Expr type = NodeManager::currentNM()->mkSkolem(TypeNode::fromType(selectorType)).toExpr();
+ Expr type = NodeManager::currentNM()->mkSkolem("unresolved_" + selectorName + "_$$", TypeNode::fromType(selectorType), "is an unresolved selector type placeholder").toExpr();
Debug("datatypes") << type << endl;
d_args.push_back(DatatypeConstructorArg(selectorName, type));
}
diff --git a/src/util/dump.h b/src/util/dump.h
index 382092474..8e81086b2 100644
--- a/src/util/dump.h
+++ b/src/util/dump.h
@@ -96,17 +96,6 @@ public:
void clear() { d_commands.clear(); }
const CommandSequence& getCommands() const { return d_commands; }
- void declareVar(Expr e, std::string comment) {
- if(isOn("declarations")) {
- std::stringstream ss;
- ss << Expr::setlanguage(Expr::setlanguage::getLanguage(getStream())) << e;
- std::string s = ss.str();
- CVC4dumpstream(getStream(), d_commands)
- << CommentCommand(s + " is " + comment)
- << DeclareFunctionCommand(s, e, e.getType());
- }
- }
-
bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; }
bool on (std::string tag) { d_tags.insert(tag); return true; }
bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 50713e2b4..e8a539615 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -55,9 +55,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output,
TypeNode nodeType = node.getType();
if(!nodeType.isBoolean()) {
// Make the skolem to represent the ITE
- Node skolem = nodeManager->mkSkolem(nodeType);
-
- Dump.declareVar(skolem.toExpr(), "a variable introduced due to term-level ITE removal");
+ Node skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
// The new assertion
Node newAssertion =
diff --git a/src/util/model.cpp b/src/util/model.cpp
index 50683fdff..8b0e956cf 100644
--- a/src/util/model.cpp
+++ b/src/util/model.cpp
@@ -2,14 +2,39 @@
/*! \file model.cpp
** \verbatim
** Original author: ajreynol
- ** Major contributors: none
+ ** Major contributors: mdeters
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** 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 implementation of Model class
- **/ \ No newline at end of file
+ **/
+
+#include "util/model.h"
+#include "expr/command.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/command_list.h"
+
+#include <vector>
+
+using namespace std;
+
+namespace CVC4 {
+
+Model::Model() :
+ d_smt(*smt::currentSmtEngine()) {
+}
+
+size_t Model::getNumCommands() const {
+ return d_smt.d_modelCommands->size();
+}
+
+const Command* Model::getCommand(size_t i) const {
+ return (*d_smt.d_modelCommands)[i];
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/model.h b/src/util/model.h
index 36a5464b4..97010dd45 100644
--- a/src/util/model.h
+++ b/src/util/model.h
@@ -2,10 +2,10 @@
/*! \file model.h
** \verbatim
** Original author: ajreynol
- ** Major contributors: none
+ ** Major contributors: mdeters
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** 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
@@ -27,41 +27,28 @@
namespace CVC4 {
-class Command;
+class CVC4_PUBLIC Command;
+class CVC4_PUBLIC SmtEngine;
-class Model
-{
-public:
- //types of commands that are recorded for get-model
- enum {
- COMMAND_DECLARE_SORT, //DeclareTypeCommand
- COMMAND_DECLARE_FUN, //DeclareFunctionCommand
- COMMAND_DECLARE_DATATYPES, //DatatypeDeclarationCommand
- };
+class CVC4_PUBLIC Model {
private:
- //list of commands that the model must report when calling get model
- std::vector< Command* > d_commands;
- std::vector< int > d_command_types;
+ /** The SmtEngine we're associated to */
+ const SmtEngine& d_smt;
public:
+ /** construct the base class */
+ Model();
/** virtual destructor */
- virtual ~Model() {}
- /** add command */
- virtual void addCommand( Command* c, int c_type ){
- d_commands.push_back( c );
- d_command_types.push_back( c_type );
- }
+ virtual ~Model() { }
/** get number of commands to report */
- size_t getNumCommands() { return d_commands.size(); }
+ size_t getNumCommands() const;
/** get command */
- Command* getCommand( int i ) { return d_commands[i]; }
- /** get type of command */
- int getCommandType( int i ) { return d_command_types[i]; }
+ const Command* getCommand(size_t i) const;
public:
/** get value for expression */
- virtual Expr getValue( const Expr& expr ) = 0;
+ virtual Expr getValue(Expr expr) = 0;
/** get cardinality for sort */
- virtual Cardinality getCardinality( const Type& t ) = 0;
- /** to stream function */
+ virtual Cardinality getCardinality(Type t) = 0;
+ /** write the model to a stream */
virtual void toStream(std::ostream& out) = 0;
};/* class Model */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback