GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/fmf/first_order_model_fmc.cpp Lines: 69 69 100.0 %
Date: 2021-03-22 Branches: 124 254 48.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file first_order_model_fmc.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 first order model for full model check
13
 **/
14
15
#include "theory/quantifiers/fmf/first_order_model_fmc.h"
16
17
#include "theory/quantifiers/fmf/full_model_check.h"
18
#include "theory/rewriter.h"
19
20
using namespace CVC4::kind;
21
22
namespace CVC4 {
23
namespace theory {
24
namespace quantifiers {
25
namespace fmcheck {
26
27
824
FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersState& qs,
28
                                       QuantifiersRegistry& qr,
29
                                       TermRegistry& tr,
30
824
                                       std::string name)
31
824
    : FirstOrderModel(qs, qr, tr, name)
32
{
33
824
}
34
35
2472
FirstOrderModelFmc::~FirstOrderModelFmc()
36
{
37
1768
  for (std::pair<const Node, Def*>& d : d_models)
38
  {
39
944
    delete d.second;
40
  }
41
1648
}
42
43
3176
void FirstOrderModelFmc::processInitialize(bool ispre)
44
{
45
3176
  if (!ispre)
46
  {
47
1588
    return;
48
  }
49
9052
  for (std::pair<const Node, Def*>& d : d_models)
50
  {
51
7464
    d.second->reset();
52
  }
53
}
54
55
162745
void FirstOrderModelFmc::processInitializeModelForTerm(Node n)
56
{
57
162745
  if (n.getKind() == APPLY_UF)
58
  {
59
    // cannot be a bound variable
60
62186
    Node op = n.getOperator();
61
31093
    if (op.getKind() != BOUND_VARIABLE)
62
    {
63
31093
      if (d_models.find(op) == d_models.end())
64
      {
65
944
        d_models[op] = new Def;
66
      }
67
    }
68
  }
69
162745
}
70
71
2020579
bool FirstOrderModelFmc::isStar(Node n)
72
{
73
2020579
  return n.getAttribute(IsStarAttribute());
74
}
75
76
787200
Node FirstOrderModelFmc::getStar(TypeNode tn)
77
{
78
787200
  std::map<TypeNode, Node>::iterator it = d_type_star.find(tn);
79
787200
  if (it != d_type_star.end())
80
  {
81
786527
    return it->second;
82
  }
83
  Node st = NodeManager::currentNM()->mkSkolem(
84
1346
      "star", tn, "skolem created for full-model checking");
85
673
  d_type_star[tn] = st;
86
673
  st.setAttribute(IsStarAttribute(), true);
87
673
  return st;
88
}
89
90
8408
Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix)
91
{
92
8408
  Trace("fmc-model") << "Get function value for " << op << std::endl;
93
8408
  NodeManager* nm = NodeManager::currentNM();
94
16816
  TypeNode type = op.getType();
95
16816
  std::vector<Node> vars;
96
22049
  for (size_t i = 0, nargs = type.getNumChildren() - 1; i < nargs; i++)
97
  {
98
27282
    std::stringstream ss;
99
13641
    ss << argPrefix << (i + 1);
100
27282
    Node b = nm->mkBoundVar(ss.str(), type[i]);
101
13641
    vars.push_back(b);
102
  }
103
16816
  Node boundVarList = nm->mkNode(BOUND_VAR_LIST, vars);
104
16816
  Node curr;
105
8408
  Def* odef = d_models[op];
106
28160
  for (size_t i = 0, ncond = odef->d_cond.size(); i < ncond; i++)
107
  {
108
19752
    size_t ii = (ncond - 1) - i;
109
39504
    Node v = odef->d_value[ii];
110
19752
    Trace("fmc-model-func") << "Value is : " << v << std::endl;
111
19752
    Assert(v.isConst());
112
19752
    if (curr.isNull())
113
    {
114
8408
      Trace("fmc-model-func") << "base : " << v << std::endl;
115
8408
      curr = v;
116
    }
117
    else
118
    {
119
      // make the condition
120
22688
      Node cond = odef->d_cond[ii];
121
11344
      Trace("fmc-model-func") << "...cond : " << cond << std::endl;
122
22688
      std::vector<Node> children;
123
32585
      for (size_t j = 0, nchild = cond.getNumChildren(); j < nchild; j++)
124
      {
125
42482
        TypeNode tn = vars[j].getType();
126
21241
        if (!isStar(cond[j]))
127
        {
128
42482
          Node c = getRepresentative(cond[j]);
129
21241
          c = getRepresentative(c);
130
21241
          children.push_back(nm->mkNode(EQUAL, vars[j], c));
131
        }
132
      }
133
11344
      Assert(!children.empty());
134
22688
      Node cc = nm->mkAnd(children);
135
136
22688
      Trace("fmc-model-func")
137
11344
          << "condition : " << cc << ", value : " << v << std::endl;
138
11344
      curr = nm->mkNode(ITE, cc, v, curr);
139
    }
140
  }
141
8408
  Trace("fmc-model") << "Made " << curr << " for " << op << std::endl;
142
8408
  curr = Rewriter::rewrite(curr);
143
16816
  return nm->mkNode(LAMBDA, boundVarList, curr);
144
}
145
146
}  // namespace fmcheck
147
}  // namespace quantifiers
148
}  // namespace theory
149
26676
}  // namespace CVC4