András Salamon
András Salamon
In current conjure `Repository version 3fcbbbbab (2021-12-17 13:08:56 +0300)` calling an SMT solver backend other than Boolector fails, because the version of Savile Row which conjure installs always thinks it...
As of late 2018, conjure supported specs of the form: ``` given n : int(1..) letting ind be domain int(1..n) find P : matrix indexed by [ind] of bool such...
In many graph problems there are at least two graphs, a pattern H and a target graph G. Typically the idea is to try an Essence model for all combinations...
(Recording this from email.) The following fails: ``` given m : int(1..) find Cs : sequence (size m) of int(0..m) such that exists Cz : sequence (size m) of int(0..m)...
To express graph connectivity of n-vertex graphs using adjacency matrices, we need to compute \log_2 n as one of the dimensions of an auxiliary matrix. Usually n is given as...
It is often convenient to describe transformations in terms of functions, especially when dealing with several transformations that can be written as compositions of more basic ones. Currently, Conjure turns...
Essence is a fragment of relational second-order logic. All logics have a syntax for defining predicates, so that more complex expressions can be expressed succinctly in terms of predicates, with...
According to the Constraints 2008 paper defining Essence, `image(f,S)` should (p.289, lines 7–9) be a valid way to specify the set {f(s) | s in S}.
``` > conjure pretty --output-format=json essence/5x7-ps1-a13.param Parsing as a parameter file Error: Cannot convert the following to simple JSON: letting vertices be new type enum {loc_2_2, loc_3_2, loc_4_2, loc_2_3, loc_3_3,...
The following simple spec ``` given vertices new type enum find move : function (total) int(1..1) --> tuple(vertices,vertices) such that move(1) = (min(vertices),min(vertices)) ``` works great with `conjure solve tmp.essence...