Fixed side conditions for CBQI BV, added unit tests. (#1434)

This fixes the side conditions for BITVECTOR_UREM_TOTAL, BITVECTOR_UDIV_TOTAL, 
BITVECTOR_LSHR, BITVECTOR_ASHR, BITVECTOR_SHL.

It refactors side condition generation for better readability and unit testing.
It further adds unit tests for all side conditions we generate in order to check if they too weak
or to restrictive (which may result in unsound behavior).

This is achieved by checking the following two implications:
not (exists x. s * x = t => SC) ... if sat, SC is too restrictive
not (SC => exists x. s * x = t) ... if sat SC is too weak

This simplifies to checking not (SC <=> exists x. s * x = t).

1 files changed, 6 insertions, 12 deletions

diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h
index 56f8d492b..a44d64904 100644
--- a/src/theory/quantifiers/bv_inverter.h
+++ b/src/theory/quantifiers/bv_inverter.h
@@ -50,9 +50,6 @@ class BvInverterStatus {
   BvInverterStatus() : d_status(0) {}
   ~BvInverterStatus() {}
   int d_status;
-  // TODO : may not need this (conditions now appear explicitly in solved
-  // forms) side conditions
-  std::vector<Node> d_conds;
 };
 
 // inverter class
@@ -89,15 +86,15 @@ class BvInverter {
   Node getPathToPv(Node lit, Node pv, Node sv, Node pvs,
                    std::vector<unsigned>& path);
 
-  /** solve_bv_lit
+  /** solveBvLit
    * solve for sv in lit, where lit.path = sv
    * status accumulates side conditions
    */
-  Node solve_bv_lit(Node sv,
-                    Node lit,
-                    std::vector<unsigned>& path,
-                    BvInverterQuery* m,
-                    BvInverterStatus& status);
+  Node solveBvLit(Node sv,
+                  Node lit,
+                  std::vector<unsigned>& path,
+                  BvInverterQuery* m,
+                  BvInverterStatus& status);
 
  private:
   /** dummy variables for each type */
@@ -106,9 +103,6 @@ class BvInverter {
   /** helper function for getPathToPv */
   Node getPathToPv(Node lit, Node pv, Node sv, std::vector<unsigned>& path,
                    std::unordered_set<TNode, TNodeHashFunction>& visited);
-
-  // is operator k invertible?
-  bool isInvertible(Kind k, unsigned index);
 };
 
 }  // namespace quantifiers