| /dports/misc/gpsim/gpsim-0.31.0/src/ |
| H A D | 14bit-instructions.cc | 42 m_lit = opcode & 0x3f; in ADDFSR()
43 if (m_lit & 0x20) m_lit -= 0x40; in ADDFSR()
66 m_lit); in name()
107 m_lit = opcode & 0x3f; in MOVIW()
108 if (m_lit & 0x20) m_lit -= 0x40; in MOVIW()
164 gpsimObject::name().c_str(), m_lit, in name()
203 ia->fsr_delta = m_lit; in execute()
217 m_lit = opcode & 0x3f; in MOVWI()
218 if (m_lit & 0x20) m_lit -= 0x40; in MOVWI()
274 gpsimObject::name().c_str(), m_lit, in name()
[all …]
|
| H A D | 14bit-instructions.h | 50 int m_lit; variable
176 int m_lit; variable
203 int m_lit; variable
|
| H A D | 16bit-instructions.cc | 133 m_lit = opcode & 0x3f; in ADDULNK()
142 m_lit); in name()
151 cpu16->ind2.put_fsr(cpu16->ind2.get_fsr_value() - m_lit); // SUBULNK in execute()
154 cpu16->ind2.put_fsr(cpu16->ind2.get_fsr_value() + m_lit); // ADDULNK in execute()
172 m_lit = opcode & 0x3f; in ADDFSR16()
200 m_lit); in name()
213 ia->put_fsr(ia->get_fsr_value() - m_lit); //SUBFSR in execute()
216 ia->put_fsr(ia->get_fsr_value() + m_lit); //ADDFSR in execute()
252 m_lit(new_opcode & 0xff) in PUSHL()
261 gpsimObject::name().c_str(), m_lit); in name()
[all …]
|
| H A D | 16bit-instructions.h | 118 unsigned int m_lit;
153 unsigned int m_lit; variable
212 unsigned int m_lit;
|
| /dports/math/z3/z3-z3-4.8.13/src/nlsat/ |
| H A D | nlsat_scoped_literal_vector.h | 79 literal m_lit; variable
81 scoped_literal(solver & s):m_solver(s), m_lit(null_literal) {} in scoped_literal()
82 ~scoped_literal() { m_solver.dec_ref(m_lit); } in ~scoped_literal()
85 m_solver.dec_ref(m_lit);
86 m_lit = l;
89 scoped_literal & operator=(scoped_literal const & l) { return operator=(l.m_lit); }
90 operator literal&() { return m_lit; }
91 operator literal const &() const { return m_lit; }
92 void neg() { m_lit.neg(); } in neg()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/nlsat/ |
| H A D | nlsat_scoped_literal_vector.h | 79 literal m_lit; variable
81 scoped_literal(solver & s):m_solver(s), m_lit(null_literal) {} in scoped_literal()
82 ~scoped_literal() { m_solver.dec_ref(m_lit); } in ~scoped_literal()
85 m_solver.dec_ref(m_lit);
86 m_lit = l;
89 scoped_literal & operator=(scoped_literal const & l) { return operator=(l.m_lit); }
90 operator literal&() { return m_lit; }
91 operator literal const &() const { return m_lit; }
92 void neg() { m_lit.neg(); } in neg()
|
| /dports/math/vampire/vampire-4.5.1/Kernel/ |
| H A D | LiteralByMatchability.hpp | 48 Literal* m_lit; member in Kernel::LiteralByMatchability
53 : m_lit(lit), m_val(computeRating(lit)) in LiteralByMatchability()
61 Literal* lit() const { return m_lit; } in lit()
65 return m_val < other.m_val || (m_val == other.m_val && m_lit->getId() < other.m_lit->getId()); in operator <()
70 bool operator==(LiteralByMatchability const& other) const { return m_lit == other.m_lit; } in operator ==()
|
| /dports/math/z3/z3-z3-4.8.13/src/sat/smt/ |
| H A D | pb_constraint.h | 39 literal m_lit; variable
53 m_tag(t), m_lit(l), m_size(sz), m_obj_size(osz), m_id(id), m_k(k) { in constraint()
62 literal lit() const { return m_lit; } in lit()
65 void update_literal(literal l) { m_lit = l; } in update_literal()
68 void nullify_literal() { m_lit = sat::null_literal; } in nullify_literal()
75 bool is_watched() const { return m_watch == m_lit && m_lit != sat::null_literal; } in is_watched()
76 void set_watch() { m_watch = m_lit; } in set_watch()
78 bool is_clear() const { return m_watch == sat::null_literal && m_lit != sat::null_literal; } in is_clear()
|
| H A D | euf_solver.h | 118 constraint* m_lit = nullptr; variable
202 constraint& lit_constraint() { return mk_constraint(m_lit, constraint::kind_t::lit); } in lit_constraint()
216 if (m_lit) dealloc(sat::constraint_base::mem2base_ptr(m_lit)); in ~solver()
|
| H A D | pb_pb.h | 34 literal lit() const { return m_lit; } in lit()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/ |
| H A D | ba_constraint.h | 42 literal m_lit; variable
55 …m_tag(t), m_removed(false), m_lit(l), m_watch(sat::null_literal), m_glue(0), m_psm(0), m_size(sz),… in constraint()
61 literal lit() const { return m_lit; } in lit()
64 void update_literal(literal l) { m_lit = l; } in update_literal()
67 void nullify_literal() { m_lit = sat::null_literal; } in nullify_literal()
74 bool is_watched() const { return m_watch == m_lit && m_lit != sat::null_literal; } in is_watched()
75 void set_watch() { m_watch = m_lit; } in set_watch()
77 bool is_clear() const { return m_watch == sat::null_literal && m_lit != sat::null_literal; } in is_clear()
|
| H A D | euf_solver.h | 110 constraint* m_lit{ nullptr };
188 constraint& lit_constraint() { return mk_constraint(m_lit, constraint::kind_t::lit); } in lit_constraint()
202 if (m_lit) dealloc(sat::constraint_base::mem2base_ptr(m_lit)); in ~solver()
|
| H A D | ba_pb.h | 34 literal lit() const { return m_lit; } in lit()
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | theory_pb.h | 108 literal m_lit; // literal representing predicate member
123 m_mpz(m), m_lit(l), m_is_eq(is_eq), in ineq()
129 arg_t const& args() const { return m_args[m_lit.sign()]; } in args()
130 arg_t& args() { return m_args[m_lit.sign()]; } in args()
132 literal lit() const { return m_lit; } in lit()
191 literal m_lit; // literal representing predicate variable
200 m_lit(l), in card()
209 literal lit() const { return m_lit; } in lit()
|
| H A D | seq_regex.h | 98 literal m_lit; member
103 m_lit(l), m_s(s), m_re(r), m_active(true) {} in s_in_re()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | theory_pb.h | 108 literal m_lit; // literal representing predicate member
123 m_mpz(m), m_lit(l), m_is_eq(is_eq), in ineq()
129 arg_t const& args() const { return m_args[m_lit.sign()]; } in args()
130 arg_t& args() { return m_args[m_lit.sign()]; } in args()
132 literal lit() const { return m_lit; } in lit()
191 literal m_lit; // literal representing predicate variable
200 m_lit(l), in card()
209 literal lit() const { return m_lit; } in lit()
|
| H A D | seq_regex.h | 98 literal m_lit; member
103 m_lit(l), m_s(s), m_re(r), m_active(true) {} in s_in_re()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/arith/ |
| H A D | pb2bv_tactic.cpp | 157 lit m_lit; member
158 monomial(lit l):m_a(1), m_lit(l) {} in monomial()
327 if (it->m_lit.sign()) in display()
329 out << mk_ismt2_pp(it->m_lit.var(), m); in display()
355 return int2lit(to_app(mo.m_lit.var()), mo.m_lit.sign()); in mon_lit2lit()
465 m.mk_ite(mon_lit2lit(mo.m_lit), in bitblast_pbc()
604 if (m1.m_lit.sign() == m2.m_lit.sign()) in is_eq_vector()
795 m.m_lit.neg(); in convert()
807 app * x_i = to_app(m_p[i].m_lit.var()); in convert()
808 app * y_i = to_app(m_p[i+1].m_lit.var()); in convert()
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/tactic/arith/ |
| H A D | pb2bv_tactic.cpp | 157 lit m_lit; member
158 monomial(lit l):m_a(1), m_lit(l) {} in monomial()
327 if (it->m_lit.sign()) in display()
329 out << mk_ismt2_pp(it->m_lit.var(), m); in display()
355 return int2lit(to_app(mo.m_lit.var()), mo.m_lit.sign()); in mon_lit2lit()
465 m.mk_ite(mon_lit2lit(mo.m_lit), in bitblast_pbc()
604 if (m1.m_lit.sign() == m2.m_lit.sign()) in is_eq_vector()
796 m.m_lit.neg(); in convert()
808 app * x_i = to_app(m_p[i].m_lit.var()); in convert()
809 app * y_i = to_app(m_p[i+1].m_lit.var()); in convert()
[all …]
|
| /dports/math/z3/z3-z3-4.8.13/src/util/ |
| H A D | sat_literal.h | 165 literal m_lit; member
166 explicit dimacs_lit(literal l):m_lit(l) {} in dimacs_lit()
170 literal l = dl.m_lit;
|
| /dports/math/ogdf/OGDF/include/ogdf/energybased/ |
| H A D | SpringEmbedderGridVariant.h | 102 ListIterator<int> m_lit; member
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/ |
| H A D | sat_types.h | 211 literal m_lit; member
212 dimacs_lit(literal l):m_lit(l) {} in dimacs_lit()
216 literal l = dl.m_lit;
|
| /dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/what4-1.1/test/ |
| H A D | ExprsTest.hs | 78 m_lit <- intLit sym m
79 nm <- intMul sym n_lit m_lit
80 mn <- intMul sym m_lit n_lit
|
| /dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | bva.cpp | 333 for(const lit_pair m_lit: m_lits) { in bva_simplify_system() local
335 bva_tmp_lits.push_back(m_lit.lit1); in bva_simplify_system()
336 if (m_lit.lit2 != lit_Undef) { in bva_simplify_system()
337 bva_tmp_lits.push_back(m_lit.lit2); in bva_simplify_system()
|
| /dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | bva.cpp | 333 for(const lit_pair m_lit: m_lits) { in bva_simplify_system() local
335 bva_tmp_lits.push_back(m_lit.lit1); in bva_simplify_system()
336 if (m_lit.lit2 != lit_Undef) { in bva_simplify_system()
337 bva_tmp_lits.push_back(m_lit.lit2); in bva_simplify_system()
|