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 |
5208 |
NlExtTheoryCallback::NlExtTheoryCallback(eq::EqualityEngine* ee) : d_ee(ee) |
29 |
|
{ |
30 |
5208 |
d_zero = NodeManager::currentNM()->mkConst(Rational(0)); |
31 |
5208 |
} |
32 |
|
|
33 |
4397 |
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 |
8794 |
std::map<Node, std::vector<int>> rep_to_subs_index; |
41 |
|
|
42 |
4397 |
bool retVal = false; |
43 |
28640 |
for (unsigned i = 0; i < vars.size(); i++) |
44 |
|
{ |
45 |
48486 |
Node n = vars[i]; |
46 |
24243 |
if (d_ee->hasTerm(n)) |
47 |
|
{ |
48 |
36178 |
Node nr = d_ee->getRepresentative(n); |
49 |
18089 |
if (nr.isConst()) |
50 |
|
{ |
51 |
3882 |
subs.push_back(nr); |
52 |
7764 |
Trace("nl-subs") << "Basic substitution : " << n << " -> " << nr |
53 |
3882 |
<< std::endl; |
54 |
3882 |
exp[n].push_back(n.eqNode(nr)); |
55 |
3882 |
retVal = true; |
56 |
|
} |
57 |
|
else |
58 |
|
{ |
59 |
14207 |
rep_to_subs_index[nr].push_back(i); |
60 |
14207 |
subs.push_back(n); |
61 |
|
} |
62 |
|
} |
63 |
|
else |
64 |
|
{ |
65 |
6154 |
subs.push_back(n); |
66 |
|
} |
67 |
|
} |
68 |
|
|
69 |
|
// return true if the substitution is non-trivial |
70 |
8794 |
return retVal; |
71 |
|
} |
72 |
|
|
73 |
6779 |
bool NlExtTheoryCallback::isExtfReduced( |
74 |
|
int effort, Node n, Node on, std::vector<Node>& exp, ExtReducedId& id) |
75 |
|
{ |
76 |
6779 |
if (n != d_zero) |
77 |
|
{ |
78 |
4366 |
Kind k = n.getKind(); |
79 |
7932 |
if (k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND |
80 |
7158 |
&& k != POW2) |
81 |
|
{ |
82 |
2792 |
id = ExtReducedId::ARITH_SR_LINEAR; |
83 |
2792 |
return true; |
84 |
|
} |
85 |
1574 |
return false; |
86 |
|
} |
87 |
2413 |
Assert(n == d_zero); |
88 |
2413 |
id = ExtReducedId::ARITH_SR_ZERO; |
89 |
2413 |
if (on.getKind() == NONLINEAR_MULT) |
90 |
|
{ |
91 |
4444 |
Trace("nl-ext-zero-exp") |
92 |
2222 |
<< "Infer zero : " << on << " == " << n << std::endl; |
93 |
|
// minimize explanation if a substitution+rewrite results in zero |
94 |
2222 |
const std::set<Node> vars(on.begin(), on.end()); |
95 |
|
|
96 |
2282 |
for (unsigned i = 0, size = exp.size(); i < size; i++) |
97 |
|
{ |
98 |
4564 |
Trace("nl-ext-zero-exp") |
99 |
2282 |
<< " exp[" << i << "] = " << exp[i] << std::endl; |
100 |
2342 |
std::vector<Node> eqs; |
101 |
2282 |
if (exp[i].getKind() == EQUAL) |
102 |
|
{ |
103 |
2282 |
eqs.push_back(exp[i]); |
104 |
|
} |
105 |
|
else if (exp[i].getKind() == AND) |
106 |
|
{ |
107 |
|
for (const Node& ec : exp[i]) |
108 |
|
{ |
109 |
|
if (ec.getKind() == EQUAL) |
110 |
|
{ |
111 |
|
eqs.push_back(ec); |
112 |
|
} |
113 |
|
} |
114 |
|
} |
115 |
|
|
116 |
2342 |
for (unsigned j = 0; j < eqs.size(); j++) |
117 |
|
{ |
118 |
4624 |
for (unsigned r = 0; r < 2; r++) |
119 |
|
{ |
120 |
4564 |
if (eqs[j][r] == d_zero && vars.find(eqs[j][1 - r]) != vars.end()) |
121 |
|
{ |
122 |
4444 |
Trace("nl-ext-zero-exp") |
123 |
2222 |
<< "...single exp : " << eqs[j] << std::endl; |
124 |
2222 |
exp.clear(); |
125 |
2222 |
exp.push_back(eqs[j]); |
126 |
2222 |
return true; |
127 |
|
} |
128 |
|
} |
129 |
|
} |
130 |
|
} |
131 |
|
} |
132 |
191 |
return true; |
133 |
|
} |
134 |
|
|
135 |
|
} // namespace nl |
136 |
|
} // namespace arith |
137 |
|
} // namespace theory |
138 |
29502 |
} // namespace cvc5 |