@Test(groups = "1s") public void testDetachLearnt() throws Exception { }
public void detachLearnt(int ci) { Clause cr = learnts.get(ci); learnts.remove(ci); ArrayList<Watcher> ws = watches_.get(negated(cr._g(0))); int i = ws.size() - 1; while (i >= 0 && ws.get(i).clause != cr) { i--; } assert i > -1; ws.remove(i); ws = watches_.get(negated(cr._g(1))); i = ws.size() - 1; while (i >= 0 && ws.get(i).clause != cr) { i--; } assert i > -1; ws.remove(i); }
SatSolver implements SatFactory { public void detachLearnt(int ci) { Clause cr = learnts.get(ci); learnts.remove(ci); ArrayList<Watcher> ws = watches_.get(negated(cr._g(0))); int i = ws.size() - 1; while (i >= 0 && ws.get(i).clause != cr) { i--; } assert i > -1; ws.remove(i); ws = watches_.get(negated(cr._g(1))); i = ws.size() - 1; while (i >= 0 && ws.get(i).clause != cr) { i--; } assert i > -1; ws.remove(i); } }
SatSolver implements SatFactory { public void detachLearnt(int ci) { Clause cr = learnts.get(ci); learnts.remove(ci); ArrayList<Watcher> ws = watches_.get(negated(cr._g(0))); int i = ws.size() - 1; while (i >= 0 && ws.get(i).clause != cr) { i--; } assert i > -1; ws.remove(i); ws = watches_.get(negated(cr._g(1))); i = ws.size() - 1; while (i >= 0 && ws.get(i).clause != cr) { i--; } assert i > -1; ws.remove(i); } SatSolver(); }
SatSolver implements SatFactory { public void detachLearnt(int ci) { Clause cr = learnts.get(ci); learnts.remove(ci); ArrayList<Watcher> ws = watches_.get(negated(cr._g(0))); int i = ws.size() - 1; while (i >= 0 && ws.get(i).clause != cr) { i--; } assert i > -1; ws.remove(i); ws = watches_.get(negated(cr._g(1))); i = ws.size() - 1; while (i >= 0 && ws.get(i).clause != cr) { i--; } assert i > -1; ws.remove(i); } 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 detachLearnt(int ci) { Clause cr = learnts.get(ci); learnts.remove(ci); ArrayList<Watcher> ws = watches_.get(negated(cr._g(0))); int i = ws.size() - 1; while (i >= 0 && ws.get(i).clause != cr) { i--; } assert i > -1; ws.remove(i); ws = watches_.get(negated(cr._g(1))); i = ws.size() - 1; while (i >= 0 && ws.get(i).clause != cr) { i--; } assert i > -1; ws.remove(i); } 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_; }