src/theory/quantifiers/bv_inverter.h

   1 /*********************                                                        */
   2 /*! \file bv_inverter.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   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 inverse rules for bit-vector operators
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef __CVC4__BV_INVERTER_H
  18 #define __CVC4__BV_INVERTER_H
  19
  20 #include <map>
  21 #include <unordered_map>
  22 #include <unordered_set>
  23 #include <vector>
  24
  25 #include "expr/node.h"
  26
  27 namespace CVC4 {
  28 namespace theory {
  29 namespace quantifiers {
  30
  31 /** BvInverterQuery
  32  *
  33  * This is a virtual class for queries
  34  * required by the BvInverter class.
  35  */
  36 class BvInverterQuery
  37 {
  38  public:
  39   BvInverterQuery() {}
  40   ~BvInverterQuery() {}
  41   /** returns the current model value of n */
  42   virtual Node getModelValue(Node n) = 0;
  43   /** returns a bound variable of type tn */
  44   virtual Node getBoundVariable(TypeNode tn) = 0;
  45 };
  46
  47 // inverter class
  48 // TODO : move to theory/bv/ if generally useful?
  49 class BvInverter
  50 {
  51  public:
  52   BvInverter() {}
  53   ~BvInverter() {}
  54   /** get dummy fresh variable of type tn, used as argument for sv */
  55   Node getSolveVariable(TypeNode tn);
  56
  57   /** Get path to pv in lit, replace that occurrence by sv and all others by
  58    * pvs. If return value R is non-null, then : lit.path = pv R.path = sv
  59    *   R.path' = pvs for all lit.path' = pv, where path' != path
  60    */
  61   Node getPathToPv(
  62       Node lit, Node pv, Node sv, Node pvs, std::vector<unsigned>& path);
  63
  64   /** solveBvLit
  65    * solve for sv in lit, where lit.path = sv
  66    * status accumulates side conditions
  67    */
  68   Node solveBvLit(Node sv,
  69                   Node lit,
  70                   std::vector<unsigned>& path,
  71                   BvInverterQuery* m);
  72
  73  private:
  74   /** Dummy variables for each type */
  75   std::map<TypeNode, Node> d_solve_var;
  76
  77   /** Helper function for getPathToPv */
  78   Node getPathToPv(Node lit,
  79                    Node pv,
  80                    Node sv,
  81                    std::vector<unsigned>& path,
  82                    std::unordered_set<TNode, TNodeHashFunction>& visited);
  83
  84   /** Helper function for getInv.
  85    *
  86    * This expects a condition cond where:
  87    *   (exists x. cond)
  88    * is a BV tautology where x is getSolveVariable( tn ).
  89    *
  90    * It returns a term of the form:
  91    *   (choice y. cond { x -> y })
  92    * where y is a bound variable and x is getSolveVariable( tn ).
  93    *
  94    * In some cases, we may return a term t if cond implies an equality on
  95    * the solve variable. For example, if cond is x = t where x is
  96    * getSolveVariable(tn), then we return t instead of introducing the choice
  97    * function.
  98    */
  99   Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m);
 100 };
 101
 102 }  // namespace quantifiers
 103 }  // namespace theory
 104 }  // namespace CVC4
 105
 106 #endif /* __CVC4__BV_INVERTER_H */