Recent Releases
3.028 Sep 2020 22:05
major bugfix:
Numerous improvements on the SAT compiler.
Reimplemented the circuit constraint of the sat module, as reported in the CP'20 paper.
Support of Horn clauses. Horn clauses are translated into pattern-matching rules based on user-supplied or automatically generated
index declarations.
Support of DCG rules. DCG rules are translated into pattern-matching rules via Horn clauses.
Added the following new built-in predicates from Prolog:
arg(I,T,A)
functor(T,F,N).
'=..'(X,Y).
+.
!.
Changed the binding rules for higher-order calls.
Improved the implementation of higher-order calls.
Improved the deger. No private calls or compiler-generated calls can be traced.
a in big-integer compilation.
Improved the implementation of the multiplication constraint in cp.
a in the preprocessor of non-linear constraints that use //, div, mod, or abs.
a in listdir/1 for Windows.
Changed the behavior of open(File,Mode): it returns a new stream for a file even if the file has already been opened.
Improved the translation of functions into tail-recursive predicates.
Improved the handling of the power function in constraints so that it's less likely to cause overflows.
a in vars/1 functions.
Beautified the C source code.
2.806 Dec 2019 04:25
minor feature:
Added new built-in constraints in the sat module.
Subcircuit_grid(A).
Subcircuit_grid(A,K)
Improved SAT encodings for at-most-k constraints.
Improved error messages.
Added the nn (Neural Network) module.
New_nn(Layers) = NN.
New_sparse_nn(Layers) = NN
New_sparse_nn(Layers,Rate) = NN
New_standard_nn(Layers) = NN
Nn_destroy(NN)
Nn_destroy_all
Nn_load(File) = NN
Nn_print(NN)
Nn_run(NN, Input) = Output
Nn_run(NN, Input, Opts) = Output
Nn_save(NN,File)
Nn_set_activation_function_hidden(NN, Func)
Nn_set_activation_function_layer(NN, Func, Layer)
Nn_set_activation_function_output(NN, Func)
Nn_set_activation_steepness_hidden(NN, Steepness)
Nn_set_activation_steepness_layer(NN, Steepness, Layer)
Nn_set_activation_steepness_output(NN, Steepness)
Nn_train(NN,Data)
Nn_train(NN,Data,Opts)
Nn_train_data_get(Data, I) = Pair
Nn_train_data_load(File) = Data
Nn_train_data_save(Data, File)
Nn_train_data_size(Data) = Size
Support of Cbc as an underlying MIP solver.
The solve predicate in the mip module supports a new option, named cbc, which instructs Picat to.
Use the Cbc MIP solver. Picat uses the following command to call the Cbc solver:
Cbc TmpFile solve solu SolFile.
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 cbc is not available.
Significant improvement of the SAT compiler.
Use direct encoding if no variables are involved in arithmetic constraints.
Hybrid encodings of table constraints.
New encodings for small-domain arithmetic constraints.
New implementation of the branch-and-bound algorithm for optimization problems.
New decomposers for circuit, subcircuit, and regular constraints.
New built-ins on ASCII characters.
Ascii_digit(Char) = ascii_digit(Char).
Ascii_alpha(Char) = ascii_alpha(Char).
Ascii_alpha_digit(Char) = ascii_alpha_digit(Char).
Ascii_lowercase(Char) = ascii_lowercase(Char).
Ascii_uppercase(Char) = ascii_uppercase(Char).
Changed
2.609 Feb 2019 17:25
minor feature:
Table constraints can involve short tuples, where values can be the don't-care symbol *.
Added the new built-in predicate bigint(X) in the basic module.
Improved error messages.
BDD encoding for table constraints.
Tuples in table constraints must have the syntax a1...,an , and the syntax (a1...,an) is no longer supported for tuples in table constraints.
2.509 Oct 2018 14:05
minor bugfix:
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 in the regular constraint.
in the SAT encoder.
One in big-integer arithmetic.
2.416 Apr 2018 13:25
minor feature:
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.
: round.
2.303 Feb 2018 02:45
minor feature:
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.
: map/1, SAT compiler.
2.211 Aug 2017 16:05
minor bugfix:
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.
2.114 Mar 2017 02:05
minor bugfix:
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.
a in comparison of integers between -2 56..-2 28 and 2 28..2 56
a in the pow function that occurs when the operands are floats
a in the sat compiler that affects large domains.
2.019 Nov 2016 06:45
major feature:
Improvements in sat.
New implementations of the circuit, subcircuit, and regular constraints
New and better odering for breaking constraints into primitives 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), XY, 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(
1.904 Apr 2016 06:25
minor feature:
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
1.820 Feb 2016 02:45
minor bugfix:
New built-ins.
Math:
Pow_mod(X,Y,Z) = pow_mod(X,Y,Z). (the same as XY 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
The matrix_element constraint is extended so that the matrix can be non-ground.
The missing internal predicate ' bc_clause'/1 added.
1.704 Jan 2016 15:45
minor feature:
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.
1.614 Dec 2015 06:45
minor bugfix:
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)
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).
.
1.429 Sep 2015 17:25
minor bugfix:
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 entailmemnt constraints.
An improvement in the propagator for the multiplication constraint.
Arrays can be iterated over by foreach loops without being converted into lists.
A 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.
1.302 Aug 2015 11:05
minor feature:
The sort functions are improved.
A bug in the parsr 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.
1.213 Jun 2015 12:25
minor feature:
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.
Bug fixes in find_first_of/2 and find_last_of/2 in the util module.
1.115 May 2015 18:05
minor feature:
=================================
.
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(_)).
.
1.0.004 Apr 2015 14:05
major feature:
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.
Homepage
Download