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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
nlsat_explain.h
Abstract:
Functor that implements the "explain" procedure defined in Dejan and Leo's paper.
Uses paper Haokun Li and Bican Xia, "Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection",https://arxiv.org/abs/2003.00409,
and code from https://github.com/hybridSMT/hybridSMT.git
Author:
Leonardo de Moura (leonardo) 2012-01-13.
Revision History:
--*/
#pragma once
#include "nlsat/nlsat_solver.h"
#include "nlsat/nlsat_scoped_literal_vector.h"
#include "math/polynomial/polynomial_cache.h"
#include "math/polynomial/algebraic_numbers.h"
namespace nlsat {
class evaluator;
class explain {
public:
struct imp;
private:
imp * m_imp;
public:
explain(solver & s, assignment const & x2v, polynomial::cache & u,
atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool canonicalize);
~explain();
void reset();
void set_simplify_cores(bool f);
void set_full_dimensional(bool f);
void set_minimize_cores(bool f);
void set_factor(bool f);
void set_add_all_coeffs(bool f);
void set_add_zero_disc(bool f);
/**
\brief Given a set of literals ls[0], ... ls[n-1] s.t.
- n > 0
- all of them are arithmetic literals.
- all of them have the same maximal variable.
- (ls[0] and ... and ls[n-1]) is infeasible in the current interpretation.
Let x be the maximal variable in {ls[0], ..., ls[n-1]}.
Remark: the current interpretation assigns all variables in ls[0], ..., ls[n-1] but x.
This procedure stores in result a set of literals: s_1, ..., s_m
s.t.
- (s_1 or ... or s_m or ~ls[0] or ... or ~ls[n-1]) is a valid clause
- s_1, ..., s_m do not contain variable x.
- s_1, ..., s_m are false in the current interpretation
If this operation throws, result may contain partial output and must
be cleared before retrying. Internal duplicate-literal marks are
cleared even on exception, so the explanation engine can be reused.
*/
void compute_conflict_explanation(unsigned n, literal const * ls, scoped_literal_vector & result);
/**
\brief A variant of compute_conflict_explanation, but all resulting literals s_i are linear.
This is achieved by adding new polynomials during the projection, thereby under-approximating
the computed cell.
*/
void compute_linear_explanation(unsigned n, literal const * ls, scoped_literal_vector & result);
/**
\brief projection for a given variable.
Given: M |= l1[x] /\ ... /\ ln[x]
Find: M |= s1, ..., sm
Such that: |= ~s1 \/ ... \/ ~sm \/ E x. l1[x] /\ ... /\ ln[x]
Contrast this with with the core-based projection above:
Given: M |= A x . l1[x] \/ ... \/ ln[x]
Find: M |= ~s1, ..., ~sm.
Such that: |= s1 \/ ... \/ sm \/ A x . l1[x] \/ ... \/ ln[x]
Claim: the two compute the same solutions if the projection operators are independent of the value of x.
Claim: A complete, convergent projection operator can be obtained from M in a way that is independent of x.
*/
void project(var x, unsigned n, literal const * ls, scoped_literal_vector & result);
/**
Print the polynomials that were passed to levelwise in the last call (for debugging).
*/
void display_last_lws_input(std::ostream& out);
/**
Unit test routine.
*/
void test_root_literal(atom::kind k, var y, unsigned i, poly* p, scoped_literal_vector & result);
};
}