diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-21 20:12:42 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-21 21:08:00 -0400 |
commit | 3264f3bb76944129074c2a3204a94f0b02740e23 (patch) | |
tree | 08c1717bc353a258b6f273ed150057d085a1fa9a /src/compat | |
parent | a5f710d9147870024996bc5a1dedfcf183b6257c (diff) |
Fix to the compatibility library (this does fix the build).
Diffstat (limited to 'src/compat')
-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 { |