summaryrefslogtreecommitdiff
path: root/src/theory/bv
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv')
-rw-r--r--src/theory/bv/bitblaster_template.h56
-rw-r--r--src/theory/bv/bv_inequality_graph.h8
-rw-r--r--src/theory/bv/bv_subtheory_algebraic.h25
-rw-r--r--src/theory/bv/bv_subtheory_bitblast.h16
-rw-r--r--src/theory/bv/bv_subtheory_core.h37
-rw-r--r--src/theory/bv/bv_subtheory_inequality.h18
-rw-r--r--src/theory/bv/type_enumerator.h7
7 files changed, 89 insertions, 78 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 1dc2d8b1e..3bb701fdf 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -169,15 +169,15 @@ class TLazyBitblaster : public TBitblaster<Node> {
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();
@@ -219,7 +219,7 @@ public:
*
* @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);
@@ -274,7 +274,7 @@ class EagerBitblaster : public TBitblaster<Node> {
// 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:
@@ -282,14 +282,14 @@ 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();
@@ -303,7 +303,7 @@ public:
BitblastingRegistrar(EagerBitblaster* bb)
: d_bitblaster(bb)
{}
- void preRegister(Node n);
+ void preRegister(Node n) override;
}; /* class Registrar */
class AigBitblaster : public TBitblaster<Abc_Obj_t*> {
@@ -322,9 +322,9 @@ 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);
@@ -332,14 +332,18 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> {
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();
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 30270b3c3..deba84631 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -201,11 +201,9 @@ class InequalityGraph : public context::ContextNotifyObj{
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();
diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index 0534c0f17..c963f15d7 100644
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -224,16 +224,19 @@ public:
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
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 5927feddc..f88810fca 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -65,17 +65,17 @@ public:
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 */
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 6cc6253ff..05c9535c3 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -53,14 +53,17 @@ class CoreSolver : public SubtheorySolver {
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 {}
};
@@ -100,17 +103,19 @@ class CoreSolver : public SubtheorySolver {
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;
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index be0492125..620cd075b 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -65,15 +65,15 @@ public:
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;
};
}
diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
index 718121499..dd65fc08f 100644
--- a/src/theory/bv/type_enumerator.h
+++ b/src/theory/bv/type_enumerator.h
@@ -42,20 +42,21 @@ public:
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback