1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Yancheng Ou, Michael Chang |
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 |
|
* Optimizer for Integer type. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "omt/integer_optimizer.h" |
17 |
|
|
18 |
|
#include "options/smt_options.h" |
19 |
|
#include "smt/smt_engine.h" |
20 |
|
|
21 |
|
using namespace cvc5::smt; |
22 |
|
namespace cvc5::omt { |
23 |
|
|
24 |
8 |
OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker, |
25 |
|
TNode target, |
26 |
|
bool isMinimize) |
27 |
|
{ |
28 |
|
// linear search for integer goal |
29 |
|
// the smt engine to which we send intermediate queries |
30 |
|
// for the linear search. |
31 |
8 |
NodeManager* nm = optChecker->getNodeManager(); |
32 |
|
|
33 |
16 |
Result intermediateSatResult = optChecker->checkSat(); |
34 |
|
// Model-value of objective (used in optimization loop) |
35 |
16 |
Node value; |
36 |
8 |
if (intermediateSatResult.isUnknown()) |
37 |
|
{ |
38 |
|
return OptimizationResult(OptimizationResult::UNKNOWN, value); |
39 |
|
} |
40 |
8 |
if (intermediateSatResult.isSat() == Result::UNSAT) |
41 |
|
{ |
42 |
2 |
return OptimizationResult(OptimizationResult::UNSAT, value); |
43 |
|
} |
44 |
|
// asserts objective > old_value (used in optimization loop) |
45 |
12 |
Node increment; |
46 |
6 |
Kind incrementalOperator = kind::NULL_EXPR; |
47 |
6 |
if (isMinimize) |
48 |
|
{ |
49 |
|
// if objective is minimize, |
50 |
|
// then assert optimization_target < current_model_value |
51 |
4 |
incrementalOperator = kind::LT; |
52 |
|
} |
53 |
|
else |
54 |
|
{ |
55 |
|
// if objective is maximize, |
56 |
|
// then assert optimization_target > current_model_value |
57 |
2 |
incrementalOperator = kind::GT; |
58 |
|
} |
59 |
|
// Workhorse of linear search: |
60 |
|
// This loop will keep incrmenting/decrementing the objective until unsat |
61 |
|
// When unsat is hit, |
62 |
|
// the optimized value is the model value just before the unsat call |
63 |
410 |
while (intermediateSatResult.isSat() == Result::SAT) |
64 |
|
{ |
65 |
202 |
value = optChecker->getValue(target); |
66 |
202 |
Assert(!value.isNull()); |
67 |
202 |
increment = nm->mkNode(incrementalOperator, target, value); |
68 |
202 |
optChecker->assertFormula(increment); |
69 |
202 |
intermediateSatResult = optChecker->checkSat(); |
70 |
|
} |
71 |
6 |
return OptimizationResult(OptimizationResult::OPTIMAL, value); |
72 |
|
} |
73 |
|
|
74 |
4 |
OptimizationResult OMTOptimizerInteger::minimize(SmtEngine* optChecker, |
75 |
|
TNode target) |
76 |
|
{ |
77 |
4 |
return this->optimize(optChecker, target, true); |
78 |
|
} |
79 |
4 |
OptimizationResult OMTOptimizerInteger::maximize(SmtEngine* optChecker, |
80 |
|
TNode target) |
81 |
|
{ |
82 |
4 |
return this->optimize(optChecker, target, false); |
83 |
|
} |
84 |
|
|
85 |
28191 |
} // namespace cvc5::omt |