1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
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 |
|
* Relational match generator class. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/ematching/relational_match_generator.h" |
17 |
|
|
18 |
|
#include "theory/quantifiers/term_util.h" |
19 |
|
#include "util/rational.h" |
20 |
|
|
21 |
|
using namespace cvc5::kind; |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
namespace theory { |
25 |
|
namespace quantifiers { |
26 |
|
namespace inst { |
27 |
|
|
28 |
10 |
RelationalMatchGenerator::RelationalMatchGenerator(Trigger* tparent, |
29 |
|
Node rtrigger, |
30 |
|
bool hasPol, |
31 |
10 |
bool pol) |
32 |
20 |
: InstMatchGenerator(tparent, Node::null()), |
33 |
|
d_vindex(-1), |
34 |
|
d_hasPol(hasPol), |
35 |
|
d_pol(pol), |
36 |
30 |
d_counter(0) |
37 |
|
{ |
38 |
10 |
Assert((rtrigger.getKind() == EQUAL && rtrigger[0].getType().isReal()) |
39 |
|
|| rtrigger.getKind() == GEQ); |
40 |
20 |
Trace("relational-match-gen") |
41 |
10 |
<< "Relational trigger: " << rtrigger << ", hasPol/pol = " << hasPol |
42 |
10 |
<< "/" << pol << std::endl; |
43 |
10 |
for (size_t i = 0; i < 2; i++) |
44 |
|
{ |
45 |
10 |
if (rtrigger[i].getKind() == INST_CONSTANT) |
46 |
|
{ |
47 |
10 |
d_var = rtrigger[i]; |
48 |
10 |
d_vindex = d_var.getAttribute(InstVarNumAttribute()); |
49 |
10 |
d_rhs = rtrigger[1 - i]; |
50 |
10 |
Assert(!quantifiers::TermUtil::hasInstConstAttr(d_rhs)); |
51 |
10 |
Kind k = rtrigger.getKind(); |
52 |
10 |
d_rel = (i == 0 ? k : (k == GEQ ? LEQ : k)); |
53 |
10 |
break; |
54 |
|
} |
55 |
|
} |
56 |
20 |
Trace("relational-match-gen") << "...processed " << d_var << " (" << d_vindex |
57 |
10 |
<< ") " << d_rel << " " << d_rhs << std::endl; |
58 |
10 |
AlwaysAssert(!d_var.isNull()) |
59 |
|
<< "Failed to initialize RelationalMatchGenerator"; |
60 |
10 |
} |
61 |
|
|
62 |
10 |
bool RelationalMatchGenerator::reset(Node eqc) |
63 |
|
{ |
64 |
10 |
d_counter = 0; |
65 |
10 |
return true; |
66 |
|
} |
67 |
|
|
68 |
21 |
int RelationalMatchGenerator::getNextMatch(Node q, InstMatch& m) |
69 |
|
{ |
70 |
21 |
Trace("relational-match-gen") << "getNextMatch, rel match gen" << std::endl; |
71 |
|
// try (up to) two different terms |
72 |
42 |
Node s; |
73 |
42 |
Node rhs = d_rhs; |
74 |
21 |
bool rmPrev = m.get(d_vindex).isNull(); |
75 |
27 |
while (d_counter < 2) |
76 |
|
{ |
77 |
20 |
bool checkPol = false; |
78 |
20 |
if (d_counter == 0) |
79 |
|
{ |
80 |
10 |
checkPol = d_pol; |
81 |
|
} |
82 |
|
else |
83 |
|
{ |
84 |
10 |
Assert(d_counter == 1); |
85 |
10 |
if (d_hasPol) |
86 |
|
{ |
87 |
6 |
break; |
88 |
|
} |
89 |
|
// try the opposite polarity |
90 |
4 |
checkPol = !d_pol; |
91 |
|
} |
92 |
14 |
NodeManager* nm = NodeManager::currentNM(); |
93 |
|
// falsify ( d_var <d_rel> d_rhs ) = checkPol |
94 |
14 |
s = rhs; |
95 |
14 |
if (!checkPol) |
96 |
|
{ |
97 |
7 |
s = nm->mkNode(PLUS, s, nm->mkConst(Rational(d_rel == GEQ ? -1 : 1))); |
98 |
|
} |
99 |
14 |
d_counter++; |
100 |
28 |
Trace("relational-match-gen") |
101 |
14 |
<< "...try set " << s << " for " << checkPol << std::endl; |
102 |
14 |
if (m.set(d_qstate, d_vindex, s)) |
103 |
|
{ |
104 |
14 |
Trace("relational-match-gen") << "...success" << std::endl; |
105 |
14 |
int ret = continueNextMatch(q, m, InferenceId::UNKNOWN); |
106 |
14 |
if (ret > 0) |
107 |
|
{ |
108 |
11 |
Trace("relational-match-gen") << "...returned " << ret << std::endl; |
109 |
11 |
return ret; |
110 |
|
} |
111 |
3 |
Trace("relational-match-gen") << "...failed to gen inst" << std::endl; |
112 |
|
// failed |
113 |
3 |
if (rmPrev) |
114 |
|
{ |
115 |
3 |
m.d_vals[d_vindex] = Node::null(); |
116 |
|
} |
117 |
|
} |
118 |
|
} |
119 |
10 |
return -1; |
120 |
|
} |
121 |
|
|
122 |
|
} // namespace inst |
123 |
|
} // namespace quantifiers |
124 |
|
} // namespace theory |
125 |
31137 |
} // namespace cvc5 |