1 /********************* */
4 ** Original author: mdeters
5 ** Major contributors: dejan
6 ** Minor contributors (to current version): cconway
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 SmtEngine: the main public entry point of libcvc4.
16 ** SmtEngine: the main public entry point of libcvc4.
19 #include "cvc4_public.h"
21 #ifndef __CVC4__SMT_ENGINE_H
22 #define __CVC4__SMT_ENGINE_H
26 #include "context/cdlist_forward.h"
27 #include "context/cdmap_forward.h"
28 #include "context/cdset_forward.h"
29 #include "expr/expr.h"
30 #include "expr/expr_manager.h"
31 #include "smt/bad_option_exception.h"
32 #include "smt/modal_exception.h"
33 #include "smt/no_such_function_exception.h"
34 #include "util/hash.h"
35 #include "util/options.h"
36 #include "util/result.h"
37 #include "util/sexpr.h"
38 #include "util/stats.h"
39 #include "proof/proof_manager.h"
41 // In terms of abstraction, this is below (and provides services to)
42 // ValidityChecker and above (and requires the services of)
48 template <bool ref_count
> class NodeTemplate
;
49 typedef NodeTemplate
<true> Node
;
50 typedef NodeTemplate
<false> TNode
;
51 class NodeHashFunction
;
55 class StatisticsRegistry
;
60 }/* CVC4::context namespace */
64 }/* CVC4::prop namespace */
68 * Representation of a defined function. We keep these around in
69 * SmtEngine to permit expanding definitions late (and lazily), to
70 * support getValue() over defined functions, to support user output
71 * in terms of defined functions, etc.
73 class DefinedFunction
;
75 class SmtEnginePrivate
;
76 }/* CVC4::smt namespace */
78 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
79 // hood): use a type parameter and have check() delegate, or subclass
80 // SmtEngine and override check()?
82 // Probably better than that is to have a configuration object that
83 // indicates which passes are desired. The configuration occurs
84 // elsewhere (and can even occur at runtime). A simple "pass manager"
85 // of sorts determines check()'s behavior.
87 // The CNF conversion can go on in PropEngine.
89 class CVC4_PUBLIC SmtEngine
{
91 /** The type of our internal map of defined functions */
92 typedef context::CDMap
<Node
, smt::DefinedFunction
, NodeHashFunction
>
94 /** The type of our internal assertion list */
95 typedef context::CDList
<Expr
> AssertionList
;
96 /** The type of our internal assignment set */
97 typedef context::CDSet
<Node
, NodeHashFunction
> AssignmentSet
;
99 /** Expr manager context */
100 context::Context
* d_context
;
102 /** The context levels of user pushes */
103 std::vector
<int> d_userLevels
;
104 /** User level context */
105 context::UserContext
* d_userContext
;
107 /** Our expression manager */
108 ExprManager
* d_exprManager
;
109 /** Our internal expression/node manager */
110 NodeManager
* d_nodeManager
;
111 /** The decision engine */
112 TheoryEngine
* d_theoryEngine
;
113 /** The propositional engine */
114 prop::PropEngine
* d_propEngine
;
115 /** An index of our defined functions */
116 DefinedFunctionMap
* d_definedFunctions
;
118 * The assertion list (before any conversion) for supporting
119 * getAssertions(). Only maintained if in interactive mode.
121 AssertionList
* d_assertionList
;
124 * List of items for which to retrieve values using getAssignment().
126 AssignmentSet
* d_assignments
;
129 * The logic we're in.
134 * Whether or not we have added any assertions/declarations/definitions
135 * since the last checkSat/query (and therefore we're not responsible
136 * for an assignment).
138 bool d_problemExtended
;
141 * Whether or not a query() or checkSat() has already been made through
142 * this SmtEngine. If true, and incrementalSolving is false, then
143 * attempting an additional query() or checkSat() will fail with a
148 /** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */
149 unsigned long d_timeBudgetCumulative
;
150 /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */
151 unsigned long d_timeBudgetPerCall
;
152 /** A user-imposed cumulative resource budget. 0 = no limit. */
153 unsigned long d_resourceBudgetCumulative
;
154 /** A user-imposed per-call resource budget. 0 = no limit. */
155 unsigned long d_resourceBudgetPerCall
;
157 /** The number of milliseconds used by this SmtEngine since its inception. */
158 unsigned long d_cumulativeTimeUsed
;
159 /** The amount of resource used by this SmtEngine since its inception. */
160 unsigned long d_cumulativeResourceUsed
;
163 * Most recent result of last checkSat/query or (set-info :status).
168 * A private utility class to SmtEngine.
170 smt::SmtEnginePrivate
* d_private
;
173 * This is called by the destructor, just before destroying the
174 * PropEngine, TheoryEngine, and DecisionEngine (in that order). It
175 * is important because there are destruction ordering issues
176 * between PropEngine and Theory.
181 * Full check of consistency in current context. Returns true iff
187 * Quick check of consistency in current context: calls
188 * processAssertionList() then look for inconsistency (based only on
194 * Fully type-check the argument, and also type-check that it's
197 void ensureBoolean(const BoolExpr
& e
);
203 friend class ::CVC4::smt::SmtEnginePrivate
;
205 // === STATISTICS ===
206 /** time spent in definition-expansion */
207 TimerStat d_definitionExpansionTime
;
208 /** time spent in non-clausal simplification */
209 TimerStat d_nonclausalSimplificationTime
;
210 /** time spent in static learning */
211 TimerStat d_staticLearningTime
;
216 * Construct an SmtEngine with the given expression manager.
218 SmtEngine(ExprManager
* em
) throw(AssertionException
);
221 * Destruct the SMT engine.
226 * Set the logic of the script.
228 void setLogic(const std::string
& logic
) throw(ModalException
);
231 * Set information about the script executing.
233 void setInfo(const std::string
& key
, const SExpr
& value
)
234 throw(BadOptionException
, ModalException
);
237 * Query information about the SMT environment.
239 SExpr
getInfo(const std::string
& key
) const
240 throw(BadOptionException
);
243 * Set an aspect of the current SMT execution environment.
245 void setOption(const std::string
& key
, const SExpr
& value
)
246 throw(BadOptionException
, ModalException
);
249 * Get an aspect of the current SMT execution environment.
251 SExpr
getOption(const std::string
& key
) const
252 throw(BadOptionException
);
255 * Add a formula to the current context: preprocess, do per-theory
256 * setup, use processAssertionList(), asserting to T-solver for
257 * literals and conjunction of literals. Returns false iff
260 void defineFunction(Expr func
,
261 const std::vector
<Expr
>& formals
,
265 * Add a formula to the current context: preprocess, do per-theory
266 * setup, use processAssertionList(), asserting to T-solver for
267 * literals and conjunction of literals. Returns false iff
270 Result
assertFormula(const BoolExpr
& e
);
273 * Check validity of an expression with respect to the current set
274 * of assertions by asserting the query expression's negation and
275 * calling check(). Returns valid, invalid, or unknown result.
277 Result
query(const BoolExpr
& e
);
280 * Assert a formula (if provided) to the current context and call
281 * check(). Returns sat, unsat, or unknown result.
283 Result
checkSat(const BoolExpr
& e
= BoolExpr());
286 * Simplify a formula without doing "much" work. Does not involve
287 * the SAT Engine in the simplification, but uses the current
288 * assertions and the current partial model, if one has been
291 * @todo (design) is this meant to give an equivalent or an
292 * equisatisfiable formula?
294 Expr
simplify(const Expr
& e
);
297 * Get the assigned value of an expr (only if immediately preceded
298 * by a SAT or INVALID query). Only permitted if the SmtEngine is
299 * set to operate interactively and produce-models is on.
301 Expr
getValue(const Expr
& e
) throw(ModalException
, AssertionException
);
304 * Add a function to the set of expressions whose value is to be
305 * later returned by a call to getAssignment(). The expression
306 * should be a Boolean zero-ary defined function or a Boolean
307 * variable. Rather than throwing a ModalException on modal
308 * failures (not in interactive mode or not producing assignments),
309 * this function returns true if the expression was added and false
310 * if this request was ignored.
312 bool addToAssignment(const Expr
& e
) throw(AssertionException
);
315 * Get the assignment (only if immediately preceded by a SAT or
316 * INVALID query). Only permitted if the SmtEngine is set to
317 * operate interactively and produce-assignments is on.
319 SExpr
getAssignment() throw(ModalException
, AssertionException
);
322 * Get the current set of assertions. Only permitted if the
323 * SmtEngine is set to operate interactively.
325 std::vector
<Expr
> getAssertions() throw(ModalException
, AssertionException
);
328 * Get the current context level.
330 size_t getStackLevel() const;
333 * Push a user-level context.
338 * Pop a user-level context. Throws an exception if nothing to pop.
343 * Interrupt a running query. This can be called from another thread
344 * or from a signal handler. Throws a ModalException if the SmtEngine
345 * isn't currently in a query.
347 void interrupt() throw(ModalException
);
350 * Set a resource limit for SmtEngine operations. This is like a time
351 * limit, but it's deterministic so that reproducible results can be
352 * obtained. However, please note that it may not be deterministic
353 * between different versions of CVC4, or even the same version on
354 * different platforms.
356 * A cumulative and non-cumulative (per-call) resource limit can be
357 * set at the same time. A call to setResourceLimit() with
358 * cumulative==true replaces any cumulative resource limit currently
359 * in effect; a call with cumulative==false replaces any per-call
360 * resource limit currently in effect. Time limits can be set in
361 * addition to resource limits; the SmtEngine obeys both. That means
362 * that up to four independent limits can control the SmtEngine
365 * When an SmtEngine is first created, it has no time or resource
368 * Currently, these limits only cause the SmtEngine to stop what its
369 * doing when the limit expires (or very shortly thereafter); no
370 * heuristics are altered by the limits or the threat of them expiring.
371 * We reserve the right to change this in the future.
373 * @param units the resource limit, or 0 for no limit
374 * @param cumulative whether this resource limit is to be a cumulative
375 * resource limit for all remaining calls into the SmtEngine (true), or
376 * whether it's a per-call resource limit (false); the default is false
378 void setResourceLimit(unsigned long units
, bool cumulative
= false);
381 * Set a time limit for SmtEngine operations.
383 * A cumulative and non-cumulative (per-call) time limit can be
384 * set at the same time. A call to setTimeLimit() with
385 * cumulative==true replaces any cumulative time limit currently
386 * in effect; a call with cumulative==false replaces any per-call
387 * time limit currently in effect. Resource limits can be set in
388 * addition to time limits; the SmtEngine obeys both. That means
389 * that up to four independent limits can control the SmtEngine
392 * Note that the cumulative timer only ticks away when one of the
393 * SmtEngine's workhorse functions (things like assertFormula(),
394 * query(), checkSat(), and simplify()) are running. Between calls,
395 * the timer is still.
397 * When an SmtEngine is first created, it has no time or resource
400 * Currently, these limits only cause the SmtEngine to stop what its
401 * doing when the limit expires (or very shortly thereafter); no
402 * heuristics are altered by the limits or the threat of them expiring.
403 * We reserve the right to change this in the future.
405 * @param millis the time limit in milliseconds, or 0 for no limit
406 * @param cumulative whether this time limit is to be a cumulative
407 * time limit for all remaining calls into the SmtEngine (true), or
408 * whether it's a per-call time limit (false); the default is false
410 void setTimeLimit(unsigned long millis
, bool cumulative
= false);
413 * Get the current resource usage count for this SmtEngine. This
414 * function can be used to ascertain reasonable values to pass as
415 * resource limits to setResourceLimit().
417 unsigned long getResourceUsage() const;
420 * Get the current millisecond count for this SmtEngine.
422 unsigned long getTimeUsage() const;
425 * Get the remaining resources that can be consumed by this SmtEngine
426 * according to the currently-set cumulative resource limit. If there
427 * is not a cumulative resource limit set, this function throws a
430 unsigned long getResourceRemaining() const throw(ModalException
);
433 * Get the remaining number of milliseconds that can be consumed by
434 * this SmtEngine according to the currently-set cumulative time limit.
435 * If there is not a cumulative resource limit set, this function
436 * throws a ModalException.
438 unsigned long getTimeRemaining() const throw(ModalException
);
441 * Permit access to the underlying StatisticsRegistry.
443 StatisticsRegistry
* getStatisticsRegistry() const;
445 };/* class SmtEngine */
447 }/* CVC4 namespace */
449 #endif /* __CVC4__SMT_ENGINE_H */