diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-03-03 04:28:45 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-03 10:28:45 +0000 |
| commit | 6db84f6e373f9651af48df7b654e3992f68472ac (patch) | |
| tree | 3c146a185ce575431ea7a63cf97a8e0bb1031c0b /test/unit/theory | |
| parent | c4709cb01356dd73fdd767d19af85b36ffd566c4 (diff) | |
Remove uses of SExpr class. (#6035)
This PR is a step towards removing SExpr class. It replaces SExpr with std::string for set-info and set-option commands.
Diffstat (limited to 'test/unit/theory')
| -rw-r--r-- | test/unit/theory/theory_arith_white.cpp | 2 | ||||
| -rw-r--r-- | test/unit/theory/theory_bv_white.cpp | 6 | ||||
| -rw-r--r-- | test/unit/theory/theory_quantifiers_bv_inverter_white.cpp | 4 |
3 files changed, 6 insertions, 6 deletions
diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp index 5e5b52d3e..4c8834c8d 100644 --- a/test/unit/theory/theory_arith_white.cpp +++ b/test/unit/theory/theory_arith_white.cpp @@ -41,7 +41,7 @@ class TestTheoryWhiteArith : public TestSmtNoFinishInit void SetUp() override { TestSmtNoFinishInit::SetUp(); - d_smtEngine->setOption("incremental", CVC4::SExpr(false)); + d_smtEngine->setOption("incremental", "false"); d_smtEngine->finishInit(); d_context = d_smtEngine->getContext(); d_user_context = d_smtEngine->getUserContext(); diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp index c07f2c402..976724c8e 100644 --- a/test/unit/theory/theory_bv_white.cpp +++ b/test/unit/theory/theory_bv_white.cpp @@ -43,8 +43,8 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core) { d_smtEngine->setLogic("QF_BV"); - d_smtEngine->setOption("bitblast", SExpr("eager")); - d_smtEngine->setOption("incremental", SExpr("false")); + d_smtEngine->setOption("bitblast", "eager"); + d_smtEngine->setOption("incremental", "false"); // Notice that this unit test uses the theory engine of a created SMT // engine d_smtEngine. We must ensure that d_smtEngine is properly initialized // via the following call, which constructs its underlying theory engine. @@ -72,7 +72,7 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core) TEST_F(TestTheoryWhiteBv, mkUmulo) { - d_smtEngine->setOption("incremental", SExpr("true")); + d_smtEngine->setOption("incremental", "true"); for (uint32_t w = 1; w < 16; ++w) { d_smtEngine->push(); diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp index 5c222d2c1..b5996a684 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp @@ -35,8 +35,8 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit void SetUp() override { TestSmtNoFinishInit::SetUp(); - d_smtEngine->setOption("cegqi-full", CVC4::SExpr(true)); - d_smtEngine->setOption("produce-models", CVC4::SExpr(true)); + d_smtEngine->setOption("cegqi-full", "true"); + d_smtEngine->setOption("produce-models", "true"); d_smtEngine->finishInit(); d_s = d_nodeManager->mkVar("s", d_nodeManager->mkBitVectorType(4)); |