3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00

Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api

This commit is contained in:
Christoph M. Wintersteiger 2013-06-28 12:14:53 +01:00
commit 10df5e950d
3 changed files with 89 additions and 5 deletions

View file

@ -1,3 +1,21 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
ast_util.cpp
Abstract:
Helper functions
Author:
Leonardo de Moura (leonardo) 2007-06-08.
Revision History:
--*/
#include "ast_util.h"
app * mk_list_assoc_app(ast_manager & m, func_decl * f, unsigned num_args, expr * const * args) {
@ -138,3 +156,38 @@ expr * get_clause_literal(ast_manager & m, expr * cls, unsigned idx) {
SASSERT(m.is_or(cls));
return to_app(cls)->get_arg(idx);
}
expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args) {
if (num_args == 0)
return m.mk_true();
else if (num_args == 1)
return args[0];
else
return m.mk_and(num_args, args);
}
expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args) {
if (num_args == 0)
return m.mk_false();
else if (num_args == 1)
return args[0];
else
return m.mk_or(num_args, args);
}
expr * mk_not(ast_manager & m, expr * arg) {
expr * atom;
if (m.is_not(arg, atom))
return atom;
else
return m.mk_not(arg);
}
expr * expand_distinct(ast_manager & m, unsigned num_args, expr * const * args) {
expr_ref_buffer new_diseqs(m);
for (unsigned i = 0; i < num_args; i++) {
for (unsigned j = i + 1; j < num_args; j++)
new_diseqs.push_back(m.mk_not(m.mk_eq(args[i], args[j])));
}
return mk_and(m, new_diseqs.size(), new_diseqs.c_ptr());
}

View file

@ -95,5 +95,36 @@ bool is_clause(ast_manager & m, expr * n);
unsigned get_clause_num_literals(ast_manager & m, expr * cls);
expr * get_clause_literal(ast_manager & m, expr * cls, unsigned idx);
// -----------------------------------
//
// Goodies for creating Boolean expressions
//
// -----------------------------------
/**
Return (and args[0] ... args[num_args-1]) if num_args >= 2
Return args[0] if num_args == 1
Return true if num_args == 0
*/
expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args);
/**
Return (or args[0] ... args[num_args-1]) if num_args >= 2
Return args[0] if num_args == 1
Return false if num_args == 0
*/
expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args);
/**
Return a if arg = (not a)
Retur (not arg) otherwise
*/
expr * mk_not(ast_manager & m, expr * arg);
/**
Return the expression (and (not (= args[0] args[1])) (not (= args[0] args[2])) ... (not (= args[num_args-2] args[num_args-1])))
*/
expr * expand_distinct(ast_manager & m, unsigned num_args, expr * const * args);
#endif /* _AST_UTIL_H_ */

View file

@ -23,7 +23,7 @@ Notes:
#include"smt_kernel.h"
#include"ast_pp.h"
#include"mk_simplified_app.h"
#include"ast_util.h"
class ctx_solver_simplify_tactic : public tactic {
ast_manager& m;
@ -104,7 +104,7 @@ protected:
return;
ptr_vector<expr> fmls;
g.get_formulas(fmls);
fml = m.mk_and(fmls.size(), fmls.c_ptr());
fml = mk_and(m, fmls.size(), fmls.c_ptr());
m_solver.push();
reduce(fml);
m_solver.pop(1);
@ -119,7 +119,7 @@ protected:
{
m_solver.push();
expr_ref fml1(m);
fml1 = m.mk_and(fmls.size(), fmls.c_ptr());
fml1 = mk_and(m, fmls.size(), fmls.c_ptr());
fml1 = m.mk_iff(fml, fml1);
fml1 = m.mk_not(fml1);
m_solver.assert_expr(fml1);
@ -218,7 +218,7 @@ protected:
else if (m.is_bool(arg)) {
res = local_simplify(a, n, id, i);
TRACE("ctx_solver_simplify_tactic",
tout << "Already cached: " << path_r.first << " " << mk_pp(res, m) << "\n";);
tout << "Already cached: " << path_r.first << " " << mk_pp(arg, m) << " |-> " << mk_pp(res, m) << "\n";);
args.push_back(res);
}
else {
@ -327,7 +327,7 @@ protected:
tmp = m.mk_eq(result, n);
m_solver.assert_expr(tmp);
if (!simplify_bool(n2, result)) {
result = a;
result = a->get_arg(index);
}
m_solver.pop(1);
return result;