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 |
|
* Branch and bound for arithmetic |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/arith/branch_and_bound.h" |
17 |
|
|
18 |
|
#include "options/arith_options.h" |
19 |
|
#include "proof/eager_proof_generator.h" |
20 |
|
#include "proof/proof_node.h" |
21 |
|
#include "theory/arith/arith_utilities.h" |
22 |
|
#include "theory/rewriter.h" |
23 |
|
#include "theory/theory.h" |
24 |
|
|
25 |
|
using namespace cvc5::kind; |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace theory { |
29 |
|
namespace arith { |
30 |
|
|
31 |
9940 |
BranchAndBound::BranchAndBound(Env& env, |
32 |
|
ArithState& s, |
33 |
|
InferenceManager& im, |
34 |
|
PreprocessRewriteEq& ppre, |
35 |
9940 |
ProofNodeManager* pnm) |
36 |
|
: EnvObj(env), |
37 |
|
d_astate(s), |
38 |
|
d_im(im), |
39 |
|
d_ppre(ppre), |
40 |
19880 |
d_pfGen(new EagerProofGenerator(pnm, userContext())), |
41 |
29820 |
d_pnm(pnm) |
42 |
|
{ |
43 |
9940 |
} |
44 |
|
|
45 |
1141 |
TrustNode BranchAndBound::branchIntegerVariable(TNode var, Rational value) |
46 |
|
{ |
47 |
1141 |
TrustNode lem = TrustNode::null(); |
48 |
1141 |
NodeManager* nm = NodeManager::currentNM(); |
49 |
2282 |
Integer floor = value.floor(); |
50 |
1141 |
if (options().arith.brabTest) |
51 |
|
{ |
52 |
1137 |
Trace("integers") << "branch-round-and-bound enabled" << std::endl; |
53 |
2274 |
Integer ceil = value.ceiling(); |
54 |
2274 |
Rational f = value - floor; |
55 |
|
// Multiply by -1 to get abs value. |
56 |
2274 |
Rational c = (value - ceil) * (-1); |
57 |
2274 |
Integer nearest = (c > f) ? floor : ceil; |
58 |
|
|
59 |
|
// Prioritize trying a simple rounding of the real solution first, |
60 |
|
// it that fails, fall back on original branch and bound strategy. |
61 |
|
Node ub = |
62 |
2274 |
Rewriter::rewrite(nm->mkNode(LEQ, var, mkRationalNode(nearest - 1))); |
63 |
|
Node lb = |
64 |
2274 |
Rewriter::rewrite(nm->mkNode(GEQ, var, mkRationalNode(nearest + 1))); |
65 |
2274 |
Node right = nm->mkNode(OR, ub, lb); |
66 |
2274 |
Node rawEq = nm->mkNode(EQUAL, var, mkRationalNode(nearest)); |
67 |
2274 |
Node eq = Rewriter::rewrite(rawEq); |
68 |
|
// Also preprocess it before we send it out. This is important since |
69 |
|
// arithmetic may prefer eliminating equalities. |
70 |
2274 |
TrustNode teq; |
71 |
1137 |
if (Theory::theoryOf(eq) == THEORY_ARITH) |
72 |
|
{ |
73 |
1002 |
teq = d_ppre.ppRewriteEq(eq); |
74 |
1002 |
eq = teq.isNull() ? eq : teq.getNode(); |
75 |
|
} |
76 |
2274 |
Node literal = d_astate.getValuation().ensureLiteral(eq); |
77 |
1137 |
Trace("integers") << "eq: " << eq << "\nto: " << literal << std::endl; |
78 |
1137 |
d_im.requirePhase(literal, true); |
79 |
2274 |
Node l = nm->mkNode(OR, literal, right); |
80 |
1137 |
Trace("integers") << "l: " << l << std::endl; |
81 |
1137 |
if (proofsEnabled()) |
82 |
|
{ |
83 |
246 |
Node less = nm->mkNode(LT, var, mkRationalNode(nearest)); |
84 |
246 |
Node greater = nm->mkNode(GT, var, mkRationalNode(nearest)); |
85 |
|
// TODO (project #37): justify. Thread proofs through *ensureLiteral*. |
86 |
123 |
Debug("integers::pf") << "less: " << less << std::endl; |
87 |
123 |
Debug("integers::pf") << "greater: " << greater << std::endl; |
88 |
123 |
Debug("integers::pf") << "literal: " << literal << std::endl; |
89 |
123 |
Debug("integers::pf") << "eq: " << eq << std::endl; |
90 |
123 |
Debug("integers::pf") << "rawEq: " << rawEq << std::endl; |
91 |
246 |
Pf pfNotLit = d_pnm->mkAssume(literal.negate()); |
92 |
|
// rewrite notLiteral to notRawEq, using teq. |
93 |
|
Pf pfNotRawEq = |
94 |
123 |
literal == rawEq |
95 |
|
? pfNotLit |
96 |
|
: d_pnm->mkNode( |
97 |
|
PfRule::MACRO_SR_PRED_TRANSFORM, |
98 |
|
{pfNotLit, |
99 |
123 |
teq.getGenerator()->getProofFor(teq.getProven())}, |
100 |
369 |
{rawEq.negate()}); |
101 |
123 |
Pf pfBot = d_pnm->mkNode( |
102 |
|
PfRule::CONTRA, |
103 |
123 |
{d_pnm->mkNode(PfRule::ARITH_TRICHOTOMY, |
104 |
246 |
{d_pnm->mkAssume(less.negate()), pfNotRawEq}, |
105 |
369 |
{greater}), |
106 |
246 |
d_pnm->mkAssume(greater.negate())}, |
107 |
1107 |
{}); |
108 |
|
std::vector<Node> assumptions = { |
109 |
246 |
literal.negate(), less.negate(), greater.negate()}; |
110 |
|
// Proof of (not (and (not (= v i)) (not (< v i)) (not (> v i)))) |
111 |
246 |
Pf pfNotAnd = d_pnm->mkScope(pfBot, assumptions); |
112 |
123 |
Pf pfL = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, |
113 |
246 |
{d_pnm->mkNode(PfRule::NOT_AND, {pfNotAnd}, {})}, |
114 |
492 |
{l}); |
115 |
123 |
lem = d_pfGen->mkTrustNode(l, pfL); |
116 |
|
} |
117 |
|
else |
118 |
|
{ |
119 |
1014 |
lem = TrustNode::mkTrustLemma(l, nullptr); |
120 |
|
} |
121 |
|
} |
122 |
|
else |
123 |
|
{ |
124 |
8 |
Node ub = Rewriter::rewrite(nm->mkNode(LEQ, var, mkRationalNode(floor))); |
125 |
8 |
Node lb = ub.notNode(); |
126 |
4 |
if (proofsEnabled()) |
127 |
|
{ |
128 |
|
lem = |
129 |
|
d_pfGen->mkTrustNode(nm->mkNode(OR, ub, lb), PfRule::SPLIT, {}, {ub}); |
130 |
|
} |
131 |
|
else |
132 |
|
{ |
133 |
4 |
lem = TrustNode::mkTrustLemma(nm->mkNode(OR, ub, lb), nullptr); |
134 |
|
} |
135 |
|
} |
136 |
|
|
137 |
1141 |
Trace("integers") << "integers: branch & bound: " << lem << std::endl; |
138 |
2282 |
return lem; |
139 |
|
} |
140 |
|
|
141 |
1141 |
bool BranchAndBound::proofsEnabled() const { return d_pnm != nullptr; } |
142 |
|
|
143 |
|
} // namespace arith |
144 |
|
} // namespace theory |
145 |
29574 |
} // namespace cvc5 |