diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2017-12-06 04:45:06 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-06 06:45:06 -0600 |
commit | 6a37fd136eea6ad95aae4e598faee0d47c110343 (patch) | |
tree | fb6d016a14cded96e6b05d988f3c7856100dc71b /test/system | |
parent | 108b5ed9d1f66884af7ede96155670bb1dc2fb43 (diff) |
Remove CDChunkList (#1414)
Diffstat (limited to 'test/system')
-rw-r--r-- | test/system/Makefile.am | 1 | ||||
-rw-r--r-- | test/system/reset_assertions.cpp | 53 |
2 files changed, 54 insertions, 0 deletions
diff --git a/test/system/Makefile.am b/test/system/Makefile.am index 55a6c2b09..1be242e3d 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -3,6 +3,7 @@ TEST_EXTENSIONS = .class CPLUSPLUS_TESTS = \ boilerplate \ ouroborous \ + reset_assertions \ two_smt_engines \ smt2_compliance \ statistics diff --git a/test/system/reset_assertions.cpp b/test/system/reset_assertions.cpp new file mode 100644 index 000000000..4fed06698 --- /dev/null +++ b/test/system/reset_assertions.cpp @@ -0,0 +1,53 @@ +/********************* */ +/*! \file reset_assertions.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A simple test for SmtEngine::resetAssertions() + ** + ** This program indirectly also tests some corner cases w.r.t. + ** context-dependent datastructures: resetAssertions() pops the contexts to + ** zero but some context-dependent datastructures are created at leevel 1, + ** which the datastructure needs to handle properly problematic. + **/ + +#include <iostream> +#include <sstream> + +#include "expr/expr.h" +#include "smt/smt_engine.h" + +using namespace CVC4; + +int main() +{ + ExprManager em; + SmtEngine smt(&em); + + smt.setOption("incremental", SExpr(true)); + + Type real = em.realType(); + Expr x = em.mkVar("x", real); + Expr four = em.mkConst(Rational(4)); + Expr xEqFour = em.mkExpr(Kind::EQUAL, x, four); + smt.assertFormula(xEqFour); + std::cout << smt.checkSat() << std::endl; + + smt.resetAssertions(); + + Type elementType = em.integerType(); + Type indexType = em.integerType(); + Type arrayType = em.mkArrayType(indexType, elementType); + Expr array = em.mkVar("array", arrayType); + Expr arrayAtFour = em.mkExpr(Kind::SELECT, array, four); + Expr ten = em.mkConst(Rational(10)); + Expr arrayAtFour_eq_ten = em.mkExpr(Kind::EQUAL, arrayAtFour, ten); + smt.assertFormula(arrayAtFour_eq_ten); + std::cout << smt.checkSat() << std::endl; +} |