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