diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-08 02:18:54 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-08 02:19:10 -0500 |
commit | 2ca4e063ca007851ebf73ccb2ac6b7c85e73133d (patch) | |
tree | eb2c18c8cf202c4c05b61f1a1b87cf06c3215b45 /src/theory/quantifiers/ambqi_builder.h | |
parent | fdbc8e0582dfe1addb229d406201a2ec1d513959 (diff) |
Basic optimizations for ambqi : only normalize UF applied to variables, direct handling of NOT
Diffstat (limited to 'src/theory/quantifiers/ambqi_builder.h')
-rwxr-xr-x | src/theory/quantifiers/ambqi_builder.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h index 29cee448b..def074177 100755 --- a/src/theory/quantifiers/ambqi_builder.h +++ b/src/theory/quantifiers/ambqi_builder.h @@ -69,11 +69,14 @@ public: std::map< unsigned, int >& bchildren,
std::map< unsigned, int >& vchildren,
int varChCount );
+ void negate();
Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 );
static bool isSimple( unsigned n );
static unsigned getId( unsigned n, unsigned start=0 );
Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args );
Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 );
+ //for debugging
+ bool is_normalized();
};
class AbsMbqiBuilder : public QModelBuilder
|