gistfile1.cpp

void test_forall_with_uninterpreted_function()
 {
   Z3_config cfg = Z3_mk_config();
	 Z3_context ctx = Z3_mk_context( cfg ) ;	

	 Z3_sort  int_sort = Z3_mk_int_sort(ctx);
	 Z3_sort  bool_sort = Z3_mk_bool_sort(ctx);

	 string _next_org_name = "func1";
	 string _next_name = "func2"; 

	 Z3_symbol next_name ;
	 Z3_symbol next_org_name;
	 Z3_sort domain_next[2];
	 Z3_sort domain[1];

	 next_name = Z3_mk_string_symbol(ctx, _next_name.c_str()) ;
	 next_org_name = Z3_mk_string_symbol(ctx, _next_org_name.c_str()) ;

	 domain[0]=bool_sort;
	 domain_next[0] = bool_sort;
	 domain_next[1] = int_sort;

	 Z3_func_decl func1 = Z3_mk_func_decl(ctx,next_org_name,1,domain,bool_sort);
	 Z3_func_decl func2 = Z3_mk_func_decl(ctx, next_name, 2, domain_next, bool_sort );

	 Z3_ast one_ast;
	 Z3_ast zero_ast; 

	 one_ast = mk_int(ctx,1);  // 1
	 zero_ast = mk_int(ctx,0); //0

	 Z3_ast _ii_1_ast ;

	 Z3_ast tmp[2];

	 Z3_ast fun_arg_ast [] = { Z3_mk_bound(ctx,0,int_sort) };

	 tmp[0] =  fun_arg_ast[0];
	 tmp[1] =  one_ast;
	 _ii_1_ast = Z3_mk_sub(ctx, 2, tmp); 

	 Z3_ast part[11];

	 part[0] = Z3_mk_gt(ctx,fun_arg_ast[1], one_ast) ; 

	 tmp[1] = fun_arg_ast[0];
	 Z3_ast p_ast = mk_var(ctx,"pp",bool_sort);
	 tmp[0]=p_ast;

	 part[1] = Z3_mk_app(ctx,func2, 2, tmp);   // func2(p, i)



	 tmp[0] = p_ast;
	 tmp[1] = _ii_1_ast;
	 Z3_ast tmp_ast; 
	 tmp_ast = Z3_mk_app(ctx, func2, 2, tmp);  
	 Z3_ast han_tmp_ast=Z3_mk_app(ctx, func1, 1, tmp);

	 tmp[0] = tmp_ast;
	 part[2] = Z3_mk_app(ctx, func1, 1, tmp);
	 hyh_new<<"part[2]定义完毕！！！"<<endl;

	 part[3] = Z3_mk_eq(ctx, part[1], part[2] );    

	 part[4] = Z3_mk_implies(ctx, part[0], part[3]); //

	 part[5] = Z3_mk_eq(ctx, fun_arg_ast[0], one_ast);   // i == 0 

	 part[6] = Z3_mk_eq(ctx, part[1], han_tmp_ast);


	 part[7] = Z3_mk_implies(ctx,part[5], part[6]);//  i==0 => _next(_pp, _ii) == _pp)					


	 string str_pp="pp", str_ii="ii";
	 Z3_symbol * sym = new Z3_symbol[2];  
	 sym[0] = Z3_mk_string_symbol(ctx, str_pp.c_str());
	 sym[1] = Z3_mk_string_symbol(ctx, str_ii.c_str());

	 Z3_ast fuck2 [] = {mk_var(ctx,"pp",bool_sort),one_ast};
	 Z3_ast fuck1 [] = {mk_var(ctx,"pp",bool_sort)};
	 part[8] = Z3_mk_eq(ctx,
		 Z3_mk_app(ctx,func2,2,fuck2),
		 Z3_mk_app(ctx,func1,1,fuck1)
		 ); 

	 Z3_sort fuck3 [] = { int_sort };
	 Z3_symbol fuck4 [] = { Z3_mk_string_symbol(ctx,"ii") };
	 part[9] = Z3_mk_forall(ctx,0,0,NULL,1,fuck3,fuck4,part[4]);

	 tmp[0] = part[8];
	 tmp[1] = part[9];

	 Z3_ast finall_ast =Z3_mk_and(ctx,2,tmp);

	 Z3_ast var_p=mk_var(ctx,"p",bool_sort);
	 Z3_ast var_q=mk_var(ctx,"q",bool_sort);
	 Z3_ast var_m=mk_var(ctx,"m",int_sort);
	 Z3_ast cons_Z=mk_var(ctx,"Z",bool_sort);

	 tmp[0] =  var_m;
	 tmp[1] =  one_ast;
	 Z3_ast  m_1_ast = Z3_mk_sub(ctx, 2, tmp); 
	 Z3_ast var_i;
	 var_i = Z3_mk_bound( ctx ,0 , int_sort);

	 Z3_ast args[2] ;
	 args[0] = Z3_mk_ge( ctx ,var_i, one_ast  );
	 args[1] = Z3_mk_le( ctx ,var_i ,var_m );
	 Z3_ast prefix0 = Z3_mk_and( ctx , 2 , args );

	 args[1] = Z3_mk_le( ctx ,var_i ,m_1_ast );
	 Z3_ast prefix1 = Z3_mk_and( ctx , 2 , args );


	 Z3_symbol var_sym=Z3_mk_string_symbol(ctx,"i");
	 Z3_sort types[1]; 
	 Z3_symbol  names[1]; 
	 types[0] = int_sort;
	 names[0] = var_sym;

	 tmp[0]=var_p;tmp[1]=var_i;
	 Z3_ast body_p=Z3_mk_app(ctx,func2,2,tmp);
	 tmp[0]=var_q;tmp[1]=var_i;
	 Z3_ast body_q=Z3_mk_app(ctx,func2,2,tmp);
	 Z3_ast tmp1[1]; 
	 tmp1[0]=var_p;
	 Z3_ast q_eq_func1_p = Z3_mk_eq(ctx,var_q, Z3_mk_app(ctx,func1,1,tmp1) );//q==func1(p)

	 part[1] = Z3_mk_eq(ctx, body_p,cons_Z);
	 part[2] = Z3_mk_implies(ctx,prefix0, part[1]);
	 part[3] =  Z3_mk_forall(ctx, 0, 0, NULL, 1,types ,names,part[2] ); 

	 tmp[0]=q_eq_func1_p;
	 tmp[1]=part[3];
	 part[4] = Z3_mk_and( ctx , 2 , tmp );

	 part[5] = Z3_mk_eq(ctx, body_q,cons_Z);
	 part[6] = Z3_mk_implies(ctx,prefix1, part[5]);
	 part[7] =  Z3_mk_forall(ctx, 0, 0, NULL, 1,types ,names,part[6] ); 

	 Z3_ast to_prove0 = Z3_mk_implies(ctx,part[4], part[7]);
	 Z3_ast to_prove = Z3_mk_implies(ctx,finall_ast,to_prove0);

	 hyh_new<<endl<<Z3_ast_to_string(ctx,to_prove);

	 Z3_push(ctx);
	 Z3_assert_cnstr(ctx,Z3_mk_not(ctx,to_prove));
	 Z3_model* model=new Z3_model();
	 switch (Z3_check_and_get_model(ctx,model)  ) {  

	 case Z3_L_FALSE:
		 /* proved */
		 cout << "true"<<endl<<endl;
		 break;

	 case Z3_L_UNDEF:
		 /* Z3 failed to prove/disprove f. */
		 cout << "undefined"<<endl<<endl;
		 break;

	 case Z3_L_TRUE:
		 cout << "false"<<endl<<endl;

		 break;
	 }
	 Z3_pop(ctx, 1);
	 Z3_del_config( cfg );
	 Z3_del_context( ctx );
 }