Disabled incremental solving for CP solvers.

pruemmer · Aug 19, 2019 · b43d69d · b43d69d
1 parent 86ec9fd
commit b43d69d
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 11 deletions.
diff --git a/lib/analysis.js b/lib/analysis.js
@@ -126,11 +126,7 @@
             default:
                 throw new Error(`invalid solver ${SOLVER}`);
         }
-        if (solver.isCPSolver()) {
-            if (process.env.INCREMENTAL === "0")
-                console.error("Warning: incremental option disabled for CP solvers.");
-        }
-        else {
+        if (!solver.isCPSolver()) {
             if (commandLog) {
                 solver.logCommands(commandLog);
             }

diff --git a/lib/cp.js b/lib/cp.js
@@ -1,5 +1,7 @@
 "use strict";
 
+const assert = require("assert");
+
 const fs = require("fs");
 
 const Type = require("./type");
@@ -183,7 +185,7 @@ exports.CPSolver = class CPSolver {
     }
 
     async solveSat(vars) {
-//        console.log(vars, this.model)
+        // console.log(vars, this.model)
         const decls = this.declareVars(vars);
         const n_props = this.model.N_IMPL_PROPS + this.model.N_EXPL_PROPS;
         const mzn_model = (
@@ -321,6 +323,7 @@ exports.CPSolver = class CPSolver {
     };
 
     pop(n) {
+        assert (n == 1);
         this.initModel();
     }
 

diff --git a/lib/dse.js b/lib/dse.js
@@ -1,7 +1,7 @@
 "use strict";
 
 const _ = require("lodash");
-
+const assert = require("assert");
 const { BooleanConstraint, TypeConstraint } = require("./constraint");
 const { SymbolicValue, Constant, Variable, Temporary } = require("./symbolic");
 const { parseModel } = require("./model");
@@ -273,6 +273,7 @@ class ConstraintCollector {
 
         if (idx < this._unsyncedIndex) {
             if (this.incremental) {
+                assert (!this.solver.isCPSolver());
                 this.solver.pop(this._unsyncedIndex - idx);
                 this._unsyncedIndex = idx;
             } else {
@@ -422,11 +423,11 @@ class ConstraintCollector {
                 break;
             }
         }
-//        console.log("popping ", i);
+        // console.log("popping ", i);
         this.pop(this._constraintStack.length - i);
         for (; i < prefixLength; i++) {
             this.push(constraints[i]);
-//            console.log("pushing ", constraints[i]);
+            //console.log("pushing ", constraints[i]);
         }
     }
 
@@ -441,9 +442,8 @@ class ConstraintCollector {
         }
         else
             status = await this.checkSat();
-        if (status !== "sat") {
+        if (status !== "sat")
             return { status: status };
-        }
         return { status: "sat", model: await this.getModel() };
     }
 }
@@ -456,6 +456,10 @@ class DSE {
             coreCacheSize: 8
         });
         this._solver = solver;
+        if (options.incremental && solver.isCPSolver()) {
+            console.error("Warning: incremental option disabled for CP solvers.");
+            options.incremental = false;
+        }
         this._collector = new ConstraintCollector(solver, options.incremental);
         this._program = program;
         this._inputs = [{model: {}, step: 0}];