mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #3815

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-06 19:28:51 -07:00
parent 9c6722bea8
commit bd0620f245
2 changed files with 3 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_prob.cpp
View file

@ -123,6 +123,7 @@ namespace sat {
} }
void prob::add(solver const& s) { void prob::add(solver const& s) {
m_values.reserve(s.num_vars(), false);
unsigned trail_sz = s.init_trail_size(); unsigned trail_sz = s.init_trail_size();
for (unsigned i = 0; i < trail_sz; ++i) { for (unsigned i = 0; i < trail_sz; ++i) {
add(1, s.m_trail.c_ptr() + i); add(1, s.m_trail.c_ptr() + i);

7
src/sat/sat_types.h
View file

@ -143,7 +143,7 @@ namespace sat {
typedef svector<lbool> model; typedef svector<lbool> model;
inline void negate(literal_vector& ls) { for (unsigned i = 0; i < ls.size(); ++i) ls[i].neg(); } inline void negate(literal_vector& ls) { for (unsigned i = 0; i < ls.size(); ++i) ls[i].neg(); }
inline lbool value_at(bool_var v, model const & m) { return m[v]; } inline lbool value_at(bool_var v, model const & m) { return m[v]; }
inline lbool value_at(literal l, model const & m) { lbool r = value_at(l.var(), m); return l.sign() ? ~r : r; } inline lbool value_at(literal l, model const & m) { lbool r = value_at(l.var(), m); return l.sign() ? ~r : r; }
inline std::ostream & operator<<(std::ostream & out, model const & m) { inline std::ostream & operator<<(std::ostream & out, model const & m) {
@ -169,10 +169,7 @@ namespace sat {
literal_set() {} literal_set() {}
literal_vector to_vector() const { literal_vector to_vector() const {
literal_vector result; literal_vector result;
iterator it = begin(), e = end(); for (literal lit : *this) result.push_back(lit);
for (; it != e; ++it) {
result.push_back(*it);
}
return result; return result;
} }
literal_set& operator=(literal_vector const& v) { literal_set& operator=(literal_vector const& v) {