1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
smt_implied_equalities.h
Abstract:
Procedure for obtaining implied equalities relative to the
state of a solver.
Author:
Nikolaj Bjorner (nbjorner) 2012-02-29
Revision History:
--*/
#pragma once
#include "smt/smt_solver.h"
#include "util/lbool.h"
#include "ast/ast.h"
namespace smt {
lbool implied_equalities(
ast_manager & m,
solver & solver,
unsigned num_terms, expr* const* terms,
unsigned* class_ids);
};