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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
mus.h
Abstract:
Basic MUS extraction
Author:
Nikolaj Bjorner (nbjorner) 2014-20-7
Notes:
--*/
#pragma once
class mus {
struct imp;
imp * m_imp;
public:
mus(solver& s);
~mus();
/**
Add soft constraint.
Assume that the solver context enforces that
cls is equivalent to a disjunction of args.
Assume also that cls is a literal.
*/
unsigned add_soft(expr* cls);
void add_soft(unsigned sz, expr* const* clss) {
for (unsigned i = 0; i < sz; ++i) add_soft(clss[i]);
}
/**
Additional assumption for solver to be used along with solver context,
but not used in core computation. This facility is useful when querying
for a core over only a subset of soft constraints. It has the same
logical functionality as asserting 'lit' to the solver and pushing a scope
(and popping the scope before the solver is used for other constraints).
*/
void add_assumption(expr* lit);
lbool get_mus(expr_ref_vector& mus);
void reset();
/**
Instrument MUS extraction to also provide the minimal
penalty model, if any is found.
The minimal penalty model has the least weight for the
supplied soft constraints.
*/
void set_soft(unsigned sz, expr* const* soft, rational const* weights);
rational get_best_model(model_ref& mdl);
};