1 /******************************************
2 Copyright (c) 2016, Mate Soos
3
4 Permission is hereby granted, free of charge, to any person obtaining a copy
5 of this software and associated documentation files (the "Software"), to deal
6 in the Software without restriction, including without limitation the rights
7 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
8 copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
10
11 The above copyright notice and this permission notice shall be included in
12 all copies or substantial portions of the Software.
13
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
19 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
20 THE SOFTWARE.
21 ***********************************************/
22
23 #include "gtest/gtest.h"
24
25 #include <set>
26 using std::set;
27
28 #include "src/solver.h"
29 #include "src/solverconf.h"
30 using namespace CMSat;
31 #include "test_helper.h"
32
33 namespace CMSat {
34 struct SearcherTest : public ::testing::Test {
SearcherTestCMSat::SearcherTest35 SearcherTest()
36 {
37 must_inter.store(false, std::memory_order_relaxed);
38 }
~SearcherTestCMSat::SearcherTest39 ~SearcherTest()
40 {
41 delete s;
42 }
43
set_var_polarCMSat::SearcherTest44 void set_var_polar(uint32_t var, bool polarity)
45 {
46 s->new_decision_level();
47 //it must be inverted to set
48 s->enqueue<false>(Lit(var, !polarity));
49 s->cancelUntil(0);
50 }
51
52 SolverConf conf;
53 Solver* s = NULL;
54 Searcher* ss = NULL;
55 std::vector<uint32_t> vars;
56 std::atomic<bool> must_inter;
57 };
58
59 //Regular, 1UIP fails
60
TEST_F(SearcherTest,pickpolar_rnd)61 TEST_F(SearcherTest, pickpolar_rnd)
62 {
63 conf.polarity_mode = PolarityMode::polarmode_rnd;
64 s = new Solver(&conf, &must_inter);
65 s->new_vars(30);
66 ss = (Searcher*)s;
67
68 s->add_clause_outer(str_to_cl(" 1, 2"));
69
70 uint32_t num = 0;
71 for(uint32_t i = 0 ; i < 1000000; i++)
72 num += (unsigned)ss->pick_polarity(0);
73
74 //Not far off from avg
75 ASSERT_GT(num, 400000U);
76 ASSERT_LT(num, 600000U);
77 }
78
TEST_F(SearcherTest,pickpolar_pos)79 TEST_F(SearcherTest, pickpolar_pos)
80 {
81 conf.polarity_mode = PolarityMode::polarmode_pos;
82 s = new Solver(&conf, &must_inter);
83 s->new_vars(30);
84 ss = (Searcher*)s;
85 s->add_clause_outer(str_to_cl(" 1, 2"));
86
87 uint32_t num = 0;
88 for(uint32_t i = 0 ; i < 100000; i++)
89 num += (unsigned)ss->pick_polarity(0);
90
91 ASSERT_EQ(num, 100000U);
92 }
93
TEST_F(SearcherTest,pickpolar_neg)94 TEST_F(SearcherTest, pickpolar_neg)
95 {
96 conf.polarity_mode = PolarityMode::polarmode_neg;
97 s = new Solver(&conf, &must_inter);
98 s->new_vars(30);
99 ss = (Searcher*)s;
100 s->add_clause_outer(str_to_cl(" 1, 2"));
101
102 uint32_t num = 0;
103 for(uint32_t i = 0 ; i < 100000; i++)
104 num += (unsigned)ss->pick_polarity(0);
105
106 ASSERT_EQ(num, 0U);
107 }
108
TEST_F(SearcherTest,pickpolar_auto)109 TEST_F(SearcherTest, pickpolar_auto)
110 {
111 conf.polarity_mode = PolarityMode::polarmode_automatic;
112 s = new Solver(&conf, &must_inter);
113 s->new_vars(30);
114 ss = (Searcher*)s;
115 s->add_clause_outer(str_to_cl(" 1, 2"));
116
117 s->new_decision_level();
118 set_var_polar(0, true);
119 //we expect TRUE
120 ASSERT_EQ(ss->pick_polarity(0), true);
121
122
123 set_var_polar(0, false);
124 //we expect FALSE
125 ASSERT_EQ(ss->pick_polarity(0), false);
126
127 //for unset variables, it must all be FALSE
128 for(uint32_t i = 1; i < 10; i++) {
129 ASSERT_EQ(ss->pick_polarity(i), false);
130 }
131 }
132
TEST_F(SearcherTest,pickpolar_auto_not_changed_by_simp)133 TEST_F(SearcherTest, pickpolar_auto_not_changed_by_simp)
134 {
135 conf.polarity_mode = PolarityMode::polarmode_automatic;
136 conf.doVarElim = false;
137 //conf.verbosity = 2;
138 conf.do_lucky_polar_every_n = 0;
139 conf.doSLS = false;
140 s = new Solver(&conf, &must_inter);
141 s->new_vars(30);
142 ss = (Searcher*)s;
143 s->add_clause_outer(str_to_cl(" 1, 2"));
144 s->add_clause_outer(str_to_cl(" -1, 2"));
145 s->add_clause_outer(str_to_cl(" 3, 4, 5"));
146 s->add_clause_outer(str_to_cl(" -3, 4, 5"));
147 s->add_clause_outer(str_to_cl(" -3, -4, 5"));
148 s->add_clause_outer(str_to_cl(" 2, -3, -4, 5"));
149 s->add_clause_outer(str_to_cl(" 2, -3, 4, 5"));
150 s->add_clause_outer(str_to_cl(" 4, 5"));
151 s->add_clause_outer(str_to_cl(" -4, 5"));
152 s->add_clause_outer(str_to_cl(" -4, -5"));
153
154
155 //The mod%3 is only to set it kinda randomly.
156 for(size_t i = 0; i < 30; i++) {
157 set_var_polar(i, i%3);
158 }
159
160 //for unset variables, it must all be FALSE
161 for(uint32_t i = 0; i < 30; i++) {
162 ASSERT_EQ(ss->pick_polarity(i), (bool)(i%3));
163 }
164
165 s->simplify_problem(true);
166 //for unset variables, it must all be FALSE
167 for(uint32_t i = 0; i < 30; i++) {
168 ASSERT_EQ(ss->pick_polarity(i), (bool)(i%3));
169 }
170
171 s->simplify_problem(false);
172 for(uint32_t i = 0; i < 30; i++) {
173 ASSERT_EQ(ss->pick_polarity(i), (bool)(i%3));
174 }
175 }
176
177 }
178
main(int argc,char ** argv)179 int main(int argc, char **argv) {
180 ::testing::InitGoogleTest(&argc, argv);
181 return RUN_ALL_TESTS();
182 }
183