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

Line Exec Source
1
/*********************                                                        */
2
/*! \file quant_util.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   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 quantifier util
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANT_UTIL_H
18
#define CVC4__THEORY__QUANT_UTIL_H
19
20
#include <iostream>
21
#include <map>
22
#include <vector>
23
24
#include "expr/node.h"
25
#include "theory/theory.h"
26
27
namespace CVC4 {
28
namespace theory {
29
30
/** Quantifiers utility
31
 *
32
 * This is a lightweight version of a quantifiers module that does not implement
33
 * methods for checking satisfiability.
34
 */
35
class QuantifiersUtil {
36
public:
37
36071
  QuantifiersUtil(){}
38
36059
  virtual ~QuantifiersUtil(){}
39
  /* reset
40
   * Called at the beginning of an instantiation round
41
   * Returns false if the reset failed. When reset fails, the utility should
42
   * have added a lemma via a call to d_qim.addPendingLemma.
43
   */
44
  virtual bool reset( Theory::Effort e ) = 0;
45
  /* Called for new quantifiers */
46
  virtual void registerQuantifier(Node q) = 0;
47
  /** Identify this module (for debugging, dynamic configuration, etc..) */
48
  virtual std::string identify() const = 0;
49
  /** Check complete?
50
   *
51
   * Returns false if the utility's reasoning was globally incomplete
52
   * (e.g. "sat" must be replaced with "incomplete").
53
   */
54
11030
  virtual bool checkComplete() { return true; }
55
};
56
57
class QuantPhaseReq
58
{
59
private:
60
  /** helper functions compute phase requirements */
61
  void computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs );
62
public:
63
  QuantPhaseReq(){}
64
  QuantPhaseReq( Node n, bool computeEq = false );
65
96155
  ~QuantPhaseReq(){}
66
  void initialize( Node n, bool computeEq );
67
  /** is phase required */
68
  bool isPhaseReq( Node lit ) { return d_phase_reqs.find( lit )!=d_phase_reqs.end(); }
69
  /** get phase requirement */
70
  bool getPhaseReq( Node lit ) { return d_phase_reqs.find( lit )==d_phase_reqs.end() ? false : d_phase_reqs[ lit ]; }
71
  /** phase requirements for each quantifier for each instantiation literal */
72
  std::map< Node, bool > d_phase_reqs;
73
  std::map< Node, bool > d_phase_reqs_equality;
74
  std::map< Node, Node > d_phase_reqs_equality_term;
75
76
  static void getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
77
  static void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
78
};
79
80
}
81
}
82
83
#endif /* CVC4__THEORY__QUANT_UTIL_H */