Deduplication of quantifiers with distinct QIDs?

[parno]

In the small example below, we declare two functions, lemma1 and lemma2, each of which provides the same quantified fact. The quantifiers, however, use different qid fields. In the final assert, we expect the quantifier from lemma2 to be used. However, in the trace file that's produced, it appears that user_lemma1 was instantiated instead (although it's possible we're misinterpreting the trace file), since the new-match entry points at an entry like [mk-quant] #32 user_lemma1 1 #27 #2.
Interestingly, if we change the name of the quantified variable in lemma2 from x to y, then the trace shows user_lemma2 being instantiated as expected (i.e., the new-match points at an entry like [mk-quant] #35 user_lemma2 1 #27 #25). This made us wonder if quantifers are being hashed or otherwise deduplicated in a way that ignores the qid field. If so, is that intended behavior (e.g., as an optimization), or is it inadvertent?

(set-option :auto_config false)

(set-option :trace true)
(set-option :trace_file_name small-trace.log)

(declare-fun f (Int) Bool)

(declare-fun lemma1. () Bool)
(assert
 (= lemma1. 
    (forall ((x Int)) (! (= (f x) true)
    :pattern ((f x))
    :qid user_lemma1
))))

(declare-fun lemma2. () Bool)
(assert
 (= lemma2. 
    (forall ((x Int)) (! (= (f x) true)
    :pattern ((f x))
    :qid user_lemma2
))))

(push)
 (assert
   (not (=>
     lemma2.
     (f 42)
      )))
 (check-sat)
(pop)

[NikolajBjorner]

ast.cpp: ast_manager::get_node_hash computes the hash of a quantifier without comparing qids.

    case AST_QUANTIFIER:
        a = ast_array_hash(to_quantifier(n)->get_decl_sorts(),
                           to_quantifier(n)->get_num_decls(),
                           to_quantifier(n)->get_kind() == forall_k ? 31 : 19);
        b = to_quantifier(n)->get_num_patterns();
        c = to_quantifier(n)->get_expr()->hash();
        mix(a,b,c);

Comparison on quantifiers uses compare_nodes

    case AST_QUANTIFIER:
        return
            to_quantifier(n1)->get_kind()            == to_quantifier(n2)->get_kind() &&
            to_quantifier(n1)->get_num_decls()       == to_quantifier(n2)->get_num_decls() &&
            compare_arrays(to_quantifier(n1)->get_decl_sorts(),
                           to_quantifier(n2)->get_decl_sorts(),
                           to_quantifier(n1)->get_num_decls()) &&
            compare_arrays(to_quantifier(n1)->get_decl_names(),
                           to_quantifier(n2)->get_decl_names(),
                           to_quantifier(n1)->get_num_decls()) &&
            to_quantifier(n1)->get_expr()            == to_quantifier(n2)->get_expr() &&
            to_quantifier(n1)->get_weight()          == to_quantifier(n2)->get_weight() &&
            to_quantifier(n1)->get_num_patterns() == to_quantifier(n2)->get_num_patterns() &&
            compare_arrays(to_quantifier(n1)->get_patterns(),
                           to_quantifier(n2)->get_patterns(),
                           to_quantifier(n1)->get_num_patterns()) &&
            to_quantifier(n1)->get_num_no_patterns() == to_quantifier(n2)->get_num_no_patterns() &&
            compare_arrays(to_quantifier(n1)->get_no_patterns(),
                           to_quantifier(n2)->get_no_patterns(),
                           to_quantifier(n1)->get_num_no_patterns());

meta-data is ignored.

[parno]

Thanks for identifying those two spots! Nice to have our hypothesis confirmed. Would it be reasonable to include meta-data in those two places, or would that be likely to break functionality or hurt performance?

[NikolajBjorner]

I think the question is about semantics. It allows the quantifier identifier fields to be mutable.

[NikolajBjorner]

I pushed 6e53621 to have equality relation include qid.

[parno]

Cool, thanks very much! We'll pick that up.