mirror of
https://github.com/Z3Prover/z3
synced 2025-08-22 11:07:51 +00:00
55 lines
1.4 KiB
C++
55 lines
1.4 KiB
C++
/*++
|
|
Copyright (c) 2020 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
q_eval.h
|
|
|
|
Abstract:
|
|
|
|
Evaluation of clauses
|
|
|
|
Author:
|
|
|
|
Nikolaj Bjorner (nbjorner) 2021-01-24
|
|
|
|
--*/
|
|
#pragma once
|
|
|
|
#include "sat/smt/q_clause.h"
|
|
|
|
namespace euf {
|
|
class solver;
|
|
}
|
|
|
|
namespace q {
|
|
|
|
class eval {
|
|
euf::solver& ctx;
|
|
ast_manager& m;
|
|
expr_fast_mark1 m_mark;
|
|
euf::enode_vector m_eval;
|
|
euf::enode_vector m_indirect_nodes;
|
|
ptr_vector<size_t> m_explain;
|
|
|
|
struct scoped_mark_reset;
|
|
|
|
void explain(clause& c, unsigned literal_idx, euf::enode* const* binding);
|
|
void explain_eq(unsigned n, euf::enode* const* binding, expr* s, expr* t);
|
|
void explain_diseq(unsigned n, euf::enode* const* binding, expr* s, expr* t);
|
|
|
|
// compare s, t modulo binding
|
|
lbool compare(unsigned n, euf::enode* const* binding, expr* s, expr* t);
|
|
lbool compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t);
|
|
|
|
public:
|
|
eval(euf::solver& ctx);
|
|
void explain(sat::literal l, justification& j, sat::literal_vector& r, bool probing);
|
|
|
|
lbool operator()(euf::enode* const* binding, clause& c);
|
|
lbool operator()(euf::enode* const* binding, clause& c, unsigned& idx);
|
|
euf::enode* operator()(unsigned n, euf::enode* const* binding, expr* e);
|
|
|
|
euf::enode_vector const& get_watch() { return m_indirect_nodes; }
|
|
};
|
|
}
|