9e49cf3f10b8fb580d61f485882d877b8ec44491
1 /********************* */
2 /*! \file prop_engine.h
4 ** Original author: mdeters
5 ** Major contributors: taking, dejan
6 ** Minor contributors (to current version): cconway, barrett, kshitij
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief The PropEngine (propositional engine); main interface point
15 ** between CVC4's SMT infrastructure and the SAT solver
17 ** The PropEngine (propositional engine); main interface point
18 ** between CVC4's SMT infrastructure and the SAT solver.
21 #include "cvc4_private.h"
23 #ifndef __CVC4__PROP_ENGINE_H
24 #define __CVC4__PROP_ENGINE_H
26 #include "expr/node.h"
27 #include "util/options.h"
28 #include "util/result.h"
29 #include "smt/modal_exception.h"
40 class DPLLSatSolverInterface
;
45 * A helper class to keep track of a time budget and signal
46 * the PropEngine when the budget expires.
50 PropEngine
& d_propEngine
;
56 /** Construct a SatTimer attached to the given PropEngine. */
57 SatTimer(PropEngine
& propEngine
) :
58 d_propEngine(propEngine
),
62 /** Is the timer currently active? */
67 /** Set a millisecond timer (0==off). */
68 void set(unsigned long millis
) {
70 // keep track of when it was set, even if it's disabled (i.e. == 0)
71 Trace("limit") << "SatTimer::set(" << d_ms
<< ")" << std::endl
;
72 gettimeofday(&d_limit
, NULL
);
73 Trace("limit") << "SatTimer::set(): it's " << d_limit
.tv_sec
<< "," << d_limit
.tv_usec
<< std::endl
;
74 d_limit
.tv_sec
+= millis
/ 1000;
75 d_limit
.tv_usec
+= (millis
% 1000) * 1000;
76 if(d_limit
.tv_usec
> 1000000) {
78 d_limit
.tv_usec
-= 1000000;
80 Trace("limit") << "SatTimer::set(): limit is at " << d_limit
.tv_sec
<< "," << d_limit
.tv_usec
<< std::endl
;
83 /** Return the milliseconds elapsed since last set(). */
84 unsigned long elapsed() {
86 gettimeofday(&tv
, NULL
);
87 Trace("limit") << "SatTimer::elapsed(): it's now " << tv
.tv_sec
<< "," << tv
.tv_usec
<< std::endl
;
88 tv
.tv_sec
-= d_limit
.tv_sec
- d_ms
/ 1000;
89 tv
.tv_usec
-= d_limit
.tv_usec
- (d_ms
% 1000) * 1000;
90 Trace("limit") << "SatTimer::elapsed(): elapsed time is " << tv
.tv_sec
<< "," << tv
.tv_usec
<< std::endl
;
91 return tv
.tv_sec
* 1000 + tv
.tv_usec
/ 1000;
97 gettimeofday(&tv
, NULL
);
98 Trace("limit") << "SatTimer::expired(): current time is " << tv
.tv_sec
<< "," << tv
.tv_usec
<< std::endl
;
99 Trace("limit") << "SatTimer::expired(): limit time is " << d_limit
.tv_sec
<< "," << d_limit
.tv_usec
<< std::endl
;
100 if(d_limit
.tv_sec
< tv
.tv_sec
||
101 (d_limit
.tv_sec
== tv
.tv_sec
&& d_limit
.tv_usec
<= tv
.tv_usec
)) {
102 Trace("limit") << "SatTimer::expired(): OVER LIMIT!" << std::endl
;
105 Trace("limit") << "SatTimer::expired(): within limit" << std::endl
;
111 /** Check the current time and signal the PropEngine if over-time. */
114 };/* class SatTimer */
117 * PropEngine is the abstraction of a Sat Solver, providing methods for
118 * solving the SAT problem and conversion to CNF (via the CnfStream).
123 * Indicates that the SAT solver is currently solving something and we should
124 * not mess with it's internal state.
128 /** The theory engine we will be using */
129 TheoryEngine
*d_theoryEngine
;
131 /** The decision engine we will be using */
132 DecisionEngine
*d_decisionEngine
;
135 context::Context
* d_context
;
137 /** The SAT solver proxy */
138 DPLLSatSolverInterface
* d_satSolver
;
140 /** List of all of the assertions that need to be made */
141 std::vector
<Node
> d_assertionList
;
143 /** The CNF converter in use */
144 CnfStream
* d_cnfStream
;
146 /** A timer for SAT calls */
149 /** Whether we were just interrupted (or not) */
152 /** Dump out the satisfying assignment (after SAT result) */
153 void printSatisfyingAssignment();
158 * Create a PropEngine with a particular decision and theory engine.
160 PropEngine(TheoryEngine
*, DecisionEngine
*, context::Context
*);
165 CVC4_PUBLIC
~PropEngine();
168 * This is called by SmtEngine, at shutdown time, just before
169 * destruction. It is important because there are destruction
170 * ordering issues between some parts of the system (notably between
171 * PropEngine and Theory). For now, there's nothing to do here in
177 * Converts the given formula to CNF and assert the CNF to the SAT solver.
178 * The formula is asserted permanently for the current context.
179 * @param node the formula to assert
181 void assertFormula(TNode node
);
184 * Converts the given formula to CNF and assert the CNF to the SAT solver.
185 * The formula can be removed by the SAT solver after backtracking lower
186 * than the (SAT and SMT) level at which it was asserted.
188 * @param node the formula to assert
189 * @param negated whether the node should be considered to be negated
190 * at the top level (or not)
191 * @param removable whether this lemma can be quietly removed based
192 * on an activity heuristic (or not)
194 void assertLemma(TNode node
, bool negated
, bool removable
);
197 * Checks the current context for satisfiability.
199 * @param millis the time limit for this call in milliseconds
200 * (0==off); on output, it is set to the milliseconds used
201 * @param on input, resource the number of resource units permitted
202 * for this call (0==off); on output, it is set to the resource used
204 Result
checkSat(unsigned long& millis
, unsigned long& resource
);
207 * Get the value of a boolean variable.
209 * @return mkConst<true>, mkConst<false>, or Node::null() if
212 Node
getValue(TNode node
) const;
215 * Return true if node has an associated SAT literal.
217 bool isSatLiteral(TNode node
) const;
220 * Return true if node has an associated SAT literal that is
221 * currently translated (i.e., it's relevant to the current
222 * user push/pop level).
224 bool isTranslatedSatLiteral(TNode node
) const;
227 * Check if the node has a value and return it if yes.
229 bool hasValue(TNode node
, bool& value
) const;
232 * Ensure that the given node will have a designated SAT literal
233 * that is definitionally equal to it. The result of this function
234 * is that the Node can be queried via getSatValue().
236 void ensureLiteral(TNode n
);
239 * Push the context level.
244 * Pop the context level.
249 * Return true if we are currently searching (either in this or
252 bool isRunning() const;
255 * Check the current time budget.
260 * Interrupt a running solver (cause a timeout).
262 void interrupt() throw(ModalException
);
265 * "Spend" a "resource." If the sum of these externally-counted
266 * resources and SAT-internal resources exceed the current limit,
267 * SAT should terminate.
269 void spendResource() throw();
272 * For debugging. Return true if "expl" is a well-formed
273 * explanation for "node," meaning:
275 * 1. expl is either a SAT literal or an AND of SAT literals
276 * currently assigned true;
277 * 2. node is assigned true;
278 * 3. node does not appear in expl; and
279 * 4. node was assigned after all of the literals in expl
281 bool properExplanation(TNode node
, TNode expl
) const;
283 };/* class PropEngine */
286 inline void SatTimer::check() {
287 if(d_propEngine
.isRunning() && expired()) {
288 Trace("limit") << "SatTimer::check(): interrupt!" << std::endl
;
289 d_propEngine
.interrupt();
293 inline void PropEngine::checkTime() {
297 }/* CVC4::prop namespace */
298 }/* CVC4 namespace */
300 #endif /* __CVC4__PROP_ENGINE_H */