diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-15 13:30:05 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-15 13:30:05 -0400 |
commit | 5617905a03c6810978cc66a18a370f5a95b7c5b4 (patch) | |
tree | be7056c33d500449d59e6de585fd93b5db860311 /src/smt/boolean_terms.h | |
parent | a485a56258bdac2cdb2214dbcae5268b11f1d95b (diff) |
Boolean terms rewriting for quantified variables of type Bool, when quantifier body uses them in term context
Diffstat (limited to 'src/smt/boolean_terms.h')
-rw-r--r-- | src/smt/boolean_terms.h | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h index e51a7bbb0..c53eadfa0 100644 --- a/src/smt/boolean_terms.h +++ b/src/smt/boolean_terms.h @@ -24,6 +24,7 @@ #include "expr/attribute.h" #include "expr/node.h" #include "util/hash.h" +#include <map> #include <utility> namespace CVC4 { @@ -52,6 +53,8 @@ class BooleanTermConverter { */ const Datatype& booleanTermsConvertDatatype(const Datatype& dt) throw(); + Node rewriteBooleanTermsRec(TNode n, bool boolParent, std::map<TNode, Node>& quantBoolVars) throw(); + public: BooleanTermConverter(SmtEngine& smt) : @@ -61,7 +64,10 @@ public: /** * We rewrite Boolean terms in assertions as bitvectors of length 1. */ - Node rewriteBooleanTerms(TNode n, bool boolParent = true) throw(); + Node rewriteBooleanTerms(TNode n, bool boolParent = true) throw() { + std::map<TNode, Node> quantBoolVars; + return rewriteBooleanTermsRec(n, boolParent, quantBoolVars); + } };/* class BooleanTermConverter */ |