@Test(groups = "1s") public void testNewVariable() throws Exception { Assert.assertEquals(a, 0); Assert.assertEquals(b, 1); Assert.assertEquals(c, 2); Assert.assertEquals(d, 3); Assert.assertEquals(SatSolver.makeLiteral(a, true), 1); Assert.assertEquals(SatSolver.makeLiteral(a, false), 0); Assert.assertEquals(SatSolver.makeLiteral(b, true), 3); Assert.assertEquals(SatSolver.makeLiteral(b, false), 2); Assert.assertEquals(SatSolver.makeLiteral(c, true), 5); Assert.assertEquals(SatSolver.makeLiteral(c, false), 4); Assert.assertEquals(SatSolver.makeLiteral(d, true), 7); Assert.assertEquals(SatSolver.makeLiteral(d, false), 6); }
public int newVariable() { int v = incrementVariableCounter(); assignment_.put(v, Boolean.kUndefined); return v; }
SatSolver implements SatFactory { public int newVariable() { int v = incrementVariableCounter(); assignment_.put(v, Boolean.kUndefined); return v; } }
SatSolver implements SatFactory { public int newVariable() { int v = incrementVariableCounter(); assignment_.put(v, Boolean.kUndefined); return v; } SatSolver(); }
SatSolver implements SatFactory { public int newVariable() { int v = incrementVariableCounter(); assignment_.put(v, Boolean.kUndefined); return v; } 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 int newVariable() { int v = incrementVariableCounter(); assignment_.put(v, Boolean.kUndefined); return v; } 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_; }