jwaldmann

Changing Data.Set.Set to Data.Sequence.Seq in ``` class DIMACS t where ... dimacsClauses :: t -> Seq IntSet ``` (Ersatz.Problem and Ersatz.Internal.Formula) already helps a bit (reduces 20 s for writing...

Writing the CNF still feels slow. I am counting 10 MByte per minute *after* the head of the formula is already written - so ersatz knows the number of variables...

Here's the profiling data for above example ``` speed +RTS -P -H -RTS 1000000 total time = 42.78 secs (42782 ticks @ 1000 us, 1 processor) total alloc = 31,984,151,680...

One aspect is that for this specific test, anyminisat was calling cryptominisat5 and that is inefficient at reading the assignment. I'll make a separate issue, and the fix should be...

Sorry I put the wrong issue number in my commit, so it does not appear here automatically. https://github.com/yav/simple-smt/commit/a376f570585bb9186ada83e3b747f5d066783e7d

similarly, `Bits xs + Bits ys >=? 0` should simplify to `true`, and `Bits xs + Bits ys >? 0` is equivalent to `or (xs ys)`, but the actual formulas...

detailed analysis for `Bits xs + Bits ys === 0`: ``` (-6 | -4 | -2) & (-6 | 2 | 4) & (-2 | 4 | 6) & (-4...

analysis for `Bits xs + Bits ys

with previous commit, I can parse output from ` "z3" [ "-in", "-smt2" ]`

No, output format is well-defined (meanwhile)? See 4.2.6 "Inspecting models" of http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf Yes, I will send PR.