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