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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
|
/********************* */
/*! \file atom_database.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 ArithAtomDatabase keeps a database of the arithmetic atoms.
** Importantly, ArithAtomDatabase also handles unate propagations,
** i.e. it constructs implications of the form
** "if x < c and c < b, then x < b" (where c and b are constants).
**
** ArithAtomDatabase detects unate implications amongst the atoms
** associated with the theory of arithmetic and informs the SAT solver of the
** implication. A unate implication is an implication of the form:
** "if x < c and c < b, then x < b" (where c and b are constants).
** Unate implications are always 2-SAT clauses.
** ArithAtomDatabase sends the implications to the SAT solver in an
** online fashion.
** This means that atoms may be added during solving or before.
**
** ArithAtomDatabase maintains sorted lists containing all atoms associated
** for each unique left hand side, the "x" in the inequality "x < c".
** The lists are sorted by the value of the right hand side which must be a
** rational constant.
**
** ArithAtomDatabase tries to send out a minimal number of additional
** lemmas per atom added. Let (x < a), (x < b), (x < c) be arithmetic atoms s.t.
** a < b < c.
** If the the order of adding the atoms is (x < a), (x < b), and (x < c), then
** then set of all lemmas added is:
** {(=> (x<a) (x < b)), (=> (x<b) (x < c))}
** If the order is changed to (x < a), (x < c), and (x < b), then
** the final set of implications emitted is:
** {(=> (x<a) (x < c)), (=> (x<a) (x < b)), (=> (x<b) (x < c))}
**
** \todo document this file
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__ARITH__ARITH_ATOM_DATABASE_H
#define __CVC4__THEORY__ARITH__ARITH_ATOM_DATABASE_H
#include "expr/node.h"
#include "context/context.h"
#include "theory/output_channel.h"
#include "theory/arith/ordered_set.h"
#include <ext/hash_map>
namespace CVC4 {
namespace theory {
namespace arith {
class ArithAtomDatabase {
private:
/**
* OutputChannel for the theory of arithmetic.
* The propagator uses this to pass implications back to the SAT solver.
*/
OutputChannel& d_arithOut;
struct VariablesSets {
BoundValueSet d_boundValueSet;
EqualValueSet d_eqValueSet;
};
typedef __gnu_cxx::hash_map<TNode, VariablesSets, NodeHashFunction> NodeToSetsMap;
NodeToSetsMap d_setsMap;
public:
ArithAtomDatabase(context::Context* cxt, OutputChannel& arith);
/**
* Adds an atom to the propagator.
* Any resulting lemmas will be output via d_arithOut.
*/
void addAtom(TNode atom);
/** Returns true if v has been added as a left hand side in an atom */
bool hasAnyAtoms(TNode v) const;
bool containsLiteral(TNode lit) const;
bool containsAtom(TNode atom) const;
bool containsEquality(TNode atom) const;
bool containsLeq(TNode atom) const;
bool containsGeq(TNode atom) const;
private:
VariablesSets& getVariablesSets(TNode left);
BoundValueSet& getBoundValueSet(TNode left);
EqualValueSet& getEqualValueSet(TNode left);
const VariablesSets& getVariablesSets(TNode left) const;
const BoundValueSet& getBoundValueSet(TNode left) const;
const EqualValueSet& getEqualValueSet(TNode left) const;
/** Sends an implication (=> a b) to the PropEngine via d_arithOut. */
void addImplication(TNode a, TNode b);
/** Check to make sure an lhs has been properly set-up. */
bool leftIsSetup(TNode left) const;
/** Initializes the lists associated with a unique lhs. */
void setupLefthand(TNode left);
/**
* The addImplicationsUsingKAndJList(...)
* functions are the work horses of the unate part of ArithAtomDatabase.
* These take an atom of the kind K that has just been added
* to its associated list, and the ordered list of Js associated with the lhs,
* and uses these to deduce unate implications.
* (K and J vary over EQUAL, LEQ, and GEQ.)
*
* Input:
* atom - the atom being inserted of kind K
* Jset - the list of atoms of kind J associated with the lhs.
*
* Unfortunately, these tend to be an absolute bear to read because
* of all of the special casing and C++ iterator manipulation required.
*/
void addImplicationsUsingEqualityAndEqualityValues(TNode eq);
void addImplicationsUsingEqualityAndBoundValues(TNode eq);
void addImplicationsUsingLeqAndEqualityValues(TNode leq);
void addImplicationsUsingLeqAndBoundValues(TNode leq);
void addImplicationsUsingGeqAndEqualityValues(TNode geq);
void addImplicationsUsingGeqAndBoundValues(TNode geq);
bool hasBoundValueEntry(TNode n);
Node getImpliedUpperBoundUsingLeq(TNode leq, bool weaker) const;
Node getImpliedUpperBoundUsingLT(TNode lt, bool weaker) const;
Node getImpliedLowerBoundUsingGeq(TNode geq, bool weaker) const;
Node getImpliedLowerBoundUsingGT(TNode gt, bool weaker) const;
public:
Node getBestImpliedUpperBound(TNode upperBound) const;
Node getBestImpliedLowerBound(TNode lowerBound) const;
Node getWeakerImpliedUpperBound(TNode upperBound) const;
Node getWeakerImpliedLowerBound(TNode lowerBound) const;
};
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__ARITH__ARITH_ATOM_DATABASE_H */
|
