Merge branch 'master' into rm_cdvectorrm_cdvector

2 files changed, 91 insertions, 14 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 80af4199b..703c298d3 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1023,5 +1023,74 @@ size_t TermHashFunction::operator()(const Term& t) const
   return ExprHashFunction()(*t.d_expr);
 }
 
+/* -------------------------------------------------------------------------- */
+/* OpTerm                                                                     */
+/* -------------------------------------------------------------------------- */
+
+OpTerm::OpTerm() : d_expr(new CVC4::Expr())
+{
+}
+
+OpTerm::OpTerm(const CVC4::Expr& e) : d_expr(new CVC4::Expr(e))
+{
+}
+
+OpTerm::~OpTerm()
+{
+}
+
+OpTerm& OpTerm::operator=(const OpTerm& t)
+{
+  // CHECK: expr managers must match
+  if (this != &t)
+  {
+    *d_expr = *t.d_expr;
+  }
+  return *this;
+}
+
+bool OpTerm::operator==(const OpTerm& t) const
+{
+  // CHECK: expr managers must match
+  return *d_expr == *t.d_expr;
+}
+
+bool OpTerm::operator!=(const OpTerm& t) const
+{
+  // CHECK: expr managers must match
+  return *d_expr != *t.d_expr;
+}
+
+Kind OpTerm::getKind() const
+{
+  return intToExtKind(d_expr->getKind());
+}
+
+Sort OpTerm::getSort() const
+{
+  return Sort(d_expr->getType());
+}
+
+bool OpTerm::isNull() const
+{
+  return d_expr->isNull();
+}
+
+std::string OpTerm::toString() const
+{
+  return d_expr->toString();
+}
+
+std::ostream& operator<< (std::ostream& out, const OpTerm& t)
+{
+  out << t.toString();
+  return out;
+}
+
+size_t OpTermHashFunction::operator()(const OpTerm& t) const
+{
+  return ExprHashFunction()(*t.d_expr);
+}
+
 }  // namespace api
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index fcd0838ef..c40a7c4d9 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -98,20 +98,28 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) {
   std::map< int, std::map< Node, Node > > visited_cons;
   for( unsigned i=0; i<assertions.size(); i++ ){
     bool is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end();
-    //constant boolean function definitions do not add domain constraints
-    if( !is_fd || ( is_fd && assertions[i][1].getKind()==EQUAL ) ){
-      std::vector< Node > constraints;
-      Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is function definition = " << is_fd << std::endl;
-      Node n = simplifyFormula( assertions[i], true, true, constraints, is_fd ? subs_head[i] : Node::null(), is_fd, visited, visited_cons );
-      Assert( constraints.empty() );
-      if( n!=assertions[i] ){
-        n = Rewriter::rewrite( n );
-        Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << std::endl;
-        Trace("fmf-fun-def-rewrite") << "  to " << std::endl;
-        Trace("fmf-fun-def-rewrite") << "  " << n << std::endl;
-        PROOF( ProofManager::currentPM()->addDependence(n, assertions[i]); );
-        assertions[i] = n;
-      }
+    std::vector<Node> constraints;
+    Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i]
+                                 << ", is function definition = " << is_fd
+                                 << std::endl;
+    Node n = simplifyFormula(assertions[i],
+                             true,
+                             true,
+                             constraints,
+                             is_fd ? subs_head[i] : Node::null(),
+                             is_fd,
+                             visited,
+                             visited_cons);
+    Assert(constraints.empty());
+    if (n != assertions[i])
+    {
+      n = Rewriter::rewrite(n);
+      Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i]
+                                   << std::endl;
+      Trace("fmf-fun-def-rewrite") << "  to " << std::endl;
+      Trace("fmf-fun-def-rewrite") << "  " << n << std::endl;
+      PROOF(ProofManager::currentPM()->addDependence(n, assertions[i]););
+      assertions[i] = n;
     }
   }
 }