solve.pl -- The sCASP solver

 solve(:Goals, +StackIn, -StackOut, -Model)

Solve the list of sub-goals Goal where StackIn is the list of goals already visited and returns in StackOut the list of goals visited to prove the sub-goals and in Model the model that supports the sub-goals.

 check_goal(+Goal, +Module, +Parents, +ProvedIn, -ProvedOut, +StackIn, -StackOut, -Model)[private]

Call check_CHS/3 to check the sub-goal Goal against the list of goals already visited StackIn to determine if it is a coinductive success, a coinductive failure, an already proved sub-goal, or if it has to be evaluated.

Arguments:

StackOut

- is updated by prepending one or more elements to StackIn. [], chs(Goal) Proved by co-induction [], proved(Goal) Proved in a completed subtree From solve_goal/5 Continued execution

 dynamic_consistency_check(+Goal, +Module, +StackIn) is semidet[private]

Check that the resulting literal is consistent with the nmr.

 solve_goal(+Goal, +Module, +Parents, +ProvedIn, -ProvedOut, +StackIn, -StackOut, -Model)[private]

Solve a simple sub-goal Goal where StackIn is the list of goals already visited and returns in StackOut the list of goals visited to prove the sub-goals and in Model the model with support the sub-goals

 solve_goal_forall(+Forall, +Module, +Parents, +ProvedIn, -ProvedOut, +StackIn, -StackOut, -Model)[private]

Solve a sub-goal of the form forall(Var,Goal) and success if Var success in all its domain for the goal Goal. It calls solve/4

Arguments:

Forall

- is a term forall(?Var, ?Goal)

 solve_goal_table_predicate(+Goal, +Module, +Parents, +ProvedIn, -ProvedOut, +AttStackIn, -AttStackOut, -AttModel)[private]

Used to evaluate predicates under tabling. This predicates should be defined in the program using the directive _#table pred/n._

 solve_goal_predicate(+Goal, +Module, +Parents, +ProvedIn, -ProvedOut, +StackIn, -StackOut, -Model)[private]

Used to evaluate a user predicate

 solve_goal_builtin(+Goal, -Model)[private]

Used to evaluate builtin predicates predicate

 exec_findall(+Findall, +Module, +ProvedIn, -ProvedOut, +StackIn, -StackOut, -Model)[private]

 check_CHS(+Goal, +Module, +Parents, +ProvedIn, +StackIn, -Result) is det[private]

Checks the StackIn and returns in Result if the goal Goal is a coinductive success, a coinductive failure or an already proved goal. Otherwise it is constraint against its negation atoms already visited.

 neg_in_stack(+Goal, +Parents, +Proved) is semidet[private]

True when the nagation of Goal is in Stack. If so we have a coinductive failure. Check on variants which requires tabling for proper results.

 ground_neg_in_stack(++Goal, +Parents, +Proved) is det[private]

Propagate disequality constraints of Goal through matching goals on the stack.

 constrained_neg_in_stack(+Goal, +Parents, +Proved) is det[private]

Propagate the fact that we accept Goal into all other accepted goals in the stack.

 proved_in_stack(+Goal, +Proved) is semidet[private]

True when Goal appears in one of the finished branches of the proof tree, i.e., it appears in Stack, but not as direct parent.

 check_parents(+Goal, +Parents, -Type) is semidet[private]

Type is the coinductive result. This is even if we have an even loop through negation or a simple positive match.

 stack_parents(+Stack, -Parents) is det[private]

Get the direct callers from Stack. Stack contains both previous proved stacks as well as the current list of parents.

 stack_proved(Stack, Proved:assoc) is det[private]

True when Proved is an assoc holding all goals that have already been proved in Stack. This excludes the direct parents of in the stack, i.e. only adds goals from already completed branches.

The code is based on the old proved_in_stack/2. Effectively this extracts the other half than stack_parents/2, so possibly we should sync the code with that.

 solve_c_forall(+Forall, +Module, +Parents, +ProvedIn, -ProvedOut, +StackIn, -StackOut, -Model)[private]

Solve a sub-goal of the form c_forall(Vars,Goal) and succeeds if the goal Goal succeeds covering the domain of all the vars in the list of vars `Vars. It calls solve/4

Arguments:

Forall

- is a term forall(Var, Goal).

To be done

- Improve the efficiency by removing redundant justifications w.o. losing solutions.

 solve_var_forall_(+Goal, +Module, +Parents, +ProvedIn, -ProvedOut, +Entry, +Duals, +OtherVars, +StackIn, -StackOut, -Model) is nondet[private]

Implements the forall algorithm as described in section 2.3 from "Constraint Answer Set Programming without Grounding" by Joaquin Arias et all. It works different though.

• For each step we copy the Goal, solve it and compute the instantiations created by Goal. From these instantiations we compute the duals.
• Continue until all duals are proved.

Note that the constraints on the forall variables are maintained explicitly.

 find_duals(+C_Vars, +C_Vars1, +OtherVars, -Duals)[private]

C_Vars is the list of forall variables after solve/4. C_Vars1 is a copy of this list before calling solve/4. Our task is to create a dual model from the instantiation. If subsequently we can prove the dual model to be true then we proved the forall is true. For example, if solve succeeded with [X] --> [q], it created the instantiation X=q. It we now can prove X\=q, we proved solve is true for all X.

See also

- Section 2.3 from "Constraint Answer Set Programming without Grounding" by Joaquin Arias et all.

To be done

- JW: it is not clear to me why OtherVars is needed and why it is not copied.

 dump_constraint(+C_Vars, +C_Vars1, -Dump, +Pending0, -Pending) is det[private]

Arguments:

Dump	- is a list of V1=B and V1\=B, where V1 is a variable from C_Vars1.
Pending	- is a pair of lists with variables from C_Vars and C_Vars1 that are not processed (in reverse order, why?)

 collect_vars(?Forall, ?CollectForall)[private]

Forall Vars in a list

 my_copy_term(+Var, +Term, -NewVar, -NewTerm) is det[private]

Its behaviour is similar to copy_term/2. It returns in NewTerm a copy of the term Term but it only replaces with a fresh variable NewVar the occurrences of Var

 my_diff_term(+Term, +Vars, -Others) is det[private]

Others are variables in Term that do not appear in Vars.