Changed variable representation in linear expressions from Variable to Lv (#858)

* Changed variable representation in linear expressions from Variable to Lv

* Added CHANGELOG fix

* Minor domain progress?

* Fixed failing tests

* Get rid of hashing causing non-determinismistic compilation

Author: MatthewDaggitt

ChangeLog.md

@@ -4,6 +4,8 @@
 
 * Decreased the size of generated verification plan files by 75%
 
+* Improved the ordering of constraints in generated query files.
+
 ## Version 0.15
 
 * Added functions `min` and `max` over rationals.

vehicle/src/Vehicle/Backend/LossFunction/Core.hs

@@ -7,8 +7,12 @@ import Data.Set qualified as Set
 import GHC.Generics (Generic)
 import Vehicle.Backend.Prelude (DifferentiableLogicID)
 import Vehicle.Compile.Prelude
+import Vehicle.Data.Builtin.Interface
 import Vehicle.Data.Builtin.Loss
+import Vehicle.Data.Builtin.Standard
+import Vehicle.Data.Code.Interface
 import Vehicle.Data.Code.Value (BoundEnv, Closure (..), VBinder, Value (..))
+import Vehicle.Data.Tensor
 import Vehicle.Libraries.StandardLibrary.Definitions (StdLibFunction (..))
 
 --------------------------------------------------------------------------------
@@ -62,49 +66,49 @@ type CompiledDifferentiableLogic = (DifferentiableLogicID, DifferentiableLogicIm
 
 --------------------------------------------------------------------------------
 -- Views on Boolean Tensors
-{-
+
 -- | A view on all possible expressions that can have type `Tensor Bool`.
 data BoolTensorView expr
   = VConstBoolTensor expr expr
   | VBoolTensor (Tensor Bool)
-  | VStackBoolTensor Int [expr]
-  | VAndTensor expr expr
-  | VOrTensor expr expr
-  | VNotTensor expr
-  | VOrderRatTensor OrderOp expr expr
-  | VEqualsRatTensor EqualityOp expr expr
-  | VQuantifyRatTensor Quantifier expr
-  | VReduceAndTensor expr
-  | VReduceOrTensor expr
+  | VStackBoolTensor Int (GenericArg expr) [expr]
+  | VAndTensor (GenericArg expr) expr expr
+  | VOrTensor (GenericArg expr) expr expr
+  | VNotTensor (GenericArg expr) expr
+  | VOrderRatTensor OrderOp (GenericArg expr) expr expr
+  | VEqualsRatTensor EqualityOp (GenericArg expr) expr expr
+  | VQuantifyRatTensor Quantifier (GenericArg expr) expr
+  | VReduceAndTensor (GenericArg expr) expr
+  | VReduceOrTensor (GenericArg expr) expr
 
 fromBoolTensorView :: (HasBoolTensors expr, HasDimensionData expr) => BoolTensorView expr -> expr
 fromBoolTensorView = \case
   VBoolTensor y -> INullaryBoolTensorOp (BoolTensor y)
-  VAndTensor x y -> IBoolTensorOp AndBoolTensor (explicit <$> [x, y])
-  VOrTensor x y -> IBoolTensorOp OrBoolTensor (explicit <$> [x, y])
-  VNotTensor x -> IBoolTensorOp NotBoolTensor (explicit <$> [x])
-  VOrderRatTensor op x y -> IBoolTensorOp (OrderRatTensor op) (explicit <$> [x, y])
-  VEqualsRatTensor op x y -> IBoolTensorOp (EqualsRatTensor op) (explicit <$> [x, y])
-  VQuantifyRatTensor op x -> IBoolTensorOp (QuantifyRatTensor op) (explicit <$> [x])
-  VReduceAndTensor x -> IBoolTensorOp ReduceAndTensor (explicit <$> [x])
-  VReduceOrTensor x -> IBoolTensorOp ReduceOrTensor (explicit <$> [x])
-  VConstBoolTensor x y -> IBoolConstTensor x y
-  VStackBoolTensor n xs -> IDimensionDataOp (StackTensor n) (explicit <$> xs)
+  VAndTensor dims x y -> IBoolTensorOp AndBoolTensor [dims, explicit x, explicit y]
+  VOrTensor dims x y -> IBoolTensorOp OrBoolTensor [dims, explicit x, explicit y]
+  VNotTensor dims x -> IBoolTensorOp NotBoolTensor [dims, explicit x]
+  VOrderRatTensor op dims x y -> IBoolTensorOp (OrderRatTensor op) [dims, explicit x, explicit y]
+  VEqualsRatTensor op dims x y -> IBoolTensorOp (EqualsRatTensor op) [dims, explicit x, explicit y]
+  VQuantifyRatTensor op dims x -> IBoolTensorOp (QuantifyRatTensor op) [dims, explicit x]
+  VReduceAndTensor dims x -> IBoolTensorOp ReduceAndTensor [dims, explicit x]
+  VReduceOrTensor dims x -> IBoolTensorOp ReduceOrTensor [dims, explicit x]
+  VConstBoolTensor x dims -> IDimensionDataOp ConstTensor [implicit IBoolElementType, explicit x, explicit dims]
+  VStackBoolTensor n elemDims xs -> IDimensionDataOp (StackTensor n) (implicit IBoolElementType : elemDims : (explicit <$> xs))
 
 toBoolTensorView :: (HasDimensionData expr, HasBoolTensors expr) => expr -> BoolTensorView expr
 toBoolTensorView expr = case getBoolTensorOp expr of
   Just (BoolTensor b, []) -> VBoolTensor b
-  Just (AndBoolTensor, [x, y]) -> VAndTensor (argExpr x) (argExpr y)
-  Just (OrBoolTensor, [x, y]) -> VOrTensor (argExpr x) (argExpr y)
-  Just (NotBoolTensor, [x]) -> VNotTensor (argExpr x)
-  Just (OrderRatTensor op, [x, y]) -> VOrderRatTensor op (argExpr x) (argExpr y)
-  Just (EqualsRatTensor op, [x, y]) -> VEqualsRatTensor op (argExpr x) (argExpr y)
-  Just (QuantifyRatTensor op, [x]) -> VQuantifyRatTensor op (argExpr x)
-  Just (ReduceAndTensor, [x]) -> VReduceAndTensor (argExpr x)
-  Just (ReduceOrTensor, [x]) -> VReduceOrTensor (argExpr x)
+  Just (AndBoolTensor, [dims, x, y]) -> VAndTensor dims (argExpr x) (argExpr y)
+  Just (OrBoolTensor, [dims, x, y]) -> VOrTensor dims (argExpr x) (argExpr y)
+  Just (NotBoolTensor, [dims, x]) -> VNotTensor dims (argExpr x)
+  Just (OrderRatTensor op, [dims, x, y]) -> VOrderRatTensor op dims (argExpr x) (argExpr y)
+  Just (EqualsRatTensor op, [dims, x, y]) -> VEqualsRatTensor op dims (argExpr x) (argExpr y)
+  Just (QuantifyRatTensor op, [dims, x]) -> VQuantifyRatTensor op dims (argExpr x)
+  Just (ReduceAndTensor, [dims, x]) -> VReduceAndTensor dims (argExpr x)
+  Just (ReduceOrTensor, [dims, x]) -> VReduceOrTensor dims (argExpr x)
   Nothing -> case getDimensionDataOp expr of
-    Just (ConstTensor, [x, y]) -> VConstBoolTensor (argExpr x) (argExpr y)
-    Just (StackTensor n, args) -> VStackBoolTensor n (fmap argExpr args)
+    Just (ConstTensor, [argExpr -> IBoolElementType, x, dims]) -> VConstBoolTensor (argExpr x) (argExpr dims)
+    Just (StackTensor n, (argExpr -> IBoolElementType) : elemDims : args) -> VStackBoolTensor n elemDims (fmap argExpr args)
     _ -> developerError "ill-typed BoolTensor expression"
   _ -> developerError "ill-typed BoolTensor expression"
 
@@ -116,60 +120,60 @@ data RatTensorView expr
   = VConstRatTensor expr expr
   | VRatTensor (Tensor Rational)
   | VRatTensorVar Lv
-  | VStackRatTensor Int [expr]
-  | VNegRatTensor expr
-  | VAddRatTensor expr expr
-  | VSubRatTensor expr expr
-  | VMulRatTensor expr expr
-  | VDivRatTensor expr expr
-  | VMinRatTensor expr expr
-  | VMaxRatTensor expr expr
-  | VReduceAddRatTensor expr
-  | VReduceMulRatTensor expr
-  | VReduceMinRatTensor expr
-  | VReduceMaxRatTensor expr
-  | VSearchRatTensor expr expr expr expr
+  | VStackRatTensor Int (GenericArg expr) [expr]
+  | VNegRatTensor (GenericArg expr) expr
+  | VAddRatTensor (GenericArg expr) expr expr
+  | VSubRatTensor (GenericArg expr) expr expr
+  | VMulRatTensor (GenericArg expr) expr expr
+  | VDivRatTensor (GenericArg expr) expr expr
+  | VMinRatTensor (GenericArg expr) expr expr
+  | VMaxRatTensor (GenericArg expr) expr expr
+  | VReduceAddRatTensor (GenericArg expr) expr
+  | VReduceMulRatTensor (GenericArg expr) expr
+  | VReduceMinRatTensor (GenericArg expr) expr
+  | VReduceMaxRatTensor (GenericArg expr) expr
+  | VSearchRatTensor (GenericArg expr) expr expr expr expr
 
 fromRatTensorView :: (BuiltinHasRatTensor builtin, BuiltinHasDimensionData builtin) => RatTensorView (Value builtin) -> Value builtin
 fromRatTensorView = \case
   VRatTensor y -> INullaryRatTensorOp (RatTensor y)
-  VNegRatTensor x -> IRatTensorOp NegRatTensor (explicit <$> [x])
-  VAddRatTensor x y -> IRatTensorOp AddRatTensor (explicit <$> [x, y])
-  VSubRatTensor x y -> IRatTensorOp SubRatTensor (explicit <$> [x, y])
-  VMulRatTensor x y -> IRatTensorOp MulRatTensor (explicit <$> [x, y])
-  VDivRatTensor x y -> IRatTensorOp DivRatTensor (explicit <$> [x, y])
-  VMinRatTensor x y -> IRatTensorOp MinRatTensor (explicit <$> [x, y])
-  VMaxRatTensor x y -> IRatTensorOp MaxRatTensor (explicit <$> [x, y])
-  VReduceAddRatTensor x -> IRatTensorOp ReduceAddRatTensor (explicit <$> [x])
-  VReduceMulRatTensor x -> IRatTensorOp ReduceMulRatTensor (explicit <$> [x])
-  VReduceMinRatTensor x -> IRatTensorOp ReduceMinRatTensor (explicit <$> [x])
-  VReduceMaxRatTensor x -> IRatTensorOp ReduceMaxRatTensor (explicit <$> [x])
-  VConstRatTensor x y -> IRatConstTensor [x, y]
-  VStackRatTensor n xs -> IDimensionDataOp (StackTensor n) (explicit <$> xs)
-  VSearchRatTensor reduce lower upper fn -> IRatTensorOp SearchRatTensor (explicit <$> [reduce, lower, upper, fn])
+  VNegRatTensor dims x -> IRatTensorOp NegRatTensor [dims, explicit x]
+  VAddRatTensor dims x y -> IRatTensorOp AddRatTensor [dims, explicit x, explicit y]
+  VSubRatTensor dims x y -> IRatTensorOp SubRatTensor [dims, explicit x, explicit y]
+  VMulRatTensor dims x y -> IRatTensorOp MulRatTensor [dims, explicit x, explicit y]
+  VDivRatTensor dims x y -> IRatTensorOp DivRatTensor [dims, explicit x, explicit y]
+  VMinRatTensor dims x y -> IRatTensorOp MinRatTensor [dims, explicit x, explicit y]
+  VMaxRatTensor dims x y -> IRatTensorOp MaxRatTensor [dims, explicit x, explicit y]
+  VReduceAddRatTensor dims x -> IRatTensorOp ReduceAddRatTensor [dims, explicit x]
+  VReduceMulRatTensor dims x -> IRatTensorOp ReduceMulRatTensor [dims, explicit x]
+  VReduceMinRatTensor dims x -> IRatTensorOp ReduceMinRatTensor [dims, explicit x]
+  VReduceMaxRatTensor dims x -> IRatTensorOp ReduceMaxRatTensor [dims, explicit x]
+  VConstRatTensor x dims -> IDimensionDataOp ConstTensor [implicit IRatElementType, explicit x, explicit dims]
+  VStackRatTensor n elemDims xs -> IDimensionDataOp (StackTensor n) (implicit IRatElementType : elemDims : (explicit <$> xs))
+  VSearchRatTensor dims reduce lower upper fn -> IRatTensorOp SearchRatTensor (dims : (explicit <$> [reduce, lower, upper, fn]))
   VRatTensorVar v -> VBoundVar v []
 
 toRatTensorView :: (BuiltinHasRatTensor builtin, BuiltinHasDimensionData builtin) => Value builtin -> RatTensorView (Value builtin)
 toRatTensorView expr = case getRatTensorOp expr of
   Just (RatTensor b, []) -> VRatTensor b
-  Just (NegRatTensor, [x]) -> VNegRatTensor (argExpr x)
-  Just (AddRatTensor, [x, y]) -> VAddRatTensor (argExpr x) (argExpr y)
-  Just (SubRatTensor, [x, y]) -> VSubRatTensor (argExpr x) (argExpr y)
-  Just (MulRatTensor, [x, y]) -> VMulRatTensor (argExpr x) (argExpr y)
-  Just (DivRatTensor, [x, y]) -> VDivRatTensor (argExpr x) (argExpr y)
-  Just (MinRatTensor, [x, y]) -> VMinRatTensor (argExpr x) (argExpr y)
-  Just (MaxRatTensor, [x, y]) -> VMaxRatTensor (argExpr x) (argExpr y)
-  Just (ReduceAddRatTensor, [x]) -> VReduceAddRatTensor (argExpr x)
-  Just (ReduceMulRatTensor, [x]) -> VReduceMulRatTensor (argExpr x)
-  Just (ReduceMinRatTensor, [x]) -> VReduceMinRatTensor (argExpr x)
-  Just (ReduceMaxRatTensor, [x]) -> VReduceMaxRatTensor (argExpr x)
-  Just (SearchRatTensor, [reduce, lower, upper, fn]) -> VSearchRatTensor (argExpr reduce) (argExpr lower) (argExpr upper) (argExpr fn)
+  Just (NegRatTensor, [dims, x]) -> VNegRatTensor dims (argExpr x)
+  Just (AddRatTensor, [dims, x, y]) -> VAddRatTensor dims (argExpr x) (argExpr y)
+  Just (SubRatTensor, [dims, x, y]) -> VSubRatTensor dims (argExpr x) (argExpr y)
+  Just (MulRatTensor, [dims, x, y]) -> VMulRatTensor dims (argExpr x) (argExpr y)
+  Just (DivRatTensor, [dims, x, y]) -> VDivRatTensor dims (argExpr x) (argExpr y)
+  Just (MinRatTensor, [dims, x, y]) -> VMinRatTensor dims (argExpr x) (argExpr y)
+  Just (MaxRatTensor, [dims, x, y]) -> VMaxRatTensor dims (argExpr x) (argExpr y)
+  Just (ReduceAddRatTensor, [dims, x]) -> VReduceAddRatTensor dims (argExpr x)
+  Just (ReduceMulRatTensor, [dims, x]) -> VReduceMulRatTensor dims (argExpr x)
+  Just (ReduceMinRatTensor, [dims, x]) -> VReduceMinRatTensor dims (argExpr x)
+  Just (ReduceMaxRatTensor, [dims, x]) -> VReduceMaxRatTensor dims (argExpr x)
+  Just (SearchRatTensor, [dims, reduce, lower, upper, fn]) -> VSearchRatTensor dims (argExpr reduce) (argExpr lower) (argExpr upper) (argExpr fn)
   Nothing -> case getDimensionDataOp expr of
-    Just (ConstTensor, [x, y]) -> VConstRatTensor (argExpr x) (argExpr y)
-    Just (StackTensor n, args) -> VStackRatTensor n (fmap argExpr args)
+    Just (ConstTensor, [argExpr -> IRatElementType, x, dims]) -> VConstRatTensor (argExpr x) (argExpr dims)
+    Just (StackTensor n, (argExpr -> IRatElementType) : dims : args) -> VStackRatTensor n dims (fmap argExpr args)
     _ -> developerError "ill-typed RatTensor expression"
   _ -> developerError "ill-typed RatTensor expression"
--}
+
 --------------------------------------------------------------------------------
 -- Other