From 0539b0342b46e9fb96467a23f703bf2317692bb2 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 23 Jun 2020 09:55:01 -0700 Subject: [PATCH] Add support for eqrange predicate (#4562) This commit adds support for an eqrange predicate. (eqrange a b i j) is true if arrays a and b are equal on all indices within indices i and j, i.e., \forall k . i <= k <= j --> a[k] = b[k]. Requires option --arrays-exp to be enabled. --- src/api/cvc4cpp.cpp | 1 + src/api/cvc4cppkind.h | 17 ++++++ src/options/arrays_options.toml | 9 ++++ src/parser/smt2/smt2.cpp | 6 +++ src/printer/smt2/smt2_printer.cpp | 5 +- src/smt/set_defaults.cpp | 16 ++++++ src/theory/arrays/kinds | 4 ++ src/theory/arrays/theory_arrays.cpp | 55 ++++++++++++++++++++ src/theory/arrays/theory_arrays.h | 2 + src/theory/arrays/theory_arrays_type_rules.h | 51 ++++++++++++++++++ test/regress/CMakeLists.txt | 3 ++ test/regress/regress0/eqrange1.smt2 | 15 ++++++ test/regress/regress0/eqrange2.smt2 | 12 +++++ test/regress/regress0/eqrange3.smt2 | 16 ++++++ 14 files changed, 210 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/eqrange1.smt2 create mode 100644 test/regress/regress0/eqrange2.smt2 create mode 100644 test/regress/regress0/eqrange3.smt2 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 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& 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& 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) + -- 2.30.2