fixing labels in duality

src/duality/duality.h

@@ -434,6 +434,7 @@ namespace Duality {
 	hash_map<func_decl,int> relMap;
 	hash_map<ast,Term> varMap;
 	Edge *map;
+	Term labeled;
 	
       Edge(Node *_Parent, const Transformer &_F, const std::vector<Node *> &_Children, RPFP *_owner, int _number)
 	: F(_F), Parent(_Parent), Children(_Children), dual(expr(_owner->ctx)) {
@@ -634,8 +635,7 @@ namespace Duality {
 #ifdef WIN32
        __declspec(dllexport)
 #endif
-	 void FromClauses(const std::vector<Term> &clauses,
-			 std::vector<std::vector<label_struct> > &clause_labels);
+       void FromClauses(const std::vector<Term> &clauses);
 
        void FromFixpointContext(fixedpoint fp, std::vector<Term> &queries);
 
@@ -674,6 +674,10 @@ namespace Duality {
 
       int EvalTruth(hash_map<ast,int> &memo, Edge *e, const Term &f);
 
+      void GetLabels(Edge *e, std::vector<symbol> &labels);
+
+      int GetLabelsRec(hash_map<ast,int> *memo, const Term &f, std::vector<symbol> &labels, bool labpos);
+
     private:
       
 

src/duality/duality_rpfp.cpp

@@ -838,6 +838,95 @@ namespace Duality {
     return SubtermTruth(memo,tl);
   }
 
+  /** Compute truth values of all boolean subterms in current model.
+      Assumes formulas has been simplified by Z3, so only boolean ops
+      ands and, or, not. Returns result in memo. 
+  */
+
+  int RPFP::GetLabelsRec(hash_map<ast,int> *memo, const Term &f, std::vector<symbol> &labels, bool labpos){
+    if(memo[labpos].find(f) != memo[labpos].end()){
+      return memo[labpos][f];
+    }
+    int res;
+    if(f.is_app()){
+      int nargs = f.num_args();
+      decl_kind k = f.decl().get_decl_kind();
+      if(k == Implies){
+	res = GetLabelsRec(memo,!f.arg(0) || f.arg(1), labels, labpos);
+	goto done;
+      }
+      if(k == And) {
+	res = 1; 
+	for(int i = 0; i < nargs; i++){
+	  int ar = GetLabelsRec(memo,f.arg(i), labels, labpos);
+	  if(ar == 0){
+	    res = 0;
+	    goto done;
+	  }
+	  if(ar == 2)res = 2; 
+	}
+	goto done;
+      }
+      else if(k == Or) {
+	res = 0;
+	for(int i = 0; i < nargs; i++){
+	  int ar = GetLabelsRec(memo,f.arg(i), labels, labpos);
+	  if(ar == 1){
+	    res = 1;
+	    goto done;
+	  }
+	  if(ar == 2)res = 2; 
+	}
+	goto done;
+      }
+      else if(k == Not) {
+	int ar = GetLabelsRec(memo,f.arg(0), labels, !labpos);
+	res = (ar == 0) ? 1 : ((ar == 1) ? 0 : 2);
+	goto done;
+      }
+    }
+    {
+      bool pos; std::vector<symbol> names;
+      if(f.is_label(pos,names)){
+	res = GetLabelsRec(memo,f.arg(0), labels, labpos);
+	if(pos == labpos && res == (pos ? 1 : 0))
+	  for(unsigned i = 0; i < names.size(); i++)
+	    labels.push_back(names[i]);
+	goto done;
+      }
+    }
+    {
+      expr bv = dualModel.eval(f);
+      if(bv.is_app() && bv.decl().get_decl_kind() == Equal && 
+	 bv.arg(0).is_array()){
+	bv = EvalArrayEquality(bv);
+      }
+      // Hack!!!! array equalities can occur negatively!
+      if(bv.is_app() && bv.decl().get_decl_kind() == Not && 
+	 bv.arg(0).decl().get_decl_kind() == Equal &&
+	 bv.arg(0).arg(0).is_array()){
+	bv = dualModel.eval(!EvalArrayEquality(bv.arg(0)));
+      }
+      if(eq(bv,ctx.bool_val(true)))
+	res = 1;
+      else if(eq(bv,ctx.bool_val(false)))
+	res = 0;
+      else
+	res = 2;
+    }
+  done:
+    memo[labpos][f] = res;
+    return res;
+  }
+
+  void RPFP::GetLabels(Edge *e, std::vector<symbol> &labels){
+    if(!e->map || e->map->labeled.null())
+      return;
+    Term tl = Localize(e, e->map->labeled);
+    hash_map<ast,int> memo[2];
+    GetLabelsRec(memo,tl,labels,true);
+  }
+
 #ifdef Z3OPS
   static Z3_subterm_truth *stt;
 #endif
@@ -1742,8 +1831,7 @@ namespace Duality {
 			    arg.decl().get_decl_kind() == Uninterpreted);
   }
 
-  void RPFP::FromClauses(const std::vector<Term> &unskolemized_clauses,
-			 std::vector<std::vector<label_struct> > &clause_labels){
+  void RPFP::FromClauses(const std::vector<Term> &unskolemized_clauses){
     hash_map<func_decl,Node *> pmap;
     func_decl fail_pred = ctx.fresh_func_decl("@Fail", ctx.bool_sort());
     
@@ -1810,7 +1898,6 @@ 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);
@@ -1841,13 +1928,15 @@ namespace Duality {
       hash_map<ast,Term> scan_memo;
       std::vector<Node *> Children;
       body = ScanBody(scan_memo,body,pmap,Relparams,Children);
-      body = RemoveLabels(body,clause_labels[i]);
+      Term labeled = body;
+      std::vector<label_struct > lbls;  // TODO: throw this away for now
+      body = RemoveLabels(body,lbls);
       body = body.simplify();
 
       // Create the edge
       Transformer T = CreateTransformer(Relparams,Indparams,body);
-      // Edge *edge = 
-      CreateEdge(Parent,T,Children);
+      Edge *edge = CreateEdge(Parent,T,Children);
+      edge->labeled = labeled;; // remember for label extraction
       // edges.push_back(edge);
     }
   }

src/duality/duality_wrapper.cpp

@@ -25,6 +25,7 @@ Revision History:
 #include "statistics.h"
 #include "expr_abstract.h"
 #include "stopwatch.h"
+#include "model_smt2_pp.h"
 
 namespace Duality {
 
@@ -534,18 +535,20 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     std::cout << mk_pp(raw(), m()) << std::endl;
   }
 
-#if 0
   void model::show() const {
-    std::cout << Z3_model_to_string(ctx(), m_model) << std::endl;
+    model_smt2_pp(std::cout, m(), *m_model, 0);
+    std::cout << std::endl;
   }
   
-  Z3_ast ast_to_track = 0;
-#endif
 
   void include_ast_show(ast &a){
     a.show();
   }
 
+  void include_model_show(model &a){
+    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);

src/muz_qe/duality_dl_interface.cpp

@@ -161,7 +161,7 @@ void dl_interface::check_reset() {
   }
   
   // creates 1-1 map between clauses and rpfp edges
-  _d->rpfp->FromClauses(clauses,_d->clause_labels);
+  _d->rpfp->FromClauses(clauses);
 
   // populate the edge-to-clause map
   for(unsigned i = 0; i < _d->rpfp->edges.size(); ++i)
@@ -265,16 +265,12 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp
   out << "  )\n";
   
   out << "  (labels";
-  std::vector<RPFP::label_struct> &labels = d->dd()->clause_labels[orig_clause];
-  {
-    hash_map<ast,int> memo;
-    for(unsigned j = 0; j < labels.size(); j++){
-      RPFP::label_struct &lab = labels[j];
-      int truth = cex.tree->EvalTruth(memo,&edge,lab.value);
-      if(truth == 1 && lab.pos || truth == 0 && !lab.pos)
-	out << " " << lab.name;
-    }
+  std::vector<symbol> labels;
+  cex.tree->GetLabels(&edge,labels);
+  for(unsigned j = 0; j < labels.size(); j++){
+    out << " " << labels[j];
   }
+  
   out << "  )\n";
 
   // reference the proofs of all the children, in syntactic order