diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 56 | ||||
-rw-r--r-- | src/theory/bv/bv_inequality_graph.h | 8 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.h | 25 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.h | 16 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.h | 37 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.h | 18 | ||||
-rw-r--r-- | src/theory/bv/type_enumerator.h | 7 |
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 */ |