cvc4-1.4
smt_engine.h
Go to the documentation of this file.
1 /********************* */
17 #include "cvc4_public.h"
18 
19 #ifndef __CVC4__SMT_ENGINE_H
20 #define __CVC4__SMT_ENGINE_H
21 
22 #include <string>
23 #include <vector>
24 
25 #include "context/cdlist_forward.h"
28 #include "expr/expr.h"
29 #include "expr/expr_manager.h"
30 #include "util/proof.h"
31 #include "smt/modal_exception.h"
32 #include "smt/logic_exception.h"
33 #include "options/options.h"
34 #include "util/result.h"
35 #include "util/sexpr.h"
36 #include "util/hash.h"
37 #include "util/statistics.h"
38 #include "theory/logic_info.h"
39 
40 // In terms of abstraction, this is below (and provides services to)
41 // ValidityChecker and above (and requires the services of)
42 // PropEngine.
43 
44 namespace CVC4 {
45 
46 template <bool ref_count> class NodeTemplate;
47 typedef NodeTemplate<true> Node;
49 struct NodeHashFunction;
50 
51 class Command;
52 class GetModelCommand;
53 
54 class SmtEngine;
55 class DecisionEngine;
56 class TheoryEngine;
57 
58 class ProofManager;
59 
60 class Model;
61 class LogicRequest;
62 class StatisticsRegistry;
63 
64 namespace context {
65  class Context;
66  class UserContext;
67 }/* CVC4::context namespace */
68 
69 namespace prop {
70  class PropEngine;
71 }/* CVC4::prop namespace */
72 
73 namespace smt {
80  class DefinedFunction;
81 
82  struct SmtEngineStatistics;
83  class SmtEnginePrivate;
84  class SmtScope;
85  class BooleanTermConverter;
86 
87  void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
88  ProofManager* currentProofManager();
89 
90  struct CommandCleanup;
91  typedef context::CDList<Command*, CommandCleanup> CommandList;
92 }/* CVC4::smt namespace */
93 
94 namespace theory {
95  class TheoryModel;
96 }/* CVC4::theory namespace */
97 
98 namespace stats {
99  StatisticsRegistry* getStatisticsRegistry(SmtEngine*);
100 }/* CVC4::stats namespace */
101 
102 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
103 // hood): use a type parameter and have check() delegate, or subclass
104 // SmtEngine and override check()?
105 //
106 // Probably better than that is to have a configuration object that
107 // indicates which passes are desired. The configuration occurs
108 // elsewhere (and can even occur at runtime). A simple "pass manager"
109 // of sorts determines check()'s behavior.
110 //
111 // The CNF conversion can go on in PropEngine.
112 
114 
116  typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>
117  DefinedFunctionMap;
119  typedef context::CDList<Expr> AssertionList;
121  typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet;
122 
124  context::Context* d_context;
125 
127  std::vector<int> d_userLevels;
129  context::UserContext* d_userContext;
130 
132  ExprManager* d_exprManager;
134  NodeManager* d_nodeManager;
136  DecisionEngine* d_decisionEngine;
138  TheoryEngine* d_theoryEngine;
140  prop::PropEngine* d_propEngine;
142  ProofManager* d_proofManager;
144  DefinedFunctionMap* d_definedFunctions;
145 
150  AssertionList* d_assertionList;
151 
155  AssignmentSet* d_assignments;
156 
162  std::vector<Command*> d_modelGlobalCommands;
163 
169  smt::CommandList* d_modelCommands;
170 
177  std::vector<Command*> d_dumpCommands;
178 
182  LogicInfo d_logic;
183 
187  unsigned d_pendingPops;
188 
195  bool d_fullyInited;
196 
202  bool d_problemExtended;
203 
210  bool d_queryMade;
211 
216  bool d_needPostsolve;
217 
218  /*
219  * Whether to call theory preprocessing during simplification - on by default* but gets turned off if arithRewriteEq is on
220  */
221  bool d_earlyTheoryPP;
222 
224  unsigned long d_timeBudgetCumulative;
226  unsigned long d_timeBudgetPerCall;
228  unsigned long d_resourceBudgetCumulative;
230  unsigned long d_resourceBudgetPerCall;
231 
233  unsigned long d_cumulativeTimeUsed;
235  unsigned long d_cumulativeResourceUsed;
236 
240  Result d_status;
241 
245  std::string d_filename;
246 
250  std::map<std::string, Integer> d_commandVerbosity;
251 
255  smt::SmtEnginePrivate* d_private;
256 
260  void checkProof();
261 
266  void checkModel(bool hardFailure = true);
267 
273  Node postprocess(TNode n, TypeNode expectedType) const;
274 
281  void finalOptionsAreSet();
282 
287  void setDefaults();
288 
293  void finishInit();
294 
301  void shutdown();
302 
307  Result check();
308 
314  Result quickCheck();
315 
320  void ensureBoolean(const Expr& e) throw(TypeCheckingException);
321 
322  void internalPush();
323 
324  void internalPop(bool immediate = false);
325 
326  void doPendingPops();
327 
332  void setLogicInternal() throw();
333 
334  friend class ::CVC4::smt::SmtEnginePrivate;
335  friend class ::CVC4::smt::SmtScope;
336  friend class ::CVC4::smt::BooleanTermConverter;
337  friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*);
338  friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
339  friend ProofManager* ::CVC4::smt::currentProofManager();
340  friend class ::CVC4::LogicRequest;
341  // to access d_modelCommands
342  friend class ::CVC4::Model;
343  friend class ::CVC4::theory::TheoryModel;
344  // to access getModel(), which is private (for now)
345  friend class GetModelCommand;
346 
347  StatisticsRegistry* d_statisticsRegistry;
348 
349  smt::SmtEngineStatistics* d_stats;
350 
355  void addToModelCommandAndDump(const Command& c, uint32_t flags = 0, bool userVisible = true, const char* dumpTag = "declarations");
356 
362  Model* getModel() throw(ModalException);
363 
364  // disallow copy/assignment
366  SmtEngine& operator=(const SmtEngine&) CVC4_UNDEFINED;
367 
368 public:
369 
373  SmtEngine(ExprManager* em) throw();
374 
378  ~SmtEngine() throw();
379 
383  void setLogic(const std::string& logic) throw(ModalException, LogicException);
384 
388  void setLogic(const char* logic) throw(ModalException, LogicException);
389 
393  void setLogic(const LogicInfo& logic) throw(ModalException);
394 
398  LogicInfo getLogicInfo() const;
399 
403  void setInfo(const std::string& key, const CVC4::SExpr& value)
404  throw(OptionException, ModalException);
405 
409  CVC4::SExpr getInfo(const std::string& key) const
410  throw(OptionException, ModalException);
411 
415  void setOption(const std::string& key, const CVC4::SExpr& value)
416  throw(OptionException, ModalException);
417 
421  CVC4::SExpr getOption(const std::string& key) const
422  throw(OptionException);
423 
430  void defineFunction(Expr func,
431  const std::vector<Expr>& formals,
432  Expr formula);
433 
440  Result assertFormula(const Expr& e) throw(TypeCheckingException, LogicException);
441 
447  Result query(const Expr& e) throw(TypeCheckingException, ModalException, LogicException);
448 
453  Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException, ModalException, LogicException);
454 
464  Expr simplify(const Expr& e) throw(TypeCheckingException, LogicException);
465 
470  Expr expandDefinitions(const Expr& e) throw(TypeCheckingException, LogicException);
471 
477  Expr getValue(const Expr& e) const throw(ModalException, TypeCheckingException, LogicException);
478 
488  bool addToAssignment(const Expr& e) throw();
489 
495  CVC4::SExpr getAssignment() throw(ModalException);
496 
502  Proof* getProof() throw(ModalException);
503 
507  void printInstantiations( std::ostream& out );
508 
513  std::vector<Expr> getAssertions() throw(ModalException);
514 
518  void push() throw(ModalException, LogicException);
519 
523  void pop() throw(ModalException);
524 
530  void interrupt() throw(ModalException);
531 
563  void setResourceLimit(unsigned long units, bool cumulative = false);
564 
595  void setTimeLimit(unsigned long millis, bool cumulative = false);
596 
602  unsigned long getResourceUsage() const;
603 
607  unsigned long getTimeUsage() const;
608 
615  unsigned long getResourceRemaining() const throw(ModalException);
616 
623  unsigned long getTimeRemaining() const throw(ModalException);
624 
628  ExprManager* getExprManager() const {
629  return d_exprManager;
630  }
631 
635  Statistics getStatistics() const throw();
636 
640  SExpr getStatistic(std::string name) const throw();
641 
645  Result getStatusOfLastCommand() const throw() {
646  return d_status;
647  }
648 
654  void setUserAttribute(const std::string& attr, Expr expr);
655 
659  void setPrintFuncInModel(Expr f, bool p);
660 
661 };/* class SmtEngine */
662 
663 }/* CVC4 namespace */
664 
665 #endif /* __CVC4__SMT_ENGINE_H */
NodeTemplate< true > Node
Definition: smt_engine.h:46
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:227
Class representing an option-parsing exception such as badly-typed or missing arguments, arguments out of bounds, etc.
Definition: input.h:32
A class giving information about a logic (group a theory modules and configuration information) ...
StatisticsRegistry * getStatisticsRegistry(SmtEngine *)
A LogicInfo instance describes a collection of theory modules and some basic configuration about them...
Definition: logic_info.h:45
[[ Add one-line brief description here ]]
STL namespace.
Simple representation of S-expressions.
NodeTemplate< false > TNode
Definition: smt_engine.h:48
This is a forward declaration header to declare the CDList<> template.
[[ Add one-line brief description here ]]
This is a forward declaration header to declare the CDHashMap<> template.
Encapsulation of the result of a query.
context::CDList< Command *, CommandCleanup > CommandList
Definition: smt_engine.h:90
void beforeSearch(std::string, bool, SmtEngine *)
An exception that is thrown when a feature is used outside the logic that CVC4 is currently using...
Exception thrown in the case of type-checking errors.
Definition: expr.h:151
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Global (command-line, set-option, ...) parameters for SMT.
Macros that should be defined everywhere during the building of the libraries and driver binary...
Three-valued SMT result, with optional explanation.
Definition: result.h:36
expr_manager.h
#define CVC4_UNDEFINED
Definition: cvc4_public.h:52
struct CVC4::options::out__option_t out
[[ Add one-line brief description here ]]
void * Context
expr.h
A simple S-expression.
Definition: sexpr.h:51
struct CVC4::options::expandDefinitions__option_t expandDefinitions
This is a forward declaration header to declare the CDSet<> template.
ProofManager * currentProofManager()