GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/model_core_builder.cpp Lines: 1 50 2.0 %
Date: 2021-03-22 Branches: 2 182 1.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file model_core_builder.cpp
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 Implementation of utility for building model cores
13
 **/
14
15
#include "smt/model_core_builder.h"
16
17
#include "theory/subs_minimize.h"
18
19
using namespace CVC4::kind;
20
21
namespace CVC4 {
22
23
bool ModelCoreBuilder::setModelCore(const std::vector<Node>& assertions,
24
                                    theory::TheoryModel* m,
25
                                    options::ModelCoresMode mode)
26
{
27
  if (Trace.isOn("model-core"))
28
  {
29
    Trace("model-core") << "Compute model core, assertions:" << std::endl;
30
    for (const Node& a : assertions)
31
    {
32
      Trace("model-core") << "  " << a << std::endl;
33
    }
34
  }
35
36
  // convert to nodes
37
  NodeManager* nm = NodeManager::currentNM();
38
39
  Node formula = nm->mkAnd(assertions);
40
  std::vector<Node> vars;
41
  std::vector<Node> subs;
42
  Trace("model-core") << "Assignments: " << std::endl;
43
  std::unordered_set<TNode, TNodeHashFunction> visited;
44
  std::vector<TNode> visit;
45
  TNode cur;
46
  visit.push_back(formula);
47
  do
48
  {
49
    cur = visit.back();
50
    visit.pop_back();
51
    if (visited.find(cur) == visited.end())
52
    {
53
      visited.insert(cur);
54
      if (cur.isVar())
55
      {
56
        Node vcur = m->getValue(cur);
57
        Trace("model-core") << "  " << cur << " -> " << vcur << std::endl;
58
        vars.push_back(cur);
59
        subs.push_back(vcur);
60
      }
61
      if (cur.getMetaKind() == metakind::PARAMETERIZED)
62
      {
63
        visit.push_back(cur.getOperator());
64
      }
65
      visit.insert(visit.end(), cur.begin(), cur.end());
66
    }
67
  } while (!visit.empty());
68
69
  Node truen = nm->mkConst(true);
70
71
  Trace("model-core") << "Minimizing substitution..." << std::endl;
72
  std::vector<Node> coreVars;
73
  std::vector<Node> impliedVars;
74
  bool minimized = false;
75
  if (mode == options::ModelCoresMode::NON_IMPLIED)
76
  {
77
    minimized = theory::SubstitutionMinimize::findWithImplied(
78
        formula, vars, subs, coreVars, impliedVars);
79
  }
80
  else if (mode == options::ModelCoresMode::SIMPLE)
81
  {
82
    minimized = theory::SubstitutionMinimize::find(
83
        formula, truen, vars, subs, coreVars);
84
  }
85
  else
86
  {
87
    Unreachable() << "Unknown model cores mode";
88
  }
89
  Assert(minimized)
90
      << "cannot compute model core, since model does not satisfy input!";
91
  if (minimized)
92
  {
93
    m->setUsingModelCore();
94
    Trace("model-core") << "...got core vars : " << coreVars << std::endl;
95
96
    for (const Node& cv : coreVars)
97
    {
98
      m->recordModelCoreSymbol(cv);
99
    }
100
    return true;
101
  }
102
  Trace("model-core") << "...failed, model does not satisfy input!"
103
                      << std::endl;
104
  return false;
105
}
106
107
26676
} /* namespace CVC4 */