GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/model.cpp Lines: 24 24 100.0 %
Date: 2021-03-23 Branches: 11 40 27.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file model.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Tim King
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 Model class
13
 **/
14
15
#include "smt/model.h"
16
17
#include "expr/expr_iomanip.h"
18
#include "options/base_options.h"
19
#include "printer/printer.h"
20
#include "smt/dump_manager.h"
21
#include "smt/node_command.h"
22
#include "smt/smt_engine.h"
23
#include "smt/smt_engine_scope.h"
24
#include "theory/theory_model.h"
25
26
namespace CVC4 {
27
namespace smt {
28
29
8997
Model::Model(theory::TheoryModel* tm) : d_isKnownSat(false), d_tmodel(tm)
30
{
31
8997
  Assert(d_tmodel != nullptr);
32
8997
}
33
34
25
std::ostream& operator<<(std::ostream& out, const Model& m) {
35
50
  expr::ExprDag::Scope scope(out, false);
36
25
  Printer::getPrinter(options::outputLanguage())->toStream(out, m);
37
50
  return out;
38
}
39
40
30
theory::TheoryModel* Model::getTheoryModel() { return d_tmodel; }
41
42
59
const theory::TheoryModel* Model::getTheoryModel() const { return d_tmodel; }
43
44
30
bool Model::isModelCoreSymbol(TNode sym) const
45
{
46
30
  return d_tmodel->isModelCoreSymbol(sym);
47
}
48
24244
Node Model::getValue(TNode n) const { return d_tmodel->getValue(n); }
49
50
5683
bool Model::hasApproximations() const { return d_tmodel->hasApproximations(); }
51
52
25
void Model::clearModelDeclarations()
53
{
54
25
  d_declareTerms.clear();
55
25
  d_declareSorts.clear();
56
25
}
57
58
4
void Model::addDeclarationSort(TypeNode tn) { d_declareSorts.push_back(tn); }
59
60
30
void Model::addDeclarationTerm(Node n) { d_declareTerms.push_back(n); }
61
25
const std::vector<TypeNode>& Model::getDeclaredSorts() const
62
{
63
25
  return d_declareSorts;
64
}
65
25
const std::vector<Node>& Model::getDeclaredTerms() const
66
{
67
25
  return d_declareTerms;
68
}
69
70
}  // namespace smt
71
26685
}/* CVC4 namespace */