diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-01 09:56:14 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-01 16:56:14 +0000 |
commit | 05a53a2ac405bcd18a84024247145f161809c3b0 (patch) | |
tree | 34241c0a82f79d717ddbfbb0c294f9a09c7edb0c /examples | |
parent | afaf4413775ff7d6054a5893f1397ad908e0773c (diff) |
Rename namespace CVC5 to cvc5. (#6258)
Diffstat (limited to 'examples')
28 files changed, 56 insertions, 56 deletions
diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index 1cbfdb031..043bbf8aa 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -19,7 +19,7 @@ #include <cvc4/api/cvc4cpp.h> using namespace std; -using namespace CVC5::api; +using namespace cvc5::api; int main() { diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/bitvectors_and_arrays.cpp index 5c243e1d1..2bca1eb4c 100644 --- a/examples/api/bitvectors_and_arrays.cpp +++ b/examples/api/bitvectors_and_arrays.cpp @@ -20,7 +20,7 @@ #include <cvc4/api/cvc4cpp.h> using namespace std; -using namespace CVC5::api; +using namespace cvc5::api; int main() { diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp index 2651bf80f..9ea2f55ed 100644 --- a/examples/api/combination.cpp +++ b/examples/api/combination.cpp @@ -21,7 +21,7 @@ #include <cvc4/api/cvc4cpp.h> using namespace std; -using namespace CVC5::api; +using namespace cvc5::api; void prefixPrintGetValue(Solver& slv, Term t, int level = 0) { diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp index c2b3bc4c4..49253e466 100644 --- a/examples/api/datatypes.cpp +++ b/examples/api/datatypes.cpp @@ -18,7 +18,7 @@ #include <cvc4/api/cvc4cpp.h> -using namespace CVC5::api; +using namespace cvc5::api; void test(Solver& slv, Sort& consListSort) { diff --git a/examples/api/extract.cpp b/examples/api/extract.cpp index a6a43a7c2..760f5d0fe 100644 --- a/examples/api/extract.cpp +++ b/examples/api/extract.cpp @@ -19,7 +19,7 @@ #include <cvc4/api/cvc4cpp.h> using namespace std; -using namespace CVC5::api; +using namespace cvc5::api; int main() { diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp index 89b0e212d..092e2a79a 100644 --- a/examples/api/helloworld.cpp +++ b/examples/api/helloworld.cpp @@ -18,7 +18,7 @@ #include <cvc4/api/cvc4cpp.h> -using namespace CVC5::api; +using namespace cvc5::api; int main() { diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp index ca3e8a2b9..b56982daa 100644 --- a/examples/api/linear_arith.cpp +++ b/examples/api/linear_arith.cpp @@ -20,7 +20,7 @@ #include "cvc4/api/cvc4cpp.h" using namespace std; -using namespace CVC5::api; +using namespace cvc5::api; int main() { diff --git a/examples/api/sequences.cpp b/examples/api/sequences.cpp index 6272b423b..3498b3275 100644 --- a/examples/api/sequences.cpp +++ b/examples/api/sequences.cpp @@ -18,7 +18,7 @@ #include <iostream> -using namespace CVC5::api; +using namespace cvc5::api; int main() { diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp index cac705415..59385896c 100644 --- a/examples/api/sets.cpp +++ b/examples/api/sets.cpp @@ -19,7 +19,7 @@ #include <cvc4/api/cvc4cpp.h> using namespace std; -using namespace CVC5::api; +using namespace cvc5::api; int main() { diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp index b926395de..53352d266 100644 --- a/examples/api/strings.cpp +++ b/examples/api/strings.cpp @@ -18,7 +18,7 @@ #include <cvc4/api/cvc4cpp.h> -using namespace CVC5::api; +using namespace cvc5::api; int main() { diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp index a29cdb132..be4d3e8d5 100644 --- a/examples/api/sygus-fun.cpp +++ b/examples/api/sygus-fun.cpp @@ -49,7 +49,7 @@ #include <iostream> -using namespace CVC5::api; +using namespace cvc5::api; int main() { diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp index 6491dc0a5..61b00f6de 100644 --- a/examples/api/sygus-grammar.cpp +++ b/examples/api/sygus-grammar.cpp @@ -46,7 +46,7 @@ #include <iostream> -using namespace CVC5::api; +using namespace cvc5::api; int main() { diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp index 206803eb6..56b5a0aaa 100644 --- a/examples/api/sygus-inv.cpp +++ b/examples/api/sygus-inv.cpp @@ -37,7 +37,7 @@ #include <iostream> -using namespace CVC5::api; +using namespace cvc5::api; int main() { diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp index 6fa7954ea..0545ce048 100644 --- a/examples/hashsmt/sha1_collision.cpp +++ b/examples/hashsmt/sha1_collision.cpp @@ -34,7 +34,7 @@ #include "word.h" using namespace std; -using namespace CVC5; +using namespace cvc5; hashsmt::cvc4_uchar8 *createInput(unsigned size, std::string prefix, std::ostream& output) { hashsmt::cvc4_uchar8 *input = new hashsmt::cvc4_uchar8[size]; @@ -102,7 +102,7 @@ int main(int argc, char* argv[]) { delete[] cvc4input1; delete[] cvc4input2; } - catch (CVC5::Exception& e) + catch (cvc5::Exception& e) { cerr << e << endl; } diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp index 957f9225e..a4acfc3c6 100644 --- a/examples/hashsmt/sha1_inversion.cpp +++ b/examples/hashsmt/sha1_inversion.cpp @@ -43,7 +43,7 @@ #include "word.h" using namespace std; -using namespace CVC5; +using namespace cvc5; int main(int argc, char* argv[]) { @@ -105,7 +105,7 @@ int main(int argc, char* argv[]) { // Checksat command output << CheckSatCommand() << endl; } - catch (CVC5::Exception& e) + catch (cvc5::Exception& e) { cerr << e << endl; } diff --git a/examples/hashsmt/word.cpp b/examples/hashsmt/word.cpp index 5fd5b7979..79b868d1c 100644 --- a/examples/hashsmt/word.cpp +++ b/examples/hashsmt/word.cpp @@ -33,8 +33,8 @@ using namespace std; using namespace hashsmt; -using namespace CVC5; -using namespace CVC5::options; +using namespace cvc5; +using namespace cvc5::options; Expr Word::extendToSize(unsigned newSize) const { if (newSize <= size()) { @@ -50,10 +50,10 @@ ExprManager* Word::s_manager = 0; ExprManager* Word::em() { if (s_manager == 0) { - CVC5::Options options; + cvc5::Options options; options.setInputLanguage(language::input::LANG_SMTLIB_V2); options.setOutputLanguage(language::output::LANG_SMTLIB_V2); - s_manager = new CVC5::ExprManager(options); + s_manager = new cvc5::ExprManager(options); } return s_manager; } @@ -71,7 +71,7 @@ Word Word::concat(const Word words[], unsigned size) { } void Word::print(ostream& out) const { - out << CVC5::expr::ExprSetDepth(-1) << d_expr; + out << cvc5::expr::ExprSetDepth(-1) << d_expr; } Word::Word(unsigned newSize, unsigned value) { diff --git a/examples/hashsmt/word.h b/examples/hashsmt/word.h index 4a1d142f4..f5b95ba32 100644 --- a/examples/hashsmt/word.h +++ b/examples/hashsmt/word.h @@ -35,20 +35,20 @@ namespace hashsmt { class Word { /** Expression managaer we're using for all word expressions */ - static CVC5::ExprManager* s_manager; + static cvc5::ExprManager* s_manager; protected: /** The expression of this word */ - CVC5::Expr d_expr; + cvc5::Expr d_expr; /** Get the expression manager words are using */ - static CVC5::ExprManager* em(); + static cvc5::ExprManager* em(); - Word(CVC5::Expr expr = CVC5::Expr()) : d_expr(expr) {} + Word(cvc5::Expr expr = cvc5::Expr()) : d_expr(expr) {} /** Extend the representing expression to the given size >= size() */ - CVC5::Expr extendToSize(unsigned size) const; + cvc5::Expr extendToSize(unsigned size) const; public: @@ -70,10 +70,10 @@ class Word { void print(std::ostream& out) const; - CVC5::Expr getExpr() const { return d_expr; } + cvc5::Expr getExpr() const { return d_expr; } /** Returns the comparison expression */ - CVC5::Expr operator==(const Word& b) const; + cvc5::Expr operator==(const Word& b) const; /** Concatenate the given words */ static Word concat(const Word words[], unsigned size); diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp index daa7d920d..ba495e1fd 100644 --- a/examples/nra-translate/normalize.cpp +++ b/examples/nra-translate/normalize.cpp @@ -28,9 +28,9 @@ #include <cvc4/options/set_language.h> using namespace std; -using namespace CVC5; -using namespace CVC5::parser; -using namespace CVC5::theory; +using namespace cvc5; +using namespace cvc5::parser; +using namespace cvc5::theory; int main(int argc, char* argv[]) { diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp index 661747ab0..1eb4b3d4d 100644 --- a/examples/nra-translate/smt2info.cpp +++ b/examples/nra-translate/smt2info.cpp @@ -25,9 +25,9 @@ #include <cvc4/cvc4.h> using namespace std; -using namespace CVC5; -using namespace CVC5::parser; -using namespace CVC5::options; +using namespace cvc5; +using namespace cvc5::parser; +using namespace cvc5::options; unsigned compute_degree(ExprManager& exprManager, const Expr& term) { unsigned n = term.getNumChildren(); diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp index 2a12b828e..8139a4d91 100644 --- a/examples/nra-translate/smt2todreal.cpp +++ b/examples/nra-translate/smt2todreal.cpp @@ -28,9 +28,9 @@ #include <cvc4/options/set_language.h> using namespace std; -using namespace CVC5; -using namespace CVC5::parser; -using namespace CVC5::options; +using namespace cvc5; +using namespace cvc5::parser; +using namespace cvc5::options; int main(int argc, char* argv[]) { diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp index aecdf5ba2..09b0c69d8 100644 --- a/examples/nra-translate/smt2toisat.cpp +++ b/examples/nra-translate/smt2toisat.cpp @@ -26,9 +26,9 @@ #include <cvc4/cvc4.h> using namespace std; -using namespace CVC5; -using namespace CVC5::parser; -using namespace CVC5::options; +using namespace cvc5; +using namespace cvc5::parser; +using namespace cvc5::options; void translate_to_isat( string input, diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp index 02795dc1f..6cb51f17c 100644 --- a/examples/nra-translate/smt2tomathematica.cpp +++ b/examples/nra-translate/smt2tomathematica.cpp @@ -26,8 +26,8 @@ #include <cvc4/cvc4.h> using namespace std; -using namespace CVC5; -using namespace CVC5::parser; +using namespace cvc5; +using namespace cvc5::parser; void translate_to_mathematica( string input, diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp index 1bfe9424b..afd468d5d 100644 --- a/examples/nra-translate/smt2toqepcad.cpp +++ b/examples/nra-translate/smt2toqepcad.cpp @@ -26,8 +26,8 @@ #include <cvc4/cvc4.h> using namespace std; -using namespace CVC5; -using namespace CVC5::parser; +using namespace cvc5; +using namespace cvc5::parser; void translate_to_qepcad( string input, diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp index 4238e9f13..d9bd6012a 100644 --- a/examples/nra-translate/smt2toredlog.cpp +++ b/examples/nra-translate/smt2toredlog.cpp @@ -26,9 +26,9 @@ #include <cvc4/cvc4.h> using namespace std; -using namespace CVC5; -using namespace CVC5::parser; -using namespace CVC5::options; +using namespace cvc5; +using namespace cvc5::parser; +using namespace cvc5::options; void translate_to_redlog( string input, diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp index b9ced3d79..ec95b5f70 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/examples/sets-translate/sets_translate.cpp @@ -28,9 +28,9 @@ #include <cvc4/options/set_language.h> using namespace std; -using namespace CVC5; -using namespace CVC5::parser; -using namespace CVC5::options; +using namespace cvc5; +using namespace cvc5::parser; +using namespace cvc5::options; bool nonsense(char c) { return !isalnum(c); } diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index b6890e6ef..b97b86bb8 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -20,7 +20,7 @@ #include <iostream> -using namespace CVC5::api; +using namespace cvc5::api; int main() { Solver slv; diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp index e6778fa41..73dbfe34f 100644 --- a/examples/simple_vc_quant_cxx.cpp +++ b/examples/simple_vc_quant_cxx.cpp @@ -18,7 +18,7 @@ #include <iostream> -using namespace CVC5::api; +using namespace cvc5::api; int main() { Solver slv; diff --git a/examples/translator.cpp b/examples/translator.cpp index 1a9de7f80..4838e06fb 100644 --- a/examples/translator.cpp +++ b/examples/translator.cpp @@ -28,9 +28,9 @@ #include <cvc4/options/set_language.h> using namespace std; -using namespace CVC5; -using namespace CVC5::language; -using namespace CVC5::parser; +using namespace cvc5; +using namespace cvc5::language; +using namespace cvc5::parser; enum { INPUT_LANG = 'L', |