GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/decision/decision_engine.cpp Lines: 40 42 95.2 %
Date: 2021-03-22 Branches: 54 154 35.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file decision_engine.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Kshitij Bansal, Aina Niemetz, Andrew Reynolds
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Decision engine
13
 **
14
 ** Decision engine
15
 **/
16
#include "decision/decision_engine.h"
17
18
#include "decision/decision_attributes.h"
19
#include "decision/justification_heuristic.h"
20
#include "expr/node.h"
21
#include "options/decision_options.h"
22
#include "options/smt_options.h"
23
#include "util/resource_manager.h"
24
25
using namespace std;
26
27
namespace CVC4 {
28
29
9027
DecisionEngine::DecisionEngine(context::Context* sc,
30
                               context::UserContext* uc,
31
9027
                               ResourceManager* rm)
32
    : d_cnfStream(nullptr),
33
      d_satSolver(nullptr),
34
      d_satContext(sc),
35
      d_userContext(uc),
36
      d_result(sc, SAT_VALUE_UNKNOWN),
37
      d_engineState(0),
38
      d_resourceManager(rm),
39
9027
      d_enabledITEStrategy(nullptr)
40
{
41
9027
  Trace("decision") << "Creating decision engine" << std::endl;
42
9027
}
43
44
9027
void DecisionEngine::init()
45
{
46
9027
  Assert(d_engineState == 0);
47
9027
  d_engineState = 1;
48
49
9027
  Trace("decision-init") << "DecisionEngine::init()" << std::endl;
50
18054
  Trace("decision-init") << " * options->decisionMode: "
51
61592
                         << options::decisionMode() << std:: endl;
52
18054
  Trace("decision-init") << " * options->decisionStopOnly: "
53
2537894
                         << options::decisionStopOnly() << std::endl;
54
55
9027
  if (options::decisionMode() == options::DecisionMode::JUSTIFICATION)
56
  {
57
12980
    d_enabledITEStrategy.reset(new decision::JustificationHeuristic(
58
6490
        this, d_userContext, d_satContext));
59
  }
60
9027
}
61
62
9024
void DecisionEngine::shutdown()
63
{
64
9024
  Trace("decision") << "Shutting down decision engine" << std::endl;
65
66
9024
  Assert(d_engineState == 1);
67
9024
  d_engineState = 2;
68
9024
  d_enabledITEStrategy.reset(nullptr);
69
9024
}
70
71
2510897
SatLiteral DecisionEngine::getNext(bool& stopSearch)
72
{
73
2510897
  d_resourceManager->spendResource(ResourceManager::Resource::DecisionStep);
74
2510897
  Assert(d_cnfStream != nullptr)
75
      << "Forgot to set cnfStream for decision engine?";
76
2510897
  Assert(d_satSolver != nullptr)
77
      << "Forgot to set satSolver for decision engine?";
78
79
2510897
  return d_enabledITEStrategy == nullptr
80
             ? undefSatLiteral
81
2510897
             : d_enabledITEStrategy->getNext(stopSearch);
82
}
83
84
443588
void DecisionEngine::addAssertion(TNode assertion)
85
{
86
  // new assertions, reset whatever result we knew
87
443588
  d_result = SAT_VALUE_UNKNOWN;
88
443588
  if (d_enabledITEStrategy != nullptr)
89
  {
90
257064
    d_enabledITEStrategy->addAssertion(assertion);
91
  }
92
443588
}
93
94
29563
void DecisionEngine::addSkolemDefinition(TNode lem, TNode skolem)
95
{
96
  // new assertions, reset whatever result we knew
97
29563
  d_result = SAT_VALUE_UNKNOWN;
98
29563
  if (d_enabledITEStrategy != nullptr)
99
  {
100
20634
    d_enabledITEStrategy->addSkolemDefinition(lem, skolem);
101
  }
102
29563
}
103
104
344246582
}/* CVC4 namespace */