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
|
/********************* -*- C++ -*- */
/** cnf_stream.h
** Original author: taking
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009 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
//TODO: Why am i including this? Who knows...
#include "cvc4_config.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 {
class CnfStream {
private:
/**
* d_propEngine is the PropEngine that the CnfStream interacts with directly through
* the follwoing 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.
*/
std::map<Node,minisat::Lit> d_translationCache;
protected:
/**
* Uniform interface for sending a clause back to d_propEngine.
* May want to have internal datastructures 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;
minisat::Lit lookupInCache(const Node & n) const;
/**
* Empties the internal translation cache.
*/
void flushCache();
//negotiates the mapping of atoms to literals with PropEngine
void registerMapping(const Node & node, minisat::Lit lit, bool atom = false);
minisat::Lit acquireFreshLit(const Node & n);
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 pe.
*/
CnfStream(CVC4::PropEngine *pe);
/**
* 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 subsistute 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 responsibile for:
* - constructing a new literal, l (if nessecary)
* - calling registerNode(n,l)
* - adding clauses asure that l is equivalent to the Node
* - calling recTransform on its children (if nessecary)
* - 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()
*/
void mapRecTransformOverChildren(const Node& n, minisat::vec<minisat::Lit> & target);
//Recurisively 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 */
|
