added code for ctg_state lifting that ignores constraints

diffblue · Jun 18, 2017 · a8d913d · a8d913d
1 parent 8b1bce5
commit a8d913d
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 10 deletions.
diff --git a/src/ic3/c5tg.cc b/src/ic3/c5tg.cc
@@ -81,8 +81,11 @@ void CompInfo::lift_ctg_state(CUBE &Ctg_cube,CUBE &Ctg_st,CUBE &Inps,
   add_assumps1(Assmps,Inps);
 
 
-  Mlit act_lit;  
-  add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube);
+  Mlit act_lit;
+  if (standard_mode) 
+    add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube,false);
+  else
+    add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube,true);
 
   Assmps.push(act_lit);
   add_assumps2(Assmps,Ctg_st);

diff --git a/src/ic3/l0ift_states.cc b/src/ic3/l0ift_states.cc
@@ -42,7 +42,7 @@ void CompInfo::lift_good_state(CUBE &Gst_cube,CUBE &Prs_st,
 
 
   Mlit act_lit;  
-  add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube);
+  add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube,true);
 
   Assmps.push(act_lit);
 
@@ -139,7 +139,7 @@ void CompInfo::gen_state_cube(CUBE &St_cube,CUBE &St,SatSolver &Slvr)
   A D D _ C L S _ E X C L _ S T _ C U B E
 
   ===========================================*/
-void CompInfo::add_cls_excl_st_cube(Mlit &act_lit,SatSolver &Slvr,CUBE &St)
+void CompInfo::add_cls_excl_st_cube(Mlit &act_lit,SatSolver &Slvr,CUBE &St,bool add_cnstr_lits)
 {
   CLAUSE C;
   act_lit = IctMinisat::mkLit(Slvr.Mst->newVar(),false);
@@ -155,12 +155,17 @@ void CompInfo::add_cls_excl_st_cube(Mlit &act_lit,SatSolver &Slvr,CUBE &St)
 
   // add literals constraining internal variables
 
-  for (size_t i=0; i < Tr_coi_lits.size(); i++) {
-    int lit = Tr_coi_lits[i];
-    int var_ind = abs(lit)-1;
-    assert (Var_info[var_ind].type == INTERN);
-    C.push_back(-lit);
+  if (add_cnstr_lits) {
+    SCUBE::iterator pnt;
+    for (pnt = Constr_nilits.begin(); pnt != Constr_nilits.end(); pnt++) {
+      int lit = *pnt;
+      int var_ind = abs(lit)-1;
+      if (Var_info[var_ind].type != INTERN) continue;
+      C.push_back(-lit);
+    }
   }
+
+
 
   accept_new_clause(Slvr,C);
 

diff --git a/src/ic3/m2ethods.hh b/src/ic3/m2ethods.hh
@@ -128,7 +128,7 @@ bool check_sat2(SatSolver &Slvr,MvecLits &Assmps);
 void add_negated_assumps1(MvecLits &Assmps,CLAUSE &C);
 void add_negated_assumps2(MvecLits &Assmps,CLAUSE &C,bool sort);
 void gen_assump_clause(CLAUSE &C,SatSolver &Slvr,MvecLits &Assmps);
-void add_cls_excl_st_cube(Mlit &act_lit,SatSolver &Slvr,CUBE &St);
+void add_cls_excl_st_cube(Mlit &act_lit,SatSolver &Slvr,CUBE &St,bool add_cnstr_lits);
 void add_temp_clause(Mlit &act_lit,SatSolver &Slvr,CLAUSE &C);
 void simplify_tf_solvers();
 void print_tf_assgns(int tf_ind);