GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/cegqi/nested_qe.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file nested_qe.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   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 Methods for counterexample-guided quantifier instantiation
13
 ** based on nested quantifier elimination.
14
 **/
15
16
#include "cvc4_private.h"
17
18
#ifndef CVC4__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H
19
#define CVC4__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H
20
21
#include <unordered_set>
22
23
#include "context/cdhashmap.h"
24
#include "expr/node.h"
25
26
namespace CVC4 {
27
namespace theory {
28
namespace quantifiers {
29
30
class NestedQe
31
{
32
  using NodeNodeMap = context::CDHashMap<Node, Node, NodeHashFunction>;
33
34
 public:
35
  NestedQe(context::UserContext* u);
36
30
  ~NestedQe() {}
37
  /**
38
   * Process quantified formula. If this returns true, then q was processed
39
   * via nested quantifier elimination (either during this call or previously
40
   * in this user context). If q was processed in this call, the lemma:
41
   *   (= q qqe)
42
   * is added to lem, where qqe is the result of nested quantifier elimination
43
   * on q.
44
   */
45
  bool process(Node q, std::vector<Node>& lems);
46
  /**
47
   * Have we processed q using the above method?
48
   */
49
  bool hasProcessed(Node q) const;
50
51
  /**
52
   * Get nested quantification. Returns true if q has nested quantifiers.
53
   * Adds each nested quantifier in the body of q to nqs.
54
   */
55
  static bool getNestedQuantification(
56
      Node q, std::unordered_set<Node, NodeHashFunction>& nqs);
57
  /**
58
   * Does quantified formula q have nested quantification?
59
   */
60
  static bool hasNestedQuantification(Node q);
61
  /**
62
   * Do nested quantifier elimination. Returns a formula that is equivalent to
63
   * q and has no nested quantification. If keepTopLevel is false, then the
64
   * returned formula is quantifier-free. Otherwise, it is a quantified formula
65
   * with no nested quantification.
66
   */
67
  static Node doNestedQe(Node q, bool keepTopLevel = false);
68
  /**
69
   * Run quantifier elimination on quantified formula q, where q has no nested
70
   * quantification. This method invokes a subsolver for performing quantifier
71
   * elimination.
72
   */
73
  static Node doQe(Node q);
74
75
 private:
76
  /**
77
   * Mapping from quantified formulas q to the result of doNestedQe(q, true).
78
   */
79
  NodeNodeMap d_qnqe;
80
};
81
82
}  // namespace quantifiers
83
}  // namespace theory
84
}  // namespace CVC4
85
86
#endif