mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
finished script for auto-gen of install_tactic procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
fab47f5f7d
commit
ec43b3bf7a
|
|
@ -70,8 +70,6 @@ add_dot_net_dll('dotnetV3', ['api_dll'], 'bindings/dotnet/Microsoft.Z3V3', dll_n
|
|||
mk_auto_src()
|
||||
update_version(4, 2, 0, 0)
|
||||
|
||||
mk_all_install_tactic_cpps()
|
||||
|
||||
#
|
||||
mk_makefile()
|
||||
|
||||
|
|
|
|||
|
|
@ -395,7 +395,7 @@ def reg_component(name, c):
|
|||
_ComponentNames.add(name)
|
||||
_Name2Component[name] = c
|
||||
if VERBOSE:
|
||||
print "Processed '%s'" % name
|
||||
print "New component: '%s'" % name
|
||||
|
||||
def add_lib(name, deps=[], path=None):
|
||||
c = LibComponent(name, path, deps)
|
||||
|
|
@ -464,6 +464,7 @@ def mk_makefile():
|
|||
def mk_auto_src():
|
||||
if not ONLY_MAKEFILES:
|
||||
mk_pat_db()
|
||||
mk_all_install_tactic_cpps()
|
||||
|
||||
# TODO: delete after src/ast/pattern/expr_pattern_match
|
||||
# database.smt ==> database.h
|
||||
|
|
@ -552,18 +553,23 @@ def update_assembly_info_version(assemblyinfo, major, minor, build, revision, is
|
|||
print "Updated %s" % assemblyinfo
|
||||
|
||||
ADD_TACTIC_DATA=[]
|
||||
ADD_PROBE_DATA=[]
|
||||
|
||||
def ADD_TACTIC(name, descr, cmd):
|
||||
global ADD_TACTIC_DATA
|
||||
ADD_TACTIC_DATA.append((name, descr, cmd))
|
||||
|
||||
def ADD_PROBE(name, descr, cmd):
|
||||
global ADD_PROBE_DATA
|
||||
ADD_PROBE_DATA.append((name, descr, cmd))
|
||||
|
||||
# Generate an install_tactics.cpp at path.
|
||||
# This file implements the procedure
|
||||
# void install_tactics(tactic_manager & ctx)
|
||||
# It installs all tactics in the given component (name) list cnames
|
||||
# The procedure looks for ADD_TACTIC commands in the .h files of these components.
|
||||
def mk_install_tactic_cpp(cnames, path):
|
||||
global ADD_TACTIC_DATA
|
||||
global ADD_TACTIC_DATA, ADD_PROBE_DATA
|
||||
ADD_TACTIC_DATA = []
|
||||
fullname = '%s/install_tactic.cpp' % path
|
||||
fout = open(fullname, 'w')
|
||||
|
|
@ -571,19 +577,31 @@ def mk_install_tactic_cpp(cnames, path):
|
|||
fout.write('#include"tactic.h"\n')
|
||||
fout.write('#include"tactic_cmds.h"\n')
|
||||
fout.write('#include"cmd_context.h"\n')
|
||||
pat = re.compile('[ \t]*ADD_TACTIC\(.*\)')
|
||||
tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)')
|
||||
probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)')
|
||||
for cname in cnames:
|
||||
c = _Name2Component[cname]
|
||||
h_files = filter(lambda f: f.endswith('.h'), os.listdir(c.src_dir))
|
||||
for h_file in h_files:
|
||||
added_include = False
|
||||
fin = open("%s/%s" % (c.src_dir, h_file), 'r')
|
||||
for line in fin:
|
||||
if pat.match(line):
|
||||
fout.write('#include"%s"\n' % h_file)
|
||||
if tactic_pat.match(line):
|
||||
if not added_include:
|
||||
added_include = True
|
||||
fout.write('#include"%s"\n' % h_file)
|
||||
try:
|
||||
exec line.strip('\n ') in globals()
|
||||
except:
|
||||
raise MKException("Failed processing ADD_TACTIC command at '%s'\n%s" % (fullname, line))
|
||||
if probe_pat.match(line):
|
||||
if not added_include:
|
||||
added_include = True
|
||||
fout.write('#include"%s"\n' % h_file)
|
||||
try:
|
||||
exec line.strip('\n ') in globals()
|
||||
except:
|
||||
raise MKException("Failed processing ADD_PROBE command at '%s'\n%s" % (fullname, line))
|
||||
# First pass will just generate the tactic factories
|
||||
idx = 0
|
||||
for data in ADD_TACTIC_DATA:
|
||||
|
|
@ -596,6 +614,8 @@ def mk_install_tactic_cpp(cnames, path):
|
|||
for data in ADD_TACTIC_DATA:
|
||||
fout.write(' ADD_TACTIC_CMD("%s", "%s", __Z3_local_factory_%s);\n' % (data[0], data[1], idx))
|
||||
idx = idx + 1
|
||||
for data in ADD_PROBE_DATA:
|
||||
fout.write(' ADD_PROBE("%s", "%s", %s);\n' % data)
|
||||
fout.write('}\n')
|
||||
if VERBOSE:
|
||||
print "Generated '%s'" % fullname
|
||||
|
|
|
|||
|
|
@ -1,178 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
install_tactics.cpp
|
||||
|
||||
Abstract:
|
||||
Install tactics in the SMT 2.0 frontend.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2012-02-19
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#include"tactic_cmds.h"
|
||||
#include"cmd_context.h"
|
||||
#include"simplify_tactic.h"
|
||||
#include"split_clause_tactic.h"
|
||||
#include"normalize_bounds_tactic.h"
|
||||
#include"elim_uncnstr_tactic.h"
|
||||
#include"add_bounds_tactic.h"
|
||||
#include"ctx_simplify_tactic.h"
|
||||
#include"ctx_solver_simplify_tactic.h"
|
||||
|
||||
#include"bit_blaster_tactic.h"
|
||||
#include"bv1_blaster_tactic.h"
|
||||
#include"der_tactic.h"
|
||||
#include"aig_tactic.h"
|
||||
#include"smt_tactic.h"
|
||||
#include"sat_tactic.h"
|
||||
#include"occf_tactic.h"
|
||||
#include"qe_tactic.h"
|
||||
#include"qe_sat_tactic.h"
|
||||
#include"propagate_values_tactic.h"
|
||||
#include"nnf_tactic.h"
|
||||
#include"solve_eqs_tactic.h"
|
||||
#include"max_bv_sharing_tactic.h"
|
||||
#include"elim_term_ite_tactic.h"
|
||||
#include"fix_dl_var_tactic.h"
|
||||
#include"tseitin_cnf_tactic.h"
|
||||
#include"degree_shift_tactic.h"
|
||||
#include"purify_arith_tactic.h"
|
||||
#include"nla2bv_tactic.h"
|
||||
#include"nlsat_tactic.h"
|
||||
#include"factor_tactic.h"
|
||||
#include"fm_tactic.h"
|
||||
#include"diff_neq_tactic.h"
|
||||
#include"lia2pb_tactic.h"
|
||||
#include"fpa2bv_tactic.h"
|
||||
#include"qffpa_tactic.h"
|
||||
#include"pb2bv_tactic.h"
|
||||
#include"recover_01_tactic.h"
|
||||
#include"symmetry_reduce_tactic.h"
|
||||
#include"distribute_forall_tactic.h"
|
||||
#include"reduce_args_tactic.h"
|
||||
#include"bv_size_reduction_tactic.h"
|
||||
#include"propagate_ineqs_tactic.h"
|
||||
#include"cofactor_term_ite_tactic.h"
|
||||
// include"mip_tactic.h"
|
||||
#include"vsubst_tactic.h"
|
||||
#include"sls_tactic.h"
|
||||
#include"probe_arith.h"
|
||||
#include"qflia_tactic.h"
|
||||
#include"qflra_tactic.h"
|
||||
#include"qfnia_tactic.h"
|
||||
#include"qfnra_tactic.h"
|
||||
#include"qfbv_tactic.h"
|
||||
#include"subpaving_tactic.h"
|
||||
#include"unit_subsumption_tactic.h"
|
||||
#include"qfnra_nlsat_tactic.h"
|
||||
#include"ufbv_tactic.h"
|
||||
|
||||
MK_SIMPLE_TACTIC_FACTORY(simplifier_fct, mk_simplify_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(split_clause_fct, mk_split_clause_tactic(p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(normalize_bounds_fct, mk_normalize_bounds_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(elim_uncnstr_fct, mk_elim_uncnstr_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(add_bounds_fct, mk_add_bounds_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(bitblaster_fct, mk_bit_blaster_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(bv1blaster_fct, mk_bv1_blaster_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(aig_fct, mk_aig_tactic(p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(skip_fct, mk_skip_tactic());
|
||||
MK_SIMPLE_TACTIC_FACTORY(fail_fct, mk_fail_tactic());
|
||||
MK_SIMPLE_TACTIC_FACTORY(smt_fct, mk_smt_tactic(p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(sat_fct, mk_sat_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(sat_preprocess_fct, mk_sat_preprocessor_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(ctx_simplify_fct, mk_ctx_simplify_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(ctx_solver_simplify_fct, mk_ctx_solver_simplify_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(unit_subsume_fct, mk_unit_subsumption_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(der_fct, mk_der_tactic(m));
|
||||
MK_SIMPLE_TACTIC_FACTORY(occf_fct, mk_occf_tactic(m));
|
||||
MK_SIMPLE_TACTIC_FACTORY(qe_fct, mk_qe_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(qe_sat_fct, qe::mk_sat_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(propagate_values_fct, mk_propagate_values_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(snf_fct, mk_snf_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(nnf_fct, mk_nnf_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(solve_eqs_fct, mk_solve_eqs_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(max_bv_sharing_fct, mk_max_bv_sharing_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(elim_term_ite_fct, mk_elim_term_ite_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(fix_dl_var_fct, mk_fix_dl_var_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(tseitin_cnf_fct, mk_tseitin_cnf_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(tseitin_cnf_core_fct, mk_tseitin_cnf_core_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(degree_shift_fct, mk_degree_shift_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(purify_arith_fct, mk_purify_arith_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(nlsat_fct, mk_nlsat_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(factor_fct, mk_factor_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(fm_fct, mk_fm_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(fail_if_undecided_fct, mk_fail_if_undecided_tactic());
|
||||
MK_SIMPLE_TACTIC_FACTORY(diff_neq_fct, mk_diff_neq_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(lia2pb_fct, mk_lia2pb_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(fpa2bv_fct, mk_fpa2bv_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(qffpa_fct, mk_qffpa_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(pb2bv_fct, mk_pb2bv_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(recover_01_fct, mk_recover_01_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(elim_and_fct, mk_elim_and_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(symmetry_reduce_fct, mk_symmetry_reduce_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(distribute_forall_fct, mk_distribute_forall_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(reduce_args_fct, mk_reduce_args_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(bv_size_reduction_fct, mk_bv_size_reduction_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(propagate_ineqs_fct, mk_propagate_ineqs_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(cofactor_term_ite_fct, mk_cofactor_term_ite_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(nla2bv_fct, mk_nla2bv_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(vsubst_fct, mk_vsubst_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(qfbv_sls_fct, mk_qfbv_sls_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(subpaving_fct, mk_subpaving_tactic(m, p));
|
||||
|
||||
MK_SIMPLE_TACTIC_FACTORY(qflia_fct, mk_qflia_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(qflra_fct, mk_qflra_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(qfbv_fct, mk_qfbv_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(qfnia_fct, mk_qfnia_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(qfnra_fct, mk_qfnra_tactic(m, p));
|
||||
MK_SIMPLE_TACTIC_FACTORY(ufbv_fct, mk_ufbv_tactic(m, p));
|
||||
|
||||
#define ADD_TACTIC_CMD(NAME, DESCR, FACTORY) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, alloc(FACTORY)))
|
||||
#define ADD_PROBE(NAME, DESCR, PROBE) ctx.insert(alloc(probe_info, symbol(NAME), DESCR, PROBE))
|
||||
|
||||
void install_tactics(tactic_manager & ctx) {
|
||||
|
||||
|
||||
ADD_TACTIC_CMD("ctx-solver-simplify", "apply solver-based contextual simplification rules.", ctx_solver_simplify_fct);
|
||||
ADD_TACTIC_CMD("unit-subsume-simplify", "unit subsumption simplification.", unit_subsume_fct);
|
||||
|
||||
|
||||
ADD_PROBE("memory", "ammount of used memory in megabytes.", mk_memory_probe());
|
||||
ADD_PROBE("depth", "depth of the input goal.", mk_depth_probe());
|
||||
ADD_PROBE("size", "number of assertions in the given goal.", mk_size_probe());
|
||||
ADD_PROBE("num-exprs", "number of expressions/terms in the given goal.", mk_num_exprs_probe());
|
||||
ADD_PROBE("num-consts", "number of non Boolean constants in the given goal.", mk_num_consts_probe());
|
||||
ADD_PROBE("num-bool-consts", "number of Boolean constants in the given goal.", mk_num_bool_consts_probe());
|
||||
ADD_PROBE("num-arith-consts", "number of arithmetic constants in the given goal.", mk_num_arith_consts_probe());
|
||||
ADD_PROBE("num-bv-consts", "number of bit-vector constants in the given goal.", mk_num_bv_consts_probe());
|
||||
ADD_PROBE("produce-proofs", "true if proof generation is enabled for the given goal.", mk_produce_proofs_probe());
|
||||
ADD_PROBE("produce-model", "true if model generation is enabled for the given goal.", mk_produce_models_probe());
|
||||
ADD_PROBE("produce-unsat-cores", "true if unsat-core generation is enabled for the given goal.", mk_produce_unsat_cores_probe());
|
||||
ADD_PROBE("has-patterns", "true if the goal contains quantifiers with patterns.", mk_has_pattern_probe());
|
||||
ADD_PROBE("is-propositional", "true if the goal is in propositional logic.", mk_is_propositional_probe());
|
||||
ADD_PROBE("is-qfbv", "true if the goal is in QF_BV.", mk_is_qfbv_probe());
|
||||
ADD_PROBE("is-qfbv-eq", "true if the goal is in a fragment of QF_BV which uses only =, extract, concat.", mk_is_qfbv_eq_probe());
|
||||
ADD_PROBE("is-qflia", "true if the goal is in QF_LIA.", mk_is_qflia_probe());
|
||||
ADD_PROBE("is-qflra", "true if the goal is in QF_LRA.", mk_is_qflra_probe());
|
||||
ADD_PROBE("is-qflira", "true if the goal is in QF_LIRA.", mk_is_qflira_probe());
|
||||
ADD_PROBE("is-ilp", "true if the goal is ILP.", mk_is_ilp_probe());
|
||||
ADD_PROBE("is-unbounded", "true if the goal contains integer/real constants that do not have lower/upper bounds.", mk_is_unbounded_probe());
|
||||
ADD_PROBE("is-pb", "true if the goal is a pseudo-boolean problem.", mk_is_pb_probe());
|
||||
ADD_PROBE("arith-max-deg", "max polynomial total degree of an arithmetic atom.", mk_arith_max_degree_probe());
|
||||
ADD_PROBE("arith-avg-deg", "avg polynomial total degree of an arithmetic atom.", mk_arith_avg_degree_probe());
|
||||
ADD_PROBE("arith-max-bw", "max coefficient bit width.", mk_arith_max_bw_probe());
|
||||
ADD_PROBE("arith-avg-bw", "avg coefficient bit width.", mk_arith_avg_bw_probe());
|
||||
|
||||
ADD_PROBE("is-qfnia", "true if the goal is in QF_NIA (quantifier-free nonlinear integer arithmetic).", mk_is_qfnia_probe());
|
||||
ADD_PROBE("is-qfnra", "true if the goal is in QF_NRA (quantifier-free nonlinear real arithmetic).", mk_is_qfnra_probe());
|
||||
ADD_PROBE("is-nia", "true if the goal is in NIA (nonlinear integer arithmetic, formula may have quantifiers).", mk_is_nia_probe());
|
||||
ADD_PROBE("is-nra", "true if the goal is in NRA (nonlinear real arithmetic, formula may have quantifiers).", mk_is_nra_probe());
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -1,24 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
install_tactics.h
|
||||
|
||||
Abstract:
|
||||
Install tactics in the SMT 2.0 frontend.
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo (leonardo) 2012-02-19
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef _INSTALL_TACTICS_H_
|
||||
#define _INSTALL_TACTICS_H_
|
||||
|
||||
class tactic_manager;
|
||||
void install_tactics(tactic_manager & ctx);
|
||||
|
||||
#endif
|
||||
|
|
@ -26,5 +26,8 @@ Notes:
|
|||
#include "tactic.h"
|
||||
|
||||
tactic * mk_unit_subsumption_tactic(ast_manager & m, params_ref const & p = params_ref());
|
||||
/*
|
||||
ADD_TACTIC("unit-subsume-simplify", "unit subsumption simplification.", "mk_unit_subsumption_tactic(m, p)")
|
||||
*/
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -32,7 +32,8 @@ probe * mk_is_unbounded_probe();
|
|||
tactic * mk_add_bounds_tactic(ast_manager & m, params_ref const & p = params_ref());
|
||||
|
||||
/*
|
||||
ADD_TACTIC("add-bounds", "add bounds to unbounded variables (under approximation).", "mk_add_bounds_tactic(m, p)")
|
||||
ADD_TACTIC("add-bounds", "add bounds to unbounded variables (under approximation).", "mk_add_bounds_tactic(m, p)")
|
||||
ADD_PROBE("is-unbounded", "true if the goal contains integer/real constants that do not have lower/upper bounds.", "mk_is_unbounded_probe()")
|
||||
*/
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -30,4 +30,8 @@ tactic * mk_pb2bv_tactic(ast_manager & m, params_ref const & p = params_ref());
|
|||
|
||||
probe * mk_is_pb_probe();
|
||||
|
||||
/*
|
||||
ADD_PROBE("is-pb", "true if the goal is a pseudo-boolean problem.", "mk_is_pb_probe()")
|
||||
*/
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -25,15 +25,35 @@ probe * mk_arith_max_bw_probe();
|
|||
probe * mk_arith_avg_degree_probe();
|
||||
probe * mk_arith_max_degree_probe();
|
||||
|
||||
/*
|
||||
ADD_PROBE("arith-max-deg", "max polynomial total degree of an arithmetic atom.", "mk_arith_max_degree_probe()")
|
||||
ADD_PROBE("arith-avg-deg", "avg polynomial total degree of an arithmetic atom.", "mk_arith_avg_degree_probe()")
|
||||
ADD_PROBE("arith-max-bw", "max coefficient bit width.", "mk_arith_max_bw_probe()")
|
||||
ADD_PROBE("arith-avg-bw", "avg coefficient bit width.", "mk_arith_avg_bw_probe()")
|
||||
*/
|
||||
|
||||
probe * mk_is_qflia_probe();
|
||||
probe * mk_is_qflra_probe();
|
||||
probe * mk_is_qflira_probe();
|
||||
probe * mk_is_ilp_probe();
|
||||
probe * mk_is_mip_probe();
|
||||
|
||||
/*
|
||||
ADD_PROBE("is-qflia", "true if the goal is in QF_LIA.", "mk_is_qflia_probe()")
|
||||
ADD_PROBE("is-qflra", "true if the goal is in QF_LRA.", "mk_is_qflra_probe()")
|
||||
ADD_PROBE("is-qflira", "true if the goal is in QF_LIRA.", "mk_is_qflira_probe()")
|
||||
ADD_PROBE("is-ilp", "true if the goal is ILP.", "mk_is_ilp_probe()")
|
||||
*/
|
||||
|
||||
probe * mk_is_qfnia_probe();
|
||||
probe * mk_is_qfnra_probe();
|
||||
probe * mk_is_nia_probe();
|
||||
probe * mk_is_nra_probe();
|
||||
|
||||
/*
|
||||
ADD_PROBE("is-qfnia", "true if the goal is in QF_NIA (quantifier-free nonlinear integer arithmetic).", "mk_is_qfnia_probe()")
|
||||
ADD_PROBE("is-qfnra", "true if the goal is in QF_NRA (quantifier-free nonlinear real arithmetic).", "mk_is_qfnra_probe()")
|
||||
ADD_PROBE("is-nia", "true if the goal is in NIA (nonlinear integer arithmetic, formula may have quantifiers).", "mk_is_nia_probe()")
|
||||
ADD_PROBE("is-nra", "true if the goal is in NRA (nonlinear real arithmetic, formula may have quantifiers).", "mk_is_nra_probe()")
|
||||
*/
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -33,5 +33,6 @@ tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p = params_re
|
|||
probe * mk_is_qfbv_eq_probe();
|
||||
/*
|
||||
ADD_TACTIC("bv1-blast", "reduce bit-vector expressions into bit-vectors of size 1 (notes: only equality, extract and concat are supported).", "mk_bv1_blaster_tactic(m, p)")
|
||||
ADD_PROBE("is-qfbv-eq", "true if the goal is in a fragment of QF_BV which uses only =, extract, concat.", "mk_is_qfbv_eq_probe()")
|
||||
*/
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -55,20 +55,44 @@ public:
|
|||
|
||||
typedef ref<probe> probe_ref;
|
||||
|
||||
probe * mk_const_probe(double val);
|
||||
|
||||
probe * mk_memory_probe();
|
||||
probe * mk_depth_probe();
|
||||
probe * mk_size_probe();
|
||||
|
||||
/*
|
||||
ADD_PROBE("memory", "ammount of used memory in megabytes.", "mk_memory_probe()")
|
||||
ADD_PROBE("depth", "depth of the input goal.", "mk_depth_probe()")
|
||||
ADD_PROBE("size", "number of assertions in the given goal.", "mk_size_probe()")
|
||||
*/
|
||||
|
||||
probe * mk_num_exprs_probe();
|
||||
probe * mk_const_probe(double val);
|
||||
probe * mk_num_consts_probe();
|
||||
probe * mk_num_bool_consts_probe();
|
||||
probe * mk_num_arith_consts_probe();
|
||||
probe * mk_num_bv_consts_probe();
|
||||
|
||||
/*
|
||||
ADD_PROBE("num-exprs", "number of expressions/terms in the given goal.", "mk_num_exprs_probe()")
|
||||
ADD_PROBE("num-consts", "number of non Boolean constants in the given goal.", "mk_num_consts_probe()")
|
||||
ADD_PROBE("num-bool-consts", "number of Boolean constants in the given goal.", "mk_num_bool_consts_probe()")
|
||||
ADD_PROBE("num-arith-consts", "number of arithmetic constants in the given goal.", "mk_num_arith_consts_probe()")
|
||||
ADD_PROBE("num-bv-consts", "number of bit-vector constants in the given goal.", "mk_num_bv_consts_probe()")
|
||||
*/
|
||||
|
||||
probe * mk_produce_proofs_probe();
|
||||
probe * mk_produce_models_probe();
|
||||
probe * mk_produce_unsat_cores_probe();
|
||||
probe * mk_has_pattern_probe();
|
||||
|
||||
/*
|
||||
ADD_PROBE("produce-proofs", "true if proof generation is enabled for the given goal.", "mk_produce_proofs_probe()")
|
||||
ADD_PROBE("produce-model", "true if model generation is enabled for the given goal.", "mk_produce_models_probe()")
|
||||
ADD_PROBE("produce-unsat-cores", "true if unsat-core generation is enabled for the given goal.", "mk_produce_unsat_cores_probe()")
|
||||
ADD_PROBE("has-patterns", "true if the goal contains quantifiers with patterns.", "mk_has_pattern_probe()")
|
||||
*/
|
||||
|
||||
// Some basic combinators for probes
|
||||
probe * mk_not(probe * p1);
|
||||
probe * mk_and(probe * p1, probe * p2);
|
||||
|
|
@ -88,4 +112,9 @@ probe * mk_div(probe * p1, probe * p2);
|
|||
probe * mk_is_propositional_probe();
|
||||
probe * mk_is_qfbv_probe();
|
||||
|
||||
/*
|
||||
ADD_PROBE("is-propositional", "true if the goal is in propositional logic.", "mk_is_propositional_probe()")
|
||||
ADD_PROBE("is-qfbv", "true if the goal is in QF_BV.", "mk_is_qfbv_probe()")
|
||||
*/
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -22,5 +22,8 @@ Notes:
|
|||
#include"tactical.h"
|
||||
|
||||
tactic * mk_ctx_solver_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());
|
||||
/*
|
||||
ADD_TACTIC("ctx-solver-simplify", "apply solver-based contextual simplification rules.", "mk_ctx_solver_simplify_tactic(m, p)")
|
||||
*/
|
||||
|
||||
#endif
|
||||
|
|
|
|||
Loading…
Reference in a new issue