From e7b44afe8a667afd5154c95b6df9a7d663137fc5 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Tue, 25 Sep 2018 18:02:57 -0500 Subject: [PATCH] tests are in maude files --- tests/tools/meta/Makefile.am | 8 + .../hereditarily-finite-set.maude | 168 ++++++++++++++++++ tests/tools/meta/nelson-oppen/matrix.maude | 115 ++++++++++++ 3 files changed, 291 insertions(+) create mode 100644 tests/tools/meta/nelson-oppen/hereditarily-finite-set.maude create mode 100644 tests/tools/meta/nelson-oppen/matrix.maude diff --git a/tests/tools/meta/Makefile.am b/tests/tools/meta/Makefile.am index 20cc9269..db311df1 100644 --- a/tests/tools/meta/Makefile.am +++ b/tests/tools/meta/Makefile.am @@ -11,6 +11,10 @@ TESTS = \ mtransform.maude \ mconstruction.maude \ nelson-oppen-combination.maude \ + nelson-oppen/hereditarily-finite-set.maude \ + nelson-oppen/integer-list.maude \ + nelson-oppen/lexical-trichotomy-law.maude \ + nelson-oppen/matrix.maude \ sort-ops.maude \ unification.maude \ variables.maude \ @@ -28,6 +32,10 @@ RESULT_FILES = \ mtransform.expected \ mconstruction.expected \ nelson-oppen-combination.expected \ + nelson-oppen/hereditarily-finite-set.expected \ + nelson-oppen/integer-list.expected \ + nelson-oppen/lexical-trichotomy-law.expected \ + nelson-oppen/matrix.expected \ sort-ops.expected \ unification.expected \ variables.expected \ diff --git a/tests/tools/meta/nelson-oppen/hereditarily-finite-set.maude b/tests/tools/meta/nelson-oppen/hereditarily-finite-set.maude new file mode 100644 index 00000000..533868b4 --- /dev/null +++ b/tests/tools/meta/nelson-oppen/hereditarily-finite-set.maude @@ -0,0 +1,168 @@ +--- Hereditarily Finite Sets with Reals +--- ----------------------------------- +--- +--- In this example, we demonstrate the combination algorithm with non-convex theories -- non-linear +--- real arithmetic and hereditarily finite sets. Hereditarily finite sets is an example of a theory not +--- currently definable in CVC4 or Yices2 because of its use of algebraic data types modulo axioms like +--- associativity-commutativity and having FVP equations. Hereditarily finite sets (HFS) are a model of +--- set theory without the axiom of infinity. Although hereditarily finite sets are expressive enough to +--- encode constructs like the integers and the natural numbers, its initial model is a countable model +--- and so cannot encode the real numbers. + +set include BOOL off . + +fmod HEREDITARILY-FINITE-SET is + sort MyBool . + op tt : -> MyBool [ctor] . + op ff : -> MyBool [ctor] . + +--- We have three sorts, `X`, the parametric sort, `Set`s and `Magma`s. +--- Both `X`s and `Set`s are `Magma`s. + + sorts X Set Magma . + subsorts X Set < Magma . + + vars M M' M'' : Magma . + vars S : Set . + +--- The elements of a hereditarily finite set can be elements of the parameter sort `X` of "atomic +--- elements", or can be other hereditarily constructed inductively from the following three +--- constructors. First, `empty` is a `Set`: + + op empty : -> Set [ctor] . + +--- Second, the union operator is an associative, commutative and idemopotent operator: + + op _ , _ : Magma Magma -> Magma [ctor assoc comm] . + ---------------------------------------------------------------------------- + eq M , M , M' = M , M' [variant] . + eq M , M = M [variant] . + +--- Finally, a `Set` may be constructed from any `Magma` by enclosing it in braces. + + op { _ } : Magma -> Set [ctor] . + +--- We also have a subset operator and the various equations (not detailed here) defining it: + + op _ C= _ : Magma Magma -> MyBool . + ---------------------------------------------------------------------------- + eq empty C= M = tt [variant] . + eq { M } C= { M, M' } = tt [variant] . + + eq { M } C= { M } = tt [variant] . + eq { M } C= empty = ff [variant] . + + eq { M, M' } C= { M, M'' } + = { M' } C= { M, M'' } [variant] . + eq { M, M' } C= { M } + = { M' } C= { M } [variant] . + +--- Since `var-sat` does not support `[owise]`, we do not implement the equation +--- for handling the negative case. Since the theory is OS-Compact, we can just let +--- the predicate get stuck, partially evaluated. + + op _ U _ : Set Set -> Set . + ---------------------------------------------------------------------------- + eq empty U S = S [variant] . + eq { M } U { M' } = { M, M' } [variant] . +endfm + +fmod TEST-HEREDITARILY-FINITE-SET-SANITY is + protecting HEREDITARILY-FINITE-SET . + protecting BOOL . + vars M M' : Magma . +endfm + +reduce M, M', M == M, M' . +reduce { { empty }, { { empty } }, empty } + == { { empty }, { { empty } }, empty } + . + +reduce empty C= { empty } == tt . +reduce { empty } C= empty . +reduce { empty } C= { { empty } } . +reduce { empty } C= { empty, { empty } } == tt . +reduce { empty } C= { { empty }, { { empty } } } . +reduce { M, M' } C= { M, M' } . + +reduce { empty, empty } C= { empty } . + +--- Nelson Oppen +--- ------------ +--- +--- We must trick `var-sat` into thinking that the `X` sort is countable. +--- We instantiate this module with `Real`s as a subsort of `X`: + +fmod HFS-REAL is + including HEREDITARILY-FINITE-SET . + sorts Real . + subsorts Real < X . + + op fake-0 : -> Real [ctor] . + op fake-s : Real -> Real [ctor] . +endfm + +load ../../../contrib/tools/meta/nelson-oppen-combination + +fmod HEREDITARILY-FINITE-SET-TEST-VARSAT is + protecting BOOL . + protecting VAR-SAT . + protecting HFS-REAL . + vars M M' : Magma . +endfm + +--- TODO: This does not reduce as I expect it to +reduce upTerm({ X:Real, Y:Real, Z:Real } C= { X:Real }) . + +reduce upTerm({ X:Real, Y:Real, Z:Real } C= { A:Real }) . +reduce upTerm({ X:Real, Y:Real, Z:Real } ) . + +reduce var-sat( upModule('HFS-REAL, true) + , upTerm({ empty , M } C= { empty }) ?= 'tt.MyBool + ) . +reduce var-sat( upModule('HFS-REAL, true) + , upTerm({ empty , M } C= { empty }) ?= 'tt.MyBool + /\ upTerm(M) != 'empty.Set + ) . +reduce var-sat( upModule('HFS-REAL, true) + , upTerm({ empty , M } C= { empty , M' }) ?= 'tt.MyBool + ) . + +--- get variants { X:Magma, Y:Magma, Z:Magma } . +--- --- Lots and lots of variants? or variant computation is slow? +--- reduce var-sat( upModule('HFS-REAL, true) +--- , upTerm({ X:Magma, Y:Magma, Z:Magma } C= { X:Magma }) ?= 'tt.MyBool +--- ) == true . + +reduce var-sat( upModule('HFS-REAL, true) + , upTerm({ X:Real, Y:Real, Z:Real }) ?= upTerm({ X:Real }) + ) == true . + +reduce var-sat( upModule('HFS-REAL, true) + , upTerm({ X:Real, Y:Real, Z:Real } C= { X:Real }) ?= 'tt.MyBool + ) == true . + +--- Finally, we check the satisfiability of the formula $\{ x^2 , y^2, z^2 \} \subseteq \{ a \} \land x \ne y$. i.e. "is +--- it possible for the set of squares of three numbers, two of which must be distinct, to be a +--- subset of a set with a single element." This is indeed possible, since every positive real number +--- has two distinct square roots. Since set union is idempotent, if the two distinct numbers are +--- additive inverses of each other and the third is equal to either, then the proposition would indeed +--- be satisfied. + +set print attribute on . + +--- Our query is: + +reduce in NELSON-OPPEN-COMBINATION : + nelson-oppen-sat( ( tagged(tt, ('mod > 'REAL) ; ('check-sat > 'smt-sat)) + , tagged(tt, ('mod > 'HFS-REAL); ('check-sat > 'var-sat)) + ) + , ( '_C=_[ '`{_`}['_`,_[ '_*_ [ 'Z:Real, 'Z:Real ] + , '_*_ [ 'X:Real, 'X:Real ] + , '_*_ [ 'Y:Real, 'Y:Real ] + ]] + , '`{_`}['A:Real]] + ?= 'tt.MyBool + ) + /\ 'X:Real != 'Y:Real + ) . diff --git a/tests/tools/meta/nelson-oppen/matrix.maude b/tests/tools/meta/nelson-oppen/matrix.maude new file mode 100644 index 00000000..586aac76 --- /dev/null +++ b/tests/tools/meta/nelson-oppen/matrix.maude @@ -0,0 +1,115 @@ +--- Matrices with real and integer entries +--- -------------------------------------- +--- +--- We can define in Maude the theory of $2 \times 2$ matrices over a ring as the following module +--- parameterized by the theory of rings as its parameter theory: + +--- What is crucial about this theory instantiation is that, since the operators in \texttt{MATRIX-OPS} +--- are all definitional extensions, they can all be evaluated away to their righthand sides, i.e., to +--- operators in the disjoint union of two theories: (i) the FVP theory \texttt{MATRIX} obtained by +--- completely removing its \texttt{RING} parameter part, and (ii) the theory \texttt{REAL} to which the +--- parameter theory \texttt{RING} is instantiated. Therefore, the order-sorted Nelson-Oppen algorithm +--- can be invoked to decide validity and satisfiability of formulas in \texttt{MATRIX-REAL}, once we: +--- (i) evaluate away all defined operations in \texttt{MATRIX-OPS} appearing in a formula, and (ii) +--- purify the formula into its two disjoint parts. + +set include BOOL off . +load ../../../contrib/tools/meta/nelson-oppen-combination.maude + +fmod MATRIX-X is + sort X Matrix . + op matrix : X X X X -> Matrix [ctor] . + + vars A B C D : X . + op m11 : Matrix -> X . + op m12 : Matrix -> X . + op m21 : Matrix -> X . + op m22 : Matrix -> X . + + eq m11(matrix(A, B, C, D)) = A [variant] . + eq m12(matrix(A, B, C, D)) = B [variant] . + eq m21(matrix(A, B, C, D)) = C [variant] . + eq m22(matrix(A, B, C, D)) = D [variant] . +endfm + +--- Next, we define multiplication, determinant and identify as meta-functions -- +--- functions over terms at the meta-level. + +fmod MATRIX-TEST is + protecting NELSON-OPPEN-COMBINATION . + + vars A B A1 B1 A2 B2 ZERO ONE : Term . + + op mulSum : Term Term Term Term -> Term . + eq mulSum(A1, B1, A2, B2) = '_+_ [ '_*_ [ A1 , B1 ] + , '_*_ [ A2 , B2 ] + ] . + + op multiply : Term Term -> Term . + eq multiply(A, B) = 'matrix[ mulSum('m11[A], 'm11[B], 'm12[A], 'm21[B]) + , mulSum('m11[A], 'm12[B], 'm12[A], 'm22[B]) + , mulSum('m21[A], 'm11[B], 'm22[A], 'm21[B]) + , mulSum('m21[A], 'm12[B], 'm22[A], 'm22[B]) + ] . + op determinant : Term -> Term . + eq determinant(A) = '_-_ [ '_*_ [ 'm11[A], 'm22[A] ] + , '_*_ [ 'm12[A], 'm21[A] ] + ] . + + op identity : Term Term -> Term . + eq identity(ZERO, ONE) = 'matrix[ONE, ZERO, ZERO, ONE] . +endfm + +--- Finally, we the parameterise this theory over the reals: + +fmod MATRIX-REAL is + including MATRIX-X . + sort Real . + subsorts Real < X . + --- Convince var-sat that Real is an infinite sort. + op fake-zero : -> Real [ctor] . + op fake-succ : Real -> Real [ctor] . +endfm + +set print attribute on . + +reduce in MATRIX-TEST : nelson-oppen-valid( + ( tagged(tt, (('mod > 'MATRIX-REAL); ('check-sat > 'var-sat))) + , tagged(tt, (('mod > 'REAL); ('check-sat > 'smt-sat))) + ), + (multiply('A:Matrix, 'B:Matrix) ?= identity('0/1.Real, '1/1.Real)) + => (determinant('A:Matrix) != '0/1.Real) + ) . + +--- It turns out that if we combine this module with the Integers instead of the Reals, we can prove +--- something stronger: that any invertible matrix must have determinant $\pm 1$. Unfortunately, CVC4 is +--- not able to solve the non-linear arithmetic needed to prove this. We must instead turn to the Yices +--- solver, the other SMT solver available in Maude. Even so, the default configuration for Yices does +--- not enable the solver for non-linear arithmetic (MCSAT), and running this example involved modifying +--- the Maude C++ source code to enable that configuration. Even so, the computational difficulty +--- involved in solving non-linear integer arithmetic forced us to restrict the proof to +--- upper-triangular matrices. + +fmod MATRIX-INTEGER is + including MATRIX-X . + sort Integer . + subsorts Integer < X . + --- Convince var-sat that Integer is an infinite sort. + op fake-zero : -> Integer [ctor] . + op fake-succ : Integer -> Integer [ctor] . +endfm + +reduce in MATRIX-TEST : nelson-oppen-valid( + ( tagged(tt, (('mod > 'MATRIX-INTEGER); + ('check-sat > 'var-sat); ('convex > 'true))) + , tagged(tt, (('mod > 'INTEGER ); + ('check-sat > 'smt-sat); ('convex > 'false))) + ), + ( multiply('A:Matrix, 'B:Matrix) ?= identity('0.Integer, '1.Integer) + /\ 'm21['A:Matrix] ?= '0.Integer + /\ 'm21['B:Matrix] ?= '0.Integer + ) + => ( determinant('A:Matrix) ?= '1.Integer + \/ determinant('A:Matrix) ?= '-_['1.Integer] + ) + ) .