mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
commit
1d4b996765
|
|
@ -1,449 +0,0 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2015 Microsoft Corporation
|
||||
|
||||
--*/
|
||||
|
||||
#include <stdio.h>
|
||||
#include <stdlib.h>
|
||||
#include <iostream>
|
||||
#include <string>
|
||||
#include <vector>
|
||||
#include "z3++.h"
|
||||
|
||||
|
||||
|
||||
int usage(const char **argv){
|
||||
std::cerr << "usage: " << argv[0] << " [options] file.smt" << std::endl;
|
||||
std::cerr << std::endl;
|
||||
std::cerr << "options:" << std::endl;
|
||||
std::cerr << " -t,--tree tree interpolation" << std::endl;
|
||||
std::cerr << " -c,--check check result" << std::endl;
|
||||
std::cerr << " -p,--profile profile execution" << std::endl;
|
||||
std::cerr << " -w,--weak weak interpolants" << std::endl;
|
||||
std::cerr << " -f,--flat ouput flat formulas" << std::endl;
|
||||
std::cerr << " -o <file> ouput to SMT-LIB file" << std::endl;
|
||||
std::cerr << " -a,--anon anonymize" << std::endl;
|
||||
std::cerr << " -s,--simple simple proof mode" << std::endl;
|
||||
std::cerr << std::endl;
|
||||
return 1;
|
||||
}
|
||||
|
||||
int main(int argc, const char **argv) {
|
||||
|
||||
bool tree_mode = false;
|
||||
bool check_mode = false;
|
||||
bool profile_mode = false;
|
||||
bool incremental_mode = false;
|
||||
std::string output_file;
|
||||
bool flat_mode = false;
|
||||
bool anonymize = false;
|
||||
bool write = false;
|
||||
|
||||
z3::config cfg;
|
||||
// Z3_interpolation_options options = Z3_mk_interpolation_options();
|
||||
// Z3_params options = 0;
|
||||
|
||||
/* Parse the command line */
|
||||
int argn = 1;
|
||||
while(argn < argc-1){
|
||||
std::string flag = argv[argn];
|
||||
if(flag[0] == '-'){
|
||||
if(flag == "-t" || flag == "--tree")
|
||||
tree_mode = true;
|
||||
else if(flag == "-c" || flag == "--check")
|
||||
check_mode = true;
|
||||
else if(flag == "-p" || flag == "--profile")
|
||||
profile_mode = true;
|
||||
#if 0
|
||||
else if(flag == "-w" || flag == "--weak")
|
||||
Z3_set_interpolation_option(options,"weak","1");
|
||||
else if(flag == "--secondary")
|
||||
Z3_set_interpolation_option(options,"secondary","1");
|
||||
#endif
|
||||
else if(flag == "-i" || flag == "--incremental")
|
||||
incremental_mode = true;
|
||||
else if(flag == "-o"){
|
||||
argn++;
|
||||
if(argn >= argc) return usage(argv);
|
||||
output_file = argv[argn];
|
||||
}
|
||||
else if(flag == "-f" || flag == "--flat")
|
||||
flat_mode = true;
|
||||
else if(flag == "-a" || flag == "--anon")
|
||||
anonymize = true;
|
||||
else if(flag == "-w" || flag == "--write")
|
||||
write = true;
|
||||
else if(flag == "-s" || flag == "--simple")
|
||||
Z3_set_param_value(cfg,"PREPROCESS","false");
|
||||
else
|
||||
return usage(argv);
|
||||
}
|
||||
argn++;
|
||||
}
|
||||
if(argn != argc-1)
|
||||
return usage(argv);
|
||||
const char *filename = argv[argn];
|
||||
|
||||
|
||||
/* Create a Z3 context to contain formulas */
|
||||
z3::context ctx(cfg, z3::context::interpolation());
|
||||
|
||||
if(write || anonymize)
|
||||
Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB2_COMPLIANT);
|
||||
else if(!flat_mode)
|
||||
Z3_set_ast_print_mode(ctx,Z3_PRINT_SMTLIB_COMPLIANT);
|
||||
|
||||
/* Read an interpolation problem */
|
||||
|
||||
unsigned num;
|
||||
Z3_ast *constraints;
|
||||
unsigned *parents = 0;
|
||||
const char *error;
|
||||
bool ok;
|
||||
unsigned num_theory;
|
||||
Z3_ast *theory;
|
||||
|
||||
ok = Z3_read_interpolation_problem(ctx, &num, &constraints, tree_mode ? &parents : 0, filename, &error, &num_theory, &theory) != 0;
|
||||
|
||||
/* If parse failed, print the error message */
|
||||
|
||||
if(!ok){
|
||||
std::cerr << error << "\n";
|
||||
return 1;
|
||||
}
|
||||
|
||||
/* if we get only one formula, and it is a conjunction, split it into conjuncts. */
|
||||
if(!tree_mode && num == 1){
|
||||
Z3_app app = Z3_to_app(ctx,constraints[0]);
|
||||
Z3_func_decl func = Z3_get_app_decl(ctx,app);
|
||||
Z3_decl_kind dk = Z3_get_decl_kind(ctx,func);
|
||||
if(dk == Z3_OP_AND){
|
||||
int nconjs = Z3_get_app_num_args(ctx,app);
|
||||
if(nconjs > 1){
|
||||
std::cout << "Splitting formula into " << nconjs << " conjuncts...\n";
|
||||
num = nconjs;
|
||||
constraints = new Z3_ast[num];
|
||||
for(unsigned k = 0; k < num; k++)
|
||||
constraints[k] = Z3_get_app_arg(ctx,app,k);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/* Write out anonymized version. */
|
||||
|
||||
if(write || anonymize){
|
||||
#if 0
|
||||
Z3_anonymize_ast_vector(ctx,num,constraints);
|
||||
#endif
|
||||
std::string ofn = output_file.empty() ? "iz3out.smt2" : output_file;
|
||||
Z3_write_interpolation_problem(ctx, num, constraints, parents, ofn.c_str(), num_theory, theory);
|
||||
std::cout << "anonymized problem written to " << ofn << "\n";
|
||||
exit(0);
|
||||
}
|
||||
|
||||
/* Compute an interpolant, or get a model. */
|
||||
|
||||
Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast));
|
||||
Z3_model z3model = 0;
|
||||
Z3_lbool result;
|
||||
|
||||
if(!incremental_mode){
|
||||
/* In non-incremental mode, we just pass the constraints. */
|
||||
result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, constraints, parents, options, interpolants, &z3model, 0, false, num_theory, theory);
|
||||
}
|
||||
else {
|
||||
|
||||
/* This is a somewhat useless demonstration of incremental mode.
|
||||
Here, we assert the constraints in the context, then pass them to
|
||||
iZ3 in an array, so iZ3 knows the sequence. Note it's safe to pass
|
||||
"true", even though we haven't techically asserted if. */
|
||||
|
||||
z3::solver s(ctx);
|
||||
z3::expr_vector asserted(ctx), saved_interpolants(ctx);
|
||||
|
||||
/* We start with nothing asserted. */
|
||||
for(unsigned i = 0; i < num; i++) asserted.push_back(ctx.bool_val(true));
|
||||
|
||||
/* Now we assert the constrints one at a time until UNSAT. */
|
||||
|
||||
for(unsigned i = 0; i < num; i++){
|
||||
asserted[i] = z3::expr(ctx, constraints[i]);
|
||||
s.add(asserted[i]);
|
||||
result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, &asserted[0], parents, options, interpolants, &z3model, 0, true, 0, 0);
|
||||
if(result == Z3_L_FALSE){
|
||||
for(unsigned j = 0; j < num-1; j++)
|
||||
/* Since we want the interpolant formulas to survive a "pop", we
|
||||
"persist" them here. */
|
||||
saved_interpolants.push_back(z3::expr(ctx, interpolants[j]));
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
switch (result) {
|
||||
|
||||
/* If UNSAT, print the interpolants */
|
||||
case Z3_L_FALSE:
|
||||
printf("unsat\n");
|
||||
if(output_file.empty()){
|
||||
printf("interpolant:\n");
|
||||
for(unsigned i = 0; i < num-1; i++)
|
||||
printf("%s\n", Z3_ast_to_string(ctx, interpolants[i]));
|
||||
}
|
||||
else {
|
||||
#if 0
|
||||
Z3_write_interpolation_problem(ctx,num-1,interpolants,0,output_file.c_str());
|
||||
printf("interpolant written to %s\n",output_file.c_str());
|
||||
#endif
|
||||
}
|
||||
#if 1
|
||||
if(check_mode){
|
||||
std::cout << "Checking interpolant...\n";
|
||||
bool chk;
|
||||
chk = Z3_check_interpolant(ctx,num,constraints,parents,interpolants,&error,num_theory,theory) != 0;
|
||||
if(chk)
|
||||
std::cout << "Interpolant is correct\n";
|
||||
else {
|
||||
std::cout << "Interpolant is incorrect\n";
|
||||
std::cout << error;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
#endif
|
||||
break;
|
||||
case Z3_L_UNDEF:
|
||||
printf("fail\n");
|
||||
break;
|
||||
case Z3_L_TRUE:
|
||||
printf("sat\n");
|
||||
printf("model:\n%s\n", Z3_model_to_string(ctx, z3model));
|
||||
break;
|
||||
}
|
||||
|
||||
if(profile_mode)
|
||||
std::cout << Z3_interpolation_profile(ctx);
|
||||
|
||||
|
||||
free(interpolants);
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
||||
|
||||
#if 0
|
||||
|
||||
|
||||
|
||||
int test(){
|
||||
int i;
|
||||
|
||||
/* Create a Z3 context to contain formulas */
|
||||
|
||||
Z3_config cfg = Z3_mk_config();
|
||||
Z3_context ctx = iz3_mk_context(cfg);
|
||||
|
||||
int num = 2;
|
||||
|
||||
Z3_ast *constraints = (Z3_ast *)malloc(num * sizeof(Z3_ast));
|
||||
|
||||
#if 1
|
||||
Z3_sort arr = Z3_mk_array_sort(ctx,Z3_mk_int_sort(ctx),Z3_mk_bool_sort(ctx));
|
||||
Z3_symbol as = Z3_mk_string_symbol(ctx, "a");
|
||||
Z3_symbol bs = Z3_mk_string_symbol(ctx, "b");
|
||||
Z3_symbol xs = Z3_mk_string_symbol(ctx, "x");
|
||||
|
||||
Z3_ast a = Z3_mk_const(ctx,as,arr);
|
||||
Z3_ast b = Z3_mk_const(ctx,bs,arr);
|
||||
Z3_ast x = Z3_mk_const(ctx,xs,Z3_mk_int_sort(ctx));
|
||||
|
||||
Z3_ast c1 = Z3_mk_eq(ctx,a,Z3_mk_store(ctx,b,x,Z3_mk_true(ctx)));
|
||||
Z3_ast c2 = Z3_mk_not(ctx,Z3_mk_select(ctx,a,x));
|
||||
#else
|
||||
Z3_symbol xs = Z3_mk_string_symbol(ctx, "x");
|
||||
Z3_ast x = Z3_mk_const(ctx,xs,Z3_mk_bool_sort(ctx));
|
||||
Z3_ast c1 = Z3_mk_eq(ctx,x,Z3_mk_true(ctx));
|
||||
Z3_ast c2 = Z3_mk_eq(ctx,x,Z3_mk_false(ctx));
|
||||
|
||||
#endif
|
||||
|
||||
constraints[0] = c1;
|
||||
constraints[1] = c2;
|
||||
|
||||
/* print out the result for grins. */
|
||||
|
||||
// Z3_string smtout = Z3_benchmark_to_smtlib_string (ctx, "foo", "QFLIA", "sat", "", num, constraints, Z3_mk_true(ctx));
|
||||
|
||||
// Z3_string smtout = Z3_ast_to_string(ctx,constraints[0]);
|
||||
// Z3_string smtout = Z3_context_to_string(ctx);
|
||||
// puts(smtout);
|
||||
|
||||
iz3_print(ctx,num,constraints,"iZ3temp.smt");
|
||||
|
||||
/* Make room for interpolants. */
|
||||
|
||||
Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast));
|
||||
|
||||
/* Make room for the model. */
|
||||
|
||||
Z3_model model = 0;
|
||||
|
||||
/* Call the prover */
|
||||
|
||||
Z3_lbool result = iz3_interpolate(ctx, num, constraints, interpolants, &model);
|
||||
|
||||
switch (result) {
|
||||
|
||||
/* If UNSAT, print the interpolants */
|
||||
case Z3_L_FALSE:
|
||||
printf("unsat, interpolants:\n");
|
||||
for(i = 0; i < num-1; i++)
|
||||
printf("%s\n", Z3_ast_to_string(ctx, interpolants[i]));
|
||||
break;
|
||||
case Z3_L_UNDEF:
|
||||
printf("fail\n");
|
||||
break;
|
||||
case Z3_L_TRUE:
|
||||
printf("sat\n");
|
||||
printf("model:\n%s\n", Z3_model_to_string(ctx, model));
|
||||
break;
|
||||
}
|
||||
|
||||
/* Delete the model if there is one */
|
||||
|
||||
if (model)
|
||||
Z3_del_model(ctx, model);
|
||||
|
||||
/* Delete logical context (note, we call iz3_del_context, not
|
||||
Z3_del_context */
|
||||
|
||||
iz3_del_context(ctx);
|
||||
|
||||
return 1;
|
||||
}
|
||||
|
||||
struct z3_error {
|
||||
Z3_error_code c;
|
||||
z3_error(Z3_error_code _c) : c(_c) {}
|
||||
};
|
||||
|
||||
extern "C" {
|
||||
static void throw_z3_error(Z3_error_code c){
|
||||
throw z3_error(c);
|
||||
}
|
||||
}
|
||||
|
||||
int main(int argc, const char **argv) {
|
||||
|
||||
/* Create a Z3 context to contain formulas */
|
||||
|
||||
Z3_config cfg = Z3_mk_config();
|
||||
Z3_context ctx = iz3_mk_context(cfg);
|
||||
Z3_set_error_handler(ctx, throw_z3_error);
|
||||
|
||||
/* Make some constraints, by parsing an smtlib formatted file given as arg 1 */
|
||||
|
||||
try {
|
||||
Z3_parse_smtlib_file(ctx, argv[1], 0, 0, 0, 0, 0, 0);
|
||||
}
|
||||
catch(const z3_error &err){
|
||||
std::cerr << "Z3 error: " << Z3_get_error_msg(err.c) << "\n";
|
||||
std::cerr << Z3_get_smtlib_error(ctx) << "\n";
|
||||
return(1);
|
||||
}
|
||||
|
||||
/* Get the constraints from the parser. */
|
||||
|
||||
int num = Z3_get_smtlib_num_formulas(ctx);
|
||||
|
||||
if(num == 0){
|
||||
std::cerr << "iZ3 error: File contains no formulas.\n";
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
||||
Z3_ast *constraints = (Z3_ast *)malloc(num * sizeof(Z3_ast));
|
||||
|
||||
int i;
|
||||
for (i = 0; i < num; i++)
|
||||
constraints[i] = Z3_get_smtlib_formula(ctx, i);
|
||||
|
||||
/* if we get only one formula, and it is a conjunction, split it into conjuncts. */
|
||||
if(num == 1){
|
||||
Z3_app app = Z3_to_app(ctx,constraints[0]);
|
||||
Z3_func_decl func = Z3_get_app_decl(ctx,app);
|
||||
Z3_decl_kind dk = Z3_get_decl_kind(ctx,func);
|
||||
if(dk == Z3_OP_AND){
|
||||
int nconjs = Z3_get_app_num_args(ctx,app);
|
||||
if(nconjs > 1){
|
||||
std::cout << "Splitting formula into " << nconjs << " conjuncts...\n";
|
||||
num = nconjs;
|
||||
constraints = new Z3_ast[num];
|
||||
for(int k = 0; k < num; k++)
|
||||
constraints[k] = Z3_get_app_arg(ctx,app,k);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/* print out the result for grins. */
|
||||
|
||||
// Z3_string smtout = Z3_benchmark_to_smtlib_string (ctx, "foo", "QFLIA", "sat", "", num, constraints, Z3_mk_true(ctx));
|
||||
|
||||
// Z3_string smtout = Z3_ast_to_string(ctx,constraints[0]);
|
||||
// Z3_string smtout = Z3_context_to_string(ctx);
|
||||
// puts(smtout);
|
||||
|
||||
// iz3_print(ctx,num,constraints,"iZ3temp.smt");
|
||||
|
||||
/* Make room for interpolants. */
|
||||
|
||||
Z3_ast *interpolants = (Z3_ast *)malloc((num-1) * sizeof(Z3_ast));
|
||||
|
||||
/* Make room for the model. */
|
||||
|
||||
Z3_model model = 0;
|
||||
|
||||
/* Call the prover */
|
||||
|
||||
Z3_lbool result = iz3_interpolate(ctx, num, constraints, interpolants, &model);
|
||||
|
||||
switch (result) {
|
||||
|
||||
/* If UNSAT, print the interpolants */
|
||||
case Z3_L_FALSE:
|
||||
printf("unsat, interpolants:\n");
|
||||
for(i = 0; i < num-1; i++)
|
||||
printf("%s\n", Z3_ast_to_string(ctx, interpolants[i]));
|
||||
std::cout << "Checking interpolants...\n";
|
||||
const char *error;
|
||||
if(iZ3_check_interpolant(ctx, num, constraints, 0, interpolants, &error))
|
||||
std::cout << "Interpolant is correct\n";
|
||||
else {
|
||||
std::cout << "Interpolant is incorrect\n";
|
||||
std::cout << error << "\n";
|
||||
}
|
||||
break;
|
||||
case Z3_L_UNDEF:
|
||||
printf("fail\n");
|
||||
break;
|
||||
case Z3_L_TRUE:
|
||||
printf("sat\n");
|
||||
printf("model:\n%s\n", Z3_model_to_string(ctx, model));
|
||||
break;
|
||||
}
|
||||
|
||||
/* Delete the model if there is one */
|
||||
|
||||
if (model)
|
||||
Z3_del_model(ctx, model);
|
||||
|
||||
/* Delete logical context (note, we call iz3_del_context, not
|
||||
Z3_del_context */
|
||||
|
||||
iz3_del_context(ctx);
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -94,7 +94,6 @@ def init_project_def():
|
|||
set_z3py_dir('api/python')
|
||||
# Examples
|
||||
add_cpp_example('cpp_example', 'c++')
|
||||
add_cpp_example('iz3', 'interp')
|
||||
add_cpp_example('z3_tptp', 'tptp')
|
||||
add_c_example('c_example', 'c')
|
||||
add_c_example('maxsat')
|
||||
|
|
|
|||
|
|
@ -2592,7 +2592,7 @@ def mk_z3consts_py(api_files):
|
|||
if Z3PY_SRC_DIR is None:
|
||||
raise MKException("You must invoke set_z3py_dir(path):")
|
||||
|
||||
blank_pat = re.compile("^ *$")
|
||||
blank_pat = re.compile("^ *\r?$")
|
||||
comment_pat = re.compile("^ *//.*$")
|
||||
typedef_pat = re.compile("typedef enum *")
|
||||
typedef2_pat = re.compile("typedef enum { *")
|
||||
|
|
@ -2653,6 +2653,8 @@ def mk_z3consts_py(api_files):
|
|||
z3consts.write('%s = %s\n' % (k, i))
|
||||
z3consts.write('\n')
|
||||
mode = SEARCHING
|
||||
elif len(words) <= 2:
|
||||
assert False, "Invalid %s, line: %s" % (api_file, linenum)
|
||||
else:
|
||||
if words[2] != '':
|
||||
if len(words[2]) > 1 and words[2][1] == 'x':
|
||||
|
|
@ -2670,7 +2672,7 @@ def mk_z3consts_py(api_files):
|
|||
|
||||
# Extract enumeration types from z3_api.h, and add .Net definitions
|
||||
def mk_z3consts_dotnet(api_files):
|
||||
blank_pat = re.compile("^ *$")
|
||||
blank_pat = re.compile("^ *\r?$")
|
||||
comment_pat = re.compile("^ *//.*$")
|
||||
typedef_pat = re.compile("typedef enum *")
|
||||
typedef2_pat = re.compile("typedef enum { *")
|
||||
|
|
@ -2740,6 +2742,8 @@ def mk_z3consts_dotnet(api_files):
|
|||
z3consts.write(' %s = %s,\n' % (k, i))
|
||||
z3consts.write(' }\n\n')
|
||||
mode = SEARCHING
|
||||
elif len(words) <= 2:
|
||||
assert False, "Invalid %s, line: %s" % (api_file, linenum)
|
||||
else:
|
||||
if words[2] != '':
|
||||
if len(words[2]) > 1 and words[2][1] == 'x':
|
||||
|
|
|
|||
|
|
@ -99,7 +99,7 @@ else:
|
|||
if s != None:
|
||||
enc = sys.stdout.encoding
|
||||
if enc != None: return s.decode(enc)
|
||||
else: return s
|
||||
else: return s.decode('ascii')
|
||||
else:
|
||||
return ""
|
||||
|
||||
|
|
|
|||
|
|
@ -103,9 +103,7 @@ namespace api {
|
|||
|
||||
m_smtlib_parser = 0;
|
||||
m_smtlib_parser_has_decls = false;
|
||||
|
||||
z3_bound_num_procs();
|
||||
|
||||
|
||||
m_error_handler = &default_error_handler;
|
||||
|
||||
m_basic_fid = m().get_basic_family_id();
|
||||
|
|
|
|||
|
|
@ -2613,8 +2613,13 @@ namespace Microsoft.Z3
|
|||
/// <paramref name="patterns"/> is an array of patterns, <paramref name="sorts"/> is an array
|
||||
/// with the sorts of the bound variables, <paramref name="names"/> is an array with the
|
||||
/// 'names' of the bound variables, and <paramref name="body"/> is the body of the
|
||||
/// quantifier. Quantifiers are associated with weights indicating
|
||||
/// the importance of using the quantifier during instantiation.
|
||||
/// quantifier. Quantifiers are associated with weights indicating the importance of
|
||||
/// using the quantifier during instantiation.
|
||||
/// Note that the bound variables are de-Bruijn indices created using <see cref="MkBound"/>.
|
||||
/// Z3 applies the convention that the last element in <paramref name="names"/> and
|
||||
/// <paramref name="sorts"/> refers to the variable with index 0, the second to last element
|
||||
/// of <paramref name="names"/> and <paramref name="sorts"/> refers to the variable
|
||||
/// with index 1, etc.
|
||||
/// </remarks>
|
||||
/// <param name="sorts">the sorts of the bound variables.</param>
|
||||
/// <param name="names">names of the bound variables</param>
|
||||
|
|
@ -2644,6 +2649,11 @@ namespace Microsoft.Z3
|
|||
/// <summary>
|
||||
/// Create a universal Quantifier.
|
||||
/// </summary>
|
||||
/// <remarks>
|
||||
/// Creates a universal quantifier using a list of constants that will
|
||||
/// form the set of bound variables.
|
||||
/// <seealso cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
|
||||
/// </remarks>
|
||||
public Quantifier MkForall(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
|
||||
{
|
||||
Contract.Requires(body != null);
|
||||
|
|
@ -2659,7 +2669,10 @@ namespace Microsoft.Z3
|
|||
/// <summary>
|
||||
/// Create an existential Quantifier.
|
||||
/// </summary>
|
||||
/// <seealso cref="MkForall(Sort[],Symbol[],Expr,uint,Pattern[],Expr[],Symbol,Symbol)"/>
|
||||
/// <remarks>
|
||||
/// Creates an existential quantifier using de-Brujin indexed variables.
|
||||
/// (<see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>).
|
||||
/// </remarks>
|
||||
public Quantifier MkExists(Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
|
||||
{
|
||||
Contract.Requires(sorts != null);
|
||||
|
|
@ -2678,6 +2691,11 @@ namespace Microsoft.Z3
|
|||
/// <summary>
|
||||
/// Create an existential Quantifier.
|
||||
/// </summary>
|
||||
/// <remarks>
|
||||
/// Creates an existential quantifier using a list of constants that will
|
||||
/// form the set of bound variables.
|
||||
/// <seealso cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
|
||||
/// </remarks>
|
||||
public Quantifier MkExists(Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
|
||||
{
|
||||
Contract.Requires(body != null);
|
||||
|
|
@ -2693,6 +2711,7 @@ namespace Microsoft.Z3
|
|||
/// <summary>
|
||||
/// Create a Quantifier.
|
||||
/// </summary>
|
||||
/// <see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
|
||||
public Quantifier MkQuantifier(bool universal, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
|
||||
{
|
||||
Contract.Requires(body != null);
|
||||
|
|
@ -2716,6 +2735,7 @@ namespace Microsoft.Z3
|
|||
/// <summary>
|
||||
/// Create a Quantifier.
|
||||
/// </summary>
|
||||
/// <see cref="MkForall(Sort[], Symbol[], Expr, uint, Pattern[], Expr[], Symbol, Symbol)"/>
|
||||
public Quantifier MkQuantifier(bool universal, Expr[] boundConstants, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
|
||||
{
|
||||
Contract.Requires(body != null);
|
||||
|
|
|
|||
|
|
@ -433,8 +433,8 @@ public class Context extends IDisposable
|
|||
/**
|
||||
* Creates a fresh function declaration with a name prefixed with
|
||||
* {@code prefix}.
|
||||
* @see mkFuncDecl(String,Sort,Sort)
|
||||
* @see mkFuncDecl(String,Sort[],Sort)
|
||||
* @see #mkFuncDecl(String,Sort,Sort)
|
||||
* @see #mkFuncDecl(String,Sort[],Sort)
|
||||
**/
|
||||
public FuncDecl mkFreshFuncDecl(String prefix, Sort[] domain, Sort range)
|
||||
|
||||
|
|
@ -1722,9 +1722,9 @@ public class Context extends IDisposable
|
|||
**/
|
||||
public Expr mkArrayExt(ArrayExpr arg1, ArrayExpr arg2)
|
||||
{
|
||||
checkContextMatch(arg1);
|
||||
checkContextMatch(arg2);
|
||||
return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
|
||||
checkContextMatch(arg1);
|
||||
checkContextMatch(arg2);
|
||||
return Expr.create(this, Native.mkArrayExt(nCtx(), arg1.getNativeObject(), arg2.getNativeObject()));
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -2025,6 +2025,7 @@ public class Context extends IDisposable
|
|||
|
||||
/**
|
||||
* Create a universal Quantifier.
|
||||
*
|
||||
* @param sorts the sorts of the bound variables.
|
||||
* @param names names of the bound variables
|
||||
* @param body the body of the quantifier.
|
||||
|
|
@ -2034,17 +2035,22 @@ public class Context extends IDisposable
|
|||
* @param quantifierID optional symbol to track quantifier.
|
||||
* @param skolemID optional symbol to track skolem constants.
|
||||
*
|
||||
* Remarks: Creates a forall formula, where
|
||||
* {@code weight"/> is the weight, <paramref name="patterns} is
|
||||
* @return Creates a forall formula, where
|
||||
* {@code weight} is the weight, {@code patterns} is
|
||||
* an array of patterns, {@code sorts} is an array with the sorts
|
||||
* of the bound variables, {@code names} is an array with the
|
||||
* 'names' of the bound variables, and {@code body} is the body
|
||||
* of the quantifier. Quantifiers are associated with weights indicating the
|
||||
* importance of using the quantifier during instantiation.
|
||||
* Note that the bound variables are de-Bruijn indices created using {@link mkBound}.
|
||||
* Z3 applies the convention that the last element in {@code names} and
|
||||
* {@code sorts} refers to the variable with index 0, the second to last element
|
||||
* of {@code names} and {@code sorts} refers to the variable
|
||||
* with index 1, etc.
|
||||
**/
|
||||
public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body,
|
||||
int weight, Pattern[] patterns, Expr[] noPatterns,
|
||||
Symbol quantifierID, Symbol skolemID)
|
||||
int weight, Pattern[] patterns, Expr[] noPatterns,
|
||||
Symbol quantifierID, Symbol skolemID)
|
||||
{
|
||||
|
||||
return new Quantifier(this, true, sorts, names, body, weight, patterns,
|
||||
|
|
@ -2052,11 +2058,12 @@ public class Context extends IDisposable
|
|||
}
|
||||
|
||||
/**
|
||||
* Create a universal Quantifier.
|
||||
* Creates a universal quantifier using a list of constants that will form the set of bound variables.
|
||||
* @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
|
||||
**/
|
||||
public Quantifier mkForall(Expr[] boundConstants, Expr body, int weight,
|
||||
Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
|
||||
Symbol skolemID)
|
||||
Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
|
||||
Symbol skolemID)
|
||||
{
|
||||
|
||||
return new Quantifier(this, true, boundConstants, body, weight,
|
||||
|
|
@ -2064,12 +2071,12 @@ public class Context extends IDisposable
|
|||
}
|
||||
|
||||
/**
|
||||
* Create an existential Quantifier.
|
||||
* Creates an existential quantifier using de-Brujin indexed variables.
|
||||
* @see mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
|
||||
**/
|
||||
public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,
|
||||
int weight, Pattern[] patterns, Expr[] noPatterns,
|
||||
Symbol quantifierID, Symbol skolemID)
|
||||
int weight, Pattern[] patterns, Expr[] noPatterns,
|
||||
Symbol quantifierID, Symbol skolemID)
|
||||
{
|
||||
|
||||
return new Quantifier(this, false, sorts, names, body, weight,
|
||||
|
|
@ -2077,11 +2084,12 @@ public class Context extends IDisposable
|
|||
}
|
||||
|
||||
/**
|
||||
* Create an existential Quantifier.
|
||||
* Creates an existential quantifier using a list of constants that will form the set of bound variables.
|
||||
* @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
|
||||
**/
|
||||
public Quantifier mkExists(Expr[] boundConstants, Expr body, int weight,
|
||||
Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
|
||||
Symbol skolemID)
|
||||
Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID,
|
||||
Symbol skolemID)
|
||||
{
|
||||
|
||||
return new Quantifier(this, false, boundConstants, body, weight,
|
||||
|
|
@ -2090,11 +2098,12 @@ public class Context extends IDisposable
|
|||
|
||||
/**
|
||||
* Create a Quantifier.
|
||||
* @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
|
||||
**/
|
||||
public Quantifier mkQuantifier(boolean universal, Sort[] sorts,
|
||||
Symbol[] names, Expr body, int weight, Pattern[] patterns,
|
||||
Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
|
||||
|
||||
Symbol[] names, Expr body, int weight, Pattern[] patterns,
|
||||
Expr[] noPatterns, Symbol quantifierID, Symbol skolemID)
|
||||
|
||||
{
|
||||
|
||||
if (universal)
|
||||
|
|
@ -2106,11 +2115,12 @@ public class Context extends IDisposable
|
|||
}
|
||||
|
||||
/**
|
||||
* Create a Quantifier.
|
||||
* Create a Quantifier
|
||||
* @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
|
||||
**/
|
||||
public Quantifier mkQuantifier(boolean universal, Expr[] boundConstants,
|
||||
Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
|
||||
Symbol quantifierID, Symbol skolemID)
|
||||
Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
|
||||
Symbol quantifierID, Symbol skolemID)
|
||||
{
|
||||
|
||||
if (universal)
|
||||
|
|
|
|||
|
|
@ -4862,7 +4862,7 @@ class Goal(Z3PPObject):
|
|||
elif sz == 1:
|
||||
return self.get(0)
|
||||
else:
|
||||
return And([ self.get(i) for i in range(len(self)) ])
|
||||
return And([ self.get(i) for i in range(len(self)) ], self.ctx)
|
||||
|
||||
#########################################
|
||||
#
|
||||
|
|
|
|||
|
|
@ -1157,7 +1157,13 @@ def set_pp_option(k, v):
|
|||
def obj_to_string(a):
|
||||
out = io.StringIO()
|
||||
_PP(out, _Formatter(a))
|
||||
return out.getvalue()
|
||||
r = out.getvalue()
|
||||
if sys.version < '3':
|
||||
return r
|
||||
else:
|
||||
enc = sys.stdout.encoding
|
||||
if enc != None: return r.decode(enc)
|
||||
return r
|
||||
|
||||
_html_out = None
|
||||
|
||||
|
|
|
|||
|
|
@ -166,6 +166,11 @@ expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args) {
|
|||
return m.mk_and(num_args, args);
|
||||
}
|
||||
|
||||
app* mk_and(ast_manager & m, unsigned num_args, app * const * args) {
|
||||
return to_app(mk_and(m, num_args, (expr* const*) args));
|
||||
}
|
||||
|
||||
|
||||
expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args) {
|
||||
if (num_args == 0)
|
||||
return m.mk_false();
|
||||
|
|
@ -175,6 +180,10 @@ expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args) {
|
|||
return m.mk_or(num_args, args);
|
||||
}
|
||||
|
||||
app* mk_or(ast_manager & m, unsigned num_args, app * const * args) {
|
||||
return to_app(mk_or(m, num_args, (expr* const*) args));
|
||||
}
|
||||
|
||||
expr * mk_not(ast_manager & m, expr * arg) {
|
||||
expr * atom;
|
||||
if (m.is_not(arg, atom))
|
||||
|
|
|
|||
|
|
@ -107,6 +107,9 @@ expr * get_clause_literal(ast_manager & m, expr * cls, unsigned idx);
|
|||
Return true if num_args == 0
|
||||
*/
|
||||
expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args);
|
||||
app * mk_and(ast_manager & m, unsigned num_args, app * const * args);
|
||||
inline app_ref mk_and(app_ref_vector const& args) { return app_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
|
||||
inline expr_ref mk_and(expr_ref_vector const& args) { return expr_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
|
||||
|
||||
/**
|
||||
Return (or args[0] ... args[num_args-1]) if num_args >= 2
|
||||
|
|
@ -114,6 +117,10 @@ expr * mk_and(ast_manager & m, unsigned num_args, expr * const * args);
|
|||
Return false if num_args == 0
|
||||
*/
|
||||
expr * mk_or(ast_manager & m, unsigned num_args, expr * const * args);
|
||||
app * mk_or(ast_manager & m, unsigned num_args, app * const * args);
|
||||
inline app_ref mk_or(app_ref_vector const& args) { return app_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
|
||||
inline expr_ref mk_or(expr_ref_vector const& args) { return expr_ref(mk_or(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); }
|
||||
|
||||
|
||||
/**
|
||||
Return a if arg = (not a)
|
||||
|
|
|
|||
|
|
@ -1401,9 +1401,10 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
|
|||
unsigned rlimit = m_params.m_rlimit;
|
||||
scoped_watch sw(*this);
|
||||
lbool r;
|
||||
bool was_pareto = false, was_opt = false;
|
||||
|
||||
if (m_opt && !m_opt->empty()) {
|
||||
bool was_pareto = false;
|
||||
was_opt = true;
|
||||
m_check_sat_result = get_opt();
|
||||
cancel_eh<opt_wrapper> eh(*get_opt());
|
||||
scoped_ctrl_c ctrlc(eh);
|
||||
|
|
@ -1436,9 +1437,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
|
|||
r = l_true;
|
||||
}
|
||||
get_opt()->set_status(r);
|
||||
if (r != l_false && !was_pareto) {
|
||||
get_opt()->display_assignment(regular_stream());
|
||||
}
|
||||
}
|
||||
else if (m_solver) {
|
||||
m_check_sat_result = m_solver.get(); // solver itself stores the result.
|
||||
|
|
@ -1465,6 +1463,10 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
|
|||
}
|
||||
display_sat_result(r);
|
||||
validate_check_sat_result(r);
|
||||
if (was_opt && r != l_false && !was_pareto) {
|
||||
get_opt()->display_assignment(regular_stream());
|
||||
}
|
||||
|
||||
if (r == l_true) {
|
||||
validate_model();
|
||||
if (m_params.m_dump_models) {
|
||||
|
|
|
|||
|
|
@ -50,6 +50,7 @@ Notes:
|
|||
#include "blast_term_ite_tactic.h"
|
||||
#include "model_implicant.h"
|
||||
#include "expr_safe_replace.h"
|
||||
#include "ast_util.h"
|
||||
|
||||
namespace pdr {
|
||||
|
||||
|
|
@ -448,6 +449,7 @@ namespace pdr {
|
|||
else if (is_sat == l_false) {
|
||||
uses_level = m_solver.assumes_level();
|
||||
}
|
||||
m_solver.set_model(0);
|
||||
return is_sat;
|
||||
}
|
||||
|
||||
|
|
@ -481,6 +483,7 @@ namespace pdr {
|
|||
prop_solver::scoped_level _sl(m_solver, level);
|
||||
m_solver.set_core(&core);
|
||||
m_solver.set_subset_based_core(true);
|
||||
m_solver.set_model(0);
|
||||
lbool res = m_solver.check_assumptions_and_formula(lits, fml);
|
||||
if (res == l_false) {
|
||||
lits.reset();
|
||||
|
|
@ -775,6 +778,13 @@ namespace pdr {
|
|||
}
|
||||
// only initial states are not set by the PDR search.
|
||||
SASSERT(m_model.get());
|
||||
if (!m_model.get()) {
|
||||
std::stringstream msg;
|
||||
msg << "no model for node " << state();
|
||||
IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
|
||||
throw default_exception(msg.str());
|
||||
}
|
||||
|
||||
datalog::rule const& rl1 = pt().find_rule(*m_model);
|
||||
if (is_ini(rl1)) {
|
||||
set_rule(&rl1);
|
||||
|
|
@ -793,15 +803,23 @@ namespace pdr {
|
|||
}
|
||||
}
|
||||
SASSERT(!tags.empty());
|
||||
ini_tags = m.mk_or(tags.size(), tags.c_ptr());
|
||||
ini_tags = ::mk_or(tags);
|
||||
ini_state = m.mk_and(ini_tags, pt().initial_state(), state());
|
||||
model_ref mdl;
|
||||
pt().get_solver().set_model(&mdl);
|
||||
TRACE("pdr", tout << mk_pp(ini_state, m) << "\n";);
|
||||
VERIFY(l_true == pt().get_solver().check_conjunction_as_assumptions(ini_state));
|
||||
TRACE("pdr", tout << ini_state << "\n";);
|
||||
if (l_true != pt().get_solver().check_conjunction_as_assumptions(ini_state)) {
|
||||
std::stringstream msg;
|
||||
msg << "Unsatisfiable initial state: " << ini_state << "\n";
|
||||
display(msg, 2);
|
||||
IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
|
||||
throw default_exception(msg.str());
|
||||
}
|
||||
SASSERT(mdl.get());
|
||||
datalog::rule const& rl2 = pt().find_rule(*mdl);
|
||||
SASSERT(is_ini(rl2));
|
||||
set_rule(&rl2);
|
||||
pt().get_solver().set_model(0);
|
||||
return const_cast<datalog::rule*>(m_rule);
|
||||
}
|
||||
|
||||
|
|
@ -830,7 +848,7 @@ namespace pdr {
|
|||
}
|
||||
r0 = get_rule();
|
||||
app_ref_vector& inst = pt().get_inst(r0);
|
||||
TRACE("pdr", tout << mk_pp(state(), m) << " instance: " << inst.size() << "\n";);
|
||||
TRACE("pdr", tout << state() << " instance: " << inst.size() << "\n";);
|
||||
for (unsigned i = 0; i < inst.size(); ++i) {
|
||||
expr* v;
|
||||
if (model.find(inst[i].get(), v)) {
|
||||
|
|
@ -852,7 +870,7 @@ namespace pdr {
|
|||
for (unsigned i = 0; i < indent; ++i) out << " ";
|
||||
out << m_level << " " << m_pt.head()->get_name() << " " << (m_closed?"closed":"open") << "\n";
|
||||
for (unsigned i = 0; i < indent; ++i) out << " ";
|
||||
out << " " << mk_pp(m_state, m_state.get_manager(), indent) << "\n";
|
||||
out << " " << mk_pp(m_state, m_state.get_manager(), indent) << " " << m_state->get_id() << "\n";
|
||||
for (unsigned i = 0; i < children().size(); ++i) {
|
||||
children()[i]->display(out, indent + 1);
|
||||
}
|
||||
|
|
@ -925,17 +943,6 @@ namespace pdr {
|
|||
}
|
||||
}
|
||||
|
||||
bool model_search::is_repeated(model_node& n) const {
|
||||
model_node* p = n.parent();
|
||||
while (p) {
|
||||
if (p->state() == n.state()) {
|
||||
TRACE("pdr", tout << n.state() << "repeated\n";);
|
||||
return true;
|
||||
}
|
||||
p = p->parent();
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void model_search::add_leaf(model_node& n) {
|
||||
SASSERT(n.children().empty());
|
||||
|
|
@ -1012,11 +1019,11 @@ namespace pdr {
|
|||
nodes.erase(&n);
|
||||
bool is_goal = n.is_goal();
|
||||
remove_goal(n);
|
||||
if (!nodes.empty() && is_goal && backtrack) {
|
||||
// TBD: siblings would also fail if n is not a goal.
|
||||
if (!nodes.empty() && backtrack && nodes[0]->children().empty() && nodes[0]->is_closed()) {
|
||||
TRACE("pdr_verbose", for (unsigned i = 0; i < nodes.size(); ++i) n.display(tout << &n << "\n", 2););
|
||||
model_node* n1 = nodes[0];
|
||||
n1->set_open();
|
||||
SASSERT(n1->children().empty());
|
||||
n1->set_open();
|
||||
enqueue_leaf(n1);
|
||||
}
|
||||
|
||||
|
|
@ -1702,7 +1709,15 @@ namespace pdr {
|
|||
|
||||
void context::validate_search() {
|
||||
expr_ref tr = m_search.get_trace(*this);
|
||||
// TBD: tr << "\n";
|
||||
smt::kernel solver(m, get_fparams());
|
||||
solver.assert_expr(tr);
|
||||
lbool res = solver.check();
|
||||
if (res != l_true) {
|
||||
std::stringstream msg;
|
||||
msg << "rule validation failed when checking: " << tr;
|
||||
IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
|
||||
throw default_exception(msg.str());
|
||||
}
|
||||
}
|
||||
|
||||
void context::validate_model() {
|
||||
|
|
@ -1938,11 +1953,11 @@ namespace pdr {
|
|||
proof_ref proof(m);
|
||||
SASSERT(m_last_result == l_true);
|
||||
proof = m_search.get_proof_trace(*this);
|
||||
TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
|
||||
TRACE("pdr", tout << "PDR trace: " << proof << "\n";);
|
||||
apply(m, m_pc.get(), proof);
|
||||
TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
|
||||
TRACE("pdr", tout << "PDR trace: " << proof << "\n";);
|
||||
// proof_utils::push_instantiations_up(proof);
|
||||
// TRACE("pdr", tout << "PDR up: " << mk_pp(proof, m) << "\n";);
|
||||
// TRACE("pdr", tout << "PDR up: " << proof << "\n";);
|
||||
return proof;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -268,7 +268,6 @@ namespace pdr {
|
|||
void enqueue_leaf(model_node* n); // add leaf to priority queue.
|
||||
void update_models();
|
||||
void set_leaf(model_node& n); // Set node as leaf, remove children.
|
||||
bool is_repeated(model_node& n) const;
|
||||
unsigned num_goals() const;
|
||||
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -191,7 +191,7 @@ namespace opt {
|
|||
m_msolver->set_adjust_value(m_adjust_value);
|
||||
is_sat = (*m_msolver)();
|
||||
if (is_sat != l_false) {
|
||||
m_msolver->get_model(m_model);
|
||||
m_msolver->get_model(m_model, m_labels);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -247,8 +247,9 @@ namespace opt {
|
|||
m_upper = r;
|
||||
}
|
||||
|
||||
void maxsmt::get_model(model_ref& mdl) {
|
||||
void maxsmt::get_model(model_ref& mdl, svector<symbol>& labels) {
|
||||
mdl = m_model.get();
|
||||
labels = m_labels;
|
||||
}
|
||||
|
||||
void maxsmt::commit_assignment() {
|
||||
|
|
|
|||
|
|
@ -46,7 +46,7 @@ namespace opt {
|
|||
virtual bool get_assignment(unsigned index) const = 0;
|
||||
virtual void set_cancel(bool f) = 0;
|
||||
virtual void collect_statistics(statistics& st) const = 0;
|
||||
virtual void get_model(model_ref& mdl) = 0;
|
||||
virtual void get_model(model_ref& mdl, svector<symbol>& labels) = 0;
|
||||
virtual void updt_params(params_ref& p) = 0;
|
||||
void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; }
|
||||
|
||||
|
|
@ -67,6 +67,7 @@ namespace opt {
|
|||
rational m_lower;
|
||||
rational m_upper;
|
||||
model_ref m_model;
|
||||
svector<symbol> m_labels;
|
||||
svector<bool> m_assignment; // truth assignment to soft constraints
|
||||
params_ref m_params; // config
|
||||
|
||||
|
|
@ -79,9 +80,9 @@ namespace opt {
|
|||
virtual bool get_assignment(unsigned index) const { return m_assignment[index]; }
|
||||
virtual void set_cancel(bool f) { m_cancel = f; if (f) s().cancel(); else s().reset_cancel(); }
|
||||
virtual void collect_statistics(statistics& st) const { }
|
||||
virtual void get_model(model_ref& mdl) { mdl = m_model.get(); }
|
||||
virtual void get_model(model_ref& mdl, svector<symbol>& labels) { mdl = m_model.get(); labels = m_labels;}
|
||||
virtual void commit_assignment();
|
||||
void set_model() { s().get_model(m_model); }
|
||||
void set_model() { s().get_model(m_model); s().get_labels(m_labels); }
|
||||
virtual void updt_params(params_ref& p);
|
||||
solver& s();
|
||||
void init();
|
||||
|
|
@ -122,6 +123,7 @@ namespace opt {
|
|||
rational m_upper;
|
||||
adjust_value m_adjust_value;
|
||||
model_ref m_model;
|
||||
svector<symbol> m_labels;
|
||||
params_ref m_params;
|
||||
public:
|
||||
maxsmt(maxsat_context& c);
|
||||
|
|
@ -139,7 +141,7 @@ namespace opt {
|
|||
rational get_upper() const;
|
||||
void update_lower(rational const& r);
|
||||
void update_upper(rational const& r);
|
||||
void get_model(model_ref& mdl);
|
||||
void get_model(model_ref& mdl, svector<symbol>& labels);
|
||||
bool get_assignment(unsigned index) const;
|
||||
void display_answer(std::ostream& out) const;
|
||||
void collect_statistics(statistics& st) const;
|
||||
|
|
|
|||
|
|
@ -167,6 +167,10 @@ namespace opt {
|
|||
m_hard_constraints.reset();
|
||||
}
|
||||
|
||||
void context::get_labels(svector<symbol> & r) {
|
||||
r.append(m_labels);
|
||||
}
|
||||
|
||||
void context::set_hard_constraints(ptr_vector<expr>& fmls) {
|
||||
if (m_scoped_state.set(fmls)) {
|
||||
clear_state();
|
||||
|
|
@ -228,6 +232,7 @@ namespace opt {
|
|||
TRACE("opt", tout << "initial search result: " << is_sat << "\n";);
|
||||
if (is_sat != l_false) {
|
||||
s.get_model(m_model);
|
||||
s.get_labels(m_labels);
|
||||
}
|
||||
if (is_sat != l_true) {
|
||||
return is_sat;
|
||||
|
|
@ -276,11 +281,6 @@ namespace opt {
|
|||
}
|
||||
}
|
||||
|
||||
void context::set_model(model_ref& mdl) {
|
||||
m_model = mdl;
|
||||
fix_model(mdl);
|
||||
}
|
||||
|
||||
void context::get_model(model_ref& mdl) {
|
||||
mdl = m_model;
|
||||
fix_model(mdl);
|
||||
|
|
@ -289,7 +289,7 @@ namespace opt {
|
|||
lbool context::execute_min_max(unsigned index, bool committed, bool scoped, bool is_max) {
|
||||
if (scoped) get_solver().push();
|
||||
lbool result = m_optsmt.lex(index, is_max);
|
||||
if (result == l_true) m_optsmt.get_model(m_model);
|
||||
if (result == l_true) m_optsmt.get_model(m_model, m_labels);
|
||||
if (scoped) get_solver().pop(1);
|
||||
if (result == l_true && committed) m_optsmt.commit_assignment(index);
|
||||
return result;
|
||||
|
|
@ -300,7 +300,7 @@ namespace opt {
|
|||
maxsmt& ms = *m_maxsmts.find(id);
|
||||
if (scoped) get_solver().push();
|
||||
lbool result = ms();
|
||||
if (result != l_false && (ms.get_model(tmp), tmp.get())) ms.get_model(m_model);
|
||||
if (result != l_false && (ms.get_model(tmp, m_labels), tmp.get())) ms.get_model(m_model, m_labels);
|
||||
if (scoped) get_solver().pop(1);
|
||||
if (result == l_true && committed) ms.commit_assignment();
|
||||
return result;
|
||||
|
|
@ -453,7 +453,7 @@ namespace opt {
|
|||
}
|
||||
|
||||
void context::yield() {
|
||||
m_pareto->get_model(m_model);
|
||||
m_pareto->get_model(m_model, m_labels);
|
||||
update_bound(true);
|
||||
update_bound(false);
|
||||
}
|
||||
|
|
@ -1121,16 +1121,20 @@ namespace opt {
|
|||
}
|
||||
|
||||
void context::display_assignment(std::ostream& out) {
|
||||
out << "(objectives\n";
|
||||
for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) {
|
||||
objective const& obj = m_scoped_state.m_objectives[i];
|
||||
out << " (";
|
||||
display_objective(out, obj);
|
||||
if (get_lower_as_num(i) != get_upper_as_num(i)) {
|
||||
out << " |-> [" << get_lower(i) << ":" << get_upper(i) << "]\n";
|
||||
out << " (" << get_lower(i) << " " << get_upper(i) << ")";
|
||||
}
|
||||
else {
|
||||
out << " |-> " << get_lower(i) << "\n";
|
||||
out << " " << get_lower(i);
|
||||
}
|
||||
out << ")\n";
|
||||
}
|
||||
out << ")\n";
|
||||
}
|
||||
|
||||
void context::display_objective(std::ostream& out, objective const& obj) const {
|
||||
|
|
|
|||
|
|
@ -162,6 +162,7 @@ namespace opt {
|
|||
bool m_pp_neat;
|
||||
symbol m_maxsat_engine;
|
||||
symbol m_logic;
|
||||
svector<symbol> m_labels;
|
||||
public:
|
||||
context(ast_manager& m);
|
||||
virtual ~context();
|
||||
|
|
@ -180,11 +181,10 @@ namespace opt {
|
|||
virtual lbool optimize();
|
||||
virtual bool print_model() const;
|
||||
virtual void get_model(model_ref& _m);
|
||||
virtual void set_model(model_ref& _m);
|
||||
virtual void fix_model(model_ref& _m);
|
||||
virtual void collect_statistics(statistics& stats) const;
|
||||
virtual proof* get_proof() { return 0; }
|
||||
virtual void get_labels(svector<symbol> & r) {}
|
||||
virtual void get_labels(svector<symbol> & r);
|
||||
virtual void get_unsat_core(ptr_vector<expr> & r) {}
|
||||
virtual std::string reason_unknown() const;
|
||||
|
||||
|
|
|
|||
|
|
@ -38,6 +38,7 @@ namespace opt {
|
|||
return l_undef;
|
||||
}
|
||||
m_solver->get_model(m_model);
|
||||
m_solver->get_labels(m_labels);
|
||||
IF_VERBOSE(1,
|
||||
model_ref mdl(m_model);
|
||||
cb.fix_model(mdl);
|
||||
|
|
@ -96,6 +97,7 @@ namespace opt {
|
|||
}
|
||||
if (is_sat == l_true) {
|
||||
m_solver->get_model(m_model);
|
||||
m_solver->get_labels(m_labels);
|
||||
mk_not_dominated_by();
|
||||
}
|
||||
return is_sat;
|
||||
|
|
|
|||
|
|
@ -31,7 +31,6 @@ namespace opt {
|
|||
virtual expr_ref mk_gt(unsigned i, model_ref& model) = 0;
|
||||
virtual expr_ref mk_ge(unsigned i, model_ref& model) = 0;
|
||||
virtual expr_ref mk_le(unsigned i, model_ref& model) = 0;
|
||||
virtual void set_model(model_ref& m) = 0;
|
||||
virtual void fix_model(model_ref& m) = 0;
|
||||
};
|
||||
class pareto_base {
|
||||
|
|
@ -42,6 +41,7 @@ namespace opt {
|
|||
ref<solver> m_solver;
|
||||
params_ref m_params;
|
||||
model_ref m_model;
|
||||
svector<symbol> m_labels;
|
||||
public:
|
||||
pareto_base(
|
||||
ast_manager & m,
|
||||
|
|
@ -77,8 +77,9 @@ namespace opt {
|
|||
}
|
||||
virtual lbool operator()() = 0;
|
||||
|
||||
virtual void get_model(model_ref& mdl) {
|
||||
virtual void get_model(model_ref& mdl, svector<symbol>& labels) {
|
||||
mdl = m_model;
|
||||
labels = m_labels;
|
||||
}
|
||||
|
||||
protected:
|
||||
|
|
|
|||
|
|
@ -51,6 +51,7 @@ namespace opt {
|
|||
if (src[i] >= dst[i]) {
|
||||
dst[i] = src[i];
|
||||
m_models.set(i, m_s->get_model(i));
|
||||
m_s->get_labels(m_labels);
|
||||
m_lower_fmls[i] = fmls[i].get();
|
||||
if (dst[i].is_pos() && !dst[i].is_finite()) { // review: likely done already.
|
||||
m_lower_fmls[i] = m.mk_false();
|
||||
|
|
@ -156,7 +157,8 @@ namespace opt {
|
|||
if (is_sat == l_true) {
|
||||
disj.reset();
|
||||
m_s->maximize_objectives(disj);
|
||||
m_s->get_model(m_model);
|
||||
m_s->get_model(m_model);
|
||||
m_s->get_labels(m_labels);
|
||||
for (unsigned i = 0; i < ors.size(); ++i) {
|
||||
expr_ref tmp(m);
|
||||
m_model->eval(ors[i].get(), tmp);
|
||||
|
|
@ -203,6 +205,7 @@ namespace opt {
|
|||
expr_ref optsmt::update_lower() {
|
||||
expr_ref_vector disj(m);
|
||||
m_s->get_model(m_model);
|
||||
m_s->get_labels(m_labels);
|
||||
m_s->maximize_objectives(disj);
|
||||
set_max(m_lower, m_s->get_objective_values(), disj);
|
||||
TRACE("opt",
|
||||
|
|
@ -331,6 +334,7 @@ namespace opt {
|
|||
|
||||
m_s->maximize_objective(obj_index, block);
|
||||
m_s->get_model(m_model);
|
||||
m_s->get_labels(m_labels);
|
||||
inf_eps obj = m_s->saved_objective_value(obj_index);
|
||||
if (obj > m_lower[obj_index]) {
|
||||
m_lower[obj_index] = obj;
|
||||
|
|
@ -405,8 +409,9 @@ namespace opt {
|
|||
return m_upper[i];
|
||||
}
|
||||
|
||||
void optsmt::get_model(model_ref& mdl) {
|
||||
void optsmt::get_model(model_ref& mdl, svector<symbol> & labels) {
|
||||
mdl = m_model.get();
|
||||
labels = m_labels;
|
||||
}
|
||||
|
||||
// force lower_bound(i) <= objective_value(i)
|
||||
|
|
|
|||
|
|
@ -38,6 +38,7 @@ namespace opt {
|
|||
svector<smt::theory_var> m_vars;
|
||||
symbol m_optsmt_engine;
|
||||
model_ref m_model;
|
||||
svector<symbol> m_labels;
|
||||
sref_vector<model> m_models;
|
||||
public:
|
||||
optsmt(ast_manager& m):
|
||||
|
|
@ -60,7 +61,7 @@ namespace opt {
|
|||
inf_eps get_lower(unsigned index) const;
|
||||
inf_eps get_upper(unsigned index) const;
|
||||
bool objective_is_model_valid(unsigned index) const;
|
||||
void get_model(model_ref& mdl);
|
||||
void get_model(model_ref& mdl, svector<symbol>& labels);
|
||||
model* get_model(unsigned index) const { return m_models[index]; }
|
||||
|
||||
void update_lower(unsigned idx, inf_eps const& r);
|
||||
|
|
|
|||
|
|
@ -250,7 +250,6 @@ public:
|
|||
return "no reason given";
|
||||
}
|
||||
virtual void get_labels(svector<symbol> & r) {
|
||||
UNREACHABLE();
|
||||
}
|
||||
virtual unsigned get_num_assertions() const {
|
||||
return m_fmls.size();
|
||||
|
|
|
|||
|
|
@ -3646,6 +3646,9 @@ namespace smt {
|
|||
approx_set::iterator it1 = plbls1.begin();
|
||||
approx_set::iterator end1 = plbls1.end();
|
||||
for (; it1 != end1; ++it1) {
|
||||
if (m_context.get_cancel_flag()) {
|
||||
break;
|
||||
}
|
||||
unsigned plbl1 = *it1;
|
||||
SASSERT(plbls1.may_contain(plbl1));
|
||||
approx_set::iterator it2 = plbls2.begin();
|
||||
|
|
@ -3687,6 +3690,9 @@ namespace smt {
|
|||
approx_set::iterator it1 = plbls.begin();
|
||||
approx_set::iterator end1 = plbls.end();
|
||||
for (; it1 != end1; ++it1) {
|
||||
if (m_context.get_cancel_flag()) {
|
||||
break;
|
||||
}
|
||||
unsigned plbl1 = *it1;
|
||||
SASSERT(plbls.may_contain(plbl1));
|
||||
approx_set::iterator it2 = clbls.begin();
|
||||
|
|
@ -3706,6 +3712,9 @@ namespace smt {
|
|||
svector<qp_pair>::iterator it1 = m_new_patterns.begin();
|
||||
svector<qp_pair>::iterator end1 = m_new_patterns.end();
|
||||
for (; it1 != end1; ++it1) {
|
||||
if (m_context.get_cancel_flag()) {
|
||||
break;
|
||||
}
|
||||
quantifier * qa = it1->first;
|
||||
app * mp = it1->second;
|
||||
SASSERT(m_ast_manager.is_pattern(mp));
|
||||
|
|
|
|||
|
|
@ -721,8 +721,8 @@ namespace smt {
|
|||
IF_VERBOSE(100, verbose_stream() << "(smt.collecting-features)\n";);
|
||||
st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas());
|
||||
IF_VERBOSE(1000, st.display_primitive(verbose_stream()););
|
||||
bool fixnum = st.arith_k_sum_is_small();
|
||||
bool int_only = !st.m_has_rational && !st.m_has_real;
|
||||
bool fixnum = st.arith_k_sum_is_small() && m_params.m_arith_fixnum;
|
||||
bool int_only = !st.m_has_rational && !st.m_has_real && m_params.m_arith_int_only;
|
||||
switch(m_params.m_arith_mode) {
|
||||
case AS_NO_ARITH:
|
||||
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("arith"), "no arithmetic"));
|
||||
|
|
|
|||
|
|
@ -305,14 +305,16 @@ public:
|
|||
m_nonfd.mark(f, true);
|
||||
expr* e1, *e2;
|
||||
if (m.is_eq(f, e1, e2)) {
|
||||
if (is_fd(e1, e2)) {
|
||||
if (is_fd(e1, e2) || is_fd(e2, e1)) {
|
||||
continue;
|
||||
}
|
||||
if (is_fd(e2, e1)) {
|
||||
continue;
|
||||
}
|
||||
}
|
||||
}
|
||||
m_todo.append(to_app(f)->get_num_args(), to_app(f)->get_args());
|
||||
if (is_app(f)) {
|
||||
m_todo.append(to_app(f)->get_num_args(), to_app(f)->get_args());
|
||||
}
|
||||
else if (is_quantifier(f)) {
|
||||
m_todo.push_back(to_quantifier(f)->get_expr());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -151,24 +151,3 @@ void escaped::display(std::ostream & out) const {
|
|||
}
|
||||
}
|
||||
|
||||
#ifdef _WINDOWS
|
||||
#ifdef ARRAYSIZE
|
||||
#undef ARRAYSIZE
|
||||
#endif
|
||||
#include <windows.h>
|
||||
#endif
|
||||
|
||||
void z3_bound_num_procs() {
|
||||
|
||||
#ifdef _Z3_COMMERCIAL
|
||||
#define Z3_COMMERCIAL_MAX_CORES 4
|
||||
#ifdef _WINDOWS
|
||||
DWORD_PTR numProcs = (1 << Z3_COMMERCIAL_MAX_CORES) - 1;
|
||||
SetProcessAffinityMask(GetCurrentProcess(), numProcs);
|
||||
#endif
|
||||
#else
|
||||
// Not bounded: Research evaluations are
|
||||
// not reasonable if run with artificial
|
||||
// or hidden throttles.
|
||||
#endif
|
||||
}
|
||||
|
|
|
|||
|
|
@ -400,7 +400,6 @@ inline size_t megabytes_to_bytes(unsigned mb) {
|
|||
return r;
|
||||
}
|
||||
|
||||
void z3_bound_num_procs();
|
||||
|
||||
#endif /* UTIL_H_ */
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue