diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-10 16:20:42 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-10 16:20:42 -0400 |
commit | c30a3426c7c2cbaff88b5183b8d8c368a393ac4d (patch) | |
tree | bd621f3766d2ae330a6c11499fe0a49958afa95d /src/theory/bv | |
parent | d4f76fdfaed04bf63bb609a5fd26b0d45a9e94f4 (diff) | |
parent | e926fd162c6cee95d31044305e3b4df90b59f9fc (diff) |
Merge remote-tracking branch 'origin/master' into segfaultfix
Diffstat (limited to 'src/theory/bv')
49 files changed, 425 insertions, 357 deletions
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index 3bff9fc95..c414ac749 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -1,19 +1,17 @@ /********************* */ /*! \file abstraction.cpp -** \verbatim -** Original author: Liana Hadarean -** Major contributors: none. -** Minor contributors (to current version): none. -** This file is part of the CVC4 project. -** Copyright (c) 2009-2013 New York University and The University of Iowa -** 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 -**/ + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ #include "theory/bv/abstraction.h" #include "theory/bv/theory_bv_utils.h" diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h index cd4c443a7..2e86c834d 100644 --- a/src/theory/bv/abstraction.h +++ b/src/theory/bv/abstraction.h @@ -1,11 +1,11 @@ - /********************* */ +/********************* */ /*! \file abstraction.h ** \verbatim ** Original author: Liana Hadarean - ** Major contributors: none. - ** Minor contributors (to current version): none. + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/aig_bitblaster.h b/src/theory/bv/aig_bitblaster.cpp index d1635f950..ce775874f 100644 --- a/src/theory/bv/aig_bitblaster.h +++ b/src/theory/bv/aig_bitblaster.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file aig_bitblaster.h +/*! \file aig_bitblaster.cpp ** \verbatim ** Original author: Liana Hadarean ** Major contributors: none - ** Minor contributors (to current version): lianah + ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -15,11 +15,6 @@ **/ #include "cvc4_private.h" - -#ifndef __CVC4__AIG__BITBLASTER_H -#define __CVC4__AIG__BITBLASTER_H - - #include "bitblaster_template.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" @@ -112,6 +107,14 @@ 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; @@ -467,13 +470,6 @@ AigBitblaster::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_solveTime); } - - -} /*bv namespace */ -} /* theory namespace */ -} /* CVC4 namespace*/ - - #else // CVC4_USE_ABC namespace CVC4 { @@ -547,6 +543,13 @@ Abc_Obj_t* mkIte<Abc_Obj_t*>(Abc_Obj_t* cond, Abc_Obj_t* a, Abc_Obj_t* b) { return NULL; } +} /* CVC4::theory::bv */ +} /* CVC4::theory */ +} /* CVC4 */ + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; Abc_Ntk_t* AigBitblaster::abcAigNetwork = NULL; @@ -647,12 +650,4 @@ AigBitblaster::Statistics::~Statistics() {} AigBitblaster::AigBitblaster() { Unreachable(); } - -} // namespace bv -} // namespace theory -} // namespace CVC4 - - #endif // CVC4_USE_ABC - -#endif // __CVC4__AIG__BITBLASTER_H diff --git a/src/theory/bv/bitblast_mode.cpp b/src/theory/bv/bitblast_mode.cpp index 91a140539..51c0290af 100644 --- a/src/theory/bv/bitblast_mode.cpp +++ b/src/theory/bv/bitblast_mode.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bitblast_mode.h b/src/theory/bv/bitblast_mode.h index 318e17467..89ecdc381 100644 --- a/src/theory/bv/bitblast_mode.h +++ b/src/theory/bv/bitblast_mode.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bitblast_strategies_template.h b/src/theory/bv/bitblast_strategies_template.h index fba744d69..62c92c0a8 100644 --- a/src/theory/bv/bitblast_strategies_template.h +++ b/src/theory/bv/bitblast_strategies_template.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file bitblast_strategies.h +/*! \file bitblast_strategies_template.h ** \verbatim ** Original author: Liana Hadarean - ** Major contributors: Liana Hadarean - ** Minor contributors (to current version): Clark Barrett, Dejan Jovanovic, Morgan Deters, Tim King + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bitblast_utils.h b/src/theory/bv/bitblast_utils.h index 91cc2d640..a236c69e8 100644 --- a/src/theory/bv/bitblast_utils.h +++ b/src/theory/bv/bitblast_utils.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Liana Hadarean ** Major contributors: none - ** Minor contributors (to current version): none. + ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 25de81f2c..ecd7013c7 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file bitblaster.h +/*! \file bitblaster_template.h ** \verbatim ** Original author: Liana Hadarean ** Major contributors: none - ** Minor contributors (to current version): lianah, Morgan Deters, Dejan Jovanovic + ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -27,6 +27,7 @@ #include "bitblast_strategies_template.h" #include "prop/sat_solver.h" #include "theory/valuation.h" +#include "theory/theory_registrar.h" class Abc_Obj_t_; typedef Abc_Obj_t_ Abc_Obj_t; @@ -57,6 +58,8 @@ namespace bv { class BitblastingRegistrar; typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; +typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + class AbstractionModule; /** @@ -70,7 +73,7 @@ class TBitblaster { protected: typedef std::vector<T> Bits; typedef __gnu_cxx::hash_map <Node, Bits, NodeHashFunction> TermDefMap; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AtomSet; + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; typedef void (*TermBBStrategy) (TNode, Bits&, TBitblaster<T>*); typedef T (*AtomBBStrategy) (TNode, TBitblaster<T>*); @@ -104,8 +107,6 @@ class TheoryBV; class TLazyBitblaster : public TBitblaster<Node> { typedef std::vector<Node> Bits; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> VarSet; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AtomSet; typedef context::CDList<prop::SatLiteral> AssertionList; typedef context::CDHashMap<prop::SatLiteral, std::vector<prop::SatLiteral> , prop::SatLiteralHashFunction> ExplanationMap; @@ -134,12 +135,12 @@ class TLazyBitblaster : public TBitblaster<Node> { prop::BVSatSolverInterface* d_satSolver; prop::CnfStream* d_cnfStream; - AssertionList d_assertedAtoms; /**< context dependent list storing the atoms + AssertionList* d_assertedAtoms; /**< context dependent list storing the atoms currently asserted by the DPLL SAT solver. */ - ExplanationMap d_explanations; /**< context dependent list of explanations for the propagated literals. + ExplanationMap* d_explanations; /**< context dependent list of explanations for the propagated literals. Only used when bvEagerPropagate option enabled. */ - VarSet d_variables; - AtomSet d_bbAtoms; + TNodeSet d_variables; + TNodeSet d_bbAtoms; AbstractionModule* d_abstraction; bool d_emptyNotify; @@ -188,7 +189,7 @@ public: */ void collectModelInfo(TheoryModel* m, bool fullModel); - typedef VarSet::const_iterator vars_iterator; + typedef TNodeSet::const_iterator vars_iterator; vars_iterator beginVars() { return d_variables.begin(); } vars_iterator endVars() { return d_variables.end(); } @@ -239,7 +240,14 @@ class EagerBitblaster : public TBitblaster<Node> { BitblastingRegistrar* d_bitblastingRegistrar; context::Context* d_nullContext; prop::CnfStream* d_cnfStream; - TNodeSet d_bbAtoms; + + theory::bv::TheoryBV* d_bv; + TNodeSet d_bbAtoms; + TNodeSet d_variables; + + Node getVarValue(TNode a, bool fullModel); + bool isSharedTerm(TNode node); + public: void addAtom(TNode atom); void makeVariable(TNode node, Bits& bits); @@ -249,12 +257,22 @@ public: bool hasBBAtom(TNode atom) const; void bbFormula(TNode formula); void storeBBAtom(TNode atom, Node atom_bb); - EagerBitblaster(); + EagerBitblaster(theory::bv::TheoryBV* theory_bv); ~EagerBitblaster(); bool assertToSat(TNode node, bool propagate = true); - bool solve(); + bool solve(); + void collectModelInfo(TheoryModel* m, bool fullModel); }; +class BitblastingRegistrar: public prop::Registrar { + EagerBitblaster* d_bitblaster; +public: + BitblastingRegistrar(EagerBitblaster* bb) + : d_bitblaster(bb) + {} + void preRegister(Node n); +}; /* class Registrar */ + class AigBitblaster : public TBitblaster<Abc_Obj_t*> { typedef std::hash_map<TNode, Abc_Obj_t*, TNodeHashFunction > TNodeAigMap; typedef std::hash_map<Node, Abc_Obj_t*, NodeHashFunction > NodeAigMap; diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index af35c0499..f9f8ff581 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file bv_eager_solver.h +/*! \file bv_eager_solver.cpp ** \verbatim - ** Original author: Liana Hadarean + ** Original author: Liana Hadarean ** Major contributors: none - ** Minor contributors (to current version): + ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -16,19 +16,19 @@ #include "theory/bv/bv_eager_solver.h" #include "theory/bv/bitblaster_template.h" -#include "theory/bv/eager_bitblaster.h" -#include "theory/bv/aig_bitblaster.h" +#include "theory/bv/options.h" using namespace std; using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; -EagerBitblastSolver::EagerBitblastSolver() +EagerBitblastSolver::EagerBitblastSolver(TheoryBV* bv) : d_assertionSet() , d_bitblaster(NULL) , d_aigBitblaster(NULL) , d_useAig(options::bitvectorAig()) + , d_bv(bv) {} EagerBitblastSolver::~EagerBitblastSolver() { @@ -53,7 +53,7 @@ void EagerBitblastSolver::initialize() { if (d_useAig) { d_aigBitblaster = new AigBitblaster(); } else { - d_bitblaster = new EagerBitblaster(); + d_bitblaster = new EagerBitblaster(d_bv); } } @@ -106,3 +106,8 @@ bool EagerBitblastSolver::hasAssertions(const std::vector<TNode> &formulas) { } return true; } + +void EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) { + AlwaysAssert(!d_useAig && d_bitblaster); + d_bitblaster->collectModelInfo(m, fullModel); +} diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h index 1fb65c9c8..37e1bd9ba 100644 --- a/src/theory/bv/bv_eager_solver.h +++ b/src/theory/bv/bv_eager_solver.h @@ -1,11 +1,11 @@ /********************* */ /*! \file bv_eager_solver.h ** \verbatim - ** Original author: Liana Hadarean + ** Original author: Liana Hadarean ** Major contributors: none - ** Minor contributors (to current version): + ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -16,6 +16,8 @@ #include "cvc4_private.h" #include "expr/node.h" +#include "theory/theory_model.h" +#include "theory/bv/theory_bv.h" #include <vector> #pragma once @@ -37,8 +39,9 @@ class EagerBitblastSolver { EagerBitblaster* d_bitblaster; AigBitblaster* d_aigBitblaster; bool d_useAig; + TheoryBV* d_bv; public: - EagerBitblastSolver(); + EagerBitblastSolver(theory::bv::TheoryBV* bv); ~EagerBitblastSolver(); bool checkSat(); void assertFormula(TNode formula); @@ -48,6 +51,7 @@ public: void turnOffAig(); bool isInitialized(); void initialize(); + void collectModelInfo(theory::TheoryModel* m, bool fullModel); }; } diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp index ff344d307..aa605de04 100644 --- a/src/theory/bv/bv_inequality_graph.cpp +++ b/src/theory/bv/bv_inequality_graph.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 9a898ebe6..3c67f506f 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -39,9 +39,6 @@ extern const ReasonId AxiomReasonId; class InequalityGraph : public context::ContextNotifyObj{ - - context::Context* d_context; - struct InequalityEdge { TermId next; ReasonId reason; @@ -126,7 +123,6 @@ class InequalityGraph : public context::ContextNotifyObj{ context::CDO<bool> d_inConflict; std::vector<TNode> d_conflict; - bool d_signed; ModelValues d_modelValues; void initializeModelValue(TNode node); @@ -214,12 +210,10 @@ public: InequalityGraph(context::Context* c, bool s = false) : ContextNotifyObj(c), - d_context(c), d_ineqNodes(), d_ineqEdges(), d_inConflict(c, false), d_conflict(), - d_signed(s), d_modelValues(c), d_disequalities(c), d_disequalitiesAlreadySplit(), diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp index 1adbb83d9..5f35f95e3 100644 --- a/src/theory/bv/bv_quick_check.cpp +++ b/src/theory/bv/bv_quick_check.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file bv_quick_check.cpp ** \verbatim - ** Original author: Liana Hadaren + ** Original author: Liana Hadarean ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index c09994c06..6c32fbb4d 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Liana Hadarean ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -26,6 +26,7 @@ #include "context/cdo.h" #include "prop/sat_solver_types.h" #include "util/statistics_registry.h" +#include "theory/bv/theory_bv_utils.h" namespace CVC4 { namespace theory { @@ -34,11 +35,6 @@ class TheoryModel; namespace bv { - - -typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; -typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; - class TLazyBitblaster; class TheoryBV; diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 8d21734db..9a314fd6a 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -5,7 +5,7 @@ ** Major contributors: Andrew Reynolds, Dejan Jovanovic ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 9dd86b5ea..4c784ce6f 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -1,18 +1,19 @@ /********************* */ -/*! \file bv_subtheory_bitblast.cpp -** \verbatim -** Original author: Liana Hadarean -** Major contributors: none -** Minor contributors (to current version): none -** This file is part of the CVC4 project. -** Copyright (c) 2009-2013 New York University and The University of Iowa -** See the file COPYING in the top-level source directory for licensing -** information.\endverbatim -** -** \brief Algebraic solver. -** -** Algebraic solver. -**/ +/*! \file bv_subtheory_algebraic.cpp + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Algebraic solver. + ** + ** Algebraic solver. + **/ + #include "util/boolean_simplification.h" #include "theory/theory_model.h" diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h index fbc8c3ff0..03588a78f 100644 --- a/src/theory/bv/bv_subtheory_algebraic.h +++ b/src/theory/bv/bv_subtheory_algebraic.h @@ -1,18 +1,18 @@ /********************* */ /*! \file bv_subtheory_algebraic.h -** \verbatim -** Original author: Liana Hadarean -** Major contributors: none -** Minor contributors (to current version): none -** This file is part of the CVC4 project. -** Copyright (c) 2009-2013 New York University and The University of Iowa -** See the file COPYING in the top-level source directory for licensing -** information.\endverbatim -** -** \brief Algebraic solver. -** -** Algebraic solver. -**/ + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Algebraic solver. + ** + ** Algebraic solver. + **/ #pragma once diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index ebe017ee1..a2a6e19ac 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -2,10 +2,10 @@ /*! \file bv_subtheory_bitblast.cpp ** \verbatim ** Original author: Dejan Jovanovic - ** Major contributors: Liana Hadarean, Clark Barrett - ** Minor contributors (to current version): Morgan Deters, Andrew Reynolds, Kshitij Bansal + ** Major contributors: Clark Barrett, Liana Hadarean + ** Minor contributors (to current version): Morgan Deters, Kshitij Bansal, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -17,9 +17,10 @@ #include "theory/bv/bv_subtheory_bitblast.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" -#include "theory/bv/lazy_bitblaster.h" +#include "theory/bv/bitblaster_template.h" #include "theory/bv/bv_quick_check.h" #include "theory/bv/options.h" +#include "theory/bv/abstraction.h" #include "theory/decision_attributes.h" #include "decision/options.h" diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 511318521..414abdcce 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -2,10 +2,10 @@ /*! \file bv_subtheory_bitblast.h ** \verbatim ** Original author: Dejan Jovanovic - ** Major contributors: none - ** Minor contributors (to current version): Morgan Deters, Andrew Reynolds, Liana Hadarean, Clark Barrett + ** Major contributors: Liana Hadarean + ** Minor contributors (to current version): Morgan Deters, Andrew Reynolds, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 179f3a44d..d2c79fec2 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -5,7 +5,7 @@ ** Major contributors: Andrew Reynolds ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 9ab6cfce4..5b9c54095 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -5,7 +5,7 @@ ** Major contributors: Andrew Reynolds ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 4b894fe2a..4f9eb0823 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -5,7 +5,7 @@ ** Major contributors: Andrew Reynolds ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index ef03166e6..b9195c7d1 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Liana Hadarean ** Major contributors: Andrew Reynolds - ** Minor contributors (to current version): Morgan Deters + ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index aef1437a0..06a1d4a44 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Liana Hadarean ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index 28501ba96..b266b591b 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/bvintropow2.cpp b/src/theory/bv/bvintropow2.cpp index d7f5d6fde..5df170e21 100644 --- a/src/theory/bv/bvintropow2.cpp +++ b/src/theory/bv/bvintropow2.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file bvintropow2.cpp + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** 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/bvintropow2.h" #include "theory/rewriter.h" #include "theory/bv/theory_bv_rewrite_rules_simplification.h" diff --git a/src/theory/bv/bvintropow2.h b/src/theory/bv/bvintropow2.h index 3844d03e1..774645560 100644 --- a/src/theory/bv/bvintropow2.h +++ b/src/theory/bv/bvintropow2.h @@ -1,3 +1,20 @@ +/********************* */ +/*! \file bvintropow2.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** 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" diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h index 01aeeab91..5ffe7032a 100644 --- a/src/theory/bv/cd_set_collection.h +++ b/src/theory/bv/cd_set_collection.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/eager_bitblaster.h b/src/theory/bv/eager_bitblaster.cpp index da73c7f09..e8fee00f5 100644 --- a/src/theory/bv/eager_bitblaster.h +++ b/src/theory/bv/eager_bitblaster.cpp @@ -1,51 +1,42 @@ /********************* */ -/*! \file eager_bitblaster.h +/*! \file eager_bitblaster.cpp ** \verbatim ** Original author: Liana Hadarean ** Major contributors: none - ** Minor contributors (to current version): lianah + ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** ** \brief ** - ** Bitblaster for the lazy bv solver. + ** Bitblaster for the eager bv solver. **/ #include "cvc4_private.h" -#ifndef __CVC4__EAGER__BITBLASTER_H -#define __CVC4__EAGER__BITBLASTER_H - - -#include "bitblaster_template.h" -#include "theory/theory_registrar.h" +#include "theory/bv/bitblaster_template.h" +#include "theory/bv/options.h" +#include "theory/theory_model.h" +#include "theory/bv/theory_bv.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" -#include "theory/bv/options.h" -namespace CVC4 { -namespace theory { -namespace bv { +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; -class BitblastingRegistrar: public prop::Registrar { - EagerBitblaster* d_bitblaster; -public: - BitblastingRegistrar(EagerBitblaster* bb) - : d_bitblaster(bb) - {} - void preRegister(Node n) { - d_bitblaster->bbAtom(n); - }; +void BitblastingRegistrar::preRegister(Node n) { + d_bitblaster->bbAtom(n); +}; -};/* class Registrar */ - -EagerBitblaster::EagerBitblaster() +EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) : TBitblaster<Node>() + , d_bv(theory_bv) , d_bbAtoms() + , d_variables() { d_bitblastingRegistrar = new BitblastingRegistrar(this); d_nullContext = new context::Context(); @@ -126,6 +117,7 @@ void EagerBitblaster::makeVariable(TNode var, Bits& bits) { for (unsigned i = 0; i < utils::getSize(var); ++i) { bits.push_back(utils::mkBitOf(var, i)); } + d_variables.insert(var); } Node EagerBitblaster::getBBAtom(TNode node) const { @@ -154,10 +146,63 @@ bool EagerBitblaster::solve() { } -} /*bv namespace */ -} /* theory namespace */ -} /* CVC4 namespace*/ +/** + * Returns the value a is currently assigned to in the SAT solver + * or null if the value is completely unassigned. + * + * @param a + * @param fullModel whether to create a "full model," i.e., add + * constants to equivalence classes that don't already have them + * + * @return + */ +Node EagerBitblaster::getVarValue(TNode a, bool fullModel) { + if (!hasBBTerm(a)) { + Assert(isSharedTerm(a)); + return Node(); + } + Bits bits; + getBBTerm(a, bits); + Integer value(0); + for (int i = bits.size() -1; i >= 0; --i) { + prop::SatValue bit_value; + if (d_cnfStream->hasLiteral(bits[i])) { + prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]); + bit_value = d_satSolver->value(bit); + Assert (bit_value != prop::SAT_VALUE_UNKNOWN); + } else { + // the bit is unconstrainted so we can give it an arbitrary value + bit_value = prop::SAT_VALUE_FALSE; + } + Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0); + value = value * 2 + bit_int; + } + return utils::mkConst(BitVector(bits.size(), value)); +} +void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { + TNodeSet::const_iterator it = d_variables.begin(); + for (; it!= d_variables.end(); ++it) { + TNode var = *it; + if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { + Node const_value = getVarValue(var, fullModel); + if(const_value == Node()) { + if( fullModel ){ + // if the value is unassigned just set it to zero + const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); + } + } + if(const_value != Node()) { + Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= " + << var << " " + << const_value << "))\n"; + m->assertEquality(var, const_value, true); + } + } + } +} -#endif +bool EagerBitblaster::isSharedTerm(TNode node) { + return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); +} diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 4b2bba741..b4ecc1d3d 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -25,7 +25,7 @@ constant CONST_BITVECTOR \ ::CVC4::BitVector \ ::CVC4::BitVectorHashFunction \ "util/bitvector.h" \ - "a fixed-width bit-vector constant" + "a fixed-width bit-vector constant; payload is an instance of the CVC4::BitVector class" enumerator BITVECTOR_TYPE \ "::CVC4::theory::bv::BitVectorEnumerator" \ @@ -36,101 +36,101 @@ well-founded BITVECTOR_TYPE \ "(*CVC4::theory::TypeEnumerator(%TYPE%))" \ "theory/type_enumerator.h" -operator BITVECTOR_CONCAT 2: "bit-vector concatenation" -operator BITVECTOR_AND 2: "bitwise and" -operator BITVECTOR_OR 2: "bitwise or" -operator BITVECTOR_XOR 2: "bitwise xor" -operator BITVECTOR_NOT 1 "bitwise not" -operator BITVECTOR_NAND 2 "bitwise nand" -operator BITVECTOR_NOR 2 "bitwise nor" -operator BITVECTOR_XNOR 2 "bitwise xnor" -operator BITVECTOR_COMP 2 "equality comparison (returns one bit)" -operator BITVECTOR_MULT 2: "bit-vector multiplication" -operator BITVECTOR_PLUS 2: "bit-vector addition" -operator BITVECTOR_SUB 2 "bit-vector subtraction" -operator BITVECTOR_NEG 1 "bit-vector unary negation" -operator BITVECTOR_UDIV 2 "bit-vector unsigned division, truncating towards 0 (undefined if divisor is 0)" -operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating division (undefined if divisor is 0)" -operator BITVECTOR_SDIV 2 "bit-vector 2's complement signed division" -operator BITVECTOR_SREM 2 "bit-vector 2's complement signed remainder (sign follows dividend)" -operator BITVECTOR_SMOD 2 "bit-vector 2's complement signed remainder (sign follows divisor)" -# total division kinds -operator BITVECTOR_UDIV_TOTAL 2 "bit-vector total unsigned division, truncating towards 0 (undefined if divisor is 0)" -operator BITVECTOR_UREM_TOTAL 2 "bit-vector total unsigned remainder from truncating division (undefined if divisor is 0)" - -operator BITVECTOR_SHL 2 "bit-vector left shift" -operator BITVECTOR_LSHR 2 "bit-vector logical shift right" -operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right" -operator BITVECTOR_ULT 2 "bit-vector unsigned less than" -operator BITVECTOR_ULE 2 "bit-vector unsigned less than or equal" -operator BITVECTOR_UGT 2 "bit-vector unsigned greater than" -operator BITVECTOR_UGE 2 "bit-vector unsigned greater than or equal" -operator BITVECTOR_SLT 2 "bit-vector signed less than" -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" - -operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting" -operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bitblasting ackerman expansion of bvudiv" -operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bitblasting ackerman expansion of bvurem" +operator BITVECTOR_CONCAT 2: "concatenation of two or more bit-vectors" +operator BITVECTOR_AND 2: "bitwise and of two or more bit-vectors" +operator BITVECTOR_OR 2: "bitwise or of two or more bit-vectors" +operator BITVECTOR_XOR 2: "bitwise xor of two or more bit-vectors" +operator BITVECTOR_NOT 1 "bitwise not of a bit-vector" +operator BITVECTOR_NAND 2 "bitwise nand of two bit-vectors" +operator BITVECTOR_NOR 2 "bitwise nor of two bit-vectors" +operator BITVECTOR_XNOR 2 "bitwise xnor of two bit-vectors" +operator BITVECTOR_COMP 2 "equality comparison of two bit-vectors (returns one bit)" +operator BITVECTOR_MULT 2: "multiplication of two or more bit-vectors" +operator BITVECTOR_PLUS 2: "addition of two or more bit-vectors" +operator BITVECTOR_SUB 2 "subtraction of two bit-vectors" +operator BITVECTOR_NEG 1 "unary negation of a bit-vector" +operator BITVECTOR_UDIV 2 "unsigned division of two bit-vectors, truncating towards 0 (undefined if divisor is 0)" +operator BITVECTOR_UREM 2 "unsigned remainder from truncating division of two bit-vectors (undefined if divisor is 0)" +operator BITVECTOR_SDIV 2 "2's complement signed division" +operator BITVECTOR_SREM 2 "2's complement signed remainder (sign follows dividend)" +operator BITVECTOR_SMOD 2 "2's complement signed remainder (sign follows divisor)" +# total division kinds +operator BITVECTOR_UDIV_TOTAL 2 "unsigned division of two bit-vectors, truncating towards 0 (defined to be the all-ones bit pattern, if divisor is 0)" +operator BITVECTOR_UREM_TOTAL 2 "unsigned remainder from truncating division of two bit-vectors (defined to be equal to the dividend, if divisor is 0)" + +operator BITVECTOR_SHL 2 "bit-vector shift left (the two bit-vector parameters must have same width)" +operator BITVECTOR_LSHR 2 "bit-vector logical shift right (the two bit-vector parameters must have same width)" +operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right (the two bit-vector parameters must have same width)" +operator BITVECTOR_ULT 2 "bit-vector unsigned less than (the two bit-vector parameters must have same width)" +operator BITVECTOR_ULE 2 "bit-vector unsigned less than or equal (the two bit-vector parameters must have same width)" +operator BITVECTOR_UGT 2 "bit-vector unsigned greater than (the two bit-vector parameters must have same width)" +operator BITVECTOR_UGE 2 "bit-vector unsigned greater than or equal (the two bit-vector parameters must have same width)" +operator BITVECTOR_SLT 2 "bit-vector signed less than (the two bit-vector parameters must have same width)" +operator BITVECTOR_SLE 2 "bit-vector signed less than or equal (the two bit-vector parameters must have same width)" +operator BITVECTOR_SGT 2 "bit-vector signed greater than (the two bit-vector parameters must have same width)" +operator BITVECTOR_SGE 2 "bit-vector signed greater than or equal (the two bit-vector parameters must have same width)" + +operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bit-blasting (internal-only symbol)" +operator BITVECTOR_ACKERMANIZE_UDIV 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvudiv (internal-only symbol)" +operator BITVECTOR_ACKERMANIZE_UREM 1 "term to be treated as a variable; used for eager bit-blasting Ackermann expansion of bvurem (internal-only symbol)" constant BITVECTOR_BITOF_OP \ ::CVC4::BitVectorBitOf \ ::CVC4::BitVectorBitOfHashFunction \ "util/bitvector.h" \ - "operator for the bit-vector boolean bit extract" + "operator for the bit-vector boolean bit extract; payload is an instance of the CVC4::BitVectorBitOf class" constant BITVECTOR_EXTRACT_OP \ ::CVC4::BitVectorExtract \ ::CVC4::BitVectorExtractHashFunction \ "util/bitvector.h" \ - "operator for the bit-vector extract" + "operator for the bit-vector extract; payload is an instance of the CVC4::BitVectorExtract class" constant BITVECTOR_REPEAT_OP \ ::CVC4::BitVectorRepeat \ "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRepeat >" \ "util/bitvector.h" \ - "operator for the bit-vector repeat" + "operator for the bit-vector repeat; payload is an instance of the CVC4::BitVectorRepeat class" constant BITVECTOR_ZERO_EXTEND_OP \ ::CVC4::BitVectorZeroExtend \ "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorZeroExtend >" \ "util/bitvector.h" \ - "operator for the bit-vector zero-extend" + "operator for the bit-vector zero-extend; payload is an instance of the CVC4::BitVectorZeroExtend class" constant BITVECTOR_SIGN_EXTEND_OP \ ::CVC4::BitVectorSignExtend \ "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSignExtend >" \ "util/bitvector.h" \ - "operator for the bit-vector sign-extend" + "operator for the bit-vector sign-extend; payload is an instance of the CVC4::BitVectorSignExtend class" constant BITVECTOR_ROTATE_LEFT_OP \ ::CVC4::BitVectorRotateLeft \ "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateLeft >" \ "util/bitvector.h" \ - "operator for the bit-vector rotate left" + "operator for the bit-vector rotate left; payload is an instance of the CVC4::BitVectorRotateLeft class" constant BITVECTOR_ROTATE_RIGHT_OP \ ::CVC4::BitVectorRotateRight \ "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateRight >" \ "util/bitvector.h" \ - "operator for the bit-vector rotate right" + "operator for the bit-vector rotate right; payload is an instance of the CVC4::BitVectorRotateRight class" -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" -parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend" -parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left" -parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right" +parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term" +parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term" +parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term" +parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term" +parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term" +parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term" +parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term" constant INT_TO_BITVECTOR_OP \ ::CVC4::IntToBitVector \ "::CVC4::UnsignedHashFunction< ::CVC4::IntToBitVector >" \ "util/bitvector.h" \ - "operator for the integer conversion to bit-vector" -parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector" -operator BITVECTOR_TO_NAT 1 "bit-vector conversion to (nonnegative) integer" + "operator for the integer conversion to bit-vector; payload is an instance of the CVC4::IntToBitVector class" +parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term" +operator BITVECTOR_TO_NAT 1 "bit-vector conversion to (nonnegative) integer; parameter is a bit-vector" typerule CONST_BITVECTOR ::CVC4::theory::bv::BitVectorConstantTypeRule @@ -142,7 +142,7 @@ typerule BITVECTOR_NAND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_NOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_XNOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule -typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorCompRule +typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorCompTypeRule typerule BITVECTOR_MULT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule typerule BITVECTOR_PLUS ::CVC4::theory::bv::BitVectorFixedWidthTypeRule @@ -178,7 +178,7 @@ typerule BITVECTOR_ACKERMANIZE_UREM ::CVC4::theory::bv::BitVectorAckermanization typerule BITVECTOR_EXTRACT_OP ::CVC4::theory::bv::BitVectorExtractOpTypeRule typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule typerule BITVECTOR_BITOF ::CVC4::theory::bv::BitVectorBitOfTypeRule -typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatRule +typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatTypeRule typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule diff --git a/src/theory/bv/lazy_bitblaster.h b/src/theory/bv/lazy_bitblaster.cpp index 013e230f6..f721a22f0 100644 --- a/src/theory/bv/lazy_bitblaster.h +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -1,25 +1,20 @@ /********************* */ -/*! \file lazy_bitblaster.h -** \verbatim -** Original author: Liana Hadarean -** Major contributors: none -** Minor contributors (to current version): lianah -** This file is part of the CVC4 project. -** Copyright (c) 2009-2013 New York University and The University of Iowa -** See the file COPYING in the top-level source directory for licensing -** information.\endverbatim -** -** \brief -** -** Bitblaster for the lazy bv solver. -**/ +/*! \file lazy_bitblaster.cpp + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Bitblaster for the lazy bv solver. + ** + ** Bitblaster for the lazy bv solver. + **/ #include "cvc4_private.h" - -#ifndef __CVC4__LAZY__BITBLASTER_H -#define __CVC4__LAZY__BITBLASTER_H - - #include "bitblaster_template.h" #include "theory_bv_utils.h" #include "theory/rewriter.h" @@ -31,16 +26,17 @@ #include "theory/theory_model.h" #include "theory/bv/abstraction.h" -namespace CVC4 { -namespace theory { -namespace bv { +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; + TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name, bool emptyNotify) - : TBitblaster() + : TBitblaster<Node>() , d_bv(bv) , d_ctx(c) - , d_assertedAtoms(c) - , d_explanations(c) + , d_assertedAtoms(new(true) context::CDList<prop::SatLiteral>(c)) + , d_explanations(new(true) ExplanationMap(c)) , d_variables() , d_bbAtoms() , d_abstraction(NULL) @@ -192,8 +188,8 @@ void TLazyBitblaster::explain(TNode atom, std::vector<TNode>& explanation) { ++(d_statistics.d_numExplainedPropagations); if (options::bvEagerExplanations()) { - Assert (d_explanations.find(lit) != d_explanations.end()); - const std::vector<prop::SatLiteral>& literal_explanation = d_explanations[lit].get(); + Assert (d_explanations->find(lit) != d_explanations->end()); + const std::vector<prop::SatLiteral>& literal_explanation = (*d_explanations)[lit].get(); for (unsigned i = 0; i < literal_explanation.size(); ++i) { explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); } @@ -241,7 +237,7 @@ bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) { prop::SatValue ret = d_satSolver->assertAssumption(markerLit, propagate); - d_assertedAtoms.push_back(markerLit); + d_assertedAtoms->push_back(markerLit); return ret == prop::SAT_VALUE_TRUE || ret == prop::SAT_VALUE_UNKNOWN; } @@ -256,24 +252,24 @@ bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) { bool TLazyBitblaster::solve() { if (Trace.isOn("bitvector")) { Trace("bitvector") << "TLazyBitblaster::solve() asserted atoms "; - context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms.begin(); - for (; it != d_assertedAtoms.end(); ++it) { + context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms->begin(); + for (; it != d_assertedAtoms->end(); ++it) { Trace("bitvector") << " " << d_cnfStream->getNode(*it) << "\n"; } } - Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; + Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n"; return prop::SAT_VALUE_TRUE == d_satSolver->solve(); } prop::SatValue TLazyBitblaster::solveWithBudget(unsigned long budget) { if (Trace.isOn("bitvector")) { Trace("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms "; - context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms.begin(); - for (; it != d_assertedAtoms.end(); ++it) { + context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms->begin(); + for (; it != d_assertedAtoms->end(); ++it) { Trace("bitvector") << " " << d_cnfStream->getNode(*it) << "\n"; } } - Debug("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms " << d_assertedAtoms.size() <<"\n"; + Debug("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms " << d_assertedAtoms->size() <<"\n"; return d_satSolver->solve(budget); } @@ -327,10 +323,10 @@ TLazyBitblaster::Statistics::~Statistics() { bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) { if(options::bvEagerExplanations()) { // compute explanation - if (d_lazyBB->d_explanations.find(lit) == d_lazyBB->d_explanations.end()) { + if (d_lazyBB->d_explanations->find(lit) == d_lazyBB->d_explanations->end()) { std::vector<prop::SatLiteral> literal_explanation; d_lazyBB->d_satSolver->explain(lit, literal_explanation); - d_lazyBB->d_explanations.insert(lit, literal_explanation); + d_lazyBB->d_explanations->insert(lit, literal_explanation); } else { // we propagated it at a lower level return true; @@ -453,7 +449,7 @@ Node TLazyBitblaster::getVarValue(TNode a, bool fullModel) { } void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { - __gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin(); + TNodeSet::iterator it = d_variables.begin(); for (; it!= d_variables.end(); ++it) { TNode var = *it; if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { @@ -478,8 +474,10 @@ void TLazyBitblaster::clearSolver() { Assert (d_ctx->getLevel() == 0); delete d_satSolver; delete d_cnfStream; - d_assertedAtoms = context::CDList<prop::SatLiteral>(d_ctx); - d_explanations = ExplanationMap(d_ctx); + d_assertedAtoms->deleteSelf(); + d_assertedAtoms = new(true) context::CDList<prop::SatLiteral>(d_ctx); + d_explanations->deleteSelf(); + d_explanations = new(true) ExplanationMap(d_ctx); d_bbAtoms.clear(); d_variables.clear(); d_termCache.clear(); @@ -495,9 +493,3 @@ void TLazyBitblaster::clearSolver() { (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this); d_satSolver->setNotify(notify); } - -} /*bv namespace */ -} /* theory namespace */ -} /* CVC4 namespace*/ - -#endif diff --git a/src/theory/bv/options b/src/theory/bv/options index b5a4fea93..81d88421b 100644 --- a/src/theory/bv/options +++ b/src/theory/bv/options @@ -5,14 +5,14 @@ module BV "theory/bv/options.h" Bitvector theory -# Option to set the bit-blasting mode (lazy, eager, eager-aig) +# Option to set the bit-blasting mode (lazy, eager) option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :handler CVC4::theory::bv::stringToBitblastMode :default CVC4::theory::bv::BITBLAST_MODE_LAZY :read-write :include "theory/bv/bitblast_mode.h" :handler-include "theory/bv/options_handlers.h" choose bitblasting mode, see --bitblast=help # Options for eager bit-blasting -option bitvectorAig --bitblast-aig bool :default false :predicate CVC4::theory::bv::abcEnabledBuild :predicate-include "theory/bv/options_handlers.h" :read-write :link --bitblast=eager +option bitvectorAig --bitblast-aig bool :default false :predicate CVC4::theory::bv::abcEnabledBuild :predicate-include "theory/bv/options_handlers.h" :read-write :link --bitblast=eager :link --bv-aig-simp="balance;drw" bitblast by first converting to AIG (only if --bitblast=eager) expert-option bitvectorAigSimplifications --bv-aig-simp=FILE std::string :default "" :predicate CVC4::theory::bv::abcEnabledBuild :read-write :link --bitblast-aig diff --git a/src/theory/bv/options_handlers.h b/src/theory/bv/options_handlers.h index 5d85a1be0..c917aa9dd 100644 --- a/src/theory/bv/options_handlers.h +++ b/src/theory/bv/options_handlers.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -56,9 +56,6 @@ lazy (default)\n\ \n\ eager\n\ + Bitblast eagerly to bv SAT solver\n\ -\n\ -aig\n\ -+ Bitblast eagerly to bv SAT solver by converting to AIG\n\ "; inline BitblastMode stringToBitblastMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { @@ -70,7 +67,8 @@ inline BitblastMode stringToBitblastMode(std::string option, std::string optarg, options::bitvectorEqualitySolver.set(true); } if (!options::bitvectorEqualitySlicer.wasSetByUser()) { - if (options::incrementalSolving()) { + if (options::incrementalSolving() || + options::produceModels()) { options::bitvectorEqualitySlicer.set(BITVECTOR_SLICER_OFF); } else { options::bitvectorEqualitySlicer.set(BITVECTOR_SLICER_AUTO); @@ -85,10 +83,6 @@ inline BitblastMode stringToBitblastMode(std::string option, std::string optarg, } return BITBLAST_MODE_LAZY; } else if(optarg == "eager") { - if (options::produceModels()) { - throw OptionException(std::string("Eager bit-blasting does not currently support model generation. \n\ - Try --bitblast=lazy")); - } if (options::incrementalSolving() && options::incrementalSolving.wasSetByUser()) { @@ -96,14 +90,6 @@ inline BitblastMode stringToBitblastMode(std::string option, std::string optarg, Try --bitblast=lazy")); } - if (!options::bitvectorAig.wasSetByUser()) { - options::bitvectorAig.set(true); - abcEnabledBuild("--bitblast-aig", true, NULL); - } - if (!options::bitvectorAigSimplifications.wasSetByUser()) { - // due to a known bug in abc switching to using drw instead of rw - options::bitvectorAigSimplifications.set("balance;drw"); - } if (!options::bitvectorToBool.wasSetByUser()) { options::bitvectorToBool.set(true); } diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index c37c8089d..a7587bedf 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index 15c0b9c0b..7b55054bc 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index d3da10a90..4abf25bb1 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -1,18 +1,16 @@ /********************* */ /*! \file theory_bv.cpp -** \verbatim -** Original author: Dejan Jovanovic -** Major contributors: Morgan Deters, Liana Hadarean -** Minor contributors (to current version): Tim King, Kshitij Bansal, Clark Barrett, Andrew Reynolds -** This file is part of the CVC4 project. -** Copyright (c) 2009-2013 New York University and The University of Iowa -** 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 + ** \verbatim + ** Original author: Dejan Jovanovic + ** Major contributors: Liana Hadarean + ** Minor contributors (to current version): Tim King, Kshitij Bansal, Clark Barrett, Andrew Reynolds, Morgan Deters, Martin Brain <> + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** [[ Add lengthier description here ]] + ** \todo document this file **/ #include "smt/options.h" @@ -61,7 +59,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& { if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - d_eagerSolver = new EagerBitblastSolver(); + d_eagerSolver = new EagerBitblastSolver(this); return; } @@ -434,7 +432,9 @@ void TheoryBV::check(Effort e) void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){ Assert(!inConflict()); - + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + d_eagerSolver->collectModelInfo(m, fullModel); + } for (unsigned i = 0; i < d_subtheories.size(); ++i) { if (d_subtheories[i]->isComplete()) { d_subtheories[i]->collectModelInfo(m, fullModel); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 26ed8c296..22d9f6775 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Morgan Deters ** Major contributors: Dejan Jovanovic, Liana Hadarean - ** Minor contributors (to current version): Clark Barrett, Kshitij Bansal, Tim King, Andrew Reynolds + ** Minor contributors (to current version): Clark Barrett, Kshitij Bansal, Tim King, Andrew Reynolds, Martin Brain <> ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -105,7 +105,7 @@ private: /** - * Return the uinterpreted function symbol corresponding to division-by-zero + * Return the uninterpreted function symbol corresponding to division-by-zero * for this particular bit-width * @param k should be UREM or UDIV * @param width @@ -121,7 +121,7 @@ private: NodeSet d_staticLearnCache; /** - * Maps from bit-vector width to divison-by-zero uninterpreted + * Maps from bit-vector width to division-by-zero uninterpreted * function symbols. */ __gnu_cxx::hash_map<unsigned, Node> d_BVDivByZero; @@ -209,6 +209,7 @@ private: friend class LazyBitblaster; friend class TLazyBitblaster; + friend class EagerBitblaster; friend class BitblastSolver; friend class EqualitySolver; friend class CoreSolver; diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 5e85cb145..bc9095f03 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -5,7 +5,7 @@ ** Major contributors: Liana Hadarean ** Minor contributors (to current version): Tim King, Clark Barrett, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index db774ebe3..1f8799682 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -5,7 +5,7 @@ ** Major contributors: Clark Barrett ** Minor contributors (to current version): Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h index 43acfef75..676df5dde 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_core.h +++ b/src/theory/bv/theory_bv_rewrite_rules_core.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Tim King, Clark Barrett, Liana Hadarean, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 3e6e02952..21b59fa8c 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -5,7 +5,7 @@ ** Major contributors: Clark Barrett ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h index 6c0ba90d4..0442c47d9 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h +++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters, Clark Barrett ** Minor contributors (to current version): Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index c8705e121..3bf390ded 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -2,10 +2,10 @@ /*! \file theory_bv_rewrite_rules_simplification.h ** \verbatim ** Original author: Liana Hadarean - ** Major contributors: Clark Barrett - ** Minor contributors (to current version): Morgan Deters, Dejan Jovanovic, Tim King + ** Major contributors: none + ** Minor contributors (to current version): Morgan Deters, Dejan Jovanovic, Tim King, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 4a0da44cc..306a3bd97 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -5,7 +5,7 @@ ** Major contributors: Liana Hadarean ** Minor contributors (to current version): Tim King, Clark Barrett, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index def8e24fe..42bccb534 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters, Liana Hadarean ** Minor contributors (to current version): Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index c1829ce69..81a2d9a27 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -2,16 +2,16 @@ /*! \file theory_bv_type_rules.h ** \verbatim ** Original author: Dejan Jovanovic - ** Major contributors: Liana Hadarean, Christopher L. Conway, Morgan Deters + ** Major contributors: Christopher L. Conway, Liana Hadarean, Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Bitvector theory. + ** \brief Bitvector theory typing rules ** - ** Bitvector theory. + ** Bitvector theory typing rules. **/ #include "cvc4_private.h" @@ -36,18 +36,17 @@ public: } return nodeManager->mkBitVectorType(n.getConst<BitVector>().getSize()); } -}; - +};/* class BitVectorConstantTypeRule */ class BitVectorBitOfTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate) { - + if(check) { BitVectorBitOf info = n.getOperator().getConst<BitVectorBitOf>(); TypeNode t = n[0].getType(check); - + if (!t.isBitVector()) { throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } @@ -55,12 +54,11 @@ public: throw TypeCheckingExceptionPrivate(n, "extract index is larger than the bitvector size"); } } - return nodeManager->booleanType(); + return nodeManager->booleanType(); } -}; - +};/* class BitVectorBitOfTypeRule */ -class BitVectorCompRule { +class BitVectorCompTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { @@ -73,7 +71,7 @@ public: } return nodeManager->mkBitVectorType(1); } -}; +};/* class BitVectorCompTypeRule */ class BitVectorFixedWidthTypeRule { public: @@ -94,7 +92,7 @@ public: } return t; } -}; +};/* class BitVectorFixedWidthTypeRule */ class BitVectorPredicateTypeRule { public: @@ -112,7 +110,7 @@ public: } return nodeManager->booleanType(); } -}; +};/* class BitVectorPredicateTypeRule */ class BitVectorEagerAtomTypeRule { public: @@ -126,7 +124,7 @@ public: } return nodeManager->booleanType(); } -}; +};/* class BitVectorEagerAtomTypeRule */ class BitVectorAckermanizationUdivTypeRule { public: @@ -138,9 +136,9 @@ public: throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } } - return lhsType; + return lhsType; } -}; +};/* class BitVectorAckermanizationUdivTypeRule */ class BitVectorAckermanizationUremTypeRule { public: @@ -152,10 +150,9 @@ public: throw TypeCheckingExceptionPrivate(n, "expecting bit-vector term"); } } - return lhsType; + return lhsType; } -}; - +};/* class BitVectorAckermanizationUremTypeRule */ class BitVectorExtractTypeRule { public: @@ -181,7 +178,7 @@ public: } return nodeManager->mkBitVectorType(extractInfo.high - extractInfo.low + 1); } -}; +};/* class BitVectorExtractTypeRule */ class BitVectorExtractOpTypeRule { public: @@ -190,9 +187,9 @@ public: Assert(n.getKind() == kind::BITVECTOR_EXTRACT_OP); return nodeManager->builtinOperatorType(); } -}; +};/* class BitVectorExtractOpTypeRule */ -class BitVectorConcatRule { +class BitVectorConcatTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { @@ -211,7 +208,7 @@ public: } return nodeManager->mkBitVectorType(size); } -}; +};/* class BitVectorConcatTypeRule */ class BitVectorRepeatTypeRule { public: @@ -227,7 +224,7 @@ public: unsigned repeatAmount = n.getOperator().getConst<BitVectorRepeat>(); return nodeManager->mkBitVectorType(repeatAmount * t.getBitVectorSize()); } -}; +};/* class BitVectorRepeatTypeRule */ class BitVectorExtendTypeRule { public: @@ -245,7 +242,7 @@ public: (unsigned) n.getOperator().getConst<BitVectorZeroExtend>(); return nodeManager->mkBitVectorType(extendAmount + t.getBitVectorSize()); } -}; +};/* class BitVectorExtendTypeRule */ class BitVectorConversionTypeRule { public: @@ -268,7 +265,7 @@ public: InternalError("bv-conversion typerule invoked for non-bv-conversion kind"); } -}; +};/* class BitVectorConversionTypeRule */ class CardinalityComputer { public: diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index 705a784f2..824dc5b92 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file theory_bv_utils.h +/*! \file theory_bv_utils.cpp ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Liana Hadarean - ** Minor contributors (to current version): Clark Barrett, Morgan Deters, Kshitij Bansal + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 9679c0260..6ebc9db92 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Dejan Jovanovic ** Major contributors: Liana Hadarean - ** Minor contributors (to current version): Clark Barrett, Morgan Deters, Kshitij Bansal + ** Minor contributors (to current version): Kshitij Bansal, Clark Barrett, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -24,10 +24,13 @@ #include <sstream> #include "expr/node_manager.h" - namespace CVC4 { namespace theory { namespace bv { + +typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; +typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; + namespace utils { inline uint32_t pow2(uint32_t power) { @@ -254,8 +257,6 @@ inline unsigned isPow2Const(TNode node) { return bv.isPow2(); } -typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> TNodeSet; - inline Node mkOr(const std::vector<Node>& nodes) { std::set<TNode> all; all.insert(nodes.begin(), nodes.end()); diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h index 01741737f..1d835dd23 100644 --- a/src/theory/bv/type_enumerator.h +++ b/src/theory/bv/type_enumerator.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** |