mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 17:08:45 +00:00
Code Activity

term_le -> term_lt

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-11 14:31:20 -07:00 • committed by Arie Gurfinkel
parent f963fc06f4
commit 5ab6d6ca16
2 changed files with 101 additions and 101 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/qe/qe_term_graph.cpp
View file

@ -77,7 +77,7 @@ namespace qe {
};
class children {
term const& t;
term const& t;
public:
children(term const& _t):t(_t) {}
children(term const* _t):t(*_t) {}
@ -533,7 +533,7 @@ namespace qe {
// prefer uninterpreted constants over values
// prefer smaller expressions over larger ones
if (t1.get_num_args() == 0 || t2.get_num_args() == 0) {
if (t1.get_num_args() == t2.get_num_args()) {
if (t1.get_num_args() == t2.get_num_args()) {
// t1.get_num_args() == t2.get_num_args() == 0
if (m.is_value(t1.get_expr()) == m.is_value(t2.get_expr()))
return t1.get_id() < t2.get_id();
@ -637,7 +637,7 @@ namespace qe {
// use work-list + marking to propagate.
// - produce equalities over represented classes.
// - produce other literals over represented classes
// (walk disequalities in m_lits and represent lhs/rhs over decls or excluding decls)
// (walk disequalities in m_lits and represent lhs/rhs over decls or excluding decls)
expr_ref_vector result(m);
m_term2app.reset();