mirror of
https://github.com/Z3Prover/z3
synced 2025-08-23 11:37:54 +00:00
50 lines
1.3 KiB
C++
50 lines
1.3 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;
|
|
|
|
struct scoped_mark_reset;
|
|
|
|
// compare s, t modulo binding
|
|
lbool compare(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_vector& evidence);
|
|
lbool compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_vector& evidence);
|
|
|
|
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, euf::enode_pair_vector& evidence);
|
|
lbool operator()(euf::enode* const* binding, clause& c, unsigned& idx, euf::enode_pair_vector& evidence);
|
|
euf::enode* operator()(unsigned n, euf::enode* const* binding, expr* e, euf::enode_pair_vector& evidence);
|
|
|
|
euf::enode_vector const& get_watch() { return m_indirect_nodes; }
|
|
};
|
|
}
|