Adds missing override keywords.
CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES])
CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
+CVC4_CXX_OPTION([-Wsuggest-override], [W_SUGGEST_OVERRIDE])
CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
AC_SUBST([WERROR])
AC_SUBST([WNO_CONVERSION_NULL])
AC_SUBST([WNO_PARENTHESES])
AC_SUBST([WNO_UNINITIALIZED])
AC_SUBST([WNO_UNUSED_VARIABLE])
+AC_SUBST([W_SUGGEST_OVERRIDE])
AC_SUBST([FNO_STRICT_ALIASING])
+CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }${W_SUGGEST_OVERRIDE}"
+
# On Mac, we have to fix the visibility of standard library symbols.
# Otherwise, exported template instantiations---even though explicitly
# CVC4_PUBLIC, can be generated as symbols with internal-only linkage.
* stream. Perhaps this is not so critical, but recommended; this
* way the output stream looks like it's functioning, in a non-error
* state. */
- int overflow(int c) { return c; }
+ int overflow(int c) override { return c; }
};/* class null_streambuf */
/** A null stream-buffer singleton */
CDOhash_map* d_prev;
CDOhash_map* d_next;
- virtual ContextObj* save(ContextMemoryManager* pCMM) {
+ ContextObj* save(ContextMemoryManager* pCMM) override
+ {
return new(pCMM) CDOhash_map(*this);
}
- virtual void restore(ContextObj* data) {
+ void restore(ContextObj* data) override
+ {
CDOhash_map* p = static_cast<CDOhash_map*>(data);
if(d_map != NULL) {
if(p->d_map == NULL) {
Context* d_context;
// Nothing to save; the elements take care of themselves
- virtual ContextObj* save(ContextMemoryManager* pCMM) {
- Unreachable();
- }
+ ContextObj* save(ContextMemoryManager* pCMM) override { Unreachable(); }
// Similarly, nothing to restore
- virtual void restore(ContextObj* data) {
- Unreachable();
- }
+ void restore(ContextObj* data) override { Unreachable(); }
// no copy or assignment
CDHashMap(const CDHashMap&) CVC4_UNDEFINED;
* restored on a pop). The saved information is allocated using the
* ContextMemoryManager.
*/
- ContextObj* save(ContextMemoryManager* pCMM) {
+ ContextObj* save(ContextMemoryManager* pCMM) override
+ {
ContextObj* data = new(pCMM) CDInsertHashMap<Key, Data, HashFcn>(*this);
Debug("CDInsertHashMap") << "save " << this
<< " at level " << this->getContext()->getLevel()
* of new pushFront calls have happened since saving.
* The d_insertMap is untouched and d_pushFronts is also kept.
*/
- void restore(ContextObj* data) {
- Debug("CDInsertHashMap") << "restore " << this
- << " level " << this->getContext()->getLevel()
- << " data == " << data
- << " d_insertMap == " << this->d_insertMap << std::endl;
- size_t oldSize = ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_size;
- size_t oldPushFronts = ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_pushFronts;
- Assert(oldPushFronts <= d_pushFronts);
-
- // The size to restore to.
- size_t restoreSize = oldSize + (d_pushFronts - oldPushFronts);
- d_insertMap->pop_to_size(restoreSize);
- d_size = restoreSize;
- Assert(d_insertMap->size() == d_size);
- Debug("CDInsertHashMap") << "restore " << this
- << " level " << this->getContext()->getLevel()
- << " size back to " << this->d_size << std::endl;
+ void restore(ContextObj* data) override
+ {
+ Debug("CDInsertHashMap")
+ << "restore " << this << " level " << this->getContext()->getLevel()
+ << " data == " << data << " d_insertMap == " << this->d_insertMap
+ << std::endl;
+ size_t oldSize = ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_size;
+ size_t oldPushFronts =
+ ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_pushFronts;
+ Assert(oldPushFronts <= d_pushFronts);
+
+ // The size to restore to.
+ size_t restoreSize = oldSize + (d_pushFronts - oldPushFronts);
+ d_insertMap->pop_to_size(restoreSize);
+ d_size = restoreSize;
+ Assert(d_insertMap->size() == d_size);
+ Debug("CDInsertHashMap")
+ << "restore " << this << " level " << this->getContext()->getLevel()
+ << " size back to " << this->d_size << std::endl;
}
public:
* restored on a pop). The saved information is allocated using the
* ContextMemoryManager.
*/
- ContextObj* save(ContextMemoryManager* pCMM) {
+ ContextObj* save(ContextMemoryManager* pCMM) override
+ {
ContextObj* data = new(pCMM) CDList<T, CleanUp, Allocator>(*this);
Debug("cdlist") << "save " << this
<< " at level " << this->getContext()->getLevel()
* restores the previous size. Note that the list pointer and the
* allocated size are not changed.
*/
- void restore(ContextObj* data) {
- Debug("cdlist") << "restore " << this
- << " level " << this->getContext()->getLevel()
- << " data == " << data
- << " call dtor == " << this->d_callDestructor
- << " d_list == " << this->d_list << std::endl;
- truncateList(((CDList<T, CleanUp, Allocator>*)data)->d_size);
- Debug("cdlist") << "restore " << this
- << " level " << this->getContext()->getLevel()
- << " size back to " << this->d_size
- << " sizeAlloc at " << this->d_sizeAlloc << std::endl;
+ void restore(ContextObj* data) override
+ {
+ Debug("cdlist") << "restore " << this << " level "
+ << this->getContext()->getLevel() << " data == " << data
+ << " call dtor == " << this->d_callDestructor
+ << " d_list == " << this->d_list << std::endl;
+ truncateList(((CDList<T, CleanUp, Allocator>*)data)->d_size);
+ Debug("cdlist") << "restore " << this << " level "
+ << this->getContext()->getLevel() << " size back to "
+ << this->d_size << " sizeAlloc at " << this->d_sizeAlloc
+ << std::endl;
}
/**
* current data to a copy using the copy constructor. Memory is allocated
* using the ContextMemoryManager.
*/
- virtual ContextObj* save(ContextMemoryManager* pCMM) {
+ ContextObj* save(ContextMemoryManager* pCMM) override
+ {
Debug("context") << "save cdo " << this;
ContextObj* p = new(pCMM) CDO<T>(*this);
Debug("context") << " to " << p << std::endl;
* Implementation of mandatory ContextObj method restore: simply copies the
* saved data back from the saved copy using operator= for T.
*/
- virtual void restore(ContextObj* pContextObj) {
+ void restore(ContextObj* pContextObj) override
+ {
//Debug("context") << "restore cdo " << this;
CDO<T>* p = static_cast<CDO<T>*>(pContextObj);
d_data = p->d_data;
/** Implementation of mandatory ContextObj method save:
* We assume that the base class do the job inside their copy constructor.
*/
- ContextObj* save(ContextMemoryManager* pCMM) {
+ ContextObj* save(ContextMemoryManager* pCMM) override
+ {
ContextObj* data = new(pCMM) CDQueue<T, CleanUp, Allocator>(*this);
// We save the d_size in d_lastsave and we should never destruct below this
// indices before the corresponding restore.
* restores the previous size, iter and lastsave indices. Note that
* the list pointer and the allocated size are not changed.
*/
- void restore(ContextObj* data) {
+ void restore(ContextObj* data) override
+ {
CDQueue<T, CleanUp, Allocator>* qdata = static_cast<CDQueue<T, CleanUp, Allocator>*>(data);
d_iter = qdata->d_iter;
d_lastsave = qdata->d_lastsave;
* the current sizes to a copy using the copy constructor,
* The saved information is allocated using the ContextMemoryManager.
*/
- ContextObj* save(ContextMemoryManager* pCMM) {
+ ContextObj* save(ContextMemoryManager* pCMM) override
+ {
ContextObj* data = new(pCMM) CDTrailHashMap<Key, Data, HashFcn>(*this);
Debug("CDTrailHashMap") << "save " << this
<< " at level " << this->getContext()->getLevel()
* restores the previous size. Note that the list pointer and the
* allocated size are not changed.
*/
- void restore(ContextObj* data) {
- Debug("CDTrailHashMap") << "restore " << this
- << " level " << this->getContext()->getLevel()
- << " data == " << data
- << " d_trailMap == " << this->d_trailMap << std::endl;
- size_t oldSize = ((CDTrailHashMap<Key, Data, HashFcn>*)data)->d_trailSize;
- d_trailMap->pop_to_size(oldSize);
- d_trailSize = oldSize;
- Assert(d_trailMap->trailSize() == d_trailSize);
-
- d_prevTrailSize = ((CDTrailHashMap<Key, Data, HashFcn>*)data)->d_prevTrailSize;
- Debug("CDTrailHashMap") << "restore " << this
- << " level " << this->getContext()->getLevel()
- << " size back to " << this->d_trailSize << std::endl;
+ void restore(ContextObj* data) override
+ {
+ Debug("CDTrailHashMap") << "restore " << this << " level "
+ << this->getContext()->getLevel()
+ << " data == " << data
+ << " d_trailMap == " << this->d_trailMap
+ << std::endl;
+ size_t oldSize = ((CDTrailHashMap<Key, Data, HashFcn>*)data)->d_trailSize;
+ d_trailMap->pop_to_size(oldSize);
+ d_trailSize = oldSize;
+ Assert(d_trailMap->trailSize() == d_trailSize);
+
+ d_prevTrailSize =
+ ((CDTrailHashMap<Key, Data, HashFcn>*)data)->d_prevTrailSize;
+ Debug("CDTrailHashMap") << "restore " << this << " level "
+ << this->getContext()->getLevel() << " size back to "
+ << this->d_trailSize << std::endl;
}
/**
DecisionStrategy(de, c) {
}
-
- bool needIteSkolemMap() { return true; }
+ bool needIteSkolemMap() override { return true; }
virtual void addAssertions(const std::vector<Node> &assertions,
unsigned assertionsEnd,
~JustificationHeuristic();
- prop::SatLiteral getNext(bool &stopSearch);
+ prop::SatLiteral getNext(bool &stopSearch) override;
void addAssertions(const std::vector<Node> &assertions,
unsigned assertionsEnd,
- IteSkolemMap iteSkolemMap);
+ IteSkolemMap iteSkolemMap) override;
-private:
+ private:
/* getNext with an option to specify threshold */
prop::SatLiteral getNextThresh(bool &stopSearch, DecisionWeight threshold);
class TlimitListener : public Listener {
public:
TlimitListener(ResourceManager* rm) : d_rm(rm) {}
- virtual void notify();
+ void notify() override;
+
private:
ResourceManager* d_rm;
};
class TlimitPerListener : public Listener {
public:
TlimitPerListener(ResourceManager* rm) : d_rm(rm) {}
- virtual void notify();
+ void notify() override;
+
private:
ResourceManager* d_rm;
};
class RlimitListener : public Listener {
public:
RlimitListener(ResourceManager* rm) : d_rm(rm) {}
- virtual void notify();
+ void notify() override;
+
private:
ResourceManager* d_rm;
};
class RlimitPerListener : public Listener {
public:
RlimitPerListener(ResourceManager* rm) : d_rm(rm) {}
- virtual void notify();
+ void notify() override;
+
private:
ResourceManager* d_rm;
};
-I@builddir@/.. -I@srcdir@/../include -I@srcdir@/..
AM_CFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+# This is a workaround for now to fix some warnings related to unsupported
+# compiler flags since we are compiling C code here. CXXFLAGS is set via
+# configure, however, we should actually set AM_CXXFLAGS.
+CXXFLAGS = $(AM_CXXFLAGS)
noinst_LTLIBRARIES = libreplacements.la
* Preconditions:
* - argc and argv are non-null.
*/
- void getArguments(int* argc, char*** argv) const;
+ void getArguments(int* argc, char*** argv) const override;
/** Returns the number of arguments that are . */
- size_t numArguments() const;
+ size_t numArguments() const override;
/**
* Inserts a copy of element into the front of the arguments list.
* Preconditions: element is non-null and 0 terminated.
*/
- void pushFrontArgument(const char* element);
+ void pushFrontArgument(const char* element) override;
/**
* Inserts a copy of element into the back of the arguments list.
* Preconditions: element is non-null and 0 terminated.
*/
- void pushBackArgument(const char* element);
+ void pushBackArgument(const char* element) override;
/** Removes the front of the arguments list.*/
- void popFrontArgument();
+ void popFrontArgument() override;
/** Adds a new preemption to the arguments list. */
- void pushBackPreemption(const char* element);
+ void pushBackPreemption(const char* element) override;
/**
* Moves all of the preemptions into the front of the arguments
* list.
*/
- void movePreemptionsToArguments();
+ void movePreemptionsToArguments() override;
/** Returns true iff there is a pending preemption.*/
- bool hasPreemptions() const;
+ bool hasPreemptions() const override;
-private:
+ private:
typedef std::list< char* > CharPointerList;
public:
ExprStream(Parser* parser) : d_parser(parser) {}
~ExprStream() { delete d_parser; }
- Expr nextExpr() { return d_parser->nextExpression(); }
+ Expr nextExpr() override { return d_parser->nextExpression(); }
};/* class Parser::ExprStream */
//------------------------ operator overloading
*/
void addTheory(Theory theory);
- bool logicIsSet();
+ bool logicIsSet() override;
/**
* Sets the logic for the current benchmark. Declares any logic and theory symbols.
bool isTheoryEnabled(Theory theory) const;
- bool logicIsSet();
-
+ bool logicIsSet() override;
+
/**
* Returns the expression that name should be interpreted as.
*/
- virtual Expr getExpressionForNameAndType(const std::string& name, Type t);
+ Expr getExpressionForNameAndType(const std::string& name, Type t) override;
/** Make function defined by a define-fun(s)-rec command.
*
std::vector<Expr>& bvs,
bool bindingLevel = false);
- void reset();
+ void reset() override;
void resetAssertions();
public:
ArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine);
- virtual void registerTerm(Expr term);
+ void registerTerm(Expr term) override;
};
class LFSCArithProof : public ArithProof {
LFSCArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine)
: ArithProof(arith, proofEngine)
{}
- virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
- virtual void printOwnedSort(Type type, std::ostream& os);
- virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
- virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
+ void printOwnedTerm(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map) override;
+ void printOwnedSort(Type type, std::ostream& os) override;
+ void printTheoryLemmaProof(std::vector<Expr>& lemma,
+ std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& map) override;
+ void printSortDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printTermDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printDeferredDeclarations(std::ostream& os,
+ std::ostream& paren) override;
+ void printAliasingDeclarations(std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& globalLetMap) override;
};
std::string skolemToLiteral(Expr skolem);
- virtual void registerTerm(Expr term);
+ void registerTerm(Expr term) override;
};
class LFSCArrayProof : public ArrayProof {
: ArrayProof(arrays, proofEngine)
{}
- virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
- virtual void printOwnedSort(Type type, std::ostream& os);
- virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
- virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
-
- bool printsAsBool(const Node &n);
+ void printOwnedTerm(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map) override;
+ void printOwnedSort(Type type, std::ostream& os) override;
+ void printTheoryLemmaProof(std::vector<Expr>& lemma,
+ std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& map) override;
+ void printSortDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printTermDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printDeferredDeclarations(std::ostream& os,
+ std::ostream& paren) override;
+ void printAliasingDeclarations(std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& globalLetMap) override;
+
+ bool printsAsBool(const Node& n) override;
};
void registerTermBB(Expr term);
void registerAtomBB(Expr atom, Expr atom_bb);
- virtual void registerTerm(Expr term);
+ void registerTerm(Expr term) override;
virtual void printTermBitblasting(Expr term, std::ostream& os) = 0;
virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap) = 0;
LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
:BitVectorProof(bv, proofEngine)
{}
- virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
- virtual void printOwnedSort(Type type, std::ostream& os);
- virtual void printTermBitblasting(Expr term, std::ostream& os);
- virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap);
- virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os);
- virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
- virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
- virtual void printBitblasting(std::ostream& os, std::ostream& paren);
- virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap);
- void calculateAtomsInBitblastingProof();
- const std::set<Node>* getAtomsInBitblastingProof();
- void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
- void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2);
+ void printOwnedTerm(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map) override;
+ void printOwnedSort(Type type, std::ostream& os) override;
+ void printTermBitblasting(Expr term, std::ostream& os) override;
+ void printAtomBitblasting(Expr term, std::ostream& os, bool swap) override;
+ void printAtomBitblastingToFalse(Expr term, std::ostream& os) override;
+ void printTheoryLemmaProof(std::vector<Expr>& lemma,
+ std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& map) override;
+ void printSortDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printTermDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printDeferredDeclarations(std::ostream& os,
+ std::ostream& paren) override;
+ void printAliasingDeclarations(std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& globalLetMap) override;
+ void printBitblasting(std::ostream& os, std::ostream& paren) override;
+ void printResolutionProof(std::ostream& os,
+ std::ostream& paren,
+ ProofLetMap& letMap) override;
+ void calculateAtomsInBitblastingProof() override;
+ const std::set<Node>* getAtomsInBitblastingProof() override;
+ void printConstantDisequalityProof(std::ostream& os,
+ Expr c1,
+ Expr c2,
+ const ProofLetMap& globalLetMap) override;
+ void printRewriteProof(std::ostream& os,
+ const Node& n1,
+ const Node& n2) override;
};
}/* CVC4 namespace */
void printAtomMapping(const std::set<Node>& atoms,
std::ostream& os,
- std::ostream& paren);
+ std::ostream& paren) override;
void printAtomMapping(const std::set<Node>& atoms,
std::ostream& os,
std::ostream& paren,
- ProofLetMap &letMap);
+ ProofLetMap& letMap) override;
void printClause(const prop::SatClause& clause,
std::ostream& os,
- std::ostream& paren);
+ std::ostream& paren) override;
void printCnfProofForClause(ClauseId id,
const prop::SatClause* clause,
std::ostream& os,
- std::ostream& paren);
+ std::ostream& paren) override;
};/* class LFSCCnfProof */
} /* CVC4 namespace */
LFSCSatProof(SatSolver* solver, context::Context* context,
const std::string& name, bool checkRes = false)
: TSatProof<SatSolver>(solver, context, name, checkRes) {}
- virtual void printResolution(ClauseId id, std::ostream& out,
- std::ostream& paren);
- virtual void printResolutions(std::ostream& out, std::ostream& paren);
- virtual void printResolutionEmptyClause(std::ostream& out,
- std::ostream& paren);
- virtual void printAssumptionsResolution(ClauseId id, std::ostream& out,
- std::ostream& paren);
+ void printResolution(ClauseId id,
+ std::ostream& out,
+ std::ostream& paren) override;
+ void printResolutions(std::ostream& out, std::ostream& paren) override;
+ void printResolutionEmptyClause(std::ostream& out,
+ std::ostream& paren) override;
+ void printAssumptionsResolution(ClauseId id,
+ std::ostream& out,
+ std::ostream& paren) override;
}; /* class LFSCSatProof */
template <class Solver>
LFSCTheoryProofEngine()
: TheoryProofEngine() {}
- void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map);
+ void printTheoryTerm(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map) override;
- void registerTermsFromAssertions();
+ void registerTermsFromAssertions() override;
void printSortDeclarations(std::ostream& os, std::ostream& paren);
void printTermDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map);
- virtual void printLetTerm(Expr term, std::ostream& os);
- virtual void printBoundTerm(Expr term, std::ostream& os, const ProofLetMap& map);
- virtual void printAssertions(std::ostream& os, std::ostream& paren);
- virtual void printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren);
- virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
- virtual void printTheoryLemmas(const IdToSatClause& lemmas,
- std::ostream& os,
+ void printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map);
+ void printLetTerm(Expr term, std::ostream& os) override;
+ void printBoundTerm(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map) override;
+ void printAssertions(std::ostream& os, std::ostream& paren) override;
+ void printLemmaRewrites(NodePairSet& rewrites,
+ std::ostream& os,
+ std::ostream& paren);
+ void printDeferredDeclarations(std::ostream& os,
+ std::ostream& paren) override;
+ void printAliasingDeclarations(std::ostream& os,
std::ostream& paren,
- ProofLetMap& map);
- virtual void printSort(Type type, std::ostream& os);
+ const ProofLetMap& globalLetMap) override;
+ void printTheoryLemmas(const IdToSatClause& lemmas,
+ std::ostream& os,
+ std::ostream& paren,
+ ProofLetMap& map) override;
+ void printSort(Type type, std::ostream& os) override;
void performExtraRegistrations();
public:
BooleanProof(TheoryProofEngine* proofEngine);
- virtual void registerTerm(Expr term);
-
- virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
-
- virtual void printOwnedSort(Type type, std::ostream& os) = 0;
- virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) = 0;
- virtual void printSortDeclarations(std::ostream& os, std::ostream& paren) = 0;
- virtual void printTermDeclarations(std::ostream& os, std::ostream& paren) = 0;
- virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
- virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) = 0;
+ void registerTerm(Expr term) override;
};
class LFSCBooleanProof : public BooleanProof {
LFSCBooleanProof(TheoryProofEngine* proofEngine)
: BooleanProof(proofEngine)
{}
- virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
- virtual void printOwnedSort(Type type, std::ostream& os);
- virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
- virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
+ void printOwnedTerm(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map) override;
+ void printOwnedSort(Type type, std::ostream& os) override;
+ void printTheoryLemmaProof(std::vector<Expr>& lemma,
+ std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& map) override;
+ void printSortDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printTermDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printDeferredDeclarations(std::ostream& os,
+ std::ostream& paren) override;
+ void printAliasingDeclarations(std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& globalLetMap) override;
- bool printsAsBool(const Node &n);
- void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
+ bool printsAsBool(const Node& n) override;
+ void printConstantDisequalityProof(std::ostream& os,
+ Expr c1,
+ Expr c2,
+ const ProofLetMap& globalLetMap) override;
};
} /* CVC4 namespace */
public:
UFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine);
- virtual void registerTerm(Expr term);
+ void registerTerm(Expr term) override;
};
class LFSCUFProof : public UFProof {
LFSCUFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine)
: UFProof(uf, proofEngine)
{}
- virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
- virtual void printOwnedSort(Type type, std::ostream& os);
- virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
- virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
- virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
-
- bool printsAsBool(const Node &n);
-
- void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
+ void printOwnedTerm(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map) override;
+ void printOwnedSort(Type type, std::ostream& os) override;
+ void printTheoryLemmaProof(std::vector<Expr>& lemma,
+ std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& map) override;
+ void printSortDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printTermDeclarations(std::ostream& os, std::ostream& paren) override;
+ void printDeferredDeclarations(std::ostream& os,
+ std::ostream& paren) override;
+ void printAliasingDeclarations(std::ostream& os,
+ std::ostream& paren,
+ const ProofLetMap& globalLetMap) override;
+
+ bool printsAsBool(const Node& n) override;
+
+ void printConstantDisequalityProof(std::ostream& os,
+ Expr c1,
+ Expr c2,
+ const ProofLetMap& globalLetMap) override;
};
public:
MinisatNotify(BVSatSolverInterface::Notify* notify) : d_notify(notify) {}
- bool notify(BVMinisat::Lit lit)
+ bool notify(BVMinisat::Lit lit) override
{
return d_notify->notify(toSatLiteral(lit));
}
- void notify(BVMinisat::vec<BVMinisat::Lit>& clause);
- void spendResource(unsigned amount) { d_notify->spendResource(amount); }
- void safePoint(unsigned amount) { d_notify->safePoint(amount); }
+ void notify(BVMinisat::vec<BVMinisat::Lit>& clause) override;
+ void spendResource(unsigned amount) override
+ {
+ d_notify->spendResource(amount);
+ }
+ void safePoint(unsigned amount) override { d_notify->safePoint(amount); }
};
BVMinisat::SimpSolver* d_minisat;
context::CDO<unsigned> d_lastPropagation;
protected:
-
- void contextNotifyPop();
+ void contextNotifyPop() override;
public:
BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name = "");
virtual ~BVMinisatSatSolver();
- void setNotify(Notify* notify);
+ void setNotify(Notify* notify) override;
- ClauseId addClause(SatClause& clause, bool removable);
+ ClauseId addClause(SatClause& clause, bool removable) override;
- ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) {
+ ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
+ {
Unreachable("Minisat does not support native XOR reasoning");
}
-
- SatValue propagate();
- SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true);
+ SatValue propagate() override;
- SatVariable trueVar() { return d_minisat->trueVar(); }
- SatVariable falseVar() { return d_minisat->falseVar(); }
+ SatVariable newVar(bool isTheoryAtom = false,
+ bool preRegister = false,
+ bool canErase = true) override;
- void markUnremovable(SatLiteral lit);
+ SatVariable trueVar() override { return d_minisat->trueVar(); }
+ SatVariable falseVar() override { return d_minisat->falseVar(); }
- void interrupt();
+ void markUnremovable(SatLiteral lit) override;
- SatValue solve();
- SatValue solve(long unsigned int&);
- bool ok() const;
- void getUnsatCore(SatClause& unsatCore);
+ void interrupt() override;
- SatValue value(SatLiteral l);
- SatValue modelValue(SatLiteral l);
+ SatValue solve() override;
+ SatValue solve(long unsigned int&) override;
+ bool ok() const override;
+ void getUnsatCore(SatClause& unsatCore) override;
+
+ SatValue value(SatLiteral l) override;
+ SatValue modelValue(SatLiteral l) override;
void unregisterVar(SatLiteral lit);
void renewVar(SatLiteral lit, int level = -1);
- unsigned getAssertionLevel() const;
-
+ unsigned getAssertionLevel() const override;
// helper methods for converting from the internal Minisat representation
static void toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause);
static void toSatClause (const BVMinisat::Clause& clause, SatClause& sat_clause);
- void addMarkerLiteral(SatLiteral lit);
+ void addMarkerLiteral(SatLiteral lit) override;
- void explain(SatLiteral lit, std::vector<SatLiteral>& explanation);
+ void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) override;
- SatValue assertAssumption(SatLiteral lit, bool propagate);
+ SatValue assertAssumption(SatLiteral lit, bool propagate) override;
- void popAssumption();
-
- void setProofLog( BitVectorProof * bvp );
+ void popAssumption() override;
-private:
+ void setProofLog(BitVectorProof* bvp) override;
+
+ private:
/* Disable the default constructor. */
BVMinisatSatSolver() CVC4_UNDEFINED;
// Memory managment:
//
- virtual void garbageCollect();
-
+ void garbageCollect() override;
// Generate a (possibly simplified) DIMACS file:
//
operator double& (void) { return value; }
DoubleOption& operator=(double x) { value = x; return *this; }
- virtual bool parse(const char* str){
- const char* span = str;
+ bool parse(const char* str) override
+ {
+ const char* span = str;
- if (!match(span, "-") || !match(span, name) || !match(span, "="))
- return false;
-
- char* end;
- double tmp = strtod(span, &end);
-
- if (end == NULL)
- return false;
- else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end)){
- fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
- exit(1);
- }else if (tmp <= range.begin && (!range.begin_inclusive || tmp != range.begin)){
- fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
- exit(1); }
+ if (!match(span, "-") || !match(span, name) || !match(span, "="))
+ return false;
- value = tmp;
- // fprintf(stderr, "READ VALUE: %g\n", value);
+ char* end;
+ double tmp = strtod(span, &end);
- return true;
+ if (end == NULL)
+ return false;
+ else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end))
+ {
+ fprintf(stderr,
+ "ERROR! value <%s> is too large for option \"%s\".\n",
+ span,
+ name);
+ exit(1);
+ }
+ else if (tmp <= range.begin
+ && (!range.begin_inclusive || tmp != range.begin))
+ {
+ fprintf(stderr,
+ "ERROR! value <%s> is too small for option \"%s\".\n",
+ span,
+ name);
+ exit(1);
+ }
+
+ value = tmp;
+ // fprintf(stderr, "READ VALUE: %g\n", value);
+
+ return true;
}
- virtual void help (bool verbose = false){
- fprintf(stderr, " -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n",
- name, type_name,
- range.begin_inclusive ? '[' : '(',
- range.begin,
- range.end,
- range.end_inclusive ? ']' : ')',
- value);
- if (verbose){
- fprintf(stderr, "\n %s\n", description);
- fprintf(stderr, "\n");
- }
+ void help(bool verbose = false) override
+ {
+ fprintf(stderr,
+ " -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n",
+ name,
+ type_name,
+ range.begin_inclusive ? '[' : '(',
+ range.begin,
+ range.end,
+ range.end_inclusive ? ']' : ')',
+ value);
+ if (verbose)
+ {
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
}
};
operator int32_t& (void) { return value; }
IntOption& operator= (int32_t x) { value = x; return *this; }
- virtual bool parse(const char* str){
- const char* span = str;
-
- if (!match(span, "-") || !match(span, name) || !match(span, "="))
- return false;
+ bool parse(const char* str) override
+ {
+ const char* span = str;
- char* end;
- int32_t tmp = strtol(span, &end, 10);
-
- if (end == NULL)
- return false;
- else if (tmp > range.end){
- fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
- exit(1);
- }else if (tmp < range.begin){
- fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
- exit(1); }
+ if (!match(span, "-") || !match(span, name) || !match(span, "="))
+ return false;
- value = tmp;
+ char* end;
+ int32_t tmp = strtol(span, &end, 10);
- return true;
+ if (end == NULL)
+ return false;
+ else if (tmp > range.end)
+ {
+ fprintf(stderr,
+ "ERROR! value <%s> is too large for option \"%s\".\n",
+ span,
+ name);
+ exit(1);
+ }
+ else if (tmp < range.begin)
+ {
+ fprintf(stderr,
+ "ERROR! value <%s> is too small for option \"%s\".\n",
+ span,
+ name);
+ exit(1);
+ }
+
+ value = tmp;
+
+ return true;
}
- virtual void help (bool verbose = false){
- fprintf(stderr, " -%-12s = %-8s [", name, type_name);
- if (range.begin == INT32_MIN)
- fprintf(stderr, "imin");
- else
- fprintf(stderr, "%4d", range.begin);
-
- fprintf(stderr, " .. ");
- if (range.end == INT32_MAX)
- fprintf(stderr, "imax");
- else
- fprintf(stderr, "%4d", range.end);
-
- fprintf(stderr, "] (default: %d)\n", value);
- if (verbose){
- fprintf(stderr, "\n %s\n", description);
- fprintf(stderr, "\n");
- }
+ void help(bool verbose = false) override
+ {
+ fprintf(stderr, " -%-12s = %-8s [", name, type_name);
+ if (range.begin == INT32_MIN)
+ fprintf(stderr, "imin");
+ else
+ fprintf(stderr, "%4d", range.begin);
+
+ fprintf(stderr, " .. ");
+ if (range.end == INT32_MAX)
+ fprintf(stderr, "imax");
+ else
+ fprintf(stderr, "%4d", range.end);
+
+ fprintf(stderr, "] (default: %d)\n", value);
+ if (verbose)
+ {
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
}
};
operator int64_t& (void) { return value; }
Int64Option& operator= (int64_t x) { value = x; return *this; }
- virtual bool parse(const char* str){
- const char* span = str;
-
- if (!match(span, "-") || !match(span, name) || !match(span, "="))
- return false;
+ bool parse(const char* str) override
+ {
+ const char* span = str;
- char* end;
- int64_t tmp = strtoll(span, &end, 10);
-
- if (end == NULL)
- return false;
- else if (tmp > range.end){
- fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
- exit(1);
- }else if (tmp < range.begin){
- fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
- exit(1); }
+ if (!match(span, "-") || !match(span, name) || !match(span, "="))
+ return false;
- value = tmp;
+ char* end;
+ int64_t tmp = strtoll(span, &end, 10);
- return true;
+ if (end == NULL)
+ return false;
+ else if (tmp > range.end)
+ {
+ fprintf(stderr,
+ "ERROR! value <%s> is too large for option \"%s\".\n",
+ span,
+ name);
+ exit(1);
+ }
+ else if (tmp < range.begin)
+ {
+ fprintf(stderr,
+ "ERROR! value <%s> is too small for option \"%s\".\n",
+ span,
+ name);
+ exit(1);
+ }
+
+ value = tmp;
+
+ return true;
}
- virtual void help (bool verbose = false){
- fprintf(stderr, " -%-12s = %-8s [", name, type_name);
- if (range.begin == INT64_MIN)
- fprintf(stderr, "imin");
- else
- fprintf(stderr, "%4" PRIi64, range.begin);
-
- fprintf(stderr, " .. ");
- if (range.end == INT64_MAX)
- fprintf(stderr, "imax");
- else
- fprintf(stderr, "%4" PRIi64, range.end);
-
- fprintf(stderr, "] (default: %" PRIi64")\n", value);
- if (verbose){
- fprintf(stderr, "\n %s\n", description);
- fprintf(stderr, "\n");
- }
+ void help(bool verbose = false) override
+ {
+ fprintf(stderr, " -%-12s = %-8s [", name, type_name);
+ if (range.begin == INT64_MIN)
+ fprintf(stderr, "imin");
+ else
+ fprintf(stderr, "%4" PRIi64, range.begin);
+
+ fprintf(stderr, " .. ");
+ if (range.end == INT64_MAX)
+ fprintf(stderr, "imax");
+ else
+ fprintf(stderr, "%4" PRIi64, range.end);
+
+ fprintf(stderr, "] (default: %" PRIi64 ")\n", value);
+ if (verbose)
+ {
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
}
};
#endif
operator const char*& (void) { return value; }
StringOption& operator= (const char* x) { value = x; return *this; }
- virtual bool parse(const char* str){
- const char* span = str;
+ bool parse(const char* str) override
+ {
+ const char* span = str;
- if (!match(span, "-") || !match(span, name) || !match(span, "="))
- return false;
+ if (!match(span, "-") || !match(span, name) || !match(span, "="))
+ return false;
- value = span;
- return true;
+ value = span;
+ return true;
}
- virtual void help (bool verbose = false){
- fprintf(stderr, " -%-10s = %8s\n", name, type_name);
- if (verbose){
- fprintf(stderr, "\n %s\n", description);
- fprintf(stderr, "\n");
- }
+ void help(bool verbose = false) override
+ {
+ fprintf(stderr, " -%-10s = %8s\n", name, type_name);
+ if (verbose)
+ {
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
}
};
operator bool& (void) { return value; }
BoolOption& operator=(bool b) { value = b; return *this; }
- virtual bool parse(const char* str){
- const char* span = str;
-
- if (match(span, "-")){
- bool b = !match(span, "no-");
+ bool parse(const char* str) override
+ {
+ const char* span = str;
+
+ if (match(span, "-"))
+ {
+ bool b = !match(span, "no-");
- if (strcmp(span, name) == 0){
- value = b;
- return true; }
+ if (strcmp(span, name) == 0)
+ {
+ value = b;
+ return true;
}
+ }
- return false;
+ return false;
}
- virtual void help (bool verbose = false){
+ void help(bool verbose = false) override
+ {
+ fprintf(stderr, " -%s, -no-%s", name, name);
- fprintf(stderr, " -%s, -no-%s", name, name);
+ for (uint32_t i = 0; i < 32 - strlen(name) * 2; i++) fprintf(stderr, " ");
- for (uint32_t i = 0; i < 32 - strlen(name)*2; i++)
- fprintf(stderr, " ");
-
- fprintf(stderr, " ");
- fprintf(stderr, "(default: %s)\n", value ? "on" : "off");
- if (verbose){
- fprintf(stderr, "\n %s\n", description);
- fprintf(stderr, "\n");
- }
+ fprintf(stderr, " ");
+ fprintf(stderr, "(default: %s)\n", value ? "on" : "off");
+ if (verbose)
+ {
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
}
};
* @param removable is this something that can be erased
* @param negated true if negated
*/
- void convertAndAssert(TNode node, bool removable, bool negated,
- ProofRule rule, TNode from = TNode::null());
+ void convertAndAssert(TNode node,
+ bool removable,
+ bool negated,
+ ProofRule rule,
+ TNode from = TNode::null()) override;
private:
/**
*/
SatLiteral toCNF(TNode node, bool negated = false);
- void ensureLiteral(TNode n, bool noPreregistration = false);
+ void ensureLiteral(TNode n, bool noPreregistration = false) override;
}; /* class TseitinCnfStream */
static void toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause);
static void toSatClause (const Minisat::Clause& clause, SatClause& sat_clause);
- void initialize(context::Context* context, TheoryProxy* theoryProxy);
+ void initialize(context::Context* context, TheoryProxy* theoryProxy) override;
- ClauseId addClause(SatClause& clause, bool removable);
- ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) {
+ ClauseId addClause(SatClause& clause, bool removable) override;
+ ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
+ {
Unreachable("Minisat does not support native XOR reasoning");
}
- SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase);
- SatVariable trueVar() { return d_minisat->trueVar(); }
- SatVariable falseVar() { return d_minisat->falseVar(); }
+ SatVariable newVar(bool isTheoryAtom,
+ bool preRegister,
+ bool canErase) override;
+ SatVariable trueVar() override { return d_minisat->trueVar(); }
+ SatVariable falseVar() override { return d_minisat->falseVar(); }
- SatValue solve();
- SatValue solve(long unsigned int&);
+ SatValue solve() override;
+ SatValue solve(long unsigned int&) override;
- bool ok() const;
-
- void interrupt();
+ bool ok() const override;
- SatValue value(SatLiteral l);
+ void interrupt() override;
- SatValue modelValue(SatLiteral l);
+ SatValue value(SatLiteral l) override;
- bool properExplanation(SatLiteral lit, SatLiteral expl) const;
+ SatValue modelValue(SatLiteral l) override;
+
+ bool properExplanation(SatLiteral lit, SatLiteral expl) const override;
/** Incremental interface */
- unsigned getAssertionLevel() const;
+ unsigned getAssertionLevel() const override;
- void push();
+ void push() override;
- void pop();
+ void pop() override;
- void requirePhase(SatLiteral lit);
+ void requirePhase(SatLiteral lit) override;
- bool flipDecision();
+ bool flipDecision() override;
- bool isDecision(SatVariable decn) const;
+ bool isDecision(SatVariable decn) const override;
-private:
+ private:
/** The SatSolver used */
Minisat::SimpSolver* d_minisat;
// Memory managment:
//
- virtual void garbageCollect();
-
+ void garbageCollect() override;
// Generate a (possibly simplified) DIMACS file:
//
operator double& (void) { return value; }
DoubleOption& operator=(double x) { value = x; return *this; }
- virtual bool parse(const char* str){
- const char* span = str;
+ bool parse(const char* str) override
+ {
+ const char* span = str;
- if (!match(span, "-") || !match(span, name) || !match(span, "="))
- return false;
-
- char* end;
- double tmp = strtod(span, &end);
-
- if (end == NULL)
- return false;
- else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end)){
- fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
- exit(1);
- }else if (tmp <= range.begin && (!range.begin_inclusive || tmp != range.begin)){
- fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
- exit(1); }
+ if (!match(span, "-") || !match(span, name) || !match(span, "="))
+ return false;
- value = tmp;
- // fprintf(stderr, "READ VALUE: %g\n", value);
+ char* end;
+ double tmp = strtod(span, &end);
- return true;
+ if (end == NULL)
+ return false;
+ else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end))
+ {
+ fprintf(stderr,
+ "ERROR! value <%s> is too large for option \"%s\".\n",
+ span,
+ name);
+ exit(1);
+ }
+ else if (tmp <= range.begin
+ && (!range.begin_inclusive || tmp != range.begin))
+ {
+ fprintf(stderr,
+ "ERROR! value <%s> is too small for option \"%s\".\n",
+ span,
+ name);
+ exit(1);
+ }
+
+ value = tmp;
+ // fprintf(stderr, "READ VALUE: %g\n", value);
+
+ return true;
}
- virtual void help (bool verbose = false){
- fprintf(stderr, " -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n",
- name, type_name,
- range.begin_inclusive ? '[' : '(',
- range.begin,
- range.end,
- range.end_inclusive ? ']' : ')',
- value);
- if (verbose){
- fprintf(stderr, "\n %s\n", description);
- fprintf(stderr, "\n");
- }
+ void help(bool verbose = false) override
+ {
+ fprintf(stderr,
+ " -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n",
+ name,
+ type_name,
+ range.begin_inclusive ? '[' : '(',
+ range.begin,
+ range.end,
+ range.end_inclusive ? ']' : ')',
+ value);
+ if (verbose)
+ {
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
}
};
operator int32_t& (void) { return value; }
IntOption& operator= (int32_t x) { value = x; return *this; }
- virtual bool parse(const char* str){
- const char* span = str;
-
- if (!match(span, "-") || !match(span, name) || !match(span, "="))
- return false;
+ bool parse(const char* str) override
+ {
+ const char* span = str;
- char* end;
- int32_t tmp = strtol(span, &end, 10);
-
- if (end == NULL)
- return false;
- else if (tmp > range.end){
- fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
- exit(1);
- }else if (tmp < range.begin){
- fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
- exit(1); }
+ if (!match(span, "-") || !match(span, name) || !match(span, "="))
+ return false;
- value = tmp;
+ char* end;
+ int32_t tmp = strtol(span, &end, 10);
- return true;
+ if (end == NULL)
+ return false;
+ else if (tmp > range.end)
+ {
+ fprintf(stderr,
+ "ERROR! value <%s> is too large for option \"%s\".\n",
+ span,
+ name);
+ exit(1);
+ }
+ else if (tmp < range.begin)
+ {
+ fprintf(stderr,
+ "ERROR! value <%s> is too small for option \"%s\".\n",
+ span,
+ name);
+ exit(1);
+ }
+
+ value = tmp;
+
+ return true;
}
- virtual void help (bool verbose = false){
- fprintf(stderr, " -%-12s = %-8s [", name, type_name);
- if (range.begin == INT32_MIN)
- fprintf(stderr, "imin");
- else
- fprintf(stderr, "%4d", range.begin);
-
- fprintf(stderr, " .. ");
- if (range.end == INT32_MAX)
- fprintf(stderr, "imax");
- else
- fprintf(stderr, "%4d", range.end);
-
- fprintf(stderr, "] (default: %d)\n", value);
- if (verbose){
- fprintf(stderr, "\n %s\n", description);
- fprintf(stderr, "\n");
- }
+ void help(bool verbose = false) override
+ {
+ fprintf(stderr, " -%-12s = %-8s [", name, type_name);
+ if (range.begin == INT32_MIN)
+ fprintf(stderr, "imin");
+ else
+ fprintf(stderr, "%4d", range.begin);
+
+ fprintf(stderr, " .. ");
+ if (range.end == INT32_MAX)
+ fprintf(stderr, "imax");
+ else
+ fprintf(stderr, "%4d", range.end);
+
+ fprintf(stderr, "] (default: %d)\n", value);
+ if (verbose)
+ {
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
}
};
operator int64_t& (void) { return value; }
Int64Option& operator= (int64_t x) { value = x; return *this; }
- virtual bool parse(const char* str){
- const char* span = str;
-
- if (!match(span, "-") || !match(span, name) || !match(span, "="))
- return false;
+ bool parse(const char* str) override
+ {
+ const char* span = str;
- char* end;
- int64_t tmp = strtoll(span, &end, 10);
-
- if (end == NULL)
- return false;
- else if (tmp > range.end){
- fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name);
- exit(1);
- }else if (tmp < range.begin){
- fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name);
- exit(1); }
+ if (!match(span, "-") || !match(span, name) || !match(span, "="))
+ return false;
- value = tmp;
+ char* end;
+ int64_t tmp = strtoll(span, &end, 10);
- return true;
+ if (end == NULL)
+ return false;
+ else if (tmp > range.end)
+ {
+ fprintf(stderr,
+ "ERROR! value <%s> is too large for option \"%s\".\n",
+ span,
+ name);
+ exit(1);
+ }
+ else if (tmp < range.begin)
+ {
+ fprintf(stderr,
+ "ERROR! value <%s> is too small for option \"%s\".\n",
+ span,
+ name);
+ exit(1);
+ }
+
+ value = tmp;
+
+ return true;
}
- virtual void help (bool verbose = false){
- fprintf(stderr, " -%-12s = %-8s [", name, type_name);
- if (range.begin == INT64_MIN)
- fprintf(stderr, "imin");
- else
- fprintf(stderr, "%4" PRIi64, range.begin);
-
- fprintf(stderr, " .. ");
- if (range.end == INT64_MAX)
- fprintf(stderr, "imax");
- else
- fprintf(stderr, "%4" PRIi64, range.end);
-
- fprintf(stderr, "] (default: %" PRIi64")\n", value);
- if (verbose){
- fprintf(stderr, "\n %s\n", description);
- fprintf(stderr, "\n");
- }
+ void help(bool verbose = false) override
+ {
+ fprintf(stderr, " -%-12s = %-8s [", name, type_name);
+ if (range.begin == INT64_MIN)
+ fprintf(stderr, "imin");
+ else
+ fprintf(stderr, "%4" PRIi64, range.begin);
+
+ fprintf(stderr, " .. ");
+ if (range.end == INT64_MAX)
+ fprintf(stderr, "imax");
+ else
+ fprintf(stderr, "%4" PRIi64, range.end);
+
+ fprintf(stderr, "] (default: %" PRIi64 ")\n", value);
+ if (verbose)
+ {
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
}
};
#endif
operator const char*& (void) { return value; }
StringOption& operator= (const char* x) { value = x; return *this; }
- virtual bool parse(const char* str){
- const char* span = str;
+ bool parse(const char* str) override
+ {
+ const char* span = str;
- if (!match(span, "-") || !match(span, name) || !match(span, "="))
- return false;
+ if (!match(span, "-") || !match(span, name) || !match(span, "="))
+ return false;
- value = span;
- return true;
+ value = span;
+ return true;
}
- virtual void help (bool verbose = false){
- fprintf(stderr, " -%-10s = %8s\n", name, type_name);
- if (verbose){
- fprintf(stderr, "\n %s\n", description);
- fprintf(stderr, "\n");
- }
+ void help(bool verbose = false) override
+ {
+ fprintf(stderr, " -%-10s = %8s\n", name, type_name);
+ if (verbose)
+ {
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
}
};
operator bool& (void) { return value; }
BoolOption& operator=(bool b) { value = b; return *this; }
- virtual bool parse(const char* str){
- const char* span = str;
-
- if (match(span, "-")){
- bool b = !match(span, "no-");
+ bool parse(const char* str) override
+ {
+ const char* span = str;
+
+ if (match(span, "-"))
+ {
+ bool b = !match(span, "no-");
- if (strcmp(span, name) == 0){
- value = b;
- return true; }
+ if (strcmp(span, name) == 0)
+ {
+ value = b;
+ return true;
}
+ }
- return false;
+ return false;
}
- virtual void help (bool verbose = false){
+ void help(bool verbose = false) override
+ {
+ fprintf(stderr, " -%s, -no-%s", name, name);
- fprintf(stderr, " -%s, -no-%s", name, name);
+ for (uint32_t i = 0; i < 32 - strlen(name) * 2; i++) fprintf(stderr, " ");
- for (uint32_t i = 0; i < 32 - strlen(name)*2; i++)
- fprintf(stderr, " ");
-
- fprintf(stderr, " ");
- fprintf(stderr, "(default: %s)\n", value ? "on" : "off");
- if (verbose){
- fprintf(stderr, "\n %s\n", description);
- fprintf(stderr, "\n");
- }
+ fprintf(stderr, " ");
+ fprintf(stderr, "(default: %s)\n", value ? "on" : "off");
+ if (verbose)
+ {
+ fprintf(stderr, "\n %s\n", description);
+ fprintf(stderr, "\n");
+ }
}
};
class NullRegistrar : public Registrar {
public:
- void preRegister(Node n) {}
+ void preRegister(Node n) override {}
};/* class NullRegistrar */
virtual void popAssumption() = 0;
- virtual bool ok() const = 0;
-
- virtual void setProofLog( BitVectorProof * bvp ) {}
-
};/* class BVSatSolverInterface */
virtual bool flipDecision() = 0;
virtual bool isDecision(SatVariable decn) const = 0;
-
- virtual bool ok() const = 0;
};/* class DPLLSatSolverInterface */
inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
SetToDefaultSourceListener(ManagedOstream* managedOstream)
: d_managedOstream(managedOstream){}
- virtual void notify() {
+ void notify() override
+ {
d_managedOstream->set(d_managedOstream->defaultSource());
}
ManagedDumpOStream(){}
~ManagedDumpOStream();
- virtual const char* getName() const { return "dump-to"; }
- virtual std::string defaultSource() const;
+ const char* getName() const override { return "dump-to"; }
+ std::string defaultSource() const override;
protected:
/** Initializes an output stream. Not necessarily managed. */
- virtual void initialize(std::ostream* outStream);
+ void initialize(std::ostream* outStream) override;
/** Adds special cases to an ostreamopener. */
- virtual void addSpecialCases(OstreamOpener* opener) const;
+ void addSpecialCases(OstreamOpener* opener) const override;
};/* class ManagedDumpOStream */
/**
/** Assumes Options are in scope. */
~ManagedRegularOutputChannel();
- virtual const char* getName() const { return "regular-output-channel"; }
- virtual std::string defaultSource() const;
+ const char* getName() const override { return "regular-output-channel"; }
+ std::string defaultSource() const override;
protected:
/** Initializes an output stream. Not necessarily managed. */
- virtual void initialize(std::ostream* outStream);
+ void initialize(std::ostream* outStream) override;
/** Adds special cases to an ostreamopener. */
- virtual void addSpecialCases(OstreamOpener* opener) const;
+ void addSpecialCases(OstreamOpener* opener) const override;
};/* class ManagedRegularOutputChannel */
/** Assumes Options are in scope. */
~ManagedDiagnosticOutputChannel();
- virtual const char* getName() const { return "diagnostic-output-channel"; }
- virtual std::string defaultSource() const;
+ const char* getName() const override { return "diagnostic-output-channel"; }
+ std::string defaultSource() const override;
protected:
/** Initializes an output stream. Not necessarily managed. */
- virtual void initialize(std::ostream* outStream);
+ void initialize(std::ostream* outStream) override;
/** Adds special cases to an ostreamopener. */
- virtual void addSpecialCases(OstreamOpener* opener) const;
+ void addSpecialCases(OstreamOpener* opener) const override;
};/* class ManagedRegularOutputChannel */
/** This controls the memory associated with replay-log. */
~ManagedReplayLogOstream();
std::ostream* getReplayLog() const { return d_replayLog; }
- virtual const char* getName() const { return "replay-log"; }
- virtual std::string defaultSource() const;
+ const char* getName() const override { return "replay-log"; }
+ std::string defaultSource() const override;
protected:
/** Initializes an output stream. Not necessarily managed. */
- virtual void initialize(std::ostream* outStream);
+ void initialize(std::ostream* outStream) override;
/** Adds special cases to an ostreamopener. */
- virtual void addSpecialCases(OstreamOpener* opener) const;
+ void addSpecialCases(OstreamOpener* opener) const override;
private:
std::ostream* d_replayLog;
class SoftResourceOutListener : public Listener {
public:
SoftResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
- virtual void notify() {
+ void notify() override
+ {
SmtScope scope(d_smt);
Assert(smt::smtEngineInScope());
d_smt->interrupt();
class HardResourceOutListener : public Listener {
public:
HardResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
- virtual void notify() {
+ void notify() override
+ {
SmtScope scope(d_smt);
theory::Rewriter::clearCaches();
}
class SetLogicListener : public Listener {
public:
SetLogicListener(SmtEngine& smt) : d_smt(&smt) {}
- virtual void notify() {
+ void notify() override
+ {
LogicInfo inOptions(options::forceLogicString());
d_smt->setLogic(inOptions);
}
class BeforeSearchListener : public Listener {
public:
BeforeSearchListener(SmtEngine& smt) : d_smt(&smt) {}
- virtual void notify() {
- d_smt->beforeSearch();
- }
+ void notify() override { d_smt->beforeSearch(); }
+
private:
SmtEngine* d_smt;
}; /* class BeforeSearchListener */
: d_theoryEngine(theoryEngine)
{}
- void notify() {
+ void notify() override
+ {
std::stringstream commaList(options::useTheoryList());
std::string token;
class SetDefaultExprDepthListener : public Listener {
public:
- virtual void notify() {
+ void notify() override
+ {
int depth = options::defaultExprDepth();
Debug.getStream() << expr::ExprSetDepth(depth);
Trace.getStream() << expr::ExprSetDepth(depth);
class SetDefaultExprDagListener : public Listener {
public:
- virtual void notify() {
+ void notify() override
+ {
int dag = options::defaultDagThresh();
Debug.getStream() << expr::ExprDag(dag);
Trace.getStream() << expr::ExprDag(dag);
class SetPrintExprTypesListener : public Listener {
public:
- virtual void notify() {
+ void notify() override
+ {
bool value = options::printExprTypes();
Debug.getStream() << expr::ExprPrintTypes(value);
Trace.getStream() << expr::ExprPrintTypes(value);
class DumpModeListener : public Listener {
public:
- virtual void notify() {
+ void notify() override
+ {
const std::string& value = options::dumpModeString();
Dump.setDumpFromString(value);
}
class PrintSuccessListener : public Listener {
public:
- virtual void notify() {
+ void notify() override
+ {
bool value = options::printSuccess();
Debug.getStream() << Command::printsuccess(value);
Trace.getStream() << Command::printsuccess(value);
d_resourceManager->spendResource(amount);
}
- void nmNotifyNewSort(TypeNode tn, uint32_t flags) {
+ void nmNotifyNewSort(TypeNode tn, uint32_t flags) override
+ {
DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
0,
tn.toType());
}
}
- void nmNotifyNewSortConstructor(TypeNode tn) {
+ void nmNotifyNewSortConstructor(TypeNode tn) override
+ {
DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()),
tn.getAttribute(expr::SortArityAttr()),
tn.toType());
d_smt.addToModelCommandAndDump(c);
}
- void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) {
+ void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) override
+ {
DatatypeDeclarationCommand c(dtts);
d_smt.addToModelCommandAndDump(c);
}
- void nmNotifyNewVar(TNode n, uint32_t flags) {
+ void nmNotifyNewVar(TNode n, uint32_t flags) override
+ {
DeclareFunctionCommand c(n.getAttribute(expr::VarNameAttr()),
n.toExpr(),
n.getType().toType());
}
}
- void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) {
+ void nmNotifyNewSkolem(TNode n,
+ const std::string& comment,
+ uint32_t flags) override
+ {
string id = n.getAttribute(expr::VarNameAttr());
- DeclareFunctionCommand c(id,
- n.toExpr(),
- n.getType().toType());
+ DeclareFunctionCommand c(id, n.toExpr(), n.getType().toType());
if(Dump.isOn("skolems") && comment != "") {
Dump("skolems") << CommentCommand(id + " is " + comment);
}
}
}
- void nmNotifyDeleteNode(TNode n) {}
+ void nmNotifyDeleteNode(TNode n) override {}
Node applySubstitutions(TNode node) const {
return Rewriter::rewrite(d_topLevelSubstitutions.apply(node));
class OptionsErrOstreamUpdate : public OstreamUpdate {
public:
- virtual std::ostream& get() { return *(options::err()); }
- virtual void set(std::ostream* setTo) { return options::err.set(setTo); }
+ std::ostream& get() override { return *(options::err()); }
+ void set(std::ostream* setTo) override { return options::err.set(setTo); }
}; /* class OptionsErrOstreamUpdate */
class DumpOstreamUpdate : public OstreamUpdate {
public:
- virtual std::ostream& get() { return Dump.getStream(); }
- virtual void set(std::ostream* setTo) { Dump.setStream(setTo); }
+ std::ostream& get() override { return Dump.getStream(); }
+ void set(std::ostream* setTo) override { Dump.setStream(setTo); }
}; /* class DumpOstreamUpdate */
class DebugOstreamUpdate : public OstreamUpdate {
public:
- virtual std::ostream& get() { return Debug.getStream(); }
- virtual void set(std::ostream* setTo) { Debug.setStream(setTo); }
+ std::ostream& get() override { return Debug.getStream(); }
+ void set(std::ostream* setTo) override { Debug.setStream(setTo); }
}; /* class DebugOstreamUpdate */
class WarningOstreamUpdate : public OstreamUpdate {
public:
- virtual std::ostream& get() { return Warning.getStream(); }
- virtual void set(std::ostream* setTo) { Warning.setStream(setTo); }
+ std::ostream& get() override { return Warning.getStream(); }
+ void set(std::ostream* setTo) override { Warning.setStream(setTo); }
}; /* class WarningOstreamUpdate */
class MessageOstreamUpdate : public OstreamUpdate {
public:
- virtual std::ostream& get() { return Message.getStream(); }
- virtual void set(std::ostream* setTo) { Message.setStream(setTo); }
+ std::ostream& get() override { return Message.getStream(); }
+ void set(std::ostream* setTo) override { Message.setStream(setTo); }
}; /* class MessageOstreamUpdate */
class NoticeOstreamUpdate : public OstreamUpdate {
public:
- virtual std::ostream& get() { return Notice.getStream(); }
- virtual void set(std::ostream* setTo) { Notice.setStream(setTo); }
+ std::ostream& get() override { return Notice.getStream(); }
+ void set(std::ostream* setTo) override { Notice.setStream(setTo); }
}; /* class NoticeOstreamUpdate */
class ChatOstreamUpdate : public OstreamUpdate {
public:
- virtual std::ostream& get() { return Chat.getStream(); }
- virtual void set(std::ostream* setTo) { Chat.setStream(setTo); }
+ std::ostream& get() override { return Chat.getStream(); }
+ void set(std::ostream* setTo) override { Chat.setStream(setTo); }
}; /* class ChatOstreamUpdate */
class TraceOstreamUpdate : public OstreamUpdate {
public:
- virtual std::ostream& get() { return Trace.getStream(); }
- virtual void set(std::ostream* setTo) { Trace.setStream(setTo); }
+ std::ostream& get() override { return Trace.getStream(); }
+ void set(std::ostream* setTo) override { Trace.setStream(setTo); }
}; /* class TraceOstreamUpdate */
}/* CVC4 namespace */
Result::Sat attempt(const ApproximateSimplex::Solution& sol);
- Result::Sat findModel(bool exactResult){
- Unreachable();
- }
+ Result::Sat findModel(bool exactResult) override { Unreachable(); }
-private:
+ private:
bool matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const;
bool processSignals(){
TheoryArithPrivate& d_arith;
public:
SetupLiteralCallBack(TheoryArithPrivate& ta);
- void operator()(TNode lit);
+ void operator()(TNode lit) override;
};
class DeltaComputeCallback : public RationalCallBack {
const TheoryArithPrivate& d_ta;
public:
DeltaComputeCallback(const TheoryArithPrivate& ta);
- Rational operator()() const;
+ Rational operator()() const override;
};
class BasicVarModelUpdateCallBack : public ArithVarCallBack{
TheoryArithPrivate& d_ta;
public:
BasicVarModelUpdateCallBack(TheoryArithPrivate& ta);
- void operator()(ArithVar x);
+ void operator()(ArithVar x) override;
};
class TempVarMalloc : public ArithVarMalloc {
TheoryArithPrivate& d_ta;
public:
TempVarMalloc(TheoryArithPrivate& ta);
- ArithVar request();
- void release(ArithVar v);
+ ArithVar request() override;
+ void release(ArithVar v) override;
};
class RaiseConflict {
public:
ArithCongruenceNotify(ArithCongruenceManager& acm);
- bool eqNotifyTriggerEquality(TNode equality, bool value);
+ bool eqNotifyTriggerEquality(TNode equality, bool value) override;
- bool eqNotifyTriggerPredicate(TNode predicate, bool value);
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
- bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
+ bool eqNotifyTriggerTermEquality(TheoryId tag,
+ TNode t1,
+ TNode t2,
+ bool value) override;
- void eqNotifyConstantTermMerge(TNode t1, TNode t2);
- void eqNotifyNewClass(TNode t);
- void eqNotifyPreMerge(TNode t1, TNode t2);
- void eqNotifyPostMerge(TNode t1, TNode t2);
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
+ void eqNotifyNewClass(TNode t) override;
+ void eqNotifyPreMerge(TNode t1, TNode t2) override;
+ void eqNotifyPostMerge(TNode t1, TNode t2) override;
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
};
ArithCongruenceNotify d_notify;
public:
DualSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
- Result::Sat findModel(bool exactResult) {
+ Result::Sat findModel(bool exactResult) override
+ {
return dualFindModel(exactResult);
}
public:
FCSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
- Result::Sat findModel(bool exactResult);
+ Result::Sat findModel(bool exactResult) override;
// other error variables are dropping
WitnessImprovement dualLikeImproveError(ArithVar evar);
LinearEqualityModule* d_linEq;
public:
TrackingCallback(LinearEqualityModule* le) : d_linEq(le) {}
- void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn){
+ void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) override
+ {
d_linEq->trackingCoefficientChange(ridx, nb, oldSgn, currSgn);
}
- void multiplyRow(RowIndex ridx, int sgn){
+ void multiplyRow(RowIndex ridx, int sgn) override
+ {
d_linEq->trackingMultiplyRow(ridx, sgn);
}
- bool canUseRow(RowIndex ridx) const {
+ bool canUseRow(RowIndex ridx) const override
+ {
ArithVar basic = d_linEq->getTableau().rowIndexToBasic(ridx);
return d_linEq->basicIsTracked(basic);
}
LinearEqualityModule* d_mod;
public:
UpdateTrackingCallback(LinearEqualityModule* mod): d_mod(mod){}
- void operator()(ArithVar v, const BoundsInfo& bi){
+ void operator()(ArithVar v, const BoundsInfo& bi) override
+ {
d_mod->includeBoundUpdate(v, bi);
}
};
class NoEffectCCCB : public CoefficientChangeCallback {
public:
- void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn);
- void multiplyRow(RowIndex ridx, int Sgn);
- bool canUseRow(RowIndex ridx) const;
+ void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) override;
+ void multiplyRow(RowIndex ridx, int Sgn) override;
+ bool canUseRow(RowIndex ridx) const override;
};
template<class T>
public:
SumOfInfeasibilitiesSPD(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
- Result::Sat findModel(bool exactResult);
+ Result::Sat findModel(bool exactResult) override;
// other error variables are dropping
WitnessImprovement dualLikeImproveError(ArithVar evar);
public:
NotifyClass(TheoryArrays& arrays): d_arrays(arrays) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) {
+ bool eqNotifyTriggerEquality(TNode equality, bool value) override
+ {
Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
// Just forward to arrays
if (value) {
}
}
- bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+ {
Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
// Just forward to arrays
if (value) {
}
}
- bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
+ bool eqNotifyTriggerTermEquality(TheoryId tag,
+ TNode t1,
+ TNode t2,
+ bool value) override
+ {
Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
if (value) {
if (t1.getType().isArray()) {
return true;
}
- void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
+ {
Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
d_arrays.conflict(t1, t2);
}
- void eqNotifyNewClass(TNode t) { }
- void eqNotifyPreMerge(TNode t1, TNode t2) { }
- void eqNotifyPostMerge(TNode t1, TNode t2) {
+ void eqNotifyNewClass(TNode t) override {}
+ void eqNotifyPreMerge(TNode t1, TNode t2) override {}
+ void eqNotifyPostMerge(TNode t1, TNode t2) override
+ {
if (t1.getType().isArray()) {
d_arrays.mergeArrays(t1, t2);
}
}
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
};
/** The notify class for d_equalityEngine */
context::Context* d_satContext;
context::Context* d_contextToPop;
protected:
- void contextNotifyPop() {
- if (d_contextToPop->getLevel() > d_satContext->getLevel()) {
- d_contextToPop->pop();
- }
+ void contextNotifyPop() override
+ {
+ if (d_contextToPop->getLevel() > d_satContext->getLevel())
+ {
+ d_contextToPop->pop();
+ }
}
public:
ContextPopper(context::Context* context, context::Context* contextToPop)
class DataClearer : context::ContextNotifyObj {
T& d_data;
protected:
- void contextNotifyPop() {
- Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data "
- << "(size was " << d_data.size() << ")" << std::endl;
- d_data.clear();
+ void contextNotifyPop() override
+ {
+ Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data "
+ << "(size was " << d_data.size() << ")" << std::endl;
+ d_data.clear();
}
public:
DataClearer(context::Context* context, T& data) :
: Theory(THEORY_BOOL, c, u, out, valuation, logicInfo)
{}
- PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+ PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
//void check(Effort);
-
- std::string identify() const { return std::string("TheoryBool"); }
+
+ std::string identify() const override { return std::string("TheoryBool"); }
};/* class TheoryBool */
}/* CVC4::theory::booleans namespace */
OutputChannel& out, Valuation valuation,
const LogicInfo& logicInfo)
: Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) {}
- std::string identify() const { return std::string("TheoryBuiltin"); }
+ std::string identify() const override { return std::string("TheoryBuiltin"); }
};/* class TheoryBuiltin */
}/* CVC4::theory::builtin namespace */
void addAtom(TNode atom);
bool hasValue(TNode a);
- Node getModelFromSatSolver(TNode a, bool fullModel);
+ Node getModelFromSatSolver(TNode a, bool fullModel) override;
-public:
- void bbTerm(TNode node, Bits& bits);
- void bbAtom(TNode node);
- Node getBBAtom(TNode atom) const;
- void storeBBAtom(TNode atom, Node atom_bb);
- void storeBBTerm(TNode node, const Bits& bits);
- bool hasBBAtom(TNode atom) const;
+ public:
+ void bbTerm(TNode node, Bits& bits) override;
+ void bbAtom(TNode node) override;
+ Node getBBAtom(TNode atom) const override;
+ void storeBBAtom(TNode atom, Node atom_bb) override;
+ void storeBBTerm(TNode node, const Bits& bits) override;
+ bool hasBBAtom(TNode atom) const override;
TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name="", bool emptyNotify = false);
~TLazyBitblaster();
*
* @param var
*/
- void makeVariable(TNode var, Bits& bits);
+ void makeVariable(TNode var, Bits& bits) override;
bool isSharedTerm(TNode node);
uint64_t computeAtomWeight(TNode node, NodeSet& seen);
// This is either an MinisatEmptyNotify or NULL.
MinisatEmptyNotify* d_notify;
- Node getModelFromSatSolver(TNode a, bool fullModel);
+ Node getModelFromSatSolver(TNode a, bool fullModel) override;
bool isSharedTerm(TNode node);
public:
~EagerBitblaster();
void addAtom(TNode atom);
- void makeVariable(TNode node, Bits& bits);
- void bbTerm(TNode node, Bits& bits);
- void bbAtom(TNode node);
- Node getBBAtom(TNode node) const;
- bool hasBBAtom(TNode atom) const;
+ void makeVariable(TNode node, Bits& bits) override;
+ void bbTerm(TNode node, Bits& bits) override;
+ void bbAtom(TNode node) override;
+ Node getBBAtom(TNode node) const override;
+ bool hasBBAtom(TNode atom) const override;
void bbFormula(TNode formula);
- void storeBBAtom(TNode atom, Node atom_bb);
- void storeBBTerm(TNode node, const Bits& bits);
+ void storeBBAtom(TNode atom, Node atom_bb) override;
+ void storeBBTerm(TNode node, const Bits& bits) override;
bool assertToSat(TNode node, bool propagate = true);
bool solve();
BitblastingRegistrar(EagerBitblaster* bb)
: d_bitblaster(bb)
{}
- void preRegister(Node n);
+ void preRegister(Node n) override;
}; /* class Registrar */
class AigBitblaster : public TBitblaster<Abc_Obj_t*> {
void addAtom(TNode atom);
void simplifyAig();
- void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb);
- Abc_Obj_t* getBBAtom(TNode atom) const;
- bool hasBBAtom(TNode atom) const;
+ void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) override;
+ Abc_Obj_t* getBBAtom(TNode atom) const override;
+ bool hasBBAtom(TNode atom) const override;
void cacheAig(TNode node, Abc_Obj_t* aig);
bool hasAig(TNode node);
Abc_Obj_t* getAig(TNode node);
bool hasInput(TNode input);
void convertToCnfAndAssert();
void assertToSatSolver(Cnf_Dat_t* pCnf);
- Node getModelFromSatSolver(TNode a, bool fullModel) { Unreachable(); }
-public:
+ Node getModelFromSatSolver(TNode a, bool fullModel) override
+ {
+ Unreachable();
+ }
+
+ public:
AigBitblaster();
~AigBitblaster();
- void makeVariable(TNode node, Bits& bits);
- void bbTerm(TNode node, Bits& bits);
- void bbAtom(TNode node);
+ void makeVariable(TNode node, Bits& bits) override;
+ void bbTerm(TNode node, Bits& bits) override;
+ void bbAtom(TNode node) override;
Abc_Obj_t* bbFormula(TNode formula);
bool solve(TNode query);
static Abc_Aig_t* currentAigM();
Node makeDiseqSplitLemma(TNode diseq);
/** Backtracking mechanisms **/
std::vector<std::pair<TermId, InequalityEdge> > d_undoStack;
- context::CDO<unsigned> d_undoStackIndex;
-
- void contextNotifyPop() {
- backtrack();
- }
+ context::CDO<unsigned> d_undoStackIndex;
+
+ void contextNotifyPop() override { backtrack(); }
void backtrack();
AlgebraicSolver(context::Context* c, TheoryBV* bv);
~AlgebraicSolver();
- void preRegister(TNode node) {}
- bool check(Theory::Effort e);
- void explain(TNode literal, std::vector<TNode>& assumptions) {Unreachable("AlgebraicSolver does not propagate.\n");}
- EqualityStatus getEqualityStatus(TNode a, TNode b);
- bool collectModelInfo(TheoryModel* m, bool fullModel);
- Node getModelValue(TNode node);
- bool isComplete();
- virtual void assertFact(TNode fact);
+ void preRegister(TNode node) override {}
+ bool check(Theory::Effort e) override;
+ void explain(TNode literal, std::vector<TNode>& assumptions) override
+ {
+ Unreachable("AlgebraicSolver does not propagate.\n");
+ }
+ EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+ bool collectModelInfo(TheoryModel* m, bool fullModel) override;
+ Node getModelValue(TNode node) override;
+ bool isComplete() override;
+ void assertFact(TNode fact) override;
};
-}
-}
-}
+} // namespace bv
+} // namespace theory
+} // namespace CVC4
BitblastSolver(context::Context* c, TheoryBV* bv);
~BitblastSolver();
- void preRegister(TNode node);
- bool check(Theory::Effort e);
- void explain(TNode literal, std::vector<TNode>& assumptions);
- EqualityStatus getEqualityStatus(TNode a, TNode b);
- bool collectModelInfo(TheoryModel* m, bool fullModel);
- Node getModelValue(TNode node);
- bool isComplete() { return true; }
+ void preRegister(TNode node) override;
+ bool check(Theory::Effort e) override;
+ void explain(TNode literal, std::vector<TNode>& assumptions) override;
+ EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+ bool collectModelInfo(TheoryModel* m, bool fullModel) override;
+ Node getModelValue(TNode node) override;
+ bool isComplete() override { return true; }
void bitblastQueue();
void setAbstraction(AbstractionModule* module);
uint64_t computeAtomWeight(TNode atom);
- void setProofLog( BitVectorProof * bvp );
+ void setProofLog(BitVectorProof* bvp) override;
};
} /* namespace CVC4::theory::bv */
public:
NotifyClass(CoreSolver& solver): d_solver(solver) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value);
- bool eqNotifyTriggerPredicate(TNode predicate, bool value);
- bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
- void eqNotifyConstantTermMerge(TNode t1, TNode t2);
- void eqNotifyNewClass(TNode t);
- void eqNotifyPreMerge(TNode t1, TNode t2) { }
- void eqNotifyPostMerge(TNode t1, TNode t2) { }
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
+ bool eqNotifyTriggerEquality(TNode equality, bool value) override;
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
+ bool eqNotifyTriggerTermEquality(TheoryId tag,
+ TNode t1,
+ TNode t2,
+ bool value) override;
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
+ void eqNotifyNewClass(TNode t) override;
+ void eqNotifyPreMerge(TNode t1, TNode t2) override {}
+ void eqNotifyPostMerge(TNode t1, TNode t2) override {}
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
};
public:
CoreSolver(context::Context* c, TheoryBV* bv);
~CoreSolver();
- bool isComplete() { return d_isComplete; }
+ bool isComplete() override { return d_isComplete; }
void setMasterEqualityEngine(eq::EqualityEngine* eq);
- void preRegister(TNode node);
- bool check(Theory::Effort e);
- void explain(TNode literal, std::vector<TNode>& assumptions);
- bool collectModelInfo(TheoryModel* m, bool fullModel);
- Node getModelValue(TNode var);
- void addSharedTerm(TNode t) {
+ void preRegister(TNode node) override;
+ bool check(Theory::Effort e) override;
+ void explain(TNode literal, std::vector<TNode>& assumptions) override;
+ bool collectModelInfo(TheoryModel* m, bool fullModel) override;
+ Node getModelValue(TNode var) override;
+ void addSharedTerm(TNode t) override
+ {
d_equalityEngine.addTriggerTerm(t, THEORY_BV);
}
- EqualityStatus getEqualityStatus(TNode a, TNode b) {
+ EqualityStatus getEqualityStatus(TNode a, TNode b) override
+ {
if (d_equalityEngine.areEqual(a, b)) {
// The terms are implied to be equal
return EQUALITY_TRUE;
d_statistics()
{}
- bool check(Theory::Effort e);
- void propagate(Theory::Effort e);
- void explain(TNode literal, std::vector<TNode>& assumptions);
- bool isComplete() { return d_isComplete; }
- bool collectModelInfo(TheoryModel* m, bool fullModel);
- Node getModelValue(TNode var);
- EqualityStatus getEqualityStatus(TNode a, TNode b);
- void assertFact(TNode fact);
- void preRegister(TNode node);
+ bool check(Theory::Effort e) override;
+ void propagate(Theory::Effort e) override;
+ void explain(TNode literal, std::vector<TNode>& assumptions) override;
+ bool isComplete() override { return d_isComplete; }
+ bool collectModelInfo(TheoryModel* m, bool fullModel) override;
+ Node getModelValue(TNode var) override;
+ EqualityStatus getEqualityStatus(TNode a, TNode b) override;
+ void assertFact(TNode fact) override;
+ void preRegister(TNode node) override;
};
}
d_bits(0) {
}
- Node operator*() {
+ Node operator*() override
+ {
if(d_bits != d_bits.modByPow2(d_size)) {
throw NoMoreValuesException(getType());
}
return utils::mkConst(d_size, d_bits);
}
- BitVectorEnumerator& operator++()
+ BitVectorEnumerator& operator++() override
{
d_bits += 1;
return *this;
}
- bool isFinished() { return d_bits != d_bits.modByPow2(d_size); }
+ bool isFinished() override { return d_bits != d_bits.modByPow2(d_size); }
};/* BitVectorEnumerator */
}/* CVC4::theory::bv namespace */
TheoryDatatypes& d_dt;
public:
NotifyClass(TheoryDatatypes& dt): d_dt(dt) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) {
+ bool eqNotifyTriggerEquality(TNode equality, bool value) override
+ {
Debug("dt") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
if (value) {
return d_dt.propagate(equality);
return d_dt.propagate(equality.notNode());
}
}
- bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+ {
Debug("dt") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
if (value) {
return d_dt.propagate(predicate);
return d_dt.propagate(predicate.notNode());
}
}
- bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
+ bool eqNotifyTriggerTermEquality(TheoryId tag,
+ TNode t1,
+ TNode t2,
+ bool value) override
+ {
Debug("dt") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
if (value) {
return d_dt.propagate(t1.eqNode(t2));
return d_dt.propagate(t1.eqNode(t2).notNode());
}
}
- void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
+ {
Debug("dt") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
d_dt.conflict(t1, t2);
}
- void eqNotifyNewClass(TNode t) {
+ void eqNotifyNewClass(TNode t) override
+ {
Debug("dt") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl;
d_dt.eqNotifyNewClass(t);
}
- void eqNotifyPreMerge(TNode t1, TNode t2) {
+ void eqNotifyPreMerge(TNode t1, TNode t2) override
+ {
Debug("dt") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl;
d_dt.eqNotifyPreMerge(t1, t2);
}
- void eqNotifyPostMerge(TNode t1, TNode t2) {
+ void eqNotifyPostMerge(TNode t1, TNode t2) override
+ {
Debug("dt") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl;
d_dt.eqNotifyPostMerge(t1, t2);
}
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
+ {
Debug("dt") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl;
d_dt.eqNotifyDisequal(t1, t2, reason);
}
public:
NotifyClass(TheoryFp& solver) : d_theorySolver(solver) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value);
- bool eqNotifyTriggerPredicate(TNode predicate, bool value);
- bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2,
- bool value);
- void eqNotifyConstantTermMerge(TNode t1, TNode t2);
- void eqNotifyNewClass(TNode t) {}
- void eqNotifyPreMerge(TNode t1, TNode t2) {}
- void eqNotifyPostMerge(TNode t1, TNode t2) {}
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {}
+ bool eqNotifyTriggerEquality(TNode equality, bool value) override;
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
+ bool eqNotifyTriggerTermEquality(TheoryId tag,
+ TNode t1,
+ TNode t2,
+ bool value) override;
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
+ void eqNotifyNewClass(TNode t) override {}
+ void eqNotifyPreMerge(TNode t1, TNode t2) override {}
+ void eqNotifyPostMerge(TNode t1, TNode t2) override {}
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
};
friend NotifyClass;
Valuation valuation, const LogicInfo& logicInfo);
/** Pre-processing of input atoms */
- Node ppRewrite(TNode atom);
+ Node ppRewrite(TNode atom) override;
/** Check the assertions for satisfiability */
- void check(Effort effort);
+ void check(Effort effort) override;
/** Identity string */
- std::string identify() const { return "THEORY_IDL"; }
+ std::string identify() const override { return "THEORY_IDL"; }
};/* class TheoryIdl */
bool pconnected = true );
/* Call during quantifier engine's check */
- void check(Theory::Effort e, QEffort quant_e);
+ void check(Theory::Effort e, QEffort quant_e) override;
/* Called for new quantifiers */
- void registerQuantifier( Node q ) {}
- void assertNode( Node n ) {}
+ void registerQuantifier(Node q) override {}
+ void assertNode(Node n) override {}
/** Identify this module (for debugging, dynamic configuration, etc..) */
- std::string identify() const { return "QuantAntiSkolem"; }
+ std::string identify() const override { return "QuantAntiSkolem"; }
private:
typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
bool useModelValue(CegInstantiator* ci,
SolvedForm& sf,
Node pv,
- CegInstEffort effort)
+ CegInstEffort effort) override
{
return true;
}
- std::string identify() const { return "ModelValue"; }
+ std::string identify() const override { return "ModelValue"; }
};
/** instantiator preprocess
}
~CegInstantiatorBvInverterQuery() {}
/** return the model value of n */
- Node getModelValue( Node n ) {
- return d_ci->getModelValue( n );
- }
+ Node getModelValue(Node n) override { return d_ci->getModelValue(n); }
/** get bound variable of type tn */
- Node getBoundVariable(TypeNode tn) { return d_ci->getBoundVariable(tn); }
+ Node getBoundVariable(TypeNode tn) override
+ {
+ return d_ci->getBoundVariable(tn);
+ }
+
protected:
// pointer to class that is able to query model values
CegInstantiator * d_ci;
public:
ArithInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
virtual ~ArithInstantiator(){}
- virtual void reset(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- CegInstEffort effort) override;
- virtual bool hasProcessEquality(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- CegInstEffort effort) override
+ void reset(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ CegInstEffort effort) override;
+ bool hasProcessEquality(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ CegInstEffort effort) override
{
return true;
}
- virtual bool processEquality(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- std::vector<TermProperties>& term_props,
- std::vector<Node>& terms,
- CegInstEffort effort) override;
- virtual bool hasProcessAssertion(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- CegInstEffort effort) override
+ bool processEquality(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ std::vector<TermProperties>& term_props,
+ std::vector<Node>& terms,
+ CegInstEffort effort) override;
+ bool hasProcessAssertion(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ CegInstEffort effort) override
{
return true;
}
- virtual Node hasProcessAssertion(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- Node lit,
- CegInstEffort effort) override;
- virtual bool processAssertion(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- Node lit,
- Node alit,
- CegInstEffort effort) override;
- virtual bool processAssertions(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- CegInstEffort effort) override;
- virtual bool needsPostProcessInstantiationForVariable(
- CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- CegInstEffort effort) override;
- virtual bool postProcessInstantiationForVariable(
- CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- CegInstEffort effort,
- std::vector<Node>& lemmas) override;
- virtual std::string identify() const override { return "Arith"; }
+ Node hasProcessAssertion(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ Node lit,
+ CegInstEffort effort) override;
+ bool processAssertion(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ Node lit,
+ Node alit,
+ CegInstEffort effort) override;
+ bool processAssertions(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ CegInstEffort effort) override;
+ bool needsPostProcessInstantiationForVariable(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ CegInstEffort effort) override;
+ bool postProcessInstantiationForVariable(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ CegInstEffort effort,
+ std::vector<Node>& lemmas) override;
+ std::string identify() const override { return "Arith"; }
+
private:
Node d_vts_sym[2];
std::vector<Node> d_mbp_bounds[2];
public:
DtInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
virtual ~DtInstantiator(){}
- virtual void reset(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- CegInstEffort effort) override;
- virtual bool processEqualTerms(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- std::vector<Node>& eqc,
- CegInstEffort effort) override;
- virtual bool hasProcessEquality(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- CegInstEffort effort) override
+ void reset(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ CegInstEffort effort) override;
+ bool processEqualTerms(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ std::vector<Node>& eqc,
+ CegInstEffort effort) override;
+ bool hasProcessEquality(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ CegInstEffort effort) override
{
return true;
}
- virtual bool processEquality(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- std::vector<TermProperties>& term_props,
- std::vector<Node>& terms,
- CegInstEffort effort) override;
- virtual std::string identify() const override { return "Dt"; }
+ bool processEquality(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ std::vector<TermProperties>& term_props,
+ std::vector<Node>& terms,
+ CegInstEffort effort) override;
+ std::string identify() const override { return "Dt"; }
+
private:
Node solve_dt(Node v, Node a, Node b, Node sa, Node sb);
};
public:
EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){}
virtual ~EprInstantiator(){}
- virtual void reset(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- CegInstEffort effort) override;
- virtual bool processEqualTerm(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- TermProperties& pv_prop,
- Node n,
- CegInstEffort effort) override;
- virtual bool processEqualTerms(CegInstantiator* ci,
- SolvedForm& sf,
- Node pv,
- std::vector<Node>& eqc,
- CegInstEffort effort) override;
- virtual std::string identify() const override { return "Epr"; }
+ void reset(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ CegInstEffort effort) override;
+ bool processEqualTerm(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ TermProperties& pv_prop,
+ Node n,
+ CegInstEffort effort) override;
+ bool processEqualTerms(CegInstantiator* ci,
+ SolvedForm& sf,
+ Node pv,
+ std::vector<Node>& eqc,
+ CegInstEffort effort) override;
+ std::string identify() const override { return "Epr"; }
+
private:
std::vector<Node> d_equal_terms;
void computeMatchScore(CegInstantiator* ci,
/** whether to do CBQI for quantifier q */
bool doCbqi( Node q );
/** process functions */
- bool needsCheck( Theory::Effort e );
- QEffort needsModel(Theory::Effort e);
- void reset_round( Theory::Effort e );
- void check(Theory::Effort e, QEffort quant_e);
- bool checkComplete();
- bool checkCompleteFor( Node q );
- void preRegisterQuantifier( Node q );
- void registerQuantifier( Node q );
+ bool needsCheck(Theory::Effort e) override;
+ QEffort needsModel(Theory::Effort e) override;
+ void reset_round(Theory::Effort e) override;
+ void check(Theory::Effort e, QEffort quant_e) override;
+ bool checkComplete() override;
+ bool checkCompleteFor(Node q) override;
+ void preRegisterQuantifier(Node q) override;
+ void registerQuantifier(Node q) override;
/** get next decision request */
- Node getNextDecisionRequest( unsigned& priority );
+ Node getNextDecisionRequest(unsigned& priority) override;
};
//generalized counterexample guided quantifier instantiation
public:
CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){}
InstStrategyCegqi * d_out;
- bool doAddInstantiation( std::vector< Node >& subs );
- bool isEligibleForInstantiation( Node n );
- bool addLemma( Node lem );
+ bool doAddInstantiation(std::vector<Node>& subs) override;
+ bool isEligibleForInstantiation(Node n) override;
+ bool addLemma(Node lem) override;
};
class InstStrategyCegqi : public InstStrategyCbqi {
ConjectureGenerator& d_sg;
public:
NotifyClass(ConjectureGenerator& sg): d_sg(sg) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
- bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
- bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
- void eqNotifyConstantTermMerge(TNode t1, TNode t2) { }
- void eqNotifyNewClass(TNode t) { d_sg.eqNotifyNewClass(t); }
- void eqNotifyPreMerge(TNode t1, TNode t2) { d_sg.eqNotifyPreMerge(t1, t2); }
- void eqNotifyPostMerge(TNode t1, TNode t2) { d_sg.eqNotifyPostMerge(t1, t2); }
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {d_sg.eqNotifyDisequal(t1, t2, reason); }
+ bool eqNotifyTriggerEquality(TNode equality, bool value) override
+ {
+ return true;
+ }
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+ {
+ return true;
+ }
+ bool eqNotifyTriggerTermEquality(TheoryId tag,
+ TNode t1,
+ TNode t2,
+ bool value) override
+ {
+ return true;
+ }
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
+ void eqNotifyNewClass(TNode t) override { d_sg.eqNotifyNewClass(t); }
+ void eqNotifyPreMerge(TNode t1, TNode t2) override
+ {
+ d_sg.eqNotifyPreMerge(t1, t2);
+ }
+ void eqNotifyPostMerge(TNode t1, TNode t2) override
+ {
+ d_sg.eqNotifyPostMerge(t1, t2);
+ }
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
+ {
+ d_sg.eqNotifyDisequal(t1, t2, reason);
+ }
};/* class ConjectureGenerator::NotifyClass */
/** The notify class */
NotifyClass d_notify;
ConjectureGenerator( QuantifiersEngine * qe, context::Context* c );
/* needs check */
- bool needsCheck( Theory::Effort e );
+ bool needsCheck(Theory::Effort e) override;
/* reset at a round */
- void reset_round( Theory::Effort e );
+ void reset_round(Theory::Effort e) override;
/* Call during quantifier engine's check */
- void check(Theory::Effort e, QEffort quant_e);
+ void check(Theory::Effort e, QEffort quant_e) override;
/* Called for new quantifiers */
- void registerQuantifier( Node q );
- void assertNode( Node n );
+ void registerQuantifier(Node q) override;
+ void assertNode(Node n) override;
/** Identify this module (for debugging, dynamic configuration, etc..) */
- std::string identify() const { return "ConjectureGenerator"; }
-//options
-private:
+ std::string identify() const override { return "ConjectureGenerator"; }
+ // options
+ private:
bool optReqDistinctVarPatterns();
bool optFilterUnknown();
int optFilterScoreThreshold();
* Extends Trigger::addInstantiations to also send
* lemmas based on addHoTypeMatchPredicateLemmas.
*/
- virtual int addInstantiations() override;
+ int addInstantiations() override;
protected:
/**
/** counter for quantifiers */
std::map< Node, int > d_counter;
/** process functions */
- void processResetInstantiationRound( Theory::Effort effort );
- int process( Node f, Theory::Effort effort, int e );
-public:
+ void processResetInstantiationRound(Theory::Effort effort) override;
+ int process(Node f, Theory::Effort effort, int e) override;
+
+ public:
InstStrategyUserPatterns( QuantifiersEngine* ie ) :
InstStrategy( ie ){}
~InstStrategyUserPatterns(){}
/** get user pattern */
inst::Trigger* getUserGenerator( Node q, int i ) { return d_user_gen[q][ i ]; }
/** identify */
- std::string identify() const { return std::string("UserPatterns"); }
+ std::string identify() const override { return std::string("UserPatterns"); }
};/* class InstStrategyUserPatterns */
class InstStrategyAutoGenTriggers : public InstStrategy {
std::map< Node, Node > d_pat_to_mpat;
private:
/** process functions */
- void processResetInstantiationRound( Theory::Effort effort );
- int process( Node q, Theory::Effort effort, int e );
- /** generate triggers */
- void generateTriggers( Node q );
- void addPatternToPool( Node q, Node pat, unsigned num_fv, Node mpat );
- void addTrigger( inst::Trigger * tr, Node f );
- /** has user patterns */
- bool hasUserPatterns( Node q );
- /** has user patterns */
- std::map< Node, bool > d_hasUserPatterns;
+ void processResetInstantiationRound(Theory::Effort effort) override;
+ int process(Node q, Theory::Effort effort, int e) override;
+ /** generate triggers */
+ void generateTriggers(Node q);
+ void addPatternToPool(Node q, Node pat, unsigned num_fv, Node mpat);
+ void addTrigger(inst::Trigger* tr, Node f);
+ /** has user patterns */
+ bool hasUserPatterns(Node q);
+ /** has user patterns */
+ std::map<Node, bool> d_hasUserPatterns;
public:
InstStrategyAutoGenTriggers( QuantifiersEngine* qe );
~InstStrategyAutoGenTriggers(){}
/** get auto-generated trigger */
inst::Trigger* getAutoGenTrigger( Node q );
/** identify */
- std::string identify() const { return std::string("AutoGenTriggers"); }
+ std::string identify() const override
+ {
+ return std::string("AutoGenTriggers");
+ }
/** add pattern */
void addUserNoPattern( Node q, Node pat );
};/* class InstStrategyAutoGenTriggers */
public:
InstantiationEngine(QuantifiersEngine* qe);
~InstantiationEngine();
- void presolve();
- bool needsCheck(Theory::Effort e);
- void reset_round(Theory::Effort e);
- void check(Theory::Effort e, QEffort quant_e);
- bool checkCompleteFor(Node q);
- void preRegisterQuantifier(Node q);
- void registerQuantifier(Node q);
+ void presolve() override;
+ bool needsCheck(Theory::Effort e) override;
+ void reset_round(Theory::Effort e) override;
+ void check(Theory::Effort e, QEffort quant_e) override;
+ bool checkCompleteFor(Node q) override;
+ void preRegisterQuantifier(Node q) override;
+ void registerQuantifier(Node q) override;
Node explain(TNode n) { return Node::null(); }
/** add user pattern */
void addUserPattern(Node q, Node pat);
void addUserNoPattern(Node q, Node pat);
/** Identify this module */
- std::string identify() const { return "InstEngine"; }
+ std::string identify() const override { return "InstEngine"; }
}; /* class InstantiationEngine */
}/* CVC4::theory::quantifiers namespace */
EqualityQueryQuantifiersEngine(context::Context* c, QuantifiersEngine* qe);
virtual ~EqualityQueryQuantifiersEngine();
/** reset */
- virtual bool reset(Theory::Effort e);
+ bool reset(Theory::Effort e) override;
/* Called for new quantifiers */
- virtual void registerQuantifier(Node q) {}
+ void registerQuantifier(Node q) override {}
/** identify */
- virtual std::string identify() const { return "EqualityQueryQE"; }
+ std::string identify() const override { return "EqualityQueryQE"; }
/** does the equality engine have term a */
- bool hasTerm(Node a);
+ bool hasTerm(Node a) override;
/** get the representative of a */
- Node getRepresentative(Node a);
+ Node getRepresentative(Node a) override;
/** are a and b equal? */
- bool areEqual(Node a, Node b);
+ bool areEqual(Node a, Node b) override;
/** are a and b disequal? */
- bool areDisequal(Node a, Node b);
+ bool areDisequal(Node a, Node b) override;
/** get equality engine
* This may either be the master equality engine or the model's equality
* engine.
*/
- eq::EqualityEngine* getEngine();
+ eq::EqualityEngine* getEngine() override;
/** get list of members in the equivalence class of a */
- void getEquivalenceClass(Node a, std::vector<Node>& eqc);
+ void getEquivalenceClass(Node a, std::vector<Node>& eqc) override;
/** get congruent term
* If possible, returns a term n such that:
* (1) n is a term in the equality engine from getEngine().
* Notice that f should be a "match operator", returned by
* TermDb::getMatchOperator.
*/
- TNode getCongruentTerm(Node f, std::vector<TNode>& args);
+ TNode getCongruentTerm(Node f, std::vector<TNode>& args) override;
/** gets the current best representative in the equivalence
* class of a, based on some heuristic. Currently, the default heuristic
* chooses terms that were previously chosen as representatives
QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {}
virtual ~QRepBoundExt() {}
/** set bound */
- virtual RepSetIterator::RsiEnumType setBound(
- Node owner, unsigned i, std::vector<Node>& elements) override;
+ RepSetIterator::RsiEnumType setBound(Node owner,
+ unsigned i,
+ std::vector<Node>& elements) override;
/** reset index */
- virtual bool resetIndex(RepSetIterator* rsi,
- Node owner,
- unsigned i,
- bool initial,
- std::vector<Node>& elements) override;
+ bool resetIndex(RepSetIterator* rsi,
+ Node owner,
+ unsigned i,
+ bool initial,
+ std::vector<Node>& elements) override;
/** initialize representative set for type */
- virtual bool initializeRepresentativesForType(TypeNode tn) override;
+ bool initializeRepresentativesForType(TypeNode tn) override;
/** get variable order */
- virtual bool getVariableOrder(Node owner,
- std::vector<unsigned>& varOrder) override;
+ bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder) override;
private:
/** quantifiers engine associated with this bound */
public:
FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name);
- FirstOrderModelIG * asFirstOrderModelIG() { return this; }
+ FirstOrderModelIG* asFirstOrderModelIG() override { return this; }
// initialize the model
- void processInitialize( bool ispre );
+ void processInitialize(bool ispre) override;
//for initialize model
- void processInitializeModelForTerm( Node n );
+ void processInitializeModelForTerm(Node n) override;
/** reset evaluation */
void resetEvaluate();
/** evaluate functions */
context::CDO< bool > d_has_range;
context::CDO< int > d_curr_range;
IntBoolMap d_ranges_proxied;
- void initialize();
- void assertNode(Node n);
- Node getNextDecisionRequest();
- bool proxyCurrentRange();
+ void initialize() override;
+ void assertNode(Node n) override;
+ Node getNextDecisionRequest() override;
+ bool proxyCurrentRange() override;
};
private:
//information for minimizing ranges
public:
BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
virtual ~BoundedIntegers();
-
- void presolve();
- bool needsCheck( Theory::Effort e );
- void check(Theory::Effort e, QEffort quant_e);
- void registerQuantifier( Node q );
- void preRegisterQuantifier( Node q );
- void assertNode( Node n );
- Node getNextDecisionRequest( unsigned& priority );
+
+ void presolve() override;
+ bool needsCheck(Theory::Effort e) override;
+ void check(Theory::Effort e, QEffort quant_e) override;
+ void registerQuantifier(Node q) override;
+ void preRegisterQuantifier(Node q) override;
+ void assertNode(Node n) override;
+ Node getNextDecisionRequest(unsigned& priority) override;
bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); }
unsigned getBoundVarType( Node q, Node v );
unsigned getNumBoundVars( Node q ) { return d_set[q].size(); }
bool getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements );
/** Identify this module */
- std::string identify() const { return "BoundedIntegers"; }
+ std::string identify() const override { return "BoundedIntegers"; }
};
}
void debugPrintCond(const char * tr, Node n, bool dispStar = false);
void debugPrint(const char * tr, Node n, bool dispStar = false);
- int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
+ int doExhaustiveInstantiation(FirstOrderModel* fm,
+ Node f,
+ int effort) override;
Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );
- /** process build model */
- bool preProcessBuildModel(TheoryModel* m);
- bool processBuildModel(TheoryModel* m);
+ /** process build model */
+ bool preProcessBuildModel(TheoryModel* m) override;
+ bool processBuildModel(TheoryModel* m) override;
bool useSimpleModels();
};/* class FullModelChecker */
protected:
//quantifiers engine
QuantifiersEngine* d_qe;
- bool preProcessBuildModel(TheoryModel* m); //must call preProcessBuildModelStd
+ // must call preProcessBuildModelStd
+ bool preProcessBuildModel(TheoryModel* m) override;
bool preProcessBuildModelStd(TheoryModel* m);
/** number of lemmas generated while building model */
unsigned d_addedLemmas;
/** exist instantiation ? */
virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
//debug model
- virtual void debugModel( TheoryModel* m );
+ void debugModel(TheoryModel* m) override;
//statistics
unsigned getNumAddedLemmas() { return d_addedLemmas; }
unsigned getNumTriedLemmas() { return d_triedLemmas; }
//whether inst gen was done
bool d_didInstGen;
/** process build model */
- virtual bool processBuildModel( TheoryModel* m );
+ bool processBuildModel(TheoryModel* m) override;
protected:
//reset
// is quantifier active?
bool isQuantifierActive( Node f );
//do exhaustive instantiation
- int doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
+ int doExhaustiveInstantiation(FirstOrderModel* fm,
+ Node f,
+ int effort) override;
//temporary stats
int d_numQuantSat;
ModelEngine( context::Context* c, QuantifiersEngine* qe );
virtual ~ModelEngine();
public:
- bool needsCheck( Theory::Effort e );
- QEffort needsModel(Theory::Effort e);
- void reset_round( Theory::Effort e );
- void check(Theory::Effort e, QEffort quant_e);
- bool checkComplete();
- bool checkCompleteFor( Node q );
- void registerQuantifier( Node f );
- void assertNode( Node f );
- Node explain(TNode n){ return Node::null(); }
- void debugPrint( const char* c );
- /** Identify this module */
- std::string identify() const { return "ModelEngine"; }
+ bool needsCheck(Theory::Effort e) override;
+ QEffort needsModel(Theory::Effort e) override;
+ void reset_round(Theory::Effort e) override;
+ void check(Theory::Effort e, QEffort quant_e) override;
+ bool checkComplete() override;
+ bool checkCompleteFor(Node q) override;
+ void registerQuantifier(Node f) override;
+ void assertNode(Node f) override;
+ Node explain(TNode n) { return Node::null(); }
+ void debugPrint(const char* c);
+ /** Identify this module */
+ std::string identify() const override { return "ModelEngine"; }
};/* class ModelEngine */
}/* CVC4::theory::quantifiers namespace */
~FunDefEngine(){}
/* whether this module needs to check this round */
- bool needsCheck( Theory::Effort e );
+ bool needsCheck(Theory::Effort e) override;
/* reset at a round */
- void reset_round( Theory::Effort e );
+ void reset_round(Theory::Effort e) override;
/* Call during quantifier engine's check */
- void check(Theory::Effort e, QEffort quant_e);
+ void check(Theory::Effort e, QEffort quant_e) override;
/* Called for new quantifiers */
- void registerQuantifier( Node q );
+ void registerQuantifier(Node q) override;
/** called for everything that gets asserted */
- void assertNode( Node n );
+ void assertNode(Node n) override;
/** Identify this module (for debugging, dynamic configuration, etc..) */
- std::string identify() const { return "FunDefEngine"; }
+ std::string identify() const override { return "FunDefEngine"; }
};
EqualityQueryInstProp( QuantifiersEngine* qe );
~EqualityQueryInstProp(){};
/** reset */
- virtual bool reset(Theory::Effort e);
+ bool reset(Theory::Effort e) override;
/* Called for new quantifiers */
- virtual void registerQuantifier(Node q) {}
+ void registerQuantifier(Node q) override {}
/** identify */
- virtual std::string identify() const { return "EqualityQueryInstProp"; }
+ std::string identify() const override { return "EqualityQueryInstProp"; }
/** extends engine */
- bool extendsEngine() { return true; }
+ bool extendsEngine() override { return true; }
/** contains term */
- bool hasTerm( Node a );
+ bool hasTerm(Node a) override;
/** get the representative of the equivalence class of a */
- Node getRepresentative( Node a );
+ Node getRepresentative(Node a) override;
/** returns true if a and b are equal in the current context */
- bool areEqual( Node a, Node b );
+ bool areEqual(Node a, Node b) override;
/** returns true is a and b are disequal in the current context */
- bool areDisequal( Node a, Node b );
+ bool areDisequal(Node a, Node b) override;
/** get the equality engine associated with this query */
- eq::EqualityEngine* getEngine();
+ eq::EqualityEngine* getEngine() override;
/** get the equivalence class of a */
- void getEquivalenceClass( Node a, std::vector< Node >& eqc );
+ void getEquivalenceClass(Node a, std::vector<Node>& eqc) override;
/** get congruent term */
- TNode getCongruentTerm( Node f, std::vector< TNode >& args );
-public:
+ TNode getCongruentTerm(Node f, std::vector<TNode>& args) override;
+
+ public:
/** get the representative of the equivalence class of a, with explanation */
Node getRepresentativeExp( Node a, std::vector< Node >& exp );
/** returns true if a and b are equal in the current context */
InstPropagator& d_ip;
public:
InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {}
- virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
- Node q,
- Node lem,
- std::vector<Node>& terms,
- Node body)
+ bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
+ Node q,
+ Node lem,
+ std::vector<Node>& terms,
+ Node body) override
{
return d_ip.notifyInstantiation( quant_e, q, lem, terms, body );
}
- virtual void filterInstantiations() { d_ip.filterInstantiations(); }
+ void filterInstantiations() override { d_ip.filterInstantiations(); }
};
InstantiationNotifyInstPropagator d_notify;
/** notify instantiation method */
InstPropagator( QuantifiersEngine* qe );
~InstPropagator(){}
/** reset */
- virtual bool reset(Theory::Effort e) override;
+ bool reset(Theory::Effort e) override;
/* Called for new quantifiers */
- virtual void registerQuantifier(Node q) override {}
+ void registerQuantifier(Node q) override {}
/** identify */
- virtual std::string identify() const override { return "InstPropagator"; }
+ std::string identify() const override { return "InstPropagator"; }
/** get the notify mechanism */
InstantiationNotify* getInstantiationNotify() { return &d_notify; }
};
~Instantiate();
/** reset */
- virtual bool reset(Theory::Effort e) override;
+ bool reset(Theory::Effort e) override;
/** register quantifier */
- virtual void registerQuantifier(Node q) override;
+ void registerQuantifier(Node q) override;
/** identify */
- virtual std::string identify() const override { return "Instantiate"; }
+ std::string identify() const override { return "Instantiate"; }
/** check incomplete */
- virtual bool checkComplete() override;
+ bool checkComplete() override;
//--------------------------------------notify objects
/** add instantiation notify
public:
LtePartialInst( QuantifiersEngine * qe, context::Context* c );
/** determine whether this quantified formula will be reduced */
- void preRegisterQuantifier( Node q );
+ void preRegisterQuantifier(Node q) override;
/** was invoked */
bool wasInvoked() { return d_wasInvoked; }
/* whether this module needs to check this round */
- bool needsCheck( Theory::Effort e );
+ bool needsCheck(Theory::Effort e) override;
/* Call during quantifier engine's check */
- void check(Theory::Effort e, QEffort quant_e);
+ void check(Theory::Effort e, QEffort quant_e) override;
/* Called for new quantifiers */
- void registerQuantifier( Node q ) {}
+ void registerQuantifier(Node q) override {}
/* check complete */
- bool checkComplete() { return !d_wasInvoked; }
- void assertNode( Node n ) {}
+ bool checkComplete() override { return !d_wasInvoked; }
+ void assertNode(Node n) override {}
/** Identify this module (for debugging, dynamic configuration, etc..) */
- std::string identify() const { return "LtePartialInst"; }
-
+ std::string identify() const override { return "LtePartialInst"; }
};
}
QuantConflictFind( QuantifiersEngine * qe, context::Context* c );
/** register quantifier */
- void registerQuantifier( Node q );
-public:
+ void registerQuantifier(Node q) override;
+
+ public:
/** assert quantifier */
- void assertNode( Node q );
+ void assertNode(Node q) override;
/** new node */
void newEqClass( Node n );
/** merge */
/** assert disequal */
void assertDisequal( Node a, Node b );
/** needs check */
- bool needsCheck( Theory::Effort level );
+ bool needsCheck(Theory::Effort level) override;
/** reset round */
- void reset_round( Theory::Effort level );
+ void reset_round(Theory::Effort level) override;
/** check */
- void check(Theory::Effort level, QEffort quant_e);
+ void check(Theory::Effort level, QEffort quant_e) override;
private:
bool d_needs_computeRelEqr;
};
Statistics d_statistics;
/** Identify this module */
- std::string identify() const { return "QcfEngine"; }
+ std::string identify() const override { return "QcfEngine"; }
};
std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e);
QuantEqualityEngine& d_qee;
public:
NotifyClass(QuantEqualityEngine& qee): d_qee(qee) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
- bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
- bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
- void eqNotifyConstantTermMerge(TNode t1, TNode t2) { d_qee.conflict(t1, t2); }
- void eqNotifyNewClass(TNode t) { d_qee.eqNotifyNewClass(t); }
- void eqNotifyPreMerge(TNode t1, TNode t2) { d_qee.eqNotifyPreMerge(t1, t2); }
- void eqNotifyPostMerge(TNode t1, TNode t2) { d_qee.eqNotifyPostMerge(t1, t2); }
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {d_qee.eqNotifyDisequal(t1, t2, reason); }
+ bool eqNotifyTriggerEquality(TNode equality, bool value) override
+ {
+ return true;
+ }
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+ {
+ return true;
+ }
+ bool eqNotifyTriggerTermEquality(TheoryId tag,
+ TNode t1,
+ TNode t2,
+ bool value) override
+ {
+ return true;
+ }
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
+ {
+ d_qee.conflict(t1, t2);
+ }
+ void eqNotifyNewClass(TNode t) override { d_qee.eqNotifyNewClass(t); }
+ void eqNotifyPreMerge(TNode t1, TNode t2) override
+ {
+ d_qee.eqNotifyPreMerge(t1, t2);
+ }
+ void eqNotifyPostMerge(TNode t1, TNode t2) override
+ {
+ d_qee.eqNotifyPostMerge(t1, t2);
+ }
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
+ {
+ d_qee.eqNotifyDisequal(t1, t2, reason);
+ }
};/* class ConjectureGenerator::NotifyClass */
/** The notify class */
NotifyClass d_notify;
QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c );
/* whether this module needs to check this round */
- bool needsCheck( Theory::Effort e );
+ bool needsCheck(Theory::Effort e) override;
/* reset at a round */
- void reset_round( Theory::Effort e );
+ void reset_round(Theory::Effort e) override;
/* Call during quantifier engine's check */
- void check(Theory::Effort e, QEffort quant_e);
+ void check(Theory::Effort e, QEffort quant_e) override;
/* Called for new quantifiers */
- void registerQuantifier( Node q );
+ void registerQuantifier(Node q) override;
/** called for everything that gets asserted */
- void assertNode( Node n );
+ void assertNode(Node n) override;
/** Identify this module (for debugging, dynamic configuration, etc..) */
- std::string identify() const { return "QuantEqualityEngine"; }
+ std::string identify() const override { return "QuantEqualityEngine"; }
/** queries */
bool areUnivDisequal( TNode n1, TNode n2 );
bool areUnivEqual( TNode n1, TNode n2 );
QuantRelevance(bool cr) : d_computeRel(cr) {}
~QuantRelevance() {}
/** reset */
- virtual bool reset(Theory::Effort e) override { return true; }
+ bool reset(Theory::Effort e) override { return true; }
/** register quantifier */
- virtual void registerQuantifier(Node q) override;
+ void registerQuantifier(Node q) override;
/** identify */
- virtual std::string identify() const override { return "QuantRelevance"; }
+ std::string identify() const override { return "QuantRelevance"; }
/** set relevance of symbol s to r */
void setRelevance(Node s, int r);
/** get relevance of symbol s */
public:
QuantDSplit( QuantifiersEngine * qe, context::Context* c );
/** determine whether this quantified formula will be reduced */
- void preRegisterQuantifier( Node q );
-
+ void preRegisterQuantifier(Node q) override;
+
/* whether this module needs to check this round */
- bool needsCheck( Theory::Effort e );
+ bool needsCheck(Theory::Effort e) override;
/* Call during quantifier engine's check */
- void check(Theory::Effort e, QEffort quant_e);
+ void check(Theory::Effort e, QEffort quant_e) override;
/* Called for new quantifiers */
- void registerQuantifier( Node q ) {}
- void assertNode( Node n ) {}
- bool checkCompleteFor( Node q );
+ void registerQuantifier(Node q) override {}
+ void assertNode(Node n) override {}
+ bool checkCompleteFor(Node q) override;
/** Identify this module (for debugging, dynamic configuration, etc..) */
- std::string identify() const { return "QuantDSplit"; }
+ std::string identify() const override { return "QuantDSplit"; }
};
}
RelevantDomain(QuantifiersEngine* qe);
virtual ~RelevantDomain();
/** Reset. */
- virtual bool reset(Theory::Effort e) override;
+ bool reset(Theory::Effort e) override;
/** Register the quantified formula q */
- virtual void registerQuantifier(Node q) override;
+ void registerQuantifier(Node q) override;
/** identify */
- virtual std::string identify() const override { return "RelevantDomain"; }
+ std::string identify() const override { return "RelevantDomain"; }
/** Compute the relevant domain */
void compute();
/** Relevant domain representation.
public:
RewriteEngine( context::Context* c, QuantifiersEngine* qe );
- bool needsCheck( Theory::Effort e );
- void check(Theory::Effort e, QEffort quant_e);
- void registerQuantifier( Node f );
- void assertNode( Node n );
- bool checkCompleteFor( Node q );
+ bool needsCheck(Theory::Effort e) override;
+ void check(Theory::Effort e, QEffort quant_e) override;
+ void registerQuantifier(Node f) override;
+ void assertNode(Node n) override;
+ bool checkCompleteFor(Node q) override;
/** Identify this module */
- std::string identify() const { return "RewriteEngine"; }
+ std::string identify() const override { return "RewriteEngine"; }
};
}
CegInstantiation( QuantifiersEngine * qe, context::Context* c );
~CegInstantiation();
public:
- bool needsCheck( Theory::Effort e );
- QEffort needsModel(Theory::Effort e);
- /* Call during quantifier engine's check */
- void check(Theory::Effort e, QEffort quant_e);
- /* Called for new quantifiers */
- void registerQuantifier( Node q );
- /** get the next decision request */
- Node getNextDecisionRequest( unsigned& priority );
- /** Identify this module (for debugging, dynamic configuration, etc..) */
- std::string identify() const { return "CegInstantiation"; }
- /** print solution for synthesis conjectures */
- void printSynthSolution( std::ostream& out );
- /** get synth solutions
- *
- * This function adds entries to sol_map that map functions-to-synthesize
- * with their solutions, for all active conjectures (currently just the one
- * assigned to d_conj). This should be called immediately after the solver
- * answers unsat for sygus input.
- *
- * For details on what is added to sol_map, see
- * CegConjecture::getSynthSolutions.
- */
- void getSynthSolutions(std::map<Node, Node>& sol_map);
- /** preregister assertion (before rewrite) */
- void preregisterAssertion( Node n );
+ bool needsCheck(Theory::Effort e) override;
+ QEffort needsModel(Theory::Effort e) override;
+ /* Call during quantifier engine's check */
+ void check(Theory::Effort e, QEffort quant_e) override;
+ /* Called for new quantifiers */
+ void registerQuantifier(Node q) override;
+ /** get the next decision request */
+ Node getNextDecisionRequest(unsigned& priority) override;
+ /** Identify this module (for debugging, dynamic configuration, etc..) */
+ std::string identify() const override { return "CegInstantiation"; }
+ /** print solution for synthesis conjectures */
+ void printSynthSolution(std::ostream& out);
+ /** get synth solutions
+ *
+ * This function adds entries to sol_map that map functions-to-synthesize
+ * with their solutions, for all active conjectures (currently just the one
+ * assigned to d_conj). This should be called immediately after the solver
+ * answers unsat for sygus input.
+ *
+ * For details on what is added to sol_map, see
+ * CegConjecture::getSynthSolutions.
+ */
+ void getSynthSolutions(std::map<Node, Node>& sol_map);
+ /** preregister assertion (before rewrite) */
+ void preregisterAssertion(Node n);
public:
class Statistics {
public:
CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){}
virtual ~CegqiOutputSingleInv() {}
CegConjectureSingleInv * d_out;
- bool doAddInstantiation( std::vector< Node >& subs );
- bool isEligibleForInstantiation( Node n );
- bool addLemma( Node lem );
+ bool doAddInstantiation(std::vector<Node>& subs) override;
+ bool isEligibleForInstantiation(Node n) override;
+ bool addLemma(Node lem) override;
};
class DetTrace {
protected:
/** does d_conj{ d_var -> nvn } still rewrite to d_result? */
- bool invariant(TermDbSygus* tds, Node nvn, Node x);
+ bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
private:
/** the formula we are evaluating */
protected:
/** checks whether the analog of nvn still rewrites to d_bvr */
- bool invariant(TermDbSygus* tds, Node nvn, Node x);
+ bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
private:
/** the conjecture associated with the enumerator d_enum */
protected:
/** checks whether nvn involves division by zero. */
- bool invariant(TermDbSygus* tds, Node nvn, Node x);
+ bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
};
/** NegContainsSygusInvarianceTest
protected:
/** checks if contains( out_i, nvn[in_i] ) --> false for some I/O pair i. */
- bool invariant(TermDbSygus* tds, Node nvn, Node x);
+ bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
private:
/** The enumerator whose value we are considering in this invariance test */
std::vector<Node>& vars,
std::vector<Node>& pt);
/** evaluate n on sample point index */
- Node evaluate(Node n, unsigned index);
+ Node evaluate(Node n, unsigned index) override;
/**
* Returns the index of a sample point such that the evaluation of a and b
* diverge, or -1 if no such sample point exists.
* from the set of all previous input/output pairs based on the
* d_drewrite utility.
*/
- virtual Node registerTerm(Node n, bool forceKeep = false) override;
+ Node registerTerm(Node n, bool forceKeep = false) override;
private:
/** dynamic rewriter class */
/** presolve (called once per user check-sat) */
void presolve();
/** reset (calculate which terms are active) */
- virtual bool reset(Theory::Effort effort) override;
+ bool reset(Theory::Effort effort) override;
/** register quantified formula */
- virtual void registerQuantifier(Node q) override;
+ void registerQuantifier(Node q) override;
/** identify */
- virtual std::string identify() const override { return "TermDb"; }
+ std::string identify() const override { return "TermDb"; }
/** get number of operators */
unsigned getNumOperators();
/** get operator at index i */
Node d_one;
/** reset */
- virtual bool reset(Theory::Effort e) override { return true; }
+ bool reset(Theory::Effort e) override { return true; }
/** register quantifier */
- virtual void registerQuantifier(Node q) override;
+ void registerQuantifier(Node q) override;
/** identify */
- virtual std::string identify() const override { return "TermUtil"; }
+ std::string identify() const override { return "TermUtil"; }
// for inst constant
private:
/** map from universal quantifiers to the list of variables */
public:
NotifyClass(TheorySep& sep) : d_sep(sep) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value)
+ bool eqNotifyTriggerEquality(TNode equality, bool value) override
{
Debug("sep::propagate")
<< "NotifyClass::eqNotifyTriggerEquality(" << equality << ", "
}
}
- bool eqNotifyTriggerPredicate(TNode predicate, bool value)
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
{
Unreachable();
}
bool eqNotifyTriggerTermEquality(TheoryId tag,
TNode t1,
TNode t2,
- bool value)
+ bool value) override
{
Debug("sep::propagate")
<< "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2
return true;
}
- void eqNotifyConstantTermMerge(TNode t1, TNode t2)
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
{
Debug("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1
<< ", " << t2 << ")" << std::endl;
d_sep.conflict(t1, t2);
}
- void eqNotifyNewClass(TNode t) {}
- void eqNotifyPreMerge(TNode t1, TNode t2)
+ void eqNotifyNewClass(TNode t) override {}
+ void eqNotifyPreMerge(TNode t1, TNode t2) override
{
d_sep.eqNotifyPreMerge(t1, t2);
}
- void eqNotifyPostMerge(TNode t1, TNode t2)
+ void eqNotifyPostMerge(TNode t1, TNode t2) override
{
d_sep.eqNotifyPostMerge(t1, t2);
}
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {}
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
};
/** The notify class for d_equalityEngine */
public:
NotifyClass(TheorySetsPrivate& theory): d_theory(theory) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value);
- bool eqNotifyTriggerPredicate(TNode predicate, bool value);
- bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
- void eqNotifyConstantTermMerge(TNode t1, TNode t2);
- void eqNotifyNewClass(TNode t);
- void eqNotifyPreMerge(TNode t1, TNode t2);
- void eqNotifyPostMerge(TNode t1, TNode t2);
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+ bool eqNotifyTriggerEquality(TNode equality, bool value) override;
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) override;
+ bool eqNotifyTriggerTermEquality(TheoryId tag,
+ TNode t1,
+ TNode t2,
+ bool value) override;
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) override;
+ void eqNotifyNewClass(TNode t) override;
+ void eqNotifyPreMerge(TNode t1, TNode t2) override;
+ void eqNotifyPostMerge(TNode t1, TNode t2) override;
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
} d_notify;
/** Equality engine */
SharedTermsDatabase& d_sharedTerms;
public:
EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) {
+ bool eqNotifyTriggerEquality(TNode equality, bool value) override
+ {
d_sharedTerms.propagateEquality(equality, value);
return true;
}
- bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+ {
Unreachable();
return true;
}
- bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) {
+ bool eqNotifyTriggerTermEquality(theory::TheoryId tag,
+ TNode t1,
+ TNode t2,
+ bool value) override
+ {
return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value);
}
- void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
+ {
d_sharedTerms.conflict(t1, t2, true);
}
- void eqNotifyNewClass(TNode t) { }
- void eqNotifyPreMerge(TNode t1, TNode t2) { }
- void eqNotifyPostMerge(TNode t1, TNode t2) { }
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
+ void eqNotifyNewClass(TNode t) override {}
+ void eqNotifyPreMerge(TNode t1, TNode t2) override {}
+ void eqNotifyPostMerge(TNode t1, TNode t2) override {}
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
};
/** The notify class for d_equalityEngine */
/**
* This method gets called on backtracks from the context manager.
*/
- void contextNotifyPop() {
- backtrack();
- }
+ void contextNotifyPop() override { backtrack(); }
};
}
TheoryStrings& d_str;
public:
NotifyClass(TheoryStrings& t_str): d_str(t_str) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) {
+ bool eqNotifyTriggerEquality(TNode equality, bool value) override
+ {
Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
if (value) {
return d_str.propagate(equality);
return d_str.propagate(equality.notNode());
}
}
- bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+ {
Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
if (value) {
return d_str.propagate(predicate);
return d_str.propagate(predicate.notNode());
}
}
- bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
+ bool eqNotifyTriggerTermEquality(TheoryId tag,
+ TNode t1,
+ TNode t2,
+ bool value) override
+ {
Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
if (value) {
return d_str.propagate(t1.eqNode(t2));
return d_str.propagate(t1.eqNode(t2).notNode());
}
}
- void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
+ {
Debug("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
d_str.conflict(t1, t2);
}
- void eqNotifyNewClass(TNode t) {
+ void eqNotifyNewClass(TNode t) override
+ {
Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl;
d_str.eqNotifyNewClass(t);
}
- void eqNotifyPreMerge(TNode t1, TNode t2) {
+ void eqNotifyPreMerge(TNode t1, TNode t2) override
+ {
Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl;
d_str.eqNotifyPreMerge(t1, t2);
}
- void eqNotifyPostMerge(TNode t1, TNode t2) {
+ void eqNotifyPostMerge(TNode t1, TNode t2) override
+ {
Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl;
d_str.eqNotifyPostMerge(t1, t2);
}
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
+ {
Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl;
d_str.eqNotifyDisequal(t1, t2, reason);
}
class CacheInvalidator : public context::ContextNotifyObj {
bool& d_cacheInvalidated;
protected:
- void contextNotifyPop() {
- d_cacheInvalidated = true;
- }
+ void contextNotifyPop() override { d_cacheInvalidated = true; }
+
public:
CacheInvalidator(context::Context* context, bool& cacheInvalidated) :
context::ContextNotifyObj(context),
TheoryEngine& d_te;
public:
NotifyClass(TheoryEngine& te): d_te(te) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
- bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
- bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
- void eqNotifyConstantTermMerge(TNode t1, TNode t2) {}
- void eqNotifyNewClass(TNode t) { d_te.eqNotifyNewClass(t); }
- void eqNotifyPreMerge(TNode t1, TNode t2) { d_te.eqNotifyPreMerge(t1, t2); }
- void eqNotifyPostMerge(TNode t1, TNode t2) { d_te.eqNotifyPostMerge(t1, t2); }
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { d_te.eqNotifyDisequal(t1, t2, reason); }
+ bool eqNotifyTriggerEquality(TNode equality, bool value) override
+ {
+ return true;
+ }
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+ {
+ return true;
+ }
+ bool eqNotifyTriggerTermEquality(theory::TheoryId tag,
+ TNode t1,
+ TNode t2,
+ bool value) override
+ {
+ return true;
+ }
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
+ void eqNotifyNewClass(TNode t) override { d_te.eqNotifyNewClass(t); }
+ void eqNotifyPreMerge(TNode t1, TNode t2) override
+ {
+ d_te.eqNotifyPreMerge(t1, t2);
+ }
+ void eqNotifyPostMerge(TNode t1, TNode t2) override
+ {
+ d_te.eqNotifyPostMerge(t1, t2);
+ }
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
+ {
+ d_te.eqNotifyDisequal(t1, t2, reason);
+ }
};/* class TheoryEngine::NotifyClass */
NotifyClass d_masterEENotify;
* builder in steps (2) or (5), for instance, if the model we
* are building fails to satisfy a quantified formula.
*/
- virtual bool buildModel(Model* m) override;
+ bool buildModel(Model* m) override;
/** Debug check model.
*
* This throws an assertion failure if the model
TheoryRegistrar(TheoryEngine* te) : d_theoryEngine(te) { }
- void preRegister(Node n) {
- d_theoryEngine->preRegister(n);
- }
+ void preRegister(Node n) override { d_theoryEngine->preRegister(n); }
};/* class TheoryRegistrar */
TypeEnumeratorInterface(type) {
}
- TypeEnumeratorInterface* clone() const { return new T(static_cast<const T&>(*this)); }
+ TypeEnumeratorInterface* clone() const override
+ {
+ return new T(static_cast<const T&>(*this));
+ }
};/* class TypeEnumeratorBase */
*/
class EqualityEngineNotifyNone : public EqualityEngineNotify {
public:
- bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
- bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
- bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
- void eqNotifyConstantTermMerge(TNode t1, TNode t2) { }
- void eqNotifyNewClass(TNode t) { }
- void eqNotifyPreMerge(TNode t1, TNode t2) { }
- void eqNotifyPostMerge(TNode t1, TNode t2) { }
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
+ bool eqNotifyTriggerEquality(TNode equality, bool value) override
+ {
+ return true;
+ }
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+ {
+ return true;
+ }
+ bool eqNotifyTriggerTermEquality(TheoryId tag,
+ TNode t1,
+ TNode t2,
+ bool value) override
+ {
+ return true;
+ }
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {}
+ void eqNotifyNewClass(TNode t) override {}
+ void eqNotifyPreMerge(TNode t1, TNode t2) override {}
+ void eqNotifyPostMerge(TNode t1, TNode t2) override {}
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
};/* class EqualityEngineNotifyNone */
/**
/**
* This method gets called on backtracks from the context manager.
*/
- void contextNotifyPop() {
- backtrack();
- }
+ void contextNotifyPop() override { backtrack(); }
/**
* Constructor initialization stuff.
public:
NotifyClass(TheoryUF& uf): d_uf(uf) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) {
+ bool eqNotifyTriggerEquality(TNode equality, bool value) override
+ {
Debug("uf") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
if (value) {
return d_uf.propagate(equality);
}
}
- bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
+ {
Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
if (value) {
return d_uf.propagate(predicate);
}
}
- bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
+ bool eqNotifyTriggerTermEquality(TheoryId tag,
+ TNode t1,
+ TNode t2,
+ bool value) override
+ {
Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
if (value) {
return d_uf.propagate(t1.eqNode(t2));
}
}
- void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
+ {
Debug("uf-notify") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
d_uf.conflict(t1, t2);
}
- void eqNotifyNewClass(TNode t) {
+ void eqNotifyNewClass(TNode t) override
+ {
Debug("uf-notify") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl;
d_uf.eqNotifyNewClass(t);
}
- void eqNotifyPreMerge(TNode t1, TNode t2) {
+ void eqNotifyPreMerge(TNode t1, TNode t2) override
+ {
Debug("uf-notify") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl;
d_uf.eqNotifyPreMerge(t1, t2);
}
- void eqNotifyPostMerge(TNode t1, TNode t2) {
+ void eqNotifyPostMerge(TNode t1, TNode t2) override
+ {
Debug("uf-notify") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl;
d_uf.eqNotifyPostMerge(t1, t2);
}
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override
+ {
Debug("uf-notify") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl;
d_uf.eqNotifyDisequal(t1, t2, reason);
}
virtual const T& getDataRef() const = 0;
/** Flush the value of the statistic to the given output stream. */
- void flushInformation(std::ostream& out) const {
+ void flushInformation(std::ostream& out) const override
+ {
if(__CVC4_USE_STATISTICS) {
out << getData();
}
}
- virtual void safeFlushInformation(int fd) const {
+ void safeFlushInformation(int fd) const override
+ {
if (__CVC4_USE_STATISTICS) {
safe_print<T>(fd, getDataRef());
}
}
- SExpr getValue() const {
- return mkSExpr(getData());
- }
+ SExpr getValue() const override { return mkSExpr(getData()); }
};/* class ReadOnlyDataStat<T> */
}
/** Set this reference statistic to refer to the given data cell. */
- void setData(const T& t) {
+ void setData(const T& t) override
+ {
if(__CVC4_USE_STATISTICS) {
d_data = &t;
}
}
/** Get the value of the referenced data cell. */
- virtual T getData() const { return *d_data; }
+ T getData() const override { return *d_data; }
/** Get a reference to the value of the referenced data cell. */
- virtual const T& getDataRef() const { return *d_data; }
+ const T& getDataRef() const override { return *d_data; }
};/* class ReferenceStat<T> */
}
/** Set the underlying data value to the given value. */
- void setData(const T& t) {
+ void setData(const T& t) override
+ {
if(__CVC4_USE_STATISTICS) {
d_data = t;
}
}
/** Get the underlying data value. */
- virtual T getData() const { return d_data; }
+ T getData() const override { return d_data; }
/** Get a reference to the underlying data value. */
- virtual const T& getDataRef() const { return d_data; }
+ const T& getDataRef() const override { return d_data; }
};/* class BackedStat<T> */
}
/** Get the data of the underlying (wrapped) statistic. */
- virtual T getData() const { return d_stat.getData(); }
+ T getData() const override { return d_stat.getData(); }
/** Get a reference to the data of the underlying (wrapped) statistic. */
- virtual const T& getDataRef() const { return d_stat.getDataRef(); }
+ const T& getDataRef() const override { return d_stat.getDataRef(); }
- virtual void safeFlushInformation(int fd) const {
+ void safeFlushInformation(int fd) const override
+ {
// ReadOnlyDataStat uses getDataRef() to get the information to print,
// which might not be appropriate for all wrapped statistics. Delegate the
// printing to the wrapped statistic instead.
d_stat.safeFlushInformation(fd);
}
- SExpr getValue() const {
- return d_stat.getValue();
- }
+ SExpr getValue() const override { return d_stat.getValue(); }
};/* class WrappedStat<T> */
}
}
- SExpr getValue() const {
- return SExpr(Integer(d_data));
- }
+ SExpr getValue() const override { return SExpr(Integer(d_data)); }
};/* class IntStat */
Stat(name), d_sized(sized) {}
~SizeStat() {}
- void flushInformation(std::ostream& out) const {
+ void flushInformation(std::ostream& out) const override
+ {
out << d_sized.size();
}
- void safeFlushInformation(int fd) const {
+ void safeFlushInformation(int fd) const override
+ {
safe_print<uint64_t>(fd, d_sized.size());
}
- SExpr getValue() const {
- return SExpr(Integer(d_sized.size()));
- }
+ SExpr getValue() const override { return SExpr(Integer(d_sized.size())); }
};/* class SizeStat */
}
}
- SExpr getValue() const {
+ SExpr getValue() const override
+ {
std::stringstream ss;
ss << std::fixed << std::setprecision(8) << d_data;
return SExpr(Rational::fromDecimal(ss.str()));
SExprStat(const std::string& name, const SExpr& init) :
Stat(name), d_data(init){}
- virtual void flushInformation(std::ostream& out) const {
+ void flushInformation(std::ostream& out) const override
+ {
out << d_data << std::endl;
}
- virtual void safeFlushInformation(int fd) const {
+ void safeFlushInformation(int fd) const override
+ {
// SExprStat is only used in statistics.cpp in copyFrom, which we cannot
// do in a signal handler anyway.
safe_print(fd, "<unsupported>");
}
- SExpr getValue() const {
- return d_data;
- }
+ SExpr getValue() const override { return d_data; }
};/* class SExprStat */
HistogramStat(const std::string& name) : Stat(name) {}
~HistogramStat() {}
- void flushInformation(std::ostream& out) const{
+ void flushInformation(std::ostream& out) const override
+ {
if(__CVC4_USE_STATISTICS) {
typename Histogram::const_iterator i = d_hist.begin();
typename Histogram::const_iterator end = d_hist.end();
}
}
- virtual void safeFlushInformation(int fd) const {
+ void safeFlushInformation(int fd) const override
+ {
if (__CVC4_USE_STATISTICS) {
typename Histogram::const_iterator i = d_hist.begin();
typename Histogram::const_iterator end = d_hist.end();
* Set the name of this statistic registry, used as prefix during
* output. (This version overrides StatisticsBase::setPrefix().)
*/
- void setPrefix(const std::string& name) {
- d_prefix = d_name = name;
- }
+ void setPrefix(const std::string& name) override { d_prefix = d_name = name; }
/** Overridden to avoid the name being printed */
- void flushStat(std::ostream &out) const;
+ void flushStat(std::ostream& out) const override;
- virtual void flushInformation(std::ostream& out) const;
+ void flushInformation(std::ostream& out) const override;
- virtual void safeFlushInformation(int fd) const;
+ void safeFlushInformation(int fd) const override;
- SExpr getValue() const {
+ SExpr getValue() const override
+ {
std::vector<SExpr> v;
for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
std::vector<SExpr> w;
/** If the timer is currently running */
bool running() const;
- virtual timespec getData() const;
+ timespec getData() const override;
- virtual void safeFlushInformation(int fd) const {
+ void safeFlushInformation(int fd) const override
+ {
// Overwrite the implementation in the superclass because we cannot use
// getDataRef(): it might return stale data if the timer is currently
// running.
safe_print<timespec>(fd, data);
}
- SExpr getValue() const;
+ SExpr getValue() const override;
};/* class TimerStat */
projects / cvc5.git / commitdiff