Merge dfe48b0 into 827cd9c

Makefile.build

@@ -87,7 +87,7 @@ MKVERSION=./utils/make_source_version
 srcdir = src
 srcsubdirs = mt io terms utils solvers solvers/floyd_warshall \
     solvers/funs solvers/bv solvers/egraph solvers/cdcl solvers/simplex solvers/quant \
-    parser_utils model scratch api frontend frontend/common \
+    parser_utils model api frontend frontend/common \
     frontend/smt1 frontend/yices frontend/smt2 context exists_forall \
     mcsat mcsat/eq mcsat/weq mcsat/uf mcsat/bool mcsat/ite mcsat/nra mcsat/bv \
     mcsat/bv/explain mcsat/utils

src/Makefile

@@ -436,9 +436,6 @@ extra_src_c := \
 	model/large_bvsets.c \
 	model/rb_bvsets.c \
 	model/small_bvsets.c \
-	scratch/booleq_table.c \
-	scratch/bool_vartable.c \
-	scratch/update_graph.c \
 	solvers/bv/bvsolver_printer.c \
 	solvers/cdcl/clause_pool.c \
 	solvers/cdcl/gates_printer.c \

src/solvers/cdcl/smt_core.c

@@ -1588,7 +1588,8 @@ void init_smt_core(smt_core_t *s, uint32_t n, void *th,
   init_checkpoint_stack(&s->checkpoints);
   s->cp_flag = false;
 
-  s->etable = NULL;
+  // EXPERIMENTAL
+  // s->etable = NULL;
   s->trace = NULL;
 
   s->interrupt_push = false;

src/solvers/cdcl/smt_core.h

@@ -63,7 +63,7 @@
 
 
 // EXPERIMENTAL
-#include "scratch/booleq_table.h"
+// #include "scratch/booleq_table.h"
 
 
 /***********
@@ -1051,7 +1051,7 @@ typedef struct smt_core_s {
   bool cp_flag;  // set true when backtracking. false when checkpoints are added
 
   /* EXPERIMENTAL (default to NULL) */
-  booleq_table_t *etable;
+  // booleq_table_t *etable;
 
   /* Tracer object (default to NULL) */
   tracer_t *trace;