1 /********************* */
2 /*! \file valuation.cpp
4 ** Top contributors (to current version):
5 ** Dejan Jovanovic, Andrew Reynolds, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief A "valuation" proxy for TheoryEngine
14 ** Implementation of Valuation class.
17 #include "theory/valuation.h"
19 #include "expr/node.h"
20 #include "options/theory_options.h"
21 #include "theory/rewriter.h"
22 #include "theory/theory_engine.h"
23 #include "theory/theory_model.h"
28 std::ostream
& operator<<(std::ostream
& os
, EqualityStatus s
)
32 case EQUALITY_TRUE_AND_PROPAGATED
:
33 os
<< "EQUALITY_TRUE_AND_PROPAGATED";
35 case EQUALITY_FALSE_AND_PROPAGATED
:
36 os
<< "EQUALITY_FALSE_AND_PROPAGATED";
38 case EQUALITY_TRUE
: os
<< "EQUALITY_TRUE"; break;
39 case EQUALITY_FALSE
: os
<< "EQUALITY_FALSE"; break;
40 case EQUALITY_TRUE_IN_MODEL
: os
<< "EQUALITY_TRUE_IN_MODEL"; break;
41 case EQUALITY_FALSE_IN_MODEL
: os
<< "EQUALITY_FALSE_IN_MODEL"; break;
42 case EQUALITY_UNKNOWN
: os
<< "EQUALITY_UNKNOWN"; break;
43 default: Unhandled(); break;
48 bool equalityStatusCompatible(EqualityStatus s1
, EqualityStatus s2
) {
51 case EQUALITY_TRUE_IN_MODEL
:
52 case EQUALITY_TRUE_AND_PROPAGATED
:
55 case EQUALITY_TRUE_IN_MODEL
:
56 case EQUALITY_TRUE_AND_PROPAGATED
:
63 case EQUALITY_FALSE_IN_MODEL
:
64 case EQUALITY_FALSE_AND_PROPAGATED
:
67 case EQUALITY_FALSE_IN_MODEL
:
68 case EQUALITY_FALSE_AND_PROPAGATED
:
79 bool Valuation::isSatLiteral(TNode n
) const {
80 Assert(d_engine
!= nullptr);
81 return d_engine
->getPropEngine()->isSatLiteral(n
);
84 Node
Valuation::getSatValue(TNode n
) const {
85 Assert(d_engine
!= nullptr);
86 if(n
.getKind() == kind::NOT
) {
87 Node atomRes
= d_engine
->getPropEngine()->getValue(n
[0]);
88 if(atomRes
.getKind() == kind::CONST_BOOLEAN
) {
89 return NodeManager::currentNM()->mkConst(!atomRes
.getConst
<bool>());
91 Assert(atomRes
.isNull());
95 return d_engine
->getPropEngine()->getValue(n
);
99 bool Valuation::hasSatValue(TNode n
, bool& value
) const {
100 Assert(d_engine
!= nullptr);
101 if (d_engine
->getPropEngine()->isSatLiteral(n
)) {
102 return d_engine
->getPropEngine()->hasValue(n
, value
);
108 EqualityStatus
Valuation::getEqualityStatus(TNode a
, TNode b
) {
109 Assert(d_engine
!= nullptr);
110 return d_engine
->getEqualityStatus(a
, b
);
113 Node
Valuation::getModelValue(TNode var
) {
114 Assert(d_engine
!= nullptr);
115 return d_engine
->getModelValue(var
);
118 TheoryModel
* Valuation::getModel() {
119 if (d_engine
== nullptr)
121 // no theory engine, thus we don't have a model object
124 return d_engine
->getModel();
127 void Valuation::setUnevaluatedKind(Kind k
)
129 TheoryModel
* m
= getModel();
132 m
->setUnevaluatedKind(k
);
134 // If no model is available, this command has no effect. This is the case
135 // when e.g. calling Theory::finishInit for theories that are using a
136 // Valuation with no model.
139 void Valuation::setSemiEvaluatedKind(Kind k
)
141 TheoryModel
* m
= getModel();
144 m
->setSemiEvaluatedKind(k
);
148 Node
Valuation::ensureLiteral(TNode n
) {
149 Assert(d_engine
!= nullptr);
150 return d_engine
->ensureLiteral(n
);
153 bool Valuation::isDecision(Node lit
) const {
154 Assert(d_engine
!= nullptr);
155 return d_engine
->getPropEngine()->isDecision(lit
);
158 unsigned Valuation::getAssertionLevel() const{
159 Assert(d_engine
!= nullptr);
160 return d_engine
->getPropEngine()->getAssertionLevel();
163 std::pair
<bool, Node
> Valuation::entailmentCheck(options::TheoryOfMode mode
,
166 Assert(d_engine
!= nullptr);
167 return d_engine
->entailmentCheck(mode
, lit
);
170 bool Valuation::needCheck() const{
171 Assert(d_engine
!= nullptr);
172 return d_engine
->needCheck();
175 }/* CVC4::theory namespace */
176 }/* CVC4 namespace */