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 |
15273 |
BranchAndBound::BranchAndBound(Env& env, |
32 |
|
ArithState& s, |
33 |
|
InferenceManager& im, |
34 |
|
PreprocessRewriteEq& ppre, |
35 |
15273 |
ProofNodeManager* pnm) |
36 |
|
: EnvObj(env), |
37 |
|
d_astate(s), |
38 |
|
d_im(im), |
39 |
|
d_ppre(ppre), |
40 |
30546 |
d_pfGen(new EagerProofGenerator(pnm, userContext())), |
41 |
45819 |
d_pnm(pnm) |
42 |
|
{ |
43 |
15273 |
} |
44 |
|
|
45 |
1301 |
TrustNode BranchAndBound::branchIntegerVariable(TNode var, Rational value) |
46 |
|
{ |
47 |
1301 |
TrustNode lem = TrustNode::null(); |
48 |
1301 |
NodeManager* nm = NodeManager::currentNM(); |
49 |
2602 |
Integer floor = value.floor(); |
50 |
1301 |
if (options().arith.brabTest) |
51 |
|
{ |
52 |
1297 |
Trace("integers") << "branch-round-and-bound enabled" << std::endl; |
53 |
2594 |
Integer ceil = value.ceiling(); |
54 |
2594 |
Rational f = value - floor; |
55 |
|
// Multiply by -1 to get abs value. |
56 |
2594 |
Rational c = (value - ceil) * (-1); |
57 |
2594 |
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 |
2594 |
Node ub = rewrite(nm->mkNode(LEQ, var, mkRationalNode(nearest - 1))); |
62 |
2594 |
Node lb = rewrite(nm->mkNode(GEQ, var, mkRationalNode(nearest + 1))); |
63 |
2594 |
Node right = nm->mkNode(OR, ub, lb); |
64 |
2594 |
Node rawEq = nm->mkNode(EQUAL, var, mkRationalNode(nearest)); |
65 |
2594 |
Node eq = rewrite(rawEq); |
66 |
|
// Also preprocess it before we send it out. This is important since |
67 |
|
// arithmetic may prefer eliminating equalities. |
68 |
2594 |
TrustNode teq; |
69 |
1297 |
if (Theory::theoryOf(eq) == THEORY_ARITH) |
70 |
|
{ |
71 |
1120 |
teq = d_ppre.ppRewriteEq(eq); |
72 |
1120 |
eq = teq.isNull() ? eq : teq.getNode(); |
73 |
|
} |
74 |
2594 |
Node literal = d_astate.getValuation().ensureLiteral(eq); |
75 |
1297 |
Trace("integers") << "eq: " << eq << "\nto: " << literal << std::endl; |
76 |
1297 |
d_im.requirePhase(literal, true); |
77 |
2594 |
Node l = nm->mkNode(OR, literal, right); |
78 |
1297 |
Trace("integers") << "l: " << l << std::endl; |
79 |
1297 |
if (proofsEnabled()) |
80 |
|
{ |
81 |
272 |
Node less = nm->mkNode(LT, var, mkRationalNode(nearest)); |
82 |
272 |
Node greater = nm->mkNode(GT, var, mkRationalNode(nearest)); |
83 |
|
// TODO (project #37): justify. Thread proofs through *ensureLiteral*. |
84 |
136 |
Debug("integers::pf") << "less: " << less << std::endl; |
85 |
136 |
Debug("integers::pf") << "greater: " << greater << std::endl; |
86 |
136 |
Debug("integers::pf") << "literal: " << literal << std::endl; |
87 |
136 |
Debug("integers::pf") << "eq: " << eq << std::endl; |
88 |
136 |
Debug("integers::pf") << "rawEq: " << rawEq << std::endl; |
89 |
272 |
Pf pfNotLit = d_pnm->mkAssume(literal.negate()); |
90 |
|
// rewrite notLiteral to notRawEq, using teq. |
91 |
|
Pf pfNotRawEq = |
92 |
136 |
literal == rawEq |
93 |
|
? pfNotLit |
94 |
14 |
: d_pnm->mkNode( |
95 |
|
PfRule::MACRO_SR_PRED_TRANSFORM, |
96 |
|
{pfNotLit, |
97 |
150 |
teq.getGenerator()->getProofFor(teq.getProven())}, |
98 |
436 |
{rawEq.negate()}); |
99 |
136 |
Pf pfBot = d_pnm->mkNode( |
100 |
|
PfRule::CONTRA, |
101 |
136 |
{d_pnm->mkNode(PfRule::ARITH_TRICHOTOMY, |
102 |
272 |
{d_pnm->mkAssume(less.negate()), pfNotRawEq}, |
103 |
408 |
{greater}), |
104 |
272 |
d_pnm->mkAssume(greater.negate())}, |
105 |
1224 |
{}); |
106 |
|
std::vector<Node> assumptions = { |
107 |
272 |
literal.negate(), less.negate(), greater.negate()}; |
108 |
|
// Proof of (not (and (not (= v i)) (not (< v i)) (not (> v i)))) |
109 |
272 |
Pf pfNotAnd = d_pnm->mkScope(pfBot, assumptions); |
110 |
136 |
Pf pfL = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, |
111 |
272 |
{d_pnm->mkNode(PfRule::NOT_AND, {pfNotAnd}, {})}, |
112 |
544 |
{l}); |
113 |
136 |
lem = d_pfGen->mkTrustNode(l, pfL); |
114 |
|
} |
115 |
|
else |
116 |
|
{ |
117 |
1161 |
lem = TrustNode::mkTrustLemma(l, nullptr); |
118 |
|
} |
119 |
|
} |
120 |
|
else |
121 |
|
{ |
122 |
8 |
Node ub = rewrite(nm->mkNode(LEQ, var, mkRationalNode(floor))); |
123 |
8 |
Node lb = ub.notNode(); |
124 |
4 |
if (proofsEnabled()) |
125 |
|
{ |
126 |
|
lem = |
127 |
|
d_pfGen->mkTrustNode(nm->mkNode(OR, ub, lb), PfRule::SPLIT, {}, {ub}); |
128 |
|
} |
129 |
|
else |
130 |
|
{ |
131 |
4 |
lem = TrustNode::mkTrustLemma(nm->mkNode(OR, ub, lb), nullptr); |
132 |
|
} |
133 |
|
} |
134 |
|
|
135 |
1301 |
Trace("integers") << "integers: branch & bound: " << lem << std::endl; |
136 |
2602 |
return lem; |
137 |
|
} |
138 |
|
|
139 |
1301 |
bool BranchAndBound::proofsEnabled() const { return d_pnm != nullptr; } |
140 |
|
|
141 |
|
} // namespace arith |
142 |
|
} // namespace theory |
143 |
31137 |
} // namespace cvc5 |