GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/var_match_generator.cpp Lines: 31 32 96.9 %
Date: 2021-03-23 Branches: 52 100 52.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file var_match_generator.cpp
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 Implementation of variable match generator class
13
 **/
14
#include "theory/quantifiers/ematching/var_match_generator.h"
15
16
#include "theory/quantifiers/term_util.h"
17
#include "theory/quantifiers_engine.h"
18
#include "theory/rewriter.h"
19
20
using namespace CVC4::kind;
21
22
namespace CVC4 {
23
namespace theory {
24
namespace inst {
25
26
8
VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs(Trigger* tparent,
27
                                                     Node var,
28
8
                                                     Node subs)
29
16
    : InstMatchGenerator(tparent, Node::null()),
30
      d_var(var),
31
      d_subs(subs),
32
24
      d_rm_prev(false)
33
{
34
8
  d_children_types.push_back(d_var.getAttribute(InstVarNumAttribute()));
35
8
  d_var_type = d_var.getType();
36
8
}
37
38
8
bool VarMatchGeneratorTermSubs::reset(Node eqc)
39
{
40
8
  d_eq_class = eqc;
41
8
  return true;
42
}
43
44
8
int VarMatchGeneratorTermSubs::getNextMatch(Node q, InstMatch& m)
45
{
46
8
  int ret_val = -1;
47
8
  if (!d_eq_class.isNull())
48
  {
49
16
    Trace("var-trigger-matching") << "Matching " << d_eq_class << " against "
50
8
                                  << d_var << " in " << d_subs << std::endl;
51
11
    TNode tvar = d_var;
52
11
    Node s = d_subs.substitute(tvar, d_eq_class);
53
8
    s = Rewriter::rewrite(s);
54
16
    Trace("var-trigger-matching")
55
8
        << "...got " << s << ", " << s.getKind() << std::endl;
56
8
    d_eq_class = Node::null();
57
    // if( s.getType().isSubtypeOf( d_var_type ) ){
58
8
    d_rm_prev = m.get(d_children_types[0]).isNull();
59
8
    if (!m.set(d_qstate, d_children_types[0], s))
60
    {
61
      return -1;
62
    }
63
    else
64
    {
65
8
      ret_val = continueNextMatch(
66
          q, m, InferenceId::QUANTIFIERS_INST_E_MATCHING_VAR_GEN);
67
8
      if (ret_val > 0)
68
      {
69
5
        return ret_val;
70
      }
71
    }
72
  }
73
3
  if (d_rm_prev)
74
  {
75
3
    m.d_vals[d_children_types[0]] = Node::null();
76
3
    d_rm_prev = false;
77
  }
78
3
  return -1;
79
}
80
81
}  // namespace inst
82
}  // namespace theory
83
26685
}  // namespace CVC4