diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-02-25 18:23:10 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-02-25 18:23:10 +0000 |
commit | 7aa55e0d38e73a02b11ad0c5a60196b610674050 (patch) | |
tree | c59def0ed00dcde29a5a6498cf74ac87dc3a2a6f /src/theory/bv/bitblast_strategies.h | |
parent | d8da6a3644d1cdbe62d44a8eb80068da4d1d2855 (diff) |
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
Diffstat (limited to 'src/theory/bv/bitblast_strategies.h')
-rw-r--r-- | src/theory/bv/bitblast_strategies.h | 112 |
1 files changed, 112 insertions, 0 deletions
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<Node> 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 |