GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/decision/decision_engine.h Lines: 30 30 100.0 %
Date: 2021-03-22 Branches: 22 90 24.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file decision_engine.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Kshitij Bansal, Andrew Reynolds, Morgan Deters
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
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__DECISION__DECISION_ENGINE_H
20
#define CVC4__DECISION__DECISION_ENGINE_H
21
22
#include "base/output.h"
23
#include "context/cdo.h"
24
#include "decision/decision_strategy.h"
25
#include "expr/node.h"
26
#include "prop/cnf_stream.h"
27
#include "prop/sat_solver.h"
28
#include "prop/sat_solver_types.h"
29
#include "util/result.h"
30
31
using namespace CVC4::prop;
32
using namespace CVC4::decision;
33
34
namespace CVC4 {
35
36
class DecisionEngine {
37
38
  // PropEngine* d_propEngine;
39
  CnfStream* d_cnfStream;
40
  CDCLTSatSolverInterface* d_satSolver;
41
42
  context::Context* d_satContext;
43
  context::UserContext* d_userContext;
44
45
  // Does decision engine know the answer?
46
  context::CDO<SatValue> d_result;
47
48
  // Disable creating decision engine without required parameters
49
  DecisionEngine();
50
51
  // init/shutdown state
52
  unsigned d_engineState;    // 0=pre-init; 1=init,pre-shutdown; 2=shutdown
53
  /** Pointer to resource manager for associated SmtEngine */
54
  ResourceManager* d_resourceManager;
55
56
 public:
57
  // Necessary functions
58
59
  /** Constructor */
60
  DecisionEngine(context::Context* sc,
61
                 context::UserContext* uc,
62
                 ResourceManager* rm);
63
64
  /** Destructor, currently does nothing */
65
18048
  ~DecisionEngine() {
66
9024
    Trace("decision") << "Destroying decision engine" << std::endl;
67
9024
  }
68
69
9027
  void setSatSolver(CDCLTSatSolverInterface* ss)
70
  {
71
    // setPropEngine should not be called more than once
72
9027
    Assert(d_satSolver == NULL);
73
9027
    Assert(ss != NULL);
74
9027
    d_satSolver = ss;
75
9027
  }
76
77
9027
  void setCnfStream(CnfStream* cs) {
78
    // setPropEngine should not be called more than once
79
9027
    Assert(d_cnfStream == NULL);
80
9027
    Assert(cs != NULL);
81
9027
    d_cnfStream = cs;
82
9027
  }
83
84
  /* Enables decision strategy based on options. */
85
  void init();
86
87
  /**
88
   * This is called by SmtEngine, at shutdown time, just before
89
   * destruction.  It is important because there are destruction
90
   * ordering issues between some parts of the system.
91
   */
92
  void shutdown();
93
94
  // Interface for External World to use our services
95
96
  /** Gets the next decision based on strategies that are enabled */
97
  SatLiteral getNext(bool& stopSearch);
98
99
  /** Is the DecisionEngine in a state where it has solved everything? */
100
64809
  bool isDone() {
101
129618
    Trace("decision") << "DecisionEngine::isDone() returning "
102
129618
                      << (d_result != SAT_VALUE_UNKNOWN)
103
129618
                      << (d_result != SAT_VALUE_UNKNOWN ? "true" : "false")
104
64809
                      << std::endl;
105
64809
    return (d_result != SAT_VALUE_UNKNOWN);
106
  }
107
108
  /** */
109
  Result getResult() {
110
    switch(d_result.get()) {
111
    case SAT_VALUE_TRUE: return Result(Result::SAT);
112
    case SAT_VALUE_FALSE: return Result(Result::UNSAT);
113
    case SAT_VALUE_UNKNOWN: return Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
114
    default: Assert(false) << "d_result is garbage";
115
    }
116
    return Result();
117
  }
118
119
  /** */
120
39155
  void setResult(SatValue val) {
121
39155
    d_result = val;
122
39155
  }
123
124
  // External World helping us help the Strategies
125
126
  /**
127
   * Notify this class that assertion is an (input) assertion, not corresponding
128
   * to a skolem definition.
129
   */
130
  void addAssertion(TNode assertion);
131
  /**
132
   * Notify this class  that lem is the skolem definition for skolem, which is
133
   * a part of the current assertions.
134
   */
135
  void addSkolemDefinition(TNode lem, TNode skolem);
136
137
  // Interface for Strategies to use stuff stored in Decision Engine
138
  // (which was possibly requested by them on initialization)
139
140
  // Interface for Strategies to get information about External World
141
142
40247314
  bool hasSatLiteral(TNode n) {
143
40247314
    return d_cnfStream->hasLiteral(n);
144
  }
145
39564256
  SatLiteral getSatLiteral(TNode n) {
146
39564256
    return d_cnfStream->getLiteral(n);
147
  }
148
38932036
  SatValue getSatValue(SatLiteral l) {
149
38932036
    return d_satSolver->value(l);
150
  }
151
38932036
  SatValue getSatValue(TNode n) {
152
38932036
    return getSatValue(getSatLiteral(n));
153
  }
154
  Node getNode(SatLiteral l) {
155
    return d_cnfStream->getNode(l);
156
  }
157
158
 private:
159
  /** The ITE decision strategy we have allocated */
160
  std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy;
161
};/* DecisionEngine class */
162
163
}/* CVC4 namespace */
164
165
#endif /* CVC4__DECISION__DECISION_ENGINE_H */