This works best when used in tandem with ~N+, since it is currently
equivalent to ~0| and does not take the actual text position into account.
However, when using relative positions, this works as intended.
This is to accommodate goals that are used for their side-effects,
when we are interested in their output.
Examples:
?- portray_clause((a :- a)).
a :-
a.
true
; false.
?- format("hello~w~n", [!]).
hello!
true
; false.
The preceding use of atom_length/2 already ensures that C has the
correct type (i.e., atom). However, its domain may still be wrong,
if its length is greater than 1.
The preceding use of atom_length/2 already ensures that C has the
correct type (i.e., atom). However, its domain may still be wrong,
if its length is greater than 1.
Pairs must be keysorted and may also contain variables as keys.
Examples:
?- group_pairs_by_key([1-a,1-b,2-c], Ps).
Ps = [1-[a,b],2-[c]].
?- group_pairs_by_key([X-a,X-b,2-c], Ps).
Ps = [X-[a,b],2-[c]].
At the moment, library(format) seems to be a fitting place.
In the eventual library organization, portray_clause/1 and
related predicates may be moved to their own dedicated library.
library(clpz) implements declarative integer arithmetic.
The most important predicates for reasoning about integers are:
(#=)/2 equality
(#\=)/2 disequality
(#<)/2 less than
(#>)/2 greater than
(#=<)/2 less than or equal to
(#>=)/2 greater than or equal to
In addition, the library provides several global constraints, such as
all_distinct/1 and global_cardinality/2, and reification predicates
that reflect the truth values of constraints into integer variables.
Enumeration predicates such label/1 and labeling/2 can be used to
search for solutions over finite domains.
Almost all Prolog programs also reason about integers. Therefore, I
recommend to add this library to your .scryerrc configuration file so
that declarative integer arithmetic is available in all your programs.
More information about CLP(ℤ):
https://www.metalevel.at/prolog/clpz
Enjoy!
This library provides the nonterminal format_//2 to describe
formatted strings. format/2 is provided for impure output.
Usage:
======
phrase(format_(FormatString, Arguments), Ls)
format_//2 describes a list of characters Ls that are formatted
according to FormatString. FormatString is a string (i.e.,
a list of characters) that specifies the layout of Ls.
The characters in FormatString are used literally, except
for the following tokens with special meaning:
~w use the next available argument from Arguments here,
which must be atomic (a current limitation)
~f use the next argument here, a floating point number
~Nf where N is an integer: format the float argument
using N digits after the decimal point
~s use the next argument here, which must be a string
~N| where N is an integer: place a tab stop at text column N
~N+ where N is an integer: place a tab stop N characters
after the previous tab stop (or start of line)
~t distribute spaces evenly between the two closest tabstops
~`Ct like ~t, use character C instead of spaces to fill the space
~n newline
~~ the literal ~
The predicate format/2 is like format_//2, except that it outputs
the text on the terminal instead of describing it declaratively.
If at all possible, format_//2 should be used, to stress pure parts
that enable easy testing etc. If necessary, you can emit the list Ls
with maplist(write, Ls).
The entire library only works if the Prolog flag double_quotes
is set to chars, the default value in Scryer Prolog. This should
also stay that way, to encourage a sensible environment.
Example:
?- phrase(format_("~s~n~`.t~w!~12|", ["hello",there]), Cs).
%@ Cs = [h,e,l,l,o,'\n','.','.','.','.','.','.',t,h,e,r,e,!] ;
%@ false.
library(clpb) provides CLP(B), Constraint Logic Programming over
Boolean variables. It is a SAT solver that seamlessly integrates into
Prolog in the sense that logic variables are used to state constraints
and report solutions. This library can be used to model and solve many
combinatorial problems such as verification, allocation and covering
tasks.
CLP(B) is an instance of the general CLP(X) scheme, extending logic
programming with reasoning over specialised domains.
The implementation is based on reduced and ordered Binary Decision
Diagrams (BDDs).
Usage examples of this library are available in a public git
repository:
https://github.com/triska/clpb
For more information, benchmarks and publications visit:
https://www.metalevel.at/clpb/
The interface of this library is consciously kept compatible with the
CLP(B) solver of SICStus Prolog, which served as the main inspiration
of this library. Many thanks to Mats Carlsson for his elegant example!
It is my hope that library(clpb) will allow a port of cTI, and —
eventually — of Ulrich Neumerkel's GUPU to Scryer Prolog.
Boolean expressions
===================
A Boolean expression is one of:
0 false
1 true
variable unknown truth value
atom universally quantified variable
~ Expr logical NOT
Expr + Expr logical OR
Expr * Expr logical AND
Expr # Expr exclusive OR
Var ^ Expr existential quantification
Expr =:= Expr equality
Expr =\= Expr disequality (same as #)
Expr =< Expr less or equal (implication)
Expr >= Expr greater or equal
Expr < Expr less than
Expr > Expr greater than
card(Is,Exprs) see below
+(Exprs) see below
*(Exprs) see below
where Expr again denotes a Boolean expression.
The Boolean expression card(Is,Exprs) is true iff the number of true
expressions in the list Exprs is a member of the list Is of
integers and integer ranges of the form From-To.
+(Exprs) and *(Exprs) denote, respectively, the disjunction and
conjunction of all elements in the list Exprs of Boolean
expressions.
Atoms denote parametric values that are universally quantified. All
universal quantifiers appear implicitly in front of the entire
expression. In residual goals, universally quantified variables always
appear on the right-hand side of equations. Therefore, they can be
used to express functional dependencies on input variables.
Interface predicates
====================
The most frequently used CLP(B) predicates are:
* sat(+Expr)
True iff the Boolean expression Expr is satisfiable.
* taut(+Expr, -T)
If Expr is a tautology with respect to the posted constraints, succeeds
with T = 1. If Expr cannot be satisfied, succeeds with T = 0.
Otherwise, it fails.
* labeling(+Vs)
Assigns truth values to the variables Vs such that all constraints
are satisfied.
The unification of a CLP(B) variable X with a term T is equivalent
to posting the constraint sat(X=:=T).
Examples
========
Here is an example session with a few queries and their answers:
?- use_module(library(clpb)).
true.
?- sat(X*Y).
X = Y, Y = 1.
?- sat(X * ~X).
false.
?- taut(X * ~X, T).
T = 0,
sat(X=:=X).
?- sat(X^Y^(X+Y)).
sat(X=:=X),
sat(Y=:=Y).
?- sat(X*Y + X*Z), labeling([X,Y,Z]).
X = Z, Z = 1, Y = 0 ;
X = Y, Y = 1, Z = 0 ;
X = Y, Y = Z, Z = 1.
?- sat(X =< Y), sat(Y =< Z), taut(X =< Z, T).
T = 1,
sat(X=:=X*Y),
sat(Y=:=Y*Z).
?- sat(1#X#a#b).
sat(X=:=a#b).
The pending residual goals constrain remaining variables to Boolean
expressions and are declaratively equivalent to the original query.
The last example illustrates that when applicable, remaining variables
are expressed as functions of universally quantified variables.
Obtaining BDDs
==============
By default, CLP(B) residual goals appear in (approximately) algebraic
normal form (ANF). This projection is often computationally expensive.
Assert the fact clpb:clpb_residuals(bdd) to see the BDD representation
of all constraints. This results in faster projection to residual
goals, and is also useful for learning more about BDDs.
For example:
?- asserta(clpb:clpb_residuals(bdd)).
true.
?- sat(X#Y).
node(3)- (v(X, 0)->node(2);node(1)),
node(1)- (v(Y, 1)->true;false),
node(2)- (v(Y, 1)->false;true).
Note that this representation cannot be pasted back on the toplevel,
and its details are subject to change. Use copy_term/3 to obtain
such answers as Prolog terms.
The variable order of the BDD is determined by the order in which the
variables first appear in constraints. To obtain different orders,
you can for example use:
?- sat(+[1,Y,X]), sat(X#Y).
node(3)- (v(Y, 0)->node(2);node(1)),
node(1)- (v(X, 1)->true;false),
node(2)- (v(X, 1)->false;true).
Monotonic CLP(B)
================
In the default execution mode, CLP(B) constraints are not monotonic.
This means that adding constraints can yield new solutions. For
example:
?- sat(X=:=1), X = 1+0.
false.
?- X = 1+0, sat(X=:=1), X = 1+0.
X = 1+0.
This behaviour is highly problematic from a logical point of view, and
it may render declarative debugging techniques inapplicable (see
https://www.metalevel.at/prolog/debugging for more information).
Assert the fact clpb:monotonic to make CLP(B) monotonic. If this
mode is enabled, then you must wrap CLP(B) variables with the functor
v/1. For example:
?- asserta(clpb:monotonic).
true.
?- sat(v(X)=:=1#1).
X = 0.
Enjoy!
Strictly speaking, type is currently not a type, so a domain error is
appropriate if Type is not a valid type. However, there are also other
cases where new types have been introduced in the past, and this
seems a good candidate for a new type. Let us hence use a type error.
Example:
?- can_be(listi, [a,b|Ls]).
%@ ERROR: Type error: `type' expected, found `listi' (an atom)
Markus Triska