cvc4-1.3
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 "util/hash.h"
34 #include "options/options.h"
35 #include "util/result.h"
36 #include "util/sexpr.h"
37 #include "util/hash.h"
38 #include "util/statistics.h"
39 #include "theory/logic_info.h"
40 
41 // In terms of abstraction, this is below (and provides services to)
42 // ValidityChecker and above (and requires the services of)
43 // PropEngine.
44 
45 namespace CVC4 {
46 
47 template <bool ref_count> class NodeTemplate;
48 typedef NodeTemplate<true> Node;
50 struct NodeHashFunction;
51 
52 class Command;
53 class GetModelCommand;
54 
55 class SmtEngine;
56 class DecisionEngine;
57 class TheoryEngine;
58 
59 class Model;
60 class StatisticsRegistry;
61 
62 namespace context {
63  class Context;
64  class UserContext;
65 }/* CVC4::context namespace */
66 
67 namespace prop {
68  class PropEngine;
69 }/* CVC4::prop namespace */
70 
71 namespace smt {
78  class DefinedFunction;
79 
80  struct SmtEngineStatistics;
81  class SmtEnginePrivate;
82  class SmtScope;
83  class BooleanTermConverter;
84 
85  void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
86 
87  struct CommandCleanup;
88  typedef context::CDList<Command*, CommandCleanup> CommandList;
89 }/* CVC4::smt namespace */
90 
91 namespace theory {
92  class TheoryModel;
93 }/* CVC4::theory namespace */
94 
95 namespace stats {
96  StatisticsRegistry* getStatisticsRegistry(SmtEngine*);
97 }/* CVC4::stats namespace */
98 
99 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
100 // hood): use a type parameter and have check() delegate, or subclass
101 // SmtEngine and override check()?
102 //
103 // Probably better than that is to have a configuration object that
104 // indicates which passes are desired. The configuration occurs
105 // elsewhere (and can even occur at runtime). A simple "pass manager"
106 // of sorts determines check()'s behavior.
107 //
108 // The CNF conversion can go on in PropEngine.
109 
111 
113  typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>
114  DefinedFunctionMap;
116  typedef context::CDList<Expr> AssertionList;
118  typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet;
119 
121  context::Context* d_context;
122 
124  std::vector<int> d_userLevels;
126  context::UserContext* d_userContext;
127 
129  ExprManager* d_exprManager;
131  NodeManager* d_nodeManager;
133  DecisionEngine* d_decisionEngine;
135  TheoryEngine* d_theoryEngine;
137  prop::PropEngine* d_propEngine;
139  DefinedFunctionMap* d_definedFunctions;
144  AssertionList* d_assertionList;
145 
149  AssignmentSet* d_assignments;
150 
156  std::vector<Command*> d_modelGlobalCommands;
157 
163  smt::CommandList* d_modelCommands;
164 
171  std::vector<Command*> d_dumpCommands;
172 
176  LogicInfo d_logic;
177 
181  unsigned d_pendingPops;
182 
189  bool d_fullyInited;
190 
196  bool d_problemExtended;
197 
204  bool d_queryMade;
205 
210  bool d_needPostsolve;
211 
212  /*
213  * Whether to call theory preprocessing during simplification - on by default* but gets turned off if arithRewriteEq is on
214  */
215  bool d_earlyTheoryPP;
216 
218  unsigned long d_timeBudgetCumulative;
220  unsigned long d_timeBudgetPerCall;
222  unsigned long d_resourceBudgetCumulative;
224  unsigned long d_resourceBudgetPerCall;
225 
227  unsigned long d_cumulativeTimeUsed;
229  unsigned long d_cumulativeResourceUsed;
230 
234  Result d_status;
235 
239  std::string d_filename;
240 
244  std::map<std::string, Integer> d_commandVerbosity;
245 
249  smt::SmtEnginePrivate* d_private;
250 
255  void checkModel(bool hardFailure = true);
256 
262  Node postprocess(TNode n, TypeNode expectedType) const;
263 
273  void finalOptionsAreSet();
274 
279  void finishInit();
280 
287  void shutdown();
288 
293  Result check();
294 
300  Result quickCheck();
301 
306  void ensureBoolean(const Expr& e) throw(TypeCheckingException);
307 
308  void internalPush();
309 
310  void internalPop(bool immediate = false);
311 
312  void doPendingPops();
313 
318  void setLogicInternal() throw();
319 
320  friend class ::CVC4::smt::SmtEnginePrivate;
321  friend class ::CVC4::smt::SmtScope;
322  friend class ::CVC4::smt::BooleanTermConverter;
323  friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*);
324  friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
325  // to access d_modelCommands
326  friend class ::CVC4::Model;
327  friend class ::CVC4::theory::TheoryModel;
328  // to access getModel(), which is private (for now)
329  friend class GetModelCommand;
330 
331  StatisticsRegistry* d_statisticsRegistry;
332 
333  smt::SmtEngineStatistics* d_stats;
334 
339  void addToModelCommandAndDump(const Command& c, uint32_t flags = 0, bool userVisible = true, const char* dumpTag = "declarations");
340 
346  Model* getModel() throw(ModalException);
347 
348 public:
349 
353  SmtEngine(ExprManager* em) throw();
354 
358  ~SmtEngine() throw();
359 
363  void setLogic(const std::string& logic) throw(ModalException, LogicException);
364 
368  void setLogic(const char* logic) throw(ModalException, LogicException);
369 
373  void setLogic(const LogicInfo& logic) throw(ModalException);
374 
378  LogicInfo getLogicInfo() const;
379 
383  void setInfo(const std::string& key, const CVC4::SExpr& value)
384  throw(OptionException, ModalException);
385 
389  CVC4::SExpr getInfo(const std::string& key) const
390  throw(OptionException, ModalException);
391 
395  void setOption(const std::string& key, const CVC4::SExpr& value)
396  throw(OptionException, ModalException);
397 
401  CVC4::SExpr getOption(const std::string& key) const
402  throw(OptionException);
403 
410  void defineFunction(Expr func,
411  const std::vector<Expr>& formals,
412  Expr formula);
413 
420  Result assertFormula(const Expr& e) throw(TypeCheckingException, LogicException);
421 
427  Result query(const Expr& e) throw(TypeCheckingException, ModalException, LogicException);
428 
433  Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException, ModalException, LogicException);
434 
444  Expr simplify(const Expr& e) throw(TypeCheckingException, LogicException);
445 
450  Expr expandDefinitions(const Expr& e) throw(TypeCheckingException, LogicException);
451 
457  Expr getValue(const Expr& e) const throw(ModalException, TypeCheckingException, LogicException);
458 
468  bool addToAssignment(const Expr& e) throw();
469 
475  CVC4::SExpr getAssignment() throw(ModalException);
476 
482  Proof* getProof() throw(ModalException);
483 
488  std::vector<Expr> getAssertions() throw(ModalException);
489 
493  void push() throw(ModalException, LogicException);
494 
498  void pop() throw(ModalException);
499 
505  void interrupt() throw(ModalException);
506 
538  void setResourceLimit(unsigned long units, bool cumulative = false);
539 
570  void setTimeLimit(unsigned long millis, bool cumulative = false);
571 
577  unsigned long getResourceUsage() const;
578 
582  unsigned long getTimeUsage() const;
583 
590  unsigned long getResourceRemaining() const throw(ModalException);
591 
598  unsigned long getTimeRemaining() const throw(ModalException);
599 
603  ExprManager* getExprManager() const {
604  return d_exprManager;
605  }
606 
610  Statistics getStatistics() const throw();
611 
615  SExpr getStatistic(std::string name) const throw();
616 
620  Result getStatusOfLastCommand() const throw() {
621  return d_status;
622  }
623 
629  void setUserAttribute(const std::string& attr, Expr expr);
630 
631 };/* class SmtEngine */
632 
633 }/* CVC4 namespace */
634 
635 #endif /* __CVC4__SMT_ENGINE_H */
NodeTemplate< true > Node
Definition: smt_engine.h:47
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:226
Class representing an option-parsing exception such as badly-typed or missing arguments, arguments out of bounds, etc.
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 ]]
Simple representation of S-expressions.
NodeTemplate< false > TNode
Definition: smt_engine.h:49
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:87
void beforeSearch(std::string, bool, SmtEngine *)
An exception that is thrown when a feature is used outside the logic that CVC4 is currently using...
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
Definition: README:39
Exception thrown in the case of type-checking errors.
Definition: expr.h:150
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order theory(or a combination of such theories).It is the fourth in the Cooperating Validity Checker family of tools(CVC
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
[[ 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.