diff options
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 00336a1e3..e9cb56b88 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -136,6 +136,10 @@ class TheoryEngine { } NodeBuilder<> b(in.getKind()); + if(in.getMetaKind() == kind::metakind::PARAMETERIZED){ + Assert(in.hasOperator()); + b << in.getOperator(); + } for(TNode::iterator c = in.begin(); c != in.end(); ++c) { b << rewrite(*c); } @@ -168,6 +172,8 @@ class TheoryEngine { } } + Node removeITEs(TNode t); + public: /** @@ -220,7 +226,14 @@ public: Assert(k >= 0 && k < kind::LAST_KIND); if(k == kind::VARIABLE) { - return &d_uf; + TypeNode t = n.getType(); + if(t.isBoolean()){ + return &d_bool; + }else if(t.isReal()){ + return &d_arith; + }else{ + return &d_uf; + } //Unimplemented(); } else if(k == kind::EQUAL) { // if LHS is a VARIABLE, use theoryOf(LHS.getType()) |