tests are in maude files

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 \

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
+                         ) .

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]
+           )
+     ) .