blob: cf6a90f12ddefadde69aa0d35389c27dde13f689 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds, Morgan Deters, Tim King
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* Implementation of Model class.
*/
#include "smt/model.h"
#include "expr/expr_iomanip.h"
#include "options/base_options.h"
#include "printer/printer.h"
#include "smt/dump_manager.h"
#include "smt/node_command.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/theory_model.h"
namespace cvc5 {
namespace smt {
Model::Model(theory::TheoryModel* tm) : d_isKnownSat(false), d_tmodel(tm)
{
Assert(d_tmodel != nullptr);
}
std::ostream& operator<<(std::ostream& out, const Model& m) {
expr::ExprDag::Scope scope(out, false);
Printer::getPrinter(options::outputLanguage())->toStream(out, m);
return out;
}
theory::TheoryModel* Model::getTheoryModel() { return d_tmodel; }
const theory::TheoryModel* Model::getTheoryModel() const { return d_tmodel; }
bool Model::isModelCoreSymbol(TNode sym) const
{
return d_tmodel->isModelCoreSymbol(sym);
}
Node Model::getValue(TNode n) const { return d_tmodel->getValue(n); }
bool Model::hasApproximations() const { return d_tmodel->hasApproximations(); }
void Model::clearModelDeclarations()
{
d_declareTerms.clear();
d_declareSorts.clear();
}
void Model::addDeclarationSort(TypeNode tn) { d_declareSorts.push_back(tn); }
void Model::addDeclarationTerm(Node n) { d_declareTerms.push_back(n); }
const std::vector<TypeNode>& Model::getDeclaredSorts() const
{
return d_declareSorts;
}
const std::vector<Node>& Model::getDeclaredTerms() const
{
return d_declareTerms;
}
} // namespace smt
} // namespace cvc5
|
