diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-09-22 22:12:17 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-22 22:12:17 -0500 |
| commit | 5c062833d435e3dde5db3a8223c379a3e8cca520 (patch) | |
| tree | 6be788d43297565e4a7bc769b45ec54930abb8df /test | |
| parent | 56f2e6dc41fa5fbeff1755978fa1854e800846b5 (diff) | |
Refactor Commands to use the Public API. (#5105)
This is work towards eliminating the Expr layer. This PR does the following:
Replace Expr/Type with Term/Sort in the API for commands.
Remove the command export functionality which is not supported.
Since many commands now call the Solver functions instead of the SmtEngine ones, their behavior may be a slightly different. For example, (get-unsat-assumptions) now only works in incremental mode. In some cases, CVC4 will not recover from non-fatal errors.
Diffstat (limited to 'test')
| -rw-r--r-- | test/api/smt2_compliance.cpp | 2 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/regress/regress0/smtlib/get-unsat-assumptions.smt2 | 1 |
3 files changed, 4 insertions, 2 deletions
diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp index 6f474e24f..e5781cfaa 100644 --- a/test/api/smt2_compliance.cpp +++ b/test/api/smt2_compliance.cpp @@ -68,7 +68,7 @@ void testGetInfo(api::Solver* solver, const char* s) assert(c != NULL); cout << c << endl; stringstream ss; - c->invoke(solver->getSmtEngine(), ss); + c->invoke(solver, ss); assert(p->nextCommand() == NULL); delete p; delete c; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 40a5e5ded..d118690ed 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1390,7 +1390,6 @@ set(regress_1_tests regress1/ho/issue4092-sinf.smt2 regress1/ho/issue4134-sinf.smt2 regress1/ho/nested_lambdas-AGT034^2.smt2 - regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 regress1/ho/NUM638^1.smt2 regress1/ho/NUM925^1.p regress1/ho/soundness_fmf_SYO362^5-delta.p @@ -2491,6 +2490,8 @@ set(regression_disabled_tests regress1/crash_burn_locusts.smt2 # regress1/ho/hoa0102.smt2 results in an assertion failure (see issue #1650). regress1/ho/hoa0102.smt2 + # unknown after update to commands + regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 # issue1048-arrays-int-real.smt2 -- different errors on debug and production. regress1/issue1048-arrays-int-real.smt2 # times out after update to tangent planes diff --git a/test/regress/regress0/smtlib/get-unsat-assumptions.smt2 b/test/regress/regress0/smtlib/get-unsat-assumptions.smt2 index 7a8113d8f..ba53610b3 100644 --- a/test/regress/regress0/smtlib/get-unsat-assumptions.smt2 +++ b/test/regress/regress0/smtlib/get-unsat-assumptions.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --incremental ; EXPECT: unsat ; EXPECT: (x x) ; SCRUBBER: sed -e 's/a[1-2]/x/g' |