summaryrefslogtreecommitdiff
path: root/src/compat
diff options
context:
space:
mode:
Diffstat (limited to 'src/compat')
-rw-r--r--src/compat/cvc3_compat.cpp167
-rw-r--r--src/compat/cvc3_compat.h20
2 files changed, 173 insertions, 14 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index dd9fcdfbd..51b0c6083 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -3,9 +3,9 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
- ** Minor contributors (to current version): Tim King, Dejan Jovanovic, Tianyi Liang
+ ** Minor contributors (to current version): Andrew Reynolds, Tim King, Dejan Jovanovic, Tianyi Liang
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** 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
**
@@ -350,12 +350,11 @@ bool Expr::isExists() const {
}
bool Expr::isLambda() const {
- // when implemented, also fix isClosure() below
- Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+ return getKind() == CVC4::kind::LAMBDA;
}
bool Expr::isClosure() const {
- return isQuantifier();
+ return isQuantifier() || isLambda();
}
bool Expr::isQuantifier() const {
@@ -366,10 +365,22 @@ bool Expr::isApply() const {
return hasOperator();
}
+bool Expr::isSymbol() const {
+ Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+}
+
bool Expr::isTheorem() const {
return false;
}
+bool Expr::isType() const {
+ return s_exprToType.find(*this) != s_exprToType.end();
+}
+
+bool Expr::isTerm() const {
+ return !getType().isBool();
+}
+
bool Expr::isConstant() const {
return isConst();
}
@@ -378,6 +389,122 @@ bool Expr::isRawList() const {
return false;
}
+bool Expr::isAtomic() const {
+ if (getType().isBool()) {
+ return isBoolConst();
+ }
+ for (int k = 0; k < arity(); ++k) {
+ if (!(*this)[k].isAtomic()) {
+ return false;
+ }
+ }
+ return true;
+}
+
+bool Expr::isAtomicFormula() const {
+ if (!getType().isBool()) {
+ return false;
+ }
+ switch(getKind()) {
+ case CVC4::kind::FORALL:
+ case CVC4::kind::EXISTS:
+ case CVC4::kind::XOR:
+ case CVC4::kind::NOT:
+ case CVC4::kind::AND:
+ case CVC4::kind::OR:
+ case CVC4::kind::ITE:
+ case CVC4::kind::IFF:
+ case CVC4::kind::IMPLIES:
+ return false;
+ default:
+ ; /* fall through */
+ }
+ for (Expr::iterator k = begin(), kend=end(); k != kend; ++k) {
+ if (!CVC3::Expr(*k).isAtomic()) {
+ return false;
+ }
+ }
+ return true;
+}
+
+bool Expr::isAbsAtomicFormula() const {
+ return isQuantifier() || isAtomicFormula();
+}
+
+bool Expr::isLiteral() const {
+ return isAtomicFormula() || (isNot() && (*this)[0].isAtomicFormula());
+}
+
+bool Expr::isAbsLiteral() const {
+ return isAbsAtomicFormula() || (isNot() && (*this)[0].isAbsAtomicFormula());
+}
+
+bool Expr::isBoolConnective() const {
+ if (!getType().isBool()) {
+ return false;
+ }
+ switch (getKind()) {
+ case CVC4::kind::NOT:
+ case CVC4::kind::AND:
+ case CVC4::kind::OR:
+ case CVC4::kind::IMPLIES:
+ case CVC4::kind::IFF:
+ case CVC4::kind::XOR:
+ case CVC4::kind::ITE:
+ return true;
+ default:
+ return false;
+ }
+}
+
+bool Expr::isPropLiteral() const {
+ return (isNot() && (*this)[0].isPropAtom()) || isPropAtom();
+}
+
+bool Expr::isPropAtom() const {
+ return !isTerm() && !isBoolConnective();
+}
+
+std::string Expr::getName() const {
+ Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+}
+
+std::string Expr::getUid() const {
+ Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+}
+
+std::string Expr::getString() const {
+ CVC4::CheckArgument(getKind() == CVC4::kind::CONST_STRING, *this, "CVC3::Expr::getString(): not a string Expr: `%s'", toString().c_str());
+ return getConst<CVC4::String>().toString();
+}
+
+std::vector<Expr> Expr::getVars() const {
+ CVC4::CheckArgument(isClosure(), *this, "CVC3::Expr::getVars(): not a closure Expr: `%s'", toString().c_str());
+ const vector<CVC4::Expr>& kids = (*this)[0].getChildren();
+ vector<Expr> v;
+ for(vector<CVC4::Expr>::const_iterator i = kids.begin(); i != kids.end(); ++i) {
+ v.push_back(*i);
+ }
+ return v;
+}
+
+Expr Expr::getExistential() const {
+ Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+}
+
+int Expr::getBoundIndex() const {
+ Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+}
+
+Expr Expr::getBody() const {
+ CVC4::CheckArgument(isClosure(), *this, "CVC3::Expr::getBody(): not a closure Expr: `%s'", toString().c_str());
+ return (*this)[1];
+}
+
+Theorem Expr::getTheorem() const {
+ Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+}
+
bool Expr::isEq() const {
return getKind() == CVC4::kind::EQUAL;
}
@@ -418,6 +545,11 @@ bool Expr::isSkolem() const {
return getKind() == CVC4::kind::SKOLEM;
}
+const Rational& Expr::getRational() const {
+ CVC4::CheckArgument(isRational(), *this, "CVC3::Expr::getRational(): not a rational Expr: `%s'", toString().c_str());
+ return getConst<CVC4::Rational>();
+}
+
Op Expr::mkOp() const {
return *this;
}
@@ -492,6 +624,31 @@ Type Expr::lookupType() const {
return getType();
}
+void Expr::pprint() const {
+ std::cout << *this << std::endl;
+}
+
+void Expr::pprintnodag() const {
+ CVC4::expr::ExprDag::Scope scope(std::cout, 0);
+ std::cout << *this << std::endl;
+}
+
+bool isArrayLiteral(const Expr& e) {
+ Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+}
+
+std::string ExprManager::getKindName(int kind) {
+ return CVC4::kind::kindToString(CVC4::Kind(kind));
+}
+
+InputLanguage ExprManager::getInputLang() const {
+ return getOptions()[CVC4::options::inputLanguage];
+}
+
+InputLanguage ExprManager::getOutputLang() const {
+ return CVC4::language::toInputLanguage(getOptions()[CVC4::options::outputLanguage]);
+}
+
Expr Expr::operator[](int i) const {
return Expr(this->CVC4::Expr::operator[](i));
}
diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index 444849574..0fa4a7ce5 100644
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): Francois Bobot
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** 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
**
@@ -318,6 +318,8 @@ typedef Expr Op;
*/
class CVC4_PUBLIC Expr : public CVC4::Expr {
public:
+ typedef CVC4::Expr::const_iterator iterator;
+
Expr();
Expr(const Expr& e);
Expr(const CVC4::Expr& e);
@@ -376,15 +378,15 @@ public:
bool isPropLiteral() const;
bool isPropAtom() const;
- const std::string& getName() const;
- const std::string& getUid() const;
+ std::string getName() const;
+ std::string getUid() const;
- const std::string& getString() const;
- const std::vector<Expr>& getVars() const;
- const Expr& getExistential() const;
+ std::string getString() const;
+ std::vector<Expr> getVars() const;
+ Expr getExistential() const;
int getBoundIndex() const;
- const Expr& getBody() const;
- const Theorem& getTheorem() const;
+ Expr getBody() const;
+ Theorem getTheorem() const;
bool isEq() const;
bool isNot() const;
@@ -450,7 +452,7 @@ bool isArrayLiteral(const Expr&) CVC4_PUBLIC;
class CVC4_PUBLIC ExprManager : public CVC4::ExprManager {
public:
- const std::string& getKindName(int kind);
+ std::string getKindName(int kind);
//! Get the input language for printing
InputLanguage getInputLang() const;
//! Get the output language for printing
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback