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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
|
/********************* */
/*! \file valuation.h
** \verbatim
** Original author: mdeters
** Major contributors: dejan
** Minor contributors (to current version): taking, ajreynol, barrett
** This file is part of the CVC4 prototype.
** Copyright (c) 2009-2012 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief A "valuation" proxy for TheoryEngine
**
** A "valuation" proxy for TheoryEngine. This class breaks the dependence
** of theories' getValue() implementations on TheoryEngine. getValue()
** takes a Valuation, which delegates to TheoryEngine.
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__VALUATION_H
#define __CVC4__THEORY__VALUATION_H
#include "expr/node.h"
namespace CVC4 {
class TheoryEngine;
namespace theory {
/**
* The status of an equality in the current context.
*/
enum EqualityStatus {
/** The equality is known to be true and has been propagated */
EQUALITY_TRUE_AND_PROPAGATED,
/** The equality is known to be false and has been propagated */
EQUALITY_FALSE_AND_PROPAGATED,
/** The equality is known to be true */
EQUALITY_TRUE,
/** The equality is known to be false */
EQUALITY_FALSE,
/** The equality is not known, but is true in the current model */
EQUALITY_TRUE_IN_MODEL,
/** The equality is not known, but is false in the current model */
EQUALITY_FALSE_IN_MODEL,
/** The equality is completely unknown */
EQUALITY_UNKNOWN
};
/**
* Returns true if the two statuses are compatible, i.e. bot TRUE
* or both FALSE (regardles of inmodel/propagation).
*/
bool equalityStatusCompatible(EqualityStatus s1, EqualityStatus s2);
class Valuation {
TheoryEngine* d_engine;
public:
Valuation(TheoryEngine* engine) :
d_engine(engine) {
}
/*
* Return true if n has an associated SAT literal
*/
bool isSatLiteral(TNode n) const;
/**
* Get the current SAT assignment to the node n.
*
* This is only permitted if n is a theory atom that has an associated
* SAT literal (or its negation).
*
* @return Node::null() if no current assignment; otherwise true or false.
*/
Node getSatValue(TNode n) const;
/**
* Returns true if the node has a current SAT assignment. If yes, the
* argument "value" is set to its value.
*
* This is only permitted if n is a theory atom that has an associated
* SAT literal.
*
* @return true if the literal has a current assignment, and returns the
* value in the "value" argument; otherwise false and the "value"
* argument is unmodified.
*/
bool hasSatValue(TNode n, bool& value) const;
/**
* Returns the equality status of the two terms, from the theory that owns the domain type.
* The types of a and b must be the same.
*/
EqualityStatus getEqualityStatus(TNode a, TNode b);
/**
* Ensure that the given node will have a designated SAT literal
* that is definitionally equal to it. The result of this function
* is a Node that can be queried via getSatValue().
*
* @return the actual node that's been "literalized," which may
* differ from the input due to theory-rewriting and preprocessing,
* as well as CNF conversion
*/
Node ensureLiteral(TNode n) CVC4_WARN_UNUSED_RESULT;
/**
* Returns whether the given lit (which must be a SAT literal) is a decision
* literal or not. Throws an exception if lit is not a SAT literal. "lit" may
* be in either phase; that is, if "lit" is a SAT literal, this function returns
* true both for lit and the negation of lit.
*/
bool isDecision(Node lit) const;
/**
* Get the assertion level of the SAT solver.
*/
unsigned getAssertionLevel() const;
};/* class Valuation */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__VALUATION_H */
|
