Skip to content

Commit

Permalink
Reorganize bitblaster code. (cvc5#1695)
Browse files Browse the repository at this point in the history 
This splits bitblaster_template.h into the separate header files {aig,eager,lazy}_bitblaster.h and
bitblaster.h (the template class TBitblaster). All the bitblaster related code is moved into the
sub-directory bitblast/.
  • Loading branch information
@mpreiner @aniemetz
mpreiner authored and aniemetz committed Apr 2, 2018
1 parent 2d40d7a commit a917cc2
Show file tree
Hide file tree
Showing 17 changed files with 803 additions and 683 deletions.
15 changes: 9 additions & 6 deletions src/Makefile.am
View file
Original file line number Diff line number Diff line change
Expand Up @@ -292,10 +292,15 @@ libcvc4_la_SOURCES = \
theory/builtin/type_enumerator.h \
theory/bv/abstraction.cpp \
theory/bv/abstraction.h \
theory/bv/aig_bitblaster.cpp \
theory/bv/bitblast_strategies_template.h \
theory/bv/bitblast_utils.h \
theory/bv/bitblaster_template.h \
theory/bv/bitblast/aig_bitblaster.cpp \
theory/bv/bitblast/aig_bitblaster.h \
theory/bv/bitblast/bitblast_strategies_template.h \
theory/bv/bitblast/bitblast_utils.h \
theory/bv/bitblast/bitblaster.h \
theory/bv/bitblast/eager_bitblaster.cpp \
theory/bv/bitblast/eager_bitblaster.h \
theory/bv/bitblast/lazy_bitblaster.cpp \
theory/bv/bitblast/lazy_bitblaster.h \
theory/bv/bv_eager_solver.cpp \
theory/bv/bv_eager_solver.h \
theory/bv/bv_inequality_graph.cpp \
Expand All @@ -317,8 +322,6 @@ libcvc4_la_SOURCES = \
theory/bv/bvgauss.h \
theory/bv/bvintropow2.cpp \
theory/bv/bvintropow2.h \
theory/bv/eager_bitblaster.cpp \
theory/bv/lazy_bitblaster.cpp \
theory/bv/slicer.cpp \
theory/bv/slicer.h \
theory/bv/theory_bv.cpp \
Expand Down
2 changes: 1 addition & 1 deletion src/proof/bitvector_proof.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
#include "proof/proof_utils.h"
#include "proof/sat_proof_implementation.h"
#include "prop/bvminisat/bvminisat.h"
#include "theory/bv/bitblaster_template.h"
#include "theory/bv/bitblast/bitblaster.h"
#include "theory/bv/theory_bv.h"
#include "theory/bv/theory_bv_rewrite_rules.h"

Expand Down
102 changes: 54 additions & 48 deletions src/theory/bv/aig_bitblaster.cpp → src/theory/bv/bitblast/aig_bitblaster.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,29 +9,35 @@
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief
** \brief AIG bitblaster.
**
** Bitblaster for the lazy bv solver.
** AIG bitblaster.
**/

#include "bitblaster_template.h"

#include "cvc4_private.h"

#include "theory/bv/bitblast/aig_bitblaster.h"

#include "base/cvc4_check.h"
#include "options/bv_options.h"
#include "prop/cnf_stream.h"
#include "prop/sat_solver_factory.h"
#include "smt/smt_statistics_registry.h"

#ifdef CVC4_USE_ABC
// Function is defined as static in ABC. Not sure how else to do this.
static inline int Cnf_Lit2Var( int Lit ) { return (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+1; }

extern "C" {
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
#include "base/abc/abc.h"
#include "base/main/main.h"
#include "sat/cnf/cnf.h"

extern Aig_Man_t* Abc_NtkToDar(Abc_Ntk_t* pNtk, int fExors, int fRegisters);
}

// Function is defined as static in ABC. Not sure how else to do this.
static inline int Cnf_Lit2Var(int Lit)
{
return (Lit & 1) ? -(Lit >> 1) - 1 : (Lit >> 1) + 1;
}

namespace CVC4 {
namespace theory {
Expand Down Expand Up @@ -110,26 +116,17 @@ Abc_Obj_t* mkIte<Abc_Obj_t*>(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) {
return Abc_AigMux(AigBitblaster::currentAigM(), cond, a, b);
}

} /* CVC4::theory::bv */
} /* CVC4::theory */
} /* CVC4 */

using namespace CVC4;
using namespace CVC4::theory;
using namespace CVC4::theory::bv;


Abc_Ntk_t* AigBitblaster::abcAigNetwork = NULL;
CVC4_THREAD_LOCAL Abc_Ntk_t* AigBitblaster::s_abcAigNetwork = nullptr;

Abc_Ntk_t* AigBitblaster::currentAigNtk() {
if (!AigBitblaster::abcAigNetwork) {
if (!AigBitblaster::s_abcAigNetwork) {
Abc_Start();
abcAigNetwork = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1);
s_abcAigNetwork = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1);
char pName[] = "CVC4::theory::bv::AigNetwork";
abcAigNetwork->pName = Extra_UtilStrsav(pName);
s_abcAigNetwork->pName = Extra_UtilStrsav(pName);
}

return abcAigNetwork;
return s_abcAigNetwork;
}


Expand All @@ -138,34 +135,39 @@ Abc_Aig_t* AigBitblaster::currentAigM() {
}

AigBitblaster::AigBitblaster()
: TBitblaster<Abc_Obj_t*>()
, d_aigCache()
, d_bbAtoms()
, d_aigOutputNode(NULL)
: TBitblaster<Abc_Obj_t*>(),
d_nullContext(new context::Context()),
d_aigCache(),
d_bbAtoms(),
d_aigOutputNode(NULL)
{
d_nullContext = new context::Context();
switch(options::bvSatSolver()) {
case SAT_SOLVER_MINISAT: {
prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat(d_nullContext,
smtStatisticsRegistry(),
"AigBitblaster");
MinisatEmptyNotify* notify = new MinisatEmptyNotify();
minisat->setNotify(notify);
d_satSolver = minisat;
break;
}
case SAT_SOLVER_CRYPTOMINISAT:
d_satSolver = prop::SatSolverFactory::createCryptoMinisat(smtStatisticsRegistry(),
"AigBitblaster");
break;
default: CVC4_FATAL() << "Unknown SAT solver type";
prop::SatSolver* solver = nullptr;
switch (options::bvSatSolver())
{
case SAT_SOLVER_MINISAT:
{
prop::BVSatSolverInterface* minisat =
prop::SatSolverFactory::createMinisat(
d_nullContext.get(), smtStatisticsRegistry(), "AigBitblaster");
MinisatEmptyNotify notify;
minisat->setNotify(&notify);
solver = minisat;
break;
}
case SAT_SOLVER_CADICAL:
solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(),
"AigBitblaster");
break;
case SAT_SOLVER_CRYPTOMINISAT:
solver = prop::SatSolverFactory::createCryptoMinisat(
smtStatisticsRegistry(), "AigBitblaster");
break;
default: CVC4_FATAL() << "Unknown SAT solver type";
}
d_satSolver.reset(solver);
}

AigBitblaster::~AigBitblaster() {
Assert (abcAigNetwork == NULL);
delete d_nullContext;
}
AigBitblaster::~AigBitblaster() {}

Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
Assert (node.getType().isBoolean());
Expand Down Expand Up @@ -363,7 +365,7 @@ void AigBitblaster::simplifyAig() {
fprintf( stdout, "Cannot execute command \"%s\".\n", command );
exit(-1);
}
abcAigNetwork = Abc_FrameReadNtk(pAbc);
s_abcAigNetwork = Abc_FrameReadNtk(pAbc);
}


Expand All @@ -380,7 +382,7 @@ void AigBitblaster::convertToCnfAndAssert() {

// // free old network
// Abc_NtkDelete(currentAigNtk());
// abcAigNetwork = NULL;
// s_abcAigNetwork = NULL;

Assert (pMan != NULL);
Assert (Aig_ManCheck(pMan));
Expand Down Expand Up @@ -485,4 +487,8 @@ AigBitblaster::Statistics::~Statistics() {
smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
smtStatisticsRegistry()->unregisterStat(&d_solveTime);
}

} // namespace bv
} // namespace theory
} // namespace CVC4
#endif // CVC4_USE_ABC
105 changes: 105 additions & 0 deletions src/theory/bv/bitblast/aig_bitblaster.h
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,105 @@
/********************* */
/*! \file aig_bitblaster.h
** \verbatim
** Top contributors (to current version):
** Liana Hadarean, Tim King, Aina Niemetz
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief AIG bitblaster.
**
** AIG Bitblaster based on ABC.
**/

#include "cvc4_private.h"

#ifndef __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
#define __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H

#include "theory/bv/bitblast/bitblaster.h"

#include "base/tls.h"

class Abc_Obj_t_;
typedef Abc_Obj_t_ Abc_Obj_t;

class Abc_Ntk_t_;
typedef Abc_Ntk_t_ Abc_Ntk_t;

class Abc_Aig_t_;
typedef Abc_Aig_t_ Abc_Aig_t;

class Cnf_Dat_t_;
typedef Cnf_Dat_t_ Cnf_Dat_t;

namespace CVC4 {
namespace theory {
namespace bv {

class AigBitblaster : public TBitblaster<Abc_Obj_t*>
{
public:
AigBitblaster();
~AigBitblaster();

void makeVariable(TNode node, Bits& bits) override;
void bbTerm(TNode node, Bits& bits) override;
void bbAtom(TNode node) override;
Abc_Obj_t* bbFormula(TNode formula);
bool solve(TNode query);
static Abc_Aig_t* currentAigM();
static Abc_Ntk_t* currentAigNtk();

private:
typedef std::unordered_map<TNode, Abc_Obj_t*, TNodeHashFunction> TNodeAigMap;
typedef std::unordered_map<Node, Abc_Obj_t*, NodeHashFunction> NodeAigMap;

static CVC4_THREAD_LOCAL Abc_Ntk_t* s_abcAigNetwork;
std::unique_ptr<context::Context> d_nullContext;
std::unique_ptr<prop::SatSolver> d_satSolver;
TNodeAigMap d_aigCache;
NodeAigMap d_bbAtoms;

NodeAigMap d_nodeToAigInput;
// the thing we are checking for sat
Abc_Obj_t* d_aigOutputNode;

void addAtom(TNode atom);
void simplifyAig();
void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) override;
Abc_Obj_t* getBBAtom(TNode atom) const override;
bool hasBBAtom(TNode atom) const override;
void cacheAig(TNode node, Abc_Obj_t* aig);
bool hasAig(TNode node);
Abc_Obj_t* getAig(TNode node);
Abc_Obj_t* mkInput(TNode input);
bool hasInput(TNode input);
void convertToCnfAndAssert();
void assertToSatSolver(Cnf_Dat_t* pCnf);
Node getModelFromSatSolver(TNode a, bool fullModel) override
{
Unreachable();
}

class Statistics
{
public:
IntStat d_numClauses;
IntStat d_numVariables;
TimerStat d_simplificationTime;
TimerStat d_cnfConversionTime;
TimerStat d_solveTime;
Statistics();
~Statistics();
};

Statistics d_statistics;
};

} // namespace bv
} // namespace theory
} // namespace CVC4
#endif // __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
9 changes: 5 additions & 4 deletions src/theory/bv/bitblast_strategies_template.h → ...v/bitblast/bitblast_strategies_template.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,15 +14,16 @@
** Implementation of bitblasting functions for various operators.
**/

#ifndef __CVC4__BITBLAST__STRATEGIES_TEMPLATE_H
#define __CVC4__BITBLAST__STRATEGIES_TEMPLATE_H
#include "cvc4_private.h"

#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
#define __CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H

#include <cmath>
#include <ostream>

#include "cvc4_private.h"
#include "expr/node.h"
#include "theory/bv/bitblast_utils.h"
#include "theory/bv/bitblast/bitblast_utils.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/rewriter.h"

Expand Down
23 changes: 6 additions & 17 deletions src/theory/bv/bitblast_utils.h → src/theory/bv/bitblast/bitblast_utils.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,24 +16,14 @@

#include "cvc4_private.h"

#ifndef __CVC4__BITBLAST__UTILS_H
#define __CVC4__BITBLAST__UTILS_H
#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
#define __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H


#include <ostream>
#include "expr/node.h"

#ifdef CVC4_USE_ABC
#include "base/main/main.h"
#include "base/abc/abc.h"

extern "C" {
#include "sat/cnf/cnf.h"
}
#endif

namespace CVC4 {

namespace theory {
namespace bv {

Expand Down Expand Up @@ -275,9 +265,8 @@ T inline sLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqu
return res;
}

} // namespace bv
} // namespace theory
} // namespace CVC4

}
}
}

#endif
#endif // __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
Loading

0 comments on commit a917cc2

Please sign in to comment.