GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/decision/decision_strategy.h Lines: 8 8 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file decision_strategy.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Kshitij Bansal, Andrew Reynolds, Mathias Preiner
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 strategy
13
 **
14
 ** Decision strategy
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__DECISION__DECISION_STRATEGY_H
20
#define CVC4__DECISION__DECISION_STRATEGY_H
21
22
#include <vector>
23
24
#include "expr/node.h"
25
#include "prop/sat_solver_types.h"
26
#include "smt/term_formula_removal.h"
27
28
namespace CVC4 {
29
30
class DecisionEngine;
31
32
namespace context {
33
  class Context;
34
}/* CVC4::context namespace */
35
36
namespace decision {
37
38
class DecisionStrategy {
39
protected:
40
  DecisionEngine* d_decisionEngine;
41
public:
42
6490
  DecisionStrategy(DecisionEngine* de, context::Context *c) :
43
6490
    d_decisionEngine(de) {
44
6490
  }
45
46
6489
  virtual ~DecisionStrategy() { }
47
48
  virtual prop::SatLiteral getNext(bool&) = 0;
49
};/* class DecisionStrategy */
50
51
6489
class ITEDecisionStrategy : public DecisionStrategy {
52
public:
53
6490
  ITEDecisionStrategy(DecisionEngine* de, context::Context *c) :
54
6490
    DecisionStrategy(de, c) {
55
6490
  }
56
  /**
57
   * Add that assertion is an (input) assertion, not corresponding to a
58
   * skolem definition.
59
   */
60
  virtual void addAssertion(TNode assertion) = 0;
61
  /**
62
   * Add that lem is the skolem definition for skolem, which is a part of
63
   * the current assertions.
64
   */
65
  virtual void addSkolemDefinition(TNode lem, TNode skolem) = 0;
66
};/* class ITEDecisionStrategy */
67
68
}/* CVC4::decision namespace */
69
}/* CVC4 namespace */
70
71
#endif /* CVC4__DECISION__DECISION_STRATEGY_H */