diff options
Diffstat (limited to 'src/theory/bv/bitblaster_template.h')
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 56 |
1 files changed, 30 insertions, 26 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(); |