A problem with correctly using C tactics

[gogo9th]

Hi Z3 experts,

I have a trouble with using Z3 APIs. I have the following SMT problem to sholve, which should return -1 (i.e., can't be modelled):

(declare-const cookie String)
(assert (= cookie "name=hello"))
(declare-fun |0 Fill 2|() String)
(declare-fun |0 Fill 3|() String)
(declare-fun |0 Fill 4|() String)
(assert(= |0 Fill 2| "bye"))
(assert (= cookie (str.++ |0 Fill 3| |0 Fill 2| |0 Fill 4|)))

The above problem basically checks if concatenation of |0 Fill 2|, |0 Fill 3|, and |0 Fill 4| can be equal to the string "name=hello" given |0 Fill 2| is "bye". The answer is no.

To verify the above by using Z3, I wrote the following short C program called "simple_z3.c" to solve the above with two tactics: simplify & solve-eqs.

#include <stdio.h>
#include <z3.h>
void main(int argc, char** argv[])
{   Z3_config cfg = Z3_mk_config();
   Z3_context ctx = Z3_mk_context(cfg);

   Z3_tactic tactic0 = Z3_mk_tactic(ctx, "simplify");
   Z3_tactic_inc_ref(ctx,tactic0);

   Z3_tactic tactic1 = Z3_mk_tactic(ctx, "solve-eqs");
   Z3_tactic_inc_ref(ctx,tactic1);

   Z3_tactic finalTactic = Z3_tactic_and_then(ctx, tactic0, tactic1);
   Z3_solver solv = Z3_mk_solver_from_tactic(ctx, finalTactic);

   Z3_solver_from_string(ctx, solv, argv[1]);

   printf("Result: %i\n", Z3_solver_check(ctx, solv));
   Z3_model mdl = Z3_solver_get_model(ctx, solv);
   if (mdl)
      printf("Model: %s\n", Z3_model_to_string(ctx, mdl));
}

If I run the above C code for the above SMT problem, I get the following result:

**:Desktop/Z3$** gcc -o simple_z3 simple_z3.c -lz3
**:Desktop/Z3$** ./simple_z3 "(declare-const cookie String)
(assert (= cookie \"name=hello\"))
(declare-fun |0 Fill 2|() String)
(declare-fun |0 Fill 3|() String)
(declare-fun |0 Fill 4|() String)
(assert(= |0 Fill 2| \"bye\"))
(assert (= cookie (str.++ |0 Fill 3| |0 Fill 2| |0 Fill 4|)))"

======
Result: 0
Model: 0 Fill 2 -> "bye"
cookie -> "name=hello"

The program says the above problem can be modelled. However, this is wrong, I think in my proram something is wrong with the way of using tactics. I need to manually use simplify & solve-eqs tactics (and bit-blast), so by using this simple program I am trying to test if my way of using tactics is correct. Could anybody please help me find out which part of my C code is wrong regarding tactics? I would really appreciate anyone's help.

[NikolajBjorner]

The return value is 0, This corresponds to undefined, per the definition in z3_api.h:

typedef enum { Z3_L_FALSE = -1, Z3_L_UNDEF, Z3_L_TRUE } Z3_lbool;

When the solver returns undef there is no guarantee that a model object can be retrieved. If it is retrieved it will almost for sure not correspond to a satisfying interpretation. In this case, what happens is that the solve-eqs tactic removes cookie and Fill2 and replaces them by their constant solutions. Then every model of the original formula has to agree with these solutions.

There is another issue with the C program: you have to also increment reference counts to solver objects and model objects as soon as they are retrieved. This is so much easier enforced using the C++ layer.

[gogo9th]

Thanks very much for your reply. I fixed the program such that I increment the reference counter for the solver and model right after they are made:

#include <stdio.h>
#include <z3.h>

void main(int argc, char** argv)
{   Z3_config cfg = Z3_mk_config();
   Z3_context ctx = Z3_mk_context(cfg);

   Z3_tactic tactic0 = Z3_mk_tactic(ctx, "simplify");
   Z3_tactic_inc_ref(ctx, tactic0);

   Z3_tactic tactic1 = Z3_mk_tactic(ctx, "solve-eqs");
   Z3_tactic_inc_ref(ctx, tactic1);

   Z3_tactic finalTactic = Z3_tactic_and_then(ctx, tactic0, tactic1);
   //Z3_solver solv = Z3_mk_solver_from_tactic(ctx, finalTactic);
   Z3_solver solv = Z3_mk_solver(ctx);
   Z3_solver_inc_ref(ctx, solv);

   Z3_solver_from_string(ctx, solv, argv[1]);

   printf("Result: %i\n", Z3_solver_check(ctx, solv));
   Z3_model mdl = Z3_solver_get_model(ctx, solv);
   Z3_model_inc_ref(ctx, mdl);
   if (mdl)
      printf("Model: %s\n", Z3_model_to_string(ctx, mdl));
}

But I still get "Result: 0:

:Desktop/Z3$ gcc -o a simple_z3.c -lz3
:Desktop/Z3$ ./a "(declare-const cookie String)
> (assert (= cookie \"name=hello\"))
> (declare-fun |0 Fill 2|() String)
> (declare-fun |0 Fill 3|() String)
> (declare-fun |0 Fill 4|() String)
> (assert(= |0 Fill 2| \"bye\"))
> (assert (= cookie (str.++ |0 Fill 3| |0 Fill 2| |0 Fill 4|)))"
Result: 0
Model: 0 Fill 2 -> "bye"
cookie -> "name=hello"

However, if I don't use my custom tactics and compile the program:

#include <stdio.h>
#include <z3.h>

void main(int argc, char** argv)
{   Z3_config cfg = Z3_mk_config();
   Z3_context ctx = Z3_mk_context(cfg);

   Z3_solver solv = Z3_mk_solver(ctx);
   Z3_solver_inc_ref(ctx, solv);

   Z3_solver_from_string(ctx, solv, argv[1]);

   printf("Result: %i\n", Z3_solver_check(ctx, solv));
   Z3_model mdl = Z3_solver_get_model(ctx, solv);
   Z3_model_inc_ref(ctx, mdl);
   if (mdl)
      printf("Model: %s\n", Z3_model_to_string(ctx, mdl));
}

I get the correct Result -1:

:Desktop/Z3$ ./a "(declare-const cookie String)
(assert (= cookie \"name=hello\"))
(declare-fun |0 Fill 2|() String)
(declare-fun |0 Fill 3|() String)
(declare-fun |0 Fill 4|() String)
(assert(= |0 Fill 2| \"bye\"))
(assert (= cookie (str.++ |0 Fill 3| |0 Fill 2| |0 Fill 4|)))"
Result: -1
Error: there is no current model

Could you please help me identify what is still wrong with my program..? I can't use C++ because my original program is written in C so needs to use these Z3 features in C...

[NikolajBjorner]

In the first program you are creating a solver object from composing two tactics. The two tactics are not complete solvers. They only simplify goals using partial heuristics. So when you use these to reach a verdict of satisfiability on the solver object all they can say is "unknown" in this case. You need to compose with the 'smt' tactic to get anything that can reach more conclusive verdicts.

[gogo9th]

Thanks a lot, now my program can correctly model constraints:

#include <stdio.h>
#include <z3.h>

void main(int argc, char** argv)
{   Z3_config cfg = Z3_mk_config();
   Z3_context ctx = Z3_mk_context(cfg);

   Z3_tactic tactic0 = Z3_mk_tactic(ctx, "simplify");
   Z3_tactic_inc_ref(ctx, tactic0);

   Z3_tactic tactic1 = Z3_mk_tactic(ctx, "solve-eqs");
   Z3_tactic_inc_ref(ctx, tactic1);

   Z3_tactic tactic2 = Z3_mk_tactic(ctx, "smt");
   Z3_tactic_inc_ref(ctx, tactic2);

   Z3_tactic tactic3 = Z3_mk_tactic(ctx, "bit-blast");
   Z3_tactic_inc_ref (ctx, tactic3);

   Z3_tactic tactic4 = Z3_mk_tactic(ctx, "aig");
   Z3_tactic_inc_ref (ctx, tactic4);

   Z3_tactic tactic5 = Z3_mk_tactic(ctx, "sat");
   Z3_tactic_inc_ref (ctx, tactic5);

   Z3_tactic finalTactic = Z3_tactic_and_then(ctx, tactic0, tactic1);
   finalTactic = Z3_tactic_and_then(ctx, finalTactic, tactic2);
   finalTactic = Z3_tactic_and_then(ctx, finalTactic, tactic3);
   finalTactic = Z3_tactic_and_then(ctx, finalTactic, tactic4);
   finalTactic = Z3_tactic_and_then(ctx, finalTactic, tactic5);
   Z3_solver solv = Z3_mk_solver_from_tactic(ctx, finalTactic);
   //Z3_solver solv = Z3_mk_solver(ctx);
   Z3_solver_inc_ref(ctx, solv);

   Z3_solver_from_string(ctx, solv, argv[1]);

   printf("Result: %i\n", Z3_solver_check(ctx, solv));
   Z3_model mdl = Z3_solver_get_model(ctx, solv);
   Z3_model_inc_ref(ctx, mdl);
   if (mdl)
      printf("Model: %s\n", Z3_model_to_string(ctx, mdl));
}

I have the final issue.. My original goal is to model the following constraints by using Z3:

(declare-fun userAgent () String) (declare-fun |0 Fill 0| () String) (declare-fun |0 Fill 1| () String) (declare-fun |0 Fill 2| () String) (declare-fun |0 Fill 3| () String) (declare-fun |0 Fill 4| () String) (declare-fun |0 Fill 6| () String) (declare-fun |0 Fill 5| () String) (declare-fun |IsMatch_/Version\\/(\\S+)\\s+Safari/_0| () Bool) (declare-fun |1 Fill 0| () String) (declare-fun |1 Fill 2| () String) (declare-fun |1 Fill 1| () String) (declare-fun IsMatch_/CriOS/_1 () Bool) (declare-fun |2 Fill 0| () String) (declare-fun |2 Fill 1| () String) (declare-fun |2 Fill 2| () String) (declare-fun |2 Fill 3| () String) (declare-fun |2 Fill 4| () String) (declare-fun |2 Fill 5| () String) (declare-fun origin () String) (assert (= origin "")) (declare-fun |IsMatch_/^https?:\\/\\//_2| () Bool) (assert (not (= userAgent ""))) (assert (= |0 Fill 0| "Version")) (assert (= |0 Fill 1| "/")) (assert (let ((a!1 (re.inter (re.complement (str.to.re "\n")) (re.inter (re.complement (str.to.re "\f")) (re.complement (str.to.re "\v")))))) (let ((a!2 (re.inter (re.complement (str.to.re "\x09")) (re.inter (re.complement (str.to.re "\r")) a!1)))) (let ((a!3 (re.inter (re.range "\x00" "\xff") (re.inter (re.complement (str.to.re " ")) a!2)))) (str.in.re |0 Fill 2| (re.++ a!3 (re.* a!3))))))) (assert (let ((a!1 (re.inter (re.complement (str.to.re "\n")) (re.inter (re.complement (str.to.re "\f")) (re.complement (str.to.re "\v")))))) (let ((a!2 (re.inter (re.complement (str.to.re "\x09")) (re.inter (re.complement (str.to.re "\r")) a!1)))) (let ((a!3 (re.inter (re.range "\x00" "\xff") (re.inter (re.complement (str.to.re " ")) a!2)))) (str.in.re |0 Fill 2| (re.++ a!3 (re.* a!3))))))) (assert (let ((a!1 (re.union (str.to.re "\r") (re.union (str.to.re "\n") (re.union (str.to.re "\f") (str.to.re "\v")))))) (let ((a!2 (re.* (re.union (str.to.re " ") (re.union (str.to.re "\x09") a!1))))) (let ((a!3 (re.++ (re.union (str.to.re " ") (re.union (str.to.re "\x09") a!1)) a!2))) (str.in.re |0 Fill 3| a!3))))) (assert (= |0 Fill 4| "Safari")) (assert (let ((a!1 (str.++ |0 Fill 0| (str.++ |0 Fill 1| (str.++ |0 Fill 2| (str.++ |0 Fill 3| |0 Fill 4|))))) (a!2 (re.inter (re.complement (str.to.re "\n")) (re.inter (re.complement (str.to.re "\f")) (re.complement (str.to.re "\v"))))) (a!5 (re.union (str.to.re "\r") (re.union (str.to.re "\n") (re.union (str.to.re "\f") (str.to.re "\v")))))) (let ((a!3 (re.inter (re.complement (str.to.re "\x09")) (re.inter (re.complement (str.to.re "\r")) a!2))) (a!6 (re.* (re.union (str.to.re " ") (re.union (str.to.re "\x09") a!5))))) (let ((a!4 (re.inter (re.range "\x00" "\xff") (re.inter (re.complement (str.to.re " ")) a!3))) (a!7 (re.++ (re.union (str.to.re " ") (re.union (str.to.re "\x09") a!5)) a!6))) (let ((a!8 (re.++ (re.++ (re.++ (str.to.re "Version") (str.to.re "/")) (re.++ a!4 (re.* a!4))) a!7))) (str.in.re a!1 (re.++ a!8 (str.to.re "Safari")))))))) (assert (let ((a!1 (re.inter (re.complement (str.to.re "\n")) (re.inter (re.complement (str.to.re "\f")) (re.complement (str.to.re "\v"))))) (a!4 (re.union (str.to.re "\r") (re.union (str.to.re "\n") (re.union (str.to.re "\f") (str.to.re "\v"))))) (a!9 (str.++ |0 Fill 1| (str.++ |0 Fill 2| (str.++ |0 Fill 3| (str.++ |0 Fill 4| |0 Fill 6|)))))) (let ((a!2 (re.inter (re.complement (str.to.re "\x09")) (re.inter (re.complement (str.to.re "\r")) a!1))) (a!5 (re.* (re.union (str.to.re " ") (re.union (str.to.re "\x09") a!4))))) (let ((a!3 (re.inter (re.range "\x00" "\xff") (re.inter (re.complement (str.to.re " ")) a!2))) (a!6 (re.++ (re.union (str.to.re " ") (re.union (str.to.re "\x09") a!4)) a!5))) (let ((a!7 (re.++ (re.++ (re.++ (str.to.re "Version") (str.to.re "/")) (re.++ a!3 (re.* a!3))) a!6))) (let ((a!8 (re.++ (re.++ (re.* (re.range "\x00" "\xff")) (re.++ a!7 (str.to.re "Safari"))) (re.* (re.range "\x00" "\xff"))))) (or (not (str.in.re userAgent a!8)) (= userAgent (str.++ |0 Fill 5| (str.++ |0 Fill 0| a!9)))))))))) (assert (let ((a!1 (re.inter (re.complement (str.to.re "\n")) (re.inter (re.complement (str.to.re "\f")) (re.complement (str.to.re "\v"))))) (a!4 (re.union (str.to.re "\r") (re.union (str.to.re "\n") (re.union (str.to.re "\f") (str.to.re "\v")))))) (let ((a!2 (re.inter (re.complement (str.to.re "\x09")) (re.inter (re.complement (str.to.re "\r")) a!1))) (a!5 (re.* (re.union (str.to.re " ") (re.union (str.to.re "\x09") a!4))))) (let ((a!3 (re.inter (re.range "\x00" "\xff") (re.inter (re.complement (str.to.re " ")) a!2))) (a!6 (re.++ (re.union (str.to.re " ") (re.union (str.to.re "\x09") a!4)) a!5))) (let ((a!7 (re.++ (re.++ (re.++ (str.to.re "Version") (str.to.re "/")) (re.++ a!3 (re.* a!3))) a!6))) (let ((a!8 (re.++ (re.++ (re.* (re.range "\x00" "\xff")) (re.++ a!7 (str.to.re "Safari"))) (re.* (re.range "\x00" "\xff"))))) (= (str.in.re userAgent a!8) |IsMatch_/Version\\/(\\S+)\\s+Safari/_0|))))))) (assert (let ((a!1 (re.inter (re.complement (str.to.re "\n")) (re.inter (re.complement (str.to.re "\f")) (re.complement (str.to.re "\v"))))) (a!4 (re.union (str.to.re "\r") (re.union (str.to.re "\n") (re.union (str.to.re "\f") (str.to.re "\v")))))) (let ((a!2 (re.inter (re.complement (str.to.re "\x09")) (re.inter (re.complement (str.to.re "\r")) a!1))) (a!5 (re.* (re.union (str.to.re " ") (re.union (str.to.re "\x09") a!4))))) (let ((a!3 (re.inter (re.range "\x00" "\xff") (re.inter (re.complement (str.to.re " ")) a!2))) (a!6 (re.++ (re.union (str.to.re " ") (re.union (str.to.re "\x09") a!4)) a!5))) (let ((a!7 (re.++ (re.++ (re.++ (str.to.re "Version") (str.to.re "/")) (re.++ a!3 (re.* a!3))) a!6))) (let ((a!8 (re.++ (re.++ (re.* (re.range "\x00" "\xff")) (re.++ a!7 (str.to.re "Safari"))) (re.* (re.range "\x00" "\xff"))))) (not (str.in.re userAgent a!8)))))))) (assert (= |1 Fill 0| "CriOS")) (assert (= |1 Fill 0| "CriOS")) (assert (let ((a!1 (re.++ (re.++ (re.* (re.range "\x00" "\xff")) (str.to.re "CriOS")) (re.* (re.range "\x00" "\xff"))))) (or (not (str.in.re userAgent a!1)) (= userAgent (str.++ |1 Fill 1| (str.++ |1 Fill 0| |1 Fill 2|)))))) (assert (let ((a!1 (re.++ (re.++ (re.* (re.range "\x00" "\xff")) (str.to.re "CriOS")) (re.* (re.range "\x00" "\xff"))))) (= (str.in.re userAgent a!1) IsMatch_/CriOS/_1))) (assert (= |2 Fill 0| "http")) (assert (str.in.re |2 Fill 1| (re.union (str.to.re "") (str.to.re "s")))) (assert (= |2 Fill 2| ":")) (assert (= |2 Fill 3| "/")) (assert (= |2 Fill 4| "/")) (assert (let ((a!1 (str.++ |2 Fill 0| (str.++ |2 Fill 1| (str.++ |2 Fill 2| (str.++ |2 Fill 3| |2 Fill 4|))))) (a!2 (re.++ (re.++ (str.to.re "http") (re.union (str.to.re "") (str.to.re "s"))) (str.to.re ":")))) (str.in.re a!1 (re.++ (re.++ a!2 (str.to.re "/")) (str.to.re "/"))))) (assert (let ((a!1 (re.++ (re.++ (str.to.re "http") (re.union (str.to.re "") (str.to.re "s"))) (str.to.re ":"))) (a!4 (str.++ |2 Fill 1| (str.++ |2 Fill 2| (str.++ |2 Fill 3| (str.++ |2 Fill 4| |2 Fill 5|)))))) (let ((a!2 (re.++ (re.++ (re.++ a!1 (str.to.re "/")) (str.to.re "/")) (re.* (re.range "\x00" "\xff"))))) (let ((a!3 (not (str.in.re (str.++ "https://www.instagram.com/p/BuXRLIXhgWC/embed/?cr=1&v=12&wp=374&rd=" (str.++ origin "&rp=undefined")) a!2)))) (or a!3 (= (str.++ "https://www.instagram.com/p/BuXRLIXhgWC/embed/?cr=1&v=12&wp=374&rd=" (str.++ origin "&rp=undefined")) (str.++ |2 Fill 0| a!4))))))) (assert (let ((a!1 (re.++ (re.++ (str.to.re "http") (re.union (str.to.re "") (str.to.re "s"))) (str.to.re ":")))) (let ((a!2 (re.++ (re.++ (re.++ a!1 (str.to.re "/")) (str.to.re "/")) (re.* (re.range "\x00" "\xff"))))) (= (str.in.re (str.++ "https://www.instagram.com/p/BuXRLIXhgWC/embed/?cr=1&v=12&wp=374&rd=" (str.++ origin "&rp=undefined")) a!2) |IsMatch_/^https?:\\/\\//_2|)))) (assert (let ((a!1 (re.++ (re.++ (str.to.re "http") (re.union (str.to.re "") (str.to.re "s"))) (str.to.re ":")))) (let ((a!2 (re.++ (re.++ (re.++ a!1 (str.to.re "/")) (str.to.re "/")) (re.* (re.range "\x00" "\xff"))))) (str.in.re (str.++ "https://www.instagram.com/p/BuXRLIXhgWC/embed/?cr=1&v=12&wp=374&rd=" (str.++ origin "&rp=undefined")) a!2)))) (check-sat) (get-model)

If I run the above from rise4fun, it takes only 1 second to give me the following satisfactory model:

sat (model (define-fun |2 Fill 5| () String "www.instagram.com/p/BuXRLIXhgWC/embed/?cr=1&v=12&wp=374&rd=&rp=undefined") (define-fun |0 Fill 2| () String "\x00") (define-fun |2 Fill 3| () String "/") (define-fun |0 Fill 1| () String "/") (define-fun |0 Fill 0| () String "Version") (define-fun |2 Fill 1| () String "s") (define-fun |2 Fill 2| () String ":") (define-fun |IsMatch_/^https?:\\\\/\\\\//_2| () Bool true) (define-fun |1 Fill 2| () String "") (define-fun IsMatch_/CriOS/_1 () Bool false) (define-fun userAgent () String "\x00") (define-fun |IsMatch_/Version\\\\/(\\\\S+)\\\\s+Safari/_0| () Bool false) (define-fun |0 Fill 4| () String "Safari") (define-fun |0 Fill 6| () String "") (define-fun origin () String "") (define-fun |2 Fill 4| () String "/") (define-fun |1 Fill 1| () String "") (define-fun |0 Fill 3| () String "\r") (define-fun |1 Fill 0| () String "CriOS") (define-fun |2 Fill 0| () String "http") (define-fun |0 Fill 5| () String "") )

But if I run it with my program above, it takes more than 1 minute. Could you please give me any insight on why my program is so slow, and if there could be any tip (or tactic) to make the program as fast as rise4fun? I really appreciate your help.

[NikolajBjorner]

It doesn't make sense to use the smt tactic followed by bit-blasting. The smt tactic performs a full SMT check. It works for bit-vectors and strings and should be invoked as a last resort (or give it a timeout and then you can use it as an alternative).

The 'sat' tactic only works for propositional logic so one has to blast bit-vectors and other finite domains into propositional logic. String constraints are not propositional.

Note that you can use tactics from the SMTLIB front-end. See the tutorial on tactics on rise4fun.com.

In general, using tactics requires some in-depth understanding of what each step does. The best way, after following the tutorial and reading the paper by Grant and Leo, is to look at the SMT logic tactics in the Z3 source code. There is also a recent paper from ETHZ on using ML techniques to compose tactics that are most suitable for a problem class. The built-in tactics are under src/tactics/smtlogics. The basic tactics are exposed over the API so you can invoke similar composition of tactics as the built-in strategies for smtlib logics.

[gogo9th]

Sorry that it took much time to reply, I have been looking into how tactics work and trying to get used to it. It's not easy, but at least now I understand where I went wrong. I will keep reading the paper and studying more to find the best tuning for my use case. Thanks a lot for all your help!