From 05158b3914fb76769d4c9692e79e77844fb5ae26 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 27 Feb 2020 21:11:07 -0800
Subject: [PATCH] add cut redundancies

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_config.cpp         |  1 +
 src/sat/sat_config.h           |  1 +
 src/sat/sat_cut_simplifier.cpp | 14 ++++++++------
 src/sat/sat_params.pyg         |  1 +
 4 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 5772e1030..7b984cd62 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -111,6 +111,7 @@ namespace sat {
         m_cut_xor           = p.cut_xor();
         m_cut_npn3          = p.cut_npn3();
         m_cut_dont_cares    = p.cut_dont_cares();
+        m_cut_redundancies  = p.cut_redundancies();
         m_cut_force         = p.cut_force();
         m_lookahead_simplify = p.lookahead_simplify();
         m_lookahead_double = p.lookahead_double();
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index bd47171f8..38bbfb00e 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -128,6 +128,7 @@ namespace sat {
         bool               m_cut_xor;
         bool               m_cut_npn3;
         bool               m_cut_dont_cares;
+        bool               m_cut_redundancies;
         bool               m_cut_force;
         bool               m_anf_simplify;
         unsigned           m_anf_delay;
diff --git a/src/sat/sat_cut_simplifier.cpp b/src/sat/sat_cut_simplifier.cpp
index 9ed5976cf..68255afb0 100644
--- a/src/sat/sat_cut_simplifier.cpp
+++ b/src/sat/sat_cut_simplifier.cpp
@@ -599,12 +599,14 @@ namespace sat {
     }
 
     void cut_simplifier::add_dont_cares(vector<cut_set> const& cuts) {
-        if (!s.m_config.m_cut_dont_cares) 
-            return;
-        cuts2bins(cuts);
-        bins2dont_cares();
-        dont_cares2cuts(cuts);        
-        // m_aig_cuts.simplify();
+        if (s.m_config.m_cut_dont_cares) {
+            cuts2bins(cuts);
+            bins2dont_cares();
+            dont_cares2cuts(cuts); 
+        }    
+        if (s.m_config.m_cut_redundancies) {
+            m_aig_cuts.simplify();
+        }
     }
 
     /**
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index d36cc1256..8ebf2459a 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -81,6 +81,7 @@ def_module_params('sat',
                           ('cut.xor',   BOOL, False, 'extract xors from clauses for cut simplification'),
                           ('cut.npn3',  BOOL, False, 'extract 3 input functions from clauses for cut simplification'),
                           ('cut.dont_cares', BOOL, True, 'integrate dont cares with cuts'),
+                          ('cut.redundancies', BOOL, True, 'integrate redundancy checking of cuts'),
                           ('cut.force', BOOL, False, 'force redoing cut-enumeration until a fixed-point'),
                           ('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'),
                           # - depth: the maximal cutoff is fixed to the value of lookahead.cube.depth.