From 32c2090301d549efcb8a6ad7034b0553ed99b433 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 21 Jun 2014 17:15:24 -0400 Subject: [PATCH] Add some missing functions in configuration and compat library. --- src/compat/cvc3_compat.cpp | 156 +++++++++++++++++++++++++++++++++++- src/compat/cvc3_compat.h | 18 +++-- src/main/options_handlers.h | 1 + src/util/configuration.cpp | 4 + 4 files changed, 168 insertions(+), 11 deletions(-) diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index dd9fcdfbd..ee96f79ec 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -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,115 @@ bool Expr::isRawList() const { return false; } +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; + } + 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; + } + 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 { + if(getKind() == CVC4::kind::SEXPR) { + CVC4::SExpr s = getConst(); + if(s.isString() || s.isKeyword()) { + return s.getValue(); + } + } else if(getKind() == CVC4::kind::CONST_STRING) { + return getConst().toString(); + } + + CVC4::CheckArgument(false, *this, "CVC3::Expr::getString(): not a string Expr: `%s'", toString().c_str()); +} + +std::vector Expr::getVars() const { + CVC4::CheckArgument(isClosure(), *this, "CVC3::Expr::getVars(): not a closure Expr: `%s'", toString().c_str()); + const vector& kids = (*this)[0].getChildren(); + vector v; + for(vector::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 +538,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(); +} + Op Expr::mkOp() const { return *this; } @@ -492,6 +617,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..a43da5aa3 100644 --- a/src/compat/cvc3_compat.h +++ b/src/compat/cvc3_compat.h @@ -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& getVars() const; - const Expr& getExistential() const; + std::string getString() const; + std::vector 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 diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h index ee16af2f2..02ebf2252 100644 --- a/src/main/options_handlers.h +++ b/src/main/options_handlers.h @@ -68,6 +68,7 @@ inline void showConfiguration(std::string option, SmtEngine* smt) { printf("gmp : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no"); printf("glpk : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no"); printf("abc : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no"); + printf("readline : %s\n", Configuration::isBuiltWithReadline() ? "yes" : "no"); printf("tls : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no"); exit(0); } diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 05f5c7678..60ee86b36 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -129,6 +129,10 @@ bool Configuration::isBuiltWithAbc() { return IS_ABC_BUILD; } +bool Configuration::isBuiltWithReadline() { + return IS_READLINE_BUILD; +} + bool Configuration::isBuiltWithCudd() { return false; } -- 2.30.2