Use Y2 backend for all abstract queries

Set Yices as the backend for all abstract queries

Note that bt and m5 backends for abstract queries were only experimental (disabled)

Now flags BACKEND_* only configures bitvector solver

Refs: #15, #16

src/reach/reach_backend.h

@@ -26,66 +26,33 @@
 /// Configurations
 /// Note: Only one of the below flag should be enabled
 
-#define BACKEND_Y2			// Yices 2 for all queries
-// #define BACKEND_HYBRID	// hybrid config
-// #define BACKEND_BT		// Boolector for all queries
-// #define BACKEND_Z3		// Z3 for all queries
-// #define BACKEND_M5		// MathSAT 5 for all queries
+#define BACKEND_Y2		// Yices 2 for all queries
+// #define BACKEND_BT		// Yices 2 for abstract, Boolector for bv queries
+// #define BACKEND_M5		// Yices 2 for abstract, MathSAT 5 for bv queries
+
+// Use Y2 backend for all abstract queries
+#define SOLVER_CTI		  y2_API		// Solver for checking SAT_abstract ? [ F[top] ^ P ^ T ^ !P+ ]
+#define SOLVER_REACH	  y2_API		// Solver for checking SAT_abstract ? [ F[k-1] ^ P ^ T ^ C+ ] and for Fast-forward check
+#define SOLVER_CONTAIN	  y2_API		// Solver for checking if frame restriction global
+#define SOLVER_AB		  y2_API		// Solver for all other abstract queries: Basis check, Lemma redundancy check
+#define SOLVER_CORE       y2_API		// Solver for getting unsat core
+#define SOLVER_MUS		  y2_API		// Solver for getting minimal unsat core
 
 /// Config: BACKEND_Y2
 #ifdef BACKEND_Y2
-	#define SOLVER_CTI		  y2_API		// Solver for checking SAT_abstract ? [ F[top] ^ P ^ T ^ !P+ ]
-	#define SOLVER_REACH	  y2_API		// Solver for checking SAT_abstract ? [ F[k-1] ^ P ^ T ^ C+ ] and for Fast-forward check
-	#define SOLVER_CONTAIN	  y2_API		// Solver for checking if frame restriction global
-	#define SOLVER_AB		  y2_API		// Solver for all other abstract queries: Basis check, Lemma redundancy check
-	#define SOLVER_CORE       y2_API		// Solver for getting unsat core
-	#define SOLVER_MUS		  y2_API		// Solver for getting minimal unsat core
-	#define SOLVER_BV         y2_API		// Solver for concrete / bit-vector queries
-#endif
-
-/// Config: BACKEND_HYBRID
-#ifdef BACKEND_HYBRID
-	#define SOLVER_CTI		  y2_API
-	#define SOLVER_REACH	  y2_API
-	#define SOLVER_CONTAIN	  y2_API
-	#define SOLVER_AB		  y2_API
-    #define SOLVER_CORE       y2_API
-	#define SOLVER_MUS		  y2_API
-	#define SOLVER_BV         bt_API
+	#define SOLVER_BV         y2_API	// Solver for concrete / bit-vector queries
 #endif
 
 /// Config: BACKEND_BT
 #ifdef BACKEND_BT
-	#define SOLVER_CTI		  bt_API
-	#define SOLVER_REACH	  bt_API
-	#define SOLVER_CONTAIN	  bt_API
-	#define SOLVER_AB		  bt_API
-    #define SOLVER_CORE       bt_API
-	#define SOLVER_MUS		  bt_API
-    #define SOLVER_BV         bt_API
+    #define SOLVER_BV         bt_API	// Solver for concrete / bit-vector queries
 #endif
 
 /// Config: BACKEND_M5
 #ifdef BACKEND_M5
-	#define SOLVER_CTI		  m5_API
-	#define SOLVER_REACH	  m5_API
-	#define SOLVER_CONTAIN	  m5_API
-	#define SOLVER_AB		  m5_API
-    #define SOLVER_CORE       m5_API
-	#define SOLVER_MUS		  m5_API
-    #define SOLVER_BV         m5_API
+    #define SOLVER_BV         m5_API	// Solver for concrete / bit-vector queries
 #endif
 
-/// Config: BACKEND_Z3
-#ifdef BACKEND_Z3
-	#define SOLVER_CTI		z3_API
-	#define SOLVER_REACH	z3_API
-	#define SOLVER_CONTAIN	z3_API
-	#define SOLVER_AB		z3_API
-    #define SOLVER_CORE     z3_API
-	#define SOLVER_MUS		z3_API
-	#define SOLVER_BV		z3_API
-#endif
 
 #define MICRO_ALARM
 

src/reach/reach_y2.cpp

@@ -88,8 +88,10 @@ void y2_API::y2_unset()
 	m_func_decs.clear();
 	m_num_to_const.clear();
 
+#ifdef ASSERT_DISTINCT_NUMBERS
 	m_distinct_constraints.second.clear();
 	m_distinct_constraints = make_pair(-1, y2_expr_vec());
+#endif
 
 	g_ctx = NULL;
 

xtras/issue15.btor2

@@ -0,0 +1,24 @@
+; source: https://github.com/aman-goel/avr/tree/92362931700b66684418a991d018c9fbdbebc06f/tests
+; BTOR description generated by Yosys 0.9+431 (git sha1 4a3b5437, clang 4.0.1-6 -fPIC -Os) for module main.
+1 sort bitvec 1
+2 input 1 clk
+3 input 1 en
+4 sort bitvec 4
+5 const 4 0001
+6 state 4 X
+7 init 4 6 5
+8 const 4 1111
+9 neq 1 6 8
+10 not 1 9
+11 output 10 prop_neg
+12 const 1 1
+13 not 1 9
+14 and 1 12 13
+15 bad 14
+16 uext 1 9 0 prop
+17 add 4 6 5
+18 eq 1 6 8
+19 ite 4 18 5 17
+20 ite 4 3 19 6
+21 next 4 6 20
+; end of yosys output