try th_lemma, update documentation of api functions for creating strings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
zmw12306 · Dec 1, 2021 · c6a5aa0 · c6a5aa0
1 parent 3b4f976
commit c6a5aa0
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 13 deletions.
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
@@ -3451,6 +3451,10 @@ extern "C" {
     /**
        \brief Create a sort for unicode strings.
 
+       The sort for characters can be changed to ASCII by setting
+       the global parameter \c encoding to \c ascii, or alternative
+       to 16 bit characters by setting \c encoding to \c bmp.
+
        def_API('Z3_mk_string_sort', SORT, (_in(CONTEXT), ))
      */
     Z3_sort Z3_API Z3_mk_string_sort(Z3_context c);
@@ -3459,7 +3463,8 @@ extern "C" {
        \brief Create a sort for unicode characters.
 
        The sort for characters can be changed to ASCII by setting
-       the global parameter \c unicode to \c false.
+       the global parameter \c encoding to \c ascii, or alternative
+       to 16 bit characters by setting \c encoding to \c bmp.
 
        def_API('Z3_mk_char_sort', SORT, (_in(CONTEXT), ))
     */

diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp
@@ -150,6 +150,13 @@ namespace smt {
 
     literal theory::mk_literal(expr* _e) {
         expr_ref e(_e, m);
+        if (has_quantifiers(e)) {
+            expr_ref fn(m.mk_fresh_const("aux-literal", m.mk_bool_sort()), m);
+            expr_ref eq(m.mk_eq(fn, e), m);
+            ctx.assert_expr(eq);
+            ctx.internalize_assertions();
+            return mk_literal(fn);
+        }
         bool is_not = m.is_not(_e, _e);
         if (!ctx.e_internalized(_e)) {
             ctx.internalize(_e, is_quantifier(_e));

diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
@@ -146,20 +146,10 @@ void theory_user_propagator::propagate() {
                 lit.neg();
             for (auto const& [a,b] : m_eqs)
                 m_lits.push_back(~mk_eq(a->get_expr(), b->get_expr(), false));
-            literal lit;
-            if (has_quantifiers(prop.m_conseq)) {
-                expr_ref fn(m.mk_fresh_const("user-conseq", m.mk_bool_sort()), m);
-                expr_ref eq(m.mk_eq(fn, prop.m_conseq), m);
-                ctx.assert_expr(eq);
-                ctx.internalize_assertions();
-                lit = mk_literal(fn);
-            }
-            else {
-                lit = mk_literal(prop.m_conseq);
-            }
+            literal lit = mk_literal(prop.m_conseq);            
             ctx.mark_as_relevant(lit);
             m_lits.push_back(lit);
-            ctx.mk_th_axiom(get_id(), m_lits);
+            ctx.mk_th_lemma(get_id(), m_lits);
             TRACE("user_propagate", ctx.display(tout););
         }
         ++m_stats.m_num_propagations;