diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/datatype.cpp | 12 | ||||
-rw-r--r-- | src/util/dump.h | 11 | ||||
-rw-r--r-- | src/util/ite_removal.cpp | 4 | ||||
-rw-r--r-- | src/util/model.cpp | 31 | ||||
-rw-r--r-- | src/util/model.h | 43 |
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 */ |