summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/Makefile.am4
-rw-r--r--src/util/boolean_simplification.h2
-rw-r--r--src/util/chain.h50
-rw-r--r--src/util/chain.i12
-rw-r--r--src/util/result.cpp21
-rw-r--r--src/util/result.h35
-rw-r--r--src/util/util_model.h6
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback