adding labels to duality

src/duality/duality.h

@@ -622,11 +622,20 @@ namespace Duality {
 	  
       */
       
+      struct label_struct {
+	symbol name;
+	expr value;
+	bool pos;
+	label_struct(const symbol &s, const expr &e, bool b)
+	: name(s), value(e), pos(b) {}
+      };
+
       
 #ifdef WIN32
        __declspec(dllexport)
 #endif
-	 void FromClauses(const std::vector<Term> &clauses);
+	 void FromClauses(const std::vector<Term> &clauses,
+			 std::vector<std::vector<label_struct> > &clause_labels);
 
        void FromFixpointContext(fixedpoint fp, std::vector<Term> &queries);
 
@@ -707,10 +716,9 @@ namespace Duality {
 		        std::vector<func_decl> &res,
                         std::vector<Node *> &nodes);
 
+      Term RemoveLabelsRec(hash_map<ast,Term> &memo, const Term &t, std::vector<label_struct> &lbls);
 
-      Term RemoveLabelsRec(hash_map<ast,Term> &memo, const Term &t);
+      Term RemoveLabels(const Term &t, std::vector<label_struct > &lbls);
-
-      Term RemoveLabels(const Term &t);
 
       Term GetAnnotation(Node *n);
 

src/duality/duality_rpfp.cpp

@@ -1631,34 +1631,39 @@ namespace Duality {
       && t.num_args() == 0;
   }
 
-  RPFP::Term RPFP::RemoveLabelsRec(hash_map<ast,Term> &memo, const Term &t){
+  RPFP::Term RPFP::RemoveLabelsRec(hash_map<ast,Term> &memo, const Term &t, 
+				   std::vector<label_struct > &lbls){
     if(memo.find(t) != memo.end())
       return memo[t];
     Term res(ctx);
     if (t.is_app()){
       func_decl f = t.decl();
-      if(t.num_args() == 1 && f.name().str().substr(0,3) == "lbl"){
+      std::vector<symbol> names;
-	res = RemoveLabelsRec(memo,t.arg(0));
+      bool pos;
+      if(t.is_label(pos,names)){
+	res = RemoveLabelsRec(memo,t.arg(0),lbls);
+	for(unsigned i = 0; i < names.size(); i++)
+	  lbls.push_back(label_struct(names[i],res,pos));
       }
       else {
 	int nargs = t.num_args();
 	std::vector<Term> args;
 	for(int i = 0; i < nargs; i++)
-	  args.push_back(RemoveLabelsRec(memo,t.arg(i)));
+	  args.push_back(RemoveLabelsRec(memo,t.arg(i),lbls));
 	res = f(nargs,&args[0]);
       }
     }
     else if (t.is_quantifier())
-      res = CloneQuantifier(t,RemoveLabelsRec(memo,t.body()));
+      res = CloneQuantifier(t,RemoveLabelsRec(memo,t.body(),lbls));
     else
       res = t;
     memo[t] = res;
     return res;
   }
 
-  RPFP::Term RPFP::RemoveLabels(const Term &t){
+  RPFP::Term RPFP::RemoveLabels(const Term &t, std::vector<label_struct > &lbls){
     hash_map<ast,Term> memo ;
-    return RemoveLabelsRec(memo,t);
+    return RemoveLabelsRec(memo,t,lbls);
   }
 
   Z3User::Term Z3User::SubstBoundRec(hash_map<int,hash_map<ast,Term> > &memo, hash_map<int,Term> &subst, int level, const Term &t)
@@ -1733,7 +1738,8 @@ namespace Duality {
 			    arg.decl().get_decl_kind() == Uninterpreted);
   }
 
-  void RPFP::FromClauses(const std::vector<Term> &unskolemized_clauses){
+  void RPFP::FromClauses(const std::vector<Term> &unskolemized_clauses,
+			 std::vector<std::vector<label_struct> > &clause_labels){
     hash_map<func_decl,Node *> pmap;
     func_decl fail_pred = ctx.fresh_func_decl("@Fail", ctx.bool_sort());
     
@@ -1800,6 +1806,7 @@ namespace Duality {
 
     // create the edges
 
+    clause_labels.resize(clauses.size());
     for(unsigned i = 0; i < clauses.size(); i++){
       Term clause = clauses[i];
       Term body = clause.arg(0);
@@ -1830,7 +1837,7 @@ namespace Duality {
       hash_map<ast,Term> scan_memo;
       std::vector<Node *> Children;
       body = ScanBody(scan_memo,body,pmap,Relparams,Children);
-      body = RemoveLabels(body);
+      body = RemoveLabels(body,clause_labels[i]);
       body = body.simplify();
 
       // Create the edge

src/duality/duality_wrapper.cpp

@@ -545,6 +545,15 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     a.show();
   }
 
+  bool expr::is_label (bool &pos,std::vector<symbol> &names) const {
+    buffer< ::symbol> _names;
+    bool res = m().is_label(to_expr(raw()),pos,_names);
+    if(res)
+      for(unsigned i = 0; i < _names.size(); i++)
+	names.push_back(symbol(ctx(),_names[i]));
+    return res;
+  }
+
 }
 
 

src/duality/duality_wrapper.h

@@ -454,6 +454,7 @@ namespace Duality {
 	bool is_app() const {return raw()->get_kind() == AST_APP;}
         bool is_quantifier() const {return raw()->get_kind() == AST_QUANTIFIER;}
         bool is_var() const {return raw()->get_kind() == AST_VAR;}
+	bool is_label (bool &pos,std::vector<symbol> &names) const ;
 
         // operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
         func_decl decl() const {return func_decl(ctx(),to_app(raw())->get_decl());}

src/muz_qe/duality_dl_interface.cpp

@@ -52,6 +52,7 @@ namespace Duality {
     
     DualityStatus status;
     std::vector<expr> clauses;
+    std::vector<std::vector<RPFP::label_struct> > clause_labels;
     hash_map<RPFP::Edge *,int> map;  // edges to clauses
     Solver::Counterexample cex;
 
@@ -157,7 +158,7 @@ void dl_interface::check_reset() {
   }
   
   // creates 1-1 map between clauses and rpfp edges
-  _d->rpfp->FromClauses(clauses);
+  _d->rpfp->FromClauses(clauses,_d->clause_labels);
 
   // populate the edge-to-clause map
   for(unsigned i = 0; i < _d->rpfp->edges.size(); ++i)
@@ -256,6 +257,7 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
   }
   out << "  )\n";
   
+
   // reference the proofs of all the children, in syntactic order
   // "true" means the child is not needed