diff options
Diffstat (limited to 'src/theory/bv')
| -rw-r--r-- | src/theory/bv/aig_bitblaster.cpp | 6 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv.h | 43 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h | 54 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 22 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 10 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv_utils.cpp | 663 | ||||
| -rw-r--r-- | src/theory/bv/theory_bv_utils.h | 661 |
7 files changed, 824 insertions, 635 deletions
diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp index 5459340f6..010eaf4e5 100644 --- a/src/theory/bv/aig_bitblaster.cpp +++ b/src/theory/bv/aig_bitblaster.cpp @@ -15,7 +15,10 @@ **/ #include "bitblaster_template.h" + #include "cvc4_private.h" + +#include "base/cvc4_check.h" #include "options/bv_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" @@ -155,8 +158,7 @@ AigBitblaster::AigBitblaster() d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(), "AigBitblaster"); break; - default: - Unreachable("Unknown SAT solver type"); + default: CVC4_FATAL() << "Unknown SAT solver type"; } } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 8cefe03b2..1992c0ae3 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -64,40 +64,43 @@ public: ~TheoryBV(); - void setMasterEqualityEngine(eq::EqualityEngine* eq); + void setMasterEqualityEngine(eq::EqualityEngine* eq) override; - Node expandDefinition(LogicRequest &logicRequest, Node node); + Node expandDefinition(LogicRequest& logicRequest, Node node) override; void mkAckermanizationAssertions(std::vector<Node>& assertions); - void preRegisterTerm(TNode n); + void preRegisterTerm(TNode n) override; - void check(Effort e); - - bool needsCheckLastEffort(); + void check(Effort e) override; + + bool needsCheckLastEffort() override; - void propagate(Effort e); + void propagate(Effort e) override; - Node explain(TNode n); + Node explain(TNode n) override; bool collectModelInfo(TheoryModel* m) override; - std::string identify() const { return std::string("TheoryBV"); } + std::string identify() const override { return std::string("TheoryBV"); } /** equality engine */ - eq::EqualityEngine * getEqualityEngine(); - bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ); - int getReduction( int effort, Node n, Node& nr ); - - PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); + eq::EqualityEngine* getEqualityEngine() override; + bool getCurrentSubstitution(int effort, + std::vector<Node>& vars, + std::vector<Node>& subs, + std::map<Node, std::vector<Node> >& exp) override; + int getReduction(int effort, Node n, Node& nr) override; + + PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; void enableCoreTheorySlicer(); - Node ppRewrite(TNode t); + Node ppRewrite(TNode t) override; - void ppStaticLearn(TNode in, NodeBuilder<>& learned); + void ppStaticLearn(TNode in, NodeBuilder<>& learned) override; - void presolve(); + void presolve() override; bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); @@ -206,13 +209,13 @@ private: */ void explain(TNode literal, std::vector<TNode>& assumptions); - void addSharedTerm(TNode t); + void addSharedTerm(TNode t) override; bool isSharedTerm(TNode t) { return d_sharedTermsSet.contains(t); } - EqualityStatus getEqualityStatus(TNode a, TNode b); + EqualityStatus getEqualityStatus(TNode a, TNode b) override; - Node getModelValue(TNode var); + Node getModelValue(TNode var) override; inline std::string indent() { diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index b53f7bb08..503fe5157 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -31,7 +31,7 @@ bool RewriteRule<EvalAnd>::applies(TNode node) { Unreachable(); return (node.getKind() == kind::BITVECTOR_AND && node.getNumChildren() == 2 && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -50,7 +50,7 @@ bool RewriteRule<EvalOr>::applies(TNode node) { Unreachable(); return (node.getKind() == kind::BITVECTOR_OR && node.getNumChildren() == 2 && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -69,7 +69,7 @@ bool RewriteRule<EvalXor>::applies(TNode node) { Unreachable(); return (node.getKind() == kind::BITVECTOR_XOR && node.getNumChildren() == 2 && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -86,7 +86,7 @@ Node RewriteRule<EvalXor>::apply(TNode node) { // template<> inline // bool RewriteRule<EvalXnor>::applies(TNode node) { // return (node.getKind() == kind::BITVECTOR_XNOR && -// utils::isBVGroundTerm(node)); +// utils::isBvConstTerm(node)); // } // template<> inline @@ -101,7 +101,7 @@ Node RewriteRule<EvalXor>::apply(TNode node) { template<> inline bool RewriteRule<EvalNot>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_NOT && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -115,7 +115,7 @@ Node RewriteRule<EvalNot>::apply(TNode node) { // template<> inline // bool RewriteRule<EvalComp>::applies(TNode node) { // return (node.getKind() == kind::BITVECTOR_COMP && -// utils::isBVGroundTerm(node)); +// utils::isBvConstTerm(node)); // } // template<> inline @@ -136,7 +136,7 @@ Node RewriteRule<EvalNot>::apply(TNode node) { template<> inline bool RewriteRule<EvalMult>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_MULT && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -153,7 +153,7 @@ Node RewriteRule<EvalMult>::apply(TNode node) { template<> inline bool RewriteRule<EvalPlus>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_PLUS && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -170,7 +170,7 @@ Node RewriteRule<EvalPlus>::apply(TNode node) { // template<> inline // bool RewriteRule<EvalSub>::applies(TNode node) { // return (node.getKind() == kind::BITVECTOR_SUB && -// utils::isBVGroundTerm(node)); +// utils::isBvConstTerm(node)); // } // template<> inline @@ -185,7 +185,7 @@ Node RewriteRule<EvalPlus>::apply(TNode node) { template<> inline bool RewriteRule<EvalNeg>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_NEG && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -198,7 +198,7 @@ Node RewriteRule<EvalNeg>::apply(TNode node) { } template<> inline bool RewriteRule<EvalUdiv>::applies(TNode node) { - return (utils::isBVGroundTerm(node) && + return (utils::isBvConstTerm(node) && (node.getKind() == kind::BITVECTOR_UDIV_TOTAL || (node.getKind() == kind::BITVECTOR_UDIV && node[1].isConst()))); } @@ -214,7 +214,7 @@ Node RewriteRule<EvalUdiv>::apply(TNode node) { } template<> inline bool RewriteRule<EvalUrem>::applies(TNode node) { - return (utils::isBVGroundTerm(node) && + return (utils::isBvConstTerm(node) && (node.getKind() == kind::BITVECTOR_UREM_TOTAL || (node.getKind() == kind::BITVECTOR_UREM && node[1].isConst()))); } @@ -231,7 +231,7 @@ Node RewriteRule<EvalUrem>::apply(TNode node) { template<> inline bool RewriteRule<EvalShl>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SHL && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -247,7 +247,7 @@ Node RewriteRule<EvalShl>::apply(TNode node) { template<> inline bool RewriteRule<EvalLshr>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_LSHR && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -263,7 +263,7 @@ Node RewriteRule<EvalLshr>::apply(TNode node) { template<> inline bool RewriteRule<EvalAshr>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_ASHR && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -279,7 +279,7 @@ Node RewriteRule<EvalAshr>::apply(TNode node) { template<> inline bool RewriteRule<EvalUlt>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_ULT && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -297,7 +297,7 @@ Node RewriteRule<EvalUlt>::apply(TNode node) { template<> inline bool RewriteRule<EvalUltBv>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_ULTBV && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -315,7 +315,7 @@ Node RewriteRule<EvalUltBv>::apply(TNode node) { template<> inline bool RewriteRule<EvalSlt>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SLT && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -334,7 +334,7 @@ Node RewriteRule<EvalSlt>::apply(TNode node) { template<> inline bool RewriteRule<EvalSltBv>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SLTBV && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -354,7 +354,7 @@ template<> inline bool RewriteRule<EvalITEBv>::applies(TNode node) { Debug("bv-rewrite") << "RewriteRule<EvalITEBv>::applies(" << node << ")" << std::endl; return (node.getKind() == kind::BITVECTOR_ITE && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -373,7 +373,7 @@ Node RewriteRule<EvalITEBv>::apply(TNode node) { template<> inline bool RewriteRule<EvalUle>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_ULE && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -391,7 +391,7 @@ Node RewriteRule<EvalUle>::apply(TNode node) { template<> inline bool RewriteRule<EvalSle>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SLE && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -409,7 +409,7 @@ Node RewriteRule<EvalSle>::apply(TNode node) { template<> inline bool RewriteRule<EvalExtract>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_EXTRACT && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -427,7 +427,7 @@ Node RewriteRule<EvalExtract>::apply(TNode node) { template<> inline bool RewriteRule<EvalConcat>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_CONCAT && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -445,7 +445,7 @@ Node RewriteRule<EvalConcat>::apply(TNode node) { template<> inline bool RewriteRule<EvalSignExtend>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_SIGN_EXTEND && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -461,7 +461,7 @@ Node RewriteRule<EvalSignExtend>::apply(TNode node) { template<> inline bool RewriteRule<EvalEquals>::applies(TNode node) { return (node.getKind() == kind::EQUAL && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline @@ -479,7 +479,7 @@ Node RewriteRule<EvalEquals>::apply(TNode node) { template<> inline bool RewriteRule<EvalComp>::applies(TNode node) { return (node.getKind() == kind::BITVECTOR_COMP && - utils::isBVGroundTerm(node)); + utils::isBvConstTerm(node)); } template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index d17f20152..ad5b37a2d 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -394,19 +394,22 @@ Node RewriteRule<MultSimplify>::apply(TNode node) { std::vector<Node> children; for (const TNode& current : node) { - if (current.getKind() == kind::CONST_BITVECTOR) { - BitVector value = current.getConst<BitVector>(); + Node c = current; + if (c.getKind() == kind::BITVECTOR_NEG) + { + isNeg = !isNeg; + c = c[0]; + } + + if (c.getKind() == kind::CONST_BITVECTOR) + { + BitVector value = c.getConst<BitVector>(); constant = constant * value; if(constant == BitVector(size, (unsigned) 0)) { return utils::mkConst(size, 0); } - } - else if (current.getKind() == kind::BITVECTOR_NEG) - { - isNeg = !isNeg; - children.push_back(current[0]); } else { - children.push_back(current); + children.push_back(c); } } BitVector oValue = BitVector(size, static_cast<unsigned>(1)); @@ -414,8 +417,7 @@ Node RewriteRule<MultSimplify>::apply(TNode node) { if (children.empty()) { - Assert(!isNeg); - return utils::mkConst(constant); + return utils::mkConst(isNeg ? -constant : constant); } std::sort(children.begin(), children.end()); diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index 067440ee2..fb083c568 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -790,7 +790,15 @@ inline Node RewriteRule<MultPow2>::apply(TNode node) } } - Node a = utils::mkNode(kind::BITVECTOR_MULT, children); + Node a; + if (children.empty()) + { + a = utils::mkOne(size); + } + else + { + a = utils::mkNode(kind::BITVECTOR_MULT, children); + } if (isNeg && size > 1) { diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index 783d04492..9b66574f6 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -2,17 +2,16 @@ /*! \file theory_bv_utils.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Tim King, Paul Meng + ** Aina Niemetz, Liana Hadarean, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] + ** \brief Util functions for theory BV. ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** Util functions for theory BV. **/ #include "theory/bv/theory_bv_utils.h" @@ -26,21 +25,422 @@ namespace theory { namespace bv { namespace utils { -Node mkSum(std::vector<Node>& children, unsigned width) +/* ------------------------------------------------------------------------- */ + +uint32_t pow2(uint32_t n) +{ + Assert(n < 32); + uint32_t one = 1; + return one << n; +} + +/* ------------------------------------------------------------------------- */ + +BitVector mkBitVectorOnes(unsigned size) +{ + Assert(size > 0); + return BitVector(1, Integer(1)).signExtend(size - 1); +} + +BitVector mkBitVectorMinSigned(unsigned size) +{ + Assert(size > 0); + return BitVector(size).setBit(size - 1); +} + +BitVector mkBitVectorMaxSigned(unsigned size) +{ + Assert(size > 0); + return ~mkBitVectorMinSigned(size); +} + +/* ------------------------------------------------------------------------- */ + +unsigned getSize(TNode node) +{ + return node.getType().getBitVectorSize(); +} + +const bool getBit(TNode node, unsigned i) +{ + Assert(i < utils::getSize(node) && node.getKind() == kind::CONST_BITVECTOR); + Integer bit = node.getConst<BitVector>().extract(i, i).getValue(); + return (bit == 1u); +} + +/* ------------------------------------------------------------------------- */ + +unsigned getExtractHigh(TNode node) +{ + return node.getOperator().getConst<BitVectorExtract>().high; +} + +unsigned getExtractLow(TNode node) +{ + return node.getOperator().getConst<BitVectorExtract>().low; +} + +unsigned getSignExtendAmount(TNode node) +{ + return node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount; +} + +/* ------------------------------------------------------------------------- */ + +bool isZero(TNode node) +{ + if (!node.isConst()) return false; + return node == utils::mkConst(utils::getSize(node), 0u); +} + +unsigned isPow2Const(TNode node, bool& isNeg) +{ + if (node.getKind() != kind::CONST_BITVECTOR) + { + return false; + } + + BitVector bv = node.getConst<BitVector>(); + unsigned p = bv.isPow2(); + if (p != 0) + { + isNeg = false; + return p; + } + BitVector nbv = -bv; + p = nbv.isPow2(); + if (p != 0) + { + isNeg = true; + return p; + } + return false; +} + +bool isBvConstTerm(TNode node) +{ + if (node.getNumChildren() == 0) + { + return node.isConst(); + } + + for (size_t i = 0; i < node.getNumChildren(); ++i) + { + if (!node[i].isConst()) + { + return false; + } + } + return true; +} + +bool isBVPredicate(TNode node) +{ + if (node.getKind() == kind::EQUAL || node.getKind() == kind::BITVECTOR_ULT + || node.getKind() == kind::BITVECTOR_SLT + || node.getKind() == kind::BITVECTOR_UGT + || node.getKind() == kind::BITVECTOR_UGE + || node.getKind() == kind::BITVECTOR_SGT + || node.getKind() == kind::BITVECTOR_SGE + || node.getKind() == kind::BITVECTOR_ULE + || node.getKind() == kind::BITVECTOR_SLE + || node.getKind() == kind::BITVECTOR_REDOR + || node.getKind() == kind::BITVECTOR_REDAND + || (node.getKind() == kind::NOT + && (node[0].getKind() == kind::EQUAL + || node[0].getKind() == kind::BITVECTOR_ULT + || node[0].getKind() == kind::BITVECTOR_SLT + || node[0].getKind() == kind::BITVECTOR_UGT + || node[0].getKind() == kind::BITVECTOR_UGE + || node[0].getKind() == kind::BITVECTOR_SGT + || node[0].getKind() == kind::BITVECTOR_SGE + || node[0].getKind() == kind::BITVECTOR_ULE + || node[0].getKind() == kind::BITVECTOR_SLE + || node[0].getKind() == kind::BITVECTOR_REDOR + || node[0].getKind() == kind::BITVECTOR_REDAND))) + { + return true; + } + else + { + return false; + } +} + +bool isCoreTerm(TNode term, TNodeBoolMap& cache) +{ + term = term.getKind() == kind::NOT ? term[0] : term; + TNodeBoolMap::const_iterator it = cache.find(term); + if (it != cache.end()) + { + return it->second; + } + + if (term.getNumChildren() == 0) return true; + + if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, term) == THEORY_BV) + { + Kind k = term.getKind(); + if (k != kind::CONST_BITVECTOR && k != kind::BITVECTOR_CONCAT + && k != kind::BITVECTOR_EXTRACT && k != kind::EQUAL + && term.getMetaKind() != kind::metakind::VARIABLE) + { + cache[term] = false; + return false; + } + } + + for (unsigned i = 0; i < term.getNumChildren(); ++i) + { + if (!isCoreTerm(term[i], cache)) + { + cache[term] = false; + return false; + } + } + + cache[term] = true; + return true; +} + +bool isEqualityTerm(TNode term, TNodeBoolMap& cache) +{ + term = term.getKind() == kind::NOT ? term[0] : term; + TNodeBoolMap::const_iterator it = cache.find(term); + if (it != cache.end()) + { + return it->second; + } + + if (term.getNumChildren() == 0) return true; + + if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, term) == THEORY_BV) + { + Kind k = term.getKind(); + if (k != kind::CONST_BITVECTOR && k != kind::EQUAL + && term.getMetaKind() != kind::metakind::VARIABLE) + { + cache[term] = false; + return false; + } + } + + for (unsigned i = 0; i < term.getNumChildren(); ++i) + { + if (!isEqualityTerm(term[i], cache)) + { + cache[term] = false; + return false; + } + } + + cache[term] = true; + return true; +} + +bool isBitblastAtom(Node lit) +{ + TNode atom = lit.getKind() == kind::NOT ? lit[0] : lit; + return atom.getKind() != kind::EQUAL || atom[0].getType().isBitVector(); +} + +/* ------------------------------------------------------------------------- */ + +Node mkTrue() +{ + return NodeManager::currentNM()->mkConst<bool>(true); +} + +Node mkFalse() +{ + return NodeManager::currentNM()->mkConst<bool>(false); +} + +Node mkOnes(unsigned size) +{ + BitVector val = mkBitVectorOnes(size); + return NodeManager::currentNM()->mkConst<BitVector>(val); +} + +Node mkZero(unsigned size) +{ + return mkConst(size, 0u); +} + +Node mkOne(unsigned size) +{ + return mkConst(size, 1u); +} + +/* ------------------------------------------------------------------------- */ + +Node mkConst(unsigned size, unsigned int value) +{ + BitVector val(size, value); + return NodeManager::currentNM()->mkConst<BitVector>(val); +} + +Node mkConst(unsigned size, Integer& value) +{ + return NodeManager::currentNM()->mkConst<BitVector>(BitVector(size, value)); +} + +Node mkConst(const BitVector& value) +{ + return NodeManager::currentNM()->mkConst<BitVector>(value); +} + +/* ------------------------------------------------------------------------- */ + +Node mkVar(unsigned size) +{ + NodeManager* nm = NodeManager::currentNM(); + + return nm->mkSkolem("BVSKOLEM$$", + nm->mkBitVectorType(size), + "is a variable created by the theory of bitvectors"); +} + +/* ------------------------------------------------------------------------- */ + +Node mkNode(Kind kind, TNode child) +{ + return NodeManager::currentNM()->mkNode(kind, child); +} + +Node mkNode(Kind kind, TNode child1, TNode child2) { - std::size_t nchildren = children.size(); + return NodeManager::currentNM()->mkNode(kind, child1, child2); +} - if (nchildren == 0) +Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3) +{ + return NodeManager::currentNM()->mkNode(kind, child1, child2, child3); +} + +Node mkNode(Kind kind, std::vector<Node>& children) +{ + Assert(children.size() > 0); + if (children.size() == 1) { - return mkZero(width); + return children[0]; } - else if (nchildren == 1) + return NodeManager::currentNM()->mkNode(kind, children); +} + +/* ------------------------------------------------------------------------- */ + +Node mkSortedNode(Kind kind, TNode child1, TNode child2) +{ + Assert(kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR + || kind == kind::BITVECTOR_XOR); + + if (child1 < child2) + { + return NodeManager::currentNM()->mkNode(kind, child1, child2); + } + else + { + return NodeManager::currentNM()->mkNode(kind, child2, child1); + } +} + +Node mkSortedNode(Kind kind, std::vector<Node>& children) +{ + Assert(kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR + || kind == kind::BITVECTOR_XOR); + Assert(children.size() > 0); + if (children.size() == 1) { return children[0]; } - return NodeManager::currentNM()->mkNode(kind::BITVECTOR_PLUS, children); + std::sort(children.begin(), children.end()); + return NodeManager::currentNM()->mkNode(kind, children); +} + +/* ------------------------------------------------------------------------- */ + +Node mkNot(Node child) +{ + return NodeManager::currentNM()->mkNode(kind::NOT, child); +} + +Node mkAnd(TNode node1, TNode node2) +{ + return NodeManager::currentNM()->mkNode(kind::AND, node1, node2); +} + +Node mkOr(TNode node1, TNode node2) +{ + return NodeManager::currentNM()->mkNode(kind::OR, node1, node2); } +Node mkXor(TNode node1, TNode node2) +{ + return NodeManager::currentNM()->mkNode(kind::XOR, node1, node2); +} + +/* ------------------------------------------------------------------------- */ + +Node mkSignExtend(TNode node, unsigned amount) +{ + NodeManager* nm = NodeManager::currentNM(); + Node signExtendOp = + nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount)); + return nm->mkNode(signExtendOp, node); +} + +/* ------------------------------------------------------------------------- */ + +Node mkExtract(TNode node, unsigned high, unsigned low) +{ + Node extractOp = NodeManager::currentNM()->mkConst<BitVectorExtract>( + BitVectorExtract(high, low)); + std::vector<Node> children; + children.push_back(node); + return NodeManager::currentNM()->mkNode(extractOp, children); +} + +Node mkBitOf(TNode node, unsigned index) +{ + Node bitOfOp = + NodeManager::currentNM()->mkConst<BitVectorBitOf>(BitVectorBitOf(index)); + return NodeManager::currentNM()->mkNode(bitOfOp, node); +} + +/* ------------------------------------------------------------------------- */ + +Node mkConcat(TNode t1, TNode t2) +{ + return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, t1, t2); +} + +Node mkConcat(std::vector<Node>& children) +{ + if (children.size() > 1) + return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, children); + else + return children[0]; +} + +Node mkConcat(TNode node, unsigned repeat) +{ + Assert(repeat); + if (repeat == 1) + { + return node; + } + NodeBuilder<> result(kind::BITVECTOR_CONCAT); + for (unsigned i = 0; i < repeat; ++i) + { + result << node; + } + Node resultNode = result; + return resultNode; +} + +/* ------------------------------------------------------------------------- */ + Node mkInc(TNode t) { return NodeManager::currentNM()->mkNode( @@ -53,6 +453,8 @@ Node mkDec(TNode t) kind::BITVECTOR_SUB, t, bv::utils::mkOne(bv::utils::getSize(t))); } +/* ------------------------------------------------------------------------- */ + Node mkUmulo(TNode t1, TNode t2) { unsigned w = getSize(t1); @@ -76,96 +478,233 @@ Node mkUmulo(TNode t1, TNode t2) return nm->mkNode(kind::EQUAL, nm->mkNode(kind::BITVECTOR_OR, tmp), mkOne(1)); } -bool isCoreTerm(TNode term, TNodeBoolMap& cache) { - term = term.getKind() == kind::NOT ? term[0] : term; - TNodeBoolMap::const_iterator it = cache.find(term); - if (it != cache.end()) { - return it->second; +/* ------------------------------------------------------------------------- */ + +Node mkConjunction(const std::set<TNode> nodes) +{ + std::set<TNode> expandedNodes; + + std::set<TNode>::const_iterator it = nodes.begin(); + std::set<TNode>::const_iterator it_end = nodes.end(); + while (it != it_end) + { + TNode current = *it; + if (current != mkTrue()) + { + Assert(current.getKind() == kind::EQUAL + || (current.getKind() == kind::NOT + && current[0].getKind() == kind::EQUAL)); + expandedNodes.insert(current); + } + ++it; } - if (term.getNumChildren() == 0) - return true; + Assert(expandedNodes.size() > 0); + if (expandedNodes.size() == 1) + { + return *expandedNodes.begin(); + } - if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, term) == THEORY_BV) { - Kind k = term.getKind(); - if (k != kind::CONST_BITVECTOR && - k != kind::BITVECTOR_CONCAT && - k != kind::BITVECTOR_EXTRACT && - k != kind::EQUAL && - term.getMetaKind() != kind::metakind::VARIABLE) { - cache[term] = false; - return false; + NodeBuilder<> conjunction(kind::AND); + + it = expandedNodes.begin(); + it_end = expandedNodes.end(); + while (it != it_end) + { + conjunction << *it; + ++it; + } + + return conjunction; +} + +Node mkConjunction(const std::vector<TNode>& nodes) +{ + std::vector<TNode> expandedNodes; + + std::vector<TNode>::const_iterator it = nodes.begin(); + std::vector<TNode>::const_iterator it_end = nodes.end(); + while (it != it_end) + { + TNode current = *it; + + if (current != mkTrue()) + { + Assert(isBVPredicate(current)); + expandedNodes.push_back(current); } + ++it; } - for (unsigned i = 0; i < term.getNumChildren(); ++i) { - if (!isCoreTerm(term[i], cache)) { - cache[term] = false; - return false; + if (expandedNodes.size() == 0) + { + return mkTrue(); + } + + if (expandedNodes.size() == 1) + { + return *expandedNodes.begin(); + } + + NodeBuilder<> conjunction(kind::AND); + + it = expandedNodes.begin(); + it_end = expandedNodes.end(); + while (it != it_end) + { + conjunction << *it; + ++it; + } + + return conjunction; +} + +/* ------------------------------------------------------------------------- */ + +void getConjuncts(TNode node, std::set<TNode>& conjuncts) +{ + if (node.getKind() != kind::AND) + { + conjuncts.insert(node); + } + else + { + for (unsigned i = 0; i < node.getNumChildren(); ++i) + { + getConjuncts(node[i], conjuncts); } } +} - cache[term]= true; - return true; +void getConjuncts(std::vector<TNode>& nodes, std::set<TNode>& conjuncts) +{ + for (unsigned i = 0, i_end = nodes.size(); i < i_end; ++i) + { + getConjuncts(nodes[i], conjuncts); + } } -bool isEqualityTerm(TNode term, TNodeBoolMap& cache) { - term = term.getKind() == kind::NOT ? term[0] : term; - TNodeBoolMap::const_iterator it = cache.find(term); - if (it != cache.end()) { - return it->second; +Node flattenAnd(std::vector<TNode>& queue) +{ + TNodeSet nodes; + while (!queue.empty()) + { + TNode current = queue.back(); + queue.pop_back(); + if (current.getKind() == kind::AND) + { + for (unsigned i = 0; i < current.getNumChildren(); ++i) + { + if (nodes.count(current[i]) == 0) + { + queue.push_back(current[i]); + } + } + } + else + { + nodes.insert(current); + } + } + std::vector<TNode> children; + for (TNodeSet::const_iterator it = nodes.begin(); it != nodes.end(); ++it) + { + children.push_back(*it); } + return mkAnd(children); +} - if (term.getNumChildren() == 0) - return true; +/* ------------------------------------------------------------------------- */ - if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, term) == THEORY_BV) { - Kind k = term.getKind(); - if (k != kind::CONST_BITVECTOR && - k != kind::EQUAL && - term.getMetaKind() != kind::metakind::VARIABLE) { - cache[term] = false; - return false; +std::string setToString(const std::set<TNode>& nodeSet) { + std::stringstream out; + out << "["; + std::set<TNode>::const_iterator it = nodeSet.begin(); + std::set<TNode>::const_iterator it_end = nodeSet.end(); + bool first = true; + while (it != it_end) { + if (!first) { + out << ","; } + first = false; + out << *it; + ++ it; } + out << "]"; + return out.str(); +} - for (unsigned i = 0; i < term.getNumChildren(); ++i) { - if (!isEqualityTerm(term[i], cache)) { - cache[term] = false; - return false; +std::string vectorToString(const std::vector<Node>& nodes) +{ + std::stringstream out; + out << "["; + for (unsigned i = 0; i < nodes.size(); ++i) + { + if (i > 0) + { + out << ","; } + out << nodes[i]; } + out << "]"; + return out.str(); +} - cache[term]= true; - return true; +/* ------------------------------------------------------------------------- */ + +// FIXME: dumb code +void intersect(const std::vector<uint32_t>& v1, + const std::vector<uint32_t>& v2, + std::vector<uint32_t>& intersection) { + for (unsigned i = 0; i < v1.size(); ++i) { + bool found = false; + for (unsigned j = 0; j < v2.size(); ++j) { + if (v2[j] == v1[i]) { + found = true; + break; + } + } + if (found) { + intersection.push_back(v1[i]); + } + } } +/* ------------------------------------------------------------------------- */ -uint64_t numNodes(TNode node, NodeSet& seen) { - if (seen.find(node) != seen.end()) - return 0; +uint64_t numNodes(TNode node, NodeSet& seen) +{ + if (seen.find(node) != seen.end()) return 0; uint64_t size = 1; - for (unsigned i = 0; i < node.getNumChildren(); ++i) { + for (unsigned i = 0; i < node.getNumChildren(); ++i) + { size += numNodes(node[i], seen); } seen.insert(node); return size; } -void collectVariables(TNode node, NodeSet& vars) { - if (vars.find(node) != vars.end()) - return; +/* ------------------------------------------------------------------------- */ - if (Theory::isLeafOf(node, THEORY_BV) && node.getKind() != kind::CONST_BITVECTOR) { +void collectVariables(TNode node, NodeSet& vars) +{ + if (vars.find(node) != vars.end()) return; + + if (Theory::isLeafOf(node, THEORY_BV) + && node.getKind() != kind::CONST_BITVECTOR) + { vars.insert(node); return; } - for (unsigned i = 0; i < node.getNumChildren(); ++i) { + for (unsigned i = 0; i < node.getNumChildren(); ++i) + { collectVariables(node[i], vars); } } +/* ------------------------------------------------------------------------- */ + }/* CVC4::theory::bv::utils namespace */ }/* CVC4::theory::bv namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index e304e4801..f6784621f 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -2,17 +2,16 @@ /*! \file theory_bv_utils.h ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Dejan Jovanovic, Morgan Deters + ** Aina Niemetz, Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] + ** \brief Util functions for theory BV. ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** Util functions for theory BV. **/ #include "cvc4_private.h" @@ -36,205 +35,153 @@ typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; namespace utils { -inline uint32_t pow2(uint32_t power) { - Assert (power < 32); - uint32_t one = 1; - return one << power; -} - -inline unsigned getExtractHigh(TNode node) { - return node.getOperator().getConst<BitVectorExtract>().high; -} - -inline unsigned getExtractLow(TNode node) { - return node.getOperator().getConst<BitVectorExtract>().low; -} +typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; +typedef std::unordered_set<Node, NodeHashFunction> NodeSet; -inline unsigned getSize(TNode node) { - return node.getType().getBitVectorSize(); -} +/* Compute 2^n. */ +uint32_t pow2(uint32_t n); -inline unsigned getSignExtendAmount(TNode node) +/* Compute the greatest common divisor for two objects of Type T. */ +template <class T> +T gcd(T a, T b) { - return node.getOperator().getConst<BitVectorSignExtend>().signExtendAmount; -} - -inline const bool getBit(TNode node, unsigned i) { - Assert (i < utils::getSize(node) && - node.getKind() == kind::CONST_BITVECTOR); - Integer bit = node.getConst<BitVector>().extract(i, i).getValue(); - return (bit == 1u); -} - -inline Node mkTrue() { - return NodeManager::currentNM()->mkConst<bool>(true); -} - -inline Node mkFalse() { - return NodeManager::currentNM()->mkConst<bool>(false); -} - -inline Node mkVar(unsigned size) { - NodeManager* nm = NodeManager::currentNM(); - - return nm->mkSkolem("BVSKOLEM$$", nm->mkBitVectorType(size), "is a variable created by the theory of bitvectors"); -} - - -inline Node mkSortedNode(Kind kind, std::vector<Node>& children) { - Assert (kind == kind::BITVECTOR_AND || - kind == kind::BITVECTOR_OR || - kind == kind::BITVECTOR_XOR); - Assert(children.size() > 0); - if (children.size() == 1) { - return children[0]; - } - std::sort(children.begin(), children.end()); - return NodeManager::currentNM()->mkNode(kind, children); -} - - -inline Node mkNode(Kind kind, std::vector<Node>& children) { - Assert (children.size() > 0); - if (children.size() == 1) { - return children[0]; - } - return NodeManager::currentNM()->mkNode(kind, children); -} - -inline Node mkNode(Kind kind, TNode child) { - return NodeManager::currentNM()->mkNode(kind, child); -} - -inline Node mkNode(Kind kind, TNode child1, TNode child2) { - return NodeManager::currentNM()->mkNode(kind, child1, child2); -} - - -inline Node mkSortedNode(Kind kind, TNode child1, TNode child2) { - Assert (kind == kind::BITVECTOR_AND || - kind == kind::BITVECTOR_OR || - kind == kind::BITVECTOR_XOR); - - if (child1 < child2) { - return NodeManager::currentNM()->mkNode(kind, child1, child2); - } else { - return NodeManager::currentNM()->mkNode(kind, child2, child1); + while (b != 0) + { + T t = b; + b = a % t; + a = t; } + return a; } -inline Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3) { - return NodeManager::currentNM()->mkNode(kind, child1, child2, child3); -} - - -inline Node mkNot(Node child) { - return NodeManager::currentNM()->mkNode(kind::NOT, child); -} - -inline Node mkAnd(TNode node1, TNode node2) { - return NodeManager::currentNM()->mkNode(kind::AND, node1, node2); -} - -inline Node mkOr(TNode node1, TNode node2) { - return NodeManager::currentNM()->mkNode(kind::OR, node1, node2); -} - -inline Node mkXor(TNode node1, TNode node2) { - return NodeManager::currentNM()->mkNode(kind::XOR, node1, node2); -} - -inline Node mkSignExtend(TNode node, unsigned amount) -{ - NodeManager* nm = NodeManager::currentNM(); - Node signExtendOp = - nm->mkConst<BitVectorSignExtend>(BitVectorSignExtend(amount)); - return nm->mkNode(signExtendOp, node); -} - -inline Node mkExtract(TNode node, unsigned high, unsigned low) { - Node extractOp = NodeManager::currentNM()->mkConst<BitVectorExtract>(BitVectorExtract(high, low)); - std::vector<Node> children; - children.push_back(node); - return NodeManager::currentNM()->mkNode(extractOp, children); -} +/* Create bit-vector of ones of given size. */ +BitVector mkBitVectorOnes(unsigned size); +/* Create bit-vector representing the minimum signed value of given size. */ +BitVector mkBitVectorMinSigned(unsigned size); +/* Create bit-vector representing the maximum signed value of given size. */ +BitVector mkBitVectorMaxSigned(unsigned size); -inline Node mkBitOf(TNode node, unsigned index) { - Node bitOfOp = NodeManager::currentNM()->mkConst<BitVectorBitOf>(BitVectorBitOf(index)); - return NodeManager::currentNM()->mkNode(bitOfOp, node); -} +/* Get the bit-width of given node. */ +unsigned getSize(TNode node); -Node mkSum(std::vector<Node>& children, unsigned width); +/* Get bit at given index. */ +const bool getBit(TNode node, unsigned i); -inline Node mkConcat(TNode node, unsigned repeat) { - Assert (repeat); - if(repeat == 1) { - return node; - } - NodeBuilder<> result(kind::BITVECTOR_CONCAT); - for (unsigned i = 0; i < repeat; ++i) { - result << node; - } - Node resultNode = result; - return resultNode; -} +/* Get the upper index of given extract node. */ +unsigned getExtractHigh(TNode node); +/* Get the lower index of given extract node. */ +unsigned getExtractLow(TNode node); -inline Node mkConcat(std::vector<Node>& children) { - if (children.size() > 1) - return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, children); - else - return children[0]; -} +/* Get the number of bits by which a given node is extended. */ +unsigned getSignExtendAmount(TNode node); -inline Node mkConcat(TNode t1, TNode t2) { - return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, t1, t2); -} - - -inline BitVector mkBitVectorOnes(unsigned size) { - Assert(size > 0); - return BitVector(1, Integer(1)).signExtend(size - 1); -} - -inline BitVector mkBitVectorMinSigned(unsigned size) +/* Returns true if given node represents a zero bit-vector. */ +bool isZero(TNode node); +/* If node is a constant of the form 2^c or -2^c, then this function returns + * c+1. Otherwise, this function returns 0. The flag isNeg is updated to + * indicate whether node is negative. */ +unsigned isPow2Const(TNode node, bool& isNeg); +/* Returns true if node or all of its children is const. */ +bool isBvConstTerm(TNode node); +/* Returns true if node is a predicate over bit-vector nodes. */ +bool isBVPredicate(TNode node); +/* Returns true if given term is a THEORY_BV term. */ +bool isCoreTerm(TNode term, TNodeBoolMap& cache); +/* Returns true if given term is a bv constant, variable or equality term. */ +bool isEqualityTerm(TNode term, TNodeBoolMap& cache); +/* Returns true if given node is an atom that is bit-blasted. */ +bool isBitblastAtom(Node lit); + +/* Create Boolean node representing true. */ +Node mkTrue(); +/* Create Boolean node representing false. */ +Node mkFalse(); +/* Create bit-vector node representing a bit-vector of ones of given size. */ +Node mkOnes(unsigned size); +/* Create bit-vector node representing a zero bit-vector of given size. */ +Node mkZero(unsigned size); +/* Create bit-vector node representing a bit-vector value one of given size. */ +Node mkOne(unsigned size); + +/* Create bit-vector constant of given size and value. */ +Node mkConst(unsigned size, unsigned int value); +Node mkConst(unsigned size, Integer& value); +/* Create bit-vector constant from given bit-vector. */ +Node mkConst(const BitVector& value); + +/* Create bit-vector variable. */ +Node mkVar(unsigned size); + +/* Create n-ary node of given kind. */ +Node mkNode(Kind kind, TNode child); +Node mkNode(Kind kind, TNode child1, TNode child2); +Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3); +Node mkNode(Kind kind, std::vector<Node>& children); + +/* Create n-ary bit-vector node of kind BITVECTOR_AND, BITVECTOR_OR or + * BITVECTOR_XOR where its children are sorted */ +Node mkSortedNode(Kind kind, TNode child1, TNode child2); +Node mkSortedNode(Kind kind, std::vector<Node>& children); + +/* Create node of kind NOT. */ +Node mkNot(Node child); +/* Create node of kind AND. */ +Node mkAnd(TNode node1, TNode node2); +/* Create n-ary node of kind AND. */ +template<bool ref_count> +Node mkAnd(const std::vector<NodeTemplate<ref_count>>& conjunctions) { - Assert(size > 0); - return BitVector(size).setBit(size - 1); -} + std::set<TNode> all(conjunctions.begin(), conjunctions.end()); -inline BitVector mkBitVectorMaxSigned(unsigned size) -{ - Assert(size > 0); - return ~mkBitVectorMinSigned(size); -} + if (all.size() == 0) { return mkTrue(); } -inline Node mkOnes(unsigned size) { - BitVector val = mkBitVectorOnes(size); - return NodeManager::currentNM()->mkConst<BitVector>(val); -} + /* All the same, or just one */ + if (all.size() == 1) { return conjunctions[0]; } -inline Node mkConst(unsigned size, unsigned int value) { - BitVector val(size, value); - return NodeManager::currentNM()->mkConst<BitVector>(val); + NodeBuilder<> conjunction(kind::AND); + for (const Node& n : all) { conjunction << n; } + return conjunction; } - -inline Node mkConst(unsigned size, Integer& value) +/* Create node of kind OR. */ +Node mkOr(TNode node1, TNode node2); +/* Create n-ary node of kind OR. */ +template<bool ref_count> +Node mkOr(const std::vector<NodeTemplate<ref_count>>& nodes) { - return NodeManager::currentNM()->mkConst<BitVector>(BitVector(size, value)); -} + std::set<TNode> all(nodes.begin(), nodes.end()); -inline Node mkConst(const BitVector& value) { - return NodeManager::currentNM()->mkConst<BitVector>(value); -} + if (all.size() == 0) { return mkTrue(); } -inline Node mkZero(unsigned size) { return mkConst(size, 0u); } + /* All the same, or just one */ + if (all.size() == 1) { return nodes[0]; } -inline Node mkOne(unsigned size) { return mkConst(size, 1u); } - -/* Increment */ + NodeBuilder<> disjunction(kind::OR); + for (const Node& n : all) { disjunction << n; } + return disjunction; +} +/* Create node of kind XOR. */ +Node mkXor(TNode node1, TNode node2); + +/* Create signed extension node where given node is extended by given amount. */ +Node mkSignExtend(TNode node, unsigned amount); + +/* Create extract node where bits from index high to index low are extracted + * from given node. */ +Node mkExtract(TNode node, unsigned high, unsigned low); +/* Create extract node of bit-width 1 where the resulting node represents + * the bit at given index. */ +Node mkBitOf(TNode node, unsigned index); + +/* Create n-ary concat node of given children. */ +Node mkConcat(TNode t1, TNode t2); +Node mkConcat(std::vector<Node>& children); +/* Create concat by repeating given node n times. + * Returns given node if n = 1. */ +Node mkConcat(TNode node, unsigned repeat); + +/* Create bit-vector addition node representing the increment of given node. */ Node mkInc(TNode t); - -/* Decrement */ +/* Create bit-vector addition node representing the decrement of given node. */ Node mkDec(TNode t); /* Unsigned multiplication overflow detection. @@ -243,345 +190,33 @@ Node mkDec(TNode t); * http://ieeexplore.ieee.org/document/987767 */ Node mkUmulo(TNode t1, TNode t2); -inline void getConjuncts(TNode node, std::set<TNode>& conjuncts) { - if (node.getKind() != kind::AND) { - conjuncts.insert(node); - } else { - for (unsigned i = 0; i < node.getNumChildren(); ++ i) { - getConjuncts(node[i], conjuncts); - } - } -} - -inline void getConjuncts(std::vector<TNode>& nodes, std::set<TNode>& conjuncts) { - for (unsigned i = 0, i_end = nodes.size(); i < i_end; ++ i) { - getConjuncts(nodes[i], conjuncts); - } -} +/* Create conjunction over a set of (dis)equalities. */ +Node mkConjunction(const std::set<TNode> nodes); +Node mkConjunction(const std::vector<TNode>& nodes); -inline Node mkConjunction(const std::set<TNode> nodes) { - std::set<TNode> expandedNodes; - - std::set<TNode>::const_iterator it = nodes.begin(); - std::set<TNode>::const_iterator it_end = nodes.end(); - while (it != it_end) { - TNode current = *it; - if (current != mkTrue()) { - Assert(current.getKind() == kind::EQUAL || (current.getKind() == kind::NOT && current[0].getKind() == kind::EQUAL)); - expandedNodes.insert(current); - } - ++ it; - } +/* Get a set of all operands of nested and nodes. */ +void getConjuncts(TNode node, std::set<TNode>& conjuncts); +void getConjuncts(std::vector<TNode>& nodes, std::set<TNode>& conjuncts); +/* Create a flattened and node. */ +Node flattenAnd(std::vector<TNode>& queue); - Assert(expandedNodes.size() > 0); - if (expandedNodes.size() == 1) { - return *expandedNodes.begin(); - } +/* Create a string representing a set of nodes. */ +std::string setToString(const std::set<TNode>& nodeSet); - NodeBuilder<> conjunction(kind::AND); +/* Create a string representing a vector of nodes. */ +std::string vectorToString(const std::vector<Node>& nodes); - it = expandedNodes.begin(); - it_end = expandedNodes.end(); - while (it != it_end) { - conjunction << *it; - ++ it; - } - - return conjunction; -} - -/** - * If node is a constant of the form 2^c or -2^c, then this function returns - * c+1. Otherwise, this function returns 0. The flag isNeg is updated to - * indicate whether node is negative. - */ -inline unsigned isPow2Const(TNode node, bool& isNeg) -{ - if (node.getKind() != kind::CONST_BITVECTOR) { - return false; - } - - BitVector bv = node.getConst<BitVector>(); - unsigned p = bv.isPow2(); - if (p != 0) - { - isNeg = false; - return p; - } - BitVector nbv = -bv; - p = nbv.isPow2(); - if (p != 0) - { - isNeg = true; - return p; - } - return false; -} - -inline Node mkOr(const std::vector<Node>& nodes) { - std::set<TNode> all; - all.insert(nodes.begin(), nodes.end()); - - if (all.size() == 0) { - return mkTrue(); - } - - if (all.size() == 1) { - // All the same, or just one - return nodes[0]; - } - - - NodeBuilder<> disjunction(kind::OR); - std::set<TNode>::const_iterator it = all.begin(); - std::set<TNode>::const_iterator it_end = all.end(); - while (it != it_end) { - disjunction << *it; - ++ it; - } - - return disjunction; -}/* mkOr() */ - - -inline Node mkAnd(const std::vector<TNode>& conjunctions) { - std::set<TNode> all; - all.insert(conjunctions.begin(), conjunctions.end()); - - if (all.size() == 0) { - return mkTrue(); - } - - if (all.size() == 1) { - // All the same, or just one - return conjunctions[0]; - } - - - NodeBuilder<> conjunction(kind::AND); - std::set<TNode>::const_iterator it = all.begin(); - std::set<TNode>::const_iterator it_end = all.end(); - while (it != it_end) { - conjunction << *it; - ++ it; - } - - return conjunction; -}/* mkAnd() */ - -inline Node mkAnd(const std::vector<Node>& conjunctions) { - std::set<TNode> all; - all.insert(conjunctions.begin(), conjunctions.end()); - - if (all.size() == 0) { - return mkTrue(); - } - - if (all.size() == 1) { - // All the same, or just one - return conjunctions[0]; - } - - - NodeBuilder<> conjunction(kind::AND); - std::set<TNode>::const_iterator it = all.begin(); - std::set<TNode>::const_iterator it_end = all.end(); - while (it != it_end) { - conjunction << *it; - ++ it; - } - - return conjunction; -}/* mkAnd() */ - -inline bool isZero(TNode node) { - if (!node.isConst()) return false; - return node == utils::mkConst(utils::getSize(node), 0u); -} - -inline Node flattenAnd(std::vector<TNode>& queue) { - TNodeSet nodes; - while(!queue.empty()) { - TNode current = queue.back(); - queue.pop_back(); - if (current.getKind() == kind::AND) { - for (unsigned i = 0; i < current.getNumChildren(); ++i) { - if (nodes.count(current[i]) == 0) { - queue.push_back(current[i]); - } - } - } else { - nodes.insert(current); - } - } - std::vector<TNode> children; - for (TNodeSet::const_iterator it = nodes.begin(); it!= nodes.end(); ++it) { - children.push_back(*it); - } - return mkAnd(children); -} - - -// need a better name, this is not technically a ground term -inline bool isBVGroundTerm(TNode node) { - if (node.getNumChildren() == 0) { - return node.isConst(); - } - - for (size_t i = 0; i < node.getNumChildren(); ++i) { - if(! node[i].isConst()) { - return false; - } - } - return true; -} - -inline bool isBVPredicate(TNode node) { - if (node.getKind() == kind::EQUAL || - node.getKind() == kind::BITVECTOR_ULT || - node.getKind() == kind::BITVECTOR_SLT || - node.getKind() == kind::BITVECTOR_UGT || - node.getKind() == kind::BITVECTOR_UGE || - node.getKind() == kind::BITVECTOR_SGT || - node.getKind() == kind::BITVECTOR_SGE || - node.getKind() == kind::BITVECTOR_ULE || - node.getKind() == kind::BITVECTOR_SLE || - node.getKind() == kind::BITVECTOR_REDOR || - node.getKind() == kind::BITVECTOR_REDAND || - ( node.getKind() == kind::NOT && (node[0].getKind() == kind::EQUAL || - node[0].getKind() == kind::BITVECTOR_ULT || - node[0].getKind() == kind::BITVECTOR_SLT || - node[0].getKind() == kind::BITVECTOR_UGT || - node[0].getKind() == kind::BITVECTOR_UGE || - node[0].getKind() == kind::BITVECTOR_SGT || - node[0].getKind() == kind::BITVECTOR_SGE || - node[0].getKind() == kind::BITVECTOR_ULE || - node[0].getKind() == kind::BITVECTOR_SLE || - node[0].getKind() == kind::BITVECTOR_REDOR || - node[0].getKind() == kind::BITVECTOR_REDAND))) - { - return true; - } - else - { - return false; - } -} - -inline Node mkConjunction(const std::vector<TNode>& nodes) { - std::vector<TNode> expandedNodes; - - std::vector<TNode>::const_iterator it = nodes.begin(); - std::vector<TNode>::const_iterator it_end = nodes.end(); - while (it != it_end) { - TNode current = *it; - - if (current != mkTrue()) { - Assert(isBVPredicate(current)); - expandedNodes.push_back(current); - } - ++ it; - } - - if (expandedNodes.size() == 0) { - return mkTrue(); - } - - if (expandedNodes.size() == 1) { - return *expandedNodes.begin(); - } - - NodeBuilder<> conjunction(kind::AND); - - it = expandedNodes.begin(); - it_end = expandedNodes.end(); - while (it != it_end) { - conjunction << *it; - ++ it; - } - - return conjunction; -} - - - -// Turn a set into a string -inline std::string setToString(const std::set<TNode>& nodeSet) { - std::stringstream out; - out << "["; - std::set<TNode>::const_iterator it = nodeSet.begin(); - std::set<TNode>::const_iterator it_end = nodeSet.end(); - bool first = true; - while (it != it_end) { - if (!first) { - out << ","; - } - first = false; - out << *it; - ++ it; - } - out << "]"; - return out.str(); -} - -// Turn a vector into a string -inline std::string vectorToString(const std::vector<Node>& nodes) { - std::stringstream out; - out << "["; - for (unsigned i = 0; i < nodes.size(); ++ i) { - if (i > 0) { - out << ","; - } - out << nodes[i]; - } - out << "]"; - return out.str(); -} - -// FIXME: dumb code -inline void intersect(const std::vector<uint32_t>& v1, - const std::vector<uint32_t>& v2, - std::vector<uint32_t>& intersection) { - for (unsigned i = 0; i < v1.size(); ++i) { - bool found = false; - for (unsigned j = 0; j < v2.size(); ++j) { - if (v2[j] == v1[i]) { - found = true; - break; - } - } - if (found) { - intersection.push_back(v1[i]); - } - } -} - -template <class T> -inline T gcd(T a, T b) { - while (b != 0) { - T t = b; - b = a % t; - a = t; - } - return a; -} - -typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap; - -bool isCoreTerm(TNode term, TNodeBoolMap& cache); -bool isEqualityTerm(TNode term, TNodeBoolMap& cache); -typedef std::unordered_set<Node, NodeHashFunction> NodeSet; +/* Create the intersection of two vectors of uint32_t. */ +void intersect(const std::vector<uint32_t>& v1, + const std::vector<uint32_t>& v2, + std::vector<uint32_t>& intersection); +/* Determine the total number of nodes that a given node consists of. */ uint64_t numNodes(TNode node, NodeSet& seen); +/* Collect all variables under a given a node. */ void collectVariables(TNode node, NodeSet& vars); -// is bitblast atom -inline bool isBitblastAtom( Node lit ) { - TNode atom = lit.getKind()==kind::NOT ? lit[0] : lit; - return atom.getKind()!=kind::EQUAL || atom[0].getType().isBitVector(); -} - } } } |