1- /*
2- * comp_archetype.h
3- *
4- * Created on: Feb 9, 2013
5- * Author: mthurley
6- */
1+ /* *****************************************
2+ Copyright (C) 2023 Authors of GANAK, see AUTHORS file
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+ ***********************************************/
722
823#pragma once
924
1025#include < cstring>
11- #include < algorithm>
1226#include < iostream>
27+ #include < limits>
1328
1429#include " ../common.hpp"
1530#include " comp.hpp"
1631#include " cacheable_comp.hpp"
1732
33+ using std::numeric_limits;
1834using std::cout;
1935using std::endl;
2036
2137namespace GanakInt {
2238
23- // State values for variables found during comp analysis (CA)
24- #define CA_VAR_IN_SUP_COMP_UNVISITED 1
25- #define CA_VAR_VISITED 2
26- #define CA_VAR_IN_PEER_COMP 4
27- // 1 + 2 + 4 == 7
28- #define CA_VAR_MASK 7
29-
30- #define CA_CL_IN_SUP_COMP_UNVISITED 8
31- #define CA_CL_VISITED 16
32- #define CA_CL_IN_PEER_COMP 32
33- /* #define WHATEVER 64 */
34- // 64+32+16+8 == 120
35- #define CA_CL_MASK 120
36-
3739class StackLevel ;
3840
3941// There is exactly ONE of this. Inside CompAnalyzer, which is inside CompManager, which is inside Solver
4042class CompArchetype {
4143public:
4244 CompArchetype () = default ;
43- ~CompArchetype () { delete[] data; }
44- CompArchetype (StackLevel &stack_level, const Comp &super_comp) :
45- super_comp_ptr (&super_comp), stack_lvl_ptr(&stack_level) {
46- }
45+ ~CompArchetype () { delete[] raw_data; }
4746
4847 // called every time we want to deal with a new component
4948 void re_initialize (StackLevel &stack_level, const Comp &super_comp) {
@@ -53,92 +52,41 @@ class CompArchetype {
5352 clear_data ();
5453 }
5554
56- const Comp &super_comp () {
57- return *super_comp_ptr;
58- }
59-
60- StackLevel& stack_level () {
61- return *stack_lvl_ptr;
62- }
63-
64- void set_var_in_sup_comp_unvisited (const uint32_t v) {
65- data[v] = CA_VAR_IN_SUP_COMP_UNVISITED | (data[v] & CA_CL_MASK);
66- }
67-
68- void set_var_in_sup_comp_unvisited_raw (const uint32_t v) {
69- data[v] = CA_VAR_IN_SUP_COMP_UNVISITED;
70- }
71-
72- void set_clause_in_sup_comp_unvisited (const ClauseIndex cl) {
73- data[cl] = CA_CL_IN_SUP_COMP_UNVISITED | (data[cl] & CA_VAR_MASK);
74- }
75-
76- void clear_var (const uint32_t v) {
77- data[v] &= CA_CL_MASK;
78- }
79-
80- void clear_cl (const ClauseIndex cl) {
81- data[cl] &= CA_VAR_MASK;
82- }
83-
84- // REMOVES from unseen of super, sets visited
85- void set_var_visited (const uint32_t v) {
86- data[v] = CA_VAR_VISITED | (data[v] & CA_CL_MASK);
87- }
55+ const Comp &super_comp () { return *super_comp_ptr; }
56+ StackLevel& stack_level () { return *stack_lvl_ptr; }
8857
89- void set_clause_visited (const ClauseIndex cl) {
90- clear_cl (cl);
91- data[cl] = CA_CL_VISITED | (data[cl] & CA_VAR_MASK);
92- }
58+ void set_var_visited (const uint32_t v) { v_data[v] = tstamp; }
59+ void set_clause_visited (const ClauseIndex cl) { cl_data[cl] = tstamp; }
9360
94- void set_var_in_peer_comp (const uint32_t v) {
95- data[v] = CA_VAR_IN_PEER_COMP | (data [v] & CA_CL_MASK);
96- }
61+ // bool var_clear (const uint32_t v) { return v_data[v] < tstamp; }
62+ void set_var_clear ( const uint32_t v) { v_data [v] = 0 ; }
63+ void set_cl_clear ( const uint32_t cl) { cl_data[cl] = 0 ; }
9764
98- bool var_in_peer_comp (const uint32_t v) const {
99- return CA_VAR_IN_PEER_COMP & (data[v] & CA_CL_MASK);
100- }
65+ void set_var_in_sup_comp_unvisited (const uint32_t v) { v_data[v] = tstamp-1 ; }
66+ void set_clause_in_sup_comp_unvisited (const ClauseIndex cl) { cl_data[cl] = tstamp-1 ; }
67+ bool var_unvisited_in_sup_comp (uint32_t v) const { return v_data[v] == tstamp-1 ; }
68+ bool clause_unvisited_in_sup_comp (ClauseIndex cl) const { return cl_data[cl] == tstamp-1 ; }
10169
102- void set_clause_in_peer_comp (const ClauseIndex cl) {
103- data[cl] = CA_CL_IN_PEER_COMP | (data[cl] & CA_VAR_MASK);
104- }
105-
106- bool var_visited (const uint32_t v) const {
107- return data[v] & CA_VAR_VISITED;
108- }
109-
110- bool clause_visited (const ClauseIndex cl) const {
111- return data[cl] & CA_CL_VISITED;
112- }
113-
114- bool var_nil (const uint32_t v) const {
115- return (data[v] & CA_VAR_MASK) == 0 ;
116- }
117-
118- bool clause_nil (const ClauseIndex cl) const {
119- return (data[cl] & CA_CL_MASK) == 0 ;
120- }
121-
122- bool var_unvisited_in_sup_comp (uint32_t v) const {
123- return data[v] & CA_VAR_IN_SUP_COMP_UNVISITED;
124- }
125-
126- bool clause_unvisited_in_sup_comp (ClauseIndex cl) const {
127- return data[cl] & CA_CL_IN_SUP_COMP_UNVISITED;
128- }
70+ bool var_visited (const uint32_t v) const { return v_data[v] == tstamp; }
71+ bool clause_visited (const ClauseIndex cl) const { return cl_data[cl] == tstamp; }
12972
13073 // called exactly once during lifetime of counter
13174 void init_data (uint32_t max_var_id, uint32_t max_cl_id) {
132- data_sz = std::max (max_var_id,max_cl_id) + 1 ;
75+ assert (tstamp == 0 );
76+ data_sz = max_var_id +1 + max_cl_id + 1 ;
13377 debug_print (" Creating new data[] of size: " " and zeroing it."
134- data = new uint8_t [data_sz];
78+ raw_data = new uint32_t [data_sz];
79+ memset (raw_data, 0 , data_sz * sizeof (uint32_t ));
80+ v_data = raw_data;
81+ cl_data = raw_data + max_var_id + 1 ;
13582 clear_data ();
13683 }
13784
13885 void clear_data () {
13986 num_long_cls = 0 ;
14087 num_bin_cls = 0 ;
141- memset (data, 0 , data_sz);
88+ tstamp+=2 ;
89+ memset (raw_data, 0 , data_sz * sizeof (uint32_t ));
14290 }
14391
14492 // At this point explore_comp has been called already which
@@ -148,9 +96,12 @@ class CompArchetype {
14896 uint32_t num_long_cls = 0 ;
14997 uint32_t num_bin_cls = 0 ;
15098private:
99+ uint32_t tstamp = 0 ;
151100 Comp const * super_comp_ptr;
152101 StackLevel *stack_lvl_ptr;
153- uint8_t * data = nullptr ; // all variables and all clause IDXs can be indexed here
102+ uint32_t * raw_data = nullptr ;
103+ uint32_t * cl_data = nullptr ;
104+ uint32_t * v_data = nullptr ;
154105 uint32_t data_sz = 0 ;
155106};
156107
0 commit comments