← Back to branch summary

~ubuntu-branches/ubuntu/wily/clasp/wily

« back to all changes in this revision

Viewing changes to libclasp/tests/solver_test.cpp

  • Committer: Package Import Robot
  • Author(s): Thomas Krennwallner
  • Date: 2015-05-12 07:18:25 UTC
  • mfrom: (20.1.12 sid)
  • Revision ID: package-import@ubuntu.com-20150512071825-vlgtxbw5245d6wni
Tags: 3.1.2-1
* Imported Upstream version 3.1.2
* Fix dep5-copyright-license-name-not-unique and
  missing-license-paragraph-in-dep5-copyright lintian warnings.

Show diffs side-by-side

added added

removed removed

Lines of Context:
libclasp/tests/solver_test.cpp
140
140
 
141
141
        CPPUNIT_TEST(testClearAssumptions);
142
142
        CPPUNIT_TEST(testStopConflict);
 
143
        CPPUNIT_TEST(testClearStopConflictResetsBtLevel);
143
144
 
144
145
        CPPUNIT_TEST(testSearchKeepsAssumptions);
145
146
        CPPUNIT_TEST(testSearchAddsLearntFacts);
1245
1246
                s.clearStopConflict();
1246
1247
                CPPUNIT_ASSERT(s.rootLevel() == 1 && s.queueSize() == 1);
1247
1248
        }
 
1249
        
 
1250
        void testClearStopConflictResetsBtLevel() {
 
1251
                Var a = ctx.addVar( Var_t::atom_var );
 
1252
                Var b = ctx.addVar( Var_t::atom_var );
 
1253
                Var c = ctx.addVar( Var_t::atom_var );
 
1254
                Var d = ctx.addVar( Var_t::atom_var );
 
1255
                Solver& s = ctx.startAddConstraints();
 
1256
                ctx.addBinary(negLit(c), posLit(d));
 
1257
                ctx.endInit();
 
1258
                s.assume(posLit(a)) && s.propagate();
 
1259
                s.assume(posLit(b)) && s.propagate();
 
1260
                s.assume(posLit(c)) && s.propagate();
 
1261
                CPPUNIT_ASSERT(s.numFreeVars() == 0);
 
1262
                s.setBacktrackLevel(s.decisionLevel());
 
1263
                s.backtrack();
 
1264
                uint32 bt = s.backtrackLevel();
 
1265
                s.assume(posLit(d)) && s.propagate();
 
1266
                CPPUNIT_ASSERT(bt != s.decisionLevel());
 
1267
                s.setStopConflict();
 
1268
                CPPUNIT_ASSERT(s.backtrackLevel() == s.decisionLevel());
 
1269
                s.clearStopConflict();
 
1270
                CPPUNIT_ASSERT(s.backtrackLevel() == bt);
 
1271
        }
1248
1272
 
1249
1273
        void testStats() {
1250
1274
                ProblemStats p1, p2;