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.
{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},
* 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,
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"
+
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)) {
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;
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:
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";
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())
{
# 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 \
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"
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 */
std::string identify() const override { return std::string("TheoryArrays"); }
+ Node expandDefinition(Node node) override;
+
/////////////////////////////////////////////////////////////////////////////
// PREPROCESSING
/////////////////////////////////////////////////////////////////////////////
}
};/* 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 */
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
--- /dev/null
+(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)
--- /dev/null
+(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)
--- /dev/null
+(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)
+
projects / cvc5.git / commitdiff