Added support for proof production in Equality Engine. Cleaned up existing proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup.

1 files changed, 16 insertions, 0 deletions

diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index edf9c78fe..7c4cb3651 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -55,6 +55,22 @@ typedef enum {
   AXIOM_INST_MODE_PRIORITY,
 } AxiomInstMode;
 
+typedef enum {
+  /** default, mbqi from CADE 24 paper */
+  MBQI_DEFAULT,
+  /** no mbqi */
+  MBQI_NONE,
+  /** implementation that mimics inst-gen */
+  MBQI_INST_GEN,
+  /** mbqi from Section 5.4.2 of AJR thesis */
+  MBQI_FMC,
+  /** mbqi with integer intervals */
+  //MBQI_FMC_INTERVAL,
+  /** mbqi with interval abstraction of uninterpreted sorts */
+  MBQI_INTERVAL,
+} MbqiMode;
+
+
 
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */