From fad7a9aafa35210bb8b685261ec1caae2c7e0624 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 4 Jul 2018 00:21:01 -0500
Subject: [PATCH] Fix fmf-fun for non-equality function definitions (#2134)

Fixes #2133. In that issue, a quantifiers rewrite triggered a model-unsoundness in fmf-fun. The rewrite made a function definition have an ITE at top-level instead of equality. The corrected code was model-unsound, since it assumed that quantified formulas that are not EQUAL can be ignored.
---
 src/theory/quantifiers/fun_def_process.cpp | 36 +++++++++++++---------
 1 file changed, 22 insertions(+), 14 deletions(-)

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;
     }
   }
 }
-- 
2.30.2