summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/api/cvc4cpp.cpp1
-rw-r--r--src/api/cvc4cppkind.h17
-rw-r--r--src/options/arrays_options.toml9
-rw-r--r--src/parser/smt2/smt2.cpp6
-rw-r--r--src/printer/smt2/smt2_printer.cpp5
-rw-r--r--src/smt/set_defaults.cpp16
-rw-r--r--src/theory/arrays/kinds4
-rw-r--r--src/theory/arrays/theory_arrays.cpp55
-rw-r--r--src/theory/arrays/theory_arrays.h2
-rw-r--r--src/theory/arrays/theory_arrays_type_rules.h51
-rw-r--r--test/regress/CMakeLists.txt3
-rw-r--r--test/regress/regress0/eqrange1.smt215
-rw-r--r--test/regress/regress0/eqrange2.smt212
-rw-r--r--test/regress/regress0/eqrange3.smt216
14 files changed, 210 insertions, 2 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 2fd5cb444..cebba9b5e 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -214,6 +214,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
{SELECT, CVC4::Kind::SELECT},
{STORE, CVC4::Kind::STORE},
{CONST_ARRAY, CVC4::Kind::STORE_ALL},
+ {EQ_RANGE, CVC4::Kind::EQ_RANGE},
/* Datatypes ----------------------------------------------------------- */
{APPLY_SELECTOR, CVC4::Kind::APPLY_SELECTOR},
{APPLY_CONSTRUCTOR, CVC4::Kind::APPLY_CONSTRUCTOR},
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 198f51024..cf9074129 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -1505,6 +1505,23 @@ enum CVC4_PUBLIC Kind : int32_t
* arrays, the solver doesn't know what to do and aborts (Issue #1667).
*/
CONST_ARRAY,
+ /**
+ * Equality over arrays a and b over a given range [i,j], i.e.,
+ * \forall k . i <= k <= j --> a[k] = b[k]
+ *
+ * Parameters: 4
+ * -[1]: First array
+ * -[2]: Second array
+ * -[3]: Lower bound of range (inclusive)
+ * -[4]: Uppper bound of range (inclusive)
+ * Create with:
+ * mkTerm(Op op, const std::vector<Term>& children)
+ *
+ * Note: We currently support the creation of array equalities over index
+ * types bit-vector, floating-point, integer and real. Option --arrays-exp is
+ * required to support this operator.
+ */
+ EQ_RANGE,
#if 0
/* array table function (internal-only symbol) */
ARR_TABLE_FUN,
diff --git a/src/options/arrays_options.toml b/src/options/arrays_options.toml
index 8c82a7fb5..389bb6e4c 100644
--- a/src/options/arrays_options.toml
+++ b/src/options/arrays_options.toml
@@ -73,3 +73,12 @@ header = "options/arrays_options.h"
type = "int"
default = "2"
help = "propagation effort for arrays: 0 is none, 1 is some, 2 is full"
+
+[[option]]
+ name = "arraysExp"
+ category = "experimental"
+ long = "arrays-exp"
+ type = "bool"
+ default = "false"
+ help = "enable experimental features in the theory of arrays"
+
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index bf4e489bb..a7eb218af 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -642,6 +642,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) {
addOperator(api::SELECT, "select");
addOperator(api::STORE, "store");
+ addOperator(api::EQ_RANGE, "eqrange");
}
if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
@@ -1824,6 +1825,11 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
Debug("parser") << "applyParseOp: return uminus " << ret << std::endl;
return ret;
}
+ if (kind == api::EQ_RANGE && d_solver->getOption("arrays-exp") != "true")
+ {
+ parseError(
+ "eqrange predicate requires option --arrays-exp to be enabled.");
+ }
api::Term ret = d_solver->mkTerm(kind, args);
Debug("parser") << "applyParseOp: return default builtin " << ret
<< std::endl;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index b88e53788..31aa67ff9 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -589,8 +589,7 @@ void Smt2Printer::toStream(std::ostream& out,
case kind::PARTIAL_SELECT_0:
case kind::PARTIAL_SELECT_1:
case kind::ARRAY_TYPE:
- out << smtKindString(k, d_variant) << " ";
- break;
+ case kind::EQ_RANGE: out << smtKindString(k, d_variant) << " "; break;
// string theory
case kind::STRING_CONCAT:
@@ -1070,6 +1069,8 @@ static string smtKindString(Kind k, Variant v)
case kind::ARRAY_TYPE: return "Array";
case kind::PARTIAL_SELECT_0: return "partial_select_0";
case kind::PARTIAL_SELECT_1: return "partial_select_1";
+ case kind::EQ_RANGE:
+ return "eqrange";
// bv theory
case kind::BITVECTOR_CONCAT: return "concat";
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 23ae65044..afc8eb7bb 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -272,6 +272,22 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
options::proofNew.set(false);
}
+ if (options::arraysExp())
+ {
+ if (!logic.isQuantified())
+ {
+ logic = logic.getUnlockedCopy();
+ logic.enableQuantifiers();
+ logic.lock();
+ }
+ // Allows to answer sat more often by default.
+ if (!options::fmfBound.wasSetByUser())
+ {
+ options::fmfBound.set(true);
+ Trace("smt") << "turning on fmf-bound, for arrays-exp" << std::endl;
+ }
+ }
+
// sygus inference may require datatypes
if (!smte.isInternalSubsolver())
{
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 1adbdb0b2..659f05ae8 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -31,6 +31,9 @@ operator SELECT 2 "array select; first parameter is an array term, second is the
# store a i e is a[i] <= e
operator STORE 3 "array store; first parameter is an array term, second is the store index, third is the term to store at the index"
+# eqrange a b i j \forall k. i <= k <= j -> a[k] = b[k]
+operator EQ_RANGE 4 "equality of two arrays over an index range lower/upper"
+
# storeall t e is \all i in indexType(t) <= e
constant STORE_ALL \
::CVC4::ArrayStoreAll \
@@ -53,6 +56,7 @@ typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
typerule STORE_ALL ::CVC4::theory::arrays::ArrayStoreTypeRule
typerule ARR_TABLE_FUN ::CVC4::theory::arrays::ArrayTableFunTypeRule
typerule ARRAY_LAMBDA ::CVC4::theory::arrays::ArrayLambdaTypeRule
+typerule EQ_RANGE ::CVC4::theory::arrays::ArrayEqRangeTypeRule
operator PARTIAL_SELECT_0 0:2 "partial array select, for internal use only"
operator PARTIAL_SELECT_1 0:2 "partial array select, for internal use only"
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 0f5d9ec8b..71e040ccc 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -2312,6 +2312,61 @@ std::string TheoryArrays::TheoryArraysDecisionStrategy::identify() const
return std::string("th_arrays_dec");
}
+Node TheoryArrays::expandDefinition(Node node)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Kind kind = node.getKind();
+
+ /* Expand
+ *
+ * (eqrange a b i j)
+ *
+ * to
+ *
+ * forall k . i <= k <= j => a[k] = b[k]
+ *
+ */
+ if (kind == kind::EQ_RANGE)
+ {
+ TNode a = node[0];
+ TNode b = node[1];
+ TNode i = node[2];
+ TNode j = node[3];
+ Node k = nm->mkBoundVar(i.getType());
+ Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, k);
+ TypeNode type = k.getType();
+
+ Kind kle;
+ Node range;
+ if (type.isBitVector())
+ {
+ kle = kind::BITVECTOR_ULE;
+ }
+ else if (type.isFloatingPoint())
+ {
+ kle = kind::FLOATINGPOINT_LEQ;
+ }
+ else if (type.isInteger() || type.isReal())
+ {
+ kle = kind::LEQ;
+ }
+ else
+ {
+ Unimplemented() << "Type " << type << " is not supported for predicate "
+ << kind;
+ }
+
+ range = nm->mkNode(kind::AND, nm->mkNode(kle, i, k), nm->mkNode(kle, k, j));
+
+ Node eq = nm->mkNode(kind::EQUAL,
+ nm->mkNode(kind::SELECT, a, k),
+ nm->mkNode(kind::SELECT, b, k));
+ Node implies = nm->mkNode(kind::IMPLIES, range, eq);
+ return nm->mkNode(kind::FORALL, bvl, implies);
+ }
+ return node;
+}
+
}/* CVC4::theory::arrays namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 8c94f08cd..c5cd24fd3 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -151,6 +151,8 @@ class TheoryArrays : public Theory {
std::string identify() const override { return std::string("TheoryArrays"); }
+ Node expandDefinition(Node node) override;
+
/////////////////////////////////////////////////////////////////////////////
// PREPROCESSING
/////////////////////////////////////////////////////////////////////////////
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index facc81f43..e5681d50f 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -224,6 +224,57 @@ struct ArrayPartialSelectTypeRule {
}
};/* struct ArrayPartialSelectTypeRule */
+struct ArrayEqRangeTypeRule
+{
+ inline static TypeNode computeType(NodeManager* nodeManager,
+ TNode n,
+ bool check)
+ {
+ Assert(n.getKind() == kind::EQ_RANGE);
+ if (check)
+ {
+ TypeNode n0_type = n[0].getType(check);
+ TypeNode n1_type = n[1].getType(check);
+ if (!n0_type.isArray())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "first operand of eqrange is not an array");
+ }
+ if (!n1_type.isArray())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "second operand of eqrange is not an array");
+ }
+ if (n0_type != n1_type)
+ {
+ throw TypeCheckingExceptionPrivate(n, "array types do not match");
+ }
+ TypeNode indexType = n0_type.getArrayIndexType();
+ TypeNode indexRangeType1 = n[2].getType(check);
+ TypeNode indexRangeType2 = n[3].getType(check);
+ if (!indexRangeType1.isSubtypeOf(indexType))
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "eqrange lower index type does not match array index type");
+ }
+ if (!indexRangeType2.isSubtypeOf(indexType))
+ {
+ throw TypeCheckingExceptionPrivate(
+ n, "eqrange upper index type does not match array index type");
+ }
+ if (!indexType.isBitVector() && !indexType.isFloatingPoint()
+ && !indexType.isInteger() && !indexType.isReal())
+ {
+ throw TypeCheckingExceptionPrivate(
+ n,
+ "eqrange only supports bit-vectors, floating-points, integers, and "
+ "reals as index type");
+ }
+ }
+ return nodeManager->booleanType();
+ }
+}; /* struct ArrayEqRangeTypeRule */
+
}/* CVC4::theory::arrays namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 690135b54..bb0f311d1 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -473,6 +473,9 @@ set(regress_0_tests
regress0/distinct.smtv1.smt2
regress0/dump-unsat-core-full.smt2
regress0/simple-dump-model.smt2
+ regress0/eqrange1.smt2
+ regress0/eqrange2.smt2
+ regress0/eqrange3.smt2
regress0/expect/scrub.01.smtv1.smt2
regress0/expect/scrub.03.smt2
regress0/expect/scrub.06.cvc
diff --git a/test/regress/regress0/eqrange1.smt2 b/test/regress/regress0/eqrange1.smt2
new file mode 100644
index 000000000..90eb7a22a
--- /dev/null
+++ b/test/regress/regress0/eqrange1.smt2
@@ -0,0 +1,15 @@
+(set-logic QF_AUFBV)
+(set-option :arrays-exp true)
+(set-option :quiet true) ; Suppress check-model warnings involving quantifiers
+(set-info :status sat)
+(declare-fun a1 () (Array (_ BitVec 2) (_ BitVec 2)))
+(declare-fun a2 () (Array (_ BitVec 2) (_ BitVec 2)))
+(declare-fun e1 () (_ BitVec 2))
+(declare-fun e2 () (_ BitVec 2))
+(assert (distinct e1 e2))
+(assert (= a1 (store (store (store (store a1 #b00 e1) #b01 e1) #b10 e1) #b11 e1)))
+(assert (= a2 (store (store (store (store a2 #b00 e1) #b01 e1) #b10 e2) #b11 e1)))
+(assert (eqrange a1 a2 #b00 #b01))
+(assert (eqrange a1 a2 #b11 #b11))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/eqrange2.smt2 b/test/regress/regress0/eqrange2.smt2
new file mode 100644
index 000000000..efddbc88b
--- /dev/null
+++ b/test/regress/regress0/eqrange2.smt2
@@ -0,0 +1,12 @@
+(set-logic AUFBV)
+(set-option :arrays-exp true)
+(set-info :status unsat)
+(declare-sort Element 0)
+(declare-const a (Array (_ BitVec 3) Element))
+(declare-const b (Array (_ BitVec 3) Element))
+(declare-const j (_ BitVec 3))
+(assert (eqrange a b (_ bv0 3) j))
+(assert (eqrange a b (bvadd j (_ bv1 3)) (_ bv7 3)))
+(assert (exists ((i (_ BitVec 3))) (not (= (select a i) (select b i)))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/eqrange3.smt2 b/test/regress/regress0/eqrange3.smt2
new file mode 100644
index 000000000..54e9d0386
--- /dev/null
+++ b/test/regress/regress0/eqrange3.smt2
@@ -0,0 +1,16 @@
+(set-logic QF_AUFLIA)
+(set-option :arrays-exp true)
+(set-option :quiet true) ; Suppress Warning
+(set-info :status sat)
+(declare-fun a1 () (Array Int Int))
+(declare-fun a2 () (Array Int Int))
+(declare-fun e1 () Int)
+(declare-fun e2 () Int)
+(assert (distinct e1 e2))
+(assert (= a1 (store (store (store (store a1 0 e1) 1 e1) 2 e1) 3 e1)))
+(assert (= a2 (store (store (store (store a2 1 e1) 0 e1) 2 e2) 3 e1)))
+(assert (eqrange a1 a2 (- 1) 1))
+(assert (eqrange a1 a2 3 3))
+(check-sat)
+(exit)
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback