diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-06 20:05:20 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-06 20:05:20 +0000 |
commit | 85a8d1bf09f91a041caa1723b30fe9f9ebf571f8 (patch) | |
tree | 8c2376e66a03a3f73a5a38b3dffc552e6999c469 /src/compat/cvc3_compat.cpp | |
parent | 84a3411720a59410c7dff7bc8ec9210638b7665b (diff) |
fixes to the compatibility layer; this fixes the broken system test
Diffstat (limited to 'src/compat/cvc3_compat.cpp')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index fafc8ccb2..4e884a9ab 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -761,6 +761,7 @@ ValidityChecker::ValidityChecker() : d_smt(NULL), d_parserContext(NULL), d_exprTypeMapRemove(), + d_stackLevel(0), d_constructors(), d_selectors() { d_em = reinterpret_cast<ExprManager*>(new CVC4::ExprManager(d_options)); @@ -779,6 +780,7 @@ ValidityChecker::ValidityChecker(const CLFlags& clflags) : d_smt(NULL), d_parserContext(NULL), d_exprTypeMapRemove(), + d_stackLevel(0), d_constructors(), d_selectors() { d_em = reinterpret_cast<ExprManager*>(new CVC4::ExprManager(d_options)); @@ -2228,19 +2230,29 @@ Proof ValidityChecker::getProofClosure() { } int ValidityChecker::stackLevel() { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + return d_stackLevel; } void ValidityChecker::push() { + ++d_stackLevel; d_smt->push(); } void ValidityChecker::pop() { d_smt->pop(); + --d_stackLevel; } void ValidityChecker::popto(int stackLevel) { - Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)"); + CheckArgument(stackLevel >= 0, stackLevel, + "Cannot pop to a negative stack level %d", stackLevel); + CheckArgument(unsigned(stackLevel) <= d_stackLevel, stackLevel, + "Cannot pop to a stack level higher than the current one! " + "At stack level %u, user requested stack level %d", + d_stackLevel, stackLevel); + while(unsigned(stackLevel) < d_stackLevel) { + pop(); + } } int ValidityChecker::scopeLevel() { @@ -2257,15 +2269,12 @@ void ValidityChecker::popScope() { void ValidityChecker::poptoScope(int scopeLevel) { CheckArgument(scopeLevel >= 0, scopeLevel, - "Cannot pop to a negative scope level %u", scopeLevel); + "Cannot pop to a negative scope level %d", scopeLevel); CheckArgument(unsigned(scopeLevel) <= d_parserContext->getDeclarationLevel(), scopeLevel, "Cannot pop to a scope level higher than the current one! " "At scope level %u, user requested scope level %d", d_parserContext->getDeclarationLevel(), scopeLevel); - CheckArgument(scopeLevel <= d_parserContext->getDeclarationLevel(), - scopeLevel, - "Cannot pop to a higher scope level"); while(unsigned(scopeLevel) < d_parserContext->getDeclarationLevel()) { popScope(); } |