Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/bv_inverter.h	Lines:	6	6	100.0 %
Date:	2021-05-22	Branches:	4	8	50.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * Inverse rules for bit-vector operators.
 */

#include "cvc5_private.h"

#ifndef CVC5__BV_INVERTER_H
#define CVC5__BV_INVERTER_H

#include <map>
#include <unordered_map>
#include <unordered_set>
#include <vector>

#include "expr/node.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

/** BvInverterQuery
 *
 * This is a virtual class for queries
 * required by the BvInverter class.
 */
class BvInverterQuery
{
 public:
  BvInverterQuery() {}
  virtual ~BvInverterQuery() {}
  /** returns the current model value of n */
  virtual Node getModelValue(Node n) = 0;
  /** returns a bound variable of type tn */
  virtual Node getBoundVariable(TypeNode tn) = 0;
};

// inverter class
// TODO : move to theory/bv/ if generally useful?
class BvInverter
{
 public:
  BvInverter() {}
  ~BvInverter() {}
  /** get dummy fresh variable of type tn, used as argument for sv */
  Node getSolveVariable(TypeNode tn);

  /**
   * Get path to pv in lit, replace that occurrence by sv and all others by
   * pvs (if pvs is non-null). If return value R is non-null, then :
   *   lit.path = pv R.path = sv
   *   R.path' = pvs for all lit.path' = pv, where path' != path
   *
   * If the flag projectNl is false, we return the null node if the
   * literal lit is non-linear with respect to pv.
   */
  Node getPathToPv(Node lit,
                   Node pv,
                   Node sv,
                   Node pvs,
                   std::vector<unsigned>& path,
                   bool projectNl);

  /**
   * Same as above, but does not linearize lit for pv.
   * Use this version if we know lit is linear wrt pv.
   */
  Node getPathToPv(Node lit, Node pv, std::vector<unsigned>& path)
  {
    return getPathToPv(lit, pv, pv, Node::null(), path, false);
  }

  /** solveBvLit
   *
   * Solve for sv in lit, where lit.path = sv. If this function returns a
   * non-null node t, then sv = t is the solved form of lit.
   *
   * If the BvInverterQuery provided to this function call is null, then
   * the solution returned by this call will not contain WITNESS expressions.
   * If the solved form for lit requires introducing a WITNESS expression,
   * then this call will return null.
   */
  Node solveBvLit(Node sv,
                  Node lit,
                  std::vector<unsigned>& path,
                  BvInverterQuery* m);

 private:
  /** Dummy variables for each type */
  std::map<TypeNode, Node> d_solve_var;

  /** Helper function for getPathToPv */
  Node getPathToPv(Node lit,
                   Node pv,
                   Node sv,
                   std::vector<unsigned>& path,
                   std::unordered_set<TNode>& visited);

  /** Helper function for getInv.
   *
   * This expects a condition cond where:
   *   (exists x. cond)
   * is a BV tautology where x is getSolveVariable( tn ).
   *
   * It returns a term of the form:
   *   (witness y. cond { x -> y })
   * where y is a bound variable and x is getSolveVariable( tn ).
   *
   * In some cases, we may return a term t if cond implies an equality on
   * the solve variable. For example, if cond is x = t where x is
   * getSolveVariable(tn), then we return t instead of introducing the choice
   * function.
   *
   * This function will return the null node if the BvInverterQuery m provided
   * to this call is null.
   */
  Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m);
};

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__BV_INVERTER_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Mathias Preiner, Aina Niemetz
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 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.
11		* ****************************************************************************
12		*
13		* Inverse rules for bit-vector operators.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__BV_INVERTER_H
19		#define CVC5__BV_INVERTER_H
20
21		#include <map>
22		#include <unordered_map>
23		#include <unordered_set>
24		#include <vector>
25
26		#include "expr/node.h"
27
28		namespace cvc5 {
29		namespace theory {
30		namespace quantifiers {
31
32		/** BvInverterQuery
33		*
34		* This is a virtual class for queries
35		* required by the BvInverter class.
36		*/
37		class BvInverterQuery
38		{
39		public:
40	2912	BvInverterQuery() {}
41	2912	virtual ~BvInverterQuery() {}
42		/** returns the current model value of n */
43		virtual Node getModelValue(Node n) = 0;
44		/** returns a bound variable of type tn */
45		virtual Node getBoundVariable(TypeNode tn) = 0;
46		};
47
48		// inverter class
49		// TODO : move to theory/bv/ if generally useful?
50		class BvInverter
51		{
52		public:
53	5560	BvInverter() {}
54	5560	~BvInverter() {}
55		/** get dummy fresh variable of type tn, used as argument for sv */
56		Node getSolveVariable(TypeNode tn);
57
58		/**
59		* Get path to pv in lit, replace that occurrence by sv and all others by
60		* pvs (if pvs is non-null). If return value R is non-null, then :
61		* lit.path = pv R.path = sv
62		* R.path' = pvs for all lit.path' = pv, where path' != path
63		*
64		* If the flag projectNl is false, we return the null node if the
65		* literal lit is non-linear with respect to pv.
66		*/
67		Node getPathToPv(Node lit,
68		Node pv,
69		Node sv,
70		Node pvs,
71		std::vector<unsigned>& path,
72		bool projectNl);
73
74		/**
75		* Same as above, but does not linearize lit for pv.
76		* Use this version if we know lit is linear wrt pv.
77		*/
78	905	Node getPathToPv(Node lit, Node pv, std::vector<unsigned>& path)
79		{
80	905	return getPathToPv(lit, pv, pv, Node::null(), path, false);
81		}
82
83		/** solveBvLit
84		*
85		* Solve for sv in lit, where lit.path = sv. If this function returns a
86		* non-null node t, then sv = t is the solved form of lit.
87		*
88		* If the BvInverterQuery provided to this function call is null, then
89		* the solution returned by this call will not contain WITNESS expressions.
90		* If the solved form for lit requires introducing a WITNESS expression,
91		* then this call will return null.
92		*/
93		Node solveBvLit(Node sv,
94		Node lit,
95		std::vector<unsigned>& path,
96		BvInverterQuery* m);
97
98		private:
99		/** Dummy variables for each type */
100		std::map<TypeNode, Node> d_solve_var;
101
102		/** Helper function for getPathToPv */
103		Node getPathToPv(Node lit,
104		Node pv,
105		Node sv,
106		std::vector<unsigned>& path,
107		std::unordered_set<TNode>& visited);
108
109		/** Helper function for getInv.
110		*
111		* This expects a condition cond where:
112		* (exists x. cond)
113		* is a BV tautology where x is getSolveVariable( tn ).
114		*
115		* It returns a term of the form:
116		* (witness y. cond { x -> y })
117		* where y is a bound variable and x is getSolveVariable( tn ).
118		*
119		* In some cases, we may return a term t if cond implies an equality on
120		* the solve variable. For example, if cond is x = t where x is
121		* getSolveVariable(tn), then we return t instead of introducing the choice
122		* function.
123		*
124		* This function will return the null node if the BvInverterQuery m provided
125		* to this call is null.
126		*/
127		Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m);
128		};
129
130		} // namespace quantifiers
131		} // namespace theory
132		} // namespace cvc5
133
134		#endif /* CVC5__BV_INVERTER_H */