GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/equality_query.h Lines: 2 2 100.0 %
Date: 2021-03-23 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file equality_query.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Tim King
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 Equality query class
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
18
#define CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
19
20
#include "context/cdo.h"
21
#include "context/context.h"
22
#include "expr/node.h"
23
#include "theory/quantifiers/quant_util.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace quantifiers {
28
29
class FirstOrderModel;
30
class QuantifiersState;
31
32
/** EqualityQuery class
33
 *
34
 * The main method of this class is the function
35
 * getInternalRepresentative, which is used by instantiation-based methods
36
 * that are agnostic with respect to choosing terms within an equivalence class.
37
 * Examples of such methods are finite model finding and enumerative
38
 * instantiation. Method getInternalRepresentative returns the "best"
39
 * representative based on the internal heuristic, which is currently based on
40
 * choosing the term that was previously chosen as a representative earliest.
41
 */
42
class EqualityQuery : public QuantifiersUtil
43
{
44
 public:
45
  EqualityQuery(QuantifiersState& qs, FirstOrderModel* m);
46
  virtual ~EqualityQuery();
47
48
  /** reset */
49
  bool reset(Theory::Effort e) override;
50
  /* Called for new quantifiers */
51
23483
  void registerQuantifier(Node q) override {}
52
  /** identify */
53
28265
  std::string identify() const override { return "EqualityQuery"; }
54
  /** gets the current best representative in the equivalence
55
   * class of a, based on some heuristic. Currently, the default heuristic
56
   * chooses terms that were previously chosen as representatives
57
   * on the earliest instantiation round.
58
   *
59
   * If q is non-null, then q/index is the quantified formula
60
   * and variable position that we are choosing for instantiation.
61
   *
62
   * This function avoids certain terms that are "ineligible" for instantiation.
63
   * If cbqi is active, we terms that contain instantiation constants
64
   * are ineligible. As a result, this function may return
65
   * Node::null() if all terms in the equivalence class of a
66
   * are ineligible.
67
   */
68
  Node getInternalRepresentative(Node a, Node q, size_t index);
69
70
 private:
71
  /** the quantifiers state */
72
  QuantifiersState& d_qstate;
73
  /** Pointer to the model */
74
  FirstOrderModel* d_model;
75
  /** quantifiers equality inference */
76
  context::CDO< unsigned > d_eqi_counter;
77
  /** internal representatives */
78
  std::map< TypeNode, std::map< Node, Node > > d_int_rep;
79
  /** rep score */
80
  std::map<Node, int32_t> d_rep_score;
81
  /** the number of times reset( e ) has been called */
82
  size_t d_reset_count;
83
  /** processInferences : will merge equivalence classes in master equality engine, if possible */
84
  bool processInferences( Theory::Effort e );
85
  /** node contains */
86
  Node getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache );
87
  /** get score */
88
  int32_t getRepScore(Node n, Node f, size_t index, TypeNode v_tn);
89
}; /* EqualityQuery */
90
91
}/* CVC4::theory::quantifiers namespace */
92
}/* CVC4::theory namespace */
93
}/* CVC4 namespace */
94
95
#endif /* CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */