Changing bv_to_int options (#4721)

This PR changes --solve-bv-as-int from a numerical option (specifying the granularity) to an enum (specifying the approach). Currently we support only two modes: OFF and SUM. Future PRs will add more modes.
The numerical value of the granularity is now captured by the new option --bvand-integer-granularity.
Tests are updated accordingly.

10 files changed, 18 insertions, 18 deletions

diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2
index 1df9ec2d6..d9190128e 100644
--- a/test/regress/regress0/bv/bv_to_int1.smt2
+++ b/test/regress/regress0/bv/bv_to_int1.smt2
@@ -1,7 +1,7 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
-; COMMAND-LINE: --solve-bv-as-int=2 --no-check-models  --no-check-unsat-cores --no-check-proofs
-; COMMAND-LINE: --solve-bv-as-int=3 --no-check-models  --no-check-unsat-cores --no-check-proofs
-; COMMAND-LINE: --solve-bv-as-int=4 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-models  --no-check-unsat-cores --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun x () (_ BitVec 4))
diff --git a/test/regress/regress0/bv/bv_to_int2.smt2 b/test/regress/regress0/bv/bv_to_int2.smt2
index ab1bf10f3..00fd51baf 100644
--- a/test/regress/regress0/bv/bv_to_int2.smt2
+++ b/test/regress/regress0/bv/bv_to_int2.smt2
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=5 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-models  --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))
diff --git a/test/regress/regress0/bv/bv_to_int_bitwise.smt2 b/test/regress/regress0/bv/bv_to_int_bitwise.smt2
index 52eb78830..4bcbac20c 100644
--- a/test/regress/regress0/bv/bv_to_int_bitwise.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bitwise.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
-; COMMAND-LINE: --solve-bv-as-int=5 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-models  --no-check-unsat-cores --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun s () (_ BitVec 4))
diff --git a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2
index d0d699b4d..ec4206812 100644
--- a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=4 --no-check-models  --no-check-unsat-cores
-; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=8 --no-check-models  --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))
diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
index 541229813..05cd312d7 100644
--- a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun T4_180 () (_ BitVec 32))
diff --git a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 b/test/regress/regress0/bv/bv_to_int_elim_err.smt2
index 16731b01e..b17aeeacf 100644
--- a/test/regress/regress0/bv/bv_to_int_elim_err.smt2
+++ b/test/regress/regress0/bv/bv_to_int_elim_err.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models 
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models 
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun _substvar_183_ () (_ BitVec 32))
diff --git a/test/regress/regress0/bv/bv_to_int_zext.smt2 b/test/regress/regress0/bv/bv_to_int_zext.smt2
index 3525cebb6..5c6be19b5 100644
--- a/test/regress/regress0/bv/bv_to_int_zext.smt2
+++ b/test/regress/regress0/bv/bv_to_int_zext.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun T1_31078 () (_ BitVec 8))
diff --git a/test/regress/regress0/bv/bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bvuf_to_intuf.smt2
index 7176f4012..c621aa112 100644
--- a/test/regress/regress0/bv/bvuf_to_intuf.smt2
+++ b/test/regress/regress0/bv/bvuf_to_intuf.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_UFBV)
 (declare-fun a () (_ BitVec 4))
diff --git a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 b/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2
index 297bb2422..3db8e87ee 100644
--- a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2
+++ b/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2
@@ -1,4 +1,4 @@
-;COMMAND-LINE: --solve-bv-as-int=1 --no-produce-models --no-produce-unsat-cores --no-check-proofs
+;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-models --no-produce-unsat-cores --no-check-proofs
 ;EXPECT: unsat
 
 (set-logic QF_UFBV)
diff --git a/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2
index 873acd6c4..8fbe96eab 100644
--- a/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2
+++ b/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_UFBV)
 (declare-sort S 0)