Proper SMT CHC tests

smtchecker.js

@@ -25,10 +25,10 @@ function handleSMTQueries (inputJSON, outputJSON, solver) {
   return inputJSON;
 }
 
-function smtCallback (solver) {
+function smtCallback (solverFunction, solver) {
   return function (query) {
     try {
-      var result = solver(query);
+      var result = solverFunction(query, solver);
       return { contents: result };
     } catch (err) {
       return { error: err };

smtsolver.js

@@ -3,37 +3,70 @@ var execSync = require('child_process').execSync;
 var fs = require('fs');
 var tmp = require('tmp');
 
-const timeout = 10000;
+// Timeout in seconds.
+const timeout = 300;
 
 var potentialSolvers = [
+  {
+    name: 'Eldarica Vanilla',
+    command: 'eld',
+    params: '-horn'
+  },
+  {
+    name: 'Eldarica No Abstraction',
+    command: 'eld',
+    params: '-horn -abstract:off'
+  },
+  {
+    name: 'Eldarica Term Abstraction',
+    command: 'eld',
+    params: '-horn -abstract:term'
+  },
+  {
+    name: 'Eldarica Oct Abstraction',
+    command: 'eld',
+    params: '-horn -abstract:oct'
+  },
+  {
+    name: 'Spacer Vanilla',
+    command: 'z3',
+    params: '-smt2 timeout=' + (timeout * 1000) + ' rewriter.pull_cheap_ite=true'
+  },
+  {
+    name: 'Spacer Quant',
+    command: 'z3',
+    params: '-smt2 timeout=' + (timeout * 1000) + ' rewriter.pull_cheap_ite=true fp.spacer.q3.use_qgen=true fp.spacer.mbqi=false fp.spacer.ground_pobs=false'
+  }
+/*
   {
     name: 'z3',
-    params: '-smt2 rlimit=20000000 rewriter.pull_cheap_ite=true fp.spacer.q3.use_qgen=true fp.spacer.mbqi=false fp.spacer.ground_pobs=false'
+    params: ' timeout=' + timeout + ' rewriter.pull_cheap_ite=true fp.spacer.q3.use_qgen=true fp.spacer.mbqi=false fp.spacer.ground_pobs=false'
   },
   {
     name: 'cvc4',
     params: '--lang=smt2 --tlimit=' + timeout
   }
+*/
 ];
-var solvers = potentialSolvers.filter(solver => commandExistsSync(solver.name));
+var solvers = potentialSolvers.filter(solver => commandExistsSync(solver.command));
 
-function solve (query) {
-  if (solvers.length === 0) {
+function solve (query, solver) {
+  if (solver === undefined) {
     throw new Error('No SMT solver available. Assertion checking will not be performed.');
   }
 
+  console.log("Running solver " + solver.name);
   var tmpFile = tmp.fileSync({ postfix: '.smt2' });
   fs.writeFileSync(tmpFile.name, query);
-  // TODO For now only the first SMT solver found is used.
-  // At some point a computation similar to the one done in
-  // SMTPortfolio::check should be performed, where the results
-  // given by different solvers are compared and an error is
-  // reported if solvers disagree (i.e. SAT vs UNSAT).
+  console.log(query);
   var solverOutput;
   try {
     solverOutput = execSync(
-      solvers[0].name + ' ' + solvers[0].params + ' ' + tmpFile.name, {
-        stdio: 'pipe'
+      solver.command + ' ' + solver.params + ' ' + tmpFile.name, {
+        encoding: 'utf8',
+        maxBuffer: 1024 * 1024 * 1024,
+        stdio: 'pipe',
+        timeout: timeout * 1000
       }
     ).toString();
   } catch (e) {
@@ -44,17 +77,21 @@ function solve (query) {
     if (
       !solverOutput.startsWith('sat') &&
       !solverOutput.startsWith('unsat') &&
-      !solverOutput.startsWith('unknown')
+      !solverOutput.startsWith('unknown') &&
+      !solverOutput.startsWith('(error') &&
+      !solverOutput.startsWith('error')
     ) {
       throw new Error('Failed to solve SMT query. ' + e.toString());
     }
   }
   // Trigger early manual cleanup
   tmpFile.removeCallback();
+  console.log("OUTPUT IS");
+  console.log(solverOutput);
   return solverOutput;
 }
 
 module.exports = {
   smtSolver: solve,
-  availableSolvers: solvers.length
+  availableSolvers: solvers
 };

solcjs

@@ -53,8 +53,12 @@ function stripBasePath(path) {
 }
 
 var callbacks = undefined
-if (program.basePath)
-  callbacks = {'import': readFileCallback};
+if (program.basePath) {
+  callbacks = {
+    'import': readFileCallback,
+    'smtSolver': smtchecker.smtCallback(smtsolver.smtSolver, smtsolver.availableSolvers[1])
+  };
+}
 
 if (program.standardJson) {
   var input = fs.readFileSync(process.stdin.fd).toString('utf8');