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 "solutionextender.h"
24 #include "solver.h"
25 #include "varreplacer.h"
26 #include "occsimplifier.h"
27 
28 //#define VERBOSE_DEBUG_SOLUTIONEXTENDER
29 
30 using namespace CMSat;
31 
SolutionExtender(Solver * _solver,OccSimplifier * _simplifier)32 SolutionExtender::SolutionExtender(Solver* _solver, OccSimplifier* _simplifier) :
33     solver(_solver)
34     , simplifier(_simplifier)
35 {
36 }
37 
extend()38 void SolutionExtender::extend()
39 {
40     if (solver->conf.verbosity >= 10) {
41         cout << "c Exteding solution -- SolutionExtender::extend()" << endl;
42     }
43 
44     #ifdef SLOW_DEBUG
45     for(uint32_t i = 0; i < solver->varData.size(); i++) {
46         uint32_t v_inter = solver->map_outer_to_inter(i);
47         if (
48             //decomposed's solution has beed added already, it SHOULD be set
49             //but everything else is NOT OK
50             (solver->varData[v_inter].removed != Removed::none
51                 && solver->varData[v_inter].removed != Removed::decomposed
52                 && solver->varData[v_inter].removed != Removed::clashed
53             )
54             && solver->model[i] != l_Undef
55         ) {
56             cout << "ERROR: variable " << i + 1
57             << " set even though it's removed: "
58             << removed_type_to_string(solver->varData[v_inter].removed) << endl;
59             //solver->model[i] = l_Undef;
60             assert(solver->model[i] == l_Undef);
61         }
62     }
63     #endif
64 
65     //Extend variables already set
66     solver->varReplacer->extend_model_already_set();
67 
68     if (simplifier) {
69         simplifier->extend_model(this);
70     }
71 
72     //clause has been added with "lit, ~lit" so var must be set
73     for(size_t i = 0; i < solver->undef_must_set_vars.size(); i++) {
74         if (solver->undef_must_set_vars[i]
75             && solver->model_value(i) == l_Undef
76         ) {
77             solver->model[i] = l_False;
78         }
79     }
80 
81     //All variables, not just those set
82     solver->varReplacer->extend_model_set_undef();
83 }
84 
satisfied(const vector<Lit> & lits) const85 inline bool SolutionExtender::satisfied(const vector< Lit >& lits) const
86 {
87     for(const Lit lit: lits) {
88         if (solver->model_value(lit) == l_True)
89             return true;
90     }
91 
92     return false;
93 }
94 
95 //called with _outer_ variable in "blockedOn"
dummyBlocked(const uint32_t blockedOn)96 void SolutionExtender::dummyBlocked(const uint32_t blockedOn)
97 {
98     #ifdef VERBOSE_DEBUG_SOLUTIONEXTENDER
99     cout
100     << "dummy blocked lit (outer) "
101     << blockedOn + 1
102     << endl;
103     #endif
104 
105     #ifdef SLOW_DEBUG
106     const uint32_t blockedOn_inter = solver->map_outer_to_inter(blockedOn);
107     assert(solver->varData[blockedOn_inter].removed == Removed::elimed);
108     #endif
109 
110     //Blocked clauses set its value already
111     if (solver->model_value(blockedOn) != l_Undef)
112         return;
113 
114     solver->model[blockedOn] = l_False;
115 
116     //If var is replacing something else, it MUST be set.
117     if (solver->varReplacer->var_is_replacing(blockedOn)) {
118         solver->varReplacer->extend_model(blockedOn);
119     }
120 }
121 
addClause(const vector<Lit> & lits,const uint32_t blockedOn)122 bool SolutionExtender::addClause(const vector<Lit>& lits, const uint32_t blockedOn)
123 {
124     #ifdef VERBOSE_DEBUG_SOLUTIONEXTENDER
125     cout
126     << "outer clause: "
127     << lits
128     << endl;
129     #endif
130 
131     #ifdef SLOW_DEBUG
132     const uint32_t blocked_on_inter = solver->map_outer_to_inter(blockedOn);
133     assert(solver->varData[blocked_on_inter].removed == Removed::elimed);
134     assert(contains_var(lits, blockedOn));
135     #endif
136 
137     //Try to extend through setting variables that have been blocked but
138     //were not required to be set until now
139     /*for(Lit l: lits) {
140         if (solver->model_value(l) == l_Undef
141             && var_has_been_blocked[l.var()]
142         ) {
143             solver->model[l.var()] = l.sign() ? l_False : l_True;
144             solver->varReplacer->extend_model(l.var());
145             return false;
146         }
147     }*/
148 
149     //Try to set var that hasn't been set
150 //     for(Lit l: lits) {
151 //         uint32_t v_inter = solver->map_outer_to_inter(l.var());
152 //         if (solver->model_value(l) == l_Undef
153 //             && solver->varData[v_inter].removed == Removed::none
154 //         ) {
155 //             solver->model[l.var()] = l.sign() ? l_False : l_True;
156 //             solver->varReplacer->extend_model(l.var());
157 //             return false;
158 //         }
159 //     }
160 
161     if (solver->conf.verbosity >= 10) {
162         for(Lit lit: lits) {
163             Lit lit_inter = solver->map_outer_to_inter(lit);
164             cout
165             << lit << ": " << solver->model_value(lit)
166             << "(elim: " << removed_type_to_string(solver->varData[lit_inter.var()].removed) << ")"
167             << ", ";
168         }
169         cout << "blocked on: " <<  blockedOn+1 << endl;
170     }
171 
172     if (solver->model_value(blockedOn) != l_Undef) {
173         cout << "ERROR: Model value for var " << blockedOn+1 << " is "
174         << solver->model_value(blockedOn)
175         << " but that doesn't satisfy a v-elim clause on the stack!"
176         << " clause is: " << lits
177         << endl;
178 
179         for(Lit l: lits) {
180             uint32_t v_inter = solver->map_outer_to_inter(l.var());
181             cout << "Value of " << l << " : " << solver-> model_value(l)
182             << " removed: " << removed_type_to_string(solver->varData[v_inter].removed)
183             << endl;
184         }
185     }
186     assert(solver->model_value(blockedOn) == l_Undef);
187 
188     //satisfy this one clause
189     Lit actual_lit = lit_Undef;
190     for(Lit l: lits) {
191         lbool model_value = solver-> model_value(l);
192         assert(model_value != l_True);
193         if (l.var() == blockedOn) {
194             actual_lit = l;
195         } else {
196             if (model_value == l_Undef) {
197             } else {
198                 assert(model_value == l_False);
199             }
200         }
201     }
202     assert(actual_lit != lit_Undef);
203     lbool val = actual_lit.sign() ? l_False : l_True;
204     solver->model[blockedOn] = val;
205 
206     if (solver->conf.verbosity >= 10) {
207         cout << "Extending VELIM cls. -- setting model for var "
208         << blockedOn + 1 << " to " << solver->model[blockedOn] << endl;
209     }
210     solver->varReplacer->extend_model(blockedOn);
211 
212     assert(satisfied(lits));
213 
214     //it's been set now
215     return true;
216 }
217