GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/theory_quantifiers.h Lines: 1 3 33.3 %
Date: 2021-03-22 Branches: 0 2 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_quantifiers.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, 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 Theory of quantifiers.
13
 **
14
 ** Theory of quantifiers.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
20
#define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
21
22
#include "expr/node.h"
23
#include "theory/quantifiers/first_order_model.h"
24
#include "theory/quantifiers/proof_checker.h"
25
#include "theory/quantifiers/quantifiers_inference_manager.h"
26
#include "theory/quantifiers/quantifiers_registry.h"
27
#include "theory/quantifiers/quantifiers_rewriter.h"
28
#include "theory/quantifiers/quantifiers_state.h"
29
#include "theory/quantifiers/term_registry.h"
30
#include "theory/quantifiers_engine.h"
31
#include "theory/theory.h"
32
#include "theory/valuation.h"
33
34
namespace CVC4 {
35
namespace theory {
36
namespace quantifiers {
37
38
class TheoryQuantifiers : public Theory {
39
 public:
40
  TheoryQuantifiers(context::Context* c,
41
                    context::UserContext* u,
42
                    OutputChannel& out,
43
                    Valuation valuation,
44
                    const LogicInfo& logicInfo,
45
                    ProofNodeManager* pnm = nullptr);
46
  ~TheoryQuantifiers();
47
48
  //--------------------------------- initialization
49
  /** get the official theory rewriter of this theory */
50
  TheoryRewriter* getTheoryRewriter() override;
51
  /** finish initialization */
52
  void finishInit() override;
53
  /** needs equality engine */
54
  bool needsEqualityEngine(EeSetupInfo& esi) override;
55
  //--------------------------------- end initialization
56
57
  void preRegisterTerm(TNode n) override;
58
  void presolve() override;
59
  void ppNotifyAssertions(const std::vector<Node>& assertions) override;
60
  //--------------------------------- standard check
61
  /** Post-check, called after the fact queue of the theory is processed. */
62
  void postCheck(Effort level) override;
63
  /** Pre-notify fact, return true if processed. */
64
  bool preNotifyFact(TNode atom,
65
                     bool pol,
66
                     TNode fact,
67
                     bool isPrereg,
68
                     bool isInternal) override;
69
  //--------------------------------- end standard check
70
  /** Collect model values in m based on the relevant terms given by termSet */
71
  bool collectModelValues(TheoryModel* m,
72
                          const std::set<Node>& termSet) override;
73
8986
  void shutdown() override {}
74
  std::string identify() const override
75
  {
76
    return std::string("TheoryQuantifiers");
77
  }
78
  void setUserAttribute(const std::string& attr,
79
                        Node n,
80
                        std::vector<Node> node_values,
81
                        std::string str_value) override;
82
83
 private:
84
  /** The theory rewriter for this theory. */
85
  QuantifiersRewriter d_rewriter;
86
  /** The proof rule checker */
87
  QuantifiersProofRuleChecker d_qChecker;
88
  /** The quantifiers state */
89
  QuantifiersState d_qstate;
90
  /** The quantifiers registry */
91
  QuantifiersRegistry d_qreg;
92
  /** extended model object */
93
  std::unique_ptr<FirstOrderModel> d_qmodel;
94
  /** The term registry */
95
  TermRegistry d_treg;
96
  /** The quantifiers inference manager */
97
  QuantifiersInferenceManager d_qim;
98
  /** The quantifiers engine, which lives here */
99
  std::unique_ptr<QuantifiersEngine> d_qengine;
100
};/* class TheoryQuantifiers */
101
102
}/* CVC4::theory::quantifiers namespace */
103
}/* CVC4::theory namespace */
104
}/* CVC4 namespace */
105
106
#endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H */