1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Makai Mann, Gereon Kremer |
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 |
|
* Implementation of pow2 solver. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/arith/nl/pow2_solver.h" |
17 |
|
|
18 |
|
#include "options/arith_options.h" |
19 |
|
#include "options/smt_options.h" |
20 |
|
#include "preprocessing/passes/bv_to_int.h" |
21 |
|
#include "theory/arith/arith_msum.h" |
22 |
|
#include "theory/arith/arith_state.h" |
23 |
|
#include "theory/arith/arith_utilities.h" |
24 |
|
#include "theory/arith/inference_manager.h" |
25 |
|
#include "theory/arith/nl/nl_model.h" |
26 |
|
#include "theory/rewriter.h" |
27 |
|
#include "util/bitvector.h" |
28 |
|
|
29 |
|
using namespace cvc5::kind; |
30 |
|
|
31 |
|
namespace cvc5 { |
32 |
|
namespace theory { |
33 |
|
namespace arith { |
34 |
|
namespace nl { |
35 |
|
|
36 |
3429 |
Pow2Solver::Pow2Solver(Env& env, |
37 |
|
InferenceManager& im, |
38 |
|
ArithState& state, |
39 |
3429 |
NlModel& model) |
40 |
3429 |
: EnvObj(env), d_im(im), d_model(model), d_initRefine(userContext()) |
41 |
|
{ |
42 |
3429 |
NodeManager* nm = NodeManager::currentNM(); |
43 |
3429 |
d_false = nm->mkConst(false); |
44 |
3429 |
d_true = nm->mkConst(true); |
45 |
3429 |
d_zero = nm->mkConst(Rational(0)); |
46 |
3429 |
d_one = nm->mkConst(Rational(1)); |
47 |
3429 |
d_two = nm->mkConst(Rational(2)); |
48 |
3429 |
} |
49 |
|
|
50 |
3427 |
Pow2Solver::~Pow2Solver() {} |
51 |
|
|
52 |
1486 |
void Pow2Solver::initLastCall(const std::vector<Node>& assertions, |
53 |
|
const std::vector<Node>& false_asserts, |
54 |
|
const std::vector<Node>& xts) |
55 |
|
{ |
56 |
1486 |
d_pow2s.clear(); |
57 |
1486 |
Trace("pow2-mv") << "POW2 terms : " << std::endl; |
58 |
10388 |
for (const Node& a : xts) |
59 |
|
{ |
60 |
8902 |
Kind ak = a.getKind(); |
61 |
8902 |
if (ak != POW2) |
62 |
|
{ |
63 |
|
// don't care about other terms |
64 |
8877 |
continue; |
65 |
|
} |
66 |
25 |
d_pow2s.push_back(a); |
67 |
|
} |
68 |
1486 |
Trace("pow2") << "We have " << d_pow2s.size() << " pow2 terms." << std::endl; |
69 |
1486 |
} |
70 |
|
|
71 |
1486 |
void Pow2Solver::checkInitialRefine() |
72 |
|
{ |
73 |
1486 |
Trace("pow2-check") << "Pow2Solver::checkInitialRefine" << std::endl; |
74 |
1486 |
NodeManager* nm = NodeManager::currentNM(); |
75 |
1511 |
for (const Node& i : d_pow2s) |
76 |
|
{ |
77 |
25 |
if (d_initRefine.find(i) != d_initRefine.end()) |
78 |
|
{ |
79 |
|
// already sent initial axioms for i in this user context |
80 |
18 |
continue; |
81 |
|
} |
82 |
7 |
d_initRefine.insert(i); |
83 |
|
// initial refinement lemmas |
84 |
14 |
std::vector<Node> conj; |
85 |
|
// x>=0 -> x < pow2(x) |
86 |
14 |
Node xgeq0 = nm->mkNode(LEQ, d_zero, i[0]); |
87 |
14 |
Node xltpow2x = nm->mkNode(LT, i[0], i); |
88 |
7 |
conj.push_back(nm->mkNode(IMPLIES, xgeq0, xltpow2x)); |
89 |
14 |
Node lem = nm->mkAnd(conj); |
90 |
14 |
Trace("pow2-lemma") << "Pow2Solver::Lemma: " << lem << " ; INIT_REFINE" |
91 |
7 |
<< std::endl; |
92 |
7 |
d_im.addPendingLemma(lem, InferenceId::ARITH_NL_POW2_INIT_REFINE); |
93 |
|
} |
94 |
1486 |
} |
95 |
|
|
96 |
312 |
void Pow2Solver::sortPow2sBasedOnModel() |
97 |
|
{ |
98 |
|
struct |
99 |
|
{ |
100 |
2 |
bool operator()(Node a, Node b, NlModel& model) const |
101 |
|
{ |
102 |
4 |
return model.computeConcreteModelValue(a[0]) |
103 |
6 |
< model.computeConcreteModelValue(b[0]); |
104 |
|
} |
105 |
|
} modelSort; |
106 |
|
using namespace std::placeholders; |
107 |
312 |
std::sort( |
108 |
624 |
d_pow2s.begin(), d_pow2s.end(), std::bind(modelSort, _1, _2, d_model)); |
109 |
312 |
} |
110 |
|
|
111 |
312 |
void Pow2Solver::checkFullRefine() |
112 |
|
{ |
113 |
312 |
Trace("pow2-check") << "Pow2Solver::checkFullRefine" << std::endl; |
114 |
312 |
NodeManager* nm = NodeManager::currentNM(); |
115 |
312 |
sortPow2sBasedOnModel(); |
116 |
|
// add lemmas for each pow2 term |
117 |
318 |
for (uint64_t i = 0, size = d_pow2s.size(); i < size; i++) |
118 |
|
{ |
119 |
10 |
Node n = d_pow2s[i]; |
120 |
10 |
Node valPow2xAbstract = d_model.computeAbstractModelValue(n); |
121 |
10 |
Node valPow2xConcrete = d_model.computeConcreteModelValue(n); |
122 |
10 |
Node valXConcrete = d_model.computeConcreteModelValue(n[0]); |
123 |
6 |
if (Trace.isOn("pow2-check")) |
124 |
|
{ |
125 |
|
Trace("pow2-check") << "* " << i << ", value = " << valPow2xAbstract |
126 |
|
<< std::endl; |
127 |
|
Trace("pow2-check") << " actual " << valXConcrete << " = " |
128 |
|
<< valPow2xConcrete << std::endl; |
129 |
|
} |
130 |
8 |
if (valPow2xAbstract == valPow2xConcrete) |
131 |
|
{ |
132 |
2 |
Trace("pow2-check") << "...already correct" << std::endl; |
133 |
2 |
continue; |
134 |
|
} |
135 |
|
|
136 |
8 |
Integer x = valXConcrete.getConst<Rational>().getNumerator(); |
137 |
8 |
Integer pow2x = valPow2xAbstract.getConst<Rational>().getNumerator(); |
138 |
|
// add monotinicity lemmas |
139 |
5 |
for (uint64_t j = i + 1; j < size; j++) |
140 |
|
{ |
141 |
2 |
Node m = d_pow2s[j]; |
142 |
2 |
Node valPow2yAbstract = d_model.computeAbstractModelValue(m); |
143 |
2 |
Node valYConcrete = d_model.computeConcreteModelValue(m[0]); |
144 |
|
|
145 |
2 |
Integer y = valYConcrete.getConst<Rational>().getNumerator(); |
146 |
2 |
Integer pow2y = valPow2yAbstract.getConst<Rational>().getNumerator(); |
147 |
|
|
148 |
1 |
if (x < y && pow2x >= pow2y) |
149 |
|
{ |
150 |
2 |
Node assumption = nm->mkNode(LEQ, n[0], m[0]); |
151 |
2 |
Node conclusion = nm->mkNode(LEQ, n, m); |
152 |
2 |
Node lem = nm->mkNode(IMPLIES, assumption, conclusion); |
153 |
1 |
d_im.addPendingLemma( |
154 |
|
lem, InferenceId::ARITH_NL_POW2_MONOTONE_REFINE, nullptr, true); |
155 |
|
} |
156 |
|
} |
157 |
|
|
158 |
|
// triviality lemmas: pow2(x) = 0 whenever x < 0 |
159 |
4 |
if (x < 0 && pow2x != 0) |
160 |
|
{ |
161 |
4 |
Node assumption = nm->mkNode(LT, n[0], d_zero); |
162 |
4 |
Node conclusion = nm->mkNode(EQUAL, n, d_zero); |
163 |
4 |
Node lem = nm->mkNode(IMPLIES, assumption, conclusion); |
164 |
2 |
d_im.addPendingLemma( |
165 |
|
lem, InferenceId::ARITH_NL_POW2_TRIVIAL_CASE_REFINE, nullptr, true); |
166 |
|
} |
167 |
|
|
168 |
|
// Place holder for additional lemma schemas |
169 |
|
|
170 |
|
// End of additional lemma schemas |
171 |
|
|
172 |
|
// this is the most naive model-based schema based on model values |
173 |
8 |
Node lem = valueBasedLemma(n); |
174 |
8 |
Trace("pow2-lemma") << "Pow2Solver::Lemma: " << lem << " ; VALUE_REFINE" |
175 |
4 |
<< std::endl; |
176 |
|
// send the value lemma |
177 |
4 |
d_im.addPendingLemma( |
178 |
|
lem, InferenceId::ARITH_NL_POW2_VALUE_REFINE, nullptr, true); |
179 |
|
} |
180 |
312 |
} |
181 |
|
|
182 |
4 |
Node Pow2Solver::valueBasedLemma(Node i) |
183 |
|
{ |
184 |
4 |
Assert(i.getKind() == POW2); |
185 |
8 |
Node x = i[0]; |
186 |
|
|
187 |
8 |
Node valX = d_model.computeConcreteModelValue(x); |
188 |
|
|
189 |
4 |
NodeManager* nm = NodeManager::currentNM(); |
190 |
8 |
Node valC = nm->mkNode(POW2, valX); |
191 |
4 |
valC = Rewriter::rewrite(valC); |
192 |
|
|
193 |
4 |
Node lem = nm->mkNode(IMPLIES, x.eqNode(valX), i.eqNode(valC)); |
194 |
8 |
return lem; |
195 |
|
} |
196 |
|
|
197 |
|
} // namespace nl |
198 |
|
} // namespace arith |
199 |
|
} // namespace theory |
200 |
22746 |
} // namespace cvc5 |