#endif
colnum = 1;
break;
- case EOF:
+ case char(EOF):
break;
default:
colnum++;
while(isspace(c = our_getc()));
if (c == ';') {
// comment to end of line
- while((c = our_getc()) != '\n' && c != EOF);
+ while((c = our_getc()) != '\n' && c != char(EOF));
return non_ws();
}
return c;
inline const char *prefix_id() {
int i = 0;
char c = idbuf[i++] = non_ws();
- while (!isspace(c) && c != '(' && c != ')' && c != EOF) {
+ while (!isspace(c) && c != '(' && c != ')' && c != char(EOF)) {
if (i == IDBUF_LEN)
report_error("Identifier is too long");
/**
* Destructor does nothing: subclass must explicitly call destroy() instead.
*/
- virtual ~ContextObj() {}
+ virtual ~ContextObj() throw(AssertionException) {}
/**
* If you want to allocate a ContextObj object on the heap, use this
Trace("decision") << "Justification heuristic enabled" << std::endl;
}
-JustificationHeuristic::~JustificationHeuristic() {
+JustificationHeuristic::~JustificationHeuristic() throw() {
StatisticsRegistry::unregisterStat(&d_helfulness);
StatisticsRegistry::unregisterStat(&d_giveup);
StatisticsRegistry::unregisterStat(&d_timestat);
context::UserContext *uc,
context::Context *c);
- ~JustificationHeuristic();
+ ~JustificationHeuristic() throw();
prop::SatLiteral getNext(bool &stopSearch);
std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const;
/** Default constructor, makes a null expression. */
- NodeTemplate() : d_nv(&expr::NodeValue::s_null) { }
+ NodeTemplate() : d_nv(&expr::NodeValue::null()) { }
/**
* Conversion between nodes that are reference-counted and those that are
*/
bool isNull() const {
assertTNodeNotExpired();
- return d_nv == &expr::NodeValue::s_null;
+ return d_nv == &expr::NodeValue::null();
}
/**
}
template <bool ref_count>
-NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::s_null);
+NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::null());
// FIXME: escape from type system convenient but is there a better
// way? Nodes conceptually don't change their expr values but of
if(ref_count) {
d_nv->inc();
} else {
- Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::s_null,
+ Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::null(),
"TNode constructed from NodeValue with rc == 0");
}
}
}
void NodeManager::init() {
- poolInsert( &expr::NodeValue::s_null );
+ poolInsert( &expr::NodeValue::null() );
for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
Kind k = Kind(i);
reclaimZombies();
}
- poolRemove( &expr::NodeValue::s_null );
+ poolRemove( &expr::NodeValue::null() );
if(Debug.isOn("gc:leaks")) {
Debug("gc:leaks") << "still in pool:" << endl;
namespace CVC4 {
namespace expr {
-NodeValue NodeValue::s_null(0);
-
string NodeValue::toString() const {
stringstream ss;
- OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage();
+ OutputLanguage outlang = (this == &null()) ? language::output::LANG_AUTO : options::outputLanguage();
toStream(ss, -1, false, false, outlang);
return ss.str();
}
*/
class NodeValue {
- /** A convenient null-valued expression value */
- static NodeValue s_null;
-
static const unsigned NBITS_REFCOUNT = __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT;
static const unsigned NBITS_KIND = __CVC4__EXPR__NODE_VALUE__NBITS__KIND;
static const unsigned NBITS_ID = __CVC4__EXPR__NODE_VALUE__NBITS__ID;
return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d);
}
- static inline const NodeValue& null() {
- return s_null;
+ static inline NodeValue& null() {
+ static NodeValue* s_null = new NodeValue(0);
+ return *s_null;
}
/**
public:
Pickler(ExprManager* em);
- ~Pickler();
+ virtual ~Pickler();
/**
* Constructs a new Pickle of the node n.
namespace CVC4 {
-TypeNode TypeNode::s_null( &expr::NodeValue::s_null );
+TypeNode TypeNode::s_null( &expr::NodeValue::null() );
TypeNode TypeNode::substitute(const TypeNode& type,
const TypeNode& replacement,
public:
/** Default constructor, makes a null expression. */
- TypeNode() : d_nv(&expr::NodeValue::s_null) { }
+ TypeNode() : d_nv(&expr::NodeValue::null()) { }
/** Copy constructor */
TypeNode(const TypeNode& node);
* @return true if null
*/
bool isNull() const {
- return d_nv == &expr::NodeValue::s_null;
+ return d_nv == &expr::NodeValue::null();
}
/**
protected:
// derived classes can construct, but no one else.
Printer() throw() {}
+ virtual ~Printer() {}
/** write model response to command */
virtual void toStream(std::ostream& out, const Model& m, const Command* c) const throw() = 0;
// Default hash/equals functions
//
+static inline uint32_t hash(uint32_t x){ return x; }
+static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
+static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
+static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
+
template<class K> struct Hash { uint32_t operator()(const K& k) const { return hash(k); } };
template<class K> struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } };
template<class K> struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } };
template<class K> struct DeepEqual { bool operator()(const K* k1, const K* k2) const { return *k1 == *k2; } };
-static inline uint32_t hash(uint32_t x){ return x; }
-static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
-static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
-static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
//=================================================================================================
namespace CVC4 {
class ProofProxyAbstract {
public:
+ virtual ~ProofProxyAbstract() {}
virtual void updateCRef(Minisat::CRef oldref, Minisat::CRef newref) = 0;
};
}
// Default hash/equals functions
//
+static inline uint32_t hash(uint32_t x){ return x; }
+static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
+static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
+static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
+
template<class K> struct Hash { uint32_t operator()(const K& k) const { return hash(k); } };
template<class K> struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } };
template<class K> struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } };
template<class K> struct DeepEqual { bool operator()(const K* k1, const K* k2) const { return *k1 == *k2; } };
-static inline uint32_t hash(uint32_t x){ return x; }
-static inline uint32_t hash(uint64_t x){ return (uint32_t)x; }
-static inline uint32_t hash(int32_t x) { return (uint32_t)x; }
-static inline uint32_t hash(int64_t x) { return (uint32_t)x; }
//=================================================================================================
public:
/** Virtual destructor */
- virtual ~SatSolver() { }
+ virtual ~SatSolver() throw(AssertionException) { }
/** Assert a clause in the solver. */
virtual void addClause(SatClause& clause, bool removable, uint64_t proof_id) = 0;
class BVSatSolverInterface: public SatSolver {
public:
+ virtual ~BVSatSolverInterface() throw(AssertionException) {}
/** Interface for notifications */
class Notify {
public:
d_resourceManager = NodeManager::currentResourceManager();
}
- ~SmtEnginePrivate() {
+ ~SmtEnginePrivate() throw() {
if(d_propagatorNeedsFinish) {
d_propagator.finish();
d_propagatorNeedsFinish = false;
}
class BoundUpdateCallback {
public:
+ virtual ~BoundUpdateCallback() {}
virtual void operator()(ArithVar v, const BoundsInfo& up) = 0;
};
*/
class ArithVarCallBack {
public:
+ virtual ~ArithVarCallBack() {}
virtual void operator()(ArithVar x) = 0;
};
*/
class ArithVarMalloc {
public:
+ virtual ~ArithVarMalloc() {}
virtual ArithVar request() = 0;
virtual void release(ArithVar v) = 0;
};
class TNodeCallBack {
public:
+ virtual ~TNodeCallBack() {}
virtual void operator()(TNode n) = 0;
};
class NodeCallBack {
public:
+ virtual ~NodeCallBack() {}
virtual void operator()(Node n) = 0;
};
class RationalCallBack {
public:
+ virtual ~RationalCallBack() {}
virtual Rational operator()() const = 0;
};
}
void dropNonZeroes(){
- std::remove_if(d_vec.begin(), d_vec.end(), &Border::nonZero);
+ d_vec.erase(std::remove_if(d_vec.begin(), d_vec.end(), &Border::nonZero),
+ d_vec.end());
}
const Border& top() const {
class CoefficientChangeCallback {
public:
+ virtual ~CoefficientChangeCallback() {}
virtual void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) = 0;
virtual void multiplyRow(RowIndex ridx, int Sgn) = 0;
virtual bool canUseRow(RowIndex ridx) const = 0;
public:
SimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
- ~SimplexDecisionProcedure();
+ virtual ~SimplexDecisionProcedure();
/**
* Tries to update the assignments of variables such that all of the
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-
void storeBBAtom(TNode atom, Node atom_bb);
bool hasBBAtom(TNode atom) const;
TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false);
- ~TLazyBitblaster();
+ ~TLazyBitblaster() throw();
/**
* Pushes the assumption literal associated with node to the SAT
* solver assumption queue.
d_abstraction = abs;
}
-TLazyBitblaster::~TLazyBitblaster() {
+TLazyBitblaster::~TLazyBitblaster() throw() {
delete d_cnfStream;
delete d_nullRegistrar;
delete d_nullContext;
} else if( res.getKind() == kind::EQUAL &&
((res[0].getKind() == kind::BITVECTOR_PLUS &&
RewriteRule<ConcatToMult>::applies(res[1])) ||
- res[1].getKind() == kind::BITVECTOR_PLUS &&
- RewriteRule<ConcatToMult>::applies(res[0]))) {
+ (res[1].getKind() == kind::BITVECTOR_PLUS &&
+ RewriteRule<ConcatToMult>::applies(res[0])))) {
Node mult = RewriteRule<ConcatToMult>::applies(res[0])?
RewriteRule<ConcatToMult>::run<false>(res[0]) :
RewriteRule<ConcatToMult>::run<true>(res[1]);
d_staticLearnCache.insert(in);
if (in.getKind() == kind::EQUAL) {
- if(in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL ||
- in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL){
+ if((in[0].getKind() == kind::BITVECTOR_PLUS && in[1].getKind() == kind::BITVECTOR_SHL) ||
+ (in[1].getKind() == kind::BITVECTOR_PLUS && in[0].getKind() == kind::BITVECTOR_SHL)) {
TNode p = in[0].getKind() == kind::BITVECTOR_PLUS ? in[0] : in[1];
TNode s = in[0].getKind() == kind::BITVECTOR_PLUS ? in[1] : in[0];
// Note these cannot be assumed to be symmetric for +0/-0, thus no symmetry reorder
RewriteResponse compactMinMax (TNode node, bool isPreRewrite) {
+#ifdef CVC4_ASSERTIONS
Kind k = node.getKind();
-
Assert((k == kind::FLOATINGPOINT_MIN) || (k == kind::FLOATINGPOINT_MAX));
-
+#endif
if (node[0] == node[1]) {
return RewriteResponse(REWRITE_DONE, node[0]);
} else {
bool doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n );
public:
AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe );
+ ~AbsMbqiBuilder() throw() {}
//process build model
void processBuildModel(TheoryModel* m, bool fullModel);
//do exhaustive instantiation
void addLiteralFromRange( Node lit, Node r );
public:
BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
+ ~BoundedIntegers() throw() {}
bool needsCheck( Theory::Effort e );
void check( Theory::Effort e, unsigned quant_e );
class CandidateGenerator {
public:
CandidateGenerator(){}
- ~CandidateGenerator(){}
+ virtual ~CandidateGenerator(){}
/** Get candidates functions. These set up a context to get all match candidates.
cg->reset( eqc );
int d_candidate_index;
public:
CandidateGeneratorQueue() : d_candidate_index( 0 ){}
- ~CandidateGeneratorQueue(){}
+ ~CandidateGeneratorQueue() throw() {}
void addCandidate( Node n );
Node d_n;
public:
CandidateGeneratorQE( QuantifiersEngine* qe, Node op );
- ~CandidateGeneratorQE(){}
+ ~CandidateGeneratorQE() throw() {}
void resetInstantiationRound();
void reset( Node eqc );
QuantifiersEngine* d_qe;
public:
CandidateGeneratorQELitEq( QuantifiersEngine* qe, Node mpat );
- ~CandidateGeneratorQELitEq(){}
+ ~CandidateGeneratorQELitEq() throw() {}
void resetInstantiationRound();
void reset( Node eqc );
QuantifiersEngine* d_qe;
public:
CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat );
- ~CandidateGeneratorQELitDeq(){}
+ ~CandidateGeneratorQELitDeq() throw() {}
void resetInstantiationRound();
void reset( Node eqc );
bool d_firstTime;
public:
CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat );
- ~CandidateGeneratorQEAll(){}
+ ~CandidateGeneratorQEAll() throw() {}
void resetInstantiationRound();
void reset( Node eqc );
class CegqiOutput
{
public:
+ virtual ~CegqiOutput() {}
virtual bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ ) = 0;
virtual bool isEligibleForInstantiation( Node n ) = 0;
virtual bool addLemma( Node lem ) = 0;
{
public:
CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){}
+ ~CegqiOutputSingleInv() {}
CegConjectureSingleInv * d_out;
bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
bool isEligibleForInstantiation( Node n );
unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth );\r
public:\r
ConjectureGenerator( QuantifiersEngine * qe, context::Context* c );\r
+ ~ConjectureGenerator() throw() {}\r
/* needs check */\r
bool needsCheck( Theory::Effort e );\r
/* reset at a round */\r
}
-FirstOrderModelFmc::~FirstOrderModelFmc() {
+FirstOrderModelFmc::~FirstOrderModelFmc() throw() {
for(std::map<Node, Def*>::iterator i = d_models.begin(); i != d_models.end(); ++i) {
delete (*i).second;
}
virtual void processInitializeQuantifier( Node q ) {}
public:
FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name );
- virtual ~FirstOrderModel() {}
+ virtual ~FirstOrderModel() throw() {}
virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; }
virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; }
virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; }
void processInitializeModelForTerm(Node n);
public:
FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
- virtual ~FirstOrderModelFmc();
+ virtual ~FirstOrderModelFmc() throw();
FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
// initialize the model
void processInitialize( bool ispre );
Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
public:
FullModelChecker( context::Context* c, QuantifiersEngine* qe );
- ~FullModelChecker(){}
+ ~FullModelChecker() throw() {}
bool optBuildAtFullModel();
/** base class for producing InstMatch objects */
class IMGenerator {
public:
+ virtual ~IMGenerator() {}
/** reset instantiation round (call this at beginning of instantiation round) */
virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
/** reset, eqc is the equivalence class to search in (any if eqc=null) */
InstMatchGenerator( Node pat );
InstMatchGenerator();
/** destructor */
- ~InstMatchGenerator(){}
+ ~InstMatchGenerator() throw() {}
/** The pattern we are producing matches for.
If null, this is a multi trigger that is merging matches from d_children.
*/
class VarMatchGeneratorBooleanTerm : public InstMatchGenerator {
public:
VarMatchGeneratorBooleanTerm( Node var, Node comp );
+ ~VarMatchGeneratorBooleanTerm() throw() {}
Node d_comp;
bool d_rm_prev;
/** reset instantiation round (call this at beginning of instantiation round) */
class VarMatchGeneratorTermSubs : public InstMatchGenerator {
public:
VarMatchGeneratorTermSubs( Node var, Node subs );
+ ~VarMatchGeneratorTermSubs() throw() {}
TNode d_var;
Node d_subs;
bool d_rm_prev;
/** constructors */
InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe );
/** destructor */
- ~InstMatchGeneratorMulti(){}
+ ~InstMatchGeneratorMulti() throw() {}
/** reset instantiation round (call this whenever equivalence classes have changed) */
void resetInstantiationRound( QuantifiersEngine* qe );
/** reset, eqc is the equivalence class to search in (any if eqc=null) */
/** constructors */
InstMatchGeneratorSimple( Node f, Node pat );
/** destructor */
- ~InstMatchGeneratorSimple(){}
+ ~InstMatchGeneratorSimple() throw() {}
/** reset instantiation round (call this whenever equivalence classes have changed) */
void resetInstantiationRound( QuantifiersEngine* qe );
/** reset, eqc is the equivalence class to search in (any if eqc=null) */
int process( Node f, Theory::Effort effort, int e );
public:
InstStrategySimplex( arith::TheoryArith* th, QuantifiersEngine* ie );
- ~InstStrategySimplex(){}
+ ~InstStrategySimplex() throw() {}
/** identify */
std::string identify() const { return std::string("Simplex"); }
};
int process( Node f, Theory::Effort effort, int e );
public:
InstStrategyCegqi( QuantifiersEngine * qe );
- ~InstStrategyCegqi(){}
+ ~InstStrategyCegqi() throw() {}
bool addInstantiation( std::vector< Node >& subs, std::vector< int >& subs_typ );
bool isEligibleForInstantiation( Node n );
QuantifiersEngine* d_qe;
public:
QModelBuilder( context::Context* c, QuantifiersEngine* qe );
- virtual ~QModelBuilder(){}
+ virtual ~QModelBuilder() throw() {}
// is quantifier active?
virtual bool isQuantifierActive( Node f );
//do exhaustive instantiation
bool areMatchDisequal( TNode n1, TNode n2 );\r
public:\r
QuantConflictFind( QuantifiersEngine * qe, context::Context* c );\r
+ ~QuantConflictFind() throw() {}\r
/** register quantifier */\r
void registerQuantifier( Node q );\r
public:\r
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, unsigned quant_e );
option stringExp strings-exp --strings-exp bool :default false :read-write
experimental features in the theory of strings
-option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate less_equal(2) :predicate-include "smt/smt_engine.h"
+option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate options::less_equal(2) :predicate-include "smt/smt_engine.h"
the strategy of LB rule application: 0-lazy, 1-eager, 2-no
option stdASCII strings-std-ascii --strings-std-ascii bool :default true :predicate less_equal(2) :predicate-include "smt/smt_engine.h"
bool RegExpOpr::isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2) {
for(std::set< PairNodes >::const_iterator itr = s.begin();
itr != s.end(); ++itr) {
- if(itr->first == n1 && itr->second == n2 ||
- itr->first == n2 && itr->second == n1) {
+ if((itr->first == n1 && itr->second == n2) ||
+ (itr->first == n2 && itr->second == n1)) {
return true;
}
}
Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << endl;
Assert(toTheoryId != fromTheoryId);
- if(! d_logicInfo.isTheoryEnabled(toTheoryId) &&
- toTheoryId != THEORY_SAT_SOLVER) {
+ if(toTheoryId != THEORY_SAT_SOLVER &&
+ ! d_logicInfo.isTheoryEnabled(toTheoryId)) {
stringstream ss;
ss << "The logic was specified as " << d_logicInfo.getLogicString()
<< ", which doesn't include " << toTheoryId
d_eeContext->push();
}
-TheoryModel::~TheoryModel() {
+TheoryModel::~TheoryModel() throw() {
d_eeContext->pop();
delete d_equalityEngine;
delete d_eeContext;
SubstitutionMap d_substitutions;
public:
TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
- virtual ~TheoryModel();
+ virtual ~TheoryModel() throw();
/** special local context for our equalityEngine so we can clear it independently of search context */
context::Context* d_eeContext;
int len1 = a.size();
int len2 = b.size();
- int C[3][len2+1]; // cost
+ int* C[3];
+ int ii;
+ for (ii = 0; ii < 3; ++ii) {
+ C[ii] = new int[len2+1];
+ }
+ // int C[3][len2+1]; // cost
for(int j = 0; j <= len2; ++j) {
C[0][j] = j * addCost;
}
}
- return C[len1%3][len2];
+ int result = C[len1%3][len2];
+ for (ii = 0; ii < 3; ++ii) {
+ delete [] C[ii];
+ }
+ return result;
}
string DidYouMean::getMatchAsString(string input, int prefixNewLines, int suffixNewLines) {
projects / cvc5.git / commitdiff