Skip to content

Commit

Permalink
Update test results
Browse files Browse the repository at this point in the history
  • Loading branch information
@nishantjr
nishantjr committed Sep 25, 2018
1 parent 5cbe8de commit 5d86198
Show file tree
Hide file tree
Showing 2 changed files with 83 additions and 7 deletions.
13 changes: 6 additions & 7 deletions tests/systems/nelson-oppen/hereditarily-finite-set.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)) .
77 changes: 77 additions & 0 deletions tests/systems/nelson-oppen/matrix.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.

0 comments on commit 5d86198

Please sign in to comment.