diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 4 | ||||
-rw-r--r-- | src/util/boolean_simplification.h | 2 | ||||
-rw-r--r-- | src/util/chain.h | 50 | ||||
-rw-r--r-- | src/util/chain.i | 12 | ||||
-rw-r--r-- | src/util/result.cpp | 21 | ||||
-rw-r--r-- | src/util/result.h | 35 | ||||
-rw-r--r-- | src/util/util_model.h | 6 |
7 files changed, 108 insertions, 22 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 51eb5cb1a..23318b95d 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -77,6 +77,7 @@ libutil_la_SOURCES = \ ite_removal.h \ ite_removal.cpp \ node_visitor.h \ + chain.h \ index.h \ uninterpreted_constant.h \ uninterpreted_constant.cpp \ @@ -139,7 +140,8 @@ EXTRA_DIST = \ rational.i \ hash.i \ predicate.i \ - uninterpreted_constant.i + uninterpreted_constant.i \ + chain.i DISTCLEANFILES = \ integer.h.tmp \ diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h index e5c4ead6c..be39f69c1 100644 --- a/src/util/boolean_simplification.h +++ b/src/util/boolean_simplification.h @@ -22,6 +22,7 @@ #include <vector> #include <algorithm> +#include "expr/expr_manager_scope.h" #include "expr/node.h" #include "util/cvc4_assert.h" @@ -202,6 +203,7 @@ public: * @param e the Expr to negate (cannot be the null Expr) */ static Expr negate(Expr e) throw(AssertionException) { + ExprManagerScope ems(e); return negate(Node::fromExpr(e)).toExpr(); } diff --git a/src/util/chain.h b/src/util/chain.h new file mode 100644 index 000000000..2e9cf7bf6 --- /dev/null +++ b/src/util/chain.h @@ -0,0 +1,50 @@ +/********************* */ +/*! \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-2013 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 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) { + return out << ch.getOperator(); +} + +struct 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/util/chain.i b/src/util/chain.i new file mode 100644 index 000000000..1c97a527f --- /dev/null +++ b/src/util/chain.i @@ -0,0 +1,12 @@ +%{ +#include "util/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 "util/chain.h" diff --git a/src/util/result.cpp b/src/util/result.cpp index e0e34f07d..909a7d8c6 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -27,11 +27,12 @@ using namespace std; namespace CVC4 { -Result::Result(const std::string& instr) : +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_unknownExplanation(UNKNOWN_REASON), + d_inputName(inputName) { string s = instr; transform(s.begin(), s.end(), s.begin(), ::tolower); if(s == "sat" || s == "satisfiable") { @@ -115,13 +116,13 @@ Result Result::asSatisfiabilityResult() const throw() { switch(d_validity) { case INVALID: - return Result(SAT); + return Result(SAT, d_inputName); case VALID: - return Result(UNSAT); + return Result(UNSAT, d_inputName); case VALIDITY_UNKNOWN: - return Result(SAT_UNKNOWN, d_unknownExplanation); + return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName); default: Unhandled(d_validity); @@ -129,7 +130,7 @@ Result Result::asSatisfiabilityResult() const throw() { } // TYPE_NONE - return Result(SAT_UNKNOWN, NO_STATUS); + return Result(SAT_UNKNOWN, NO_STATUS, d_inputName); } Result Result::asValidityResult() const throw() { @@ -141,13 +142,13 @@ Result Result::asValidityResult() const throw() { switch(d_sat) { case SAT: - return Result(INVALID); + return Result(INVALID, d_inputName); case UNSAT: - return Result(VALID); + return Result(VALID, d_inputName); case SAT_UNKNOWN: - return Result(VALIDITY_UNKNOWN, d_unknownExplanation); + return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName); default: Unhandled(d_sat); @@ -155,7 +156,7 @@ Result Result::asValidityResult() const throw() { } // TYPE_NONE - return Result(VALIDITY_UNKNOWN, NO_STATUS); + return Result(VALIDITY_UNKNOWN, NO_STATUS, d_inputName); } string Result::toString() const { diff --git a/src/util/result.h b/src/util/result.h index cb1bd50fa..54ec3a38c 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -71,47 +71,58 @@ private: enum Validity d_validity; enum Type d_which; enum UnknownExplanation d_unknownExplanation; + std::string d_inputName; public: - Result() : + Result(std::string inputName = "") : d_sat(SAT_UNKNOWN), d_validity(VALIDITY_UNKNOWN), d_which(TYPE_NONE), - d_unknownExplanation(UNKNOWN_REASON) { + d_unknownExplanation(UNKNOWN_REASON), + d_inputName(inputName) { } - Result(enum Sat s) : + Result(enum Sat s, std::string inputName = "") : d_sat(s), d_validity(VALIDITY_UNKNOWN), d_which(TYPE_SAT), - d_unknownExplanation(UNKNOWN_REASON) { + d_unknownExplanation(UNKNOWN_REASON), + d_inputName(inputName) { CheckArgument(s != SAT_UNKNOWN, "Must provide a reason for satisfiability being unknown"); } - Result(enum Validity v) : + Result(enum Validity v, std::string inputName = "") : d_sat(SAT_UNKNOWN), d_validity(v), d_which(TYPE_VALIDITY), - d_unknownExplanation(UNKNOWN_REASON) { + 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) : + 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_unknownExplanation(unknownExplanation), + d_inputName(inputName) { CheckArgument(s == SAT_UNKNOWN, "improper use of unknown-result constructor"); } - Result(enum Validity v, enum UnknownExplanation unknownExplanation) : + 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_unknownExplanation(unknownExplanation), + d_inputName(inputName) { CheckArgument(v == VALIDITY_UNKNOWN, "improper use of unknown-result constructor"); } - Result(const std::string& s); + 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; @@ -142,6 +153,8 @@ public: std::string toString() const; + std::string getInputName() const { return d_inputName; } + };/* class Result */ inline bool Result::operator!=(const Result& r) const throw() { diff --git a/src/util/util_model.h b/src/util/util_model.h index 365e7124d..e5bd1f955 100644 --- a/src/util/util_model.h +++ b/src/util/util_model.h @@ -33,6 +33,10 @@ std::ostream& operator<<(std::ostream&, const Model&); class Model { friend std::ostream& operator<<(std::ostream&, const Model&); + friend class SmtEngine; + + /** the input name (file name, etc.) this model is associated to */ + std::string d_inputName; protected: /** The SmtEngine we're associated with */ @@ -52,6 +56,8 @@ public: SmtEngine* getSmtEngine() { return &d_smt; } /** get the smt engine (as a pointer-to-const) that this model is hooked up to */ const SmtEngine* getSmtEngine() const { return &d_smt; } + /** get the input name (file name, etc.) this model is associated to */ + std::string getInputName() const { return d_inputName; } public: /** get value for expression */ |