diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/decision_engine.cpp | 3 | ||||
-rw-r--r-- | src/util/decision_engine.h | 2 | ||||
-rw-r--r-- | src/util/options.cpp | 2 | ||||
-rw-r--r-- | src/util/output.cpp | 4 | ||||
-rw-r--r-- | src/util/rational_cln_imp.cpp | 2 | ||||
-rw-r--r-- | src/util/rational_gmp_imp.cpp | 2 | ||||
-rw-r--r-- | src/util/result.cpp | 2 |
7 files changed, 9 insertions, 8 deletions
diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp index 210391555..7641472f8 100644 --- a/src/util/decision_engine.cpp +++ b/src/util/decision_engine.cpp @@ -11,8 +11,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief . + ** \brief A decision engine for CVC4 ** + ** A decision engine for CVC4. **/ #include "util/decision_engine.h" diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h index e1d9e21b7..3eee8aeb6 100644 --- a/src/util/decision_engine.h +++ b/src/util/decision_engine.h @@ -11,7 +11,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief A decision engine for CVC4. + ** \brief A decision engine for CVC4 ** ** A decision engine for CVC4. **/ diff --git a/src/util/options.cpp b/src/util/options.cpp index f6d3c3092..1d2e4ed8b 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -79,7 +79,7 @@ string Options::getDescription() const { return optionsDescription; } -void Options::printUsage(const string msg, std::ostream& out) { +void Options::printUsage(const std::string msg, std::ostream& out) { out << msg << optionsDescription << endl << flush; // printf(usage + options.getDescription(), options.binary_name.c_str()); // printf(usage, binary_name.c_str()); diff --git a/src/util/output.cpp b/src/util/output.cpp index 10db4f723..34a3af93e 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -63,7 +63,7 @@ void DebugC::printf(const char* tag, const char* fmt, ...) { } } -void DebugC::printf(string tag, const char* fmt, ...) { +void DebugC::printf(std::string tag, const char* fmt, ...) { if(d_tags.find(tag) != d_tags.end()) { // chop off output after 1024 bytes char buf[1024]; @@ -127,7 +127,7 @@ void TraceC::printf(const char* tag, const char* fmt, ...) { } } -void TraceC::printf(string tag, const char* fmt, ...) { +void TraceC::printf(std::string tag, const char* fmt, ...) { if(d_tags.find(tag) != d_tags.end()) { // chop off output after 1024 bytes char buf[1024]; diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index c675ab6c9..057100d10 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -30,7 +30,7 @@ using namespace CVC4; /* Computes a rational given a decimal string. The rational * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>. */ -Rational Rational::fromDecimal(const string& dec) { +Rational Rational::fromDecimal(const std::string& dec) { // Find the decimal point, if there is one string::size_type i( dec.find(".") ); if( i != string::npos ) { diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp index aad1f8b2d..5921b8fd3 100644 --- a/src/util/rational_gmp_imp.cpp +++ b/src/util/rational_gmp_imp.cpp @@ -30,7 +30,7 @@ using namespace CVC4; /* Computes a rational given a decimal string. The rational * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>. */ -Rational Rational::fromDecimal(const string& dec) { +Rational Rational::fromDecimal(const std::string& dec) { // Find the decimal point, if there is one string::size_type i( dec.find(".") ); if( i != string::npos ) { diff --git a/src/util/result.cpp b/src/util/result.cpp index 9760eaefb..8e1db27c4 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -28,7 +28,7 @@ using namespace std; namespace CVC4 { -Result::Result(const string& instr) : +Result::Result(const std::string& instr) : d_sat(SAT_UNKNOWN), d_validity(VALIDITY_UNKNOWN), d_which(TYPE_NONE), |