diff options
-rw-r--r-- | src/compat/cvc3_compat.cpp | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index ee96f79ec..b4ab57283 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -389,6 +389,18 @@ 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; @@ -459,16 +471,8 @@ std::string Expr::getUid() const { } std::string Expr::getString() const { - if(getKind() == CVC4::kind::SEXPR) { - CVC4::SExpr s = getConst<CVC4::SExpr>(); - if(s.isString() || s.isKeyword()) { - return s.getValue(); - } - } else if(getKind() == CVC4::kind::CONST_STRING) { - return getConst<CVC4::String>().toString(); - } - - CVC4::CheckArgument(false, *this, "CVC3::Expr::getString(): not a string Expr: `%s'", toString().c_str()); + 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 { |