Option to include BVAnd/BVOr ops in conjunctive/disjunctive partition (…

…#102) * Option to include BVAnd/BVOr ops in conjunctive/disjunctive partition * Add comments
stanford-centaur · Sep 6, 2020 · 822af6f · 822af6f
1 parent 8725a64
commit 822af6f
Show file tree

Hide file tree

Showing 5 changed files with 189 additions and 17 deletions.
diff --git a/include/utils.h b/include/utils.h
@@ -50,10 +50,33 @@ inline void Log(std::string msg)
   }
 }
 
+namespace smt {
+
 // term helper methods
-void conjunctive_partition(const smt::Term &term, smt::TermVec &out);
+void op_partition(smt::PrimOp o, const smt::Term & term, smt::TermVec & out);
+
+/** Populates a vector with conjuncts from a term
+ *  @param the term to partition
+ *  @param out the output vector
+ *  @param include_bvand also split on BVAnd over 1-bit signals
+ *         Note: this is mainly for use with Boolector which treats
+ *         booleans as 1-bit bit-vectors. Using this option on a term
+ *         that is known to be boolean will give you the expected
+ *         partition.
+ */
+void conjunctive_partition(const smt::Term & term,
+                           smt::TermVec & out,
+                           bool include_bvand = false);
 
-void disjunctive_partition(const smt::Term &term, smt::TermVec &out);
+/** Populates a vector with disjuncts from a term
+ *  @param the term to partition
+ *  @param out the output vector
+ *  @param include_bvor also split on BVOr over 1-bit signals
+ */
+void disjunctive_partition(const smt::Term & term,
+                           smt::TermVec & out,
+                           bool include_bvor = false);
 
 void get_free_symbolic_consts(const smt::Term &term, smt::TermVec &out);
 
+}  // namespace smt
diff --git a/src/utils.cpp b/src/utils.cpp
@@ -17,6 +17,8 @@
 #include "utils.h"
 #include "ops.h"
 
+namespace smt {
+
 void op_partition(smt::PrimOp o,
                   const smt::Term &term, smt::TermVec &out)
 {
@@ -44,14 +46,60 @@ void op_partition(smt::PrimOp o,
   }
 }
 
-void conjunctive_partition(const smt::Term &term, smt::TermVec &out)
+void conjunctive_partition(const smt::Term & term,
+                           smt::TermVec & out,
+                           bool include_bvand)
 {
-  op_partition(smt::And, term, out);
+  if (!include_bvand)
+  {
+    op_partition(smt::And, term, out);
+  }
+  else
+  {
+    TermVec tmp;
+    op_partition(smt::And, term, tmp);
+    Sort sort;
+    for (auto tt : tmp)
+    {
+      sort = tt->get_sort();
+      if (sort->get_sort_kind() == BV && sort->get_width() == 1)
+      {
+        op_partition(smt::BVAnd, tt, out);
+      }
+      else
+      {
+        out.push_back(tt);
+      }
+    }
+  }
 }
 
-void disjunctive_partition(const smt::Term &term, smt::TermVec &out)
+void disjunctive_partition(const smt::Term & term,
+                           smt::TermVec & out,
+                           bool include_bvor)
 {
-  op_partition(smt::Or, term, out);
+  if (!include_bvor)
+  {
+    op_partition(smt::Or, term, out);
+  }
+  else
+  {
+    TermVec tmp;
+    op_partition(smt::Or, term, tmp);
+    Sort sort;
+    for (auto tt : tmp)
+    {
+      sort = tt->get_sort();
+      if (sort->get_sort_kind() == BV && sort->get_width() == 1)
+      {
+        op_partition(smt::BVOr, tt, out);
+      }
+      else
+      {
+        out.push_back(tt);
+      }
+    }
+  }
 }
 
 void get_free_symbolic_consts(const smt::Term &term, smt::TermVec &out)
@@ -78,3 +126,4 @@ void get_free_symbolic_consts(const smt::Term &term, smt::TermVec &out)
   }
 }
 
+}  // namespace smt
diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
@@ -93,6 +93,11 @@ target_link_libraries(unit-op gtest_main)
 target_link_libraries(unit-op test-deps)
 add_test(NAME unit-op_test COMMAND unit-op)
 
+add_executable(unit-util "${PROJECT_SOURCE_DIR}/tests/unit/unit-util.cpp")
+target_link_libraries(unit-util gtest_main)
+target_link_libraries(unit-util test-deps)
+add_test(NAME unit-util_test COMMAND unit-util)
+
 add_executable(unit-term-hashtable "${PROJECT_SOURCE_DIR}/tests/unit/unit-term-hashtable.cpp")
 target_link_libraries(unit-term-hashtable gtest_main)
 target_link_libraries(unit-term-hashtable test-deps)

diff --git a/tests/unit/unit-sort.cpp b/tests/unit/unit-sort.cpp
@@ -1,4 +1,4 @@
-/*********************                                                        */
+/*********************                                           */
 /*! \file unit-sort.cpp
 ** \verbatim
 ** Top contributors (to current version):

diff --git a/tests/unit/unit-util.cpp b/tests/unit/unit-util.cpp
@@ -1,14 +1,109 @@
+/*********************                                           */
+/*! \file unit-util.cpp
+** \verbatim
+** Top contributors (to current version):
+**   Makai Mann
+** This file is part of the smt-switch project.
+** Copyright (c) 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 LICENSE in the top-level source
+** directory for licensing information.\endverbatim
+**
+** \brief Unit tests for util functions
+**
+**
+**/
+
+#include <utility>
+#include <vector>
+
 #include "utils.h"
 
-int main()
+#include "available_solvers.h"
+#include "gtest/gtest.h"
+#include "smt.h"
+
+using namespace smt;
+using namespace std;
+
+namespace smt_tests {
+
+class UnitUtilTests : public ::testing::Test,
+                      public ::testing::WithParamInterface<SolverEnum>
+{
+ protected:
+  void SetUp() override
+  {
+    s = create_solver(GetParam());
+
+    boolsort = s->make_sort(BOOL);
+    for (size_t i = 0; i < 30; ++i)
+    {
+      symbols.push_back(s->make_symbol("x" + std::to_string(i), boolsort));
+    }
+  }
+  SmtSolver s;
+  Sort boolsort;
+  TermVec symbols;
+};
+
+TEST_P(UnitUtilTests, ConjunctivePartition)
+{
+  Term conjunction = symbols[0];
+  for (size_t j = 1; j < symbols.size(); ++j)
+  {
+    conjunction = s->make_term(And, conjunction, symbols[j]);
+  }
+
+  TermVec conjuncts;
+  // boolean argument means to include BVAnd
+  // if over 1-bit variables
+  // then this will work for Boolector even without logging
+  conjunctive_partition(conjunction, conjuncts, true);
+  ASSERT_EQ(symbols.size(), conjuncts.size());
+
+  // order not necessarily maintained
+  UnorderedTermSet conjuncts_set(conjuncts.begin(), conjuncts.end());
+
+  for (size_t j = 0; j < symbols.size(); ++j)
+  {
+    ASSERT_TRUE(conjuncts_set.find(symbols[j]) != conjuncts_set.end());
+  }
+}
+
+TEST_P(UnitUtilTests, DisjunctivePartition)
 {
-  Log<0>("message!");
-  Log<1>("no message!");
-#ifdef _DEBUG
-  Assert(true);
-#else
-  // should compile to nothing
-  Assert(false);
-#endif
-  return 0;
+  if (s->get_solver_enum() == BTOR)
+  {
+    // Boolector rewrites Ors as Not And
+    // it's equivalent, but disjunctive partition won't work
+    return;
+  }
+
+  Term disjunction = symbols[0];
+  for (size_t j = 1; j < symbols.size(); ++j)
+  {
+    disjunction = s->make_term(Or, disjunction, symbols[j]);
+  }
+
+  TermVec disjuncts;
+  // boolean argument means to include BVOr
+  // if over 1-bit variables
+  // then this will work for Boolector even without logging
+  disjunctive_partition(disjunction, disjuncts, true);
+  ASSERT_EQ(symbols.size(), disjuncts.size());
+
+  // order not necessarily maintained
+  UnorderedTermSet disjuncts_set(disjuncts.begin(), disjuncts.end());
+
+  for (size_t j = 0; j < symbols.size(); ++j)
+  {
+    ASSERT_TRUE(disjuncts_set.find(symbols[j]) != disjuncts_set.end());
+  }
 }
+
+INSTANTIATE_TEST_SUITE_P(ParameterizedUnitUtilTests,
+                         UnitUtilTests,
+                         testing::ValuesIn(filter_solver_enums({ TERMITER })));
+
+}  // namespace smt_tests