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
167
168
169
170
171
172
173
|
/********************* -*- C++ -*- */
/** cnf_stream.h
** Original author: taking
** Major contributors: dejan
** 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.
**
** This class takes a sequence of formulas.
** It outputs a stream of clauses that is propositional
** equisatisfiable with the conjunction of the formulas.
** This stream is maintained in an online fashion.
**
** Unlike other parts of the system it is aware of the PropEngine's
** internals such as the representation and translation of
**/
#ifndef __CVC4__CNF_STREAM_H
#define __CVC4__CNF_STREAM_H
#include "expr/node.h"
#include "prop/minisat/simp/SimpSolver.h"
#include "prop/minisat/core/SolverTypes.h"
#include "prop/prop_engine.h"
#include <map>
namespace CVC4 {
class PropEngine;
}
namespace CVC4 {
namespace prop {
/**
* Comments for the behavior of the whole class...
* @author Tim King <taking@cs.nyu.edu>
*/
class CnfStream {
private:
/**
* d_propEngine is the PropEngine that the CnfStream interacts with directly
* through the following functions:
* - insertClauseIntoStream
* - acquireFreshLit
* - registerMapping
*/
PropEngine *d_propEngine;
/**
* Cache of what literal have been registered to a node. Not strictly needed
* for correctness. This can be flushed when memory is under pressure.
* TODO: Use attributes when they arrive
*/
std::map<Node, minisat::Lit> d_translationCache;
protected:
bool isAtomMapped(const Node & n) const;
minisat::Var lookupAtom(const Node & n) const;
/**
* Uniform interface for sending a clause back to d_propEngine.
* May want to have internal data-structures later on
*/
void insertClauseIntoStream(minisat::vec<minisat::Lit> & c);
void insertClauseIntoStream(minisat::Lit a);
void insertClauseIntoStream(minisat::Lit a, minisat::Lit b);
void insertClauseIntoStream(minisat::Lit a, minisat::Lit b, minisat::Lit c);
//utilities for the translation cache;
bool isCached(const Node & n) const;
/**
* Method comments...
* @param n
* @return returns ...
*/
minisat::Lit lookupInCache(const Node & n) const;
//negotiates the mapping of atoms to literals with PropEngine
void cacheTranslation(const Node & node, minisat::Lit lit);
minisat::Lit aquireAndRegister(const Node & n, bool atom = false);
public:
/**
* Constructs a CnfStream that sends constructs an equisatisfiable set of clauses
* and sends them to the given PropEngine.
* @param pe
*/
CnfStream(CVC4::PropEngine *pe);
/**
* Empties the internal translation cache.
*/
void flushCache();
/**
* Converts and asserts a formula.
* @param n node to convert and assert
*/
virtual void convertAndAssert(const Node & n) = 0;
}; /* class CnfStream */
/**
* TseitinCnfStream is based on the following recursive algorithm
* http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf
* The general gist of the algorithm is to introduce a new literal that
* will be equivalent to each subexpression in the constructed equisatisfiable
* formula then substitute the new literal for the formula, and to do this
* recursively.
*
* This implementation does this in a single recursive pass.
*/
class TseitinCnfStream : public CnfStream {
public:
void convertAndAssert(const Node & n);
TseitinCnfStream(CVC4::PropEngine *pe);
private:
/* Each of these formulas handles takes care of a Node of each Kind.
*
* Each handleX(Node &n) is responsible for:
* - constructing a new literal, l (if necessary)
* - calling registerNode(n,l)
* - adding clauses assure that l is equivalent to the Node
* - calling recTransform on its children (if necessary)
* - returning l
*
* handleX( n ) can assume that n is not in d_translationCache
*/
minisat::Lit handleAtom(const Node & n);
minisat::Lit handleNot(const Node & n);
minisat::Lit handleXor(const Node & n);
minisat::Lit handleImplies(const Node & n);
minisat::Lit handleIff(const Node & n);
minisat::Lit handleIte(const Node & n);
minisat::Lit handleAnd(const Node& n);
minisat::Lit handleOr(const Node& n);
/**
* Maps recTransform over the children of a node. This is very useful for
* n-ary Kinds (OR, AND). Non n-ary kinds (IMPLIES) should avoid using this
* as it requires a tiny bit of extra overhead, and it leads to less readable
* code.
*
* precondition: target.size() == n.getNumChildren()
* @param n ...
* @param target ...
*/
void mapRecTransformOverChildren(const Node& n,
minisat::vec<minisat::Lit> & target);
//Recursively dispatches the various Kinds to the appropriate handler.
minisat::Lit recTransform(const Node & n);
}; /* class TseitinCnfStream */
}/* prop namespace */
}/* CVC4 namespace */
#endif /* __CVC4__CNF_STREAM_H */
|
