diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-24 23:23:34 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-24 23:23:34 +0000 |
commit | 80afd586eb0865efcc38aa14833d682f1b7cc27f (patch) | |
tree | aac37b28e0330bf3b72083e979ae94ee71918771 /src/compat/cvc3_compat.cpp | |
parent | 3619c784bd5dd4b91ab0a2ad429ea145636d3424 (diff) |
* disallow internal uses of mkVar() (you have to mkSkolem())
* add support for mkBoundVar() (BOUND_VAR_LISTs in quantifiers must be bound vars)
Diffstat (limited to 'src/compat/cvc3_compat.cpp')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index afac925e2..62885f55f 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -330,7 +330,7 @@ bool Expr::isString() const { } bool Expr::isBoundVar() const { - Unimplemented(); + return getKind() == CVC4::kind::BOUND_VARIABLE; } bool Expr::isLambda() const { @@ -1857,7 +1857,7 @@ Expr ValidityChecker::datatypeTestExpr(const std::string& constructor, const Exp Expr ValidityChecker::boundVarExpr(const std::string& name, const std::string& uid, const Type& type) { - Unimplemented("Quantifiers not supported by CVC4 yet (sorry!)"); + return d_em->mkBoundVar(name, type); } Expr ValidityChecker::forallExpr(const std::vector<Expr>& vars, const Expr& body) { |