1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Tim King, Tianyi Liang |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* The extended theory callback for non-linear arithmetic |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/arith/nl/ext_theory_callback.h" |
17 |
|
|
18 |
|
#include "theory/arith/arith_utilities.h" |
19 |
|
#include "theory/uf/equality_engine.h" |
20 |
|
|
21 |
|
using namespace cvc5::kind; |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
namespace theory { |
25 |
|
namespace arith { |
26 |
|
namespace nl { |
27 |
|
|
28 |
4914 |
NlExtTheoryCallback::NlExtTheoryCallback(eq::EqualityEngine* ee) : d_ee(ee) |
29 |
|
{ |
30 |
4914 |
d_zero = NodeManager::currentNM()->mkConst(Rational(0)); |
31 |
4914 |
} |
32 |
|
|
33 |
3995 |
bool NlExtTheoryCallback::getCurrentSubstitution( |
34 |
|
int effort, |
35 |
|
const std::vector<Node>& vars, |
36 |
|
std::vector<Node>& subs, |
37 |
|
std::map<Node, std::vector<Node>>& exp) |
38 |
|
{ |
39 |
|
// get the constant equivalence classes |
40 |
7990 |
std::map<Node, std::vector<int>> rep_to_subs_index; |
41 |
|
|
42 |
3995 |
bool retVal = false; |
43 |
26711 |
for (unsigned i = 0; i < vars.size(); i++) |
44 |
|
{ |
45 |
45432 |
Node n = vars[i]; |
46 |
22716 |
if (d_ee->hasTerm(n)) |
47 |
|
{ |
48 |
34386 |
Node nr = d_ee->getRepresentative(n); |
49 |
17193 |
if (nr.isConst()) |
50 |
|
{ |
51 |
3620 |
subs.push_back(nr); |
52 |
7240 |
Trace("nl-subs") << "Basic substitution : " << n << " -> " << nr |
53 |
3620 |
<< std::endl; |
54 |
3620 |
exp[n].push_back(n.eqNode(nr)); |
55 |
3620 |
retVal = true; |
56 |
|
} |
57 |
|
else |
58 |
|
{ |
59 |
13573 |
rep_to_subs_index[nr].push_back(i); |
60 |
13573 |
subs.push_back(n); |
61 |
|
} |
62 |
|
} |
63 |
|
else |
64 |
|
{ |
65 |
5523 |
subs.push_back(n); |
66 |
|
} |
67 |
|
} |
68 |
|
|
69 |
|
// return true if the substitution is non-trivial |
70 |
7990 |
return retVal; |
71 |
|
} |
72 |
|
|
73 |
5798 |
bool NlExtTheoryCallback::isExtfReduced( |
74 |
|
int effort, Node n, Node on, std::vector<Node>& exp, ExtReducedId& id) |
75 |
|
{ |
76 |
5798 |
if (n != d_zero) |
77 |
|
{ |
78 |
3711 |
Kind k = n.getKind(); |
79 |
3711 |
if (k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND) |
80 |
|
{ |
81 |
2071 |
id = ExtReducedId::ARITH_SR_LINEAR; |
82 |
2071 |
return true; |
83 |
|
} |
84 |
1640 |
return false; |
85 |
|
} |
86 |
2087 |
Assert(n == d_zero); |
87 |
2087 |
id = ExtReducedId::ARITH_SR_ZERO; |
88 |
2087 |
if (on.getKind() == NONLINEAR_MULT) |
89 |
|
{ |
90 |
3746 |
Trace("nl-ext-zero-exp") |
91 |
1873 |
<< "Infer zero : " << on << " == " << n << std::endl; |
92 |
|
// minimize explanation if a substitution+rewrite results in zero |
93 |
1873 |
const std::set<Node> vars(on.begin(), on.end()); |
94 |
|
|
95 |
2046 |
for (unsigned i = 0, size = exp.size(); i < size; i++) |
96 |
|
{ |
97 |
4092 |
Trace("nl-ext-zero-exp") |
98 |
2046 |
<< " exp[" << i << "] = " << exp[i] << std::endl; |
99 |
2219 |
std::vector<Node> eqs; |
100 |
2046 |
if (exp[i].getKind() == EQUAL) |
101 |
|
{ |
102 |
2046 |
eqs.push_back(exp[i]); |
103 |
|
} |
104 |
|
else if (exp[i].getKind() == AND) |
105 |
|
{ |
106 |
|
for (const Node& ec : exp[i]) |
107 |
|
{ |
108 |
|
if (ec.getKind() == EQUAL) |
109 |
|
{ |
110 |
|
eqs.push_back(ec); |
111 |
|
} |
112 |
|
} |
113 |
|
} |
114 |
|
|
115 |
2219 |
for (unsigned j = 0; j < eqs.size(); j++) |
116 |
|
{ |
117 |
4265 |
for (unsigned r = 0; r < 2; r++) |
118 |
|
{ |
119 |
4092 |
if (eqs[j][r] == d_zero && vars.find(eqs[j][1 - r]) != vars.end()) |
120 |
|
{ |
121 |
3746 |
Trace("nl-ext-zero-exp") |
122 |
1873 |
<< "...single exp : " << eqs[j] << std::endl; |
123 |
1873 |
exp.clear(); |
124 |
1873 |
exp.push_back(eqs[j]); |
125 |
1873 |
return true; |
126 |
|
} |
127 |
|
} |
128 |
|
} |
129 |
|
} |
130 |
|
} |
131 |
214 |
return true; |
132 |
|
} |
133 |
|
|
134 |
|
} // namespace nl |
135 |
|
} // namespace arith |
136 |
|
} // namespace theory |
137 |
28191 |
} // namespace cvc5 |