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-23 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 "expr/attribute.h"
18
#include "theory/quantifiers/fmf/full_model_check.h"
19
#include "theory/rewriter.h"
20
21
using namespace CVC4::kind;
22
23
namespace CVC4 {
24
namespace theory {
25
namespace quantifiers {
26
namespace fmcheck {
27
28
/**
29
 * Marks that a term represents the entire domain of quantified formula for
30
 * the finite model finding fmc algorithm.
31
 */
32
struct IsStarAttributeId
33
{
34
};
35
using IsStarAttribute = expr::Attribute<IsStarAttributeId, bool>;
36
37
826
FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersState& qs,
38
                                       QuantifiersRegistry& qr,
39
                                       TermRegistry& tr,
40
826
                                       std::string name)
41
826
    : FirstOrderModel(qs, qr, tr, name)
42
{
43
826
}
44
45
2478
FirstOrderModelFmc::~FirstOrderModelFmc()
46
{
47
1772
  for (std::pair<const Node, Def*>& d : d_models)
48
  {
49
946
    delete d.second;
50
  }
51
1652
}
52
53
3184
void FirstOrderModelFmc::processInitialize(bool ispre)
54
{
55
3184
  if (!ispre)
56
  {
57
1592
    return;
58
  }
59
9058
  for (std::pair<const Node, Def*>& d : d_models)
60
  {
61
7466
    d.second->reset();
62
  }
63
}
64
65
162901
void FirstOrderModelFmc::processInitializeModelForTerm(Node n)
66
{
67
162901
  if (n.getKind() == APPLY_UF)
68
  {
69
    // cannot be a bound variable
70
62202
    Node op = n.getOperator();
71
31101
    if (op.getKind() != BOUND_VARIABLE)
72
    {
73
31101
      if (d_models.find(op) == d_models.end())
74
      {
75
946
        d_models[op] = new Def;
76
      }
77
    }
78
  }
79
162901
}
80
81
2020631
bool FirstOrderModelFmc::isStar(Node n)
82
{
83
2020631
  return n.getAttribute(IsStarAttribute());
84
}
85
86
787236
Node FirstOrderModelFmc::getStar(TypeNode tn)
87
{
88
787236
  std::map<TypeNode, Node>::iterator it = d_type_star.find(tn);
89
787236
  if (it != d_type_star.end())
90
  {
91
786561
    return it->second;
92
  }
93
  Node st = NodeManager::currentNM()->mkSkolem(
94
1350
      "star", tn, "skolem created for full-model checking");
95
675
  d_type_star[tn] = st;
96
675
  st.setAttribute(IsStarAttribute(), true);
97
675
  return st;
98
}
99
100
8412
Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix)
101
{
102
8412
  Trace("fmc-model") << "Get function value for " << op << std::endl;
103
8412
  NodeManager* nm = NodeManager::currentNM();
104
16824
  TypeNode type = op.getType();
105
16824
  std::vector<Node> vars;
106
22057
  for (size_t i = 0, nargs = type.getNumChildren() - 1; i < nargs; i++)
107
  {
108
27290
    std::stringstream ss;
109
13645
    ss << argPrefix << (i + 1);
110
27290
    Node b = nm->mkBoundVar(ss.str(), type[i]);
111
13645
    vars.push_back(b);
112
  }
113
16824
  Node boundVarList = nm->mkNode(BOUND_VAR_LIST, vars);
114
16824
  Node curr;
115
8412
  Def* odef = d_models[op];
116
28168
  for (size_t i = 0, ncond = odef->d_cond.size(); i < ncond; i++)
117
  {
118
19756
    size_t ii = (ncond - 1) - i;
119
39512
    Node v = odef->d_value[ii];
120
19756
    Trace("fmc-model-func") << "Value is : " << v << std::endl;
121
19756
    Assert(v.isConst());
122
19756
    if (curr.isNull())
123
    {
124
8412
      Trace("fmc-model-func") << "base : " << v << std::endl;
125
8412
      curr = v;
126
    }
127
    else
128
    {
129
      // make the condition
130
22688
      Node cond = odef->d_cond[ii];
131
11344
      Trace("fmc-model-func") << "...cond : " << cond << std::endl;
132
22688
      std::vector<Node> children;
133
32585
      for (size_t j = 0, nchild = cond.getNumChildren(); j < nchild; j++)
134
      {
135
42482
        TypeNode tn = vars[j].getType();
136
21241
        if (!isStar(cond[j]))
137
        {
138
42482
          Node c = getRepresentative(cond[j]);
139
21241
          c = getRepresentative(c);
140
21241
          children.push_back(nm->mkNode(EQUAL, vars[j], c));
141
        }
142
      }
143
11344
      Assert(!children.empty());
144
22688
      Node cc = nm->mkAnd(children);
145
146
22688
      Trace("fmc-model-func")
147
11344
          << "condition : " << cc << ", value : " << v << std::endl;
148
11344
      curr = nm->mkNode(ITE, cc, v, curr);
149
    }
150
  }
151
8412
  Trace("fmc-model") << "Made " << curr << " for " << op << std::endl;
152
8412
  curr = Rewriter::rewrite(curr);
153
16824
  return nm->mkNode(LAMBDA, boundVarList, curr);
154
}
155
156
}  // namespace fmcheck
157
}  // namespace quantifiers
158
}  // namespace theory
159
26685
}  // namespace CVC4