mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-10 01:05:47 +00:00
Code Activity

Fixed bugs in static features and smt setup

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-02-08 16:53:08 +00:00
parent 72345026be
commit 4792c5fb7c
3 changed files with 21 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/static_features.h
View file

@ -22,6 +22,7 @@ Revision History:
#include"ast.h"
#include"arith_decl_plugin.h"
#include"bv_decl_plugin.h"
#include"array_decl_plugin.h"
#include"fpa_decl_plugin.h"
#include"map.h"
@ -29,6 +30,7 @@ struct static_features {
ast_manager & m_manager;
arith_util m_autil;
bv_util m_bvutil;
array_util m_arrayutil;
fpa_util m_fpautil;
family_id m_bfid;
family_id m_afid;
@ -72,8 +74,9 @@ struct static_features {
bool m_has_rational; //
bool m_has_int; //
bool m_has_real; //
bool m_has_bv; //
bool m_has_fpa; //
bool m_has_bv; //
bool m_has_fpa; //
bool m_has_arrays; //
rational m_arith_k_sum; // sum of the numerals in arith atoms.
unsigned m_num_arith_terms;
unsigned m_num_arith_eqs; // equalities of the form t = k where k is a numeral