From: Gereon Kremer <nafur42@gmail.com>
Date: Thu, 5 Aug 2021 00:29:11 +0000 (-0700)
Subject: No longer call solver constructor with an options object. (#6985)
X-Git-Tag: cvc5-1.0.0~1399
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=183808b608071890b4d8a05d51233fe37a133873;p=cvc5.git

No longer call solver constructor with an options object. (#6985)

This PR removes calls to the Solver constructor with an Options object, and instead uses the setOption() method.
---

diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp
index ee58b7ad4..b96f436c6 100644
--- a/test/api/smt2_compliance.cpp
+++ b/test/api/smt2_compliance.cpp
@@ -35,14 +35,11 @@ void testGetInfo(api::Solver* solver, const char* s);
 
 int main()
 {
-  Options opts;
-  opts.base.inputLanguage = language::input::LANG_SMTLIB_V2;
-  opts.base.outputLanguage = language::output::LANG_SMTLIB_V2;
-
   cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
 
-  std::unique_ptr<api::Solver> solver =
-      std::unique_ptr<api::Solver>(new api::Solver(&opts));
+  std::unique_ptr<api::Solver> solver = std::make_unique<api::Solver>();
+  solver->setOption("input-language", "smtlib2");
+  solver->setOption("output-language", "smtlib2");
   testGetInfo(solver.get(), ":error-behavior");
   testGetInfo(solver.get(), ":name");
   testGetInfo(solver.get(), ":authors");
diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp
index 10bba5e64..8c8ef15d7 100644
--- a/test/unit/parser/parser_black.cpp
+++ b/test/unit/parser/parser_black.cpp
@@ -44,9 +44,9 @@ class TestParserBlackParser : public TestInternal
   void SetUp() override
   {
     TestInternal::SetUp();
-    d_options.base.parseOnly = true;
     d_symman.reset(nullptr);
-    d_solver.reset(new cvc5::api::Solver(&d_options));
+    d_solver.reset(new cvc5::api::Solver());
+    d_solver->setOption("parse-only", "true");
   }
 
   void TearDown() override
@@ -55,13 +55,6 @@ class TestParserBlackParser : public TestInternal
     d_solver.reset(nullptr);
   }
 
-  void setUp()
-  {
-    /* ensure the old symbol manager is deleted */
-    d_symman.reset(nullptr);
-    d_solver.reset(new api::Solver(&d_options));
-  }
-
   /* Set up declaration context for expr inputs */
   void setupContext(Parser& parser)
   {
@@ -87,7 +80,7 @@ class TestParserBlackParser : public TestInternal
   {
     d_symman.reset(new SymbolManager(d_solver.get()));
     std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get())
-                                       .withOptions(d_options)
+                                       .withOptions(d_solver->getOptions())
                                        .withInputLanguage(d_lang)
                                        .build());
     parser->setInput(Input::newStringInput(d_lang, goodInput, "test"));
@@ -106,7 +99,7 @@ class TestParserBlackParser : public TestInternal
   {
     d_symman.reset(new SymbolManager(d_solver.get()));
     std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get())
-                                       .withOptions(d_options)
+                                       .withOptions(d_solver->getOptions())
                                        .withInputLanguage(d_lang)
                                        .withStrictMode(strictMode)
                                        .build());
@@ -128,7 +121,7 @@ class TestParserBlackParser : public TestInternal
   {
     d_symman.reset(new SymbolManager(d_solver.get()));
     std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get())
-                                       .withOptions(d_options)
+                                       .withOptions(d_solver->getOptions())
                                        .withInputLanguage(d_lang)
                                        .build());
     parser->setInput(Input::newStringInput(d_lang, goodExpr, "test"));
@@ -162,7 +155,7 @@ class TestParserBlackParser : public TestInternal
   {
     d_symman.reset(new SymbolManager(d_solver.get()));
     std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get())
-                                       .withOptions(d_options)
+                                       .withOptions(d_solver->getOptions())
                                        .withInputLanguage(d_lang)
                                        .withStrictMode(strictMode)
                                        .build());
@@ -177,7 +170,6 @@ class TestParserBlackParser : public TestInternal
                  , ParserException);
   }
 
-  Options d_options;
   InputLanguage d_lang;
   std::unique_ptr<cvc5::api::Solver> d_solver;
   std::unique_ptr<SymbolManager> d_symman;