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