Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * A simple test for cvc5_reset_assertions().
      11                 :            :  *
      12                 :            :  * This indirectly also tests some corner cases w.r.t. context-dependent
      13                 :            :  * datastructures: resetAssertions() pops the contexts to zero but some
      14                 :            :  * context-dependent datastructures are created at leevel 1, which the
      15                 :            :  * datastructure needs to handle properly problematic.
      16                 :            :  */
      17                 :            : 
      18                 :            : #include <cvc5/c/cvc5.h>
      19                 :            : #include <stdio.h>
      20                 :            : 
      21                 :          1 : int main()
      22                 :            : {
      23                 :          1 :   Cvc5TermManager* tm = cvc5_term_manager_new();
      24                 :          1 :   Cvc5* solver = cvc5_new(tm);
      25                 :          1 :   cvc5_set_option(solver, "incremental", "true");
      26                 :            : 
      27                 :          1 :   Cvc5Term x = cvc5_mk_const(tm, cvc5_get_real_sort(tm), "x");
      28                 :          1 :   Cvc5Term four = cvc5_mk_real_int64(tm, 4);
      29                 :          1 :   Cvc5Term args[2] = {x, four};
      30                 :          1 :   Cvc5Term x_eq_four = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args);
      31                 :          1 :   cvc5_assert_formula(solver, x_eq_four);
      32                 :          1 :   printf("%s\n", cvc5_result_to_string(cvc5_check_sat(solver)));
      33                 :            : 
      34                 :          1 :   cvc5_reset_assertions(solver);
      35                 :            : 
      36                 :          1 :   Cvc5Sort int_sort = cvc5_get_integer_sort(tm);
      37                 :          1 :   Cvc5Sort arr_sort = cvc5_mk_array_sort(tm, int_sort, int_sort);
      38                 :          1 :   Cvc5Term array = cvc5_mk_const(tm, arr_sort, "array");
      39                 :          1 :   Cvc5Term four_int = cvc5_mk_integer_int64(tm, 4);
      40                 :          1 :   args[0] = array;
      41                 :          1 :   args[1] = four_int;
      42                 :          1 :   Cvc5Term arr_at_four = cvc5_mk_term(tm, CVC5_KIND_SELECT, 2, args);
      43                 :          1 :   Cvc5Term ten = cvc5_mk_integer_int64(tm, 10);
      44                 :          1 :   args[0] = arr_at_four;
      45                 :          1 :   args[1] = ten;
      46                 :          1 :   Cvc5Term arr_at_four_eq_ten = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args);
      47                 :          1 :   cvc5_assert_formula(solver, arr_at_four_eq_ten);
      48                 :          1 :   printf("%s\n", cvc5_result_to_string(cvc5_check_sat(solver)));
      49                 :          1 :   cvc5_delete(solver);
      50                 :          1 :   cvc5_term_manager_delete(tm);
      51                 :            : }