1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 nlsat_justification.h 7 8 Abstract: 9 10 An explanation for a (Boolean) assignment in the 11 nlsat procedure 12 13 Author: 14 15 Leonardo de Moura (leonardo) 2012-01-10. 16 17 Revision History: 18 19 --*/ 20 #pragma once 21 22 #include "nlsat/nlsat_types.h" 23 #include "util/tptr.h" 24 25 namespace nlsat { 26 27 // There are two kinds of justifications in nlsat: 28 // 29 // - clause 30 // 31 // - lazy_justification: it is a set of arithmetic literals s.t. 32 // the maximal variable in each literal is the same. 33 // The set is inconsistent in the current model. 34 // Thus, our nonlinear procedure may be applied to it 35 // to produce a clause. 36 // 37 38 class lazy_justification { 39 unsigned m_num_literals; 40 unsigned m_num_clauses; 41 char m_data[0]; clauses()42 nlsat::clause* const* clauses() const { return (nlsat::clause *const*)(m_data); } 43 public: get_obj_size(unsigned nl,unsigned nc)44 static unsigned get_obj_size(unsigned nl, unsigned nc) { return sizeof(lazy_justification) + sizeof(literal)*nl + sizeof(nlsat::clause*)*nc; } lazy_justification(unsigned nl,literal const * lits,unsigned nc,nlsat::clause * const * clss)45 lazy_justification(unsigned nl, literal const * lits, unsigned nc, nlsat::clause * const* clss): 46 m_num_literals(nl), 47 m_num_clauses(nc) { 48 if (nc > 0) { 49 memcpy(m_data + 0, clss, sizeof(nlsat::clause*)*nc); 50 } 51 if (nl > 0) { 52 memcpy(m_data + sizeof(nlsat::clause*)*nc, lits, sizeof(literal)*nl); 53 } 54 } num_lits()55 unsigned num_lits() const { return m_num_literals; } lit(unsigned i)56 literal lit(unsigned i) const { SASSERT(i < num_lits()); return lits()[i]; } lits()57 literal const * lits() const { return (literal const*)(m_data + m_num_clauses*sizeof(nlsat::clause*)); } 58 num_clauses()59 unsigned num_clauses() const { return m_num_clauses; } clause(unsigned i)60 nlsat::clause const& clause(unsigned i) const { SASSERT(i < num_clauses()); return *(clauses()[i]); } 61 62 }; 63 64 class justification { 65 void * m_data; 66 public: 67 enum kind { NULL_JST = 0, DECISION, CLAUSE, LAZY }; justification()68 justification():m_data(TAG(void *, nullptr, NULL_JST)) { SASSERT(is_null()); } justification(bool)69 justification(bool):m_data(TAG(void *, nullptr, DECISION)) { SASSERT(is_decision()); } justification(clause * c)70 justification(clause * c):m_data(TAG(void *, c, CLAUSE)) { SASSERT(is_clause()); } justification(lazy_justification * j)71 justification(lazy_justification * j):m_data(TAG(void *, j, LAZY)) { SASSERT(is_lazy()); } get_kind()72 kind get_kind() const { return static_cast<kind>(GET_TAG(m_data)); } is_null()73 bool is_null() const { return get_kind() == NULL_JST; } is_decision()74 bool is_decision() const { return get_kind() == DECISION; } is_clause()75 bool is_clause() const { return get_kind() == CLAUSE; } is_lazy()76 bool is_lazy() const { return get_kind() == LAZY; } get_clause()77 clause * get_clause() const { return UNTAG(clause*, m_data); } get_lazy()78 lazy_justification * get_lazy() const { return UNTAG(lazy_justification*, m_data); } 79 bool operator==(justification other) const { return m_data == other.m_data; } 80 bool operator!=(justification other) const { return m_data != other.m_data; } 81 }; 82 83 inline std::ostream& operator<<(std::ostream& out, justification::kind k) { 84 switch (k) { 85 case justification::NULL_JST: return out << "null"; 86 case justification::DECISION: return out << "decision"; 87 case justification::CLAUSE: return out << "clause"; 88 case justification::LAZY: return out << "lazy"; 89 default: return out << "??"; 90 } 91 } 92 93 const justification null_justification; 94 const justification decided_justification(true); 95 mk_clause_jst(clause const * c)96 inline justification mk_clause_jst(clause const * c) { return justification(const_cast<clause*>(c)); } mk_lazy_jst(small_object_allocator & a,unsigned nl,literal const * lits,unsigned nc,clause * const * clauses)97 inline justification mk_lazy_jst(small_object_allocator & a, unsigned nl, literal const * lits, unsigned nc, clause *const* clauses) { 98 void * mem = a.allocate(lazy_justification::get_obj_size(nl, nc)); 99 return justification(new (mem) lazy_justification(nl, lits, nc, clauses)); 100 } 101 del_jst(small_object_allocator & a,justification jst)102 inline void del_jst(small_object_allocator & a, justification jst) { 103 if (jst.is_lazy()) { 104 lazy_justification * ptr = jst.get_lazy(); 105 unsigned obj_sz = lazy_justification::get_obj_size(ptr->num_lits(), ptr->num_clauses()); 106 a.deallocate(obj_sz, ptr); 107 } 108 } 109 }; 110 111