GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/check_models.cpp Lines: 32 47 68.1 %
Date: 2021-03-22 Branches: 58 210 27.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file check_models.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Andres Noetzli
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 Utility for constructing and maintaining abstract values.
13
 **/
14
15
#include "smt/check_models.h"
16
17
#include "options/smt_options.h"
18
#include "smt/model.h"
19
#include "smt/node_command.h"
20
#include "smt/preprocessor.h"
21
#include "smt/smt_solver.h"
22
#include "theory/rewriter.h"
23
#include "theory/substitutions.h"
24
#include "theory/theory_engine.h"
25
26
using namespace CVC4::theory;
27
28
namespace CVC4 {
29
namespace smt {
30
31
8995
CheckModels::CheckModels(SmtSolver& s) : d_smt(s) {}
32
8992
CheckModels::~CheckModels() {}
33
34
1948
void CheckModels::checkModel(Model* m,
35
                             context::CDList<Node>* al,
36
                             bool hardFailure)
37
{
38
  // Throughout, we use Notice() to give diagnostic output.
39
  //
40
  // If this function is running, the user gave --check-model (or equivalent),
41
  // and if Notice() is on, the user gave --verbose (or equivalent).
42
43
  // check-model is not guaranteed to succeed if approximate values were used.
44
  // Thus, we intentionally abort here.
45
1948
  if (m->hasApproximations())
46
  {
47
    throw RecoverableModalException(
48
1
        "Cannot run check-model on a model with approximate values.");
49
  }
50
51
  // Check individual theory assertions
52
15841
  if (options::debugCheckModels())
53
  {
54
1941
    TheoryEngine* te = d_smt.getTheoryEngine();
55
1941
    Assert(te != nullptr);
56
1941
    te->checkTheoryAssertionsWithModel(hardFailure);
57
  }
58
59
1947
  Preprocessor* pp = d_smt.getPreprocessor();
60
61
1947
  Trace("check-model") << "checkModel: Check assertions..." << std::endl;
62
2003
  std::unordered_map<Node, Node, NodeHashFunction> cache;
63
  // the list of assertions that did not rewrite to true
64
2003
  std::vector<Node> noCheckList;
65
  // Now go through all our user assertions checking if they're satisfied.
66
22456
  for (const Node& assertion : *al)
67
  {
68
20509
    Notice() << "SmtEngine::checkModel(): checking assertion " << assertion
69
             << std::endl;
70
71
    // Apply any define-funs from the problem. We do not expand theory symbols
72
    // like integer division here. Hence, the code below is not able to properly
73
    // evaluate e.g. divide-by-zero. This is intentional since the evaluation
74
    // is not trustworthy, since the UF introduced by expanding definitions may
75
    // not be properly constrained.
76
20509
    Node n = pp->expandDefinitions(assertion, cache, true);
77
20509
    Notice() << "SmtEngine::checkModel(): -- expands to " << n << std::endl;
78
79
20509
    n = Rewriter::rewrite(n);
80
20509
    Notice() << "SmtEngine::checkModel(): -- rewrites to " << n << std::endl;
81
82
    // We look up the value before simplifying. If n contains quantifiers,
83
    // this may increases the chance of finding its value before the node is
84
    // altered by simplification below.
85
20509
    n = m->getValue(n);
86
20509
    Notice() << "SmtEngine::checkModel(): -- get value : " << n << std::endl;
87
88
20509
    if (n.isConst() && n.getConst<bool>())
89
    {
90
      // assertion is true, everything is fine
91
20236
      continue;
92
    }
93
94
    // Otherwise, we did not succeed in showing the current assertion to be
95
    // true. This may either indicate that our model is wrong, or that we cannot
96
    // check it. The latter may be the case for several reasons.
97
    // For example, quantified formulas are not checkable, although we assign
98
    // them to true/false based on the satisfying assignment. However,
99
    // quantified formulas can be modified during preprocess, so they may not
100
    // correspond to those in the satisfying assignment. Hence we throw
101
    // warnings for assertions that do not simplify to either true or false.
102
    // Other theories such as non-linear arithmetic (in particular,
103
    // transcendental functions) also have the property of not being able to
104
    // be checked precisely here.
105
    // Note that warnings like these can be avoided for quantified formulas
106
    // by making preprocessing passes explicitly record how they
107
    // rewrite quantified formulas (see cvc4-wishues#43).
108
546
    if (!n.isConst())
109
    {
110
      // Not constant, print a less severe warning message here.
111
273
      Warning() << "Warning : SmtEngine::checkModel(): cannot check simplified "
112
                   "assertion : "
113
                << n << std::endl;
114
273
      noCheckList.push_back(n);
115
273
      continue;
116
    }
117
    // Assertions that simplify to false result in an InternalError or
118
    // Warning being thrown below (when hardFailure is false).
119
    Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***"
120
             << std::endl;
121
    std::stringstream ss;
122
    ss << "SmtEngine::checkModel(): "
123
       << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << std::endl
124
       << "assertion:     " << assertion << std::endl
125
       << "simplifies to: " << n << std::endl
126
       << "expected `true'." << std::endl
127
       << "Run with `--check-models -v' for additional diagnostics.";
128
    if (hardFailure)
129
    {
130
      // internal error if hardFailure is true
131
      InternalError() << ss.str();
132
    }
133
    else
134
    {
135
      Warning() << ss.str() << std::endl;
136
    }
137
  }
138
1947
  if (noCheckList.empty())
139
  {
140
1891
    Notice() << "SmtEngine::checkModel(): all assertions checked out OK !"
141
             << std::endl;
142
1891
    return;
143
  }
144
  // if the noCheckList is non-empty, we could expand definitions on this list
145
  // and check satisfiability
146
147
56
  Trace("check-model") << "checkModel: Finish" << std::endl;
148
}
149
150
}  // namespace smt
151
40570
}  // namespace CVC4