cvc4-1.4
CVC4::LogicInfo Class Reference

A LogicInfo instance describes a collection of theory modules and some basic configuration about them. More...

#include <logic_info.h>

Public Member Functions

 LogicInfo ()
 Constructs a LogicInfo for the most general logic (quantifiers, all background theory modules, ...). More...
 
 LogicInfo (std::string logicString) throw (IllegalArgumentException)
 Construct a LogicInfo from an SMT-LIB-like logic string. More...
 
 LogicInfo (const char *logicString) throw (IllegalArgumentException)
 Construct a LogicInfo from an SMT-LIB-like logic string. More...
 
std::string getLogicString () const
 Get an SMT-LIB-like logic string. More...
 
bool isSharingEnabled () const
 Is sharing enabled for this logic? More...
 
bool isTheoryEnabled (theory::TheoryId theory) const
 Is the given theory module active in this logic? More...
 
bool isQuantified () const
 Is this a quantified logic? More...
 
bool hasEverything () const
 Is this the all-inclusive logic? More...
 
bool hasNothing () const
 Is this the all-exclusive logic? (Here, that means propositional logic) More...
 
bool isPure (theory::TheoryId theory) const
 Is this a pure logic (only one "true" background theory). More...
 
bool areIntegersUsed () const
 Are integers in this logic? More...
 
bool areRealsUsed () const
 Are reals in this logic? More...
 
bool isLinear () const
 Does this logic only linear arithmetic? More...
 
bool isDifferenceLogic () const
 Does this logic only permit difference reasoning? (implies linear) More...
 
bool hasCardinalityConstraints () const
 Does this logic allow cardinality constraints? More...
 
void setLogicString (std::string logicString) throw (IllegalArgumentException)
 Initialize the LogicInfo with an SMT-LIB-like logic string. More...
 
void enableEverything ()
 Enable all functionality. More...
 
void disableEverything ()
 Disable all functionality. More...
 
void enableTheory (theory::TheoryId theory)
 Enable the given theory module. More...
 
void disableTheory (theory::TheoryId theory)
 Disable the given theory module. More...
 
void enableQuantifiers ()
 Quantifiers are a special case, since two theory modules handle them. More...
 
void disableQuantifiers ()
 Quantifiers are a special case, since two theory modules handle them. More...
 
void enableIntegers ()
 Enable the use of integers in this logic. More...
 
void disableIntegers ()
 Disable the use of integers in this logic. More...
 
void enableReals ()
 Enable the use of reals in this logic. More...
 
void disableReals ()
 Disable the use of reals in this logic. More...
 
void arithOnlyDifference ()
 Only permit difference arithmetic in this logic. More...
 
void arithOnlyLinear ()
 Only permit linear arithmetic in this logic. More...
 
void arithNonLinear ()
 Permit nonlinear arithmetic in this logic. More...
 
void lock ()
 Lock this LogicInfo, disabling further mutation and allowing queries. More...
 
bool isLocked () const
 Check whether this LogicInfo is locked, disallowing further mutation. More...
 
LogicInfo getUnlockedCopy () const
 Get a copy of this LogicInfo that is identical, but unlocked. More...
 
bool operator== (const LogicInfo &other) const
 Are these two LogicInfos equal? More...
 
bool operator!= (const LogicInfo &other) const
 Are these two LogicInfos disequal? More...
 
bool operator> (const LogicInfo &other) const
 Is this LogicInfo "greater than" (does it contain everything and more) the other? More...
 
bool operator< (const LogicInfo &other) const
 Is this LogicInfo "less than" (does it contain strictly less) the other? More...
 
bool operator<= (const LogicInfo &other) const
 Is this LogicInfo "less than or equal" the other? More...
 
bool operator>= (const LogicInfo &other) const
 Is this LogicInfo "greater than or equal" the other? More...
 
bool isComparableTo (const LogicInfo &other) const
 Are two LogicInfos comparable? That is, is one of <= or > true? More...
 

Detailed Description

A LogicInfo instance describes a collection of theory modules and some basic configuration about them.

Conceptually, it provides a background context for all operations in CVC4. Typically, when CVC4's SmtEngine is created, it is issued a setLogic() command indicating features of the assertions and queries to follow—for example, whether quantifiers are used, whether integers or reals (or both) will be used, etc.

Most places in CVC4 will only ever need to access a const reference to an instance of this class. Such an instance is generally set by the SmtEngine when setLogic() is called. However, mutating member functions are also provided by this class so that it can be used as a more general mechanism (e.g., for communicating to the SmtEngine which theories should be used, rather than having to provide an SMT-LIB string).

Definition at line 45 of file logic_info.h.

Constructor & Destructor Documentation

CVC4::LogicInfo::LogicInfo ( )

Constructs a LogicInfo for the most general logic (quantifiers, all background theory modules, ...).

CVC4::LogicInfo::LogicInfo ( std::string  logicString)
throw (IllegalArgumentException
)

Construct a LogicInfo from an SMT-LIB-like logic string.

Throws an IllegalArgumentException if the logic string cannot be interpreted.

CVC4::LogicInfo::LogicInfo ( const char *  logicString)
throw (IllegalArgumentException
)

Construct a LogicInfo from an SMT-LIB-like logic string.

Throws an IllegalArgumentException if the logic string cannot be interpreted.

Member Function Documentation

bool CVC4::LogicInfo::areIntegersUsed ( ) const
inline

Are integers in this logic?

Definition at line 156 of file logic_info.h.

References CVC4::CheckArgument(), and CVC4::theory::THEORY_ARITH.

bool CVC4::LogicInfo::areRealsUsed ( ) const
inline

Are reals in this logic?

Definition at line 162 of file logic_info.h.

References CVC4::CheckArgument(), and CVC4::theory::THEORY_ARITH.

void CVC4::LogicInfo::arithNonLinear ( )

Permit nonlinear arithmetic in this logic.

void CVC4::LogicInfo::arithOnlyDifference ( )

Only permit difference arithmetic in this logic.

void CVC4::LogicInfo::arithOnlyLinear ( )

Only permit linear arithmetic in this logic.

void CVC4::LogicInfo::disableEverything ( )

Disable all functionality.

The result will be a LogicInfo with the BUILTIN and BOOLEAN theories enabled only ("QF_SAT").

void CVC4::LogicInfo::disableIntegers ( )

Disable the use of integers in this logic.

void CVC4::LogicInfo::disableQuantifiers ( )
inline

Quantifiers are a special case, since two theory modules handle them.

Definition at line 227 of file logic_info.h.

References CVC4::theory::THEORY_QUANTIFIERS.

void CVC4::LogicInfo::disableReals ( )

Disable the use of reals in this logic.

void CVC4::LogicInfo::disableTheory ( theory::TheoryId  theory)

Disable the given theory module.

THEORY_BUILTIN and THEORY_BOOL cannot be disabled (and if given here, the request will be silently ignored).

void CVC4::LogicInfo::enableEverything ( )

Enable all functionality.

All theories, plus quantifiers, will be enabled.

void CVC4::LogicInfo::enableIntegers ( )

Enable the use of integers in this logic.

void CVC4::LogicInfo::enableQuantifiers ( )
inline

Quantifiers are a special case, since two theory modules handle them.

Definition at line 220 of file logic_info.h.

References CVC4::theory::THEORY_QUANTIFIERS.

void CVC4::LogicInfo::enableReals ( )

Enable the use of reals in this logic.

void CVC4::LogicInfo::enableTheory ( theory::TheoryId  theory)

Enable the given theory module.

std::string CVC4::LogicInfo::getLogicString ( ) const

Get an SMT-LIB-like logic string.

These are only guaranteed to be SMT-LIB-compliant if an SMT-LIB-compliant string was used in the constructor and no mutating functions were called.

LogicInfo CVC4::LogicInfo::getUnlockedCopy ( ) const

Get a copy of this LogicInfo that is identical, but unlocked.

bool CVC4::LogicInfo::hasCardinalityConstraints ( ) const
inline

Does this logic allow cardinality constraints?

Definition at line 180 of file logic_info.h.

References CVC4::CheckArgument().

bool CVC4::LogicInfo::hasEverything ( ) const
inline

Is this the all-inclusive logic?

Definition at line 124 of file logic_info.h.

References CVC4::CheckArgument(), and lock().

bool CVC4::LogicInfo::hasNothing ( ) const
inline

Is this the all-exclusive logic? (Here, that means propositional logic)

Definition at line 132 of file logic_info.h.

References CVC4::CheckArgument(), and lock().

bool CVC4::LogicInfo::isComparableTo ( const LogicInfo other) const
inline

Are two LogicInfos comparable? That is, is one of <= or > true?

Definition at line 330 of file logic_info.h.

bool CVC4::LogicInfo::isDifferenceLogic ( ) const
inline

Does this logic only permit difference reasoning? (implies linear)

Definition at line 174 of file logic_info.h.

References CVC4::CheckArgument(), and CVC4::theory::THEORY_ARITH.

bool CVC4::LogicInfo::isLinear ( ) const
inline

Does this logic only linear arithmetic?

Definition at line 168 of file logic_info.h.

References CVC4::CheckArgument(), and CVC4::theory::THEORY_ARITH.

bool CVC4::LogicInfo::isLocked ( ) const
inline

Check whether this LogicInfo is locked, disallowing further mutation.

Definition at line 253 of file logic_info.h.

Referenced by operator<=(), operator==(), and operator>=().

bool CVC4::LogicInfo::isPure ( theory::TheoryId  theory) const
inline

Is this a pure logic (only one "true" background theory).

Quantifiers can exist in such logics though; to test for quantifier-free purity, use "isPure(theory) && !isQuantified()".

Definition at line 144 of file logic_info.h.

References CVC4::CheckArgument().

bool CVC4::LogicInfo::isQuantified ( ) const
inline

Is this a quantified logic?

Definition at line 118 of file logic_info.h.

References CVC4::CheckArgument(), and CVC4::theory::THEORY_QUANTIFIERS.

bool CVC4::LogicInfo::isSharingEnabled ( ) const
inline

Is sharing enabled for this logic?

Definition at line 106 of file logic_info.h.

References CVC4::CheckArgument().

bool CVC4::LogicInfo::isTheoryEnabled ( theory::TheoryId  theory) const
inline

Is the given theory module active in this logic?

Definition at line 112 of file logic_info.h.

References CVC4::CheckArgument().

Referenced by operator<=(), and operator>=().

void CVC4::LogicInfo::lock ( )
inline

Lock this LogicInfo, disabling further mutation and allowing queries.

Definition at line 251 of file logic_info.h.

Referenced by hasEverything(), and hasNothing().

bool CVC4::LogicInfo::operator!= ( const LogicInfo other) const
inline

Are these two LogicInfos disequal?

Definition at line 279 of file logic_info.h.

bool CVC4::LogicInfo::operator< ( const LogicInfo other) const
inline

Is this LogicInfo "less than" (does it contain strictly less) the other?

Definition at line 287 of file logic_info.h.

bool CVC4::LogicInfo::operator<= ( const LogicInfo other) const
inline
bool CVC4::LogicInfo::operator== ( const LogicInfo other) const
inline

Are these two LogicInfos equal?

Definition at line 260 of file logic_info.h.

References CVC4::CheckArgument(), isLocked(), CVC4::theory::THEORY_ARITH, CVC4::theory::THEORY_FIRST, and CVC4::theory::THEORY_LAST.

bool CVC4::LogicInfo::operator> ( const LogicInfo other) const
inline

Is this LogicInfo "greater than" (does it contain everything and more) the other?

Definition at line 283 of file logic_info.h.

bool CVC4::LogicInfo::operator>= ( const LogicInfo other) const
inline

Is this LogicInfo "greater than or equal" the other?

Definition at line 310 of file logic_info.h.

References CVC4::CheckArgument(), isLocked(), isTheoryEnabled(), CVC4::theory::THEORY_ARITH, CVC4::theory::THEORY_FIRST, and CVC4::theory::THEORY_LAST.

void CVC4::LogicInfo::setLogicString ( std::string  logicString)
throw (IllegalArgumentException
)

Initialize the LogicInfo with an SMT-LIB-like logic string.

Throws an IllegalArgumentException if the string can't be interpreted.


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