Basic optimizations for ambqi : only normalize UF applied to variables, direct handling of NOT

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