cvc4-1.4
CVC4::SmtEngine Class Reference

#include <smt_engine.h>

Public Member Functions

 SmtEngine (ExprManager *em) throw ()
 Construct an SmtEngine with the given expression manager. More...
 
 ~SmtEngine () throw ()
 Destruct the SMT engine. More...
 
void setLogic (const std::string &logic) throw (ModalException, LogicException)
 Set the logic of the script. More...
 
void setLogic (const char *logic) throw (ModalException, LogicException)
 Set the logic of the script. More...
 
void setLogic (const LogicInfo &logic) throw (ModalException)
 Set the logic of the script. More...
 
LogicInfo getLogicInfo () const
 Get the logic information currently set. More...
 
void setInfo (const std::string &key, const CVC4::SExpr &value) throw (OptionException, ModalException)
 Set information about the script executing. More...
 
CVC4::SExpr getInfo (const std::string &key) const throw (OptionException, ModalException)
 Query information about the SMT environment. More...
 
void setOption (const std::string &key, const CVC4::SExpr &value) throw (OptionException, ModalException)
 Set an aspect of the current SMT execution environment. More...
 
CVC4::SExpr getOption (const std::string &key) const throw (OptionException)
 Get an aspect of the current SMT execution environment. More...
 
void defineFunction (Expr func, const std::vector< Expr > &formals, Expr formula)
 Add a formula to the current context: preprocess, do per-theory setup, use processAssertionList(), asserting to T-solver for literals and conjunction of literals. More...
 
Result assertFormula (const Expr &e) throw (TypeCheckingException, LogicException)
 Add a formula to the current context: preprocess, do per-theory setup, use processAssertionList(), asserting to T-solver for literals and conjunction of literals. More...
 
Result query (const Expr &e) throw (TypeCheckingException, ModalException, LogicException)
 Check validity of an expression with respect to the current set of assertions by asserting the query expression's negation and calling check(). More...
 
Result checkSat (const Expr &e=Expr()) throw (TypeCheckingException, ModalException, LogicException)
 Assert a formula (if provided) to the current context and call check(). More...
 
Expr simplify (const Expr &e) throw (TypeCheckingException, LogicException)
 Simplify a formula without doing "much" work. More...
 
Expr expandDefinitions (const Expr &e) throw (TypeCheckingException, LogicException)
 Expand the definitions in a term or formula. More...
 
Expr getValue (const Expr &e) const throw (ModalException, TypeCheckingException, LogicException)
 Get the assigned value of an expr (only if immediately preceded by a SAT or INVALID query). More...
 
bool addToAssignment (const Expr &e) throw ()
 Add a function to the set of expressions whose value is to be later returned by a call to getAssignment(). More...
 
CVC4::SExpr getAssignment () throw (ModalException)
 Get the assignment (only if immediately preceded by a SAT or INVALID query). More...
 
ProofgetProof () throw (ModalException)
 Get the last proof (only if immediately preceded by an UNSAT or VALID query). More...
 
void printInstantiations (std::ostream &out)
 Print all instantiations made by the quantifiers module. More...
 
std::vector< ExprgetAssertions () throw (ModalException)
 Get the current set of assertions. More...
 
void push () throw (ModalException, LogicException)
 Push a user-level context. More...
 
void pop () throw (ModalException)
 Pop a user-level context. More...
 
void interrupt () throw (ModalException)
 Interrupt a running query. More...
 
void setResourceLimit (unsigned long units, bool cumulative=false)
 Set a resource limit for SmtEngine operations. More...
 
void setTimeLimit (unsigned long millis, bool cumulative=false)
 Set a time limit for SmtEngine operations. More...
 
unsigned long getResourceUsage () const
 Get the current resource usage count for this SmtEngine. More...
 
unsigned long getTimeUsage () const
 Get the current millisecond count for this SmtEngine. More...
 
unsigned long getResourceRemaining () const throw (ModalException)
 Get the remaining resources that can be consumed by this SmtEngine according to the currently-set cumulative resource limit. More...
 
unsigned long getTimeRemaining () const throw (ModalException)
 Get the remaining number of milliseconds that can be consumed by this SmtEngine according to the currently-set cumulative time limit. More...
 
ExprManagergetExprManager () const
 Permit access to the underlying ExprManager. More...
 
Statistics getStatistics () const throw ()
 Export statistics from this SmtEngine. More...
 
SExpr getStatistic (std::string name) const throw ()
 Get the value of one named statistic from this SmtEngine. More...
 
Result getStatusOfLastCommand () const throw ()
 Returns the most recent result of checkSat/query or (set-info :status). More...
 
void setUserAttribute (const std::string &attr, Expr expr)
 Set user attribute. More...
 
void setPrintFuncInModel (Expr f, bool p)
 Set print function in model. More...
 

Friends

class ::CVC4::smt::SmtEnginePrivate
 
class ::CVC4::smt::SmtScope
 
class ::CVC4::smt::BooleanTermConverter
 
class ::CVC4::LogicRequest
 
class ::CVC4::Model
 
class ::CVC4::theory::TheoryModel
 
class GetModelCommand
 
friend::CVC4::StatisticsRegistry * CVC4::stats::getStatisticsRegistry (SmtEngine *)
 
ProofManager * CVC4::smt::currentProofManager ()
 

Detailed Description

Definition at line 113 of file smt_engine.h.

Constructor & Destructor Documentation

CVC4::SmtEngine::SmtEngine ( ExprManager em)
throw (
)

Construct an SmtEngine with the given expression manager.

CVC4::SmtEngine::~SmtEngine ( )
throw (
)

Destruct the SMT engine.

Member Function Documentation

bool CVC4::SmtEngine::addToAssignment ( const Expr e)
throw (
)

Add a function to the set of expressions whose value is to be later returned by a call to getAssignment().

The expression should be a Boolean zero-ary defined function or a Boolean variable. Rather than throwing a ModalException on modal failures (not in interactive mode or not producing assignments), this function returns true if the expression was added and false if this request was ignored.

Result CVC4::SmtEngine::assertFormula ( const Expr e)
throw (TypeCheckingException,
LogicException
)

Add a formula to the current context: preprocess, do per-theory setup, use processAssertionList(), asserting to T-solver for literals and conjunction of literals.

Returns false iff inconsistent.

Result CVC4::SmtEngine::checkSat ( const Expr e = Expr())
throw (TypeCheckingException,
ModalException,
LogicException
)

Assert a formula (if provided) to the current context and call check().

Returns sat, unsat, or unknown result.

void CVC4::SmtEngine::defineFunction ( Expr  func,
const std::vector< Expr > &  formals,
Expr  formula 
)

Add a formula to the current context: preprocess, do per-theory setup, use processAssertionList(), asserting to T-solver for literals and conjunction of literals.

Returns false iff inconsistent.

Expr CVC4::SmtEngine::expandDefinitions ( const Expr e)
throw (TypeCheckingException,
LogicException
)

Expand the definitions in a term or formula.

No other simplification or normalization is done.

std::vector<Expr> CVC4::SmtEngine::getAssertions ( )
throw (ModalException
)

Get the current set of assertions.

Only permitted if the SmtEngine is set to operate interactively.

CVC4::SExpr CVC4::SmtEngine::getAssignment ( )
throw (ModalException
)

Get the assignment (only if immediately preceded by a SAT or INVALID query).

Only permitted if the SmtEngine is set to operate interactively and produce-assignments is on.

ExprManager* CVC4::SmtEngine::getExprManager ( ) const
inline

Permit access to the underlying ExprManager.

Definition at line 628 of file smt_engine.h.

CVC4::SExpr CVC4::SmtEngine::getInfo ( const std::string &  key) const
throw (OptionException,
ModalException
)

Query information about the SMT environment.

LogicInfo CVC4::SmtEngine::getLogicInfo ( ) const

Get the logic information currently set.

CVC4::SExpr CVC4::SmtEngine::getOption ( const std::string &  key) const
throw (OptionException
)

Get an aspect of the current SMT execution environment.

Proof* CVC4::SmtEngine::getProof ( )
throw (ModalException
)

Get the last proof (only if immediately preceded by an UNSAT or VALID query).

Only permitted if CVC4 was built with proof support and produce-proofs is on.

unsigned long CVC4::SmtEngine::getResourceRemaining ( ) const
throw (ModalException
)

Get the remaining resources that can be consumed by this SmtEngine according to the currently-set cumulative resource limit.

If there is not a cumulative resource limit set, this function throws a ModalException.

unsigned long CVC4::SmtEngine::getResourceUsage ( ) const

Get the current resource usage count for this SmtEngine.

This function can be used to ascertain reasonable values to pass as resource limits to setResourceLimit().

SExpr CVC4::SmtEngine::getStatistic ( std::string  name) const
throw (
)

Get the value of one named statistic from this SmtEngine.

Statistics CVC4::SmtEngine::getStatistics ( ) const
throw (
)

Export statistics from this SmtEngine.

Result CVC4::SmtEngine::getStatusOfLastCommand ( ) const
throw (
)
inline

Returns the most recent result of checkSat/query or (set-info :status).

Definition at line 645 of file smt_engine.h.

unsigned long CVC4::SmtEngine::getTimeRemaining ( ) const
throw (ModalException
)

Get the remaining number of milliseconds that can be consumed by this SmtEngine according to the currently-set cumulative time limit.

If there is not a cumulative resource limit set, this function throws a ModalException.

unsigned long CVC4::SmtEngine::getTimeUsage ( ) const

Get the current millisecond count for this SmtEngine.

Expr CVC4::SmtEngine::getValue ( const Expr e) const
throw (ModalException,
TypeCheckingException,
LogicException
)

Get the assigned value of an expr (only if immediately preceded by a SAT or INVALID query).

Only permitted if the SmtEngine is set to operate interactively and produce-models is on.

void CVC4::SmtEngine::interrupt ( )
throw (ModalException
)

Interrupt a running query.

This can be called from another thread or from a signal handler. Throws a ModalException if the SmtEngine isn't currently in a query.

void CVC4::SmtEngine::pop ( )
throw (ModalException
)

Pop a user-level context.

Throws an exception if nothing to pop.

void CVC4::SmtEngine::printInstantiations ( std::ostream &  out)

Print all instantiations made by the quantifiers module.

void CVC4::SmtEngine::push ( )
throw (ModalException,
LogicException
)

Push a user-level context.

Result CVC4::SmtEngine::query ( const Expr e)
throw (TypeCheckingException,
ModalException,
LogicException
)

Check validity of an expression with respect to the current set of assertions by asserting the query expression's negation and calling check().

Returns valid, invalid, or unknown result.

void CVC4::SmtEngine::setInfo ( const std::string &  key,
const CVC4::SExpr value 
)
throw (OptionException,
ModalException
)

Set information about the script executing.

void CVC4::SmtEngine::setLogic ( const std::string &  logic)
throw (ModalException,
LogicException
)

Set the logic of the script.

void CVC4::SmtEngine::setLogic ( const char *  logic)
throw (ModalException,
LogicException
)

Set the logic of the script.

void CVC4::SmtEngine::setLogic ( const LogicInfo logic)
throw (ModalException
)

Set the logic of the script.

void CVC4::SmtEngine::setOption ( const std::string &  key,
const CVC4::SExpr value 
)
throw (OptionException,
ModalException
)

Set an aspect of the current SMT execution environment.

void CVC4::SmtEngine::setPrintFuncInModel ( Expr  f,
bool  p 
)

Set print function in model.

void CVC4::SmtEngine::setResourceLimit ( unsigned long  units,
bool  cumulative = false 
)

Set a resource limit for SmtEngine operations.

This is like a time limit, but it's deterministic so that reproducible results can be obtained. Currently, it's based on the number of conflicts. However, please note that the definition may change between different versions of CVC4 (as may the number of conflicts required, anyway), and it might even be different between instances of the same version of CVC4 on different platforms.

A cumulative and non-cumulative (per-call) resource limit can be set at the same time. A call to setResourceLimit() with cumulative==true replaces any cumulative resource limit currently in effect; a call with cumulative==false replaces any per-call resource limit currently in effect. Time limits can be set in addition to resource limits; the SmtEngine obeys both. That means that up to four independent limits can control the SmtEngine at the same time.

When an SmtEngine is first created, it has no time or resource limits.

Currently, these limits only cause the SmtEngine to stop what its doing when the limit expires (or very shortly thereafter); no heuristics are altered by the limits or the threat of them expiring. We reserve the right to change this in the future.

Parameters
unitsthe resource limit, or 0 for no limit
cumulativewhether this resource limit is to be a cumulative resource limit for all remaining calls into the SmtEngine (true), or whether it's a per-call resource limit (false); the default is false
void CVC4::SmtEngine::setTimeLimit ( unsigned long  millis,
bool  cumulative = false 
)

Set a time limit for SmtEngine operations.

A cumulative and non-cumulative (per-call) time limit can be set at the same time. A call to setTimeLimit() with cumulative==true replaces any cumulative time limit currently in effect; a call with cumulative==false replaces any per-call time limit currently in effect. Resource limits can be set in addition to time limits; the SmtEngine obeys both. That means that up to four independent limits can control the SmtEngine at the same time.

Note that the cumulative timer only ticks away when one of the SmtEngine's workhorse functions (things like assertFormula(), query(), checkSat(), and simplify()) are running. Between calls, the timer is still.

When an SmtEngine is first created, it has no time or resource limits.

Currently, these limits only cause the SmtEngine to stop what its doing when the limit expires (or very shortly thereafter); no heuristics are altered by the limits or the threat of them expiring. We reserve the right to change this in the future.

Parameters
millisthe time limit in milliseconds, or 0 for no limit
cumulativewhether this time limit is to be a cumulative time limit for all remaining calls into the SmtEngine (true), or whether it's a per-call time limit (false); the default is false
void CVC4::SmtEngine::setUserAttribute ( const std::string &  attr,
Expr  expr 
)

Set user attribute.

This function is called when an attribute is set by a user. In SMT-LIBv2 this is done via the syntax (! expr :attr)

Expr CVC4::SmtEngine::simplify ( const Expr e)
throw (TypeCheckingException,
LogicException
)

Simplify a formula without doing "much" work.

Does not involve the SAT Engine in the simplification, but uses the current definitions, assertions, and the current partial model, if one has been constructed. It also involves theory normalization.

Todo:
(design) is this meant to give an equivalent or an equisatisfiable formula?

Friends And Related Function Documentation

friend class ::CVC4::LogicRequest
friend

Definition at line 340 of file smt_engine.h.

friend class ::CVC4::Model
friend

Definition at line 342 of file smt_engine.h.

friend class ::CVC4::smt::BooleanTermConverter
friend

Definition at line 336 of file smt_engine.h.

friend class ::CVC4::smt::SmtEnginePrivate
friend

Definition at line 334 of file smt_engine.h.

friend class ::CVC4::smt::SmtScope
friend

Definition at line 335 of file smt_engine.h.

friend class ::CVC4::theory::TheoryModel
friend

Definition at line 343 of file smt_engine.h.

ProofManager* CVC4::smt::currentProofManager ( )
friend
::CVC4::StatisticsRegistry* CVC4::stats::getStatisticsRegistry ( SmtEngine )
friend
friend class GetModelCommand
friend

Definition at line 345 of file smt_engine.h.


The documentation for this class was generated from the following file: