1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Gereon Kremer, Aina Niemetz |
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 NlExt proof checker. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/arith/nl/ext/proof_checker.h" |
17 |
|
|
18 |
|
#include "expr/sequence.h" |
19 |
|
#include "theory/arith/arith_utilities.h" |
20 |
|
#include "theory/rewriter.h" |
21 |
|
|
22 |
|
using namespace cvc5::kind; |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
namespace theory { |
26 |
|
namespace arith { |
27 |
|
namespace nl { |
28 |
|
|
29 |
593 |
void ExtProofRuleChecker::registerTo(ProofChecker* pc) |
30 |
|
{ |
31 |
593 |
pc->registerChecker(PfRule::ARITH_MULT_SIGN, this); |
32 |
593 |
pc->registerChecker(PfRule::ARITH_MULT_TANGENT, this); |
33 |
593 |
} |
34 |
|
|
35 |
92 |
Node ExtProofRuleChecker::checkInternal(PfRule id, |
36 |
|
const std::vector<Node>& children, |
37 |
|
const std::vector<Node>& args) |
38 |
|
{ |
39 |
92 |
NodeManager* nm = NodeManager::currentNM(); |
40 |
184 |
auto zero = nm->mkConst<Rational>(0); |
41 |
184 |
auto one = nm->mkConst<Rational>(1); |
42 |
184 |
auto mone = nm->mkConst<Rational>(-1); |
43 |
184 |
auto pi = nm->mkNullaryOperator(nm->realType(), Kind::PI); |
44 |
184 |
auto mpi = nm->mkNode(Kind::MULT, mone, pi); |
45 |
92 |
Trace("nl-ext-checker") << "Checking " << id << std::endl; |
46 |
92 |
for (const auto& c : children) |
47 |
|
{ |
48 |
|
Trace("nl-ext-checker") << "\t" << c << std::endl; |
49 |
|
} |
50 |
92 |
if (id == PfRule::ARITH_MULT_SIGN) |
51 |
|
{ |
52 |
87 |
Assert(children.empty()); |
53 |
87 |
Assert(args.size() > 1); |
54 |
174 |
Node mon = args.back(); |
55 |
174 |
std::map<Node, int> exps; |
56 |
174 |
std::vector<Node> premise = args; |
57 |
87 |
premise.pop_back(); |
58 |
87 |
Assert(mon.getKind() == Kind::MULT |
59 |
|
|| mon.getKind() == Kind::NONLINEAR_MULT); |
60 |
310 |
for (const auto& v : mon) |
61 |
|
{ |
62 |
223 |
exps[v]++; |
63 |
|
} |
64 |
174 |
std::map<Node, int> signs; |
65 |
300 |
for (const auto& f : premise) |
66 |
|
{ |
67 |
223 |
if (f.getKind() == Kind::NOT) |
68 |
|
{ |
69 |
10 |
Assert(f[0].getKind() == Kind::EQUAL); |
70 |
10 |
Assert(f[0][1].isConst() && f[0][1].getConst<Rational>().isZero()); |
71 |
10 |
Assert(signs.find(f[0][0]) == signs.end()); |
72 |
10 |
signs.emplace(f[0][0], 0); |
73 |
10 |
continue; |
74 |
|
} |
75 |
203 |
Assert(f.getKind() == Kind::LT || f.getKind() == Kind::GT); |
76 |
203 |
Assert(f[1].isConst() && f[1].getConst<Rational>().isZero()); |
77 |
203 |
Assert(signs.find(f[0]) == signs.end()); |
78 |
203 |
signs.emplace(f[0], f.getKind() == Kind::LT ? -1 : 1); |
79 |
|
} |
80 |
87 |
int sign = 0; |
81 |
300 |
for (const auto& ve : exps) |
82 |
|
{ |
83 |
213 |
auto sit = signs.find(ve.first); |
84 |
213 |
Assert(sit != signs.end()); |
85 |
213 |
if (ve.second % 2 == 0) |
86 |
|
{ |
87 |
10 |
Assert(sit->second == 0); |
88 |
10 |
if (sign == 0) |
89 |
|
{ |
90 |
7 |
sign = 1; |
91 |
|
} |
92 |
|
} |
93 |
|
else |
94 |
|
{ |
95 |
203 |
Assert(sit->second != 0); |
96 |
203 |
if (sign == 0) |
97 |
|
{ |
98 |
80 |
sign = sit->second; |
99 |
|
} |
100 |
|
else |
101 |
|
{ |
102 |
123 |
sign *= sit->second; |
103 |
|
} |
104 |
|
} |
105 |
|
} |
106 |
87 |
switch (sign) |
107 |
|
{ |
108 |
34 |
case -1: |
109 |
|
return nm->mkNode( |
110 |
34 |
Kind::IMPLIES, nm->mkAnd(premise), nm->mkNode(Kind::GT, zero, mon)); |
111 |
|
case 0: |
112 |
|
return nm->mkNode(Kind::IMPLIES, |
113 |
|
nm->mkAnd(premise), |
114 |
|
nm->mkNode(Kind::DISTINCT, mon, zero)); |
115 |
53 |
case 1: |
116 |
|
return nm->mkNode( |
117 |
53 |
Kind::IMPLIES, nm->mkAnd(premise), nm->mkNode(Kind::GT, mon, zero)); |
118 |
|
default: Assert(false); return Node(); |
119 |
|
} |
120 |
|
} |
121 |
5 |
else if (id == PfRule::ARITH_MULT_TANGENT) |
122 |
|
{ |
123 |
5 |
Assert(children.empty()); |
124 |
5 |
Assert(args.size() == 6); |
125 |
5 |
Assert(args[0].getType().isReal()); |
126 |
5 |
Assert(args[1].getType().isReal()); |
127 |
5 |
Assert(args[2].getType().isReal()); |
128 |
5 |
Assert(args[3].getType().isReal()); |
129 |
5 |
Assert(args[4].getType().isReal()); |
130 |
5 |
Assert(args[5].isConst() && args[5].getKind() == Kind::CONST_RATIONAL |
131 |
|
&& args[5].getConst<Rational>().isIntegral()); |
132 |
10 |
Node t = args[0]; |
133 |
10 |
Node x = args[1]; |
134 |
10 |
Node y = args[2]; |
135 |
10 |
Node a = args[3]; |
136 |
10 |
Node b = args[4]; |
137 |
5 |
int sgn = args[5].getConst<Rational>().getNumerator().sgn(); |
138 |
5 |
Assert(sgn == -1 || sgn == 1); |
139 |
|
Node tplane = nm->mkNode(Kind::MINUS, |
140 |
20 |
nm->mkNode(Kind::PLUS, |
141 |
10 |
nm->mkNode(Kind::MULT, b, x), |
142 |
10 |
nm->mkNode(Kind::MULT, a, y)), |
143 |
20 |
nm->mkNode(Kind::MULT, a, b)); |
144 |
|
return nm->mkNode( |
145 |
|
Kind::EQUAL, |
146 |
10 |
nm->mkNode(sgn == -1 ? Kind::LEQ : Kind::GEQ, t, tplane), |
147 |
20 |
nm->mkNode( |
148 |
|
Kind::OR, |
149 |
20 |
nm->mkNode(Kind::AND, |
150 |
10 |
nm->mkNode(Kind::LEQ, x, a), |
151 |
10 |
nm->mkNode(sgn == -1 ? Kind::GEQ : Kind::LEQ, y, b)), |
152 |
20 |
nm->mkNode(Kind::AND, |
153 |
10 |
nm->mkNode(Kind::GEQ, x, a), |
154 |
25 |
nm->mkNode(sgn == -1 ? Kind::LEQ : Kind::GEQ, y, b)))); |
155 |
|
} |
156 |
|
return Node::null(); |
157 |
|
} |
158 |
|
|
159 |
|
} // namespace nl |
160 |
|
} // namespace arith |
161 |
|
} // namespace theory |
162 |
29577 |
} // namespace cvc5 |