diff options
Diffstat (limited to 'src/expr')
66 files changed, 6398 insertions, 3030 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index c5a032abc..dc6ad5833 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -3,41 +3,75 @@ AM_CPPFLAGS = \ -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) +#noinst_LTLIBRARIES = libexpr.la libstatistics.la noinst_LTLIBRARIES = libexpr.la +# libstatistics_la_CPPFLAGS = $(CPPFLAGS) $(AM_CPPFLAGS) -D__BUILDING_STATISTICS_FOR_EXPORT +# libstatistics_la_SOURCES = \ +# statistics_registry.h \ +# statistics_registry.cpp + +# EXTRA_libstatistics_la_DEPENDENCIES = \ +# builts + +# For some reason statistics were in libutil. No idea why though. libexpr_la_SOURCES = \ - node.h \ + statistics.cpp \ + statistics.h \ + statistics_registry.cpp \ + statistics_registry.h \ + array.h \ + array_store_all.cpp \ + array_store_all.h \ + ascription_type.h \ + attribute.h \ + attribute.cpp \ + attribute_internals.h \ + attribute_unique_id.h \ + convenience_node_builders.h \ + chain.h \ + emptyset.cpp \ + emptyset.h \ + expr_manager_scope.h \ + expr_stream.h \ + kind_map.h \ + matcher.h \ node.cpp \ - type_node.h \ - type_node.cpp \ + node.h \ node_builder.h \ - convenience_node_builders.h \ - type.h \ - type.cpp \ - node_value.h \ - node_value.cpp \ - node_manager.h \ node_manager.cpp \ + node_manager.h \ node_manager_attributes.h \ - type_checker.h \ - attribute_unique_id.h \ - attribute.h \ - attribute_internals.h \ - attribute.cpp \ - command.h \ - command.cpp \ - symbol_table.h \ - symbol_table.cpp \ - expr_manager_scope.h \ node_self_iterator.h \ - variable_type_map.h \ - pickle_data.h \ + node_self_iterator.h \ + node_value.cpp \ + node_value.h \ pickle_data.cpp \ - pickler.h \ + pickle_data.h \ pickler.cpp \ - node_self_iterator.h \ - expr_stream.h \ - kind_map.h + pickler.h \ + resource_manager.cpp \ + resource_manager.h \ + sexpr.cpp \ + sexpr.h \ + symbol_table.cpp \ + symbol_table.h \ + type.cpp \ + type.h \ + type_checker.h \ + type_node.cpp \ + type_node.h \ + variable_type_map.h \ + datatype.h \ + datatype.cpp \ + predicate.h \ + predicate.cpp \ + record.cpp \ + record.h \ + result.cpp \ + result.h \ + uninterpreted_constant.cpp \ + uninterpreted_constant.h nodist_libexpr_la_SOURCES = \ kind.h \ @@ -50,6 +84,12 @@ nodist_libexpr_la_SOURCES = \ type_checker.cpp EXTRA_DIST = \ + array.i \ + chain.i \ + array_store_all.i \ + ascription_type.i \ + datatype.i \ + emptyset.i \ kind_template.h \ metakind_template.h \ type_properties_template.h \ @@ -58,18 +98,23 @@ EXTRA_DIST = \ expr_template.h \ expr_template.cpp \ type_checker_template.cpp \ - options_handlers.h \ mkkind \ mkmetakind \ mkexpr \ expr_stream.i \ expr_manager.i \ symbol_table.i \ - command.i \ + statistics.i \ type.i \ kind.i \ expr.i \ - variable_type_map.i + resource_manager.i \ + sexpr.i \ + record.i \ + result.i \ + predicate.i \ + variable_type_map.i \ + uninterpreted_constant.i BUILT_SOURCES = \ kind.h \ diff --git a/src/expr/array.h b/src/expr/array.h new file mode 100644 index 000000000..ab554171f --- /dev/null +++ b/src/expr/array.h @@ -0,0 +1,26 @@ +/********************* */ +/*! \file array.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Array types. + ** + ** Array types. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__ARRAY_H +#define __CVC4__ARRAY_H + +// we get ArrayType right now by #including type.h. +// array.h is still useful for the auto-generated kinds #includes. +#include "expr/type.h" + +#endif /* __CVC4__ARRAY_H */ diff --git a/src/expr/array.i b/src/expr/array.i new file mode 100644 index 000000000..4acd7bf0c --- /dev/null +++ b/src/expr/array.i @@ -0,0 +1,5 @@ +%{ +#include "expr/array.h" +%} + +%include "expr/array.h" diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp new file mode 100644 index 000000000..62c8ec978 --- /dev/null +++ b/src/expr/array_store_all.cpp @@ -0,0 +1,31 @@ +/********************* */ +/*! \file array_store_all.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of a constant array (an array in which the + ** element is the same for all indices) + ** + ** Representation of a constant array (an array in which the element is + ** the same for all indices). + **/ + +#include "expr/array_store_all.h" + +#include <iostream> + +using namespace std; + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) { + return out << "__array_store_all__(" << asa.getType() << ", " << asa.getExpr() << ')'; +} + +}/* CVC4 namespace */ diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h new file mode 100644 index 000000000..b1d624266 --- /dev/null +++ b/src/expr/array_store_all.h @@ -0,0 +1,98 @@ +/********************* */ +/*! \file array_store_all.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of a constant array (an array in which the + ** element is the same for all indices) + ** + ** Representation of a constant array (an array in which the element is + ** the same for all indices). + **/ + +#include "cvc4_public.h" + +#pragma once + +namespace CVC4 { + // messy; Expr needs ArrayStoreAll (because it's the payload of a + // CONSTANT-kinded expression), and ArrayStoreAll needs Expr. + class CVC4_PUBLIC ArrayStoreAll; +}/* CVC4 namespace */ + +#include "expr/expr.h" +#include "expr/type.h" +#include <iostream> + +namespace CVC4 { + +class CVC4_PUBLIC ArrayStoreAll { + const ArrayType d_type; + const Expr d_expr; + +public: + + ArrayStoreAll(ArrayType type, Expr expr) throw(IllegalArgumentException) : + d_type(type), + d_expr(expr) { + + // this check is stronger than the assertion check in the expr manager that ArrayTypes are actually array types + // because this check is done in production builds too + CheckArgument(type.isArray(), type, "array store-all constants can only be created for array types, not `%s'", type.toString().c_str()); + + CheckArgument(expr.getType().isComparableTo(type.getConstituentType()), expr, "expr type `%s' does not match constituent type of array type `%s'", expr.getType().toString().c_str(), type.toString().c_str()); + CheckArgument(expr.isConst(), expr, "ArrayStoreAll requires a constant expression"); + } + + ~ArrayStoreAll() throw() { + } + + ArrayType getType() const throw() { + return d_type; + } + Expr getExpr() const throw() { + return d_expr; + } + + bool operator==(const ArrayStoreAll& asa) const throw() { + return d_type == asa.d_type && d_expr == asa.d_expr; + } + bool operator!=(const ArrayStoreAll& asa) const throw() { + return !(*this == asa); + } + + bool operator<(const ArrayStoreAll& asa) const throw() { + return d_type < asa.d_type || + (d_type == asa.d_type && d_expr < asa.d_expr); + } + bool operator<=(const ArrayStoreAll& asa) const throw() { + return d_type < asa.d_type || + (d_type == asa.d_type && d_expr <= asa.d_expr); + } + bool operator>(const ArrayStoreAll& asa) const throw() { + return !(*this <= asa); + } + bool operator>=(const ArrayStoreAll& asa) const throw() { + return !(*this < asa); + } + +};/* class ArrayStoreAll */ + +std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa) CVC4_PUBLIC; + +/** + * Hash function for the ArrayStoreAll constants. + */ +struct CVC4_PUBLIC ArrayStoreAllHashFunction { + inline size_t operator()(const ArrayStoreAll& asa) const { + return TypeHashFunction()(asa.getType()) * ExprHashFunction()(asa.getExpr()); + } +};/* struct ArrayStoreAllHashFunction */ + +}/* CVC4 namespace */ diff --git a/src/expr/array_store_all.i b/src/expr/array_store_all.i new file mode 100644 index 000000000..b66e4a178 --- /dev/null +++ b/src/expr/array_store_all.i @@ -0,0 +1,17 @@ +%{ +#include "expr/array_store_all.h" +%} + +%rename(equals) CVC4::ArrayStoreAll::operator==(const ArrayStoreAll&) const; +%ignore CVC4::ArrayStoreAll::operator!=(const ArrayStoreAll&) const; +%rename(less) CVC4::ArrayStoreAll::operator<(const ArrayStoreAll&) const; +%rename(lessEqual) CVC4::ArrayStoreAll::operator<=(const ArrayStoreAll&) const; +%rename(greater) CVC4::ArrayStoreAll::operator>(const ArrayStoreAll&) const; +%rename(greaterEqual) CVC4::ArrayStoreAll::operator>=(const ArrayStoreAll&) const; + +%rename(apply) CVC4::ArrayStoreAllHashFunction::operator()(const ArrayStoreAll&) const; + +%ignore CVC4::operator<<(std::ostream&, const ArrayStoreAll&); + +%include "expr/type.i" +%include "expr/array_store_all.h" diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h new file mode 100644 index 000000000..42906e557 --- /dev/null +++ b/src/expr/ascription_type.h @@ -0,0 +1,63 @@ +/********************* */ +/*! \file ascription_type.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A class representing a type ascription + ** + ** A class representing a parameter for the type ascription operator. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__ASCRIPTION_TYPE_H +#define __CVC4__ASCRIPTION_TYPE_H + +#include "expr/type.h" + +namespace CVC4 { + +/** + * A class used to parameterize a type ascription. For example, + * "nil :: list<nat>" is an expression of kind APPLY_TYPE_ASCRIPTION. + * The parameter is an ASCRIPTION_TYPE-kinded expression with an + * AscriptionType payload. (Essentially, all of this is a way to + * coerce a Type into the expression tree.) + */ +class CVC4_PUBLIC AscriptionType { + Type d_type; +public: + AscriptionType(Type t) throw() : d_type(t) {} + Type getType() const throw() { return d_type; } + bool operator==(const AscriptionType& other) const throw() { + return d_type == other.d_type; + } + bool operator!=(const AscriptionType& other) const throw() { + return d_type != other.d_type; + } +};/* class AscriptionType */ + +/** + * A hash function for type ascription operators. + */ +struct CVC4_PUBLIC AscriptionTypeHashFunction { + inline size_t operator()(const AscriptionType& at) const { + return TypeHashFunction()(at.getType()); + } +};/* struct AscriptionTypeHashFunction */ + +/** An output routine for AscriptionTypes */ +inline std::ostream& operator<<(std::ostream& out, AscriptionType at) { + out << at.getType(); + return out; +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__ASCRIPTION_TYPE_H */ diff --git a/src/expr/ascription_type.i b/src/expr/ascription_type.i new file mode 100644 index 000000000..57d8f97fe --- /dev/null +++ b/src/expr/ascription_type.i @@ -0,0 +1,12 @@ +%{ +#include "expr/ascription_type.h" +%} + +%rename(equals) CVC4::AscriptionType::operator==(const AscriptionType&) const; +%ignore CVC4::AscriptionType::operator!=(const AscriptionType&) const; + +%rename(apply) CVC4::AscriptionTypeHashFunction::operator()(const AscriptionType&) const; + +%ignore CVC4::operator<<(std::ostream&, AscriptionType); + +%include "expr/ascription_type.h" diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 63ea770ca..cd5b35384 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -13,14 +13,13 @@ ** ** AttributeManager implementation. **/ +#include <utility> +#include "base/output.h" #include "expr/attribute.h" #include "expr/node_value.h" -#include "util/output.h" #include "smt/smt_engine.h" -#include <utility> - using namespace std; namespace CVC4 { diff --git a/src/expr/chain.h b/src/expr/chain.h new file mode 100644 index 000000000..e052a2ed8 --- /dev/null +++ b/src/expr/chain.h @@ -0,0 +1,51 @@ +/********************* */ +/*! \file chain.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__CHAIN_H +#define __CVC4__CHAIN_H + +#include "expr/kind.h" +#include <iostream> + +namespace CVC4 { + +/** A class to represent a chained, built-in operator. */ +class CVC4_PUBLIC Chain { + Kind d_kind; +public: + explicit Chain(Kind k) : d_kind(k) { } + bool operator==(const Chain& ch) const { return d_kind == ch.d_kind; } + bool operator!=(const Chain& ch) const { return d_kind != ch.d_kind; } + Kind getOperator() const { return d_kind; } +};/* class Chain */ + +inline std::ostream& operator<<(std::ostream& out, const Chain& ch) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& out, const Chain& ch) { + return out << ch.getOperator(); +} + +struct CVC4_PUBLIC ChainHashFunction { + size_t operator()(const Chain& ch) const { + return kind::KindHashFunction()(ch.getOperator()); + } +};/* struct ChainHashFunction */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__CHAIN_H */ diff --git a/src/expr/chain.i b/src/expr/chain.i new file mode 100644 index 000000000..8de1665ce --- /dev/null +++ b/src/expr/chain.i @@ -0,0 +1,12 @@ +%{ +#include "expr/chain.h" +%} + +%rename(equals) CVC4::Chain::operator==(const Chain&) const; +%ignore CVC4::Chain::operator!=(const Chain&) const; + +%ignore CVC4::operator<<(std::ostream&, const Chain&); + +%rename(apply) CVC4::ChainHashFunction::operator()(const CVC4::Chain&) const; + +%include "expr/chain.h" diff --git a/src/expr/command.cpp b/src/expr/command.cpp deleted file mode 100644 index 1c7c1d171..000000000 --- a/src/expr/command.cpp +++ /dev/null @@ -1,1849 +0,0 @@ -/********************* */ -/*! \file command.cpp - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic, Andrew Reynolds, Francois Bobot - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of command objects. - ** - ** Implementation of command objects. - **/ - -#include <iostream> -#include <vector> -#include <utility> -#include <iterator> -#include <sstream> -#include <exception> - -#include "expr/command.h" -#include "smt/smt_engine.h" -#include "options/options.h" -#include "smt/options.h" -#include "smt/smt_engine_scope.h" -#include "util/output.h" -#include "util/dump.h" -#include "util/sexpr.h" -#include "util/model.h" -#include "expr/node.h" -#include "printer/printer.h" - -using namespace std; - -namespace CVC4 { - -const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc(); -const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess(); -const CommandInterrupted* CommandInterrupted::s_instance = new CommandInterrupted(); - -std::ostream& operator<<(std::ostream& out, const Command& c) throw() { - c.toStream(out, - Node::setdepth::getDepth(out), - Node::printtypes::getPrintTypes(out), - Node::dag::getDag(out), - Node::setlanguage::getLanguage(out)); - return out; -} - -ostream& operator<<(ostream& out, const Command* c) throw() { - if(c == NULL) { - out << "null"; - } else { - out << *c; - } - return out; -} - -std::ostream& operator<<(std::ostream& out, const CommandStatus& s) throw() { - s.toStream(out, Node::setlanguage::getLanguage(out)); - return out; -} - -ostream& operator<<(ostream& out, const CommandStatus* s) throw() { - if(s == NULL) { - out << "null"; - } else { - out << *s; - } - return out; -} - -/* class Command */ - -Command::Command() throw() : d_commandStatus(NULL), d_muted(false) { -} - -Command::Command(const Command& cmd) { - d_commandStatus = (cmd.d_commandStatus == NULL) ? NULL : &cmd.d_commandStatus->clone(); - d_muted = cmd.d_muted; -} - -Command::~Command() throw() { - if(d_commandStatus != NULL && d_commandStatus != CommandSuccess::instance()) { - delete d_commandStatus; - } -} - -bool Command::ok() const throw() { - // either we haven't run the command yet, or it ran successfully - return d_commandStatus == NULL || dynamic_cast<const CommandSuccess*>(d_commandStatus) != NULL; -} - -bool Command::fail() const throw() { - return d_commandStatus != NULL && dynamic_cast<const CommandFailure*>(d_commandStatus) != NULL; -} - -bool Command::interrupted() const throw() { - return d_commandStatus != NULL && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL; -} - -void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { - invoke(smtEngine); - if(!(isMuted() && ok())) { - printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt()); - } -} - -std::string Command::toString() const throw() { - std::stringstream ss; - toStream(ss); - return ss.str(); -} - -void Command::toStream(std::ostream& out, int toDepth, bool types, size_t dag, - OutputLanguage language) const throw() { - Printer::getPrinter(language)->toStream(out, this, toDepth, types, dag); -} - -void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const throw() { - Printer::getPrinter(language)->toStream(out, this); -} - -void Command::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(d_commandStatus != NULL) { - if((!ok() && verbosity >= 1) || verbosity >= 2) { - out << *d_commandStatus; - } - } -} - -/* class EmptyCommand */ - -EmptyCommand::EmptyCommand(std::string name) throw() : - d_name(name) { -} - -std::string EmptyCommand::getName() const throw() { - return d_name; -} - -void EmptyCommand::invoke(SmtEngine* smtEngine) throw() { - /* empty commands have no implementation */ - d_commandStatus = CommandSuccess::instance(); -} - -Command* EmptyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new EmptyCommand(d_name); -} - -Command* EmptyCommand::clone() const { - return new EmptyCommand(d_name); -} - -std::string EmptyCommand::getCommandName() const throw() { - return "empty"; -} - -/* class EchoCommand */ - -EchoCommand::EchoCommand(std::string output) throw() : - d_output(output) { -} - -std::string EchoCommand::getOutput() const throw() { - return d_output; -} - -void EchoCommand::invoke(SmtEngine* smtEngine) throw() { - /* we don't have an output stream here, nothing to do */ - d_commandStatus = CommandSuccess::instance(); -} - -void EchoCommand::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { - out << d_output << std::endl; - d_commandStatus = CommandSuccess::instance(); - printResult(out, smtEngine->getOption("command-verbosity:" + getCommandName()).getIntegerValue().toUnsignedInt()); -} - -Command* EchoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new EchoCommand(d_output); -} - -Command* EchoCommand::clone() const { - return new EchoCommand(d_output); -} - -std::string EchoCommand::getCommandName() const throw() { - return "echo"; -} - -/* class AssertCommand */ - -AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore) throw() : - d_expr(e), d_inUnsatCore(inUnsatCore) { -} - -Expr AssertCommand::getExpr() const throw() { - return d_expr; -} - -void AssertCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->assertFormula(d_expr, d_inUnsatCore); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new AssertCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); -} - -Command* AssertCommand::clone() const { - return new AssertCommand(d_expr, d_inUnsatCore); -} - -std::string AssertCommand::getCommandName() const throw() { - return "assert"; -} - -/* class PushCommand */ - -void PushCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->push(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* PushCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new PushCommand(); -} - -Command* PushCommand::clone() const { - return new PushCommand(); -} - -std::string PushCommand::getCommandName() const throw() { - return "push"; -} - -/* class PopCommand */ - -void PopCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->pop(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new PopCommand(); -} - -Command* PopCommand::clone() const { - return new PopCommand(); -} - -std::string PopCommand::getCommandName() const throw() { - return "pop"; -} - -/* class CheckSatCommand */ - -CheckSatCommand::CheckSatCommand() throw() : - d_expr() { -} - -CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore) throw() : - d_expr(expr), d_inUnsatCore(inUnsatCore) { -} - -Expr CheckSatCommand::getExpr() const throw() { - return d_expr; -} - -void CheckSatCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->checkSat(d_expr); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Result CheckSatCommand::getResult() const throw() { - return d_result; -} - -void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result << endl; - } -} - -Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); - c->d_result = d_result; - return c; -} - -Command* CheckSatCommand::clone() const { - CheckSatCommand* c = new CheckSatCommand(d_expr, d_inUnsatCore); - c->d_result = d_result; - return c; -} - -std::string CheckSatCommand::getCommandName() const throw() { - return "check-sat"; -} - -/* class QueryCommand */ - -QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore) throw() : - d_expr(e), d_inUnsatCore(inUnsatCore) { -} - -Expr QueryCommand::getExpr() const throw() { - return d_expr; -} - -void QueryCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->query(d_expr); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Result QueryCommand::getResult() const throw() { - return d_result; -} - -void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result << endl; - } -} - -Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore); - c->d_result = d_result; - return c; -} - -Command* QueryCommand::clone() const { - QueryCommand* c = new QueryCommand(d_expr, d_inUnsatCore); - c->d_result = d_result; - return c; -} - -std::string QueryCommand::getCommandName() const throw() { - return "query"; -} - -/* class ResetCommand */ - -void ResetCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->reset(); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* ResetCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new ResetCommand(); -} - -Command* ResetCommand::clone() const { - return new ResetCommand(); -} - -std::string ResetCommand::getCommandName() const throw() { - return "reset"; -} - -/* class ResetAssertionsCommand */ - -void ResetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->resetAssertions(); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* ResetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new ResetAssertionsCommand(); -} - -Command* ResetAssertionsCommand::clone() const { - return new ResetAssertionsCommand(); -} - -std::string ResetAssertionsCommand::getCommandName() const throw() { - return "reset-assertions"; -} - -/* class QuitCommand */ - -void QuitCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("benchmark") << *this; - d_commandStatus = CommandSuccess::instance(); -} - -Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new QuitCommand(); -} - -Command* QuitCommand::clone() const { - return new QuitCommand(); -} - -std::string QuitCommand::getCommandName() const throw() { - return "exit"; -} - -/* class CommentCommand */ - -CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) { -} - -std::string CommentCommand::getComment() const throw() { - return d_comment; -} - -void CommentCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("benchmark") << *this; - d_commandStatus = CommandSuccess::instance(); -} - -Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new CommentCommand(d_comment); -} - -Command* CommentCommand::clone() const { - return new CommentCommand(d_comment); -} - -std::string CommentCommand::getCommandName() const throw() { - return "comment"; -} - -/* class CommandSequence */ - -CommandSequence::CommandSequence() throw() : - d_index(0) { -} - -CommandSequence::~CommandSequence() throw() { - for(unsigned i = d_index; i < d_commandSequence.size(); ++i) { - delete d_commandSequence[i]; - } -} - -void CommandSequence::addCommand(Command* cmd) throw() { - d_commandSequence.push_back(cmd); -} - -void CommandSequence::clear() throw() { - d_commandSequence.clear(); -} - -void CommandSequence::invoke(SmtEngine* smtEngine) throw() { - for(; d_index < d_commandSequence.size(); ++d_index) { - d_commandSequence[d_index]->invoke(smtEngine); - if(! d_commandSequence[d_index]->ok()) { - // abort execution - d_commandStatus = d_commandSequence[d_index]->getCommandStatus(); - return; - } - delete d_commandSequence[d_index]; - } - - AlwaysAssert(d_commandStatus == NULL); - d_commandStatus = CommandSuccess::instance(); -} - -void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { - for(; d_index < d_commandSequence.size(); ++d_index) { - d_commandSequence[d_index]->invoke(smtEngine, out); - if(! d_commandSequence[d_index]->ok()) { - // abort execution - d_commandStatus = d_commandSequence[d_index]->getCommandStatus(); - return; - } - delete d_commandSequence[d_index]; - } - - AlwaysAssert(d_commandStatus == NULL); - d_commandStatus = CommandSuccess::instance(); -} - -Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - CommandSequence* seq = new CommandSequence(); - for(iterator i = begin(); i != end(); ++i) { - Command* cmd_to_export = *i; - Command* cmd = cmd_to_export->exportTo(exprManager, variableMap); - seq->addCommand(cmd); - Debug("export") << "[export] so far converted: " << seq << endl; - } - seq->d_index = d_index; - return seq; -} - -Command* CommandSequence::clone() const { - CommandSequence* seq = new CommandSequence(); - for(const_iterator i = begin(); i != end(); ++i) { - seq->addCommand((*i)->clone()); - } - seq->d_index = d_index; - return seq; -} - -CommandSequence::const_iterator CommandSequence::begin() const throw() { - return d_commandSequence.begin(); -} - -CommandSequence::const_iterator CommandSequence::end() const throw() { - return d_commandSequence.end(); -} - -CommandSequence::iterator CommandSequence::begin() throw() { - return d_commandSequence.begin(); -} - -CommandSequence::iterator CommandSequence::end() throw() { - return d_commandSequence.end(); -} - -std::string CommandSequence::getCommandName() const throw() { - return "sequence"; -} - -/* class DeclarationSequenceCommand */ - -/* class DeclarationDefinitionCommand */ - -DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) throw() : - d_symbol(id) { -} - -std::string DeclarationDefinitionCommand::getSymbol() const throw() { - return d_symbol; -} - -/* class DeclareFunctionCommand */ - -DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Expr func, Type t) throw() : - DeclarationDefinitionCommand(id), - d_func(func), - d_type(t), - d_printInModel(true), - d_printInModelSetByUser(false){ -} - -Expr DeclareFunctionCommand::getFunction() const throw() { - return d_func; -} - -Type DeclareFunctionCommand::getType() const throw() { - return d_type; -} - -bool DeclareFunctionCommand::getPrintInModel() const throw() { - return d_printInModel; -} - -bool DeclareFunctionCommand::getPrintInModelSetByUser() const throw() { - return d_printInModelSetByUser; -} - -void DeclareFunctionCommand::setPrintInModel( bool p ) { - d_printInModel = p; - d_printInModelSetByUser = true; -} - -void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { - d_commandStatus = CommandSuccess::instance(); -} - -Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) { - DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func.exportTo(exprManager, variableMap), - d_type.exportTo(exprManager, variableMap)); - dfc->d_printInModel = d_printInModel; - dfc->d_printInModelSetByUser = d_printInModelSetByUser; - return dfc; -} - -Command* DeclareFunctionCommand::clone() const { - DeclareFunctionCommand * dfc = new DeclareFunctionCommand(d_symbol, d_func, d_type); - dfc->d_printInModel = d_printInModel; - dfc->d_printInModelSetByUser = d_printInModelSetByUser; - return dfc; -} - -std::string DeclareFunctionCommand::getCommandName() const throw() { - return "declare-fun"; -} - -/* class DeclareTypeCommand */ - -DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() : - DeclarationDefinitionCommand(id), - d_arity(arity), - d_type(t) { -} - -size_t DeclareTypeCommand::getArity() const throw() { - return d_arity; -} - -Type DeclareTypeCommand::getType() const throw() { - return d_type; -} - -void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() { - d_commandStatus = CommandSuccess::instance(); -} - -Command* DeclareTypeCommand::exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) { - return new DeclareTypeCommand(d_symbol, d_arity, - d_type.exportTo(exprManager, variableMap)); -} - -Command* DeclareTypeCommand::clone() const { - return new DeclareTypeCommand(d_symbol, d_arity, d_type); -} - -std::string DeclareTypeCommand::getCommandName() const throw() { - return "declare-sort"; -} - -/* class DefineTypeCommand */ - -DefineTypeCommand::DefineTypeCommand(const std::string& id, - Type t) throw() : - DeclarationDefinitionCommand(id), - d_params(), - d_type(t) { -} - -DefineTypeCommand::DefineTypeCommand(const std::string& id, - const std::vector<Type>& params, - Type t) throw() : - DeclarationDefinitionCommand(id), - d_params(params), - d_type(t) { -} - -const std::vector<Type>& DefineTypeCommand::getParameters() const throw() { - return d_params; -} - -Type DefineTypeCommand::getType() const throw() { - return d_type; -} - -void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() { - d_commandStatus = CommandSuccess::instance(); -} - -Command* DefineTypeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - vector<Type> params; - transform(d_params.begin(), d_params.end(), back_inserter(params), - ExportTransformer(exprManager, variableMap)); - Type type = d_type.exportTo(exprManager, variableMap); - return new DefineTypeCommand(d_symbol, params, type); -} - -Command* DefineTypeCommand::clone() const { - return new DefineTypeCommand(d_symbol, d_params, d_type); -} - -std::string DefineTypeCommand::getCommandName() const throw() { - return "define-sort"; -} - -/* class DefineFunctionCommand */ - -DefineFunctionCommand::DefineFunctionCommand(const std::string& id, - Expr func, - Expr formula) throw() : - DeclarationDefinitionCommand(id), - d_func(func), - d_formals(), - d_formula(formula) { -} - -DefineFunctionCommand::DefineFunctionCommand(const std::string& id, - Expr func, - const std::vector<Expr>& formals, - Expr formula) throw() : - DeclarationDefinitionCommand(id), - d_func(func), - d_formals(formals), - d_formula(formula) { -} - -Expr DefineFunctionCommand::getFunction() const throw() { - return d_func; -} - -const std::vector<Expr>& DefineFunctionCommand::getFormals() const throw() { - return d_formals; -} - -Expr DefineFunctionCommand::getFormula() const throw() { - return d_formula; -} - -void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() { - try { - if(!d_func.isNull()) { - smtEngine->defineFunction(d_func, d_formals, d_formula); - } - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - Expr func = d_func.exportTo(exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED); - vector<Expr> formals; - transform(d_formals.begin(), d_formals.end(), back_inserter(formals), - ExportTransformer(exprManager, variableMap)); - Expr formula = d_formula.exportTo(exprManager, variableMap); - return new DefineFunctionCommand(d_symbol, func, formals, formula); -} - -Command* DefineFunctionCommand::clone() const { - return new DefineFunctionCommand(d_symbol, d_func, d_formals, d_formula); -} - -std::string DefineFunctionCommand::getCommandName() const throw() { - return "define-fun"; -} - -/* class DefineNamedFunctionCommand */ - -DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id, - Expr func, - const std::vector<Expr>& formals, - Expr formula) throw() : - DefineFunctionCommand(id, func, formals, formula) { -} - -void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() { - this->DefineFunctionCommand::invoke(smtEngine); - if(!d_func.isNull() && d_func.getType().isBoolean()) { - smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, d_func)); - } - d_commandStatus = CommandSuccess::instance(); -} - -Command* DefineNamedFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - Expr func = d_func.exportTo(exprManager, variableMap); - vector<Expr> formals; - transform(d_formals.begin(), d_formals.end(), back_inserter(formals), - ExportTransformer(exprManager, variableMap)); - Expr formula = d_formula.exportTo(exprManager, variableMap); - return new DefineNamedFunctionCommand(d_symbol, func, formals, formula); -} - -Command* DefineNamedFunctionCommand::clone() const { - return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula); -} - -/* class SetUserAttribute */ - -SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr ) throw() : - d_attr( attr ), d_expr( expr ){ -} - -SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr, - std::vector<Expr>& values ) throw() : - d_attr( attr ), d_expr( expr ){ - d_expr_values.insert( d_expr_values.begin(), values.begin(), values.end() ); -} - -SetUserAttributeCommand::SetUserAttributeCommand( const std::string& attr, Expr expr, - const std::string& value ) throw() : - d_attr( attr ), d_expr( expr ), d_str_value( value ){ -} - -void SetUserAttributeCommand::invoke(SmtEngine* smtEngine) throw(){ - try { - if(!d_expr.isNull()) { - smtEngine->setUserAttribute( d_attr, d_expr, d_expr_values, d_str_value ); - } - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* SetUserAttributeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap){ - Expr expr = d_expr.exportTo(exprManager, variableMap); - SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, expr, d_str_value ); - c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() ); - return c; -} - -Command* SetUserAttributeCommand::clone() const{ - SetUserAttributeCommand * c = new SetUserAttributeCommand( d_attr, d_expr, d_str_value ); - c->d_expr_values.insert( c->d_expr_values.end(), d_expr_values.begin(), d_expr_values.end() ); - return c; -} - -std::string SetUserAttributeCommand::getCommandName() const throw() { - return "set-user-attribute"; -} - -/* class SimplifyCommand */ - -SimplifyCommand::SimplifyCommand(Expr term) throw() : - d_term(term) { -} - -Expr SimplifyCommand::getTerm() const throw() { - return d_term; -} - -void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->simplify(d_term); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Expr SimplifyCommand::getResult() const throw() { - return d_result; -} - -void SimplifyCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result << endl; - } -} - -Command* SimplifyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - SimplifyCommand* c = new SimplifyCommand(d_term.exportTo(exprManager, variableMap)); - c->d_result = d_result.exportTo(exprManager, variableMap); - return c; -} - -Command* SimplifyCommand::clone() const { - SimplifyCommand* c = new SimplifyCommand(d_term); - c->d_result = d_result; - return c; -} - -std::string SimplifyCommand::getCommandName() const throw() { - return "simplify"; -} - -/* class ExpandDefinitionsCommand */ - -ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term) throw() : - d_term(term) { -} - -Expr ExpandDefinitionsCommand::getTerm() const throw() { - return d_term; -} - -void ExpandDefinitionsCommand::invoke(SmtEngine* smtEngine) throw() { - d_result = smtEngine->expandDefinitions(d_term); - d_commandStatus = CommandSuccess::instance(); -} - -Expr ExpandDefinitionsCommand::getResult() const throw() { - return d_result; -} - -void ExpandDefinitionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result << endl; - } -} - -Command* ExpandDefinitionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term.exportTo(exprManager, variableMap)); - c->d_result = d_result.exportTo(exprManager, variableMap); - return c; -} - -Command* ExpandDefinitionsCommand::clone() const { - ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term); - c->d_result = d_result; - return c; -} - -std::string ExpandDefinitionsCommand::getCommandName() const throw() { - return "expand-definitions"; -} - -/* class GetValueCommand */ - -GetValueCommand::GetValueCommand(Expr term) throw() : - d_terms() { - d_terms.push_back(term); -} - -GetValueCommand::GetValueCommand(const std::vector<Expr>& terms) throw() : - d_terms(terms) { - CheckArgument(terms.size() >= 1, terms, "cannot get-value of an empty set of terms"); -} - -const std::vector<Expr>& GetValueCommand::getTerms() const throw() { - return d_terms; -} - -void GetValueCommand::invoke(SmtEngine* smtEngine) throw() { - try { - vector<Expr> result; - ExprManager* em = smtEngine->getExprManager(); - NodeManager* nm = NodeManager::fromExprManager(em); - for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) { - Assert(nm == NodeManager::fromExprManager((*i).getExprManager())); - smt::SmtScope scope(smtEngine); - Node request = Node::fromExpr(options::expandDefinitions() ? smtEngine->expandDefinitions(*i) : *i); - Node value = Node::fromExpr(smtEngine->getValue(*i)); - if(value.getType().isInteger() && request.getType() == nm->realType()) { - // Need to wrap in special marker so that output printers know this - // is an integer-looking constant that really should be output as - // a rational. Necessary for SMT-LIB standards compliance, but ugly. - value = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, - nm->mkConst(AscriptionType(em->realType())), value); - } - result.push_back(nm->mkNode(kind::SEXPR, request, value).toExpr()); - } - d_result = em->mkExpr(kind::SEXPR, result); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Expr GetValueCommand::getResult() const throw() { - return d_result; -} - -void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - Expr::dag::Scope scope(out, false); - out << d_result << endl; - } -} - -Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - vector<Expr> exportedTerms; - for(std::vector<Expr>::const_iterator i = d_terms.begin(); i != d_terms.end(); ++i) { - exportedTerms.push_back((*i).exportTo(exprManager, variableMap)); - } - GetValueCommand* c = new GetValueCommand(exportedTerms); - c->d_result = d_result.exportTo(exprManager, variableMap); - return c; -} - -Command* GetValueCommand::clone() const { - GetValueCommand* c = new GetValueCommand(d_terms); - c->d_result = d_result; - return c; -} - -std::string GetValueCommand::getCommandName() const throw() { - return "get-value"; -} - -/* class GetAssignmentCommand */ - -GetAssignmentCommand::GetAssignmentCommand() throw() { -} - -void GetAssignmentCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->getAssignment(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -SExpr GetAssignmentCommand::getResult() const throw() { - return d_result; -} - -void GetAssignmentCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result << endl; - } -} - -Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetAssignmentCommand* c = new GetAssignmentCommand(); - c->d_result = d_result; - return c; -} - -Command* GetAssignmentCommand::clone() const { - GetAssignmentCommand* c = new GetAssignmentCommand(); - c->d_result = d_result; - return c; -} - -std::string GetAssignmentCommand::getCommandName() const throw() { - return "get-assignment"; -} - -/* class GetModelCommand */ - -GetModelCommand::GetModelCommand() throw() { -} - -void GetModelCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->getModel(); - d_smtEngine = smtEngine; - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -/* Model is private to the library -- for now -Model* GetModelCommand::getResult() const throw() { - return d_result; -} -*/ - -void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << *d_result; - } -} - -Command* GetModelCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetModelCommand* c = new GetModelCommand(); - c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - -Command* GetModelCommand::clone() const { - GetModelCommand* c = new GetModelCommand(); - c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - -std::string GetModelCommand::getCommandName() const throw() { - return "get-model"; -} - -/* class GetProofCommand */ - -GetProofCommand::GetProofCommand() throw() { -} - -void GetProofCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->getProof(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnsafeInterruptException& e) { - d_commandStatus = new CommandInterrupted(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Proof* GetProofCommand::getResult() const throw() { - return d_result; -} - -void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - d_result->toStream(out); - } -} - -Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetProofCommand* c = new GetProofCommand(); - c->d_result = d_result; - return c; -} - -Command* GetProofCommand::clone() const { - GetProofCommand* c = new GetProofCommand(); - c->d_result = d_result; - return c; -} - -std::string GetProofCommand::getCommandName() const throw() { - return "get-proof"; -} - -/* class GetInstantiationsCommand */ - -GetInstantiationsCommand::GetInstantiationsCommand() throw() { -} - -void GetInstantiationsCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_smtEngine = smtEngine; - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -//Instantiations* GetInstantiationsCommand::getResult() const throw() { -// return d_result; -//} - -void GetInstantiationsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - d_smtEngine->printInstantiations(out); - } -} - -Command* GetInstantiationsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetInstantiationsCommand* c = new GetInstantiationsCommand(); - //c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - -Command* GetInstantiationsCommand::clone() const { - GetInstantiationsCommand* c = new GetInstantiationsCommand(); - //c->d_result = d_result; - c->d_smtEngine = d_smtEngine; - return c; -} - -std::string GetInstantiationsCommand::getCommandName() const throw() { - return "get-instantiations"; -} - -/* class GetSynthSolutionCommand */ - -GetSynthSolutionCommand::GetSynthSolutionCommand() throw() { -} - -void GetSynthSolutionCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_smtEngine = smtEngine; - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -void GetSynthSolutionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - d_smtEngine->printSynthSolution(out); - } -} - -Command* GetSynthSolutionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetSynthSolutionCommand* c = new GetSynthSolutionCommand(); - c->d_smtEngine = d_smtEngine; - return c; -} - -Command* GetSynthSolutionCommand::clone() const { - GetSynthSolutionCommand* c = new GetSynthSolutionCommand(); - c->d_smtEngine = d_smtEngine; - return c; -} - -std::string GetSynthSolutionCommand::getCommandName() const throw() { - return "get-instantiations"; -} - -/* class GetUnsatCoreCommand */ - -GetUnsatCoreCommand::GetUnsatCoreCommand() throw() { -} - -GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw() : d_names(names) { -} - -void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() { - try { - d_result = smtEngine->getUnsatCore(); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - d_result.toStream(out, d_names); - } -} - -const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const throw() { - // of course, this will be empty if the command hasn't been invoked yet - return d_result; -} - -Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); - c->d_result = d_result; - return c; -} - -Command* GetUnsatCoreCommand::clone() const { - GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names); - c->d_result = d_result; - return c; -} - -std::string GetUnsatCoreCommand::getCommandName() const throw() { - return "get-unsat-core"; -} - -/* class GetAssertionsCommand */ - -GetAssertionsCommand::GetAssertionsCommand() throw() { -} - -void GetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() { - try { - stringstream ss; - const vector<Expr> v = smtEngine->getAssertions(); - ss << "(\n"; - copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") ); - ss << ")\n"; - d_result = ss.str(); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -std::string GetAssertionsCommand::getResult() const throw() { - return d_result; -} - -void GetAssertionsCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else { - out << d_result; - } -} - -Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetAssertionsCommand* c = new GetAssertionsCommand(); - c->d_result = d_result; - return c; -} - -Command* GetAssertionsCommand::clone() const { - GetAssertionsCommand* c = new GetAssertionsCommand(); - c->d_result = d_result; - return c; -} - -std::string GetAssertionsCommand::getCommandName() const throw() { - return "get-assertions"; -} - -/* class SetBenchmarkStatusCommand */ - -SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() : - d_status(status) { -} - -BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() { - return d_status; -} - -void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() { - try { - stringstream ss; - ss << d_status; - SExpr status = ss.str(); - smtEngine->setInfo("status", status); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new SetBenchmarkStatusCommand(d_status); -} - -Command* SetBenchmarkStatusCommand::clone() const { - return new SetBenchmarkStatusCommand(d_status); -} - -std::string SetBenchmarkStatusCommand::getCommandName() const throw() { - return "set-info"; -} - -/* class SetBenchmarkLogicCommand */ - -SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() : - d_logic(logic) { -} - -std::string SetBenchmarkLogicCommand::getLogic() const throw() { - return d_logic; -} - -void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->setLogic(d_logic); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new SetBenchmarkLogicCommand(d_logic); -} - -Command* SetBenchmarkLogicCommand::clone() const { - return new SetBenchmarkLogicCommand(d_logic); -} - -std::string SetBenchmarkLogicCommand::getCommandName() const throw() { - return "set-logic"; -} - -/* class SetInfoCommand */ - -SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() : - d_flag(flag), - d_sexpr(sexpr) { -} - -std::string SetInfoCommand::getFlag() const throw() { - return d_flag; -} - -SExpr SetInfoCommand::getSExpr() const throw() { - return d_sexpr; -} - -void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->setInfo(d_flag, d_sexpr); - d_commandStatus = CommandSuccess::instance(); - } catch(UnrecognizedOptionException&) { - // As per SMT-LIB spec, silently accept unknown set-info keys - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new SetInfoCommand(d_flag, d_sexpr); -} - -Command* SetInfoCommand::clone() const { - return new SetInfoCommand(d_flag, d_sexpr); -} - -std::string SetInfoCommand::getCommandName() const throw() { - return "set-info"; -} - -/* class GetInfoCommand */ - -GetInfoCommand::GetInfoCommand(std::string flag) throw() : - d_flag(flag) { -} - -std::string GetInfoCommand::getFlag() const throw() { - return d_flag; -} - -void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() { - try { - vector<SExpr> v; - v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag))); - v.push_back(smtEngine->getInfo(d_flag)); - stringstream ss; - if(d_flag == "all-options" || d_flag == "all-statistics") { - ss << PrettySExprs(true); - } - ss << SExpr(v); - d_result = ss.str(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnrecognizedOptionException&) { - d_commandStatus = new CommandUnsupported(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -std::string GetInfoCommand::getResult() const throw() { - return d_result; -} - -void GetInfoCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else if(d_result != "") { - out << d_result << endl; - } -} - -Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetInfoCommand* c = new GetInfoCommand(d_flag); - c->d_result = d_result; - return c; -} - -Command* GetInfoCommand::clone() const { - GetInfoCommand* c = new GetInfoCommand(d_flag); - c->d_result = d_result; - return c; -} - -std::string GetInfoCommand::getCommandName() const throw() { - return "get-info"; -} - -/* class SetOptionCommand */ - -SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() : - d_flag(flag), - d_sexpr(sexpr) { -} - -std::string SetOptionCommand::getFlag() const throw() { - return d_flag; -} - -SExpr SetOptionCommand::getSExpr() const throw() { - return d_sexpr; -} - -void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() { - try { - smtEngine->setOption(d_flag, d_sexpr); - d_commandStatus = CommandSuccess::instance(); - } catch(UnrecognizedOptionException&) { - d_commandStatus = new CommandUnsupported(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - return new SetOptionCommand(d_flag, d_sexpr); -} - -Command* SetOptionCommand::clone() const { - return new SetOptionCommand(d_flag, d_sexpr); -} - -std::string SetOptionCommand::getCommandName() const throw() { - return "set-option"; -} - -/* class GetOptionCommand */ - -GetOptionCommand::GetOptionCommand(std::string flag) throw() : - d_flag(flag) { -} - -std::string GetOptionCommand::getFlag() const throw() { - return d_flag; -} - -void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() { - try { - SExpr res = smtEngine->getOption(d_flag); - stringstream ss; - ss << res; - d_result = ss.str(); - d_commandStatus = CommandSuccess::instance(); - } catch(UnrecognizedOptionException&) { - d_commandStatus = new CommandUnsupported(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -std::string GetOptionCommand::getResult() const throw() { - return d_result; -} - -void GetOptionCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { - if(! ok()) { - this->Command::printResult(out, verbosity); - } else if(d_result != "") { - out << d_result << endl; - } -} - -Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - GetOptionCommand* c = new GetOptionCommand(d_flag); - c->d_result = d_result; - return c; -} - -Command* GetOptionCommand::clone() const { - GetOptionCommand* c = new GetOptionCommand(d_flag); - c->d_result = d_result; - return c; -} - -std::string GetOptionCommand::getCommandName() const throw() { - return "get-option"; -} - -/* class DatatypeDeclarationCommand */ - -DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() : - d_datatypes() { - d_datatypes.push_back(datatype); -} - -DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw() : - d_datatypes(datatypes) { -} - -const std::vector<DatatypeType>& -DatatypeDeclarationCommand::getDatatypes() const throw() { - return d_datatypes; -} - -void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { - d_commandStatus = CommandSuccess::instance(); -} - -Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - throw ExportUnsupportedException - ("export of DatatypeDeclarationCommand unsupported"); -} - -Command* DatatypeDeclarationCommand::clone() const { - return new DatatypeDeclarationCommand(d_datatypes); -} - -std::string DatatypeDeclarationCommand::getCommandName() const throw() { - return "declare-datatypes"; -} - -/* class RewriteRuleCommand */ - -RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& guards, - Expr head, Expr body, - const Triggers& triggers) throw() : - d_vars(vars), d_guards(guards), d_head(head), d_body(body), d_triggers(triggers) { -} - -RewriteRuleCommand::RewriteRuleCommand(const std::vector<Expr>& vars, - Expr head, Expr body) throw() : - d_vars(vars), d_head(head), d_body(body) { -} - -const std::vector<Expr>& RewriteRuleCommand::getVars() const throw() { - return d_vars; -} - -const std::vector<Expr>& RewriteRuleCommand::getGuards() const throw() { - return d_guards; -} - -Expr RewriteRuleCommand::getHead() const throw() { - return d_head; -} - -Expr RewriteRuleCommand::getBody() const throw() { - return d_body; -} - -const RewriteRuleCommand::Triggers& RewriteRuleCommand::getTriggers() const throw() { - return d_triggers; -} - -void RewriteRuleCommand::invoke(SmtEngine* smtEngine) throw() { - try { - ExprManager* em = smtEngine->getExprManager(); - /** build vars list */ - Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars); - /** build guards list */ - Expr guards; - if(d_guards.size() == 0) guards = em->mkConst<bool>(true); - else if(d_guards.size() == 1) guards = d_guards[0]; - else guards = em->mkExpr(kind::AND,d_guards); - /** build expression */ - Expr expr; - if( d_triggers.empty() ){ - expr = em->mkExpr(kind::RR_REWRITE,vars,guards,d_head,d_body); - } else { - /** build triggers list */ - std::vector<Expr> vtriggers; - vtriggers.reserve(d_triggers.size()); - for(Triggers::const_iterator i = d_triggers.begin(), - end = d_triggers.end(); i != end; ++i){ - vtriggers.push_back(em->mkExpr(kind::INST_PATTERN,*i)); - } - Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST,vtriggers); - expr = em->mkExpr(kind::RR_REWRITE,vars,guards,d_head,d_body,triggers); - } - smtEngine->assertFormula(expr); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* RewriteRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - /** Convert variables */ - VExpr vars; vars.reserve(d_vars.size()); - for(VExpr::iterator i = d_vars.begin(), end = d_vars.end(); - i == end; ++i){ - vars.push_back(i->exportTo(exprManager, variableMap)); - }; - /** Convert guards */ - VExpr guards; guards.reserve(d_guards.size()); - for(VExpr::iterator i = d_guards.begin(), end = d_guards.end(); - i == end; ++i){ - guards.push_back(i->exportTo(exprManager, variableMap)); - }; - /** Convert triggers */ - Triggers triggers; triggers.resize(d_triggers.size()); - for(size_t i = 0, end = d_triggers.size(); - i < end; ++i){ - triggers[i].reserve(d_triggers[i].size()); - for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end(); - j == jend; ++i){ - triggers[i].push_back(j->exportTo(exprManager, variableMap)); - }; - }; - /** Convert head and body */ - Expr head = d_head.exportTo(exprManager, variableMap); - Expr body = d_body.exportTo(exprManager, variableMap); - /** Create the converted rules */ - return new RewriteRuleCommand(vars, guards, head, body, triggers); -} - -Command* RewriteRuleCommand::clone() const { - return new RewriteRuleCommand(d_vars, d_guards, d_head, d_body, d_triggers); -} - -std::string RewriteRuleCommand::getCommandName() const throw() { - return "rewrite-rule"; -} - -/* class PropagateRuleCommand */ - -PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& guards, - const std::vector<Expr>& heads, - Expr body, - const Triggers& triggers, - bool deduction) throw() : - d_vars(vars), d_guards(guards), d_heads(heads), d_body(body), d_triggers(triggers), d_deduction(deduction) { -} - -PropagateRuleCommand::PropagateRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& heads, - Expr body, - bool deduction) throw() : - d_vars(vars), d_heads(heads), d_body(body), d_deduction(deduction) { -} - -const std::vector<Expr>& PropagateRuleCommand::getVars() const throw() { - return d_vars; -} - -const std::vector<Expr>& PropagateRuleCommand::getGuards() const throw() { - return d_guards; -} - -const std::vector<Expr>& PropagateRuleCommand::getHeads() const throw() { - return d_heads; -} - -Expr PropagateRuleCommand::getBody() const throw() { - return d_body; -} - -const PropagateRuleCommand::Triggers& PropagateRuleCommand::getTriggers() const throw() { - return d_triggers; -} - -bool PropagateRuleCommand::isDeduction() const throw() { - return d_deduction; -} - -void PropagateRuleCommand::invoke(SmtEngine* smtEngine) throw() { - try { - ExprManager* em = smtEngine->getExprManager(); - /** build vars list */ - Expr vars = em->mkExpr(kind::BOUND_VAR_LIST, d_vars); - /** build guards list */ - Expr guards; - if(d_guards.size() == 0) guards = em->mkConst<bool>(true); - else if(d_guards.size() == 1) guards = d_guards[0]; - else guards = em->mkExpr(kind::AND,d_guards); - /** build heads list */ - Expr heads; - if(d_heads.size() == 1) heads = d_heads[0]; - else heads = em->mkExpr(kind::AND,d_heads); - /** build expression */ - Expr expr; - if( d_triggers.empty() ){ - expr = em->mkExpr(kind::RR_REWRITE,vars,guards,heads,d_body); - } else { - /** build triggers list */ - std::vector<Expr> vtriggers; - vtriggers.reserve(d_triggers.size()); - for(Triggers::const_iterator i = d_triggers.begin(), - end = d_triggers.end(); i != end; ++i){ - vtriggers.push_back(em->mkExpr(kind::INST_PATTERN,*i)); - } - Expr triggers = em->mkExpr(kind::INST_PATTERN_LIST,vtriggers); - expr = em->mkExpr(kind::RR_REWRITE,vars,guards,heads,d_body,triggers); - } - smtEngine->assertFormula(expr); - d_commandStatus = CommandSuccess::instance(); - } catch(exception& e) { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* PropagateRuleCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - /** Convert variables */ - VExpr vars; vars.reserve(d_vars.size()); - for(VExpr::iterator i = d_vars.begin(), end = d_vars.end(); - i == end; ++i){ - vars.push_back(i->exportTo(exprManager, variableMap)); - }; - /** Convert guards */ - VExpr guards; guards.reserve(d_guards.size()); - for(VExpr::iterator i = d_guards.begin(), end = d_guards.end(); - i == end; ++i){ - guards.push_back(i->exportTo(exprManager, variableMap)); - }; - /** Convert heads */ - VExpr heads; heads.reserve(d_heads.size()); - for(VExpr::iterator i = d_heads.begin(), end = d_heads.end(); - i == end; ++i){ - heads.push_back(i->exportTo(exprManager, variableMap)); - }; - /** Convert triggers */ - Triggers triggers; triggers.resize(d_triggers.size()); - for(size_t i = 0, end = d_triggers.size(); - i < end; ++i){ - triggers[i].reserve(d_triggers[i].size()); - for(VExpr::iterator j = d_triggers[i].begin(), jend = d_triggers[i].end(); - j == jend; ++i){ - triggers[i].push_back(j->exportTo(exprManager, variableMap)); - }; - }; - /** Convert head and body */ - Expr body = d_body.exportTo(exprManager, variableMap); - /** Create the converted rules */ - return new PropagateRuleCommand(vars, guards, heads, body, triggers); -} - -Command* PropagateRuleCommand::clone() const { - return new PropagateRuleCommand(d_vars, d_guards, d_heads, d_body, d_triggers); -} - -std::string PropagateRuleCommand::getCommandName() const throw() { - return "propagate-rule"; -} - -/* output stream insertion operator for benchmark statuses */ -std::ostream& operator<<(std::ostream& out, - BenchmarkStatus status) throw() { - switch(status) { - - case SMT_SATISFIABLE: - return out << "sat"; - - case SMT_UNSATISFIABLE: - return out << "unsat"; - - case SMT_UNKNOWN: - return out << "unknown"; - - default: - return out << "BenchmarkStatus::[UNKNOWNSTATUS!]"; - } -} - -}/* CVC4 namespace */ diff --git a/src/expr/command.h b/src/expr/command.h deleted file mode 100644 index 9165961fb..000000000 --- a/src/expr/command.h +++ /dev/null @@ -1,904 +0,0 @@ -/********************* */ -/*! \file command.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal, Christopher L. Conway, Dejan Jovanovic, Francois Bobot, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of the command pattern on SmtEngines. - ** - ** Implementation of the command pattern on SmtEngines. Command - ** objects are generated by the parser (typically) to implement the - ** commands in parsed input (see Parser::parseNextCommand()), or by - ** client code. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__COMMAND_H -#define __CVC4__COMMAND_H - -#include <iostream> -#include <sstream> -#include <string> -#include <vector> -#include <map> - -#include "expr/expr.h" -#include "expr/type.h" -#include "expr/variable_type_map.h" -#include "util/result.h" -#include "util/sexpr.h" -#include "util/datatype.h" -#include "util/proof.h" -#include "util/unsat_core.h" - -namespace CVC4 { - -class SmtEngine; -class Command; -class CommandStatus; -class Model; - -std::ostream& operator<<(std::ostream&, const Command&) throw() CVC4_PUBLIC; -std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC; -std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC; -std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC; - -/** The status an SMT benchmark can have */ -enum BenchmarkStatus { - /** Benchmark is satisfiable */ - SMT_SATISFIABLE, - /** Benchmark is unsatisfiable */ - SMT_UNSATISFIABLE, - /** The status of the benchmark is unknown */ - SMT_UNKNOWN -};/* enum BenchmarkStatus */ - -std::ostream& operator<<(std::ostream& out, - BenchmarkStatus status) throw() CVC4_PUBLIC; - -/** - * IOStream manipulator to print success messages or not. - * - * out << Command::printsuccess(false) << CommandSuccess(); - * - * prints nothing, but - * - * out << Command::printsuccess(true) << CommandSuccess(); - * - * prints a success message (in a manner appropriate for the current - * output language). - */ -class CVC4_PUBLIC CommandPrintSuccess { - /** - * The allocated index in ios_base for our depth setting. - */ - static const int s_iosIndex; - - /** - * The default setting, for ostreams that haven't yet had a - * setdepth() applied to them. - */ - static const int s_defaultPrintSuccess = false; - - /** - * When this manipulator is used, the setting is stored here. - */ - bool d_printSuccess; - -public: - /** - * Construct a CommandPrintSuccess with the given setting. - */ - CommandPrintSuccess(bool printSuccess) throw() : d_printSuccess(printSuccess) {} - - inline void applyPrintSuccess(std::ostream& out) throw() { - out.iword(s_iosIndex) = d_printSuccess; - } - - static inline bool getPrintSuccess(std::ostream& out) throw() { - return out.iword(s_iosIndex); - } - - static inline void setPrintSuccess(std::ostream& out, bool printSuccess) throw() { - out.iword(s_iosIndex) = printSuccess; - } - - /** - * Set the print-success state on the output stream for the current - * stack scope. This makes sure the old state is reset on the - * stream after normal OR exceptional exit from the scope, using the - * RAII C++ idiom. - */ - class Scope { - std::ostream& d_out; - bool d_oldPrintSuccess; - - public: - - inline Scope(std::ostream& out, bool printSuccess) throw() : - d_out(out), - d_oldPrintSuccess(CommandPrintSuccess::getPrintSuccess(out)) { - CommandPrintSuccess::setPrintSuccess(out, printSuccess); - } - - inline ~Scope() throw() { - CommandPrintSuccess::setPrintSuccess(d_out, d_oldPrintSuccess); - } - - };/* class CommandPrintSuccess::Scope */ - -};/* class CommandPrintSuccess */ - -/** - * Sets the default print-success setting when pretty-printing an Expr - * to an ostream. Use like this: - * - * // let out be an ostream, e an Expr - * out << Expr::setdepth(n) << e << endl; - * - * The depth stays permanently (until set again) with the stream. - */ -inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() CVC4_PUBLIC; -inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() { - cps.applyPrintSuccess(out); - return out; -} - -class CVC4_PUBLIC CommandStatus { -protected: - // shouldn't construct a CommandStatus (use a derived class) - CommandStatus() throw() {} -public: - virtual ~CommandStatus() throw() {} - void toStream(std::ostream& out, - OutputLanguage language = language::output::LANG_AUTO) const throw(); - virtual CommandStatus& clone() const = 0; -};/* class CommandStatus */ - -class CVC4_PUBLIC CommandSuccess : public CommandStatus { - static const CommandSuccess* s_instance; -public: - static const CommandSuccess* instance() throw() { return s_instance; } - CommandStatus& clone() const { return const_cast<CommandSuccess&>(*this); } -};/* class CommandSuccess */ - -class CVC4_PUBLIC CommandInterrupted : public CommandStatus { - static const CommandInterrupted* s_instance; -public: - static const CommandInterrupted* instance() throw() { return s_instance; } - CommandStatus& clone() const { return const_cast<CommandInterrupted&>(*this); } -};/* class CommandInterrupted */ - -class CVC4_PUBLIC CommandUnsupported : public CommandStatus { -public: - CommandStatus& clone() const { return *new CommandUnsupported(*this); } -};/* class CommandSuccess */ - -class CVC4_PUBLIC CommandFailure : public CommandStatus { - std::string d_message; -public: - CommandFailure(std::string message) throw() : d_message(message) {} - CommandFailure& clone() const { return *new CommandFailure(*this); } - ~CommandFailure() throw() {} - std::string getMessage() const throw() { return d_message; } -};/* class CommandFailure */ - -class CVC4_PUBLIC Command { -protected: - /** - * This field contains a command status if the command has been - * invoked, or NULL if it has not. This field is either a - * dynamically-allocated pointer, or it's a pointer to the singleton - * CommandSuccess instance. Doing so is somewhat asymmetric, but - * it avoids the need to dynamically allocate memory in the common - * case of a successful command. - */ - const CommandStatus* d_commandStatus; - - /** - * True if this command is "muted"---i.e., don't print "success" on - * successful execution. - */ - bool d_muted; - -public: - typedef CommandPrintSuccess printsuccess; - - Command() throw(); - Command(const Command& cmd); - - virtual ~Command() throw(); - - virtual void invoke(SmtEngine* smtEngine) throw() = 0; - virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); - - virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const throw(); - - std::string toString() const throw(); - - virtual std::string getCommandName() const throw() = 0; - - /** - * If false, instruct this Command not to print a success message. - */ - void setMuted(bool muted) throw() { d_muted = muted; } - - /** - * Determine whether this Command will print a success message. - */ - bool isMuted() throw() { return d_muted; } - - /** - * Either the command hasn't run yet, or it completed successfully - * (CommandSuccess, not CommandUnsupported or CommandFailure). - */ - bool ok() const throw(); - - /** - * The command completed in a failure state (CommandFailure, not - * CommandSuccess or CommandUnsupported). - */ - bool fail() const throw(); - - /** - * The command was ran but was interrupted due to resource limiting. - */ - bool interrupted() const throw(); - - /** Get the command status (it's NULL if we haven't run yet). */ - const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; } - - virtual void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - - /** - * Maps this Command into one for a different ExprManager, using - * variableMap for the translation and extending it with any new - * mappings. - */ - virtual Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) = 0; - - /** - * Clone this Command (make a shallow copy). - */ - virtual Command* clone() const = 0; - -protected: - class ExportTransformer { - ExprManager* d_exprManager; - ExprManagerMapCollection& d_variableMap; - public: - ExportTransformer(ExprManager* exprManager, ExprManagerMapCollection& variableMap) : - d_exprManager(exprManager), - d_variableMap(variableMap) { - } - Expr operator()(Expr e) { - return e.exportTo(d_exprManager, d_variableMap); - } - Type operator()(Type t) { - return t.exportTo(d_exprManager, d_variableMap); - } - };/* class Command::ExportTransformer */ -};/* class Command */ - -/** - * EmptyCommands are the residue of a command after the parser handles - * them (and there's nothing left to do). - */ -class CVC4_PUBLIC EmptyCommand : public Command { -protected: - std::string d_name; -public: - EmptyCommand(std::string name = "") throw(); - ~EmptyCommand() throw() {} - std::string getName() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class EmptyCommand */ - -class CVC4_PUBLIC EchoCommand : public Command { -protected: - std::string d_output; -public: - EchoCommand(std::string output = "") throw(); - ~EchoCommand() throw() {} - std::string getOutput() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class EchoCommand */ - -class CVC4_PUBLIC AssertCommand : public Command { -protected: - Expr d_expr; - bool d_inUnsatCore; -public: - AssertCommand(const Expr& e, bool inUnsatCore = true) throw(); - ~AssertCommand() throw() {} - Expr getExpr() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class AssertCommand */ - -class CVC4_PUBLIC PushCommand : public Command { -public: - ~PushCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class PushCommand */ - -class CVC4_PUBLIC PopCommand : public Command { -public: - ~PopCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class PopCommand */ - -class CVC4_PUBLIC DeclarationDefinitionCommand : public Command { -protected: - std::string d_symbol; -public: - DeclarationDefinitionCommand(const std::string& id) throw(); - ~DeclarationDefinitionCommand() throw() {} - virtual void invoke(SmtEngine* smtEngine) throw() = 0; - std::string getSymbol() const throw(); -};/* class DeclarationDefinitionCommand */ - -class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand { -protected: - Expr d_func; - Type d_type; - bool d_printInModel; - bool d_printInModelSetByUser; -public: - DeclareFunctionCommand(const std::string& id, Expr func, Type type) throw(); - ~DeclareFunctionCommand() throw() {} - Expr getFunction() const throw(); - Type getType() const throw(); - bool getPrintInModel() const throw(); - bool getPrintInModelSetByUser() const throw(); - void setPrintInModel( bool p ); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class DeclareFunctionCommand */ - -class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand { -protected: - size_t d_arity; - Type d_type; -public: - DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw(); - ~DeclareTypeCommand() throw() {} - size_t getArity() const throw(); - Type getType() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class DeclareTypeCommand */ - -class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand { -protected: - std::vector<Type> d_params; - Type d_type; -public: - DefineTypeCommand(const std::string& id, Type t) throw(); - DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t) throw(); - ~DefineTypeCommand() throw() {} - const std::vector<Type>& getParameters() const throw(); - Type getType() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class DefineTypeCommand */ - -class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand { -protected: - Expr d_func; - std::vector<Expr> d_formals; - Expr d_formula; -public: - DefineFunctionCommand(const std::string& id, Expr func, Expr formula) throw(); - DefineFunctionCommand(const std::string& id, Expr func, - const std::vector<Expr>& formals, Expr formula) throw(); - ~DefineFunctionCommand() throw() {} - Expr getFunction() const throw(); - const std::vector<Expr>& getFormals() const throw(); - Expr getFormula() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class DefineFunctionCommand */ - -/** - * This differs from DefineFunctionCommand only in that it instructs - * the SmtEngine to "remember" this function for later retrieval with - * getAssignment(). Used for :named attributes in SMT-LIBv2. - */ -class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand { -public: - DefineNamedFunctionCommand(const std::string& id, Expr func, - const std::vector<Expr>& formals, Expr formula) throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; -};/* class DefineNamedFunctionCommand */ - -/** - * The command when an attribute is set by a user. In SMT-LIBv2 this is done - * via the syntax (! expr :attr) - */ -class CVC4_PUBLIC SetUserAttributeCommand : public Command { -protected: - std::string d_attr; - Expr d_expr; - std::vector<Expr> d_expr_values; - std::string d_str_value; -public: - SetUserAttributeCommand( const std::string& attr, Expr expr ) throw(); - SetUserAttributeCommand( const std::string& attr, Expr expr, std::vector<Expr>& values ) throw(); - SetUserAttributeCommand( const std::string& attr, Expr expr, const std::string& value ) throw(); - ~SetUserAttributeCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class SetUserAttributeCommand */ - -class CVC4_PUBLIC CheckSatCommand : public Command { -protected: - Expr d_expr; - Result d_result; - bool d_inUnsatCore; -public: - CheckSatCommand() throw(); - CheckSatCommand(const Expr& expr, bool inUnsatCore = true) throw(); - ~CheckSatCommand() throw() {} - Expr getExpr() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Result getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class CheckSatCommand */ - -class CVC4_PUBLIC QueryCommand : public Command { -protected: - Expr d_expr; - Result d_result; - bool d_inUnsatCore; -public: - QueryCommand(const Expr& e, bool inUnsatCore = true) throw(); - ~QueryCommand() throw() {} - Expr getExpr() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Result getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class QueryCommand */ - -// this is TRANSFORM in the CVC presentation language -class CVC4_PUBLIC SimplifyCommand : public Command { -protected: - Expr d_term; - Expr d_result; -public: - SimplifyCommand(Expr term) throw(); - ~SimplifyCommand() throw() {} - Expr getTerm() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Expr getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class SimplifyCommand */ - -class CVC4_PUBLIC ExpandDefinitionsCommand : public Command { -protected: - Expr d_term; - Expr d_result; -public: - ExpandDefinitionsCommand(Expr term) throw(); - ~ExpandDefinitionsCommand() throw() {} - Expr getTerm() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Expr getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class ExpandDefinitionsCommand */ - -class CVC4_PUBLIC GetValueCommand : public Command { -protected: - std::vector<Expr> d_terms; - Expr d_result; -public: - GetValueCommand(Expr term) throw(); - GetValueCommand(const std::vector<Expr>& terms) throw(); - ~GetValueCommand() throw() {} - const std::vector<Expr>& getTerms() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Expr getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetValueCommand */ - -class CVC4_PUBLIC GetAssignmentCommand : public Command { -protected: - SExpr d_result; -public: - GetAssignmentCommand() throw(); - ~GetAssignmentCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - SExpr getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetAssignmentCommand */ - -class CVC4_PUBLIC GetModelCommand : public Command { -protected: - Model* d_result; - SmtEngine* d_smtEngine; -public: - GetModelCommand() throw(); - ~GetModelCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - // Model is private to the library -- for now - //Model* getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetModelCommand */ - -class CVC4_PUBLIC GetProofCommand : public Command { -protected: - Proof* d_result; -public: - GetProofCommand() throw(); - ~GetProofCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - Proof* getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetProofCommand */ - -class CVC4_PUBLIC GetInstantiationsCommand : public Command { -protected: - //Instantiations* d_result; - SmtEngine* d_smtEngine; -public: - GetInstantiationsCommand() throw(); - ~GetInstantiationsCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - //Instantiations* getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetInstantiationsCommand */ - -class CVC4_PUBLIC GetSynthSolutionCommand : public Command { -protected: - SmtEngine* d_smtEngine; -public: - GetSynthSolutionCommand() throw(); - ~GetSynthSolutionCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetSynthSolutionCommand */ - -class CVC4_PUBLIC GetUnsatCoreCommand : public Command { -protected: - UnsatCore d_result; - std::map<Expr, std::string> d_names; -public: - GetUnsatCoreCommand() throw(); - GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw(); - ~GetUnsatCoreCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - const UnsatCore& getUnsatCore() const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetUnsatCoreCommand */ - -class CVC4_PUBLIC GetAssertionsCommand : public Command { -protected: - std::string d_result; -public: - GetAssertionsCommand() throw(); - ~GetAssertionsCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - std::string getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetAssertionsCommand */ - -class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { -protected: - BenchmarkStatus d_status; -public: - SetBenchmarkStatusCommand(BenchmarkStatus status) throw(); - ~SetBenchmarkStatusCommand() throw() {} - BenchmarkStatus getStatus() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class SetBenchmarkStatusCommand */ - -class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { -protected: - std::string d_logic; -public: - SetBenchmarkLogicCommand(std::string logic) throw(); - ~SetBenchmarkLogicCommand() throw() {} - std::string getLogic() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class SetBenchmarkLogicCommand */ - -class CVC4_PUBLIC SetInfoCommand : public Command { -protected: - std::string d_flag; - SExpr d_sexpr; -public: - SetInfoCommand(std::string flag, const SExpr& sexpr) throw(); - ~SetInfoCommand() throw() {} - std::string getFlag() const throw(); - SExpr getSExpr() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class SetInfoCommand */ - -class CVC4_PUBLIC GetInfoCommand : public Command { -protected: - std::string d_flag; - std::string d_result; -public: - GetInfoCommand(std::string flag) throw(); - ~GetInfoCommand() throw() {} - std::string getFlag() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - std::string getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetInfoCommand */ - -class CVC4_PUBLIC SetOptionCommand : public Command { -protected: - std::string d_flag; - SExpr d_sexpr; -public: - SetOptionCommand(std::string flag, const SExpr& sexpr) throw(); - ~SetOptionCommand() throw() {} - std::string getFlag() const throw(); - SExpr getSExpr() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class SetOptionCommand */ - -class CVC4_PUBLIC GetOptionCommand : public Command { -protected: - std::string d_flag; - std::string d_result; -public: - GetOptionCommand(std::string flag) throw(); - ~GetOptionCommand() throw() {} - std::string getFlag() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - std::string getResult() const throw(); - void printResult(std::ostream& out, uint32_t verbosity = 2) const throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class GetOptionCommand */ - -class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { -private: - std::vector<DatatypeType> d_datatypes; -public: - DatatypeDeclarationCommand(const DatatypeType& datatype) throw(); - ~DatatypeDeclarationCommand() throw() {} - DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw(); - const std::vector<DatatypeType>& getDatatypes() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class DatatypeDeclarationCommand */ - -class CVC4_PUBLIC RewriteRuleCommand : public Command { -public: - typedef std::vector< std::vector< Expr > > Triggers; -protected: - typedef std::vector< Expr > VExpr; - VExpr d_vars; - VExpr d_guards; - Expr d_head; - Expr d_body; - Triggers d_triggers; -public: - RewriteRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& guards, - Expr head, - Expr body, - const Triggers& d_triggers) throw(); - RewriteRuleCommand(const std::vector<Expr>& vars, - Expr head, - Expr body) throw(); - ~RewriteRuleCommand() throw() {} - const std::vector<Expr>& getVars() const throw(); - const std::vector<Expr>& getGuards() const throw(); - Expr getHead() const throw(); - Expr getBody() const throw(); - const Triggers& getTriggers() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class RewriteRuleCommand */ - -class CVC4_PUBLIC PropagateRuleCommand : public Command { -public: - typedef std::vector< std::vector< Expr > > Triggers; -protected: - typedef std::vector< Expr > VExpr; - VExpr d_vars; - VExpr d_guards; - VExpr d_heads; - Expr d_body; - Triggers d_triggers; - bool d_deduction; -public: - PropagateRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& guards, - const std::vector<Expr>& heads, - Expr body, - const Triggers& d_triggers, - /* true if we want a deduction rule */ - bool d_deduction = false) throw(); - PropagateRuleCommand(const std::vector<Expr>& vars, - const std::vector<Expr>& heads, - Expr body, - bool d_deduction = false) throw(); - ~PropagateRuleCommand() throw() {} - const std::vector<Expr>& getVars() const throw(); - const std::vector<Expr>& getGuards() const throw(); - const std::vector<Expr>& getHeads() const throw(); - Expr getBody() const throw(); - const Triggers& getTriggers() const throw(); - bool isDeduction() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class PropagateRuleCommand */ - -class CVC4_PUBLIC ResetCommand : public Command { -public: - ResetCommand() throw() {} - ~ResetCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class ResetCommand */ - -class CVC4_PUBLIC ResetAssertionsCommand : public Command { -public: - ResetAssertionsCommand() throw() {} - ~ResetAssertionsCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class ResetAssertionsCommand */ - -class CVC4_PUBLIC QuitCommand : public Command { -public: - QuitCommand() throw() {} - ~QuitCommand() throw() {} - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class QuitCommand */ - -class CVC4_PUBLIC CommentCommand : public Command { - std::string d_comment; -public: - CommentCommand(std::string comment) throw(); - ~CommentCommand() throw() {} - std::string getComment() const throw(); - void invoke(SmtEngine* smtEngine) throw(); - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class CommentCommand */ - -class CVC4_PUBLIC CommandSequence : public Command { -private: - /** All the commands to be executed (in sequence) */ - std::vector<Command*> d_commandSequence; - /** Next command to be executed */ - unsigned int d_index; -public: - CommandSequence() throw(); - ~CommandSequence() throw(); - - void addCommand(Command* cmd) throw(); - void clear() throw(); - - void invoke(SmtEngine* smtEngine) throw(); - void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); - - typedef std::vector<Command*>::iterator iterator; - typedef std::vector<Command*>::const_iterator const_iterator; - - const_iterator begin() const throw(); - const_iterator end() const throw(); - - iterator begin() throw(); - iterator end() throw(); - - Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); - Command* clone() const; - std::string getCommandName() const throw(); -};/* class CommandSequence */ - -class CVC4_PUBLIC DeclarationSequence : public CommandSequence { -public: - ~DeclarationSequence() throw() {} -};/* class DeclarationSequence */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__COMMAND_H */ diff --git a/src/expr/command.i b/src/expr/command.i deleted file mode 100644 index d6cbfe272..000000000 --- a/src/expr/command.i +++ /dev/null @@ -1,77 +0,0 @@ -%{ -#include "expr/command.h" - -#ifdef SWIGJAVA - -#include "bindings/java_iterator_adapter.h" -#include "bindings/java_stream_adapters.h" - -#endif /* SWIGJAVA */ -%} - -%ignore CVC4::operator<<(std::ostream&, const Command&) throw(); -%ignore CVC4::operator<<(std::ostream&, const Command*) throw(); -%ignore CVC4::operator<<(std::ostream&, const CommandStatus&) throw(); -%ignore CVC4::operator<<(std::ostream&, const CommandStatus*) throw(); -%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status) throw(); -%ignore CVC4::operator<<(std::ostream&, CommandPrintSuccess) throw(); - -%ignore CVC4::GetProofCommand; -%ignore CVC4::CommandPrintSuccess::Scope; - -#ifdef SWIGJAVA - -// Instead of CommandSequence::begin() and end(), create an -// iterator() method on the Java side that returns a Java-style -// Iterator. -%ignore CVC4::CommandSequence::begin(); -%ignore CVC4::CommandSequence::end(); -%ignore CVC4::CommandSequence::begin() const; -%ignore CVC4::CommandSequence::end() const; -%extend CVC4::CommandSequence { - CVC4::JavaIteratorAdapter<CVC4::CommandSequence> iterator() { - return CVC4::JavaIteratorAdapter<CVC4::CommandSequence>(*$self); - } -} - -// CommandSequence is "iterable" on the Java side -%typemap(javainterfaces) CVC4::CommandSequence "java.lang.Iterable<edu.nyu.acsys.CVC4.Command>"; - -// the JavaIteratorAdapter should not be public, and implements Iterator -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "class"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "java.util.Iterator<edu.nyu.acsys.CVC4.Command>"; -// add some functions to the Java side (do it here because there's no way to do these in C++) -%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> " - public void remove() { - throw new java.lang.UnsupportedOperationException(); - } - - public edu.nyu.acsys.CVC4.Command next() { - if(hasNext()) { - return getNext(); - } else { - throw new java.util.NoSuchElementException(); - } - } -" -// getNext() just allows C++ iterator access from Java-side next(), make it private -%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::CommandSequence>::getNext() "private"; - -// map the types appropriately -%typemap(jni) CVC4::CommandSequence::const_iterator::value_type "jobject"; -%typemap(jtype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command"; -%typemap(jstype) CVC4::CommandSequence::const_iterator::value_type "edu.nyu.acsys.CVC4.Command"; -%typemap(javaout) CVC4::CommandSequence::const_iterator::value_type { return $jnicall; } - -#endif /* SWIGJAVA */ - -%include "expr/command.h" - -#ifdef SWIGJAVA - -%include "bindings/java_iterator_adapter.h" -%include "bindings/java_stream_adapters.h" - -%template(JavaIteratorAdapter_CommandSequence) CVC4::JavaIteratorAdapter<CVC4::CommandSequence>; - -#endif /* SWIGJAVA */ diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp new file mode 100644 index 000000000..c758fe297 --- /dev/null +++ b/src/expr/datatype.cpp @@ -0,0 +1,1023 @@ +/********************* */ +/*! \file datatype.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: Andrew Reynolds + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A class representing a Datatype definition + ** + ** A class representing a Datatype definition for the theory of + ** inductive datatypes. + **/ +#include "expr/datatype.h" + +#include <string> +#include <sstream> + +#include "base/cvc4_assert.h" +#include "expr/attribute.h" +#include "expr/expr_manager.h" +#include "expr/expr_manager_scope.h" +#include "expr/matcher.h" +#include "expr/node.h" +#include "expr/node_manager.h" +#include "expr/type.h" + +using namespace std; + +namespace CVC4 { + +namespace expr { + namespace attr { + struct DatatypeIndexTag {}; + struct DatatypeConsIndexTag {}; + struct DatatypeFiniteTag {}; + struct DatatypeFiniteComputedTag {}; + }/* CVC4::expr::attr namespace */ +}/* CVC4::expr namespace */ + +typedef expr::Attribute<expr::attr::DatatypeIndexTag, uint64_t> DatatypeIndexAttr; +typedef expr::Attribute<expr::attr::DatatypeConsIndexTag, uint64_t> DatatypeConsIndexAttr; +typedef expr::Attribute<expr::attr::DatatypeFiniteTag, bool> DatatypeFiniteAttr; +typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFiniteComputedAttr; + +const Datatype& Datatype::datatypeOf(Expr item) { + ExprManagerScope ems(item); + TypeNode t = Node::fromExpr(item).getType(); + switch(t.getKind()) { + case kind::CONSTRUCTOR_TYPE: + return DatatypeType(t[t.getNumChildren() - 1].toType()).getDatatype(); + case kind::SELECTOR_TYPE: + case kind::TESTER_TYPE: + return DatatypeType(t[0].toType()).getDatatype(); + default: + Unhandled("arg must be a datatype constructor, selector, or tester"); + } +} + +size_t Datatype::indexOf(Expr item) { + ExprManagerScope ems(item); + CheckArgument(item.getType().isConstructor() || + item.getType().isTester() || + item.getType().isSelector(), + item, + "arg must be a datatype constructor, selector, or tester"); + TNode n = Node::fromExpr(item); + if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){ + return indexOf( item[0] ); + }else{ + Assert(n.hasAttribute(DatatypeIndexAttr())); + return n.getAttribute(DatatypeIndexAttr()); + } +} + +size_t Datatype::cindexOf(Expr item) { + ExprManagerScope ems(item); + CheckArgument(item.getType().isSelector(), + item, + "arg must be a datatype selector"); + TNode n = Node::fromExpr(item); + if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){ + return cindexOf( item[0] ); + }else{ + Assert(n.hasAttribute(DatatypeConsIndexAttr())); + return n.getAttribute(DatatypeConsIndexAttr()); + } +} + +void Datatype::resolve(ExprManager* em, + const std::map<std::string, DatatypeType>& resolutions, + const std::vector<Type>& placeholders, + const std::vector<Type>& replacements, + const std::vector< SortConstructorType >& paramTypes, + const std::vector< DatatypeType >& paramReplacements) + throw(IllegalArgumentException, DatatypeResolutionException) { + + CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager"); + CheckArgument(!d_resolved, this, "cannot resolve a Datatype twice"); + CheckArgument(resolutions.find(d_name) != resolutions.end(), resolutions, + "Datatype::resolve(): resolutions doesn't contain me!"); + CheckArgument(placeholders.size() == replacements.size(), placeholders, + "placeholders and replacements must be the same size"); + CheckArgument(paramTypes.size() == paramReplacements.size(), paramTypes, + "paramTypes and paramReplacements must be the same size"); + CheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors"); + DatatypeType self = (*resolutions.find(d_name)).second; + CheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!"); + d_resolved = true; + size_t index = 0; + for(std::vector<DatatypeConstructor>::iterator i = d_constructors.begin(), i_end = d_constructors.end(); i != i_end; ++i) { + (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements, index); + Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index); + Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++); + } + d_self = self; + + d_involvesExt = false; + for(const_iterator i = begin(); i != end(); ++i) { + if( (*i).involvesExternalType() ){ + d_involvesExt = true; + break; + } + } +} + +void Datatype::addConstructor(const DatatypeConstructor& c) { + CheckArgument(!d_resolved, this, + "cannot add a constructor to a finalized Datatype"); + d_constructors.push_back(c); +} + + +void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ + CheckArgument(!d_resolved, this, + "cannot set sygus type to a finalized Datatype"); + d_sygus_type = st; + d_sygus_bvl = bvl; + d_sygus_allow_const = allow_const || allow_all; + d_sygus_allow_all = allow_all; +} + + +Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) { + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + std::vector< Type > processing; + computeCardinality( processing ); + return d_card; +} + +Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException){ + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){ + d_card = Cardinality::INTEGERS; + }else{ + processing.push_back( d_self ); + Cardinality c = 0; + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + c += (*i).computeCardinality( processing ); + } + d_card = c; + processing.pop_back(); + } + return d_card; +} + +bool Datatype::isRecursiveSingleton() const throw(IllegalArgumentException) { + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + if( d_card_rec_singleton==0 ){ + Assert( d_card_u_assume.empty() ); + std::vector< Type > processing; + if( computeCardinalityRecSingleton( processing, d_card_u_assume ) ){ + d_card_rec_singleton = 1; + }else{ + d_card_rec_singleton = -1; + } + if( d_card_rec_singleton==1 ){ + Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume.size() << " uninterpreted sorts: " << std::endl; + for( unsigned i=0; i<d_card_u_assume.size(); i++ ){ + Trace("dt-card") << " " << d_card_u_assume [i] << std::endl; + } + Trace("dt-card") << std::endl; + } + } + return d_card_rec_singleton==1; +} + +unsigned Datatype::getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException) { + return d_card_u_assume.size(); +} +Type Datatype::getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException) { + return d_card_u_assume[i]; +} + +bool Datatype::computeCardinalityRecSingleton( std::vector< Type >& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException){ + if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){ + return true; + }else{ + if( d_card_rec_singleton==0 ){ + //if not yet computed + if( d_constructors.size()==1 ){ + bool success = false; + processing.push_back( d_self ); + for(unsigned i = 0; i<d_constructors[0].getNumArgs(); i++ ) { + Type t = ((SelectorType)d_constructors[0][i].getType()).getRangeType(); + //if it is an uninterpreted sort, then we depend on it having cardinality one + if( t.isSort() ){ + if( std::find( u_assume.begin(), u_assume.end(), t )==u_assume.end() ){ + u_assume.push_back( t ); + } + //if it is a datatype, recurse + }else if( t.isDatatype() ){ + const Datatype & dt = ((DatatypeType)t).getDatatype(); + if( !dt.computeCardinalityRecSingleton( processing, u_assume ) ){ + return false; + }else{ + success = true; + } + //if it is a builtin type, it must have cardinality one + }else if( !t.getCardinality().isOne() ){ + return false; + } + } + processing.pop_back(); + return success; + }else{ + return false; + } + }else if( d_card_rec_singleton==-1 ){ + return false; + }else{ + for( unsigned i=0; i<d_card_u_assume.size(); i++ ){ + if( std::find( u_assume.begin(), u_assume.end(), d_card_u_assume[i] )==u_assume.end() ){ + u_assume.push_back( d_card_u_assume[i] ); + } + } + return true; + } + } +} + +bool Datatype::isFinite() const throw(IllegalArgumentException) { + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_self); + + TypeNode self = TypeNode::fromType(d_self); + + // is this already in the cache ? + if(self.getAttribute(DatatypeFiniteComputedAttr())) { + return self.getAttribute(DatatypeFiniteAttr()); + } + + Cardinality c = 0; + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + if(! (*i).isFinite()) { + self.setAttribute(DatatypeFiniteComputedAttr(), true); + self.setAttribute(DatatypeFiniteAttr(), false); + return false; + } + } + self.setAttribute(DatatypeFiniteComputedAttr(), true); + self.setAttribute(DatatypeFiniteAttr(), true); + return true; +} + +bool Datatype::isWellFounded() const throw(IllegalArgumentException) { + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + if( d_well_founded==0 ){ + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_self); + std::vector< Type > processing; + if( computeWellFounded( processing ) ){ + d_well_founded = 1; + }else{ + d_well_founded = -1; + } + } + return d_well_founded==1; +} + +bool Datatype::computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException) { + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){ + return d_isCo; + }else{ + processing.push_back( d_self ); + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + if( (*i).computeWellFounded( processing ) ){ + processing.pop_back(); + return true; + }else{ + Trace("dt-wf") << "Constructor " << (*i).getName() << " is not well-founded." << std::endl; + } + } + processing.pop_back(); + Trace("dt-wf") << "Datatype " << getName() << " is not well-founded." << std::endl; + return false; + } +} + +Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { + CheckArgument(isResolved(), this, "this datatype is not yet resolved"); + ExprManagerScope ems(d_self); + + + // is this already in the cache ? + std::map< Type, Expr >::iterator it = d_ground_term.find( t ); + if( it != d_ground_term.end() ){ + Debug("datatypes") << "\nin cache: " << d_self << " => " << it->second << std::endl; + return it->second; + } else { + std::vector< Type > processing; + Expr groundTerm = computeGroundTerm( t, processing ); + if(!groundTerm.isNull() ) { + // we found a ground-term-constructing constructor! + d_ground_term[t] = groundTerm; + Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl; + } + if( groundTerm.isNull() ){ + if( !d_isCo ){ + // if we get all the way here, we aren't well-founded + CheckArgument(false, *this, "datatype is not well-founded, cannot construct a ground term!"); + }else{ + return groundTerm; + } + }else{ + return groundTerm; + } + } +} + +Expr getSubtermWithType( Expr e, Type t, bool isTop ){ + if( !isTop && e.getType()==t ){ + return e; + }else{ + for( unsigned i=0; i<e.getNumChildren(); i++ ){ + Expr se = getSubtermWithType( e[i], t, false ); + if( !se.isNull() ){ + return se; + } + } + return Expr(); + } +} + +Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) { + if( std::find( processing.begin(), processing.end(), d_self )==processing.end() ){ + processing.push_back( d_self ); + for( unsigned r=0; r<2; r++ ){ + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + //do nullary constructors first + if( ((*i).getNumArgs()==0)==(r==0)){ + Debug("datatypes") << "Try constructing for " << (*i).getName() << ", processing = " << processing.size() << std::endl; + Expr e = (*i).computeGroundTerm( t, processing, d_ground_term ); + if( !e.isNull() ){ + //must check subterms for the same type to avoid infinite loops in type enumeration + Expr se = getSubtermWithType( e, t, true ); + if( !se.isNull() ){ + Debug("datatypes") << "Take subterm " << se << std::endl; + e = se; + } + processing.pop_back(); + return e; + }else{ + Debug("datatypes") << "...failed." << std::endl; + } + } + } + } + processing.pop_back(); + }else{ + Debug("datatypes") << "...already processing " << t << std::endl; + } + return Expr(); +} + +DatatypeType Datatype::getDatatypeType() const throw(IllegalArgumentException) { + CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType"); + CheckArgument(!d_self.isNull(), *this); + return DatatypeType(d_self); +} + +DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params) + const throw(IllegalArgumentException) { + CheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType"); + CheckArgument(!d_self.isNull() && DatatypeType(d_self).isParametric(), this); + return DatatypeType(d_self).instantiate(params); +} + +bool Datatype::operator==(const Datatype& other) const throw() { + // two datatypes are == iff the name is the same and they have + // exactly matching constructors (in the same order) + + if(this == &other) { + return true; + } + + if(isResolved() != other.isResolved()) { + return false; + } + + if( d_name != other.d_name || + getNumConstructors() != other.getNumConstructors() ) { + return false; + } + for(const_iterator i = begin(), j = other.begin(); i != end(); ++i, ++j) { + Assert(j != other.end()); + // two constructors are == iff they have the same name, their + // constructors and testers are equal and they have exactly + // matching args (in the same order) + if((*i).getName() != (*j).getName() || + (*i).getNumArgs() != (*j).getNumArgs()) { + return false; + } + // testing equivalence of constructors and testers is harder b/c + // this constructor might not be resolved yet; only compare them + // if they are both resolved + Assert(isResolved() == !(*i).d_constructor.isNull() && + isResolved() == !(*i).d_tester.isNull() && + (*i).d_constructor.isNull() == (*j).d_constructor.isNull() && + (*i).d_tester.isNull() == (*j).d_tester.isNull()); + if(!(*i).d_constructor.isNull() && (*i).d_constructor != (*j).d_constructor) { + return false; + } + if(!(*i).d_tester.isNull() && (*i).d_tester != (*j).d_tester) { + return false; + } + for(DatatypeConstructor::const_iterator k = (*i).begin(), l = (*j).begin(); k != (*i).end(); ++k, ++l) { + Assert(l != (*j).end()); + if((*k).getName() != (*l).getName()) { + return false; + } + // testing equivalence of selectors is harder b/c args might not + // be resolved yet + Assert(isResolved() == (*k).isResolved() && + (*k).isResolved() == (*l).isResolved()); + if((*k).isResolved()) { + // both are resolved, so simply compare the selectors directly + if((*k).d_selector != (*l).d_selector) { + return false; + } + } else { + // neither is resolved, so compare their (possibly unresolved) + // types; we don't know if they'll be resolved the same way, + // so we can't ever say unresolved types are equal + if(!(*k).d_selector.isNull() && !(*l).d_selector.isNull()) { + if((*k).d_selector.getType() != (*l).d_selector.getType()) { + return false; + } + } else { + if((*k).isUnresolvedSelf() && (*l).isUnresolvedSelf()) { + // Fine, the selectors are equal if the rest of the + // enclosing datatypes are equal... + } else { + return false; + } + } + } + } + } + return true; +} + +const DatatypeConstructor& Datatype::operator[](size_t index) const { + CheckArgument(index < getNumConstructors(), index, "index out of bounds"); + return d_constructors[index]; +} + +const DatatypeConstructor& Datatype::operator[](std::string name) const { + for(const_iterator i = begin(); i != end(); ++i) { + if((*i).getName() == name) { + return *i; + } + } + CheckArgument(false, name, "No such constructor `%s' of datatype `%s'", name.c_str(), d_name.c_str()); +} + +Expr Datatype::getConstructor(std::string name) const { + return (*this)[name].getConstructor(); +} + +Type Datatype::getSygusType() const { + return d_sygus_type; +} + +Expr Datatype::getSygusVarList() const { + return d_sygus_bvl; +} + +bool Datatype::getSygusAllowConst() const { + return d_sygus_allow_const; +} + +bool Datatype::getSygusAllowAll() const { + return d_sygus_allow_const; +} + +bool Datatype::involvesExternalType() const{ + return d_involvesExt; +} + +void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, + const std::map<std::string, DatatypeType>& resolutions, + const std::vector<Type>& placeholders, + const std::vector<Type>& replacements, + const std::vector< SortConstructorType >& paramTypes, + const std::vector< DatatypeType >& paramReplacements, size_t cindex) + throw(IllegalArgumentException, DatatypeResolutionException) { + + CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager"); + CheckArgument(!isResolved(), + "cannot resolve a Datatype constructor twice; " + "perhaps the same constructor was added twice, " + "or to two datatypes?"); + + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(*em); + + NodeManager* nm = NodeManager::fromExprManager(em); + TypeNode selfTypeNode = TypeNode::fromType(self); + size_t index = 0; + for(std::vector<DatatypeConstructorArg>::iterator i = d_args.begin(), i_end = d_args.end(); i != i_end; ++i) { + if((*i).d_selector.isNull()) { + // the unresolved type wasn't created here; do name resolution + 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), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr(); + } else { + map<string, DatatypeType>::const_iterator j = resolutions.find(typeName); + if(j == resolutions.end()) { + stringstream msg; + msg << "cannot resolve type \"" << typeName << "\" " + << "in selector \"" << (*i).d_name << "\" " + << "of constructor \"" << d_name << "\""; + throw DatatypeResolutionException(msg.str()); + } else { + (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType((*j).second)), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr(); + } + } + } else { + // the type for the selector already exists; may need + // complex-type substitution + Type range = (*i).d_selector.getType(); + if(!placeholders.empty()) { + range = range.substitute(placeholders, replacements); + } + if(!paramTypes.empty() ) { + range = doParametricSubstitution( range, paramTypes, paramReplacements ); + } + (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range)), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr(); + } + Node::fromExpr((*i).d_selector).setAttribute(DatatypeConsIndexAttr(), cindex); + Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++); + (*i).d_resolved = true; + } + + Assert(index == getNumArgs()); + + // Set constructor/tester last, since DatatypeConstructor::isResolved() + // returns true when d_tester is not the null Expr. If something + // 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), "is a tester", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr(); + d_constructor = nm->mkSkolem(getName(), nm->mkConstructorType(*this, selfTypeNode), "is a constructor", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr(); + // associate constructor with all selectors + for(std::vector<DatatypeConstructorArg>::iterator i = d_args.begin(), i_end = d_args.end(); i != i_end; ++i) { + (*i).d_constructor = d_constructor; + } +} + +Type DatatypeConstructor::doParametricSubstitution( Type range, + const std::vector< SortConstructorType >& paramTypes, + const std::vector< DatatypeType >& paramReplacements ) { + TypeNode typn = TypeNode::fromType( range ); + if(typn.getNumChildren() == 0) { + return range; + } else { + std::vector< Type > origChildren; + std::vector< Type > children; + for(TypeNode::const_iterator i = typn.begin(), iend = typn.end();i != iend; ++i) { + origChildren.push_back( (*i).toType() ); + children.push_back( doParametricSubstitution( (*i).toType(), paramTypes, paramReplacements ) ); + } + for( unsigned i = 0; i < paramTypes.size(); ++i ) { + if( paramTypes[i].getArity() == origChildren.size() ) { + Type tn = paramTypes[i].instantiate( origChildren ); + if( range == tn ) { + return paramReplacements[i].instantiate( children ); + } + } + } + NodeBuilder<> nb(typn.getKind()); + for( unsigned i = 0; i < children.size(); ++i ) { + nb << TypeNode::fromType( children[i] ); + } + return nb.constructTypeNode().toType(); + } +} + +DatatypeConstructor::DatatypeConstructor(std::string name) : + // We don't want to introduce a new data member, because eventually + // we're going to be a constant stuffed inside a node. So we stow + // the tester name away inside the constructor name until + // resolution. + d_name(name + '\0' + "is_" + name), // default tester name is "is_FOO" + d_tester(), + d_args() { + CheckArgument(name != "", name, "cannot construct a datatype constructor without a name"); +} + +DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) : + // We don't want to introduce a new data member, because eventually + // we're going to be a constant stuffed inside a node. So we stow + // the tester name away inside the constructor name until + // resolution. + d_name(name + '\0' + tester), + d_tester(), + d_args() { + CheckArgument(name != "", name, "cannot construct a datatype constructor without a name"); + CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester"); +} + +void DatatypeConstructor::setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_args ){ + d_sygus_op = op; + d_sygus_let_body = let_body; + d_sygus_let_args.insert( d_sygus_let_args.end(), let_args.begin(), let_args.end() ); + d_sygus_num_let_input_args = num_let_input_args; +} + + +void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) { + // We don't want to introduce a new data member, because eventually + // we're going to be a constant stuffed inside a node. So we stow + // the selector type away inside a var until resolution (when we can + // create the proper selector type) + CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor"); + CheckArgument(!selectorType.isNull(), selectorType, "cannot add a null selector type"); + + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(selectorType); + + Expr type = NodeManager::currentNM()->mkSkolem("unresolved_" + selectorName, TypeNode::fromType(selectorType), "is an unresolved selector type placeholder", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr(); + Debug("datatypes") << type << endl; + d_args.push_back(DatatypeConstructorArg(selectorName, type)); +} + +void DatatypeConstructor::addArg(std::string selectorName, DatatypeUnresolvedType selectorType) { + // We don't want to introduce a new data member, because eventually + // we're going to be a constant stuffed inside a node. So we stow + // the selector type away after a NUL in the name string until + // resolution (when we can create the proper selector type) + CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor"); + CheckArgument(selectorType.getName() != "", selectorType, "cannot add a null selector type"); + d_args.push_back(DatatypeConstructorArg(selectorName + '\0' + selectorType.getName(), Expr())); +} + +void DatatypeConstructor::addArg(std::string selectorName, DatatypeSelfType) { + // We don't want to introduce a new data member, because eventually + // we're going to be a constant stuffed inside a node. So we mark + // the name string with a NUL to indicate that we have a + // self-selecting selector until resolution (when we can create the + // proper selector type) + CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor"); + d_args.push_back(DatatypeConstructorArg(selectorName + '\0', Expr())); +} + +std::string DatatypeConstructor::getName() const throw() { + return d_name.substr(0, d_name.find('\0')); +} + +std::string DatatypeConstructor::getTesterName() const throw() { + return d_name.substr(d_name.find('\0') + 1); +} + +Expr DatatypeConstructor::getConstructor() const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_constructor; +} + +Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + ExprManagerScope ems(d_constructor); + const Datatype& dt = Datatype::datatypeOf(d_constructor); + CheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric"); + DatatypeType dtt = dt.getDatatypeType(); + Matcher m(dtt); + m.doMatching( TypeNode::fromType(dtt), TypeNode::fromType(returnType) ); + vector<Type> subst; + m.getMatches(subst); + vector<Type> params = dt.getParameters(); + return d_constructor.getType().substitute(params, subst); +} + +Expr DatatypeConstructor::getTester() const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_tester; +} + +Expr DatatypeConstructor::getSygusOp() const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_sygus_op; +} + +Expr DatatypeConstructor::getSygusLetBody() const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_sygus_let_body; +} + +unsigned DatatypeConstructor::getNumSygusLetArgs() const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_sygus_let_args.size(); +} + +Expr DatatypeConstructor::getSygusLetArg( unsigned i ) const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_sygus_let_args[i]; +} + +unsigned DatatypeConstructor::getNumSygusLetInputArgs() const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_sygus_num_let_input_args; +} + +bool DatatypeConstructor::isSygusIdFunc() const { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body; +} + +Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + + Cardinality c = 1; + + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + c *= SelectorType((*i).getSelector().getType()).getRangeType().getCardinality(); + } + + return c; +} + +/** compute the cardinality of this datatype */ +Cardinality DatatypeConstructor::computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException){ + Cardinality c = 1; + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + Type t = SelectorType((*i).getSelector().getType()).getRangeType(); + if( t.isDatatype() ){ + const Datatype& dt = ((DatatypeType)t).getDatatype(); + c *= dt.computeCardinality( processing ); + }else{ + c *= t.getCardinality(); + } + } + return c; +} + +bool DatatypeConstructor::computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException){ + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + Type t = SelectorType((*i).getSelector().getType()).getRangeType(); + if( t.isDatatype() ){ + const Datatype& dt = ((DatatypeType)t).getDatatype(); + if( !dt.computeWellFounded( processing ) ){ + return false; + } + } + } + return true; +} + + +bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_constructor); + + TNode self = Node::fromExpr(d_constructor); + + // is this already in the cache ? + if(self.getAttribute(DatatypeFiniteComputedAttr())) { + return self.getAttribute(DatatypeFiniteAttr()); + } + + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + if(! SelectorType((*i).getSelector().getType()).getRangeType().getCardinality().isFinite()) { + self.setAttribute(DatatypeFiniteComputedAttr(), true); + self.setAttribute(DatatypeFiniteAttr(), false); + return false; + } + } + + self.setAttribute(DatatypeFiniteComputedAttr(), true); + self.setAttribute(DatatypeFiniteAttr(), true); + return true; +} + +Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing, std::map< Type, Expr >& gt ) const throw(IllegalArgumentException) { +// we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_constructor); + + std::vector<Expr> groundTerms; + groundTerms.push_back(getConstructor()); + + // for each selector, get a ground term + std::vector< Type > instTypes; + std::vector< Type > paramTypes; + if( DatatypeType(t).isParametric() ){ + paramTypes = DatatypeType(t).getDatatype().getParameters(); + instTypes = DatatypeType(t).getParamTypes(); + } + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + Type selType = SelectorType((*i).getSelector().getType()).getRangeType(); + if( DatatypeType(t).isParametric() ){ + selType = selType.substitute( paramTypes, instTypes ); + } + Expr arg; + if( selType.isDatatype() ){ + std::map< Type, Expr >::iterator itgt = gt.find( selType ); + if( itgt != gt.end() ){ + arg = itgt->second; + }else{ + const Datatype & dt = DatatypeType(selType).getDatatype(); + arg = dt.computeGroundTerm( selType, processing ); + } + }else{ + arg = selType.mkGroundTerm(); + } + if( arg.isNull() ){ + Debug("datatypes") << "...unable to construct arg of " << (*i).getName() << std::endl; + return Expr(); + }else{ + Debug("datatypes") << "...constructed arg " << arg.getType() << std::endl; + groundTerms.push_back(arg); + } + } + + Expr groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms); + if( groundTerm.getType()!=t ){ + Assert( Datatype::datatypeOf( d_constructor ).isParametric() ); + //type is ambiguous, must apply type ascription + Debug("datatypes-gt") << "ambiguous type for " << groundTerm << ", ascribe to " << t << std::endl; + groundTerms[0] = getConstructor().getExprManager()->mkExpr(kind::APPLY_TYPE_ASCRIPTION, + getConstructor().getExprManager()->mkConst(AscriptionType(getSpecializedConstructorType(t))), + groundTerms[0]); + groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms); + } + return groundTerm; +} + + +const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const { + CheckArgument(index < getNumArgs(), index, "index out of bounds"); + return d_args[index]; +} + +const DatatypeConstructorArg& DatatypeConstructor::operator[](std::string name) const { + for(const_iterator i = begin(); i != end(); ++i) { + if((*i).getName() == name) { + return *i; + } + } + CheckArgument(false, name, "No such arg `%s' of constructor `%s'", name.c_str(), d_name.c_str()); +} + +Expr DatatypeConstructor::getSelector(std::string name) const { + return (*this)[name].getSelector(); +} + +bool DatatypeConstructor::involvesExternalType() const{ + for(const_iterator i = begin(); i != end(); ++i) { + if(! SelectorType((*i).getSelector().getType()).getRangeType().isDatatype()) { + return true; + } + } + return false; +} + +DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector) : + d_name(name), + d_selector(selector), + d_resolved(false) { + CheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name"); +} + +std::string DatatypeConstructorArg::getName() const throw() { + string name = d_name; + const size_t nul = name.find('\0'); + if(nul != string::npos) { + name.resize(nul); + } + return name; +} + +Expr DatatypeConstructorArg::getSelector() const { + CheckArgument(isResolved(), this, "cannot get a selector for an unresolved datatype constructor"); + return d_selector; +} + +Expr DatatypeConstructorArg::getConstructor() const { + CheckArgument(isResolved(), this, + "cannot get a associated constructor for argument of an unresolved datatype constructor"); + return d_constructor; +} + +SelectorType DatatypeConstructorArg::getType() const { + return getSelector().getType(); +} + +bool DatatypeConstructorArg::isUnresolvedSelf() const throw() { + return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1; +} + +static const int s_printDatatypeNamesOnly = std::ios_base::xalloc(); + +std::string DatatypeConstructorArg::getTypeName() const { + Type t; + if(isResolved()) { + t = SelectorType(d_selector.getType()).getRangeType(); + } else { + if(d_selector.isNull()) { + string typeName = d_name.substr(d_name.find('\0') + 1); + return (typeName == "") ? "[self]" : typeName; + } else { + t = d_selector.getType(); + } + } + + // Unfortunately, in the case of complex selector types, we can + // enter nontrivial recursion here. Make sure that doesn't happen. + stringstream ss; + ss << Expr::setlanguage(language::output::LANG_CVC4); + ss.iword(s_printDatatypeNamesOnly) = 1; + t.toStream(ss); + return ss.str(); +} + +std::ostream& operator<<(std::ostream& os, const Datatype& dt) { + // These datatype things are recursive! Be very careful not to + // print an infinite chain of them. + long& printNameOnly = os.iword(s_printDatatypeNamesOnly); + Debug("datatypes-output") << "printNameOnly is " << printNameOnly << std::endl; + if(printNameOnly) { + return os << dt.getName(); + } + + class Scope { + long& d_ref; + long d_oldValue; + public: + Scope(long& ref, long value) : d_ref(ref), d_oldValue(ref) { d_ref = value; } + ~Scope() { d_ref = d_oldValue; } + } scope(printNameOnly, 1); + // when scope is destructed, the value pops back + + Debug("datatypes-output") << "printNameOnly is now " << printNameOnly << std::endl; + + // can only output datatypes in the CVC4 native language + Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); + + os << "DATATYPE " << dt.getName(); + if(dt.isParametric()) { + os << '['; + for(size_t i = 0; i < dt.getNumParameters(); ++i) { + if(i > 0) { + os << ','; + } + os << dt.getParameter(i); + } + os << ']'; + } + os << " =" << endl; + Datatype::const_iterator i = dt.begin(), i_end = dt.end(); + if(i != i_end) { + os << " "; + do { + os << *i << endl; + if(++i != i_end) { + os << "| "; + } + } while(i != i_end); + } + os << "END;" << endl; + + return os; +} + +std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) { + // can only output datatypes in the CVC4 native language + Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); + + os << ctor.getName(); + + DatatypeConstructor::const_iterator i = ctor.begin(), i_end = ctor.end(); + if(i != i_end) { + os << "("; + do { + os << *i; + if(++i != i_end) { + os << ", "; + } + } while(i != i_end); + os << ")"; + } + + return os; +} + +std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) { + // can only output datatypes in the CVC4 native language + Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); + + os << arg.getName() << ": " << arg.getTypeName(); + + return os; +} + +}/* CVC4 namespace */ diff --git a/src/expr/datatype.h b/src/expr/datatype.h new file mode 100644 index 000000000..c1ec475e5 --- /dev/null +++ b/src/expr/datatype.h @@ -0,0 +1,866 @@ +/********************* */ +/*! \file datatype.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: Andrew Reynolds + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A class representing a Datatype definition + ** + ** A class representing a Datatype definition for the theory of + ** inductive datatypes. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__DATATYPE_H +#define __CVC4__DATATYPE_H + +#include <iostream> +#include <string> +#include <vector> +#include <map> + +namespace CVC4 { + // messy; Expr needs Datatype (because it's the payload of a + // CONSTANT-kinded expression), and Datatype needs Expr. + class CVC4_PUBLIC Datatype; +}/* CVC4 namespace */ + +#include "base/exception.h" +#include "expr/expr.h" +#include "expr/type.h" +#include "util/hash.h" + + +namespace CVC4 { + +class CVC4_PUBLIC ExprManager; + +class CVC4_PUBLIC DatatypeConstructor; +class CVC4_PUBLIC DatatypeConstructorArg; + +class CVC4_PUBLIC DatatypeConstructorIterator { + const std::vector<DatatypeConstructor>* d_v; + size_t d_i; + + friend class Datatype; + + DatatypeConstructorIterator(const std::vector<DatatypeConstructor>& v, bool start) : d_v(&v), d_i(start ? 0 : v.size()) { + } + +public: + typedef const DatatypeConstructor& value_type; + const DatatypeConstructor& operator*() const { return (*d_v)[d_i]; } + const DatatypeConstructor* operator->() const { return &(*d_v)[d_i]; } + DatatypeConstructorIterator& operator++() { ++d_i; return *this; } + DatatypeConstructorIterator operator++(int) { DatatypeConstructorIterator i(*this); ++d_i; return i; } + bool operator==(const DatatypeConstructorIterator& other) const { return d_v == other.d_v && d_i == other.d_i; } + bool operator!=(const DatatypeConstructorIterator& other) const { return d_v != other.d_v || d_i != other.d_i; } +};/* class DatatypeConstructorIterator */ + +class CVC4_PUBLIC DatatypeConstructorArgIterator { + const std::vector<DatatypeConstructorArg>* d_v; + size_t d_i; + + friend class DatatypeConstructor; + + DatatypeConstructorArgIterator(const std::vector<DatatypeConstructorArg>& v, bool start) : d_v(&v), d_i(start ? 0 : v.size()) { + } + +public: + typedef const DatatypeConstructorArg& value_type; + const DatatypeConstructorArg& operator*() const { return (*d_v)[d_i]; } + const DatatypeConstructorArg* operator->() const { return &(*d_v)[d_i]; } + DatatypeConstructorArgIterator& operator++() { ++d_i; return *this; } + DatatypeConstructorArgIterator operator++(int) { DatatypeConstructorArgIterator i(*this); ++d_i; return i; } + bool operator==(const DatatypeConstructorArgIterator& other) const { return d_v == other.d_v && d_i == other.d_i; } + bool operator!=(const DatatypeConstructorArgIterator& other) const { return d_v != other.d_v || d_i != other.d_i; } +};/* class DatatypeConstructorArgIterator */ + +/** + * An exception that is thrown when a datatype resolution fails. + */ +class CVC4_PUBLIC DatatypeResolutionException : public Exception { +public: + inline DatatypeResolutionException(std::string msg); +};/* class DatatypeResolutionException */ + +/** + * A holder type (used in calls to DatatypeConstructor::addArg()) + * to allow a Datatype to refer to itself. Self-typed fields of + * Datatypes will be properly typed when a Type is created for the + * Datatype by the ExprManager (which calls Datatype::resolve()). + */ +class CVC4_PUBLIC DatatypeSelfType { +};/* class DatatypeSelfType */ + +/** + * An unresolved type (used in calls to + * DatatypeConstructor::addArg()) to allow a Datatype to refer to + * itself or to other mutually-recursive Datatypes. Unresolved-type + * fields of Datatypes will be properly typed when a Type is created + * for the Datatype by the ExprManager (which calls + * Datatype::resolve()). + */ +class CVC4_PUBLIC DatatypeUnresolvedType { + std::string d_name; +public: + inline DatatypeUnresolvedType(std::string name); + inline std::string getName() const throw(); +};/* class DatatypeUnresolvedType */ + +/** + * A Datatype constructor argument (i.e., a Datatype field). + */ +class CVC4_PUBLIC DatatypeConstructorArg { + + std::string d_name; + Expr d_selector; + /** the constructor associated with this selector */ + Expr d_constructor; + bool d_resolved; + + DatatypeConstructorArg(std::string name, Expr selector); + friend class DatatypeConstructor; + friend class Datatype; + + bool isUnresolvedSelf() const throw(); + +public: + + /** Get the name of this constructor argument. */ + std::string getName() const throw(); + + /** + * Get the selector for this constructor argument; this call is + * only permitted after resolution. + */ + Expr getSelector() const; + + /** + * Get the associated constructor for this constructor argument; + * this call is only permitted after resolution. + */ + Expr getConstructor() const; + + /** + * Get the type of the selector for this constructor argument; + * this call is only permitted after resolution. + */ + SelectorType getType() const; + + /** + * Get the name of the type of this constructor argument + * (Datatype field). Can be used for not-yet-resolved Datatypes + * (in which case the name of the unresolved type, or "[self]" + * for a self-referential type is returned). + */ + std::string getTypeName() const; + + /** + * Returns true iff this constructor argument has been resolved. + */ + bool isResolved() const throw(); + +};/* class DatatypeConstructorArg */ + +/** + * A constructor for a Datatype. + */ +class CVC4_PUBLIC DatatypeConstructor { +public: + + /** The type for iterators over constructor arguments. */ + typedef DatatypeConstructorArgIterator iterator; + /** The (const) type for iterators over constructor arguments. */ + typedef DatatypeConstructorArgIterator const_iterator; + +private: + + std::string d_name; + Expr d_constructor; + Expr d_tester; + std::vector<DatatypeConstructorArg> d_args; + /** the operator associated with this constructor (for sygus) */ + Expr d_sygus_op; + Expr d_sygus_let_body; + std::vector< Expr > d_sygus_let_args; + unsigned d_sygus_num_let_input_args; + + void resolve(ExprManager* em, DatatypeType self, + const std::map<std::string, DatatypeType>& resolutions, + const std::vector<Type>& placeholders, + const std::vector<Type>& replacements, + const std::vector< SortConstructorType >& paramTypes, + const std::vector< DatatypeType >& paramReplacements, size_t cindex) + throw(IllegalArgumentException, DatatypeResolutionException); + friend class Datatype; + + /** Helper function for resolving parametric datatypes. + This replaces instances of the SortConstructorType produced for unresolved + parametric datatypes, with the corresponding resolved DatatypeType. For example, take + the parametric definition of a list, list[T] = cons(car : T, cdr : list[T]) | null. + If "range" is the unresolved parametric datatype: + DATATYPE list = cons(car: SORT_TAG_1, cdr: SORT_TAG_2(SORT_TAG_1)) | null END;, + this function will return the resolved type: + DATATYPE list = cons(car: SORT_TAG_1, cdr: (list PARAMETERIC_DATATYPE SORT_TAG_1)) | null END; + */ + Type doParametricSubstitution(Type range, + const std::vector< SortConstructorType >& paramTypes, + const std::vector< DatatypeType >& paramReplacements); + + /** compute the cardinality of this datatype */ + Cardinality computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException); + /** compute whether this datatype is well-founded */ + bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException); + /** compute ground term */ + Expr computeGroundTerm( Type t, std::vector< Type >& processing, std::map< Type, Expr >& gt ) const throw(IllegalArgumentException); +public: + /** + * Create a new Datatype constructor with the given name for the + * constructor and the same name (prefixed with "is_") for the + * tester. The actual constructor and tester (meaning, the Exprs + * representing operators for these entities) aren't created until + * resolution time. + */ + explicit DatatypeConstructor(std::string name); + + /** + * Create a new Datatype constructor with the given name for the + * constructor and the given name for the tester. The actual + * constructor and tester aren't created until resolution time. + */ + DatatypeConstructor(std::string name, std::string tester); + + /** set sygus */ + void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus ); + + /** + * Add an argument (i.e., a data field) of the given name and type + * to this Datatype constructor. Selector names need not be unique; + * they are for convenience and pretty-printing only. + */ + void addArg(std::string selectorName, Type selectorType); + + /** + * Add an argument (i.e., a data field) of the given name to this + * Datatype constructor that refers to an as-yet-unresolved + * Datatype (which may be mutually-recursive). Selector names need + * not be unique; they are for convenience and pretty-printing only. + */ + void addArg(std::string selectorName, DatatypeUnresolvedType selectorType); + + /** + * Add a self-referential (i.e., a data field) of the given name + * to this Datatype constructor that refers to the enclosing + * Datatype. For example, using the familiar "nat" Datatype, to + * create the "pred" field for "succ" constructor, one uses + * succ::addArg("pred", DatatypeSelfType())---the actual Type + * cannot be passed because the Datatype is still under + * construction. Selector names need not be unique; they are for + * convenience and pretty-printing only. + * + * This is a special case of + * DatatypeConstructor::addArg(std::string, DatatypeUnresolvedType). + */ + void addArg(std::string selectorName, DatatypeSelfType); + + /** Get the name of this Datatype constructor. */ + std::string getName() const throw(); + + /** + * Get the constructor operator of this Datatype constructor. The + * Datatype must be resolved. + */ + Expr getConstructor() const; + + /** + * Get the tester operator of this Datatype constructor. The + * Datatype must be resolved. + */ + Expr getTester() const; + + /** get sygus op */ + Expr getSygusOp() const; + /** get sygus let body */ + Expr getSygusLetBody() const; + /** get number of sygus let args */ + unsigned getNumSygusLetArgs() const; + /** get sygus let arg */ + Expr getSygusLetArg( unsigned i ) const; + /** get number of let arguments that should be printed as arguments to let */ + unsigned getNumSygusLetInputArgs() const; + /** is this a sygus identity function */ + bool isSygusIdFunc() const; + + /** + * Get the tester name for this Datatype constructor. + */ + std::string getTesterName() const throw(); + + /** + * Get the number of arguments (so far) of this Datatype constructor. + */ + inline size_t getNumArgs() const throw(); + + /** + * Get the specialized constructor type for a parametric + * constructor; this call is only permitted after resolution. + * Given a (concrete) returnType, the constructor's concrete + * type in this parametric datatype is returned. + * + * For instance, if the datatype is list[T], with constructor + * "cons[T]" of type "T -> list[T] -> list[T]", then calling + * this function with "list[int]" will return the concrete + * "cons" constructor type for lists of int---namely, + * "int -> list[int] -> list[int]". + */ + Type getSpecializedConstructorType(Type returnType) const; + + /** + * Return the cardinality of this constructor (the product of the + * cardinalities of its arguments). + */ + Cardinality getCardinality() const throw(IllegalArgumentException); + + /** + * Return true iff this constructor is finite (it is nullary or + * each of its argument types are finite). This function can + * only be called for resolved constructors. + */ + bool isFinite() const throw(IllegalArgumentException); + + /** + * Returns true iff this Datatype constructor has already been + * resolved. + */ + inline bool isResolved() const throw(); + + /** Get the beginning iterator over DatatypeConstructor args. */ + inline iterator begin() throw(); + /** Get the ending iterator over DatatypeConstructor args. */ + inline iterator end() throw(); + /** Get the beginning const_iterator over DatatypeConstructor args. */ + inline const_iterator begin() const throw(); + /** Get the ending const_iterator over DatatypeConstructor args. */ + inline const_iterator end() const throw(); + + /** Get the ith DatatypeConstructor arg. */ + const DatatypeConstructorArg& operator[](size_t index) const; + + /** + * Get the DatatypeConstructor arg named. This is a linear search + * through the arguments, so in the case of multiple, + * similarly-named arguments, the first is returned. + */ + const DatatypeConstructorArg& operator[](std::string name) const; + + /** + * Get the selector named. This is a linear search + * through the arguments, so in the case of multiple, + * similarly-named arguments, the selector for the first + * is returned. + */ + Expr getSelector(std::string name) const; + + /** + * Get whether this datatype involves an external type. If so, + * then we will pose additional requirements for sharing. + */ + bool involvesExternalType() const; + +};/* class DatatypeConstructor */ + +/** + * The representation of an inductive datatype. + * + * This is far more complicated than it first seems. Consider this + * datatype definition: + * + * DATATYPE nat = + * succ(pred: nat) + * | zero + * END; + * + * You cannot define "nat" until you have a Type for it, but you + * cannot have a Type for it until you fill in the type of the "pred" + * selector, which needs the Type. So we have a chicken-and-egg + * problem. It's even more complicated when we have mutual recursion + * between datatypes, since the CVC presentation language does not + * require forward-declarations. Here, we define trees of lists that + * contain trees of lists (etc): + * + * DATATYPE + * tree = node(left: tree, right: tree) | leaf(list), + * list = cons(car: tree, cdr: list) | nil + * END; + * + * Note that while parsing the "tree" definition, we have to take it + * on faith that "list" is a valid type. We build Datatype objects to + * describe "tree" and "list", and their constructors and constructor + * arguments, but leave any unknown types (including self-references) + * in an "unresolved" state. After parsing the whole DATATYPE block, + * we create a DatatypeType through + * ExprManager::mkMutualDatatypeTypes(). The ExprManager creates a + * DatatypeType for each, but before "releasing" this type into the + * wild, it does a round of in-place "resolution" on each Datatype by + * calling Datatype::resolve() with a map of string -> DatatypeType to + * allow the datatype to construct the necessary testers and + * selectors. + * + * An additional point to make is that we want to ease the burden on + * both the parser AND the users of the CVC4 API, so this class takes + * on the task of generating its own selectors and testers, for + * instance. That means that, after reifying the Datatype with the + * ExprManager, the parser needs to go through the (now-resolved) + * Datatype and request the constructor, selector, and tester terms. + * See src/parser/parser.cpp for how this is done. For API usage + * ideas, see test/unit/util/datatype_black.h. + * + * Datatypes may also be defined parametrically, such as this example: + * + * DATATYPE + * list[T] = cons(car : T, cdr : list[T]) | null, + * tree = node(children : list[tree]) | leaf + * END; + * + * Here, the definition of the parametric datatype list, where T is a type variable. + * In other words, this defines a family of types list[C] where C is any concrete + * type. Datatypes can be parameterized over multiple type variables using the + * syntax sym[ T1, ..., Tn ] = ..., + * + */ +class CVC4_PUBLIC Datatype { + friend class DatatypeConstructor; +public: + /** + * Get the datatype of a constructor, selector, or tester operator. + */ + static const Datatype& datatypeOf(Expr item) CVC4_PUBLIC; + + /** + * Get the index of a constructor or tester in its datatype, or the + * index of a selector in its constructor. (Zero is always the + * first index.) + */ + static size_t indexOf(Expr item) CVC4_PUBLIC; + + /** + * Get the index of constructor corresponding to selector. (Zero is + * always the first index.) + */ + static size_t cindexOf(Expr item) CVC4_PUBLIC; + + /** The type for iterators over constructors. */ + typedef DatatypeConstructorIterator iterator; + /** The (const) type for iterators over constructors. */ + typedef DatatypeConstructorIterator const_iterator; + +private: + std::string d_name; + std::vector<Type> d_params; + bool d_isCo; + std::vector<DatatypeConstructor> d_constructors; + bool d_resolved; + Type d_self; + bool d_involvesExt; + /** information for sygus */ + Type d_sygus_type; + Expr d_sygus_bvl; + bool d_sygus_allow_const; + bool d_sygus_allow_all; + + // "mutable" because computing the cardinality can be expensive, + // and so it's computed just once, on demand---this is the cache + mutable Cardinality d_card; + + // is this type a recursive singleton type + mutable int d_card_rec_singleton; + // if d_card_rec_singleton is true, + // infinite cardinality depends on at least one of the following uninterpreted sorts having cardinality > 1 + mutable std::vector< Type > d_card_u_assume; + // is this well-founded + mutable int d_well_founded; + // ground term for this datatype + mutable std::map< Type, Expr > d_ground_term; + + /** + * Datatypes refer to themselves, recursively, and we have a + * chicken-and-egg problem. The DatatypeType around the Datatype + * cannot exist until the Datatype is finalized, and the Datatype + * cannot refer to the DatatypeType representing itself until it + * exists. resolve() is called by the ExprManager when a Type is + * ultimately requested of the Datatype specification (that is, when + * ExprManager::mkDatatypeType() or ExprManager::mkMutualDatatypeTypes() + * is called). Has the effect of freezing the object, too; that is, + * addConstructor() will fail after a call to resolve(). + * + * The basic goal of resolution is to assign constructors, selectors, + * and testers. To do this, any UnresolvedType/SelfType references + * must be cleared up. This is the purpose of the "resolutions" map; + * it includes any mutually-recursive datatypes that are currently + * under resolution. The four vectors come in two pairs (so, really + * they are two maps). placeholders->replacements give type variables + * that should be resolved in the case of parametric datatypes. + * + * @param em the ExprManager at play + * @param resolutions a map of strings to DatatypeTypes currently under resolution + * @param placeholders the types in these Datatypes under resolution that must be replaced + * @param replacements the corresponding replacements + * @param paramTypes the sort constructors in these Datatypes under resolution that must be replaced + * @param paramReplacements the corresponding (parametric) DatatypeTypes + */ + void resolve(ExprManager* em, + const std::map<std::string, DatatypeType>& resolutions, + const std::vector<Type>& placeholders, + const std::vector<Type>& replacements, + const std::vector< SortConstructorType >& paramTypes, + const std::vector< DatatypeType >& paramReplacements) + throw(IllegalArgumentException, DatatypeResolutionException); + friend class ExprManager;// for access to resolve() + + /** compute the cardinality of this datatype */ + Cardinality computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException); + /** compute whether this datatype is a recursive singleton */ + bool computeCardinalityRecSingleton( std::vector< Type >& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException); + /** compute whether this datatype is well-founded */ + bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException); + /** compute ground term */ + Expr computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException); +public: + + /** Create a new Datatype of the given name. */ + inline explicit Datatype(std::string name, bool isCo = false); + + /** + * Create a new Datatype of the given name, with the given + * parameterization. + */ + inline Datatype(std::string name, const std::vector<Type>& params, bool isCo = false); + + /** + * Add a constructor to this Datatype. Constructor names need not + * be unique; they are for convenience and pretty-printing only. + */ + void addConstructor(const DatatypeConstructor& c); + + /** set the sygus information of this datatype + * st : the builtin type for this grammar + * bvl : the list of arguments for the synth-fun + * allow_const : whether all constants are (implicitly) included in the grammar + */ + void setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ); + + /** Get the name of this Datatype. */ + inline std::string getName() const throw(); + + /** Get the number of constructors (so far) for this Datatype. */ + inline size_t getNumConstructors() const throw(); + + /** Is this datatype parametric? */ + inline bool isParametric() const throw(); + + /** Get the nubmer of type parameters */ + inline size_t getNumParameters() const throw(); + + /** Get parameter */ + inline Type getParameter( unsigned int i ) const; + + /** Get parameters */ + inline std::vector<Type> getParameters() const; + + /** is this a co-datatype? */ + inline bool isCodatatype() const; + + /** is this a sygus datatype? */ + inline bool isSygus() const; + + /** + * Return the cardinality of this datatype (the sum of the + * cardinalities of its constructors). The Datatype must be + * resolved. + */ + Cardinality getCardinality() const throw(IllegalArgumentException); + + /** + * Return true iff this Datatype is finite (all constructors are + * finite, i.e., there are finitely many ground terms). If the + * datatype is not well-founded, this function returns false. The + * Datatype must be resolved or an exception is thrown. + */ + bool isFinite() const throw(IllegalArgumentException); + + /** + * Return true iff this datatype is well-founded (there exist ground + * terms). The Datatype must be resolved or an exception is thrown. + */ + bool isWellFounded() const throw(IllegalArgumentException); + + /** + * Return true iff this datatype is a recursive singleton + */ + bool isRecursiveSingleton() const throw(IllegalArgumentException); + + + /** get number of recursive singleton argument types */ + unsigned getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException); + Type getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException); + + /** + * Construct and return a ground term of this Datatype. The + * Datatype must be both resolved and well-founded, or else an + * exception is thrown. + */ + Expr mkGroundTerm( Type t ) const throw(IllegalArgumentException); + + /** + * Get the DatatypeType associated to this Datatype. Can only be + * called post-resolution. + */ + DatatypeType getDatatypeType() const throw(IllegalArgumentException); + + /** + * Get the DatatypeType associated to this (parameterized) Datatype. Can only be + * called post-resolution. + */ + DatatypeType getDatatypeType(const std::vector<Type>& params) const throw(IllegalArgumentException); + + /** + * Return true iff the two Datatypes are the same. + * + * We need == for mkConst(Datatype) to properly work---since if the + * Datatype Expr requested is the same as an already-existing one, + * we need to return that one. For that, we have a hash and + * operator==. We provide != for symmetry. We don't provide + * operator<() etc. because given two Datatype Exprs, you could + * simply compare those rather than the (bare) Datatypes. This + * means, though, that Datatype cannot be stored in a sorted list or + * RB tree directly, so maybe we can consider adding these + * comparison operators later on. + */ + bool operator==(const Datatype& other) const throw(); + /** Return true iff the two Datatypes are not the same. */ + inline bool operator!=(const Datatype& other) const throw(); + + /** Return true iff this Datatype has already been resolved. */ + inline bool isResolved() const throw(); + + /** Get the beginning iterator over DatatypeConstructors. */ + inline iterator begin() throw(); + /** Get the ending iterator over DatatypeConstructors. */ + inline iterator end() throw(); + /** Get the beginning const_iterator over DatatypeConstructors. */ + inline const_iterator begin() const throw(); + /** Get the ending const_iterator over DatatypeConstructors. */ + inline const_iterator end() const throw(); + + /** Get the ith DatatypeConstructor. */ + const DatatypeConstructor& operator[](size_t index) const; + + /** + * Get the DatatypeConstructor named. This is a linear search + * through the constructors, so in the case of multiple, + * similarly-named constructors, the first is returned. + */ + const DatatypeConstructor& operator[](std::string name) const; + + /** + * Get the constructor operator for the named constructor. + * This is a linear search through the constructors, so in + * the case of multiple, similarly-named constructors, the + * first is returned. + * + * This Datatype must be resolved. + */ + Expr getConstructor(std::string name) const; + + /** get sygus type */ + Type getSygusType() const; + /** get sygus var list */ + Expr getSygusVarList() const; + /** does it allow constants */ + bool getSygusAllowConst() const; + /** does it allow constants */ + bool getSygusAllowAll() const; + + /** + * Get whether this datatype involves an external type. If so, + * then we will pose additional requirements for sharing. + */ + bool involvesExternalType() const; + +};/* class Datatype */ + +/** + * A hash function for Datatypes. Needed to store them in hash sets + * and hash maps. + */ +struct CVC4_PUBLIC DatatypeHashFunction { + inline size_t operator()(const Datatype& dt) const { + return StringHashFunction()(dt.getName()); + } + inline size_t operator()(const Datatype* dt) const { + return StringHashFunction()(dt->getName()); + } + inline size_t operator()(const DatatypeConstructor& dtc) const { + return StringHashFunction()(dtc.getName()); + } + inline size_t operator()(const DatatypeConstructor* dtc) const { + return StringHashFunction()(dtc->getName()); + } +};/* struct DatatypeHashFunction */ + +// FUNCTION DECLARATIONS FOR OUTPUT STREAMS + +std::ostream& operator<<(std::ostream& os, const Datatype& dt) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) CVC4_PUBLIC; + +// INLINE FUNCTIONS + +inline DatatypeResolutionException::DatatypeResolutionException(std::string msg) : + Exception(msg) { +} + +inline DatatypeUnresolvedType::DatatypeUnresolvedType(std::string name) : + d_name(name) { +} + +inline std::string DatatypeUnresolvedType::getName() const throw() { + return d_name; +} + +inline Datatype::Datatype(std::string name, bool isCo) : + d_name(name), + d_params(), + d_isCo(isCo), + d_constructors(), + d_resolved(false), + d_self(), + d_involvesExt(false), + d_card(CardinalityUnknown()), + d_card_rec_singleton(0), + d_well_founded(0) { +} + +inline Datatype::Datatype(std::string name, const std::vector<Type>& params, bool isCo) : + d_name(name), + d_params(params), + d_isCo(isCo), + d_constructors(), + d_resolved(false), + d_self(), + d_involvesExt(false), + d_card(CardinalityUnknown()), + d_card_rec_singleton(0), + d_well_founded(0) { +} + +inline std::string Datatype::getName() const throw() { + return d_name; +} + +inline size_t Datatype::getNumConstructors() const throw() { + return d_constructors.size(); +} + +inline bool Datatype::isParametric() const throw() { + return d_params.size() > 0; +} + +inline size_t Datatype::getNumParameters() const throw() { + return d_params.size(); +} + +inline Type Datatype::getParameter( unsigned int i ) const { + CheckArgument(isParametric(), this, "cannot get type parameter of a non-parametric datatype"); + CheckArgument(i < d_params.size(), i, "type parameter index out of range for datatype"); + return d_params[i]; +} + +inline std::vector<Type> Datatype::getParameters() const { + CheckArgument(isParametric(), this, "cannot get type parameters of a non-parametric datatype"); + return d_params; +} + +inline bool Datatype::isCodatatype() const { + return d_isCo; +} + +inline bool Datatype::isSygus() const { + return !d_sygus_type.isNull(); +} + +inline bool Datatype::operator!=(const Datatype& other) const throw() { + return !(*this == other); +} + +inline bool Datatype::isResolved() const throw() { + return d_resolved; +} + +inline Datatype::iterator Datatype::begin() throw() { + return iterator(d_constructors, true); +} + +inline Datatype::iterator Datatype::end() throw() { + return iterator(d_constructors, false); +} + +inline Datatype::const_iterator Datatype::begin() const throw() { + return const_iterator(d_constructors, true); +} + +inline Datatype::const_iterator Datatype::end() const throw() { + return const_iterator(d_constructors, false); +} + +inline bool DatatypeConstructor::isResolved() const throw() { + return !d_tester.isNull(); +} + +inline size_t DatatypeConstructor::getNumArgs() const throw() { + return d_args.size(); +} + +inline bool DatatypeConstructorArg::isResolved() const throw() { + // We could just write: + // + // return !d_selector.isNull() && d_selector.getType().isSelector(); + // + // HOWEVER, this causes problems in ExprManager tear-down, because + // the attributes are removed before the pool is purged. When the + // pool is purged, this triggers an equality test between Datatypes, + // and this triggers a call to isResolved(), which breaks because + // d_selector has no type after attributes are stripped. + // + // This problem, coupled with the fact that this function is called + // _often_, means we should just use a boolean flag. + // + return d_resolved; +} + +inline DatatypeConstructor::iterator DatatypeConstructor::begin() throw() { + return iterator(d_args, true); +} + +inline DatatypeConstructor::iterator DatatypeConstructor::end() throw() { + return iterator(d_args, false); +} + +inline DatatypeConstructor::const_iterator DatatypeConstructor::begin() const throw() { + return const_iterator(d_args, true); +} + +inline DatatypeConstructor::const_iterator DatatypeConstructor::end() const throw() { + return const_iterator(d_args, false); +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__DATATYPE_H */ diff --git a/src/expr/datatype.i b/src/expr/datatype.i new file mode 100644 index 000000000..a7456df38 --- /dev/null +++ b/src/expr/datatype.i @@ -0,0 +1,175 @@ +%{ +#include "expr/datatype.h" + +#ifdef SWIGJAVA + +#include "bindings/java_iterator_adapter.h" +#include "bindings/java_stream_adapters.h" + +#endif /* SWIGJAVA */ +%} + +%extend std::vector< CVC4::Datatype > { + /* These member functions have slightly different signatures in + * different swig language packages. The underlying issue is that + * DatatypeConstructor doesn't have a default constructor */ +#if defined(SWIGOCAML) || defined(SWIGPERL) || defined(SWIGTCL) + %ignore vector(unsigned int size = 0); + %ignore set( int i, const CVC4::Datatype &x ); + %ignore to_array(); +#endif /* SWIGOCAML || SWIGPERL || SWIGTCL */ + %ignore vector(size_type);// java/python/perl/others? + %ignore resize(size_type);// java/python/perl/others? + %ignore set(int i, const CVC4::Datatype& x); + %ignore to_array(); +}; +%template(vectorDatatype) std::vector< CVC4::Datatype >; + +%extend std::vector< CVC4::DatatypeConstructor > { + /* These member functions have slightly different signatures in + * different swig language packages. The underlying issue is that + * DatatypeConstructor doesn't have a default constructor */ +#if defined(SWIGOCAML) || defined(SWIGPERL) || defined(SWIGTCL) + %ignore vector(unsigned int size = 0); + %ignore set( int i, const CVC4::DatatypeConstructor &x ); + %ignore to_array(); +#endif /* SWIGOCAML || SWIGPERL || SWIGTCL */ + %ignore vector(size_type);// java/python/perl/others? + %ignore resize(size_type);// java/python/perl/others? + %ignore set(int i, const CVC4::Datatype::Constructor& x); + %ignore to_array(); +}; +//%template(vectorDatatypeConstructor) std::vector< CVC4::DatatypeConstructor >; + +%rename(equals) CVC4::Datatype::operator==(const Datatype&) const; +%ignore CVC4::Datatype::operator!=(const Datatype&) const; + +%ignore CVC4::Datatype::begin(); +%ignore CVC4::Datatype::end(); +%ignore CVC4::Datatype::begin() const; +%ignore CVC4::Datatype::end() const; + +%rename(get) CVC4::Datatype::operator[](size_t) const; +%rename(get) CVC4::Datatype::operator[](std::string) const; + +%rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype&) const; +%ignore CVC4::DatatypeHashFunction::operator()(const Datatype*) const; +%rename(apply) CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor&) const; +%ignore CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor*) const; + +%ignore CVC4::DatatypeConstructor::begin(); +%ignore CVC4::DatatypeConstructor::end(); +%ignore CVC4::DatatypeConstructor::begin() const; +%ignore CVC4::DatatypeConstructor::end() const; + +%rename(get) CVC4::DatatypeConstructor::operator[](size_t) const; +%rename(get) CVC4::DatatypeConstructor::operator[](std::string) const; + +%ignore CVC4::operator<<(std::ostream&, const Datatype&); +%ignore CVC4::operator<<(std::ostream&, const DatatypeConstructor&); +%ignore CVC4::operator<<(std::ostream&, const DatatypeConstructorArg&); + +%ignore CVC4::DatatypeConstructorIterator; +%ignore CVC4::DatatypeConstructorArgIterator; + +%feature("valuewrapper") CVC4::DatatypeUnresolvedType; +%feature("valuewrapper") CVC4::DatatypeConstructor; + +#ifdef SWIGJAVA + +// Instead of Datatype::begin() and end(), create an +// iterator() method on the Java side that returns a Java-style +// Iterator. +%extend CVC4::Datatype { + CVC4::JavaIteratorAdapter<CVC4::Datatype> iterator() { + return CVC4::JavaIteratorAdapter<CVC4::Datatype>(*$self); + } + + std::string toString() const { + std::stringstream ss; + ss << *$self; + return ss.str(); + } +} +%extend CVC4::DatatypeConstructor { + CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> iterator() { + return CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor>(*$self); + } + + std::string toString() const { + std::stringstream ss; + ss << *$self; + return ss.str(); + } +} +%extend CVC4::DatatypeConstructorArg { + std::string toString() const { + std::stringstream ss; + ss << *$self; + return ss.str(); + } +} + +// Datatype is "iterable" on the Java side +%typemap(javainterfaces) CVC4::Datatype "java.lang.Iterable<DatatypeConstructor>"; +%typemap(javainterfaces) CVC4::DatatypeConstructor "java.lang.Iterable<DatatypeConstructorArg>"; + +// the JavaIteratorAdapter should not be public, and implements Iterator +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Datatype> "class"; +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Datatype> "java.util.Iterator<DatatypeConstructor>"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> "java.util.Iterator<DatatypeConstructorArg>"; +// add some functions to the Java side (do it here because there's no way to do these in C++) +%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::Datatype> " + public void remove() { + throw new java.lang.UnsupportedOperationException(); + } + + public DatatypeConstructor next() { + if(hasNext()) { + return getNext(); + } else { + throw new java.util.NoSuchElementException(); + } + } +" +%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> " + public void remove() { + throw new java.lang.UnsupportedOperationException(); + } + + public DatatypeConstructorArg next() { + if(hasNext()) { + return getNext(); + } else { + throw new java.util.NoSuchElementException(); + } + } +" +// getNext() just allows C++ iterator access from Java-side next(), make it private +%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Datatype>::getNext() "private"; +%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor>::getNext() "private"; + +// map the types appropriately. +%typemap(jni) CVC4::Datatype::iterator::value_type "jobject"; +%typemap(jtype) CVC4::Datatype::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructor"; +%typemap(jstype) CVC4::Datatype::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructor"; +%typemap(javaout) CVC4::Datatype::iterator::value_type { return $jnicall; } +%typemap(jni) CVC4::DatatypeConstructor::iterator::value_type "jobject"; +%typemap(jtype) CVC4::DatatypeConstructor::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructorArg"; +%typemap(jstype) CVC4::DatatypeConstructor::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructorArg"; +%typemap(javaout) CVC4::DatatypeConstructor::iterator::value_type { return $jnicall; } + +#endif /* SWIGJAVA */ + +%include "expr/datatype.h" + +#ifdef SWIGJAVA + +%include "bindings/java_iterator_adapter.h" +%include "bindings/java_stream_adapters.h" + +%template(JavaIteratorAdapter_Datatype) CVC4::JavaIteratorAdapter<CVC4::Datatype>; +%template(JavaIteratorAdapter_DatatypeConstructor) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor>; + +#endif /* SWIGJAVA */ diff --git a/src/expr/emptyset.cpp b/src/expr/emptyset.cpp new file mode 100644 index 000000000..69e34b848 --- /dev/null +++ b/src/expr/emptyset.cpp @@ -0,0 +1,28 @@ +/********************* */ +/*! \file emptyset.cpp + ** \verbatim + ** Original author: Kshitij Bansal + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "expr/emptyset.h" + +#include <iostream> + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const EmptySet& asa) { + return out << "emptyset(" << asa.getType() << ')'; +} + +}/* CVC4 namespace */ diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h new file mode 100644 index 000000000..4b3bb204f --- /dev/null +++ b/src/expr/emptyset.h @@ -0,0 +1,83 @@ +/********************* */ +/*! \file emptyset.h + ** \verbatim + ** Original author: Kshitij Bansal + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#pragma once + +namespace CVC4 { + // messy; Expr needs EmptySet (because it's the payload of a + // CONSTANT-kinded expression), and EmptySet needs Expr. + class CVC4_PUBLIC EmptySet; +}/* CVC4 namespace */ + +#include "expr/expr.h" +#include "expr/type.h" +#include <iostream> + +namespace CVC4 { + +class CVC4_PUBLIC EmptySet { + + const SetType d_type; + + EmptySet() { } +public: + + /** + * Constructs an emptyset of the specified type. Note that the argument + * is the type of the set itself, NOT the type of the elements. + */ + EmptySet(SetType setType):d_type(setType) { } + + + ~EmptySet() throw() { + } + + SetType getType() const { return d_type; } + + bool operator==(const EmptySet& es) const throw() { + return d_type == es.d_type; + } + bool operator!=(const EmptySet& es) const throw() { + return !(*this == es); + } + + bool operator<(const EmptySet& es) const throw() { + return d_type < es.d_type; + } + bool operator<=(const EmptySet& es) const throw() { + return d_type <= es.d_type; + } + bool operator>(const EmptySet& es) const throw() { + return !(*this <= es); + } + bool operator>=(const EmptySet& es) const throw() { + return !(*this < es); + } + +};/* class EmptySet */ + +std::ostream& operator<<(std::ostream& out, const EmptySet& es) CVC4_PUBLIC; + +struct CVC4_PUBLIC EmptySetHashFunction { + inline size_t operator()(const EmptySet& es) const { + return TypeHashFunction()(es.getType()); + } +};/* struct EmptySetHashFunction */ + +}/* CVC4 namespace */ diff --git a/src/expr/emptyset.i b/src/expr/emptyset.i new file mode 100644 index 000000000..ada3dd583 --- /dev/null +++ b/src/expr/emptyset.i @@ -0,0 +1,17 @@ +%{ +#include "expr/emptyset.h" +%} + +%rename(equals) CVC4::EmptySet::operator==(const EmptySet&) const; +%ignore CVC4::EmptySet::operator!=(const EmptySet&) const; + +%rename(less) CVC4::EmptySet::operator<(const EmptySet&) const; +%rename(lessEqual) CVC4::EmptySet::operator<=(const EmptySet&) const; +%rename(greater) CVC4::EmptySet::operator>(const EmptySet&) const; +%rename(greaterEqual) CVC4::EmptySet::operator>=(const EmptySet&) const; + +%rename(apply) CVC4::EmptySetHashFunction::operator()(const EmptySet&) const; + +%ignore CVC4::operator<<(std::ostream& out, const EmptySet& es); + +%include "expr/emptyset.h" diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 91387bc41..e7088a395 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -14,14 +14,15 @@ ** Public-facing expression manager interface, implementation. **/ -#include "expr/node_manager.h" #include "expr/expr_manager.h" -#include "expr/variable_type_map.h" -#include "options/options.h" -#include "util/statistics_registry.h" #include <map> +#include "expr/node_manager.h" +#include "expr/statistics_registry.h" +#include "expr/variable_type_map.h" +#include "options/options.h" + ${includes} // This is a hack, but an important one: if there's an error, the diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index d7c89ecdc..31983d5a9 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -21,12 +21,11 @@ #include <vector> +#include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" -#include "expr/expr.h" +#include "expr/statistics.h" #include "util/subrange_bound.h" -#include "util/statistics.h" -#include "util/sexpr.h" ${includes} @@ -34,7 +33,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 38 "${template}" +#line 37 "${template}" namespace CVC4 { diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 47042b458..0739e3355 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -14,11 +14,11 @@ ** Public-facing expression interface, implementation. **/ +#include "base/cvc4_assert.h" #include "expr/expr.h" #include "expr/node.h" #include "expr/expr_manager_scope.h" #include "expr/variable_type_map.h" -#include "util/cvc4_assert.h" #include "expr/node_manager_attributes.h" #include <vector> diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index ae0fad897..f609d8990 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -26,21 +26,22 @@ ${includes} #ifndef __CVC4__EXPR_H #define __CVC4__EXPR_H -#include <string> +#include <stdint.h> #include <iostream> #include <iterator> -#include <stdint.h> -#include "util/exception.h" -#include "util/language.h" +#include <string> + +#include "base/exception.h" +#include "options/expr_options.h" +#include "options/language.h" #include "util/hash.h" -#include "expr/options.h" // This is a hack, but an important one: if there's an error, the // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 44 "${template}" +#line 45 "${template}" namespace CVC4 { @@ -934,7 +935,7 @@ public: ${getConst_instantiations} -#line 938 "${template}" +#line 939 "${template}" namespace expr { diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index f93df4132..c2ccb6b5e 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -22,7 +22,7 @@ #include <iostream> #include <sstream> -#include "util/exception.h" +#include "base/exception.h" namespace CVC4 { namespace kind { diff --git a/src/expr/matcher.h b/src/expr/matcher.h new file mode 100644 index 000000000..92b1ce109 --- /dev/null +++ b/src/expr/matcher.h @@ -0,0 +1,119 @@ +/********************* */ +/*! \file matcher.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: Andrew Reynolds + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A class representing a type matcher + ** + ** A class representing a type matcher. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__MATCHER_H +#define __CVC4__MATCHER_H + +#include <iostream> +#include <string> +#include <vector> +#include <map> + +#include "base/cvc4_assert.h" +#include "expr/node.h" +#include "expr/type_node.h" + +namespace CVC4 { + +class Matcher { +private: + std::vector< TypeNode > d_types; + std::vector< TypeNode > d_match; +public: + Matcher(){} + Matcher( DatatypeType dt ){ + addTypesFromDatatype( dt ); + } + ~Matcher(){} + + void addTypesFromDatatype( DatatypeType dt ){ + std::vector< Type > argTypes = dt.getParamTypes(); + addTypes( argTypes ); + Debug("typecheck-idt") << "instantiating matcher for " << dt << std::endl; + for(unsigned i = 0; i < argTypes.size(); ++i) { + if(dt.isParameterInstantiated(i)) { + Debug("typecheck-idt") << "++ instantiate param " << i << " : " << d_types[i] << std::endl; + d_match[i] = d_types[i]; + } + } + } + void addType( Type t ){ + d_types.push_back( TypeNode::fromType( t ) ); + d_match.push_back( TypeNode::null() ); + } + void addTypes( std::vector< Type > types ){ + for( int i=0; i<(int)types.size(); i++ ){ + addType( types[i] ); + } + } + + bool doMatching( TypeNode pattern, TypeNode tn ){ + Debug("typecheck-idt") << "doMatching() : " << pattern << " : " << tn << std::endl; + std::vector< TypeNode >::iterator i = std::find( d_types.begin(), d_types.end(), pattern ); + if( i!=d_types.end() ){ + int index = i - d_types.begin(); + if( !d_match[index].isNull() ){ + Debug("typecheck-idt") << "check subtype " << tn << " " << d_match[index] << std::endl; + TypeNode tnn = TypeNode::leastCommonTypeNode( tn, d_match[index] ); + //recognize subtype relation + if( !tnn.isNull() ){ + d_match[index] = tnn; + return true; + }else{ + return false; + } + }else{ + d_match[ i - d_types.begin() ] = tn; + return true; + } + }else if( pattern==tn ){ + return true; + }else if( pattern.getKind()!=tn.getKind() || pattern.getNumChildren()!=tn.getNumChildren() ){ + return false; + }else{ + for( int i=0; i<(int)pattern.getNumChildren(); i++ ){ + if( !doMatching( pattern[i], tn[i] ) ){ + return false; + } + } + return true; + } + } + + TypeNode getMatch( unsigned int i ){ return d_match[i]; } + void getTypes( std::vector<Type>& types ) { + types.clear(); + for( int i=0; i<(int)d_match.size(); i++ ){ + types.push_back( d_types[i].toType() ); + } + } + void getMatches( std::vector<Type>& types ) { + types.clear(); + for( int i=0; i<(int)d_match.size(); i++ ){ + if(d_match[i].isNull()) { + types.push_back( d_types[i].toType() ); + } else { + types.push_back( d_match[i].toType() ); + } + } + } +};/* class Matcher */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__MATCHER_H */ diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 73f48ba04..539db1c91 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -21,8 +21,8 @@ #include <iostream> +#include "base/cvc4_assert.h" #include "expr/kind.h" -#include "util/cvc4_assert.h" namespace CVC4 { diff --git a/src/expr/node.cpp b/src/expr/node.cpp index deceda840..2b5c0a2c8 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -13,14 +13,15 @@ ** ** Reference-counted encapsulation of a pointer to node information. **/ - #include "expr/node.h" -#include "expr/attribute.h" -#include "util/output.h" #include <iostream> #include <cstring> +#include "base/output.h" +#include "expr/attribute.h" + + using namespace std; namespace CVC4 { diff --git a/src/expr/node.h b/src/expr/node.h index 2a884d35a..384dbcc03 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -30,15 +30,15 @@ #include <functional> #include <stdint.h> +#include "base/cvc4_assert.h" +#include "base/exception.h" +#include "base/output.h" #include "expr/type.h" #include "expr/kind.h" #include "expr/metakind.h" #include "expr/expr.h" -#include "util/cvc4_assert.h" +#include "options/language.h" #include "util/configuration.h" -#include "util/output.h" -#include "util/exception.h" -#include "util/language.h" #include "util/utility.h" #include "util/hash.h" diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index bea51b576..e1a083a78 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -169,11 +169,12 @@ namespace CVC4 { class NodeManager; }/* CVC4 namespace */ +#include "base/cvc4_assert.h" +#include "base/output.h" #include "expr/kind.h" #include "expr/metakind.h" -#include "util/cvc4_assert.h" #include "expr/node_value.h" -#include "util/output.h" + namespace CVC4 { @@ -751,7 +752,7 @@ public: #include "expr/node.h" #include "expr/node_manager.h" -#include "expr/options.h" +#include "options/expr_options.h" namespace CVC4 { diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index dad21e90a..1b9bfcd10 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -15,24 +15,23 @@ ** ** Reviewed by Chris Conway, Apr 5 2010 (bug #65). **/ - #include "expr/node_manager.h" -#include "expr/node_manager_attributes.h" - -#include "expr/attribute.h" -#include "util/cvc4_assert.h" -#include "options/options.h" -#include "smt/options.h" -#include "util/statistics_registry.h" -#include "util/resource_manager.h" -#include "util/tls.h" - -#include "expr/type_checker.h" #include <algorithm> +#include <ext/hash_set> #include <stack> #include <utility> -#include <ext/hash_set> + +#include "base/cvc4_assert.h" +#include "base/tls.h" +#include "expr/attribute.h" +#include "expr/node_manager_attributes.h" +#include "expr/type_checker.h" +#include "options/options.h" +#include "options/smt_options.h" +#include "expr/resource_manager.h" +#include "expr/statistics_registry.h" + using namespace std; using namespace CVC4::expr; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index f52c7732f..390af8967 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -32,11 +32,11 @@ #include <string> #include <ext/hash_set> +#include "base/tls.h" #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node_value.h" #include "util/subrange_bound.h" -#include "util/tls.h" #include "options/options.h" namespace CVC4 { @@ -940,24 +940,25 @@ public: class NodeManagerScope { /** The old NodeManager, to be restored on destruction. */ NodeManager* d_oldNodeManager; - + Options::OptionsScope d_optionsScope; public: - NodeManagerScope(NodeManager* nm) : - d_oldNodeManager(NodeManager::s_current) { + NodeManagerScope(NodeManager* nm) + : d_oldNodeManager(NodeManager::s_current) + , d_optionsScope(nm ? nm->d_options : NULL) { // There are corner cases where nm can be NULL and it's ok. // For example, if you write { Expr e; }, then when the null // Expr is destructed, there's no active node manager. //Assert(nm != NULL); NodeManager::s_current = nm; - Options::s_current = nm ? nm->d_options : NULL; + //Options::s_current = nm ? nm->d_options : NULL; Debug("current") << "node manager scope: " << NodeManager::s_current << "\n"; } ~NodeManagerScope() { NodeManager::s_current = d_oldNodeManager; - Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL; + //Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL; Debug("current") << "node manager scope: " << "returning to " << NodeManager::s_current << "\n"; } diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h index 401cc6152..77fc05e3b 100644 --- a/src/expr/node_self_iterator.h +++ b/src/expr/node_self_iterator.h @@ -21,7 +21,7 @@ #include <iterator> -#include "util/cvc4_assert.h" +#include "base/cvc4_assert.h" #include "expr/node.h" namespace CVC4 { diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 6b48fd9b7..dbe7d09eb 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -17,15 +17,16 @@ ** cvc4::Node rather than by pointer; cvc4::Node maintains the ** reference count on NodeValue instances and **/ - #include "expr/node_value.h" -#include "expr/node.h" + +#include <sstream> + #include "expr/kind.h" #include "expr/metakind.h" -#include "util/language.h" +#include "expr/node.h" +#include "options/language.h" #include "options/options.h" #include "printer/printer.h" -#include <sstream> using namespace std; diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 785f8909f..c39c14604 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -26,12 +26,13 @@ #ifndef __CVC4__EXPR__NODE_VALUE_H #define __CVC4__EXPR__NODE_VALUE_H -#include "expr/kind.h" -#include "util/language.h" - #include <stdint.h> -#include <string> + #include <iterator> +#include <string> + +#include "expr/kind.h" +#include "options/language.h" namespace CVC4 { diff --git a/src/expr/options b/src/expr/options deleted file mode 100644 index b4608832f..000000000 --- a/src/expr/options +++ /dev/null @@ -1,33 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module EXPR "expr/options.h" Expression package - -option defaultExprDepth --default-expr-depth=N int :default 0 :predicate CVC4::expr::setDefaultExprDepth :predicate-include "expr/options_handlers.h" - print exprs to depth N (0 == default, -1 == no limit) -undocumented-alias --expr-depth=N = --default-expr-depth=N - -option defaultDagThresh default-dag-thresh --default-dag-thresh=N int :default 1 :predicate CVC4::expr::setDefaultDagThresh :predicate-include "expr/options_handlers.h" - dagify common subexprs appearing > N times (1 == default, 0 == don't dagify) -undocumented-alias --dag-thresh=N = --default-dag-thresh=N -undocumented-alias --dag-threshold=N = --default-dag-thresh=N - -option - --print-expr-types void :handler CVC4::expr::setPrintExprTypes :handler-include "expr/options_handlers.h" - print types with variables when printing exprs - -option earlyTypeChecking --eager-type-checking/--lazy-type-checking bool :default USE_EARLY_TYPE_CHECKING_BY_DEFAULT - type check expressions immediately on creation (debug builds only) -/type check expressions only when necessary (default) - -# --no-type-checking will override any --early-type-checking or --lazy-type-checking option -# --lazy-type-checking is linked because earlyTypeChecking should be set false too -option typeChecking /--no-type-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--lazy-type-checking - never type check expressions - -option biasedITERemoval --biased-ites bool :default false - try the new remove ite pass that is biased against term ites appearing - -endmodule - diff --git a/src/expr/options_handlers.h b/src/expr/options_handlers.h deleted file mode 100644 index e2a92ade7..000000000 --- a/src/expr/options_handlers.h +++ /dev/null @@ -1,69 +0,0 @@ -/********************* */ -/*! \file options_handlers.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Custom handlers and predicates for expression package options - ** - ** Custom handlers and predicates for expression package options. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__EXPR__OPTIONS_HANDLERS_H -#define __CVC4__EXPR__OPTIONS_HANDLERS_H - -#include "util/output.h" -#include "util/dump.h" - -namespace CVC4 { -namespace expr { - -inline void setDefaultExprDepth(std::string option, int depth, SmtEngine* smt) { - if(depth < -1) { - throw OptionException("--default-expr-depth requires a positive argument, or -1."); - } - - Debug.getStream() << Expr::setdepth(depth); - Trace.getStream() << Expr::setdepth(depth); - Notice.getStream() << Expr::setdepth(depth); - Chat.getStream() << Expr::setdepth(depth); - Message.getStream() << Expr::setdepth(depth); - Warning.getStream() << Expr::setdepth(depth); - // intentionally exclude Dump stream from this list -} - -inline void setDefaultDagThresh(std::string option, int dag, SmtEngine* smt) { - if(dag < 0) { - throw OptionException("--default-dag-thresh requires a nonnegative argument."); - } - - Debug.getStream() << Expr::dag(dag); - Trace.getStream() << Expr::dag(dag); - Notice.getStream() << Expr::dag(dag); - Chat.getStream() << Expr::dag(dag); - Message.getStream() << Expr::dag(dag); - Warning.getStream() << Expr::dag(dag); - Dump.getStream() << Expr::dag(dag); -} - -inline void setPrintExprTypes(std::string option, SmtEngine* smt) { - Debug.getStream() << Expr::printtypes(true); - Trace.getStream() << Expr::printtypes(true); - Notice.getStream() << Expr::printtypes(true); - Chat.getStream() << Expr::printtypes(true); - Message.getStream() << Expr::printtypes(true); - Warning.getStream() << Expr::printtypes(true); - // intentionally exclude Dump stream from this list -} - -}/* CVC4::expr namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__EXPR__OPTIONS_HANDLERS_H */ diff --git a/src/expr/pickle_data.cpp b/src/expr/pickle_data.cpp index 6f47f9207..e273bcece 100644 --- a/src/expr/pickle_data.cpp +++ b/src/expr/pickle_data.cpp @@ -22,6 +22,7 @@ #include <sstream> #include <string> +#include "base/cvc4_assert.h" #include "expr/pickle_data.h" #include "expr/expr.h" #include "expr/node.h" @@ -29,7 +30,6 @@ #include "expr/node_value.h" #include "expr/expr_manager_scope.h" #include "expr/variable_type_map.h" -#include "util/cvc4_assert.h" #include "expr/kind.h" #include "expr/metakind.h" diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp index 20e8859e3..d0501ca2b 100644 --- a/src/expr/pickler.cpp +++ b/src/expr/pickler.cpp @@ -20,6 +20,8 @@ #include <sstream> #include <string> +#include "base/cvc4_assert.h" +#include "base/output.h" #include "expr/pickler.h" #include "expr/pickle_data.h" #include "expr/expr.h" @@ -28,10 +30,8 @@ #include "expr/node_value.h" #include "expr/expr_manager_scope.h" #include "expr/variable_type_map.h" -#include "util/cvc4_assert.h" #include "expr/kind.h" #include "expr/metakind.h" -#include "util/output.h" namespace CVC4 { namespace expr { diff --git a/src/expr/pickler.h b/src/expr/pickler.h index 8c3da5f40..cf1754d93 100644 --- a/src/expr/pickler.h +++ b/src/expr/pickler.h @@ -23,7 +23,7 @@ #include "expr/variable_type_map.h" #include "expr/expr.h" -#include "util/exception.h" +#include "base/exception.h" #include <exception> #include <stack> diff --git a/src/expr/predicate.cpp b/src/expr/predicate.cpp new file mode 100644 index 000000000..b88951bf9 --- /dev/null +++ b/src/expr/predicate.cpp @@ -0,0 +1,56 @@ +/********************* */ +/*! \file predicate.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of predicates for predicate subtyping + ** + ** Simple class to represent predicates for predicate subtyping. + ** Instances of this class are carried as the payload of + ** the CONSTANT-metakinded SUBTYPE_TYPE types. + **/ +#include "expr/predicate.h" + +#include "base/cvc4_assert.h" +#include "expr/expr.h" + + +using namespace std; + +namespace CVC4 { + +Predicate::Predicate(Expr e, Expr w) throw(IllegalArgumentException) : d_predicate(e), d_witness(w) { + CheckArgument(! e.isNull(), e, "Predicate cannot be null"); + CheckArgument(e.getType().isPredicate(), e, "Expression given is not predicate"); + CheckArgument(FunctionType(e.getType()).getArgTypes().size() == 1, e, "Expression given is not predicate of a single argument"); +} + +Predicate::operator Expr() const { + return d_predicate; +} + +bool Predicate::operator==(const Predicate& p) const { + return d_predicate == p.d_predicate && d_witness == p.d_witness; +} + +std::ostream& +operator<<(std::ostream& out, const Predicate& p) { + out << p.d_predicate; + if(! p.d_witness.isNull()) { + out << " : " << p.d_witness; + } + return out; +} + +size_t PredicateHashFunction::operator()(const Predicate& p) const { + ExprHashFunction h; + return h(p.d_witness) * 5039 + h(p.d_predicate); +} + +}/* CVC4 namespace */ diff --git a/src/expr/predicate.h b/src/expr/predicate.h new file mode 100644 index 000000000..cc3e8b576 --- /dev/null +++ b/src/expr/predicate.h @@ -0,0 +1,64 @@ +/********************* */ +/*! \file predicate.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of predicates for predicate subtyping + ** + ** Simple class to represent predicates for predicate subtyping. + ** Instances of this class are carried as the payload of + ** the CONSTANT-metakinded SUBTYPE_TYPE types. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__PREDICATE_H +#define __CVC4__PREDICATE_H + +#include "base/exception.h" + +namespace CVC4 { + +class Predicate; + +std::ostream& operator<<(std::ostream& out, const Predicate& p) CVC4_PUBLIC; + +struct CVC4_PUBLIC PredicateHashFunction { + size_t operator()(const Predicate& p) const; +};/* class PredicateHashFunction */ + +}/* CVC4 namespace */ + +// TIM: This needs to be here due to a circular dependency. +#warning "TODO: Track down the circular dependence on expr.h." +#include "expr/expr.h" + +namespace CVC4 { + +class CVC4_PUBLIC Predicate { + + Expr d_predicate; + Expr d_witness; + +public: + + Predicate(Expr e, Expr w = Expr()) throw(IllegalArgumentException); + + operator Expr() const; + + bool operator==(const Predicate& p) const; + + friend std::ostream& CVC4::operator<<(std::ostream& out, const Predicate& p); + friend size_t PredicateHashFunction::operator()(const Predicate& p) const; + +};/* class Predicate */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__PREDICATE_H */ diff --git a/src/expr/predicate.i b/src/expr/predicate.i new file mode 100644 index 000000000..aa80a98b5 --- /dev/null +++ b/src/expr/predicate.i @@ -0,0 +1,12 @@ +%{ +#include "expr/predicate.h" +%} + +%rename(equals) CVC4::Predicate::operator==(const Predicate&) const; +%rename(toExpr) CVC4::Predicate::operator Expr() const; + +%rename(apply) CVC4::PredicateHashFunction::operator()(const Predicate&) const; + +%ignore CVC4::operator<<(std::ostream&, const Predicate&); + +%include "expr/predicate.h" diff --git a/src/expr/record.cpp b/src/expr/record.cpp new file mode 100644 index 000000000..dfcba0d46 --- /dev/null +++ b/src/expr/record.cpp @@ -0,0 +1,36 @@ +/********************* */ +/*! \file record.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A class representing a record definition + ** + ** A class representing a record definition. + **/ + +#include "expr/record.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& os, const Record& r) { + os << "[# "; + bool first = true; + for(Record::iterator i = r.begin(); i != r.end(); ++i) { + if(!first) { + os << ", "; + } + os << (*i).first << ":" << (*i).second; + first = false; + } + os << " #]"; + + return os; +} + +}/* CVC4 namespace */ diff --git a/src/expr/record.h b/src/expr/record.h new file mode 100644 index 000000000..a255649da --- /dev/null +++ b/src/expr/record.h @@ -0,0 +1,154 @@ +/********************* */ +/*! \file record.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A class representing a Record definition + ** + ** A class representing a Record definition. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__RECORD_H +#define __CVC4__RECORD_H + +#include <iostream> +#include <string> +#include <vector> +#include <utility> +#include "util/hash.h" + +namespace CVC4 { + +class CVC4_PUBLIC Record; + +// operators for record select and update + +class CVC4_PUBLIC RecordSelect { + std::string d_field; +public: + RecordSelect(const std::string& field) throw() : d_field(field) { } + std::string getField() const throw() { return d_field; } + bool operator==(const RecordSelect& t) const throw() { return d_field == t.d_field; } + bool operator!=(const RecordSelect& t) const throw() { return d_field != t.d_field; } +};/* class RecordSelect */ + +class CVC4_PUBLIC RecordUpdate { + std::string d_field; +public: + RecordUpdate(const std::string& field) throw() : d_field(field) { } + std::string getField() const throw() { return d_field; } + bool operator==(const RecordUpdate& t) const throw() { return d_field == t.d_field; } + bool operator!=(const RecordUpdate& t) const throw() { return d_field != t.d_field; } +};/* class RecordUpdate */ + +struct CVC4_PUBLIC RecordSelectHashFunction { + inline size_t operator()(const RecordSelect& t) const { + return StringHashFunction()(t.getField()); + } +};/* struct RecordSelectHashFunction */ + +struct CVC4_PUBLIC RecordUpdateHashFunction { + inline size_t operator()(const RecordUpdate& t) const { + return StringHashFunction()(t.getField()); + } +};/* struct RecordUpdateHashFunction */ + +std::ostream& operator<<(std::ostream& out, const RecordSelect& t) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) CVC4_PUBLIC; + +inline std::ostream& operator<<(std::ostream& out, const RecordSelect& t) { + return out << "[" << t.getField() << "]"; +} + +inline std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) { + return out << "[" << t.getField() << "]"; +} + +}/* CVC4 namespace */ + +#warning "TODO: Address circular dependence in Record." +#include "expr/expr.h" +#include "expr/type.h" + +namespace CVC4 { + +// now an actual record definition + +class CVC4_PUBLIC Record { + std::vector< std::pair<std::string, Type> > d_fields; + +public: + + typedef std::vector< std::pair<std::string, Type> >::const_iterator const_iterator; + typedef const_iterator iterator; + + Record(const std::vector< std::pair<std::string, Type> >& fields) : + d_fields(fields) { + } + + const_iterator find(std::string name) const { + const_iterator i; + for(i = begin(); i != end(); ++i) { + if((*i).first == name) { + break; + } + } + return i; + } + + size_t getIndex(std::string name) const { + const_iterator i = find(name); + CheckArgument(i != end(), name, "requested field `%s' does not exist in record", name.c_str()); + return i - begin(); + } + + size_t getNumFields() const { + return d_fields.size(); + } + + const_iterator begin() const { + return d_fields.begin(); + } + + const_iterator end() const { + return d_fields.end(); + } + + std::pair<std::string, Type> operator[](size_t index) const { + CheckArgument(index < d_fields.size(), index, "index out of bounds for record type"); + return d_fields[index]; + } + + bool operator==(const Record& r) const { + return d_fields == r.d_fields; + } + + bool operator!=(const Record& r) const { + return !(*this == r); + } + +};/* class Record */ + +struct CVC4_PUBLIC RecordHashFunction { + inline size_t operator()(const Record& r) const { + size_t n = 0; + for(Record::iterator i = r.begin(); i != r.end(); ++i) { + n = (n << 3) ^ TypeHashFunction()((*i).second); + } + return n; + } +};/* struct RecordHashFunction */ + +std::ostream& operator<<(std::ostream& os, const Record& r) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__RECORD_H */ diff --git a/src/expr/record.i b/src/expr/record.i new file mode 100644 index 000000000..283f01106 --- /dev/null +++ b/src/expr/record.i @@ -0,0 +1,110 @@ +%{ +#include "expr/record.h" + +#ifdef SWIGJAVA + +#include "bindings/java_iterator_adapter.h" +#include "bindings/java_stream_adapters.h" + +#endif /* SWIGJAVA */ +%} + +%rename(equals) CVC4::RecordSelect::operator==(const RecordSelect&) const; +%ignore CVC4::RecordSelect::operator!=(const RecordSelect&) const; + +%rename(equals) CVC4::RecordUpdate::operator==(const RecordUpdate&) const; +%ignore CVC4::RecordUpdate::operator!=(const RecordUpdate&) const; + +%rename(equals) CVC4::Record::operator==(const Record&) const; +%ignore CVC4::Record::operator!=(const Record&) const; +%rename(getField) CVC4::Record::operator[](size_t) const; + +%rename(apply) CVC4::RecordHashFunction::operator()(const Record&) const; +%rename(apply) CVC4::RecordSelectHashFunction::operator()(const RecordSelect&) const; +%rename(apply) CVC4::RecordUpdateHashFunction::operator()(const RecordUpdate&) const; + +%ignore CVC4::operator<<(std::ostream&, const Record&); +%ignore CVC4::operator<<(std::ostream&, const RecordSelect&); +%ignore CVC4::operator<<(std::ostream&, const RecordUpdate&); + +#ifdef SWIGJAVA + +// These Object arrays are always of two elements, the first is a String and the second a +// Type. (On the C++ side, it is a std::pair<std::string, Type>.) +%typemap(jni) std::pair<std::string, CVC4::Type> "jobjectArray"; +%typemap(jtype) std::pair<std::string, CVC4::Type> "java.lang.Object[]"; +%typemap(jstype) std::pair<std::string, CVC4::Type> "java.lang.Object[]"; +%typemap(javaout) std::pair<std::string, CVC4::Type> { return $jnicall; } +%typemap(out) std::pair<std::string, CVC4::Type> { + $result = jenv->NewObjectArray(2, jenv->FindClass("java/lang/Object"), $null); + jenv->SetObjectArrayElement($result, 0, jenv->NewStringUTF($1.first.c_str())); + jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/Type"); + jmethodID methodid = jenv->GetMethodID(clazz, "<init>", "(JZ)V"); + jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast<long>(new CVC4::Type($1.second)), true)); + }; + +// Instead of Record::begin() and end(), create an +// iterator() method on the Java side that returns a Java-style +// Iterator. +%ignore CVC4::Record::begin() const; +%ignore CVC4::Record::end() const; +%extend CVC4::Record { + CVC4::Type find(std::string name) const { + CVC4::Record::const_iterator i; + for(i = $self->begin(); i != $self->end(); ++i) { + if((*i).first == name) { + return (*i).second; + } + } + return CVC4::Type(); + } + + CVC4::JavaIteratorAdapter<CVC4::Record> iterator() { + return CVC4::JavaIteratorAdapter<CVC4::Record>(*$self); + } +} + +// Record is "iterable" on the Java side +%typemap(javainterfaces) CVC4::Record "java.lang.Iterable<Object[]>"; + +// the JavaIteratorAdapter should not be public, and implements Iterator +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Record> "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Record> "java.util.Iterator<Object[]>"; +// add some functions to the Java side (do it here because there's no way to do these in C++) +%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::Record> " + public void remove() { + throw new java.lang.UnsupportedOperationException(); + } + + public Object[] next() { + if(hasNext()) { + return getNext(); + } else { + throw new java.util.NoSuchElementException(); + } + } +" +// getNext() just allows C++ iterator access from Java-side next(), make it private +%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Record>::getNext() "private"; + +// map the types appropriately. for records, the "payload" of the iterator is an Object[]. +// These Object arrays are always of two elements, the first is a String and the second a +// Type. (On the C++ side, it is a std::pair<std::string, SExpr>.) +%typemap(jni) CVC4::Record::const_iterator::value_type = std::pair<std::string, CVC4::Type>; +%typemap(jtype) CVC4::Record::const_iterator::value_type = std::pair<std::string, CVC4::Type>; +%typemap(jstype) CVC4::Record::const_iterator::value_type = std::pair<std::string, CVC4::Type>; +%typemap(javaout) CVC4::Record::const_iterator::value_type = std::pair<std::string, CVC4::Type>; +%typemap(out) CVC4::Record::const_iterator::value_type = std::pair<std::string, CVC4::Type>; + +#endif /* SWIGJAVA */ + +%include "expr/record.h" + +#ifdef SWIGJAVA + +%include "bindings/java_iterator_adapter.h" +%include "bindings/java_stream_adapters.h" + +%template(JavaIteratorAdapter_Record) CVC4::JavaIteratorAdapter<CVC4::Record>; + +#endif /* SWIGJAVA */ diff --git a/src/expr/resource_manager.cpp b/src/expr/resource_manager.cpp new file mode 100644 index 000000000..f36200282 --- /dev/null +++ b/src/expr/resource_manager.cpp @@ -0,0 +1,291 @@ +/********************* */ +/*! \file resource_manager.cpp +** \verbatim +** Original author: Liana Hadarean +** Major contributors: none +** Minor contributors (to current version): none +** This file is part of the CVC4 project. +** Copyright (c) 2009-2014 New York University and The University of Iowa +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief Manages and updates various resource and time limits. +** +** Manages and updates various resource and time limits. +**/ +#include "expr/resource_manager.h" + +#include "base/output.h" +#include "options/smt_options.h" +#include "smt/smt_engine_scope.h" +#include "theory/rewriter.h" + +#warning "TODO: Break the dependence of the ResourceManager on the theory" +#warning "rewriter and scope. Move this file back into util/ afterwards." + +using namespace std; + +namespace CVC4 { + +void Timer::set(uint64_t millis, bool wallTime) { + d_ms = millis; + Trace("limit") << "Timer::set(" << d_ms << ")" << std::endl; + // keep track of when it was set, even if it's disabled (i.e. == 0) + d_wall_time = wallTime; + if (d_wall_time) { + // Wall time + gettimeofday(&d_wall_limit, NULL); + Trace("limit") << "Timer::set(): it's " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl; + d_wall_limit.tv_sec += millis / 1000; + d_wall_limit.tv_usec += (millis % 1000) * 1000; + if(d_wall_limit.tv_usec > 1000000) { + ++d_wall_limit.tv_sec; + d_wall_limit.tv_usec -= 1000000; + } + Trace("limit") << "Timer::set(): limit is at " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl; + } else { + // CPU time + d_cpu_start_time = ((double)clock())/(CLOCKS_PER_SEC *0.001); + d_cpu_limit = d_cpu_start_time + d_ms; + } +} + +/** Return the milliseconds elapsed since last set(). */ +uint64_t Timer::elapsedWall() const { + Assert (d_wall_time); + timeval tv; + gettimeofday(&tv, NULL); + Trace("limit") << "Timer::elapsedWallTime(): it's now " << tv.tv_sec << "," << tv.tv_usec << std::endl; + tv.tv_sec -= d_wall_limit.tv_sec - d_ms / 1000; + tv.tv_usec -= d_wall_limit.tv_usec - (d_ms % 1000) * 1000; + Trace("limit") << "Timer::elapsedWallTime(): elapsed time is " << tv.tv_sec << "," << tv.tv_usec << std::endl; + return tv.tv_sec * 1000 + tv.tv_usec / 1000; +} + +uint64_t Timer::elapsedCPU() const { + Assert (!d_wall_time); + clock_t elapsed = ((double)clock())/(CLOCKS_PER_SEC *0.001)- d_cpu_start_time; + Trace("limit") << "Timer::elapsedCPUTime(): elapsed time is " << elapsed << " ms" <<std::endl; + return elapsed; +} + +uint64_t Timer::elapsed() const { + if (d_wall_time) + return elapsedWall(); + return elapsedCPU(); +} + +bool Timer::expired() const { + if (!on()) return false; + + if (d_wall_time) { + timeval tv; + gettimeofday(&tv, NULL); + Debug("limit") << "Timer::expired(): current wall time is " << tv.tv_sec << "," << tv.tv_usec << std::endl; + Debug("limit") << "Timer::expired(): limit wall time is " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl; + if(d_wall_limit.tv_sec < tv.tv_sec || + (d_wall_limit.tv_sec == tv.tv_sec && d_wall_limit.tv_usec <= tv.tv_usec)) { + Debug("limit") << "Timer::expired(): OVER LIMIT!" << std::endl; + return true; + } + Debug("limit") << "Timer::expired(): within limit" << std::endl; + return false; + } + + // cpu time + double current = ((double)clock())/(CLOCKS_PER_SEC*0.001); + Debug("limit") << "Timer::expired(): current cpu time is " << current << std::endl; + Debug("limit") << "Timer::expired(): limit cpu time is " << d_cpu_limit << std::endl; + if (current >= d_cpu_limit) { + Debug("limit") << "Timer::expired(): OVER LIMIT!" << current << std::endl; + return true; + } + return false; +} + +const uint64_t ResourceManager::s_resourceCount = 1000; + +ResourceManager::ResourceManager() + : d_cumulativeTimer() + , d_perCallTimer() + , d_timeBudgetCumulative(0) + , d_timeBudgetPerCall(0) + , d_resourceBudgetCumulative(0) + , d_resourceBudgetPerCall(0) + , d_cumulativeTimeUsed(0) + , d_cumulativeResourceUsed(0) + , d_thisCallResourceUsed(0) + , d_thisCallTimeBudget(0) + , d_thisCallResourceBudget(0) + , d_isHardLimit() + , d_on(false) + , d_cpuTime(false) + , d_spendResourceCalls(0) +{} + + +void ResourceManager::setResourceLimit(uint64_t units, bool cumulative) { + d_on = true; + if(cumulative) { + Trace("limit") << "ResourceManager: setting cumulative resource limit to " << units << endl; + d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units); + d_thisCallResourceBudget = d_resourceBudgetCumulative; + } else { + Trace("limit") << "ResourceManager: setting per-call resource limit to " << units << endl; + d_resourceBudgetPerCall = units; + } +} + +void ResourceManager::setTimeLimit(uint64_t millis, bool cumulative) { + d_on = true; + if(cumulative) { + Trace("limit") << "ResourceManager: setting cumulative time limit to " << millis << " ms" << endl; + d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis); + d_cumulativeTimer.set(millis, !d_cpuTime); + } else { + Trace("limit") << "ResourceManager: setting per-call time limit to " << millis << " ms" << endl; + d_timeBudgetPerCall = millis; + // perCall timer will be set in beginCall + } + +} + +uint64_t ResourceManager::getResourceUsage() const { + return d_cumulativeResourceUsed; +} + +uint64_t ResourceManager::getTimeUsage() const { + if (d_timeBudgetCumulative) { + return d_cumulativeTimer.elapsed(); + } + return d_cumulativeTimeUsed; +} + +uint64_t ResourceManager::getResourceRemaining() const { + if (d_thisCallResourceBudget <= d_thisCallResourceUsed) + return 0; + return d_thisCallResourceBudget - d_thisCallResourceUsed; +} + +uint64_t ResourceManager::getTimeRemaining() const { + uint64_t time_passed = d_cumulativeTimer.elapsed(); + if (time_passed >= d_thisCallTimeBudget) + return 0; + return d_thisCallTimeBudget - time_passed; +} + +void ResourceManager::spendResource(unsigned ammount) throw (UnsafeInterruptException) { + ++d_spendResourceCalls; + d_cumulativeResourceUsed += ammount; + if (!d_on) return; + + Debug("limit") << "ResourceManager::spendResource()" << std::endl; + d_thisCallResourceUsed += ammount; + if(out()) { + Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl; + Trace("limit") << " on call " << d_spendResourceCalls << std::endl; + if (outOfTime()) { + Trace("limit") << "ResourceManager::spendResource: elapsed time" << d_cumulativeTimer.elapsed() << std::endl; + } + + if (d_isHardLimit) { + if (smt::smtEngineInScope()) { + theory::Rewriter::clearCaches(); + } + throw UnsafeInterruptException(); + } + + // interrupt it next time resources are checked + if (smt::smtEngineInScope()) { + smt::currentSmtEngine()->interrupt(); + } + } +} + +void ResourceManager::beginCall() { + + d_perCallTimer.set(d_timeBudgetPerCall, !d_cpuTime); + d_thisCallResourceUsed = 0; + if (!d_on) return; + + if (cumulativeLimitOn()) { + if (d_resourceBudgetCumulative) { + d_thisCallResourceBudget = d_resourceBudgetCumulative <= d_cumulativeResourceUsed ? 0 : + d_resourceBudgetCumulative - d_cumulativeResourceUsed; + } + + if (d_timeBudgetCumulative) { + + AlwaysAssert(d_cumulativeTimer.on()); + // timer was on since the option was set + d_cumulativeTimeUsed = d_cumulativeTimer.elapsed(); + d_thisCallTimeBudget = d_timeBudgetCumulative <= d_cumulativeTimeUsed? 0 : + d_timeBudgetCumulative - d_cumulativeTimeUsed; + d_cumulativeTimer.set(d_thisCallTimeBudget, d_cpuTime); + } + // we are out of resources so we shouldn't update the + // budget for this call to the per call budget + if (d_thisCallTimeBudget == 0 || + d_thisCallResourceUsed == 0) + return; + } + + if (perCallLimitOn()) { + // take min of what's left and per-call budget + if (d_resourceBudgetPerCall) { + d_thisCallResourceBudget = d_thisCallResourceBudget < d_resourceBudgetPerCall && d_thisCallResourceBudget != 0 ? d_thisCallResourceBudget : d_resourceBudgetPerCall; + } + + if (d_timeBudgetPerCall) { + d_thisCallTimeBudget = d_thisCallTimeBudget < d_timeBudgetPerCall && d_thisCallTimeBudget != 0 ? d_thisCallTimeBudget : d_timeBudgetPerCall; + } + } +} + +void ResourceManager::endCall() { + uint64_t usedInCall = d_perCallTimer.elapsed(); + d_perCallTimer.set(0); + d_cumulativeTimeUsed += usedInCall; +} + +bool ResourceManager::cumulativeLimitOn() const { + return d_timeBudgetCumulative || d_resourceBudgetCumulative; +} + +bool ResourceManager::perCallLimitOn() const { + return d_timeBudgetPerCall || d_resourceBudgetPerCall; +} + +bool ResourceManager::outOfResources() const { + // resource limiting not enabled + if (d_resourceBudgetPerCall == 0 && + d_resourceBudgetCumulative == 0) + return false; + + return getResourceRemaining() == 0; +} + +bool ResourceManager::outOfTime() const { + if (d_timeBudgetPerCall == 0 && + d_timeBudgetCumulative == 0) + return false; + + return d_cumulativeTimer.expired() || d_perCallTimer.expired(); +} + +void ResourceManager::useCPUTime(bool cpu) { + Trace("limit") << "ResourceManager::useCPUTime("<< cpu <<")\n"; + d_cpuTime = cpu; +} + +void ResourceManager::setHardLimit(bool value) { + Trace("limit") << "ResourceManager::setHardLimit("<< value <<")\n"; + d_isHardLimit = value; +} + +void ResourceManager::enable(bool on) { + Trace("limit") << "ResourceManager::enable("<< on <<")\n"; + d_on = on; +} + +} /* namespace CVC4 */ diff --git a/src/expr/resource_manager.h b/src/expr/resource_manager.h new file mode 100644 index 000000000..c4ad35564 --- /dev/null +++ b/src/expr/resource_manager.h @@ -0,0 +1,158 @@ +/********************* */ +/*! \file resource_manager.h +** \verbatim +** Original author: Liana Hadarean +** Major contributors: none +** Minor contributors (to current version): none +** This file is part of the CVC4 project. +** Copyright (c) 2009-2014 New York University and The University of Iowa +** See the file COPYING in the top-level source directory for licensing +** information.\endverbatim +** +** \brief Manages and updates various resource and time limits +** +** Manages and updates various resource and time limits. +**/ + +#include "cvc4_public.h" + +#ifndef __CVC4__RESOURCE_MANAGER_H +#define __CVC4__RESOURCE_MANAGER_H + +#include <cstddef> +#include <sys/time.h> + +#include "base/exception.h" +#include "util/unsafe_interrupt_exception.h" + +namespace CVC4 { + +/** + * A helper class to keep track of a time budget and signal + * the PropEngine when the budget expires. + */ +class CVC4_PUBLIC Timer { + + uint64_t d_ms; + timeval d_wall_limit; + clock_t d_cpu_start_time; + clock_t d_cpu_limit; + + bool d_wall_time; + + /** Return the milliseconds elapsed since last set() cpu time. */ + uint64_t elapsedCPU() const; + /** Return the milliseconds elapsed since last set() wall time. */ + uint64_t elapsedWall() const; + +public: + + /** Construct a Timer. */ + Timer() + : d_ms(0) + , d_cpu_start_time(0) + , d_cpu_limit(0) + , d_wall_time(true) + {} + + /** Is the timer currently active? */ + bool on() const { + return d_ms != 0; + } + + /** Set a millisecond timer (0==off). */ + void set(uint64_t millis, bool wall_time = true); + /** Return the milliseconds elapsed since last set() wall/cpu time + depending on d_wall_time*/ + uint64_t elapsed() const; + bool expired() const; + +};/* class Timer */ + + +class CVC4_PUBLIC ResourceManager { + + Timer d_cumulativeTimer; + Timer d_perCallTimer; + + /** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */ + uint64_t d_timeBudgetCumulative; + /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */ + uint64_t d_timeBudgetPerCall; + /** A user-imposed cumulative resource budget. 0 = no limit. */ + uint64_t d_resourceBudgetCumulative; + /** A user-imposed per-call resource budget. 0 = no limit. */ + uint64_t d_resourceBudgetPerCall; + + /** The number of milliseconds used. */ + uint64_t d_cumulativeTimeUsed; + /** The amount of resource used. */ + uint64_t d_cumulativeResourceUsed; + + /** The ammount of resource used during this call. */ + uint64_t d_thisCallResourceUsed; + + /** + * The ammount of resource budget for this call (min between per call + * budget and left-over cumulative budget. + */ + uint64_t d_thisCallTimeBudget; + uint64_t d_thisCallResourceBudget; + + bool d_isHardLimit; + bool d_on; + bool d_cpuTime; + uint64_t d_spendResourceCalls; + + /** Counter indicating how often to check resource manager in loops */ + static const uint64_t s_resourceCount; + +public: + + ResourceManager(); + + bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); } + bool cumulativeLimitOn() const; + bool perCallLimitOn() const; + + bool outOfResources() const; + bool outOfTime() const; + bool out() const { return d_on && (outOfResources() || outOfTime()); } + + uint64_t getResourceUsage() const; + uint64_t getTimeUsage() const; + uint64_t getResourceRemaining() const; + uint64_t getTimeRemaining() const; + + uint64_t getResourceBudgetForThisCall() { + return d_thisCallResourceBudget; + } + + void spendResource(unsigned ammount) throw(UnsafeInterruptException); + + void setHardLimit(bool value); + void setResourceLimit(uint64_t units, bool cumulative = false); + void setTimeLimit(uint64_t millis, bool cumulative = false); + void useCPUTime(bool cpu); + + void enable(bool on); + + /** + * Resets perCall limits to mark the start of a new call, + * updates budget for current call and starts the timer + */ + void beginCall(); + + /** + * Marks the end of a SmtEngine check call, stops the per + * call timer, updates cumulative time used. + */ + void endCall(); + + static uint64_t getFrequencyCount() { return s_resourceCount; } + friend class SmtEngine; +};/* class ResourceManager */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__RESOURCE_MANAGER_H */ diff --git a/src/expr/resource_manager.i b/src/expr/resource_manager.i new file mode 100644 index 000000000..77edbd8c3 --- /dev/null +++ b/src/expr/resource_manager.i @@ -0,0 +1,5 @@ +%{ +#include "expr/resource_manager.h" +%} + +%include "expr/resource_manager.h" diff --git a/src/expr/result.cpp b/src/expr/result.cpp new file mode 100644 index 000000000..95e382b98 --- /dev/null +++ b/src/expr/result.cpp @@ -0,0 +1,295 @@ +/********************* */ +/*! \file result.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Encapsulation of the result of a query. + ** + ** Encapsulation of the result of a query. + **/ +#include "expr/result.h" + +#include <algorithm> +#include <cctype> +#include <iostream> +#include <string> + +#include "base/cvc4_assert.h" +#include "expr/node.h" + +using namespace std; + +#warning "TODO: Move Node::setLanguage out of Node and into util/. Then move Result back into util/." + +namespace CVC4 { + +Result::Result(const std::string& instr, std::string inputName) : + d_sat(SAT_UNKNOWN), + d_validity(VALIDITY_UNKNOWN), + d_which(TYPE_NONE), + d_unknownExplanation(UNKNOWN_REASON), + d_inputName(inputName) { + string s = instr; + transform(s.begin(), s.end(), s.begin(), ::tolower); + if(s == "sat" || s == "satisfiable") { + d_which = TYPE_SAT; + d_sat = SAT; + } else if(s == "unsat" || s == "unsatisfiable") { + d_which = TYPE_SAT; + d_sat = UNSAT; + } else if(s == "valid") { + d_which = TYPE_VALIDITY; + d_validity = VALID; + } else if(s == "invalid") { + d_which = TYPE_VALIDITY; + d_validity = INVALID; + } else if(s == "incomplete") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = INCOMPLETE; + } else if(s == "timeout") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = TIMEOUT; + } else if(s == "resourceout") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = RESOURCEOUT; + } else if(s == "memout") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = MEMOUT; + } else if(s == "interrupted") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = INTERRUPTED; + } else if(s.size() >= 7 && s.compare(0, 7, "unknown") == 0) { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + } else { + IllegalArgument(s, "expected satisfiability/validity result, " + "instead got `%s'", s.c_str()); + } +} + +bool Result::operator==(const Result& r) const throw() { + if(d_which != r.d_which) { + return false; + } + if(d_which == TYPE_SAT) { + return d_sat == r.d_sat && + ( d_sat != SAT_UNKNOWN || + d_unknownExplanation == r.d_unknownExplanation ); + } + if(d_which == TYPE_VALIDITY) { + return d_validity == r.d_validity && + ( d_validity != VALIDITY_UNKNOWN || + d_unknownExplanation == r.d_unknownExplanation ); + } + return false; +} + +bool operator==(enum Result::Sat sr, const Result& r) throw() { + return r == sr; +} + +bool operator==(enum Result::Validity vr, const Result& r) throw() { + return r == vr; +} +bool operator!=(enum Result::Sat s, const Result& r) throw(){ + return !(s == r); +} +bool operator!=(enum Result::Validity v, const Result& r) throw(){ + return !(v == r); +} + +Result Result::asSatisfiabilityResult() const throw() { + if(d_which == TYPE_SAT) { + return *this; + } + + if(d_which == TYPE_VALIDITY) { + switch(d_validity) { + + case INVALID: + return Result(SAT, d_inputName); + + case VALID: + return Result(UNSAT, d_inputName); + + case VALIDITY_UNKNOWN: + return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName); + + default: + Unhandled(d_validity); + } + } + + // TYPE_NONE + return Result(SAT_UNKNOWN, NO_STATUS, d_inputName); +} + +Result Result::asValidityResult() const throw() { + if(d_which == TYPE_VALIDITY) { + return *this; + } + + if(d_which == TYPE_SAT) { + switch(d_sat) { + + case SAT: + return Result(INVALID, d_inputName); + + case UNSAT: + return Result(VALID, d_inputName); + + case SAT_UNKNOWN: + return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName); + + default: + Unhandled(d_sat); + } + } + + // TYPE_NONE + return Result(VALIDITY_UNKNOWN, NO_STATUS, d_inputName); +} + +string Result::toString() const { + stringstream ss; + ss << *this; + return ss.str(); +} + +ostream& operator<<(ostream& out, enum Result::Sat s) { + switch(s) { + case Result::UNSAT: out << "UNSAT"; break; + case Result::SAT: out << "SAT"; break; + case Result::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break; + default: Unhandled(s); + } + return out; +} + +ostream& operator<<(ostream& out, enum Result::Validity v) { + switch(v) { + case Result::INVALID: out << "INVALID"; break; + case Result::VALID: out << "VALID"; break; + case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break; + default: Unhandled(v); + } + return out; +} + +ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) { + switch(e) { + case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break; + case Result::INCOMPLETE: out << "INCOMPLETE"; break; + case Result::TIMEOUT: out << "TIMEOUT"; break; + case Result::RESOURCEOUT: out << "RESOURCEOUT"; break; + case Result::MEMOUT: out << "MEMOUT"; break; + case Result::INTERRUPTED: out << "INTERRUPTED"; break; + case Result::NO_STATUS: out << "NO_STATUS"; break; + case Result::UNSUPPORTED: out << "UNSUPPORTED"; break; + case Result::OTHER: out << "OTHER"; break; + case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break; + default: Unhandled(e); + } + return out; +} + +ostream& operator<<(ostream& out, const Result& r) { + r.toStream(out, Node::setlanguage::getLanguage(out)); + return out; +}/* operator<<(ostream&, const Result&) */ + + +void Result::toStreamDefault(std::ostream& out) const throw() { + if(getType() == Result::TYPE_SAT) { + switch(isSat()) { + case Result::UNSAT: + out << "unsat"; + break; + case Result::SAT: + out << "sat"; + break; + case Result::SAT_UNKNOWN: + out << "unknown"; + if(whyUnknown() != Result::UNKNOWN_REASON) { + out << " (" << whyUnknown() << ")"; + } + break; + } + } else { + switch(isValid()) { + case Result::INVALID: + out << "invalid"; + break; + case Result::VALID: + out << "valid"; + break; + case Result::VALIDITY_UNKNOWN: + out << "unknown"; + if(whyUnknown() != Result::UNKNOWN_REASON) { + out << " (" << whyUnknown() << ")"; + } + break; + } + } +}/* Result::toStreamDefault() */ + + +void Result::toStreamSmt2(ostream& out) const throw(){ + if(getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN) { + out << "unknown"; + } else { + toStreamDefault(out); + } +} + +void Result::toStreamTptp(std::ostream& out) const throw() { + out << "% SZS status "; + if(isSat() == Result::SAT) { + out << "Satisfiable"; + } else if(isSat() == Result::UNSAT) { + out << "Unsatisfiable"; + } else if(isValid() == Result::VALID) { + out << "Theorem"; + } else if(isValid() == Result::INVALID) { + out << "CounterSatisfiable"; + } else { + out << "GaveUp"; + } + out << " for " << getInputName(); +} + +void Result::toStream(std::ostream& out, OutputLanguage language) const throw() { + switch(language) { + case language::output::LANG_SMTLIB_V2_0: + case language::output::LANG_SMTLIB_V2_5: + case language::output::LANG_SYGUS: + case language::output::LANG_Z3STR: + toStreamSmt2(out); + break; + case language::output::LANG_TPTP: + toStreamTptp(out); + break; + case language::output::LANG_AST: + case language::output::LANG_AUTO: + case language::output::LANG_CVC3: + case language::output::LANG_CVC4: + case language::output::LANG_MAX: + case language::output::LANG_SMTLIB_V1: + default: + toStreamDefault(out); + break; + }; +} + +}/* CVC4 namespace */ diff --git a/src/expr/result.h b/src/expr/result.h new file mode 100644 index 000000000..74697eba6 --- /dev/null +++ b/src/expr/result.h @@ -0,0 +1,206 @@ +/********************* */ +/*! \file result.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Encapsulation of the result of a query. + ** + ** Encapsulation of the result of a query. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__RESULT_H +#define __CVC4__RESULT_H + +#include <iostream> +#include <string> + +#include "base/exception.h" +#include "options/language.h" + +namespace CVC4 { + +class Result; + +std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC; + +/** + * Three-valued SMT result, with optional explanation. + */ +class CVC4_PUBLIC Result { +public: + enum Sat { + UNSAT = 0, + SAT = 1, + SAT_UNKNOWN = 2 + }; + + enum Validity { + INVALID = 0, + VALID = 1, + VALIDITY_UNKNOWN = 2 + }; + + enum Type { + TYPE_SAT, + TYPE_VALIDITY, + TYPE_NONE + }; + + enum UnknownExplanation { + REQUIRES_FULL_CHECK, + INCOMPLETE, + TIMEOUT, + RESOURCEOUT, + MEMOUT, + INTERRUPTED, + NO_STATUS, + UNSUPPORTED, + OTHER, + UNKNOWN_REASON + }; + +private: + enum Sat d_sat; + enum Validity d_validity; + enum Type d_which; + enum UnknownExplanation d_unknownExplanation; + std::string d_inputName; + +public: + Result() : + d_sat(SAT_UNKNOWN), + d_validity(VALIDITY_UNKNOWN), + d_which(TYPE_NONE), + d_unknownExplanation(UNKNOWN_REASON), + d_inputName("") { + } + Result(enum Sat s, std::string inputName = "") : + d_sat(s), + d_validity(VALIDITY_UNKNOWN), + d_which(TYPE_SAT), + d_unknownExplanation(UNKNOWN_REASON), + d_inputName(inputName) { + CheckArgument(s != SAT_UNKNOWN, + "Must provide a reason for satisfiability being unknown"); + } + Result(enum Validity v, std::string inputName = "") : + d_sat(SAT_UNKNOWN), + d_validity(v), + d_which(TYPE_VALIDITY), + d_unknownExplanation(UNKNOWN_REASON), + d_inputName(inputName) { + CheckArgument(v != VALIDITY_UNKNOWN, + "Must provide a reason for validity being unknown"); + } + Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName = "") : + d_sat(s), + d_validity(VALIDITY_UNKNOWN), + d_which(TYPE_SAT), + d_unknownExplanation(unknownExplanation), + d_inputName(inputName) { + CheckArgument(s == SAT_UNKNOWN, + "improper use of unknown-result constructor"); + } + Result(enum Validity v, enum UnknownExplanation unknownExplanation, std::string inputName = "") : + d_sat(SAT_UNKNOWN), + d_validity(v), + d_which(TYPE_VALIDITY), + d_unknownExplanation(unknownExplanation), + d_inputName(inputName) { + CheckArgument(v == VALIDITY_UNKNOWN, + "improper use of unknown-result constructor"); + } + Result(const std::string& s, std::string inputName = ""); + + Result(const Result& r, std::string inputName) { + *this = r; + d_inputName = inputName; + } + + enum Sat isSat() const { + return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; + } + enum Validity isValid() const { + return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN; + } + bool isUnknown() const { + return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN; + } + Type getType() const { + return d_which; + } + bool isNull() const { + return d_which == TYPE_NONE; + } + enum UnknownExplanation whyUnknown() const { + CheckArgument( isUnknown(), this, + "This result is not unknown, so the reason for " + "being unknown cannot be inquired of it" ); + return d_unknownExplanation; + } + + bool operator==(const Result& r) const throw(); + inline bool operator!=(const Result& r) const throw(); + Result asSatisfiabilityResult() const throw(); + Result asValidityResult() const throw(); + + std::string toString() const; + + std::string getInputName() const { return d_inputName; } + + /** + * Write a Result out to a stream in this language. + */ + void toStream(std::ostream& out, OutputLanguage language) const throw(); + + /** + * This is mostly the same the default + * If getType() == Result::TYPE_SAT && isSat() == Result::SAT_UNKNOWN, + * + */ + void toStreamSmt2(std::ostream& out) const throw(); + + /** + * Write a Result out to a stream in the Tptp format + */ + void toStreamTptp(std::ostream& out) const throw(); + + /** + * Write a Result out to a stream. + * + * The default implementation writes a reasonable string in lowercase + * for sat, unsat, valid, invalid, or unknown results. This behavior + * is overridable by each Printer, since sometimes an output language + * has a particular preference for how results should appear. + */ + void toStreamDefault(std::ostream& out) const throw(); +};/* class Result */ + +inline bool Result::operator!=(const Result& r) const throw() { + return !(*this == r); +} + +std::ostream& operator<<(std::ostream& out, + enum Result::Sat s) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, + enum Result::Validity v) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, + enum Result::UnknownExplanation e) CVC4_PUBLIC; + +bool operator==(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC; +bool operator==(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC; + +bool operator!=(enum Result::Sat s, const Result& r) throw() CVC4_PUBLIC; +bool operator!=(enum Result::Validity v, const Result& r) throw() CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__RESULT_H */ diff --git a/src/expr/result.i b/src/expr/result.i new file mode 100644 index 000000000..becbe9aa9 --- /dev/null +++ b/src/expr/result.i @@ -0,0 +1,20 @@ +%{ +#include "expr/result.h" +%} + +%ignore CVC4::operator<<(std::ostream&, const Result& r); + +%rename(equals) CVC4::Result::operator==(const Result& r) const; +%ignore CVC4::Result::operator!=(const Result& r) const; + +%ignore CVC4::operator<<(std::ostream&, enum Result::Sat); +%ignore CVC4::operator<<(std::ostream&, enum Result::Validity); +%ignore CVC4::operator<<(std::ostream&, enum Result::UnknownExplanation); + +%ignore CVC4::operator==(enum Result::Sat, const Result&); +%ignore CVC4::operator!=(enum Result::Sat, const Result&); + +%ignore CVC4::operator==(enum Result::Validity, const Result&); +%ignore CVC4::operator!=(enum Result::Validity, const Result&); + +%include "expr/result.h" diff --git a/src/expr/sexpr.cpp b/src/expr/sexpr.cpp new file mode 100644 index 000000000..a321f85aa --- /dev/null +++ b/src/expr/sexpr.cpp @@ -0,0 +1,233 @@ +/********************* */ +/*! \file sexpr.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Simple representation of S-expressions + ** + ** Simple representation of S-expressions. + ** + ** SExprs have their own language specific printing procedures. The reason for + ** this being implemented on SExpr and not on the Printer class is that the + ** Printer class lives in libcvc4. It has to currently as it prints fairly + ** complicated objects, like Model, which in turn uses SmtEngine pointers. + ** However, SExprs need to be printed by Statistics. To get the output consistent + ** with the previous version, the printing of SExprs in different languages is + ** handled in the SExpr class and the libexpr library. + **/ + +#include "expr/sexpr.h" + +#include <iostream> +#include <sstream> +#include <vector> + +#include "base/cvc4_assert.h" +#include "expr/expr.h" +#include "util/smt2_quote_string.h" + + +namespace CVC4 { + +const int PrettySExprs::s_iosIndex = std::ios_base::xalloc(); + +std::ostream& operator<<(std::ostream& out, PrettySExprs ps) { + ps.applyPrettySExprs(out); + return out; +} + +std::string SExpr::toString() const { + std::stringstream ss; + ss << (*this); + return ss.str(); +} + +std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) { + SExpr::toStream(out, sexpr); + return out; +} + +void SExpr::toStream(std::ostream& out, const SExpr& sexpr) throw() { + toStream(out, sexpr, Expr::setlanguage::getLanguage(out)); +} + +void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw() { + toStream(out, sexpr, language, PrettySExprs::getPrettySExprs(out) ? 2 : 0); +} + +void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw() { + if( sexpr.isKeyword() && languageQuotesKeywords(language) ){ + out << quoteSymbol(sexpr.getValue()); + } else { + toStreamRec(out, sexpr, language, indent); + } +} + + +void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw() { + if(sexpr.isInteger()) { + out << sexpr.getIntegerValue(); + } else if(sexpr.isRational()) { + out << std::fixed << sexpr.getRationalValue().getDouble(); + } else if(sexpr.isKeyword()) { + out << sexpr.getValue(); + } else if(sexpr.isString()) { + std::string s = sexpr.getValue(); + // escape backslash and quote + for(size_t i = 0; i < s.length(); ++i) { + if(s[i] == '"') { + s.replace(i, 1, "\\\""); + ++i; + } else if(s[i] == '\\') { + s.replace(i, 1, "\\\\"); + ++i; + } + } + out << "\"" << s << "\""; + } else { + const std::vector<SExpr>& kids = sexpr.getChildren(); + out << (indent > 0 && kids.size() > 1 ? "( " : "("); + bool first = true; + for(std::vector<SExpr>::const_iterator i = kids.begin(); i != kids.end(); ++i) { + if(first) { + first = false; + } else { + if(indent > 0) { + out << "\n" << std::string(indent, ' '); + } else { + out << ' '; + } + } + toStreamRec(out, *i, language, indent <= 0 || indent > 2 ? 0 : indent + 2); + } + if(indent > 0 && kids.size() > 1) { + out << '\n'; + if(indent > 2) { + out << std::string(indent - 2, ' '); + } + } + out << ')'; + } +}/* toStreamRec() */ + + +bool SExpr::languageQuotesKeywords(OutputLanguage language) { + switch(language) { + case language::output::LANG_SMTLIB_V1: + case language::output::LANG_SMTLIB_V2_0: + case language::output::LANG_SMTLIB_V2_5: + case language::output::LANG_SYGUS: + case language::output::LANG_TPTP: + case language::output::LANG_Z3STR: + return true; + case language::output::LANG_AST: + case language::output::LANG_CVC3: + case language::output::LANG_CVC4: + default: + return false; + }; +} + + + +std::string SExpr::getValue() const { + CheckArgument( isAtom(), this ); + switch(d_sexprType) { + case SEXPR_INTEGER: + return d_integerValue.toString(); + case SEXPR_RATIONAL: { + // We choose to represent rationals as decimal strings rather than + // "numerator/denominator." Perhaps an additional SEXPR_DECIMAL + // could be added if we need both styles, even if it's backed by + // the same Rational object. + std::stringstream ss; + ss << std::fixed << d_rationalValue.getDouble(); + return ss.str(); + } + case SEXPR_STRING: + case SEXPR_KEYWORD: + return d_stringValue; + case SEXPR_NOT_ATOM: + return std::string(); + } + return std::string(); + +} + +const CVC4::Integer& SExpr::getIntegerValue() const { + CheckArgument( isInteger(), this ); + return d_integerValue; +} + +const CVC4::Rational& SExpr::getRationalValue() const { + CheckArgument( isRational(), this ); + return d_rationalValue; +} + +const std::vector<SExpr>& SExpr::getChildren() const { + CheckArgument( !isAtom(), this ); + return d_children; +} + +bool SExpr::operator==(const SExpr& s) const { + return d_sexprType == s.d_sexprType && + d_integerValue == s.d_integerValue && + d_rationalValue == s.d_rationalValue && + d_stringValue == s.d_stringValue && + d_children == s.d_children; +} + +bool SExpr::operator!=(const SExpr& s) const { + return !(*this == s); +} + + +SExpr SExpr::parseAtom(const std::string& atom) { + if(atom == "true"){ + return SExpr(true); + } else if(atom == "false"){ + return SExpr(false); + } else { + try { + Integer z(atom); + return SExpr(z); + }catch(std::invalid_argument&){ + // Fall through to the next case + } + try { + Rational q(atom); + return SExpr(q); + }catch(std::invalid_argument&){ + // Fall through to the next case + } + return SExpr(atom); + } +} + +SExpr SExpr::parseListOfAtoms(const std::vector<std::string>& atoms) { + std::vector<SExpr> parsedAtoms; + typedef std::vector<std::string>::const_iterator const_iterator; + for(const_iterator i = atoms.begin(), i_end=atoms.end(); i != i_end; ++i){ + parsedAtoms.push_back(parseAtom(*i)); + } + return SExpr(parsedAtoms); +} + +SExpr SExpr::parseListOfListOfAtoms(const std::vector< std::vector<std::string> >& atoms_lists) { + std::vector<SExpr> parsedListsOfAtoms; + typedef std::vector< std::vector<std::string> >::const_iterator const_iterator; + for(const_iterator i = atoms_lists.begin(), i_end = atoms_lists.end(); i != i_end; ++i){ + parsedListsOfAtoms.push_back(parseListOfAtoms(*i)); + } + return SExpr(parsedListsOfAtoms); +} + + + +}/* CVC4 namespace */ diff --git a/src/expr/sexpr.h b/src/expr/sexpr.h new file mode 100644 index 000000000..f30045c68 --- /dev/null +++ b/src/expr/sexpr.h @@ -0,0 +1,383 @@ +/********************* */ +/*! \file sexpr.h + ** \verbatim + ** Original author: Christopher L. Conway + ** Major contributors: Tim King, Morgan Deters + ** Minor contributors (to current version): Dejan Jovanovic + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Simple representation of S-expressions + ** + ** Simple representation of S-expressions. + ** These are used when a simple, and obvious interface for basic + ** expressions is appropraite. + ** + ** These are quite ineffecient. + ** These are totally disconnected from any ExprManager. + ** These keep unique copies of all of their children. + ** These are VERY overly verbose and keep much more data than is needed. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__SEXPR_H +#define __CVC4__SEXPR_H + +#include <iomanip> +#include <sstream> +#include <string> +#include <vector> + +#include "base/exception.h" +#include "options/language.h" +#include "util/integer.h" +#include "util/rational.h" + +namespace CVC4 { + +class CVC4_PUBLIC SExprKeyword { + std::string d_str; +public: + SExprKeyword(const std::string& s) : d_str(s) {} + const std::string& getString() const { return d_str; } +};/* class SExpr::Keyword */ + +/** + * A simple S-expression. An S-expression is either an atom with a + * string value, or a list of other S-expressions. + */ +class CVC4_PUBLIC SExpr { + + enum SExprTypes { + SEXPR_STRING, + SEXPR_KEYWORD, + SEXPR_INTEGER, + SEXPR_RATIONAL, + SEXPR_NOT_ATOM + } d_sexprType; + + /** The value of an atomic integer-valued S-expression. */ + CVC4::Integer d_integerValue; + + /** The value of an atomic rational-valued S-expression. */ + CVC4::Rational d_rationalValue; + + /** The value of an atomic S-expression. */ + std::string d_stringValue; + + /** The children of a list S-expression. */ + std::vector<SExpr> d_children; + +public: + + typedef SExprKeyword Keyword; + + SExpr() : + d_sexprType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(""), + d_children() { + } + + SExpr(const CVC4::Integer& value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children() { + } + + SExpr(int value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children() { + } + + SExpr(long int value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children() { + } + + SExpr(unsigned int value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children() { + } + + SExpr(unsigned long int value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children() { + } + + SExpr(const CVC4::Rational& value) : + d_sexprType(SEXPR_RATIONAL), + d_integerValue(0), + d_rationalValue(value), + d_stringValue(""), + d_children() { + } + + SExpr(const std::string& value) : + d_sexprType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value), + d_children() { + } + + /** + * This constructs a string expression from a const char* value. + * This cannot be removed in order to support SExpr("foo"). + * Given the other constructors this SExpr("foo") converts to bool. + * instead of SExpr(string("foo")). + */ + SExpr(const char* value) : + d_sexprType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value), + d_children() { + } + + /** + * This adds a convenience wrapper to SExpr to cast from bools. + * This is internally handled as the strings "true" and "false" + */ + SExpr(bool value) : +#warning "TODO: Discuss this change with Clark." + d_sexprType(SEXPR_KEYWORD), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value ? "true" : "false"), + d_children() { + } + + SExpr(const Keyword& value) : + d_sexprType(SEXPR_KEYWORD), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value.getString()), + d_children() { + } + + SExpr(const std::vector<SExpr>& children) : + d_sexprType(SEXPR_NOT_ATOM), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(""), + d_children(children) { + } + + /** Is this S-expression an atom? */ + bool isAtom() const { + return d_sexprType != SEXPR_NOT_ATOM; + } + + /** Is this S-expression an integer? */ + bool isInteger() const { + return d_sexprType == SEXPR_INTEGER; + } + + /** Is this S-expression a rational? */ + bool isRational() const { + return d_sexprType == SEXPR_RATIONAL; + } + + /** Is this S-expression a string? */ + bool isString() const { + return d_sexprType == SEXPR_STRING; + } + + /** Is this S-expression a keyword? */ + bool isKeyword() const { + return d_sexprType == SEXPR_KEYWORD; + } + + /** + * This wraps the toStream() printer. + * NOTE: toString() and getValue() may differ on Keywords based on + * the current language set in expr. + */ + std::string toString() const; + + /** + * Get the string value of this S-expression. This will cause an + * error if this S-expression is not an atom. + */ + std::string getValue() const; + + /** + * Get the integer value of this S-expression. This will cause an + * error if this S-expression is not an integer. + */ + const CVC4::Integer& getIntegerValue() const; + + /** + * Get the rational value of this S-expression. This will cause an + * error if this S-expression is not a rational. + */ + const CVC4::Rational& getRationalValue() const; + + /** + * Get the children of this S-expression. This will cause an error + * if this S-expression is not a list. + */ + const std::vector<SExpr>& getChildren() const; + + /** Is this S-expression equal to another? */ + bool operator==(const SExpr& s) const; + + /** Is this S-expression different from another? */ + bool operator!=(const SExpr& s) const; + + + /** + * This returns the best match in the following order: + * match atom with + * "true", "false" -> SExpr(value) + * | is and integer -> as integer + * | is a rational -> as rational + * | _ -> SExpr() + */ + static SExpr parseAtom(const std::string& atom); + + /** + * Parses a list of atoms. + */ + static SExpr parseListOfAtoms(const std::vector<std::string>& atoms); + + /** + * Parses a list of list of atoms. + */ + static SExpr parseListOfListOfAtoms(const std::vector< std::vector<std::string> >& atoms_lists); + + + /** + * Outputs the SExpr onto the ostream out. This version reads defaults to the + * OutputLanguage, Expr::setlanguage::getLanguage(out). The indent level is + * set to 2 if PrettySExprs::getPrettySExprs() is on and is 0 otherwise. + */ + static void toStream(std::ostream& out, const SExpr& sexpr) throw(); + + /** + * Outputs the SExpr onto the ostream out. This version sets the indent level + * to 2 if PrettySExprs::getPrettySExprs() is on. + */ + static void toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw(); + + /** + * Outputs the SExpr onto the ostream out. + * If the languageQuotesKeywords(language), then a top level keyword, " X", + * that needs quoting according to the SMT2 language standard is printed with + * quotes, "| X|". + * Otherwise this prints using toStreamRec(). + * + * TIM: Keywords that are children are not currently quoted. This seems + * incorrect but I am just reproduicing the old behavior even if it does not make + * sense. + */ + static void toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw(); + +private: + + /** + * Simple printer for SExpr to an ostream. + * The current implementation is language independent. + */ + static void toStreamRec(std::ostream& out, const SExpr& sexpr, OutputLanguage language, int indent) throw(); + + + /** Returns true if this language quotes Keywords when printing. */ + static bool languageQuotesKeywords(OutputLanguage language); + +};/* class SExpr */ + +/** Prints an SExpr. */ +std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_PUBLIC; + +/** + * IOStream manipulator to pretty-print SExprs. + */ +class CVC4_PUBLIC PrettySExprs { + /** + * The allocated index in ios_base for our setting. + */ + static const int s_iosIndex; + + /** + * When this manipulator is used, the setting is stored here. + */ + bool d_prettySExprs; + +public: + /** + * Construct a PrettySExprs with the given setting. + */ + PrettySExprs(bool prettySExprs) : d_prettySExprs(prettySExprs) {} + + inline void applyPrettySExprs(std::ostream& out) { + out.iword(s_iosIndex) = d_prettySExprs; + } + + static inline bool getPrettySExprs(std::ostream& out) { + return out.iword(s_iosIndex); + } + + static inline void setPrettySExprs(std::ostream& out, bool prettySExprs) { + out.iword(s_iosIndex) = prettySExprs; + } + + /** + * Set the pretty-sexprs state on the output stream for the current + * stack scope. This makes sure the old state is reset on the + * stream after normal OR exceptional exit from the scope, using the + * RAII C++ idiom. + */ + class Scope { + std::ostream& d_out; + bool d_oldPrettySExprs; + + public: + + inline Scope(std::ostream& out, bool prettySExprs) : + d_out(out), + d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) { + PrettySExprs::setPrettySExprs(out, prettySExprs); + } + + inline ~Scope() { + PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs); + } + + };/* class PrettySExprs::Scope */ + +};/* class PrettySExprs */ + +/** + * Sets the default pretty-sexprs setting for an ostream. Use like this: + * + * // let out be an ostream, s an SExpr + * out << PrettySExprs(true) << s << endl; + * + * The setting stays permanently (until set again) with the stream. + */ +std::ostream& operator<<(std::ostream& out, PrettySExprs ps); + + +}/* CVC4 namespace */ + +#endif /* __CVC4__SEXPR_H */ diff --git a/src/expr/sexpr.i b/src/expr/sexpr.i new file mode 100644 index 000000000..f6229782e --- /dev/null +++ b/src/expr/sexpr.i @@ -0,0 +1,21 @@ +%{ +#include "expr/sexpr.h" +%} + +%ignore CVC4::operator<<(std::ostream&, const SExpr&); +%ignore CVC4::operator<<(std::ostream&, SExpr::SexprTypes); + +// for Java and the like +%extend CVC4::SExpr { + std::string toString() const { return self->getValue(); } +};/* CVC4::SExpr */ + +%ignore CVC4::SExpr::SExpr(int); +%ignore CVC4::SExpr::SExpr(unsigned int); +%ignore CVC4::SExpr::SExpr(unsigned long); +%ignore CVC4::SExpr::SExpr(const char*); + +%rename(equals) CVC4::SExpr::operator==(const SExpr&) const; +%ignore CVC4::SExpr::operator!=(const SExpr&) const; + +%include "expr/sexpr.h" diff --git a/src/expr/statistics.cpp b/src/expr/statistics.cpp new file mode 100644 index 000000000..e5d3f6e69 --- /dev/null +++ b/src/expr/statistics.cpp @@ -0,0 +1,133 @@ +/********************* */ +/*! \file statistics.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include <typeinfo> + +#include "expr/statistics.h" +#include "expr/statistics_registry.h" // for details about class Stat + + +namespace CVC4 { + +std::string StatisticsBase::s_regDelim("::"); + +bool StatisticsBase::StatCmp::operator()(const Stat* s1, const Stat* s2) const { + return s1->getName() < s2->getName(); +} + +StatisticsBase::iterator::value_type StatisticsBase::iterator::operator*() const { + return std::make_pair((*d_it)->getName(), (*d_it)->getValue()); +} + +StatisticsBase::StatisticsBase() : + d_prefix(), + d_stats() { +} + +StatisticsBase::StatisticsBase(const StatisticsBase& stats) : + d_prefix(stats.d_prefix), + d_stats() { +} + +StatisticsBase& StatisticsBase::operator=(const StatisticsBase& stats) { + d_prefix = stats.d_prefix; + return *this; +} + +void Statistics::copyFrom(const StatisticsBase& stats) { + // This is ugly, but otherwise we have to introduce a "friend" relation for + // Base to its derived class (really obnoxious). + StatSet::const_iterator i_begin = ((const Statistics*) &stats)->d_stats.begin(); + StatSet::const_iterator i_end = ((const Statistics*) &stats)->d_stats.end(); + for(StatSet::const_iterator i = i_begin; i != i_end; ++i) { + SExprStat* p = new SExprStat((*i)->getName(), (*i)->getValue()); + d_stats.insert(p); + } +} + +void Statistics::clear() { + for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) { + delete *i; + } + d_stats.clear(); +} + +Statistics::Statistics(const StatisticsBase& stats) : + StatisticsBase(stats) { + copyFrom(stats); +} + +Statistics::Statistics(const Statistics& stats) : + StatisticsBase(stats) { + copyFrom(stats); +} + +Statistics::~Statistics() { + clear(); +} + +Statistics& Statistics::operator=(const StatisticsBase& stats) { + clear(); + this->StatisticsBase::operator=(stats); + copyFrom(stats); + + return *this; +} + +Statistics& Statistics::operator=(const Statistics& stats) { + return this->operator=((const StatisticsBase&)stats); +} + +StatisticsBase::const_iterator StatisticsBase::begin() const { + return iterator(d_stats.begin()); +} + +StatisticsBase::const_iterator StatisticsBase::end() const { + return iterator(d_stats.end()); +} + +void StatisticsBase::flushInformation(std::ostream &out) const { +#ifdef CVC4_STATISTICS_ON + for(StatSet::iterator i = d_stats.begin(); + i != d_stats.end(); + ++i) { + Stat* s = *i; + if(d_prefix != "") { + out << d_prefix << s_regDelim; + } + s->flushStat(out); + out << std::endl; + } +#endif /* CVC4_STATISTICS_ON */ +} + +SExpr StatisticsBase::getStatistic(std::string name) const { + SExpr value; + IntStat s(name, 0); + StatSet::iterator i = d_stats.find(&s); + if(i != d_stats.end()) { + return (*i)->getValue(); + } else { + return SExpr(); + } +} + +void StatisticsBase::setPrefix(const std::string& prefix) { + d_prefix = prefix; +} + +}/* CVC4 namespace */ diff --git a/src/expr/statistics.h b/src/expr/statistics.h new file mode 100644 index 000000000..425404692 --- /dev/null +++ b/src/expr/statistics.h @@ -0,0 +1,129 @@ +/********************* */ +/*! \file statistics.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__STATISTICS_H +#define __CVC4__STATISTICS_H + +#include "expr/sexpr.h" + +#include <iterator> +#include <ostream> +#include <set> +#include <string> +#include <utility> + +namespace CVC4 { + +class Stat; + +class CVC4_PUBLIC StatisticsBase { +protected: + + static std::string s_regDelim; + + /** A helper class for comparing two statistics */ + struct StatCmp { + bool operator()(const Stat* s1, const Stat* s2) const; + };/* struct StatisticsRegistry::StatCmp */ + + /** A type for a set of statistics */ + typedef std::set< Stat*, StatCmp > StatSet; + + std::string d_prefix; + + /** The set of statistics in this object */ + StatSet d_stats; + + StatisticsBase(); + StatisticsBase(const StatisticsBase& stats); + StatisticsBase& operator=(const StatisticsBase& stats); + +public: + + virtual ~StatisticsBase() { } + + class CVC4_PUBLIC iterator : public std::iterator< std::input_iterator_tag, std::pair<std::string, SExpr> > { + StatSet::iterator d_it; + + iterator(StatSet::iterator it) : d_it(it) { } + + friend class StatisticsBase; + + public: + iterator() : d_it() { } + iterator(const iterator& it) : d_it(it.d_it) { } + value_type operator*() const; + iterator& operator++() { ++d_it; return *this; } + iterator operator++(int) { iterator old = *this; ++d_it; return old; } + bool operator==(const iterator& i) const { return d_it == i.d_it; } + bool operator!=(const iterator& i) const { return d_it != i.d_it; } + };/* class StatisticsBase::iterator */ + + /** An iterator type over a set of statistics. */ + typedef iterator const_iterator; + + /** Set the output prefix for this set of statistics. */ + virtual void setPrefix(const std::string& prefix); + + /** Flush all statistics to the given output stream. */ + void flushInformation(std::ostream& out) const; + + /** Get the value of a named statistic. */ + SExpr getStatistic(std::string name) const; + + /** + * Get an iterator to the beginning of the range of the set of + * statistics. + */ + const_iterator begin() const; + + /** + * Get an iterator to the end of the range of the set of statistics. + */ + const_iterator end() const; + +};/* class StatisticsBase */ + +class CVC4_PUBLIC Statistics : public StatisticsBase { + void clear(); + void copyFrom(const StatisticsBase&); + +public: + + /** + * Override the copy constructor to do a "deep" copy of statistics + * values. + */ + Statistics(const StatisticsBase& stats); + Statistics(const Statistics& stats); + + ~Statistics(); + + /** + * Override the assignment operator to do a "deep" copy of statistics + * values. + */ + Statistics& operator=(const StatisticsBase& stats); + Statistics& operator=(const Statistics& stats); + +};/* class Statistics */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__STATISTICS_H */ diff --git a/src/expr/statistics.i b/src/expr/statistics.i new file mode 100644 index 000000000..990f465f5 --- /dev/null +++ b/src/expr/statistics.i @@ -0,0 +1,79 @@ +%{ +#include "expr/statistics.h" + +#ifdef SWIGJAVA + +#include "bindings/java_iterator_adapter.h" +#include "bindings/java_stream_adapters.h" + +#endif /* SWIGJAVA */ +%} + +%rename(assign) CVC4::Statistics::operator=(const StatisticsBase&); +%rename(assign) CVC4::Statistics::operator=(const Statistics& stats); + +#ifdef SWIGJAVA + +// Instead of StatisticsBase::begin() and end(), create an +// iterator() method on the Java side that returns a Java-style +// Iterator. +%ignore CVC4::StatisticsBase::begin(); +%ignore CVC4::StatisticsBase::end(); +%ignore CVC4::StatisticsBase::begin() const; +%ignore CVC4::StatisticsBase::end() const; +%extend CVC4::StatisticsBase { + CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> iterator() { + return CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>(*$self); + } +} + +// StatisticsBase is "iterable" on the Java side +%typemap(javainterfaces) CVC4::StatisticsBase "java.lang.Iterable<Object[]>"; + +// the JavaIteratorAdapter should not be public, and implements Iterator +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "java.util.Iterator<Object[]>"; +// add some functions to the Java side (do it here because there's no way to do these in C++) +%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> " + public void remove() { + throw new java.lang.UnsupportedOperationException(); + } + + public Object[] next() { + if(hasNext()) { + return getNext(); + } else { + throw new java.util.NoSuchElementException(); + } + } +" +// getNext() just allows C++ iterator access from Java-side next(), make it private +%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>::getNext() "private"; + +// map the types appropriately. for statistics, the "payload" of the iterator is an Object[]. +// These Object arrays are always of two elements, the first is a String and the second an +// SExpr. (On the C++ side, it is a std::pair<std::string, SExpr>.) +%typemap(jni) CVC4::StatisticsBase::const_iterator::value_type "jobjectArray"; +%typemap(jtype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]"; +%typemap(jstype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]"; +%typemap(javaout) CVC4::StatisticsBase::const_iterator::value_type { return $jnicall; } +%typemap(out) CVC4::StatisticsBase::const_iterator::value_type { + $result = jenv->NewObjectArray(2, jenv->FindClass("java/lang/Object"), $null); + jenv->SetObjectArrayElement($result, 0, jenv->NewStringUTF($1.first.c_str())); + jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/SExpr"); + jmethodID methodid = jenv->GetMethodID(clazz, "<init>", "(JZ)V"); + jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast<long>(new CVC4::SExpr($1.second)), true)); + }; + +#endif /* SWIGJAVA */ + +%include "expr/statistics.h" + +#ifdef SWIGJAVA + +%include "bindings/java_iterator_adapter.h" +%include "bindings/java_stream_adapters.h" + +%template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>; + +#endif /* SWIGJAVA */ diff --git a/src/expr/statistics_registry.cpp b/src/expr/statistics_registry.cpp new file mode 100644 index 000000000..c1db992c5 --- /dev/null +++ b/src/expr/statistics_registry.cpp @@ -0,0 +1,168 @@ +/********************* */ +/*! \file statistics_registry.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Kshitij Bansal, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "expr/statistics_registry.h" + +#include "expr/expr_manager.h" +#include "lib/clock_gettime.h" +#include "smt/smt_engine.h" + +#ifndef __BUILDING_STATISTICS_FOR_EXPORT +# include "smt/smt_engine_scope.h" +#endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */ + +#ifdef CVC4_STATISTICS_ON +# define __CVC4_USE_STATISTICS true +#else +# define __CVC4_USE_STATISTICS false +#endif + +#warning "TODO: Make StatisticsRegistry non-public again." +#warning "TODO: Make TimerStat non-public again." + +namespace CVC4 { + +namespace stats { + +// This is a friend of SmtEngine, just to reach in and get it. +// this isn't a class function because then there's a cyclic +// dependence. +inline StatisticsRegistry* getStatisticsRegistry(SmtEngine* smt) { + return smt->d_statisticsRegistry; +} + +inline StatisticsRegistry* getStatisticsRegistry(ExprManager* em) { + return em->getStatisticsRegistry(); +} + +}/* CVC4::stats namespace */ + +#ifndef __BUILDING_STATISTICS_FOR_EXPORT + +StatisticsRegistry* StatisticsRegistry::current() { + return stats::getStatisticsRegistry(smt::currentSmtEngine()); +} + +void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) { +#ifdef CVC4_STATISTICS_ON + StatSet& stats = current()->d_stats; + CheckArgument(stats.find(s) == stats.end(), s, + "Statistic `%s' was already registered with this registry.", + s->getName().c_str()); + stats.insert(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::registerStat() */ + +void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) { +#ifdef CVC4_STATISTICS_ON + StatSet& stats = current()->d_stats; + CheckArgument(stats.find(s) != stats.end(), s, + "Statistic `%s' was not registered with this registry.", + s->getName().c_str()); + stats.erase(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::unregisterStat() */ + +#endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */ + +void StatisticsRegistry::registerStat_(Stat* s) throw(CVC4::IllegalArgumentException) { +#ifdef CVC4_STATISTICS_ON + CheckArgument(d_stats.find(s) == d_stats.end(), s); + d_stats.insert(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::registerStat_() */ + +void StatisticsRegistry::unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException) { +#ifdef CVC4_STATISTICS_ON + CheckArgument(d_stats.find(s) != d_stats.end(), s); + d_stats.erase(s); +#endif /* CVC4_STATISTICS_ON */ +}/* StatisticsRegistry::unregisterStat_() */ + +void StatisticsRegistry::flushStat(std::ostream &out) const { +#ifdef CVC4_STATISTICS_ON + flushInformation(out); +#endif /* CVC4_STATISTICS_ON */ +} + +void StatisticsRegistry::flushInformation(std::ostream &out) const { +#ifdef CVC4_STATISTICS_ON + this->StatisticsBase::flushInformation(out); +#endif /* CVC4_STATISTICS_ON */ +} + +void TimerStat::start() { + if(__CVC4_USE_STATISTICS) { + CheckArgument(!d_running, *this, "timer already running"); + clock_gettime(CLOCK_MONOTONIC, &d_start); + d_running = true; + } +}/* TimerStat::start() */ + +void TimerStat::stop() { + if(__CVC4_USE_STATISTICS) { + CheckArgument(d_running, *this, "timer not running"); + ::timespec end; + clock_gettime(CLOCK_MONOTONIC, &end); + d_data += end - d_start; + d_running = false; + } +}/* TimerStat::stop() */ + +bool TimerStat::running() const { + return d_running; +}/* TimerStat::running() */ + +timespec TimerStat::getData() const { + ::timespec data = d_data; + if(__CVC4_USE_STATISTICS && d_running) { + ::timespec end; + clock_gettime(CLOCK_MONOTONIC, &end); + data += end - d_start; + } + return data; +} + +SExpr TimerStat::getValue() const { + ::timespec data = d_data; + if(__CVC4_USE_STATISTICS && d_running) { + ::timespec end; + clock_gettime(CLOCK_MONOTONIC, &end); + data += end - d_start; + } + std::stringstream ss; + ss << std::fixed << std::setprecision(8) << data; + return SExpr(Rational::fromDecimal(ss.str())); +}/* TimerStat::getValue() */ + +RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) : + d_reg(stats::getStatisticsRegistry(&em)), + d_stat(stat) { + d_reg->registerStat_(d_stat); +} + +RegisterStatistic::RegisterStatistic(SmtEngine& smt, Stat* stat) : + d_reg(stats::getStatisticsRegistry(&smt)), + d_stat(stat) { + d_reg->registerStat_(d_stat); +} + + + +}/* CVC4 namespace */ + +#undef __CVC4_USE_STATISTICS diff --git a/src/expr/statistics_registry.h b/src/expr/statistics_registry.h new file mode 100644 index 000000000..89efe4021 --- /dev/null +++ b/src/expr/statistics_registry.h @@ -0,0 +1,932 @@ +/********************* */ +/*! \file statistics_registry.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: Tim King + ** Minor contributors (to current version): Kshitij Bansal + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Statistics utility classes + ** + ** Statistics utility classes, including classes for holding (and referring + ** to) statistics, the statistics registry, and some other associated + ** classes. + **/ + +#include "cvc4_private_library.h" + +#ifndef __CVC4__STATISTICS_REGISTRY_H +#define __CVC4__STATISTICS_REGISTRY_H + +#include <stdint.h> + +#include <cassert> +#include <ctime> +#include <iomanip> +#include <map> +#include <sstream> +#include <vector> + +#include "base/exception.h" +#include "expr/statistics.h" +#include "lib/clock_gettime.h" + +namespace CVC4 { + +#ifdef CVC4_STATISTICS_ON +# define __CVC4_USE_STATISTICS true +#else +# define __CVC4_USE_STATISTICS false +#endif + +class ExprManager; +class SmtEngine; + +/** + * The base class for all statistics. + * + * This base class keeps the name of the statistic and declares the (pure) + * virtual function flushInformation(). Derived classes must implement + * this function and pass their name to the base class constructor. + * + * This class also (statically) maintains the delimiter used to separate + * the name and the value when statistics are output. + */ +class Stat { +protected: + /** The name of this statistic */ + std::string d_name; + +public: + + /** Nullary constructor, does nothing */ + Stat() { } + + /** + * Construct a statistic with the given name. Debug builds of CVC4 + * will throw an assertion exception if the given name contains the + * statistic delimiter string. + */ + Stat(const std::string& name) throw(CVC4::IllegalArgumentException) : + d_name(name) { + if(__CVC4_USE_STATISTICS) { + CheckArgument(d_name.find(", ") == std::string::npos, name, + "Statistics names cannot include a comma (',')"); + } + } + + /** Destruct a statistic. This base-class version does nothing. */ + virtual ~Stat() {} + + /** + * Flush the value of this statistic to an output stream. Should + * finish the output with an end-of-line character. + */ + virtual void flushInformation(std::ostream& out) const = 0; + + /** + * Flush the name,value pair of this statistic to an output stream. + * Uses the statistic delimiter string between name and value. + * + * May be redefined by a child class + */ + virtual void flushStat(std::ostream& out) const { + if(__CVC4_USE_STATISTICS) { + out << d_name << ", "; + flushInformation(out); + } + } + + /** Get the name of this statistic. */ + const std::string& getName() const { + return d_name; + } + + /** Get the value of this statistic as a string. */ + virtual SExpr getValue() const { + std::stringstream ss; + flushInformation(ss); + return SExpr(ss.str()); + } + +};/* class Stat */ + +// A generic way of making a SExpr from templated stats code. +// for example, the uint64_t version ensures that we create +// Integer-SExprs for ReadOnlyDataStats (like those inside +// Minisat) without having to specialize the entire +// ReadOnlyDataStat class template. +template <class T> +inline SExpr mkSExpr(const T& x) { + std::stringstream ss; + ss << x; + return SExpr(ss.str()); +} + +template <> +inline SExpr mkSExpr(const uint64_t& x) { + return SExpr(Integer(x)); +} + +template <> +inline SExpr mkSExpr(const int64_t& x) { + return SExpr(Integer(x)); +} + +template <> +inline SExpr mkSExpr(const int& x) { + return SExpr(Integer(x)); +} + +template <> +inline SExpr mkSExpr(const Integer& x) { + return SExpr(x); +} + +template <> +inline SExpr mkSExpr(const double& x) { + // roundabout way to get a Rational from a double + std::stringstream ss; + ss << std::fixed << std::setprecision(8) << x; + return SExpr(Rational::fromDecimal(ss.str())); +} + +template <> +inline SExpr mkSExpr(const Rational& x) { + return SExpr(x); +} + +/** + * A class to represent a "read-only" data statistic of type T. Adds to + * the Stat base class the pure virtual function getData(), which returns + * type T, and flushInformation(), which outputs the statistic value to an + * output stream (using the same existing stream insertion operator). + * + * Template class T must have stream insertion operation defined: + * std::ostream& operator<<(std::ostream&, const T&) + */ +template <class T> +class ReadOnlyDataStat : public Stat { +public: + /** The "payload" type of this data statistic (that is, T). */ + typedef T payload_t; + + /** Construct a read-only data statistic with the given name. */ + ReadOnlyDataStat(const std::string& name) : + Stat(name) { + } + + /** Get the value of the statistic. */ + virtual T getData() const = 0; + + /** Flush the value of the statistic to the given output stream. */ + void flushInformation(std::ostream& out) const { + if(__CVC4_USE_STATISTICS) { + out << getData(); + } + } + + SExpr getValue() const { + return mkSExpr(getData()); + } + +};/* class ReadOnlyDataStat<T> */ + + +/** + * A data statistic class. This class extends a read-only data statistic + * with assignment (the statistic can be set as well as read). This class + * adds to the read-only case a pure virtual function setData(), thus + * providing the basic interface for a data statistic: getData() to get the + * statistic value, and setData() to set it. + * + * As with the read-only data statistic class, template class T must have + * stream insertion operation defined: + * std::ostream& operator<<(std::ostream&, const T&) + */ +template <class T> +class DataStat : public ReadOnlyDataStat<T> { +public: + + /** Construct a data statistic with the given name. */ + DataStat(const std::string& name) : + ReadOnlyDataStat<T>(name) { + } + + /** Set the data statistic. */ + virtual void setData(const T&) = 0; + +};/* class DataStat<T> */ + + +/** + * A data statistic that references a data cell of type T, + * implementing getData() by referencing that memory cell, and + * setData() by reassigning the statistic to point to the new + * data cell. The referenced data cell is kept as a const + * reference, meaning the referenced data is never actually + * modified by this class (it must be externally modified for + * a reference statistic to make sense). A common use for + * this type of statistic is to output a statistic that is kept + * outside the statistics package (for example, one that's kept + * by a theory implementation for internal heuristic purposes, + * which is important to keep even if statistics are turned off). + * + * Template class T must have an assignment operator=(). + */ +template <class T> +class ReferenceStat : public DataStat<T> { +private: + /** The referenced data cell */ + const T* d_data; + +public: + /** + * Construct a reference stat with the given name and a reference + * to NULL. + */ + ReferenceStat(const std::string& name) : + DataStat<T>(name), + d_data(NULL) { + } + + /** + * Construct a reference stat with the given name and a reference to + * the given data. + */ + ReferenceStat(const std::string& name, const T& data) : + DataStat<T>(name), + d_data(NULL) { + setData(data); + } + + /** Set this reference statistic to refer to the given data cell. */ + void setData(const T& t) { + if(__CVC4_USE_STATISTICS) { + d_data = &t; + } + } + + /** Get the value of the referenced data cell. */ + T getData() const { + return *d_data; + } + +};/* class ReferenceStat<T> */ + + +/** + * A data statistic that keeps a T and sets it with setData(). + * + * Template class T must have an operator=() and a copy constructor. + */ +template <class T> +class BackedStat : public DataStat<T> { +protected: + /** The internally-kept statistic value */ + T d_data; + +public: + + /** Construct a backed statistic with the given name and initial value. */ + BackedStat(const std::string& name, const T& init) : + DataStat<T>(name), + d_data(init) { + } + + /** Set the underlying data value to the given value. */ + void setData(const T& t) { + if(__CVC4_USE_STATISTICS) { + d_data = t; + } + } + + /** Identical to setData(). */ + BackedStat<T>& operator=(const T& t) { + if(__CVC4_USE_STATISTICS) { + d_data = t; + } + return *this; + } + + /** Get the underlying data value. */ + T getData() const { + return d_data; + } + +};/* class BackedStat<T> */ + + +/** + * A wrapper Stat for another Stat. + * + * This type of Stat is useful in cases where a module (like the + * CongruenceClosure module) might keep its own statistics, but might + * be instantiated in many contexts by many clients. This makes such + * a statistic inappopriate to register with the StatisticsRegistry + * directly, as all would be output with the same name (and may be + * unregistered too quickly anyway). A WrappedStat allows the calling + * client (say, TheoryUF) to wrap the Stat from the client module, + * giving it a globally unique name. + */ +template <class Stat> +class WrappedStat : public ReadOnlyDataStat<typename Stat::payload_t> { + typedef typename Stat::payload_t T; + + const ReadOnlyDataStat<T>& d_stat; + + /** Private copy constructor undefined (no copy permitted). */ + WrappedStat(const WrappedStat&) CVC4_UNDEFINED; + /** Private assignment operator undefined (no copy permitted). */ + WrappedStat<T>& operator=(const WrappedStat&) CVC4_UNDEFINED; + +public: + + /** + * Construct a wrapped statistic with the given name that wraps the + * given statistic. + */ + WrappedStat(const std::string& name, const ReadOnlyDataStat<T>& stat) : + ReadOnlyDataStat<T>(name), + d_stat(stat) { + } + + /** Get the data of the underlying (wrapped) statistic. */ + T getData() const { + return d_stat.getData(); + } + + SExpr getValue() const { + return d_stat.getValue(); + } + +};/* class WrappedStat<T> */ + +/** + * A backed integer-valued (64-bit signed) statistic. + * This doesn't functionally differ from its base class BackedStat<int64_t>, + * except for adding convenience functions for dealing with integers. + */ +class IntStat : public BackedStat<int64_t> { +public: + + /** + * Construct an integer-valued statistic with the given name and + * initial value. + */ + IntStat(const std::string& name, int64_t init) : + BackedStat<int64_t>(name, init) { + } + + /** Increment the underlying integer statistic. */ + IntStat& operator++() { + if(__CVC4_USE_STATISTICS) { + ++d_data; + } + return *this; + } + + /** Increment the underlying integer statistic by the given amount. */ + IntStat& operator+=(int64_t val) { + if(__CVC4_USE_STATISTICS) { + d_data += val; + } + return *this; + } + + /** Keep the maximum of the current statistic value and the given one. */ + void maxAssign(int64_t val) { + if(__CVC4_USE_STATISTICS) { + if(d_data < val) { + d_data = val; + } + } + } + + /** Keep the minimum of the current statistic value and the given one. */ + void minAssign(int64_t val) { + if(__CVC4_USE_STATISTICS) { + if(d_data > val) { + d_data = val; + } + } + } + + SExpr getValue() const { + return SExpr(Integer(d_data)); + } + +};/* class IntStat */ + +template <class T> +class SizeStat : public Stat { +private: + const T& d_sized; +public: + SizeStat(const std::string&name, const T& sized) : + Stat(name), d_sized(sized) {} + ~SizeStat() {} + + void flushInformation(std::ostream& out) const { + out << d_sized.size(); + } + + SExpr getValue() const { + return SExpr(Integer(d_sized.size())); + } + +};/* class SizeStat */ + +/** + * The value for an AverageStat is the running average of (e1, e_2, ..., e_n), + * (e1 + e_2 + ... + e_n)/n, + * where e_i is an entry added by an addEntry(e_i) call. + * The value is initially always 0. + * (This is to avoid making parsers confused.) + * + * A call to setData() will change the running average but not reset the + * running count, so should generally be avoided. Call addEntry() to add + * an entry to the average calculation. + */ +class AverageStat : public BackedStat<double> { +private: + /** + * The number of accumulations of the running average that we + * have seen so far. + */ + uint32_t d_count; + double d_sum; + +public: + /** Construct an average statistic with the given name. */ + AverageStat(const std::string& name) : + BackedStat<double>(name, 0.0), d_count(0), d_sum(0.0) { + } + + /** Add an entry to the running-average calculation. */ + void addEntry(double e) { + if(__CVC4_USE_STATISTICS) { + ++d_count; + d_sum += e; + setData(d_sum / d_count); + } + } + + SExpr getValue() const { + std::stringstream ss; + ss << std::fixed << std::setprecision(8) << d_data; + return SExpr(Rational::fromDecimal(ss.str())); + } + +};/* class AverageStat */ + +/** A statistic that contains a SExpr. */ +class SExprStat : public Stat { +private: + SExpr d_data; + +public: + + /** + * Construct a SExpr-valued statistic with the given name and + * initial value. + */ + SExprStat(const std::string& name, const SExpr& init) : + Stat(name), d_data(init){} + + virtual void flushInformation(std::ostream& out) const { + out << d_data << std::endl; + } + + SExpr getValue() const { + return d_data; + } + +};/* class SExprStat */ + +template <class T> +class ListStat : public Stat { +private: + typedef std::vector<T> List; + List d_list; +public: + + /** + * Construct an integer-valued statistic with the given name and + * initial value. + */ + ListStat(const std::string& name) : Stat(name) {} + ~ListStat() {} + + void flushInformation(std::ostream& out) const{ + if(__CVC4_USE_STATISTICS) { + typename List::const_iterator i = d_list.begin(), end = d_list.end(); + out << "["; + if(i != end){ + out << *i; + ++i; + for(; i != end; ++i){ + out << ", " << *i; + } + } + out << "]"; + } + } + + ListStat& operator<<(const T& val){ + if(__CVC4_USE_STATISTICS) { + d_list.push_back(val); + } + return (*this); + } + +};/* class ListStat */ + +template <class T> +class HistogramStat : public Stat { +private: + typedef std::map<T, unsigned int> Histogram; + Histogram d_hist; +public: + + /** Construct a histogram of a stream of entries. */ + HistogramStat(const std::string& name) : Stat(name) {} + ~HistogramStat() {} + + void flushInformation(std::ostream& out) const{ + if(__CVC4_USE_STATISTICS) { + typename Histogram::const_iterator i = d_hist.begin(); + typename Histogram::const_iterator end = d_hist.end(); + out << "["; + while(i != end){ + const T& key = (*i).first; + unsigned int count = (*i).second; + out << "("<<key<<" : "<<count<< ")"; + ++i; + if(i != end){ + out << ", "; + } + } + out << "]"; + } + } + + HistogramStat& operator<<(const T& val){ + if(__CVC4_USE_STATISTICS) { + if(d_hist.find(val) == d_hist.end()){ + d_hist.insert(std::make_pair(val,0)); + } + d_hist[val]++; + } + return (*this); + } + +};/* class HistogramStat */ + +/****************************************************************************/ +/* Statistics Registry */ +/****************************************************************************/ + +/** + * The main statistics registry. This registry maintains the list of + * currently active statistics and is able to "flush" them all. + */ +class CVC4_PUBLIC StatisticsRegistry : public StatisticsBase, public Stat { +private: + + /** Private copy constructor undefined (no copy permitted). */ + StatisticsRegistry(const StatisticsRegistry&) CVC4_UNDEFINED; + +public: + + /** Construct an nameless statistics registry */ + StatisticsRegistry() {} + + /** Construct a statistics registry */ + StatisticsRegistry(const std::string& name) + throw(CVC4::IllegalArgumentException) : + Stat(name) { + d_prefix = name; + if(__CVC4_USE_STATISTICS) { + CheckArgument(d_name.find(s_regDelim) == std::string::npos, name, + "StatisticsRegistry names cannot contain the string \"%s\"", + s_regDelim.c_str()); + } + } + + /** + * Set the name of this statistic registry, used as prefix during + * output. (This version overrides StatisticsBase::setPrefix().) + */ + void setPrefix(const std::string& name) { + d_prefix = d_name = name; + } + +#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT) + /** Get a pointer to the current statistics registry */ + static StatisticsRegistry* current(); +#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && ! __BUILDING_STATISTICS_FOR_EXPORT */ + + /** Overridden to avoid the name being printed */ + void flushStat(std::ostream &out) const; + + virtual void flushInformation(std::ostream& out) const; + + SExpr getValue() const { + std::vector<SExpr> v; + for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) { + std::vector<SExpr> w; + w.push_back(SExpr((*i)->getName())); + w.push_back((*i)->getValue()); + v.push_back(SExpr(w)); + } + return SExpr(v); + } + +#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT) + /** Register a new statistic, making it active. */ + static void registerStat(Stat* s) throw(CVC4::IllegalArgumentException); + + /** Unregister an active statistic, making it inactive. */ + static void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException); +#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB) && ! __BUILDING_STATISTICS_FOR_EXPORT */ + + /** Register a new statistic */ + void registerStat_(Stat* s) throw(CVC4::IllegalArgumentException); + + /** Unregister a new statistic */ + void unregisterStat_(Stat* s) throw(CVC4::IllegalArgumentException); + +};/* class StatisticsRegistry */ + +}/* CVC4 namespace */ + +/****************************************************************************/ +/* Some utility functions for timespec */ +/****************************************************************************/ + +inline std::ostream& operator<<(std::ostream& os, const timespec& t); + +/** Compute the sum of two timespecs. */ +inline timespec& operator+=(timespec& a, const timespec& b) { + using namespace CVC4; + // assumes a.tv_nsec and b.tv_nsec are in range + const long nsec_per_sec = 1000000000L; // one thousand million + CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a); + CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b); + a.tv_sec += b.tv_sec; + long nsec = a.tv_nsec + b.tv_nsec; + assert(nsec >= 0); + if(nsec < 0) { + nsec += nsec_per_sec; + --a.tv_sec; + } + if(nsec >= nsec_per_sec) { + nsec -= nsec_per_sec; + ++a.tv_sec; + } + assert(nsec >= 0 && nsec < nsec_per_sec); + a.tv_nsec = nsec; + return a; +} + +/** Compute the difference of two timespecs. */ +inline timespec& operator-=(timespec& a, const timespec& b) { + using namespace CVC4; + // assumes a.tv_nsec and b.tv_nsec are in range + const long nsec_per_sec = 1000000000L; // one thousand million + CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a); + CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b); + a.tv_sec -= b.tv_sec; + long nsec = a.tv_nsec - b.tv_nsec; + if(nsec < 0) { + nsec += nsec_per_sec; + --a.tv_sec; + } + if(nsec >= nsec_per_sec) { + nsec -= nsec_per_sec; + ++a.tv_sec; + } + assert(nsec >= 0 && nsec < nsec_per_sec); + a.tv_nsec = nsec; + return a; +} + +/** Add two timespecs. */ +inline timespec operator+(const timespec& a, const timespec& b) { + timespec result = a; + return result += b; +} + +/** Subtract two timespecs. */ +inline timespec operator-(const timespec& a, const timespec& b) { + timespec result = a; + return result -= b; +} + +/** Compare two timespecs for equality. */ +inline bool operator==(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec; +} + +/** Compare two timespecs for disequality. */ +inline bool operator!=(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return !(a == b); +} + +/** Compare two timespecs, returning true iff a < b. */ +inline bool operator<(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return a.tv_sec < b.tv_sec || + (a.tv_sec == b.tv_sec && a.tv_nsec < b.tv_nsec); +} + +/** Compare two timespecs, returning true iff a > b. */ +inline bool operator>(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return a.tv_sec > b.tv_sec || + (a.tv_sec == b.tv_sec && a.tv_nsec > b.tv_nsec); +} + +/** Compare two timespecs, returning true iff a <= b. */ +inline bool operator<=(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return !(a > b); +} + +/** Compare two timespecs, returning true iff a >= b. */ +inline bool operator>=(const timespec& a, const timespec& b) { + // assumes a.tv_nsec and b.tv_nsec are in range + return !(a < b); +} + +/** Output a timespec on an output stream. */ +inline std::ostream& operator<<(std::ostream& os, const timespec& t) { + // assumes t.tv_nsec is in range + return os << t.tv_sec << "." + << std::setfill('0') << std::setw(9) << std::right << t.tv_nsec; +} + +namespace CVC4 { + +class CodeTimer; + +/** + * A timer statistic. The timer can be started and stopped + * arbitrarily, like a stopwatch; the value of the statistic at the + * end is the accumulated time over all (start,stop) pairs. + */ +class CVC4_PUBLIC TimerStat : public BackedStat<timespec> { + + // strange: timespec isn't placed in 'std' namespace ?! + /** The last start time of this timer */ + timespec d_start; + + /** Whether this timer is currently running */ + bool d_running; + +public: + + typedef CVC4::CodeTimer CodeTimer; + + /** + * Construct a timer statistic with the given name. Newly-constructed + * timers have a 0.0 value and are not running. + */ + TimerStat(const std::string& name) : + BackedStat< timespec >(name, timespec()), + d_running(false) { + /* timespec is POD and so may not be initialized to zero; + * here, ensure it is */ + d_data.tv_sec = d_data.tv_nsec = 0; + } + + /** Start the timer. */ + void start(); + + /** + * Stop the timer and update the statistic value with the + * accumulated time. + */ + void stop(); + + /** If the timer is currently running */ + bool running() const; + + timespec getData() const; + + SExpr getValue() const; + +};/* class TimerStat */ + +/** + * Utility class to make it easier to call stop() at the end of a + * code block. When constructed, it starts the timer. When + * destructed, it stops the timer. + */ +class CodeTimer { + TimerStat& d_timer; + bool d_reentrant; + + /** Private copy constructor undefined (no copy permitted). */ + CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED; + /** Private assignment operator undefined (no copy permitted). */ + CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED; + +public: + CodeTimer(TimerStat& timer, bool allow_reentrant = false) : d_timer(timer), d_reentrant(false) { + if(!allow_reentrant || !(d_reentrant = d_timer.running())) { + d_timer.start(); + } + } + ~CodeTimer() { + if(!d_reentrant) { + d_timer.stop(); + } + } +};/* class CodeTimer */ + +/** + * To use a statistic, you need to declare it, initialize it in your + * constructor, register it in your constructor, and deregister it in + * your destructor. Instead, this macro does it all for you (and + * therefore also keeps the statistic type, field name, and output + * string all in the same place in your class's header. Its use is + * like in this example, which takes the place of the declaration of a + * statistics field "d_checkTimer": + * + * KEEP_STATISTIC(TimerStat, d_checkTimer, "theory::uf::checkTime"); + * + * If any args need to be passed to the constructor, you can specify + * them after the string. + * + * The macro works by creating a nested class type, derived from the + * statistic type you give it, which declares a registry-aware + * constructor/destructor pair. + */ +#define KEEP_STATISTIC(_StatType, _StatField, _StatName, _CtorArgs...) \ + struct Statistic_##_StatField : public _StatType { \ + Statistic_##_StatField() : _StatType(_StatName, ## _CtorArgs) { \ + StatisticsRegistry::registerStat(this); \ + } \ + ~Statistic_##_StatField() { \ + StatisticsRegistry::unregisterStat(this); \ + } \ + } _StatField + +/** + * Resource-acquisition-is-initialization idiom for statistics + * registry. Useful for stack-based statistics (like in the driver). + * Generally, for statistics kept in a member field of class, it's + * better to use the above KEEP_STATISTIC(), which does declaration of + * the member, construction of the statistic, and + * registration/unregistration. This RAII class only does + * registration and unregistration. + */ +class RegisterStatistic { + + StatisticsRegistry* d_reg; + Stat* d_stat; + +public: + +#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && ! defined(__BUILDING_STATISTICS_FOR_EXPORT) + RegisterStatistic(Stat* stat) : + d_reg(StatisticsRegistry::current()), + d_stat(stat) { + if(d_reg != NULL) { + throw CVC4::Exception("There is no current statistics registry!"); + } + StatisticsRegistry::registerStat(d_stat); + } +#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && ! __BUILDING_STATISTICS_FOR_EXPORT */ + + RegisterStatistic(StatisticsRegistry* reg, Stat* stat) : + d_reg(reg), + d_stat(stat) { + CheckArgument(reg != NULL, reg, + "You need to specify a statistics registry" + "on which to set the statistic"); + d_reg->registerStat_(d_stat); + } + + RegisterStatistic(ExprManager& em, Stat* stat); + + RegisterStatistic(SmtEngine& smt, Stat* stat); + + ~RegisterStatistic() { + d_reg->unregisterStat_(d_stat); + } + +};/* class RegisterStatistic */ + +#undef __CVC4_USE_STATISTICS + +}/* CVC4 namespace */ + +#endif /* __CVC4__STATISTICS_REGISTRY_H */ diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 46705a849..327be72eb 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -13,16 +13,16 @@ ** ** Implementation of expression types. **/ +#include "expr/type.h" #include <iostream> #include <string> #include <vector> +#include "base/exception.h" #include "expr/node_manager.h" #include "expr/node_manager_attributes.h" -#include "expr/type.h" #include "expr/type_node.h" -#include "util/exception.h" using namespace std; diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 0f5e020d8..ce006a4f1 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -27,9 +27,9 @@ #include <iostream> #include <stdint.h> +#include "base/cvc4_assert.h" #include "expr/kind.h" #include "expr/metakind.h" -#include "util/cvc4_assert.h" #include "util/cardinality.h" namespace CVC4 { diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index b54fd8809..bc780a7e5 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -21,13 +21,13 @@ #line 23 "${template}" +#include <sstream> + +#include "base/cvc4_assert.h" +#include "options/language.h" #include "expr/type_node.h" -#include "util/cvc4_assert.h" #include "expr/kind.h" #include "expr/expr.h" -#include "util/language.h" - -#include <sstream> ${type_properties_includes} diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp new file mode 100644 index 000000000..d41ab1045 --- /dev/null +++ b/src/expr/uninterpreted_constant.cpp @@ -0,0 +1,39 @@ +/********************* */ +/*! \file uninterpreted_constant.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of constants of uninterpreted sorts + ** + ** Representation of constants of uninterpreted sorts. + **/ + +#include "expr/uninterpreted_constant.h" + +#include <iostream> +#include <sstream> +#include <string> + +using namespace std; + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) { + stringstream ss; + ss << uc.getType(); + string t = ss.str(); + size_t i = 0; + // replace everything that isn't in [a-zA-Z0-9_] with an _ + while((i = t.find_first_not_of("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ1234567890_", i)) != string::npos) { + t.replace(i, 1, 1, '_'); + } + return out << "uc_" << t << '_' << uc.getIndex(); +} + +}/* CVC4 namespace */ diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h new file mode 100644 index 000000000..13a80a19d --- /dev/null +++ b/src/expr/uninterpreted_constant.h @@ -0,0 +1,84 @@ +/********************* */ +/*! \file uninterpreted_constant.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of constants of uninterpreted sorts + ** + ** Representation of constants of uninterpreted sorts. + **/ + +#include "cvc4_public.h" + +#pragma once + +#include "expr/type.h" +#include <iostream> + +namespace CVC4 { + +class CVC4_PUBLIC UninterpretedConstant { + const Type d_type; + const Integer d_index; + +public: + + UninterpretedConstant(Type type, Integer index) throw(IllegalArgumentException) : + d_type(type), + d_index(index) { + //CheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str()); + CheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str()); + } + + ~UninterpretedConstant() throw() { + } + + Type getType() const throw() { + return d_type; + } + const Integer& getIndex() const throw() { + return d_index; + } + + bool operator==(const UninterpretedConstant& uc) const throw() { + return d_type == uc.d_type && d_index == uc.d_index; + } + bool operator!=(const UninterpretedConstant& uc) const throw() { + return !(*this == uc); + } + + bool operator<(const UninterpretedConstant& uc) const throw() { + return d_type < uc.d_type || + (d_type == uc.d_type && d_index < uc.d_index); + } + bool operator<=(const UninterpretedConstant& uc) const throw() { + return d_type < uc.d_type || + (d_type == uc.d_type && d_index <= uc.d_index); + } + bool operator>(const UninterpretedConstant& uc) const throw() { + return !(*this <= uc); + } + bool operator>=(const UninterpretedConstant& uc) const throw() { + return !(*this < uc); + } + +};/* class UninterpretedConstant */ + +std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) CVC4_PUBLIC; + +/** + * Hash function for the BitVector constants. + */ +struct CVC4_PUBLIC UninterpretedConstantHashFunction { + inline size_t operator()(const UninterpretedConstant& uc) const { + return TypeHashFunction()(uc.getType()) * IntegerHashFunction()(uc.getIndex()); + } +};/* struct UninterpretedConstantHashFunction */ + +}/* CVC4 namespace */ diff --git a/src/expr/uninterpreted_constant.i b/src/expr/uninterpreted_constant.i new file mode 100644 index 000000000..1636eba5b --- /dev/null +++ b/src/expr/uninterpreted_constant.i @@ -0,0 +1,17 @@ +%{ +#include "expr/uninterpreted_constant.h" +%} + +%rename(less) CVC4::UninterpretedConstant::operator<(const UninterpretedConstant&) const; +%rename(lessEqual) CVC4::UninterpretedConstant::operator<=(const UninterpretedConstant&) const; +%rename(greater) CVC4::UninterpretedConstant::operator>(const UninterpretedConstant&) const; +%rename(greaterEqual) CVC4::UninterpretedConstant::operator>=(const UninterpretedConstant&) const; + +%rename(equals) CVC4::UninterpretedConstant::operator==(const UninterpretedConstant&) const; +%ignore CVC4::UninterpretedConstant::operator!=(const UninterpretedConstant&) const; + +%rename(apply) CVC4::UninterpretedConstantHashFunction::operator()(const UninterpretedConstant&) const; + +%ignore CVC4::operator<<(std::ostream&, const UninterpretedConstant&); + +%include "expr/uninterpreted_constant.h" |