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