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 ee58b7ad48a01ed858ce59f479d143e77dd9b42a..b96f436c6a6d7c106994f4bd0430114b3224720c 100644 (file)
--- 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 10bba5e6457371ee2fbd24d20c36be34b337660d..8c8ef15d7e90f6ad898b75cd6c940d7755c869c1 100644 (file)
--- 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;