@Test(groups = "1s") public void testCancelUntil() throws Exception { int ap = SatSolver.makeLiteral(a, true); int an = SatSolver.makeLiteral(a, false); int bp = SatSolver.makeLiteral(b, true); int cp = SatSolver.makeLiteral(c, true); int cn = SatSolver.makeLiteral(c, false); int dp = SatSolver.makeLiteral(d, true); sat.addClause(an, bp); sat.addClause(cn, dp); sat.propagateOneLiteral(ap); Assert.assertEquals(sat.valueVar(a), SatSolver.Boolean.kFalse); Assert.assertEquals(sat.valueVar(b), SatSolver.Boolean.kFalse); Assert.assertEquals(sat.valueVar(c), SatSolver.Boolean.kUndefined); Assert.assertEquals(sat.valueVar(d), SatSolver.Boolean.kUndefined); Assert.assertEquals(sat.qhead_, 2); Assert.assertEquals(sat.trail_.size(), 2); Assert.assertEquals(sat.trail_.get(0), 1); Assert.assertEquals(sat.trail_.get(1), 3); Assert.assertEquals(sat.trail_markers_.size(), 1); Assert.assertEquals(sat.trailMarker(), 1); Assert.assertEquals(sat.trail_markers_.get(0), 0); sat.propagateOneLiteral(cp); Assert.assertEquals(sat.valueVar(a), SatSolver.Boolean.kFalse); Assert.assertEquals(sat.valueVar(b), SatSolver.Boolean.kFalse); Assert.assertEquals(sat.valueVar(c), SatSolver.Boolean.kFalse); Assert.assertEquals(sat.valueVar(d), SatSolver.Boolean.kFalse); Assert.assertEquals(sat.qhead_, 4); Assert.assertEquals(sat.trail_.size(), 4); Assert.assertEquals(sat.trail_.get(0), 1); Assert.assertEquals(sat.trail_.get(1), 3); Assert.assertEquals(sat.trail_.get(2), 5); Assert.assertEquals(sat.trail_.get(3), 7); Assert.assertEquals(sat.trail_markers_.size(), 2); Assert.assertEquals(sat.trailMarker(), 2); Assert.assertEquals(sat.trail_markers_.get(0), 0); Assert.assertEquals(sat.trail_markers_.get(1), 2); sat.cancelUntil(1); Assert.assertEquals(sat.valueVar(a), SatSolver.Boolean.kFalse); Assert.assertEquals(sat.valueVar(b), SatSolver.Boolean.kFalse); Assert.assertEquals(sat.valueVar(c), SatSolver.Boolean.kUndefined); Assert.assertEquals(sat.valueVar(d), SatSolver.Boolean.kUndefined); Assert.assertEquals(sat.qhead_, 2); Assert.assertEquals(sat.trail_.size(), 2); Assert.assertEquals(sat.trail_.get(0), 1); Assert.assertEquals(sat.trail_.get(1), 3); Assert.assertEquals(sat.trail_markers_.size(), 1); Assert.assertEquals(sat.trailMarker(), 1); Assert.assertEquals(sat.trail_markers_.get(0), 0); sat.cancelUntil(0); Assert.assertEquals(sat.valueVar(a), SatSolver.Boolean.kUndefined); Assert.assertEquals(sat.valueVar(b), SatSolver.Boolean.kUndefined); Assert.assertEquals(sat.valueVar(c), SatSolver.Boolean.kUndefined); Assert.assertEquals(sat.valueVar(d), SatSolver.Boolean.kUndefined); Assert.assertEquals(sat.qhead_, 0); Assert.assertEquals(sat.trail_.size(), 0); Assert.assertEquals(sat.trail_markers_.size(), 0); Assert.assertEquals(sat.trailMarker(), 0); }
public void cancelUntil(int level) { if (trailMarker() > level) { for (int c = trail_.size() - 1; c >= trail_markers_.get(level); c--) { int x = var(trail_.get(c)); assignment_.put(x, Boolean.kUndefined); } qhead_ = trail_markers_.get(level); trail_.remove(trail_markers_.get(level), trail_.size() - trail_markers_.get(level)); trail_markers_.remove(level, trail_markers_.size() - level); } }
SatSolver implements SatFactory { public void cancelUntil(int level) { if (trailMarker() > level) { for (int c = trail_.size() - 1; c >= trail_markers_.get(level); c--) { int x = var(trail_.get(c)); assignment_.put(x, Boolean.kUndefined); } qhead_ = trail_markers_.get(level); trail_.remove(trail_markers_.get(level), trail_.size() - trail_markers_.get(level)); trail_markers_.remove(level, trail_markers_.size() - level); } } }
SatSolver implements SatFactory { public void cancelUntil(int level) { if (trailMarker() > level) { for (int c = trail_.size() - 1; c >= trail_markers_.get(level); c--) { int x = var(trail_.get(c)); assignment_.put(x, Boolean.kUndefined); } qhead_ = trail_markers_.get(level); trail_.remove(trail_markers_.get(level), trail_.size() - trail_markers_.get(level)); trail_markers_.remove(level, trail_markers_.size() - level); } } SatSolver(); }
SatSolver implements SatFactory { public void cancelUntil(int level) { if (trailMarker() > level) { for (int c = trail_.size() - 1; c >= trail_markers_.get(level); c--) { int x = var(trail_.get(c)); assignment_.put(x, Boolean.kUndefined); } qhead_ = trail_markers_.get(level); trail_.remove(trail_markers_.get(level), trail_.size() - trail_markers_.get(level)); trail_markers_.remove(level, trail_markers_.size() - level); } } SatSolver(); @Override SatSolver _me(); int newVariable(); boolean addClause(TIntList ps); boolean learnClause(int... ps); boolean addClause(int l); void cancelUntil(int level); int trailMarker(); int nLearnt(); boolean propagateOneLiteral(int lit); void detachLearnt(int ci); static int makeLiteral(int var, boolean sign); static int negated(int l); static boolean sign(int l); static int var(int l); void copyFrom(SatSolver o); long nbclauses(); long numvars(); }
SatSolver implements SatFactory { public void cancelUntil(int level) { if (trailMarker() > level) { for (int c = trail_.size() - 1; c >= trail_markers_.get(level); c--) { int x = var(trail_.get(c)); assignment_.put(x, Boolean.kUndefined); } qhead_ = trail_markers_.get(level); trail_.remove(trail_markers_.get(level), trail_.size() - trail_markers_.get(level)); trail_markers_.remove(level, trail_markers_.size() - level); } } SatSolver(); @Override SatSolver _me(); int newVariable(); boolean addClause(TIntList ps); boolean learnClause(int... ps); boolean addClause(int l); void cancelUntil(int level); int trailMarker(); int nLearnt(); boolean propagateOneLiteral(int lit); void detachLearnt(int ci); static int makeLiteral(int var, boolean sign); static int negated(int l); static boolean sign(int l); static int var(int l); void copyFrom(SatSolver o); long nbclauses(); long numvars(); public boolean ok_; public ArrayList<Clause> clauses; public ArrayList<Clause> learnts; public TIntObjectHashMap<TIntArrayList> implies_; public TIntArrayList touched_variables_; }