From 7aa55e0d38e73a02b11ad0c5a60196b610674050 Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Sat, 25 Feb 2012 18:23:10 +0000 Subject: Refactored CnfStream to work with the bv theory Bitblaster: * separated SatSolverInput interface class into two classes: - TheoryProxy for the sat solver to communicate with the theories - SatSolverInterface abstract class to communicate with the sat solver * instead of using #ifdef typedef for SatClauses and SatLiterals, now there are CVC4 SatLiteral/SatClause types and mappings between them and the internal sat solver clause/literal representation * added abstract classes for DPLLSatSolver and BVSatSolver different interfaces Replaced TheoryBV with bitblasting implementation: * all operators bitblasted * only operator elimination rewrite rules so far --- src/theory/Makefile.am | 2 +- src/theory/bv/Makefile.am | 12 +- src/theory/bv/bitblast_strategies.cpp | 824 +++++++++++++++++++++++++ src/theory/bv/bitblast_strategies.h | 112 ++++ src/theory/bv/bv_sat.cpp | 300 +++++++++ src/theory/bv/bv_sat.h | 144 +++++ src/theory/bv/bv_solver_types.cpp | 78 +++ src/theory/bv/bv_solver_types.h | 185 ++++++ src/theory/bv/equality_engine.cpp | 27 - src/theory/bv/equality_engine.h | 844 -------------------------- src/theory/bv/kinds | 8 + src/theory/bv/slice_manager.h | 677 --------------------- src/theory/bv/theory_bv.cpp | 257 +++----- src/theory/bv/theory_bv.h | 126 +--- src/theory/bv/theory_bv_rewrite_rules.h | 51 +- src/theory/bv/theory_bv_rewrite_rules_arith.h | 321 ++++++++++ src/theory/bv/theory_bv_rewriter.cpp | 78 ++- src/theory/bv/theory_bv_rewriter.h | 2 +- src/theory/bv/theory_bv_type_rules.h | 22 + src/theory/bv/theory_bv_utils.h | 120 +++- src/theory/registrar.h | 50 -- src/theory/theory_registrar.h | 51 ++ 22 files changed, 2411 insertions(+), 1880 deletions(-) create mode 100644 src/theory/bv/bitblast_strategies.cpp create mode 100644 src/theory/bv/bitblast_strategies.h create mode 100644 src/theory/bv/bv_sat.cpp create mode 100644 src/theory/bv/bv_sat.h create mode 100644 src/theory/bv/bv_solver_types.cpp create mode 100644 src/theory/bv/bv_solver_types.h delete mode 100644 src/theory/bv/equality_engine.cpp delete mode 100644 src/theory/bv/equality_engine.h delete mode 100644 src/theory/bv/slice_manager.h create mode 100644 src/theory/bv/theory_bv_rewrite_rules_arith.h delete mode 100644 src/theory/registrar.h create mode 100644 src/theory/theory_registrar.h (limited to 'src/theory') diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index c1a77d988..eb289937f 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -16,7 +16,7 @@ libtheory_la_SOURCES = \ theory_test_utils.h \ theory.h \ theory.cpp \ - registrar.h \ + theory_registrar.h \ rewriter.h \ rewriter_attributes.h \ rewriter.cpp \ diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index 08dde4349..1b8e902e0 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -1,22 +1,26 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ + -D __STDC_LIMIT_MACROS \ + -D __STDC_FORMAT_MACROS \ -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libbv.la libbv_la_SOURCES = \ + theory_bv_utils.h \ + bv_sat.h \ + bv_sat.cpp \ + bitblast_strategies.h \ + bitblast_strategies.cpp \ theory_bv.h \ theory_bv.cpp \ - theory_bv_utils.h \ theory_bv_rewrite_rules.h \ theory_bv_rewrite_rules_core.h \ + theory_bv_rewrite_rules_arith.h \ theory_bv_type_rules.h \ theory_bv_rewriter.h \ theory_bv_rewriter.cpp \ - equality_engine.h \ - equality_engine.cpp \ - slice_manager.h \ cd_set_collection.h EXTRA_DIST = kinds diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp new file mode 100644 index 000000000..b0a02c0a5 --- /dev/null +++ b/src/theory/bv/bitblast_strategies.cpp @@ -0,0 +1,824 @@ +/********************* */ +/*! \file bitblast_strategies.cpp + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of bitblasting functions for various operators. + ** + ** Implementation of bitblasting functions for various operators. + **/ + +#include "bitblast_strategies.h" +#include "bv_sat.h" +#include "prop/sat_module.h" +#include "theory/booleans/theory_bool_rewriter.h" + +using namespace CVC4::prop; +using namespace CVC4::theory::bv::utils; +namespace CVC4 { +namespace theory { +namespace bv { + +/* + Purely debugging + */ + +Bits* rewriteBits(const Bits& bits) { + Bits* newbits = new Bits(); + for (unsigned i = 0; i < bits.size(); ++i) { + newbits->push_back(Rewriter::rewrite(bits[i])); + } + return newbits; +} + +Node rewrite(Node node) { + return Rewriter::rewrite(node); +} + +/* + Various helper functions that get called by the bitblasting procedures + */ + +void inline extractBits(const Bits& b, Bits& dest, unsigned lo, unsigned hi) { + Assert ( lo < b.size() && hi < b.size() && lo <= hi); + for (unsigned i = lo; i <= hi; ++i) { + dest.push_back(b[i]); + } +} + +void inline negateBits(const Bits& bits, Bits& negated_bits) { + for(int i = 0; i < bits.size(); ++i) { + negated_bits.push_back(utils::mkNot(bits[i])); + } +} + +bool inline isZero(const Bits& bits) { + for(int i = 0; i < bits.size(); ++i) { + if(bits[i] != mkFalse()) { + return false; + } + } + return true; +} + +void inline rshift(Bits& bits, unsigned amount) { + for (unsigned i = 0; i < bits.size() - amount; ++i) { + bits[i] = bits[i+amount]; + } + for(unsigned i = bits.size() - amount; i < bits.size(); ++i) { + bits[i] = mkFalse(); + } +} + +void inline lshift(Bits& bits, unsigned amount) { + for (int i = bits.size() - 1; i >= amount ; --i) { + bits[i] = bits[i-amount]; + } + for(unsigned i = 0; i < amount; ++i) { + bits[i] = mkFalse(); + } +} + +void inline makeZero(Bits& bits, unsigned width) { + Assert(bits.size() == 0); + for(unsigned i = 0; i < width; ++i) { + bits.push_back(mkFalse()); + } +} + + +/** + * Constructs a simple ripple carry adder + * + * @param a first term to be added + * @param b second term to be added + * @param sum the sum + * @param carry the carry-in bit + * + * @return the carry-out + */ +Node inline rippleCarryAdder(const Bits&a, const Bits& b, Bits& res, Node carry) { + Assert(res.size() == 0 && a.size() == b.size()); + + for (unsigned i = 0 ; i < a.size(); ++i) { + Node sum = mkXor(mkXor(a[i], b[i]), carry); + carry = mkOr( mkAnd(a[i], b[i]), + mkAnd( mkXor(a[i], b[i]), + carry)); + res.push_back(sum); + } + + return carry; +} + + +Node inline uLessThanBB(const Bits&a, const Bits& b, bool orEqual) { + Assert (a.size() && b.size()); + + Node res = mkNode(kind::AND, mkNode(kind::NOT, a[0]), b[0]); + + if(orEqual) { + res = mkNode(kind::OR, res, mkNode(kind::IFF, a[0], b[0])); + } + + for (unsigned i = 1; i < a.size(); ++i) { + // a < b iff ( a[i] <-> b[i] AND a[i-1:0] < b[i-1:0]) OR (~a[i] AND b[i]) + res = mkNode(kind::OR, + mkNode(kind::AND, mkNode(kind::IFF, a[i], b[i]), res), + mkNode(kind::AND, mkNode(kind::NOT, a[i]), b[i])); + } + return res; +} + +Node inline sLessThanBB(const Bits&a, const Bits& b, bool orEqual) { + Assert (a.size() && b.size()); + if (a.size() == 1) { + if(orEqual) { + return mkNode(kind::OR, + mkNode(kind::IFF, a[0], b[0]), + mkNode(kind::AND, a[0], mkNode(kind::NOT, b[0]))); + } + + return mkNode(kind::AND, a[0], mkNode(kind::NOT, b[0])); + } + unsigned n = a.size() - 1; + Bits a1, b1; + extractBits(a, a1, 0, n-1); + extractBits(b, b1, 0, n-1); + + // unsigned comparison of the first n-1 bits + Node ures = uLessThanBB(a1, b1, orEqual); + Node res = mkNode(kind::OR, + // a b have the same sign + mkNode(kind::AND, + mkNode(kind::IFF, a[n], b[n]), + ures), + // a is negative and b positive + mkNode(kind::AND, + a[n], + mkNode(kind::NOT, b[n]))); + return res; +} + + +/* + Atom bitblasting strategies + */ + + +Node UndefinedAtomBBStrategy(TNode node, Bitblaster* bb) { + Debug("bitvector") << "TheoryBV::Bitblaster Undefined bitblasting strategy for kind: " + << node.getKind() << "\n"; + Unreachable(); +} + +Node DefaultEqBB(TNode node, Bitblaster* bb) { + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + + Assert(node.getKind() == kind::EQUAL); + Bits lhs, rhs; + bb->bbTerm(node[0], lhs); + bb->bbTerm(node[1], rhs); + + Assert(lhs.size() == rhs.size()); + + NodeManager* nm = NodeManager::currentNM(); + + std::vector bits_eq; + for (unsigned i = 0; i < lhs.size(); i++) { + Node bit_eq = nm->mkNode(kind::IFF, lhs[i], rhs[i]); + bits_eq.push_back(bit_eq); + } + Node bv_eq = utils::mkAnd(bits_eq); + return bv_eq; +} + + +Node AdderUltBB(TNode node, Bitblaster* bb) { + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_ULT); + Bits a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + Assert(a.size() == b.size()); + + // a < b <=> ~ (add(a, ~b, 1).carry_out) + Bits not_b; + negateBits(b, not_b); + Node carry = mkTrue(); + + for (unsigned i = 0 ; i < a.size(); ++i) { + carry = mkOr( mkAnd(a[i], not_b[i]), + mkAnd( mkXor(a[i], not_b[i]), + carry)); + } + return mkNot(carry); +} + + +Node DefaultUltBB(TNode node, Bitblaster* bb) { + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_ULT); + Bits a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + Assert(a.size() == b.size()); + + // construct bitwise comparison + Node res = uLessThanBB(a, b, false); + return res; +} + +Node DefaultUleBB(TNode node, Bitblaster* bb){ + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_ULE); + Bits a, b; + + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + Assert(a.size() == b.size()); + // construct bitwise comparison + Node res = uLessThanBB(a, b, true); + return res; +} + +Node DefaultUgtBB(TNode node, Bitblaster* bb){ + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + // should be rewritten + Unimplemented(); +} +Node DefaultUgeBB(TNode node, Bitblaster* bb){ + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + // should be rewritten + Unimplemented(); +} + +Node DefaultSltBB(TNode node, Bitblaster* bb){ + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + + Bits a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + Assert(a.size() == b.size()); + + Node res = sLessThanBB(a, b, false); + return res; +} + +Node DefaultSleBB(TNode node, Bitblaster* bb){ + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + + Bits a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + Assert(a.size() == b.size()); + + Node res = sLessThanBB(a, b, true); + return res; +} + +Node DefaultSgtBB(TNode node, Bitblaster* bb){ + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + // should be rewritten + Unimplemented(); +} + +Node DefaultSgeBB(TNode node, Bitblaster* bb){ + Debug("bitvector-bb") << "Bitblasting node " << node << "\n"; + // should be rewritten + Unimplemented(); +} + + +/// Term bitblasting strategies + +void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector") << "theory::bv:: Undefined bitblasting strategy for kind: " + << node.getKind() << "\n"; + Unreachable(); +} + +void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) { + Assert (node.getKind() == kind::VARIABLE); + Assert(bits.size() == 0); + + for (unsigned i = 0; i < utils::getSize(node); ++i) { + bits.push_back(utils::mkBitOf(node, i)); + } + + Debug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << " with bits " << toString(bits); +} + +void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultConstBB bitblasting " << node << "\n"; + Assert(node.getKind() == kind::CONST_BITVECTOR); + Assert(bits.size() == 0); + + NodeManager* nm = NodeManager::currentNM(); + for (unsigned i = 0; i < utils::getSize(node); ++i) { + Integer bit = node.getConst().extract(i, i).getValue(); + if(bit == Integer(0)){ + bits.push_back(utils::mkFalse()); + } else { + Assert (bit == Integer(1)); + bits.push_back(utils::mkTrue()); + } + } + Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; +} + + +void DefaultNotBB (TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultNotBB bitblasting " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_NOT); + Assert(bits.size() == 0); + Bits bv; + bb->bbTerm(node[0], bv); + negateBits(bv, bits); +} + +void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultConcatBB bitblasting " << node << "\n"; + Assert(bits.size() == 0); + + Assert (node.getKind() == kind::BITVECTOR_CONCAT); + for (int i = node.getNumChildren() -1 ; i >= 0; --i ) { + TNode current = node[i]; + Bits current_bits; + bb->bbTerm(current, current_bits); + + for(unsigned j = 0; j < utils::getSize(current); ++j) { + bits.push_back(current_bits[j]); + } + } + Assert (bits.size() == utils::getSize(node)); + Debug("bitvector-bb") << "with bits: " << toString(bits) << "\n"; +} + + +void DefaultAndBB (TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultAndBB bitblasting " << node << "\n"; + + Assert(node.getNumChildren() == 2 && + node.getKind() == kind::BITVECTOR_AND && + bits.size() == 0); + + Bits lhs, rhs; + bb->bbTerm(node[0], rhs); + bb->bbTerm(node[1], lhs); + + Assert (lhs.size() == rhs.size()); + for (unsigned i = 0; i < lhs.size(); ++i) { + bits.push_back(utils::mkAnd(lhs[i], rhs[i])); + } + +} + +void DefaultOrBB (TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultOrBB bitblasting " << node << "\n"; + + Assert(node.getNumChildren() == 2 && + node.getKind() == kind::BITVECTOR_OR && + bits.size() == 0); + + Bits lhs, rhs; + bb->bbTerm(node[0], lhs); + bb->bbTerm(node[1], rhs); + Assert(lhs.size() == rhs.size()); + + for (unsigned i = 0; i < lhs.size(); ++i) { + bits.push_back(utils::mkOr(lhs[i], rhs[i])); + } +} + +void DefaultXorBB (TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultXorBB bitblasting " << node << "\n"; + + Assert(node.getNumChildren() == 2 && + node.getKind() == kind::BITVECTOR_XOR && + bits.size() == 0); + + Bits lhs, rhs; + bb->bbTerm(node[0], lhs); + bb->bbTerm(node[1], rhs); + Assert(lhs.size() == rhs.size()); + + for (unsigned i = 0; i < lhs.size(); ++i) { + bits.push_back(utils::mkXor(lhs[i], rhs[i])); + } +} + +void DefaultXnorBB (TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultXnorBB bitblasting " << node << "\n"; + + Assert(node.getNumChildren() == 2 && + node.getKind() == kind::BITVECTOR_XNOR && + bits.size() == 0); + Bits lhs, rhs; + bb->bbTerm(node[0], lhs); + bb->bbTerm(node[1], rhs); + Assert(lhs.size() == rhs.size()); + + for (unsigned i = 0; i < lhs.size(); ++i) { + bits.push_back(utils::mkNode(kind::IFF, lhs[i], rhs[i])); + } +} + + +void DefaultNandBB (TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector") << "theory::bv:: Unimplemented kind " + << node.getKind() << "\n"; + Unimplemented(); +} +void DefaultNorBB (TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector") << "theory::bv:: Unimplemented kind " + << node.getKind() << "\n"; + Unimplemented(); +} +void DefaultCompBB (TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector") << "theory::bv:: DefaultCompBB bitblasting "<< node << "\n"; + + Assert(getSize(node) == 1 && bits.size() == 0 && node.getKind() == kind::BITVECTOR_COMP); + Bits a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + + std::vector bit_eqs; + NodeManager* nm = NodeManager::currentNM(); + for (unsigned i = 0; i < a.size(); ++i) { + Node eq = nm->mkNode(kind::IFF, a[i], b[i]); + bit_eqs.push_back(eq); + } + Node a_eq_b = mkAnd(bit_eqs); + bits.push_back(a_eq_b); +} + +void DefaultMultBB (TNode node, Bits& res, Bitblaster* bb) { + Debug("bitvector") << "theory::bv:: DefaultMultBB bitblasting "<< node << "\n"; + Assert(res.size() == 0 && + node.getKind() == kind::BITVECTOR_MULT); + Bits a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + + // constructs a simple shift and add multiplier building the result in + // in res + + for (unsigned i = 0; i < a.size(); ++i) { + res.push_back(mkNode(kind::AND, b[0], a[i])); + } + + for(unsigned k = 1; k < res.size(); ++k) { + Node carry_in = mkFalse(); + Node carry_out; + for(unsigned j = 0; j < res.size() -k; ++j) { + Node aj = mkAnd(a[j], b[k]); + carry_out = mkOr(mkAnd(res[j+k], aj), + mkAnd( mkXor(res[j+k], aj), carry_in)); + res[j+k] = mkXor(mkXor(res[j+k], aj), carry_in); + carry_in = carry_out; + } + } + Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; +} + +void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaulPlusBB bitblasting " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_PLUS && + res.size() == 0); + + Bits a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + + Assert(a.size() == b.size() && utils::getSize(node) == a.size()); + rippleCarryAdder(a, b, res, mkFalse()); +} + + +void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefautSubBB bitblasting " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_SUB && bits.size() == 0); + + Bits a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + Assert(a.size() == b.size() && utils::getSize(node) == a.size()); + + // bvsub a b = adder(a, ~b, 1) + Bits not_b; + negateBits(b, not_b); + Node carry = utils::mkTrue(); + rippleCarryAdder(a, not_b, bits, mkTrue()); +} + +void DefaultNegBB (TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefautNegBB bitblasting " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_NEG); + + Bits a; + bb->bbTerm(node[0], a); + Assert(utils::getSize(node) == a.size()); + + // -a = add(~a, 0, 1). + Bits not_a; + negateBits(a, not_a); + Bits zero; + makeZero(zero, getSize(node)); + + rippleCarryAdder(not_a, zero, bits, mkTrue()); +} + +void uDivModRec(const Bits& a, const Bits& b, Bits& q, Bits& r, unsigned rec_width) { + Assert( q.size() == 0 && r.size() == 0); + + if(rec_width == 0 || isZero(a)) { + makeZero(q, a.size()); + makeZero(r, a.size()); + return; + } + + Bits q1, r1; + Bits a1 = a; + rshift(a1, 1); + + uDivModRec(a1, b, q1, r1, rec_width - 1); + // shift the quotient and remainder (i.e. multiply by two) and add 1 to remainder if a is odd + lshift(q1, 1); + lshift(r1, 1); + + + Node is_odd = mkNode(kind::IFF, a[0], mkTrue()); + Node one_if_odd = mkNode(kind::ITE, is_odd, mkTrue(), mkFalse()); + + Bits zero; + makeZero(zero, b.size()); + + Bits r1_shift_add; + // account for a being odd + rippleCarryAdder(r1, zero, r1_shift_add, one_if_odd); + // now check if the remainder is greater than b + Bits not_b; + negateBits(b, not_b); + Bits r_minus_b; + Node co1; + // use adder because we need r_minus_b anyway + co1 = rippleCarryAdder(r1_shift_add, not_b, r_minus_b, mkTrue()); + // sign is true if r1 < b + Node sign = mkNode(kind::NOT, co1); + + q1[0] = mkNode(kind::ITE, sign, q1[0], mkTrue()); + + // would be nice to have a high level ITE instead of bitwise + for(unsigned i = 0; i < a.size(); ++i) { + r1_shift_add[i] = mkNode(kind::ITE, sign, r1_shift_add[i], r_minus_b[i]); + } + + // check if a < b + + Bits a_minus_b; + Node co2 = rippleCarryAdder(a, not_b, a_minus_b, mkTrue()); + // Node a_lt_b = a_minus_b.back(); + Node a_lt_b = mkNode(kind::NOT, co2); + + for(unsigned i = 0; i < a.size(); ++i) { + Node qval = mkNode(kind::ITE, a_lt_b, mkFalse(), q1[i]); + Node rval = mkNode(kind::ITE, a_lt_b, a[i], r1_shift_add[i]); + q.push_back(qval); + r.push_back(rval); + } + +} + +void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefautUdivBB bitblasting " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_UDIV && q.size() == 0); + + Bits a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + + Bits r; + uDivModRec(a, b, q, r, getSize(node)); + + // cache the remainder in case we need it later + Node remainder = mkNode(kind::BITVECTOR_UREM, node[0], node[1]); + bb->cacheTermDef(remainder, r); +} + +void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefautUremBB bitblasting " << node << "\n"; + Assert(node.getKind() == kind::BITVECTOR_UREM && rem.size() == 0); + + Bits a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + + Bits q; + uDivModRec(a, b, q, rem, getSize(node)); + + // cache the quotient in case we need it later + Node quotient = mkNode(kind::BITVECTOR_UDIV, node[0], node[1]); + bb->cacheTermDef(quotient, q); +} + + +void DefaultSdivBB (TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector") << "theory::bv:: Unimplemented kind " + << node.getKind() << "\n"; + Unimplemented(); +} +void DefaultSremBB (TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector") << "theory::bv:: Unimplemented kind " + << node.getKind() << "\n"; + Unimplemented(); +} +void DefaultSmodBB (TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector") << "theory::bv:: Unimplemented kind " + << node.getKind() << "\n"; + Unimplemented(); +} + +void DefaultShlBB (TNode node, Bits& res, Bitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultShlBB bitblasting " << node << "\n"; + Assert (node.getKind() == kind::BITVECTOR_SHL && + res.size() == 0); + Bits a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + + res = a; + Bits prev_res; + + for(unsigned s = 0; s < b.size(); ++s) { + // barrel shift stage: at each stage you can either shift by 2^s bits + // or leave the previous stage untouched + prev_res = res; + unsigned threshold = pow(2, s); + for(unsigned i = 0; i < a.size(); ++i) { + if (i < threshold) { + // if b[s] is true then we must have shifted by at least 2^b bits so + // all bits bellow 2^s will be 0, otherwise just use previous shift value + res[i] = mkNode(kind::ITE, b[s], mkFalse(), prev_res[i]); + } else { + // if b[s]= 0, use previous value, otherwise shift by threshold bits + Assert(i >= threshold); + res[i] = mkNode(kind::ITE, mkNot(b[s]), prev_res[i], prev_res[i-threshold]); + } + } + } + Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; +} + +void DefaultLshrBB (TNode node, Bits& res, Bitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultLshrBB bitblasting " << node << "\n"; + Assert (node.getKind() == kind::BITVECTOR_LSHR && + res.size() == 0); + Bits a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + + res = a; + Bits prev_res; + + for(int s = 0; s < b.size(); ++s) { + // barrel shift stage: at each stage you can either shift by 2^s bits + // or leave the previous stage untouched + prev_res = res; + int threshold = pow(2, s); + for(int i = 0; i < a.size(); ++i) { + if (i + threshold >= a.size()) { + // if b[s] is true then we must have shifted by at least 2^b bits so + // all bits above 2^s will be 0, otherwise just use previous shift value + res[i] = mkNode(kind::ITE, b[s], mkFalse(), prev_res[i]); + } else { + // if b[s]= 0, use previous value, otherwise shift by threshold bits + Assert (i+ threshold < a.size()); + res[i] = mkNode(kind::ITE, mkNot(b[s]), prev_res[i], prev_res[i+threshold]); + } + } + } + Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; +} + +void DefaultAshrBB (TNode node, Bits& res, Bitblaster* bb) { + + Debug("bitvector-bb") << "theory::bv::DefaultAshrBB bitblasting " << node << "\n"; + Assert (node.getKind() == kind::BITVECTOR_ASHR && + res.size() == 0); + Bits a, b; + bb->bbTerm(node[0], a); + bb->bbTerm(node[1], b); + + res = a; + TNode sign_bit = a.back(); + Bits prev_res; + + for(int s = 0; s < b.size(); ++s) { + // barrel shift stage: at each stage you can either shift by 2^s bits + // or leave the previous stage untouched + prev_res = res; + int threshold = pow(2, s); + for(int i = 0; i < a.size(); ++i) { + if (i + threshold >= a.size()) { + // if b[s] is true then we must have shifted by at least 2^b bits so + // all bits above 2^s will be the sign bit, otherwise just use previous shift value + res[i] = mkNode(kind::ITE, b[s], sign_bit, prev_res[i]); + } else { + // if b[s]= 0, use previous value, otherwise shift by threshold bits + Assert (i+ threshold < a.size()); + res[i] = mkNode(kind::ITE, mkNot(b[s]), prev_res[i], prev_res[i+threshold]); + } + } + } + Debug("bitvector-bb") << "with bits: " << toString(res) << "\n"; + +} + +void DefaultExtractBB (TNode node, Bits& bits, Bitblaster* bb) { + Assert (node.getKind() == kind::BITVECTOR_EXTRACT); + Assert(bits.size() == 0); + + Bits base_bits; + bb->bbTerm(node[0], base_bits); + unsigned high = utils::getExtractHigh(node); + unsigned low = utils::getExtractLow(node); + + for (unsigned i = low; i <= high; ++i) { + bits.push_back(base_bits[i]); + } + Assert (bits.size() == high - low + 1); + + Debug("bitvector-bb") << "theory::bv::DefaultExtractBB bitblasting " << node << "\n"; + Debug("bitvector-bb") << " with bits " << toString(bits); + +} + + +void DefaultRepeatBB (TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector") << "theory::bv:: Unimplemented kind " + << node.getKind() << "\n"; + // this should be rewritten + Unimplemented(); +} + +void DefaultZeroExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) { + + Debug("bitvector-bb") << "theory::bv::DefaultZeroExtendBB bitblasting " << node << "\n"; + + // this should be rewritten + Unimplemented(); + +} + +void DefaultSignExtendBB (TNode node, Bits& res_bits, Bitblaster* bb) { + Debug("bitvector-bb") << "theory::bv::DefaultSignExtendBB bitblasting " << node << "\n"; + + Assert (node.getKind() == kind::BITVECTOR_SIGN_EXTEND && + res_bits.size() == 0); + + Bits bits; + bb->bbTerm(node[0], bits); + + TNode sign_bit = bits.back(); + unsigned amount = node.getOperator().getConst().signExtendAmount; + + for (unsigned i = 0; i < bits.size(); ++i ) { + res_bits.push_back(bits[i]); + } + + for (unsigned i = 0 ; i < amount ; ++i ) { + res_bits.push_back(sign_bit); + } + + Assert (res_bits.size() == amount + bits.size()); +} + +void DefaultRotateRightBB (TNode node, Bits& res, Bitblaster* bb) { + Debug("bitvector") << "theory::bv:: Unimplemented kind " + << node.getKind() << "\n"; + + Unimplemented(); +} + +void DefaultRotateLeftBB (TNode node, Bits& bits, Bitblaster* bb) { + Debug("bitvector") << "theory::bv:: Unimplemented kind " + << node.getKind() << "\n"; + Unimplemented(); +} + + +} +} +} + + diff --git a/src/theory/bv/bitblast_strategies.h b/src/theory/bv/bitblast_strategies.h new file mode 100644 index 000000000..504755e6c --- /dev/null +++ b/src/theory/bv/bitblast_strategies.h @@ -0,0 +1,112 @@ +/********************* */ +/*! \file bitblast_strategies.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of bitblasting functions for various operators. + ** + ** Implementation of bitblasting functions for various operators. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BITBLAST__STRATEGIES_H +#define __CVC4__BITBLAST__STRATEGIES_H + + +#include "expr/node.h" +#include "prop/sat_module.h" + +namespace CVC4 { + + +namespace theory { +namespace bv { + +class Bitblaster; + + +typedef std::vector Bits; + + +/** + * Default Atom Bitblasting strategies: + * + * @param node the atom to be bitblasted + * @param markerLit the marker literal corresponding to the atom + * @param bb the bitblaster + */ + +Node UndefinedAtomBBStrategy (TNode node, Bitblaster* bb); +Node DefaultEqBB(TNode node, Bitblaster* bb); + +Node DefaultUltBB(TNode node, Bitblaster* bb); +Node DefaultUleBB(TNode node, Bitblaster* bb); +Node DefaultUgtBB(TNode node, Bitblaster* bb); +Node DefaultUgeBB(TNode node, Bitblaster* bb); + +Node DefaultSltBB(TNode node, Bitblaster* bb); +Node DefaultSleBB(TNode node, Bitblaster* bb); +Node DefaultSgtBB(TNode node, Bitblaster* bb); +Node DefaultSgeBB(TNode node, Bitblaster* bb); + +/// other modes +Node AdderUltBB(TNode node, Bitblaster* bb); + + + +/** + * Default Term Bitblasting strategies + * + * @param node the term to be bitblasted + * @param bb the bitblaster in which the clauses are added + * + * @return the bits representing the new term + */ + +void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb); + +void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultNotBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultConcatBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultAndBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultOrBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultXorBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultXnorBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultNandBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultNorBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultCompBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultMultBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultPlusBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultNegBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultUdivBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultUremBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultSdivBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultSremBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultSmodBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultShlBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultLshrBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultAshrBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultExtractBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultRepeatBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultZeroExtendBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultSignExtendBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultRotateRightBB (TNode node, Bits& bits, Bitblaster* bb); +void DefaultRotateLeftBB (TNode node, Bits& bits, Bitblaster* bb); + + +} +} +} + +#endif diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp new file mode 100644 index 000000000..22a679693 --- /dev/null +++ b/src/theory/bv/bv_sat.cpp @@ -0,0 +1,300 @@ +/********************* */ +/*! \file bv_sat.cpp + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** + **/ + +#include "bv_sat.h" +#include "theory_bv_utils.h" +#include "theory/rewriter.h" +#include "prop/cnf_stream.h" +#include "prop/sat_module.h" + +using namespace std; + +using namespace CVC4::theory::bv::utils; +using namespace CVC4::context; +using namespace CVC4::prop; + +namespace CVC4 { +namespace theory { +namespace bv{ + + +std::string toString(Bits& bits) { + ostringstream os; + for (int i = bits.size() - 1; i >= 0; --i) { + TNode bit = bits[i]; + if (bit.getKind() == kind::CONST_BOOLEAN) { + os << (bit.getConst() ? "1" : "0"); + } else { + os << bit<< " "; + } + } + os <<"\n"; + + return os.str(); +} +/////// Bitblaster + +Bitblaster::Bitblaster(context::Context* c) : + d_termCache(), + d_bitblastedAtoms(), + d_assertedAtoms(c), + d_statistics() + { + d_satSolver = prop::SatSolverFactory::createMinisat(); + d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar()); + + // initializing the bit-blasting strategies + initAtomBBStrategies(); + initTermBBStrategies(); + } + + +/** + * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver + * NOTE: duplicate clauses are not detected because of marker literal + * @param node the atom to be bitblasted + * + */ +void Bitblaster::bbAtom(TNode node) { + if (hasBBAtom(node)) { + return; + } + + // the bitblasted definition of the atom + Node atom_bb = d_atomBBStrategies[node.getKind()](node, this); + // asserting that the atom is true iff the definition holds + Node atom_definition = mkNode(kind::IFF, node, atom_bb); + // do boolean simplifications if possible + Node rewritten = Rewriter::rewrite(atom_definition); + d_cnfStream->convertAndAssert(rewritten, true, false); + d_bitblastedAtoms.insert(node); +} + + +void Bitblaster::bbTerm(TNode node, Bits& bits) { + if (hasBBTerm(node)) { + getBBTerm(node, bits); + return; + } + + d_termBBStrategies[node.getKind()] (node, bits,this); + + Assert (bits.size() == utils::getSize(node)); + cacheTermDef(node, bits); +} + +/// Public methods + +/** + * Called from preregistration bitblasts the node + * + * @param node + * + * @return + */ +void Bitblaster::bitblast(TNode node) { + TimerStat::CodeTimer codeTimer(d_statistics.d_bitblastTimer); + + /// strip the not + if (node.getKind() == kind::NOT) { + node = node[0]; + } + + if (node.getKind() == kind::EQUAL || + node.getKind() == kind::BITVECTOR_ULT || + node.getKind() == kind::BITVECTOR_SLT || + node.getKind() == kind::BITVECTOR_ULE || + node.getKind() == kind::BITVECTOR_SLE ) + { + bbAtom(node); + } + else if (node.getKind() == kind::BITVECTOR_UGT || + node.getKind() == kind::BITVECTOR_UGE || + node.getKind() == kind::BITVECTOR_SGT || + node.getKind() == kind::BITVECTOR_SGE ) + { + Unhandled(node.getKind()); + } + else + { + Bits bits; + bbTerm(node, bits); + } +} + +/** + * Asserts the clauses corresponding to the atom to the Sat Solver + * by turning on the marker literal (i.e. setting it to false) + * @param node the atom to be aserted + * + */ + +void Bitblaster::assertToSat(TNode lit) { + // strip the not + TNode atom; + if (lit.getKind() == kind::NOT) { + atom = lit[0]; + } else { + atom = lit; + } + + Assert (hasBBAtom(atom)); + SatLiteral markerLit = d_cnfStream->getLiteral(atom); + + if(lit.getKind() == kind::NOT) { + markerLit = ~markerLit; + } + + Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n"; + Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal: " << markerLit << "\n"; + + d_assertedAtoms.push_back(markerLit); +} + +/** + * Calls the solve method for the Sat Solver. + * passing it the marker literals to be asserted + * + * @return true for sat, and false for unsat + */ + +bool Bitblaster::solve() { + return SatValTrue == d_satSolver->solve(d_assertedAtoms); +} + +void Bitblaster::getConflict(std::vector& conflict) { + SatClause conflictClause; + d_satSolver->getUnsatCore(conflictClause); + + for (unsigned i = 0; i < conflictClause.size(); i++) { + SatLiteral lit = conflictClause[i]; + TNode atom = d_cnfStream->getNode(lit); + Node not_atom; + if (atom.getKind() == kind::NOT) { + not_atom = atom[0]; + } else { + not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom); + } + conflict.push_back(not_atom); + } +} + + +/// Helper methods + + +void Bitblaster::initAtomBBStrategies() { + for (int i = 0 ; i < kind::LAST_KIND; ++i ) { + d_atomBBStrategies[i] = UndefinedAtomBBStrategy; + } + + /// setting default bb strategies for atoms + d_atomBBStrategies [ kind::EQUAL ] = DefaultEqBB; + d_atomBBStrategies [ kind::BITVECTOR_ULT ] = DefaultUltBB; + d_atomBBStrategies [ kind::BITVECTOR_ULE ] = DefaultUleBB; + d_atomBBStrategies [ kind::BITVECTOR_UGT ] = DefaultUgtBB; + d_atomBBStrategies [ kind::BITVECTOR_UGE ] = DefaultUgeBB; + d_atomBBStrategies [ kind::BITVECTOR_SLT ] = DefaultSltBB; + d_atomBBStrategies [ kind::BITVECTOR_SLE ] = DefaultSleBB; + d_atomBBStrategies [ kind::BITVECTOR_SGT ] = DefaultSgtBB; + d_atomBBStrategies [ kind::BITVECTOR_SGE ] = DefaultSgeBB; + +} + +void Bitblaster::initTermBBStrategies() { + for (int i = 0 ; i < kind::LAST_KIND; ++i ) { + d_termBBStrategies[i] = UndefinedTermBBStrategy; + } + + /// setting default bb strategies for terms: + d_termBBStrategies [ kind::VARIABLE ] = DefaultVarBB; + d_termBBStrategies [ kind::CONST_BITVECTOR ] = DefaultConstBB; + d_termBBStrategies [ kind::BITVECTOR_NOT ] = DefaultNotBB; + d_termBBStrategies [ kind::BITVECTOR_CONCAT ] = DefaultConcatBB; + d_termBBStrategies [ kind::BITVECTOR_AND ] = DefaultAndBB; + d_termBBStrategies [ kind::BITVECTOR_OR ] = DefaultOrBB; + d_termBBStrategies [ kind::BITVECTOR_XOR ] = DefaultXorBB; + d_termBBStrategies [ kind::BITVECTOR_XNOR ] = DefaultXnorBB; + d_termBBStrategies [ kind::BITVECTOR_NAND ] = DefaultNandBB ; + d_termBBStrategies [ kind::BITVECTOR_NOR ] = DefaultNorBB; + d_termBBStrategies [ kind::BITVECTOR_COMP ] = DefaultCompBB ; + d_termBBStrategies [ kind::BITVECTOR_MULT ] = DefaultMultBB; + d_termBBStrategies [ kind::BITVECTOR_PLUS ] = DefaultPlusBB; + d_termBBStrategies [ kind::BITVECTOR_SUB ] = DefaultSubBB; + d_termBBStrategies [ kind::BITVECTOR_NEG ] = DefaultNegBB; + d_termBBStrategies [ kind::BITVECTOR_UDIV ] = DefaultUdivBB; + d_termBBStrategies [ kind::BITVECTOR_UREM ] = DefaultUremBB; + d_termBBStrategies [ kind::BITVECTOR_SDIV ] = DefaultSdivBB; + d_termBBStrategies [ kind::BITVECTOR_SREM ] = DefaultSremBB; + d_termBBStrategies [ kind::BITVECTOR_SMOD ] = DefaultSmodBB; + d_termBBStrategies [ kind::BITVECTOR_SHL ] = DefaultShlBB; + d_termBBStrategies [ kind::BITVECTOR_LSHR ] = DefaultLshrBB; + d_termBBStrategies [ kind::BITVECTOR_ASHR ] = DefaultAshrBB; + d_termBBStrategies [ kind::BITVECTOR_EXTRACT ] = DefaultExtractBB; + d_termBBStrategies [ kind::BITVECTOR_REPEAT ] = DefaultRepeatBB; + d_termBBStrategies [ kind::BITVECTOR_ZERO_EXTEND ] = DefaultZeroExtendBB; + d_termBBStrategies [ kind::BITVECTOR_SIGN_EXTEND ] = DefaultSignExtendBB; + d_termBBStrategies [ kind::BITVECTOR_ROTATE_RIGHT ] = DefaultRotateRightBB; + d_termBBStrategies [ kind::BITVECTOR_ROTATE_LEFT ] = DefaultRotateLeftBB; + +} + +bool Bitblaster::hasBBAtom(TNode atom) { + return d_bitblastedAtoms.find(atom) != d_bitblastedAtoms.end(); +} + +void Bitblaster::cacheTermDef(TNode term, Bits def) { + Assert (d_termCache.find(term) == d_termCache.end()); + d_termCache[term] = def; +} + +bool Bitblaster::hasBBTerm(TNode node) { + return d_termCache.find(node) != d_termCache.end(); +} + +void Bitblaster::getBBTerm(TNode node, Bits& bits) { + + Assert (hasBBTerm(node)); + // copy? + bits = d_termCache[node]; +} + +Bitblaster::Statistics::Statistics() : + d_numTermClauses("theory::bv::NumberOfTermSatClauses", 0), + d_numAtomClauses("theory::bv::NumberOfAtomSatClauses", 0), + d_bitblastTimer("theory::bv::BitblastTimer") +{ + StatisticsRegistry::registerStat(&d_numTermClauses); + StatisticsRegistry::registerStat(&d_numAtomClauses); + StatisticsRegistry::registerStat(&d_bitblastTimer); +} + + +Bitblaster::Statistics::~Statistics() { + StatisticsRegistry::unregisterStat(&d_numTermClauses); + StatisticsRegistry::unregisterStat(&d_numAtomClauses); + StatisticsRegistry::unregisterStat(&d_bitblastTimer); +} + + + + +} /*bv namespace */ +} /* theory namespace */ +} /* CVC4 namespace*/ diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h new file mode 100644 index 000000000..9844cd982 --- /dev/null +++ b/src/theory/bv/bv_sat.h @@ -0,0 +1,144 @@ +/********************* */ +/*! \file bv_sat.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Wrapper around the SAT solver used for bitblasting + ** + ** Wrapper around the SAT solver used for bitblasting. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BV__SAT_H +#define __CVC4__BV__SAT_H + + +#include "expr/node.h" +#include +#include +#include +#include +#include + +#include "context/cdo.h" +#include "context/cdset.h" +#include "context/cdlist.h" + +#include "theory_bv_utils.h" +#include "util/stats.h" +#include "bitblast_strategies.h" + +#include "prop/sat_module.h" + +namespace CVC4 { + +// forward declarations +namespace prop { +class CnfStream; +class BVSatSolverInterface; +} + + +namespace theory { +namespace bv { + + +std::string toString (Bits& bits); + +/** + * The Bitblaster that manages the mapping between Nodes + * and their bitwise definition + * + */ + +typedef std::vector Bits; + +class Bitblaster { + + typedef __gnu_cxx::hash_map TermDefMap; + typedef __gnu_cxx::hash_set AtomSet; + + typedef void (*TermBBStrategy) (TNode, Bits&, Bitblaster*); + typedef Node (*AtomBBStrategy) (TNode, Bitblaster*); + + // sat solver used for bitblasting and associated CnfStream + prop::BVSatSolverInterface* d_satSolver; + prop::CnfStream* d_cnfStream; + + // caches and mappings + TermDefMap d_termCache; + AtomSet d_bitblastedAtoms; + + context::CDList d_assertedAtoms; /**< context dependent list storing the atoms + currently asserted by the DPLL SAT solver. */ + + /// helper methods + bool hasBBAtom(TNode node); + bool hasBBTerm(TNode node); + void getBBTerm(TNode node, Bits& bits); + + + + + /// function tables for the various bitblasting strategies indexed by node kind + TermBBStrategy d_termBBStrategies[kind::LAST_KIND]; + AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; + + // helper methods to initialize function tables + void initAtomBBStrategies(); + void initTermBBStrategies(); + + + void bbAtom(TNode node); + // division is bitblasted in terms of constraints + // so it needs to use private bitblaster interface + void bbUdiv(TNode node, Bits& bits); + void bbUrem(TNode node, Bits& bits); +public: + void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division + void bbTerm(TNode node, Bits& bits); + +public: + Bitblaster(context::Context* c); + ~Bitblaster() { + delete d_cnfStream; + delete d_satSolver; + } + + void assertToSat(TNode node); + bool solve(); + void bitblast(TNode node); + void getConflict(std::vector& conflict); + +private: + + + class Statistics { + public: + IntStat d_numTermClauses, d_numAtomClauses; + TimerStat d_bitblastTimer; + Statistics(); + ~Statistics(); + }; + + Statistics d_statistics; +}; + + + +} /* bv namespace */ + +} /* theory namespace */ + +} /* CVC4 namespace */ + +#endif /* __CVC4__BV__SAT_H */ diff --git a/src/theory/bv/bv_solver_types.cpp b/src/theory/bv/bv_solver_types.cpp new file mode 100644 index 000000000..2589e5712 --- /dev/null +++ b/src/theory/bv/bv_solver_types.cpp @@ -0,0 +1,78 @@ +/********************* */ +/*! \file bv_sat.cpp + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** + **/ + +#include "bv_solver_types.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +#ifdef BV_MINISAT +using namespace BVMinisat; +SatLit neg(const SatLit& lit) { + return ~lit; +} + +SatLit mkLit(SatVar var) { + return BVMinisat::mkLit(var, false); +} + +SatVar mkVar(SatLit lit) { + return BVMinisat::var(lit); +} +bool polarity(SatLit lit) { + return !(BVMinisat::sign(lit)); +} + + +std::string toStringLit(SatLit lit) { + std::ostringstream os; + os << (polarity(lit) ? "" : "-") << var(lit) + 1; + return os.str(); +} +#endif + +#ifdef BV_PICOSAT + +SatLit mkLit(SatVar var) { + return var; +} +SatVar mkVar(SatLit lit) { + return (lit > 0 ? lit : -lit); +} +bool polarity(SatLit lit) { + return (lit > 0); +} + +SatLit neg(const SatLit& lit) { + return -lit; +} + +std::string toStringLit(SatLit lit) { + std::ostringstream os; + os << (lit < 0 ? "-" : "") << lit; + return os.str(); +} + + +#endif + +} +} +} diff --git a/src/theory/bv/bv_solver_types.h b/src/theory/bv/bv_solver_types.h new file mode 100644 index 000000000..fb99ae4c6 --- /dev/null +++ b/src/theory/bv/bv_solver_types.h @@ -0,0 +1,185 @@ +//********************* */ +/*! \file bv_solver_types.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Definitions of the SatSolver literal and clause types + ** + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BV__SOLVER__TYPES_H +#define __CVC4__BV__SOLVER__TYPES_H + +#define BV_MINISAT +//#define BV_PICOSAT + +#ifdef BV_MINISAT /* BV_MINISAT if we are using the minisat solver for the theory of bitvectors*/ +#include "theory/bv/bvminisat/core/Solver.h" +#include "theory/bv/bvminisat/core/SolverTypes.h" +#include "theory/bv/bvminisat/simp/SimpSolver.h" +#endif /* BV_MINISAT */ + +#ifdef BV_PICOSAT /* BV_PICOSAT */ +#include "picosat/picosat.h" +#endif /* BV_PICOSAT */ + +#include "expr/node.h" +#include +#include +#include +#include +#include +#include "context/cdlist.h" +#include "util/stats.h" + + +namespace CVC4 { +namespace theory { +namespace bv { + +#endif /* BV_MINISAT */ + + + +// #ifdef BV_PICOSAT /* BV_PICOSAT */ +// /** +// * PICOSAT type-definitions +// * +// * +// */ + +// typedef int SatVar; +// typedef int SatLit; + +// std::string toStringLit(SatLit lit); + + +// SatLit neg(const SatLit& lit); + +// struct SatLitHash { +// static size_t hash (const SatLit& lit) { +// return (size_t) lit; +// } + +// }; + +// struct SatLitHashFunction { +// size_t operator()(SatLit lit) const { +// return (size_t) lit; +// } +// }; + +// struct SatLitLess{ +// static bool compare(const SatLit& x, const SatLit& y) +// { +// return x < y; +// } +// }; + +// #endif /* BV_PICOSAT */ + +// #ifdef BV_PICOSAT /* BV_PICOSAT */ + +// /** +// * Some helper functions that should be defined for each SAT solver supported +// * +// * +// * @return +// */ + +// SatLit mkLit(SatVar var); +// SatVar mkVar(SatLit lit); +// bool polarity(SatLit lit); + + +// /** +// * Wrapper to create the impression of a SatSolver class for Picosat +// * which is written in C +// */ + +// class SatSolver: public SatSolverInterface { +// int d_varCount; +// bool d_started; +// public: +// SatSolver() : +// d_varCount(0), +// d_started(false) +// { +// picosat_init(); /// call constructor +// picosat_enable_trace_generation(); // required for unsat cores +// } + +// ~SatSolver() { +// picosat_reset(); +// } + +// void addClause(const SatClause* cl) { +// Assert (cl); +// const SatClause& clause = *cl; +// for (unsigned i = 0; i < clause.size(); ++i ) { +// picosat_add(clause[i]); +// } +// picosat_add(0); // ends clause +// } + +// bool solve () { +// if(d_started) { +// picosat_remove_learned(100); +// } +// int res = picosat_sat(-1); // no decision limit +// // 0 UNKNOWN, 10 SATISFIABLE and 20 UNSATISFIABLE +// d_started = true; +// Assert (res == 10 || res == 20); +// return res == 10; +// } + +// bool solve(const context::CDList & assumps) { +// context::CDList::const_iterator it = assumps.begin(); +// for (; it!= assumps.end(); ++it) { +// picosat_assume(*it); +// } +// return solve (); +// } + +// SatVar newVar() { return ++d_varCount; } + +// void setUnremovable(SatLit lit) {}; + +// SatClause* getUnsatCore() { +// const int* failedAssumption = picosat_failed_assumptions(); +// Assert(failedAssumption); + +// SatClause* unsatCore = new SatClause(); +// while (*failedAssumption != 0) { +// SatLit lit = *failedAssumption; +// unsatCore->addLiteral(neg(lit)); +// ++failedAssumption; +// } +// unsatCore->sort(); +// return unsatCore; +// } +// }; + + +// #endif /* BV_PICOSAT */ + + + + +} /* bv namespace */ + +} /* theory namespace */ + +} /* CVC4 namespace */ + +#endif /* __CVC4__BV__SOLVER__TYPES_H */ diff --git a/src/theory/bv/equality_engine.cpp b/src/theory/bv/equality_engine.cpp deleted file mode 100644 index a4d2e6329..000000000 --- a/src/theory/bv/equality_engine.cpp +++ /dev/null @@ -1,27 +0,0 @@ -/********************* */ -/*! \file equality_engine.cpp - ** \verbatim - ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "theory/bv/equality_engine.h" - -using namespace CVC4::theory::bv; - -const size_t BitSizeTraits::id_null = (1u << BitSizeTraits::id_bits) - 1; -const size_t BitSizeTraits::trigger_id_null = (1u << BitSizeTraits::trigger_id_bits) - 1; - - diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h deleted file mode 100644 index 558fd2b7b..000000000 --- a/src/theory/bv/equality_engine.h +++ /dev/null @@ -1,844 +0,0 @@ -/********************* */ -/*! \file equality_engine.h - ** \verbatim - ** Original author: dejan - ** Major contributors: none - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_private.h" - -#pragma once - -#include -#include -#include - -#include "expr/node.h" -#include "context/cdo.h" -#include "util/output.h" -#include "util/stats.h" -#include "theory/rewriter.h" -#include "theory/bv/theory_bv_utils.h" - -namespace CVC4 { -namespace theory { -namespace bv { - -struct BitSizeTraits { - /** The null id */ - static const size_t id_null; // Defined in the cpp file (GCC bug) - /** The null trigger id */ - static const size_t trigger_id_null; - - /** Number of bits we use for the id */ - static const size_t id_bits = 24; - /** Number of bits we use for the size the equivalence class */ - static const size_t size_bits = 16; - /** Number of bits we use for the trigger id */ - static const size_t trigger_id_bits = 24; -}; - -class EqualityNode { - -public: - - /** The size of this equivalence class (if it's a representative) */ - size_t d_size : BitSizeTraits::size_bits; - - /** The id (in the eq-manager) of the representative equality node */ - size_t d_findId : BitSizeTraits::id_bits; - - /** The next equality node in this class */ - size_t d_nextId : BitSizeTraits::id_bits; - -public: - - /** - * Creates a new node, which is in a list of it's own. - */ - EqualityNode(size_t nodeId = BitSizeTraits::id_null) - : d_size(1), d_findId(nodeId), d_nextId(nodeId) {} - - /** Initialize the equality node */ - inline void init(size_t nodeId) { - d_size = 1; - d_findId = d_nextId = nodeId; - } - - /** - * Returns the next node in the class circular list. - */ - inline size_t getNext() const { - return d_nextId; - } - - /** - * Returns the size of this equivalence class (only valid if this is the representative). - */ - inline size_t getSize() const { - return d_size; - } - - /** - * Merges the two lists. If add size is true the size of this node is increased by the size of - * the other node, otherwise the size is decreased by the size of the other node. - */ - template - inline void merge(EqualityNode& other) { - size_t tmp = d_nextId; d_nextId = other.d_nextId; other.d_nextId = tmp; - if (addSize) { - d_size += other.d_size; - } else { - d_size -= other.d_size; - } - } - - /** - * Returns the class representative. - */ - inline size_t getFind() const { return d_findId; } - - /** - * Set the class representative. - */ - inline void setFind(size_t findId) { d_findId = findId; } -}; - -template -class EqualityEngine { - -public: - - /** Statistics about the equality engine instance */ - struct Statistics { - /** Total number of merges */ - IntStat mergesCount; - /** Number of terms managed by the system */ - IntStat termsCount; - /** Number of function terms managed by the system */ - IntStat functionTermsCount; - /** Number of times we performed a backtrack */ - IntStat backtracksCount; - - Statistics(std::string name) - : mergesCount(name + "::mergesCount", 0), - termsCount(name + "::termsCount", 0), - functionTermsCount(name + "functionTermsCoutn", 0), - backtracksCount(name + "::backtracksCount", 0) - { - StatisticsRegistry::registerStat(&mergesCount); - StatisticsRegistry::registerStat(&termsCount); - StatisticsRegistry::registerStat(&functionTermsCount); - StatisticsRegistry::registerStat(&backtracksCount); - } - - ~Statistics() { - StatisticsRegistry::unregisterStat(&mergesCount); - StatisticsRegistry::unregisterStat(&termsCount); - StatisticsRegistry::unregisterStat(&functionTermsCount); - StatisticsRegistry::unregisterStat(&backtracksCount); - } - }; - -private: - - /** The class to notify when a representative changes for a term */ - NotifyClass d_notify; - - /** Map from nodes to their ids */ - __gnu_cxx::hash_map d_nodeIds; - - /** Map from ids to the nodes */ - std::vector d_nodes; - - /** Map from ids to the equality nodes */ - std::vector d_equalityNodes; - - /** Number of asserted equalities we have so far */ - context::CDO d_assertedEqualitiesCount; - - /** - * We keep a list of asserted equalities. Not among original terms, but - * among the class representatives. - */ - struct Equality { - /** Left hand side of the equality */ - size_t lhs : BitSizeTraits::id_bits; - /** Right hand side of the equality */ - size_t rhs : BitSizeTraits::id_bits; - /** Equality constructor */ - Equality(size_t lhs = BitSizeTraits::id_null, size_t rhs = BitSizeTraits::id_null) - : lhs(lhs), rhs(rhs) {} - }; - - /** The ids of the classes we have merged */ - std::vector d_assertedEqualities; - - /** The reasons for the equalities */ - - /** - * An edge in the equality graph. This graph is an undirected graph (both edges added) - * containing the actual asserted equalities. - */ - class EqualityEdge { - - // The id of the RHS of this equality - size_t d_nodeId : BitSizeTraits::id_bits; - // The next edge - size_t d_nextId : BitSizeTraits::id_bits; - - public: - - EqualityEdge(size_t nodeId = BitSizeTraits::id_null, size_t nextId = BitSizeTraits::id_null) - : d_nodeId(nodeId), d_nextId(nextId) {} - - /** Returns the id of the next edge */ - inline size_t getNext() const { return d_nextId; } - - /** Returns the id of the target edge node */ - inline size_t getNodeId() const { return d_nodeId; } - }; - - /** - * All the equality edges (twice as many as the number of asserted equalities. If an equality - * t1 = t2 is asserted, the edges added are -> t2, -> t1 (in this order). Hance, having the index - * of one of the edges you can reconstruct the original equality. - */ - std::vector d_equalityEdges; - - /** - * Returns the string representation of the edges. - */ - std::string edgesToString(size_t edgeId) const; - - /** - * Reasons for equalities. - */ - std::vector d_equalityReasons; - - /** - * Map from a node to it's first edge in the equality graph. Edges are added to the front of the - * list which makes the insertion/backtracking easy. - */ - std::vector d_equalityGraph; - - /** Add an edge to the equality graph */ - inline void addGraphEdge(size_t t1, size_t t2, Node reason); - - /** Returns the equality node of the given node */ - inline EqualityNode& getEqualityNode(TNode node); - - /** Returns the equality node of the given node */ - inline EqualityNode& getEqualityNode(size_t nodeId); - - /** Returns the id of the node */ - inline size_t getNodeId(TNode node) const; - - /** Merge the class2 into class1 */ - void merge(EqualityNode& class1, EqualityNode& class2, std::vector& triggers); - - /** Undo the mereg of class2 into class1 */ - void undoMerge(EqualityNode& class1, EqualityNode& class2, size_t class2Id); - - /** Backtrack the information if necessary */ - void backtrack(); - - /** - * Data used in the BFS search through the equality graph. - */ - struct BfsData { - // The current node - size_t nodeId : BitSizeTraits::id_bits; - // The index of the edge we traversed - size_t edgeId : BitSizeTraits::id_bits; - // Index in the queue of the previous node. Shouldn't be too much of them, at most the size - // of the biggest equivalence class - size_t previousIndex : BitSizeTraits::size_bits; - - BfsData(size_t nodeId = BitSizeTraits::id_null, size_t edgeId = BitSizeTraits::id_null, size_t prev = 0) - : nodeId(nodeId), edgeId(edgeId), previousIndex(prev) {} - }; - - /** - * Trigger that will be updated - */ - struct Trigger { - /** The current class id of the LHS of the trigger */ - size_t classId : BitSizeTraits::id_bits; - /** Next trigger for class 1 */ - size_t nextTrigger : BitSizeTraits::id_bits; - - Trigger(size_t classId, size_t nextTrigger) - : classId(classId), nextTrigger(nextTrigger) {} - }; - - /** - * Vector of triggers (persistent and not-backtrackable). Triggers come in pairs for an - * equality trigger (t1, t2): one at position 2k for t1, and one at position 2k + 1 for t2. When - * updating triggers we always know where the other one is (^1). - */ - std::vector d_equalityTriggers; - - /** - * Trigger lists per node. The begin id changes as we merge, but the end always points to - * the actual end of the triggers for this node. - */ - std::vector d_nodeTriggers; - - /** - * Adds the trigger with triggerId to the beginning of the trigger list of the node with id nodeId. - */ - inline void addTriggerToList(size_t nodeId, size_t triggerId); - - /** Statistics */ - Statistics d_stats; - -public: - - /** - * Initialize the equality engine, given the owning class. This will initialize the notifier with - * the owner information. - */ - EqualityEngine(OwnerClass& owner, context::Context* context, std::string name) - : d_notify(owner), d_assertedEqualitiesCount(context, 0), d_stats(name) { - BVDebug("equality") << "EqualityEdge::EqualityEdge(): id_null = " << BitSizeTraits::id_null << - ", trigger_id_null = " << BitSizeTraits::trigger_id_null << std::endl; - } - - /** - * Adds a term to the term database. Returns the internal id of the term. - */ - size_t addTerm(TNode t); - - /** - * Check whether the node is already in the database. - */ - inline bool hasTerm(TNode t) const; - - /** - * Adds an equality t1 = t2 to the database. Returns false if any of the triggers failed, or a - * conflict was introduced. - */ - bool addEquality(TNode t1, TNode t2, Node reason); - - /** - * Returns the representative of the term t. - */ - inline TNode getRepresentative(TNode t) const; - - /** - * Returns true if the two nodes are in the same class. - */ - inline bool areEqual(TNode t1, TNode t2) const; - - /** - * Get an explanation of the equality t1 = t2. Returns the asserted equalities that - * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere - * else. TODO: mark the phantom equalities (skolems). - */ - void getExplanation(TNode t1, TNode t2, std::vector& equalities) const; - - /** - * Adds a notify trigger for equality t1 = t2, i.e. when t1 = t2 the notify will be called with - * (t1, t2). - */ - size_t addTrigger(TNode t1, TNode t2); - - /** - * Normalizes a term by finding the representative. If the representative can be decomposed (using - * UnionFindPreferences) it will try and recursively find the representatives, and substitute. - * Assumptions used in normalization are retruned in the set. - */ - Node normalize(TNode node, std::set& assumptions); - -private: - - /** Hash of normalizations to avioid cycles */ - typedef __gnu_cxx::hash_map normalization_cache; - normalization_cache d_normalizationCache; - - /** - * Same as above, but does cahcing to avoid loops. - */ - Node normalizeWithCache(TNode node, std::set& assumptions); - -}; - -template -size_t EqualityEngine::addTerm(TNode t) { - - BVDebug("equality") << "EqualityEngine::addTerm(" << t << ")" << std::endl; - - // If term already added, retrurn it's id - if (hasTerm(t)) return getNodeId(t); - - ++ d_stats.termsCount; - - // Register the new id of the term - size_t newId = d_nodes.size(); - d_nodeIds[t] = newId; - // Add the node to it's position - d_nodes.push_back(t); - // Add the trigger list for this node - d_nodeTriggers.push_back(BitSizeTraits::trigger_id_null); - // Add it to the equality graph - d_equalityGraph.push_back(BitSizeTraits::id_null); - // Add the equality node to the nodes - if (d_equalityNodes.size() <= newId) { - d_equalityNodes.resize(newId + 100); - } - d_equalityNodes[newId].init(newId); - // Return the id of the term - return newId; -} - -template -bool EqualityEngine::hasTerm(TNode t) const { - return d_nodeIds.find(t) != d_nodeIds.end(); -} - -template -size_t EqualityEngine::getNodeId(TNode node) const { - Assert(hasTerm(node), node.toString().c_str()); - return (*d_nodeIds.find(node)).second; -} - -template -EqualityNode& EqualityEngine::getEqualityNode(TNode t) { - return getEqualityNode(getNodeId(t)); -} - -template -EqualityNode& EqualityEngine::getEqualityNode(size_t nodeId) { - Assert(nodeId < d_equalityNodes.size()); - return d_equalityNodes[nodeId]; -} - -template -bool EqualityEngine::addEquality(TNode t1, TNode t2, Node reason) { - - BVDebug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl; - - // Backtrack if necessary - backtrack(); - - // Add the terms if they are not already in the database - size_t t1Id = getNodeId(t1); - size_t t2Id = getNodeId(t2); - - // Get the representatives - size_t t1classId = getEqualityNode(t1Id).getFind(); - size_t t2classId = getEqualityNode(t2Id).getFind(); - - // If already the same, we're done - if (t1classId == t2classId) return true; - - // Check for constants - if (d_nodes[t1classId].getMetaKind() == kind::metakind::CONSTANT && - d_nodes[t2classId].getMetaKind() == kind::metakind::CONSTANT) { - std::vector reasons; - getExplanation(t1, d_nodes[t1classId], reasons); - getExplanation(t2, d_nodes[t2classId], reasons); - reasons.push_back(reason); - d_notify.conflict(utils::mkAnd(reasons)); - return false; - } - - // Get the nodes of the representatives - EqualityNode& node1 = getEqualityNode(t1classId); - EqualityNode& node2 = getEqualityNode(t2classId); - - Assert(node1.getFind() == t1classId); - Assert(node2.getFind() == t2classId); - - // Depending on the merge preference (such as size), merge them - std::vector triggers; - if (UnionFindPreferences::mergePreference(d_nodes[t2classId], node2.getSize(), d_nodes[t1classId], node1.getSize())) { - BVDebug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << "): merging " << t1 << " into " << t2 << std::endl; - merge(node2, node1, triggers); - d_assertedEqualities.push_back(Equality(t2classId, t1classId)); - } else { - BVDebug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << "): merging " << t2 << " into " << t1 << std::endl; - merge(node1, node2, triggers); - d_assertedEqualities.push_back(Equality(t1classId, t2classId)); - } - - // Add the actuall equality to the equality graph - addGraphEdge(t1Id, t2Id, reason); - - // One more equality added - d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1; - - Assert(2*d_assertedEqualities.size() == d_equalityEdges.size()); - Assert(d_assertedEqualities.size() == d_assertedEqualitiesCount); - - // Notify the triggers - for (size_t i = 0, i_end = triggers.size(); i < i_end; ++ i) { - // Notify the trigger and exit if it fails - if (!d_notify(triggers[i])) return false; - } - - return true; -} - -template -TNode EqualityEngine::getRepresentative(TNode t) const { - - BVDebug("equality") << "EqualityEngine::getRepresentative(" << t << ")" << std::endl; - - Assert(hasTerm(t)); - - // Both following commands are semantically const - const_cast(this)->backtrack(); - size_t representativeId = const_cast(this)->getEqualityNode(t).getFind(); - - BVDebug("equality") << "EqualityEngine::getRepresentative(" << t << ") => " << d_nodes[representativeId] << std::endl; - - return d_nodes[representativeId]; -} - -template -bool EqualityEngine::areEqual(TNode t1, TNode t2) const { - BVDebug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ")" << std::endl; - - Assert(hasTerm(t1)); - Assert(hasTerm(t2)); - - // Both following commands are semantically const - const_cast(this)->backtrack(); - size_t rep1 = const_cast(this)->getEqualityNode(t1).getFind(); - size_t rep2 = const_cast(this)->getEqualityNode(t2).getFind(); - - BVDebug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ") => " << (rep1 == rep2 ? "true" : "false") << std::endl; - - return rep1 == rep2; -} - -template -void EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vector& triggers) { - - BVDebug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl; - - Assert(triggers.empty()); - - ++ d_stats.mergesCount; - - size_t class1Id = class1.getFind(); - size_t class2Id = class2.getFind(); - - // Update class2 representative information - size_t currentId = class2Id; - do { - // Get the current node - EqualityNode& currentNode = getEqualityNode(currentId); - - // Update it's find to class1 id - currentNode.setFind(class1Id); - - // Go through the triggers and inform if necessary - size_t currentTrigger = d_nodeTriggers[currentId]; - while (currentTrigger != BitSizeTraits::trigger_id_null) { - Trigger& trigger = d_equalityTriggers[currentTrigger]; - Trigger& otherTrigger = d_equalityTriggers[currentTrigger ^ 1]; - - // If the two are not already in the same class - if (otherTrigger.classId != trigger.classId) { - trigger.classId = class1Id; - // If they became the same, call the trigger - if (otherTrigger.classId == class1Id) { - // Id of the real trigger is half the internal one - triggers.push_back(currentTrigger >> 1); - } - } - - // Go to the next trigger - currentTrigger = trigger.nextTrigger; - } - - // Move to the next node - currentId = currentNode.getNext(); - - } while (currentId != class2Id); - - // Now merge the lists - class1.merge(class2); -} - -template -void EqualityEngine::undoMerge(EqualityNode& class1, EqualityNode& class2, size_t class2Id) { - - BVDebug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << ")" << std::endl; - - // Now unmerge the lists (same as merge) - class1.merge(class2); - - // Update class2 representative information - size_t currentId = class2Id; - do { - // Get the current node - EqualityNode& currentNode = getEqualityNode(currentId); - - // Update it's find to class1 id - currentNode.setFind(class2Id); - - // Go through the trigger list (if any) and undo the class - size_t currentTrigger = d_nodeTriggers[currentId]; - while (currentTrigger != BitSizeTraits::trigger_id_null) { - Trigger& trigger = d_equalityTriggers[currentTrigger]; - trigger.classId = class2Id; - currentTrigger = trigger.nextTrigger; - } - - // Move to the next node - currentId = currentNode.getNext(); - - } while (currentId != class2Id); - -} - -template -void EqualityEngine::backtrack() { - - // If we need to backtrack then do it - if (d_assertedEqualitiesCount < d_assertedEqualities.size()) { - - ++ d_stats.backtracksCount; - - BVDebug("equality") << "EqualityEngine::backtrack(): nodes" << std::endl; - - for (int i = (int)d_assertedEqualities.size() - 1, i_end = (int)d_assertedEqualitiesCount; i >= i_end; --i) { - // Get the ids of the merged classes - Equality& eq = d_assertedEqualities[i]; - // Undo the merge - undoMerge(d_equalityNodes[eq.lhs], d_equalityNodes[eq.rhs], eq.rhs); - } - - d_assertedEqualities.resize(d_assertedEqualitiesCount); - - BVDebug("equality") << "EqualityEngine::backtrack(): edges" << std::endl; - - for (int i = (int)d_equalityEdges.size() - 2, i_end = (int)(2*d_assertedEqualitiesCount); i >= i_end; i -= 2) { - EqualityEdge& edge1 = d_equalityEdges[i]; - EqualityEdge& edge2 = d_equalityEdges[i | 1]; - d_equalityGraph[edge2.getNodeId()] = edge1.getNext(); - d_equalityGraph[edge1.getNodeId()] = edge2.getNext(); - } - - d_equalityEdges.resize(2 * d_assertedEqualitiesCount); - d_equalityReasons.resize(d_assertedEqualitiesCount); - } - -} - -template -void EqualityEngine::addGraphEdge(size_t t1, size_t t2, Node reason) { - BVDebug("equality") << "EqualityEngine::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << ")" << std::endl; - size_t edge = d_equalityEdges.size(); - d_equalityEdges.push_back(EqualityEdge(t2, d_equalityGraph[t1])); - d_equalityEdges.push_back(EqualityEdge(t1, d_equalityGraph[t2])); - d_equalityGraph[t1] = edge; - d_equalityGraph[t2] = edge | 1; - d_equalityReasons.push_back(reason); -} - -template -std::string EqualityEngine::edgesToString(size_t edgeId) const { - std::stringstream out; - bool first = true; - while (edgeId != BitSizeTraits::id_null) { - const EqualityEdge& edge = d_equalityEdges[edgeId]; - if (!first) out << ","; - out << d_nodes[edge.getNodeId()]; - edgeId = edge.getNext(); - first = false; - } - return out.str(); -} - - -template -void EqualityEngine::getExplanation(TNode t1, TNode t2, std::vector& equalities) const { - Assert(getRepresentative(t1) == getRepresentative(t2)); - - BVDebug("equality") << "EqualityEngine::getExplanation(" << t1 << "," << t2 << ")" << std::endl; - - // If the nodes are the same, we're done - if (t1 == t2) return; - - const_cast(this)->backtrack(); - - // Queue for the BFS containing nodes - std::vector bfsQueue; - - // The id's of the nodes - size_t t1Id = getNodeId(t1); - size_t t2Id = getNodeId(t2); - - // Find a path from t1 to t2 in the graph (BFS) - bfsQueue.push_back(BfsData(t1Id, BitSizeTraits::id_null, 0)); - size_t currentIndex = 0; - while (true) { - // There should always be a path, and every node can be visited only once (tree) - Assert(currentIndex < bfsQueue.size()); - - // The next node to visit - BfsData current = bfsQueue[currentIndex]; - size_t currentNode = current.nodeId; - - BVDebug("equality") << "EqualityEngine::getExplanation(): currentNode = " << d_nodes[currentNode] << std::endl; - - // Go through the equality edges of this node - size_t currentEdge = d_equalityGraph[currentNode]; - - BVDebug("equality") << "EqualityEngine::getExplanation(): edges = " << edgesToString(currentEdge) << std::endl; - - while (currentEdge != BitSizeTraits::id_null) { - // Get the edge - const EqualityEdge& edge = d_equalityEdges[currentEdge]; - - // If not just the backwards edge - if ((currentEdge | 1u) != (current.edgeId | 1u)) { - - BVDebug("equality") << "EqualityEngine::getExplanation(): currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl; - - // Did we find the path - if (edge.getNodeId() == t2Id) { - - BVDebug("equality") << "EqualityEngine::getExplanation(): path found: " << std::endl; - - // Reconstruct the path - do { - // Add the actual equality to the vector - equalities.push_back(d_equalityReasons[currentEdge >> 1]); - BVDebug("equality") << "EqualityEngine::getExplanation(): adding: " << d_equalityReasons[currentEdge >> 1] << std::endl; - - // Go to the previous - currentEdge = bfsQueue[currentIndex].edgeId; - currentIndex = bfsQueue[currentIndex].previousIndex; - } while (currentEdge != BitSizeTraits::id_null); - - // Done - return; - } - - // Push to the visitation queue if it's not the backward edge - bfsQueue.push_back(BfsData(edge.getNodeId(), currentEdge, currentIndex)); - } - - // Go to the next edge - currentEdge = edge.getNext(); - } - - // Go to the next node to visit - ++ currentIndex; - } -} - -template -size_t EqualityEngine::addTrigger(TNode t1, TNode t2) { - - BVDebug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ")" << std::endl; - - Assert(hasTerm(t1)); - Assert(hasTerm(t2)); - - // Get the information about t1 - size_t t1Id = getNodeId(t1); - size_t t1TriggerId = d_nodeTriggers[t1Id]; - size_t t1classId = getEqualityNode(t1Id).getFind(); - - // Get the information about t2 - size_t t2Id = getNodeId(t2); - size_t t2TriggerId = d_nodeTriggers[t2Id]; - size_t t2classId = getEqualityNode(t2Id).getFind(); - - // Create the triggers - size_t t1NewTriggerId = d_equalityTriggers.size(); - size_t t2NewTriggerId = t1NewTriggerId | 1; - d_equalityTriggers.push_back(Trigger(t1classId, t1TriggerId)); - d_equalityTriggers.push_back(Trigger(t2classId, t2TriggerId)); - - // Add the trigger to the trigger graph - d_nodeTriggers[t1Id] = t1NewTriggerId; - d_nodeTriggers[t2Id] = t2NewTriggerId; - - BVDebug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => " << t1NewTriggerId / 2 << std::endl; - - // Return the global id of the trigger - return t1NewTriggerId / 2; -} - -template -Node EqualityEngine::normalize(TNode node, std::set& assumptions) { - d_normalizationCache.clear(); - Node result = Rewriter::rewrite(normalizeWithCache(node, assumptions)); - d_normalizationCache.clear(); - return result; -} - - -template -Node EqualityEngine::normalizeWithCache(TNode node, std::set& assumptions) { - - BVDebug("equality") << "EqualityEngine::normalize(" << node << ")" << push << std::endl; - - normalization_cache::iterator find = d_normalizationCache.find(node); - if (find != d_normalizationCache.end()) { - if (find->second.isNull()) { - // We are in a cycle - return node; - } else { - // Not in a cycle, return it - return find->second; - } - } else { - d_normalizationCache[node] = Node(); - } - - // Get the representative - Node result = hasTerm(node) ? getRepresentative(node) : node; - if (node != result) { - std::vector equalities; - getExplanation(result, node, equalities); - utils::getConjuncts(equalities, assumptions); - } - - // If asked, substitute the children with their representatives - if (UnionFindPreferences::descend(result)) { - // Make the builder for substitution - NodeBuilder<> builder; - builder << result.getKind(); - kind::MetaKind metaKind = result.getMetaKind(); - if (metaKind == kind::metakind::PARAMETERIZED) { - builder << result.getOperator(); - } - for (unsigned i = 0; i < result.getNumChildren(); ++ i) { - builder << normalizeWithCache(result[i], assumptions); - } - result = builder; - } - - BVDebug("equality") << "EqualityEngine::normalize(" << node << ") => " << result << pop << std::endl; - - // Cache the result for real now - d_normalizationCache[node] = result; - - return result; -} - -} // Namespace bv -} // Namespace theory -} // Namespace CVC4 - diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index d502c5ecb..36d25de2a 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -57,6 +57,12 @@ operator BITVECTOR_SLE 2 "bit-vector signed less than or equal" operator BITVECTOR_SGT 2 "bit-vector signed greater than" operator BITVECTOR_SGE 2 "signed greater than or equal" +constant BITVECTOR_BITOF_OP \ + ::CVC4::BitVectorBitOf \ + ::CVC4::BitVectorBitOfHashStrategy \ + "util/bitvector.h" \ + "operator for the bit-vector boolean bit extract" + constant BITVECTOR_EXTRACT_OP \ ::CVC4::BitVectorExtract \ ::CVC4::BitVectorExtractHashStrategy \ @@ -93,6 +99,7 @@ constant BITVECTOR_ROTATE_RIGHT_OP \ "util/bitvector.h" \ "operator for the bit-vector rotate right" +parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract" parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract" parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat" parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend" @@ -138,6 +145,7 @@ typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule +typerule BITVECTOR_BITOF ::CVC4::theory::bv::BitVectorBitOfTypeRule typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatRule typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule diff --git a/src/theory/bv/slice_manager.h b/src/theory/bv/slice_manager.h deleted file mode 100644 index 80ac98001..000000000 --- a/src/theory/bv/slice_manager.h +++ /dev/null @@ -1,677 +0,0 @@ -/********************* */ -/*! \file slice_manager.h - ** \verbatim - ** Original author: dejan - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -/* - * slice_manager.h - * - * Created on: Feb 16, 2011 - * Author: dejan - */ - -#include "cvc4_private.h" - -#pragma once - -#include "context/cdo.h" -#include "theory/bv/theory_bv_utils.h" -#include "theory/bv/equality_engine.h" -#include "theory/bv/cd_set_collection.h" - -#include -#include -#include - -namespace CVC4 { -namespace theory { -namespace bv { - -/** - * Representation of the slice points in tree. - */ -class slice_point -{ -public: - - /** Number of bits we use for the index of the slice */ - static const size_t s_slice_index_bits = 31; - /** Number of bits we use for the index of the slice_point in the slice memory (reference) */ - static const size_t s_slice_point_reference_bits = 32; - /** The null reference (maximal number in the given bits) */ - static const size_t null = (1llu << s_slice_point_reference_bits) - 1; - - /** Type of the reference for the outside world */ - typedef size_t reference_type; - - /** Type of the value for the outside world */ - typedef size_t value_type; - -private: - - /** The value of the slice point (bit index) */ - size_t d_value : s_slice_index_bits; - /** Is this the left child */ - size_t d_isLeftChild : 1; - /** Reference to the left in the tree */ - size_t d_left : s_slice_point_reference_bits; - /** Reference to the right of the tree */ - size_t d_right : s_slice_point_reference_bits; - /** Reference to the parent */ - size_t d_parent : s_slice_point_reference_bits; - -public: - - slice_point(size_t value, size_t left, size_t right, size_t parent, bool isLeftChild) - : d_value(value), d_isLeftChild(isLeftChild ? 1 : 0), d_left(left), d_right(right), d_parent(parent) {} - - bool isLeft() const { return d_isLeftChild == 1; } - bool isRight() const { return d_isLeftChild == 0; } - - bool hasLeft() const { return d_left != null; } - bool hasRight() const { return d_right != null; } - bool hasParent() const { return d_parent != null; } - - reference_type getLeft() const { return d_left; } - reference_type getRight() const { return d_right; } - reference_type getParent() const { return d_parent; } - - void removeLeft() { Assert(d_left != null); d_left = null; } - void removeRight() { Assert(d_right != null); d_right = null; } - - void setLeft(reference_type left) { Assert(d_left == null && left != null); d_left = left; } - void setRight(reference_type right) { Assert(d_right == null && right != null); d_right = right; } - - value_type getValue() const { return d_value; } -}; - -/** - * Slice manager should keep the database of slices for the core theory leaf terms, for example - * - * term core leaf terms - * ---------------------------------------------- - * (x + y)[31:0] x + y - * a[10:0]@a[11:10]@(b + c)[1:0] a, b, (b + c) - * (a << 5)[10] (a << 5) - * - * If an (dis-)equality is added to the system, we refine the slicing in order to align the extracts, for example - * - * equality slicing - * ---------------------------------------------- - * x = y x[32,0], y[32,0] - * x@y = z x[32,0], y[32,0], z[64,32,0] - * x@y = z, x[31:16] = y[15:0] x[32,16,0], y[32,16,0], z[64,48,32,16,0] - * - * As a result of the slicing the slicing equalities are added to the equality engine, using the (associative) - * concat function that is generated for the equality manager, for example - * - * equality added equalities - * ---------------------------------------------- - * x = y none - * x@y = z z = concat(z[63:32],z[31:0]) - * x@y = z, x[31:16] = y[15:0] z = concat(z[63:32],z[31:0]), - * z[63:32] = concat(z[63:48], z[47:32]), - * z[31:0] = concat(z[31:16], z[15:0]) - * - * In the last example, since concat is associative, the equality engine will know that z = concat(z[63:48], z[47:32], - * z[31:16], z[15:0]). - * - */ -template -class SliceManager { - -public: - - /** The references to backtrackable sets */ - typedef slice_point::reference_type set_reference; - - /** The set collection we'll be using */ - typedef context::BacktrackableSetCollection, slice_point, set_reference> set_collection; - - /** The map type from nodes to their references */ - typedef context::CDMap slicing_map; - - /** The equality engine theory of bit-vectors is using */ - typedef typename TheoryBitvector::BvEqualityEngine EqualityEngine; - -private: - - /** The theory of bitvectors */ - TheoryBitvector& d_theoryBitvector; - - /** The equality engine */ - EqualityEngine& d_equalityEngine; - - /** The collection of backtrackable sets */ - set_collection d_setCollection; - - /** - * A map from base nodes to slice points. For each node, the slice points are - * 0 = i_1 < i_2 < ... < i_n = size, and the slices are - * x[i_n-1:i_{n-1}]@x[i_{n-1}-1:i_{n-2}]@...@x[i_2-1:i_1] - * Each time we add a slict t = t1@t2@...@tn of a term (or a slice), we also notify the equality engine with an - * extra assertion. Since the equality engine is backtrackable, we will need to backtrack the slices accordingly. - */ - slicing_map d_nodeSlicing; - -public: - - SliceManager(TheoryBitvector& theoryBitvector, context::Context* context) - : d_theoryBitvector(theoryBitvector), - d_equalityEngine(theoryBitvector.getEqualityEngine()), - d_setCollection(context), - d_nodeSlicing(context) - { - } - - /** - * Adds the equality (lhs = rhs) to the slice manager. The equality is first normalized according to the equality - * manager, i.e. each base term is taken from the equality manager, replaced in, and then the whole concatenation - * normalized and sliced wrt the current slicing. The method will not add the equalities to the equality manager, - * but instead will slice the equality according to the current slicing in order to align all the slices. - * - * The terms that get sliced get sent to the theory engine as equalities, i.e if we slice x[10:0] into x[10:5]@x[4:0] - * equality engine gets the assertion x[10:0] = concat(x[10:5], x[4:0]). - * - * input output slicing - * -------------------------------------------------------------------------------------------------------------- - * x@y = y@x x = y, y = x empty - * x[31:0]@x[64:32] = x x = x[31:0]@x[63:32] x:{64,32,0} - * x@y = 0000@x@0000 x = 0000@x[7:4], y = x[3:0]@0000 x:{8,4,0} - * - */ - inline bool solveEquality(TNode lhs, TNode rhs); - -private: - - inline bool solveEquality(TNode lhs, TNode rhs, const std::set& assumptions); - - /** - * Slices up lhs and rhs and returns the slices in lhsSlices and rhsSlices. The slices are not atomic, - * they are sliced in order to make one of lhs or rhs atomic, the other one can be a concatenation. - */ - inline bool sliceAndSolve(std::vector& lhs, std::vector& rhs, const std::set& assumptions); - - /** - * Returns true if the term is already sliced wrt the current slicing. Note that, for example, even though - * the slicing is empty, x[i:j] is considered sliced. Sliced means that there is no slice points between i and j. - */ - inline bool isSliced(TNode node) const; - - /** - * Slices the term wrt the current slicing. When done, isSliced returns true - */ - inline bool slice(TNode node, std::vector& sliced); - - /** - * Returns the base term in the core theory of the given term, i.e. - * x => x - * x[i:j] => x - * (x + y) => x+y - * (x + y)[i:j] => x+y - */ - static inline TNode baseTerm(TNode node); - - /** - * Adds a new slice to the slice set of the given term. - */ - inline bool addSlice(Node term, unsigned slicePoint); -}; - -template -bool SliceManager::solveEquality(TNode lhs, TNode rhs) { - std::set assumptions; - assumptions.insert(lhs.eqNode(rhs)); - bool ok = solveEquality(lhs, rhs, assumptions); - return ok; -} - -template -bool SliceManager::solveEquality(TNode lhs, TNode rhs, const std::set& assumptions) { - - BVDebug("slicing") << "SliceMagager::solveEquality(" << lhs << "," << rhs << "," << utils::setToString(assumptions) << ")" << push << std::endl; - - bool ok; - - // The concatenations on the left-hand side (reverse order, first is on top) - std::vector lhsTerms; - if (lhs.getKind() == kind::BITVECTOR_CONCAT) { - for (int i = (int) lhs.getNumChildren() - 1; i >= 0; -- i) { - lhsTerms.push_back(lhs[i]); - } - } else { - lhsTerms.push_back(lhs); - } - - // The concatenations on the right-hand side (reverse order, first is on top) - std::vector rhsTerms; - if (rhs.getKind() == kind::BITVECTOR_CONCAT) { - for (int i = (int) rhs.getNumChildren() - 1; i >= 0; --i) { - rhsTerms.push_back(rhs[i]); - } - } else { - rhsTerms.push_back(rhs); - } - - // Slice the individual terms to align them - ok = sliceAndSolve(lhsTerms, rhsTerms, assumptions); - - BVDebug("slicing") << "SliceMagager::solveEquality(" << lhs << "," << rhs << "," << utils::setToString(assumptions) << ")" << pop << std::endl; - - return ok; -} - - -template -bool SliceManager::sliceAndSolve(std::vector& lhs, std::vector& rhs, const std::set& assumptions) -{ - - BVDebug("slicing") << "SliceManager::sliceAndSolve()" << std::endl; - - // Go through the work-list, solve and align - while (!lhs.empty()) { - - Assert(!rhs.empty()); - - BVDebug("slicing") << "SliceManager::sliceAndSolve(): lhs " << utils::vectorToString(lhs) << std::endl; - BVDebug("slicing") << "SliceManager::sliceAndSolve(): rhs " << utils::vectorToString(rhs) << std::endl; - - // The terms that we need to slice - Node lhsTerm = lhs.back(); - Node rhsTerm = rhs.back(); - - BVDebug("slicing") << "SliceManager::sliceAndSolve(): " << lhsTerm << " : " << rhsTerm << std::endl; - - // If the terms are not sliced wrt the current slicing, we have them sliced - lhs.pop_back(); - if (!isSliced(lhsTerm)) { - if (!slice(lhsTerm, lhs)) return false; - BVDebug("slicing") << "SliceManager::sliceAndSolve(): lhs sliced" << std::endl; - continue; - } - rhs.pop_back(); - if (!isSliced(rhsTerm)) { - if (!slice(rhsTerm, rhs)) return false; - // We also need to put lhs back - lhs.push_back(lhsTerm); - BVDebug("slicing") << "SliceManager::sliceAndSolve(): rhs sliced" << std::endl; - continue; - } - - BVDebug("slicing") << "SliceManager::sliceAndSolve(): both lhs and rhs sliced already" << std::endl; - - // The solving concatenation - std::vector concatTerms; - - // If the slices are of the same size we do the additional work - int sizeDifference = utils::getSize(lhsTerm) - utils::getSize(rhsTerm); - - // We slice constants immediately - if (sizeDifference > 0 && lhsTerm.getKind() == kind::CONST_BITVECTOR) { - Node low = utils::mkConst(lhsTerm.getConst().extract(sizeDifference - 1, 0)); - Node high = utils::mkConst(lhsTerm.getConst().extract(utils::getSize(lhsTerm) - 1, sizeDifference)); - d_equalityEngine.addTerm(low); d_equalityEngine.addTerm(high); - lhs.push_back(low); - lhs.push_back(high); - rhs.push_back(rhsTerm); - continue; - } - if (sizeDifference < 0 && rhsTerm.getKind() == kind::CONST_BITVECTOR) { - Node low = utils::mkConst(rhsTerm.getConst().extract(-sizeDifference - 1, 0)); - Node high = utils::mkConst(rhsTerm.getConst().extract(utils::getSize(rhsTerm) - 1, -sizeDifference)); - d_equalityEngine.addTerm(low); d_equalityEngine.addTerm(high); - rhs.push_back(low); - rhs.push_back(high); - lhs.push_back(lhsTerm); - continue; - } - - enum SolvingFor { - SOLVING_FOR_LHS, - SOLVING_FOR_RHS - } solvingFor = sizeDifference < 0 || lhsTerm.getKind() == kind::CONST_BITVECTOR ? SOLVING_FOR_RHS : SOLVING_FOR_LHS; - - BVDebug("slicing") << "SliceManager::sliceAndSolve(): " << (solvingFor == SOLVING_FOR_LHS ? "solving for LHS" : "solving for RHS") << std::endl; - - // When we slice in order to align, we might have to reslice the one we are solving for - bool reslice = false; - - switch (solvingFor) { - case SOLVING_FOR_RHS: { - concatTerms.push_back(lhsTerm); - // Maybe we need to add more lhs to make them equal - while (sizeDifference < 0 && !reslice) { - Assert(lhs.size() > 0); - // Get the next part for lhs - lhsTerm = lhs.back(); - lhs.pop_back(); - // Slice if necessary - if (!isSliced(lhsTerm)) { - if (!slice(lhsTerm, lhs)) return false; - continue; - } - // If we go above 0, we need to cut it - if (sizeDifference + (int)utils::getSize(lhsTerm) > 0) { - // Slice it so it fits - addSlice(lhsTerm, (int)utils::getSize(lhsTerm) + sizeDifference); - if (!slice(lhsTerm, lhs)) return false; - if (!isSliced(rhsTerm)) { - if (!slice(rhsTerm, rhs)) return false; - while(!concatTerms.empty()) { - lhs.push_back(concatTerms.back()); - concatTerms.pop_back(); - } - reslice = true; - } - continue; - } - concatTerms.push_back(lhsTerm); - sizeDifference += utils::getSize(lhsTerm); - } - break; - } - case SOLVING_FOR_LHS: { - concatTerms.push_back(rhsTerm); - // Maybe we need to add more rhs to make them equal - while (sizeDifference > 0 && !reslice) { - Assert(rhs.size() > 0); - // Get the next part for lhs - rhsTerm = rhs.back(); - rhs.pop_back(); - // Slice if necessary - if (!isSliced(rhsTerm)) { - if (!slice(rhsTerm, rhs)) return false; - continue; - } - // If we go below 0, we need to cut it - if (sizeDifference - (int)utils::getSize(rhsTerm) < 0) { - // Slice it so it fits - addSlice(rhsTerm, (int)utils::getSize(rhsTerm) - sizeDifference); - if (!slice(rhsTerm, rhs)) return false; - if (!isSliced(lhsTerm)) { - if (!slice(lhsTerm, lhs)) return false; - while(!concatTerms.empty()) { - rhs.push_back(concatTerms.back()); - concatTerms.pop_back(); - } - reslice = true; - } - continue; - } - concatTerms.push_back(rhsTerm); - sizeDifference -= utils::getSize(rhsTerm); - } - break; - } - } - - // If we need to reslice - if (reslice) { - continue; - } - - Assert(sizeDifference == 0); - - Node concat = utils::mkConcat(concatTerms); - BVDebug("slicing") << "SliceManager::sliceAndSolve(): concatenation " << concat << std::endl; - - // We have them equal size now. If the base term of the one we are solving is solved into a - // non-trivial concatenation already, we have to normalize. A concatenation is non-trivial if - // it is not a direct slicing, i.e it is a concat, and normalize(x) != x - switch (solvingFor) { - case SOLVING_FOR_LHS: { - TNode lhsTermRepresentative = d_equalityEngine.getRepresentative(lhsTerm); - if (lhsTermRepresentative != lhsTerm && - (lhsTermRepresentative.getKind() == kind::BITVECTOR_CONCAT || lhsTermRepresentative.getKind() == kind::CONST_BITVECTOR)) { - // We need to normalize and solve the normalized equations - std::vector explanation; - d_equalityEngine.getExplanation(lhsTerm, lhsTermRepresentative, explanation); - std::set additionalAssumptions(assumptions); - utils::getConjuncts(explanation, additionalAssumptions); - bool ok = solveEquality(lhsTermRepresentative, concat, additionalAssumptions); - if (!ok) return false; - } else { - // We're fine, just add the equality - BVDebug("slicing") << "SliceManager::sliceAndSolve(): adding " << lhsTerm << " = " << concat << " " << utils::setToString(assumptions) << std::endl; - d_equalityEngine.addTerm(concat); - bool ok = d_equalityEngine.addEquality(lhsTerm, concat, utils::mkConjunction(assumptions)); - if (!ok) return false; - } - break; - } - case SOLVING_FOR_RHS: { - TNode rhsTermRepresentative = d_equalityEngine.getRepresentative(rhsTerm); - if (rhsTermRepresentative != rhsTerm && - (rhsTermRepresentative.getKind() == kind::BITVECTOR_CONCAT || rhsTermRepresentative.getKind() == kind::CONST_BITVECTOR)) { - // We need to normalize and solve the normalized equations - std::vector explanation; - d_equalityEngine.getExplanation(rhsTerm, rhsTermRepresentative, explanation); - std::set additionalAssumptions(assumptions); - utils::getConjuncts(explanation, additionalAssumptions); - bool ok = solveEquality(rhsTermRepresentative, concat, additionalAssumptions); - if (!ok) return false; - } else { - // We're fine, just add the equality - BVDebug("slicing") << "SliceManager::sliceAndSolve(): adding " << rhsTerm << " = " << concat << utils::setToString(assumptions) << std::endl; - d_equalityEngine.addTerm(concat); - bool ok = d_equalityEngine.addEquality(rhsTerm, concat, utils::mkConjunction(assumptions)); - if (!ok) return false; - } - break; - } - } - } - - return true; -} - -template -bool SliceManager::isSliced(TNode node) const { - - BVDebug("slicing") << "SliceManager::isSliced(" << node << ")" << std::endl; - - bool result = false; - - // Constants are always sliced - if (node.getKind() == kind::CONST_BITVECTOR) { - result = true; - } else { - // The indices of the beginning and end - Kind nodeKind = node.getKind(); - unsigned high = nodeKind == kind::BITVECTOR_EXTRACT ? utils::getExtractHigh(node) : utils::getSize(node) - 1; - unsigned low = nodeKind == kind::BITVECTOR_EXTRACT ? utils::getExtractLow(node) : 0; - - // Get the base term - TNode nodeBase = baseTerm(node); - Assert(nodeBase.getKind() != kind::BITVECTOR_CONCAT); - Assert(nodeBase.getKind() != kind::CONST_BITVECTOR); - - // Get the base term slice set - slicing_map::const_iterator find = d_nodeSlicing.find(nodeBase); - // If no slices, it's just a term, so we are done, UNLESS it's an extract - if (find == d_nodeSlicing.end()) { - result = nodeKind != kind::BITVECTOR_EXTRACT; - } else { - set_reference sliceSet = (*find).second; - Assert(d_setCollection.size(sliceSet) >= 2); - // The term is not sliced if one of the borders is not in the slice set or - // there is a point between the borders - result = - d_setCollection.contains(sliceSet, low) && d_setCollection.contains(sliceSet, high + 1) && - (low == high || d_setCollection.count(sliceSet, low + 1, high) == 0); - } - } - - BVDebug("slicing") << "SliceManager::isSliced(" << node << ") => " << (result ? "true" : "false") << std::endl; - return result; -} - -template -bool SliceManager::addSlice(Node node, unsigned slicePoint) { - BVDebug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ")" << std::endl; - - bool ok = true; - - int low = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractLow(node) : 0; - int high = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractHigh(node) + 1: utils::getSize(node); - slicePoint += low; - - TNode nodeBase = baseTerm(node); - - Assert(nodeBase.getKind() != kind::CONST_BITVECTOR); - - set_reference sliceSet; - slicing_map::iterator find = d_nodeSlicing.find(nodeBase); - if (find == d_nodeSlicing.end()) { - d_nodeSlicing[nodeBase] = sliceSet = d_setCollection.newSet(0); - d_setCollection.insert(sliceSet, utils::getSize(nodeBase)); - } else { - sliceSet = (*find).second; - } - - Assert(d_setCollection.size(sliceSet) >= 2); - - // What are the points surrounding the new slice point - int prev = d_setCollection.prev(sliceSet, slicePoint); - int next = d_setCollection.next(sliceSet, slicePoint); - - // Add the slice to the set - d_setCollection.insert(sliceSet, slicePoint); - BVDebug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << "): current set " << d_setCollection.toString(sliceSet) << std::endl; - - // Add the terms and the equality to the equality engine - Node t1 = utils::mkExtract(nodeBase, next - 1, slicePoint); - Node t2 = utils::mkExtract(nodeBase, slicePoint - 1, prev); - Node nodeSlice = (next == high && prev == low) ? node : utils::mkExtract(nodeBase, next - 1, prev); - Node concat = utils::mkConcat(t1, t2); - - d_equalityEngine.addTerm(t1); - d_equalityEngine.addTerm(t2); - d_equalityEngine.addTerm(nodeSlice); - d_equalityEngine.addTerm(concat); - - // We are free to add this slice, unless the slice has a representative that's already a concat - TNode nodeSliceRepresentative = d_equalityEngine.getRepresentative(nodeSlice); - if (nodeSliceRepresentative.getKind() != kind::BITVECTOR_CONCAT) { - // Add the slice to the equality engine - ok = d_equalityEngine.addEquality(nodeSlice, concat, utils::mkTrue()); - } else { - // If the representative is a concat, we must solve it - // There is no need do add nodeSlice = concat as we will solve the representative of nodeSlice - std::set assumptions; - std::vector equalities; - d_equalityEngine.getExplanation(nodeSlice, nodeSliceRepresentative, equalities); - utils::getConjuncts(equalities, assumptions); - ok = solveEquality(nodeSliceRepresentative, concat, assumptions); - } - - BVDebug("slicing") << "SliceMagager::addSlice(" << node << "," << slicePoint << ") => " << d_setCollection.toString(d_nodeSlicing[nodeBase]) << std::endl; - - return ok; -} - -template -inline bool SliceManager::slice(TNode node, std::vector& sliced) { - - BVDebug("slicing") << "SliceManager::slice(" << node << ")" << std::endl; - - Assert(!isSliced(node)); - - // The indices of the beginning and (one past) end - unsigned high = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractHigh(node) + 1 : utils::getSize(node); - unsigned low = node.getKind() == kind::BITVECTOR_EXTRACT ? utils::getExtractLow(node) : 0; - BVDebug("slicing") << "SliceManager::slice(" << node << "): low: " << low << std::endl; - BVDebug("slicing") << "SliceManager::slice(" << node << "): high: " << high << std::endl; - - // Get the base term - TNode nodeBase = baseTerm(node); - Assert(nodeBase.getKind() != kind::BITVECTOR_CONCAT); - Assert(nodeBase.getKind() != kind::CONST_BITVECTOR); - - // The nodes slice set - set_reference nodeSliceSet; - - // Find the current one or construct it - slicing_map::iterator findSliceSet = d_nodeSlicing.find(nodeBase); - if (findSliceSet == d_nodeSlicing.end()) { - d_nodeSlicing[nodeBase] = nodeSliceSet = d_setCollection.newSet(0); - d_setCollection.insert(nodeSliceSet, utils::getSize(nodeBase)); - } else { - nodeSliceSet = d_nodeSlicing[nodeBase]; - } - - Assert(d_setCollection.size(nodeSliceSet) >= 2); - - BVDebug("slicing") << "SliceManager::slice(" << node << "): current: " << d_setCollection.toString(nodeSliceSet) << std::endl; - - // Go through all the points i_0 <= low < i_1 < ... < i_{n-1} < high <= i_n from the slice set - // and generate the slices [i_0:low-1][low:i_1-1] [i_1:i2] ... [i_{n-1}:high-1][high:i_n-1]. They are in reverse order, - // as they should be - - // The high bound already in the slicing - size_t i_n = high == utils::getSize(nodeBase) ? high: d_setCollection.next(nodeSliceSet, high - 1); - BVDebug("slicing") << "SliceManager::slice(" << node << "): i_n: " << i_n << std::endl; - // Add the new point to the slice set (they might be there already) - if (high < i_n) { - if (!addSlice(nodeBase, high)) return false; - } - // The low bound already in the slicing (slicing might have changed after adding high) - size_t i_0 = low == 0 ? 0 : d_setCollection.prev(nodeSliceSet, low + 1); - BVDebug("slicing") << "SliceManager::slice(" << node << "): i_0: " << i_0 << std::endl; - // Add the new points to the slice set (they might be there already) - if (i_0 < low) { - if (!addSlice(nodeBase, low)) return false; - } - - // Get the slice points - std::vector slicePoints; - if (low + 1 < high) { - d_setCollection.getElements(nodeSliceSet, low + 1, high - 1, slicePoints); - } - - // Construct the actuall slicing - if (slicePoints.size() > 0) { - BVDebug("slicing") << "SliceManager::slice(" << node << "): adding" << utils::mkExtract(nodeBase, slicePoints[0] - 1, low) << std::endl; - sliced.push_back(utils::mkExtract(nodeBase, slicePoints[0] - 1, low)); - for (unsigned i = 1; i < slicePoints.size(); ++ i) { - BVDebug("slicing") << "SliceManager::slice(" << node << "): adding" << utils::mkExtract(nodeBase, slicePoints[i] - 1, slicePoints[i-1])<< std::endl; - sliced.push_back(utils::mkExtract(nodeBase, slicePoints[i] - 1, slicePoints[i-1])); - } - BVDebug("slicing") << "SliceManager::slice(" << node << "): adding" << utils::mkExtract(nodeBase, high-1, slicePoints.back()) << std::endl; - sliced.push_back(utils::mkExtract(nodeBase, high-1, slicePoints.back())); - } else { - sliced.push_back(utils::mkExtract(nodeBase, high - 1, low)); - } - - return true; -} - -template -TNode SliceManager::baseTerm(TNode node) { - if (node.getKind() == kind::BITVECTOR_EXTRACT) { - Assert(node[0].getKind() != kind::BITVECTOR_EXTRACT); - Assert(node[0].getKind() != kind::CONST_BITVECTOR); - return node[0]; - } else { - Assert(node.getKind() != kind::BITVECTOR_CONCAT); - return node; - } -} - -} // Namespace bv -} // Namespace theory -} // Namespace CVC4 diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index c977435ec..79c065d7e 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -19,196 +19,82 @@ #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" - #include "theory/valuation.h" +#include "theory/bv/bv_sat.h" + using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; -using namespace CVC4::theory::bv::utils; +using namespace CVC4::context; using namespace std; +using namespace CVC4::theory::bv::utils; -void TheoryBV::preRegisterTerm(TNode node) { +TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) + : Theory(THEORY_BV, c, u, out, valuation), + d_context(c), + d_assertions(c), + d_bitblaster(new Bitblaster(c) ), + d_statistics() + { + d_true = utils::mkTrue(); + } +TheoryBV::~TheoryBV() { + delete d_bitblaster; +} +TheoryBV::Statistics::Statistics(): + d_avgConflictSize("theory::bv::AvgBVConflictSize"), + d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0) +{ + StatisticsRegistry::registerStat(&d_avgConflictSize); + StatisticsRegistry::registerStat(&d_solveSubstitutions); +} - BVDebug("bitvector") << "TheoryBV::preRegister(" << node << ")" << std::endl; +TheoryBV::Statistics::~Statistics() { + StatisticsRegistry::unregisterStat(&d_avgConflictSize); + StatisticsRegistry::unregisterStat(&d_solveSubstitutions); +} - if (node.getKind() == kind::EQUAL) { - d_eqEngine.addTerm(node[0]); - if (node[0].getKind() == kind::BITVECTOR_CONCAT) { - for (unsigned i = 0, i_end = node[0].getNumChildren(); i < i_end; ++ i) { - d_eqEngine.addTerm(node[0][i]); - } - } - d_eqEngine.addTerm(node[1]); - if (node[1].getKind() == kind::BITVECTOR_CONCAT) { - for (unsigned i = 0, i_end = node[1].getNumChildren(); i < i_end; ++ i) { - d_eqEngine.addTerm(node[1][i]); - } - } +void TheoryBV::preRegisterTerm(TNode node) { - d_normalization[node] = new Normalization(d_context, node); - } + BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl; + //marker literal: bitblast all terms before we start + d_bitblaster->bitblast(node); } void TheoryBV::check(Effort e) { - BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; - - // Normalization iterators - NormalizationMap::iterator it = d_normalization.begin(); - NormalizationMap::iterator it_end = d_normalization.end(); - - // Get all the assertions - std::vector assertionsList; - while (!done()) { - // Get the assertion - TNode assertion = get(); - d_assertions.insert(assertion); - assertionsList.push_back(assertion); - } - - bool normalizeEqualities = false; - - for (unsigned i = 0; i < assertionsList.size(); ++ i) { - - TNode assertion = assertionsList[i]; - - BVDebug("bitvector") << "TheoryBV::check(" << e << "): asserting: " << assertion << std::endl; - - // Do the right stuff - switch (assertion.getKind()) { - case kind::EQUAL: { - // Slice and solve the equality - bool ok = d_sliceManager.solveEquality(assertion[0], assertion[1]); - if (!ok) return; - // Normalize all equalities - normalizeEqualities = true; - it = d_normalization.begin(); - it = d_normalization.end(); - break; + if (fullEffort(e)) { + std::vector assertions; + while (!done()) { + TNode assertion = get(); + Debug("bitvector") << "assertion " << assertion << "\n"; + assertions.push_back(assertion); + d_bitblaster->bitblast(assertion); } - case kind::NOT: { - if (!normalizeEqualities) { - // We still need to check this dis-equality, as it might have been pre-registered just now - // so we didn't have a chance to propagate - it = d_normalization.find(assertion[0]); - if (it->second->assumptions.size() == 1) { - // Just normalize this equality - normalizeEqualities = true; - it_end = it; - it_end ++; - } - } - break; + + std::vector::const_iterator it = assertions.begin(); + for (; it != assertions.end(); ++it) { + d_bitblaster->assertToSat(*it); } - default: - Unhandled(assertion.getKind()); - } - } - - if (normalizeEqualities) { + bool res = d_bitblaster->solve(); + if (res == false) { + std::vector conflictAtoms; + d_bitblaster->getConflict(conflictAtoms); - BVDebug("bitvector") << "Checking for propagations" << std::endl; - - NormalizationMap::iterator it = d_normalization.begin(); - NormalizationMap::iterator it_end = d_normalization.end(); - for(; it != it_end; ++ it) { - - TNode equality = it->first; - BVDebug("bitvector") << "Checking " << equality << std::endl; - Normalization& normalization = *it->second; + d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size()); - // If asserted, we don't care - if (d_assertions.find(equality) != d_assertions.end()) continue; - - // Assumptions - std::set assumptions; - TNode lhs = normalization.equalities.back()[0]; - TNode rhs = normalization.equalities.back()[1]; - // If already satisfied, do nothing - if (lhs == rhs) continue; - - Node lhsNormalized = d_eqEngine.normalize(lhs, assumptions); - Node rhsNormalized = d_eqEngine.normalize(rhs, assumptions); - - if (lhsNormalized == lhs && rhsNormalized == rhs) continue; - - normalization.equalities.push_back(lhsNormalized.eqNode(rhsNormalized)); - normalization.assumptions.push_back(assumptions); - - BVDebug("bitvector") << "Adding normalization " << lhsNormalized.eqNode(rhsNormalized) << std::endl; - BVDebug("bitvector") << " assumptions " << utils::setToString(assumptions) << std::endl; - - - BVDebug("bitvector") << "TheoryBV::check(" << e << "): normalizes to " << lhsNormalized << " = " << rhsNormalized << std::endl; - - // If both are equal we can propagate - bool propagate = lhsNormalized == rhsNormalized; - // otherwise if both are constants, we propagate negation (if not already there) - bool propagateNegation = !propagate && - lhsNormalized.getKind() == kind::CONST_BITVECTOR && rhsNormalized.getKind() == kind::CONST_BITVECTOR - && d_assertions.find(equality.notNode()) == d_assertions.end(); - ; - if (propagate || propagateNegation) { - Node implied = propagate ? Node(equality) : equality.notNode() ; - Node impliedNegated = propagate ? equality.notNode() : Node(equality) ; - // If the negation of what's implied has been asserted, we are in conflict - if (d_assertions.find(impliedNegated) != d_assertions.end()) { - BVDebug("bitvector") << "TheoryBV::check(" << e << "): conflict with " << utils::setToString(assumptions) << std::endl; - // Construct the assumptions - for (unsigned i = 0; i < normalization.assumptions.size(); ++ i) { - assumptions.insert(normalization.assumptions[i].begin(), normalization.assumptions[i].end()); - } - // Make the conflict - assumptions.insert(impliedNegated); - d_out->conflict(mkConjunction(assumptions)); - return; - } - // Otherwise we propagate the implication - else { - BVDebug("bitvector") << "TheoryBV::check(" << e << "): propagating " << implied << std::endl; - d_out->propagate(implied); - d_assertions.insert(implied); - } - } + Node conflict = mkConjunction(conflictAtoms); + d_out->conflict(conflict); + return; } } } -bool TheoryBV::triggerEquality(size_t triggerId) { - BVDebug("bitvector") << "TheoryBV::triggerEquality(" << triggerId << ")" << std::endl; - Assert(triggerId < d_triggers.size()); - BVDebug("bitvector") << "TheoryBV::triggerEquality(" << triggerId << "): " << d_triggers[triggerId] << std::endl; - - return true; - - TNode equality = d_triggers[triggerId]; - - // If we have just asserted this equality ignore it - if (d_assertions.contains(equality)) return true; - - // If we have a negation asserted, we have a confict - if (d_assertions.contains(equality.notNode())) { - - std::vector explanation; - d_eqEngine.getExplanation(equality[0], equality[1], explanation); - std::set assumptions; - assumptions.insert(equality.notNode()); - utils::getConjuncts(explanation, assumptions); - d_out->conflict(utils::mkConjunction(assumptions)); - - return false; - } - - // Otherwise we propagate this equality - d_out->propagate(equality); - - return true; -} Node TheoryBV::getValue(TNode n) { - NodeManager* nodeManager = NodeManager::currentNM(); + //NodeManager* nodeManager = NodeManager::currentNM(); switch(n.getKind()) { @@ -216,8 +102,7 @@ Node TheoryBV::getValue(TNode n) { Unhandled(kind::VARIABLE); case kind::EQUAL: // 2 args - return nodeManager-> - mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) ); + Unhandled(kind::VARIABLE); default: Unhandled(n.getKind()); @@ -229,13 +114,37 @@ Node TheoryBV::explain(TNode node) { TNode equality = node.getKind() == kind::NOT ? node[0] : node; Assert(equality.getKind() == kind::EQUAL); + Assert(0); + return node; + +} - context::CDList< set >& vec = d_normalization[equality]->assumptions; - std::set assumptions; - for (unsigned i = 0; i < vec.size(); ++ i) { - BVDebug("bitvector") << "Adding normalization " << d_normalization[equality]->equalities[i] << std::endl; - BVDebug("bitvector") << " assumptions " << utils::setToString(d_normalization[equality]->assumptions[i]) << std::endl; - assumptions.insert(vec[i].begin(), vec[i].end()); +// Node TheoryBV::preprocessTerm(TNode term) { +// return term; //d_staticEqManager.find(term); +// } + +Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { + switch(in.getKind()) { + case kind::EQUAL: + + if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) { + ++(d_statistics.d_solveSubstitutions); + outSubstitutions.addSubstitution(in[0], in[1]); + return PP_ASSERT_STATUS_SOLVED; + } + if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) { + ++(d_statistics.d_solveSubstitutions); + outSubstitutions.addSubstitution(in[1], in[0]); + return PP_ASSERT_STATUS_SOLVED; + } + // to do constant propagations + + break; + case kind::NOT: + break; + default: + // TODO other predicates + break; } - return utils::mkConjunction(assumptions); + return PP_ASSERT_STATUS_UNSOLVED; } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 11ddceaae..5303b6595 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -23,119 +23,42 @@ #include "theory/theory.h" #include "context/context.h" -#include "context/cdset.h" #include "context/cdlist.h" -#include "theory/bv/equality_engine.h" -#include "theory/bv/slice_manager.h" +#include "theory/bv/theory_bv_utils.h" +#include "util/stats.h" + +namespace BVMinisat { +class SimpSolver; +} + namespace CVC4 { namespace theory { namespace bv { +/// forward declarations +class Bitblaster; + class TheoryBV : public Theory { public: - class EqualityNotify { - TheoryBV& d_theoryBV; - public: - EqualityNotify(TheoryBV& theoryBV) - : d_theoryBV(theoryBV) {} - - bool operator () (size_t triggerId) { - return d_theoryBV.triggerEquality(triggerId); - } - void conflict(Node explanation) { - std::set assumptions; - utils::getConjuncts(explanation, assumptions); - d_theoryBV.d_out->conflict(utils::mkConjunction(assumptions)); - } - }; - - struct BVEqualitySettings { - static inline bool descend(TNode node) { - return node.getKind() == kind::BITVECTOR_CONCAT || node.getKind() == kind::BITVECTOR_EXTRACT; - } - - /** Returns true if node1 has preference to node2 as a representative, otherwise node2 is used */ - static inline bool mergePreference(TNode node1, unsigned node1size, TNode node2, unsigned node2size) { - if (node1.getKind() == kind::CONST_BITVECTOR) { - Assert(node2.getKind() != kind::CONST_BITVECTOR); - return true; - } - if (node2.getKind() == kind::CONST_BITVECTOR) { - Assert(node1.getKind() != kind::CONST_BITVECTOR); - return false; - } - if (node1.getKind() == kind::BITVECTOR_CONCAT) { - Assert(node2.getKind() != kind::BITVECTOR_CONCAT); - return true; - } - if (node2.getKind() == kind::BITVECTOR_CONCAT) { - Assert(node1.getKind() != kind::BITVECTOR_CONCAT); - return false; - } - return node2size < node1size; - } - }; - - typedef EqualityEngine BvEqualityEngine; - private: - /** Equality reasoning engine */ - BvEqualityEngine d_eqEngine; - - /** Slice manager */ - SliceManager d_sliceManager; - - /** Equality triggers indexed by ids from the equality manager */ - std::vector d_triggers; - /** The context we are using */ context::Context* d_context; /** The asserted stuff */ - context::CDSet d_assertions; - - /** Asserted dis-equalities */ - context::CDList d_disequalities; - - struct Normalization { - context::CDList equalities; - context::CDList< std::set > assumptions; - Normalization(context::Context* c, TNode eq) - : equalities(c), assumptions(c) { - equalities.push_back(eq); - assumptions.push_back(std::set()); - } - }; - - /** Map from equalities to their noramlization information */ - typedef __gnu_cxx::hash_map NormalizationMap; - NormalizationMap d_normalization; - - /** Called by the equality managere on triggers */ - bool triggerEquality(size_t triggerId); - + context::CDList d_assertions; + + /** Bitblaster */ + Bitblaster* d_bitblaster; Node d_true; - + public: - TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) - : Theory(THEORY_BV, c, u, out, valuation), - d_eqEngine(*this, c, "theory::bv::EqualityEngine"), - d_sliceManager(*this, c), - d_context(c), - d_assertions(c), - d_disequalities(c) - { - d_true = utils::mkTrue(); - } - - BvEqualityEngine& getEqualityEngine() { - return d_eqEngine; - } + TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); + ~TheoryBV(); void preRegisterTerm(TNode n); @@ -150,6 +73,21 @@ public: Node getValue(TNode n); std::string identify() const { return std::string("TheoryBV"); } + + //Node preprocessTerm(TNode term); + PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); +private: + + class Statistics { + public: + AverageStat d_avgConflictSize; + IntStat d_solveSubstitutions; + Statistics(); + ~Statistics(); + }; + + Statistics d_statistics; + };/* class TheoryBV */ }/* CVC4::theory::bv namespace */ diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 32bbf973f..2e2347d3c 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -31,6 +31,7 @@ namespace theory { namespace bv { enum RewriteRuleId { + /// core rewrite rules EmptyRule, ConcatFlatten, ConcatExtractMerge, @@ -42,7 +43,24 @@ enum RewriteRuleId { FailEq, SimplifyEq, ReflexivityEq, -}; + /// operator elimination rules + UgtToUlt, + UgeToUle, + SgeToSle, + SgtToSlt, + RepeatEliminate, + RotateLeftEliminate, + RotateRightEliminate, + NandEliminate, + NorEliminate, + SdivEliminate, + UdivEliminate, + SmodEliminate, + SremEliminate, + ZeroExtendEliminate, + // division by zero guards: rewrite a / b as b!=0 => a/b = ... + DivZeroGuard + }; inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { switch (ruleId) { @@ -57,6 +75,20 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case FailEq: out << "FailEq"; return out; case SimplifyEq: out << "SimplifyEq"; return out; case ReflexivityEq: out << "ReflexivityEq"; return out; + case UgtToUlt: out << "UgtToUlt"; return out; + case SgtToSlt: out << "SgtToSlt"; return out; + case UgeToUle: out << "UgeToUle"; return out; + case SgeToSle: out << "SgeToSle"; return out; + case RepeatEliminate: out << "RepeatEliminate"; return out; + case RotateLeftEliminate: out << "RotateLeftEliminate"; return out; + case RotateRightEliminate:out << "RotateRightEliminate";return out; + case NandEliminate: out << "NandEliminate"; return out; + case NorEliminate : out << "NorEliminate"; return out; + case SdivEliminate : out << "SdivEliminate"; return out; + case SremEliminate : out << "SremEliminate"; return out; + case SmodEliminate : out << "SmodEliminate"; return out; + case ZeroExtendEliminate :out << "ZeroExtendEliminate"; return out; + case DivZeroGuard : out << "DivZeroGuard"; return out; default: Unreachable(); } @@ -147,6 +179,7 @@ typename RewriteRule::RuleStatistics* RewriteRule::s_statistics = NU /** Have to list all the rewrite rules to get the statistics out */ struct AllRewriteRules { + RewriteRule rule00; RewriteRule rule01; RewriteRule rule02; @@ -158,6 +191,20 @@ struct AllRewriteRules { RewriteRule rule08; RewriteRule rule09; RewriteRule rule10; + RewriteRule rule11; + RewriteRule rule12; + RewriteRule rule13; + RewriteRule rule14; + RewriteRule rule17; + RewriteRule rule18; + RewriteRule rule19; + RewriteRule rule20; + RewriteRule rule21; + RewriteRule rule22; + RewriteRule rule23; + RewriteRule rule24; + RewriteRule rule25; + }; template<> @@ -202,7 +249,7 @@ struct ApplyRuleToChildren { template < typename R1, - typename R2, + typename R2 = RewriteRule, typename R3 = RewriteRule, typename R4 = RewriteRule, typename R5 = RewriteRule, diff --git a/src/theory/bv/theory_bv_rewrite_rules_arith.h b/src/theory/bv/theory_bv_rewrite_rules_arith.h new file mode 100644 index 000000000..08a571db3 --- /dev/null +++ b/src/theory/bv/theory_bv_rewrite_rules_arith.h @@ -0,0 +1,321 @@ +/********************* */ +/*! \file theory_bv_rewrite_rules_core.h + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#pragma once + +#include "theory/bv/theory_bv_rewrite_rules.h" +#include "theory/bv/theory_bv_utils.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +template<> +bool RewriteRule::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_UGT); +} + +template<> +Node RewriteRule::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + TNode a = node[0]; + TNode b = node[1]; + Node result = utils::mkNode(kind::BITVECTOR_ULT, b, a); + return result; +} + + +template<> +bool RewriteRule::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_UGE); +} + +template<> +Node RewriteRule::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + TNode a = node[0]; + TNode b = node[1]; + Node result = utils::mkNode(kind::BITVECTOR_ULE, b, a); + return result; +} + + +template<> +bool RewriteRule::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_SGT); +} + +template<> +Node RewriteRule::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + TNode a = node[0]; + TNode b = node[1]; + Node result = utils::mkNode(kind::BITVECTOR_SLT, b, a); + return result; +} + + +template<> +bool RewriteRule::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_SGE); +} + +template<> +Node RewriteRule::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + TNode a = node[0]; + TNode b = node[1]; + Node result = utils::mkNode(kind::BITVECTOR_SLE, b, a); + return result; +} + +template<> +bool RewriteRule::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_REPEAT); +} + +template<> +Node RewriteRule::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + TNode a = node[0]; + unsigned amount = node.getOperator().getConst().repeatAmount; + Assert(amount >= 1); + if(amount == 1) { + return a; + } + NodeBuilder<> result(kind::BITVECTOR_CONCAT); + for(unsigned i = 0; i < amount; ++i) { + result << node[0]; + } + Node resultNode = result; + return resultNode; +} + +template<> +bool RewriteRule::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_ROTATE_LEFT); +} + +template<> +Node RewriteRule::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + TNode a = node[0]; + unsigned amount = node.getOperator().getConst().rotateLeftAmount; + amount = amount % utils::getSize(a); + if (amount == 0) { + return a; + } + + Node left = utils::mkExtract(a, utils::getSize(a)-1 - amount, 0); + Node right = utils::mkExtract(a, utils::getSize(a) -1, utils::getSize(a) - amount); + Node result = utils::mkConcat(left, right); + + return result; +} + +template<> +bool RewriteRule::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_ROTATE_RIGHT); +} + +template<> +Node RewriteRule::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + TNode a = node[0]; + unsigned amount = node.getOperator().getConst().rotateRightAmount; + amount = amount % utils::getSize(a); + if (amount == 0) { + return a; + } + + Node left = utils::mkExtract(a, amount - 1, 0); + Node right = utils::mkExtract(a, utils::getSize(a)-1, amount); + Node result = utils::mkConcat(left, right); + + return result; +} + +template<> +bool RewriteRule::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_NAND); +} + +template<> +Node RewriteRule::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + TNode a = node[0]; + TNode b = node[1]; + Node andNode = utils::mkNode(kind::BITVECTOR_AND, a, b); + Node result = utils::mkNode(kind::BITVECTOR_NOT, andNode); + return result; +} + +template<> +bool RewriteRule::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_NOR); +} + +template<> +Node RewriteRule::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + TNode a = node[0]; + TNode b = node[1]; + Node orNode = utils::mkNode(kind::BITVECTOR_OR, a, b); + Node result = utils::mkNode(kind::BITVECTOR_NOT, orNode); + return result; +} + +template<> +bool RewriteRule::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_SDIV); +} + +template<> +Node RewriteRule::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + + TNode a = node[0]; + TNode b = node[1]; + unsigned size = utils::getSize(a); + + Node one = utils::mkConst(1, 1); + Node a_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), one); + Node b_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), one); + Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a); + Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b); + + Node a_udiv_b = utils::mkNode(kind::BITVECTOR_UDIV, abs_a, abs_b); + Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_udiv_b); + + Node condition = utils::mkNode(kind::XOR, a_lt_0, b_lt_0); + Node result = utils::mkNode(kind::ITE, condition, neg_result, a_udiv_b); + + return result; +} + + +template<> +bool RewriteRule::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_SREM); +} + +template<> +Node RewriteRule::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + TNode a = node[0]; + TNode b = node[1]; + unsigned size = utils::getSize(a); + + Node one = utils::mkConst(1, 1); + Node a_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), one); + Node b_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), one); + Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a); + Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b); + + Node a_urem_b = utils::mkNode(kind::BITVECTOR_UREM, abs_a, abs_b); + Node neg_result = utils::mkNode(kind::BITVECTOR_NEG, a_urem_b); + + Node result = utils::mkNode(kind::ITE, a_lt_0, neg_result, a_urem_b); + + return result; +} + +template<> +bool RewriteRule::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_SMOD); +} + +template<> +Node RewriteRule::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + TNode a = node[0]; + TNode b = node[1]; + unsigned size = utils::getSize(a); + + Node one = utils::mkConst(1, 1); + Node zero = utils::mkConst(1, 0); + Node a_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), one); + Node b_lt_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), one); + + Node a_gte_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(a, size-1, size-1), zero); + Node b_gte_0 = utils::mkNode(kind::EQUAL, utils::mkExtract(b, size-1, size-1), zero); + + Node abs_a = utils::mkNode(kind::ITE, a_lt_0, utils::mkNode(kind::BITVECTOR_NEG, a), a); + Node abs_b = utils::mkNode(kind::ITE, b_lt_0, utils::mkNode(kind::BITVECTOR_NEG, b), b); + + Node a_urem_b = utils::mkNode(kind::BITVECTOR_UREM, abs_a, abs_b); + Node neg_rem = utils::mkNode(kind::BITVECTOR_NEG, a_urem_b); + + + Node aneg_bpos = utils::mkNode(kind::AND, a_lt_0, b_gte_0); + Node apos_bneg = utils::mkNode(kind::AND, a_gte_0, b_lt_0); + Node aneg_bneg = utils::mkNode(kind::AND, a_lt_0, b_lt_0); + + Node result = utils::mkNode(kind::ITE, aneg_bpos, utils::mkNode(kind::BITVECTOR_PLUS, neg_rem, b), + utils::mkNode(kind::ITE, apos_bneg, utils::mkNode(kind::BITVECTOR_PLUS, a_urem_b, b), + utils::mkNode(kind::ITE, aneg_bneg, neg_rem, + a_urem_b))); + return result; +} + + +template<> +bool RewriteRule::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_ZERO_EXTEND); +} + +template<> +Node RewriteRule::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + + TNode bv = node[0]; + unsigned amount = node.getOperator().getConst().zeroExtendAmount; + + Node zero = utils::mkConst(amount, 0); + Node result = utils::mkConcat(zero, node[0]); + + return result; +} + + +template<> +bool RewriteRule::applies(Node node) { + return (node.getKind() == kind::BITVECTOR_UDIV || + node.getKind() == kind::BITVECTOR_UREM || + node.getKind() == kind::BITVECTOR_SDIV || + node.getKind() == kind::BITVECTOR_SREM || + node.getKind() == kind::BITVECTOR_SMOD); +} + +template<> +Node RewriteRule::apply(Node node) { + BVDebug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + + Unimplemented(); + +} + + + + +} +} +} diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 566bf3a68..2f3538837 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -21,17 +21,17 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_rewrite_rules_core.h" +#include "theory/bv/theory_bv_rewrite_rules_arith.h" using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; RewriteResponse TheoryBVRewriter::postRewrite(TNode node) { - + BVDebug("bitvector") << "TheoryBV::postRewrite(" << node << ")" << std::endl; - - Node result; - + + Node result = node; if (node.getKind() == kind::CONST_BITVECTOR || (node.getKind() != kind::EQUAL && Theory::isLeafOf(node, THEORY_BV))) { result = node; } else { @@ -67,10 +67,78 @@ RewriteResponse TheoryBVRewriter::postRewrite(TNode node) { RewriteRule, // If both sides are equal equality is true RewriteRule, - // Normalize the equalities + // Eliminate the equalities RewriteRule >::apply(node); break; + case kind::BITVECTOR_UGT: + result = LinearRewriteStrategy < + RewriteRule + >::apply(node); + break; + + case kind::BITVECTOR_UGE: + result = LinearRewriteStrategy < + RewriteRule + >::apply(node); + break; + case kind::BITVECTOR_SGT: + result = LinearRewriteStrategy < + RewriteRule + >::apply(node); + break; + case kind::BITVECTOR_SGE: + result = LinearRewriteStrategy < + RewriteRule + >::apply(node); + break; + case kind::BITVECTOR_REPEAT: + result = LinearRewriteStrategy < + RewriteRule + >::apply(node); + break; + case kind::BITVECTOR_ROTATE_RIGHT: + result = LinearRewriteStrategy < + RewriteRule + >::apply(node); + break; + case kind::BITVECTOR_ROTATE_LEFT: + result = LinearRewriteStrategy < + RewriteRule + >::apply(node); + break; + case kind::BITVECTOR_NAND: + result = LinearRewriteStrategy < + RewriteRule + >::apply(node); + break; + case kind::BITVECTOR_NOR: + result = LinearRewriteStrategy < + RewriteRule + >::apply(node); + break; + + case kind::BITVECTOR_SDIV: + result = LinearRewriteStrategy < + RewriteRule + >::apply(node); + break; + case kind::BITVECTOR_SREM: + result = LinearRewriteStrategy < + RewriteRule + >::apply(node); + break; + case kind::BITVECTOR_SMOD: + result = LinearRewriteStrategy < + RewriteRule + >::apply(node); + break; + case kind::BITVECTOR_ZERO_EXTEND: + result = LinearRewriteStrategy < + RewriteRule + >::apply(node); + break; + default: // TODO: figure out when this is an operator result = node; diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index f0eb621ca..1893977a8 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -39,7 +39,7 @@ public: static RewriteResponse postRewrite(TNode node); static inline RewriteResponse preRewrite(TNode node) { - return RewriteResponse(REWRITE_DONE, node); + return postRewrite(node); } static inline Node rewriteEquality(TNode node) { diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 192295bc0..91b3a0e5d 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -35,6 +35,28 @@ public: } }; + +class BitVectorBitOfTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate) { + + if(check) { + BitVectorBitOf info = n.getOperator().getConst(); + TypeNode t = n[0].getType(check); + + if (!t.isBitVector()) { + throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); + } + if (info.bitIndex >= t.getBitVectorSize()) { + throw TypeCheckingExceptionPrivate(n, "extract index is larger than the bitvector size"); + } + } + return nodeManager->booleanType(); + } +}; + + class BitVectorCompRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 80c5ca7f7..6bd7368c9 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -49,6 +49,13 @@ inline unsigned getSize(TNode node) { return node.getType().getBitVectorSize(); } +// this seems to behave strangely +inline const Integer& getBit(TNode node, unsigned i) { + Assert (0); + Assert (node.getKind() == kind::CONST_BITVECTOR); + return node.getConst().extract(i, i).getValue(); +} + inline Node mkTrue() { return NodeManager::currentNM()->mkConst(true); } @@ -57,6 +64,11 @@ inline Node mkFalse() { return NodeManager::currentNM()->mkConst(false); } +inline Node mkVar(unsigned size) { + NodeManager* nm = NodeManager::currentNM(); + return nm->mkVar(nm->mkBitVectorType(size)); +} + inline Node mkAnd(std::vector& children) { if (children.size() > 1) { return NodeManager::currentNM()->mkNode(kind::AND, children); @@ -65,8 +77,43 @@ inline Node mkAnd(std::vector& 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 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 mkAnd(std::vector& children) { - return NodeManager::currentNM()->mkNode(kind::AND, children); + if(children.size() > 1) { + return NodeManager::currentNM()->mkNode(kind::AND, children); + } else { + return children[0]; + } } inline Node mkExtract(TNode node, unsigned high, unsigned low) { @@ -76,6 +123,12 @@ inline Node mkExtract(TNode node, unsigned high, unsigned low) { return NodeManager::currentNM()->mkNode(extractOp, children); } +inline Node mkBitOf(TNode node, unsigned index) { + Node bitOfOp = NodeManager::currentNM()->mkConst(BitVectorBitOf(index)); + return NodeManager::currentNM()->mkNode(bitOfOp, node); + +} + inline Node mkConcat(std::vector& children) { if (children.size() > 1) return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, children); @@ -88,6 +141,11 @@ inline Node mkConcat(TNode t1, TNode t2) { } +inline Node mkConst(unsigned size, unsigned int value) { + BitVector val(size, value); + return NodeManager::currentNM()->mkConst(val); +} + inline Node mkConst(const BitVector& value) { return NodeManager::currentNM()->mkConst(value); } @@ -139,6 +197,66 @@ inline Node mkConjunction(const std::set nodes) { return conjunction; } +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::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))) + { + return true; + } + else + { + return false; + } +} + +inline Node mkConjunction(const std::vector& nodes) { + std::vector expandedNodes; + + std::vector::const_iterator it = nodes.begin(); + std::vector::const_iterator it_end = nodes.end(); + while (it != it_end) { + TNode current = *it; + if (current != mkTrue()) { + Assert(isBVPredicate(current)); + expandedNodes.push_back(current); + } + ++ it; + } + + Assert(expandedNodes.size() > 0); + 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& nodeSet) { std::stringstream out; diff --git a/src/theory/registrar.h b/src/theory/registrar.h deleted file mode 100644 index 19315827e..000000000 --- a/src/theory/registrar.h +++ /dev/null @@ -1,50 +0,0 @@ -/********************* */ -/*! \file registrar.h - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Class to encapsulate preregistration duties - ** - ** Class to encapsulate preregistration duties. This class permits the - ** CNF stream implementation to reach into the theory engine to - ** preregister only those terms with an associated SAT literal (at the - ** point when they get the SAT literal), without having to refer to the - ** TheoryEngine class directly. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__REGISTRAR_H -#define __CVC4__THEORY__REGISTRAR_H - -#include "theory/theory_engine.h" - -namespace CVC4 { -namespace theory { - -class Registrar { -private: - TheoryEngine* d_theoryEngine; - -public: - - Registrar(TheoryEngine* te) : d_theoryEngine(te) { } - - void preRegister(Node n) { - d_theoryEngine->preRegister(n); - } - -};/* class Registrar */ - -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__REGISTRAR_H */ diff --git a/src/theory/theory_registrar.h b/src/theory/theory_registrar.h new file mode 100644 index 000000000..810ef1f67 --- /dev/null +++ b/src/theory/theory_registrar.h @@ -0,0 +1,51 @@ +/********************* */ +/*! \file registrar.h + ** \verbatim + ** Original author: taking + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Class to encapsulate preregistration duties + ** + ** Class to encapsulate preregistration duties. This class permits the + ** CNF stream implementation to reach into the theory engine to + ** preregister only those terms with an associated SAT literal (at the + ** point when they get the SAT literal), without having to refer to the + ** TheoryEngine class directly. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__THEORY_REGISTRAR_H +#define __CVC4__THEORY__THEORY_REGISTRAR_H + +#include "prop/registrar.h" +#include "theory/theory_engine.h" + +namespace CVC4 { +namespace theory { + +class TheoryRegistrar: public prop::Registrar { +private: + TheoryEngine* d_theoryEngine; + +public: + + TheoryRegistrar(TheoryEngine* te) : d_theoryEngine(te) { } + + void preRegister(Node n) { + d_theoryEngine->preRegister(n); + } + +};/* class TheoryRegistrar */ + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__THEORY_REGISTRAR_H */ -- cgit v1.2.3