Branch data     Line data    Source code

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