Removing more miscellaneous throw specifiers.
delete d_parser;
}
-Command* InteractiveShell::readCommand() throw (UnsafeInterruptException) {
+Command* InteractiveShell::readCommand()
+{
char* lineBuf = NULL;
string line = "";
* Read a command from the interactive shell. This will read as
* many lines as necessary to parse a well-formed command.
*/
- Command* readCommand() throw (UnsafeInterruptException);
+ Command* readCommand();
/**
* Return the internal parser being used.
default_terminator = set_terminate(cvc4terminate);
}
-void cvc4_shutdown() throw () {
+void cvc4_shutdown() noexcept
+{
#ifndef __WIN32__
#ifdef HAVE_SIGALTSTACK
free(cvc4StackBase);
double d_dbound;
bool d_hasLbound;
-public:
- comparator(int i) throw() : d_lbound(i), d_dbound(0.0), d_hasLbound(true) {}
- comparator(long l) throw() : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {}
- comparator(double d) throw() : d_lbound(0), d_dbound(d), d_hasLbound(false) {}
-
+ public:
+ comparator(int i) : d_lbound(i), d_dbound(0.0), d_hasLbound(true) {}
+ comparator(long l) : d_lbound(l), d_dbound(0.0), d_hasLbound(true) {}
+ comparator(double d) : d_lbound(0), d_dbound(d), d_hasLbound(false) {}
template <class T>
void operator()(std::string option, const T& value) {
if((d_hasLbound && !(Cmp<T>()(value, T(d_lbound)))) ||
};/* class comparator */
struct greater : public comparator<std::greater> {
- greater(int i) throw() : comparator<std::greater>(i) {}
- greater(long l) throw() : comparator<std::greater>(l) {}
- greater(double d) throw() : comparator<std::greater>(d) {}
+ greater(int i) : comparator<std::greater>(i) {}
+ greater(long l) : comparator<std::greater>(l) {}
+ greater(double d) : comparator<std::greater>(d) {}
};/* struct greater */
struct greater_equal : public comparator<std::greater_equal> {
- greater_equal(int i) throw() : comparator<std::greater_equal>(i) {}
- greater_equal(long l) throw() : comparator<std::greater_equal>(l) {}
- greater_equal(double d) throw() : comparator<std::greater_equal>(d) {}
+ greater_equal(int i) : comparator<std::greater_equal>(i) {}
+ greater_equal(long l) : comparator<std::greater_equal>(l) {}
+ greater_equal(double d) : comparator<std::greater_equal>(d) {}
};/* struct greater_equal */
struct less : public comparator<std::less> {
- less(int i) throw() : comparator<std::less>(i) {}
- less(long l) throw() : comparator<std::less>(l) {}
- less(double d) throw() : comparator<std::less>(d) {}
+ less(int i) : comparator<std::less>(i) {}
+ less(long l) : comparator<std::less>(l) {}
+ less(double d) : comparator<std::less>(d) {}
};/* struct less */
struct less_equal : public comparator<std::less_equal> {
- less_equal(int i) throw() : comparator<std::less_equal>(i) {}
- less_equal(long l) throw() : comparator<std::less_equal>(l) {}
- less_equal(double d) throw() : comparator<std::less_equal>(d) {}
+ less_equal(int i) : comparator<std::less_equal>(i) {}
+ less_equal(long l) : comparator<std::less_equal>(l) {}
+ less_equal(double d) : comparator<std::less_equal>(d) {}
};/* struct less_equal */
struct not_equal : public comparator<std::not_equal_to> {
- not_equal(int i) throw() : comparator<std::not_equal_to>(i) {}
- not_equal(long l) throw() : comparator<std::not_equal_to>(l) {}
- not_equal(double d) throw() : comparator<std::not_equal_to>(d) {}
+ not_equal(int i) : comparator<std::not_equal_to>(i) {}
+ not_equal(long l) : comparator<std::not_equal_to>(l) {}
+ not_equal(double d) : comparator<std::not_equal_to>(d) {}
};/* struct not_equal_to */
}/* CVC4::options namespace */
* to the given name. Returns an empty string if there are no
* suggestions.
*/
- static std::string suggestCommandLineOptions(const std::string& optionName) throw();
+ static std::string suggestCommandLineOptions(const std::string& optionName);
/**
* Look up SMT option names that bear some similarity to
* useful in case of typos. Can return an empty vector if there are
* no suggestions.
*/
- static std::vector<std::string> suggestSmtOptions(const std::string& optionName) throw();
+ static std::vector<std::string> suggestSmtOptions(
+ const std::string& optionName);
/**
* Initialize the Options object options based on the given
/**
* Get the setting for all options.
*/
- std::vector< std::vector<std::string> > getOptions() const throw();
-
+ std::vector<std::vector<std::string> > getOptions() const;
/**
* Registers a listener for the notification, notifyBeforeSearch.
}
}
-void OptionsHandler::setProduceAssertions(std::string option, bool value) throw() {
+void OptionsHandler::setProduceAssertions(std::string option, bool value)
+{
options::produceAssertions.set(value);
options::interactiveMode.set(value);
}
SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException);
SygusSolutionOutMode stringToSygusSolutionOutMode(
std::string option, std::string optarg) throw(OptionException);
- void setProduceAssertions(std::string option, bool value) throw();
+ void setProduceAssertions(std::string option, bool value);
void proofEnabledBuild(std::string option, bool value) throw(OptionException);
void LFSCEnabledBuild(std::string option, bool value);
void notifyDumpToFile(std::string option);
free(argv);
}
-std::string Options::suggestCommandLineOptions(const std::string& optionName) throw() {
+std::string Options::suggestCommandLineOptions(const std::string& optionName)
+{
DidYouMean didYouMean;
const char* opt;
NULL
};/* smtOptions[] */
-std::vector<std::string> Options::suggestSmtOptions(const std::string& optionName) throw() {
+std::vector<std::string> Options::suggestSmtOptions(
+ const std::string& optionName)
+{
std::vector<std::string> suggestions;
const char* opt;
return suggestions;
}
-std::vector< std::vector<std::string> > Options::getOptions() const throw() {
+std::vector<std::vector<std::string> > Options::getOptions() const
+{
std::vector< std::vector<std::string> > opts;
${all_modules_get_options}
#include "options/theoryof_mode.h"
#include <ostream>
-#include "base/cvc4_assert.h"
namespace CVC4 {
namespace theory {
-std::ostream& operator<<(std::ostream& out, TheoryOfMode m) throw() {
+std::ostream& operator<<(std::ostream& out, TheoryOfMode m)
+{
switch(m) {
case THEORY_OF_TYPE_BASED: return out << "THEORY_OF_TYPE_BASED";
case THEORY_OF_TERM_BASED: return out << "THEORY_OF_TERM_BASED";
default: return out << "TheoryOfMode!UNKNOWN";
}
-
- Unreachable();
}
}/* CVC4::theory namespace */
THEORY_OF_TERM_BASED
};/* enum TheoryOfMode */
-std::ostream& operator<<(std::ostream& out, TheoryOfMode m) throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, TheoryOfMode m) CVC4_PUBLIC;
}/* CVC4::theory namespace */
}/* CVC4 namespace */
public:
StaticFactManager() {}
- ~StaticFactManager() throw() { }
/**
* Return a Node's union-find representative, doing path compression.
/** Our current offset in the d_trace stack (context-dependent). */
context::CDO<size_t> d_offset;
-public:
+ public:
UnionFind(context::Context* ctxt) :
context::ContextNotifyObj(ctxt),
d_offset(ctxt, 0) {
}
- ~UnionFind() throw() { }
-
/**
* Return a Node's union-find representative, doing path compression.
*/
bool hasBBAtom(TNode atom) const;
TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false);
- ~TLazyBitblaster() throw();
+ ~TLazyBitblaster();
/**
* Pushes the assumption literal associated with node to the SAT
* solver assumption queue.
d_abstraction = abs;
}
-TLazyBitblaster::~TLazyBitblaster() throw() {
+TLazyBitblaster::~TLazyBitblaster()
+{
delete d_cnfStream;
delete d_nullRegistrar;
delete d_nullContext;
return utils::mkConst(d_size, d_bits);
}
- BitVectorEnumerator& operator++() throw() {
+ BitVectorEnumerator& operator++()
+ {
d_bits += 1;
return *this;
}
- bool isFinished() throw() {
- return d_bits != d_bits.modByPow2(d_size);
- }
-
+ bool isFinished() { return d_bits != d_bits.modByPow2(d_size); }
};/* BitVectorEnumerator */
}/* CVC4::theory::bv namespace */
: d_rewrittenLemma(rewrittenLemma), d_level(level) {}
/** Get the T-rewritten form of the lemma. */
- TNode getRewrittenLemma() const throw() { return d_rewrittenLemma; }
-
+ TNode getRewrittenLemma() const { return d_rewrittenLemma; }
/**
* Get the user-level at which the lemma resides. After this user level
* is popped, the lemma is un-asserted from the SAT layer. This level
* will be 0 if the lemma didn't reach the SAT layer at all.
*/
- unsigned getLevel() const throw() { return d_level; }
-
+ unsigned getLevel() const { return d_level; }
private:
Node d_rewrittenLemma;
unsigned d_level;
bool doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n );
public:
AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe );
- ~AbsMbqiBuilder() throw() {}
+
//process build model
- bool processBuildModel(TheoryModel* m);
+ bool processBuildModel(TheoryModel* m) override;
//do exhaustive instantiation
- int doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
+ int doExhaustiveInstantiation(FirstOrderModel* fm,
+ Node q,
+ int effort) override;
};
}
/** candidate generator queue (for manual candidate generation) */
class CandidateGeneratorQueue : public CandidateGenerator {
-private:
+ private:
std::vector< Node > d_candidates;
int d_candidate_index;
-public:
+
+ public:
CandidateGeneratorQueue( QuantifiersEngine* qe ) : CandidateGenerator( qe ), d_candidate_index( 0 ){}
- ~CandidateGeneratorQueue() throw() {}
- void addCandidate( Node n );
+ void addCandidate(Node n) override;
- void resetInstantiationRound(){}
- void reset( Node eqc );
- Node getNextCandidate();
+ void resetInstantiationRound() override {}
+ void reset(Node eqc) override;
+ Node getNextCandidate() override;
};/* class CandidateGeneratorQueue */
//the default generator
class CandidateGeneratorQE : public CandidateGenerator
{
friend class CandidateGeneratorQEDisequal;
-private:
+
+ private:
//operator you are looking for
Node d_op;
//the equality class iterator
bool isLegalOpCandidate( Node n );
Node d_n;
std::map< Node, bool > d_exclude_eqc;
-public:
+
+ public:
CandidateGeneratorQE( QuantifiersEngine* qe, Node pat );
- ~CandidateGeneratorQE() throw() {}
- void resetInstantiationRound();
- void reset( Node eqc );
- Node getNextCandidate();
+ void resetInstantiationRound() override;
+ void reset(Node eqc) override;
+ Node getNextCandidate() override;
void excludeEqc( Node r ) { d_exclude_eqc[r] = true; }
bool isExcludedEqc( Node r ) { return d_exclude_eqc.find( r )!=d_exclude_eqc.end(); }
};
class CandidateGeneratorQELitEq : public CandidateGenerator
{
-private:
+ private:
//the equality classes iterator
eq::EqClassesIterator d_eq;
//equality you are trying to match equalities for
Node d_match_pattern;
Node d_match_gterm;
bool d_do_mgt;
-public:
+
+ public:
CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat );
- ~CandidateGeneratorQELitEq() throw() {}
- void resetInstantiationRound();
- void reset( Node eqc );
- Node getNextCandidate();
+ void resetInstantiationRound() override;
+ void reset(Node eqc) override;
+ Node getNextCandidate() override;
};
class CandidateGeneratorQELitDeq : public CandidateGenerator
{
-private:
+ private:
//the equality class iterator for false
eq::EqClassIterator d_eqc_false;
//equality you are trying to match disequalities for
Node d_match_pattern;
//type of disequality
TypeNode d_match_pattern_type;
-public:
+
+ public:
CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat );
- ~CandidateGeneratorQELitDeq() throw() {}
- void resetInstantiationRound();
- void reset( Node eqc );
- Node getNextCandidate();
+ void resetInstantiationRound() override;
+ void reset(Node eqc) override;
+ Node getNextCandidate() override;
};
class CandidateGeneratorQEAll : public CandidateGenerator
{
-private:
+ private:
//the equality classes iterator
eq::EqClassesIterator d_eq;
//equality you are trying to match equalities for
unsigned d_index;
//first time
bool d_firstTime;
-public:
+
+ public:
CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat );
- ~CandidateGeneratorQEAll() throw() {}
- void resetInstantiationRound();
- void reset( Node eqc );
- Node getNextCandidate();
+ void resetInstantiationRound() override;
+ void reset(Node eqc) override;
+ Node getNextCandidate() override;
};
}/* CVC4::theory::inst namespace */
unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth );
public:
ConjectureGenerator( QuantifiersEngine * qe, context::Context* c );
- ~ConjectureGenerator() throw() {}
+
/* needs check */
bool needsCheck( Theory::Effort e );
/* reset at a round */
}
-FirstOrderModelFmc::~FirstOrderModelFmc() throw() {
+FirstOrderModelFmc::~FirstOrderModelFmc()
+{
for(std::map<Node, Def*>::iterator i = d_models.begin(); i != d_models.end(); ++i) {
delete (*i).second;
}
}
-FirstOrderModelAbs::~FirstOrderModelAbs() throw() {
+FirstOrderModelAbs::~FirstOrderModelAbs()
+{
for(std::map<Node, AbsDef*>::iterator i = d_models.begin(); i != d_models.end(); ++i) {
delete (*i).second;
}
{
public:
FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name);
- virtual ~FirstOrderModel() throw() {}
+
virtual FirstOrderModelIG* asFirstOrderModelIG() { return nullptr; }
virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; }
virtual FirstOrderModelQInt* asFirstOrderModelQInt() { return nullptr; }
//the following functions are for evaluating quantifier bodies
public:
FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name);
- ~FirstOrderModelIG() throw() {}
+
FirstOrderModelIG * asFirstOrderModelIG() { return this; }
// initialize the model
void processInitialize( bool ispre );
void processInitializeModelForTerm(Node n);
public:
FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
- virtual ~FirstOrderModelFmc() throw();
+ ~FirstOrderModelFmc() override;
FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
// initialize the model
void processInitialize( bool ispre );
class FirstOrderModelAbs : public FirstOrderModel
{
-public:
+ public:
std::map< Node, AbsDef * > d_models;
std::map< Node, bool > d_models_valid;
std::map< TNode, unsigned > d_rep_id;
std::map< TypeNode, unsigned > d_domain;
std::map< Node, std::vector< int > > d_var_order;
std::map< Node, std::map< int, int > > d_var_index;
-private:
+
+ private:
/** get current model value */
- void processInitializeModelForTerm(Node n);
- void processInitializeQuantifier( Node q );
+ void processInitializeModelForTerm(Node n) override;
+ void processInitializeQuantifier(Node q) override;
void collectEqVars( TNode q, TNode n, std::map< int, bool >& eq_vars );
TNode getUsedRepresentative( TNode n );
-public:
+
+ public:
FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name);
- ~FirstOrderModelAbs() throw();
- FirstOrderModelAbs * asFirstOrderModelAbs() { return this; }
- void processInitialize( bool ispre );
+ ~FirstOrderModelAbs() override;
+ FirstOrderModelAbs* asFirstOrderModelAbs() override { return this; }
+ void processInitialize(bool ispre) override;
unsigned getRepresentativeId( TNode n );
bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); }
Node getFunctionValue(Node op, const char* argPrefix );
Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
public:
FullModelChecker( context::Context* c, QuantifiersEngine* qe );
- ~FullModelChecker() throw() {}
void debugPrintCond(const char * tr, Node n, bool dispStar = false);
void debugPrint(const char * tr, Node n, bool dispStar = false);
d_independent_gen = false;
}
-InstMatchGenerator::~InstMatchGenerator() throw() {
+InstMatchGenerator::~InstMatchGenerator()
+{
for( unsigned i=0; i<d_children.size(); i++ ){
delete d_children[i];
}
}
}
-InstMatchGeneratorMultiLinear::~InstMatchGeneratorMultiLinear() throw() {
-
-}
-
int InstMatchGeneratorMultiLinear::resetChildren( QuantifiersEngine* qe ){
for( unsigned i=0; i<d_children.size(); i++ ){
if( !d_children[i]->reset( Node::null(), qe ) ){
}
}
-InstMatchGeneratorMulti::~InstMatchGeneratorMulti() throw() {
+InstMatchGeneratorMulti::~InstMatchGeneratorMulti()
+{
for( unsigned i=0; i<d_children.size(); i++ ){
delete d_children[i];
}
* ground terms not in the equivalence class of b.
*/
class InstMatchGenerator : public IMGenerator {
-public:
- /** destructor */
- virtual ~InstMatchGenerator() throw();
+ public:
+ /** destructor */
+ ~InstMatchGenerator() override;
- /** Reset instantiation round. */
- void resetInstantiationRound(QuantifiersEngine* qe) override;
- /** Reset. */
- bool reset(Node eqc, QuantifiersEngine* qe) override;
- /** Get the next match. */
- int getNextMatch(Node q,
- InstMatch& m,
- QuantifiersEngine* qe,
- Trigger* tparent) override;
- /** Add instantiations. */
- int addInstantiations(Node q,
- QuantifiersEngine* qe,
- Trigger* tparent) override;
+ /** Reset instantiation round. */
+ void resetInstantiationRound(QuantifiersEngine* qe) override;
+ /** Reset. */
+ bool reset(Node eqc, QuantifiersEngine* qe) override;
+ /** Get the next match. */
+ int getNextMatch(Node q,
+ InstMatch& m,
+ QuantifiersEngine* qe,
+ Trigger* tparent) override;
+ /** Add instantiations. */
+ int addInstantiations(Node q,
+ QuantifiersEngine* qe,
+ Trigger* tparent) override;
- /** set active add flag (true by default)
- *
- * If active add is true, we call sendInstantiation in calls to getNextMatch,
- * instead of returning the match. This is necessary so that we can ensure
- * policies that are dependent upon knowing when instantiations are
- * successfully added to the output channel through
- * Instantiate::addInstantiation(...).
- */
- void setActiveAdd(bool val);
- /** Get active score for this inst match generator
- *
- * See Trigger::getActiveScore for details.
+ /** set active add flag (true by default)
+ *
+ * If active add is true, we call sendInstantiation in calls to getNextMatch,
+ * instead of returning the match. This is necessary so that we can ensure
+ * policies that are dependent upon knowing when instantiations are
+ * successfully added to the output channel through
+ * Instantiate::addInstantiation(...).
*/
- int getActiveScore(QuantifiersEngine* qe);
- /** exclude match
- *
- * Exclude matching d_match_pattern with Node n on subsequent calls to
- * getNextMatch.
+ void setActiveAdd(bool val);
+ /** Get active score for this inst match generator
+ *
+ * See Trigger::getActiveScore for details.
+ */
+ int getActiveScore(QuantifiersEngine* qe);
+ /** exclude match
+ *
+ * Exclude matching d_match_pattern with Node n on subsequent calls to
+ * getNextMatch.
+ */
+ void excludeMatch(Node n) { d_curr_exclude_match[n] = true; }
+ /** Get current match.
+ * Returns the term we are currently matching.
+ */
+ Node getCurrentMatch() { return d_curr_matched; }
+ /** set that this match generator is independent
+ *
+ * A match generator is indepndent when this generator fails to produce a
+ * match in a call to getNextMatch, the overall matching fails.
*/
- void excludeMatch(Node n) { d_curr_exclude_match[n] = true; }
- /** Get current match.
- * Returns the term we are currently matching.
+ void setIndependent() { d_independent_gen = true; }
+ //-------------------------------construction of inst match generators
+ /** mkInstMatchGenerator for single triggers, calls the method below */
+ static InstMatchGenerator* mkInstMatchGenerator(Node q,
+ Node pat,
+ QuantifiersEngine* qe);
+ /** mkInstMatchGenerator for the multi trigger case
+ *
+ * This linked list of InstMatchGenerator classes with one
+ * InstMatchGeneratorMultiLinear at the head and a list of trailing
+ * InstMatchGenerators corresponding to each unique subterm of pats with
+ * free variables.
*/
- Node getCurrentMatch() { return d_curr_matched; }
- /** set that this match generator is independent
+ static InstMatchGenerator* mkInstMatchGeneratorMulti(Node q,
+ std::vector<Node>& pats,
+ QuantifiersEngine* qe);
+ /** mkInstMatchGenerator
*
- * A match generator is indepndent when this generator fails to produce a
- * match in a call to getNextMatch, the overall matching fails.
- */
- void setIndependent() { d_independent_gen = true; }
- //-------------------------------construction of inst match generators
- /** mkInstMatchGenerator for single triggers, calls the method below */
- static InstMatchGenerator* mkInstMatchGenerator(Node q,
- Node pat,
- QuantifiersEngine* qe);
- /** mkInstMatchGenerator for the multi trigger case
- *
- * This linked list of InstMatchGenerator classes with one
- * InstMatchGeneratorMultiLinear at the head and a list of trailing
- * InstMatchGenerators corresponding to each unique subterm of pats with
- * free variables.
- */
- static InstMatchGenerator* mkInstMatchGeneratorMulti(Node q,
- std::vector<Node>& pats,
- QuantifiersEngine* qe);
- /** mkInstMatchGenerator
- *
- * This generates a linked list of InstMatchGenerators for each unique
- * subterm of pats with free variables.
- *
- * q is the quantified formula associated with the generator we are making
- * pats is a set of terms we are making InstMatchGenerator nodes for
- * qe is a pointer to the quantifiers engine (used for querying necessary
- * information during initialization) pat_map_init maps from terms to
- * generators we have already made for them.
- *
- * It calls initialize(...) for all InstMatchGenerators generated by this call.
- */
- static InstMatchGenerator* mkInstMatchGenerator(
- Node q,
- std::vector<Node>& pats,
- QuantifiersEngine* qe,
- std::map<Node, InstMatchGenerator*>& pat_map_init);
- //-------------------------------end construction of inst match generators
-
-protected:
- /** constructors
+ * This generates a linked list of InstMatchGenerators for each unique
+ * subterm of pats with free variables.
*
- * These are intentionally private, and are called during linked list
- * construction in mkInstMatchGenerator.
- */
- InstMatchGenerator(Node pat);
- InstMatchGenerator();
- /** The pattern we are producing matches for.
+ * q is the quantified formula associated with the generator we are making
+ * pats is a set of terms we are making InstMatchGenerator nodes for
+ * qe is a pointer to the quantifiers engine (used for querying necessary
+ * information during initialization) pat_map_init maps from terms to
+ * generators we have already made for them.
*
- * This term and d_match_pattern can be different since this
- * term may involve information regarding phase and (dis)equality entailment,
- * or other special cases of Triggers.
- *
- * For example, for the trigger for P( x ) = false, which matches P( x ) with
- * P( t ) in the equivalence class of false,
- * P( x ) = false is d_pattern
- * P( x ) is d_match_pattern
- * Another example, for pure theory triggers like head( x ), we have
- * head( x ) is d_pattern
- * x is d_match_pattern
- * since head( x ) can match any (List) datatype term x.
- *
- * If null, this is a multi trigger that is merging matches from d_children,
- * which is used in InstMatchGeneratorMulti.
- */
- Node d_pattern;
- /** The match pattern
- * This is the term that is matched against ground terms,
- * see examples above.
- */
- Node d_match_pattern;
- /** The current term we are matching. */
- Node d_curr_matched;
- /** do we need to call reset on this generator? */
- bool d_needsReset;
- /** candidate generator
- * This is the back-end utility for InstMatchGenerator.
- * It generates a stream of candidate terms to match against d_match_pattern
- * below, dependending upon what kind of term we are matching
- * (e.g. a matchable term, a variable, a relation, etc.).
+ * It calls initialize(...) for all InstMatchGenerators generated by this call.
*/
- CandidateGenerator* d_cg;
- /** children generators
- * These match generators correspond to the children of the term
- * we are matching with this generator.
- * For example [ f( x, a ) ] is a child of [ f( y, f( x, a ) ) ]
- * in the example (EX1) above.
- */
- std::vector<InstMatchGenerator*> d_children;
- /** for each child, the index in the term
- * For example [ f( x, a ) ] has index 1 in [ f( y, f( x, a ) ) ]
- * in the example (EX1) above, indicating it is the 2nd child
- * of the term.
+ static InstMatchGenerator* mkInstMatchGenerator(
+ Node q,
+ std::vector<Node>& pats,
+ QuantifiersEngine* qe,
+ std::map<Node, InstMatchGenerator*>& pat_map_init);
+ //-------------------------------end construction of inst match generators
+
+ protected:
+ /** constructors
+ *
+ * These are intentionally private, and are called during linked list
+ * construction in mkInstMatchGenerator.
*/
- std::vector<int> d_children_index;
- /** children types
+ InstMatchGenerator(Node pat);
+ InstMatchGenerator();
+ /** The pattern we are producing matches for.
+ *
+ * This term and d_match_pattern can be different since this
+ * term may involve information regarding phase and (dis)equality entailment,
+ * or other special cases of Triggers.
*
- * If d_match_pattern is an instantiation constant, then this is a singleton
- * vector containing the variable number of the d_match_pattern itself.
- * If d_match_patterm is a term of the form f( t1, ..., tn ), then for each
- * index i, d_children[i] stores the type of node ti is, where:
- * >= 0 : variable (indicates its number),
- * -1 : ground term,
- * -2 : child term.
- */
- std::vector<int> d_children_types;
- /** The next generator in the linked list
- * that this generator is a part of.
- */
- InstMatchGenerator* d_next;
- /** The equivalence class we are currently matching in. */
- Node d_eq_class;
- /** If non-null, then this is a relational trigger of the form x ~
- * d_eq_class_rel. */
- Node d_eq_class_rel;
- /** Excluded matches
- * Stores the terms we are not allowed to match.
- * These can for instance be specified by the smt2
- * extended syntax (! ... :no-pattern).
- */
- std::map<Node, bool> d_curr_exclude_match;
- /** Current first candidate
- * Used in a key fail-quickly optimization which generates
- * the first candidate term to match during reset().
- */
- Node d_curr_first_candidate;
- /** Indepdendent generate
- * If this flag is true, failures to match should be cached.
- */
- bool d_independent_gen;
- /** active add flag, described above. */
- bool d_active_add;
- /** cached value of d_match_pattern.getType() */
- TypeNode d_match_pattern_type;
- /** the match operator for d_match_pattern
+ * For example, for the trigger for P( x ) = false, which matches P( x ) with
+ * P( t ) in the equivalence class of false,
+ * P( x ) = false is d_pattern
+ * P( x ) is d_match_pattern
+ * Another example, for pure theory triggers like head( x ), we have
+ * head( x ) is d_pattern
+ * x is d_match_pattern
+ * since head( x ) can match any (List) datatype term x.
*
- * See TermDatabase::getMatchOperator for details on match operators.
+ * If null, this is a multi trigger that is merging matches from d_children,
+ * which is used in InstMatchGeneratorMulti.
*/
- Node d_match_pattern_op;
- /** get the match against ground term or formula t.
- *
- * d_match_pattern and t should have the same shape, that is,
- * their match operator (see TermDatabase::getMatchOperator) is the same.
- * only valid for use where !d_match_pattern.isNull().
+ Node d_pattern;
+ /** The match pattern
+ * This is the term that is matched against ground terms,
+ * see examples above.
+ */
+ Node d_match_pattern;
+ /** The current term we are matching. */
+ Node d_curr_matched;
+ /** do we need to call reset on this generator? */
+ bool d_needsReset;
+ /** candidate generator
+ * This is the back-end utility for InstMatchGenerator.
+ * It generates a stream of candidate terms to match against d_match_pattern
+ * below, dependending upon what kind of term we are matching
+ * (e.g. a matchable term, a variable, a relation, etc.).
+ */
+ CandidateGenerator* d_cg;
+ /** children generators
+ * These match generators correspond to the children of the term
+ * we are matching with this generator.
+ * For example [ f( x, a ) ] is a child of [ f( y, f( x, a ) ) ]
+ * in the example (EX1) above.
+ */
+ std::vector<InstMatchGenerator*> d_children;
+ /** for each child, the index in the term
+ * For example [ f( x, a ) ] has index 1 in [ f( y, f( x, a ) ) ]
+ * in the example (EX1) above, indicating it is the 2nd child
+ * of the term.
+ */
+ std::vector<int> d_children_index;
+ /** children types
+ *
+ * If d_match_pattern is an instantiation constant, then this is a singleton
+ * vector containing the variable number of the d_match_pattern itself.
+ * If d_match_patterm is a term of the form f( t1, ..., tn ), then for each
+ * index i, d_children[i] stores the type of node ti is, where:
+ * >= 0 : variable (indicates its number),
+ * -1 : ground term,
+ * -2 : child term.
+ */
+ std::vector<int> d_children_types;
+ /** The next generator in the linked list
+ * that this generator is a part of.
+ */
+ InstMatchGenerator* d_next;
+ /** The equivalence class we are currently matching in. */
+ Node d_eq_class;
+ /** If non-null, then this is a relational trigger of the form x ~
+ * d_eq_class_rel. */
+ Node d_eq_class_rel;
+ /** Excluded matches
+ * Stores the terms we are not allowed to match.
+ * These can for instance be specified by the smt2
+ * extended syntax (! ... :no-pattern).
*/
- int getMatch(
- Node q, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent);
- /** Initialize this generator.
- *
- * q is the quantified formula associated with this generator.
- *
- * This constructs the appropriate information about what
- * patterns we are matching and children generators.
- *
- * It may construct new (child) generators needed to implement
- * the matching algorithm for this term. For each new generator
- * constructed in this way, it adds them to gens.
+ std::map<Node, bool> d_curr_exclude_match;
+ /** Current first candidate
+ * Used in a key fail-quickly optimization which generates
+ * the first candidate term to match during reset().
*/
- void initialize(Node q,
- QuantifiersEngine* qe,
- std::vector<InstMatchGenerator*>& gens);
- /** Continue next match
- *
- * This is called during getNextMatch when the current generator in the linked
- * list succesfully satisfies its matching constraint. This function either
- * calls getNextMatch of the next element in the linked list, or finalizes the
- * match (calling sendInstantiation(...) if active add is true, or returning a
- * value >0 if active add is false). Its return value has the same semantics
- * as getNextMatch.
- */
- int continueNextMatch(Node q,
- InstMatch& m,
- QuantifiersEngine* qe,
- Trigger* tparent);
- /** Get inst match generator
- *
- * Gets the InstMatchGenerator that implements the
- * appropriate matching algorithm for n within q
- * within a linked list of InstMatchGenerators.
+ Node d_curr_first_candidate;
+ /** Indepdendent generate
+ * If this flag is true, failures to match should be cached.
*/
- static InstMatchGenerator* getInstMatchGenerator(Node q, Node n);
+ bool d_independent_gen;
+ /** active add flag, described above. */
+ bool d_active_add;
+ /** cached value of d_match_pattern.getType() */
+ TypeNode d_match_pattern_type;
+ /** the match operator for d_match_pattern
+ *
+ * See TermDatabase::getMatchOperator for details on match operators.
+ */
+ Node d_match_pattern_op;
+ /** get the match against ground term or formula t.
+ *
+ * d_match_pattern and t should have the same shape, that is,
+ * their match operator (see TermDatabase::getMatchOperator) is the same.
+ * only valid for use where !d_match_pattern.isNull().
+ */
+ int getMatch(
+ Node q, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent);
+ /** Initialize this generator.
+ *
+ * q is the quantified formula associated with this generator.
+ *
+ * This constructs the appropriate information about what
+ * patterns we are matching and children generators.
+ *
+ * It may construct new (child) generators needed to implement
+ * the matching algorithm for this term. For each new generator
+ * constructed in this way, it adds them to gens.
+ */
+ void initialize(Node q,
+ QuantifiersEngine* qe,
+ std::vector<InstMatchGenerator*>& gens);
+ /** Continue next match
+ *
+ * This is called during getNextMatch when the current generator in the linked
+ * list succesfully satisfies its matching constraint. This function either
+ * calls getNextMatch of the next element in the linked list, or finalizes the
+ * match (calling sendInstantiation(...) if active add is true, or returning a
+ * value >0 if active add is false). Its return value has the same semantics
+ * as getNextMatch.
+ */
+ int continueNextMatch(Node q,
+ InstMatch& m,
+ QuantifiersEngine* qe,
+ Trigger* tparent);
+ /** Get inst match generator
+ *
+ * Gets the InstMatchGenerator that implements the
+ * appropriate matching algorithm for n within q
+ * within a linked list of InstMatchGenerators.
+ */
+ static InstMatchGenerator* getInstMatchGenerator(Node q, Node n);
};/* class InstMatchGenerator */
/** match generator for Boolean term ITEs
class VarMatchGeneratorBooleanTerm : public InstMatchGenerator {
public:
VarMatchGeneratorBooleanTerm( Node var, Node comp );
- virtual ~VarMatchGeneratorBooleanTerm() throw() {}
+
/** Reset */
bool reset(Node eqc, QuantifiersEngine* qe) override
{
class VarMatchGeneratorTermSubs : public InstMatchGenerator {
public:
VarMatchGeneratorTermSubs( Node var, Node subs );
- virtual ~VarMatchGeneratorTermSubs() throw() {}
+
/** Reset */
bool reset(Node eqc, QuantifiersEngine* qe) override
{
friend class InstMatchGenerator;
public:
- /** destructor */
- virtual ~InstMatchGeneratorMultiLinear() throw();
-
/** Reset. */
bool reset(Node eqc, QuantifiersEngine* qe) override;
/** Get the next match. */
std::vector<Node>& pats,
QuantifiersEngine* qe);
/** destructor */
- virtual ~InstMatchGeneratorMulti() throw();
+ ~InstMatchGeneratorMulti() override;
/** Reset instantiation round. */
void resetInstantiationRound(QuantifiersEngine* qe) override;
public:
/** constructors */
InstMatchGeneratorSimple(Node q, Node pat, QuantifiersEngine* qe);
- /** destructor */
- ~InstMatchGeneratorSimple() throw() {}
+
/** Reset instantiation round. */
void resetInstantiationRound(QuantifiersEngine* qe) override;
/** Add instantiations. */
d_qid_count = 0;
}
-InstStrategyCbqi::~InstStrategyCbqi() throw(){}
-
bool InstStrategyCbqi::needsCheck( Theory::Effort e ) {
return e>=Theory::EFFORT_LAST_CALL;
}
d_check_vts_lemma_lc = false;
}
-InstStrategyCegqi::~InstStrategyCegqi() throw () {
+InstStrategyCegqi::~InstStrategyCegqi()
+{
delete d_out;
for(std::map< Node, CegInstantiator * >::iterator i = d_cinst.begin(),
class InstStrategyCbqi : public QuantifiersModule {
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
-protected:
+
+ protected:
bool d_cbqi_set_quant_inactive;
bool d_incomplete_check;
/** whether we have added cbqi lemma */
/** process functions */
virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
virtual void process( Node q, Theory::Effort effort, int e ) = 0;
-protected:
+
+ protected:
//for identification
uint64_t d_qid_count;
//nested qe map
NodeIntMap d_nested_qe_waitlist_size;
NodeIntMap d_nested_qe_waitlist_proc;
std::map< Node, std::vector< Node > > d_nested_qe_waitlist;
-public:
+
+ public:
//do nested quantifier elimination
Node doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts );
-public:
+
+ public:
InstStrategyCbqi( QuantifiersEngine * qe );
- ~InstStrategyCbqi() throw();
+
/** whether to do CBQI for quantifier q */
bool doCbqi( Node q );
/** process functions */
void registerCounterexampleLemma( Node q, Node lem );
public:
InstStrategyCegqi( QuantifiersEngine * qe );
- ~InstStrategyCegqi() throw();
+ ~InstStrategyCegqi() override;
bool doAddInstantiation( std::vector< Node >& subs );
bool isEligibleForInstantiation( Node n );
unsigned d_triedLemmas;
public:
QModelBuilder( context::Context* c, QuantifiersEngine* qe );
- virtual ~QModelBuilder() throw() {}
+
//do exhaustive instantiation
// 0 : failed, but resorting to true exhaustive instantiation may work
// >0 : success
class QModelBuilderIG : public QModelBuilder
{
typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
-protected:
+
+ protected:
BoolMap d_basisNoMatch;
//map from operators to model preference data
std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
bool d_didInstGen;
/** process build model */
virtual bool processBuildModel( TheoryModel* m );
-protected:
+
+ protected:
//reset
virtual void reset( FirstOrderModel* fm ) = 0;
//initialize quantifiers, return number of lemmas produced
virtual int doInstGen( FirstOrderModel* fm, Node f ) = 0;
//theory-specific build models
virtual void constructModelUf( FirstOrderModel* fm, Node op ) = 0;
-protected:
+
+ protected:
//map from quantifiers to if are SAT
//std::map< Node, bool > d_quant_sat;
//which quantifiers have been initialized
std::map< Node, bool > d_quant_basis_match_added;
//map from quantifiers to model basis match
std::map< Node, InstMatch > d_quant_basis_match;
-protected: //helper functions
+
+ protected: // helper functions
/** term has constant definition */
bool hasConstantDefinition( Node n );
-public:
+
+ public:
QModelBuilderIG( context::Context* c, QuantifiersEngine* qe );
- virtual ~QModelBuilderIG() throw() {}
-public:
+
+ public:
/** statistics class */
class Statistics {
public:
class QModelBuilderDefault : public QModelBuilderIG
{
-private: ///information for (old) InstGen
- //map from quantifiers to their selection literals
+ private: /// information for (old) InstGen
+ // map from quantifiers to their selection literals
std::map< Node, Node > d_quant_selection_lit;
std::map< Node, std::vector< Node > > d_quant_selection_lit_candidates;
//map from quantifiers to their selection literal terms
std::map< Node, std::vector< Node > > d_op_selection_terms;
//get selection score
int getSelectionScore( std::vector< Node >& uf_terms );
-protected:
+
+ protected:
//reset
- void reset( FirstOrderModel* fm );
+ void reset(FirstOrderModel* fm) override;
//analyze quantifier
- void analyzeQuantifier( FirstOrderModel* fm, Node f );
+ void analyzeQuantifier(FirstOrderModel* fm, Node f) override;
//do InstGen techniques for quantifier, return number of lemmas produced
- int doInstGen( FirstOrderModel* fm, Node f );
+ int doInstGen(FirstOrderModel* fm, Node f) override;
//theory-specific build models
void constructModelUf( FirstOrderModel* fm, Node op );
-protected:
+
+ protected:
std::map< Node, QuantPhaseReq > d_phase_reqs;
-public:
+
+ public:
QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
- ~QModelBuilderDefault() throw() {}
+
//options
bool optReconsiderFuncConstants() { return true; }
//has inst gen
bool areMatchDisequal( TNode n1, TNode n2 );
public:
QuantConflictFind( QuantifiersEngine * qe, context::Context* c );
- ~QuantConflictFind() throw() {}
+
/** register quantifier */
void registerQuantifier( Node q );
public:
TNode getUnivRepresentativeInternal( TNode n );
public:
QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c );
- virtual ~QuantEqualityEngine() throw (){}
/* whether this module needs to check this round */
bool needsCheck( Theory::Effort e );
int checkRewriteRule( Node f, Theory::Effort e );
public:
RewriteEngine( context::Context* c, QuantifiersEngine* qe );
- ~RewriteEngine() throw() {}
bool needsCheck( Theory::Effort e );
void check(Theory::Effort e, QEffort quant_e);
friend class TheoryEngineModelBuilder;
public:
TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
- virtual ~TheoryModel() throw();
+ ~TheoryModel() override;
/** reset the model */
virtual void reset();
Statistics d_stats;
-protected:
-
- void contextNotifyPop() {
+ protected:
+ void contextNotifyPop() override
+ {
Debug("ufsymm") << "UFSYMM: clearing state due to pop" << std::endl;
clear();
}
-public:
-
+ public:
SymmetryBreaker(context::Context* context, std::string name = "");
- ~SymmetryBreaker() throw() {}
+
void assertFormula(TNode phi);
void apply(std::vector<Node>& newClauses);
return out << "@" << val.getIndex();
}
-AbstractValue::AbstractValue(Integer index) throw(IllegalArgumentException) :
- d_index(index) {
- PrettyCheckArgument(index >= 1, index, "index >= 1 required for abstract value, not `%s'", index.toString().c_str());
+AbstractValue::AbstractValue(Integer index) : d_index(index)
+{
+ PrettyCheckArgument(index >= 1,
+ index,
+ "index >= 1 required for abstract value, not `%s'",
+ index.toString().c_str());
}
}/* CVC4 namespace */
class CVC4_PUBLIC AbstractValue {
const Integer d_index;
-public:
+ public:
+ AbstractValue(Integer index);
- AbstractValue(Integer index) throw(IllegalArgumentException);
-
- ~AbstractValue() throw() {}
-
- const Integer& getIndex() const throw() {
- return d_index;
- }
-
- bool operator==(const AbstractValue& val) const throw() {
+ const Integer& getIndex() const { return d_index; }
+ bool operator==(const AbstractValue& val) const
+ {
return d_index == val.d_index;
}
- bool operator!=(const AbstractValue& val) const throw() {
- return !(*this == val);
- }
-
- bool operator<(const AbstractValue& val) const throw() {
+ bool operator!=(const AbstractValue& val) const { return !(*this == val); }
+ bool operator<(const AbstractValue& val) const
+ {
return d_index < val.d_index;
}
- bool operator<=(const AbstractValue& val) const throw() {
+ bool operator<=(const AbstractValue& val) const
+ {
return d_index <= val.d_index;
}
- bool operator>(const AbstractValue& val) const throw() {
- return !(*this <= val);
- }
- bool operator>=(const AbstractValue& val) const throw() {
- return !(*this < val);
- }
-
+ bool operator>(const AbstractValue& val) const { return !(*this <= val); }
+ bool operator>=(const AbstractValue& val) const { return !(*this < val); }
};/* class AbstractValue */
std::ostream& operator<<(std::ostream& out, const AbstractValue& val) CVC4_PUBLIC;
bool d_fired;
public:
- Scope(Cache<T, U, Hasher>& cache, const T& elt) throw(AssertionException) :
- d_cache(cache),
- d_fired(d_cache.computing(elt)) {
+ Scope(Cache<T, U, Hasher>& cache, const T& elt)
+ : d_cache(cache), d_fired(d_cache.computing(elt))
+ {
}
~Scope() {
}
}
- operator bool() throw() {
- return d_fired;
- }
-
- const U& get() throw(AssertionException) {
+ operator bool() const { return d_fired; }
+ const U& get() const
+ {
Assert(d_fired, "nothing in cache");
return d_cache.get();
}
- U& operator()(U& computed) throw(AssertionException) {
+ U& operator()(U& computed)
+ {
Assert(!d_fired, "can only cache a computation once");
d_fired = true;
return d_cache(computed);
}
- const U& operator()(const U& computed) throw(AssertionException) {
+ const U& operator()(const U& computed)
+ {
Assert(!d_fired, "can only cache a computation once");
d_fired = true;
return d_cache(computed);
return Integer( cln::exquo(d_value, y.d_value) );
}
-
-void Integer::parseInt(const std::string& s, unsigned base) throw(std::invalid_argument) {
+void Integer::parseInt(const std::string& s, unsigned base)
+{
cln::cl_read_flags flags;
flags.syntax = cln::syntax_integer;
flags.lsyntax = cln::lsyntax_standard;
readInt(flags, s, base);
}
-void Integer::readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument) {
+void Integer::readInt(const cln::cl_read_flags& flags,
+ const std::string& s,
+ unsigned base)
+{
try {
// Removing leading zeroes, CLN has a bug for these inputs up to and
// including CLN v1.3.2.
* Constructs an Integer by copying a CLN C++ primitive.
*/
Integer(const cln::cl_I& val) : d_value(val) {}
+ // Throws a std::invalid_argument on invalid input `s` for the given base.
+ void readInt(const cln::cl_read_flags& flags,
+ const std::string& s,
+ unsigned base);
- void readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument);
-
- void parseInt(const std::string& s, unsigned base) throw(std::invalid_argument);
-
+ // Throws a std::invalid_argument on invalid inputs.
+ void parseInt(const std::string& s, unsigned base);
// These constants are to help with CLN conversion in 32 bit.
// See http://www.ginac.de/CLN/cln.html#Conversions
* For more information about what is a valid rational string,
* see GMP's documentation for mpq_set_str().
*/
- explicit Integer(const char* sp, unsigned base = 10) throw (std::invalid_argument) {
+ explicit Integer(const char* sp, unsigned base = 10)
+ {
parseInt(std::string(sp), base);
}
- explicit Integer(const std::string& s, unsigned base = 10) throw (std::invalid_argument) {
+ explicit Integer(const std::string& s, unsigned base = 10)
+ {
parseInt(s, base);
}
/** Constructs a rational with the value 0/1. */
Rational() : d_value(0){
}
-
/**
* Constructs a Rational from a C string in a given base (defaults to 10).
+ *
* Throws std::invalid_argument if the string is not a valid rational.
* For more information about what is a valid rational string,
* see GMP's documentation for mpq_set_str().
*/
- explicit Rational(const char* s, unsigned base = 10) throw (std::invalid_argument){
+ explicit Rational(const char* s, unsigned base = 10)
+ {
cln::cl_read_flags flags;
flags.syntax = cln::syntax_rational;
throw std::invalid_argument(ss.str());
}
}
- Rational(const std::string& s, unsigned base = 10) throw (std::invalid_argument){
+ Rational(const std::string& s, unsigned base = 10)
+ {
cln::cl_read_flags flags;
flags.syntax = cln::syntax_rational;
return d_thisCallTimeBudget - time_passed;
}
-void ResourceManager::spendResource(unsigned ammount) throw (UnsafeInterruptException) {
+void ResourceManager::spendResource(unsigned amount)
+{
++d_spendResourceCalls;
- d_cumulativeResourceUsed += ammount;
+ d_cumulativeResourceUsed += amount;
if (!d_on) return;
Debug("limit") << "ResourceManager::spendResource()" << std::endl;
- d_thisCallResourceUsed += ammount;
+ d_thisCallResourceUsed += amount;
if(out()) {
Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
Trace("limit") << " on call " << d_spendResourceCalls << std::endl;
uint64_t getResourceBudgetForThisCall() {
return d_thisCallResourceBudget;
}
-
- void spendResource(unsigned ammount) throw(UnsafeInterruptException);
+ // Throws an UnsafeInterruptException if there are no remaining resources.
+ void spendResource(unsigned amount);
void setHardLimit(bool value);
void setResourceLimit(uint64_t units, bool cumulative = false);
/** Construct a statistics registry */
-StatisticsRegistry::StatisticsRegistry(const std::string& name)
- throw(CVC4::IllegalArgumentException) :
- Stat(name) {
-
+StatisticsRegistry::StatisticsRegistry(const std::string& name) : Stat(name)
+{
d_prefix = name;
if(__CVC4_USE_STATISTICS) {
PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name,
}
}
-void StatisticsRegistry::registerStat(Stat* s) throw(CVC4::IllegalArgumentException) {
+void StatisticsRegistry::registerStat(Stat* s)
+{
#ifdef CVC4_STATISTICS_ON
PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s,
"Statistic `%s' was not registered with this registry.",
#endif /* CVC4_STATISTICS_ON */
}/* StatisticsRegistry::registerStat_() */
-void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException) {
+void StatisticsRegistry::unregisterStat(Stat* s)
+{
#ifdef CVC4_STATISTICS_ON
PrettyCheckArgument(d_stats.find(s) != d_stats.end(), s,
"Statistic `%s' was not registered with this registry.",
* will throw an assertion exception if the given name contains the
* statistic delimiter string.
*/
- Stat(const std::string& name) throw(CVC4::IllegalArgumentException) :
- d_name(name) {
+ Stat(const std::string& name) : d_name(name)
+ {
if(__CVC4_USE_STATISTICS) {
CheckArgument(d_name.find(", ") == std::string::npos, name,
"Statistics names cannot include a comma (',')");
StatisticsRegistry() {}
/** Construct a statistics registry */
- StatisticsRegistry(const std::string& name)
- throw(CVC4::IllegalArgumentException);
+ StatisticsRegistry(const std::string& name);
/**
* Set the name of this statistic registry, used as prefix during
}
/** Register a new statistic */
- void registerStat(Stat* s) throw(CVC4::IllegalArgumentException);
+ void registerStat(Stat* s);
/** Unregister a new statistic */
- void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException);
+ void unregisterStat(Stat* s);
};/* class StatisticsRegistry */
class CVC4_PUBLIC TupleUpdate {
unsigned d_index;
-public:
- TupleUpdate(unsigned index) throw() : d_index(index) { }
- unsigned getIndex() const throw() { return d_index; }
- bool operator==(const TupleUpdate& t) const throw() { return d_index == t.d_index; }
- bool operator!=(const TupleUpdate& t) const throw() { return d_index != t.d_index; }
+
+ public:
+ TupleUpdate(unsigned index) : d_index(index) {}
+ unsigned getIndex() const { return d_index; }
+ bool operator==(const TupleUpdate& t) const { return d_index == t.d_index; }
+ bool operator!=(const TupleUpdate& t) const { return d_index != t.d_index; }
};/* class TupleUpdate */
struct CVC4_PUBLIC TupleUpdateHashFunction {
projects / cvc5.git / commitdiff