From 5d861985807668e663f8e8a6d36bc05227d9f5df Mon Sep 17 00:00:00 2001
From: Nishant Rodrigues <nishantjr@gmail.com>
Date: Tue, 10 Jul 2018 12:24:45 +0530
Subject: [PATCH] Update test results

---
 .../hereditarily-finite-set.expected          | 13 ++--
 tests/systems/nelson-oppen/matrix.expected    | 77 +++++++++++++++++++
 2 files changed, 83 insertions(+), 7 deletions(-)

diff --git a/tests/systems/nelson-oppen/hereditarily-finite-set.expected b/tests/systems/nelson-oppen/hereditarily-finite-set.expected
index 69379d08..309e8a8b 100644
--- a/tests/systems/nelson-oppen/hereditarily-finite-set.expected
+++ b/tests/systems/nelson-oppen/hereditarily-finite-set.expected
@@ -89,10 +89,9 @@ Warning: sort declarations for operator resolveNames failed preregularity check
     on 6 out of 47 sort tuples. First such tuple is (Type).
 Warning: sort declarations for operator resolveNames failed preregularity check
     on 1 out of 26 sort tuples. First such tuple is (NullDeclSet).
-Warning: <standard input>, line 191: didn't expect token `{_`}:
-nelson-oppen-valid ( ( tagged ( tt , ( 'mod > 'REAL ) ; ( 'check-sat > 'smt-sat
-    ) ) , tagged ( tt , ( 'mod > 'HFS-REAL ) ; ( 'check-sat > 'var-sat ) ) ) ,
-    ( '`{_`} [ '_`,_ [ '_*_ [ 'Z:Real , 'Z:Real ] , '_*_ [ 'X:Real , 'X:Real ]
-    , '_*_ [ 'Y:Real , 'Y:Real ] ] ] ?= `{_`} <---*HERE*
-Warning: <standard input>, line 184: no parse for term.
-Bye.
+==========================================
+reduce in NELSON-OPPEN-COMBINATION : nelson-oppen-valid(tagged(tt, ('check-sat
+    > 'smt-sat) ; 'mod > 'REAL),tagged(tt, ('check-sat > 'var-sat) ; 'mod >
+    'HFS-REAL), ('tt.MyBool ?= '_C=_['`{_`}['_`,_['_*_['Z:Real,'Z:Real],'_*_[
+    'X:Real,'X:Real],'_*_['Y:Real,'Y:Real]]],'`{_`}['_`,_['A:Real]]] /\ 'X:Real
+    != 'Y:Real) => ('X:Real ?= 'Z:Real \/ 'Y:Real ?= 'Z:Real)) .
diff --git a/tests/systems/nelson-oppen/matrix.expected b/tests/systems/nelson-oppen/matrix.expected
index cf2e4f34..7994f578 100644
--- a/tests/systems/nelson-oppen/matrix.expected
+++ b/tests/systems/nelson-oppen/matrix.expected
@@ -44,3 +44,80 @@ Purified:
     '#makeVariable`(1/1.Real`):Real,'#makeVariable`(0/1.Real`):Real,
     '#makeVariable`(0/1.Real`):Real,'#makeVariable`(1/1.Real`):Real] ?=
     'matrix['#makeVariable`(_+_`[_*_`[#makeVariable`(m11`[A:Matrix`]`):Real`,#makeVariable`(m11`[B:Matrix`]`):Real`]`,_*_`[#makeVariable`(m12`[A:Matrix`]`):Real`,#makeVariable`(m21`[B:Matrix`]`):Real`]`]`):Real,'#makeVariable`(_+_`[_*_`[#makeVariable`(m11`[A:Matrix`]`):Real`,#makeVariable`(m12`[B:Matrix`]`):Real`]`,_*_`[#makeVariable`(m12`[A:Matrix`]`):Real`,#makeVariable`(m22`[B:Matrix`]`):Real`]`]`):Real,'#makeVariable`(_+_`[_*_`[#makeVariable`(m21`[A:Matrix`]`):Real`,#makeVariable`(m11`[B:Matrix`]`):Real`]`,_*_`[#makeVariable`(m22`[A:Matrix`]`):Real`,#makeVariable`(m21`[B:Matrix`]`):Real`]`]`):Real,'#makeVariable`(_+_`[_*_`[#makeVariable`(m21`[A:Matrix`]`):Real`,#makeVariable`(m12`[B:Matrix`]`):Real`]`,_*_`[#makeVariable`(m22`[A:Matrix`]`):Real`,#makeVariable`(m22`[B:Matrix`]`):Real`]`]`):Real], ('check-sat > 'var-sat) ; ('convex > 'false) ; 'mod > 'MATRIX-REAL)
+EqualityProp: 'MATRIX-REAL: => '#makeVariable`(0/1.Real`):Real ?= '#makeVariable`(_+_`[_*_`[#makeVariable`(m11`[A:Matrix`]`):Real`,#makeVariable`(m12`[B:Matrix`]`):Real`]`,_*_`[#makeVariable`(m12`[A:Matrix`]`):Real`,#makeVariable`(m22`[B:Matrix`]`):Real`]`]`):Real
+EqualityProp: 'MATRIX-REAL: => '#makeVariable`(1/1.Real`):Real ?= '#makeVariable`(_+_`[_*_`[#makeVariable`(m11`[A:Matrix`]`):Real`,#makeVariable`(m11`[B:Matrix`]`):Real`]`,_*_`[#makeVariable`(m12`[A:Matrix`]`):Real`,#makeVariable`(m21`[B:Matrix`]`):Real`]`]`):Real
+EqualityProp: 'REAL: => '#makeVariable`(_+_`[_*_`[#makeVariable`(m11`[A:Matrix`]`):Real`,#makeVariable`(m12`[B:Matrix`]`):Real`]`,_*_`[#makeVariable`(m12`[A:Matrix`]`):Real`,#makeVariable`(m22`[B:Matrix`]`):Real`]`]`):Real ?= '#makeVariable`(_+_`[_*_`[#makeVariable`(m21`[A:Matrix`]`):Real`,#makeVariable`(m12`[B:Matrix`]`):Real`]`,_*_`[#makeVariable`(m22`[A:Matrix`]`):Real`,#makeVariable`(m22`[B:Matrix`]`):Real`]`]`):Real
+EqualityProp: 'MATRIX-REAL: => '#makeVariable`(_+_`[_*_`[#makeVariable`(m11`[A:Matrix`]`):Real`,#makeVariable`(m11`[B:Matrix`]`):Real`]`,_*_`[#makeVariable`(m12`[A:Matrix`]`):Real`,#makeVariable`(m21`[B:Matrix`]`):Real`]`]`):Real ?= '#makeVariable`(_+_`[_*_`[#makeVariable`(m21`[A:Matrix`]`):Real`,#makeVariable`(m11`[B:Matrix`]`):Real`]`,_*_`[#makeVariable`(m22`[A:Matrix`]`):Real`,#makeVariable`(m21`[B:Matrix`]`):Real`]`]`):Real
+EqualityProp: 'REAL: => '#makeVariable`(m11`[A:Matrix`]`):Real ?=
+    '#makeVariable`(m21`[A:Matrix`]`):Real
+EqualityProp: 'REAL: => '#makeVariable`(m12`[A:Matrix`]`):Real ?=
+    '#makeVariable`(m22`[A:Matrix`]`):Real
+EqualityProp: 'MATRIX-REAL: => '#makeVariable`(_+_`[_*_`[#makeVariable`(m21`[A:Matrix`]`):Real`,#makeVariable`(m11`[B:Matrix`]`):Real`]`,_*_`[#makeVariable`(m22`[A:Matrix`]`):Real`,#makeVariable`(m21`[B:Matrix`]`):Real`]`]`):Real ?= '#makeVariable`(_+_`[_*_`[#makeVariable`(m21`[A:Matrix`]`):Real`,#makeVariable`(m12`[B:Matrix`]`):Real`]`,_*_`[#makeVariable`(m22`[A:Matrix`]`):Real`,#makeVariable`(m22`[B:Matrix`]`):Real`]`]`):Real
+rewrites: 73440
+result Bool: (true).Bool
+==========================================
+reduce in MATRIX-TEST : nelson-oppen-valid(tagged(tt, (('check-sat > 'smt-sat)
+    ; 'convex > 'false) ; 'mod > 'INTEGER),tagged(tt, (('check-sat > 'var-sat)
+    ; 'convex > 'true) ; 'mod > 'MATRIX-INTEGER), (multiply('A:Matrix,
+    'B:Matrix) ?= identity('0.Integer, '1.Integer) /\ '0.Integer ?= 'm21[
+    'A:Matrix] /\ '0.Integer ?= 'm21['B:Matrix]) => ('1.Integer ?= determinant(
+    'A:Matrix) \/ determinant('A:Matrix) ?= '-_['1.Integer])) .
+Purified:
+	tagged('#makeVariable`(0.Integer`):Integer ?=
+    '#makeVariable`(m21`[A:Matrix`]`):Integer /\
+    '#makeVariable`(0.Integer`):Integer ?=
+    '#makeVariable`(m21`[B:Matrix`]`):Integer /\
+    '#makeVariable`(0.Integer`):Integer ?= '0.Integer /\
+    '#makeVariable`(1.Integer`):Integer ?= '1.Integer /\ '#makeVariable`(_+_`[_*_`[#makeVariable`(m11`[A:Matrix`]`):Integer`,#makeVariable`(m11`[B:Matrix`]`):Integer`]`,_*_`[#makeVariable`(m12`[A:Matrix`]`):Integer`,#makeVariable`(m21`[B:Matrix`]`):Integer`]`]`):Integer ?= '_+_['_*_[
+    '#makeVariable`(m11`[A:Matrix`]`):Integer,
+    '#makeVariable`(m11`[B:Matrix`]`):Integer],'_*_[
+    '#makeVariable`(m12`[A:Matrix`]`):Integer,
+    '#makeVariable`(m21`[B:Matrix`]`):Integer]] /\ '#makeVariable`(_+_`[_*_`[#makeVariable`(m11`[A:Matrix`]`):Integer`,#makeVariable`(m12`[B:Matrix`]`):Integer`]`,_*_`[#makeVariable`(m12`[A:Matrix`]`):Integer`,#makeVariable`(m22`[B:Matrix`]`):Integer`]`]`):Integer ?= '_+_['_*_[
+    '#makeVariable`(m11`[A:Matrix`]`):Integer,
+    '#makeVariable`(m12`[B:Matrix`]`):Integer],'_*_[
+    '#makeVariable`(m12`[A:Matrix`]`):Integer,
+    '#makeVariable`(m22`[B:Matrix`]`):Integer]] /\ '#makeVariable`(_+_`[_*_`[#makeVariable`(m21`[A:Matrix`]`):Integer`,#makeVariable`(m11`[B:Matrix`]`):Integer`]`,_*_`[#makeVariable`(m22`[A:Matrix`]`):Integer`,#makeVariable`(m21`[B:Matrix`]`):Integer`]`]`):Integer ?= '_+_['_*_[
+    '#makeVariable`(m21`[A:Matrix`]`):Integer,
+    '#makeVariable`(m11`[B:Matrix`]`):Integer],'_*_[
+    '#makeVariable`(m22`[A:Matrix`]`):Integer,
+    '#makeVariable`(m21`[B:Matrix`]`):Integer]] /\ '#makeVariable`(_+_`[_*_`[#makeVariable`(m21`[A:Matrix`]`):Integer`,#makeVariable`(m12`[B:Matrix`]`):Integer`]`,_*_`[#makeVariable`(m22`[A:Matrix`]`):Integer`,#makeVariable`(m22`[B:Matrix`]`):Integer`]`]`):Integer ?= '_+_['_*_[
+    '#makeVariable`(m21`[A:Matrix`]`):Integer,
+    '#makeVariable`(m12`[B:Matrix`]`):Integer],'_*_[
+    '#makeVariable`(m22`[A:Matrix`]`):Integer,
+    '#makeVariable`(m22`[B:Matrix`]`):Integer]] /\ '1.Integer != '_-_['_*_[
+    '#makeVariable`(m11`[A:Matrix`]`):Integer,
+    '#makeVariable`(m22`[A:Matrix`]`):Integer],'_*_[
+    '#makeVariable`(m12`[A:Matrix`]`):Integer,
+    '#makeVariable`(m21`[A:Matrix`]`):Integer]] /\ '-_['1.Integer] != '_-_[
+    '_*_['#makeVariable`(m11`[A:Matrix`]`):Integer,
+    '#makeVariable`(m22`[A:Matrix`]`):Integer],'_*_[
+    '#makeVariable`(m12`[A:Matrix`]`):Integer,
+    '#makeVariable`(m21`[A:Matrix`]`):Integer]], ('check-sat > 'smt-sat) ; (
+    'convex > 'false) ; 'mod > 'INTEGER)
+	tagged('#makeVariable`(0.Integer`):Integer ?=
+    '#makeVariable`(m21`[A:Matrix`]`):Integer /\
+    '#makeVariable`(0.Integer`):Integer ?=
+    '#makeVariable`(m21`[B:Matrix`]`):Integer /\
+    '#makeVariable`(m11`[A:Matrix`]`):Integer ?= 'm11['A:Matrix] /\
+    '#makeVariable`(m11`[B:Matrix`]`):Integer ?= 'm11['B:Matrix] /\
+    '#makeVariable`(m12`[A:Matrix`]`):Integer ?= 'm12['A:Matrix] /\
+    '#makeVariable`(m12`[B:Matrix`]`):Integer ?= 'm12['B:Matrix] /\
+    '#makeVariable`(m21`[A:Matrix`]`):Integer ?= 'm21['A:Matrix] /\
+    '#makeVariable`(m21`[B:Matrix`]`):Integer ?= 'm21['B:Matrix] /\
+    '#makeVariable`(m22`[A:Matrix`]`):Integer ?= 'm22['A:Matrix] /\
+    '#makeVariable`(m22`[B:Matrix`]`):Integer ?= 'm22['B:Matrix] /\ 'matrix[
+    '#makeVariable`(1.Integer`):Integer,'#makeVariable`(0.Integer`):Integer,
+    '#makeVariable`(0.Integer`):Integer,'#makeVariable`(1.Integer`):Integer] ?=
+    'matrix['#makeVariable`(_+_`[_*_`[#makeVariable`(m11`[A:Matrix`]`):Integer`,#makeVariable`(m11`[B:Matrix`]`):Integer`]`,_*_`[#makeVariable`(m12`[A:Matrix`]`):Integer`,#makeVariable`(m21`[B:Matrix`]`):Integer`]`]`):Integer,'#makeVariable`(_+_`[_*_`[#makeVariable`(m11`[A:Matrix`]`):Integer`,#makeVariable`(m12`[B:Matrix`]`):Integer`]`,_*_`[#makeVariable`(m12`[A:Matrix`]`):Integer`,#makeVariable`(m22`[B:Matrix`]`):Integer`]`]`):Integer,'#makeVariable`(_+_`[_*_`[#makeVariable`(m21`[A:Matrix`]`):Integer`,#makeVariable`(m11`[B:Matrix`]`):Integer`]`,_*_`[#makeVariable`(m22`[A:Matrix`]`):Integer`,#makeVariable`(m21`[B:Matrix`]`):Integer`]`]`):Integer,'#makeVariable`(_+_`[_*_`[#makeVariable`(m21`[A:Matrix`]`):Integer`,#makeVariable`(m12`[B:Matrix`]`):Integer`]`,_*_`[#makeVariable`(m22`[A:Matrix`]`):Integer`,#makeVariable`(m22`[B:Matrix`]`):Integer`]`]`):Integer], (
+    'check-sat > 'var-sat) ; ('convex > 'true) ; 'mod > 'MATRIX-INTEGER)
+EqualityProp: 'INTEGER: => '#makeVariable`(0.Integer`):Integer ?= '#makeVariable`(_+_`[_*_`[#makeVariable`(m21`[A:Matrix`]`):Integer`,#makeVariable`(m11`[B:Matrix`]`):Integer`]`,_*_`[#makeVariable`(m22`[A:Matrix`]`):Integer`,#makeVariable`(m21`[B:Matrix`]`):Integer`]`]`):Integer
+EqualityProp: 'INTEGER: => '#makeVariable`(_+_`[_*_`[#makeVariable`(m21`[A:Matrix`]`):Integer`,#makeVariable`(m11`[B:Matrix`]`):Integer`]`,_*_`[#makeVariable`(m22`[A:Matrix`]`):Integer`,#makeVariable`(m21`[B:Matrix`]`):Integer`]`]`):Integer ?= '#makeVariable`(m21`[A:Matrix`]`):Integer
+EqualityProp: 'INTEGER: => '#makeVariable`(m21`[A:Matrix`]`):Integer ?=
+    '#makeVariable`(m21`[B:Matrix`]`):Integer
+EqualityProp: 'MATRIX-INTEGER: => '#makeVariable`(1.Integer`):Integer ?= '#makeVariable`(_+_`[_*_`[#makeVariable`(m11`[A:Matrix`]`):Integer`,#makeVariable`(m11`[B:Matrix`]`):Integer`]`,_*_`[#makeVariable`(m12`[A:Matrix`]`):Integer`,#makeVariable`(m21`[B:Matrix`]`):Integer`]`]`):Integer
+EqualityProp: 'INTEGER: => '#makeVariable`(m11`[A:Matrix`]`):Integer ?=
+    '#makeVariable`(m11`[B:Matrix`]`):Integer
+EqualityProp: 'MATRIX-INTEGER: => '#makeVariable`(_+_`[_*_`[#makeVariable`(m11`[A:Matrix`]`):Integer`,#makeVariable`(m11`[B:Matrix`]`):Integer`]`,_*_`[#makeVariable`(m12`[A:Matrix`]`):Integer`,#makeVariable`(m21`[B:Matrix`]`):Integer`]`]`):Integer ?= '#makeVariable`(_+_`[_*_`[#makeVariable`(m21`[A:Matrix`]`):Integer`,#makeVariable`(m12`[B:Matrix`]`):Integer`]`,_*_`[#makeVariable`(m22`[A:Matrix`]`):Integer`,#makeVariable`(m22`[B:Matrix`]`):Integer`]`]`):Integer
+rewrites: 61607
+result Bool: (true).Bool
+Bye.