__int128 support

[JoD]

RoundingSat with LP solving computes Farkas constraints using __int128 precision. These Farkas constraints are divided down to fit 32 bit before storing them in the learned constraint database, but the computations to obtain them require 128 bit precision.

I tried for a short while to get VeriPB to use 128 bit computation, see https://github.com/StephanGocht/VeriPB/tree/bigint .

However, I got the following runtime error:

Sorry, there was an internal error. Because you are running in debug mode I will give you the exception.
Traceback (most recent call last):
  File "/home/jodv/.local/bin/veripb", line 11, in <module>
    load_entry_point('veripb', 'console_scripts', 'veripb')()
  File "/home/jodv/workspace/_systems/VeriPB/veripb/utils.py", line 156, in run_cmd_main
    return runUI(args.formula, args.derivation, verifyerSettings, arbitraryPrecision = args.arbitraryPrecision)
  File "/home/jodv/workspace/_systems/VeriPB/veripb/utils.py", line 116, in runUI
    raise e
  File "/home/jodv/workspace/_systems/VeriPB/veripb/utils.py", line 84, in runUI
    result = run(*args, **kwargs)
  File "/home/jodv/workspace/_systems/VeriPB/veripb/utils.py", line 48, in run
    formula = OPBParser(context.ineqFactory).parse(formulaFile)
  File "/home/jodv/workspace/_systems/VeriPB/veripb/timed_function.py", line 22, in wrapper
    res = function(*args, **kwargs)
  File "/home/jodv/workspace/_systems/VeriPB/veripb/parser.py", line 188, in parse
    constraints.extend(self.parseLine(line.rstrip()))
  File "/home/jodv/workspace/_systems/VeriPB/veripb/parser.py", line 233, in parseLine
    result = self.parseOPB(words)
  File "/home/jodv/workspace/_systems/VeriPB/veripb/parser.py", line 287, in parseOPB
    result = [self.ineqFactory.fromTerms(terms, degree)]
  File "constraints.pyx", line 404, in veripb.constraints.CppIneqFactory.fromTerms
TypeError: __init__(): incompatible constructor arguments. The following argument types are supported:
    1. veripb.optimized.constraints.CppInequality(arg0: List[__int128], arg1: List[int], arg2: __int128)

Invoked with: [], [], 0

Maybe the issue resides with the fact that the C interface should only provide long long CoefTypes, which currently seems to be the full __int128 type.

In any case, @StephanGocht, I'd be grateful if could you have a look, as it would be great if I could keep the proof checking for VeriPB working with LP integration.

I can provide some formula and proof files in which 128bit calculations are used if these would be of use.

[StephanGocht]

Is the --arbitraryPrecision flag too slow?

[StephanGocht]

Can you test if the latest commit on the branch is working for you? This should work as long as all mentioned coefficients in the proof are at most long long.

[StephanGocht]

VeriPB uses arbitrary precision by default now, so this should be resolved.