str.to-int WIP

src/smt/theory_str.cpp

@@ -55,6 +55,7 @@ theory_str::theory_str(ast_manager & m):
 		avoidLoopCut(true),
 		loopDetected(false),
 		contains_map(m),
+		string_int_conversion_terms(m),
 		m_find(*this),
 		m_trail_stack(*this)
 {
@@ -821,7 +822,7 @@ bool theory_str::can_propagate() {
             || !m_axiom_CharAt_todo.empty() || !m_axiom_StartsWith_todo.empty() || !m_axiom_EndsWith_todo.empty()
             || !m_axiom_Contains_todo.empty() || !m_axiom_Indexof_todo.empty() || !m_axiom_Indexof2_todo.empty() || !m_axiom_LastIndexof_todo.empty()
             || !m_axiom_Substr_todo.empty() || !m_axiom_Replace_todo.empty()
-			|| !m_axiom_RegexIn_todo.empty()
+			|| !m_axiom_RegexIn_todo.empty() || !m_library_aware_axiom_todo.empty()
 			|| !m_delayed_axiom_setup_terms.empty();
             ;
 }
@@ -904,6 +905,17 @@ void theory_str::propagate() {
         }
         m_axiom_RegexIn_todo.reset();
 
+        for (unsigned i = 0; i < m_library_aware_axiom_todo.size(); ++i) {
+        	enode * e = m_library_aware_axiom_todo[i];
+        	if (is_str_to_int(e)) {
+        		instantiate_axiom_str_to_int(e);
+        	} else {
+        		TRACE("t_str", tout << "BUG: unhandled library-aware term " << mk_pp(e->get_owner(), get_manager()) << std::endl;);
+        		NOT_IMPLEMENTED_YET();
+        	}
+        }
+        m_library_aware_axiom_todo.reset();
+
         for (unsigned i = 0; i < m_delayed_axiom_setup_terms.size(); ++i) {
             // I think this is okay
             ctx.internalize(m_delayed_axiom_setup_terms[i].get(), false);
@@ -1563,6 +1575,53 @@ void theory_str::instantiate_axiom_Replace(enode * e) {
     assert_axiom(finalAxiom);
 }
 
+void theory_str::instantiate_axiom_str_to_int(enode * e) {
+	context & ctx = get_context();
+	ast_manager & m = get_manager();
+
+	app * ex = e->get_owner();
+	if (axiomatized_terms.contains(ex)) {
+		TRACE("t_str_detail", tout << "already set up str.to-int axiom for " << mk_pp(ex, m) << std::endl;);
+		return;
+	}
+	axiomatized_terms.insert(ex);
+
+	TRACE("t_str_detail", tout << "instantiate str.to-int axiom for " << mk_pp(ex, m) << std::endl;);
+
+	// let expr = (str.to-int S)
+	// axiom 1: expr >= -1
+	// axiom 2: expr = 0 <==> S = "0"
+	// axiom 3: expr >= 1 ==> len(S) > 0 AND S[0] != "0"
+
+	expr * S = ex->get_arg(0);
+	{
+		expr_ref axiom1(m_autil.mk_ge(ex, m_autil.mk_numeral(rational::minus_one(), true)), m);
+		SASSERT(axiom1);
+		assert_axiom(axiom1);
+	}
+
+	{
+		expr_ref lhs(ctx.mk_eq_atom(ex, m_autil.mk_numeral(rational::zero(), true)), m);
+		expr_ref rhs(ctx.mk_eq_atom(S, m_strutil.mk_string("0")), m);
+		expr_ref axiom2(ctx.mk_eq_atom(lhs, rhs), m);
+		SASSERT(axiom2);
+		assert_axiom(axiom2);
+	}
+
+	{
+		expr_ref premise(m_autil.mk_ge(ex, m_autil.mk_numeral(rational::one(), true)), m);
+		expr_ref hd(mk_str_var("hd"), m);
+		expr_ref tl(mk_str_var("tl"), m);
+		expr_ref conclusion1(ctx.mk_eq_atom(S, mk_concat(hd, tl)), m);
+		expr_ref conclusion2(ctx.mk_eq_atom(mk_strlen(hd), m_autil.mk_numeral(rational::one(), true)), m);
+		expr_ref conclusion3(m.mk_not(ctx.mk_eq_atom(hd, m_strutil.mk_string("0"))), m);
+		expr_ref conclusion(m.mk_and(conclusion1, conclusion2, conclusion3), m);
+		SASSERT(premise);
+		SASSERT(conclusion);
+		assert_implication(premise, conclusion);
+	}
+}
+
 expr * theory_str::mk_RegexIn(expr * str, expr * regexp) {
     expr * args[2] = {str, regexp};
     app * regexIn = get_manager().mk_app(get_id(), OP_RE_REGEXIN, 0, 0, 2, args);
@@ -6438,6 +6497,9 @@ void theory_str::set_up_axioms(expr * ex) {
                 m_axiom_Indexof2_todo.push_back(n);
             } else if (is_LastIndexof(ap)) {
                 m_axiom_LastIndexof_todo.push_back(n);
+            } else if (is_str_to_int(ap)) {
+            	string_int_conversion_terms.push_back(ap);
+            	m_library_aware_axiom_todo.push_back(n);
             }
         }
     } else {
@@ -7570,6 +7632,42 @@ int theory_str::ctx_dep_analysis(std::map<expr*, int> & strVarMap, std::map<expr
 	return 0;
 }
 
+// Check agreement between integer and string theories for the term a = (str.to-int S).
+// Returns true if axioms were added, and false otherwise.
+bool theory_str::finalcheck_str2int(app * a) {
+	bool axiomAdd = false;
+	context & ctx = get_context();
+	ast_manager & m = get_manager();
+
+	expr * S = a->get_arg(0);
+
+	// check integer theory
+	rational Ival;
+	bool Ival_exists = get_value(a, Ival);
+	if (Ival_exists) {
+		TRACE("t_str_detail", tout << "integer theory assigns " << mk_pp(a, m) << " = " << Ival.to_string() << std::endl;);
+		// if that value is not -1, we can assert (str.to-int S) = Ival --> S = "Ival"
+		if (!Ival.is_minus_one()) {
+			std::string Ival_str = Ival.to_string();
+			expr_ref premise(ctx.mk_eq_atom(a, m_autil.mk_numeral(Ival, true)), m);
+			expr_ref conclusion(ctx.mk_eq_atom(S, m_strutil.mk_string(Ival_str)), m);
+			expr_ref axiom(m.mk_or(m.mk_not(premise), conclusion), m);
+			if (!string_int_axioms.contains(axiom)) {
+				string_int_axioms.insert(axiom);
+				assert_axiom(axiom);
+				m_trail_stack.push(insert_obj_trail<theory_str, expr>(string_int_axioms, axiom));
+				axiomAdd = true;
+			}
+		}
+	} else {
+		TRACE("t_str_detail", tout << "integer theory has no assignment for " << mk_pp(a, m) << std::endl;);
+		NOT_IMPLEMENTED_YET();
+	}
+	// TODO also check assignment in string theory
+
+	return axiomAdd;
+}
+
 final_check_status theory_str::final_check_eh() {
     context & ctx = get_context();
     ast_manager & m = get_manager();
@@ -7671,6 +7769,26 @@ final_check_status theory_str::final_check_eh() {
     }
 
     if (!needToAssignFreeVars) {
+
+    	// check string-int terms
+    	bool addedStrIntAxioms = false;
+    	for (unsigned i = 0; i < string_int_conversion_terms.size(); ++i) {
+    		app * ex = to_app(string_int_conversion_terms[i].get());
+    		if (is_str_to_int(ex)) {
+    			bool axiomAdd = finalcheck_str2int(ex);
+    			if (axiomAdd) {
+    				addedStrIntAxioms = true;
+    			}
+    		} else {
+    			// TODO int.to-str
+    			NOT_IMPLEMENTED_YET();
+    		}
+    	}
+    	if (addedStrIntAxioms) {
+    		TRACE("t_str", tout << "Resuming search due to addition of string-integer conversion axioms." << std::endl;);
+    		return FC_CONTINUE;
+    	}
+
         if (unused_internal_variables.empty()) {
             TRACE("t_str", tout << "All variables are assigned. Done!" << std::endl;);
             return FC_DONE;

src/smt/theory_str.h

@@ -201,6 +201,9 @@ namespace smt {
         ptr_vector<enode> m_axiom_Replace_todo;
         ptr_vector<enode> m_axiom_RegexIn_todo;
 
+        // TODO refactor everything to use this worklist
+        ptr_vector<enode> m_library_aware_axiom_todo;
+
         // hashtable of all exprs for which we've already set up term-specific axioms --
         // this prevents infinite recursive descent with respect to axioms that
         // include an occurrence of the term for which axioms are being generated
@@ -260,6 +263,10 @@ namespace smt {
 
         obj_pair_map<expr, expr, expr*> concat_astNode_map;
 
+        // all (str.to-int) and (int.to-str) terms
+        expr_ref_vector string_int_conversion_terms;
+        obj_hashtable<expr> string_int_axioms;
+
         th_union_find m_find;
         th_trail_stack m_trail_stack;
         theory_var get_var(expr * n) const;
@@ -320,6 +327,8 @@ namespace smt {
         bool is_Substr(enode const * n) const { return is_Substr(n->get_owner()); }
         bool is_Replace(app const * a) const { return a->is_app_of(get_id(), OP_STR_REPLACE); }
         bool is_Replace(enode const * n) const { return is_Replace(n->get_owner()); }
+        bool is_str_to_int(app const * a) const { return a->is_app_of(get_id(), OP_STR_STR2INT); }
+		bool is_str_to_int(enode const * n) const { return is_str_to_int(n->get_owner()); }
 
         bool is_RegexIn(app const * a) const { return a->is_app_of(get_id(), OP_RE_REGEXIN); }
         bool is_RegexIn(enode const * n) const { return is_RegexIn(n->get_owner()); }
@@ -348,6 +357,7 @@ namespace smt {
         void instantiate_axiom_LastIndexof(enode * e);
         void instantiate_axiom_Substr(enode * e);
         void instantiate_axiom_Replace(enode * e);
+        void instantiate_axiom_str_to_int(enode * e);
 
         expr * mk_RegexIn(expr * str, expr * regexp);
         void instantiate_axiom_RegexIn(enode * e);
@@ -469,6 +479,8 @@ namespace smt {
         void get_const_str_asts_in_node(expr * node, expr_ref_vector & constList);
         expr * eval_concat(expr * n1, expr * n2);
 
+        bool finalcheck_str2int(app * a);
+
         // strRegex
 
         void get_eqc_allUnroll(expr * n, expr * &constStr, std::set<expr*> & unrollFuncSet);