19 #ifndef __CVC4__SMT_ENGINE_H
20 #define __CVC4__SMT_ENGINE_H
49 struct NodeHashFunction;
62 class StatisticsRegistry;
80 class DefinedFunction;
82 struct SmtEngineStatistics;
83 class SmtEnginePrivate;
85 class BooleanTermConverter;
90 struct CommandCleanup;
91 typedef context::CDList<Command*, CommandCleanup>
CommandList;
116 typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>
119 typedef context::CDList<Expr> AssertionList;
121 typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet;
127 std::vector<int> d_userLevels;
129 context::UserContext* d_userContext;
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;
150 AssertionList* d_assertionList;
155 AssignmentSet* d_assignments;
162 std::vector<Command*> d_modelGlobalCommands;
177 std::vector<Command*> d_dumpCommands;
187 unsigned d_pendingPops;
202 bool d_problemExtended;
216 bool d_needPostsolve;
221 bool d_earlyTheoryPP;
224 unsigned long d_timeBudgetCumulative;
226 unsigned long d_timeBudgetPerCall;
228 unsigned long d_resourceBudgetCumulative;
230 unsigned long d_resourceBudgetPerCall;
233 unsigned long d_cumulativeTimeUsed;
235 unsigned long d_cumulativeResourceUsed;
245 std::string d_filename;
250 std::map<std::string, Integer> d_commandVerbosity;
255 smt::SmtEnginePrivate* d_private;
266 void checkModel(
bool hardFailure =
true);
273 Node postprocess(TNode n, TypeNode expectedType)
const;
281 void finalOptionsAreSet();
324 void internalPop(
bool immediate =
false);
326 void doPendingPops();
332 void setLogicInternal()
throw();
334 friend class ::CVC4::smt::SmtEnginePrivate;
335 friend class ::CVC4::smt::SmtScope;
336 friend class ::CVC4::smt::BooleanTermConverter;
340 friend class ::
CVC4::LogicRequest;
343 friend class ::
CVC4::theory::TheoryModel;
347 StatisticsRegistry* d_statisticsRegistry;
349 smt::SmtEngineStatistics* d_stats;
355 void addToModelCommandAndDump(const
Command& c, uint32_t flags = 0,
bool userVisible = true, const
char* dumpTag = "declarations");
362 Model* getModel() throw(ModalException);
388 void setLogic(const
char* logic) throw(ModalException, LogicException);
393 void setLogic(const
LogicInfo& logic) throw(ModalException);
403 void setInfo(const
std::
string& key, const
CVC4::
SExpr& value)
410 throw(OptionException, ModalException);
415 void setOption(const
std::
string& key, const
CVC4::
SExpr& value)
416 throw(OptionException, ModalException);
422 throw(OptionException);
430 void defineFunction(
Expr func,
431 const
std::vector<
Expr>& formals,
447 Result query(const
Expr& e) throw(TypeCheckingException, ModalException, LogicException);
453 Result checkSat(const
Expr& e =
Expr()) throw(TypeCheckingException, ModalException, LogicException);
464 Expr simplify(const
Expr& e) throw(TypeCheckingException, LogicException);
477 Expr getValue(const
Expr& e) const throw(ModalException, TypeCheckingException, LogicException);
488 bool addToAssignment(const
Expr& e) throw();
495 CVC4::
SExpr getAssignment() throw(ModalException);
502 Proof* getProof() throw(ModalException);
507 void printInstantiations(
std::ostream&
out );
513 std::vector<
Expr> getAssertions() throw(ModalException);
518 void push() throw(ModalException, LogicException);
523 void pop() throw(ModalException);
530 void interrupt() throw(ModalException);
563 void setResourceLimit(
unsigned long units,
bool cumulative = false);
595 void setTimeLimit(
unsigned long millis,
bool cumulative = false);
602 unsigned long getResourceUsage() const;
607 unsigned long getTimeUsage() const;
615 unsigned long getResourceRemaining() const throw(ModalException);
623 unsigned long getTimeRemaining() const throw(ModalException);
629 return d_exprManager;
640 SExpr getStatistic(
std::
string name) const throw();
645 Result getStatusOfLastCommand() const throw() {
654 void setUserAttribute(
const std::string& attr,
Expr expr);
659 void setPrintFuncInModel(
Expr f,
bool p);
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...
Exception thrown in the case of type-checking errors.
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.
struct CVC4::options::out__option_t out
[[ Add one-line brief description here ]]
struct CVC4::options::expandDefinitions__option_t expandDefinitions
This is a forward declaration header to declare the CDSet<> template.
ProofManager * currentProofManager()