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
129
130
|
/********************* */
/*! \file arith_propagator.h
** \verbatim
** Original author: taking
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__ARITH__ARITH_PROPAGATOR_H
#define __CVC4__THEORY__ARITH__ARITH_PROPAGATOR_H
#include "expr/node.h"
#include "context/cdlist.h"
#include "context/context.h"
#include "context/cdo.h"
#include "theory/arith/ordered_bounds_list.h"
#include <algorithm>
#include <vector>
namespace CVC4 {
namespace theory {
namespace arith {
class ArithUnatePropagator {
private:
/** Index of assertions. */
context::CDList<Node> d_assertions;
/** Index of the last assertion in d_assertions to be asserted. */
context::CDO<unsigned int> d_pendingAssertions;
public:
ArithUnatePropagator(context::Context* cxt);
/**
* Adds a new atom for the propagator to watch.
* Atom is assumed to have been rewritten by TheoryArith::rewrite().
*/
void addAtom(TNode atom);
/**
* Informs the propagator that a literal has been asserted to the theory.
*/
void assertLiteral(TNode lit);
/**
* returns a vector of literals that are
*/
std::vector<Node> getImpliedLiterals();
/** Explains a literal that was asserted in the current context. */
Node explain(TNode lit);
private:
/** returns true if the left hand side side left has been setup. */
bool leftIsSetup(TNode left);
/**
* Sets up a left hand side.
* This initializes the attributes PropagatorEqList, PropagatorGeqList, and PropagatorLeqList for left.
*/
void setupLefthand(TNode left);
/**
* Given that the literal lit is now asserted,
* enqueue additional entailed assertions in buffer.
*/
void enqueueImpliedLiterals(TNode lit, std::vector<Node>& buffer);
void enqueueEqualityImplications(TNode original, std::vector<Node>& buffer);
void enqueueLowerBoundImplications(TNode atom, TNode original, std::vector<Node>& buffer);
/**
* Given that the literal original is now asserted, which is either (<= x c) or (not (>= x c)),
* enqueue additional entailed assertions in buffer.
*/
void enqueueUpperBoundImplications(TNode atom, TNode original, std::vector<Node>& buffer);
};
namespace propagator {
/** Basic memory management wrapper for deleting PropagatorEqList, PropagatorGeqList, and PropagatorLeqList.*/
struct ListCleanupStrategy{
static void cleanup(OrderedBoundsList* l){
Debug("arithgc") << "cleaning up " << l << "\n";
delete l;
}
};
struct PropagatorEqListID {};
typedef expr::Attribute<PropagatorEqListID, OrderedBoundsList*, ListCleanupStrategy> PropagatorEqList;
struct PropagatorGeqListID {};
typedef expr::Attribute<PropagatorGeqListID, OrderedBoundsList*, ListCleanupStrategy> PropagatorGeqList;
struct PropagatorLeqListID {};
typedef expr::Attribute<PropagatorLeqListID, OrderedBoundsList*, ListCleanupStrategy> PropagatorLeqList;
struct PropagatorMarkedID {};
typedef expr::CDAttribute<PropagatorMarkedID, bool> PropagatorMarked;
struct PropagatorExplanationID {};
typedef expr::CDAttribute<PropagatorExplanationID, Node> PropagatorExplanation;
}/* CVC4::theory::arith::propagator */
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_H */
|
