From 0ff3d2dbf187376c3a9aeeeae8d3f47e4d73c1c9 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 23 Aug 2017 11:13:07 -0700 Subject: [PATCH] Fix typos --- src/smt/smt_engine.cpp | 6 +++--- src/theory/bv/theory_bv.cpp | 4 ++-- src/theory/bv/theory_bv.h | 2 +- src/theory/theory_engine.cpp | 4 ++-- src/theory/theory_engine.h | 2 +- 5 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 20209fdcb..f360ae2fd 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -742,8 +742,8 @@ public: } ResourceManager* getResourceManager() { return d_resourceManager; } - void spendResource(unsigned ammount) throw(UnsafeInterruptException) { - d_resourceManager->spendResource(ammount); + void spendResource(unsigned amount) throw(UnsafeInterruptException) { + d_resourceManager->spendResource(amount); } void nmNotifyNewSort(TypeNode tn, uint32_t flags) { @@ -3992,7 +3992,7 @@ void SmtEnginePrivate::processAssertions() { } if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertions.ref()); + d_smt.d_theoryEngine->mkAckermanizationAssertions(d_assertions.ref()); } if ( options::bvAbstraction() && diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index fcd731266..116903ea6 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -217,8 +217,8 @@ void TheoryBV::storeFunction(TNode func, TNode term) { } } -void TheoryBV::mkAckermanizationAsssertions(std::vector& assertions) { - Debug("bv-ackermanize") << "TheoryBV::mkAckermanizationAsssertions\n"; +void TheoryBV::mkAckermanizationAssertions(std::vector& assertions) { + Debug("bv-ackermanize") << "TheoryBV::mkAckermanizationAssertions\n"; Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); AlwaysAssert(!options::incrementalSolving()); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index c20df35d5..c21938aa7 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -68,7 +68,7 @@ public: Node expandDefinition(LogicRequest &logicRequest, Node node); - void mkAckermanizationAsssertions(std::vector& assertions); + void mkAckermanizationAssertions(std::vector& assertions); void preRegisterTerm(TNode n); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 1023071dc..59a52a048 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1945,9 +1945,9 @@ bool TheoryEngine::ppBvAbstraction(const std::vector& assertions, std::ve return bv_theory->applyAbstraction(assertions, new_assertions); } -void TheoryEngine::mkAckermanizationAsssertions(std::vector& assertions) { +void TheoryEngine::mkAckermanizationAssertions(std::vector& assertions) { bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV]; - bv_theory->mkAckermanizationAsssertions(assertions); + bv_theory->mkAckermanizationAssertions(assertions); } Node TheoryEngine::ppSimpITE(TNode assertion) diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 408bff228..7dd3f57a6 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -834,7 +834,7 @@ public: void ppBvToBool(const std::vector& assertions, std::vector& new_assertions); void ppBoolToBv(const std::vector& assertions, std::vector& new_assertions); bool ppBvAbstraction(const std::vector& assertions, std::vector& new_assertions); - void mkAckermanizationAsssertions(std::vector& assertions); + void mkAckermanizationAssertions(std::vector& assertions); Node ppSimpITE(TNode assertion); /** Returns false if an assertion simplified to false. */ -- 2.30.2