19 #ifndef __CVC4__SMT_ENGINE_H
20 #define __CVC4__SMT_ENGINE_H
50 struct NodeHashFunction;
60 class StatisticsRegistry;
78 class DefinedFunction;
80 struct SmtEngineStatistics;
81 class SmtEnginePrivate;
83 class BooleanTermConverter;
87 struct CommandCleanup;
88 typedef context::CDList<Command*, CommandCleanup>
CommandList;
113 typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>
116 typedef context::CDList<Expr> AssertionList;
118 typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet;
124 std::vector<int> d_userLevels;
126 context::UserContext* d_userContext;
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;
149 AssignmentSet* d_assignments;
156 std::vector<Command*> d_modelGlobalCommands;
171 std::vector<Command*> d_dumpCommands;
181 unsigned d_pendingPops;
196 bool d_problemExtended;
210 bool d_needPostsolve;
215 bool d_earlyTheoryPP;
218 unsigned long d_timeBudgetCumulative;
220 unsigned long d_timeBudgetPerCall;
222 unsigned long d_resourceBudgetCumulative;
224 unsigned long d_resourceBudgetPerCall;
227 unsigned long d_cumulativeTimeUsed;
229 unsigned long d_cumulativeResourceUsed;
239 std::string d_filename;
244 std::map<std::string, Integer> d_commandVerbosity;
249 smt::SmtEnginePrivate* d_private;
255 void checkModel(
bool hardFailure =
true);
262 Node postprocess(
TNode n, TypeNode expectedType)
const;
273 void finalOptionsAreSet();
310 void internalPop(
bool immediate =
false);
312 void doPendingPops();
318 void setLogicInternal()
throw();
320 friend class ::CVC4::smt::SmtEnginePrivate;
321 friend class ::CVC4::smt::SmtScope;
322 friend class ::CVC4::smt::BooleanTermConverter;
331 StatisticsRegistry* d_statisticsRegistry;
333 smt::SmtEngineStatistics* d_stats;
339 void addToModelCommandAndDump(const
Command& c, uint32_t flags = 0,
bool userVisible = true, const
char* dumpTag = "declarations");
346 Model* getModel() throw(ModalException);
363 void setLogic(const std::
string& logic) throw(ModalException,
LogicException);
368 void setLogic(const
char* logic) throw(ModalException, LogicException);
373 void setLogic(const
LogicInfo& logic) throw(ModalException);
383 void setInfo(const std::
string& key, const
CVC4::
SExpr& value)
389 CVC4::
SExpr getInfo(const std::
string& key) const
390 throw(OptionException, ModalException);
395 void setOption(const std::
string& key, const
CVC4::
SExpr& value)
396 throw(OptionException, ModalException);
401 CVC4::
SExpr getOption(const std::
string& key) const
402 throw(OptionException);
410 void defineFunction(
Expr func,
411 const std::vector<
Expr>& formals,
427 Result query(const
Expr& e) throw(TypeCheckingException, ModalException, LogicException);
433 Result checkSat(const
Expr& e =
Expr()) throw(TypeCheckingException, ModalException, LogicException);
444 Expr simplify(const
Expr& e) throw(TypeCheckingException, LogicException);
457 Expr getValue(const
Expr& e) const throw(ModalException, TypeCheckingException, LogicException);
468 bool addToAssignment(const
Expr& e) throw();
475 CVC4::
SExpr getAssignment() throw(ModalException);
482 Proof* getProof() throw(ModalException);
488 std::vector<
Expr> getAssertions() throw(ModalException);
493 void push() throw(ModalException, LogicException);
498 void pop() throw(ModalException);
505 void interrupt() throw(ModalException);
538 void setResourceLimit(
unsigned long units,
bool cumulative = false);
570 void setTimeLimit(
unsigned long millis,
bool cumulative = false);
577 unsigned long getResourceUsage() const;
582 unsigned long getTimeUsage() const;
590 unsigned long getResourceRemaining() const throw(ModalException);
598 unsigned long getTimeRemaining() const throw(ModalException);
604 return d_exprManager;
615 SExpr getStatistic(std::
string name) const throw();
620 Result getStatusOfLastCommand() const throw() {
629 void setUserAttribute(
const std::string& attr,
Expr expr);
NodeTemplate< true > Node
Class encapsulating CVC4 expressions and methods for constructing new expressions.
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...
[[ Add one-line brief description here ]]
Simple representation of S-expressions.
NodeTemplate< false > TNode
An exception that is thrown when an interactive-only feature while CVC4 is being used in a non-intera...
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
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
Exception thrown in the case of type-checking errors.
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.
[[ Add one-line brief description here ]]
struct CVC4::options::expandDefinitions__option_t expandDefinitions
This is a forward declaration header to declare the CDSet<> template.