GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/cegqi/ceg_dt_instantiator.h Lines: 3 3 100.0 %
Date: 2021-03-22 Branches: 2 4 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ceg_dt_instantiator.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 ceg_dt_instantiator
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
18
#define CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
19
20
#include "expr/node.h"
21
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
22
23
namespace CVC4 {
24
namespace theory {
25
namespace quantifiers {
26
27
/** Datatypes Instantiator
28
 *
29
 * This class implements a selection function for datatypes based on solving
30
 * for occurrences of variables in subfields of datatypes.
31
 */
32
class DtInstantiator : public Instantiator
33
{
34
 public:
35
35
  DtInstantiator(TypeNode tn) : Instantiator(tn) {}
36
70
  virtual ~DtInstantiator() {}
37
  /** reset */
38
  void reset(CegInstantiator* ci,
39
             SolvedForm& sf,
40
             Node pv,
41
             CegInstEffort effort) override;
42
  /** this instantiator implements hasProcessEqualTerm */
43
  bool hasProcessEqualTerm(CegInstantiator* ci,
44
                           SolvedForm& sf,
45
                           Node pv,
46
                           CegInstEffort effort) override;
47
  /** process equal terms
48
   *
49
   * This tries to find an equality eqc[i] = eqc[j] such that pv can be solved
50
   * for (via solve_dt). If a solved form for pv can be found in this way, we
51
   * add the substitution for pv to sf and recurse.
52
   */
53
  bool processEqualTerms(CegInstantiator* ci,
54
                         SolvedForm& sf,
55
                         Node pv,
56
                         std::vector<Node>& eqc,
57
                         CegInstEffort effort) override;
58
  /** this instantiator processes equalities */
59
  bool hasProcessEquality(CegInstantiator* ci,
60
                          SolvedForm& sf,
61
                          Node pv,
62
                          CegInstEffort effort) override;
63
  /** process equality
64
   *
65
   * This tries to find a solved form for pv based on the equality
66
   * terms[0] = terms[1] via solve_dt. If a solved form for pv can be found in
67
   * this way, we add the substitution for pv to sf and recurse.
68
   */
69
  bool processEquality(CegInstantiator* ci,
70
                       SolvedForm& sf,
71
                       Node pv,
72
                       std::vector<TermProperties>& term_props,
73
                       std::vector<Node>& terms,
74
                       CegInstEffort effort) override;
75
  /** identify */
76
43
  std::string identify() const override { return "Dt"; }
77
78
 private:
79
  /** solve datatype
80
   *
81
   * If this method returns a non-null node ret, then v -> ret is a
82
   * solution for v in the equality a = b and ret does not contain v.
83
   *
84
   * For example, if cons( v, nil ) = cons( 5, nil ), this method returns 5.
85
   * For example, if cons( v, nil ) = L, this method returns head( L ).
86
   * For example, if cons( v, nil ) = cons( v+1, nil ), this method returns
87
   * the null node.
88
   */
89
  Node solve_dt(Node v, Node a, Node b, Node sa, Node sb);
90
};
91
92
}  // namespace quantifiers
93
}  // namespace theory
94
}  // namespace CVC4
95
96
#endif /* CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */