diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2020-10-14 12:40:13 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-14 14:40:13 -0500 |
commit | 42dd10f9936c6a9be158842f482cc7ebd4a972ed (patch) | |
tree | f55e21c2367039abd214e3880644fa769548ed84 /src/theory/arith/nl | |
parent | 155e35ec2b38771917312d35f784a2e35b4b41d3 (diff) |
bv2int: implementing the iand-sum mode (#5265)
There are 3 potential modes to lazily treat the iand operator:
(1) by value (typical CEGAR loop)
(2) by sum (lazily expanding each iand node into a sum of ITEs)
(3) by bit-wise equalities (lazily expanding each iand node into bit-wise equalities)
This PR implements (2).
The relevant option is added to existing tests, and a new test is added. In a few other tests, some options are removed to make them run faster.
Diffstat (limited to 'src/theory/arith/nl')
-rw-r--r-- | src/theory/arith/nl/iand_solver.cpp | 17 | ||||
-rw-r--r-- | src/theory/arith/nl/iand_solver.h | 9 | ||||
-rw-r--r-- | src/theory/arith/nl/iand_table.cpp | 5 |
3 files changed, 29 insertions, 2 deletions
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index 954f921ce..30441a8f4 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -148,7 +148,10 @@ void IAndSolver::checkFullRefine() // ************* additional lemma schemas go here if (options::iandMode() == options::IandMode::SUM) { - // add lemmas based on sum mode + Node lem = sumBasedLemma(i); // add lemmas based on sum mode + Trace("iand-lemma") + << "IAndSolver::Lemma: " << lem << " ; SUM_REFINE" << std::endl; + d_im.addPendingArithLemma(lem, InferenceId::NL_IAND_SUM_REFINE, true); } else if (options::iandMode() == options::IandMode::BITWISE) { @@ -245,6 +248,18 @@ Node IAndSolver::valueBasedLemma(Node i) return lem; } +Node IAndSolver::sumBasedLemma(Node i) +{ + Assert(i.getKind() == IAND); + Node x = i[0]; + Node y = i[1]; + size_t bvsize = i.getOperator().getConst<IntAnd>().d_size; + uint64_t granularity = options::BVAndIntegerGranularity(); + NodeManager* nm = NodeManager::currentNM(); + Node lem = nm->mkNode( + EQUAL, i, d_iandTable.createBitwiseNode(x, y, bvsize, granularity)); + return lem; +} } // namespace nl } // namespace arith diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h index d74365784..e00cb92a9 100644 --- a/src/theory/arith/nl/iand_solver.h +++ b/src/theory/arith/nl/iand_solver.h @@ -22,6 +22,7 @@ #include "expr/node.h" #include "theory/arith/arith_state.h" #include "theory/arith/inference_manager.h" +#include "theory/arith/nl/iand_table.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" @@ -88,6 +89,7 @@ class IAndSolver Node d_two; Node d_true; Node d_false; + IAndTable d_iandTable; /** IAND terms that have been given initial refinement lemmas */ NodeSet d_initRefine; /** all IAND terms, for each bit-width */ @@ -118,6 +120,13 @@ class IAndSolver * ((_ iand k) x y) = Rewriter::rewrite(((_ iand k) M(x) M(y))) */ Node valueBasedLemma(Node i); + /** + * Sum-based refinement lemma for i of the form ((_ iand k) x y). Returns: + * i = 2^0*min(x[0],y[0])+...2^{k-1}*min(x[k-1],y[k-1]) + * where x[i] is x div i mod 2 + * and min is defined with an ite. + */ + Node sumBasedLemma(Node i); }; /* class IAndSolver */ } // namespace nl diff --git a/src/theory/arith/nl/iand_table.cpp b/src/theory/arith/nl/iand_table.cpp index 12e06ed58..050e6baed 100644 --- a/src/theory/arith/nl/iand_table.cpp +++ b/src/theory/arith/nl/iand_table.cpp @@ -198,7 +198,7 @@ void IAndTable::addDefaultValue( } // compute the most common result - uint64_t most_common_result; + uint64_t most_common_result = 0; uint64_t max_num_of_occ = 0; for (uint64_t i = 0; i <= num_of_values; i++) { @@ -208,6 +208,9 @@ void IAndTable::addDefaultValue( most_common_result = i; } } + // sanity check: some value appears at least once. + Assert(max_num_of_occ != 0); + // -1 is the default case of the table. // add it to the table table[std::make_pair(-1, -1)] = most_common_result; |