src/proof/bitvector_proof.h

   1 /*********************                                                        */
   2 /*! \file bitvector_proof.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Guy Katz, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Bitvector proof
  13  **
  14  ** Bitvector proof
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__BITVECTOR__PROOF_H
  20 #define __CVC4__BITVECTOR__PROOF_H
  21
  22 #include <iostream>
  23 #include <set>
  24 #include <sstream>
  25 #include <unordered_map>
  26 #include <unordered_set>
  27 #include <vector>
  28
  29 #include "expr/expr.h"
  30 #include "proof/theory_proof.h"
  31 #include "prop/bvminisat/core/Solver.h"
  32
  33
  34 namespace CVC4 {
  35
  36 namespace prop {
  37 class CnfStream;
  38 } /* namespace CVC4::prop */
  39
  40 namespace theory {
  41 namespace bv {
  42 class TheoryBV;
  43 template <class T> class TBitblaster;
  44 } /* namespace CVC4::theory::bv */
  45 } /* namespace CVC4::theory */
  46
  47 class CnfProof;
  48 } /* namespace CVC4 */
  49
  50 namespace CVC4 {
  51
  52 template <class Solver> class TSatProof;
  53 typedef TSatProof< CVC4::BVMinisat::Solver> BVSatProof;
  54
  55 template <class Solver> class LFSCSatProof;
  56 typedef LFSCSatProof< CVC4::BVMinisat::Solver> LFSCBVSatProof;
  57
  58 typedef std::unordered_set<Expr, ExprHashFunction> ExprSet;
  59 typedef std::unordered_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId;
  60 typedef std::unordered_map<Expr, unsigned, ExprHashFunction> ExprToId;
  61 typedef std::unordered_map<Expr, Expr, ExprHashFunction> ExprToExpr;
  62 typedef std::unordered_map<Expr, std::string, ExprHashFunction> ExprToString;
  63
  64 class BitVectorProof : public TheoryProof {
  65 protected:
  66   ExprSet d_declarations;
  67
  68   ExprSet d_usedBB; // terms and formulas that are actually relevant to the proof
  69
  70   ExprSet d_seenBBTerms; // terms that need to be bit-blasted
  71   std::vector<Expr> d_bbTerms; // order of bit-blasting
  72   ExprToExpr d_bbAtoms; // atoms that need to be bit-blasted
  73
  74   // map from Expr representing normalized lemma to ClauseId in SAT solver
  75   ExprToClauseId d_bbConflictMap;
  76   BVSatProof* d_resolutionProof;
  77
  78   CnfProof* d_cnfProof;
  79
  80   bool d_isAssumptionConflict;
  81   theory::bv::TBitblaster<Node>* d_bitblaster;
  82   std::string getBBTermName(Expr expr);
  83
  84   std::map<Expr,std::string> d_constantLetMap;
  85   bool d_useConstantLetification;
  86
  87   context::Context d_fakeContext;
  88 public:
  89   BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine);
  90
  91   void initSatProof(CVC4::BVMinisat::Solver* solver);
  92   void initCnfProof(prop::CnfStream* cnfStream, context::Context* ctx);
  93   void setBitblaster(theory::bv::TBitblaster<Node>* bb);
  94
  95   BVSatProof* getSatProof();
  96   CnfProof* getCnfProof() {return d_cnfProof; }
  97   void finalizeConflicts(std::vector<Expr>& conflicts);
  98
  99   void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr);
 100   void startBVConflict(CVC4::BVMinisat::Solver::TLit lit);
 101   /**
 102    * All the
 103    *
 104    * @param confl an inconsistent set of bv literals
 105    */
 106   void endBVConflict(const BVMinisat::Solver::TLitVec& confl);
 107   void markAssumptionConflict() { d_isAssumptionConflict = true; }
 108   bool isAssumptionConflict() { return d_isAssumptionConflict; }
 109
 110   void registerTermBB(Expr term);
 111   void registerAtomBB(Expr atom, Expr atom_bb);
 112
 113   virtual void registerTerm(Expr term);
 114
 115   virtual void printTermBitblasting(Expr term, std::ostream& os) = 0;
 116   virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap) = 0;
 117   virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os) = 0;
 118
 119   virtual void printBitblasting(std::ostream& os, std::ostream& paren) = 0;
 120   virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap) = 0;
 121   virtual const std::set<Node>* getAtomsInBitblastingProof() = 0;
 122   virtual void calculateAtomsInBitblastingProof() = 0;
 123 };
 124
 125 class LFSCBitVectorProof: public BitVectorProof {
 126
 127   void printConstant(Expr term, std::ostream& os);
 128   void printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map);
 129   void printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map);
 130   void printPredicate(Expr term, std::ostream& os, const ProofLetMap& map);
 131   void printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map);
 132   void printBitOf(Expr term, std::ostream& os, const ProofLetMap& map);
 133
 134   ExprToString d_exprToVariableName;
 135   ExprToString d_assignedAliases;
 136   std::map<std::string, std::string> d_aliasToBindDeclaration;
 137   std::string assignAlias(Expr expr);
 138   bool hasAlias(Expr expr);
 139
 140   std::set<Node> d_atomsInBitblastingProof;
 141
 142 public:
 143   LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
 144     :BitVectorProof(bv, proofEngine)
 145   {}
 146   virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
 147   virtual void printOwnedSort(Type type, std::ostream& os);
 148   virtual void printTermBitblasting(Expr term, std::ostream& os);
 149   virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap);
 150   virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os);
 151   virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
 152   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
 153   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
 154   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
 155   virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
 156   virtual void printBitblasting(std::ostream& os, std::ostream& paren);
 157   virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap);
 158   void calculateAtomsInBitblastingProof();
 159   const std::set<Node>* getAtomsInBitblastingProof();
 160   void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
 161   void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2);
 162 };
 163
 164 }/* CVC4 namespace */
 165
 166 #endif /* __CVC4__BITVECTOR__PROOF_H */