reading string value from the output of z3 consequence API throws exception

[chauhansantosh17]

Recently, we have started consuming consequence API from z3 solver class. We are getting some unexpected behaviour from get_string API when it is invoked on z3 expr returned by the consequence API. Let's consider the c++ code snippet that demonstrate the problem

void testConsequenceAPI() { context c; // declare z3 context //declare bool constants expr a = c.bool_const("a"); expr b = c.bool_const("b"); expr d = c.bool_const("d"); expr x = c.int_const("x"); // declare integer constant expr y = c.string_const("y"); // declare string constant

solver s(c); // create a default z3 solver object from the context
expr c1 = c.bool_const("c1");
s.add( c1 == (x > 0 & x < 4)); // this assert limit value of x to be between 0 and 4
expr c2 = c.bool_const("c2");
expr stringValue = c.string_val("ABC");
s.add(c2 == implies(a, (x == 1 & y == stringValue))); // when c2 is true, then if a is true then x should be 1 and y should be "ABC"
expr c3 = c.bool_const("c3");
expr stringValue2 = c.string_val("XYZ");
s.add(c3 == implies(b, (x == 2 & y == stringValue2))); // when c3 is true, then if b is true then x should be 2 and y should be "XYZ"
expr c4 = c.bool_const("c4");
s.add(c4 == implies(a, d)); // when c4 is true, then if a is true then d should be true

expr_vector inputConstraints(c);
inputConstraints.push_back(c1);
inputConstraints.push_back(c2); // this would enforce x=1 & y ="ABC"
inputConstraints.push_back(c3); // this would enforce b =false
inputConstraints.push_back(c4); // this would enforce d = true
inputConstraints.push_back(a); // this would enforce a=true

expr_vector familiesToExpand(c);
familiesToExpand.push_back(x);
familiesToExpand.push_back(y);
familiesToExpand.push_back(b);
familiesToExpand.push_back(d);

expr_vector expandedFamilies(c);
**z3::check_result consequenceResult = s.consequences(inputConstraints, familiesToExpand, expandedFamilies);**
if(consequenceResult == z3::sat)
{
    // the below line prints the below output
    /*
    //(ast-vector
    //(=> (and c4 a) d)
    //(=> (and c2 a)
    //    (= y
    //       (str.++ (seq.unit (_ Char 65))
    //               (seq.unit (_ Char 66))
    //               (seq.unit (_ Char 67)))))
    //(=> (and c2 a) (= x 1))
    //(=> (and c2 c3 a) (not b)))
    /**/
    std::cout << "consequence result: " << expandedFamilies << "\n";

    // process the above output on at a time in each iteration of the below loop
    std::for_each(expandedFamilies.begin(), expandedFamilies.end(),
        [](const z3::expr& currentConsequence)
        {
            if(currentConsequence.is_implies()) // every expr is a implies in output vector from consequence API
            {
                const z3::expr& antecedent = currentConsequence.arg(0);
                const z3::expr& consequent = currentConsequence.arg(1);
                std::cout << "Constraint responsible for current expansion: " << antecedent << "\n";
                if(consequent.is_bool()) // every consequent expr is of bool sort
                {
                    const size_t argCount = consequent.num_args();
                    std::cout << "Consequent: " << consequent << "\n";
                    if(argCount == 0)
                    {
                        // it mean this is boolean family which is assigned true in consequence result
                        // 'd' boolean constant is assigned true in consequence result
                        std::cout << "Current Family Name: " << consequent.decl().name().str() << ". Solution:True" << "\n";
                    }
                    else if(argCount == 1)
                    {
                        // 'b' boolean constant is assigned false in consequence result
                        std::cout << "Current Family Name: " << consequent.arg(0).decl().name().str() << "." << "\n";
                        Z3_decl_kind currentResultOperation = consequent.decl().decl_kind();
                        if(Z3_OP_NOT == currentResultOperation)
                        {
                            std::cout << "boolean family is assigned false in consequence result\n";
                        }

                    }
                    else if(argCount == 2)
                    {
                        const z3::expr& family = consequent.arg(0); // this would either family varible - x or Y
                        std::cout << "Current Family: " << family.decl().name().str() << ". Sort Type:" << family.get_sort().sort_kind() << "\n";
                        if(family.get_sort().is_int())
                        {
                            int64_t value = 0;
                            if(consequent.arg(1).is_numeral_i64(value)) // this get integer value assigned to x family in consequence result
                            {
                                std::cout << "Current assignment: " << value << "." << "\n";
                            }
                        }
                        else if(family.get_sort().sort_kind() == Z3_SEQ_SORT) // string is considered as sequence of characters
                        {
                            z3::sort currentSeq = consequent.arg(1).get_sort(); // arg(1) is the value assigned to string family 'y' in consequence result
                            if(currentSeq.is_seq())
                            {
                                Z3_sort_kind seqSortType = currentSeq.sort_kind();
                                std::cout << "Current assignment is seq sort: " << seqSortType << std::endl;

                                // My understanding is at this point consequent.arg(1) holds the below information:
                                //       (str.++ (seq.unit (_ Char 65))
                                //               (seq.unit (_ Char 66))
                                //               (seq.unit (_ Char 67)))))
                                **std::cout << "Current assignment value:" << consequent.arg(1).get_string() << std::endl;**
                            }
                        }
                    }
                    else
                    {
                        std::cout << "Consequent: " << consequent << "\n";
                    }
                }
                else
                {
                    std::cout << "Consequent: " << consequent << "\n";
                }
            }
        });
}
else
{
    std::cout << "unsat\n";
    expr_vector core = s.unsat_core();
    std::cout << "core size: " << core << "\n";
}

}

The get_string API in the above highlighted line throw exception terminating the program. My expectation is: the get_string API should return a string containing "ABC", considering the assumption expr(inputConstraints) for the consequence API?

Am I missing something? Could you please help to understand why the above get_string API throw expection? What corrective action we can take to fix the exception and to get "ABC" as the return string?

[NikolajBjorner]

pre-processing converts string literals into a concatenation of characters. The output of consequence finding has been pre-processed. It is semantically equal to a string literal, but the get_string() API only works for string literals.