Run SMT solver on requested queries

[leonardoalt]

and rerun compiler with given responses

[axic]

There are 3 PRs fixing this and this doesn't work on Node 4 :)

[leonardoalt]

What's the workaround then?

[axic]

#105 is the real solution. A quick intermediate solutions it dropping Node 4 support.

#127 and #246 do the same change as you.

[coveralls]

Coverage remained the same at 56.982% when pulling 1aaffe1 on smt_wrapper into 1cee2ae on master.

[axic]

It seems however that your change is somewhat a 3rd option which indeed works.

[axic]

Oh works because ti doesn't have the test! :)

[axic]

Can you try adding your version to #127 (just push a commit) ?

[leonardoalt]

It should be the same, shouldn't it?

[leonardoalt]

Pushed there

[axic]

This is my proposal:

// Returns `null` if nothing is to be solved or a new `input` if it needs to be run again.
function handleSMTQueries(input, output, solver) {
  if (!output.auxiliaryInputRequested)
    return null

  // Could also just throw an exception here?
  if (!solverCallback)
    return null

  let queries = output.auxiliaryInputRequested.smtlib2queries
  var responses = {}
  for (var queryKey in queries) {
    responses[queryKey] = solver(queries[queryKey])
  }

  input.auxiliaryInput.smtlib2esponses = responses
  return input
}

[leonardoalt]

input.auxiliaryInput.smtlib2esponses = responses
doesn't work because input.auxiliaryInput is still undefined at that point

[axic]

It is the high level design :)

[leonardoalt]

Updated extracting the solve part into a sync function

[leonardoalt]

not sure about the changes to solcjs, it's gotten quite long with the error handling

[axic]

Reordered some things and fixed lint.

@leonardoalt can you double check it works?

Can you create an issue for adding tests? That will need a manual installation of cvc4/z3.

[leonardoalt]

Yes, it works!