diff options
| author | Cristian Cadar <cristic@cs.stanford.edu> | 2009-07-10 22:10:54 +0000 |
|---|---|---|
| committer | Cristian Cadar <cristic@cs.stanford.edu> | 2009-07-10 22:10:54 +0000 |
| commit | 6c7d0d1db055bfca93b962de1cd2eaa5f1d3c8dd (patch) | |
| tree | aa73c2bf3ca3bffdd7ff2a3e681b919de7e9b246 /lib/SMT/SMTParser.h | |
| parent | 3951254da613913829b2419b05cb7c3758570e98 (diff) | |
| download | klee-6c7d0d1db055bfca93b962de1cd2eaa5f1d3c8dd.tar.gz | |
Added support for not, zero_extend, and sign_extend to the SMTLIB parser.
Added support for n-ary and, or and xor. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75299 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'lib/SMT/SMTParser.h')
| -rw-r--r-- | lib/SMT/SMTParser.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h index bae4a23f..3d64a9b2 100644 --- a/lib/SMT/SMTParser.h +++ b/lib/SMT/SMTParser.h @@ -60,6 +60,10 @@ class SMTParser : public klee::expr::Parser { void DeclareExpr(std::string name, Expr::Width w); + ExprHandle CreateAnd(std::vector<ExprHandle>); + ExprHandle CreateOr(std::vector<ExprHandle>); + ExprHandle CreateXor(std::vector<ExprHandle>); + typedef std::map<const std::string, ExprHandle> VarEnv; typedef std::map<const std::string, ExprHandle> FVarEnv; |