diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 15 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 4 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Alg.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/mtl/BasicHeap.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/mtl/BoxedVec.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Heap.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Map.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Queue.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Sort.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/mtl/Vec.h | 2 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 1 | ||||
-rw-r--r-- | src/prop/sat.h | 4 |
12 files changed, 26 insertions, 14 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 44768009e..611689c2b 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -113,15 +113,12 @@ SatLiteral TseitinCnfStream::handleAtom(TNode node) { bool theoryLiteral = node.getKind() != kind::VARIABLE; SatLiteral lit = newLiteral(node, theoryLiteral); - switch(node.getKind()) { - case TRUE: - assertClause(lit); - break; - case FALSE: - assertClause(~lit); - break; - default: - break; + if(node.getKind() == kind::CONST_BOOLEAN) { + if(node.getConst<bool>()) { + assertClause(lit); + } else { + assertClause(~lit); + } } return lit; diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 131999e38..bf2018338 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -17,16 +17,16 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef __CVC4__PROP__MINISAT__SOLVER_H #define __CVC4__PROP__MINISAT__SOLVER_H -#include "cvc4_private.h" #include "context/context.h" #include <cstdio> #include <cassert> -#include "cvc4_config.h" #include "../mtl/Vec.h" #include "../mtl/Heap.h" #include "../mtl/Alg.h" diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h index 0fe6d84c7..e636f2b87 100644 --- a/src/prop/minisat/mtl/Alg.h +++ b/src/prop/minisat/mtl/Alg.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef CVC4_MiniSat_Alg_h #define CVC4_MiniSat_Alg_h diff --git a/src/prop/minisat/mtl/BasicHeap.h b/src/prop/minisat/mtl/BasicHeap.h index 39d825411..cb6a7cbd8 100644 --- a/src/prop/minisat/mtl/BasicHeap.h +++ b/src/prop/minisat/mtl/BasicHeap.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef CVC4_MiniSat_BasicHeap_h #define CVC4_MiniSat_BasicHeap_h diff --git a/src/prop/minisat/mtl/BoxedVec.h b/src/prop/minisat/mtl/BoxedVec.h index 05b801004..7cf5ba14f 100644 --- a/src/prop/minisat/mtl/BoxedVec.h +++ b/src/prop/minisat/mtl/BoxedVec.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef CVC4_MiniSat_BoxedVec_h #define CVC4_MiniSat_BoxedVec_h diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h index 0c2019b65..20d379b1d 100644 --- a/src/prop/minisat/mtl/Heap.h +++ b/src/prop/minisat/mtl/Heap.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef CVC4_MiniSat_Heap_h #define CVC4_MiniSat_Heap_h diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h index 9168dde0e..715b84da4 100644 --- a/src/prop/minisat/mtl/Map.h +++ b/src/prop/minisat/mtl/Map.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef CVC4_MiniSat_Map_h #define CVC4_MiniSat_Map_h diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h index e02ac7222..291a1f2e3 100644 --- a/src/prop/minisat/mtl/Queue.h +++ b/src/prop/minisat/mtl/Queue.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef CVC4_MiniSat_Queue_h #define CVC4_MiniSat_Queue_h diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h index 2b9d5bb15..19e89803b 100644 --- a/src/prop/minisat/mtl/Sort.h +++ b/src/prop/minisat/mtl/Sort.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef CVC4_MiniSat_Sort_h #define CVC4_MiniSat_Sort_h diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h index fae1d0c5d..364991aa9 100644 --- a/src/prop/minisat/mtl/Vec.h +++ b/src/prop/minisat/mtl/Vec.h @@ -17,6 +17,8 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ +#include "cvc4_private.h" + #ifndef CVC4_MiniSat_Vec_h #define CVC4_MiniSat_Vec_h diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index d699153b2..36f6cb0cb 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -19,7 +19,6 @@ #ifndef __CVC4__PROP_ENGINE_H #define __CVC4__PROP_ENGINE_H -#include "cvc4_config.h" #include "expr/node.h" #include "util/result.h" #include "util/options.h" diff --git a/src/prop/sat.h b/src/prop/sat.h index 93e95eedf..207ed90fd 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -13,11 +13,11 @@ ** SAT Solver. **/ +#include "cvc4_private.h" + #ifndef __CVC4__PROP__SAT_H #define __CVC4__PROP__SAT_H -#include "cvc4_private.h" - #define __CVC4_USE_MINISAT #ifdef __CVC4_USE_MINISAT |