Version 2.5 (October 8, 2018)
=================================
+ Added a new module, named smt, for constraint solving. The module requires z3 or cvc4 as the SMT solver.
+ Allow ranges in subscripts: A[From..To] is the same as slice(A,From,To).
+ copy_term_shalow(T) = copy_term_shalow(T).
+ one bug fix in the regular constraint
+ bug fixes in the SAT encoder
+ one bug fix in big-integer arithmetic
Version 2.4 (April 15, 2018)
=================================
+ Support of the heap data structure
heap_is_empty(Heap) => heap_is_empty(Heap).
heap_pop(Heap) = heap_pop(Heap).
heap_push(Heap,Elm) => heap_push(Heap,Elm).
heap_size(Heap) = heap_size(Heap).
heap_to_list(Heap) = heap_to_list(Heap).
heap_top(Heap) = heap_top(Heap).
new_max_heap(IntOrList) = new_max_heap(IntOrList).
new_min_heap(IntOrList) = new_min_heap(IntOrList).
+ Dot-notations are treated as functions in term constructors and constraints.
Examples:
X = $f(math.pi)
R = new_rectangle(), R.x #= R.y, R.width #= R.height, R.color #= cg.red
+ Improvements on the SAT compiler for Pseudo-Boolean constraints and global constraints
+ Colors in error messages (unix only)
+ A special comparator is used in comparing arrays
+ 64-bit executable for Windows
+ Bug fixes: round, **
Version 2.3 (February 1, 2018)
=================================
+ Incorporated new SAT encodings for the following global constraints: element, regular, circuit, subcircuit, table_in, and table_notin.
+ Added a new built-in in the planner module, named best_plan_bin, which uses branch-and-bound and binary search to find a best plan.
+ The compiler unfolds higher-order calls to map/2, map/3, reduce/2, and reduce/3, so that these calls are more efficient and obey the name-resolving rules in modules.
+ Minor improvements: sort, SAT compiler, tabling, planner.
+ Bug fixes: map/1, SAT compiler.
Version 2.2 (August 10, 2017)
=================================
+ The mip module supports the same set of constraints as the sat and cp modules, including global constraints.
+ The solve/1-2 predicates in the mip module are non-deterministic, and can be used to return all solutions.
+ The sat module supports a new labeling option, named $threads(N), which, when specified, solves the generated CNF code using plingeling with N threads. The option threads is the same as $threads(8).
+ New constraint in cp, sat, and mip:
count(V,FDVars,N): V occurs in FDVars N times.
+ Significant improvements in the SAT compiler. The PicatSAT solver submitted to MiniZinc Challenge 2017 is based on this version.
+ Added the following functions into the math module:
acosh(X)
acoth(X)
acsch(X)
asech(X)
asinh(X)
atanh(X)
cosh(X)
coth(X)
csch(X)
frand(Low,High)
random(Low,High)
sech(X)
tanh(X)
sinh(X)
+ several bug fixes
Version 2.1 (March 12, 2017)
=================================
+ Extensions
count(V,L) can occur in constraint expressions.
+ Improvements
The SAT compiler performs constant propagation, which may lead to reduction in code sizes.
The preprocessor of the SAT compiler is improved so that it excludes more no-good values.
+ bug fixes
a bug in comparison of integers between -2^56..-2^28 and 2^28..2^56
a bug in the pow function that occurs when the operands are floats
a bug in the sat compiler that affects large domains
Version 2.0 (November 17, 2016)
=================================
+ Improvements in sat
New implementations of the circuit, subcircuit, and regular constraints
New and better ordering for breaking constraints into primitive ones
+ Extension of the planner module
In addition to defining the final/1 (or final/3) and action/4 predicates, users can also provide
a function, named heuristic(S), and a predicate, named sequence(P,A). The heuristic(S) function is
used by the planner to check the heuristic value before each state expansion, and the sequence/2
predicate determines the next set of actions based on the current partial plan.
+ Interface to Gurobi
The solve predicate in the mip module supports a new option, named gurobi, which instructs Picat to
use the Gurobi MIP solver. Picat uses the following command to call the Gurobi solver:
gurobi_cl ResultFile=SolFile TmpFile
where SolFile is a file for the solution, and TmpFile is a file that stores the CPLEX-format constraints.
Picat throws existence_error if the command gurobi_cl is not available.
+ Interface to GLPK
The tight interface with GLPK was removed, and a new interface that interacts with GLPK through files was
added. The solve predicate in the mip module supports a new option, named glpk, which instructs Picat to
use the GLPK MIP solver. Picat uses the following command to call the GLPK solver:
glpsol --lp -o SolFile TmpFile
where SolFile is a file for the solution, and TmpFile is a file that stores the CPLEX-format constraints.
Picat throws existence_error if the command glpsol is not available.
+ Capable of compiling programs that include big structures and big arrays (before the limit was 255).
+ Exceptions in math functions: asin(X), acos(X), X**Y, log(X), log10(X), log2(X), log(B,X)
+ Clean up exceptions.
+ zip(Lists) added into the basic module.
+ to_number(NumOrCharOrStr) added into the basic module.
+ cl_facts_table(Facts) and cl_facts_table(Facts,IndexInfo) added into the sys module.
+ New math functions added:
acot(X) = acot(X).
acsc(X) = acsc(X).
asec(X) = asec(X).
cot(X) = cot(X).
csc(X) = csc(X).
sec(X) = sec(X).
+ New command line option "--v" and "--version"
+ New command line option "-s Size" for specifying initial stack/heap size.
+ New built-in functions added to the util module: take(L,N), drop(L,N), chunks_of(L,N).
Version 1.9 (April 3, 2016)
=================================
+ Improvements in sat
more compact encodings for PB constraints and all_different.
new algorithm for breaking arithmetic constraints.
binary search for optimization.
+ Improvements in planner
binary search for optimization (best_plan and best_plan_bb).
+ New built-in functions in basic
maxint_small() = maxint_small().
minint_small() = minint_small().
+ Removal of built-ins
best_plan_downward/n in planner
Version 1.8 (February 18, 2016)
=================================
+ New built-ins
math:
pow_mod(X,Y,Z) = pow_mod(X,Y,Z). (the same as X**Y mod Z, but more efficient)
basic:
to_radix_string(Val,Base) = to_radix_string(Val,Base).
parse_radix_string(String,Base) = parse_radix_string(String,Base).
put_attr(AttrVar,Key,Val) => put_attr(AttrVar,Key,Val).
get_attr(AttrVar,Key) = get_attr(AttrVar,Key)
get_attr(AttrVar,Key,DefaultVal) = get_attr(AttrVar,Key,DefaultVal)
cp:
solve_suspended => solve_suspended.
solve_suspended(Options) => solve_suspended(Options).
+ Improvements
multiplication and mod operations on big integers
tabling for functions and single-answer predicates
+ Bug fixes
The matrix_element constraint is extended so that the matrix can be non-ground.
The missing internal predicate '$bc_clause'/1 added.
Version 1.7 (January 3, 2016)
=================================
+ New built-in functions in basic:
get_heap_map(ID)
get_global_map(ID)
get_table_map(ID)
+ Improvements of operations on global and table maps.
+ Improvements of maxof and minof.
Version 1.6 (December 13, 2015)
=================================
+ New built-ins in basic:
int(Term) => int(Term).
sorted(ListOrArray) => sorted(ListOrArray).
sorted_down(ListOrArray) => sorted_down(ListOrArray).
to_float(NumOrString) = to_float(NumOrString).
to_int(NumOrCharOrString) = to_int(NumOrCharOrString).
+ New global constraints in cp and sat:
decreasing(FDVars) => decreasing(FDVars).
decreasing_strict(FDVars) => decreasing_strict(FDVars).
increasing(FDVars) => increasing(FDVars).
increasing_strict(FDVars) => increasing_strict(FDVars).
+ Overloaded built-ins for arrays:
avg(ListOrArray)
max(ListOrArray)
min(ListOrArray)
prod(ListOrArray)
sort(ListOrArray)
sort(ListOrArray,Index)
sort_down(ListOrArray)
sort_down(ListOrArray,Index)
sort_down_remove_dups(ListOrArray)
sort_down_remove_dups(ListOrArray,Index)
sort_remove_dups(ListOrArray)
sort_remove_dups(ListOrArray,Index)
sum(ListOrArray)
+ bug fixes
to_integer(String) where String begins with a sign
f(X) = 1..X.
f(X,Y) = X++Y.
Vertion 1.5 (November 23, 2015)
=================================
+ Support nested as-patterns in rule heads.
+ New built-in functions and predicates in the basic module:
count_all(Goal) = Count
return the number of instances of Goal that are true.
new_set() = Map
return a set, which is a map where all keys are mapped to the atom not_a_value.
put(Map,Key)
the same as put(Map,Key,not_a_value).
+ Bug fixes
Version 1.4 (September 28, 2015)
=================================
+ Integers in the range from -2^56-1 to 2^56-1 are represented as one word on 64-bit platforms.
+ The default lower and upper bounds of domains are, respectively, -2^56-1 and 2^56-1 on 64-bit platforms.
+ An improved SAT encoding for entailment constraints.
+ An improvement in the propagator for the multiplication constraint.
+ Arrays can be iterated over by foreach loops without being converted into lists.
+ A bug fix in tabling.
+ Output logs from GLPK are suppressed.
+ The "lib" directory contains more library modules, including:
fzn_picat_cp.pi: A FlatZinc interpreter in Picat using the cp module.
fzn_picat_sat.pi: A FlatZinc interpreter in Picat using the sat module.
gen_indent_all.pi: generates command lines for indenting C files using Stan Warford's function.
json.pi: a JSON encoder and decoder by Mike Bionchik.
sugar2pi.pi: A converter from Sugar's CSP format to Picat.
sugar2pi.pi: A converter from Sugar's CSP format to Picat.
xcsp2pi.pi: A converter from XCSP to Picat.
Version 1.3 (August 1, 2015)
=================================
+ The sort functions are improved.
+ A bug in the parser that caused errors in parsing unary operators as atoms is fixed.
+ An improvement on the SAT encoding of the circuit constraint.
+ An improvement on the min(L) and max(L) constraint expressions.
Version 1.2 (June 12, 2015)
=================================
+ Following predicates in the planner module are made polymorphic:
plan/3: plan(S,Limit,Plan) and plan(S,Plan,PlanCost)
best_plan/3: best_plan(S,Limit,Plan) and best_plan(S,Plan,PlanCost)
best_plan_nondet/3: best_plan_nondet(S,Limit,Plan) and best_plan_nondet(S,Plan,PlanCost)
best_plan_upward/3: best_plan_upward(S,Limit,Plan) and best_plan_upward(S,Plan,PlanCost)
plan_unbounded/3: plan_unbounded(S,Limit,Plan) and plan_unbounded(S,Plan,PlanCost)
+ 'best_plan_upward' is renamed to 'best_plan_bb' (best_plan_upward is deprecated now).
+ New predicates added.
sort(List,KeyIndex)
sort_remove_dups(List,KeyIndex)
sort_down(List,KeyIndex)
sort_down_remove_dups(List,KeyIndex)
+ The functions min and max are modified in the following way:
min(X,Y) and max(X,Y): X and Y can be any terms
min(L) and max(L): L is a list of any terms
+ The compiler compiles min([Elm : ...]) and max([Elm : ...]) so that the generated code
computes the aggregate but does not create a list.
+ The zip functions don't require argument lists to have the same length.
+ For the foreach iterator {E1,E2} in zip(L1,L2), the compiler generates code to avoid creating a zipped list.
+ Reimplement the built-ins in the os module to avoid creating temporary symbols.
+ Bug fixes in find_first_of/2 and find_last_of/2 in the util module.
Version 1.1 (May 11, 2015)
=================================
+ A change in the GC policy.
+ A bug fix in the global table map, which can affect some planning programs.
+ A bug fix in the 'dump' option in solve/2.
+ Improvements in the SAT compiler.
+ An improved implementation of the function len(_) (also length(_)).
Version 1.0 (April 3, 2015)
=================================
+ Added an external language interface with C. Users have to download the C source code in order to use this interface.
+ An improvement on the compiler enables it to compile huge rules (rules that contain tens of thousands subgoals and variables).
+ Added array comprehensions. An array comprehension {E : Iterator, ...} is the same as to_array([E : Iterator, ...]).
+ Added a new built-in function: insert_ordered_down(OrderedList,Elm).
+ New built-ins best_plan_nondet/2-4 added into the planner module, which allows returning multiple plans through backtracking.
+ Added the module 'datetime'. It only has three functions:
current_datetime(),
current_date(),
current_day(), and
current_time().
+ Added a new command option '-g InitGoal', which allows Picat to execute a specified goal rather than the default main/0 or main/1.
+ Redundant commas and semicolons in if-then-else and loops give warnings rather than errors.
+ The exception evaluation_error(undefined) is changed to evaluation_error(undefined,error_value).
+ The exception evaluation_error(zero_divisor) is changed to zero_divisor.
+ Improvements on the SAT compiler.
+ New global constraints added into cp and sat:
matrix_element(M,I,J,V),
scalar_product(A, X, Product),
scalar_product(A, X, Rel, Product),
all_different_except_0(Xs),
exactly(N, X, V),
at_most(N,X,V), and
at_least(N,X,V).
+ The command "picat File" returns 1 if a run-time or syntax error occurs whiling executing File. It returns 0 if no error occurs.
Version 0.9 (March 1, 2015)
=================================
+ Table constraints accept arrays as tuples. For example, table_in({V1,V2},[{1,2},{2,3}]).
The form (a1,a2,...,an) for tuples still works but is obsolete.
+ Espresso is used to generate compact CNF codes for the domain, table, element, and regular constraints.
+ SAT removed from the MSV version; the cygwin version must be used on Windows.
+ This version issues a more user-friendly error message for Prolog-style if-then (A -> B) with no else part.
+ Bug fixes (including bugs reported by Sergii Dymchenko)
+ All global constraints are removed from the mip module. Now, the mip module only supports linear constraints.
Version 0.8 (January 24, 2015)
=================================
+ New space and parenthesis rules are applied to printing expressions.
+ Significant improvements in the SAT compiler, especially in the handling of arithmetic, reified arithmetic, table, cumulative, and all_different constraints.
+ The SAT solver can be called multiple times in one program execution and can be backtracked over.
+ The count(V,L,Rel,Count) constraint can be reified for cp, sat, and mip.
+ The option dump(File) added for solve/2 in the sat module, which dumps the generated CNF code into File.
+ The implementation of cp/2 in the os module is modified such that no file can be copied onto itself.
+ Type checking is added to several built-ins.
+ New built-ins added: bool_dvar(X) into basic, and nvalue(N,L) into sat and cp.
+ An improvement in evaluation of tabled programs that require only one answer.
Version 0.7 (November 13, 2014)
=================================
+ In insert_ordered(L,T): L must be a proper list.
+ The two-product encoding is used in sat for the at-most-one constraint.
+ More efficient translation of X #=> Y in sat.
+ The function len(Term) is added, which is equivalent to length(Term).
+ The attribute len is added as an alias of length (e.g., [1,2].len = L)
+ Change the default labeling strategy for max/min back to maxof/minof (in version 0.6, it was maxof_inc/minof_inc).
+ The objective expression in minof/maxof/minof_inc/maxof_inc cannot contain dot or index notations.
+ An improvement in the debugger.
+ A bug fix in read_file_lines(File) for reading UTF-8 characters.
+ Standardize the behaviors of mod/2 and div/2 for cp, sat, and mip (// is the same as div).
Version 0.6 (August 15, 2014)
=================================
+ Improvements in the SAT compiler (reified constraints, X #=< Y, etc.).
+ A new decomposition algorithm for the cumulative constraint.
+ A linear-time algorithm for vars(Term)=Vs.
+ New built-ins added to basic: minof_inc/2-3, maxof_inc/2-3.
+ maxof/2-3, minof/2-3, maxof_inc/2-3, minof_inc/2-3 are allowed to have real-number objective expressions.
+ nth(I,S,V) is modified such that S can be a structure (including an array).
+ A negative number such as -1 is treated as a number even in patterns. So integer($-1) succeeds.
Version 0.5 (July 16, 2014)
=================================
+ Improvements in the SAT compiler.
+ Standardize the behaviors of mod/2 and div/2 for cp, sat, mip, and basic.
+ Improved implementation of X #= max(L) and X #= min(L) in cp.
Version 0.4 (July 2, 2014)
=================================
+ New function get_table_map() added into basic. A table map is stored in the table area and both
keys and values are hash-consed.
+ New predicates is_tabled_state(S) and current_resource_plan_cost(Amount,Plan,Cost) added into planner.
+ New global constraints added in cp and sat: subcircuit/1, lex_le/2, lex_lt/2, regular/6.
+ Re-implement cp/2 for copying files in os.
+ New statistics flag, table_blocks, added.
+ Several significant improvements in the SAT compiler.
+ Bug fixes: neqs/1, put non-ground pairs into the global map,...
Version 0.3 (May 23, 2014)
=================================
+ Added the mip module that links Picat with GLPK. The mip module also supports real-domain
linear constraints in addition to integer-domain constraints supported by cp and sat.
See mip models at http://www.hakank.org/picat/#mip
+ the solve(Options,Vars) built-in in the sat and mip modules are also non-deterministic.
+ New labeling options for the cp module: rand, rand_var, and rand_val.
+ Reifications B #<=> X :: Y and B #<=> X notin Y are supported by all three constraint modules
+ The operator '++' is changed to right-associative.
Version 0.2#1 (April 1, 2014)
=================================
+ The prism module added (the executable is picat_prism)
+ New built-ins added to 'basic' module.
new_list(N,InitVal) = new_list(N,InitVal).
bind_vars(Term,Val) => bind_vars(Term,Val).
+ bug fixes
big-int arithmetic
statistics on fd backtracks
fd_degree
between/3
etc.
Version 0.1 (stable) (Feb. 3, 2014)
=================================
+ command(String)=Status added to module 'sys'.
+ length(Atom) returns the number of UTF-8 chars of Atom if Atom is an atom.
+ New built-in added to module 'ordset'.
ordset(Term) => ordset(Term).
+ sublist/3 is removed from the 'basic' module. slice/2-3 can be used instead.
+ An improvement in the multiplication constraint X #= Y*Z in CP.
+ New functions in 'io' module
read_picat_token() = TokenValue
read_picat_token(FD) = TokenValue
+ bug fixes
attribute variables
@>=/2, @<=/2
writable/1
user's guide
Version 0.1 beta-10 (Jan. 15, 2014)
=================================
+ Support UTF-8
+ char_code(Char) is replaced by ord(Char)
+ code_char(Code) is replaced by chr(Code)
+ New built-ins added to the 'basic' module
'@>'(X,Y) => X @> Y.
'@>='(X,Y) => X @>= Y.
'@<'(X,Y) => X @< Y.
'@<='(X,Y) => X @=< Y.
'@=<'(X,Y) => X @=< Y.
list_to_and(L) = list_to_and(L).
and_to_list(And) = and_to_list(And).
+ New built-ins added to the io module
read_char_code() = read_char_code(stdin).
read_char_code(FD,N) = read_char_code(FD,N).
read_char_code(FD) = read_char_code(FD).
write_char(Chars) => write_char(stdout,Chars).
write_char(FD,Chars) => write_char(FD,Chars).
write_char_code(Codes) => write_char_code(stdout,Codes).
write_char_code(FD,Codes) => write_char_code(FD,Codes).
+ Bug fixes:
the module system
printf & writef
Version 0.1 beta-8 (Dec. 15, 2013)
=================================
+ Allows the user to define the condition of the final states with final(+S,-Plan,-Cost).
+ New functions and predicates added to the planner module
current_plan()
current_resource_plan(Resource,Plan)
+ best_plan(...) is changed to use the downward algorithm.
+ Throws an exception if the top-level main predicate of a Picat application fails
+ size(Map) added that returns the size of Map.
Version 0.1 beta-7 (Nov. 25, 2013)
=================================
+ length([X : Iterator,...]) is compiled into a loop that does not create the list
+ The ordset module is added
+ The circuit constraint is added into the sat module
+ The sat compiler is improved (reification and element constraints)
+ bug fixes:
compiling list comprehensions in disjunction
module lookup
Version 0.1 beta-6 (Nov. 10, 2013)
=================================
+ function current_resource/0 is added to the planner module.
+ '::'/2 is added to cp and sat.
+ in/2 and notin/2 are removed from basic.
+ improvements of operations on maps
+ bug fix: indomain(X) in cp
Version 0.1 beta-5 (Nov. 3, 2013)
================================
+ X in D: D must be an integer list
+ X notin D: D must be an integer list
+ table constraints are added into cp and sat: table_in(VarTuples,ValTuples), table_notin(VarTuples,ValTuples)
+ assignment, cumulative are added into the sat module
+ slice/1-2 added into the 'basic' module: L.slice(StartIndex), L.slice(FromIndex,ToIndex)
+ bug fix: in module qualified names, the module name can be a pre-imported module. For example, math.pi.
+ the built-in 'false' is added.
+ allow Boolean expressions in arithmetic constraints for sat.
Version 0.1 beta-4 (Oct. 5, 2013)
================================
+ new operators:
(A && B) is the same as (A,B)
(A || B) is the same as (A;B)
+ new predicate in the sys module
cl (read a program from the console)
+ changes to the 'basic' module:
array(Term) (array({}) succeeds now)
to_list(Term) (to_list({}) returns [])
delete(List,X) = NewList (use = for equality test rather than ==)
delete_all(List,X) = NewList (use = for equality test rather than ==)
find(String, Substring, From, To) (moved to util)
find_ignore_case(String, Substring, From, To) (moved to util)
replace(T,Old,New) = CopyT (change of the prototype)
+ new predicates added to the util module:
find(String, Substring, From, To) (originally in the 'basic' module)
find_first_of(T,Pattern)=Index,
find_ignore_case(String, Substring, From, To) (originally in the 'basic' module)
find_last_of(T,Pattern)=Index.
lstrip(L)
lstrip(L,Elms),
replace_at(T,I,New)=CopyT,
rstrip(L),
rstrip(L,Elms),
strip(L),
strip(L,Elms),
+ (sum(a++b) #= 1) raises an exception rather than fails
+ document the report option in solve/2 (sat).
+ improve the element constraint in the sat module
+ change the precedence of := (:= cannot be part of an expresion)
+ X[...] := Exp (raise an error if the updated term is not a heap one).
+ bug fixes:
a bug in read_int(FD) and read_int().
a bug in the loop compiler