Update copyright headers.

[cvc5.git] / src / theory / quantifiers / bv_inverter.h

diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h
index 10ef6ab4ce231371b24c60a0167f3c277d13e60b..dbd04aad193b87a46e382934ab87d37433b8b7fa 100644 (file)
--- a/src/theory/quantifiers/bv_inverter.h
+++ b/src/theory/quantifiers/bv_inverter.h
@@ -2,9 +2,9 @@
 /*! \file bv_inverter.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Mathias Preiner, Andrew Reynolds, Aina Niemetz
+ **   Andrew Reynolds, Mathias Preiner, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__BV_INVERTER_H
-#define __CVC4__BV_INVERTER_H
+#ifndef CVC4__BV_INVERTER_H
+#define CVC4__BV_INVERTER_H
 
 #include <map>
 #include <unordered_map>
@@ -37,7 +37,7 @@ class BvInverterQuery
 {
  public:
   BvInverterQuery() {}
-  ~BvInverterQuery() {}
+  virtual ~BvInverterQuery() {}
   /** returns the current model value of n */
   virtual Node getModelValue(Node n) = 0;
   /** returns a bound variable of type tn */
@@ -59,9 +59,16 @@ class BvInverter
    * 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);
+  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.
@@ -69,7 +76,7 @@ class BvInverter
    */
   Node getPathToPv(Node lit, Node pv, std::vector<unsigned>& path)
   {
-    return getPathToPv(lit, pv, pv, Node::null(), path);
+    return getPathToPv(lit, pv, pv, Node::null(), path, false);
   }
 
   /** solveBvLit
@@ -78,8 +85,8 @@ class BvInverter
    * 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 CHOICE expressions.
-   * If the solved form for lit requires introducing a CHOICE expression,
+   * 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,
@@ -105,7 +112,7 @@ class BvInverter
    * is a BV tautology where x is getSolveVariable( tn ).
    *
    * It returns a term of the form:
-   *   (choice y. cond { x -> y })
+   *   (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
@@ -123,4 +130,4 @@ class BvInverter
 }  // namespace theory
 }  // namespace CVC4
 
-#endif /* __CVC4__BV_INVERTER_H */
+#endif /* CVC4__BV_INVERTER_H */