1 /*++
2 Copyright (c) 2020 Microsoft Corporation
3 
4 Module Name:
5 
6     q_eval.h
7 
8 Abstract:
9 
10     Evaluation of clauses
11 
12 Author:
13 
14     Nikolaj Bjorner (nbjorner) 2021-01-24
15 
16 --*/
17 #pragma once
18 
19 #include "ast/has_free_vars.h"
20 #include "sat/smt/q_clause.h"
21 
22 namespace euf {
23     class solver;
24 }
25 
26 namespace q {
27 
28     class eval {
29         euf::solver&       ctx;
30         ast_manager&       m;
31         expr_fast_mark1    m_mark;
32         euf::enode_vector  m_eval;
33         euf::enode_vector  m_indirect_nodes;
34         bool               m_freeze_swap = false;
35         euf::enode_pair    m_diseq_undef;
36         contains_vars      m_contains_vars;
37 
38         struct scoped_mark_reset;
39 
40         // compare s, t modulo binding
41         lbool compare(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_vector& evidence);
42         lbool compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_vector& evidence);
43 
44     public:
45         eval(euf::solver& ctx);
46         void explain(sat::literal l, justification& j, sat::literal_vector& r, bool probing);
47 
48         lbool operator()(euf::enode* const* binding, clause& c, euf::enode_pair_vector& evidence);
49         lbool operator()(euf::enode* const* binding, clause& c, unsigned& idx, euf::enode_pair_vector& evidence);
50         euf::enode* operator()(unsigned n, euf::enode* const* binding, expr* e, euf::enode_pair_vector& evidence);
51 
get_watch()52         euf::enode_vector const& get_watch() { return m_indirect_nodes; }
53     };
54 }
55