Pw/defaults

CHANGES.md

@@ -2,6 +2,8 @@
 
 ## Ongoing
 
+- - introduce basic support for defaults, using the
+    `variable_default(LABEL,X,DEFAULT_EXPR,COND)` declarations.
 - - type equality and inequality between values of incompatible types to return
     `bool`
 - - introduce warning `correction/1`

design.md

@@ -0,0 +1,4 @@
+- domain and define are mutually exclusive, leads to non-elaboration tolerant
+  knowledge bases
+- missing values leads to bad
+- domain plus define leads to bad

src/constraint_handler/data/0_default_arguments/README.md

@@ -5,8 +5,9 @@ ensure/1. ensure/2.
 evaluate/2. evaluate/3.
 variable_declare/2. variable_declare/3.
 variable_declareOptional/1. variable_declareOptional/2.
-variable_domain/2. variable_domain/3.
 variable_define/2. variable_define/3.
+variable_domain/2. variable_domain/3.
+variable_default/2. variable_default/3. variable_default/4.
 multimap_declare/1. multimap_declare/2.
 multimap_assign/3. multimap_assign/4.
 set_declare/1. set_declare/2.
@@ -35,9 +36,9 @@ _passed(defaultArgs,LBL,ensure/1).
 _passed(defaultArgs,LBL,evaluate/2).
 _passed(defaultArgs,LBL,variable_declare/2).
 _passed(defaultArgs,LBL,variable_declareOptional/1).
-_passed(defaultArgs,LBL,variable_domain/2).
 _passed(defaultArgs,LBL,variable_define/2).
-_passed(defaultArgs,LBL,multimap_declare/1).
+_passed(defaultArgs,LBL,variable_default/3).
+_passed(defaultArgs,LBL,variable_domain/2).
 _passed(defaultArgs,LBL,multimap_assign/3).
 _passed(defaultArgs,LBL,set_declare/1).
 _passed(defaultArgs,LBL,set_assign/2).

src/constraint_handler/data/0_default_arguments/default_arguments.lp

@@ -22,6 +22,9 @@ _passed(defaultArgs,LBL,evaluate(OP,ARGS)) :- evaluate(LBL,OP,ARGS).
 #defined variable_define/3.
 #defined variable_domain/2.
 #defined variable_domain/3.
+#defined variable_default/2.
+#defined variable_default/3.
+#defined variable_default/4.
 
 _defaultArgs_variableDeclared(X) :- variable_declare(X,E).
 _defaultArgs_variableDeclared(X) :- variable_declare(LBL,X,E).
@@ -33,6 +36,9 @@ _passed(defaultArgs,LBL,variable_declareOptional(X)) :- variable_declareOptional
 _passed(defaultArgs,_label_anonymous,variable_domain(X,E)) :- variable_domain(X,E), not _defaultArgs_variableDeclared(X).
 _passed(defaultArgs,LBL,variable_domain(X,E)) :- variable_domain(X,E), _passed(defaultArgs,LBL,variable_declare(X,D)).
 _passed(defaultArgs,LBL,variable_domain(X,E)) :- variable_domain(LBL,X,E).
+_passed(defaultArgs,_label_anonymous,variable_default(X,D,val(bool,true))) :- variable_default(X,D).
+_passed(defaultArgs,_label_anonymous,variable_default(X,D,C)) :- variable_default(X,D,C).
+_passed(defaultArgs,LBL,variable_default(X,D,C)) :- variable_default(LBL,X,D,C).
 
 _passed(defaultArgs,_label_anonymous,variable_define(X,E)) :- variable_define(X,E).
 _passed(defaultArgs,LBL,variable_define(X,E)) :- variable_define(LBL,X,E).

src/constraint_handler/data/2_sugar/README.md

@@ -3,8 +3,8 @@
 _passed(defaultArgs,LBL,bool_evaluate/1).
 _passed(defaultArgs,LBL,ensure/1).
 _passed(defaultArgs,LBL,evaluate/2).
-_passed(defaultArgs,LBL,variable_define/2).
 _passed(defaultArgs,LBL,variable_declare/2).
+_passed(defaultArgs,LBL,variable_define/2).
 _passed(defaultArgs,LBL,variable_domain/2).
 _passed(defaultArgs,LBL,variable_declareOptional/1).
 _passed(defaultArgs,LBL,multimap_declare/1).
@@ -30,6 +30,7 @@ _passed(sugar,LBL,ensure/1).
 _passed(sugar,LBL,evaluate/2).
 _passed(sugar,LBL,variable_declare/2).
 _passed(sugar,LBL,variable_define/2).
+_passed(sugar,LBL,variable_default/3).
 _passed(sugar,LBL,variable_domain/2).
 _passed(sugar,LBL,variable_interface/1).
 _passed(sugar,LBL,multimap_assign/3).

src/constraint_handler/data/2_sugar/sugar.lp

@@ -15,6 +15,7 @@ _passed(sugar,LBL,variable_domain(X,E)) :- _passed(defaultArgs,LBL,variable_decl
 _passed(sugar,LBL,variable_domain(X,val(bool,(false;true)))) :- _passed(defaultArgs,LBL,variable_declare(X,boolDomain)).
 _passed(sugar,LBL,variable_domain(X,val(none,none))) :- _passed(defaultArgs,LBL,variable_declareOptional(X)).
 _passed(sugar,LBL,variable_domain(X,E)) :- _passed(defaultArgs,LBL,variable_domain(X,E)).
+_passed(sugar,LBL,variable_default(X,D,C)) :- _passed(defaultArgs,LBL,variable_default(X,D,C)).
 _expression(sugar,val(bool,(false;true))) :- _passed(defaultArgs,LBL,variable_declare(X,boolDomain)).
 _expression(sugar,val(none,none)) :- _passed(defaultArgs,LBL,variable_declareOptional(X)).
 
@@ -62,6 +63,7 @@ _passed(sugar,LBL,warning_ignore(KIND)) :- _passed(defaultArgs,LBL,warning_ignor
 _variable_execution_outputVar(X) :- _passed(ssa,LBL,variable_declare(X,DOM)), X=execution_output(PRG,VAR).
 _variable_internal(X) :- _passed(ssa,LBL,variable_declare(X,DOM)), not _variable_execution_outputVar(X).
 _passed(sugar,LBL,variable_interface(X)) :- _passed(sugar,LBL,variable_declare(X,DOM)), not _variable_internal(X).
+_passed(sugar,LBL,variable_interface(X)) :- _passed(sugar,LBL,variable_default(X,VAL,COND)), not _variable_internal(X).
 
 %%%%%% internal declarations
 _passed(internal_declaration,LBL,variable_declare(X,DOM)) :- _passed(ssa,LBL,variable_declare(X,DOM)), _variable_internal(X).

src/constraint_handler/data/3_domain/domain.lp

@@ -16,6 +16,7 @@ _expression_domain(bad,bad).
 _expression_domain(EXPR,val(T,V)) :- _expression(sugar,EXPR), EXPR=val(T,V).
 _expression_domain(EXPR,V) :- _expression(sugar,EXPR), EXPR=variable(X), _passed(sugar,LBL,variable_define(X,E2)), _expression_domain(E2,V).
 _expression_domain(EXPR,V) :- _expression(sugar,EXPR), EXPR=variable(X), _passed(sugar,LBL,variable_domain(X,E2)), _expression_domain(E2,V).
+_expression_domain(EXPR,V) :- _expression(sugar,EXPR), EXPR=variable(X), _passed(sugar,LBL,variable_default(X,E2,C)), _expression_domain(E2,V).
 
 _expression_tupleDomainAux(EXPR,N,()) :- _expression(sugar,EXPR), _expression_tupleLength(sugar,EXPR,N), #false.
 _expression_tupleDomainAux(EXPR,IDX,(V,L)) :- _expression_tupleDomainAux(EXPR,IDX+1,L), _expression_tupleIndex(sugar,EXPR,IDX,E), _expression_domain(E,V).

src/constraint_handler/data/4_solve/defaults.lp

@@ -0,0 +1,33 @@
+#defined default_mode/1.
+
+_default_possibleMode(basic;define;depends;none).
+_default_modeProvided :- default_mode(MODE), _default_possibleMode(MODE).
+_default_mode(MODE) :- default_mode(MODE), _default_possibleMode(MODE).
+_default_mode(define) :- not _default_modeProvided.
+
+%TODO: rework phase integration and value introduction to be compatible with the propagator engine
+
+_se_value(variable(X),V) :- _passed(solve,LBL,variable_default(X,D,C)), _se_value(D,V), not -_default_apply(X,D,C), _se_value(C,val(bool,true)).
+
+%%%%%% mode basic
+-_default_apply(X,D,C) :- _passed(solve,LBL,variable_default(X,D,C)),
+                 _se_value(D,V), _se_value(variable(X),V'), V != V',
+                 _default_mode(basic).
+
+%%%%%% mode define
+-_default_apply(X,D,C) :- _passed(solve,LBL,variable_default(X,D,C)), _passed(solve,LBL',variable_define(X,E)),
+                 _se_value(D,V), _se_value(E,V'), V != V',
+                 _default_mode(define).
+
+%%%%%% mode depends
+% Collect all variables that occur in ensure declarations.
+_default_ensureVariable(E,X) :- _passed(solve,LBL,ensure(E)), _default_mode(depends), X=@pythonExpressionVariable(E).
+_default_dependVariable(E,X) :- _default_ensureVariable(E,X), _passed(solve,LBL,variable_default(X,D,C)).
+
+_default_depends(X,X) :- _default_dependVariable(E,X).
+_default_depends(X,Y) :- _default_dependVariable(E,X), _default_ensureVariable(E,Y), X != Y.
+
+-_default_apply(X,D,C) :- _passed(solve,LBL,variable_default(X,D,C)), _passed(solve,LBL',variable_define(X',E')),
+                 _default_depends(X,X'),
+                 _se_value(D,V), _se_value(variable(X),V'), V != V',
+                 _default_mode(depends).

src/constraint_handler/data/4_solve/solve.lp

@@ -6,6 +6,7 @@ _passed(presolve,LBL,DECL) :- _passed(correction(REASON,add),LBL,DECL).
 _variable_involve(presolve,LBL,X,DECL) :- _passed(presolve,LBL,DECL), DECL=variable_declare(X,D).
 _variable_involve(presolve,LBL,X,DECL) :- _passed(presolve,LBL,DECL), DECL=variable_define(X,D).
 _variable_involve(presolve,LBL,X,DECL) :- _passed(presolve,LBL,DECL), DECL=variable_domain(X,D).
+_variable_involve(presolve,LBL,X,DECL) :- _passed(presolve,LBL,DECL), DECL=variable_default(X,V,COND).
 _variable_involve(presolve,LBL,X,DECL) :- _passed(presolve,LBL,DECL), DECL=set_assign(X,D).
 _variable_involve(presolve,LBL,X,DECL) :- _passed(presolve,LBL,DECL), DECL=set_baseDomain(X,D).
 _variable_involve(presolve,LBL,X,DECL) :- _passed(presolve,LBL,DECL), DECL=multimap_assign(X,D,E).

src/constraint_handler/data/correction.lp

@@ -24,6 +24,9 @@ _correction_proposed(PHASE,LBL,variable_define(X,E),variable_define(X,NE)) :-
 _correction_proposed(PHASE,LBL,variable_domain(X,E),variable_domain(X,NE)) :-
   _passed(sugar,LBL,variable_domain(X,E)),
   _correction_expressionOutput(PHASE,E,NE).
+_correction_proposed(PHASE,LBL,variable_default(X,E,C),variable_default(X,NE,NC)) :-
+  _passed(sugar,LBL,variable_default(X,E,C)),
+  _correction_expressionOutput(PHASE,E,NE), _correction_expressionOutput(PHASE,C,NC).
 _correction_proposed(PHASE,LBL,set_assign(X,E),set_assign(X,NE)) :-
   _passed(sugar,LBL,set_assign(X,E)),
   _correction_expressionOutput(PHASE,E,NE).

src/constraint_handler/data/expression.lp

@@ -4,6 +4,7 @@ _expression(PHASE,LBL,DECL,operation(OP,ARGS)) :- _passed(PHASE,LBL,DECL), DECL=
 
 _expression(PHASE,LBL,DECL,E) :- _passed(PHASE,LBL,DECL), DECL=variable_define(X,E).
 _expression(PHASE,LBL,DECL,E) :- _passed(PHASE,LBL,DECL), DECL=variable_domain(X,E).
+_expression(PHASE,LBL,DECL,(D;C)) :- _passed(PHASE,LBL,DECL), DECL=variable_default(X,D,C).
 _expression(PHASE,LBL,DECL,E) :- _passed(PHASE,LBL,DECL), DECL=set_assign(X,E).
 _expression(PHASE,LBL,DECL,E) :- _passed(PHASE,LBL,DECL), DECL=set_baseDomain(X,E).
 _expression(PHASE,LBL,DECL,(K;B)) :- _passed(PHASE,LBL,DECL), DECL=multimap_assign(X,K,B).

src/constraint_handler/main.py

@@ -97,6 +97,7 @@
 module_4_solve = (
     [
         "4_solve/engine",
+        "4_solve/defaults",
         "4_solve/finiteDomain",
         "4_solve/optimize",
         "4_solve/preference",

tests/correctness/default/basic_true.expected.all

@@ -0,0 +1,4 @@
+value(x,val(int,4))
+value(y,val(int,4))
+value(z,val(int,4))
+value(t,val(int,4))

tests/correctness/default/basic_true.lp

@@ -0,0 +1,5 @@
+variable_define(x,val(int,4)).
+
+variable_default(y,variable(x),val(bool,true)).
+variable_default(z,variable(x)).
+variable_default(some_label,t,variable(x),val(bool,true)).

tests/correctness/default/define/condition.expected.any

@@ -0,0 +1,4 @@
+evaluated(add,(variable(frontwheel),(variable(backwheel),())),val(int,21))
+evaluated(add,(variable(frontwheel),(variable(backwheel),())),val(int,12))
+evaluated(add,(variable(frontwheel),(variable(backwheel),())),val(int,22))
+evaluated(add,(variable(frontwheel),(variable(backwheel),())),val(int,32))

tests/correctness/default/define/condition.expected.none

@@ -0,0 +1,2 @@
+evaluated(add,(variable(frontwheel),(variable(backwheel),())),val(int,11))
+evaluated(add,(variable(frontwheel),(variable(backwheel),())),val(int,31))

tests/correctness/default/define/condition.lp

@@ -0,0 +1,13 @@
+% Variant: frontwheel default condition is expression-based.
+% The default for frontwheel is active only when backwheel == 1.
+default_mode(define).
+
+variable_domain(frontwheel,val(int,10)).
+variable_domain(frontwheel,val(int,20)).
+variable_domain(frontwheel,val(int,30)).
+
+variable_default(frontwheel,val(int,20),operation(eq,(variable(backwheel),(val(int,1),())))).
+
+evaluate(add,(variable(frontwheel),(variable(backwheel),()))).
+
+1 { variable_define(backwheel,val(int,(1;2))) } 1.

tests/correctness/default/define/disabled.expected.any

@@ -0,0 +1,3 @@
+value(frontwheel,val(int,20))
+value(frontwheel,val(int,21))
+value(frontwheel,val(int,22))

tests/correctness/default/define/disabled.lp

@@ -0,0 +1,8 @@
+% Variant: frontwheel default is disabled by a false condition.
+default_mode(define).
+
+variable_domain(frontwheel,val(int,20)).
+variable_domain(frontwheel,val(int,21)).
+variable_domain(frontwheel,val(int,22)).
+
+variable_default(frontwheel,val(int,21),val(bool,false)).

tests/correctness/default/define/no_domain.expected.all

@@ -0,0 +1 @@
+value(frontwheel,val(int,20))

tests/correctness/default/define/no_domain.lp

@@ -0,0 +1,5 @@
+% Variant: frontwheel default condition is expression-based.
+default_mode(define).
+
+variable_define(backwheel,val(int,20)).
+variable_default(frontwheel,variable(backwheel),val(bool,true)).

tests/correctness/default/define/single.expected.stats

@@ -0,0 +1 @@
+models=0

tests/correctness/default/define/single.lp

@@ -0,0 +1,12 @@
+% Variant: single default on frontwheel that is coupled to backwheel via ensure.
+default_mode(define).
+
+variable_domain(frontwheel,val(int,20)).
+variable_domain(frontwheel,val(int,21)).
+variable_domain(frontwheel,val(int,22)).
+
+variable_default(frontwheel,val(int,21),val(bool,true)).
+
+variable_define(backwheel,val(int,20)).
+
+ensure(operation(eq,(variable(frontwheel),(variable(backwheel),())))).

tests/correctness/default/define/with_domain.expected.stats

@@ -0,0 +1 @@
+models=0

tests/correctness/default/define/with_domain.lp

@@ -0,0 +1,13 @@
+% Variant: default value for backwheel matches its explicit definition.
+default_mode(define).
+
+variable_domain(frontwheel,val(int,20)).
+variable_domain(frontwheel,val(int,21)).
+variable_domain(frontwheel,val(int,22)).
+
+variable_default(frontwheel,val(int,21),val(bool,true)).
+variable_default(backwheel,val(int,20),val(bool,true)).
+
+variable_define(backwheel,val(int,20)).
+
+ensure(operation(eq,(variable(frontwheel),(variable(backwheel),())))).

tests/correctness/default/depends/condition.expected.any

@@ -0,0 +1,4 @@
+evaluated(add,(variable(frontwheel),(variable(backwheel),())),val(int,21))
+evaluated(add,(variable(frontwheel),(variable(backwheel),())),val(int,12))
+evaluated(add,(variable(frontwheel),(variable(backwheel),())),val(int,22))
+evaluated(add,(variable(frontwheel),(variable(backwheel),())),val(int,32))

tests/correctness/default/depends/condition.expected.none

@@ -0,0 +1,2 @@
+evaluated(add,(variable(frontwheel),(variable(backwheel),())),val(int,11))
+evaluated(add,(variable(frontwheel),(variable(backwheel),())),val(int,31))

tests/correctness/default/depends/condition.lp

@@ -0,0 +1,13 @@
+% Variant: frontwheel default condition is expression-based.
+% The default for frontwheel is active only when backwheel == 1.
+default_mode(depends).
+
+variable_domain(frontwheel,val(int,10)).
+variable_domain(frontwheel,val(int,20)).
+variable_domain(frontwheel,val(int,30)).
+
+variable_default(frontwheel,val(int,20),operation(eq,(variable(backwheel),(val(int,1),())))).
+
+evaluate(add,(variable(frontwheel),(variable(backwheel),()))).
+
+1 { variable_define(backwheel,val(int,(1;2))) } 1.

tests/correctness/default/depends/disabled.expected.any

@@ -0,0 +1,3 @@
+value(frontwheel,val(int,20))
+value(frontwheel,val(int,21))
+value(frontwheel,val(int,22))

tests/correctness/default/depends/disabled.lp

@@ -0,0 +1,8 @@
+% Variant: frontwheel default is disabled by a false condition.
+default_mode(define).
+
+variable_domain(frontwheel,val(int,20)).
+variable_domain(frontwheel,val(int,21)).
+variable_domain(frontwheel,val(int,22)).
+
+variable_default(frontwheel,val(int,21),val(bool,false)).

tests/correctness/default/depends/no_domain.expected.all

@@ -0,0 +1 @@
+value(frontwheel,val(int,20))

tests/correctness/default/depends/no_domain.lp

@@ -0,0 +1,5 @@
+% Variant: frontwheel default condition is expression-based.
+default_mode(depends).
+
+variable_define(backwheel,val(int,20)).
+variable_default(frontwheel,variable(backwheel),val(bool,true)).

tests/correctness/default/depends/single.expected.all

@@ -0,0 +1 @@
+value(frontwheel,val(int,20))

tests/correctness/default/depends/single.expected.none

@@ -0,0 +1,2 @@
+value(frontwheel,val(int,21))
+value(frontwheel,val(int,22))

tests/correctness/default/depends/single.lp

@@ -0,0 +1,12 @@
+% Variant: single default on frontwheel that is coupled to backwheel via ensure.
+default_mode(depends).
+
+variable_domain(frontwheel,val(int,20)).
+variable_domain(frontwheel,val(int,21)).
+variable_domain(frontwheel,val(int,22)).
+
+variable_default(frontwheel,val(int,21),val(bool,true)).
+
+ensure(operation(eq,(variable(frontwheel),(variable(backwheel),())))).
+
+variable_define(backwheel,val(int,20)).

tests/correctness/default/depends/with_domain.expected.all

@@ -0,0 +1 @@
+value(frontwheel,val(int,20))

tests/correctness/default/depends/with_domain.expected.none

@@ -0,0 +1,2 @@
+value(frontwheel,val(int,21))
+value(frontwheel,val(int,22))

tests/correctness/default/depends/with_domain.lp

@@ -0,0 +1,13 @@
+% Variant: default value for backwheel matches its explicit definition.
+default_mode(depends).
+
+variable_domain(frontwheel,val(int,20)).
+variable_domain(frontwheel,val(int,21)).
+variable_domain(frontwheel,val(int,22)).
+
+variable_default(frontwheel,val(int,21),val(bool,true)).
+variable_default(backwheel,val(int,20),val(bool,true)).
+
+variable_define(backwheel,val(int,20)).
+
+ensure(operation(eq,(variable(frontwheel),(variable(backwheel),())))).

tests/correctness/default/test.lp

@@ -0,0 +1,12 @@
+default_mode(depends).
+
+variable_domain(x,val(int,4)).
+variable_default(x,val(int,1),val(bool,true)).
+
+variable_define(y,val(int,4)).
+
+variable_define(z,operation(eq,(variable(x),(variable(y),())))).
+
+ensure(variable(z)).
+
+#show _se_value/2.