<commit_before>/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    duality_rpfp.h

Abstract:

   implements relational post-fixedpoint problem
   (RPFP) data structure.

Author:

    <NAME> (kenmcmil)

Revision History:


--*/



#include "duality.h"
#include "duality_profiling.h"
#include <algorithm>
#include <fstream>
#include <set>
#include <iterator>

#ifndef WIN32
// #define Z3OPS
#endif

// TODO: do we need these?
#ifdef Z3OPS

class Z3_subterm_truth {
 public:
  virtual bool eval(Z3_ast f) = 0;
  ~Z3_subterm_truth(){}
};

Z3_subterm_truth *Z3_mk_subterm_truth(Z3_context ctx, Z3_model model);

#endif

#include <stdio.h>

// TODO: use something official for this
int debug_gauss = 0;

namespace Duality {

  static char string_of_int_buffer[20];

  const char *Z3User::string_of_int(int n){
    sprintf(string_of_int_buffer,"%d",n);
    return string_of_int_buffer;
  }

  RPFP::Term RPFP::SuffixVariable(const Term &t, int n)
  {
    std::string name = t.decl().name().str() + "_" + string_of_int(n);
    return ctx.constant(name.c_str(), t.get_sort());
  }

  RPFP::Term RPFP::HideVariable(const Term &t, int n)
  {
    std::string name = std::string("@p_") + t.decl().name().str() + "_" + string_of_int(n);
    return ctx.constant(name.c_str(), t.get_sort());
  }

  void RPFP::RedVars(Node *node, Term &b, std::vector<Term> &v)
  {
    int idx = node->number;
    if(HornClauses)
      b = ctx.bool_val(true);
    else {
      std::string name = std::string("@b_") + string_of_int(idx);
      symbol sym = ctx.str_symbol(name.c_str());
      b = ctx.constant(sym,ctx.bool_sort());
    }
    // ctx.constant(name.c_str(), ctx.bool_sort());
    v = node->Annotation.IndParams;
    for(unsigned i = 0; i < v.size(); i++)
      v[i] = SuffixVariable(v[i],idx);
  }

  void Z3User::SummarizeRec(hash_set<ast> &memo, std::vector<expr> &lits, int &ops, const Term &t){
    if(memo.find(t) != memo.end())
      return;
    memo.insert(t);
    if(t.is_app()){
      decl_kind k = t.decl().get_decl_kind();
      if(k == And || k == Or || k == Not || k == Implies || k == Iff){
	ops++;
	int nargs = t.num_args();
	for(int i = 0; i < nargs; i++)
	  SummarizeRec(memo,lits,ops,t.arg(i));
	return;
      }
    }
    lits.push_back(t);
  }

  int Z3User::CumulativeDecisions(){
#if 0
    std::string stats = Z3_statistics_to_string(ctx);
    int pos = stats.find("decisions:");
    pos += 10;
    int end = stats.find('\n',pos);
    std::string val = stats.substr(pos,end-pos);
    return atoi(val.c_str());
#endif
    return slvr.get_num_decisions();
  }


  void Z3User::Summarize(const Term &t){
    hash_set<ast> memo; std::vector<expr> lits; int ops = 0;
    SummarizeRec(memo, lits, ops, t);
    std::cout << ops << ": ";
    for(unsigned i = 0; i < lits.size(); i++){
      if(i > 0) std::cout << ", ";
      std::cout << lits[i];
    }
  }

  int Z3User::CountOperatorsRec(hash_set<ast> &memo, const Term &t){
    if(memo.find(t) != memo.end())
      return 0;
    memo.insert(t);
    if(t.is_app()){
      decl_kind k = t.decl().get_decl_kind();
      if(k == And || k == Or){
	int count = 1;
	int nargs = t.num_args();
	for(int i = 0; i < nargs; i++)
	  count += CountOperatorsRec(memo,t.arg(i));
	return count;
      }
      return 0;
    }
    if(t.is_quantifier())
      return CountOperatorsRec(memo,t.body())+1;
    return 0;
  }

  int Z3User::CountOperators(const Term &t){
    hash_set<ast> memo;
    return CountOperatorsRec(memo,t);
  }


  Z3User::Term Z3User::conjoin(const std::vector<Term> &args){
    return ctx.make(And,args);
  }
  
  Z3User::Term Z3User::sum(const std::vector<Term> &args){
    return ctx.make(Plus,args);
  }

  RPFP::Term RPFP::RedDualRela(Edge *e, std::vector<Term> &args, int idx){
    Node *child = e->Children[idx];
    Term b(ctx);
    std::vector<Term> v;
    RedVars(child, b, v);
    for (unsigned i = 0; i < args.size(); i++)
      {
	if (eq(args[i].get_sort(),ctx.bool_sort()))<commit_msg>fussing more with qe in duality<commit_after>/*++
Copyright (c) 2012 Microsoft Corporation

Module Name:

    duality_rpfp.h

Abstract:

   implements relational post-fixedpoint problem
   (RPFP) data structure.

Author:

    <NAME> (kenmcmil)

Revision History:


--*/



#include "duality.h"
#include "duality_profiling.h"
#include <algorithm>
#include <fstream>
#include <set>
#include <iterator>

#ifndef WIN32
// #define Z3OPS
#endif

// TODO: do we need these?
#ifdef Z3OPS

class Z3_subterm_truth {
 public:
  virtual bool eval(Z3_ast f) = 0;
  ~Z3_subterm_truth(){}
};

Z3_subterm_truth *Z3_mk_subterm_truth(Z3_context ctx, Z3_model model);

#endif

#include <stdio.h>

// TODO: use something official for this
int debug_gauss = 0;

namespace Duality {

  static char string_of_int_buffer[20];

  const char *Z3User::string_of_int(int n){
    sprintf(string_of_int_buffer,"%d",n);
    return string_of_int_buffer;
  }

  RPFP::Term RPFP::SuffixVariable(const Term &t, int n)
  {
    std::string name = t.decl().name().str() + "_" + string_of_int(n);
    return ctx.constant(name.c_str(), t.get_sort());
  }

  RPFP::Term RPFP::HideVariable(const Term &t, int n)
  {
    std::string name = std::string("@p_") + t.decl().name().str() + "_" + string_of_int(n);
    return ctx.constant(name.c_str(), t.get_sort());
  }

  void RPFP::RedVars(Node *node, Term &b, std::vector<Term> &v)
  {
    int idx = node->number;
    if(HornClauses)
      b = ctx.bool_val(true);
    else {
      std::string name = std::string("@b_") + string_of_int(idx);
      symbol sym = ctx.str_symbol(name.c_str());
      b = ctx.constant(sym,ctx.bool_sort());
    }
    // ctx.constant(name.c_str(), ctx.bool_sort());
    v = node->Annotation.IndParams;
    for(unsigned i = 0; i < v.size(); i++)
      v[i] = SuffixVariable(v[i],idx);
  }

  void Z3User::SummarizeRec(hash_set<ast> &memo, std::vector<expr> &lits, int &ops, const Term &t){
    if(memo.find(t) != memo.end())
      return;
    memo.insert(t);
    if(t.is_app()){
      decl_kind k = t.decl().get_decl_kind();
      if(k == And || k == Or || k == Not || k == Implies || k == Iff){
	ops++;
	int nargs = t.num_args();
	for(int i = 0; i < nargs; i++)
	  SummarizeRec(memo,lits,ops,t.arg(i));
	return;
      }
    }
    lits.push_back(t);
  }

  int Z3User::CumulativeDecisions(){
#if 0
    std::string stats = Z3_statistics_to_string(ctx);
    int pos = stats.find("decisions:");
    pos += 10;
    int end = stats.find('\n',pos);
    std::string val = stats.substr(pos,end-pos);
    return atoi(val.c_str());
#endif
    return slvr.get_num_decisions();
  }


  void Z3User::Summarize(const Term &t){
    hash_set<ast> memo; std::vector<expr> lits; int ops = 0;
    SummarizeRec(memo, lits, ops, t);
    std::cout << ops << ": ";
    for(unsigned i = 0; i < lits.size(); i++){
      if(i > 0) std::cout << ", ";
      std::cout << lits[i];
    }
  }

  int Z3User::CountOperatorsRec(hash_set<ast> &memo, const Term &t){
    if(memo.find(t) != memo.end())
      return 0;
    memo.insert(t);
    if(t.is_app()){
      decl_kind k = t.decl().get_decl_kind();
      if(k == And || k == Or){
	int count = 1;
	int nargs = t.num_args();
	for(int i = 0; i < nargs; i++)
	  count += CountOperatorsRec(memo,t.arg(i));
	return count;
      }
      return 0;
    }
    if(t.is_quantifier())
      return CountOperatorsRec(memo,t.body())+2; // count 2 for a quantifier
    return 0;
  }

  int Z3User::CountOperators(const Term &t){
    hash_set<ast> memo;
    return CountOperatorsRec(memo,t);
  }


  Z3User::Term Z3User::conjoin(const std::vector<Term> &args){
    return ctx.make(And,args);
  }
  
  Z3User::Term Z3User::sum(const std::vector<Term> &args){
    return ctx.make(Plus,args);
  }

  RPFP::Term RPFP::RedDualRela(Edge *e, std::vector<Term> &args, int idx){
    Node *child = e->Children[idx];
    Term b(ctx);
    std::vector<Term> v;
    RedVars(child, b, v);
    for (unsigned i = 0; i < args.size(); i++)
      {
	if (eq(args[i].get_sort(),ctx.bool_sort()))
{'fraction_non_alphanumeric': 0.1779171894604768, 'fraction_numerical': 0.011417816813048933, 'mean_word_length': 3.355737704918033, 'pattern_counts': {'":': 2, '<': 63, '<?xml version=': 0, '>': 45, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4305383', 'n_tokens_mistral': 3224, 'n_tokens_neox': 3113, 'n_words': 661}