diff options
author | François Bobot <francois@bobot.eu> | 2012-06-22 15:11:11 +0000 |
---|---|---|
committer | François Bobot <francois@bobot.eu> | 2012-06-22 15:11:11 +0000 |
commit | dbd59549e5e48118fdac71048de0a37059c1d5a1 (patch) | |
tree | 5f85b0c8382605cf48cd783fdfffbb34158fe9a9 /src/parser/parser.h | |
parent | eaa2d2f4311ed2830011835ab9b21ad54f0560f6 (diff) |
Parser: add the possibility to bind at level 0.
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r-- | src/parser/parser.h | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index a3ddba013..635dd6b6c 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -337,16 +337,19 @@ public: Type getType(const std::string& var_name, SymbolType type = SYM_VARIABLE); /** Create a new CVC4 variable expression of the given type. */ - Expr mkVar(const std::string& name, const Type& type); + Expr mkVar(const std::string& name, const Type& type, + bool levelZero = false); /** * Create a set of new CVC4 variable expressions of the given type. */ std::vector<Expr> - mkVars(const std::vector<std::string> names, const Type& type); + mkVars(const std::vector<std::string> names, const Type& type, + bool levelZero = false); /** Create a new CVC4 function expression of the given type. */ - Expr mkFunction(const std::string& name, const Type& type); + Expr mkFunction(const std::string& name, const Type& type, + bool levelZero = false); /** * Create a new CVC4 function expression of the given type, @@ -356,10 +359,12 @@ public: Expr mkAnonymousFunction(const std::string& prefix, const Type& type); /** Create a new variable definition (e.g., from a let binding). */ - void defineVar(const std::string& name, const Expr& val); + void defineVar(const std::string& name, const Expr& val, + bool levelZero = false); /** Create a new function definition (e.g., from a define-fun). */ - void defineFunction(const std::string& name, const Expr& val); + void defineFunction(const std::string& name, const Expr& val, + bool levelZero = false); /** Create a new type definition. */ void defineType(const std::string& name, const Type& type); @@ -432,7 +437,8 @@ public: /** * Preempt the next returned command with other ones; used to * support the :named attribute in SMT-LIBv2, which implicitly - * inserts a new command before the current one. + * inserts a new command before the current one. Also used in TPTP + * because function and predicate symbols are implicitly declared. */ void preemptCommand(Command* cmd); |