1 /********************* */
4 ** Original author: mdeters
5 ** Major contributors: dejan
6 ** Minor contributors (to current version): cconway, 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 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/cdhashmap_forward.h"
28 #include "context/cdhashset_forward.h"
29 #include "expr/expr.h"
30 #include "expr/expr_manager.h"
31 #include "util/proof.h"
32 #include "smt/bad_option_exception.h"
33 #include "smt/modal_exception.h"
34 #include "smt/no_such_function_exception.h"
35 #include "util/hash.h"
36 #include "util/options.h"
37 #include "util/result.h"
38 #include "util/sexpr.h"
39 #include "util/stats.h"
40 #include "theory/logic_info.h"
42 // In terms of abstraction, this is below (and provides services to)
43 // ValidityChecker and above (and requires the services of)
49 template <bool ref_count
> class NodeTemplate
;
50 typedef NodeTemplate
<true> Node
;
51 typedef NodeTemplate
<false> TNode
;
52 class NodeHashFunction
;
57 class StatisticsRegistry
;
62 }/* CVC4::context namespace */
66 }/* CVC4::prop namespace */
70 * Representation of a defined function. We keep these around in
71 * SmtEngine to permit expanding definitions late (and lazily), to
72 * support getValue() over defined functions, to support user output
73 * in terms of defined functions, etc.
75 class DefinedFunction
;
77 class SmtEnginePrivate
;
78 }/* CVC4::smt namespace */
80 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
81 // hood): use a type parameter and have check() delegate, or subclass
82 // SmtEngine and override check()?
84 // Probably better than that is to have a configuration object that
85 // indicates which passes are desired. The configuration occurs
86 // elsewhere (and can even occur at runtime). A simple "pass manager"
87 // of sorts determines check()'s behavior.
89 // The CNF conversion can go on in PropEngine.
91 class CVC4_PUBLIC SmtEngine
{
93 /** The type of our internal map of defined functions */
94 typedef context::CDHashMap
<Node
, smt::DefinedFunction
, NodeHashFunction
>
96 /** The type of our internal assertion list */
97 typedef context::CDList
<Expr
> AssertionList
;
98 /** The type of our internal assignment set */
99 typedef context::CDHashSet
<Node
, NodeHashFunction
> AssignmentSet
;
101 /** Expr manager context */
102 context::Context
* d_context
;
104 /** The context levels of user pushes */
105 std::vector
<int> d_userLevels
;
106 /** User level context */
107 context::UserContext
* d_userContext
;
109 /** Our expression manager */
110 ExprManager
* d_exprManager
;
111 /** Our internal expression/node manager */
112 NodeManager
* d_nodeManager
;
113 /** The decision engine */
114 DecisionEngine
* d_decisionEngine
;
115 /** The theory engine */
116 TheoryEngine
* d_theoryEngine
;
117 /** The propositional engine */
118 prop::PropEngine
* d_propEngine
;
119 /** An index of our defined functions */
120 DefinedFunctionMap
* d_definedFunctions
;
122 * The assertion list (before any conversion) for supporting
123 * getAssertions(). Only maintained if in interactive mode.
125 AssertionList
* d_assertionList
;
128 * List of items for which to retrieve values using getAssignment().
130 AssignmentSet
* d_assignments
;
133 * The logic we're in.
138 * Whether the logic has been set yet.
143 * Whether or not we have added any assertions/declarations/definitions
144 * since the last checkSat/query (and therefore we're not responsible
145 * for an assignment).
147 bool d_problemExtended
;
150 * Whether or not a query() or checkSat() has already been made through
151 * this SmtEngine. If true, and incrementalSolving is false, then
152 * attempting an additional query() or checkSat() will fail with a
158 * Internal status flag to indicate whether we've sent a theory
159 * presolve() notification and need to match it with a postsolve().
161 bool d_needPostsolve
;
163 /** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */
164 unsigned long d_timeBudgetCumulative
;
165 /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */
166 unsigned long d_timeBudgetPerCall
;
167 /** A user-imposed cumulative resource budget. 0 = no limit. */
168 unsigned long d_resourceBudgetCumulative
;
169 /** A user-imposed per-call resource budget. 0 = no limit. */
170 unsigned long d_resourceBudgetPerCall
;
172 /** The number of milliseconds used by this SmtEngine since its inception. */
173 unsigned long d_cumulativeTimeUsed
;
174 /** The amount of resource used by this SmtEngine since its inception. */
175 unsigned long d_cumulativeResourceUsed
;
178 * Most recent result of last checkSat/query or (set-info :status).
183 * A private utility class to SmtEngine.
185 smt::SmtEnginePrivate
* d_private
;
188 * This is called by the destructor, just before destroying the
189 * PropEngine, TheoryEngine, and DecisionEngine (in that order). It
190 * is important because there are destruction ordering issues
191 * between PropEngine and Theory.
196 * Full check of consistency in current context. Returns true iff
202 * Quick check of consistency in current context: calls
203 * processAssertionList() then look for inconsistency (based only on
209 * Fully type-check the argument, and also type-check that it's
212 void ensureBoolean(const BoolExpr
& e
);
219 * Internally handle the setting of a logic.
221 void setLogicInternal(const LogicInfo
& logic
) throw();
223 friend class ::CVC4::smt::SmtEnginePrivate
;
225 // === STATISTICS ===
226 /** time spent in definition-expansion */
227 TimerStat d_definitionExpansionTime
;
228 /** time spent in non-clausal simplification */
229 TimerStat d_nonclausalSimplificationTime
;
230 /** time spent in static learning */
231 TimerStat d_staticLearningTime
;
232 /** time spent in simplifying ITEs */
233 TimerStat d_simpITETime
;
234 /** time spent removing ITEs */
235 TimerStat d_iteRemovalTime
;
236 /** time spent in theory preprocessing */
237 TimerStat d_theoryPreprocessTime
;
238 /** time spent converting to CNF */
239 TimerStat d_cnfConversionTime
;
240 /** Num of assertions before ite removal */
241 IntStat d_numAssertionsPre
;
242 /** Num of assertions after ite removal */
243 IntStat d_numAssertionsPost
;
245 /** how the SMT engine got the answer -- SAT solver or DE */
246 BackedStat
<std::string
> d_statResultSource
;
251 * Construct an SmtEngine with the given expression manager.
253 SmtEngine(ExprManager
* em
) throw(AssertionException
);
256 * Destruct the SMT engine.
258 ~SmtEngine() throw();
261 * Set the logic of the script.
263 void setLogic(const std::string
& logic
) throw(ModalException
);
266 * Set the logic of the script.
268 void setLogic(const LogicInfo
& logic
) throw(ModalException
);
271 * Set information about the script executing.
273 void setInfo(const std::string
& key
, const SExpr
& value
)
274 throw(BadOptionException
, ModalException
);
277 * Query information about the SMT environment.
279 SExpr
getInfo(const std::string
& key
) const
280 throw(BadOptionException
);
283 * Set an aspect of the current SMT execution environment.
285 void setOption(const std::string
& key
, const SExpr
& value
)
286 throw(BadOptionException
, ModalException
);
289 * Get an aspect of the current SMT execution environment.
291 SExpr
getOption(const std::string
& key
) const
292 throw(BadOptionException
);
295 * Add a formula to the current context: preprocess, do per-theory
296 * setup, use processAssertionList(), asserting to T-solver for
297 * literals and conjunction of literals. Returns false iff
300 void defineFunction(Expr func
,
301 const std::vector
<Expr
>& formals
,
305 * Add a formula to the current context: preprocess, do per-theory
306 * setup, use processAssertionList(), asserting to T-solver for
307 * literals and conjunction of literals. Returns false iff
310 Result
assertFormula(const BoolExpr
& e
);
313 * Check validity of an expression with respect to the current set
314 * of assertions by asserting the query expression's negation and
315 * calling check(). Returns valid, invalid, or unknown result.
317 Result
query(const BoolExpr
& e
);
320 * Assert a formula (if provided) to the current context and call
321 * check(). Returns sat, unsat, or unknown result.
323 Result
checkSat(const BoolExpr
& e
= BoolExpr());
326 * Simplify a formula without doing "much" work. Does not involve
327 * the SAT Engine in the simplification, but uses the current
328 * assertions and the current partial model, if one has been
331 * @todo (design) is this meant to give an equivalent or an
332 * equisatisfiable formula?
334 Expr
simplify(const Expr
& e
);
337 * Get the assigned value of an expr (only if immediately preceded
338 * by a SAT or INVALID query). Only permitted if the SmtEngine is
339 * set to operate interactively and produce-models is on.
341 Expr
getValue(const Expr
& e
) throw(ModalException
, AssertionException
);
344 * Add a function to the set of expressions whose value is to be
345 * later returned by a call to getAssignment(). The expression
346 * should be a Boolean zero-ary defined function or a Boolean
347 * variable. Rather than throwing a ModalException on modal
348 * failures (not in interactive mode or not producing assignments),
349 * this function returns true if the expression was added and false
350 * if this request was ignored.
352 bool addToAssignment(const Expr
& e
) throw(AssertionException
);
355 * Get the assignment (only if immediately preceded by a SAT or
356 * INVALID query). Only permitted if the SmtEngine is set to
357 * operate interactively and produce-assignments is on.
359 SExpr
getAssignment() throw(ModalException
, AssertionException
);
362 * Get the last proof (only if immediately preceded by an UNSAT
363 * or VALID query). Only permitted if CVC4 was built with proof
364 * support and produce-proofs is on.
366 Proof
* getProof() throw(ModalException
, AssertionException
);
369 * Get the current set of assertions. Only permitted if the
370 * SmtEngine is set to operate interactively.
372 std::vector
<Expr
> getAssertions() throw(ModalException
, AssertionException
);
375 * Get the current context level.
377 size_t getStackLevel() const;
380 * Push a user-level context.
385 * Pop a user-level context. Throws an exception if nothing to pop.
390 * Interrupt a running query. This can be called from another thread
391 * or from a signal handler. Throws a ModalException if the SmtEngine
392 * isn't currently in a query.
394 void interrupt() throw(ModalException
);
397 * Set a resource limit for SmtEngine operations. This is like a time
398 * limit, but it's deterministic so that reproducible results can be
399 * obtained. However, please note that it may not be deterministic
400 * between different versions of CVC4, or even the same version on
401 * different platforms.
403 * A cumulative and non-cumulative (per-call) resource limit can be
404 * set at the same time. A call to setResourceLimit() with
405 * cumulative==true replaces any cumulative resource limit currently
406 * in effect; a call with cumulative==false replaces any per-call
407 * resource limit currently in effect. Time limits can be set in
408 * addition to resource limits; the SmtEngine obeys both. That means
409 * that up to four independent limits can control the SmtEngine
412 * When an SmtEngine is first created, it has no time or resource
415 * Currently, these limits only cause the SmtEngine to stop what its
416 * doing when the limit expires (or very shortly thereafter); no
417 * heuristics are altered by the limits or the threat of them expiring.
418 * We reserve the right to change this in the future.
420 * @param units the resource limit, or 0 for no limit
421 * @param cumulative whether this resource limit is to be a cumulative
422 * resource limit for all remaining calls into the SmtEngine (true), or
423 * whether it's a per-call resource limit (false); the default is false
425 void setResourceLimit(unsigned long units
, bool cumulative
= false);
428 * Set a time limit for SmtEngine operations.
430 * A cumulative and non-cumulative (per-call) time limit can be
431 * set at the same time. A call to setTimeLimit() with
432 * cumulative==true replaces any cumulative time limit currently
433 * in effect; a call with cumulative==false replaces any per-call
434 * time limit currently in effect. Resource limits can be set in
435 * addition to time limits; the SmtEngine obeys both. That means
436 * that up to four independent limits can control the SmtEngine
439 * Note that the cumulative timer only ticks away when one of the
440 * SmtEngine's workhorse functions (things like assertFormula(),
441 * query(), checkSat(), and simplify()) are running. Between calls,
442 * the timer is still.
444 * When an SmtEngine is first created, it has no time or resource
447 * Currently, these limits only cause the SmtEngine to stop what its
448 * doing when the limit expires (or very shortly thereafter); no
449 * heuristics are altered by the limits or the threat of them expiring.
450 * We reserve the right to change this in the future.
452 * @param millis the time limit in milliseconds, or 0 for no limit
453 * @param cumulative whether this time limit is to be a cumulative
454 * time limit for all remaining calls into the SmtEngine (true), or
455 * whether it's a per-call time limit (false); the default is false
457 void setTimeLimit(unsigned long millis
, bool cumulative
= false);
460 * Get the current resource usage count for this SmtEngine. This
461 * function can be used to ascertain reasonable values to pass as
462 * resource limits to setResourceLimit().
464 unsigned long getResourceUsage() const;
467 * Get the current millisecond count for this SmtEngine.
469 unsigned long getTimeUsage() const;
472 * Get the remaining resources that can be consumed by this SmtEngine
473 * according to the currently-set cumulative resource limit. If there
474 * is not a cumulative resource limit set, this function throws a
477 unsigned long getResourceRemaining() const throw(ModalException
);
480 * Get the remaining number of milliseconds that can be consumed by
481 * this SmtEngine according to the currently-set cumulative time limit.
482 * If there is not a cumulative resource limit set, this function
483 * throws a ModalException.
485 unsigned long getTimeRemaining() const throw(ModalException
);
488 * Permit access to the underlying StatisticsRegistry.
490 StatisticsRegistry
* getStatisticsRegistry() const;
492 Result
getStatusOfLastCommand() const {
496 };/* class SmtEngine */
498 }/* CVC4 namespace */
500 #endif /* __CVC4__SMT_ENGINE_H */