Constrained Horn Clause(CHC)

Abstract Post

From programs to horn clause

using weakest preconditions to translate programs to clauses 

Logic was well understood

Propositional logic < FOL < Higher-order logic etc

Can we conclude Q?

华科网安机试题  

第一题

以下为模拟题

#include <stdio.h>

#include <algorithm>

using namespace std;

unsigned num[1000010]; //数组长度大于10^6，将其定义为全局变量

int main()

{

int i,k,n,num_count=0;

unsigned number;

scanf("%d",&n);

scanf("%d",&k);

for(i=0;i<n;i++)

scanf("%u",&num[i]);

sort(num,num+n); //排序

  number=num[0]-1; //保证number的初始值与num[0]不同

for(i=0;i<n;i++)

{

if(num[i]!=number) //若num[i]与前一个数(number)不同

{

num_count++; //计数

number=num[i]; //更新number

if(num_count==k) break; //找到第k小的数，退出循环

}

}

    printf("%u\n",number);

return 0;

}

#include <bits/stdc++.h>

using namespace std;

const int MAX = 1000005;

int N, M;

string words[MAX], *tree[4 * MAX], init;

inline string* str_max(string *a, string *b){

if(*a > *b) return a;

else return b;

}

void build(int node, int left, int right){

if(left == right){

tree[node] = &words[left];

return;

}

int mid = (left + right) >> 1;

build(node << 1, left, mid);

build(node << 1 | 1, mid + 1, right);

tree[node] = str_max(tree[node << 1], tree[node << 1 | 1]);

return;

} 

string* query(int node, int left, int right, int ql, int qr){

if(ql <= left && qr >= right) return tree[node];

string *res = &init;

int mid = (left + right) >> 1;

if(ql <= mid) res = str_max(res, query(node << 1, left, mid, ql, qr));

if(mid < qr) res = str_max(res, query(node << 1 | 1, mid + 1, right, ql, qr));

return res;

}

int main(){

scanf("%d", &N);

char buf[20];

for(int i = 1; i <= N; i++){

scanf("%s", buf);

words[i] = string(buf);

}

build(1, 1, N);

scanf("%d", &M);

int l, r;

for(int i = 1; i <= M; i++){

scanf("%d%d", &l, &r);

for(auto &ch : *query(1, 1, N, l, r)) putchar(ch);

putchar('\n');