How to add additional variables to the solver

[arey0pushpa]

I'm trying to check properties about arrays (lets say at least one is true in the whole array or a trivial sorting).

1. As far i can see i can talk about quantified variables i,j,k. But how to represent assertions about the array such that the quantified variables are indexes of the array. for i for j > i a[j] > a[i]. I can build the Boolean variable B1. Using _Bool B1 = false and iterate over array elements and make sure that B1 = B1 && a[j] > a[i] but how can i add assert(B1 == true) to the solver ? i.e a[i] such that B1 is true. Unable to code it in last few hours.

2. How can i quantify over boolean functions ?

3. How can specify facts about the code ? Something of this kind. __CPROVER_assume(__CPROVER_forall { int i; (i>=0 && i<5) ==> b[i]==a[i]});

In your directory provided examples are great, please add more to those.

One additional type that i can think of now (assert (not (forall ((a (Array Int Int)) (b (Array Int Int))) (=> (forall ((i Int)) (= (select a i) (select b i))) (= a b))))) (check-sat) Like in Z3 ? how should i achieve same here ?

Thanks,

[lonsing]

Hi, In DepQBF, there is no way to directly specify constraints over arrays or functions because DepQBF accepts only quantified Boolean formulas in prenex conjunctive normal form over propositional variables as input. That is, properties about arrays and functions must be manually encoded as propositional formula.

The QDIMACS format that DepQBF accepts as input allows only to specify formulas in prenex conjunctive normal form over Boolean variables.

Florian