diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-07 07:16:49 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-07 07:16:49 +0000 |
commit | 2d7ff62cd52c5c56f29b6567489310cc45767236 (patch) | |
tree | afb975f93b219e7b7a670a4dfc2897e425fd9bf7 /src/expr | |
parent | ce4a5fe6a2529f11eaff66b6cdcdb32ef5309323 (diff) |
SMT-LIBv2 (define-fun...) command now functional; does eager expansion at preprocessing time
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 35 | ||||
-rw-r--r-- | src/expr/command.h | 11 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 6 | ||||
-rw-r--r-- | src/expr/expr_template.h | 14 | ||||
-rw-r--r-- | src/expr/node.h | 67 | ||||
-rw-r--r-- | src/expr/node_value.h | 64 | ||||
-rw-r--r-- | src/expr/type.cpp | 5 | ||||
-rw-r--r-- | src/expr/type.h | 4 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 25 | ||||
-rw-r--r-- | src/expr/type_node.h | 36 |
10 files changed, 215 insertions, 52 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index a1486fcab..8c90f337e 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -23,6 +23,7 @@ #include "expr/command.h" #include "smt/smt_engine.h" +#include "smt/bad_option_exception.h" #include "util/output.h" using namespace std; @@ -217,26 +218,26 @@ void DeclarationCommand::toStream(std::ostream& out) const { /* class DefineFunctionCommand */ -DefineFunctionCommand::DefineFunctionCommand(const std::string& name, - const std::vector<std::pair<std::string, Type> >& args, - Type type, - Expr formula) : - d_name(name), - d_args(args), - d_type(type), +DefineFunctionCommand::DefineFunctionCommand(Expr func, + const std::vector<Expr>& formals, + Expr formula) : + d_func(func), + d_formals(formals), d_formula(formula) { } void DefineFunctionCommand::invoke(SmtEngine* smtEngine) { - smtEngine->defineFunction(d_name, d_args, d_type, d_formula); + smtEngine->defineFunction(d_func, d_formals, d_formula); } void DefineFunctionCommand::toStream(std::ostream& out) const { - out << "DefineFunction( \"" << d_name << "\", ["; - copy( d_args.begin(), d_args.end() - 1, - ostream_iterator<std::pair<std::string, Type> >(out, ", ") ); - out << d_args.back(); - out << "], << " << d_type << " >>, << " << d_formula << " >> )"; + out << "DefineFunction( \"" << d_func << "\", ["; + if(d_formals.size() > 0) { + copy( d_formals.begin(), d_formals.end() - 1, + ostream_iterator<Expr>(out, ", ") ); + out << d_formals.back(); + } + out << "], << " << d_formula << " >> )"; } /* class GetValueCommand */ @@ -324,7 +325,7 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) { try { smtEngine->setInfo(d_flag, d_sexpr); //d_result = "success"; - } catch(BadOption& bo) { + } catch(BadOptionException& bo) { d_result = "unsupported"; } } @@ -352,7 +353,7 @@ GetInfoCommand::GetInfoCommand(std::string flag) : void GetInfoCommand::invoke(SmtEngine* smtEngine) { try { d_result = smtEngine->getInfo(d_flag).getValue(); - } catch(BadOption& bo) { + } catch(BadOptionException& bo) { d_result = "unsupported"; } } @@ -382,7 +383,7 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) { try { smtEngine->setOption(d_flag, d_sexpr); //d_result = "success"; - } catch(BadOption& bo) { + } catch(BadOptionException& bo) { d_result = "unsupported"; } } @@ -410,7 +411,7 @@ GetOptionCommand::GetOptionCommand(std::string flag) : void GetOptionCommand::invoke(SmtEngine* smtEngine) { try { d_result = smtEngine->getOption(d_flag).getValue(); - } catch(BadOption& bo) { + } catch(BadOptionException& bo) { d_result = "unsupported"; } } diff --git a/src/expr/command.h b/src/expr/command.h index 0c78dd1c6..4c74cfd6c 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -111,14 +111,13 @@ public: class CVC4_PUBLIC DefineFunctionCommand : public Command { protected: - std::string d_name; - std::vector<std::pair<std::string, Type> > d_args; - Type d_type; + Expr d_func; + std::vector<Expr> d_formals; Expr d_formula; public: - DefineFunctionCommand(const std::string& name, - const std::vector<std::pair<std::string, Type> >& args, - Type type, Expr formula); + DefineFunctionCommand(Expr func, + const std::vector<Expr>& formals, + Expr formula); void invoke(SmtEngine* smtEngine); void toStream(std::ostream& out) const; };/* class DefineFunctionCommand */ diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 803808b0f..5fb931a65 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -223,7 +223,11 @@ void Expr::toStream(std::ostream& out, int depth, bool types) const { d_node->toStream(out, depth, types); } -Node Expr::getNode() const { +Node Expr::getNode() const throw() { + return *d_node; +} + +TNode Expr::getTNode() const throw() { return *d_node; } diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 8fab13b37..bb227f92f 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -43,8 +43,13 @@ class NodeTemplate; class Expr; class ExprManager; +class SmtEngine; class Type; +namespace smt { + class SmtEnginePrivate; +}/* CVC4::smt namespace */ + namespace expr { class CVC4_PUBLIC ExprSetDepth; class CVC4_PUBLIC ExprPrintTypes; @@ -383,10 +388,17 @@ protected: * Returns the actual internal node. * @return the internal node */ - NodeTemplate<true> getNode() const; + NodeTemplate<true> getNode() const throw(); + + /** + * Returns the actual internal node as a TNode. + * @return the internal node + */ + NodeTemplate<false> getTNode() const throw(); // Friend to access the actual internal expr information and private methods friend class SmtEngine; + friend class smt::SmtEnginePrivate; friend class ExprManager; }; diff --git a/src/expr/node.h b/src/expr/node.h index 67d46a977..bd6b53522 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -380,6 +380,20 @@ public: throw (CVC4::TypeCheckingExceptionPrivate, CVC4::AssertionException); /** + * Substitution of Nodes. + */ + Node substitute(TNode node, TNode replacement) const; + + /** + * Simultaneous substitution of Nodes. + */ + template <class Iterator1, class Iterator2> + Node substitute(Iterator1 nodesBegin, + Iterator1 nodesEnd, + Iterator2 replacementsBegin, + Iterator2 replacementsEnd) const; + + /** * Returns the kind of this node. * @return the kind */ @@ -1035,6 +1049,59 @@ TypeNode NodeTemplate<ref_count>::getType(bool check) const return NodeManager::currentNM()->getType(*this, check); } +template <bool ref_count> +Node NodeTemplate<ref_count>::substitute(TNode node, + TNode replacement) const { + NodeBuilder<> nb(getKind()); + if(getMetaKind() == kind::metakind::PARAMETERIZED) { + // push the operator + nb << getOperator(); + } + for(TNode::const_iterator i = begin(), + iend = end(); + i != iend; + ++i) { + if(*i == node) { + nb << replacement; + } else { + (*i).substitute(node, replacement); + } + } + Node n = nb; + return n; +} + +template <bool ref_count> +template <class Iterator1, class Iterator2> +Node NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, + Iterator1 nodesEnd, + Iterator2 replacementsBegin, + Iterator2 replacementsEnd) const { + Assert( nodesEnd - nodesBegin == replacementsEnd - replacementsBegin, + "Substitution iterator ranges must be equal size" ); + Iterator1 j = find(nodesBegin, nodesEnd, *this); + if(j != nodesEnd) { + return *(replacementsBegin + (j - nodesBegin)); + } else if(getNumChildren() == 0) { + return *this; + } else { + NodeBuilder<> nb(getKind()); + if(getMetaKind() == kind::metakind::PARAMETERIZED) { + // push the operator + nb << getOperator(); + } + for(TNode::const_iterator i = begin(), + iend = end(); + i != iend; + ++i) { + nb << (*i).substitute(nodesBegin, nodesEnd, + replacementsBegin, replacementsEnd); + } + Node n = nb; + return n; + } +} + #ifdef CVC4_DEBUG /** * Pretty printer for use within gdb. This is not intended to be used diff --git a/src/expr/node_value.h b/src/expr/node_value.h index e4fc479b7..658cb1e2d 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -171,8 +171,48 @@ private: return iterator(d_i++); } - typedef std::input_iterator_tag iterator_category; - }; + iterator& operator--() { + --d_i; + return *this; + } + + iterator operator--(int) { + return iterator(d_i--); + } + + iterator& operator+=(difference_type p) { + d_i += p; + return *this; + } + + iterator& operator-=(difference_type p) { + d_i -= p; + return *this; + } + + iterator operator+(difference_type p) { + return iterator(d_i + p); + } + + iterator operator-(difference_type p) { + return iterator(d_i - p); + } + + difference_type operator-(iterator i) { + return d_i - i.d_i; + } + + typedef std::random_access_iterator_tag iterator_category; + };/* class NodeValue::iterator<T> */ + + // operator+ (as a function) cannot be a template, so we have to + // define two versions + friend NodeValue::iterator<NodeTemplate<true> > + operator+(NodeValue::iterator<NodeTemplate<true> >::difference_type p, + NodeValue::iterator<NodeTemplate<true> > i); + friend NodeValue::iterator<NodeTemplate<false> > + operator+(NodeValue::iterator<NodeTemplate<false> >::difference_type p, + NodeValue::iterator<NodeTemplate<false> > i); /** Decrement ref counts of children */ inline void decrRefCounts(); @@ -259,6 +299,26 @@ private: };/* class NodeValue */ /** + * Provides a symmetric addition operator to that already defined in + * the iterator class. + */ +inline NodeValue::iterator<NodeTemplate<true> > +operator+(NodeValue::iterator<NodeTemplate<true> >::difference_type p, + NodeValue::iterator<NodeTemplate<true> > i) { + return i + p; +} + +/** + * Provides a symmetric addition operator to that already defined in + * the iterator class. + */ +inline NodeValue::iterator<NodeTemplate<false> > +operator+(NodeValue::iterator<NodeTemplate<false> >::difference_type p, + NodeValue::iterator<NodeTemplate<false> > i) { + return i + p; +} + +/** * For hash_maps, hash_sets, etc.. but this is for expr package * internal use only at present! This is likely to be POORLY * PERFORMING for other uses! NodeValue::poolHash() will lead to diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 05b69f6f4..8cf555eb0 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -111,7 +111,10 @@ Type Type::substitute(const vector<Type>& types, replacementsNodes.push_back(*(*i).d_typeNode); } - return makeType(d_typeNode->substitute(typesNodes, replacementsNodes)); + return makeType(d_typeNode->substitute(typesNodes.begin(), + typesNodes.end(), + replacementsNodes.begin(), + replacementsNodes.end())); } void Type::toStream(ostream& out) const { diff --git a/src/expr/type.h b/src/expr/type.h index 57ec3bf5c..19c3d27f3 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -60,6 +60,8 @@ struct CVC4_PUBLIC TypeHashStrategy { */ class CVC4_PUBLIC Type { + friend class SmtEngine; + friend class SmtEnginePrivate; friend class ExprManager; friend class TypeNode; friend class TypeHashStrategy; @@ -87,7 +89,7 @@ protected: Type(NodeManager* em, TypeNode* typeNode); /** Accessor for derived classes */ - static TypeNode* getTypeNode(const Type& t) { return t.d_typeNode; } + static TypeNode* getTypeNode(const Type& t) throw() { return t.d_typeNode; } public: diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index a55c05c5a..badc3b72f 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -33,7 +33,10 @@ TypeNode TypeNode::substitute(const TypeNode& type, // push the operator nb << TypeNode(d_nv->d_children[0]); } - for(TypeNode::iterator i = begin(), iend = end(); i != iend; ++i) { + for(TypeNode::const_iterator i = begin(), + iend = end(); + i != iend; + ++i) { if(*i == type) { nb << replacement; } else { @@ -43,26 +46,6 @@ TypeNode TypeNode::substitute(const TypeNode& type, return nb.constructTypeNode(); } -TypeNode TypeNode::substitute(const vector<TypeNode>& types, - const vector<TypeNode>& replacements) const { - vector<TypeNode>::const_iterator j = find(types.begin(), types.end(), *this); - if(j != types.end()) { - return replacements[j - types.begin()]; - } else if(getNumChildren() == 0) { - return *this; - } else { - NodeBuilder<> nb(getKind()); - if(getMetaKind() == kind::metakind::PARAMETERIZED) { - // push the operator - nb << TypeNode(d_nv->d_children[0]); - } - for(TypeNode::iterator i = begin(), iend = end(); i != iend; ++i) { - nb << (*i).substitute(types, replacements); - } - return nb.constructTypeNode(); - } -} - bool TypeNode::isBoolean() const { return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE; diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 6780b08f7..0e763128f 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -118,8 +118,11 @@ public: /** * Simultaneous substitution of TypeNodes. */ - TypeNode substitute(const std::vector<TypeNode>& types, - const std::vector<TypeNode>& replacements) const; + template <class Iterator1, class Iterator2> + TypeNode substitute(Iterator1 typesBegin, + Iterator1 typesEnd, + Iterator2 replacementsBegin, + Iterator2 replacementsEnd) const; /** * Structural comparison operator for expressions. @@ -436,6 +439,35 @@ struct TypeNodeHashStrategy { namespace CVC4 { +template <class Iterator1, class Iterator2> +TypeNode TypeNode::substitute(Iterator1 typesBegin, + Iterator1 typesEnd, + Iterator2 replacementsBegin, + Iterator2 replacementsEnd) const { + Assert( typesEnd - typesBegin == replacementsEnd - replacementsBegin, + "Substitution iterator ranges must be equal size" ); + Iterator1 j = find(typesBegin, typesEnd, *this); + if(j != typesEnd) { + return *(replacementsBegin + (j - typesBegin)); + } else if(getNumChildren() == 0) { + return *this; + } else { + NodeBuilder<> nb(getKind()); + if(getMetaKind() == kind::metakind::PARAMETERIZED) { + // push the operator + nb << TypeNode(d_nv->d_children[0]); + } + for(TypeNode::const_iterator i = begin(), + iend = end(); + i != iend; + ++i) { + nb << (*i).substitute(typesBegin, typesEnd, + replacementsBegin, replacementsEnd); + } + return nb.constructTypeNode(); + } +} + inline size_t TypeNode::getNumChildren() const { return d_nv->getNumChildren(); } |