Home
last modified time | relevance | path

Searched refs:m_reinit (Results 1 – 14 of 14) sorted by relevance

/dports/math/z3/z3-z3-4.8.13/src/smt/
H A Dsmt_clause.h59 …unsigned m_reinit:1; //!< true if the clause is in the reinit stack (only for learned… variable
139 SASSERT(!m_reinit); in set_num_literals()
145 SASSERT(!m_reinit); in set_justification()
177 return m_reinit; in in_reinit_stack()
H A Dsmt_clause.cpp39 cls->m_reinit = save_atoms; in mk()
86 SASSERT(m_reinit || get_atom(i) == 0); in deallocate()
H A Dsmt_internalizer.cpp1211 cls->m_reinit = true; in mark_for_reinit()
H A Dsmt_context.cpp2260 cls->m_reinit = false; in reinit_clauses()
2349 cls->m_reinit = false; in reinit_clauses()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/
H A Dsmt_clause.h59 …unsigned m_reinit:1; //!< true if the clause is in the reinit stack (only for learned… variable
139 SASSERT(!m_reinit); in set_num_literals()
145 SASSERT(!m_reinit); in set_justification()
177 return m_reinit; in in_reinit_stack()
H A Dsmt_clause.cpp39 cls->m_reinit = save_atoms; in mk()
86 SASSERT(m_reinit || get_atom(i) == 0); in deallocate()
H A Dsmt_internalizer.cpp1205 cls->m_reinit = true; in mark_for_reinit()
H A Dsmt_context.cpp2272 cls->m_reinit = false; in reinit_clauses()
2361 cls->m_reinit = false; in reinit_clauses()
/dports/editors/abiword/abiword-3.0.5/src/wp/ap/cocoa/
H A Dap_CocoaDialog_Options.h125 m_reinit = value; in setReinit()
129 return m_reinit; in getReinit()
223 bool m_reinit; variable
H A Dap_CocoaDialog_Options.cpp54 , m_reinit(false) in AP_CocoaDialog_Options()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/
H A Deuf_solver.cpp492 m_reinit.reset(); in start_reinit()
496 … m_reinit.push_back(reinit_t(expr_ref(e, m), get_enode(e)?get_enode(e)->generation():0, v)); in start_reinit()
506 if (m_reinit.empty()) in finish_reinit()
522 for (auto const& t : m_reinit) in finish_reinit()
526 for (auto const& t : m_reinit) { in finish_reinit()
H A Deuf_solver.h126 vector<reinit_t> m_reinit; variable
/dports/math/z3/z3-z3-4.8.13/src/sat/smt/
H A Deuf_solver.cpp565 m_reinit.reset(); in start_reinit()
569 … m_reinit.push_back(reinit_t(expr_ref(e, m), get_enode(e)?get_enode(e)->generation():0, v)); in start_reinit()
579 if (m_reinit.empty()) in finish_reinit()
595 for (auto const& [e, generation, v] : m_reinit) in finish_reinit()
599 for (auto const& [e, generation, v] : m_reinit) { in finish_reinit()
620 for (auto const& [e, generation, v] : m_reinit) in finish_reinit()
H A Deuf_solver.h135 vector<reinit_t> m_reinit; variable