Changes tuple_ to tuple. for consistency.
Also fixes the lexer list for smt2 and updates the datatypes theory reference with missing content.
'=>', '=', 'true', 'false', 'not', 'and', 'or', 'xor', 'distinct',
'ite',
# datatypes
- 'tuple', 'tuple_project', 'tuple_select',
+ 'tuple', 'tuple\.project', 'tuple\.select', 'tuple\.update',
# fp
'RNE', 'RNA', 'RTP', 'RTN', 'RTZ', 'fp', 'NaN', 'fp\.abs', 'fp\.neg',
'fp\.add', 'fp\.sub', 'fp\.mul', 'fp\.div', 'fp\.fma', 'fp\.sqrt',
'<', '>', '<=', '>=', '!=', '\+', '-', '\*', '/', 'div', 'mod', 'abs',
'divisible', 'to_real', 'to_int', 'is_int', 'iand', 'int2bv',
# separation logic
- 'emp', 'pto', 'sep', 'wand', 'nil',
+ 'sep\.emp', 'pto', 'sep', 'wand', 'sep\.nil',
# sets / relations
- 'union', 'setminus', 'member', 'subset', 'emptyset', 'singleton',
- 'card', 'insert', 'complement', 'univset', 'transpose', 'tclosure',
- 'join', 'product', 'intersection',
+ 'set\.union', 'set\.minus', 'set\.member', 'set\.subset', 'set\.empty',
+ 'set\.singleton', 'set\.card', 'set\.insert', 'set\.complement',
+ 'set\.universe', 'rel\.transpose', 'rel\.tclosure', 'rel\.join',
+ 'rel\.product', 'set\.inter',
# string
- 'char', 'str\.\+\+', 'str\.len', 'str\.<', 'str\.to_re', 'str\.in_re',
- 're\.none', 're\.all', 're\.allchar', 're\.\+\+', 're\.union',
- 're\.inter', 're\.*', 'str\.<=', 'str\.at', 'str\.substr',
+ 'char', 'str\.\+\+', 'str\.len', 'str\.<', 'str\.<=', 'str\.to_re',
+ 'str\.in_re', 're\.none', 're\.all', 're\.allchar', 're\.\+\+',
+ 're\.union', 're\.inter', 're\.*', 'str\.<=', 'str\.at', 'str\.substr',
'str\.prefixof', 'str\.suffixof', 'str\.contains', 'str\.indexof',
'str\.replace', 'str\.replace_all', 'str\.replace_re',
'str\.replace_re_all', 're\.comp', 're\.diff', 're\.\+', 're\.opt',
.. code:: smtlib
(declare-datatypes ((D1 n1) ... (Dk nk))
- (((C1 (S1 T1) ... (Si Ti)) ... (Cj ... ))
+ (((C1 (S11 T1) ... (S1i Ti)) ... (Cj ... ))
...
((...) ... (...)))
where ``D1 ... Dk`` are datatype types, ``C1 ... Cj`` are the constructors for
datatype ``D1``,
-``S1 ... Si`` are the selectors (or "destructors") of constructor ``C1``, and
+``S11 ... S1i`` are the selectors (or "destructors") of constructor ``C1``, and
each ``T1 ... Ti`` is a previously declared type or one of ``D1 ... Dk``.
The numbers ``n1 ... nk`` denote the number of type
parameters for the datatype, where ``0`` is used for non-parametric datatypes.
.. code:: smtlib
(declare-const t (Tuple Int Int))
- (assert (= ((_ tuple_select 0) t) 3))
+ (assert (= ((_ tuple.select 0) t) 3))
(assert (not (= t (tuple 3 4))))
+--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
| Logic String | ``(set-logic QF_DT)`` | ``solver.setLogic("QF_DT");`` |
+--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
+| Datatype Sort | ``(declare-datatype ...)`` | ``Sort s = solver.mkDatatypeSort(...);`` |
++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
+| Datatype Sorts | ``(declare-datatypes ...)`` | ``std::vector<Sort> s = solver.mkDatatypeSorts(...);`` |
++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
+| Constructor | ``(Ci <Term_1>, ..., <Term_n>)`` | ``Sort s = solver.mkDatatypeSort(...);`` |
+| | | |
+| | | ``Datatype dt = s.getDatatype();`` |
+| | | |
+| | | ``Term ci = dt[i].getConstructorTerm();`` |
+| | | |
+| | | ``Term r = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {ci, <Term_1>, ..., <Term_n>});`` |
++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
+| Selector | ``(Sij t)`` | ``Sort s = solver.mkDatatypeSort(...);`` |
+| | | |
+| | | ``Datatype dt = s.getDatatype();`` |
+| | | |
+| | | ``Term sij = dt[i].getSelector(j).getSelectorTerm();`` |
+| | | |
+| | | ``Term r = solver.mkTerm(Kind::APPLY_SELECTOR, {sij, t});`` |
++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
+| Updater | ``((_ update Sij) t u)`` | ``Sort s = solver.mkDatatypeSort(...);`` |
+| | | |
+| | | ``Datatype dt = s.getDatatype();`` |
+| | | |
+| | | ``Term upd = dt[i].getSelector(j).getUpdaterTerm();`` |
+| | | |
+| | | ``Term r = solver.mkTerm(Kind::APPLY_UPDATER, {upd, t, u});`` |
++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
+| Tester | ``((_ is Ci) t)`` | ``Sort s = solver.mkDatatypeSort(...);`` |
+| | | |
+| | | ``Datatype dt = s.getDatatype();`` |
+| | | |
+| | | ``Term upd = dt[i].getTesterTerm();`` |
+| | | |
+| | | ``Term r = solver.mkTerm(Kind::APPLY_TESTER, {upd, t, u});`` |
++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
| Tuple Sort | ``(Tuple <Sort_1>, ..., <Sort_n>)`` | ``std::vector<cvc5::api::Sort> sorts = { ... };`` |
| | | |
| | | ``Sort s = solver.mkTupleSort(sorts);`` |
| | | |
| | | ``Datatype dt = s.getDatatype();`` |
| | | |
-| | | ``Term c = dt[0].getConstructor();`` |
+| | | ``Term c = dt[0].getConstructorTerm();`` |
+| | | |
+| | | ``Term r = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, <Term_1>, ..., <Term_n>});`` |
++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
+| Tuple Selector | ``((_ tuple.select i) t)`` | ``Sort s = solver.mkTupleSort(sorts);`` |
+| | | |
+| | | ``Datatype dt = s.getDatatype();`` |
+| | | |
+| | | ``Term sel = dt[0].getSelector(i).getSelectorTerm();`` |
+| | | |
+| | | ``Term r = solver.mkTerm(Kind::APPLY_SELECTOR, {sel, t});`` |
++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
+| Tuple Updater | ``((_ tuple.update i) t u)`` | ``Sort s = solver.mkTupleSort(sorts);`` |
+| | | |
+| | | ``Datatype dt = s.getDatatype();`` |
+| | | |
+| | | ``Term upd = dt[0].getSelector(i).getUpdaterTerm();`` |
| | | |
-| | | ``Term t = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, <Term_1>, ..., <Term_n>});`` |
+| | | ``Term r = solver.mkTerm(Kind::APPLY_UPDATER, {upd, t, u});`` |
+--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
-| Tuple Selector | ``((_ tuple_select i) t)`` | ``Sort s = solver.mkTupleSort(sorts);`` |
+| Tuple Projection | ``((_ tuple.project i1 ... in) t)`` | ``Sort s = solver.mkTupleSort(sorts);`` |
| | | |
| | | ``Datatype dt = s.getDatatype();`` |
| | | |
-| | | ``Term c = dt[0].getSelector(i);`` |
+| | | ``Term proj = solver.mkOp(Kind::TUPLE_PROJECT, {i1, ..., in});`` |
| | | |
-| | | ``Term s = solver.mkTerm(Kind::APPLY_SELECTOR, {s, t});`` |
+| | | ``Term r = solver.mkTerm(Kind::TUPLE_PROJECT, {proj, t});`` |
+--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
| Record Sort | n/a | ``Sort s = mkRecordSort(const std::vector<std::pair<std::string, Sort>>& fields);`` |
+--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
| | | |
| | | ``Datatype dt = s.getDatatype();`` |
| | | |
-| | | ``Term c = dt[0].getConstructor();`` |
+| | | ``Term c = dt[0].getConstructorTerm();`` |
| | | |
-| | | ``Term t = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, <Term_1>, ..., <Term_n>});`` |
+| | | ``Term r = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, <Term_1>, ..., <Term_n>});`` |
+--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
| Record Selector | n/a | ``Sort s = mkRecordSort(fields);`` |
| | | |
| | | ``Datatype dt = s.getDatatype();`` |
| | | |
-| | | ``Term c = dt[0].getSelector(name);`` |
+| | | ``Term sel = dt[0].getSelector(name).getSelectorTerm();`` |
+| | | |
+| | | ``Term r = solver.mkTerm(Kind::APPLY_SELECTOR, {sel, t});`` |
++--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
+| Record Updater | n/a | ``Sort s = solver.mkRecordSort(sorts);`` |
+| | | |
+| | | ``Datatype dt = s.getDatatype();`` |
+| | | |
+| | | ``Term upd = dt[0].getSelector(name).getUpdaterTerm();`` |
| | | |
-| | | ``Term s = solver.mkTerm(Kind::APPLY_SELECTOR, {s, t});`` |
+| | | ``Term r = solver.mkTerm(Kind::APPLY_UPDATER, {upd, t, u});`` |
+--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
* \rst
* .. code:: smtlib
*
- * ((_ tuple_project 1 2 2 3 1) (tuple 10 20 30 40))
+ * ((_ tuple.project 1 2 2 3 1) (tuple 10 20 30 40))
* \endrst
* yields
* \rst
}
| TUPLE_PROJECT_TOK nonemptyNumeralList[numerals]
{
- // we adopt a special syntax (_ tuple_project i_1 ... i_n) where
+ // we adopt a special syntax (_ tuple.project i_1 ... i_n) where
// i_1, ..., i_n are numerals
p.d_kind = cvc5::TUPLE_PROJECT;
p.d_op = SOLVER->mkOp(cvc5::TUPLE_PROJECT, numerals);
CHAR_TOK : { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_STRINGS) }? 'char';
TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_DATATYPES) }? 'tuple';
-TUPLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_DATATYPES) }? 'tuple_project';
+TUPLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(internal::theory::THEORY_DATATYPES) }? 'tuple.project';
FMF_CARD_TOK: { !PARSER_STATE->strictModeEnabled() && PARSER_STATE->hasCardinalityConstraints() }? 'fmf.card';
HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->';
// Notice that tuple operators, we use the generic APPLY_SELECTOR and
// APPLY_UPDATER kinds. These are processed based on the context
// in which they are parsed, e.g. when parsing identifiers.
- addIndexedOperator(cvc5::APPLY_SELECTOR, "tuple_select");
- addIndexedOperator(cvc5::APPLY_UPDATER, "tuple_update");
+ addIndexedOperator(cvc5::APPLY_SELECTOR, "tuple.select");
+ addIndexedOperator(cvc5::APPLY_UPDATER, "tuple.update");
}
}
}
else if (p.d_kind != cvc5::NULL_TERM)
{
- // It is a special case, e.g. tuple_select or array constant specification.
+ // It is a special case, e.g. tuple.select or array constant specification.
// We have to wait until the arguments are parsed to resolve it.
}
else if (!p.d_expr.isNull())
TupleProjectOp op = n.getOperator().getConst<TupleProjectOp>();
if (op.getIndices().empty())
{
- // e.g. (tuple_project tuple)
- out << "tuple_project " << n[0] << ")";
+ // e.g. (tuple.project tuple)
+ out << "tuple.project " << n[0] << ")";
}
else
{
- // e.g. ((_ tuple_project 2 4 4) tuple)
- out << "(_ tuple_project" << op << ") " << n[0] << ")";
+ // e.g. ((_ tuple.project 2 4 4) tuple)
+ out << "(_ tuple.project" << op << ") " << n[0] << ")";
}
return;
}
if (dt.isTuple())
{
stillNeedToPrintParams = false;
- out << "(_ tuple_select " << DType::indexOf(op) << ") ";
+ out << "(_ tuple.select " << DType::indexOf(op) << ") ";
}
}
break;
if (dt.isTuple())
{
stillNeedToPrintParams = false;
- out << "(_ tuple_update " << DType::indexOf(op) << ") ";
+ out << "(_ tuple.update " << DType::indexOf(op) << ") ";
}
else
{
(declare-fun x () (list Real))
(declare-fun y () (Tuple Int Bool Int))
(assert (= y (tuple 5 true 4)))
-(assert ((_ tuple_select 1) y))
+(assert ((_ tuple.select 1) y))
(assert (= x ((as cons (list Real)) (/ 11 10) true (as nil (list Real)))))
(check-sat)
(set-logic ALL)
(set-option :incremental false)
(declare-fun x () (Tuple Int Int))
-(assert (= ((_ tuple_select 0) x) 5))
+(assert (= ((_ tuple.select 0) x) 5))
(check-sat)
(define-fun foo ((x |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)|)) |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)| ((_ update int) x (int x)))
(declare-fun m () |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)|)
(define-fun w () (Tuple |__cvc5_record_int_(Array Int Int)_queries_(Array Int Int)| Int) (ite (= x 0) (tuple (foo m) 0) (tuple m 0)))
-(check-sat-assuming ( (not (= ((_ tuple_select 1) (ite (= x 0) (tuple (foo m) 0) (tuple m 0))) 1)) ))
+(check-sat-assuming ( (not (= ((_ tuple.select 1) (ite (= x 0) (tuple (foo m) 0) (tuple m 0))) 1)) ))
(set-logic ALL)
(set-option :incremental false)
(define-fun x () (Tuple Real Int Real) (tuple (/ 4 5) 9 (/ 11 9)))
-(define-fun first_elem () Real ((_ tuple_select 0) (tuple (/ 4 5) 9 (/ 11 9))))
-(define-fun third_elem () Real ((_ tuple_select 2) (tuple (/ 4 5) 9 (/ 11 9))))
+(define-fun first_elem () Real ((_ tuple.select 0) (tuple (/ 4 5) 9 (/ 11 9))))
+(define-fun third_elem () Real ((_ tuple.select 2) (tuple (/ 4 5) 9 (/ 11 9))))
(define-fun y () (Tuple Real Int Real) (tuple (/ 4 5) 9 (/ 11 9)))
-(define-fun y1 () (Tuple Real Int Real) ((_ tuple_update 1) (tuple (/ 4 5) 9 (/ 11 9)) 3))
-(check-sat-assuming ( (not (let ((_let_1 (tuple (/ 4 5) 9 (/ 11 9)))) (let ((_let_2 ((_ tuple_update 1) _let_1 3))) (and (and (and (= _let_1 _let_1) (= ((_ tuple_select 0) _let_1) ((_ tuple_select 0) _let_2))) (= ((_ tuple_select 2) _let_1) ((_ tuple_select 2) _let_2))) (= ((_ tuple_select 1) _let_2) 3))))) ))
+(define-fun y1 () (Tuple Real Int Real) ((_ tuple.update 1) (tuple (/ 4 5) 9 (/ 11 9)) 3))
+(check-sat-assuming ( (not (let ((_let_1 (tuple (/ 4 5) 9 (/ 11 9)))) (let ((_let_2 ((_ tuple.update 1) _let_1 3))) (and (and (and (= _let_1 _let_1) (= ((_ tuple.select 0) _let_1) ((_ tuple.select 0) _let_2))) (= ((_ tuple.select 2) _let_1) ((_ tuple.select 2) _let_2))) (= ((_ tuple.select 1) _let_2) 3))))) ))
(set-info :status sat)
(declare-fun x () (Tuple Int Int))
(declare-fun y () (Tuple Int Int))
-(assert (= ((_ tuple_update 0) x 1) ((_ tuple_update 1) y 2)))
+(assert (= ((_ tuple.update 0) x 1) ((_ tuple.update 1) y 2)))
(check-sat)
(declare-fun i () String)
(assert (= t (tuple 0 "0")))
-(assert (= i ((_ tuple_select 1) t)))
+(assert (= i ((_ tuple.select 1) t)))
(check-sat)
; EXPECT: sat
; EXPECT: (((a r) "active"))
-; EXPECT: ((((_ tuple_select 1) y) 9))
+; EXPECT: ((((_ tuple.select 1) y) 9))
(set-logic ALL)
(set-option :incremental false)
(set-option :produce-models true)
(assert (= y (tuple (/ 4 5) 9 (/ 11 9))))
(check-sat-assuming ( (not (= (a r) "what?")) ))
(get-value ( (a r) ))
-(get-value ( ((_ tuple_select 1) y) ))
+(get-value ( ((_ tuple.select 1) y) ))
(assert (bag.member y B))
(assert (bag.member z C))
-(assert (distinct x y ((_ tuple_project 0 1 2) z) ((_ tuple_project 3 4 5) z)))
+(assert (distinct x y ((_ tuple.project 0 1 2) z) ((_ tuple.project 3 4 5) z)))
(check-sat)
(declare-fun v () Tuple)
(declare-fun x () String)
(assert (= t (tuple "a" "b" "c" "d")))
-(assert (= x ((_ tuple_select 0) t)))
-(assert (= u ((_ tuple_project 2 3) t)))
-(assert (= v (tuple_project t)))
+(assert (= x ((_ tuple.select 0) t)))
+(assert (= u ((_ tuple.project 2 3) t)))
+(assert (= v (tuple.project t)))
(check-sat)
\ No newline at end of file
(declare-fun b () (Set (Tuple Int Real)))
(declare-fun x () (Tuple Real Real))
(assert (let ((_let_1 0.0)) (not (= x (tuple _let_1 _let_1)))))
-(assert (set.member (tuple ((_ tuple_select 0) x) (to_int ((_ tuple_select 1) x))) a))
-(assert (set.member (tuple (to_int ((_ tuple_select 0) x)) ((_ tuple_select 1) x)) b))
-(assert (not (= ((_ tuple_select 0) x) ((_ tuple_select 1) x))))
+(assert (set.member (tuple ((_ tuple.select 0) x) (to_int ((_ tuple.select 1) x))) a))
+(assert (set.member (tuple (to_int ((_ tuple.select 0) x)) ((_ tuple.select 1) x)) b))
+(assert (not (= ((_ tuple.select 0) x) ((_ tuple.select 1) x))))
(check-sat)
}
ASSERT_EQ(
- "((_ tuple_project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton "
+ "((_ tuple.project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton "
"\"Z\")))",
projection.toString());
}
assertEquals(elements[indices[i]], simplifiedTerm);
}
- assertEquals("((_ tuple_project 0 3 2 0 1 2) (tuple true 3 \"C\" "
+ assertEquals("((_ tuple.project 0 3 2 0 1 2) (tuple true 3 \"C\" "
+ "(set.singleton \"Z\")))",
projection.toString());
}
simplifiedTerm = solver.simplify(selectedTerm)
assert elements[i] == simplifiedTerm
- assert "((_ tuple_project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton \"Z\")))" == str(
+ assert "((_ tuple.project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton \"Z\")))" == str(
projection)
projects / cvc5.git / commitdiff