1 /*++
2   Copyright (c) 2020 Microsoft Corporation
3 
4   Module Name:
5 
6    sat_aig_finder.h
7 
8   Abstract:
9 
10     extract AIG definitions from clauses.
11     An example AIG clause is:
12        head \/ l1 \/ l2
13     such that
14        ~l1 /\ ~l2 => head
15        head => ~l1, head => ~l2
16 
17   Author:
18 
19     Nikolaj Bjorner 2020-01-02
20 
21   Notes:
22 
23     AIG finder
24   --*/
25 
26 #pragma once
27 
28 #include "util/params.h"
29 #include "util/statistics.h"
30 #include "sat/sat_clause.h"
31 #include "sat/sat_types.h"
32 #include "sat/sat_big.h"
33 
34 namespace sat {
35 
36     class solver;
37 
38     class aig_finder {
39         solver& s;
40         big                     m_big;
41         literal_vector          m_ands;
42         std::function<void (literal head, literal_vector const& ands)> m_on_aig;
43         std::function<void (literal head, literal cond, literal th, literal el)> m_on_if;
44         bool implies(literal a, literal b);
45         bool find_aig(clause& c);
46         void find_ifs(clause_vector& clauses);
47         void find_aigs(clause_vector& clauses);
48         void validate_and(literal head, literal_vector const& ands, clause const& c);
49         void validate_if(literal x, literal c, literal t, literal e, clause const& c0, clause const* c1, clause const* c2, clause const* c3);
50         void validate_clause(literal x, literal y, literal z, vector<literal_vector> const& clauses);
51         void validate_clause(literal_vector const& clause, vector<literal_vector> const& clauses);
52 
53     public:
54         aig_finder(solver& s);
~aig_finder()55         ~aig_finder() {}
set(std::function<void (literal head,literal_vector const & ands)> const & f)56         void set(std::function<void (literal head, literal_vector const& ands)> const& f) { m_on_aig = f; }
set(std::function<void (literal head,literal cond,literal th,literal el)> const & f)57         void set(std::function<void (literal head, literal cond, literal th, literal el)> const& f) { m_on_if = f; }
58         void operator()(clause_vector& clauses);
59     };
60 }
61