mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

Added tactic for qfnra purely based on nlsat

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-12 17:34:23 -07:00
parent 5c0d82d555
commit 6145ccc077
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
lib/install_tactics.cpp
View file

@ -70,6 +70,7 @@ Notes:
#include"qfbv_tactic.h"
#include"subpaving_tactic.h"
#include"unit_subsumption_tactic.h"
#include"qfnra_nlsat_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));
@ -193,6 +194,7 @@ void install_tactics(tactic_manager & ctx) {
ADD_TACTIC_CMD("qflra", "builtin strategy for solving QF_LRA problems.", qflra_fct);
ADD_TACTIC_CMD("qfnia", "builtin strategy for solving QF_NIA problems.", qfnia_fct);
ADD_TACTIC_CMD("qfnra", "builtin strategy for solving QF_NRA problems.", qfnra_fct);
ADD_TACTIC_CMD("qfnra-nlsat", "builtin strategy for solving QF_NRA problems using only nlsat.", qfnra_nlsat_fct);
ADD_TACTIC_CMD("qfbv", "builtin strategy for solving QF_BV problems.", qfbv_fct);
#ifndef _EXTERNAL_RELEASE
ADD_TACTIC_CMD("subpaving", "tactic for testing subpaving module.", subpaving_fct);