From 3fc001baeafa6bf57be781e59bc1d9276ef3ca0c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 29 Apr 2020 10:15:54 -0700
Subject: [PATCH] simplifications noticed by trying #4147

The change masks possible bugs in smt.threads and arrays.
---
 src/smt/seq_axioms.cpp                        |  9 ++++----
 src/smt/smt_parallel.cpp                      |  2 +-
 src/smt/tactic/ctx_solver_simplify_tactic.cpp | 21 ++++++++++++++++---
 src/tactic/core/distribute_forall_tactic.cpp  |  3 ++-
 4 files changed, 25 insertions(+), 10 deletions(-)

diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp
index a751df7aa..8f24cb528 100644
--- a/src/smt/seq_axioms.cpp
+++ b/src/smt/seq_axioms.cpp
@@ -563,16 +563,15 @@ void seq_axioms::add_itos_axiom(expr* e) {
 /**
    stoi(s) >= -1
    stoi("") = -1
-   stoi(s) >= 0 => len(s) > 0
    stoi(s) >= 0 => is_digit(nth(s,0))
 */
 void seq_axioms::add_stoi_axiom(expr* e) {
     TRACE("seq", tout << mk_pp(e, m) << "\n";);
+    literal ge0 = mk_ge(e, 0);      
     expr* s = nullptr;
     VERIFY (seq.str.is_stoi(e, s));    
     add_axiom(mk_ge(e, -1));                             // stoi(s) >= -1
     add_axiom(~mk_eq_empty(s), mk_eq(e, a.mk_int(-1)));  // s = "" => stoi(s) = -1
-    literal ge0 = mk_ge(e, 0);      
     add_axiom(~ge0, is_digit(mk_nth(s, 0)));             // stoi(s) >= 0 => is_digit(nth(s,0))
 
 }
@@ -614,9 +613,9 @@ void seq_axioms::add_stoi_axiom(expr* e, unsigned k) {
     expr_ref len = mk_len(s);
     literal ge0 = mk_ge(e, 0);
     literal lek = mk_le(len, k);
-    add_axiom(~lek, mk_eq(e, stoi2(k-1)));                                          // len(s) <= k  => stoi(s) = stoi(s, k-1)
-    add_axiom(mk_le(len, 0), ~is_digit_(0), mk_eq(stoi2(0), digit(0)));             // len(s) > 0, is_digit(nth(s, 0)) => stoi(s,0) = digit(s,0)
-    add_axiom(mk_le(len, 0), is_digit_(0),  mk_eq(stoi2(0), a.mk_int(-1)));         // len(s) > 0, ~is_digit(nth(s, 0)) => stoi(s,0) = -1
+    add_axiom(~lek, mk_eq(e, stoi2(k-1)));                                    // len(s) <= k  => stoi(s) = stoi(s, k-1)
+    add_axiom(mk_le(len, 0), ~is_digit_(0), mk_eq(stoi2(0), digit(0)));       // len(s) > 0, is_digit(nth(s, 0)) => stoi(s,0) = digit(s,0)
+    add_axiom(mk_le(len, 0), is_digit_(0),  mk_eq(stoi2(0), a.mk_int(-1)));   // len(s) > 0, ~is_digit(nth(s, 0)) => stoi(s,0) = -1
     for (unsigned i = 1; i < k; ++i) {
 
         // len(s) <= i => stoi(s, i) = stoi(s, i - 1)
diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index d4f3af840..0b5afcae5 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -183,7 +183,7 @@ namespace smt {
             }
         };
 
-        // for debugging: num_threads = 1;
+        // for debugging:  num_threads = 1;
 
         while (true) {
             vector<std::thread> threads(num_threads);
diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
index f0df5b949..e16f8d921 100644
--- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp
+++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
@@ -15,6 +15,16 @@ Author:
 
 Notes:
 
+Implement the inference rule
+
+     n = V |- F[n] = F[x]
+     --------------------
+         F[x] = F[V]
+
+where n is an uninterpreted variable (fresh for F[x])
+and V is a value (true or false) and x is a subterm 
+(different from V).
+
 --*/
 
 #include "smt/tactic/ctx_solver_simplify_tactic.h"
@@ -184,9 +194,14 @@ protected:
             if (cache.contains(e)) {
                 goto done;
             }
+            if (m.is_true(e) || m.is_false(e)) {
+                res = e;
+                goto done;
+            }
             if (m.is_bool(e) && simplify_bool(n, res)) {
-                TRACE("ctx_solver_simplify_tactic", 
-                      tout << "simplified: " << mk_pp(e, m) << " |-> " << mk_pp(res, m) << "\n";);
+                TRACE("ctx_solver_simplify_tactic",
+                    m_solver.display(tout) << "\n";
+                      tout << "simplified: " << mk_pp(n, m) << "\n" << mk_pp(e, m) << " |-> " << mk_pp(res, m) << "\n";);
                 goto done;
             }
             if (!is_app(e)) {
@@ -214,7 +229,7 @@ protected:
                         args.push_back(arg);
                     }
                 }
-                else if (!n2) {
+                else if (!n2 && !m.is_value(arg)) {
                     n2 = mk_fresh(id, m.get_sort(arg));
                     trail.push_back(n2);
                     todo.push_back(expr_pos(self_pos, ++child_id, i, arg));
diff --git a/src/tactic/core/distribute_forall_tactic.cpp b/src/tactic/core/distribute_forall_tactic.cpp
index aa1ef07c8..cbf1b019b 100644
--- a/src/tactic/core/distribute_forall_tactic.cpp
+++ b/src/tactic/core/distribute_forall_tactic.cpp
@@ -15,6 +15,7 @@ Author:
 
 --*/
 #include "tactic/tactical.h"
+#include "ast/ast_util.h"
 #include "ast/rewriter/rewriter_def.h"
 #include "ast/rewriter/var_subst.h"
 
@@ -46,7 +47,7 @@ class distribute_forall_tactic : public tactic {
                 expr_ref_buffer new_args(m);
                 for (unsigned i = 0; i < num_args; i++) {
                     expr * arg     = or_e->get_arg(i);
-                    expr * not_arg = m.mk_not(arg);
+                    expr * not_arg = mk_not(m, arg);
                     quantifier_ref tmp_q(m);
                     tmp_q = m.update_quantifier(old_q, not_arg);
                     new_args.push_back(elim_unused_vars(m, tmp_q, params_ref()));